tuned
authornipkow
Tue May 14 20:35:09 2019 +0200 (5 days ago ago)
changeset 7045340b6bc5a4721
parent 70452 81403d7b9038
child 70454 4065e3b0e5bf
tuned
src/HOL/Data_Structures/Tries_Binary.thy
     1.1 --- a/src/HOL/Data_Structures/Tries_Binary.thy	Tue May 14 17:21:13 2019 +0200
     1.2 +++ b/src/HOL/Data_Structures/Tries_Binary.thy	Tue May 14 20:35:09 2019 +0200
     1.3 @@ -184,7 +184,7 @@
     1.4  apply(auto split: list.split)
     1.5  done
     1.6  
     1.7 -lemma isinP:
     1.8 +lemma abs_trieP_isinP:
     1.9    "isinP t ks = isin (abs_trieP t) ks"
    1.10  apply(induction t arbitrary: ks rule: abs_trieP.induct)
    1.11   apply(auto simp: isin_prefix_trie split: list.split)
    1.12 @@ -260,21 +260,26 @@
    1.13  definition set_trieP :: "trieP \<Rightarrow> bool list set" where
    1.14  "set_trieP = set_trie o abs_trieP"
    1.15  
    1.16 +lemma isinP_set_trieP: "isinP t xs = (xs \<in> set_trieP t)"
    1.17 +by(simp add: abs_trieP_isinP set_trie_isin set_trieP_def)
    1.18 +
    1.19  lemma set_trieP_insertP: "set_trieP (insertP xs t) = set_trieP t \<union> {xs}"
    1.20  by(simp add: abs_trieP_insertP set_trie_insert set_trieP_def)
    1.21  
    1.22 +lemma set_trieP_deleteP: "set_trieP (deleteP xs t) = set_trieP t - {xs}"
    1.23 +by(auto simp: set_trie_delete set_trieP_def simp flip: delete_abs_trieP)
    1.24 +
    1.25  interpretation SP: Set
    1.26  where empty = emptyP and isin = isinP and insert = insertP and delete = deleteP
    1.27  and set = set_trieP and invar = "\<lambda>t. True"
    1.28  proof (standard, goal_cases)
    1.29    case 1 show ?case by (simp add: set_trieP_def set_trie_def)
    1.30  next
    1.31 -  case 2 thus ?case by(simp add: isinP set_trieP_def set_trie_def)
    1.32 +  case 2 show ?case by(rule isinP_set_trieP)
    1.33  next
    1.34    case 3 thus ?case by (auto simp: set_trieP_insertP)
    1.35  next
    1.36 -  case 4 thus ?case
    1.37 -    by(auto simp: isin_delete set_trieP_def set_trie_def simp flip: delete_abs_trieP)
    1.38 +  case 4 thus ?case by(auto simp: set_trieP_deleteP)
    1.39  qed (rule TrueI)+
    1.40  
    1.41  end