src/HOL/Auth/Recur.thy
changeset 13507 febb8e5d2a9d
parent 11655 923e4d0d36d5
child 13922 75ae4244a596
     1.1 --- a/src/HOL/Auth/Recur.thy	Fri Aug 16 17:19:43 2002 +0200
     1.2 +++ b/src/HOL/Auth/Recur.thy	Sat Aug 17 14:55:08 2002 +0200
     1.3 @@ -122,8 +122,7 @@
     1.4                     END|}  \<in> set evs"
     1.5  apply (intro exI bexI)
     1.6  apply (rule_tac [2] recur.Nil [THEN recur.RA1, 
     1.7 -                               THEN recur.RA3 [OF _ _ respond.One]])
     1.8 -apply possibility
     1.9 +                               THEN recur.RA3 [OF _ _ respond.One]], possibility)
    1.10  done
    1.11  
    1.12  
    1.13 @@ -131,8 +130,7 @@
    1.14  lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
    1.15          Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
    1.16                     END|}  \<in> set evs"
    1.17 -apply (cut_tac Nonce_supply2 Key_supply2)
    1.18 -apply clarify
    1.19 +apply (cut_tac Nonce_supply2 Key_supply2, clarify)
    1.20  apply (intro exI bexI)
    1.21  apply (rule_tac [2] 
    1.22            recur.Nil [THEN recur.RA1, 
    1.23 @@ -149,8 +147,7 @@
    1.24  lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
    1.25          Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
    1.26                     END|}  \<in> set evs"
    1.27 -apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1")
    1.28 -apply clarify
    1.29 +apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1", clarify)
    1.30  apply (intro exI bexI)
    1.31  apply (rule_tac [2] 
    1.32            recur.Nil [THEN recur.RA1, 
    1.33 @@ -210,8 +207,7 @@
    1.34  
    1.35  lemma Spy_see_shrK [simp]:
    1.36       "evs \<in> recur ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
    1.37 -apply (erule recur.induct)
    1.38 -apply auto
    1.39 +apply (erule recur.induct, auto)
    1.40  (*RA3.  It's ugly to call auto twice, but it seems necessary.*)
    1.41  apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies)
    1.42  done
    1.43 @@ -254,9 +250,7 @@
    1.44  apply (erule recur.induct)
    1.45  apply (drule_tac [4] RA2_analz_spies,
    1.46         drule_tac [5] respond_imp_responses,
    1.47 -       drule_tac [6] RA4_analz_spies)
    1.48 -apply analz_freshK
    1.49 -apply spy_analz
    1.50 +       drule_tac [6] RA4_analz_spies, analz_freshK, spy_analz)
    1.51  (*RA3*)
    1.52  apply (simp_all add: resp_analz_image_freshK_lemma)
    1.53  done
    1.54 @@ -289,8 +283,7 @@
    1.55         drule_tac [5] respond_imp_responses,
    1.56         drule_tac [4] RA2_parts_spies)
    1.57  (*RA3 requires a further induction*)
    1.58 -apply (erule_tac [5] responses.induct)
    1.59 -apply simp_all
    1.60 +apply (erule_tac [5] responses.induct, simp_all)
    1.61  (*Nil*)
    1.62  apply force
    1.63  (*Fake*)
    1.64 @@ -345,8 +338,7 @@
    1.65  apply (simp_all del: image_insert
    1.66               add: analz_image_freshK_simps resp_analz_image_freshK_lemma)
    1.67  (*Simplification using two distinct treatments of "image"*)
    1.68 -apply (simp add: parts_insert2)
    1.69 -apply blast
    1.70 +apply (simp add: parts_insert2, blast)
    1.71  done
    1.72  
    1.73  lemmas resp_analz_insert =
    1.74 @@ -403,8 +395,7 @@
    1.75  (*Base case of respond*)
    1.76  apply blast
    1.77  (*Inductive step of respond*)
    1.78 -apply (intro allI conjI impI)
    1.79 -apply simp_all
    1.80 +apply (intro allI conjI impI, simp_all)
    1.81  (*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*)
    1.82  apply (blast dest: unique_session_keys [OF _ respond_certificate])
    1.83  apply (blast dest!: respond_certificate)
    1.84 @@ -449,8 +440,7 @@
    1.85           (PB,RB,K) \<in> respond evs |]
    1.86        ==> Hash {|Key (shrK B), M|} \<in> parts H"
    1.87  apply (erule rev_mp)
    1.88 -apply (erule respond_imp_responses [THEN responses.induct])
    1.89 -apply auto
    1.90 +apply (erule respond_imp_responses [THEN responses.induct], auto)
    1.91  done
    1.92  
    1.93  (*Only RA1 or RA2 can have caused such a part of a message to appear.