FDS Week 3 homework

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