# HG changeset patch
# User paulson
# Date 1029588908 -7200
# Node ID febb8e5d2a9d2d34b7d322191b17de798daa0498
# Parent  acc18a5d2b1a9a534f130556937800dbac9072f8
tidying of Isar scripts

diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/KerberosIV.thy
--- a/src/HOL/Auth/KerberosIV.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/KerberosIV.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -44,7 +44,7 @@
                       
  (* A is the true creator of X if she has sent X and X never appeared on
     the trace before this event. Recall that traces grow from head. *)
-  Issues :: [agent , agent, msg, event list] => bool ("_ Issues _ with _ on _")
+  Issues :: [agent, agent, msg, event list] => bool ("_ Issues _ with _ on _")
    "A Issues B with X on evs == 
       \\<exists>Y. Says A B Y \\<in> set evs & X \\<in> parts {Y} &
       X \\<notin> parts (spies (takeWhile (% z. z  \\<noteq> Says A B Y) (rev evs)))"
diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/Kerberos_BAN.thy
--- a/src/HOL/Auth/Kerberos_BAN.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -89,5 +89,4 @@
              Expired Ts evso |]
           ==> Notes Spy {|Number Ts, Key K|} # evso \\<in> kerberos_ban"
 
-
 end
diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/NS_Public.thy
--- a/src/HOL/Auth/NS_Public.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/NS_Public.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -103,8 +103,7 @@
         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
        \<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
 apply (erule rev_mp)   
-apply (erule ns_public.induct, simp_all)
-apply spy_analz
+apply (erule ns_public.induct, simp_all, spy_analz)
 apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
 done
 
@@ -166,8 +165,7 @@
        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>
       \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
 apply (erule rev_mp)
-apply (erule ns_public.induct, simp_all)
-apply spy_analz
+apply (erule ns_public.induct, simp_all, spy_analz)
 apply (blast intro: no_nonce_NS1_NS2)+
 done
 
diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/NS_Public_Bad.thy
--- a/src/HOL/Auth/NS_Public_Bad.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -106,8 +106,7 @@
         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                     
        \<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
 apply (erule rev_mp)   
-apply (erule ns_public.induct, simp_all)
-apply spy_analz
+apply (erule ns_public.induct, simp_all, spy_analz)
 apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
 done
 
@@ -167,8 +166,7 @@
        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>                      
      \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
 apply (erule rev_mp, erule rev_mp)
-apply (erule ns_public.induct, simp_all)
-apply spy_analz
+apply (erule ns_public.induct, simp_all, spy_analz)
 apply (simp_all add: all_conj_distrib) (*speeds up the next step*)
 apply (blast intro: no_nonce_NS1_NS2)+
 done
@@ -197,17 +195,15 @@
 lemma "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>            
        \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs  
            \<longrightarrow> Nonce NB \<notin> analz (spies evs)"
-apply (erule ns_public.induct, simp_all)
-apply spy_analz
+apply (erule ns_public.induct, simp_all, spy_analz)
 (*NS1: by freshness*)
 apply blast
 (*NS2: by freshness and unicity of NB*)
 apply (blast intro: no_nonce_NS1_NS2)
 (*NS3: unicity of NB identifies A and NA, but not B*)
 apply clarify
-apply (frule_tac A' = "A" in 
-       Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB])
-apply auto
+apply (frule_tac A' = A in 
+       Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto)
 apply (rename_tac C B' evs3)
 oops
 
diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -85,8 +85,7 @@
 apply (intro exI bexI)
 apply (rule_tac [2] ns_shared.Nil
        [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
-	THEN ns_shared.NS4, THEN ns_shared.NS5])
-apply possibility
+	THEN ns_shared.NS4, THEN ns_shared.NS5], possibility)
 done
 
 (*This version is similar, while instantiating ?K and ?N to epsilon-terms
@@ -116,9 +115,7 @@
 (*Spy never sees another agent's shared key! (unless it's bad at start)*)
 lemma Spy_see_shrK [simp]:
      "evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)"
-apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply simp_all
-apply blast+;
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
 done
 
 lemma Spy_analz_shrK [simp]:
@@ -129,8 +126,7 @@
 (*Nobody can have used non-existent keys!*)
 lemma new_keys_not_used [rule_format, simp]:
     "evs \\<in> ns_shared \\<Longrightarrow> Key K \\<notin> used evs \\<longrightarrow> K \\<notin> keysFor (parts (spies evs))"
-apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply simp_all
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
 (*Fake, NS2, NS4, NS5*)
 apply (blast dest!: keysFor_parts_insert)+
 done
@@ -154,8 +150,7 @@
        A \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
       \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs"
 apply (erule rev_mp)
-apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply auto
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
 done
 
 lemma cert_A_form:
@@ -182,7 +177,7 @@
    \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs
        \\<or> X \\<in> analz (spies evs)"
 apply (case_tac "A \\<in> bad")
-apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj]);
+apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj])
 by (blast dest!: A_trusts_NS2 Says_Server_message_form)
 *)
 
@@ -202,8 +197,7 @@
 lemma  "\\<lbrakk>evs \\<in> ns_shared;  Kab \\<notin> range shrK\\<rbrakk> \\<Longrightarrow>
          (Crypt KAB X) \\<in> parts (spies evs) \\<and>
          Key K \\<in> parts {X} \\<longrightarrow> Key K \\<in> parts (spies evs)"
-apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply simp_all
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
 (*Fake*)
 apply (blast dest: parts_insert_subset_Un)
 (*Base, NS4 and NS5*)
@@ -222,9 +216,7 @@
              (K \\<in> KK \\<or> Key K \\<in> analz (spies evs))"
 apply (erule ns_shared.induct, force)
 apply (drule_tac [7] Says_Server_message_form)
-apply (erule_tac [4] Says_S_message_form [THEN disjE])
-apply analz_freshK
-apply spy_analz
+apply (erule_tac [4] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
 done
 
 
@@ -242,9 +234,7 @@
      "\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
        Says Server A' (Crypt (shrK A') \\<lbrace>NA', Agent B', Key K, X'\\<rbrace>) \\<in> set evs;
        evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow> A=A' \\<and> NA=NA' \\<and> B=B' \\<and> X = X'"
-apply (erule rev_mp, erule rev_mp, erule ns_shared.induct)
-apply simp_all
-apply blast+
+apply (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
 done
 
 
@@ -263,8 +253,7 @@
 apply (frule_tac [7] Says_Server_message_form)
 apply (frule_tac [4] Says_S_message_form)
 apply (erule_tac [5] disjE)
-apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs)
-apply spy_analz  (*Fake*)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)  (*Fake*)
 apply blast      (*NS2*)
 (*NS3, Server sub-case*) (**LEVEL 8 **)
 apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
@@ -295,8 +284,7 @@
                                  Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>)
               \\<in> set evs"
 apply (erule rev_mp)
-apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply auto
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
 done
 
 
@@ -307,12 +295,10 @@
       Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
       Says B A (Crypt K (Nonce NB)) \\<in> set evs"
 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply (analz_mono_contra, simp_all)
-apply blast     (*Fake*)
+apply (analz_mono_contra, simp_all, blast)     (*Fake*)
 (*NS2: contradiction from the assumptions
   Key K \\<notin> used evs2  and Crypt K (Nonce NB) \\<in> parts (spies evs2) *)
-apply (force dest!: Crypt_imp_keysFor)
-apply blast     (*NS3*)
+apply (force dest!: Crypt_imp_keysFor, blast)     (*NS3*)
 (*NS4*)
 apply (blast dest!: B_trusts_NS3
 	     dest: Says_imp_knows_Spy [THEN analz.Inj]
@@ -338,10 +324,8 @@
      Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow>
      Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
      (\\<exists>A'. Says A' B X \\<in> set evs)"
-apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply analz_mono_contra
-apply (simp_all add: ex_disj_distrib)
-apply blast  (*Fake*)
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra)
+apply (simp_all add: ex_disj_distrib, blast)  (*Fake*)
 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
 apply blast  (*NS3*)
 (*NS4*)
