49 subsection "Correctness" |
49 subsection "Correctness" |
50 |
50 |
51 text \<open>Proof by stepwise refinement. First abstract to type @{typ "'a trie"}.\<close> |
51 text \<open>Proof by stepwise refinement. First abstract to type @{typ "'a trie"}.\<close> |
52 |
52 |
53 fun abs :: "'a::linorder trie_map \<Rightarrow> 'a trie" where |
53 fun abs :: "'a::linorder trie_map \<Rightarrow> 'a trie" where |
54 "abs (Nd b t) = Trie_Fun0.Nd b (\<lambda>a. map_option abs (lookup t a))" |
54 "abs (Nd b t) = Trie_Fun.Nd b (\<lambda>a. map_option abs (lookup t a))" |
55 |
55 |
56 fun invar :: "('a::linorder)trie_map \<Rightarrow> bool" where |
56 fun invar :: "('a::linorder)trie_map \<Rightarrow> bool" where |
57 "invar (Nd b m) = (M.invar m \<and> (\<forall>a t. lookup m a = Some t \<longrightarrow> invar t))" |
57 "invar (Nd b m) = (M.invar m \<and> (\<forall>a t. lookup m a = Some t \<longrightarrow> invar t))" |
58 |
58 |
59 lemma isin_abs: "isin t xs = Trie_Fun0.isin (abs t) xs" |
59 lemma isin_abs: "isin t xs = Trie_Fun.isin (abs t) xs" |
60 apply(induction t xs rule: isin.induct) |
60 apply(induction t xs rule: isin.induct) |
61 apply(auto split: option.split) |
61 apply(auto split: option.split) |
62 done |
62 done |
63 |
63 |
64 lemma abs_insert: "invar t \<Longrightarrow> abs(insert xs t) = Trie_Fun0.insert xs (abs t)" |
64 lemma abs_insert: "invar t \<Longrightarrow> abs(insert xs t) = Trie_Fun.insert xs (abs t)" |
65 apply(induction xs t rule: insert.induct) |
65 apply(induction xs t rule: insert.induct) |
66 apply(auto simp: M.map_specs RBT_Set.empty_def[symmetric] split: option.split) |
66 apply(auto simp: M.map_specs RBT_Set.empty_def[symmetric] split: option.split) |
67 done |
67 done |
68 |
68 |
69 lemma abs_delete: "invar t \<Longrightarrow> abs(delete xs t) = Trie_Fun0.delete xs (abs t)" |
69 lemma abs_delete: "invar t \<Longrightarrow> abs(delete xs t) = Trie_Fun.delete xs (abs t)" |
70 apply(induction xs t rule: delete.induct) |
70 apply(induction xs t rule: delete.induct) |
71 apply(auto simp: M.map_specs split: option.split) |
71 apply(auto simp: M.map_specs split: option.split) |
72 done |
72 done |
73 |
73 |
74 lemma invar_insert: "invar t \<Longrightarrow> invar (insert xs t)" |
74 lemma invar_insert: "invar t \<Longrightarrow> invar (insert xs t)" |