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*}