@@ -359,10 +343,7 @@
 			    Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>) \\<in> set evs \\<longrightarrow>
      Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs) \\<longrightarrow>
      Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs"
-apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply analz_mono_contra
-apply simp_all
-apply blast  (*Fake*)
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast)  (*Fake*)
 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
 apply (blast dest!: cert_A_form) (*NS3*)
 (*NS5*)
diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/OtwayRees.thy
--- a/src/HOL/Auth/OtwayRees.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/OtwayRees.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -98,15 +98,13 @@
 apply (rule_tac [2] otway.Nil
                     [THEN otway.OR1, THEN otway.Reception,
                      THEN otway.OR2, THEN otway.Reception,
-                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
-apply possibility
+                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
 done
 
 lemma Gets_imp_Says [dest!]:
      "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
 apply (erule rev_mp)
-apply (erule otway.induct)
-apply auto
+apply (erule otway.induct, auto)
 done
 
 
@@ -141,8 +139,7 @@
 lemma Spy_see_shrK [simp]:
      "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
 done
 
 lemma Spy_analz_shrK [simp]:
@@ -162,8 +159,7 @@
      "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
          evs \<in> otway |]
       ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
-apply (erule rev_mp, erule otway.induct, simp_all)
-apply blast
+apply (erule rev_mp, erule otway.induct, simp_all, blast)
 done
 
 
@@ -188,9 +184,7 @@
 apply (erule otway.induct, force)
 apply (frule_tac [7] Says_Server_message_form)
 apply (drule_tac [6] OR4_analz_knows_Spy)
-apply (drule_tac [4] OR2_analz_knows_Spy)
-apply analz_freshK
-apply spy_analz
+apply (drule_tac [4] OR2_analz_knows_Spy, analz_freshK, spy_analz)
 done
 
 
@@ -225,8 +219,7 @@
                  Crypt (shrK A) {|NA, Agent A, Agent B|}|}
         \<in> set evs"
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
 done
 
 lemma Crypt_imp_OR1_Gets:
@@ -248,8 +241,7 @@
       ==> B = C"
 apply (erule rev_mp, erule rev_mp)
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
 done
 
 
@@ -262,8 +254,7 @@
     ==> Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \<notin> parts (knows Spy evs)"
 apply (erule rev_mp)
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
 done
 
 (*Crucial property: If the encrypted message appears, and A has used NA
@@ -278,8 +269,7 @@
                            Crypt (shrK A) {|NA, Key K|},
                            Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)"
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast
+       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
 (*OR1: it cannot be a new Nonce, contradiction.*)
 apply blast
 (*OR3*)
@@ -321,8 +311,7 @@
 apply (frule_tac [7] Says_Server_message_form)
 apply (drule_tac [6] OR4_analz_knows_Spy)
 apply (drule_tac [4] OR2_analz_knows_Spy)
-apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
-apply spy_analz  (*Fake*)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz)  (*Fake*)
 (*OR3, OR4, Oops*)
 apply (blast dest: unique_session_keys)+
 done
@@ -363,8 +352,7 @@
                  \<in> set evs"
 apply (erule rev_mp)
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
 done
 
 
@@ -397,8 +385,7 @@
                     \<in> set evs)"
 apply simp
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast
+       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
 (*OR1: it cannot be a new Nonce, contradiction.*)
 (*OR2*)
 apply blast
diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/OtwayRees_AN.thy
--- a/src/HOL/Auth/OtwayRees_AN.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -90,8 +90,7 @@
 apply (rule_tac [2] otway.Nil
                     [THEN otway.OR1, THEN otway.Reception,
                      THEN otway.OR2, THEN otway.Reception,
-                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
-apply possibility
+                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
 done
 
 lemma Gets_imp_Says [dest!]:
@@ -115,8 +114,7 @@
 (*Spy never sees a good agent's shared key!*)
 lemma Spy_see_shrK [simp]:
      "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
-apply (erule otway.induct, simp_all)
-apply blast+
+apply (erule otway.induct, simp_all, blast+)
 done
 
 lemma Spy_analz_shrK [simp]:
@@ -139,9 +137,7 @@
          evs \<in> otway |]
       ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
 apply (erule rev_mp)
-apply (erule otway.induct)
-apply simp_all
-apply blast
+apply (erule otway.induct, simp_all, blast)
 done
 
 
@@ -166,9 +162,7 @@
           (K \<in> KK | Key K \<in> analz (knows Spy evs))"
 apply (erule otway.induct, force)
 apply (frule_tac [7] Says_Server_message_form)
-apply (drule_tac [6] OR4_analz_knows_Spy)
-apply analz_freshK
-apply spy_analz
+apply (drule_tac [6] OR4_analz_knows_Spy, analz_freshK, spy_analz)
 done
 
 lemma analz_insert_freshK:
@@ -191,8 +185,7 @@
          \<in> set evs;
         evs \<in> otway |]
      ==> A=A' & B=B' & NA=NA' & NB=NB'"
-apply (erule rev_mp, erule rev_mp, erule otway.induct)
-apply simp_all
+apply (erule rev_mp, erule rev_mp, erule otway.induct, simp_all)
 (*Remaining cases: OR3 and OR4*)
 apply blast+
 done
@@ -211,7 +204,7 @@
 apply (erule otway.induct, force)
 apply (simp_all add: ex_disj_distrib)
 (*Fake, OR3*)
-apply blast+;
+apply blast+
 done
 
 
@@ -242,8 +235,7 @@
 apply (erule otway.induct, force)
 apply (frule_tac [7] Says_Server_message_form)
 apply (drule_tac [6] OR4_analz_knows_Spy)
-apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
-apply spy_analz  (*Fake*)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz)  (*Fake*)
 (*OR3, OR4, Oops*)
 apply (blast dest: unique_session_keys)+
 done
@@ -284,7 +276,7 @@
                    \<in> set evs)"
 apply (erule otway.induct, force, simp_all add: ex_disj_distrib)
 (*Fake, OR3*)
-apply blast+;
+apply blast+
 done
 
 
diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/OtwayRees_Bad.thy
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -98,15 +98,13 @@
 apply (rule_tac [2] otway.Nil
                     [THEN otway.OR1, THEN otway.Reception,
                      THEN otway.OR2, THEN otway.Reception,
-                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
-apply possibility
+                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
 done
 
 lemma Gets_imp_Says [dest!]:
      "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
 apply (erule rev_mp)
-apply (erule otway.induct)
-apply auto
+apply (erule otway.induct, auto)
 done
 
 
@@ -142,8 +140,7 @@
 lemma Spy_see_shrK [simp]:
      "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
 done
 
 lemma Spy_analz_shrK [simp]:
@@ -164,8 +161,7 @@
          evs \<in> otway |]
       ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
 apply (erule rev_mp)
-apply (erule otway.induct, simp_all)
-apply blast
+apply (erule otway.induct, simp_all, blast)
 done
 
 
@@ -190,9 +186,7 @@
 apply (erule otway.induct, force)
 apply (frule_tac [7] Says_Server_message_form)
 apply (drule_tac [6] OR4_analz_knows_Spy)
-apply (drule_tac [4] OR2_analz_knows_Spy)
-apply analz_freshK
-apply spy_analz
+apply (drule_tac [4] OR2_analz_knows_Spy, analz_freshK, spy_analz)
 done
 
 lemma analz_insert_freshK:
@@ -231,8 +225,7 @@
 apply (frule_tac [7] Says_Server_message_form)
 apply (drule_tac [6] OR4_analz_knows_Spy)
 apply (drule_tac [4] OR2_analz_knows_Spy)
-apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
-apply spy_analz  (*Fake*)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz)  (*Fake*)
 (*OR3, OR4, Oops*)
 apply (blast dest: unique_session_keys)+
 done
