Tidied many proofs, using AddIffs to let equivalences take
authorpaulson
Thu Sep 12 10:40:05 1996 +0200 (1996-09-12)
changeset 198584cf16192e03
parent 1984 5cf82dc3ce67
child 1986 36f6bbf41477
Tidied many proofs, using AddIffs to let equivalences take
the place of separate Intr and Elim rules. Also deleted most named clasets.
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom.thy
src/HOL/IOA/NTP/Lemmas.ML
src/HOL/Lex/Auto.ML
src/HOL/List.ML
src/HOL/Nat.ML
src/HOL/Relation.ML
src/HOL/Set.ML
src/HOL/Sexp.ML
src/HOL/Sum.ML
src/HOL/Trancl.ML
src/HOL/Univ.ML
src/HOL/cladata.ML
src/HOL/ex/LList.ML
src/HOL/ex/SList.ML
src/HOL/ex/Simult.ML
src/HOL/indrule.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Sep 12 10:40:05 1996 +0200
     1.3 @@ -0,0 +1,446 @@
     1.4 +(*  Title:      HOL/Auth/OtwayRees
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Inductive relation "otway" for the Yahalom protocol.
    1.10 +
    1.11 +From page 257 of
    1.12 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    1.13 +  Proc. Royal Soc. 426 (1989)
    1.14 +*)
    1.15 +
    1.16 +open OtwayRees;
    1.17 +
    1.18 +proof_timing:=true;
    1.19 +HOL_quantifiers := false;
    1.20 +
    1.21 +(**** Inductive proofs about yahalom ****)
    1.22 +
    1.23 +(*The Enemy can see more than anybody else, except for their initial state*)
    1.24 +goal thy 
    1.25 + "!!evs. evs : yahalom ==> \
    1.26 +\     sees A evs <= initState A Un sees Enemy evs";
    1.27 +be yahalom.induct 1;
    1.28 +by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    1.29 +			        addss (!simpset))));
    1.30 +qed "sees_agent_subset_sees_Enemy";
    1.31 +
    1.32 +
    1.33 +(*Nobody sends themselves messages*)
    1.34 +goal thy "!!evs. evs : yahalom ==> ALL A X. Says A A X ~: set_of_list evs";
    1.35 +be yahalom.induct 1;
    1.36 +by (Auto_tac());
    1.37 +qed_spec_mp "not_Says_to_self";
    1.38 +Addsimps [not_Says_to_self];
    1.39 +AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    1.40 +
    1.41 +goal thy "!!evs. evs : yahalom ==> Notes A X ~: set_of_list evs";
    1.42 +be yahalom.induct 1;
    1.43 +by (Auto_tac());
    1.44 +qed "not_Notes";
    1.45 +Addsimps [not_Notes];
    1.46 +AddSEs   [not_Notes RSN (2, rev_notE)];
    1.47 +
    1.48 +
    1.49 +(** For reasoning about the encrypted portion of messages **)
    1.50 +
    1.51 +goal thy "!!evs. (Says A' B {|N, Agent A, Agent B, X|}) : set_of_list evs ==> \
    1.52 +\                X : analz (sees Enemy evs)";
    1.53 +by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    1.54 +qed "YM2_analz_sees_Enemy";
    1.55 +
    1.56 +goal thy "!!evs. (Says S B {|N, X, X'|}) : set_of_list evs ==> \
    1.57 +\                X : analz (sees Enemy evs)";
    1.58 +by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    1.59 +qed "YM4_analz_sees_Enemy";
    1.60 +
    1.61 +goal thy "!!evs. (Says B' A {|N, Crypt {|N,K|} K'|}) : set_of_list evs ==> \
    1.62 +\                K : parts (sees Enemy evs)";
    1.63 +by (fast_tac (!claset addSEs partsEs
    1.64 +	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    1.65 +qed "YM5_parts_sees_Enemy";
    1.66 +
    1.67 +(*YM2_analz... and YM4_analz... let us treat those cases using the same 
    1.68 +  argument as for the Fake case.  This is possible for most, but not all,
    1.69 +  proofs: Fake does not invent new nonces (as in YM2), and of course Fake
    1.70 +  messages originate from the Enemy. *)
    1.71 +
    1.72 +val YM2_YM4_tac = 
    1.73 +    dtac (YM2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
    1.74 +    dtac (YM4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6;
    1.75 +
    1.76 +
    1.77 +(*** Shared keys are not betrayed ***)
    1.78 +
    1.79 +(*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
    1.80 +goal thy 
    1.81 + "!!evs. [| evs : yahalom;  A ~: bad |] ==> \
    1.82 +\        Key (shrK A) ~: parts (sees Enemy evs)";
    1.83 +be yahalom.induct 1;
    1.84 +by YM2_YM4_tac;
    1.85 +by (Auto_tac());
    1.86 +(*Deals with Fake message*)
    1.87 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.88 +			     impOfSubs Fake_parts_insert]) 1);
    1.89 +qed "Enemy_not_see_shrK";
    1.90 +
    1.91 +bind_thm ("Enemy_not_analz_shrK",
    1.92 +	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
    1.93 +
    1.94 +Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK];
    1.95 +
    1.96 +(*We go to some trouble to preserve R in the 3rd and 4th subgoals
    1.97 +  As usual fast_tac cannot be used because it uses the equalities too soon*)
    1.98 +val major::prems = 
    1.99 +goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
   1.100 +\             evs : yahalom;                                 \
   1.101 +\             A:bad ==> R                                  \
   1.102 +\           |] ==> R";
   1.103 +br ccontr 1;
   1.104 +br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
   1.105 +by (swap_res_tac prems 2);
   1.106 +by (ALLGOALS (fast_tac (!claset addIs prems)));
   1.107 +qed "Enemy_see_shrK_E";
   1.108 +
   1.109 +bind_thm ("Enemy_analz_shrK_E", 
   1.110 +	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
   1.111 +
   1.112 +AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
   1.113 +
   1.114 +
   1.115 +(*** Future keys can't be seen or used! ***)
   1.116 +
   1.117 +(*Nobody can have SEEN keys that will be generated in the future.
   1.118 +  This has to be proved anew for each protocol description,
   1.119 +  but should go by similar reasoning every time.  Hardest case is the
   1.120 +  standard Fake rule.  
   1.121 +      The length comparison, and Union over C, are essential for the 
   1.122 +  induction! *)
   1.123 +goal thy "!!evs. evs : yahalom ==> \
   1.124 +\                length evs <= length evs' --> \
   1.125 +\                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   1.126 +be yahalom.induct 1;
   1.127 +by YM2_YM4_tac;
   1.128 +(*auto_tac does not work here, as it performs safe_tac first*)
   1.129 +by (ALLGOALS Asm_simp_tac);
   1.130 +by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.131 +				       impOfSubs parts_insert_subset_Un,
   1.132 +				       Suc_leD]
   1.133 +			        addss (!simpset))));
   1.134 +val lemma = result();
   1.135 +
   1.136 +(*Variant needed for the main theorem below*)
   1.137 +goal thy 
   1.138 + "!!evs. [| evs : yahalom;  length evs <= length evs' |] ==> \
   1.139 +\        Key (newK evs') ~: parts (sees C evs)";
   1.140 +by (fast_tac (!claset addDs [lemma]) 1);
   1.141 +qed "new_keys_not_seen";
   1.142 +Addsimps [new_keys_not_seen];
   1.143 +
   1.144 +(*Another variant: old messages must contain old keys!*)
   1.145 +goal thy 
   1.146 + "!!evs. [| Says A B X : set_of_list evs;  \
   1.147 +\           Key (newK evt) : parts {X};    \
   1.148 +\           evs : yahalom                 \
   1.149 +\        |] ==> length evt < length evs";
   1.150 +br ccontr 1;
   1.151 +by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   1.152 +	              addIs [impOfSubs parts_mono, leI]) 1);
   1.153 +qed "Says_imp_old_keys";
   1.154 +
   1.155 +
   1.156 +(*Nobody can have USED keys that will be generated in the future.
   1.157 +  ...very like new_keys_not_seen*)
   1.158 +goal thy "!!evs. evs : yahalom ==> \
   1.159 +\                length evs <= length evs' --> \
   1.160 +\                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   1.161 +be yahalom.induct 1;
   1.162 +by YM2_YM4_tac;
   1.163 +bd YM5_parts_sees_Enemy 7;
   1.164 +by (ALLGOALS Asm_simp_tac);
   1.165 +(*YM1 and YM3*)
   1.166 +by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   1.167 +(*Fake, YM2, YM4: these messages send unknown (X) components*)
   1.168 +by (EVERY 
   1.169 +    (map
   1.170 +     (best_tac
   1.171 +      (!claset addSDs [newK_invKey]
   1.172 +	       addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   1.173 +		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.174 +		      Suc_leD]
   1.175 +	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   1.176 +	       addss (!simpset)))
   1.177 +     [3,2,1]));
   1.178 +(*YM5: dummy message*)
   1.179 +by (best_tac (!claset addSDs [newK_invKey]
   1.180 +		        addEs  [new_keys_not_seen RSN(2,rev_notE)]
   1.181 +			addIs  [less_SucI, impOfSubs keysFor_mono]
   1.182 +			addss (!simpset addsimps [le_def])) 1);
   1.183 +val lemma = result();
   1.184 +
   1.185 +goal thy 
   1.186 + "!!evs. [| evs : yahalom;  length evs <= length evs' |] ==> \
   1.187 +\        newK evs' ~: keysFor (parts (sees C evs))";
   1.188 +by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   1.189 +qed "new_keys_not_used";
   1.190 +
   1.191 +bind_thm ("new_keys_not_analzd",
   1.192 +	  [analz_subset_parts RS keysFor_mono,
   1.193 +	   new_keys_not_used] MRS contra_subsetD);
   1.194 +
   1.195 +Addsimps [new_keys_not_used, new_keys_not_analzd];
   1.196 +
   1.197 +
   1.198 +(** Lemmas concerning the form of items passed in messages **)
   1.199 +
   1.200 +
   1.201 +(****
   1.202 + The following is to prove theorems of the form
   1.203 +
   1.204 +          Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
   1.205 +          Key K : analz (sees Enemy evs)
   1.206 +
   1.207 + A more general formula must be proved inductively.
   1.208 +
   1.209 +****)
   1.210 +
   1.211 +
   1.212 +(*NOT useful in this form, but it says that session keys are not used
   1.213 +  to encrypt messages containing other keys, in the actual protocol.
   1.214 +  We require that agents should behave like this subsequently also.*)
   1.215 +goal thy 
   1.216 + "!!evs. evs : yahalom ==> \
   1.217 +\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   1.218 +\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   1.219 +be yahalom.induct 1;
   1.220 +by YM2_YM4_tac;
   1.221 +by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.222 +(*Deals with Faked messages*)
   1.223 +by (best_tac (!claset addSEs partsEs
   1.224 +		      addDs [impOfSubs analz_subset_parts,
   1.225 +                             impOfSubs parts_insert_subset_Un]
   1.226 +                      addss (!simpset)) 2);
   1.227 +(*Base case and YM5*)
   1.228 +by (Auto_tac());
   1.229 +result();
   1.230 +
   1.231 +
   1.232 +(** Specialized rewriting for this proof **)
   1.233 +
   1.234 +Delsimps [image_insert];
   1.235 +Addsimps [image_insert RS sym];
   1.236 +
   1.237 +Delsimps [image_Un];
   1.238 +Addsimps [image_Un RS sym];
   1.239 +
   1.240 +goal thy "insert (Key (newK x)) (sees A evs) = \
   1.241 +\         Key `` (newK``{x}) Un (sees A evs)";
   1.242 +by (Fast_tac 1);
   1.243 +val insert_Key_singleton = result();
   1.244 +
   1.245 +goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
   1.246 +\         Key `` (f `` (insert x E)) Un C";
   1.247 +by (Fast_tac 1);
   1.248 +val insert_Key_image = result();
   1.249 +
   1.250 +
   1.251 +(*This lets us avoid analyzing the new message -- unless we have to!*)
   1.252 +(*NEEDED??*)
   1.253 +goal thy "synth (analz (sees Enemy evs)) <=   \
   1.254 +\         synth (analz (sees Enemy (Says A B X # evs)))";
   1.255 +by (Simp_tac 1);
   1.256 +br (subset_insertI RS analz_mono RS synth_mono) 1;
   1.257 +qed "synth_analz_thin";
   1.258 +
   1.259 +AddIs [impOfSubs synth_analz_thin];
   1.260 +
   1.261 +
   1.262 +
   1.263 +(** Session keys are not used to encrypt other session keys **)
   1.264 +
   1.265 +(*Could generalize this so that the X component doesn't have to be first
   1.266 +  in the message?*)
   1.267 +val enemy_analz_tac =
   1.268 +  SELECT_GOAL 
   1.269 +   (EVERY [REPEAT (resolve_tac [impI,notI] 1),
   1.270 +	   dtac (impOfSubs Fake_analz_insert) 1,
   1.271 +	   eresolve_tac [asm_rl, synth.Inj] 1,
   1.272 +	   Fast_tac 1,
   1.273 +	   Asm_full_simp_tac 1,
   1.274 +	   IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
   1.275 +	   ]);
   1.276 +
   1.277 +
   1.278 +(*Lemma for the trivial direction of the if-and-only-if*)
   1.279 +goal thy  
   1.280 + "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
   1.281 +\         (K : nE | Key K : analz sEe)  ==>     \
   1.282 +\        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
   1.283 +by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
   1.284 +val lemma = result();
   1.285 +
   1.286 +
   1.287 +goal thy  
   1.288 + "!!evs. evs : yahalom ==> \
   1.289 +\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   1.290 +\           (K : newK``E | Key K : analz (sees Enemy evs))";
   1.291 +be yahalom.induct 1;
   1.292 +bd YM2_analz_sees_Enemy 4;
   1.293 +bd YM4_analz_sees_Enemy 6;
   1.294 +by (REPEAT_FIRST (resolve_tac [allI, lemma]));
   1.295 +by (ALLGOALS (*Takes 35 secs*)
   1.296 +    (asm_simp_tac 
   1.297 +     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.298 +			 @ pushes)
   1.299 +               setloop split_tac [expand_if])));
   1.300 +(*YM4*) 
   1.301 +by (enemy_analz_tac 5);
   1.302 +(*YM3*)
   1.303 +by (Fast_tac 4);
   1.304 +(*YM2*) (** LEVEL 7 **)
   1.305 +by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] 
   1.306 +    (insert_commute RS ssubst) 3);
   1.307 +by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   1.308 +    (insert_commute RS ssubst) 3);
   1.309 +by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3);
   1.310 +by (enemy_analz_tac 3);
   1.311 +(*Fake case*) (** LEVEL 11 **)
   1.312 +by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] 
   1.313 +    (insert_commute RS ssubst) 2);
   1.314 +by (enemy_analz_tac 2);
   1.315 +(*Base case*)
   1.316 +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   1.317 +qed_spec_mp "analz_image_newK";
   1.318 +
   1.319 +
   1.320 +goal thy
   1.321 + "!!evs. evs : yahalom ==>                               \
   1.322 +\        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
   1.323 +\        (K = newK evt | Key K : analz (sees Enemy evs))";
   1.324 +by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.325 +				   insert_Key_singleton]) 1);
   1.326 +by (Fast_tac 1);
   1.327 +qed "analz_insert_Key_newK";
   1.328 +
   1.329 +
   1.330 +(*Describes the form *and age* of K when the following message is sent*)
   1.331 +goal thy 
   1.332 + "!!evs. [| Says Server B \
   1.333 +\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.334 +\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   1.335 +\           evs : yahalom |]                                        \
   1.336 +\        ==> (EX evt:yahalom. K = Key(newK evt) & \
   1.337 +\                           length evt < length evs) &            \
   1.338 +\            (EX i. NA = Nonce i)";
   1.339 +be rev_mp 1;
   1.340 +be yahalom.induct 1;
   1.341 +by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   1.342 +qed "Says_Server_message_form";
   1.343 +
   1.344 +
   1.345 +(*Crucial secrecy property: Enemy does not see the keys sent in msg YM3*)
   1.346 +goal thy 
   1.347 + "!!evs. [| Says Server A \
   1.348 +\            {|NA, Crypt {|NA, K|} (shrK B),                      \
   1.349 +\                  Crypt {|NB, K|} (shrK A)|} : set_of_list evs;  \
   1.350 +\           A ~: bad;  B ~: bad;  evs : yahalom |] ==>              \
   1.351 +\     K ~: analz (sees Enemy evs)";
   1.352 +be rev_mp 1;
   1.353 +be yahalom.induct 1;
   1.354 +bd YM2_analz_sees_Enemy 4;
   1.355 +bd YM4_analz_sees_Enemy 6;
   1.356 +by (ALLGOALS Asm_simp_tac);
   1.357 +(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   1.358 +by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   1.359 +by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
   1.360 +by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac));
   1.361 +by (ALLGOALS
   1.362 +    (asm_full_simp_tac 
   1.363 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.364 +			  analz_insert_Key_newK] @ pushes)
   1.365 +               setloop split_tac [expand_if])));
   1.366 +(*YM3*)
   1.367 +by (fast_tac (!claset addSEs [less_irrefl]) 3);
   1.368 +(*Fake*) (** LEVEL 10 **)
   1.369 +by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1);
   1.370 +by (enemy_analz_tac 1);
   1.371 +(*YM4*)
   1.372 +by (mp_tac 2);
   1.373 +by (enemy_analz_tac 2);
   1.374 +(*YM2*)
   1.375 +by (mp_tac 1);
   1.376 +by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   1.377 +    (insert_commute RS ssubst) 1);
   1.378 +by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   1.379 +by (enemy_analz_tac 1);
   1.380 +qed "Enemy_not_see_encrypted_key";
   1.381 +
   1.382 +
   1.383 +
   1.384 +(*** Session keys are issued at most once, and identify the principals ***)
   1.385 +
   1.386 +(** First, two lemmas for the Fake, YM2 and YM4 cases **)
   1.387 +
   1.388 +goal thy 
   1.389 + "!!evs. [| X : synth (analz (sees Enemy evs));                \
   1.390 +\           Crypt X' (shrK C) : parts{X};                      \
   1.391 +\           C ~: bad;  evs : yahalom |]  \
   1.392 +\        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
   1.393 +by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   1.394 +	              addDs [impOfSubs parts_insert_subset_Un]
   1.395 +                      addss (!simpset)) 1);
   1.396 +qed "Crypt_Fake_parts";
   1.397 +
   1.398 +goal thy 
   1.399 + "!!evs. [| Crypt X' K : parts (sees A evs);  evs : yahalom |]  \
   1.400 +\        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
   1.401 +\            Crypt X' K : parts {Y}";
   1.402 +bd parts_singleton 1;
   1.403 +by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
   1.404 +qed "Crypt_parts_singleton";
   1.405 +
   1.406 +fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   1.407 +
   1.408 +(*The Key K uniquely identifies a pair of senders in the message encrypted by
   1.409 +  C, but if C=Enemy then he could send all sorts of nonsense.*)
   1.410 +goal thy 
   1.411 + "!!evs. evs : yahalom ==>                                     \
   1.412 +\      EX A B. ALL C.                                        \
   1.413 +\         C ~: bad -->                                       \
   1.414 +\         (ALL S S' X. Says S S' X : set_of_list evs -->     \
   1.415 +\           (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
   1.416 +by (Simp_tac 1);
   1.417 +be yahalom.induct 1;
   1.418 +bd YM2_analz_sees_Enemy 4;
   1.419 +bd YM4_analz_sees_Enemy 6;
   1.420 +by (ALLGOALS 
   1.421 +    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   1.422 +by (REPEAT_FIRST (etac exE));
   1.423 +(*YM4*)
   1.424 +by (ex_strip_tac 4);
   1.425 +by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   1.426 +			      Crypt_parts_singleton]) 4);
   1.427 +(*YM3: Case split propagates some context to other subgoal...*)
   1.428 +	(** LEVEL 8 **)
   1.429 +by (excluded_middle_tac "K = newK evsa" 3);
   1.430 +by (Asm_simp_tac 3);
   1.431 +by (REPEAT (ares_tac [exI] 3));
   1.432 +(*...we prove this case by contradiction: the key is too new!*)
   1.433 +by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
   1.434 +		      addSEs partsEs
   1.435 +		      addEs [Says_imp_old_keys RS less_irrefl]
   1.436 +	              addss (!simpset)) 3);
   1.437 +(*YM2*) (** LEVEL 12 **)
   1.438 +by (ex_strip_tac 2);
   1.439 +by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   1.440 +    (insert_commute RS ssubst) 2);
   1.441 +by (Simp_tac 2);
   1.442 +by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   1.443 +			      Crypt_parts_singleton]) 2);
   1.444 +(*Fake*) (** LEVEL 16 **)
   1.445 +by (ex_strip_tac 1);
   1.446 +by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
   1.447 +qed "unique_session_keys";
   1.448 +
   1.449 +(*It seems strange but this theorem is NOT needed to prove the main result!*)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Auth/Yahalom.thy	Thu Sep 12 10:40:05 1996 +0200
     2.3 @@ -0,0 +1,73 @@
     2.4 +(*  Title:      HOL/Auth/OtwayRees
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1996  University of Cambridge
     2.8 +
     2.9 +Inductive relation "yahalom" for the Yahalom protocol.
    2.10 +
    2.11 +From page 257 of
    2.12 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    2.13 +  Proc. Royal Soc. 426 (1989)
    2.14 +*)
    2.15 +
    2.16 +OtwayRees = Shared + 
    2.17 +
    2.18 +consts  yahalom   :: "event list set"
    2.19 +inductive yahalom
    2.20 +  intrs 
    2.21 +         (*Initial trace is empty*)
    2.22 +    Nil  "[]: yahalom"
    2.23 +
    2.24 +         (*The enemy MAY say anything he CAN say.  We do not expect him to
    2.25 +           invent new nonces here, but he can also use NS1.  Common to
    2.26 +           all similar protocols.*)
    2.27 +    Fake "[| evs: yahalom;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
    2.28 +          ==> Says Enemy B X  # evs : yahalom"
    2.29 +
    2.30 +         (*Alice initiates a protocol run*)
    2.31 +    YM1  "[| evs: yahalom;  A ~= B |]
    2.32 +          ==> Says A B {|Nonce (newN evs), Agent A |} # evs : yahalom"
    2.33 +
    2.34 +         (*Bob's response to Alice's message.  Bob doesn't know who 
    2.35 +	   the sender is, hence the A' in the sender field.
    2.36 +           We modify the published protocol by NOT encrypting NB.*)
    2.37 +    YM2  "[| evs: yahalom;  B ~= Server;
    2.38 +             Says A' B {|Nonce NA, Agent A|} : set_of_list evs |]
    2.39 +          ==> Says B Server 
    2.40 +                  {|Agent B, 
    2.41 +                    Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|}
    2.42 +                 # evs : yahalom"
    2.43 +
    2.44 +         (*The Server receives Bob's message.  He responds by sending a
    2.45 +            new session key to Alice, with a packet for forwarding to Bob.*)
    2.46 +    YM3  "[| evs: yahalom;  B ~= Server;
    2.47 +             Says B' Server 
    2.48 +                  {|Nonce NA, Agent A, Agent B, 
    2.49 +                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
    2.50 +                    Nonce NB, 
    2.51 +                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
    2.52 +               : set_of_list evs |]
    2.53 +          ==> Says Server B 
    2.54 +                  {|Nonce NA, 
    2.55 +                    Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
    2.56 +                    Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
    2.57 +                 # evs : yahalom"
    2.58 +
    2.59 +         (*Bob receives the Server's (?) message and compares the Nonces with
    2.60 +	   those in the message he previously sent the Server.*)
    2.61 +    YM4  "[| evs: yahalom;  A ~= B;  
    2.62 +             Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    2.63 +               : set_of_list evs;
    2.64 +             Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
    2.65 +               : set_of_list evs |]
    2.66 +          ==> (Says B A {|Nonce NA, X|}) # evs : yahalom"
    2.67 +
    2.68 +         (*Alice checks her Nonce, then sends a dummy message to Bob,
    2.69 +           using the new session key.*)
    2.70 +    YM5  "[| evs: yahalom;  
    2.71 +             Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    2.72 +               : set_of_list evs;
    2.73 +             Says A  B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    2.74 +          ==> Says A B (Crypt (Agent A) K)  # evs : yahalom"
    2.75 +
    2.76 +end
     3.1 --- a/src/HOL/IOA/NTP/Lemmas.ML	Thu Sep 12 10:36:51 1996 +0200
     3.2 +++ b/src/HOL/IOA/NTP/Lemmas.ML	Thu Sep 12 10:40:05 1996 +0200
     3.3 @@ -156,10 +156,7 @@
     3.4  
     3.5  goal Arith.thy "~0<n --> n = 0";
     3.6    by (nat_ind_tac "n" 1);
     3.7 -  by (Asm_simp_tac 1);
     3.8 -  by (safe_tac (!claset));
     3.9 -  by (Asm_full_simp_tac 1);
    3.10 -  by (Asm_full_simp_tac 1);
    3.11 +  by (Auto_tac ());
    3.12  qed "zero_eq";
    3.13  
    3.14  goal Arith.thy "x < Suc(y) --> x<=y";
     4.1 --- a/src/HOL/Lex/Auto.ML	Thu Sep 12 10:36:51 1996 +0200
     4.2 +++ b/src/HOL/Lex/Auto.ML	Thu Sep 12 10:40:05 1996 +0200
     4.3 @@ -29,7 +29,7 @@
     4.4    by (case_tac "zs=[]" 1);
     4.5     by(hyp_subst_tac 1);
     4.6     by(Asm_full_simp_tac 1);
     4.7 -  by(fast_tac (!claset addSEs [Cons_neq_Nil]) 1);
     4.8 +  by(Fast_tac 1);
     4.9   by(res_inst_tac [("x","[x]")] exI 1);
    4.10   by(asm_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
    4.11  by(res_inst_tac [("x","x#us")] exI 1);
     5.1 --- a/src/HOL/List.ML	Thu Sep 12 10:36:51 1996 +0200
     5.2 +++ b/src/HOL/List.ML	Thu Sep 12 10:40:05 1996 +0200
     5.3 @@ -8,10 +8,8 @@
     5.4  
     5.5  open List;
     5.6  
     5.7 -val [Nil_not_Cons,Cons_not_Nil] = list.distinct;
     5.8 -
     5.9 -bind_thm("Cons_neq_Nil", Cons_not_Nil RS notE);
    5.10 -bind_thm("Nil_neq_Cons", sym RS Cons_neq_Nil);
    5.11 +AddIffs list.distinct;
    5.12 +AddIffs list.inject;
    5.13  
    5.14  bind_thm("Cons_inject", (hd list.inject) RS iffD1 RS conjE);
    5.15  
     6.1 --- a/src/HOL/Nat.ML	Thu Sep 12 10:36:51 1996 +0200
     6.2 +++ b/src/HOL/Nat.ML	Thu Sep 12 10:40:05 1996 +0200
     6.3 @@ -95,9 +95,9 @@
     6.4  by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1));
     6.5  qed "Suc_not_Zero";
     6.6  
     6.7 -bind_thm ("Zero_not_Suc", (Suc_not_Zero RS not_sym));
     6.8 +bind_thm ("Zero_not_Suc", Suc_not_Zero RS not_sym);
     6.9  
    6.10 -Addsimps [Suc_not_Zero,Zero_not_Suc];
    6.11 +AddIffs [Suc_not_Zero,Zero_not_Suc];
    6.12  
    6.13  bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE));
    6.14  val Zero_neq_Suc = sym RS Suc_neq_Zero;
    6.15 @@ -118,9 +118,11 @@
    6.16  by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]); 
    6.17  qed "Suc_Suc_eq";
    6.18  
    6.19 +AddIffs [Suc_Suc_eq];
    6.20 +
    6.21  goal Nat.thy "n ~= Suc(n)";
    6.22  by (nat_ind_tac "n" 1);
    6.23 -by (ALLGOALS(asm_simp_tac (!simpset addsimps [Suc_Suc_eq])));
    6.24 +by (ALLGOALS Asm_simp_tac);
    6.25  qed "n_not_Suc_n";
    6.26  
    6.27  bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
    6.28 @@ -128,12 +130,11 @@
    6.29  (*** nat_case -- the selection operator for nat ***)
    6.30  
    6.31  goalw Nat.thy [nat_case_def] "nat_case a f 0 = a";
    6.32 -by (fast_tac (!claset addIs [select_equality] addEs [Zero_neq_Suc]) 1);
    6.33 +by (fast_tac (!claset addIs [select_equality]) 1);
    6.34  qed "nat_case_0";
    6.35  
    6.36  goalw Nat.thy [nat_case_def] "nat_case a f (Suc k) = f(k)";
    6.37 -by (fast_tac (!claset addIs [select_equality] 
    6.38 -                       addEs [make_elim Suc_inject, Suc_neq_Zero]) 1);
    6.39 +by (fast_tac (!claset addIs [select_equality]) 1);
    6.40  qed "nat_case_Suc";
    6.41  
    6.42  (** Introduction rules for 'pred_nat' **)
    6.43 @@ -152,9 +153,8 @@
    6.44  goalw Nat.thy [wf_def] "wf(pred_nat)";
    6.45  by (strip_tac 1);
    6.46  by (nat_ind_tac "x" 1);
    6.47 -by (fast_tac (!claset addSEs [mp, pred_natE, Pair_inject, 
    6.48 -                             make_elim Suc_inject]) 2);
    6.49 -by (fast_tac (!claset addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1);
    6.50 +by (fast_tac (!claset addSEs [mp, pred_natE]) 2);
    6.51 +by (fast_tac (!claset addSEs [mp, pred_natE]) 1);
    6.52  qed "wf_pred_nat";
    6.53  
    6.54  
    6.55 @@ -226,7 +226,7 @@
    6.56  by (etac less_trans 1);
    6.57  by (rtac lessI 1);
    6.58  qed "zero_less_Suc";
    6.59 -Addsimps [zero_less_Suc];
    6.60 +AddIffs [zero_less_Suc];
    6.61  
    6.62  (** Elimination properties **)
    6.63  
    6.64 @@ -265,19 +265,19 @@
    6.65  by (etac Zero_neq_Suc 1);
    6.66  by (etac Zero_neq_Suc 1);
    6.67  qed "not_less0";
    6.68 -Addsimps [not_less0];
    6.69 +
    6.70 +AddIffs [not_less0];
    6.71  
    6.72  (* n<0 ==> R *)
    6.73 -bind_thm ("less_zeroE", (not_less0 RS notE));
    6.74 -AddSEs [less_zeroE];
    6.75 +bind_thm ("less_zeroE", not_less0 RS notE);
    6.76  
    6.77  val [major,less,eq] = goal Nat.thy
    6.78      "[| m < Suc(n);  m<n ==> P;  m=n ==> P |] ==> P";
    6.79  by (rtac (major RS lessE) 1);
    6.80  by (rtac eq 1);
    6.81 -by (fast_tac (!claset addSDs [Suc_inject]) 1);
    6.82 +by (Fast_tac 1);
    6.83  by (rtac less 1);
    6.84 -by (fast_tac (!claset addSDs [Suc_inject]) 1);
    6.85 +by (Fast_tac 1);
    6.86  qed "less_SucE";
    6.87  
    6.88  goal Nat.thy "(m < Suc(n)) = (m < n | m = n)";
    6.89 @@ -305,11 +305,8 @@
    6.90  val [prem] = goal Nat.thy "Suc(m) < n ==> m<n";
    6.91  by (rtac (prem RS rev_mp) 1);
    6.92  by (nat_ind_tac "n" 1);
    6.93 -by (rtac impI 1);
    6.94 -by (etac less_zeroE 1);
    6.95 -by (fast_tac (!claset addSIs [lessI RS less_SucI]
    6.96 -                     addSDs [Suc_inject]
    6.97 -                     addEs  [less_trans, lessE]) 1);
    6.98 +by (ALLGOALS (fast_tac (!claset addSIs [lessI RS less_SucI]
    6.99 +                                addEs  [less_trans, lessE])));
   6.100  qed "Suc_lessD";
   6.101  
   6.102  val [major,minor] = goal Nat.thy 
   6.103 @@ -321,21 +318,15 @@
   6.104  by (assume_tac 1);
   6.105  qed "Suc_lessE";
   6.106  
   6.107 -val [major] = goal Nat.thy "Suc(m) < Suc(n) ==> m<n";
   6.108 -by (rtac (major RS lessE) 1);
   6.109 -by (REPEAT (rtac lessI 1
   6.110 -     ORELSE eresolve_tac [make_elim Suc_inject, ssubst, Suc_lessD] 1));
   6.111 +goal Nat.thy "!!m n. Suc(m) < Suc(n) ==> m<n";
   6.112 +by (fast_tac (!claset addEs [lessE, Suc_lessD] addIs [lessI]) 1);
   6.113  qed "Suc_less_SucD";
   6.114  
   6.115 -val prems = goal Nat.thy "m<n ==> Suc(m) < Suc(n)";
   6.116 -by (subgoal_tac "m<n --> Suc(m) < Suc(n)" 1);
   6.117 -by (fast_tac (!claset addIs prems) 1);
   6.118 +goal Nat.thy "!!m n. m<n ==> Suc(m) < Suc(n)";
   6.119 +by (etac rev_mp 1);
   6.120  by (nat_ind_tac "n" 1);
   6.121 -by (rtac impI 1);
   6.122 -by (etac less_zeroE 1);
   6.123 -by (fast_tac (!claset addSIs [lessI]
   6.124 -                     addSDs [Suc_inject]
   6.125 -                     addEs  [less_trans, lessE]) 1);
   6.126 +by (ALLGOALS (fast_tac (!claset addSIs [lessI]
   6.127 +                                addEs  [less_trans, lessE])));
   6.128  qed "Suc_mono";
   6.129  
   6.130  
   6.131 @@ -411,7 +402,7 @@
   6.132  
   6.133  Addsimps [less_not_refl,
   6.134            (*less_Suc_eq, makes simpset non-confluent*) le0, le_0_eq,
   6.135 -          Suc_Suc_eq, Suc_n_not_le_n,
   6.136 +          Suc_n_not_le_n,
   6.137            n_not_Suc_n, Suc_n_not_n,
   6.138            nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
   6.139  
     7.1 --- a/src/HOL/Relation.ML	Thu Sep 12 10:36:51 1996 +0200
     7.2 +++ b/src/HOL/Relation.ML	Thu Sep 12 10:40:05 1996 +0200
     7.3 @@ -1,21 +1,15 @@
     7.4  (*  Title:      Relation.ML
     7.5      ID:         $Id$
     7.6 -    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
     7.7 -                Lawrence C Paulson, Cambridge University Computer Laboratory
     7.8 -    Copyright   1994 Universita' di Firenze
     7.9 -    Copyright   1993  University of Cambridge
    7.10 +    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
    7.11 +    Copyright   1996  University of Cambridge
    7.12  *)
    7.13  
    7.14 -val RSLIST = curry (op MRS);
    7.15 -
    7.16  open Relation;
    7.17  
    7.18  (** Identity relation **)
    7.19  
    7.20  goalw Relation.thy [id_def] "(a,a) : id";  
    7.21 -by (rtac CollectI 1);
    7.22 -by (rtac exI 1);
    7.23 -by (rtac refl 1);
    7.24 +by (Fast_tac 1);
    7.25  qed "idI";
    7.26  
    7.27  val major::prems = goalw Relation.thy [id_def]
    7.28 @@ -34,9 +28,9 @@
    7.29  
    7.30  (** Composition of two relations **)
    7.31  
    7.32 -val prems = goalw Relation.thy [comp_def]
    7.33 -    "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
    7.34 -by (fast_tac (!claset addIs prems) 1);
    7.35 +goalw Relation.thy [comp_def]
    7.36 +    "!!r s. [| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
    7.37 +by (Fast_tac 1);
    7.38  qed "compI";
    7.39  
    7.40  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
    7.41 @@ -45,7 +39,8 @@
    7.42  \       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
    7.43  \    |] ==> P";
    7.44  by (cut_facts_tac prems 1);
    7.45 -by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 ORELSE ares_tac prems 1));
    7.46 +by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 
    7.47 +     ORELSE ares_tac prems 1));
    7.48  qed "compE";
    7.49  
    7.50  val prems = goal Relation.thy
    7.51 @@ -59,15 +54,12 @@
    7.52  AddIs [compI, idI];
    7.53  AddSEs [compE, idE];
    7.54  
    7.55 -val comp_cs = prod_cs addIs [compI, idI] addSEs [compE, idE];
    7.56 -
    7.57  goal Relation.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    7.58  by (Fast_tac 1);
    7.59  qed "comp_mono";
    7.60  
    7.61  goal Relation.thy
    7.62 -    "!!r s. [| s <= A Times B;  r <= B Times C |] ==> \
    7.63 -\           (r O s) <= A Times C";
    7.64 +    "!!r s. [| s <= A Times B;  r <= B Times C |] ==> (r O s) <= A Times C";
    7.65  by (Fast_tac 1);
    7.66  qed "comp_subset_Sigma";
    7.67  
    7.68 @@ -78,14 +70,19 @@
    7.69  by (REPEAT (ares_tac (prems@[allI,impI]) 1));
    7.70  qed "transI";
    7.71  
    7.72 -val major::prems = goalw Relation.thy [trans_def]
    7.73 -    "[| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
    7.74 -by (cut_facts_tac [major] 1);
    7.75 -by (fast_tac (!claset addIs prems) 1);
    7.76 +goalw Relation.thy [trans_def]
    7.77 +    "!!r. [| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
    7.78 +by (Fast_tac 1);
    7.79  qed "transD";
    7.80  
    7.81  (** Natural deduction for converse(r) **)
    7.82  
    7.83 +goalw Relation.thy [converse_def] "!!a b r. ((a,b):converse r) = ((b,a):r)";
    7.84 +by (Simp_tac 1);
    7.85 +qed "converse_iff";
    7.86 +
    7.87 +AddIffs [converse_iff];
    7.88 +
    7.89  goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)";
    7.90  by (Simp_tac 1);
    7.91  qed "converseI";
    7.92 @@ -94,6 +91,7 @@
    7.93  by (Fast_tac 1);
    7.94  qed "converseD";
    7.95  
    7.96 +(*More general than converseD, as it "splits" the member of the relation*)
    7.97  qed_goalw "converseE" Relation.thy [converse_def]
    7.98      "[| yx : converse(r);  \
    7.99  \       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
   7.100 @@ -103,11 +101,7 @@
   7.101      (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
   7.102      (assume_tac 1) ]);
   7.103  
   7.104 -AddSIs [converseI];
   7.105 -AddSEs [converseD,converseE];
   7.106 -
   7.107 -val converse_cs = comp_cs addSIs [converseI]
   7.108 -                          addSEs [converseD,converseE];
   7.109 +AddSEs [converseE];
   7.110  
   7.111  goalw Relation.thy [converse_def] "converse(converse R) = R";
   7.112  by(Fast_tac 1);
   7.113 @@ -128,6 +122,9 @@
   7.114    [ (rtac (Domain_iff RS iffD1 RS exE) 1),
   7.115      (REPEAT (ares_tac prems 1)) ]);
   7.116  
   7.117 +AddIs  [DomainI];
   7.118 +AddSEs [DomainE];
   7.119 +
   7.120  (** Range **)
   7.121  
   7.122  qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
   7.123 @@ -140,11 +137,14 @@
   7.124      (resolve_tac prems 1),
   7.125      (etac converseD 1) ]);
   7.126  
   7.127 +AddIs  [RangeI];
   7.128 +AddSEs [RangeE];
   7.129 +
   7.130  (*** Image of a set under a relation ***)
   7.131  
   7.132  qed_goalw "Image_iff" Relation.thy [Image_def]
   7.133      "b : r^^A = (? x:A. (x,b):r)"
   7.134 - (fn _ => [ fast_tac (!claset addIs [RangeI]) 1 ]);
   7.135 + (fn _ => [ Fast_tac 1 ]);
   7.136  
   7.137  qed_goal "Image_singleton_iff" Relation.thy
   7.138      "(b : r^^{a}) = ((a,b):r)"
   7.139 @@ -153,40 +153,31 @@
   7.140  
   7.141  qed_goalw "ImageI" Relation.thy [Image_def]
   7.142      "!!a b r. [| (a,b): r;  a:A |] ==> b : r^^A"
   7.143 - (fn _ => [ (REPEAT (ares_tac [CollectI,RangeI,bexI] 1)),
   7.144 -            (resolve_tac [conjI ] 1),
   7.145 -            (rtac RangeI 1),
   7.146 -            (REPEAT (Fast_tac 1))]);
   7.147 + (fn _ => [ (Fast_tac 1)]);
   7.148  
   7.149  qed_goalw "ImageE" Relation.thy [Image_def]
   7.150      "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
   7.151   (fn major::prems=>
   7.152    [ (rtac (major RS CollectE) 1),
   7.153 -    (safe_tac (!claset)),
   7.154 -    (etac RangeE 1),
   7.155 +    (Step_tac 1),
   7.156      (rtac (hd prems) 1),
   7.157      (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
   7.158  
   7.159 +AddIs  [ImageI];
   7.160 +AddSEs [ImageE];
   7.161 +
   7.162  qed_goal "Image_subset" Relation.thy
   7.163      "!!A B r. r <= A Times B ==> r^^C <= B"
   7.164   (fn _ =>
   7.165    [ (rtac subsetI 1),
   7.166      (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
   7.167  
   7.168 -AddSIs [converseI]; 
   7.169 -AddIs  [ImageI, DomainI, RangeI];
   7.170 -AddSEs [ImageE, DomainE, RangeE];
   7.171 -
   7.172 -val rel_cs = converse_cs addSIs [converseI] 
   7.173 -                         addIs  [ImageI, DomainI, RangeI]
   7.174 -                         addSEs [ImageE, DomainE, RangeE];
   7.175 -
   7.176  goal Relation.thy "R O id = R";
   7.177 -by(fast_tac (!claset addIs [set_ext] addbefore (split_all_tac 1)) 1);
   7.178 +by (fast_tac (!claset addbefore (split_all_tac 1)) 1);
   7.179  qed "R_O_id";
   7.180  
   7.181  goal Relation.thy "id O R = R";
   7.182 -by(fast_tac (!claset addIs [set_ext] addbefore (split_all_tac 1)) 1);
   7.183 +by (fast_tac (!claset addbefore (split_all_tac 1)) 1);
   7.184  qed "id_O_R";
   7.185  
   7.186  Addsimps [R_O_id,id_O_R];
     8.1 --- a/src/HOL/Set.ML	Thu Sep 12 10:36:51 1996 +0200
     8.2 +++ b/src/HOL/Set.ML	Thu Sep 12 10:40:05 1996 +0200
     8.3 @@ -3,7 +3,7 @@
     8.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.5      Copyright   1991  University of Cambridge
     8.6  
     8.7 -For set.thy.  Set theory for higher-order logic.  A set is simply a predicate.
     8.8 +Set theory for higher-order logic.  A set is simply a predicate.
     8.9  *)
    8.10  
    8.11  open Set;
     9.1 --- a/src/HOL/Sexp.ML	Thu Sep 12 10:36:51 1996 +0200
     9.2 +++ b/src/HOL/Sexp.ML	Thu Sep 12 10:40:05 1996 +0200
     9.3 @@ -10,17 +10,6 @@
     9.4  
     9.5  (** sexp_case **)
     9.6  
     9.7 -val sexp_free_cs = 
     9.8 -    set_cs addSDs [Leaf_inject, Numb_inject, Scons_inject] 
     9.9 -           addSEs [Leaf_neq_Scons, Leaf_neq_Numb,
    9.10 -                   Numb_neq_Scons, Numb_neq_Leaf,
    9.11 -                   Scons_neq_Leaf, Scons_neq_Numb];
    9.12 -
    9.13 -AddSDs [Leaf_inject, Numb_inject, Scons_inject];
    9.14 -AddSEs [Leaf_neq_Scons, Leaf_neq_Numb,
    9.15 -                   Numb_neq_Scons, Numb_neq_Leaf,
    9.16 -                   Scons_neq_Leaf, Scons_neq_Numb];
    9.17 -
    9.18  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
    9.19  by (resolve_tac [select_equality] 1);
    9.20  by (ALLGOALS (Fast_tac));
    9.21 @@ -60,8 +49,7 @@
    9.22  val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp";
    9.23  by (rtac (major RS setup_induction) 1);
    9.24  by (etac sexp.induct 1);
    9.25 -by (ALLGOALS 
    9.26 -    (fast_tac (!claset addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject])));
    9.27 +by (ALLGOALS Fast_tac);
    9.28  qed "Scons_D";
    9.29  
    9.30  (** Introduction rules for 'pred_sexp' **)
    9.31 @@ -109,9 +97,7 @@
    9.32  goal Sexp.thy "wf(pred_sexp)";
    9.33  by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
    9.34  by (etac sexp.induct 1);
    9.35 -by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Scons_inject]) 3);
    9.36 -by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Numb_neq_Scons]) 2);
    9.37 -by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Leaf_neq_Scons]) 1);
    9.38 +by (ALLGOALS (fast_tac (!claset addSEs [mp, pred_sexpE])));
    9.39  qed "wf_pred_sexp";
    9.40  
    9.41  (*** sexp_rec -- by wf recursion on pred_sexp ***)
    10.1 --- a/src/HOL/Sum.ML	Thu Sep 12 10:36:51 1996 +0200
    10.2 +++ b/src/HOL/Sum.ML	Thu Sep 12 10:40:05 1996 +0200
    10.3 @@ -40,16 +40,13 @@
    10.4  by (rtac Inr_RepI 1);
    10.5  qed "Inl_not_Inr";
    10.6  
    10.7 -bind_thm ("Inl_neq_Inr", (Inl_not_Inr RS notE));
    10.8 -val Inr_neq_Inl = sym RS Inl_neq_Inr;
    10.9 +bind_thm ("Inr_not_Inl", Inl_not_Inr RS not_sym);
   10.10 +
   10.11 +AddIffs [Inl_not_Inr, Inr_not_Inl];
   10.12  
   10.13 -goal Sum.thy "(Inl(a)=Inr(b)) = False";
   10.14 -by (simp_tac (!simpset addsimps [Inl_not_Inr]) 1);
   10.15 -qed "Inl_Inr_eq";
   10.16 +bind_thm ("Inl_neq_Inr", Inl_not_Inr RS notE);
   10.17  
   10.18 -goal Sum.thy "(Inr(b)=Inl(a))  =  False";
   10.19 -by (simp_tac (!simpset addsimps [Inl_not_Inr RS not_sym]) 1);
   10.20 -qed "Inr_Inl_eq";
   10.21 +val Inr_neq_Inl = sym RS Inl_neq_Inr;
   10.22  
   10.23  
   10.24  (** Injectiveness of Inl and Inr **)
   10.25 @@ -88,16 +85,18 @@
   10.26  by (fast_tac (!claset addSEs [Inr_inject]) 1);
   10.27  qed "Inr_eq";
   10.28  
   10.29 +AddIffs [Inl_eq, Inr_eq];
   10.30 +
   10.31  (*** Rules for the disjoint sum of two SETS ***)
   10.32  
   10.33  (** Introduction rules for the injections **)
   10.34  
   10.35  goalw Sum.thy [sum_def] "!!a A B. a : A ==> Inl(a) : A plus B";
   10.36 -by (REPEAT (ares_tac [UnI1,imageI] 1));
   10.37 +by (Fast_tac 1);
   10.38  qed "InlI";
   10.39  
   10.40  goalw Sum.thy [sum_def] "!!b A B. b : B ==> Inr(b) : A plus B";
   10.41 -by (REPEAT (ares_tac [UnI2,imageI] 1));
   10.42 +by (Fast_tac 1);
   10.43  qed "InrI";
   10.44  
   10.45  (** Elimination rules **)
   10.46 @@ -113,13 +112,8 @@
   10.47  qed "plusE";
   10.48  
   10.49  
   10.50 -val sum_cs = set_cs addSIs [InlI, InrI] 
   10.51 -                    addSEs [plusE, Inl_neq_Inr, Inr_neq_Inl]
   10.52 -                    addSDs [Inl_inject, Inr_inject];
   10.53 -
   10.54  AddSIs [InlI, InrI]; 
   10.55 -AddSEs [plusE, Inl_neq_Inr, Inr_neq_Inl];
   10.56 -AddSDs [Inl_inject, Inr_inject];
   10.57 +AddSEs [plusE];
   10.58  
   10.59  
   10.60  (** sum_case -- the selection operator for sums **)
   10.61 @@ -132,6 +126,8 @@
   10.62  by (fast_tac (!claset addIs [select_equality]) 1);
   10.63  qed "sum_case_Inr";
   10.64  
   10.65 +Addsimps [sum_case_Inl, sum_case_Inr];
   10.66 +
   10.67  (** Exhaustion rule for sums -- a degenerate form of induction **)
   10.68  
   10.69  val prems = goalw Sum.thy [Inl_def,Inr_def]
   10.70 @@ -152,17 +148,10 @@
   10.71  
   10.72  goal Sum.thy "R(sum_case f g s) = \
   10.73  \             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
   10.74 -by (rtac sumE 1);
   10.75 -by (etac ssubst 1);
   10.76 -by (stac sum_case_Inl 1);
   10.77 -by (fast_tac (!claset addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
   10.78 -by (etac ssubst 1);
   10.79 -by (stac sum_case_Inr 1);
   10.80 -by (fast_tac (!claset addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
   10.81 +by (res_inst_tac [("s","s")] sumE 1);
   10.82 +by (Auto_tac());
   10.83  qed "expand_sum_case";
   10.84  
   10.85 -Addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq,  sum_case_Inl, sum_case_Inr];
   10.86 -
   10.87  (*Prevents simplification of f and g: much faster*)
   10.88  qed_goal "sum_case_weak_cong" Sum.thy
   10.89    "s=t ==> sum_case f g s = sum_case f g t"
   10.90 @@ -170,7 +159,6 @@
   10.91  
   10.92  
   10.93  
   10.94 -
   10.95  (** Rules for the Part primitive **)
   10.96  
   10.97  goalw Sum.thy [Part_def]
    11.1 --- a/src/HOL/Trancl.ML	Thu Sep 12 10:36:51 1996 +0200
    11.2 +++ b/src/HOL/Trancl.ML	Thu Sep 12 10:40:05 1996 +0200
    11.3 @@ -276,6 +276,3 @@
    11.4  by (fast_tac (!claset addSDs [lemma]) 1);
    11.5  qed "trancl_subset_Sigma";
    11.6  
    11.7 -(* Don't add r_into_rtrancl: it messes up the proofs in Lambda *)
    11.8 -val trancl_cs = rel_cs addIs [rtrancl_refl];
    11.9 -
    12.1 --- a/src/HOL/Univ.ML	Thu Sep 12 10:36:51 1996 +0200
    12.2 +++ b/src/HOL/Univ.ML	Thu Sep 12 10:40:05 1996 +0200
    12.3 @@ -27,13 +27,13 @@
    12.4  
    12.5  (** Push -- an injection, analogous to Cons on lists **)
    12.6  
    12.7 -val [major] = goalw Univ.thy [Push_def] "Push i f =Push j g  ==> i=j";
    12.8 +val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g  ==> i=j";
    12.9  by (rtac (major RS fun_cong RS box_equals RS Suc_inject) 1);
   12.10  by (rtac nat_case_0 1);
   12.11  by (rtac nat_case_0 1);
   12.12  qed "Push_inject1";
   12.13  
   12.14 -val [major] = goalw Univ.thy [Push_def] "Push i f =Push j g  ==> f=g";
   12.15 +val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g  ==> f=g";
   12.16  by (rtac (major RS fun_cong RS ext RS box_equals) 1);
   12.17  by (rtac (nat_case_Suc RS ext) 1);
   12.18  by (rtac (nat_case_Suc RS ext) 1);
   12.19 @@ -90,10 +90,8 @@
   12.20                            Pair_inject, sym RS Push_neq_K0] 1
   12.21       ORELSE resolve_tac [Node_K0_I, Rep_Node RS Node_Push_I] 1));
   12.22  qed "Scons_not_Atom";
   12.23 -bind_thm ("Atom_not_Scons", (Scons_not_Atom RS not_sym));
   12.24 +bind_thm ("Atom_not_Scons", Scons_not_Atom RS not_sym);
   12.25  
   12.26 -bind_thm ("Scons_neq_Atom", (Scons_not_Atom RS notE));
   12.27 -val Atom_neq_Scons = sym RS Scons_neq_Atom;
   12.28  
   12.29  (*** Injectiveness ***)
   12.30  
   12.31 @@ -104,12 +102,18 @@
   12.32  qed "inj_Atom";
   12.33  val Atom_inject = inj_Atom RS injD;
   12.34  
   12.35 +goal Univ.thy "(Atom(a)=Atom(b)) = (a=b)";
   12.36 +by (fast_tac (!claset addSEs [Atom_inject]) 1);
   12.37 +qed "Atom_Atom_eq";
   12.38 +AddIffs [Atom_Atom_eq];
   12.39 +
   12.40  goalw Univ.thy [Leaf_def,o_def] "inj(Leaf)";
   12.41  by (rtac injI 1);
   12.42  by (etac (Atom_inject RS Inl_inject) 1);
   12.43  qed "inj_Leaf";
   12.44  
   12.45  val Leaf_inject = inj_Leaf RS injD;
   12.46 +AddSDs [Leaf_inject];
   12.47  
   12.48  goalw Univ.thy [Numb_def,o_def] "inj(Numb)";
   12.49  by (rtac injI 1);
   12.50 @@ -117,6 +121,7 @@
   12.51  qed "inj_Numb";
   12.52  
   12.53  val Numb_inject = inj_Numb RS injD;
   12.54 +AddSDs [Numb_inject];
   12.55  
   12.56  (** Injectiveness of Push_Node **)
   12.57  
   12.58 @@ -131,7 +136,7 @@
   12.59  by (etac (Push_inject1 RS sym) 1);
   12.60  by (rtac (inj_Rep_Node RS injD) 1);
   12.61  by (etac trans 1);
   12.62 -by (safe_tac (!claset addSEs [Pair_inject,Push_inject,sym]));
   12.63 +by (safe_tac (!claset addSEs [Push_inject,sym]));
   12.64  qed "Push_Node_inject";
   12.65  
   12.66  
   12.67 @@ -139,14 +144,12 @@
   12.68  
   12.69  val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> M<=M'";
   12.70  by (cut_facts_tac [major] 1);
   12.71 -by (fast_tac (!claset addSDs [Suc_inject]
   12.72 -                     addSEs [Push_Node_inject, Zero_neq_Suc]) 1);
   12.73 +by (fast_tac (!claset addSEs [Push_Node_inject]) 1);
   12.74  qed "Scons_inject_lemma1";
   12.75  
   12.76  val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> N<=N'";
   12.77  by (cut_facts_tac [major] 1);
   12.78 -by (fast_tac (!claset addSDs [Suc_inject]
   12.79 -                     addSEs [Push_Node_inject, Suc_neq_Zero]) 1);
   12.80 +by (fast_tac (!claset addSEs [Push_Node_inject]) 1);
   12.81  qed "Scons_inject_lemma2";
   12.82  
   12.83  val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
   12.84 @@ -165,10 +168,7 @@
   12.85  by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
   12.86  qed "Scons_inject";
   12.87  
   12.88 -(*rewrite rules*)
   12.89 -goal Univ.thy "(Atom(a)=Atom(b)) = (a=b)";
   12.90 -by (fast_tac (!claset addSEs [Atom_inject]) 1);
   12.91 -qed "Atom_Atom_eq";
   12.92 +AddSDs [Scons_inject];
   12.93  
   12.94  goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')";
   12.95  by (fast_tac (!claset addSEs [Scons_inject]) 1);
   12.96 @@ -181,35 +181,35 @@
   12.97  goalw Univ.thy [Leaf_def,o_def] "(M$N) ~= Leaf(a)";
   12.98  by (rtac Scons_not_Atom 1);
   12.99  qed "Scons_not_Leaf";
  12.100 -bind_thm ("Leaf_not_Scons", (Scons_not_Leaf RS not_sym));
  12.101 +bind_thm ("Leaf_not_Scons", Scons_not_Leaf RS not_sym);
  12.102  
  12.103 -bind_thm ("Scons_neq_Leaf", (Scons_not_Leaf RS notE));
  12.104 -val Leaf_neq_Scons = sym RS Scons_neq_Leaf;
  12.105 +AddIffs [Scons_not_Leaf, Leaf_not_Scons];
  12.106 +
  12.107  
  12.108  (** Scons vs Numb **)
  12.109  
  12.110  goalw Univ.thy [Numb_def,o_def] "(M$N) ~= Numb(k)";
  12.111  by (rtac Scons_not_Atom 1);
  12.112  qed "Scons_not_Numb";
  12.113 -bind_thm ("Numb_not_Scons", (Scons_not_Numb RS not_sym));
  12.114 +bind_thm ("Numb_not_Scons", Scons_not_Numb RS not_sym);
  12.115  
  12.116 -bind_thm ("Scons_neq_Numb", (Scons_not_Numb RS notE));
  12.117 -val Numb_neq_Scons = sym RS Scons_neq_Numb;
  12.118 +AddIffs [Scons_not_Numb, Numb_not_Scons];
  12.119 +
  12.120  
  12.121  (** Leaf vs Numb **)
  12.122  
  12.123  goalw Univ.thy [Leaf_def,Numb_def] "Leaf(a) ~= Numb(k)";
  12.124 -by (simp_tac (!simpset addsimps [Atom_Atom_eq,Inl_not_Inr]) 1);
  12.125 +by (simp_tac (!simpset addsimps [Inl_not_Inr]) 1);
  12.126  qed "Leaf_not_Numb";
  12.127 -bind_thm ("Numb_not_Leaf", (Leaf_not_Numb RS not_sym));
  12.128 +bind_thm ("Numb_not_Leaf", Leaf_not_Numb RS not_sym);
  12.129  
  12.130 -bind_thm ("Leaf_neq_Numb", (Leaf_not_Numb RS notE));
  12.131 -val Numb_neq_Leaf = sym RS Leaf_neq_Numb;
  12.132 +AddIffs [Leaf_not_Numb, Numb_not_Leaf];
  12.133  
  12.134  
  12.135  (*** ndepth -- the depth of a node ***)
  12.136  
  12.137 -Addsimps [apfst_conv,Scons_not_Atom,Atom_not_Scons,Scons_Scons_eq];
  12.138 +Addsimps [apfst_conv];
  12.139 +AddIffs  [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq];
  12.140  
  12.141  
  12.142  goalw Univ.thy [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0";
  12.143 @@ -244,13 +244,11 @@
  12.144  (*** ntrunc applied to the various node sets ***)
  12.145  
  12.146  goalw Univ.thy [ntrunc_def] "ntrunc 0 M = {}";
  12.147 -by (safe_tac (!claset addSIs [equalityI] addSEs [less_zeroE]));
  12.148 +by (Fast_tac 1);
  12.149  qed "ntrunc_0";
  12.150  
  12.151  goalw Univ.thy [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)";
  12.152 -by (safe_tac (!claset addSIs [equalityI]));
  12.153 -by (stac ndepth_K0 1);
  12.154 -by (rtac zero_less_Suc 1);
  12.155 +by (fast_tac (!claset addss (!simpset addsimps [ndepth_K0])) 1);
  12.156  qed "ntrunc_Atom";
  12.157  
  12.158  goalw Univ.thy [Leaf_def,o_def] "ntrunc (Suc k) (Leaf a) = Leaf(a)";
  12.159 @@ -275,7 +273,7 @@
  12.160  goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
  12.161  by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
  12.162  by (rewtac Scons_def);
  12.163 -by (safe_tac (!claset addSIs [equalityI]));
  12.164 +by (Fast_tac 1);
  12.165  qed "ntrunc_one_In0";
  12.166  
  12.167  goalw Univ.thy [In0_def]
  12.168 @@ -286,7 +284,7 @@
  12.169  goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
  12.170  by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
  12.171  by (rewtac Scons_def);
  12.172 -by (safe_tac (!claset addSIs [equalityI]));
  12.173 +by (Fast_tac 1);
  12.174  qed "ntrunc_one_In1";
  12.175  
  12.176  goalw Univ.thy [In1_def]
  12.177 @@ -348,9 +346,9 @@
  12.178  by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1);
  12.179  qed "In0_not_In1";
  12.180  
  12.181 -bind_thm ("In1_not_In0", (In0_not_In1 RS not_sym));
  12.182 -bind_thm ("In0_neq_In1", (In0_not_In1 RS notE));
  12.183 -val In1_neq_In0 = sym RS In0_neq_In1;
  12.184 +bind_thm ("In1_not_In0", In0_not_In1 RS not_sym);
  12.185 +
  12.186 +AddIffs [In0_not_In1, In1_not_In0];
  12.187  
  12.188  val [major] = goalw Univ.thy [In0_def] "In0(M) = In0(N) ==>  M=N";
  12.189  by (rtac (major RS Scons_inject2) 1);
  12.190 @@ -360,6 +358,7 @@
  12.191  by (rtac (major RS Scons_inject2) 1);
  12.192  qed "In1_inject";
  12.193  
  12.194 +AddSDs [In0_inject, In1_inject];
  12.195  
  12.196  (*** proving equality of sets and functions using ntrunc ***)
  12.197  
  12.198 @@ -414,17 +413,15 @@
  12.199  (*** Split and Case ***)
  12.200  
  12.201  goalw Univ.thy [Split_def] "Split c (M$N) = c M N";
  12.202 -by (fast_tac (!claset addIs [select_equality] addEs [Scons_inject]) 1);
  12.203 +by (fast_tac (!claset addIs [select_equality]) 1);
  12.204  qed "Split";
  12.205  
  12.206  goalw Univ.thy [Case_def] "Case c d (In0 M) = c(M)";
  12.207 -by (fast_tac (!claset addIs [select_equality] 
  12.208 -                     addEs [make_elim In0_inject, In0_neq_In1]) 1);
  12.209 +by (fast_tac (!claset addIs [select_equality]) 1);
  12.210  qed "Case_In0";
  12.211  
  12.212  goalw Univ.thy [Case_def] "Case c d (In1 N) = d(N)";
  12.213 -by (fast_tac (!claset addIs [select_equality] 
  12.214 -                     addEs [make_elim In1_inject, In1_neq_In0]) 1);
  12.215 +by (fast_tac (!claset addIs [select_equality]) 1);
  12.216  qed "Case_In1";
  12.217  
  12.218  (**** UN x. B(x) rules ****)
  12.219 @@ -506,11 +503,6 @@
  12.220  qed "dsumE";
  12.221  
  12.222  
  12.223 -val univ_cs =
  12.224 -    prod_cs addSIs [diagI, uprodI, dprodI]
  12.225 -            addIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I]
  12.226 -            addSEs [diagE, uprodE, dprodE, usumE, dsumE];
  12.227 -
  12.228  AddSIs [diagI, uprodI, dprodI];
  12.229  AddIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I];
  12.230  AddSEs [diagE, uprodE, dprodE, usumE, dsumE];
  12.231 @@ -556,18 +548,15 @@
  12.232  (*** Domain ***)
  12.233  
  12.234  goal Univ.thy "fst `` diag(A) = A";
  12.235 -by (fast_tac (!claset addIs [diagI] addSEs [diagE]) 1);
  12.236 +by (Fast_tac 1);
  12.237  qed "fst_image_diag";
  12.238  
  12.239  goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
  12.240 -by (fast_tac (!claset addIs [uprodI, dprodI]
  12.241 -                     addSEs [uprodE, dprodE]) 1);
  12.242 +by (Fast_tac 1);
  12.243  qed "fst_image_dprod";
  12.244  
  12.245  goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
  12.246 -by (fast_tac (!claset addIs [usum_In0I, usum_In1I, 
  12.247 -                             dsum_In0I, dsum_In1I]
  12.248 -                     addSEs [usumE, dsumE]) 1);
  12.249 +by (Fast_tac 1);
  12.250  qed "fst_image_dsum";
  12.251  
  12.252  Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum];
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/cladata.ML	Thu Sep 12 10:40:05 1996 +0200
    13.3 @@ -0,0 +1,63 @@
    13.4 +(*  Title:      HOL/cladata.ML
    13.5 +    ID:         $Id$
    13.6 +    Author:     Tobias Nipkow
    13.7 +    Copyright   1996  University of Cambridge
    13.8 +
    13.9 +Setting up the classical reasoner 
   13.10 +*)
   13.11 +
   13.12 +
   13.13 +(** Applying HypsubstFun to generate hyp_subst_tac **)
   13.14 +section "Classical Reasoner";
   13.15 +
   13.16 +structure Hypsubst_Data =
   13.17 +  struct
   13.18 +  structure Simplifier = Simplifier
   13.19 +  (*Take apart an equality judgement; otherwise raise Match!*)
   13.20 +  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
   13.21 +  val eq_reflection = eq_reflection
   13.22 +  val imp_intr = impI
   13.23 +  val rev_mp = rev_mp
   13.24 +  val subst = subst
   13.25 +  val sym = sym
   13.26 +  end;
   13.27 +
   13.28 +structure Hypsubst = HypsubstFun(Hypsubst_Data);
   13.29 +open Hypsubst;
   13.30 +
   13.31 +(*** Applying ClassicalFun to create a classical prover ***)
   13.32 +structure Classical_Data = 
   13.33 +  struct
   13.34 +  val sizef     = size_of_thm
   13.35 +  val mp        = mp
   13.36 +  val not_elim  = notE
   13.37 +  val classical = classical
   13.38 +  val hyp_subst_tacs=[hyp_subst_tac]
   13.39 +  end;
   13.40 +
   13.41 +structure Classical = ClassicalFun(Classical_Data);
   13.42 +open Classical;
   13.43 +
   13.44 +(*Propositional rules*)
   13.45 +val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
   13.46 +                       addSEs [conjE,disjE,impCE,FalseE,iffE];
   13.47 +
   13.48 +(*Quantifier rules*)
   13.49 +val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
   13.50 +                     addSEs [exE,ex1E] addEs [allE];
   13.51 +
   13.52 +exception CS_DATA of claset;
   13.53 +
   13.54 +let fun merge [] = CS_DATA empty_cs
   13.55 +      | merge cs = let val cs = map (fn CS_DATA x => x) cs;
   13.56 +                   in CS_DATA (foldl merge_cs (hd cs, tl cs)) end;
   13.57 +
   13.58 +    fun put (CS_DATA cs) = claset := cs;
   13.59 +
   13.60 +    fun get () = CS_DATA (!claset);
   13.61 +in add_thydata "HOL"
   13.62 +     ("claset", ThyMethods {merge = merge, put = put, get = get})
   13.63 +end;
   13.64 +
   13.65 +claset := HOL_cs;
   13.66 +
    14.1 --- a/src/HOL/ex/LList.ML	Thu Sep 12 10:36:51 1996 +0200
    14.2 +++ b/src/HOL/ex/LList.ML	Thu Sep 12 10:40:05 1996 +0200
    14.3 @@ -362,10 +362,10 @@
    14.4  by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1));
    14.5  qed "LCons_not_LNil";
    14.6  
    14.7 -bind_thm ("LNil_not_LCons", (LCons_not_LNil RS not_sym));
    14.8 +bind_thm ("LNil_not_LCons", LCons_not_LNil RS not_sym);
    14.9  
   14.10 -bind_thm ("LCons_neq_LNil", (LCons_not_LNil RS notE));
   14.11 -val LNil_neq_LCons = sym RS LCons_neq_LNil;
   14.12 +AddIffs [LCons_not_LNil, LNil_not_LCons];
   14.13 +
   14.14  
   14.15  (** llist constructors **)
   14.16  
   14.17 @@ -392,14 +392,14 @@
   14.18  (*For reasoning about abstract llist constructors*)
   14.19  
   14.20  AddIs ([Rep_llist]@llist.intrs);
   14.21 -AddSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject];
   14.22  AddSDs [inj_onto_Abs_llist RS inj_ontoD,
   14.23 -                              inj_Rep_llist RS injD, Leaf_inject];
   14.24 +	inj_Rep_llist RS injD, Leaf_inject];
   14.25  
   14.26  goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
   14.27  by (Fast_tac 1);
   14.28  qed "LCons_LCons_eq";
   14.29 -bind_thm ("LCons_inject", (LCons_LCons_eq RS iffD1 RS conjE));
   14.30 +
   14.31 +AddIffs [LCons_LCons_eq];
   14.32  
   14.33  val [major] = goal LList.thy "CONS M N: llist(A) ==> M: A & N: llist(A)";
   14.34  by (rtac (major RS llist.elim) 1);
    15.1 --- a/src/HOL/ex/SList.ML	Thu Sep 12 10:36:51 1996 +0200
    15.2 +++ b/src/HOL/ex/SList.ML	Thu Sep 12 10:40:05 1996 +0200
    15.3 @@ -74,10 +74,7 @@
    15.4  by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1));
    15.5  qed "Cons_not_Nil";
    15.6  
    15.7 -bind_thm ("Nil_not_Cons", (Cons_not_Nil RS not_sym));
    15.8 -
    15.9 -bind_thm ("Cons_neq_Nil2", (Cons_not_Nil RS notE));
   15.10 -val Nil_neq_Cons = sym RS Cons_neq_Nil2;
   15.11 +bind_thm ("Nil_not_Cons", Cons_not_Nil RS not_sym);
   15.12  
   15.13  (** Injectiveness of CONS and Cons **)
   15.14  
   15.15 @@ -85,11 +82,11 @@
   15.16  by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
   15.17  qed "CONS_CONS_eq";
   15.18  
   15.19 -bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
   15.20 -
   15.21  (*For reasoning about abstract list constructors*)
   15.22  AddIs ([Rep_list] @ list.intrs);
   15.23 -AddSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject];
   15.24 +
   15.25 +AddIffs [CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq];
   15.26 +
   15.27  AddSDs [inj_onto_Abs_list RS inj_ontoD,
   15.28          inj_Rep_list RS injD, Leaf_inject];
   15.29  
   15.30 @@ -111,9 +108,10 @@
   15.31  qed "sexp_CONS_D";
   15.32  
   15.33  
   15.34 -(*Basic ss with constructors and their freeness*)
   15.35 -Addsimps ([Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq, CONS_not_NIL,
   15.36 -           NIL_not_CONS, CONS_CONS_eq] @ list.intrs);
   15.37 +(*Reasoning about constructors and their freeness*)
   15.38 +Addsimps list.intrs;
   15.39 +
   15.40 +AddIffs [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq];
   15.41  
   15.42  goal SList.thy "!!N. N: list(A) ==> !M. N ~= CONS M N";
   15.43  by (etac list.induct 1);
    16.1 --- a/src/HOL/ex/Simult.ML	Thu Sep 12 10:36:51 1996 +0200
    16.2 +++ b/src/HOL/ex/Simult.ML	Thu Sep 12 10:40:05 1996 +0200
    16.3 @@ -64,7 +64,7 @@
    16.4  
    16.5  AddSIs [PartI];
    16.6  AddSDs [In0_inject, In1_inject];
    16.7 -AddSEs [In0_neq_In1, In1_neq_In0, PartE];
    16.8 +AddSEs [PartE];
    16.9  
   16.10  (*Could prove  ~ TCONS M N : Part (TF A) In1  etc. *)
   16.11  
    17.1 --- a/src/HOL/indrule.ML	Thu Sep 12 10:36:51 1996 +0200
    17.2 +++ b/src/HOL/indrule.ML	Thu Sep 12 10:40:05 1996 +0200
    17.3 @@ -165,7 +165,7 @@
    17.4  
    17.5  (*Simplification largely reduces the mutual induction rule to the 
    17.6    standard rule*)
    17.7 -val mut_ss = min_ss addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq, split];
    17.8 +val mut_ss = min_ss addsimps [Inl_not_Inr, Inr_not_Inl, Inl_eq, Inr_eq, split];
    17.9  
   17.10  val all_defs = [split RS eq_reflection] @ Inductive.con_defs @ part_rec_defs;
   17.11