I agree 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.
theory Defs imports "~~/src/HOL/Library/Tree" "~~/src/HOL/Data_Structures/Map_Specs" begin datatype direction = L | R type_synonym path = "direction list" end
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
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