@@ -259,8 +252,7 @@
           Says A B {|NA, Agent A, Agent B,
                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \<in> set evs"
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
 done
 
 
@@ -279,8 +271,7 @@
                   Crypt (shrK A) {|NA, Key K|},
                   Crypt (shrK B) {|NB, Key K|}|}  \<in> set evs)"
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy)
-apply simp_all
+       drule_tac [4] OR2_parts_knows_Spy, simp_all)
 (*Fake*)
 apply blast
 (*OR1: it cannot be a new Nonce, contradiction.*)
diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Recur.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/Recur.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -122,8 +122,7 @@
                    END|}  \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] recur.Nil [THEN recur.RA1, 
-                               THEN recur.RA3 [OF _ _ respond.One]])
-apply possibility
+                               THEN recur.RA3 [OF _ _ respond.One]], possibility)
 done
 
 
@@ -131,8 +130,7 @@
 lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
         Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
                    END|}  \<in> set evs"
-apply (cut_tac Nonce_supply2 Key_supply2)
-apply clarify
+apply (cut_tac Nonce_supply2 Key_supply2, clarify)
 apply (intro exI bexI)
 apply (rule_tac [2] 
           recur.Nil [THEN recur.RA1, 
@@ -149,8 +147,7 @@
 lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
         Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
                    END|}  \<in> set evs"
-apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1")
-apply clarify
+apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1", clarify)
 apply (intro exI bexI)
 apply (rule_tac [2] 
           recur.Nil [THEN recur.RA1, 
@@ -210,8 +207,7 @@
 
 lemma Spy_see_shrK [simp]:
      "evs \<in> recur ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
-apply (erule recur.induct)
-apply auto
+apply (erule recur.induct, auto)
 (*RA3.  It's ugly to call auto twice, but it seems necessary.*)
 apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies)
 done
@@ -254,9 +250,7 @@
 apply (erule recur.induct)
 apply (drule_tac [4] RA2_analz_spies,
        drule_tac [5] respond_imp_responses,
-       drule_tac [6] RA4_analz_spies)
-apply analz_freshK
-apply spy_analz
+       drule_tac [6] RA4_analz_spies, analz_freshK, spy_analz)
 (*RA3*)
 apply (simp_all add: resp_analz_image_freshK_lemma)
 done
@@ -289,8 +283,7 @@
        drule_tac [5] respond_imp_responses,
        drule_tac [4] RA2_parts_spies)
 (*RA3 requires a further induction*)
-apply (erule_tac [5] responses.induct)
-apply simp_all
+apply (erule_tac [5] responses.induct, simp_all)
 (*Nil*)
 apply force
 (*Fake*)
@@ -345,8 +338,7 @@
 apply (simp_all del: image_insert
              add: analz_image_freshK_simps resp_analz_image_freshK_lemma)
 (*Simplification using two distinct treatments of "image"*)
-apply (simp add: parts_insert2)
-apply blast
+apply (simp add: parts_insert2, blast)
 done
 
 lemmas resp_analz_insert =
@@ -403,8 +395,7 @@
 (*Base case of respond*)
 apply blast
 (*Inductive step of respond*)
-apply (intro allI conjI impI)
-apply simp_all
+apply (intro allI conjI impI, simp_all)
 (*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*)
 apply (blast dest: unique_session_keys [OF _ respond_certificate])
 apply (blast dest!: respond_certificate)
@@ -449,8 +440,7 @@
          (PB,RB,K) \<in> respond evs |]
       ==> Hash {|Key (shrK B), M|} \<in> parts H"
 apply (erule rev_mp)
-apply (erule respond_imp_responses [THEN responses.induct])
-apply auto
+apply (erule respond_imp_responses [THEN responses.induct], auto)
 done
 
 (*Only RA1 or RA2 can have caused such a part of a message to appear.
diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/Shared.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -39,7 +39,7 @@
 (*Lets blast_tac perform this step without needing the simplifier*)
 lemma invKey_shrK_iff [iff]:
      "(Key (invKey K) \<in> X) = (Key K \<in> X)"
-by auto;
+by auto
 
 (*Specialized methods*)
 
diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/TLS.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -318,9 +318,7 @@
                     [THEN tls.ClientHello, THEN tls.ServerHello,
                      THEN tls.Certificate, THEN tls.ClientKeyExch,
                      THEN tls.ClientFinished, THEN tls.ServerFinished,
-                     THEN tls.ClientAccepts])
-apply possibility
-apply blast+
+                     THEN tls.ClientAccepts], possibility, blast+)
 done
 
 
