Trivial renamings
authorpaulson
Thu Dec 05 18:58:46 1996 +0100 (1996-12-05)
changeset 2322fbe6dd4abddc
parent 2321 083912bc5775
child 2323 3ae9b0ccee21
Trivial renamings
src/HOL/Auth/Yahalom.ML
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Dec 05 18:57:49 1996 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Dec 05 18:58:46 1996 +0100
     1.3 @@ -17,8 +17,7 @@
     1.4  Pretty.setdepth 20;
     1.5  
     1.6  
     1.7 -(*Weak liveness: there are traces that reach the end*)
     1.8 -
     1.9 +(*A "possibility property": there are traces that reach the end*)
    1.10  goal thy 
    1.11   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    1.12  \        ==> EX X NB K. EX evs: yahalom lost.          \
    1.13 @@ -315,7 +314,7 @@
    1.14  \             : set_of_list evs";
    1.15  by (etac rev_mp 1);
    1.16  by (parts_induct_tac 1);
    1.17 -qed "A_trust_YM3";
    1.18 +qed "A_trusts_YM3";
    1.19  
    1.20  
    1.21  (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
    1.22 @@ -541,7 +540,7 @@
    1.23  by (Step_tac 1);
    1.24  by (lost_tac "A" 1);
    1.25  by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
    1.26 -                             A_trust_YM3]) 1);
    1.27 +                             A_trusts_YM3]) 1);
    1.28  val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
    1.29  
    1.30  
    1.31 @@ -573,7 +572,7 @@
    1.32  by (Step_tac 1);
    1.33  by (lost_tac "A" 1);
    1.34  by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
    1.35 -                             A_trust_YM3]) 1);
    1.36 +                             A_trusts_YM3]) 1);
    1.37  result() RS mp RSN (2, rev_mp);
    1.38  
    1.39  
    1.40 @@ -659,7 +658,7 @@
    1.41  by (grind_tac 1);
    1.42  by (REPEAT (dtac not_analz_insert 1));
    1.43  by (lost_tac "A" 1);
    1.44 -by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trust_YM3) 1
    1.45 +by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
    1.46      THEN REPEAT (assume_tac 1));
    1.47  by (fast_tac (!claset delrules [allE, conjI] addSIs [bexI, exI]) 1);
    1.48  by (fast_tac (!claset delrules [conjI]
    1.49 @@ -721,7 +720,7 @@
    1.50  by (SELECT_GOAL (REPEAT_FIRST (Safe_step_tac ORELSE' spy_analz_tac)) 1);
    1.51  (** LEVEL 14 **)
    1.52  by (lost_tac "Aa" 1);
    1.53 -by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trust_YM3) 1);
    1.54 +by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
    1.55  by (forward_tac [Says_Server_message_form] 3);
    1.56  by (forward_tac [Says_Server_imp_YM2] 4);
    1.57  by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE])));
    1.58 @@ -776,7 +775,7 @@
    1.59  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
    1.60  by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
    1.61  by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1);
    1.62 -qed "B_trust_YM4";
    1.63 +qed "B_trusts_YM4";
    1.64  
    1.65  
    1.66