Renaming of functions, and tidying
authorpaulson
Mon Aug 19 11:19:55 1996 +0200 (1996-08-19)
changeset 19132809adb15eb0
parent 1912 947a34e00d1e
child 1914 86b095835de9
Renaming of functions, and tidying
src/HOL/Auth/Event.ML
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.ML
src/HOL/Auth/Message.thy
     1.1 --- a/src/HOL/Auth/Event.ML	Mon Aug 19 11:19:16 1996 +0200
     1.2 +++ b/src/HOL/Auth/Event.ML	Mon Aug 19 11:19:55 1996 +0200
     1.3 @@ -15,29 +15,25 @@
     1.4  Delrules [less_SucE];	(*Perhaps avoid inserting this in Arith.ML????*)
     1.5  
     1.6  (*FOR LIST.ML??*)
     1.7 -goal List.thy "x : setOfList (x#xs)";
     1.8 +goal List.thy "x : set_of_list (x#xs)";
     1.9  by (Simp_tac 1);
    1.10 -qed "setOfList_I1";
    1.11 +qed "set_of_list_I1";
    1.12  
    1.13 -goal List.thy "!!x. xs = x#xs' ==> x : setOfList xs";
    1.14 +goal List.thy "!!x. xs = x#xs' ==> x : set_of_list xs";
    1.15  by (Asm_simp_tac 1);
    1.16 -qed "setOfList_eqI1";
    1.17 +qed "set_of_list_eqI1";
    1.18  
    1.19 -goal List.thy "setOfList l <= setOfList (x#l)";
    1.20 +goal List.thy "set_of_list l <= set_of_list (x#l)";
    1.21  by (Simp_tac 1);
    1.22  by (Fast_tac 1);
    1.23 -qed "setOfList_subset_Cons";
    1.24 +qed "set_of_list_subset_Cons";
    1.25  
    1.26  (*Not for Addsimps -- it can cause goals to blow up!*)
    1.27  goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
    1.28  by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.29  qed "mem_if";
    1.30  
    1.31 -(*DELETE, AS ALREADY IN SET.ML*)
    1.32 -prove "imp_conj_distrib" "(P --> (Q&R)) = ((P-->Q) & (P-->R))";
    1.33 -
    1.34 -
    1.35 -(*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE!!*)
    1.36 +(*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)
    1.37  goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
    1.38  by (fast_tac (!claset addEs [equalityE]) 1);
    1.39  val subset_range_iff = result();
    1.40 @@ -45,10 +41,6 @@
    1.41  
    1.42  open Event;
    1.43  
    1.44 -goal Set.thy "A Un (insert a B) = insert a (A Un B)";
    1.45 -by (Fast_tac 1);
    1.46 -qed "Un_insert_right";
    1.47 -
    1.48  Addsimps [Un_insert_left, Un_insert_right];
    1.49  
    1.50  (*By default only o_apply is built-in.  But in the presence of eta-expansion
    1.51 @@ -94,15 +86,15 @@
    1.52  
    1.53  bind_thm ("parts_image_Key", subset_refl RS parts_image_subset);
    1.54  
    1.55 -goal thy "!!H. H <= Key``E ==> analyze H = H";
    1.56 +goal thy "!!H. H <= Key``E ==> analz H = H";
    1.57  by (Auto_tac ());
    1.58 -be analyze.induct 1;
    1.59 +be analz.induct 1;
    1.60  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.61 -qed "analyze_image_subset";
    1.62 +qed "analz_image_subset";
    1.63  
    1.64 -bind_thm ("analyze_image_Key", subset_refl RS analyze_image_subset);
    1.65 +bind_thm ("analz_image_Key", subset_refl RS analz_image_subset);
    1.66  
    1.67 -Addsimps [parts_image_Key, analyze_image_Key];
    1.68 +Addsimps [parts_image_Key, analz_image_Key];
    1.69  
    1.70  goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
    1.71  by (agent.induct_tac "C" 1);
    1.72 @@ -123,17 +115,17 @@
    1.73  
    1.74  
    1.75  (*Agents see their own serverKeys!*)
    1.76 -goal thy "Key (serverKey A) : analyze (sees A evs)";
    1.77 +goal thy "Key (serverKey A) : analz (sees A evs)";
    1.78  by (list.induct_tac "evs" 1);
    1.79 -by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analyze_mono)]) 2);
    1.80 +by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2);
    1.81  by (agent.induct_tac "A" 1);
    1.82  by (auto_tac (!claset addIs [range_eqI], !simpset));
    1.83 -qed "analyze_own_serverKey";
    1.84 +qed "analz_own_serverKey";
    1.85  
    1.86  bind_thm ("parts_own_serverKey",
    1.87 -	  [analyze_subset_parts, analyze_own_serverKey] MRS subsetD);
    1.88 +	  [analz_subset_parts, analz_own_serverKey] MRS subsetD);
    1.89  
    1.90 -Addsimps [analyze_own_serverKey, parts_own_serverKey];
    1.91 +Addsimps [analz_own_serverKey, parts_own_serverKey];
    1.92  
    1.93  
    1.94  
    1.95 @@ -197,7 +189,7 @@
    1.96  by (ALLGOALS (fast_tac (!claset addss ss)));
    1.97  qed "UN_parts_sees_Says";
    1.98  
    1.99 -goal thy "Says A B X : setOfList evs --> X : sees Enemy evs";
   1.100 +goal thy "Says A B X : set_of_list evs --> X : sees Enemy evs";
   1.101  by (list.induct_tac "evs" 1);
   1.102  by (Auto_tac ());
   1.103  qed_spec_mp "Says_imp_sees_Enemy";
   1.104 @@ -211,8 +203,8 @@
   1.105  qed "initState_subset";
   1.106  
   1.107  goal thy "X : sees C evs --> \
   1.108 -\          (EX A B. Says A B X : setOfList evs) | \
   1.109 -\          (EX A. Notes A X : setOfList evs) | \
   1.110 +\          (EX A B. Says A B X : set_of_list evs) | \
   1.111 +\          (EX A. Notes A X : set_of_list evs) | \
   1.112  \          (EX A. X = Key (serverKey A))";
   1.113  by (list.induct_tac "evs" 1);
   1.114  by (ALLGOALS Asm_simp_tac);
   1.115 @@ -244,14 +236,14 @@
   1.116  
   1.117  
   1.118  (*Nobody sends themselves messages*)
   1.119 -goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: setOfList evs";
   1.120 +goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: set_of_list evs";
   1.121  be traces.induct 1;
   1.122  by (Auto_tac());
   1.123  qed_spec_mp "not_Says_to_self";
   1.124  Addsimps [not_Says_to_self];
   1.125  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   1.126  
   1.127 -goal thy "!!evs. evs : traces ==> Notes A X ~: setOfList evs";
   1.128 +goal thy "!!evs. evs : traces ==> Notes A X ~: set_of_list evs";
   1.129  be traces.induct 1;
   1.130  by (Auto_tac());
   1.131  qed "not_Notes";
   1.132 @@ -269,18 +261,18 @@
   1.133  be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.134  by (auto_tac(!claset, !simpset addsimps [parts_insert2]));
   1.135  (*Deals with Faked messages*)
   1.136 -by (best_tac (!claset addDs [impOfSubs analyze_subset_parts,
   1.137 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.138  			     impOfSubs parts_insert_subset_Un]
   1.139  	              addss (!simpset)) 1);
   1.140  qed "Enemy_not_see_serverKey";
   1.141  
   1.142 -bind_thm ("Enemy_not_analyze_serverKey",
   1.143 -	  [analyze_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD);
   1.144 +bind_thm ("Enemy_not_analz_serverKey",
   1.145 +	  [analz_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD);
   1.146  
   1.147  Addsimps [Enemy_not_see_serverKey, 
   1.148  	  not_sym RSN (2, Enemy_not_see_serverKey), 
   1.149 -	  Enemy_not_analyze_serverKey, 
   1.150 -	  not_sym RSN (2, Enemy_not_analyze_serverKey)];
   1.151 +	  Enemy_not_analz_serverKey, 
   1.152 +	  not_sym RSN (2, Enemy_not_analz_serverKey)];
   1.153  
   1.154  (*We go to some trouble to preserve R in the 3rd subgoal*)
   1.155  val major::prems = 
   1.156 @@ -294,11 +286,11 @@
   1.157  by (ALLGOALS (fast_tac (!claset addIs prems)));
   1.158  qed "Enemy_see_serverKey_E";
   1.159  
   1.160 -bind_thm ("Enemy_analyze_serverKey_E", 
   1.161 -	  analyze_subset_parts RS subsetD RS Enemy_see_serverKey_E);
   1.162 +bind_thm ("Enemy_analz_serverKey_E", 
   1.163 +	  analz_subset_parts RS subsetD RS Enemy_see_serverKey_E);
   1.164  
   1.165  (*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *)
   1.166 -AddSEs [Enemy_see_serverKey_E, Enemy_analyze_serverKey_E];
   1.167 +AddSEs [Enemy_see_serverKey_E, Enemy_analz_serverKey_E];
   1.168  
   1.169  
   1.170  (*No Friend will ever see another agent's server key 
   1.171 @@ -316,12 +308,12 @@
   1.172  goal thy  
   1.173   "!!evs. evs : traces ==>                                  \
   1.174  \        (Key (serverKey A) \
   1.175 -\           : analyze (insert (Key (serverKey B)) (sees Enemy evs))) =  \
   1.176 +\           : analz (insert (Key (serverKey B)) (sees Enemy evs))) =  \
   1.177  \        (A=B | A=Enemy)";
   1.178 -by (best_tac (!claset addDs [impOfSubs analyze_subset_parts]
   1.179 -		      addIs [impOfSubs (subset_insertI RS analyze_mono)]
   1.180 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
   1.181 +		      addIs [impOfSubs (subset_insertI RS analz_mono)]
   1.182  	              addss (!simpset)) 1);
   1.183 -qed "serverKey_mem_analyze";
   1.184 +qed "serverKey_mem_analz";
   1.185  
   1.186  
   1.187  
   1.188 @@ -349,7 +341,7 @@
   1.189  (*Rule NS3 in protocol*)
   1.190  by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
   1.191  (*Rule Fake: where an Enemy agent can say practically anything*)
   1.192 -by (best_tac (!claset addDs [impOfSubs analyze_subset_parts,
   1.193 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.194  			     impOfSubs parts_insert_subset_Un,
   1.195  			     less_imp_le]
   1.196  	              addss (!simpset)) 1);
   1.197 @@ -365,7 +357,7 @@
   1.198  
   1.199  (*Another variant: old messages must contain old keys!*)
   1.200  goal thy 
   1.201 - "!!evs. [| Says A B X : setOfList evs;  \
   1.202 + "!!evs. [| Says A B X : set_of_list evs;  \
   1.203  \           Key (newK evt) : parts {X};    \
   1.204  \           evs : traces                 \
   1.205  \        |] ==> length evt < length evs";
   1.206 @@ -398,10 +390,10 @@
   1.207  (*Rule Fake: where an Enemy agent can say practically anything*)
   1.208  by (best_tac 
   1.209      (!claset addSDs [newK_invKey]
   1.210 -	     addDs [impOfSubs (analyze_subset_parts RS keysFor_mono),
   1.211 +	     addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   1.212  		    impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.213  		    less_imp_le]
   1.214 -             addEs [new_keys_not_seen RS not_parts_not_analyze RSN (2,rev_notE)]
   1.215 +             addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
   1.216  	     addss (!simpset)) 1);
   1.217  (*Rule NS3: quite messy...*)
   1.218  by (hyp_subst_tac 1);
   1.219 @@ -422,15 +414,15 @@
   1.220  by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   1.221  qed "new_keys_not_used";
   1.222  
   1.223 -bind_thm ("new_keys_not_analyzed",
   1.224 -	  [analyze_subset_parts RS keysFor_mono,
   1.225 +bind_thm ("new_keys_not_analzd",
   1.226 +	  [analz_subset_parts RS keysFor_mono,
   1.227  	   new_keys_not_used] MRS contra_subsetD);
   1.228  
   1.229 -Addsimps [new_keys_not_used, new_keys_not_analyzed];
   1.230 +Addsimps [new_keys_not_used, new_keys_not_analzd];
   1.231  
   1.232  
   1.233  (** Rewrites to push in Key and Crypt messages, so that other messages can
   1.234 -    be pulled out using the analyze_insert rules **)
   1.235 +    be pulled out using the analz_insert rules **)
   1.236  
   1.237  fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 
   1.238                        insert_commute;
   1.239 @@ -452,7 +444,7 @@
   1.240  (*Describes the form *and age* of K, and the form of X,
   1.241    when the following message is sent*)
   1.242  goal thy 
   1.243 - "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : setOfList evs; \
   1.244 + "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \
   1.245  \           evs : traces    \
   1.246  \        |] ==> (EX evt:traces. \
   1.247  \                         K = Key(newK evt) & \
   1.248 @@ -465,9 +457,9 @@
   1.249  by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   1.250  qed "Says_Server_message_form";
   1.251  
   1.252 -(* c ~: keysFor (parts H) ==> c ~: keysFor (analyze H) *)
   1.253 -bind_thm ("not_parts_not_keysFor_analyze", 
   1.254 -	  analyze_subset_parts RS keysFor_mono RS contra_subsetD);
   1.255 +(* c ~: keysFor (parts H) ==> c ~: keysFor (analz H) *)
   1.256 +bind_thm ("not_parts_not_keysFor_analz", 
   1.257 +	  analz_subset_parts RS keysFor_mono RS contra_subsetD);
   1.258  
   1.259  
   1.260  
   1.261 @@ -477,13 +469,13 @@
   1.262  \                 (Crypt {|N, Agent(Friend j), K, X|} K') # evs';  \
   1.263  \           evs : traces;  i~=k                                    \
   1.264  \        |] ==>                                                    \
   1.265 -\     K ~: analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
   1.266 +\     K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
   1.267  be rev_mp 1;
   1.268  be traces.induct 1;
   1.269  be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
   1.270  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.271  by (Step_tac 1);
   1.272 -by (asm_full_simp_tac (!simpset addsimps[analyze_subset_parts RS contra_subsetD]) 1);
   1.273 +by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1);
   1.274  val Enemy_not_see_encrypted_key_lemma = result();
   1.275  *)
   1.276  
   1.277 @@ -519,9 +511,9 @@
   1.278  (*Now for the Fake case*)
   1.279  by (subgoal_tac 
   1.280      "Crypt {|Nonce NA, Agent Ba, Key K, Xa|} (serverKey A) : \
   1.281 -\    parts (synthesize (analyze (sees Enemy evsa)) Un (sees Enemy evsa))" 1);
   1.282 +\    parts (synth (analz (sees Enemy evsa)) Un (sees Enemy evsa))" 1);
   1.283  by (fast_tac (!claset addSEs [impOfSubs parts_mono]) 2);
   1.284 -by (best_tac (!claset addDs [impOfSubs analyze_subset_parts]
   1.285 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
   1.286  	              addss (!simpset)) 1);
   1.287  val encrypted_form = result();
   1.288  
   1.289 @@ -531,7 +523,7 @@
   1.290   "!!evs. evs : traces ==>                             \
   1.291  \        ALL S A NA B K X.                            \
   1.292  \            Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.293 -\            : setOfList evs  -->   \
   1.294 +\            : set_of_list evs  -->   \
   1.295  \        S = Server | S = Enemy";
   1.296  be traces.induct 1;
   1.297  be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.298 @@ -541,7 +533,7 @@
   1.299  (*First justify this assumption!*)
   1.300  by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2);
   1.301  by (Step_tac 1);
   1.302 -bd (setOfList_I1 RS Says_Server_message_form) 1;
   1.303 +bd (set_of_list_I1 RS Says_Server_message_form) 1;
   1.304  by (ALLGOALS Full_simp_tac);
   1.305  (*Final case.  Clear out needless quantifiers to speed the following step*)
   1.306  by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1);
   1.307 @@ -555,7 +547,7 @@
   1.308    use Says_Server_message_form if applicable*)
   1.309  goal thy 
   1.310   "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.311 -\            : setOfList evs;                              \
   1.312 +\            : set_of_list evs;                              \
   1.313  \           evs : traces               \
   1.314  \        |] ==> (EX evt:traces. K = newK evt & length evt < length evs & \
   1.315  \                               X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   1.316 @@ -576,7 +568,7 @@
   1.317  \                               K = newK evt & \
   1.318  \                               X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   1.319  by (forward_tac [traces_eq_ConsE] 1);
   1.320 -by (dtac (setOfList_eqI1 RS Says_S_message_form) 2);
   1.321 +by (dtac (set_of_list_eqI1 RS Says_S_message_form) 2);
   1.322  by (Auto_tac());	
   1.323  qed "Says_S_message_form_eq";
   1.324  
   1.325 @@ -586,9 +578,9 @@
   1.326  (****
   1.327   The following is to prove theorems of the form
   1.328  
   1.329 -          Key K : analyze (insert (Key (newK evt)) 
   1.330 +          Key K : analz (insert (Key (newK evt)) 
   1.331  	                   (insert (Key (serverKey C)) (sees Enemy evs))) ==>
   1.332 -          Key K : analyze (insert (Key (serverKey C)) (sees Enemy evs))
   1.333 +          Key K : analz (insert (Key (serverKey C)) (sees Enemy evs))
   1.334  
   1.335   A more general formula must be proved inductively.
   1.336  
   1.337 @@ -610,7 +602,7 @@
   1.338  by (res_inst_tac [("x1","Xa")] (insert_commute RS ssubst) 2);
   1.339  by (Asm_full_simp_tac 2);
   1.340  (*Deals with Faked messages*)
   1.341 -by (best_tac (!claset addDs [impOfSubs analyze_subset_parts,
   1.342 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.343  			     impOfSubs parts_insert_subset_Un]
   1.344  	              addss (!simpset)) 1);
   1.345  result();
   1.346 @@ -636,10 +628,10 @@
   1.347  
   1.348  goal thy  
   1.349   "!!evs. evs : traces ==> \
   1.350 -\  ALL K E. (Key K : analyze (insert (Key (serverKey C)) \
   1.351 +\  ALL K E. (Key K : analz (insert (Key (serverKey C)) \
   1.352  \                             (Key``(newK``E) Un (sees Enemy evs)))) = \
   1.353  \           (K : newK``E |  \
   1.354 -\            Key K : analyze (insert (Key (serverKey C)) \
   1.355 +\            Key K : analz (insert (Key (serverKey C)) \
   1.356  \                             (sees Enemy evs)))";
   1.357  be traces.induct 1;
   1.358  be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.359 @@ -657,35 +649,35 @@
   1.360  (** LEVEL 7 **)
   1.361  (*Fake case*)
   1.362  by (REPEAT (Safe_step_tac 1));
   1.363 -by (fast_tac (!claset addSEs [impOfSubs (analyze_mono)]) 2);
   1.364 +by (fast_tac (!claset addSEs [impOfSubs (analz_mono)]) 2);
   1.365  by (subgoal_tac 
   1.366 -    "Key K : analyze \
   1.367 -\             (synthesize \
   1.368 -\              (analyze (insert (Key (serverKey C)) \
   1.369 +    "Key K : analz \
   1.370 +\             (synth \
   1.371 +\              (analz (insert (Key (serverKey C)) \
   1.372  \                        (Key``(newK``E) Un (sees Enemy evsa)))))" 1);
   1.373  (*First, justify this subgoal*)
   1.374  (*Discard the quantified formula for better speed*)
   1.375  by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.376  by (eres_inst_tac [("V","?Q ~: ?QQ")] thin_rl 2);
   1.377 -by (best_tac (!claset addIs [impOfSubs (analyze_mono RS synthesize_mono)]
   1.378 -                      addSEs [impOfSubs analyze_mono]) 2);
   1.379 +by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
   1.380 +                      addSEs [impOfSubs analz_mono]) 2);
   1.381  by (Asm_full_simp_tac 1);
   1.382 -by (deepen_tac (!claset addIs [impOfSubs analyze_mono]) 0 1);
   1.383 -qed_spec_mp "analyze_image_newK";
   1.384 +by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1);
   1.385 +qed_spec_mp "analz_image_newK";
   1.386  
   1.387  
   1.388  goal thy  
   1.389   "!!evs. evs : traces ==>                                  \
   1.390 -\        Key K : analyze (insert (Key (newK evt))          \
   1.391 +\        Key K : analz (insert (Key (newK evt))          \
   1.392  \                         (insert (Key (serverKey C))      \
   1.393  \                          (sees Enemy evs))) =            \
   1.394  \             (K = newK evt |                              \
   1.395 -\              Key K : analyze (insert (Key (serverKey C)) \
   1.396 +\              Key K : analz (insert (Key (serverKey C)) \
   1.397  \                               (sees Enemy evs)))";
   1.398 -by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analyze_image_newK, 
   1.399 +by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.400  				   insert_Key_singleton]) 1);
   1.401  by (Fast_tac 1);
   1.402 -qed "analyze_insert_Key_newK";
   1.403 +qed "analz_insert_Key_newK";
   1.404  
   1.405  
   1.406  
   1.407 @@ -694,7 +686,7 @@
   1.408   "!!evs. evs : traces ==>                      \
   1.409  \      EX X'. ALL C S A Y N B X.               \
   1.410  \         C ~= Enemy -->                       \
   1.411 -\         Says S A Y : setOfList evs -->       \
   1.412 +\         Says S A Y : set_of_list evs -->       \
   1.413  \         ((Crypt {|N, Agent B, Key K, X|} (serverKey C)) : parts{Y} --> \
   1.414  \       (X = X'))";
   1.415  be traces.induct 1;
   1.416 @@ -721,7 +713,7 @@
   1.417  by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (serverKey C) \
   1.418  \                  : parts (sees Enemy evsa)" 1);
   1.419  by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.420 -by (best_tac (!claset addSEs [impOfSubs analyze_subset_parts]
   1.421 +by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   1.422  	              addDs [impOfSubs parts_insert_subset_Un]
   1.423                        addss (!simpset)) 2);
   1.424  by (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 1);
   1.425 @@ -737,9 +729,9 @@
   1.426  (*In messages of this form, the session key uniquely identifies the rest*)
   1.427  goal thy 
   1.428   "!!evs. [| Says S A          \
   1.429 -\         (Crypt {|N, Agent B, Key K, X|} (serverKey C)) : setOfList evs; \
   1.430 +\         (Crypt {|N, Agent B, Key K, X|} (serverKey C)) : set_of_list evs; \
   1.431   \      Says S' A'                                         \
   1.432 -\         (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) : setOfList evs;                         \
   1.433 +\         (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) : set_of_list evs;                         \
   1.434  \     \
   1.435  \   evs : traces;  C ~= Enemy;  C' ~= Enemy    |] ==> X = X'";
   1.436  bd lemma 1;
   1.437 @@ -754,10 +746,10 @@
   1.438     -- even if another key is compromised*)
   1.439  goal thy 
   1.440   "!!evs. [| Says Server (Friend i) \
   1.441 -\            (Crypt {|N, Agent(Friend j), K, X|} K') : setOfList evs;  \
   1.442 +\            (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs;  \
   1.443  \           evs : traces;  Friend i ~= C;  Friend j ~= C              \
   1.444  \        |] ==>                                                       \
   1.445 -\     K ~: analyze (insert (Key (serverKey C)) (sees Enemy evs))";
   1.446 +\     K ~: analz (insert (Key (serverKey C)) (sees Enemy evs))";
   1.447  be rev_mp 1;
   1.448  be traces.induct 1;
   1.449  be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
   1.450 @@ -768,8 +760,8 @@
   1.451  by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   1.452  by (ALLGOALS 
   1.453      (asm_full_simp_tac 
   1.454 -     (!simpset addsimps ([analyze_subset_parts RS contra_subsetD,
   1.455 -			  analyze_insert_Key_newK] @ pushes)
   1.456 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.457 +			  analz_insert_Key_newK] @ pushes)
   1.458                 setloop split_tac [expand_if])));
   1.459  (*NS2*)
   1.460  by (fast_tac (!claset addSEs [less_irrefl]) 2);
   1.461 @@ -778,13 +770,13 @@
   1.462  br notI 1;
   1.463  by (subgoal_tac 
   1.464      "Key (newK evt) : \
   1.465 -\    analyze (synthesize (analyze (insert (Key (serverKey C)) \
   1.466 +\    analz (synth (analz (insert (Key (serverKey C)) \
   1.467  \                                  (sees Enemy evsa))))" 1);
   1.468 -be (impOfSubs analyze_mono) 2;
   1.469 -by (deepen_tac (!claset addIs [analyze_mono RS synthesize_mono RSN 
   1.470 +be (impOfSubs analz_mono) 2;
   1.471 +by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN 
   1.472  			     (2,rev_subsetD),
   1.473 -			     impOfSubs synthesize_increasing,
   1.474 -			     impOfSubs analyze_increasing]) 0 2);
   1.475 +			     impOfSubs synth_increasing,
   1.476 +			     impOfSubs analz_increasing]) 0 2);
   1.477  (*Proves the Fake goal*)
   1.478  by (fast_tac (!claset addss (!simpset)) 1);
   1.479  
   1.480 @@ -792,14 +784,14 @@
   1.481  (*Now for NS3*)
   1.482  (*NS3, case 1: that message from the Server was just sent*)
   1.483  by (ALLGOALS (forward_tac [traces_ConsE]));
   1.484 -by (forward_tac [setOfList_I1 RS Says_Server_message_form] 1);
   1.485 +by (forward_tac [set_of_list_I1 RS Says_Server_message_form] 1);
   1.486  by (Full_simp_tac 1);
   1.487  by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   1.488  (*Can simplify the Crypt messages: their key is secure*)
   1.489  by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1);
   1.490  by (asm_full_simp_tac
   1.491 -    (!simpset addsimps (pushes @ [analyze_insert_Crypt,
   1.492 -				  analyze_subset_parts RS contra_subsetD])) 1);
   1.493 +    (!simpset addsimps (pushes @ [analz_insert_Crypt,
   1.494 +				  analz_subset_parts RS contra_subsetD])) 1);
   1.495  
   1.496  (**LEVEL 20, one subgoal left! **)
   1.497  (*NS3, case 2: that message from the Server was sent earlier*)
   1.498 @@ -813,18 +805,18 @@
   1.499  
   1.500  (**LEVEL 24 **)
   1.501  
   1.502 -by ((forward_tac [setOfList_I1 RS Says_S_message_form]) 1);
   1.503 +by ((forward_tac [set_of_list_I1 RS Says_S_message_form]) 1);
   1.504  by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   1.505  by (asm_full_simp_tac
   1.506 -    (!simpset addsimps (mem_if::analyze_insert_Key_newK::pushes)) 1);
   1.507 +    (!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1);
   1.508  by (step_tac (!claset delrules [impCE]) 1);
   1.509  
   1.510  (**LEVEL 28 **)
   1.511 -bd ([impOfSubs setOfList_subset_Cons, setOfList_I1] MRS unique_session_keys) 1;
   1.512 +bd ([impOfSubs set_of_list_subset_Cons, set_of_list_I1] MRS unique_session_keys) 1;
   1.513  ba 1;
   1.514  by (ALLGOALS Full_simp_tac);
   1.515  by (REPEAT_FIRST (eresolve_tac [conjE] ORELSE' hyp_subst_tac));
   1.516 -by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analyze]) 1);
   1.517 +by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analz]) 1);
   1.518  qed "Enemy_not_see_encrypted_key";
   1.519  
   1.520  
   1.521 @@ -839,25 +831,25 @@
   1.522  
   1.523  goal thy 
   1.524   "!!evs. [| Says Server (Friend i) \
   1.525 -\             (Crypt {|N, Agent B, K|} K') : setOfList evs;  \
   1.526 +\             (Crypt {|N, Agent B, K|} K') : set_of_list evs;  \
   1.527  \           evs : traces;  i~=j    \
   1.528 -\         |] ==> K ~: analyze (sees (Friend j) evs)";
   1.529 -br (sees_agent_subset_sees_Enemy RS analyze_mono RS contra_subsetD) 1;
   1.530 +\         |] ==> K ~: analz (sees (Friend j) evs)";
   1.531 +br (sees_agent_subset_sees_Enemy RS analz_mono RS contra_subsetD) 1;
   1.532  by (ALLGOALS (asm_simp_tac (!simpset addsimps [Enemy_not_see_encrypted_key])));
   1.533  qed "Friend_not_see_encrypted_key";
   1.534  
   1.535  goal thy 
   1.536   "!!evs. [| Says Server (Friend i) \
   1.537 -\             (Crypt {|N, Agent B, K|} K') : setOfList evs;  \
   1.538 +\             (Crypt {|N, Agent B, K|} K') : set_of_list evs;  \
   1.539  \           A ~: {Friend i, Server};  \
   1.540  \           evs : traces    \
   1.541 -\        |] ==>  K ~: analyze (sees A evs)";
   1.542 +\        |] ==>  K ~: analz (sees A evs)";
   1.543  by (eres_inst_tac [("P", "A~:?X")] rev_mp 1);
   1.544  by (agent.induct_tac "A" 1);
   1.545  by (ALLGOALS Simp_tac);
   1.546  by (asm_simp_tac (!simpset addsimps [eq_sym_conv, 
   1.547  				     Friend_not_see_encrypted_key]) 1);
   1.548 -br ([analyze_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1;
   1.549 +br ([analz_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1;
   1.550  (*  hyp_subst_tac would deletes the equality assumption... *)
   1.551  by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac));
   1.552  qed "Agent_not_see_encrypted_key";
   1.553 @@ -866,7 +858,7 @@
   1.554  (*Neatly packaged, perhaps in a useless form*)
   1.555  goalw thy [knownBy_def]
   1.556   "!!evs. [| Says Server (Friend i) \
   1.557 -\             (Crypt {|N, Agent B, K|} K') : setOfList evs;  \
   1.558 +\             (Crypt {|N, Agent B, K|} K') : set_of_list evs;  \
   1.559  \           evs : traces    \
   1.560  \        |] ==>  knownBy evs K <= {Friend i, Server}";
   1.561  
   1.562 @@ -887,269 +879,38 @@
   1.563  \                 (Crypt {|N, Agent(Friend j), K, X|} K') # evs';  \
   1.564  \           evs : traces;  i~=k                                    \
   1.565  \        |] ==>                                                    \
   1.566 -\     K ~: analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
   1.567 +\     K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
   1.568  be rev_mp 1;
   1.569  be traces.induct 1;
   1.570  be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
   1.571  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.572  by (Step_tac 1);
   1.573 -by (asm_full_simp_tac (!simpset addsimps[analyze_subset_parts RS contra_subsetD]) 1);
   1.574 +by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1);
   1.575  val Enemy_not_see_encrypted_key_lemma = result();
   1.576  
   1.577  
   1.578  
   1.579  
   1.580 -by (asm_full_simp_tac
   1.581 -    (!simpset addsimps (pushes @
   1.582 -			[analyze_subset_parts RS contra_subsetD,
   1.583 -			 traces_ConsE RS Enemy_not_see_serverKey])) 1);
   1.584 -
   1.585 -by (asm_full_simp_tac
   1.586 -    (!simpset addsimps [analyze_subset_parts  RS keysFor_mono RS contra_subsetD,
   1.587 -			traces_ConsE RS new_keys_not_used]) 1);
   1.588 -by (Fast_tac 1); 
   1.589 -
   1.590 -
   1.591 -
   1.592 -
   1.593 -(*Precisely formulated as needed below.  Perhaps redundant, as simplification
   1.594 -  with the aid of  analyze_subset_parts RS contra_subsetD  might do the
   1.595 -  same thing.*)
   1.596 -goal thy 
   1.597 - "!!evs. [| evs : traces; A ~= Enemy;  A ~= Friend j |] ==> \
   1.598 -\        Key (serverKey A) ~:                               \
   1.599 -\          analyze (insert (Key (serverKey (Friend j))) (sees Enemy evs))";
   1.600 -br (analyze_subset_parts RS contra_subsetD) 1;
   1.601 -by (Asm_simp_tac 1);
   1.602 -qed "insert_not_analyze_serverKey";
   1.603 -
   1.604 -
   1.605 -
   1.606 -
   1.607 -by (asm_full_simp_tac
   1.608 -    (!simpset addsimps (pushes @
   1.609 -			[insert_not_analyze_serverKey, 
   1.610 -			 traces_ConsE RS insert_not_analyze_serverKey])) 1);
   1.611 -
   1.612 -
   1.613 -by (stac analyze_insert_Crypt 1);
   1.614 -
   1.615 -
   1.616 -
   1.617 -
   1.618 -
   1.619 -
   1.620 -
   1.621 -
   1.622 -
   1.623  
   1.624  
   1.625  
   1.626 -(*NS3, case 1: that message from the Server was just sent*)
   1.627 -by (asm_full_simp_tac (!simpset addsimps pushes) 1);
   1.628 -
   1.629 -(*NS3, case 2: that message from the Server was sent earlier*)
   1.630 -by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac));
   1.631 -by (mp_tac 1);
   1.632 -by (asm_full_simp_tac (!simpset addsimps pushes) 1);
   1.633 -
   1.634 -by (Step_tac 1);
   1.635 -by (asm_full_simp_tac
   1.636 -    (!simpset addsimps [traces_ConsE RS insert_not_analyze_serverKey]) 1);
   1.637 -
   1.638 -
   1.639 -
   1.640 -(*pretend we have the right lemma!*)
   1.641 -by (subgoal_tac "(EX evt. X = (Crypt {|Key(newK evt), Agent(Friend ia)|} (serverKey B)))" 1);
   1.642 -by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac));
   1.643 -by (asm_full_simp_tac (!simpset addsimps pushes) 1);
   1.644 +(*Precisely formulated as needed below.  Perhaps redundant, as simplification
   1.645 +  with the aid of  analz_subset_parts RS contra_subsetD  might do the
   1.646 +  same thing.*)
   1.647 +goal thy 
   1.648 + "!!evs. [| evs : traces; A ~= Enemy;  A ~= Friend j |] ==> \
   1.649 +\        Key (serverKey A) ~:                               \
   1.650 +\          analz (insert (Key (serverKey (Friend j))) (sees Enemy evs))";
   1.651 +br (analz_subset_parts RS contra_subsetD) 1;
   1.652 +by (Asm_simp_tac 1);
   1.653 +qed "insert_not_analz_serverKey";
   1.654  
   1.655 -by (excluded_middle_tac "ia=k" 1);
   1.656 -(*Case where the key is compromised*)
   1.657 -by (hyp_subst_tac 2);
   1.658 -by (stac insert_commute 2);   (*Pushes in the "insert X" for simplification*)
   1.659 -by (Asm_full_simp_tac 2);
   1.660 -
   1.661 -
   1.662 -
   1.663 -by (asm_full_simp_tac (!simpset addsimps pushes) 1);
   1.664 -
   1.665 -by (REPEAT_FIRST Safe_step_tac);
   1.666 -by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.667 -
   1.668 -
   1.669 -by (REPEAT (Safe_step_tac 1));
   1.670 -
   1.671 -
   1.672 -
   1.673 -by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.674 -
   1.675 -by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac));
   1.676 -
   1.677 -by (eres_inst_tac [("V","?P-->?Q")] thin_rl 1);	(*deletes the bad implication*)
   1.678 -by ((forward_tac [Says_Server_message_form] THEN' 
   1.679 -     fast_tac (!claset addSEs [traces_ConsE])) 1);
   1.680 -by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac));
   1.681  
   1.682  
   1.683  
   1.684  XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
   1.685  proof_timing:=true;
   1.686  
   1.687 -(*Case where the key is secure*)
   1.688 -by (dres_inst_tac [("psi", "?X ~: ?H")] asm_rl 1);
   1.689 -by (asm_full_simp_tac
   1.690 -    (!simpset addsimps [traces_ConsE RS insert_not_analyze_serverKey]) 1);
   1.691 -
   1.692 -
   1.693 -
   1.694 -by (full_simp_tac (!simpset addsimps [insert_Key_Agent_delay,
   1.695 -				      insert_Key_Crypt_delay]) 1);
   1.696 -
   1.697 -by (forward_tac [setOfList_I1 RS Says_Server_message_form] 1);
   1.698 -by (REPEAT_FIRST (eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac));
   1.699 -
   1.700 -
   1.701 -by (asm_full_simp_tac
   1.702 -    (!simpset addsimps [traces_ConsE RS insert_not_analyze_serverKey]) 1);
   1.703 -
   1.704 -
   1.705 -by (stac insert_commute 1);   (*Pushes in the "insert X" for simplification*)
   1.706 -by (stac analyze_insert_Crypt 1);
   1.707 -
   1.708 -by (asm_full_simp_tac
   1.709 -    (!simpset addsimps [insert_not_analyze_serverKey, 
   1.710 -			traces_ConsE RS insert_not_analyze_serverKey]) 1);
   1.711 -
   1.712 -
   1.713 - 1. !!evs A B K NA S X evsa evs' ia evs'a.
   1.714 -       [| i ~= k; j ~= k;
   1.715 -          Says S (Friend ia)
   1.716 -           (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) #
   1.717 -          evs' :
   1.718 -          traces;
   1.719 -          Friend ia ~= B;
   1.720 -          Says (Friend ia) Server {|Agent (Friend ia), Agent B, Nonce NA|} :
   1.721 -          setOfList evs';
   1.722 -          Says Server (Friend i)
   1.723 -           (Crypt
   1.724 -             {|N, Agent (Friend j), Key (newK evs'a),
   1.725 -              Crypt {|Key (newK evs'a), Agent (Friend i)|}
   1.726 -               (serverKey (Friend j))|}
   1.727 -             K') :
   1.728 -          setOfList evs';
   1.729 -          Key (newK evs'a) ~:
   1.730 -          analyze
   1.731 -           (insert
   1.732 -             (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia)))
   1.733 -             (insert (Key (serverKey (Friend k))) (sees Enemy evs')));
   1.734 -          length evs'a < length evs' |] ==>
   1.735 -       Key (newK evs'a) ~:
   1.736 -       analyze
   1.737 -        (insert X
   1.738 -          (insert
   1.739 -            (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia)))
   1.740 -            (insert (Key (serverKey (Friend k))) (sees Enemy evs'))))
   1.741 -
   1.742 -
   1.743 -by (Asm_full_simp_tac 1);
   1.744 -
   1.745 -
   1.746 -by (Simp_tac 2);
   1.747 -
   1.748 -
   1.749 -by (Simp_tac 2);
   1.750 -
   1.751 -by (simp_tac (HOL_ss addsimps [insert_commute]) 2);
   1.752 -
   1.753 -
   1.754 -by (simp_tac (HOL_ss addsimps [analyze_insert_insert]) 2);
   1.755 -by (Asm_full_simp_tac 2);
   1.756 -by (simp_tac (!simpset addsimps [insert_absorb]) 2);
   1.757 -
   1.758 -
   1.759 -by (stac analyze_insert_Decrypt 2);
   1.760 -
   1.761 -
   1.762 -goal thy "analyze (insert X (insert Y H)) = analyze (insert X (analyze (insert Y H)))";
   1.763 -br analyze_insert_cong 1;
   1.764 -by (Simp_tac 1);
   1.765 -qed "analyze_insert_insert";
   1.766 -
   1.767 -
   1.768 -
   1.769 -
   1.770 -
   1.771 -
   1.772 -
   1.773 - 1. !!evs A B K NA S X evsa evs' ia evs'a.
   1.774 -       [| i ~= k; j ~= k;
   1.775 -          Says S (Friend ia)
   1.776 -           (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia))) #
   1.777 -          evs' :
   1.778 -          traces;
   1.779 -          Friend ia ~= B;
   1.780 -          Says (Friend ia) Server {|Agent (Friend ia), Agent B, Nonce NA|} :
   1.781 -          setOfList evs';
   1.782 -          Says Server (Friend i)
   1.783 -           (Crypt
   1.784 -             {|N, Agent (Friend j), Key (newK evs'a),
   1.785 -              Crypt {|Key (newK evs'a), Agent (Friend i)|}
   1.786 -               (serverKey (Friend j))|}
   1.787 -             K') :
   1.788 -          setOfList evs';
   1.789 -          length evs'a < length evs'; ia ~= k;
   1.790 -          Key (newK evs'a) ~:
   1.791 -          analyze (insert (Key (serverKey (Friend k))) (sees Enemy evs')) |] ==>
   1.792 -       Key (newK evs'a) ~:
   1.793 -       analyze
   1.794 -        (insert X
   1.795 -          (insert
   1.796 -            (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey (Friend ia)))
   1.797 -            (insert (Key (serverKey (Friend k))) (sees Enemy evs'))))
   1.798 -
   1.799 -
   1.800 -by (ALLGOALS Asm_full_simp_tac);
   1.801 -
   1.802 -by (Asm_full_simp_tac 1);
   1.803 -
   1.804 -by (asm_simp_tac (!simpset addsimps [insert_not_analyze_serverKey]) 1);
   1.805 -fr insert_not_analyze_serverKey;
   1.806 -by (fast_tac (!claset addSEs [traces_ConsE]) 1);
   1.807 -
   1.808 -by (forward_tac [traces_ConsE] 1);
   1.809 -
   1.810 -
   1.811 -
   1.812 -by (asm_full_simp_tac (!simpset addsimps [analyze_subset_parts RS contra_subsetD]) 1);
   1.813 -
   1.814 -
   1.815 -
   1.816 -auto();
   1.817 -
   1.818 -by (REPEAT_FIRST (resolve_tac [conjI, impI]   (*DELETE NEXT TWO LINES??*)
   1.819 -          ORELSE' eresolve_tac [conjE]
   1.820 -          ORELSE' hyp_subst_tac));
   1.821 -
   1.822 -by (forward_tac [Says_Server_message_form] 2);
   1.823 -
   1.824 -bd Says_Server_message_form 2;
   1.825 -by (fast_tac (!claset addSEs [traces_ConsE]) 2);
   1.826 -auto();
   1.827 -by (ALLGOALS (full_simp_tac (!simpset addsimps [insert_Key_delay])));
   1.828 -
   1.829 -(*SUBGOAL 1: use analyze_insert_Crypt to pull out
   1.830 -       Crypt{|...|} (serverKey (Friend i))
   1.831 -  SUBGOAL 2: cannot do this, as we don't seem to have ia~=j
   1.832 -*)
   1.833 -
   1.834 -
   1.835 -
   1.836 -qed "Enemy_not_see_encrypted_key";
   1.837 -
   1.838 -XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
   1.839 -
   1.840 -
   1.841  
   1.842  
   1.843  YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
   1.844 @@ -1161,9 +922,9 @@
   1.845  goal thy 
   1.846   "!!evs. evs : traces ==>                             \
   1.847  \    ALL A B X i. Says A B (Crypt X (serverKey (Friend i))) \
   1.848 -\        : setOfList evs  -->   \
   1.849 -\    (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : setOfList evs | \
   1.850 -\            Says (Friend i) B' (Crypt X (serverKey (Friend i))) : setOfList evs)";
   1.851 +\        : set_of_list evs  -->   \
   1.852 +\    (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : set_of_list evs | \
   1.853 +\            Says (Friend i) B' (Crypt X (serverKey (Friend i))) : set_of_list evs)";
   1.854  be traces.induct 1;
   1.855  be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
   1.856  by (Step_tac 1);
   1.857 @@ -1200,10 +961,10 @@
   1.858  by (Best_tac 2);
   1.859  
   1.860  by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
   1.861 -be Crypt_synthesize 1;
   1.862 -be Key_synthesize 2;
   1.863 +be Crypt_synth 1;
   1.864 +be Key_synth 2;
   1.865  
   1.866 -(*Split up the possibilities of that message being synthesized...*)
   1.867 +(*Split up the possibilities of that message being synthd...*)
   1.868  by (Step_tac 1);
   1.869  by (Best_tac 6);
   1.870  
     2.1 --- a/src/HOL/Auth/Event.thy	Mon Aug 19 11:19:16 1996 +0200
     2.2 +++ b/src/HOL/Auth/Event.thy	Mon Aug 19 11:19:55 1996 +0200
     2.3 @@ -60,7 +60,7 @@
     2.4  
     2.5  constdefs
     2.6    knownBy :: [event list, msg] => agent set
     2.7 -  "knownBy evs X == {A. X: analyze (sees A evs)}"
     2.8 +  "knownBy evs X == {A. X: analz (sees A evs)}"
     2.9  
    2.10  
    2.11  (*Agents generate "random" nonces.  Different traces always yield
    2.12 @@ -95,7 +95,7 @@
    2.13      (*The enemy MAY say anything he CAN say.  We do not expect him to
    2.14        invent new nonces here, but he can also use NS1.*)
    2.15      Fake "[| evs: traces;  B ~= Enemy;  
    2.16 -             X: synthesize(analyze(sees Enemy evs))
    2.17 +             X: synth(analz(sees Enemy evs))
    2.18            |] ==> (Says Enemy B X) # evs : traces"
    2.19  
    2.20      NS1  "[| evs: traces;  A ~= Server
    2.21 @@ -118,15 +118,15 @@
    2.22                                (serverKey A))) 
    2.23                     # evs';
    2.24               A = Friend i;
    2.25 -             (Says A Server {|Agent A, Agent B, Nonce NA|}) : setOfList evs'
    2.26 +             (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs'
    2.27            |] ==> (Says A B X) # evs : traces"
    2.28  
    2.29  (*Initial version of NS2 had 
    2.30  
    2.31          {|Agent A, Agent B, Key (newK evs), Nonce NA|}
    2.32  
    2.33 -  for the encrypted part; the version above is LESS transparent, hence
    2.34 -  maybe HARDER to prove.  Also it is precisely as in the BAN paper.
    2.35 +  for the encrypted part; the version above is LESS explicit, hence
    2.36 +  HARDER to prove.  Also it is precisely as in the BAN paper.
    2.37  *)
    2.38  
    2.39  end
     3.1 --- a/src/HOL/Auth/Message.ML	Mon Aug 19 11:19:16 1996 +0200
     3.2 +++ b/src/HOL/Auth/Message.ML	Mon Aug 19 11:19:55 1996 +0200
     3.3 @@ -4,30 +4,12 @@
     3.4      Copyright   1996  University of Cambridge
     3.5  
     3.6  Datatypes of agents and messages;
     3.7 -Inductive relations "parts", "analyze" and "synthesize"
     3.8 +Inductive relations "parts", "analz" and "synth"
     3.9  *)
    3.10  
    3.11  open Message;
    3.12  
    3.13  
    3.14 -(**************** INSTALL CENTRALLY SOMEWHERE? ****************)
    3.15 -
    3.16 -(*Maybe swap the safe_tac and simp_tac lines?**)
    3.17 -fun auto_tac (cs,ss) = 
    3.18 -    TRY (safe_tac cs) THEN 
    3.19 -    ALLGOALS (asm_full_simp_tac ss) THEN
    3.20 -    REPEAT (FIRSTGOAL (best_tac (cs addss ss)));
    3.21 -
    3.22 -fun Auto_tac() = auto_tac (!claset, !simpset);
    3.23 -
    3.24 -fun auto() = by (Auto_tac());
    3.25 -
    3.26 -fun impOfSubs th = th RSN (2, rev_subsetD);
    3.27 -
    3.28 -(**************** INSTALL CENTRALLY SOMEWHERE? ****************)
    3.29 -
    3.30 -
    3.31 -
    3.32  (** Inverse of keys **)
    3.33  
    3.34  goal thy "!!K K'. (invKey K = invKey K') = (K=K')";
    3.35 @@ -172,7 +154,7 @@
    3.36  by (simp_tac (!simpset addsimps [UNION1_def, parts_UN]) 1);
    3.37  qed "parts_UN1";
    3.38  
    3.39 -(*Added to simplify arguments to parts, analyze and synthesize*)
    3.40 +(*Added to simplify arguments to parts, analz and synth*)
    3.41  Addsimps [parts_Un, parts_UN, parts_UN1];
    3.42  
    3.43  goal thy "insert X (parts H) <= parts(insert X H)";
    3.44 @@ -259,362 +241,360 @@
    3.45  	  parts_insert_Key, parts_insert_Crypt, parts_insert_MPair];
    3.46  
    3.47  
    3.48 -(**** Inductive relation "analyze" ****)
    3.49 +(**** Inductive relation "analz" ****)
    3.50  
    3.51  val major::prems = 
    3.52 -goal thy "[| {|X,Y|} : analyze H;       \
    3.53 -\            [| X : analyze H; Y : analyze H |] ==> P  \
    3.54 +goal thy "[| {|X,Y|} : analz H;       \
    3.55 +\            [| X : analz H; Y : analz H |] ==> P  \
    3.56  \         |] ==> P";
    3.57  by (cut_facts_tac [major] 1);
    3.58  brs prems 1;
    3.59 -by (REPEAT (eresolve_tac [asm_rl, analyze.Fst, analyze.Snd] 1));
    3.60 -qed "MPair_analyze";
    3.61 +by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1));
    3.62 +qed "MPair_analz";
    3.63  
    3.64 -AddIs  [analyze.Inj];
    3.65 -AddSEs [MPair_analyze];
    3.66 -AddDs  [analyze.Decrypt];
    3.67 +AddIs  [analz.Inj];
    3.68 +AddSEs [MPair_analz];
    3.69 +AddDs  [analz.Decrypt];
    3.70  
    3.71 -Addsimps [analyze.Inj];
    3.72 +Addsimps [analz.Inj];
    3.73  
    3.74 -goal thy "H <= analyze(H)";
    3.75 +goal thy "H <= analz(H)";
    3.76  by (Fast_tac 1);
    3.77 -qed "analyze_increasing";
    3.78 +qed "analz_increasing";
    3.79  
    3.80 -goal thy "analyze H <= parts H";
    3.81 +goal thy "analz H <= parts H";
    3.82  by (rtac subsetI 1);
    3.83 -be analyze.induct 1;
    3.84 +be analz.induct 1;
    3.85  by (ALLGOALS Fast_tac);
    3.86 -qed "analyze_subset_parts";
    3.87 +qed "analz_subset_parts";
    3.88  
    3.89 -bind_thm ("not_parts_not_analyze", analyze_subset_parts RS contra_subsetD);
    3.90 +bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD);
    3.91  
    3.92  
    3.93 -goal thy "parts (analyze H) = parts H";
    3.94 +goal thy "parts (analz H) = parts H";
    3.95  br equalityI 1;
    3.96 -br (analyze_subset_parts RS parts_mono RS subset_trans) 1;
    3.97 +br (analz_subset_parts RS parts_mono RS subset_trans) 1;
    3.98  by (Simp_tac 1);
    3.99 -by (fast_tac (!claset addDs [analyze_increasing RS parts_mono RS subsetD]) 1);
   3.100 -qed "parts_analyze";
   3.101 -Addsimps [parts_analyze];
   3.102 +by (fast_tac (!claset addDs [analz_increasing RS parts_mono RS subsetD]) 1);
   3.103 +qed "parts_analz";
   3.104 +Addsimps [parts_analz];
   3.105  
   3.106 -goal thy "analyze (parts H) = parts H";
   3.107 +goal thy "analz (parts H) = parts H";
   3.108  by (Auto_tac());
   3.109 -be analyze.induct 1;
   3.110 +be analz.induct 1;
   3.111  by (Auto_tac());
   3.112 -qed "analyze_parts";
   3.113 -Addsimps [analyze_parts];
   3.114 +qed "analz_parts";
   3.115 +Addsimps [analz_parts];
   3.116  
   3.117  (*Monotonicity; Lemma 1 of Lowe*)
   3.118 -goalw thy analyze.defs "!!G H. G<=H ==> analyze(G) <= analyze(H)";
   3.119 +goalw thy analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)";
   3.120  by (rtac lfp_mono 1);
   3.121  by (REPEAT (ares_tac basic_monos 1));
   3.122 -qed "analyze_mono";
   3.123 +qed "analz_mono";
   3.124  
   3.125  (** General equational properties **)
   3.126  
   3.127 -goal thy "analyze{} = {}";
   3.128 +goal thy "analz{} = {}";
   3.129  by (Step_tac 1);
   3.130 -be analyze.induct 1;
   3.131 +be analz.induct 1;
   3.132  by (ALLGOALS Fast_tac);
   3.133 -qed "analyze_empty";
   3.134 -Addsimps [analyze_empty];
   3.135 +qed "analz_empty";
   3.136 +Addsimps [analz_empty];
   3.137  
   3.138 -(*Converse fails: we can analyze more from the union than from the 
   3.139 +(*Converse fails: we can analz more from the union than from the 
   3.140    separate parts, as a key in one might decrypt a message in the other*)
   3.141 -goal thy "analyze(G) Un analyze(H) <= analyze(G Un H)";
   3.142 -by (REPEAT (ares_tac [Un_least, analyze_mono, Un_upper1, Un_upper2] 1));
   3.143 -qed "analyze_Un";
   3.144 +goal thy "analz(G) Un analz(H) <= analz(G Un H)";
   3.145 +by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1));
   3.146 +qed "analz_Un";
   3.147  
   3.148 -goal thy "insert X (analyze H) <= analyze(insert X H)";
   3.149 -by (fast_tac (!claset addEs [impOfSubs analyze_mono]) 1);
   3.150 -qed "analyze_insert";
   3.151 +goal thy "insert X (analz H) <= analz(insert X H)";
   3.152 +by (fast_tac (!claset addEs [impOfSubs analz_mono]) 1);
   3.153 +qed "analz_insert";
   3.154  
   3.155  (** Rewrite rules for pulling out atomic messages **)
   3.156  
   3.157 -goal thy "analyze (insert (Agent agt) H) = insert (Agent agt) (analyze H)";
   3.158 -by (rtac (analyze_insert RSN (2, equalityI)) 1);
   3.159 +goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
   3.160 +by (rtac (analz_insert RSN (2, equalityI)) 1);
   3.161  br subsetI 1;
   3.162 -be analyze.induct 1;
   3.163 +be analz.induct 1;
   3.164  (*Simplification breaks up equalities between messages;
   3.165    how to make it work for fast_tac??*)
   3.166  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.167 -qed "analyze_insert_Agent";
   3.168 +qed "analz_insert_Agent";
   3.169  
   3.170 -goal thy "analyze (insert (Nonce N) H) = insert (Nonce N) (analyze H)";
   3.171 -by (rtac (analyze_insert RSN (2, equalityI)) 1);
   3.172 +goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
   3.173 +by (rtac (analz_insert RSN (2, equalityI)) 1);
   3.174  br subsetI 1;
   3.175 -be analyze.induct 1;
   3.176 +be analz.induct 1;
   3.177  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.178 -qed "analyze_insert_Nonce";
   3.179 +qed "analz_insert_Nonce";
   3.180  
   3.181  (*Can only pull out Keys if they are not needed to decrypt the rest*)
   3.182  goalw thy [keysFor_def]
   3.183 -    "!!K. K ~: keysFor (analyze H) ==>  \
   3.184 -\         analyze (insert (Key K) H) = insert (Key K) (analyze H)";
   3.185 -by (rtac (analyze_insert RSN (2, equalityI)) 1);
   3.186 +    "!!K. K ~: keysFor (analz H) ==>  \
   3.187 +\         analz (insert (Key K) H) = insert (Key K) (analz H)";
   3.188 +by (rtac (analz_insert RSN (2, equalityI)) 1);
   3.189  br subsetI 1;
   3.190 -be analyze.induct 1;
   3.191 +be analz.induct 1;
   3.192  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.193 -qed "analyze_insert_Key";
   3.194 +qed "analz_insert_Key";
   3.195  
   3.196 -goal thy "analyze (insert {|X,Y|} H) = \
   3.197 -\         insert {|X,Y|} (analyze (insert X (insert Y H)))";
   3.198 +goal thy "analz (insert {|X,Y|} H) = \
   3.199 +\         insert {|X,Y|} (analz (insert X (insert Y H)))";
   3.200  br equalityI 1;
   3.201  br subsetI 1;
   3.202 -be analyze.induct 1;
   3.203 +be analz.induct 1;
   3.204  by (Auto_tac());
   3.205 -be analyze.induct 1;
   3.206 -by (ALLGOALS (deepen_tac (!claset addIs [analyze.Fst, analyze.Snd, analyze.Decrypt]) 0));
   3.207 -qed "analyze_insert_MPair";
   3.208 +be analz.induct 1;
   3.209 +by (ALLGOALS (deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0));
   3.210 +qed "analz_insert_MPair";
   3.211  
   3.212  (*Can pull out enCrypted message if the Key is not known*)
   3.213 -goal thy "!!H. Key (invKey K) ~: analyze H ==>  \
   3.214 -\              analyze (insert (Crypt X K) H) = \
   3.215 -\              insert (Crypt X K) (analyze H)";
   3.216 -by (rtac (analyze_insert RSN (2, equalityI)) 1);
   3.217 +goal thy "!!H. Key (invKey K) ~: analz H ==>  \
   3.218 +\              analz (insert (Crypt X K) H) = \
   3.219 +\              insert (Crypt X K) (analz H)";
   3.220 +by (rtac (analz_insert RSN (2, equalityI)) 1);
   3.221  br subsetI 1;
   3.222 -be analyze.induct 1;
   3.223 +be analz.induct 1;
   3.224  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.225 -qed "analyze_insert_Crypt";
   3.226 +qed "analz_insert_Crypt";
   3.227  
   3.228 -goal thy "!!H. Key (invKey K) : analyze H ==>  \
   3.229 -\              analyze (insert (Crypt X K) H) <= \
   3.230 -\              insert (Crypt X K) (analyze (insert X H))";
   3.231 +goal thy "!!H. Key (invKey K) : analz H ==>  \
   3.232 +\              analz (insert (Crypt X K) H) <= \
   3.233 +\              insert (Crypt X K) (analz (insert X H))";
   3.234  br subsetI 1;
   3.235 -by (eres_inst_tac [("za","x")] analyze.induct 1);
   3.236 +by (eres_inst_tac [("za","x")] analz.induct 1);
   3.237  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.238  val lemma1 = result();
   3.239  
   3.240 -goal thy "!!H. Key (invKey K) : analyze H ==>  \
   3.241 -\              insert (Crypt X K) (analyze (insert X H)) <= \
   3.242 -\              analyze (insert (Crypt X K) H)";
   3.243 +goal thy "!!H. Key (invKey K) : analz H ==>  \
   3.244 +\              insert (Crypt X K) (analz (insert X H)) <= \
   3.245 +\              analz (insert (Crypt X K) H)";
   3.246  by (Auto_tac());
   3.247 -by (eres_inst_tac [("za","x")] analyze.induct 1);
   3.248 +by (eres_inst_tac [("za","x")] analz.induct 1);
   3.249  by (Auto_tac());
   3.250 -by (best_tac (!claset addIs [subset_insertI RS analyze_mono RS subsetD,
   3.251 -			     analyze.Decrypt]) 1);
   3.252 +by (best_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD,
   3.253 +			     analz.Decrypt]) 1);
   3.254  val lemma2 = result();
   3.255  
   3.256 -goal thy "!!H. Key (invKey K) : analyze H ==>  \
   3.257 -\              analyze (insert (Crypt X K) H) = \
   3.258 -\              insert (Crypt X K) (analyze (insert X H))";
   3.259 +goal thy "!!H. Key (invKey K) : analz H ==>  \
   3.260 +\              analz (insert (Crypt X K) H) = \
   3.261 +\              insert (Crypt X K) (analz (insert X H))";
   3.262  by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
   3.263 -qed "analyze_insert_Decrypt";
   3.264 +qed "analz_insert_Decrypt";
   3.265  
   3.266  (*Case analysis: either the message is secure, or it is not!
   3.267    Use with expand_if;  apparently split_tac does not cope with patterns
   3.268 -  such as "analyze (insert (Crypt X' K) H)" *)
   3.269 -goal thy "analyze (insert (Crypt X' K) H) = \
   3.270 -\         (if (Key (invKey K)  : analyze H) then    \
   3.271 -\               insert (Crypt X' K) (analyze (insert X' H)) \
   3.272 -\          else insert (Crypt X' K) (analyze H))";
   3.273 -by (excluded_middle_tac "Key (invKey K)  : analyze H " 1);
   3.274 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [analyze_insert_Crypt, 
   3.275 -					       analyze_insert_Decrypt])));
   3.276 -qed "analyze_Crypt_if";
   3.277 +  such as "analz (insert (Crypt X' K) H)" *)
   3.278 +goal thy "analz (insert (Crypt X' K) H) = \
   3.279 +\         (if (Key (invKey K)  : analz H) then    \
   3.280 +\               insert (Crypt X' K) (analz (insert X' H)) \
   3.281 +\          else insert (Crypt X' K) (analz H))";
   3.282 +by (excluded_middle_tac "Key (invKey K)  : analz H " 1);
   3.283 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 
   3.284 +					       analz_insert_Decrypt])));
   3.285 +qed "analz_Crypt_if";
   3.286  
   3.287 -Addsimps [analyze_insert_Agent, analyze_insert_Nonce, 
   3.288 -	  analyze_insert_Key, analyze_insert_MPair, 
   3.289 -	  analyze_Crypt_if];
   3.290 +Addsimps [analz_insert_Agent, analz_insert_Nonce, 
   3.291 +	  analz_insert_Key, analz_insert_MPair, 
   3.292 +	  analz_Crypt_if];
   3.293  
   3.294  (*This rule supposes "for the sake of argument" that we have the key.*)
   3.295 -goal thy  "analyze (insert (Crypt X K) H) <=  \
   3.296 -\          insert (Crypt X K) (analyze (insert X H))";
   3.297 +goal thy  "analz (insert (Crypt X K) H) <=  \
   3.298 +\          insert (Crypt X K) (analz (insert X H))";
   3.299  br subsetI 1;
   3.300 -be analyze.induct 1;
   3.301 +be analz.induct 1;
   3.302  by (Auto_tac());
   3.303 -qed "analyze_insert_Crypt_subset";
   3.304 +qed "analz_insert_Crypt_subset";
   3.305  
   3.306  
   3.307  (** Idempotence and transitivity **)
   3.308  
   3.309 -goal thy "!!H. X: analyze (analyze H) ==> X: analyze H";
   3.310 -be analyze.induct 1;
   3.311 +goal thy "!!H. X: analz (analz H) ==> X: analz H";
   3.312 +be analz.induct 1;
   3.313  by (ALLGOALS Fast_tac);
   3.314 -qed "analyze_analyzeE";
   3.315 -AddSEs [analyze_analyzeE];
   3.316 +qed "analz_analzE";
   3.317 +AddSEs [analz_analzE];
   3.318  
   3.319 -goal thy "analyze (analyze H) = analyze H";
   3.320 +goal thy "analz (analz H) = analz H";
   3.321  by (Fast_tac 1);
   3.322 -qed "analyze_idem";
   3.323 -Addsimps [analyze_idem];
   3.324 +qed "analz_idem";
   3.325 +Addsimps [analz_idem];
   3.326  
   3.327 -goal thy "!!H. [| X: analyze G;  G <= analyze H |] ==> X: analyze H";
   3.328 -by (dtac analyze_mono 1);
   3.329 +goal thy "!!H. [| X: analz G;  G <= analz H |] ==> X: analz H";
   3.330 +by (dtac analz_mono 1);
   3.331  by (Fast_tac 1);
   3.332 -qed "analyze_trans";
   3.333 +qed "analz_trans";
   3.334  
   3.335  (*Cut; Lemma 2 of Lowe*)
   3.336 -goal thy "!!H. [| X: analyze H;  Y: analyze (insert X H) |] ==> Y: analyze H";
   3.337 -be analyze_trans 1;
   3.338 +goal thy "!!H. [| X: analz H;  Y: analz (insert X H) |] ==> Y: analz H";
   3.339 +be analz_trans 1;
   3.340  by (Fast_tac 1);
   3.341 -qed "analyze_cut";
   3.342 +qed "analz_cut";
   3.343  
   3.344  (*Cut can be proved easily by induction on
   3.345 -   "!!H. Y: analyze (insert X H) ==> X: analyze H --> Y: analyze H"
   3.346 +   "!!H. Y: analz (insert X H) ==> X: analz H --> Y: analz H"
   3.347  *)
   3.348  
   3.349  
   3.350 -(** A congruence rule for "analyze" **)
   3.351 +(** A congruence rule for "analz" **)
   3.352  
   3.353 -goal thy "!!H. [| analyze G <= analyze G'; analyze H <= analyze H' \
   3.354 -\              |] ==> analyze (G Un H) <= analyze (G' Un H')";
   3.355 +goal thy "!!H. [| analz G <= analz G'; analz H <= analz H' \
   3.356 +\              |] ==> analz (G Un H) <= analz (G' Un H')";
   3.357  by (Step_tac 1);
   3.358 -be analyze.induct 1;
   3.359 -by (ALLGOALS (best_tac (!claset addIs [analyze_mono RS subsetD])));
   3.360 -qed "analyze_subset_cong";
   3.361 +be analz.induct 1;
   3.362 +by (ALLGOALS (best_tac (!claset addIs [analz_mono RS subsetD])));
   3.363 +qed "analz_subset_cong";
   3.364  
   3.365 -goal thy "!!H. [| analyze G = analyze G'; analyze H = analyze H' \
   3.366 -\              |] ==> analyze (G Un H) = analyze (G' Un H')";
   3.367 -by (REPEAT_FIRST (ares_tac [equalityI, analyze_subset_cong]
   3.368 +goal thy "!!H. [| analz G = analz G'; analz H = analz H' \
   3.369 +\              |] ==> analz (G Un H) = analz (G' Un H')";
   3.370 +by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong]
   3.371  	  ORELSE' etac equalityE));
   3.372 -qed "analyze_cong";
   3.373 +qed "analz_cong";
   3.374  
   3.375  
   3.376 -goal thy "!!H. analyze H = analyze H'  ==>    \
   3.377 -\              analyze (insert X H) = analyze (insert X H')";
   3.378 +goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
   3.379  by (asm_simp_tac (!simpset addsimps [insert_def] 
   3.380 -		           setloop (rtac analyze_cong)) 1);
   3.381 -qed "analyze_insert_cong";
   3.382 +		           setloop (rtac analz_cong)) 1);
   3.383 +qed "analz_insert_cong";
   3.384  
   3.385 -(*If there are no pairs or encryptions then analyze does nothing*)
   3.386 +(*If there are no pairs or encryptions then analz does nothing*)
   3.387  goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt X K ~: H |] ==> \
   3.388 -\         analyze H = H";
   3.389 +\         analz H = H";
   3.390  by (Step_tac 1);
   3.391 -be analyze.induct 1;
   3.392 +be analz.induct 1;
   3.393  by (ALLGOALS Fast_tac);
   3.394 -qed "analyze_trivial";
   3.395 +qed "analz_trivial";
   3.396  
   3.397  (*Helps to prove Fake cases*)
   3.398 -goal thy "!!X. X: analyze (UN i. analyze (H i)) ==> X: analyze (UN i. H i)";
   3.399 -be analyze.induct 1;
   3.400 -by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analyze_mono])));
   3.401 +goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)";
   3.402 +be analz.induct 1;
   3.403 +by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analz_mono])));
   3.404  val lemma = result();
   3.405  
   3.406 -goal thy "analyze (UN i. analyze (H i)) = analyze (UN i. H i)";
   3.407 +goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)";
   3.408  by (fast_tac (!claset addIs [lemma]
   3.409 -		      addEs [impOfSubs analyze_mono]) 1);
   3.410 -qed "analyze_UN_analyze";
   3.411 -Addsimps [analyze_UN_analyze];
   3.412 +		      addEs [impOfSubs analz_mono]) 1);
   3.413 +qed "analz_UN_analz";
   3.414 +Addsimps [analz_UN_analz];
   3.415  
   3.416  
   3.417 -(**** Inductive relation "synthesize" ****)
   3.418 +(**** Inductive relation "synth" ****)
   3.419  
   3.420 -AddIs  synthesize.intrs;
   3.421 +AddIs  synth.intrs;
   3.422  
   3.423 -goal thy "H <= synthesize(H)";
   3.424 +goal thy "H <= synth(H)";
   3.425  by (Fast_tac 1);
   3.426 -qed "synthesize_increasing";
   3.427 +qed "synth_increasing";
   3.428  
   3.429  (*Monotonicity*)
   3.430 -goalw thy synthesize.defs "!!G H. G<=H ==> synthesize(G) <= synthesize(H)";
   3.431 +goalw thy synth.defs "!!G H. G<=H ==> synth(G) <= synth(H)";
   3.432  by (rtac lfp_mono 1);
   3.433  by (REPEAT (ares_tac basic_monos 1));
   3.434 -qed "synthesize_mono";
   3.435 +qed "synth_mono";
   3.436  
   3.437  (** Unions **)
   3.438  
   3.439 -(*Converse fails: we can synthesize more from the union than from the 
   3.440 +(*Converse fails: we can synth more from the union than from the 
   3.441    separate parts, building a compound message using elements of each.*)
   3.442 -goal thy "synthesize(G) Un synthesize(H) <= synthesize(G Un H)";
   3.443 -by (REPEAT (ares_tac [Un_least, synthesize_mono, Un_upper1, Un_upper2] 1));
   3.444 -qed "synthesize_Un";
   3.445 +goal thy "synth(G) Un synth(H) <= synth(G Un H)";
   3.446 +by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1));
   3.447 +qed "synth_Un";
   3.448  
   3.449 -goal thy "insert X (synthesize H) <= synthesize(insert X H)";
   3.450 -by (fast_tac (!claset addEs [impOfSubs synthesize_mono]) 1);
   3.451 -qed "synthesize_insert";
   3.452 +goal thy "insert X (synth H) <= synth(insert X H)";
   3.453 +by (fast_tac (!claset addEs [impOfSubs synth_mono]) 1);
   3.454 +qed "synth_insert";
   3.455  
   3.456  (** Idempotence and transitivity **)
   3.457  
   3.458 -goal thy "!!H. X: synthesize (synthesize H) ==> X: synthesize H";
   3.459 -be synthesize.induct 1;
   3.460 +goal thy "!!H. X: synth (synth H) ==> X: synth H";
   3.461 +be synth.induct 1;
   3.462  by (ALLGOALS Fast_tac);
   3.463 -qed "synthesize_synthesizeE";
   3.464 -AddSEs [synthesize_synthesizeE];
   3.465 +qed "synth_synthE";
   3.466 +AddSEs [synth_synthE];
   3.467  
   3.468 -goal thy "synthesize (synthesize H) = synthesize H";
   3.469 +goal thy "synth (synth H) = synth H";
   3.470  by (Fast_tac 1);
   3.471 -qed "synthesize_idem";
   3.472 +qed "synth_idem";
   3.473  
   3.474 -goal thy "!!H. [| X: synthesize G;  G <= synthesize H |] ==> X: synthesize H";
   3.475 -by (dtac synthesize_mono 1);
   3.476 +goal thy "!!H. [| X: synth G;  G <= synth H |] ==> X: synth H";
   3.477 +by (dtac synth_mono 1);
   3.478  by (Fast_tac 1);
   3.479 -qed "synthesize_trans";
   3.480 +qed "synth_trans";
   3.481  
   3.482  (*Cut; Lemma 2 of Lowe*)
   3.483 -goal thy "!!H. [| X: synthesize H;  Y: synthesize (insert X H) \
   3.484 -\              |] ==> Y: synthesize H";
   3.485 -be synthesize_trans 1;
   3.486 +goal thy "!!H. [| X: synth H;  Y: synth (insert X H) |] ==> Y: synth H";
   3.487 +be synth_trans 1;
   3.488  by (Fast_tac 1);
   3.489 -qed "synthesize_cut";
   3.490 +qed "synth_cut";
   3.491  
   3.492  
   3.493  (*Can only produce a nonce or key if it is already known,
   3.494 -  but can synthesize a pair or encryption from its components...*)
   3.495 -val mk_cases = synthesize.mk_cases msg.simps;
   3.496 +  but can synth a pair or encryption from its components...*)
   3.497 +val mk_cases = synth.mk_cases msg.simps;
   3.498  
   3.499 -(*NO Agent_synthesize, as any Agent name can be synthesized*)
   3.500 -val Nonce_synthesize = mk_cases "Nonce n : synthesize H";
   3.501 -val Key_synthesize   = mk_cases "Key K : synthesize H";
   3.502 -val MPair_synthesize = mk_cases "{|X,Y|} : synthesize H";
   3.503 -val Crypt_synthesize = mk_cases "Crypt X K : synthesize H";
   3.504 +(*NO Agent_synth, as any Agent name can be synthd*)
   3.505 +val Nonce_synth = mk_cases "Nonce n : synth H";
   3.506 +val Key_synth   = mk_cases "Key K : synth H";
   3.507 +val MPair_synth = mk_cases "{|X,Y|} : synth H";
   3.508 +val Crypt_synth = mk_cases "Crypt X K : synth H";
   3.509  
   3.510 -AddSEs [Nonce_synthesize, Key_synthesize, MPair_synthesize, Crypt_synthesize];
   3.511 +AddSEs [Nonce_synth, Key_synth, MPair_synth, Crypt_synth];
   3.512  
   3.513 -goal thy "(Nonce N : synthesize H) = (Nonce N : H)";
   3.514 +goal thy "(Nonce N : synth H) = (Nonce N : H)";
   3.515  by (Fast_tac 1);
   3.516 -qed "Nonce_synthesize_eq";
   3.517 +qed "Nonce_synth_eq";
   3.518  
   3.519 -goal thy "(Key K : synthesize H) = (Key K : H)";
   3.520 +goal thy "(Key K : synth H) = (Key K : H)";
   3.521  by (Fast_tac 1);
   3.522 -qed "Key_synthesize_eq";
   3.523 +qed "Key_synth_eq";
   3.524  
   3.525 -Addsimps [Nonce_synthesize_eq, Key_synthesize_eq];
   3.526 +Addsimps [Nonce_synth_eq, Key_synth_eq];
   3.527  
   3.528  
   3.529  goalw thy [keysFor_def]
   3.530 -    "keysFor (synthesize H) = keysFor H Un invKey``{K. Key K : H}";
   3.531 +    "keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}";
   3.532  by (Fast_tac 1);
   3.533 -qed "keysFor_synthesize";
   3.534 -Addsimps [keysFor_synthesize];
   3.535 +qed "keysFor_synth";
   3.536 +Addsimps [keysFor_synth];
   3.537  
   3.538  
   3.539 -(*** Combinations of parts, analyze and synthesize ***)
   3.540 +(*** Combinations of parts, analz and synth ***)
   3.541  
   3.542 -goal thy "parts (synthesize H) = parts H Un synthesize H";
   3.543 +goal thy "parts (synth H) = parts H Un synth H";
   3.544  br equalityI 1;
   3.545  br subsetI 1;
   3.546  be parts.induct 1;
   3.547  by (ALLGOALS
   3.548 -    (best_tac (!claset addIs ((synthesize_increasing RS parts_mono RS subsetD)
   3.549 +    (best_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD)
   3.550  			     ::parts.intrs))));
   3.551 -qed "parts_synthesize";
   3.552 -Addsimps [parts_synthesize];
   3.553 +qed "parts_synth";
   3.554 +Addsimps [parts_synth];
   3.555  
   3.556 -goal thy "analyze (synthesize H) = analyze H Un synthesize H";
   3.557 +goal thy "analz (synth H) = analz H Un synth H";
   3.558  br equalityI 1;
   3.559  br subsetI 1;
   3.560 -be analyze.induct 1;
   3.561 +be analz.induct 1;
   3.562  by (best_tac
   3.563 -    (!claset addIs [synthesize_increasing RS analyze_mono RS subsetD]) 5);
   3.564 +    (!claset addIs [synth_increasing RS analz_mono RS subsetD]) 5);
   3.565  (*Strange that best_tac just can't hack this one...*)
   3.566 -by (ALLGOALS (deepen_tac (!claset addIs analyze.intrs) 0));
   3.567 -qed "analyze_synthesize";
   3.568 -Addsimps [analyze_synthesize];
   3.569 +by (ALLGOALS (deepen_tac (!claset addIs analz.intrs) 0));
   3.570 +qed "analz_synth";
   3.571 +Addsimps [analz_synth];
   3.572  
   3.573  (*Hard to prove; still needed now that there's only one Enemy?*)
   3.574 -goal thy "analyze (UN i. synthesize (H i)) = \
   3.575 -\         analyze (UN i. H i) Un (UN i. synthesize (H i))";
   3.576 +goal thy "analz (UN i. synth (H i)) = \
   3.577 +\         analz (UN i. H i) Un (UN i. synth (H i))";
   3.578  br equalityI 1;
   3.579  br subsetI 1;
   3.580 -be analyze.induct 1;
   3.581 +be analz.induct 1;
   3.582  by (best_tac
   3.583 -    (!claset addEs [impOfSubs synthesize_increasing,
   3.584 -		    impOfSubs analyze_mono]) 5);
   3.585 +    (!claset addEs [impOfSubs synth_increasing,
   3.586 +		    impOfSubs analz_mono]) 5);
   3.587  by (Best_tac 1);
   3.588 -by (deepen_tac (!claset addIs [analyze.Fst]) 0 1);
   3.589 -by (deepen_tac (!claset addIs [analyze.Snd]) 0 1);
   3.590 -by (deepen_tac (!claset addSEs [analyze.Decrypt]
   3.591 -			addIs  [analyze.Decrypt]) 0 1);
   3.592 -qed "analyze_UN1_synthesize";
   3.593 -Addsimps [analyze_UN1_synthesize];
   3.594 +by (deepen_tac (!claset addIs [analz.Fst]) 0 1);
   3.595 +by (deepen_tac (!claset addIs [analz.Snd]) 0 1);
   3.596 +by (deepen_tac (!claset addSEs [analz.Decrypt]
   3.597 +			addIs  [analz.Decrypt]) 0 1);
   3.598 +qed "analz_UN1_synth";
   3.599 +Addsimps [analz_UN1_synth];
     4.1 --- a/src/HOL/Auth/Message.thy	Mon Aug 19 11:19:16 1996 +0200
     4.2 +++ b/src/HOL/Auth/Message.thy	Mon Aug 19 11:19:55 1996 +0200
     4.3 @@ -4,7 +4,7 @@
     4.4      Copyright   1996  University of Cambridge
     4.5  
     4.6  Datatypes of agents and messages;
     4.7 -Inductive relations "parts", "analyze" and "synthesize"
     4.8 +Inductive relations "parts", "analz" and "synth"
     4.9  *)
    4.10  
    4.11  Message = Arith +
    4.12 @@ -77,38 +77,29 @@
    4.13      Body    "Crypt X K : parts H ==> X : parts H"
    4.14  
    4.15  
    4.16 -(** Inductive definition of "analyze" -- what can be broken down from a set of
    4.17 +(** Inductive definition of "analz" -- what can be broken down from a set of
    4.18      messages, including keys.  A form of downward closure.  Pairs can
    4.19      be taken apart; messages decrypted with known keys.  **)
    4.20  
    4.21 -consts  analyze   :: msg set => msg set
    4.22 -inductive "analyze H"
    4.23 +consts  analz   :: msg set => msg set
    4.24 +inductive "analz H"
    4.25    intrs 
    4.26 -    Inj     "X: H ==> X: analyze H"
    4.27 -
    4.28 -    Fst     "{|X,Y|} : analyze H ==> X : analyze H"
    4.29 -
    4.30 -    Snd     "{|X,Y|} : analyze H ==> Y : analyze H"
    4.31 -
    4.32 -    Decrypt "[| Crypt X K : analyze H; Key(invKey K): analyze H
    4.33 -             |] ==> X : analyze H"
    4.34 +    Inj     "X: H ==> X: analz H"
    4.35 +    Fst     "{|X,Y|} : analz H ==> X : analz H"
    4.36 +    Snd     "{|X,Y|} : analz H ==> Y : analz H"
    4.37 +    Decrypt "[| Crypt X K : analz H; Key(invKey K): analz H |] ==> X : analz H"
    4.38  
    4.39  
    4.40 -(** Inductive definition of "synthesize" -- what can be built up from a set of
    4.41 +(** Inductive definition of "synth" -- what can be built up from a set of
    4.42      messages.  A form of upward closure.  Pairs can be built, messages
    4.43      encrypted with known keys.  Agent names may be quoted.  **)
    4.44  
    4.45 -consts  synthesize   :: msg set => msg set
    4.46 -inductive "synthesize H"
    4.47 +consts  synth   :: msg set => msg set
    4.48 +inductive "synth H"
    4.49    intrs 
    4.50 -    Inj     "X: H ==> X: synthesize H"
    4.51 -
    4.52 -    Agent   "Agent agt : synthesize H"
    4.53 -
    4.54 -    MPair   "[| X: synthesize H;  Y: synthesize H
    4.55 -             |] ==> {|X,Y|} : synthesize H"
    4.56 -
    4.57 -    Crypt   "[| X: synthesize H; Key(K): synthesize H
    4.58 -             |] ==> Crypt X K : synthesize H"
    4.59 +    Inj     "X: H ==> X: synth H"
    4.60 +    Agent   "Agent agt : synth H"
    4.61 +    MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
    4.62 +    Crypt   "[| X: synth H; Key(K): synth H |] ==> Crypt X K : synth H"
    4.63  
    4.64  end