author nipkow Sat, 11 May 2019 15:40:08 +0200 changeset 70263 805250bb7363 parent 70262 e12779b8f5b6 child 70264 ad0306b89cfb
fixed theory name
```--- a/src/HOL/Data_Structures/Trie_Map.thy	Sat May 11 15:27:11 2019 +0200
+++ b/src/HOL/Data_Structures/Trie_Map.thy	Sat May 11 15:40:08 2019 +0200
@@ -51,22 +51,22 @@
text \<open>Proof by stepwise refinement. First abstract to type @{typ "'a trie"}.\<close>

fun abs :: "'a::linorder trie_map \<Rightarrow> 'a trie" where
-"abs (Nd b t) = Trie_Fun0.Nd b (\<lambda>a. map_option abs (lookup t a))"
+"abs (Nd b t) = Trie_Fun.Nd b (\<lambda>a. map_option abs (lookup t a))"

fun invar :: "('a::linorder)trie_map \<Rightarrow> bool" where
"invar (Nd b m) = (M.invar m \<and> (\<forall>a t. lookup m a = Some t \<longrightarrow> invar t))"

-lemma isin_abs: "isin t xs = Trie_Fun0.isin (abs t) xs"
+lemma isin_abs: "isin t xs = Trie_Fun.isin (abs t) xs"
apply(induction t xs rule: isin.induct)
apply(auto split: option.split)
done

-lemma abs_insert: "invar t \<Longrightarrow> abs(insert xs t) = Trie_Fun0.insert xs (abs t)"
+lemma abs_insert: "invar t \<Longrightarrow> abs(insert xs t) = Trie_Fun.insert xs (abs t)"
apply(induction xs t rule: insert.induct)
apply(auto simp: M.map_specs RBT_Set.empty_def[symmetric] split: option.split)
done

-lemma abs_delete: "invar t \<Longrightarrow> abs(delete xs t) = Trie_Fun0.delete xs (abs t)"
+lemma abs_delete: "invar t \<Longrightarrow> abs(delete xs t) = Trie_Fun.delete xs (abs t)"
apply(induction xs t rule: delete.induct)
apply(auto simp: M.map_specs split: option.split)
done```