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 "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
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
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