Homework 3

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