Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Homework 4

This is the task corresponding to homework 4.

## Resources

### Definitions File

```theory Defs
imports "HOL-Library.Tree"
begin

declare Let_def [simp]
declare [[names_short]]

type_synonym 'a ptree = "(nat * 'a) tree"

consts set_ptree :: "('a::linorder) ptree \<Rightarrow> 'a set"

consts pbst :: "'a::linorder ptree \<Rightarrow> bool"

consts pins :: "(nat * 'a::linorder) \<Rightarrow> 'a ptree \<Rightarrow> 'a ptree"

consts pisin :: "'a::linorder \<Rightarrow> 'a ptree \<Rightarrow> ('a ptree * nat)"

consts reorder :: "('a::linorder) ptree \<Rightarrow> 'a ptree"

end```

### Template File

```theory Submission
imports Defs
begin

fun set_ptree :: "('a::linorder) ptree \<Rightarrow> 'a set"  where
"set_ptree _ = undefined"

lemma set_ptree: "set_ptree t = snd ` set_tree t"
sorry

fun pbst :: "'a::linorder ptree \<Rightarrow> bool"  where
"pbst _ = undefined"

fun pins :: "(nat * 'a::linorder) \<Rightarrow> 'a ptree \<Rightarrow> 'a ptree"  where
"pins _ = undefined"

lemma pins_invar: "pbst t \<Longrightarrow> pbst (pins x t)"
sorry

fun pisin :: "'a::linorder \<Rightarrow> 'a ptree \<Rightarrow> ('a ptree * nat)"  where
"pisin _ = undefined"

lemma pisin_set: "pbst t \<Longrightarrow> set_ptree (fst (pisin x t)) = set_ptree t"
sorry

lemma pisin_invar: "pbst t \<Longrightarrow> pbst (fst (pisin x t))"
sorry

lemma pisin_inc: "pbst t \<Longrightarrow> (n,x) \<in> set_tree t \<Longrightarrow> (Suc n,x) \<in> set_tree (fst (pisin x t))"
sorry

term "sort"

definition reorder :: "('a::linorder) ptree \<Rightarrow> 'a ptree"  where
"reorder _ = undefined"

theorem reorder_pbst: "pbst t \<Longrightarrow> pbst (reorder t)"
sorry

theorem reorder_pset: "pbst t \<Longrightarrow> set_ptree (reorder t) = set_ptree t"
sorry

theorem reorder_set: "pbst t \<Longrightarrow> set_tree (reorder t) = set_tree t"
sorry

end```

### Check File

```theory Check
imports Submission
begin

lemma set_ptree: "set_ptree t = snd ` set_tree t"
by (rule Submission.set_ptree)

lemma pins_invar: "pbst t \<Longrightarrow> pbst (pins x t)"
by (rule Submission.pins_invar)

lemma pisin_set: "pbst t \<Longrightarrow> set_ptree (fst (pisin x t)) = set_ptree t"
by (rule Submission.pisin_set)

lemma pisin_invar: "pbst t \<Longrightarrow> pbst (fst (pisin x t))"
by (rule Submission.pisin_invar)

lemma pisin_inc: "pbst t \<Longrightarrow> (n,x) \<in> set_tree t \<Longrightarrow> (Suc n,x) \<in> set_tree (fst (pisin x t))"
by (rule Submission.pisin_inc)

theorem reorder_pbst: "pbst t \<Longrightarrow> pbst (reorder t)"
by (rule Submission.reorder_pbst)

theorem reorder_pset: "pbst t \<Longrightarrow> set_ptree (reorder t) = set_ptree t"
by (rule Submission.reorder_pset)

theorem reorder_set: "pbst t \<Longrightarrow> set_tree (reorder t) = set_tree t"
by (rule Submission.reorder_set)

end```

Terms and Conditions