@@ -333,9 +331,7 @@
                     [THEN tls.ClientHello, THEN tls.ServerHello,
                      THEN tls.Certificate, THEN tls.ClientKeyExch,
                      THEN tls.ServerFinished, THEN tls.ClientFinished, 
-                     THEN tls.ServerAccepts])
-apply possibility
-apply blast+
+                     THEN tls.ServerAccepts], possibility, blast+)
 done
 
 
@@ -348,9 +344,7 @@
 apply (rule_tac [2] tls.Nil
                     [THEN tls.ClientHello, THEN tls.ServerHello,
                      THEN tls.Certificate, THEN tls.ClientKeyExch,
-                     THEN tls.CertVerify])
-apply possibility
-apply blast+
+                     THEN tls.CertVerify], possibility, blast+)
 done
 
 
@@ -370,9 +364,7 @@
 apply (intro exI bexI)
 apply (rule_tac [2] tls.ClientHello
                     [THEN tls.ServerHello,
-                     THEN tls.ServerResume, THEN tls.ClientResume])
-apply possibility
-apply blast+
+                     THEN tls.ServerResume, THEN tls.ClientResume], possibility, blast+)
 done
 
 
@@ -395,8 +387,7 @@
 (*Spy never sees a good agent's private key!*)
 lemma Spy_see_priK [simp]:
      "evs \<in> tls ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
-apply (erule tls.induct, force, simp_all)
-apply blast
+apply (erule tls.induct, force, simp_all, blast)
 done
 
 lemma Spy_analz_priK [simp]:
@@ -415,8 +406,7 @@
 lemma certificate_valid:
     "[| certificate B KB \<in> parts (spies evs);  evs \<in> tls |] ==> KB = pubK B"
 apply (erule rev_mp)
-apply (erule tls.induct, force, simp_all)
-apply blast 
+apply (erule tls.induct, force, simp_all, blast) 
 done
 
 lemmas CX_KB_is_pubKB = Says_imp_spies [THEN parts.Inj, THEN certificate_valid]
@@ -467,8 +457,7 @@
          evs \<in> tls;  A \<notin> bad |]
       ==> Says A B X \<in> set evs"
 apply (erule rev_mp, erule ssubst)
-apply (erule tls.induct, force, simp_all)
-apply blast
+apply (erule tls.induct, force, simp_all, blast)
 done
 
 (*Final version: B checks X using the distributed KA instead of priK A*)
@@ -487,8 +476,7 @@
          evs \<in> tls;  A \<notin> bad |]
       ==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
 apply (erule rev_mp)
-apply (erule tls.induct, force, simp_all)
-apply blast
+apply (erule tls.induct, force, simp_all, blast)
 done
 
 (*Final version using the distributed KA instead of priK A*)
diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/WooLam.thy
--- a/src/HOL/Auth/WooLam.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/WooLam.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -74,8 +74,7 @@
 apply (intro exI bexI)
 apply (rule_tac [2] woolam.Nil
                     [THEN woolam.WL1, THEN woolam.WL2, THEN woolam.WL3,
-                     THEN woolam.WL4, THEN woolam.WL5])
-apply possibility
+                     THEN woolam.WL4, THEN woolam.WL5], possibility)
 done
 
 (*Could prove forwarding lemmas for WL4, but we do not need them!*)
