tuned
authornipkow
Sun May 12 20:15:28 2019 +0200 (5 weeks ago)
changeset 702679fa2cf7142b7
parent 70266 0b813a1a833f
child 70268 81403d7b9038
tuned
src/HOL/Data_Structures/Tries_Binary.thy
     1.1 --- a/src/HOL/Data_Structures/Tries_Binary.thy	Sat May 11 22:19:28 2019 +0200
     1.2 +++ b/src/HOL/Data_Structures/Tries_Binary.thy	Sun May 12 20:15:28 2019 +0200
     1.3 @@ -21,6 +21,9 @@
     1.4  
     1.5  datatype trie = Lf | Nd bool "trie * trie"
     1.6  
     1.7 +definition empty :: trie where
     1.8 +[simp]: "empty = Lf"
     1.9 +
    1.10  fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool" where
    1.11  "isin Lf ks = False" |
    1.12  "isin (Nd b lr) ks =
    1.13 @@ -34,8 +37,8 @@
    1.14  "insert (k#ks) Lf = Nd False (mod2 (insert ks) k (Lf,Lf))" |
    1.15  "insert (k#ks) (Nd b lr) = Nd b (mod2 (insert ks) k lr)"
    1.16  
    1.17 -lemma isin_insert: "isin (insert as t) bs = (as = bs \<or> isin t bs)"
    1.18 -apply(induction as t arbitrary: bs rule: insert.induct)
    1.19 +lemma isin_insert: "isin (insert xs t) ys = (xs = ys \<or> isin t ys)"
    1.20 +apply(induction xs t arbitrary: ys rule: insert.induct)
    1.21  apply (auto split: list.splits if_splits)
    1.22  done
    1.23  
    1.24 @@ -65,8 +68,8 @@
    1.25        [] \<Rightarrow> node False lr |
    1.26        k#ks' \<Rightarrow> node b (mod2 (delete ks') k lr))"
    1.27  
    1.28 -lemma isin_delete: "isin (delete as t) bs = (as \<noteq> bs \<and> isin t bs)"
    1.29 -apply(induction as t arbitrary: bs rule: delete.induct)
    1.30 +lemma isin_delete: "isin (delete xs t) ys = (xs \<noteq> ys \<and> isin t ys)"
    1.31 +apply(induction xs t arbitrary: ys rule: delete.induct)
    1.32   apply simp
    1.33  apply (auto split: list.splits if_splits)
    1.34    apply (metis isin.simps(1))
    1.35 @@ -76,20 +79,29 @@
    1.36  definition set_trie :: "trie \<Rightarrow> bool list set" where
    1.37  "set_trie t = {xs. isin t xs}"
    1.38  
    1.39 +lemma set_trie_empty: "set_trie empty = {}"
    1.40 +by(simp add: set_trie_def)
    1.41 +
    1.42 +lemma set_trie_isin: "isin t xs = (xs \<in> set_trie t)"
    1.43 +by(simp add: set_trie_def)
    1.44 +
    1.45  lemma set_trie_insert: "set_trie(insert xs t) = set_trie t \<union> {xs}"
    1.46  by(auto simp add: isin_insert set_trie_def)
    1.47  
    1.48 +lemma set_trie_delete: "set_trie(delete xs t) = set_trie t - {xs}"
    1.49 +by(auto simp add: isin_delete set_trie_def)
    1.50 +
    1.51  interpretation S: Set
    1.52 -where empty = Lf and isin = isin and insert = insert and delete = delete
    1.53 +where empty = empty and isin = isin and insert = insert and delete = delete
    1.54  and set = set_trie and invar = "\<lambda>t. True"
    1.55  proof (standard, goal_cases)
    1.56 -  case 1 show ?case by (simp add: set_trie_def)
    1.57 +  case 1 show ?case by (rule set_trie_empty)
    1.58  next
    1.59 -  case 2 thus ?case by(simp add: set_trie_def)
    1.60 +  case 2 show ?case by(rule set_trie_isin)
    1.61  next
    1.62    case 3 thus ?case by(auto simp: set_trie_insert)
    1.63  next
    1.64 -  case 4 thus ?case by(auto simp: isin_delete set_trie_def)
    1.65 +  case 4 show ?case by(rule set_trie_delete)
    1.66  qed (rule TrueI)+
    1.67  
    1.68