--- 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.