# HG changeset patch
# User haftmann
# Date 1398354739 -7200
# Node ID e8d5d60d655ec790037947d7d9961a5f72623468
# Parent  4e2a0d4e7a8204480aaafa79db29d56f44e1b581
avoid non-standard simp default rule

diff -r 4e2a0d4e7a82 -r e8d5d60d655e src/HOL/Auth/Guard/Extensions.thy
--- 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)
diff -r 4e2a0d4e7a82 -r e8d5d60d655e src/HOL/Auth/Guard/Guard.thy
--- 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)+)
diff -r 4e2a0d4e7a82 -r e8d5d60d655e src/HOL/Auth/Guard/GuardK.thy
--- 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)"
diff -r 4e2a0d4e7a82 -r e8d5d60d655e src/HOL/Auth/Guard/Guard_Shared.thy
--- 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)
diff -r 4e2a0d4e7a82 -r e8d5d60d655e src/HOL/Auth/Guard/Proto.thy
--- 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"
diff -r 4e2a0d4e7a82 -r e8d5d60d655e src/HOL/Auth/NS_Public.thy
--- 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"
diff -r 4e2a0d4e7a82 -r e8d5d60d655e src/HOL/Auth/NS_Public_Bad.thy
--- 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"
diff -r 4e2a0d4e7a82 -r e8d5d60d655e src/HOL/Auth/NS_Shared.thy
--- 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*}