Introduction of metis calls and other cosmetic modifications.
authorpaulson
Wed Feb 02 14:11:26 2011 +0000 (2011-02-02)
changeset 4169347532fe9e075
parent 41692 0593a2979cd3
child 41694 a96d43a54650
Introduction of metis calls and other cosmetic modifications.
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/Shared.thy
     1.1 --- a/src/HOL/Auth/Event.thy	Wed Feb 02 15:47:57 2011 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Wed Feb 02 14:11:26 2011 +0000
     1.3 @@ -271,7 +271,7 @@
     1.4  text{*For proving @{text new_keys_not_used}*}
     1.5  lemma keysFor_parts_insert:
     1.6       "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] 
     1.7 -      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"; 
     1.8 +      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"
     1.9  by (force 
    1.10      dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
    1.11             analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
     2.1 --- a/src/HOL/Auth/Message.thy	Wed Feb 02 15:47:57 2011 +0100
     2.2 +++ b/src/HOL/Auth/Message.thy	Wed Feb 02 14:11:26 2011 +0000
     2.3 @@ -239,16 +239,15 @@
     2.4  by (metis parts_idem parts_increasing parts_mono subset_trans)
     2.5  
     2.6  lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
     2.7 -by (drule parts_mono, blast)
     2.8 +by (metis parts_subset_iff set_mp)
     2.9  
    2.10  text{*Cut*}
    2.11  lemma parts_cut:
    2.12       "[| Y\<in> parts (insert X G);  X\<in> parts H |] ==> Y\<in> parts (G \<union> H)" 
    2.13  by (blast intro: parts_trans) 
    2.14  
    2.15 -
    2.16  lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H"
    2.17 -by (force dest!: parts_cut intro: parts_insertI)
    2.18 +by (metis insert_absorb parts_idem parts_insert)
    2.19  
    2.20  
    2.21  subsubsection{*Rewrite rules for pulling out atomic messages *}
    2.22 @@ -519,7 +518,7 @@
    2.23    the forwarding of unknown components (X).  Without it, removing occurrences
    2.24    of X can be very complicated. *}
    2.25  lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
    2.26 -by (blast intro: analz_cut analz_insertI)
    2.27 +by (metis analz_cut analz_insert_eq_I insert_absorb)
    2.28  
    2.29  
    2.30  text{*A congruence rule for "analz" *}
    2.31 @@ -527,9 +526,7 @@
    2.32  lemma analz_subset_cong:
    2.33       "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |] 
    2.34        ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
    2.35 -apply simp
    2.36 -apply (iprover intro: conjI subset_trans analz_mono Un_upper1 Un_upper2) 
    2.37 -done
    2.38 +by (metis Un_mono analz_Un analz_subset_iff subset_trans)
    2.39  
    2.40  lemma analz_cong:
    2.41       "[| analz G = analz G'; analz H = analz H' |] 
     3.1 --- a/src/HOL/Auth/Shared.thy	Wed Feb 02 15:47:57 2011 +0100
     3.2 +++ b/src/HOL/Auth/Shared.thy	Wed Feb 02 14:11:26 2011 +0000
     3.3 @@ -67,10 +67,10 @@
     3.4  lemma keysFor_parts_insert:
     3.5       "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |]
     3.6        ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H"
     3.7 -by (force dest: Event.keysFor_parts_insert)  
     3.8 +by (metis invKey_K keysFor_parts_insert)
     3.9  
    3.10  lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H"
    3.11 -by (drule Crypt_imp_invKey_keysFor, simp)
    3.12 +by (metis Crypt_imp_invKey_keysFor invKey_K)
    3.13  
    3.14  
    3.15  subsection{*Function "knows"*}
    3.16 @@ -84,8 +84,7 @@
    3.17  (*For case analysis on whether or not an agent is compromised*)
    3.18  lemma Crypt_Spy_analz_bad: "[| Crypt (shrK A) X \<in> analz (knows Spy evs);  A: bad |]  
    3.19        ==> X \<in> analz (knows Spy evs)"
    3.20 -apply (force dest!: analz.Decrypt)
    3.21 -done
    3.22 +by (metis Spy_knows_Spy_bad analz.Inj analz_Decrypt')
    3.23  
    3.24  
    3.25  (** Fresh keys never clash with long-term shared keys **)
    3.26 @@ -115,8 +114,7 @@
    3.27  by (induct_tac "B", auto)
    3.28  
    3.29  lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
    3.30 -apply (simp (no_asm) add: used_Nil)
    3.31 -done
    3.32 +by (simp add: used_Nil)
    3.33  
    3.34  
    3.35  subsection{*Supply fresh nonces for possibility theorems.*}
    3.36 @@ -126,19 +124,16 @@
    3.37  apply (induct_tac "evs")
    3.38  apply (rule_tac x = 0 in exI)
    3.39  apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
    3.40 -apply safe
    3.41 -apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
    3.42 +apply (metis le_sup_iff msg_Nonce_supply)
    3.43  done
    3.44  
    3.45  lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
    3.46 -by (rule Nonce_supply_lemma [THEN exE], blast)
    3.47 +by (metis Nonce_supply_lemma order_eq_iff)
    3.48  
    3.49  lemma Nonce_supply2: "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'"
    3.50  apply (cut_tac evs = evs in Nonce_supply_lemma)
    3.51  apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify)
    3.52 -apply (rule_tac x = N in exI)
    3.53 -apply (rule_tac x = "Suc (N+Na)" in exI)
    3.54 -apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
    3.55 +apply (metis Suc_n_not_le_n nat_le_linear)
    3.56  done
    3.57  
    3.58  lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' &