27 shows "lookup t a = Some b \<Longrightarrow> size b < Suc (size_tree (\<lambda>ab. Suc (size (snd ab))) (\<lambda>x. 0) t)" |
27 shows "lookup t a = Some b \<Longrightarrow> size b < Suc (size_tree (\<lambda>ab. Suc (size (snd ab))) (\<lambda>x. 0) t)" |
28 apply(induction t a rule: lookup.induct) |
28 apply(induction t a rule: lookup.induct) |
29 apply(auto split: if_splits) |
29 apply(auto split: if_splits) |
30 done |
30 done |
31 |
31 |
|
32 |
|
33 definition empty :: "'a trie_map" where |
|
34 [simp]: "empty = Nd False Leaf" |
|
35 |
32 fun isin :: "('a::linorder) trie_map \<Rightarrow> 'a list \<Rightarrow> bool" where |
36 fun isin :: "('a::linorder) trie_map \<Rightarrow> 'a list \<Rightarrow> bool" where |
33 "isin (Nd b m) [] = b" | |
37 "isin (Nd b m) [] = b" | |
34 "isin (Nd b m) (x # xs) = (case lookup m x of None \<Rightarrow> False | Some t \<Rightarrow> isin t xs)" |
38 "isin (Nd b m) (x # xs) = (case lookup m x of None \<Rightarrow> False | Some t \<Rightarrow> isin t xs)" |
35 |
39 |
36 fun insert :: "('a::linorder) list \<Rightarrow> 'a trie_map \<Rightarrow> 'a trie_map" where |
40 fun insert :: "('a::linorder) list \<Rightarrow> 'a trie_map \<Rightarrow> 'a trie_map" where |
37 "insert [] (Nd b m) = Nd True m" | |
41 "insert [] (Nd b m) = Nd True m" | |
38 "insert (x#xs) (Nd b m) = |
42 "insert (x#xs) (Nd b m) = |
39 Nd b (update x (insert xs (case lookup m x of None \<Rightarrow> Nd False Leaf | Some t \<Rightarrow> t)) m)" |
43 Nd b (update x (insert xs (case lookup m x of None \<Rightarrow> empty | Some t \<Rightarrow> t)) m)" |
40 |
44 |
41 fun delete :: "('a::linorder) list \<Rightarrow> 'a trie_map \<Rightarrow> 'a trie_map" where |
45 fun delete :: "('a::linorder) list \<Rightarrow> 'a trie_map \<Rightarrow> 'a trie_map" where |
42 "delete [] (Nd b m) = Nd False m" | |
46 "delete [] (Nd b m) = Nd False m" | |
43 "delete (x#xs) (Nd b m) = Nd b |
47 "delete (x#xs) (Nd b m) = Nd b |
44 (case lookup m x of |
48 (case lookup m x of |
82 done |
86 done |
83 |
87 |
84 text \<open>Overall correctness w.r.t. the \<open>Set\<close> ADT:\<close> |
88 text \<open>Overall correctness w.r.t. the \<open>Set\<close> ADT:\<close> |
85 |
89 |
86 interpretation S2: Set |
90 interpretation S2: Set |
87 where empty = "Nd False Leaf" and isin = isin and insert = insert and delete = delete |
91 where empty = empty and isin = isin and insert = insert and delete = delete |
88 and set = "set o abs" and invar = invar |
92 and set = "set o abs" and invar = invar |
89 proof (standard, goal_cases) |
93 proof (standard, goal_cases) |
90 case 1 show ?case by (simp) |
94 case 1 show ?case by (simp) |
91 next |
95 next |
92 case 2 thus ?case by (simp add: isin_set isin_abs) |
96 case 2 thus ?case by (simp add: isin_set isin_abs) |