src/HOL/Data_Structures/Tries_Binary.thy

--- a/src/HOL/Data_Structures/Tries_Binary.thy	Sat May 11 22:19:28 2019 +0200
+++ b/src/HOL/Data_Structures/Tries_Binary.thy	Sun May 12 20:15:28 2019 +0200
@@ -21,6 +21,9 @@
 
 datatype trie = Lf | Nd bool "trie * trie"
 
+definition empty :: trie where
+[simp]: "empty = Lf"
+
 fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool" where
 "isin Lf ks = False" |
 "isin (Nd b lr) ks =
@@ -34,8 +37,8 @@
 "insert (k#ks) Lf = Nd False (mod2 (insert ks) k (Lf,Lf))" |
 "insert (k#ks) (Nd b lr) = Nd b (mod2 (insert ks) k lr)"
 
-lemma isin_insert: "isin (insert as t) bs = (as = bs \<or> isin t bs)"
-apply(induction as t arbitrary: bs rule: insert.induct)
+lemma isin_insert: "isin (insert xs t) ys = (xs = ys \<or> isin t ys)"
+apply(induction xs t arbitrary: ys rule: insert.induct)
 apply (auto split: list.splits if_splits)
 done
 
@@ -65,8 +68,8 @@
       [] \<Rightarrow> node False lr |
       k#ks' \<Rightarrow> node b (mod2 (delete ks') k lr))"
 
-lemma isin_delete: "isin (delete as t) bs = (as \<noteq> bs \<and> isin t bs)"
-apply(induction as t arbitrary: bs rule: delete.induct)
+lemma isin_delete: "isin (delete xs t) ys = (xs \<noteq> ys \<and> isin t ys)"
+apply(induction xs t arbitrary: ys rule: delete.induct)
  apply simp
 apply (auto split: list.splits if_splits)
   apply (metis isin.simps(1))
@@ -76,20 +79,29 @@
 definition set_trie :: "trie \<Rightarrow> bool list set" where
 "set_trie t = {xs. isin t xs}"
 
+lemma set_trie_empty: "set_trie empty = {}"
+by(simp add: set_trie_def)
+
+lemma set_trie_isin: "isin t xs = (xs \<in> set_trie t)"
+by(simp add: set_trie_def)
+
 lemma set_trie_insert: "set_trie(insert xs t) = set_trie t \<union> {xs}"
 by(auto simp add: isin_insert set_trie_def)
 
+lemma set_trie_delete: "set_trie(delete xs t) = set_trie t - {xs}"
+by(auto simp add: isin_delete set_trie_def)
+
 interpretation S: Set
-where empty = Lf and isin = isin and insert = insert and delete = delete
+where empty = empty and isin = isin and insert = insert and delete = delete
 and set = set_trie and invar = "\<lambda>t. True"
 proof (standard, goal_cases)
-  case 1 show ?case by (simp add: set_trie_def)
+  case 1 show ?case by (rule set_trie_empty)
 next
-  case 2 thus ?case by(simp add: set_trie_def)
+  case 2 show ?case by(rule set_trie_isin)
 next
   case 3 thus ?case by(auto simp: set_trie_insert)
 next
-  case 4 thus ?case by(auto simp: isin_delete set_trie_def)
+  case 4 show ?case by(rule set_trie_delete)
 qed (rule TrueI)+