--- a/src/HOL/Auth/Guard/Extensions.thy Thu Apr 24 10:33:17 2014 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy Thu Apr 24 17:52:19 2014 +0200
@@ -37,7 +37,6 @@
subsubsection{*declarations for tactics*}
declare analz_subset_parts [THEN subsetD, dest]
-declare image_eq_UN [simp]
declare parts_insert2 [simp]
declare analz_cut [dest]
declare split_if_asm [split]
@@ -112,8 +111,9 @@
lemma finite_keysFor [intro]: "finite G ==> finite (keysFor G)"
apply (simp add: keysFor_def)
-apply (rule finite_UN_I, auto)
-apply (erule finite_induct, auto)
+apply (rule finite_imageI)
+apply (induct G rule: finite_induct)
+apply auto
apply (case_tac "EX K X. x = Crypt K X", clarsimp)
apply (subgoal_tac "{Ka. EX Xa. (Ka=K & Xa=X) | Crypt Ka Xa:F}
= insert K (usekeys F)", auto simp: usekeys_def)
--- a/src/HOL/Auth/Guard/Guard.thy Thu Apr 24 10:33:17 2014 +0200
+++ b/src/HOL/Auth/Guard/Guard.thy Thu Apr 24 17:52:19 2014 +0200
@@ -56,7 +56,7 @@
by (erule guard.induct, auto)
lemma guard_Crypt: "[| Crypt K Y:guard n Ks; K ~:invKey`Ks |] ==> Y:guard n Ks"
-by (ind_cases "Crypt K Y:guard n Ks", auto)
+ by (ind_cases "Crypt K Y:guard n Ks") (auto intro!: image_eqI)
lemma guard_MPair [iff]: "({|X,Y|}:guard n Ks) = (X:guard n Ks & Y:guard n Ks)"
by (auto, (ind_cases "{|X,Y|}:guard n Ks", auto)+)
--- a/src/HOL/Auth/Guard/GuardK.thy Thu Apr 24 10:33:17 2014 +0200
+++ b/src/HOL/Auth/Guard/GuardK.thy Thu Apr 24 17:52:19 2014 +0200
@@ -63,7 +63,7 @@
by (erule guardK.induct, auto dest: kparts_parts parts_sub)
lemma guardK_Crypt: "[| Crypt K Y:guardK n Ks; K ~:invKey`Ks |] ==> Y:guardK n Ks"
-by (ind_cases "Crypt K Y:guardK n Ks", auto)
+ by (ind_cases "Crypt K Y:guardK n Ks") (auto intro!: image_eqI)
lemma guardK_MPair [iff]: "({|X,Y|}:guardK n Ks)
= (X:guardK n Ks & Y:guardK n Ks)"
--- a/src/HOL/Auth/Guard/Guard_Shared.thy Thu Apr 24 10:33:17 2014 +0200
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy Thu Apr 24 17:52:19 2014 +0200
@@ -171,7 +171,7 @@
lemma GuardK_Key_analz: "[| GuardK n Ks (spies evs); evs:p;
shrK_set Ks; good Ks; regular p; n ~:range shrK |] ==> Key n ~:analz (spies evs)"
apply (clarify, simp only: knows_decomp)
-apply (drule GuardK_invKey_keyset, clarify, simp+, simp add: initState.simps)
+apply (drule GuardK_invKey_keyset, clarify, simp+, simp add: initState.simps image_eq_UN)
apply clarify
apply (drule in_good, simp)
apply (drule in_shrK_set, simp+, clarify)
--- a/src/HOL/Auth/Guard/Proto.thy Thu Apr 24 10:33:17 2014 +0200
+++ b/src/HOL/Auth/Guard/Proto.thy Thu Apr 24 17:52:19 2014 +0200
@@ -56,7 +56,7 @@
Nonce n ~:parts (apm s `(msg `(fst R))) |] ==>
(EX k. Nonce k:parts {X} & nonce s k = n)"
apply (erule Nonce_apm, unfold wdef_def)
-apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp)
+apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp simp: image_eq_UN)
apply (drule_tac x=x in bspec, simp)
apply (drule_tac Y="msg x" and s=s in apm_parts, simp)
by (blast dest: parts_parts)
@@ -134,7 +134,7 @@
lemma ok_not_used: "[| Nonce n ~:used evs; ok evs R s;
ALL x. x:fst R --> is_Says x |] ==> Nonce n ~:parts (apm s `(msg `(fst R)))"
-apply (unfold ok_def, clarsimp)
+apply (unfold ok_def, clarsimp simp: image_eq_UN)
apply (drule_tac x=x in spec, drule_tac x=x in spec)
by (auto simp: is_Says_def dest: Says_imp_spies not_used_not_spied parts_parts)
@@ -188,10 +188,10 @@
apply (drule wdef_Nonce, simp+)
apply (frule ok_not_used, simp+)
apply (clarify, erule ok_is_Says, simp+)
-apply (clarify, rule_tac x=k in exI, simp add: newn_def)
+apply (clarify, rule_tac x=k in exI, simp add: newn_def image_eq_UN)
apply (clarify, drule_tac Y="msg x" and s=s in apm_parts)
apply (drule ok_not_used, simp+)
-by (clarify, erule ok_is_Says, simp+)
+by (clarify, erule ok_is_Says, simp_all add: image_eq_UN)
lemma fresh_rule: "[| evs' @ ev # evs:tr p; wdef p; Nonce n ~:used evs;
Nonce n:parts {msg ev} |] ==> EX R s. R:p & ap' s R = ev"
--- a/src/HOL/Auth/NS_Public.thy Thu Apr 24 10:33:17 2014 +0200
+++ b/src/HOL/Auth/NS_Public.thy Thu Apr 24 17:52:19 2014 +0200
@@ -42,8 +42,7 @@
declare knows_Spy_partsEs [elim]
declare knows_Spy_partsEs [elim]
declare analz_into_parts [dest]
-declare Fake_parts_insert_in_Un [dest]
-declare image_eq_UN [simp] (*accelerates proofs involving nested images*)
+declare Fake_parts_insert_in_Un [dest]
(*A "possibility property": there are traces that reach the end*)
lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
--- a/src/HOL/Auth/NS_Public_Bad.thy Thu Apr 24 10:33:17 2014 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy Thu Apr 24 17:52:19 2014 +0200
@@ -44,8 +44,7 @@
declare knows_Spy_partsEs [elim]
declare analz_into_parts [dest]
-declare Fake_parts_insert_in_Un [dest]
-declare image_eq_UN [simp] (*accelerates proofs involving nested images*)
+declare Fake_parts_insert_in_Un [dest]
(*A "possibility property": there are traces that reach the end*)
lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
--- a/src/HOL/Auth/NS_Shared.thy Thu Apr 24 10:33:17 2014 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Thu Apr 24 17:52:19 2014 +0200
@@ -86,7 +86,6 @@
declare parts.Body [dest]
declare Fake_parts_insert_in_Un [dest]
declare analz_into_parts [dest]
-declare image_eq_UN [simp] (*accelerates proofs involving nested images*)
text{*A "possibility property": there are traces that reach the end*}