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 3

This is the task corresponding to homework 3.

## Resources

### Definitions File

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

declare Let_def [simp]

fun split_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
"split_min (Node l a r) =
(if l = Leaf then (a,r)
else let (x,l') = split_min l
in (x, Node l' a r))"

datatype direction = L | R
type_synonym path = "direction list"

consts valid :: "'a tree \<Rightarrow> path \<Rightarrow> bool"

consts delete_subtree :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree"

consts get :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree"

consts put :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree \<Rightarrow> 'a tree"

consts map_lookup :: "('a::linorder*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option"

consts map_update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree"

consts map_delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree"

end```

### Template File

```theory Submission
imports Defs
begin

fun valid :: "'a tree \<Rightarrow> path \<Rightarrow> bool"  where
"valid _ = undefined"

fun delete_subtree :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree"  where
"delete_subtree _ = undefined"

lemma delete_subtree_invalid: "\<not>valid t p \<Longrightarrow> delete_subtree t p = t"
sorry

fun get :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree"  where
"get _ = undefined"

fun put :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree \<Rightarrow> 'a tree"  where
"put _ = undefined"

lemma put_in_delete: "put (delete_subtree t p) p (get t p) = t"
sorry

lemma delete_delete: "valid t p \<Longrightarrow> delete_subtree (delete_subtree t p) p = delete_subtree t p"
sorry

lemma delete_replaces_with_leaf[simp]: "valid t p \<Longrightarrow> get (delete_subtree t p) p = Leaf"
sorry

lemma valid_delete: "valid t p \<Longrightarrow> valid (delete_subtree t p) p"
sorry

lemma valid_append: "valid t (p@q) \<longleftrightarrow> valid t p \<and> valid (get t p) q"
sorry

lemma put_delete_get_append:
"valid t (p@q) \<Longrightarrow> delete_subtree t (p@q) = put t p (delete_subtree (get t p) q) "
sorry

lemma put_get_append:
"valid t (p@q) \<Longrightarrow> get (put t (p@q) s) p = put (get t p) q s"
sorry

thm map_of.simps upd_list.simps del_list.simps

thm del_list_simps
thm upd_list_simps
thm map_of_simps

fun map_lookup :: "('a::linorder*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option"  where
"map_lookup _ = undefined"

lemma lookup_map_of:
"sorted1(inorder t) \<Longrightarrow> map_lookup t x = map_of (inorder t) x"
sorry

fun map_update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree"  where
"map_update _ = undefined"

lemma inorder_update:
"sorted1(inorder t) \<Longrightarrow> inorder(map_update a b t) = upd_list a b (inorder t)"
sorry

fun map_delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree"  where
"map_delete _ = undefined"

lemma inorder_delete:
"sorted1(inorder t) \<Longrightarrow> inorder(map_delete x t) = del_list x (inorder t)"
sorry

end```

### Check File

```theory Check
imports Submission
begin

lemma delete_subtree_invalid: "\<not>valid t p \<Longrightarrow> delete_subtree t p = t"
by (rule Submission.delete_subtree_invalid)

lemma put_in_delete: "put (delete_subtree t p) p (get t p) = t"
by (rule Submission.put_in_delete)

lemma delete_delete: "valid t p \<Longrightarrow> delete_subtree (delete_subtree t p) p = delete_subtree t p"
by (rule Submission.delete_delete)

lemma delete_replaces_with_leaf: "valid t p \<Longrightarrow> get (delete_subtree t p) p = Leaf"
by (rule Submission.delete_replaces_with_leaf)

lemma valid_delete: "valid t p \<Longrightarrow> valid (delete_subtree t p) p"
by (rule Submission.valid_delete)

lemma valid_append: "valid t (p@q) \<longleftrightarrow> valid t p \<and> valid (get t p) q"
by (rule Submission.valid_append)

lemma put_delete_get_append: "valid t (p@q) \<Longrightarrow> delete_subtree t (p@q) = put t p (delete_subtree (get t p) q) "
by (rule Submission.put_delete_get_append)

lemma put_get_append: "valid t (p@q) \<Longrightarrow> get (put t (p@q) s) p = put (get t p) q s"
by (rule Submission.put_get_append)

lemma lookup_map_of: "sorted1(inorder t) \<Longrightarrow> map_lookup t x = map_of (inorder t) x"
by (rule Submission.lookup_map_of)

lemma inorder_update: "sorted1(inorder t) \<Longrightarrow> inorder(map_update a b t) = upd_list a b (inorder t)"
by (rule Submission.inorder_update)

lemma inorder_delete: "sorted1(inorder t) \<Longrightarrow> inorder(map_delete x t) = del_list x (inorder t)"
by (rule Submission.inorder_delete)

end```

Terms and Conditions