tidying of Isar scripts
authorpaulson
Sat Aug 17 14:55:08 2002 +0200 (2002-08-17)
changeset 13507febb8e5d2a9d
parent 13506 acc18a5d2b1a
child 13508 890d736b93a5
tidying of Isar scripts
src/HOL/Auth/KerberosIV.thy
src/HOL/Auth/Kerberos_BAN.thy
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.thy
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/OtwayRees_Bad.thy
src/HOL/Auth/Recur.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/TLS.thy
src/HOL/Auth/WooLam.thy
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.thy
src/HOL/Auth/Yahalom_Bad.thy
     1.1 --- a/src/HOL/Auth/KerberosIV.thy	Fri Aug 16 17:19:43 2002 +0200
     1.2 +++ b/src/HOL/Auth/KerberosIV.thy	Sat Aug 17 14:55:08 2002 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4                        
     1.5   (* A is the true creator of X if she has sent X and X never appeared on
     1.6      the trace before this event. Recall that traces grow from head. *)
     1.7 -  Issues :: [agent , agent, msg, event list] => bool ("_ Issues _ with _ on _")
     1.8 +  Issues :: [agent, agent, msg, event list] => bool ("_ Issues _ with _ on _")
     1.9     "A Issues B with X on evs == 
    1.10        \\<exists>Y. Says A B Y \\<in> set evs & X \\<in> parts {Y} &
    1.11        X \\<notin> parts (spies (takeWhile (% z. z  \\<noteq> Says A B Y) (rev evs)))"
     2.1 --- a/src/HOL/Auth/Kerberos_BAN.thy	Fri Aug 16 17:19:43 2002 +0200
     2.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Sat Aug 17 14:55:08 2002 +0200
     2.3 @@ -89,5 +89,4 @@
     2.4               Expired Ts evso |]
     2.5            ==> Notes Spy {|Number Ts, Key K|} # evso \\<in> kerberos_ban"
     2.6  
     2.7 -
     2.8  end
     3.1 --- a/src/HOL/Auth/NS_Public.thy	Fri Aug 16 17:19:43 2002 +0200
     3.2 +++ b/src/HOL/Auth/NS_Public.thy	Sat Aug 17 14:55:08 2002 +0200
     3.3 @@ -103,8 +103,7 @@
     3.4          A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
     3.5         \<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
     3.6  apply (erule rev_mp)   
     3.7 -apply (erule ns_public.induct, simp_all)
     3.8 -apply spy_analz
     3.9 +apply (erule ns_public.induct, simp_all, spy_analz)
    3.10  apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
    3.11  done
    3.12  
    3.13 @@ -166,8 +165,7 @@
    3.14         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>
    3.15        \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
    3.16  apply (erule rev_mp)
    3.17 -apply (erule ns_public.induct, simp_all)
    3.18 -apply spy_analz
    3.19 +apply (erule ns_public.induct, simp_all, spy_analz)
    3.20  apply (blast intro: no_nonce_NS1_NS2)+
    3.21  done
    3.22  
     4.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Fri Aug 16 17:19:43 2002 +0200
     4.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Sat Aug 17 14:55:08 2002 +0200
     4.3 @@ -106,8 +106,7 @@
     4.4          A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
     4.5         \<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
     4.6  apply (erule rev_mp)   
     4.7 -apply (erule ns_public.induct, simp_all)
     4.8 -apply spy_analz
     4.9 +apply (erule ns_public.induct, simp_all, spy_analz)
    4.10  apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
    4.11  done
    4.12  
    4.13 @@ -167,8 +166,7 @@
    4.14         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                      
    4.15       \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
    4.16  apply (erule rev_mp, erule rev_mp)
    4.17 -apply (erule ns_public.induct, simp_all)
    4.18 -apply spy_analz
    4.19 +apply (erule ns_public.induct, simp_all, spy_analz)
    4.20  apply (simp_all add: all_conj_distrib) (*speeds up the next step*)
    4.21  apply (blast intro: no_nonce_NS1_NS2)+
    4.22  done
    4.23 @@ -197,17 +195,15 @@
    4.24  lemma "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>            
    4.25         \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs  
    4.26             \<longrightarrow> Nonce NB \<notin> analz (spies evs)"
    4.27 -apply (erule ns_public.induct, simp_all)
    4.28 -apply spy_analz
    4.29 +apply (erule ns_public.induct, simp_all, spy_analz)
    4.30  (*NS1: by freshness*)
    4.31  apply blast
    4.32  (*NS2: by freshness and unicity of NB*)
    4.33  apply (blast intro: no_nonce_NS1_NS2)
    4.34  (*NS3: unicity of NB identifies A and NA, but not B*)
    4.35  apply clarify
    4.36 -apply (frule_tac A' = "A" in 
    4.37 -       Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB])
    4.38 -apply auto
    4.39 +apply (frule_tac A' = A in 
    4.40 +       Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto)
    4.41  apply (rename_tac C B' evs3)
    4.42  oops
    4.43  
     5.1 --- a/src/HOL/Auth/NS_Shared.thy	Fri Aug 16 17:19:43 2002 +0200
     5.2 +++ b/src/HOL/Auth/NS_Shared.thy	Sat Aug 17 14:55:08 2002 +0200
     5.3 @@ -85,8 +85,7 @@
     5.4  apply (intro exI bexI)
     5.5  apply (rule_tac [2] ns_shared.Nil
     5.6         [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
     5.7 -	THEN ns_shared.NS4, THEN ns_shared.NS5])
     5.8 -apply possibility
     5.9 +	THEN ns_shared.NS4, THEN ns_shared.NS5], possibility)
    5.10  done
    5.11  
    5.12  (*This version is similar, while instantiating ?K and ?N to epsilon-terms
    5.13 @@ -116,9 +115,7 @@
    5.14  (*Spy never sees another agent's shared key! (unless it's bad at start)*)
    5.15  lemma Spy_see_shrK [simp]:
    5.16       "evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)"
    5.17 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
    5.18 -apply simp_all
    5.19 -apply blast+;
    5.20 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
    5.21  done
    5.22  
    5.23  lemma Spy_analz_shrK [simp]:
    5.24 @@ -129,8 +126,7 @@
    5.25  (*Nobody can have used non-existent keys!*)
    5.26  lemma new_keys_not_used [rule_format, simp]:
    5.27      "evs \\<in> ns_shared \\<Longrightarrow> Key K \\<notin> used evs \\<longrightarrow> K \\<notin> keysFor (parts (spies evs))"
    5.28 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
    5.29 -apply simp_all
    5.30 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
    5.31  (*Fake, NS2, NS4, NS5*)
    5.32  apply (blast dest!: keysFor_parts_insert)+
    5.33  done
    5.34 @@ -154,8 +150,7 @@
    5.35         A \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
    5.36        \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs"
    5.37  apply (erule rev_mp)
    5.38 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
    5.39 -apply auto
    5.40 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
    5.41  done
    5.42  
    5.43  lemma cert_A_form:
    5.44 @@ -182,7 +177,7 @@
    5.45     \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs
    5.46         \\<or> X \\<in> analz (spies evs)"
    5.47  apply (case_tac "A \\<in> bad")
    5.48 -apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj]);
    5.49 +apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj])
    5.50  by (blast dest!: A_trusts_NS2 Says_Server_message_form)
    5.51  *)
    5.52  
    5.53 @@ -202,8 +197,7 @@
    5.54  lemma  "\\<lbrakk>evs \\<in> ns_shared;  Kab \\<notin> range shrK\\<rbrakk> \\<Longrightarrow>
    5.55           (Crypt KAB X) \\<in> parts (spies evs) \\<and>
    5.56           Key K \\<in> parts {X} \\<longrightarrow> Key K \\<in> parts (spies evs)"
    5.57 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
    5.58 -apply simp_all
    5.59 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
    5.60  (*Fake*)
    5.61  apply (blast dest: parts_insert_subset_Un)
    5.62  (*Base, NS4 and NS5*)
    5.63 @@ -222,9 +216,7 @@
    5.64               (K \\<in> KK \\<or> Key K \\<in> analz (spies evs))"
    5.65  apply (erule ns_shared.induct, force)
    5.66  apply (drule_tac [7] Says_Server_message_form)
    5.67 -apply (erule_tac [4] Says_S_message_form [THEN disjE])
    5.68 -apply analz_freshK
    5.69 -apply spy_analz
    5.70 +apply (erule_tac [4] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
    5.71  done
    5.72  
    5.73  
    5.74 @@ -242,9 +234,7 @@
    5.75       "\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
    5.76         Says Server A' (Crypt (shrK A') \\<lbrace>NA', Agent B', Key K, X'\\<rbrace>) \\<in> set evs;
    5.77         evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow> A=A' \\<and> NA=NA' \\<and> B=B' \\<and> X = X'"
    5.78 -apply (erule rev_mp, erule rev_mp, erule ns_shared.induct)
    5.79 -apply simp_all
    5.80 -apply blast+
    5.81 +apply (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
    5.82  done
    5.83  
    5.84  
    5.85 @@ -263,8 +253,7 @@
    5.86  apply (frule_tac [7] Says_Server_message_form)
    5.87  apply (frule_tac [4] Says_S_message_form)
    5.88  apply (erule_tac [5] disjE)
    5.89 -apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs)
    5.90 -apply spy_analz  (*Fake*)
    5.91 +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)  (*Fake*)
    5.92  apply blast      (*NS2*)
    5.93  (*NS3, Server sub-case*) (**LEVEL 8 **)
    5.94  apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
    5.95 @@ -295,8 +284,7 @@
    5.96                                   Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>)
    5.97                \\<in> set evs"
    5.98  apply (erule rev_mp)
    5.99 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   5.100 -apply auto
   5.101 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
   5.102  done
   5.103  
   5.104  
   5.105 @@ -307,12 +295,10 @@
   5.106        Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
   5.107        Says B A (Crypt K (Nonce NB)) \\<in> set evs"
   5.108  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   5.109 -apply (analz_mono_contra, simp_all)
   5.110 -apply blast     (*Fake*)
   5.111 +apply (analz_mono_contra, simp_all, blast)     (*Fake*)
   5.112  (*NS2: contradiction from the assumptions
   5.113    Key K \\<notin> used evs2  and Crypt K (Nonce NB) \\<in> parts (spies evs2) *)
   5.114 -apply (force dest!: Crypt_imp_keysFor)
   5.115 -apply blast     (*NS3*)
   5.116 +apply (force dest!: Crypt_imp_keysFor, blast)     (*NS3*)
   5.117  (*NS4*)
   5.118  apply (blast dest!: B_trusts_NS3
   5.119  	     dest: Says_imp_knows_Spy [THEN analz.Inj]
   5.120 @@ -338,10 +324,8 @@
   5.121       Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow>
   5.122       Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
   5.123       (\\<exists>A'. Says A' B X \\<in> set evs)"
   5.124 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   5.125 -apply analz_mono_contra
   5.126 -apply (simp_all add: ex_disj_distrib)
   5.127 -apply blast  (*Fake*)
   5.128 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra)
   5.129 +apply (simp_all add: ex_disj_distrib, blast)  (*Fake*)
   5.130  apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
   5.131  apply blast  (*NS3*)
   5.132  (*NS4*)
   5.133 @@ -359,10 +343,7 @@
   5.134  			    Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>) \\<in> set evs \\<longrightarrow>
   5.135       Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs) \\<longrightarrow>
   5.136       Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs"
   5.137 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   5.138 -apply analz_mono_contra
   5.139 -apply simp_all
   5.140 -apply blast  (*Fake*)
   5.141 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast)  (*Fake*)
   5.142  apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
   5.143  apply (blast dest!: cert_A_form) (*NS3*)
   5.144  (*NS5*)
     6.1 --- a/src/HOL/Auth/OtwayRees.thy	Fri Aug 16 17:19:43 2002 +0200
     6.2 +++ b/src/HOL/Auth/OtwayRees.thy	Sat Aug 17 14:55:08 2002 +0200
     6.3 @@ -98,15 +98,13 @@
     6.4  apply (rule_tac [2] otway.Nil
     6.5                      [THEN otway.OR1, THEN otway.Reception,
     6.6                       THEN otway.OR2, THEN otway.Reception,
     6.7 -                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
     6.8 -apply possibility
     6.9 +                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
    6.10  done
    6.11  
    6.12  lemma Gets_imp_Says [dest!]:
    6.13       "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
    6.14  apply (erule rev_mp)
    6.15 -apply (erule otway.induct)
    6.16 -apply auto
    6.17 +apply (erule otway.induct, auto)
    6.18  done
    6.19  
    6.20  
    6.21 @@ -141,8 +139,7 @@
    6.22  lemma Spy_see_shrK [simp]:
    6.23       "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
    6.24  apply (erule otway.induct, force,
    6.25 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
    6.26 -apply blast+
    6.27 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
    6.28  done
    6.29  
    6.30  lemma Spy_analz_shrK [simp]:
    6.31 @@ -162,8 +159,7 @@
    6.32       "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
    6.33           evs \<in> otway |]
    6.34        ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
    6.35 -apply (erule rev_mp, erule otway.induct, simp_all)
    6.36 -apply blast
    6.37 +apply (erule rev_mp, erule otway.induct, simp_all, blast)
    6.38  done
    6.39  
    6.40  
    6.41 @@ -188,9 +184,7 @@
    6.42  apply (erule otway.induct, force)
    6.43  apply (frule_tac [7] Says_Server_message_form)
    6.44  apply (drule_tac [6] OR4_analz_knows_Spy)
    6.45 -apply (drule_tac [4] OR2_analz_knows_Spy)
    6.46 -apply analz_freshK
    6.47 -apply spy_analz
    6.48 +apply (drule_tac [4] OR2_analz_knows_Spy, analz_freshK, spy_analz)
    6.49  done
    6.50  
    6.51  
    6.52 @@ -225,8 +219,7 @@
    6.53                   Crypt (shrK A) {|NA, Agent A, Agent B|}|}
    6.54          \<in> set evs"
    6.55  apply (erule otway.induct, force,
    6.56 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
    6.57 -apply blast+
    6.58 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
    6.59  done
    6.60  
    6.61  lemma Crypt_imp_OR1_Gets:
    6.62 @@ -248,8 +241,7 @@
    6.63        ==> B = C"
    6.64  apply (erule rev_mp, erule rev_mp)
    6.65  apply (erule otway.induct, force,
    6.66 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
    6.67 -apply blast+
    6.68 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
    6.69  done
    6.70  
    6.71  
    6.72 @@ -262,8 +254,7 @@
    6.73      ==> Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \<notin> parts (knows Spy evs)"
    6.74  apply (erule rev_mp)
    6.75  apply (erule otway.induct, force,
    6.76 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
    6.77 -apply blast+
    6.78 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
    6.79  done
    6.80  
    6.81  (*Crucial property: If the encrypted message appears, and A has used NA
    6.82 @@ -278,8 +269,7 @@
    6.83                             Crypt (shrK A) {|NA, Key K|},
    6.84                             Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)"
    6.85  apply (erule otway.induct, force,
    6.86 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
    6.87 -apply blast
    6.88 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
    6.89  (*OR1: it cannot be a new Nonce, contradiction.*)
    6.90  apply blast
    6.91  (*OR3*)
    6.92 @@ -321,8 +311,7 @@
    6.93  apply (frule_tac [7] Says_Server_message_form)
    6.94  apply (drule_tac [6] OR4_analz_knows_Spy)
    6.95  apply (drule_tac [4] OR2_analz_knows_Spy)
    6.96 -apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
    6.97 -apply spy_analz  (*Fake*)
    6.98 +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz)  (*Fake*)
    6.99  (*OR3, OR4, Oops*)
   6.100  apply (blast dest: unique_session_keys)+
   6.101  done
   6.102 @@ -363,8 +352,7 @@
   6.103                   \<in> set evs"
   6.104  apply (erule rev_mp)
   6.105  apply (erule otway.induct, force,
   6.106 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
   6.107 -apply blast+
   6.108 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
   6.109  done
   6.110  
   6.111  
   6.112 @@ -397,8 +385,7 @@
   6.113                      \<in> set evs)"
   6.114  apply simp
   6.115  apply (erule otway.induct, force,
   6.116 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
   6.117 -apply blast
   6.118 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
   6.119  (*OR1: it cannot be a new Nonce, contradiction.*)
   6.120  (*OR2*)
   6.121  apply blast
     7.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Fri Aug 16 17:19:43 2002 +0200
     7.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Sat Aug 17 14:55:08 2002 +0200
     7.3 @@ -90,8 +90,7 @@
     7.4  apply (rule_tac [2] otway.Nil
     7.5                      [THEN otway.OR1, THEN otway.Reception,
     7.6                       THEN otway.OR2, THEN otway.Reception,
     7.7 -                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
     7.8 -apply possibility
     7.9 +                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
    7.10  done
    7.11  
    7.12  lemma Gets_imp_Says [dest!]:
    7.13 @@ -115,8 +114,7 @@
    7.14  (*Spy never sees a good agent's shared key!*)
    7.15  lemma Spy_see_shrK [simp]:
    7.16       "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
    7.17 -apply (erule otway.induct, simp_all)
    7.18 -apply blast+
    7.19 +apply (erule otway.induct, simp_all, blast+)
    7.20  done
    7.21  
    7.22  lemma Spy_analz_shrK [simp]:
    7.23 @@ -139,9 +137,7 @@
    7.24           evs \<in> otway |]
    7.25        ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
    7.26  apply (erule rev_mp)
    7.27 -apply (erule otway.induct)
    7.28 -apply simp_all
    7.29 -apply blast
    7.30 +apply (erule otway.induct, simp_all, blast)
    7.31  done
    7.32  
    7.33  
    7.34 @@ -166,9 +162,7 @@
    7.35            (K \<in> KK | Key K \<in> analz (knows Spy evs))"
    7.36  apply (erule otway.induct, force)
    7.37  apply (frule_tac [7] Says_Server_message_form)
    7.38 -apply (drule_tac [6] OR4_analz_knows_Spy)
    7.39 -apply analz_freshK
    7.40 -apply spy_analz
    7.41 +apply (drule_tac [6] OR4_analz_knows_Spy, analz_freshK, spy_analz)
    7.42  done
    7.43  
    7.44  lemma analz_insert_freshK:
    7.45 @@ -191,8 +185,7 @@
    7.46           \<in> set evs;
    7.47          evs \<in> otway |]
    7.48       ==> A=A' & B=B' & NA=NA' & NB=NB'"
    7.49 -apply (erule rev_mp, erule rev_mp, erule otway.induct)
    7.50 -apply simp_all
    7.51 +apply (erule rev_mp, erule rev_mp, erule otway.induct, simp_all)
    7.52  (*Remaining cases: OR3 and OR4*)
    7.53  apply blast+
    7.54  done
    7.55 @@ -211,7 +204,7 @@
    7.56  apply (erule otway.induct, force)
    7.57  apply (simp_all add: ex_disj_distrib)
    7.58  (*Fake, OR3*)
    7.59 -apply blast+;
    7.60 +apply blast+
    7.61  done
    7.62  
    7.63  
    7.64 @@ -242,8 +235,7 @@
    7.65  apply (erule otway.induct, force)
    7.66  apply (frule_tac [7] Says_Server_message_form)
    7.67  apply (drule_tac [6] OR4_analz_knows_Spy)
    7.68 -apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
    7.69 -apply spy_analz  (*Fake*)
    7.70 +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz)  (*Fake*)
    7.71  (*OR3, OR4, Oops*)
    7.72  apply (blast dest: unique_session_keys)+
    7.73  done
    7.74 @@ -284,7 +276,7 @@
    7.75                     \<in> set evs)"
    7.76  apply (erule otway.induct, force, simp_all add: ex_disj_distrib)
    7.77  (*Fake, OR3*)
    7.78 -apply blast+;
    7.79 +apply blast+
    7.80  done
    7.81  
    7.82  
     8.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Fri Aug 16 17:19:43 2002 +0200
     8.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Sat Aug 17 14:55:08 2002 +0200
     8.3 @@ -98,15 +98,13 @@
     8.4  apply (rule_tac [2] otway.Nil
     8.5                      [THEN otway.OR1, THEN otway.Reception,
     8.6                       THEN otway.OR2, THEN otway.Reception,
     8.7 -                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
     8.8 -apply possibility
     8.9 +                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
    8.10  done
    8.11  
    8.12  lemma Gets_imp_Says [dest!]:
    8.13       "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
    8.14  apply (erule rev_mp)
    8.15 -apply (erule otway.induct)
    8.16 -apply auto
    8.17 +apply (erule otway.induct, auto)
    8.18  done
    8.19  
    8.20  
    8.21 @@ -142,8 +140,7 @@
    8.22  lemma Spy_see_shrK [simp]:
    8.23       "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
    8.24  apply (erule otway.induct, force,
    8.25 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
    8.26 -apply blast+
    8.27 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
    8.28  done
    8.29  
    8.30  lemma Spy_analz_shrK [simp]:
    8.31 @@ -164,8 +161,7 @@
    8.32           evs \<in> otway |]
    8.33        ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
    8.34  apply (erule rev_mp)
    8.35 -apply (erule otway.induct, simp_all)
    8.36 -apply blast
    8.37 +apply (erule otway.induct, simp_all, blast)
    8.38  done
    8.39  
    8.40  
    8.41 @@ -190,9 +186,7 @@
    8.42  apply (erule otway.induct, force)
    8.43  apply (frule_tac [7] Says_Server_message_form)
    8.44  apply (drule_tac [6] OR4_analz_knows_Spy)
    8.45 -apply (drule_tac [4] OR2_analz_knows_Spy)
    8.46 -apply analz_freshK
    8.47 -apply spy_analz
    8.48 +apply (drule_tac [4] OR2_analz_knows_Spy, analz_freshK, spy_analz)
    8.49  done
    8.50  
    8.51  lemma analz_insert_freshK:
    8.52 @@ -231,8 +225,7 @@
    8.53  apply (frule_tac [7] Says_Server_message_form)
    8.54  apply (drule_tac [6] OR4_analz_knows_Spy)
    8.55  apply (drule_tac [4] OR2_analz_knows_Spy)
    8.56 -apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
    8.57 -apply spy_analz  (*Fake*)
    8.58 +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz)  (*Fake*)
    8.59  (*OR3, OR4, Oops*)
    8.60  apply (blast dest: unique_session_keys)+
    8.61  done
    8.62 @@ -259,8 +252,7 @@
    8.63            Says A B {|NA, Agent A, Agent B,
    8.64                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \<in> set evs"
    8.65  apply (erule otway.induct, force,
    8.66 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
    8.67 -apply blast+
    8.68 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
    8.69  done
    8.70  
    8.71  
    8.72 @@ -279,8 +271,7 @@
    8.73                    Crypt (shrK A) {|NA, Key K|},
    8.74                    Crypt (shrK B) {|NB, Key K|}|}  \<in> set evs)"
    8.75  apply (erule otway.induct, force,
    8.76 -       drule_tac [4] OR2_parts_knows_Spy)
    8.77 -apply simp_all
    8.78 +       drule_tac [4] OR2_parts_knows_Spy, simp_all)
    8.79  (*Fake*)
    8.80  apply blast
    8.81  (*OR1: it cannot be a new Nonce, contradiction.*)
     9.1 --- a/src/HOL/Auth/Recur.thy	Fri Aug 16 17:19:43 2002 +0200
     9.2 +++ b/src/HOL/Auth/Recur.thy	Sat Aug 17 14:55:08 2002 +0200
     9.3 @@ -122,8 +122,7 @@
     9.4                     END|}  \<in> set evs"
     9.5  apply (intro exI bexI)
     9.6  apply (rule_tac [2] recur.Nil [THEN recur.RA1, 
     9.7 -                               THEN recur.RA3 [OF _ _ respond.One]])
     9.8 -apply possibility
     9.9 +                               THEN recur.RA3 [OF _ _ respond.One]], possibility)
    9.10  done
    9.11  
    9.12  
    9.13 @@ -131,8 +130,7 @@
    9.14  lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
    9.15          Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
    9.16                     END|}  \<in> set evs"
    9.17 -apply (cut_tac Nonce_supply2 Key_supply2)
    9.18 -apply clarify
    9.19 +apply (cut_tac Nonce_supply2 Key_supply2, clarify)
    9.20  apply (intro exI bexI)
    9.21  apply (rule_tac [2] 
    9.22            recur.Nil [THEN recur.RA1, 
    9.23 @@ -149,8 +147,7 @@
    9.24  lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
    9.25          Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
    9.26                     END|}  \<in> set evs"
    9.27 -apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1")
    9.28 -apply clarify
    9.29 +apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1", clarify)
    9.30  apply (intro exI bexI)
    9.31  apply (rule_tac [2] 
    9.32            recur.Nil [THEN recur.RA1, 
    9.33 @@ -210,8 +207,7 @@
    9.34  
    9.35  lemma Spy_see_shrK [simp]:
    9.36       "evs \<in> recur ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
    9.37 -apply (erule recur.induct)
    9.38 -apply auto
    9.39 +apply (erule recur.induct, auto)
    9.40  (*RA3.  It's ugly to call auto twice, but it seems necessary.*)
    9.41  apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies)
    9.42  done
    9.43 @@ -254,9 +250,7 @@
    9.44  apply (erule recur.induct)
    9.45  apply (drule_tac [4] RA2_analz_spies,
    9.46         drule_tac [5] respond_imp_responses,
    9.47 -       drule_tac [6] RA4_analz_spies)
    9.48 -apply analz_freshK
    9.49 -apply spy_analz
    9.50 +       drule_tac [6] RA4_analz_spies, analz_freshK, spy_analz)
    9.51  (*RA3*)
    9.52  apply (simp_all add: resp_analz_image_freshK_lemma)
    9.53  done
    9.54 @@ -289,8 +283,7 @@
    9.55         drule_tac [5] respond_imp_responses,
    9.56         drule_tac [4] RA2_parts_spies)
    9.57  (*RA3 requires a further induction*)
    9.58 -apply (erule_tac [5] responses.induct)
    9.59 -apply simp_all
    9.60 +apply (erule_tac [5] responses.induct, simp_all)
    9.61  (*Nil*)
    9.62  apply force
    9.63  (*Fake*)
    9.64 @@ -345,8 +338,7 @@
    9.65  apply (simp_all del: image_insert
    9.66               add: analz_image_freshK_simps resp_analz_image_freshK_lemma)
    9.67  (*Simplification using two distinct treatments of "image"*)
    9.68 -apply (simp add: parts_insert2)
    9.69 -apply blast
    9.70 +apply (simp add: parts_insert2, blast)
    9.71  done
    9.72  
    9.73  lemmas resp_analz_insert =
    9.74 @@ -403,8 +395,7 @@
    9.75  (*Base case of respond*)
    9.76  apply blast
    9.77  (*Inductive step of respond*)
    9.78 -apply (intro allI conjI impI)
    9.79 -apply simp_all
    9.80 +apply (intro allI conjI impI, simp_all)
    9.81  (*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*)
    9.82  apply (blast dest: unique_session_keys [OF _ respond_certificate])
    9.83  apply (blast dest!: respond_certificate)
    9.84 @@ -449,8 +440,7 @@
    9.85           (PB,RB,K) \<in> respond evs |]
    9.86        ==> Hash {|Key (shrK B), M|} \<in> parts H"
    9.87  apply (erule rev_mp)
    9.88 -apply (erule respond_imp_responses [THEN responses.induct])
    9.89 -apply auto
    9.90 +apply (erule respond_imp_responses [THEN responses.induct], auto)
    9.91  done
    9.92  
    9.93  (*Only RA1 or RA2 can have caused such a part of a message to appear.
    10.1 --- a/src/HOL/Auth/Shared.thy	Fri Aug 16 17:19:43 2002 +0200
    10.2 +++ b/src/HOL/Auth/Shared.thy	Sat Aug 17 14:55:08 2002 +0200
    10.3 @@ -39,7 +39,7 @@
    10.4  (*Lets blast_tac perform this step without needing the simplifier*)
    10.5  lemma invKey_shrK_iff [iff]:
    10.6       "(Key (invKey K) \<in> X) = (Key K \<in> X)"
    10.7 -by auto;
    10.8 +by auto
    10.9  
   10.10  (*Specialized methods*)
   10.11  
    11.1 --- a/src/HOL/Auth/TLS.thy	Fri Aug 16 17:19:43 2002 +0200
    11.2 +++ b/src/HOL/Auth/TLS.thy	Sat Aug 17 14:55:08 2002 +0200
    11.3 @@ -318,9 +318,7 @@
    11.4                      [THEN tls.ClientHello, THEN tls.ServerHello,
    11.5                       THEN tls.Certificate, THEN tls.ClientKeyExch,
    11.6                       THEN tls.ClientFinished, THEN tls.ServerFinished,
    11.7 -                     THEN tls.ClientAccepts])
    11.8 -apply possibility
    11.9 -apply blast+
   11.10 +                     THEN tls.ClientAccepts], possibility, blast+)
   11.11  done
   11.12  
   11.13  
   11.14 @@ -333,9 +331,7 @@
   11.15                      [THEN tls.ClientHello, THEN tls.ServerHello,
   11.16                       THEN tls.Certificate, THEN tls.ClientKeyExch,
   11.17                       THEN tls.ServerFinished, THEN tls.ClientFinished, 
   11.18 -                     THEN tls.ServerAccepts])
   11.19 -apply possibility
   11.20 -apply blast+
   11.21 +                     THEN tls.ServerAccepts], possibility, blast+)
   11.22  done
   11.23  
   11.24  
   11.25 @@ -348,9 +344,7 @@
   11.26  apply (rule_tac [2] tls.Nil
   11.27                      [THEN tls.ClientHello, THEN tls.ServerHello,
   11.28                       THEN tls.Certificate, THEN tls.ClientKeyExch,
   11.29 -                     THEN tls.CertVerify])
   11.30 -apply possibility
   11.31 -apply blast+
   11.32 +                     THEN tls.CertVerify], possibility, blast+)
   11.33  done
   11.34  
   11.35  
   11.36 @@ -370,9 +364,7 @@
   11.37  apply (intro exI bexI)
   11.38  apply (rule_tac [2] tls.ClientHello
   11.39                      [THEN tls.ServerHello,
   11.40 -                     THEN tls.ServerResume, THEN tls.ClientResume])
   11.41 -apply possibility
   11.42 -apply blast+
   11.43 +                     THEN tls.ServerResume, THEN tls.ClientResume], possibility, blast+)
   11.44  done
   11.45  
   11.46  
   11.47 @@ -395,8 +387,7 @@
   11.48  (*Spy never sees a good agent's private key!*)
   11.49  lemma Spy_see_priK [simp]:
   11.50       "evs \<in> tls ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
   11.51 -apply (erule tls.induct, force, simp_all)
   11.52 -apply blast
   11.53 +apply (erule tls.induct, force, simp_all, blast)
   11.54  done
   11.55  
   11.56  lemma Spy_analz_priK [simp]:
   11.57 @@ -415,8 +406,7 @@
   11.58  lemma certificate_valid:
   11.59      "[| certificate B KB \<in> parts (spies evs);  evs \<in> tls |] ==> KB = pubK B"
   11.60  apply (erule rev_mp)
   11.61 -apply (erule tls.induct, force, simp_all)
   11.62 -apply blast 
   11.63 +apply (erule tls.induct, force, simp_all, blast) 
   11.64  done
   11.65  
   11.66  lemmas CX_KB_is_pubKB = Says_imp_spies [THEN parts.Inj, THEN certificate_valid]
   11.67 @@ -467,8 +457,7 @@
   11.68           evs \<in> tls;  A \<notin> bad |]
   11.69        ==> Says A B X \<in> set evs"
   11.70  apply (erule rev_mp, erule ssubst)
   11.71 -apply (erule tls.induct, force, simp_all)
   11.72 -apply blast
   11.73 +apply (erule tls.induct, force, simp_all, blast)
   11.74  done
   11.75  
   11.76  (*Final version: B checks X using the distributed KA instead of priK A*)
   11.77 @@ -487,8 +476,7 @@
   11.78           evs \<in> tls;  A \<notin> bad |]
   11.79        ==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
   11.80  apply (erule rev_mp)
   11.81 -apply (erule tls.induct, force, simp_all)
   11.82 -apply blast
   11.83 +apply (erule tls.induct, force, simp_all, blast)
   11.84  done
   11.85  
   11.86  (*Final version using the distributed KA instead of priK A*)
    12.1 --- a/src/HOL/Auth/WooLam.thy	Fri Aug 16 17:19:43 2002 +0200
    12.2 +++ b/src/HOL/Auth/WooLam.thy	Sat Aug 17 14:55:08 2002 +0200
    12.3 @@ -74,8 +74,7 @@
    12.4  apply (intro exI bexI)
    12.5  apply (rule_tac [2] woolam.Nil
    12.6                      [THEN woolam.WL1, THEN woolam.WL2, THEN woolam.WL3,
    12.7 -                     THEN woolam.WL4, THEN woolam.WL5])
    12.8 -apply possibility
    12.9 +                     THEN woolam.WL4, THEN woolam.WL5], possibility)
   12.10  done
   12.11  
   12.12  (*Could prove forwarding lemmas for WL4, but we do not need them!*)
   12.13 @@ -88,8 +87,7 @@
   12.14  (*Spy never sees a good agent's shared key!*)
   12.15  lemma Spy_see_shrK [simp]:
   12.16       "evs \<in> woolam ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
   12.17 -apply (erule woolam.induct, force, simp_all)
   12.18 -apply blast+
   12.19 +apply (erule woolam.induct, force, simp_all, blast+)
   12.20  done
   12.21  
   12.22  lemma Spy_analz_shrK [simp]:
   12.23 @@ -110,8 +108,7 @@
   12.24       "[| Crypt (shrK A) (Nonce NB) \<in> parts (spies evs);
   12.25           A \<notin> bad;  evs \<in> woolam |]
   12.26        ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
   12.27 -apply (erule rev_mp, erule woolam.induct, force, simp_all)
   12.28 -apply blast+
   12.29 +apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
   12.30  done
   12.31  
   12.32  (*Guarantee for Server: if it gets a message containing a certificate from
   12.33 @@ -133,8 +130,7 @@
   12.34           evs \<in> woolam |]
   12.35        ==> \<exists>B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|}
   12.36               \<in> set evs"
   12.37 -apply (erule rev_mp, erule woolam.induct, force, simp_all)
   12.38 -apply blast+
   12.39 +apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
   12.40  done
   12.41  
   12.42  (*If the encrypted message appears then it originated with the Server!*)
   12.43 @@ -142,8 +138,7 @@
   12.44       "[| Crypt (shrK B) {|Agent A, NB|} \<in> parts (spies evs);
   12.45           B \<notin> bad;  evs \<in> woolam |]
   12.46        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs"
   12.47 -apply (erule rev_mp, erule woolam.induct, force, simp_all)
   12.48 -apply blast+
   12.49 +apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
   12.50  done
   12.51  
   12.52  (*Guarantee for B.  If B gets the Server's certificate then A has encrypted
   12.53 @@ -161,8 +156,7 @@
   12.54  lemma B_said_WL2:
   12.55       "[| Says B A (Nonce NB) \<in> set evs;  B \<noteq> Spy;  evs \<in> woolam |]
   12.56        ==> \<exists>A'. Says A' B (Agent A) \<in> set evs"
   12.57 -apply (erule rev_mp, erule woolam.induct, force, simp_all)
   12.58 -apply blast+
   12.59 +apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
   12.60  done
   12.61  
   12.62  
   12.63 @@ -171,9 +165,7 @@
   12.64    ==> Crypt (shrK A) (Nonce NB) \<in> parts (spies evs) &
   12.65        Says B A (Nonce NB) \<in> set evs
   12.66        --> Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
   12.67 -apply (erule rev_mp, erule woolam.induct, force, simp_all)
   12.68 -apply blast
   12.69 -apply auto
   12.70 +apply (erule rev_mp, erule woolam.induct, force, simp_all, blast, auto)
   12.71  oops
   12.72  
   12.73  end
    13.1 --- a/src/HOL/Auth/Yahalom.thy	Fri Aug 16 17:19:43 2002 +0200
    13.2 +++ b/src/HOL/Auth/Yahalom.thy	Sat Aug 17 14:55:08 2002 +0200
    13.3 @@ -94,8 +94,7 @@
    13.4                      [THEN yahalom.YM1, THEN yahalom.Reception, 
    13.5                       THEN yahalom.YM2, THEN yahalom.Reception, 
    13.6                       THEN yahalom.YM3, THEN yahalom.Reception, 
    13.7 -                     THEN yahalom.YM4])
    13.8 -apply possibility
    13.9 +                     THEN yahalom.YM4], possibility)
   13.10  done
   13.11  
   13.12  lemma Gets_imp_Says:
   13.13 @@ -135,8 +134,7 @@
   13.14  lemma Spy_see_shrK [simp]:
   13.15       "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
   13.16  apply (erule yahalom.induct, force, 
   13.17 -       drule_tac [6] YM4_parts_knows_Spy, simp_all)
   13.18 -apply blast+
   13.19 +       drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
   13.20  done
   13.21  
   13.22  lemma Spy_analz_shrK [simp]:
   13.23 @@ -170,8 +168,7 @@
   13.24       "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}  
   13.25             \<in> set evs;   evs \<in> yahalom |]                                 
   13.26        ==> K \<notin> range shrK"
   13.27 -apply (erule rev_mp, erule yahalom.induct, simp_all)
   13.28 -apply blast
   13.29 +apply (erule rev_mp, erule yahalom.induct, simp_all, blast)
   13.30  done
   13.31  
   13.32  
   13.33 @@ -197,9 +194,7 @@
   13.34            (Key K \<in> analz (Key`KK Un (knows Spy evs))) =   
   13.35            (K \<in> KK | Key K \<in> analz (knows Spy evs))"
   13.36  apply (erule yahalom.induct, force, 
   13.37 -       drule_tac [6] YM4_analz_knows_Spy)
   13.38 -apply analz_freshK
   13.39 -apply spy_analz
   13.40 +       drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
   13.41  apply (simp only: Says_Server_not_range analz_image_freshK_simps)
   13.42  done
   13.43  
   13.44 @@ -238,8 +233,7 @@
   13.45            Key K \<notin> analz (knows Spy evs)"
   13.46  apply (erule yahalom.induct, force, 
   13.47         drule_tac [6] YM4_analz_knows_Spy)
   13.48 -apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
   13.49 -apply spy_analz  (*Fake*)
   13.50 +apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)  (*Fake*)
   13.51  apply (blast dest: unique_session_keys)+  (*YM3, Oops*)
   13.52  done
   13.53  
   13.54 @@ -401,8 +395,7 @@
   13.55  (*Fake*) 
   13.56  apply spy_analz
   13.57  (*YM4*)  (** LEVEL 6 **)
   13.58 -apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl)
   13.59 -apply clarify
   13.60 +apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify)
   13.61  (*If A \<in> bad then NBa is known, therefore NBa \<noteq> NB.  Previous two steps make
   13.62    the next step faster.*)
   13.63  apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad
   13.64 @@ -423,7 +416,7 @@
   13.65            (Nonce NB \<in> analz (knows Spy evs))"
   13.66  by (simp_all del: image_insert image_Un imp_disjL
   13.67               add: analz_image_freshK_simps split_ifs
   13.68 -                  Nonce_secrecy Says_Server_KeyWithNonce);
   13.69 +                  Nonce_secrecy Says_Server_KeyWithNonce)
   13.70  
   13.71  
   13.72  (*** The Nonce NB uniquely identifies B's message. ***)
   13.73 @@ -474,8 +467,7 @@
   13.74           evs \<in> yahalom |]                                              
   13.75        ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |}  
   13.76               \<in> set evs"
   13.77 -apply (erule rev_mp, erule yahalom.induct)
   13.78 -apply auto
   13.79 +apply (erule rev_mp, erule yahalom.induct, auto)
   13.80  done
   13.81  
   13.82  
    14.1 --- a/src/HOL/Auth/Yahalom2.thy	Fri Aug 16 17:19:43 2002 +0200
    14.2 +++ b/src/HOL/Auth/Yahalom2.thy	Sat Aug 17 14:55:08 2002 +0200
    14.3 @@ -87,8 +87,7 @@
    14.4                      [THEN yahalom.YM1, THEN yahalom.Reception,
    14.5                       THEN yahalom.YM2, THEN yahalom.Reception,
    14.6                       THEN yahalom.YM3, THEN yahalom.Reception,
    14.7 -                     THEN yahalom.YM4])
    14.8 -apply possibility
    14.9 +                     THEN yahalom.YM4], possibility)
   14.10  done
   14.11  
   14.12  lemma Gets_imp_Says:
   14.13 @@ -124,8 +123,7 @@
   14.14  lemma Spy_see_shrK [simp]:
   14.15       "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
   14.16  apply (erule yahalom.induct, force,
   14.17 -       drule_tac [6] YM4_parts_knows_Spy, simp_all)
   14.18 -apply blast+
   14.19 +       drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
   14.20  done
   14.21  
   14.22  lemma Spy_analz_shrK [simp]:
   14.23 @@ -172,9 +170,7 @@
   14.24            (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
   14.25            (K \<in> KK | Key K \<in> analz (knows Spy evs))"
   14.26  apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
   14.27 -       drule_tac [6] YM4_analz_knows_Spy)
   14.28 -apply analz_freshK
   14.29 -apply spy_analz
   14.30 +       drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
   14.31  done
   14.32  
   14.33  lemma analz_insert_freshK:
   14.34 @@ -212,8 +208,7 @@
   14.35            Key K \<notin> analz (knows Spy evs)"
   14.36  apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
   14.37         drule_tac [6] YM4_analz_knows_Spy)
   14.38 -apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
   14.39 -apply spy_analz  (*Fake*)
   14.40 +apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)  (*Fake*)
   14.41  apply (blast dest: unique_session_keys)+  (*YM3, Oops*)
   14.42  done
   14.43  
    15.1 --- a/src/HOL/Auth/Yahalom_Bad.thy	Fri Aug 16 17:19:43 2002 +0200
    15.2 +++ b/src/HOL/Auth/Yahalom_Bad.thy	Sat Aug 17 14:55:08 2002 +0200
    15.3 @@ -76,8 +76,7 @@
    15.4                      [THEN yahalom.YM1, THEN yahalom.Reception,
    15.5                       THEN yahalom.YM2, THEN yahalom.Reception,
    15.6                       THEN yahalom.YM3, THEN yahalom.Reception,
    15.7 -                     THEN yahalom.YM4])
    15.8 -apply possibility
    15.9 +                     THEN yahalom.YM4], possibility)
   15.10  done
   15.11  
   15.12  lemma Gets_imp_Says:
   15.13 @@ -113,8 +112,7 @@
   15.14  lemma Spy_see_shrK [simp]:
   15.15       "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
   15.16  apply (erule yahalom.induct, force,
   15.17 -       drule_tac [6] YM4_parts_knows_Spy, simp_all)
   15.18 -apply blast+
   15.19 +       drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
   15.20  done
   15.21  
   15.22  lemma Spy_analz_shrK [simp]:
   15.23 @@ -152,9 +150,7 @@
   15.24            (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
   15.25            (K \<in> KK | Key K \<in> analz (knows Spy evs))"
   15.26  apply (erule yahalom.induct, force,
   15.27 -       drule_tac [6] YM4_analz_knows_Spy)
   15.28 -apply analz_freshK
   15.29 -apply spy_analz
   15.30 +       drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
   15.31  done
   15.32  
   15.33  lemma analz_insert_freshK: "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>
   15.34 @@ -189,8 +185,7 @@
   15.35             \<in> set evs -->
   15.36            Key K \<notin> analz (knows Spy evs)"
   15.37  apply (erule yahalom.induct, force, drule_tac [6] YM4_analz_knows_Spy)
   15.38 -apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
   15.39 -apply spy_analz  (*Fake*)
   15.40 +apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)  (*Fake*)
   15.41  apply (blast dest: unique_session_keys)  (*YM3*)
   15.42  done
   15.43