avoid non-standard simp default rule
authorhaftmann
Thu Apr 24 17:52:19 2014 +0200 (2014-04-24)
changeset 56681e8d5d60d655e
parent 56680 4e2a0d4e7a82
child 56682 d39926ff0487
avoid non-standard simp default rule
src/HOL/Auth/Guard/Extensions.thy
src/HOL/Auth/Guard/Guard.thy
src/HOL/Auth/Guard/GuardK.thy
src/HOL/Auth/Guard/Guard_Shared.thy
src/HOL/Auth/Guard/Proto.thy
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.thy
src/HOL/Auth/NS_Shared.thy
     1.1 --- a/src/HOL/Auth/Guard/Extensions.thy	Thu Apr 24 10:33:17 2014 +0200
     1.2 +++ b/src/HOL/Auth/Guard/Extensions.thy	Thu Apr 24 17:52:19 2014 +0200
     1.3 @@ -37,7 +37,6 @@
     1.4  subsubsection{*declarations for tactics*}
     1.5  
     1.6  declare analz_subset_parts [THEN subsetD, dest]
     1.7 -declare image_eq_UN [simp]
     1.8  declare parts_insert2 [simp]
     1.9  declare analz_cut [dest]
    1.10  declare split_if_asm [split]
    1.11 @@ -112,8 +111,9 @@
    1.12  
    1.13  lemma finite_keysFor [intro]: "finite G ==> finite (keysFor G)"
    1.14  apply (simp add: keysFor_def)
    1.15 -apply (rule finite_UN_I, auto)
    1.16 -apply (erule finite_induct, auto)
    1.17 +apply (rule finite_imageI)
    1.18 +apply (induct G rule: finite_induct)
    1.19 +apply auto
    1.20  apply (case_tac "EX K X. x = Crypt K X", clarsimp)
    1.21  apply (subgoal_tac "{Ka. EX Xa. (Ka=K & Xa=X) | Crypt Ka Xa:F}
    1.22  = insert K (usekeys F)", auto simp: usekeys_def)
     2.1 --- a/src/HOL/Auth/Guard/Guard.thy	Thu Apr 24 10:33:17 2014 +0200
     2.2 +++ b/src/HOL/Auth/Guard/Guard.thy	Thu Apr 24 17:52:19 2014 +0200
     2.3 @@ -56,7 +56,7 @@
     2.4  by (erule guard.induct, auto)
     2.5  
     2.6  lemma guard_Crypt: "[| Crypt K Y:guard n Ks; K ~:invKey`Ks |] ==> Y:guard n Ks"
     2.7 -by (ind_cases "Crypt K Y:guard n Ks", auto)
     2.8 +  by (ind_cases "Crypt K Y:guard n Ks") (auto intro!: image_eqI)
     2.9  
    2.10  lemma guard_MPair [iff]: "({|X,Y|}:guard n Ks) = (X:guard n Ks & Y:guard n Ks)"
    2.11  by (auto, (ind_cases "{|X,Y|}:guard n Ks", auto)+)
     3.1 --- a/src/HOL/Auth/Guard/GuardK.thy	Thu Apr 24 10:33:17 2014 +0200
     3.2 +++ b/src/HOL/Auth/Guard/GuardK.thy	Thu Apr 24 17:52:19 2014 +0200
     3.3 @@ -63,7 +63,7 @@
     3.4  by (erule guardK.induct, auto dest: kparts_parts parts_sub)
     3.5  
     3.6  lemma guardK_Crypt: "[| Crypt K Y:guardK n Ks; K ~:invKey`Ks |] ==> Y:guardK n Ks"
     3.7 -by (ind_cases "Crypt K Y:guardK n Ks", auto)
     3.8 +  by (ind_cases "Crypt K Y:guardK n Ks") (auto intro!: image_eqI)
     3.9  
    3.10  lemma guardK_MPair [iff]: "({|X,Y|}:guardK n Ks)
    3.11  = (X:guardK n Ks & Y:guardK n Ks)"
     4.1 --- a/src/HOL/Auth/Guard/Guard_Shared.thy	Thu Apr 24 10:33:17 2014 +0200
     4.2 +++ b/src/HOL/Auth/Guard/Guard_Shared.thy	Thu Apr 24 17:52:19 2014 +0200
     4.3 @@ -171,7 +171,7 @@
     4.4  lemma GuardK_Key_analz: "[| GuardK n Ks (spies evs); evs:p;
     4.5  shrK_set Ks; good Ks; regular p; n ~:range shrK |] ==> Key n ~:analz (spies evs)"
     4.6  apply (clarify, simp only: knows_decomp)
     4.7 -apply (drule GuardK_invKey_keyset, clarify, simp+, simp add: initState.simps)
     4.8 +apply (drule GuardK_invKey_keyset, clarify, simp+, simp add: initState.simps image_eq_UN)
     4.9  apply clarify
    4.10  apply (drule in_good, simp)
    4.11  apply (drule in_shrK_set, simp+, clarify)
     5.1 --- a/src/HOL/Auth/Guard/Proto.thy	Thu Apr 24 10:33:17 2014 +0200
     5.2 +++ b/src/HOL/Auth/Guard/Proto.thy	Thu Apr 24 17:52:19 2014 +0200
     5.3 @@ -56,7 +56,7 @@
     5.4  Nonce n ~:parts (apm s `(msg `(fst R))) |] ==>
     5.5  (EX k. Nonce k:parts {X} & nonce s k = n)"
     5.6  apply (erule Nonce_apm, unfold wdef_def)
     5.7 -apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp)
     5.8 +apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp simp: image_eq_UN)
     5.9  apply (drule_tac x=x in bspec, simp)
    5.10  apply (drule_tac Y="msg x" and s=s in apm_parts, simp)
    5.11  by (blast dest: parts_parts)
    5.12 @@ -134,7 +134,7 @@
    5.13  
    5.14  lemma ok_not_used: "[| Nonce n ~:used evs; ok evs R s;
    5.15  ALL x. x:fst R --> is_Says x |] ==> Nonce n ~:parts (apm s `(msg `(fst R)))"
    5.16 -apply (unfold ok_def, clarsimp)
    5.17 +apply (unfold ok_def, clarsimp simp: image_eq_UN)
    5.18  apply (drule_tac x=x in spec, drule_tac x=x in spec)
    5.19  by (auto simp: is_Says_def dest: Says_imp_spies not_used_not_spied parts_parts)
    5.20  
    5.21 @@ -188,10 +188,10 @@
    5.22  apply (drule wdef_Nonce, simp+)
    5.23  apply (frule ok_not_used, simp+)
    5.24  apply (clarify, erule ok_is_Says, simp+)
    5.25 -apply (clarify, rule_tac x=k in exI, simp add: newn_def)
    5.26 +apply (clarify, rule_tac x=k in exI, simp add: newn_def image_eq_UN)
    5.27  apply (clarify, drule_tac Y="msg x" and s=s in apm_parts)
    5.28  apply (drule ok_not_used, simp+)
    5.29 -by (clarify, erule ok_is_Says, simp+)
    5.30 +by (clarify, erule ok_is_Says, simp_all add: image_eq_UN)
    5.31  
    5.32  lemma fresh_rule: "[| evs' @ ev # evs:tr p; wdef p; Nonce n ~:used evs;
    5.33  Nonce n:parts {msg ev} |] ==> EX R s. R:p & ap' s R = ev"
     6.1 --- a/src/HOL/Auth/NS_Public.thy	Thu Apr 24 10:33:17 2014 +0200
     6.2 +++ b/src/HOL/Auth/NS_Public.thy	Thu Apr 24 17:52:19 2014 +0200
     6.3 @@ -42,8 +42,7 @@
     6.4  declare knows_Spy_partsEs [elim]
     6.5  declare knows_Spy_partsEs [elim]
     6.6  declare analz_into_parts [dest]
     6.7 -declare Fake_parts_insert_in_Un  [dest]
     6.8 -declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
     6.9 +declare Fake_parts_insert_in_Un [dest]
    6.10  
    6.11  (*A "possibility property": there are traces that reach the end*)
    6.12  lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
     7.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Thu Apr 24 10:33:17 2014 +0200
     7.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Thu Apr 24 17:52:19 2014 +0200
     7.3 @@ -44,8 +44,7 @@
     7.4  
     7.5  declare knows_Spy_partsEs [elim]
     7.6  declare analz_into_parts [dest]
     7.7 -declare Fake_parts_insert_in_Un  [dest]
     7.8 -declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
     7.9 +declare Fake_parts_insert_in_Un [dest]
    7.10  
    7.11  (*A "possibility property": there are traces that reach the end*)
    7.12  lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
     8.1 --- a/src/HOL/Auth/NS_Shared.thy	Thu Apr 24 10:33:17 2014 +0200
     8.2 +++ b/src/HOL/Auth/NS_Shared.thy	Thu Apr 24 17:52:19 2014 +0200
     8.3 @@ -86,7 +86,6 @@
     8.4  declare parts.Body  [dest]
     8.5  declare Fake_parts_insert_in_Un  [dest]
     8.6  declare analz_into_parts [dest]
     8.7 -declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
     8.8  
     8.9  
    8.10  text{*A "possibility property": there are traces that reach the end*}