# HG changeset patch
# User paulson
# Date 1296655886 0
# Node ID 47532fe9e075b139e5a5c4a3105ea0e75be59b65
# Parent  0593a2979cd34c4595bd89c5180a8e7109f93105
Introduction of metis calls and other cosmetic modifications.

diff -r 0593a2979cd3 -r 47532fe9e075 src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Wed Feb 02 15:47:57 2011 +0100
+++ b/src/HOL/Auth/Event.thy	Wed Feb 02 14:11:26 2011 +0000
@@ -271,7 +271,7 @@
 text{*For proving @{text new_keys_not_used}*}
 lemma keysFor_parts_insert:
      "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] 
-      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"; 
+      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"
 by (force 
     dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
            analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
diff -r 0593a2979cd3 -r 47532fe9e075 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Wed Feb 02 15:47:57 2011 +0100
+++ b/src/HOL/Auth/Message.thy	Wed Feb 02 14:11:26 2011 +0000
@@ -239,16 +239,15 @@
 by (metis parts_idem parts_increasing parts_mono subset_trans)
 
 lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
-by (drule parts_mono, blast)
+by (metis parts_subset_iff set_mp)
 
 text{*Cut*}
 lemma parts_cut:
      "[| Y\<in> parts (insert X G);  X\<in> parts H |] ==> Y\<in> parts (G \<union> H)" 
 by (blast intro: parts_trans) 
 
-
 lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H"
-by (force dest!: parts_cut intro: parts_insertI)
+by (metis insert_absorb parts_idem parts_insert)
 
 
 subsubsection{*Rewrite rules for pulling out atomic messages *}
@@ -519,7 +518,7 @@
   the forwarding of unknown components (X).  Without it, removing occurrences
   of X can be very complicated. *}
 lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
-by (blast intro: analz_cut analz_insertI)
+by (metis analz_cut analz_insert_eq_I insert_absorb)
 
 
 text{*A congruence rule for "analz" *}
@@ -527,9 +526,7 @@
 lemma analz_subset_cong:
      "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |] 
       ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
-apply simp
-apply (iprover intro: conjI subset_trans analz_mono Un_upper1 Un_upper2) 
-done
+by (metis Un_mono analz_Un analz_subset_iff subset_trans)
 
 lemma analz_cong:
      "[| analz G = analz G'; analz H = analz H' |] 
diff -r 0593a2979cd3 -r 47532fe9e075 src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Wed Feb 02 15:47:57 2011 +0100
+++ b/src/HOL/Auth/Shared.thy	Wed Feb 02 14:11:26 2011 +0000
@@ -67,10 +67,10 @@
 lemma keysFor_parts_insert:
      "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |]
       ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H"
-by (force dest: Event.keysFor_parts_insert)  
+by (metis invKey_K keysFor_parts_insert)
 
 lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H"
-by (drule Crypt_imp_invKey_keysFor, simp)
+by (metis Crypt_imp_invKey_keysFor invKey_K)
 
 
 subsection{*Function "knows"*}
@@ -84,8 +84,7 @@
 (*For case analysis on whether or not an agent is compromised*)
 lemma Crypt_Spy_analz_bad: "[| Crypt (shrK A) X \<in> analz (knows Spy evs);  A: bad |]  
       ==> X \<in> analz (knows Spy evs)"
-apply (force dest!: analz.Decrypt)
-done
+by (metis Spy_knows_Spy_bad analz.Inj analz_Decrypt')
 
 
 (** Fresh keys never clash with long-term shared keys **)
@@ -115,8 +114,7 @@
 by (induct_tac "B", auto)
 
 lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
-apply (simp (no_asm) add: used_Nil)
-done
+by (simp add: used_Nil)
 
 
 subsection{*Supply fresh nonces for possibility theorems.*}
@@ -126,19 +124,16 @@
 apply (induct_tac "evs")
 apply (rule_tac x = 0 in exI)
 apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
-apply safe
-apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
+apply (metis le_sup_iff msg_Nonce_supply)
 done
 
 lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
-by (rule Nonce_supply_lemma [THEN exE], blast)
+by (metis Nonce_supply_lemma order_eq_iff)
 
 lemma Nonce_supply2: "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'"
 apply (cut_tac evs = evs in Nonce_supply_lemma)
 apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify)
-apply (rule_tac x = N in exI)
-apply (rule_tac x = "Suc (N+Na)" in exI)
-apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
+apply (metis Suc_n_not_le_n nat_le_linear)
 done
 
 lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' &