theory Ex10_Tut imports "HOL-Data_Structures.Tree23_Map" "HOL-Data_Structures.Tries_Binary" begin fun union :: "trie \ trie \ trie" where "union _ = undefined" lemma "isin (union a b) x = isin a x \ isin b x" sorry datatype 'a trie = Leaf | Node bool "'a \ 'a trie" fun isin :: "'a trie \ 'a list \ bool" where "isin _ = undefined" fun ins :: "'a list \ 'a trie \ 'a trie" where "ins _ = undefined" lemma ins_correct: "isin (ins as t) bs = (as=bs \ isin t bs)" sorry fun delete :: "'a list \ 'a trie \ 'a trie" where "delete _ = undefined" lemma delete_correct: "isin (delete as t) bs = (as \ bs \ isin t bs)" sorry abbreviation "empty23 \ Tree23.Leaf" abbreviation "inv23 t \ complete t \ sorted1 (inorder t)" datatype 'a trie' = Leaf' | Node' bool "('a\'a trie') tree23" lemma lookup_size_aux[termination_simp]: "lookup m k = Some v \ size (v::'a trie') < Suc (size_tree23 (\x. Suc (size (snd x))) m)" sorry fun trie'_inv :: "'a::linorder trie' \ bool" where "trie'_inv _ = undefined" fun trie'_\ :: "'a::linorder trie' \ 'a trie" where "trie'_\ _ = undefined" fun isin' :: "'a::linorder trie' \ 'a list \ bool" where "isin' _ = undefined" fun ins' :: "'a::linorder list \ 'a trie' \ 'a trie'" where "ins' _ = undefined" fun delete' :: "'a::linorder list \ 'a trie' \ 'a trie'" where "delete' _ = undefined" lemmas map23_thms[simp] = M.map_empty Tree23_Map.M.map_update Tree23_Map.M.map_delete Tree23_Map.M.invar_empty Tree23_Map.M.invar_update Tree23_Map.M.invar_delete M.invar_def M.inorder_update M.inorder_inv_update sorted_upd_list lemma ins'_correct: "trie'_inv t \ (isin' (ins' xs t) ks \ xs=ks \ isin' t ks) \ trie'_inv (ins' xs t)" sorry lemma delete'_correct: "trie'_inv t \ (isin' (delete' xs t) ks \ xs\ks \ isin' t ks) \ trie'_inv (delete' xs t)" sorry end