@@ -88,8 +87,7 @@
 (*Spy never sees a good agent's shared key!*)
 lemma Spy_see_shrK [simp]:
      "evs \<in> woolam ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
-apply (erule woolam.induct, force, simp_all)
-apply blast+
+apply (erule woolam.induct, force, simp_all, blast+)
 done
 
 lemma Spy_analz_shrK [simp]:
@@ -110,8 +108,7 @@
      "[| Crypt (shrK A) (Nonce NB) \<in> parts (spies evs);
          A \<notin> bad;  evs \<in> woolam |]
       ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
-apply (erule rev_mp, erule woolam.induct, force, simp_all)
-apply blast+
+apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
 done
 
 (*Guarantee for Server: if it gets a message containing a certificate from
@@ -133,8 +130,7 @@
          evs \<in> woolam |]
       ==> \<exists>B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|}
              \<in> set evs"
-apply (erule rev_mp, erule woolam.induct, force, simp_all)
-apply blast+
+apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
 done
 
 (*If the encrypted message appears then it originated with the Server!*)
@@ -142,8 +138,7 @@
      "[| Crypt (shrK B) {|Agent A, NB|} \<in> parts (spies evs);
          B \<notin> bad;  evs \<in> woolam |]
       ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs"
-apply (erule rev_mp, erule woolam.induct, force, simp_all)
-apply blast+
+apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
 done
 
 (*Guarantee for B.  If B gets the Server's certificate then A has encrypted
@@ -161,8 +156,7 @@
 lemma B_said_WL2:
      "[| Says B A (Nonce NB) \<in> set evs;  B \<noteq> Spy;  evs \<in> woolam |]
       ==> \<exists>A'. Says A' B (Agent A) \<in> set evs"
-apply (erule rev_mp, erule woolam.induct, force, simp_all)
-apply blast+
+apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
 done
 
 
@@ -171,9 +165,7 @@
   ==> Crypt (shrK A) (Nonce NB) \<in> parts (spies evs) &
       Says B A (Nonce NB) \<in> set evs
       --> Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
-apply (erule rev_mp, erule woolam.induct, force, simp_all)
-apply blast
-apply auto
+apply (erule rev_mp, erule woolam.induct, force, simp_all, blast, auto)
 oops
 
 end
diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -94,8 +94,7 @@
                     [THEN yahalom.YM1, THEN yahalom.Reception, 
                      THEN yahalom.YM2, THEN yahalom.Reception, 
                      THEN yahalom.YM3, THEN yahalom.Reception, 
-                     THEN yahalom.YM4])
-apply possibility
+                     THEN yahalom.YM4], possibility)
 done
 
 lemma Gets_imp_Says:
@@ -135,8 +134,7 @@
 lemma Spy_see_shrK [simp]:
      "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
 apply (erule yahalom.induct, force, 
-       drule_tac [6] YM4_parts_knows_Spy, simp_all)
-apply blast+
+       drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
 done
 
 lemma Spy_analz_shrK [simp]:
@@ -170,8 +168,7 @@
      "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}  
            \<in> set evs;   evs \<in> yahalom |]                                 
       ==> K \<notin> range shrK"
-apply (erule rev_mp, erule yahalom.induct, simp_all)
-apply blast
+apply (erule rev_mp, erule yahalom.induct, simp_all, blast)
 done
 
 
