Cookies disclaimer

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.

FDS Week 3 homework

Week 3 homework

Resources

Download Files

Definitions File

```theory Defs
imports "~~/src/HOL/Library/Tree" "~~/src/HOL/Data_Structures/Map_Specs"
begin

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

end```

Template File

```theory Submission
imports Defs
begin

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

value "valid (Node Leaf (1::nat) Leaf) [L,R] = False"

value "valid (Node Leaf (1::nat) Leaf) [L,R] = False"

value "valid (Node (Node Leaf 3 Leaf) (1::nat) Leaf) [L,R] = True"

value "valid (Node (Node Leaf 3 Leaf) (1::nat) Leaf) [L,R,L] = False"

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

value "delete_subtree (Node (Node Leaf 3 (Node Leaf 2 Leaf)) (1::nat) Leaf) [L] = Node Leaf 1 Leaf"

value "delete_subtree (Node (Node Leaf 3 (Node Leaf 2 Leaf)) (1::nat) Leaf) [L,R] = Node (Node Leaf 3 Leaf) 1 Leaf"

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"

value "get (Node (Node Leaf 3 (Node Leaf 2 Leaf)) (1::nat) Leaf) [L] = Node Leaf 3 (Node Leaf 2 Leaf)"

value "get (Node (Node Leaf 3 (Node Leaf 2 Leaf)) (1::nat) Leaf) [L,R] = Node Leaf 2 Leaf"

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

value "put (Node (Node Leaf 3 (Node Leaf 2 Leaf)) (1::nat) Leaf) [L] (Node Leaf 3 (Node Leaf 2 Leaf)) =
Node (Node Leaf 3 (Node Leaf 2 Leaf)) 1 Leaf"

value "put (Node Leaf (2::nat) Leaf) [L] (Node Leaf 1 Leaf) = Node (Node Leaf 1 Leaf) 2 Leaf"

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

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

value "map_update (2::nat) 4 (Node Leaf (2,3::nat) Leaf) = (Node Leaf (2,4::nat) Leaf)"

value "map_update (3::nat) 4 (Node Leaf (2,3::nat) Leaf) = (Node Leaf (2,3::nat) (Node Leaf (3,4) Leaf))"

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"

value "map_lookup (Node Leaf (2,3::nat) Leaf) (1::nat) = None"

value "map_lookup (Node (Node Leaf (1,2) Leaf) (2,3::nat) Leaf) (1::nat) = Some 2"

value "map_lookup (Node (Node Leaf (1,2) (Node Leaf (4,5) Leaf)) (2,3::nat) Leaf) (6::nat) = None"

value "map_lookup (Node (Node Leaf (1,2) (Node Leaf (2,5) Leaf)) (3,3::nat) Leaf) (2::nat) = Some 5"

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"

value "map_delete (2::nat) (Node Leaf (2,3::nat) Leaf) = Leaf"

value "map_delete (3::nat) (Node Leaf (2,3::nat) Leaf) = (Node Leaf (2,3::nat) Leaf)"

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: "¬valid t p ⟹ 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 ⟹ delete_subtree (delete_subtree t p) p = delete_subtree t p"
by (rule Submission.delete_delete)

lemma delete_replaces_with_leaf: "valid t p ⟹ get (delete_subtree t p) p = Leaf"
by (rule Submission.delete_replaces_with_leaf)

lemma valid_delete:
"valid t p ⟹ valid (delete_subtree t p) p"
by (rule Submission.valid_delete)

lemma valid_append: "valid t (p@q) ⟷ valid t p ∧ valid (get t p) q"
by(rule Submission.valid_append)

lemma put_delete_get_append:
"valid t (p@q) ⟹ 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) ⟹ 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) ⟹ map_lookup t x = map_of (inorder t) x"
by(rule Submission.lookup_map_of)

lemma inorder_update:
"sorted1(inorder t) ⟹ inorder(map_update a b t) = upd_list a b (inorder t)"
by(rule Submission.inorder_update)

lemma inorder_delete:
"sorted1(inorder t) ⟹ inorder(map_delete x t) = del_list x (inorder t)"
supply[[unify_trace_failure]]
by (rule Submission.inorder_delete)

end```

Terms and Conditions