src/HOL/Auth/WooLam.thy
changeset 13507 febb8e5d2a9d
parent 11251 a6816d47f41d
child 14207 f20fbb141673
--- 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