Ran expandshort
authorpaulson
Fri Nov 08 14:13:56 1996 +0100 (1996-11-08)
changeset 2170c5e460f1ebb4
parent 2169 31ba286f2307
child 2171 91b4161a28e5
Ran expandshort
src/HOL/Auth/Message.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Fri Nov 08 14:07:56 1996 +0100
     1.2 +++ b/src/HOL/Auth/Message.ML	Fri Nov 08 14:13:56 1996 +0100
     1.3 @@ -664,7 +664,7 @@
     1.4  \             Key K ~: analz G |]                                   \
     1.5  \          ==> Crypt Y K : parts G Un parts H";
     1.6  by (dtac (impOfSubs Fake_parts_insert) 1);
     1.7 -ba 1;
     1.8 +by (assume_tac 1);
     1.9  by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]
    1.10                        addss (!simpset)) 1);
    1.11  qed "Crypt_Fake_parts_insert";
     2.1 --- a/src/HOL/Auth/NS_Shared.ML	Fri Nov 08 14:07:56 1996 +0100
     2.2 +++ b/src/HOL/Auth/NS_Shared.ML	Fri Nov 08 14:13:56 1996 +0100
     2.3 @@ -70,9 +70,9 @@
     2.4  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
     2.5  fun parts_induct_tac i = SELECT_GOAL
     2.6      (DETERM (etac ns_shared.induct 1 THEN parts_Fake_tac THEN
     2.7 -	     (*Fake message*)
     2.8 -	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
     2.9 -					   impOfSubs Fake_parts_insert]
    2.10 +             (*Fake message*)
    2.11 +             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    2.12 +                                           impOfSubs Fake_parts_insert]
    2.13                                      addss (!simpset)) 2)) THEN
    2.14       (*Base case*)
    2.15       fast_tac (!claset addss (!simpset)) 1 THEN
    2.16 @@ -143,10 +143,10 @@
    2.17  by (parts_induct_tac 1);
    2.18  by (REPEAT_FIRST
    2.19      (fast_tac (!claset addSEs partsEs
    2.20 -	               addSDs  [Says_imp_sees_Spy RS parts.Inj]
    2.21 -		       addDs  [impOfSubs analz_subset_parts,
    2.22 -			       impOfSubs parts_insert_subset_Un, Suc_leD]
    2.23 -		       addss (!simpset))));
    2.24 +                       addSDs  [Says_imp_sees_Spy RS parts.Inj]
    2.25 +                       addDs  [impOfSubs analz_subset_parts,
    2.26 +                               impOfSubs parts_insert_subset_Un, Suc_leD]
    2.27 +                       addss (!simpset))));
    2.28  qed_spec_mp "new_nonces_not_seen";
    2.29  Addsimps [new_nonces_not_seen];
    2.30  
    2.31 @@ -230,7 +230,7 @@
    2.32  by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
    2.33  by (fast_tac (!claset addEs  partsEs
    2.34                        addSDs [A_trust_NS2, Says_Server_message_form]
    2.35 -		      addIs [Says_imp_old_keys]
    2.36 +                      addIs [Says_imp_old_keys]
    2.37                        addss (!simpset)) 1);
    2.38  qed "Says_S_message_form";
    2.39  
    2.40 @@ -342,7 +342,7 @@
    2.41  (*Duplicate the assumption*)
    2.42  by (forw_inst_tac [("psi", "ALL A.?P(A)")] asm_rl 1);
    2.43  by (fast_tac (!claset addSDs [ spec] 
    2.44 -	              delrules [conjI] addss (!simpset)) 1);
    2.45 +                      delrules [conjI] addss (!simpset)) 1);
    2.46  qed "unique_session_keys";
    2.47  
    2.48  
    2.49 @@ -373,16 +373,16 @@
    2.50  (*NS3 and Oops subcases*) (**LEVEL 7 **)
    2.51  by (step_tac (!claset delrules [impCE]) 1);
    2.52  by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
    2.53 -be conjE 2;
    2.54 +by (etac conjE 2);
    2.55  by (mp_tac 2);
    2.56  (**LEVEL 11 **)
    2.57  by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trust_NS2] 2);
    2.58 -ba 3;
    2.59 +by (assume_tac 3);
    2.60  by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 2);
    2.61  by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 2);
    2.62  (*NS3*)
    2.63  by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trust_NS2] 1);
    2.64 -ba 2;
    2.65 +by (assume_tac 2);
    2.66  by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 1);
    2.67  by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
    2.68  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    2.69 @@ -460,10 +460,10 @@
    2.70  by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
    2.71  (*Contradiction from the assumption   
    2.72     Crypt (Nonce NB) (newK evsa) : parts (sees lost Spy evsa) *)
    2.73 -bd Crypt_imp_invKey_keysFor 1;
    2.74 +by (dtac Crypt_imp_invKey_keysFor 1);
    2.75  (**LEVEL 10**)
    2.76  by (Asm_full_simp_tac 1);
    2.77 -br disjI1 1;
    2.78 +by (rtac disjI1 1);
    2.79  by (thin_tac "?PP-->?QQ" 1);
    2.80  by (case_tac "Ba : lost" 1);
    2.81  by (dtac Says_Crypt_lost 1 THEN assume_tac 1 THEN Fast_tac 1);
    2.82 @@ -480,5 +480,5 @@
    2.83  \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
    2.84  \        ==> Says B A (Crypt (Nonce NB) K) : set_of_list evs";
    2.85  by (fast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
    2.86 -		      addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1);
    2.87 +                      addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1);
    2.88  qed "A_trust_NS4";
     3.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Nov 08 14:07:56 1996 +0100
     3.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Nov 08 14:13:56 1996 +0100
     3.3 @@ -79,9 +79,9 @@
     3.4  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
     3.5  fun parts_induct_tac i = SELECT_GOAL
     3.6      (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN
     3.7 -	     (*Fake message*)
     3.8 -	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
     3.9 -					   impOfSubs Fake_parts_insert]
    3.10 +             (*Fake message*)
    3.11 +             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    3.12 +                                           impOfSubs Fake_parts_insert]
    3.13                                      addss (!simpset)) 2)) THEN
    3.14       (*Base case*)
    3.15       fast_tac (!claset addss (!simpset)) 1 THEN
    3.16 @@ -164,10 +164,10 @@
    3.17  (*Fake and Oops: these messages send unknown (X) components*)
    3.18  by (EVERY
    3.19      (map (fast_tac
    3.20 -	  (!claset addDs [impOfSubs analz_subset_parts,
    3.21 -			  impOfSubs (analz_subset_parts RS keysFor_mono),
    3.22 -			  impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    3.23 -			  Suc_leD]
    3.24 +          (!claset addDs [impOfSubs analz_subset_parts,
    3.25 +                          impOfSubs (analz_subset_parts RS keysFor_mono),
    3.26 +                          impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    3.27 +                          Suc_leD]
    3.28                     addss (!simpset))) [3,1]));
    3.29  (*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
    3.30  by (fast_tac
    3.31 @@ -340,8 +340,8 @@
    3.32  by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
    3.33  (*Oops*) (** LEVEL 6 **)
    3.34  by (fast_tac (!claset delrules [disjE] 
    3.35 -		      addDs [unique_session_keys]
    3.36 -	              addss (!simpset)) 1);
    3.37 +                      addDs [unique_session_keys]
    3.38 +                      addss (!simpset)) 1);
    3.39  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    3.40  
    3.41  
    3.42 @@ -465,8 +465,8 @@
    3.43         REPEAT_DETERM (etac MPair_analz 1) THEN
    3.44         THEN_BEST_FIRST 
    3.45           (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
    3.46 - 	 (has_fewer_prems 1, size_of_thm)
    3.47 -	 (Step_tac 1));
    3.48 +         (has_fewer_prems 1, size_of_thm)
    3.49 +         (Step_tac 1));
    3.50  
    3.51  
    3.52  (*Variant useful for proving secrecy of NB*)
    3.53 @@ -496,12 +496,12 @@
    3.54       dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
    3.55       mp_tac));
    3.56  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    3.57 -			     impOfSubs Fake_parts_insert]
    3.58 -	              addss (!simpset)) 2);
    3.59 +                             impOfSubs Fake_parts_insert]
    3.60 +                      addss (!simpset)) 2);
    3.61  by (ALLGOALS Asm_simp_tac);
    3.62  by (fast_tac (!claset addss (!simpset)) 1);
    3.63  by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
    3.64 -	              addSIs [parts_insertI]
    3.65 +                      addSIs [parts_insertI]
    3.66                        addSEs partsEs
    3.67                        addEs [Says_imp_old_nonces RS less_irrefl]
    3.68                        addss (!simpset)) 1);
    3.69 @@ -539,7 +539,7 @@
    3.70  by (Step_tac 1);
    3.71  by (lost_tac "A" 1);
    3.72  by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
    3.73 -			     A_trust_YM3]) 1);
    3.74 +                             A_trust_YM3]) 1);
    3.75  val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
    3.76  
    3.77  
    3.78 @@ -571,7 +571,7 @@
    3.79  by (Step_tac 1);
    3.80  by (lost_tac "A" 1);
    3.81  by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
    3.82 -			     A_trust_YM3]) 1);
    3.83 +                             A_trust_YM3]) 1);
    3.84  result() RS mp RSN (2, rev_mp);
    3.85  
    3.86  
    3.87 @@ -609,8 +609,8 @@
    3.88     (Safe_step_tac ORELSE' (dtac spec THEN' mp_tac) ORELSE'
    3.89      assume_tac ORELSE'
    3.90      depth_tac (!claset delrules [conjI]
    3.91 -		       addSIs [exI, impOfSubs (subset_insertI RS analz_mono),
    3.92 -			       impOfSubs (Un_upper2 RS analz_mono)]) 2)) i;
    3.93 +                       addSIs [exI, impOfSubs (subset_insertI RS analz_mono),
    3.94 +                               impOfSubs (Un_upper2 RS analz_mono)]) 2)) i;
    3.95  
    3.96  (*The only nonces that can be found with the help of session keys are
    3.97    those distributed as nonce NB by the Server.  The form of the theorem
    3.98 @@ -628,8 +628,8 @@
    3.99      (asm_simp_tac 
   3.100       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   3.101                            analz_image_newK,
   3.102 -			  insert_Key_singleton, insert_Key_image]
   3.103 -			 @ pushes)
   3.104 +                          insert_Key_singleton, insert_Key_image]
   3.105 +                         @ pushes)
   3.106                 setloop split_tac [expand_if])));
   3.107  (*Base*)
   3.108  by (fast_tac (!claset addss (!simpset)) 1);
   3.109 @@ -639,20 +639,20 @@
   3.110  by (EVERY (map grind_tac [3,2,1]));
   3.111  (*Oops*)
   3.112  by (Full_simp_tac 2);
   3.113 -by (REPEAT ((eresolve_tac [bexE] ORELSE' hyp_subst_tac) 2));
   3.114 +by (REPEAT ((etac bexE ORELSE' hyp_subst_tac) 2));
   3.115  by (simp_tac (!simpset addsimps [insert_Key_image]) 2);
   3.116  by (grind_tac 2);
   3.117  by (fast_tac (!claset delrules [bexI] 
   3.118 -		      addDs [unique_session_keys]
   3.119 -	              addss (!simpset)) 2);
   3.120 +                      addDs [unique_session_keys]
   3.121 +                      addss (!simpset)) 2);
   3.122  (*YM4*)
   3.123  (** LEVEL 11 **)
   3.124 -br (impI RS allI) 1;
   3.125 +by (rtac (impI RS allI) 1);
   3.126  by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1 THEN 
   3.127      Fast_tac 1);
   3.128  by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
   3.129  by (asm_simp_tac (!simpset addsimps [analz_image_newK]
   3.130 -	                   setloop split_tac [expand_if]) 1);
   3.131 +                           setloop split_tac [expand_if]) 1);
   3.132  (** LEVEL 15 **)
   3.133  by (grind_tac 1);
   3.134  by (REPEAT (dtac not_analz_insert 1));
   3.135 @@ -661,8 +661,8 @@
   3.136      THEN REPEAT (assume_tac 1));
   3.137  by (fast_tac (!claset delrules [allE, conjI] addSIs [bexI, exI]) 1);
   3.138  by (fast_tac (!claset delrules [conjI]
   3.139 -	              addIs [impOfSubs (subset_insertI RS analz_mono)]
   3.140 -		      addss (!simpset)) 1);
   3.141 +                      addIs [impOfSubs (subset_insertI RS analz_mono)]
   3.142 +                      addss (!simpset)) 1);
   3.143  val Nonce_secrecy = result() RS spec RSN (2, rev_mp) |> standard;
   3.144  
   3.145  
   3.146 @@ -679,7 +679,7 @@
   3.147  by (asm_full_simp_tac (HOL_ss addsimps [insert_Key_singleton]) 1);
   3.148  by (dtac Nonce_secrecy 1 THEN assume_tac 1);
   3.149  by (fast_tac (!claset addDs [unique_session_keys]
   3.150 -	              addss (!simpset)) 1);
   3.151 +                      addss (!simpset)) 1);
   3.152  val single_Nonce_secrecy = result();
   3.153  
   3.154  
   3.155 @@ -719,7 +719,7 @@
   3.156  by (SELECT_GOAL (REPEAT_FIRST (Safe_step_tac ORELSE' spy_analz_tac)) 1);
   3.157  (** LEVEL 14 **)
   3.158  by (lost_tac "Aa" 1);
   3.159 -bd (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trust_YM3) 1;
   3.160 +by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trust_YM3) 1);
   3.161  by (forward_tac [Says_Server_message_form] 3);
   3.162  by (forward_tac [Says_Server_imp_YM2] 4);
   3.163  by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE])));
   3.164 @@ -727,11 +727,11 @@
   3.165  (** LEVEL 20 **)
   3.166  by (REPEAT_FIRST hyp_subst_tac);
   3.167  by (lost_tac "Ba" 1);
   3.168 -bd (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1;
   3.169 +by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1);
   3.170  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   3.171                        addSEs [MPair_parts]) 1);
   3.172  by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1)); 
   3.173 -bd Spy_not_see_encrypted_key 1;
   3.174 +by (dtac Spy_not_see_encrypted_key 1);
   3.175  by (REPEAT (assume_tac 1 ORELSE Fast_tac 1)); 
   3.176  by (spy_analz_tac 1);
   3.177  (*Oops case*) (** LEVEL 28 **)
   3.178 @@ -740,7 +740,7 @@
   3.179  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   3.180  by (expand_case_tac "NB = NBa" 1);
   3.181  by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1);
   3.182 -br conjI 1;
   3.183 +by (rtac conjI 1);
   3.184  by (no_nonce_tac 1);
   3.185  (** LEVEL 35 **)
   3.186  by (thin_tac "?PP|?QQ" 1);  (*subsumption!*)
   3.187 @@ -769,10 +769,10 @@
   3.188  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   3.189  by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
   3.190      dtac B_trusts_YM4_shrK 1);
   3.191 -bd B_trusts_YM4_newK 3;
   3.192 +by (dtac B_trusts_YM4_newK 3);
   3.193  by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   3.194  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   3.195 -by (dresolve_tac [unique_session_keys] 1 THEN REPEAT (assume_tac 1));
   3.196 +by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
   3.197  by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1);
   3.198  qed "B_trust_YM4";
   3.199  
     4.1 --- a/src/HOL/Auth/Yahalom2.ML	Fri Nov 08 14:07:56 1996 +0100
     4.2 +++ b/src/HOL/Auth/Yahalom2.ML	Fri Nov 08 14:13:56 1996 +0100
     4.3 @@ -80,9 +80,9 @@
     4.4  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
     4.5  fun parts_induct_tac i = SELECT_GOAL
     4.6      (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN
     4.7 -	     (*Fake message*)
     4.8 -	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
     4.9 -					   impOfSubs Fake_parts_insert]
    4.10 +             (*Fake message*)
    4.11 +             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    4.12 +                                           impOfSubs Fake_parts_insert]
    4.13                                      addss (!simpset)) 2)) THEN
    4.14       (*Base case*)
    4.15       fast_tac (!claset addss (!simpset)) 1 THEN
    4.16 @@ -157,16 +157,16 @@
    4.17  \                length evs <= length evs' --> \
    4.18  \                newK evs' ~: keysFor (parts (sees lost Spy evs))";
    4.19  by (parts_induct_tac 1);
    4.20 -by (dresolve_tac [YM4_Key_parts_sees_Spy] 5);
    4.21 +by (dtac YM4_Key_parts_sees_Spy 5);
    4.22  (*YM1, YM2 and YM3*)
    4.23  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
    4.24  (*Fake and Oops: these messages send unknown (X) components*)
    4.25  by (EVERY
    4.26      (map (fast_tac
    4.27 -	  (!claset addDs [impOfSubs analz_subset_parts,
    4.28 -			  impOfSubs (analz_subset_parts RS keysFor_mono),
    4.29 -			  impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    4.30 -			  Suc_leD]
    4.31 +          (!claset addDs [impOfSubs analz_subset_parts,
    4.32 +                          impOfSubs (analz_subset_parts RS keysFor_mono),
    4.33 +                          impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    4.34 +                          Suc_leD]
    4.35                     addss (!simpset))) [3,1]));
    4.36  (*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
    4.37  by (fast_tac
    4.38 @@ -307,8 +307,8 @@
    4.39  by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
    4.40  (*Oops*)
    4.41  by (fast_tac (!claset delrules [disjE] 
    4.42 -		      addDs [unique_session_keys]
    4.43 -	              addss (!simpset)) 1);
    4.44 +                      addDs [unique_session_keys]
    4.45 +                      addss (!simpset)) 1);
    4.46  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    4.47  
    4.48  
    4.49 @@ -392,6 +392,6 @@
    4.50  \                      Crypt {|Agent B, Key K, Nonce NA|} (shrK A),     \
    4.51  \                      Crypt {|Nonce NB, Key K, Agent A|} (shrK B)|}    \
    4.52  \                   : set_of_list evs";
    4.53 -be (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1;
    4.54 +by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
    4.55  by (fast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
    4.56  qed "B_trust_YM4";