@@ -197,9 +194,7 @@
           (Key K \<in> analz (Key`KK Un (knows Spy evs))) =   
           (K \<in> KK | Key K \<in> analz (knows Spy evs))"
 apply (erule yahalom.induct, force, 
-       drule_tac [6] YM4_analz_knows_Spy)
-apply analz_freshK
-apply spy_analz
+       drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
 apply (simp only: Says_Server_not_range analz_image_freshK_simps)
 done
 
@@ -238,8 +233,7 @@
           Key K \<notin> analz (knows Spy evs)"
 apply (erule yahalom.induct, force, 
        drule_tac [6] YM4_analz_knows_Spy)
-apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
-apply spy_analz  (*Fake*)
+apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)  (*Fake*)
 apply (blast dest: unique_session_keys)+  (*YM3, Oops*)
 done
 
@@ -401,8 +395,7 @@
 (*Fake*) 
 apply spy_analz
 (*YM4*)  (** LEVEL 6 **)
-apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl)
-apply clarify
+apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify)
 (*If A \<in> bad then NBa is known, therefore NBa \<noteq> NB.  Previous two steps make
   the next step faster.*)
 apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad
@@ -423,7 +416,7 @@
           (Nonce NB \<in> analz (knows Spy evs))"
 by (simp_all del: image_insert image_Un imp_disjL
              add: analz_image_freshK_simps split_ifs
-                  Nonce_secrecy Says_Server_KeyWithNonce);
+                  Nonce_secrecy Says_Server_KeyWithNonce)
 
 
 (*** The Nonce NB uniquely identifies B's message. ***)
@@ -474,8 +467,7 @@
          evs \<in> yahalom |]                                              
       ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |}  
              \<in> set evs"
-apply (erule rev_mp, erule yahalom.induct)
-apply auto
+apply (erule rev_mp, erule yahalom.induct, auto)
 done
 
 
diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/Yahalom2.thy
--- a/src/HOL/Auth/Yahalom2.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/Yahalom2.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -87,8 +87,7 @@
                     [THEN yahalom.YM1, THEN yahalom.Reception,
                      THEN yahalom.YM2, THEN yahalom.Reception,
                      THEN yahalom.YM3, THEN yahalom.Reception,
-                     THEN yahalom.YM4])
-apply possibility
+                     THEN yahalom.YM4], possibility)
 done
 
 lemma Gets_imp_Says:
@@ -124,8 +123,7 @@
 lemma Spy_see_shrK [simp]:
      "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
 apply (erule yahalom.induct, force,
-       drule_tac [6] YM4_parts_knows_Spy, simp_all)
-apply blast+
+       drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
 done
 
 lemma Spy_analz_shrK [simp]:
@@ -172,9 +170,7 @@
           (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
           (K \<in> KK | Key K \<in> analz (knows Spy evs))"
 apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
-       drule_tac [6] YM4_analz_knows_Spy)
-apply analz_freshK
-apply spy_analz
+       drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
 done
 
 lemma analz_insert_freshK:
@@ -212,8 +208,7 @@
           Key K \<notin> analz (knows Spy evs)"
 apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
        drule_tac [6] YM4_analz_knows_Spy)
-apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
-apply spy_analz  (*Fake*)
+apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)  (*Fake*)
 apply (blast dest: unique_session_keys)+  (*YM3, Oops*)
 done
 
diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/Yahalom_Bad.thy
--- a/src/HOL/Auth/Yahalom_Bad.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/Yahalom_Bad.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -76,8 +76,7 @@
                     [THEN yahalom.YM1, THEN yahalom.Reception,
                      THEN yahalom.YM2, THEN yahalom.Reception,
                      THEN yahalom.YM3, THEN yahalom.Reception,
-                     THEN yahalom.YM4])
-apply possibility
+                     THEN yahalom.YM4], possibility)
 done
 
 lemma Gets_imp_Says:
@@ -113,8 +112,7 @@
 lemma Spy_see_shrK [simp]:
      "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
 apply (erule yahalom.induct, force,
-       drule_tac [6] YM4_parts_knows_Spy, simp_all)
-apply blast+
+       drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
 done
 
 lemma Spy_analz_shrK [simp]:
@@ -152,9 +150,7 @@
           (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
           (K \<in> KK | Key K \<in> analz (knows Spy evs))"
 apply (erule yahalom.induct, force,
-       drule_tac [6] YM4_analz_knows_Spy)
-apply analz_freshK
-apply spy_analz
+       drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
 done
 
 lemma analz_insert_freshK: "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>
@@ -189,8 +185,7 @@
            \<in> set evs -->
           Key K \<notin> analz (knows Spy evs)"
 apply (erule yahalom.induct, force, drule_tac [6] YM4_analz_knows_Spy)
-apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
-apply spy_analz  (*Fake*)
+apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)  (*Fake*)
 apply (blast dest: unique_session_keys)  (*YM3*)
 done