# HG changeset patch
# User paulson
# Date 842517605 -7200
# Node ID 84cf16192e03732c291d8e78f14bc52ce003d634
# Parent  5cf82dc3ce672bc100ccf84bd6dffddb1ead09d4
Tidied many proofs, using AddIffs to let equivalences take
the place of separate Intr and Elim rules.  Also deleted most named clasets.

diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/Auth/Yahalom.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Yahalom.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -0,0 +1,446 @@
+(*  Title:      HOL/Auth/OtwayRees
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+Inductive relation "otway" for the Yahalom protocol.
+
+From page 257 of
+  Burrows, Abadi and Needham.  A Logic of Authentication.
+  Proc. Royal Soc. 426 (1989)
+*)
+
+open OtwayRees;
+
+proof_timing:=true;
+HOL_quantifiers := false;
+
+(**** Inductive proofs about yahalom ****)
+
+(*The Enemy can see more than anybody else, except for their initial state*)
+goal thy 
+ "!!evs. evs : yahalom ==> \
+\     sees A evs <= initState A Un sees Enemy evs";
+be yahalom.induct 1;
+by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
+			        addss (!simpset))));
+qed "sees_agent_subset_sees_Enemy";
+
+
+(*Nobody sends themselves messages*)
+goal thy "!!evs. evs : yahalom ==> ALL A X. Says A A X ~: set_of_list evs";
+be yahalom.induct 1;
+by (Auto_tac());
+qed_spec_mp "not_Says_to_self";
+Addsimps [not_Says_to_self];
+AddSEs   [not_Says_to_self RSN (2, rev_notE)];
+
+goal thy "!!evs. evs : yahalom ==> Notes A X ~: set_of_list evs";
+be yahalom.induct 1;
+by (Auto_tac());
+qed "not_Notes";
+Addsimps [not_Notes];
+AddSEs   [not_Notes RSN (2, rev_notE)];
+
+
+(** For reasoning about the encrypted portion of messages **)
+
+goal thy "!!evs. (Says A' B {|N, Agent A, Agent B, X|}) : set_of_list evs ==> \
+\                X : analz (sees Enemy evs)";
+by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
+qed "YM2_analz_sees_Enemy";
+
+goal thy "!!evs. (Says S B {|N, X, X'|}) : set_of_list evs ==> \
+\                X : analz (sees Enemy evs)";
+by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
+qed "YM4_analz_sees_Enemy";
+
+goal thy "!!evs. (Says B' A {|N, Crypt {|N,K|} K'|}) : set_of_list evs ==> \
+\                K : parts (sees Enemy evs)";
+by (fast_tac (!claset addSEs partsEs
+	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
+qed "YM5_parts_sees_Enemy";
+
+(*YM2_analz... and YM4_analz... let us treat those cases using the same 
+  argument as for the Fake case.  This is possible for most, but not all,
+  proofs: Fake does not invent new nonces (as in YM2), and of course Fake
+  messages originate from the Enemy. *)
+
+val YM2_YM4_tac = 
+    dtac (YM2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
+    dtac (YM4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6;
+
+
+(*** Shared keys are not betrayed ***)
+
+(*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
+goal thy 
+ "!!evs. [| evs : yahalom;  A ~: bad |] ==> \
+\        Key (shrK A) ~: parts (sees Enemy evs)";
+be yahalom.induct 1;
+by YM2_YM4_tac;
+by (Auto_tac());
+(*Deals with Fake message*)
+by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+			     impOfSubs Fake_parts_insert]) 1);
+qed "Enemy_not_see_shrK";
+
+bind_thm ("Enemy_not_analz_shrK",
+	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
+
+Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK];
+
+(*We go to some trouble to preserve R in the 3rd and 4th subgoals
+  As usual fast_tac cannot be used because it uses the equalities too soon*)
+val major::prems = 
+goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
+\             evs : yahalom;                                 \
+\             A:bad ==> R                                  \
+\           |] ==> R";
+br ccontr 1;
+br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
+by (swap_res_tac prems 2);
+by (ALLGOALS (fast_tac (!claset addIs prems)));
+qed "Enemy_see_shrK_E";
+
+bind_thm ("Enemy_analz_shrK_E", 
+	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
+
+AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
+
+
+(*** Future keys can't be seen or used! ***)
+
+(*Nobody can have SEEN keys that will be generated in the future.
+  This has to be proved anew for each protocol description,
+  but should go by similar reasoning every time.  Hardest case is the
+  standard Fake rule.  
+      The length comparison, and Union over C, are essential for the 
+  induction! *)
+goal thy "!!evs. evs : yahalom ==> \
+\                length evs <= length evs' --> \
+\                          Key (newK evs') ~: (UN C. parts (sees C evs))";
+be yahalom.induct 1;
+by YM2_YM4_tac;
+(*auto_tac does not work here, as it performs safe_tac first*)
+by (ALLGOALS Asm_simp_tac);
+by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+				       impOfSubs parts_insert_subset_Un,
+				       Suc_leD]
+			        addss (!simpset))));
+val lemma = result();
+
+(*Variant needed for the main theorem below*)
+goal thy 
+ "!!evs. [| evs : yahalom;  length evs <= length evs' |] ==> \
+\        Key (newK evs') ~: parts (sees C evs)";
+by (fast_tac (!claset addDs [lemma]) 1);
+qed "new_keys_not_seen";
+Addsimps [new_keys_not_seen];
+
+(*Another variant: old messages must contain old keys!*)
+goal thy 
+ "!!evs. [| Says A B X : set_of_list evs;  \
+\           Key (newK evt) : parts {X};    \
+\           evs : yahalom                 \
+\        |] ==> length evt < length evs";
+br ccontr 1;
+by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
+	              addIs [impOfSubs parts_mono, leI]) 1);
+qed "Says_imp_old_keys";
+
+
+(*Nobody can have USED keys that will be generated in the future.
+  ...very like new_keys_not_seen*)
+goal thy "!!evs. evs : yahalom ==> \
+\                length evs <= length evs' --> \
+\                newK evs' ~: keysFor (UN C. parts (sees C evs))";
+be yahalom.induct 1;
+by YM2_YM4_tac;
+bd YM5_parts_sees_Enemy 7;
+by (ALLGOALS Asm_simp_tac);
+(*YM1 and YM3*)
+by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
+(*Fake, YM2, YM4: these messages send unknown (X) components*)
+by (EVERY 
+    (map
+     (best_tac
+      (!claset addSDs [newK_invKey]
+	       addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
+		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
+		      Suc_leD]
+	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
+	       addss (!simpset)))
+     [3,2,1]));
+(*YM5: dummy message*)
+by (best_tac (!claset addSDs [newK_invKey]
+		        addEs  [new_keys_not_seen RSN(2,rev_notE)]
+			addIs  [less_SucI, impOfSubs keysFor_mono]
+			addss (!simpset addsimps [le_def])) 1);
+val lemma = result();
+
+goal thy 
+ "!!evs. [| evs : yahalom;  length evs <= length evs' |] ==> \
+\        newK evs' ~: keysFor (parts (sees C evs))";
+by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
+qed "new_keys_not_used";
+
+bind_thm ("new_keys_not_analzd",
+	  [analz_subset_parts RS keysFor_mono,
+	   new_keys_not_used] MRS contra_subsetD);
+
+Addsimps [new_keys_not_used, new_keys_not_analzd];
+
+
+(** Lemmas concerning the form of items passed in messages **)
+
+
+(****
+ The following is to prove theorems of the form
+
+          Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
+          Key K : analz (sees Enemy evs)
+
+ A more general formula must be proved inductively.
+
+****)
+
+
+(*NOT useful in this form, but it says that session keys are not used
+  to encrypt messages containing other keys, in the actual protocol.
+  We require that agents should behave like this subsequently also.*)
+goal thy 
+ "!!evs. evs : yahalom ==> \
+\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
+\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
+be yahalom.induct 1;
+by YM2_YM4_tac;
+by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
+(*Deals with Faked messages*)
+by (best_tac (!claset addSEs partsEs
+		      addDs [impOfSubs analz_subset_parts,
+                             impOfSubs parts_insert_subset_Un]
+                      addss (!simpset)) 2);
+(*Base case and YM5*)
+by (Auto_tac());
+result();
+
+
+(** Specialized rewriting for this proof **)
+
+Delsimps [image_insert];
+Addsimps [image_insert RS sym];
+
+Delsimps [image_Un];
+Addsimps [image_Un RS sym];
+
+goal thy "insert (Key (newK x)) (sees A evs) = \
+\         Key `` (newK``{x}) Un (sees A evs)";
+by (Fast_tac 1);
+val insert_Key_singleton = result();
+
+goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
+\         Key `` (f `` (insert x E)) Un C";
+by (Fast_tac 1);
+val insert_Key_image = result();
+
+
+(*This lets us avoid analyzing the new message -- unless we have to!*)
+(*NEEDED??*)
+goal thy "synth (analz (sees Enemy evs)) <=   \
+\         synth (analz (sees Enemy (Says A B X # evs)))";
+by (Simp_tac 1);
+br (subset_insertI RS analz_mono RS synth_mono) 1;
+qed "synth_analz_thin";
+
+AddIs [impOfSubs synth_analz_thin];
+
+
+
+(** Session keys are not used to encrypt other session keys **)
+
+(*Could generalize this so that the X component doesn't have to be first
+  in the message?*)
+val enemy_analz_tac =
+  SELECT_GOAL 
+   (EVERY [REPEAT (resolve_tac [impI,notI] 1),
+	   dtac (impOfSubs Fake_analz_insert) 1,
+	   eresolve_tac [asm_rl, synth.Inj] 1,
+	   Fast_tac 1,
+	   Asm_full_simp_tac 1,
+	   IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
+	   ]);
+
+
+(*Lemma for the trivial direction of the if-and-only-if*)
+goal thy  
+ "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
+\         (K : nE | Key K : analz sEe)  ==>     \
+\        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
+by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
+val lemma = result();
+
+
+goal thy  
+ "!!evs. evs : yahalom ==> \
+\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
+\           (K : newK``E | Key K : analz (sees Enemy evs))";
+be yahalom.induct 1;
+bd YM2_analz_sees_Enemy 4;
+bd YM4_analz_sees_Enemy 6;
+by (REPEAT_FIRST (resolve_tac [allI, lemma]));
+by (ALLGOALS (*Takes 35 secs*)
+    (asm_simp_tac 
+     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
+			 @ pushes)
+               setloop split_tac [expand_if])));
+(*YM4*) 
+by (enemy_analz_tac 5);
+(*YM3*)
+by (Fast_tac 4);
+(*YM2*) (** LEVEL 7 **)
+by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] 
+    (insert_commute RS ssubst) 3);
+by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
+    (insert_commute RS ssubst) 3);
+by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3);
+by (enemy_analz_tac 3);
+(*Fake case*) (** LEVEL 11 **)
+by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] 
+    (insert_commute RS ssubst) 2);
+by (enemy_analz_tac 2);
+(*Base case*)
+by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
+qed_spec_mp "analz_image_newK";
+
+
+goal thy
+ "!!evs. evs : yahalom ==>                               \
+\        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
+\        (K = newK evt | Key K : analz (sees Enemy evs))";
+by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
+				   insert_Key_singleton]) 1);
+by (Fast_tac 1);
+qed "analz_insert_Key_newK";
+
+
+(*Describes the form *and age* of K when the following message is sent*)
+goal thy 
+ "!!evs. [| Says Server B \
+\            {|NA, Crypt {|NA, K|} (shrK A),                      \
+\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
+\           evs : yahalom |]                                        \
+\        ==> (EX evt:yahalom. K = Key(newK evt) & \
+\                           length evt < length evs) &            \
+\            (EX i. NA = Nonce i)";
+be rev_mp 1;
+be yahalom.induct 1;
+by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
+qed "Says_Server_message_form";
+
+
+(*Crucial secrecy property: Enemy does not see the keys sent in msg YM3*)
+goal thy 
+ "!!evs. [| Says Server A \
+\            {|NA, Crypt {|NA, K|} (shrK B),                      \
+\                  Crypt {|NB, K|} (shrK A)|} : set_of_list evs;  \
+\           A ~: bad;  B ~: bad;  evs : yahalom |] ==>              \
+\     K ~: analz (sees Enemy evs)";
+be rev_mp 1;
+be yahalom.induct 1;
+bd YM2_analz_sees_Enemy 4;
+bd YM4_analz_sees_Enemy 6;
+by (ALLGOALS Asm_simp_tac);
+(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
+by (REPEAT_FIRST (resolve_tac [conjI, impI]));
+by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
+by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac));
+by (ALLGOALS
+    (asm_full_simp_tac 
+     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
+			  analz_insert_Key_newK] @ pushes)
+               setloop split_tac [expand_if])));
+(*YM3*)
+by (fast_tac (!claset addSEs [less_irrefl]) 3);
+(*Fake*) (** LEVEL 10 **)
+by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1);
+by (enemy_analz_tac 1);
+(*YM4*)
+by (mp_tac 2);
+by (enemy_analz_tac 2);
+(*YM2*)
+by (mp_tac 1);
+by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
+    (insert_commute RS ssubst) 1);
+by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (enemy_analz_tac 1);
+qed "Enemy_not_see_encrypted_key";
+
+
+
+(*** Session keys are issued at most once, and identify the principals ***)
+
+(** First, two lemmas for the Fake, YM2 and YM4 cases **)
+
+goal thy 
+ "!!evs. [| X : synth (analz (sees Enemy evs));                \
+\           Crypt X' (shrK C) : parts{X};                      \
+\           C ~: bad;  evs : yahalom |]  \
+\        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
+by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
+	              addDs [impOfSubs parts_insert_subset_Un]
+                      addss (!simpset)) 1);
+qed "Crypt_Fake_parts";
+
+goal thy 
+ "!!evs. [| Crypt X' K : parts (sees A evs);  evs : yahalom |]  \
+\        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
+\            Crypt X' K : parts {Y}";
+bd parts_singleton 1;
+by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
+qed "Crypt_parts_singleton";
+
+fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
+
+(*The Key K uniquely identifies a pair of senders in the message encrypted by
+  C, but if C=Enemy then he could send all sorts of nonsense.*)
+goal thy 
+ "!!evs. evs : yahalom ==>                                     \
+\      EX A B. ALL C.                                        \
+\         C ~: bad -->                                       \
+\         (ALL S S' X. Says S S' X : set_of_list evs -->     \
+\           (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
+by (Simp_tac 1);
+be yahalom.induct 1;
+bd YM2_analz_sees_Enemy 4;
+bd YM4_analz_sees_Enemy 6;
+by (ALLGOALS 
+    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
+by (REPEAT_FIRST (etac exE));
+(*YM4*)
+by (ex_strip_tac 4);
+by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
+			      Crypt_parts_singleton]) 4);
+(*YM3: Case split propagates some context to other subgoal...*)
+	(** LEVEL 8 **)
+by (excluded_middle_tac "K = newK evsa" 3);
+by (Asm_simp_tac 3);
+by (REPEAT (ares_tac [exI] 3));
+(*...we prove this case by contradiction: the key is too new!*)
+by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
+		      addSEs partsEs
+		      addEs [Says_imp_old_keys RS less_irrefl]
+	              addss (!simpset)) 3);
+(*YM2*) (** LEVEL 12 **)
+by (ex_strip_tac 2);
+by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
+    (insert_commute RS ssubst) 2);
+by (Simp_tac 2);
+by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
+			      Crypt_parts_singleton]) 2);
+(*Fake*) (** LEVEL 16 **)
+by (ex_strip_tac 1);
+by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
+qed "unique_session_keys";
+
+(*It seems strange but this theorem is NOT needed to prove the main result!*)
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/Auth/Yahalom.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Yahalom.thy	Thu Sep 12 10:40:05 1996 +0200
@@ -0,0 +1,73 @@
+(*  Title:      HOL/Auth/OtwayRees
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+Inductive relation "yahalom" for the Yahalom protocol.
+
+From page 257 of
+  Burrows, Abadi and Needham.  A Logic of Authentication.
+  Proc. Royal Soc. 426 (1989)
+*)
+
+OtwayRees = Shared + 
+
+consts  yahalom   :: "event list set"
+inductive yahalom
+  intrs 
+         (*Initial trace is empty*)
+    Nil  "[]: yahalom"
+
+         (*The enemy MAY say anything he CAN say.  We do not expect him to
+           invent new nonces here, but he can also use NS1.  Common to
+           all similar protocols.*)
+    Fake "[| evs: yahalom;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
+          ==> Says Enemy B X  # evs : yahalom"
+
+         (*Alice initiates a protocol run*)
+    YM1  "[| evs: yahalom;  A ~= B |]
+          ==> Says A B {|Nonce (newN evs), Agent A |} # evs : yahalom"
+
+         (*Bob's response to Alice's message.  Bob doesn't know who 
+	   the sender is, hence the A' in the sender field.
+           We modify the published protocol by NOT encrypting NB.*)
+    YM2  "[| evs: yahalom;  B ~= Server;
+             Says A' B {|Nonce NA, Agent A|} : set_of_list evs |]
+          ==> Says B Server 
+                  {|Agent B, 
+                    Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|}
+                 # evs : yahalom"
+
+         (*The Server receives Bob's message.  He responds by sending a
+            new session key to Alice, with a packet for forwarding to Bob.*)
+    YM3  "[| evs: yahalom;  B ~= Server;
+             Says B' Server 
+                  {|Nonce NA, Agent A, Agent B, 
+                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
+                    Nonce NB, 
+                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
+               : set_of_list evs |]
+          ==> Says Server B 
+                  {|Nonce NA, 
+                    Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
+                    Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
+                 # evs : yahalom"
+
+         (*Bob receives the Server's (?) message and compares the Nonces with
+	   those in the message he previously sent the Server.*)
+    YM4  "[| evs: yahalom;  A ~= B;  
+             Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
+               : set_of_list evs;
+             Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
+               : set_of_list evs |]
+          ==> (Says B A {|Nonce NA, X|}) # evs : yahalom"
+
+         (*Alice checks her Nonce, then sends a dummy message to Bob,
+           using the new session key.*)
+    YM5  "[| evs: yahalom;  
+             Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
+               : set_of_list evs;
+             Says A  B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
+          ==> Says A B (Crypt (Agent A) K)  # evs : yahalom"
+
+end
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/IOA/NTP/Lemmas.ML
--- a/src/HOL/IOA/NTP/Lemmas.ML	Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/IOA/NTP/Lemmas.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -156,10 +156,7 @@
 
 goal Arith.thy "~0<n --> n = 0";
   by (nat_ind_tac "n" 1);
-  by (Asm_simp_tac 1);
-  by (safe_tac (!claset));
-  by (Asm_full_simp_tac 1);
-  by (Asm_full_simp_tac 1);
+  by (Auto_tac ());
 qed "zero_eq";
 
 goal Arith.thy "x < Suc(y) --> x<=y";
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/Lex/Auto.ML
--- a/src/HOL/Lex/Auto.ML	Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/Lex/Auto.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -29,7 +29,7 @@
   by (case_tac "zs=[]" 1);
    by(hyp_subst_tac 1);
    by(Asm_full_simp_tac 1);
-  by(fast_tac (!claset addSEs [Cons_neq_Nil]) 1);
+  by(Fast_tac 1);
  by(res_inst_tac [("x","[x]")] exI 1);
  by(asm_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
 by(res_inst_tac [("x","x#us")] exI 1);
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/List.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -8,10 +8,8 @@
 
 open List;
 
-val [Nil_not_Cons,Cons_not_Nil] = list.distinct;
-
-bind_thm("Cons_neq_Nil", Cons_not_Nil RS notE);
-bind_thm("Nil_neq_Cons", sym RS Cons_neq_Nil);
+AddIffs list.distinct;
+AddIffs list.inject;
 
 bind_thm("Cons_inject", (hd list.inject) RS iffD1 RS conjE);
 
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/Nat.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -95,9 +95,9 @@
 by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1));
 qed "Suc_not_Zero";
 
-bind_thm ("Zero_not_Suc", (Suc_not_Zero RS not_sym));
+bind_thm ("Zero_not_Suc", Suc_not_Zero RS not_sym);
 
-Addsimps [Suc_not_Zero,Zero_not_Suc];
+AddIffs [Suc_not_Zero,Zero_not_Suc];
 
 bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE));
 val Zero_neq_Suc = sym RS Suc_neq_Zero;
@@ -118,9 +118,11 @@
 by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]); 
 qed "Suc_Suc_eq";
 
+AddIffs [Suc_Suc_eq];
+
 goal Nat.thy "n ~= Suc(n)";
 by (nat_ind_tac "n" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsimps [Suc_Suc_eq])));
+by (ALLGOALS Asm_simp_tac);
 qed "n_not_Suc_n";
 
 bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
@@ -128,12 +130,11 @@
 (*** nat_case -- the selection operator for nat ***)
 
 goalw Nat.thy [nat_case_def] "nat_case a f 0 = a";
-by (fast_tac (!claset addIs [select_equality] addEs [Zero_neq_Suc]) 1);
+by (fast_tac (!claset addIs [select_equality]) 1);
 qed "nat_case_0";
 
 goalw Nat.thy [nat_case_def] "nat_case a f (Suc k) = f(k)";
-by (fast_tac (!claset addIs [select_equality] 
-                       addEs [make_elim Suc_inject, Suc_neq_Zero]) 1);
+by (fast_tac (!claset addIs [select_equality]) 1);
 qed "nat_case_Suc";
 
 (** Introduction rules for 'pred_nat' **)
@@ -152,9 +153,8 @@
 goalw Nat.thy [wf_def] "wf(pred_nat)";
 by (strip_tac 1);
 by (nat_ind_tac "x" 1);
-by (fast_tac (!claset addSEs [mp, pred_natE, Pair_inject, 
-                             make_elim Suc_inject]) 2);
-by (fast_tac (!claset addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1);
+by (fast_tac (!claset addSEs [mp, pred_natE]) 2);
+by (fast_tac (!claset addSEs [mp, pred_natE]) 1);
 qed "wf_pred_nat";
 
 
@@ -226,7 +226,7 @@
 by (etac less_trans 1);
 by (rtac lessI 1);
 qed "zero_less_Suc";
-Addsimps [zero_less_Suc];
+AddIffs [zero_less_Suc];
 
 (** Elimination properties **)
 
@@ -265,19 +265,19 @@
 by (etac Zero_neq_Suc 1);
 by (etac Zero_neq_Suc 1);
 qed "not_less0";
-Addsimps [not_less0];
+
+AddIffs [not_less0];
 
 (* n<0 ==> R *)
-bind_thm ("less_zeroE", (not_less0 RS notE));
-AddSEs [less_zeroE];
+bind_thm ("less_zeroE", not_less0 RS notE);
 
 val [major,less,eq] = goal Nat.thy
     "[| m < Suc(n);  m<n ==> P;  m=n ==> P |] ==> P";
 by (rtac (major RS lessE) 1);
 by (rtac eq 1);
-by (fast_tac (!claset addSDs [Suc_inject]) 1);
+by (Fast_tac 1);
 by (rtac less 1);
-by (fast_tac (!claset addSDs [Suc_inject]) 1);
+by (Fast_tac 1);
 qed "less_SucE";
 
 goal Nat.thy "(m < Suc(n)) = (m < n | m = n)";
@@ -305,11 +305,8 @@
 val [prem] = goal Nat.thy "Suc(m) < n ==> m<n";
 by (rtac (prem RS rev_mp) 1);
 by (nat_ind_tac "n" 1);
-by (rtac impI 1);
-by (etac less_zeroE 1);
-by (fast_tac (!claset addSIs [lessI RS less_SucI]
-                     addSDs [Suc_inject]
-                     addEs  [less_trans, lessE]) 1);
+by (ALLGOALS (fast_tac (!claset addSIs [lessI RS less_SucI]
+                                addEs  [less_trans, lessE])));
 qed "Suc_lessD";
 
 val [major,minor] = goal Nat.thy 
@@ -321,21 +318,15 @@
 by (assume_tac 1);
 qed "Suc_lessE";
 
-val [major] = goal Nat.thy "Suc(m) < Suc(n) ==> m<n";
-by (rtac (major RS lessE) 1);
-by (REPEAT (rtac lessI 1
-     ORELSE eresolve_tac [make_elim Suc_inject, ssubst, Suc_lessD] 1));
+goal Nat.thy "!!m n. Suc(m) < Suc(n) ==> m<n";
+by (fast_tac (!claset addEs [lessE, Suc_lessD] addIs [lessI]) 1);
 qed "Suc_less_SucD";
 
-val prems = goal Nat.thy "m<n ==> Suc(m) < Suc(n)";
-by (subgoal_tac "m<n --> Suc(m) < Suc(n)" 1);
-by (fast_tac (!claset addIs prems) 1);
+goal Nat.thy "!!m n. m<n ==> Suc(m) < Suc(n)";
+by (etac rev_mp 1);
 by (nat_ind_tac "n" 1);
-by (rtac impI 1);
-by (etac less_zeroE 1);
-by (fast_tac (!claset addSIs [lessI]
-                     addSDs [Suc_inject]
-                     addEs  [less_trans, lessE]) 1);
+by (ALLGOALS (fast_tac (!claset addSIs [lessI]
+                                addEs  [less_trans, lessE])));
 qed "Suc_mono";
 
 
@@ -411,7 +402,7 @@
 
 Addsimps [less_not_refl,
           (*less_Suc_eq, makes simpset non-confluent*) le0, le_0_eq,
-          Suc_Suc_eq, Suc_n_not_le_n,
+          Suc_n_not_le_n,
           n_not_Suc_n, Suc_n_not_n,
           nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
 
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/Relation.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -1,21 +1,15 @@
 (*  Title:      Relation.ML
     ID:         $Id$
-    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
-                Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994 Universita' di Firenze
-    Copyright   1993  University of Cambridge
+    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
 *)
 
-val RSLIST = curry (op MRS);
-
 open Relation;
 
 (** Identity relation **)
 
 goalw Relation.thy [id_def] "(a,a) : id";  
-by (rtac CollectI 1);
-by (rtac exI 1);
-by (rtac refl 1);
+by (Fast_tac 1);
 qed "idI";
 
 val major::prems = goalw Relation.thy [id_def]
@@ -34,9 +28,9 @@
 
 (** Composition of two relations **)
 
-val prems = goalw Relation.thy [comp_def]
-    "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
-by (fast_tac (!claset addIs prems) 1);
+goalw Relation.thy [comp_def]
+    "!!r s. [| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
+by (Fast_tac 1);
 qed "compI";
 
 (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
@@ -45,7 +39,8 @@
 \       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
 \    |] ==> P";
 by (cut_facts_tac prems 1);
-by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 ORELSE ares_tac prems 1));
+by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 
+     ORELSE ares_tac prems 1));
 qed "compE";
 
 val prems = goal Relation.thy
@@ -59,15 +54,12 @@
 AddIs [compI, idI];
 AddSEs [compE, idE];
 
-val comp_cs = prod_cs addIs [compI, idI] addSEs [compE, idE];
-
 goal Relation.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
 by (Fast_tac 1);
 qed "comp_mono";
 
 goal Relation.thy
-    "!!r s. [| s <= A Times B;  r <= B Times C |] ==> \
-\           (r O s) <= A Times C";
+    "!!r s. [| s <= A Times B;  r <= B Times C |] ==> (r O s) <= A Times C";
 by (Fast_tac 1);
 qed "comp_subset_Sigma";
 
@@ -78,14 +70,19 @@
 by (REPEAT (ares_tac (prems@[allI,impI]) 1));
 qed "transI";
 
-val major::prems = goalw Relation.thy [trans_def]
-    "[| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
-by (cut_facts_tac [major] 1);
-by (fast_tac (!claset addIs prems) 1);
+goalw Relation.thy [trans_def]
+    "!!r. [| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
+by (Fast_tac 1);
 qed "transD";
 
 (** Natural deduction for converse(r) **)
 
+goalw Relation.thy [converse_def] "!!a b r. ((a,b):converse r) = ((b,a):r)";
+by (Simp_tac 1);
+qed "converse_iff";
+
+AddIffs [converse_iff];
+
 goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)";
 by (Simp_tac 1);
 qed "converseI";
@@ -94,6 +91,7 @@
 by (Fast_tac 1);
 qed "converseD";
 
+(*More general than converseD, as it "splits" the member of the relation*)
 qed_goalw "converseE" Relation.thy [converse_def]
     "[| yx : converse(r);  \
 \       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
@@ -103,11 +101,7 @@
     (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
     (assume_tac 1) ]);
 
-AddSIs [converseI];
-AddSEs [converseD,converseE];
-
-val converse_cs = comp_cs addSIs [converseI]
-                          addSEs [converseD,converseE];
+AddSEs [converseE];
 
 goalw Relation.thy [converse_def] "converse(converse R) = R";
 by(Fast_tac 1);
@@ -128,6 +122,9 @@
   [ (rtac (Domain_iff RS iffD1 RS exE) 1),
     (REPEAT (ares_tac prems 1)) ]);
 
+AddIs  [DomainI];
+AddSEs [DomainE];
+
 (** Range **)
 
 qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
@@ -140,11 +137,14 @@
     (resolve_tac prems 1),
     (etac converseD 1) ]);
 
+AddIs  [RangeI];
+AddSEs [RangeE];
+
 (*** Image of a set under a relation ***)
 
 qed_goalw "Image_iff" Relation.thy [Image_def]
     "b : r^^A = (? x:A. (x,b):r)"
- (fn _ => [ fast_tac (!claset addIs [RangeI]) 1 ]);
+ (fn _ => [ Fast_tac 1 ]);
 
 qed_goal "Image_singleton_iff" Relation.thy
     "(b : r^^{a}) = ((a,b):r)"
@@ -153,40 +153,31 @@
 
 qed_goalw "ImageI" Relation.thy [Image_def]
     "!!a b r. [| (a,b): r;  a:A |] ==> b : r^^A"
- (fn _ => [ (REPEAT (ares_tac [CollectI,RangeI,bexI] 1)),
-            (resolve_tac [conjI ] 1),
-            (rtac RangeI 1),
-            (REPEAT (Fast_tac 1))]);
+ (fn _ => [ (Fast_tac 1)]);
 
 qed_goalw "ImageE" Relation.thy [Image_def]
     "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
  (fn major::prems=>
   [ (rtac (major RS CollectE) 1),
-    (safe_tac (!claset)),
-    (etac RangeE 1),
+    (Step_tac 1),
     (rtac (hd prems) 1),
     (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
 
+AddIs  [ImageI];
+AddSEs [ImageE];
+
 qed_goal "Image_subset" Relation.thy
     "!!A B r. r <= A Times B ==> r^^C <= B"
  (fn _ =>
   [ (rtac subsetI 1),
     (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
 
-AddSIs [converseI]; 
-AddIs  [ImageI, DomainI, RangeI];
-AddSEs [ImageE, DomainE, RangeE];
-
-val rel_cs = converse_cs addSIs [converseI] 
-                         addIs  [ImageI, DomainI, RangeI]
-                         addSEs [ImageE, DomainE, RangeE];
-
 goal Relation.thy "R O id = R";
-by(fast_tac (!claset addIs [set_ext] addbefore (split_all_tac 1)) 1);
+by (fast_tac (!claset addbefore (split_all_tac 1)) 1);
 qed "R_O_id";
 
 goal Relation.thy "id O R = R";
-by(fast_tac (!claset addIs [set_ext] addbefore (split_all_tac 1)) 1);
+by (fast_tac (!claset addbefore (split_all_tac 1)) 1);
 qed "id_O_R";
 
 Addsimps [R_O_id,id_O_R];
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/Set.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-For set.thy.  Set theory for higher-order logic.  A set is simply a predicate.
+Set theory for higher-order logic.  A set is simply a predicate.
 *)
 
 open Set;
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/Sexp.ML
--- a/src/HOL/Sexp.ML	Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/Sexp.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -10,17 +10,6 @@
 
 (** sexp_case **)
 
-val sexp_free_cs = 
-    set_cs addSDs [Leaf_inject, Numb_inject, Scons_inject] 
-           addSEs [Leaf_neq_Scons, Leaf_neq_Numb,
-                   Numb_neq_Scons, Numb_neq_Leaf,
-                   Scons_neq_Leaf, Scons_neq_Numb];
-
-AddSDs [Leaf_inject, Numb_inject, Scons_inject];
-AddSEs [Leaf_neq_Scons, Leaf_neq_Numb,
-                   Numb_neq_Scons, Numb_neq_Leaf,
-                   Scons_neq_Leaf, Scons_neq_Numb];
-
 goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
 by (resolve_tac [select_equality] 1);
 by (ALLGOALS (Fast_tac));
@@ -60,8 +49,7 @@
 val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp";
 by (rtac (major RS setup_induction) 1);
 by (etac sexp.induct 1);
-by (ALLGOALS 
-    (fast_tac (!claset addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject])));
+by (ALLGOALS Fast_tac);
 qed "Scons_D";
 
 (** Introduction rules for 'pred_sexp' **)
@@ -109,9 +97,7 @@
 goal Sexp.thy "wf(pred_sexp)";
 by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
 by (etac sexp.induct 1);
-by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Scons_inject]) 3);
-by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Numb_neq_Scons]) 2);
-by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Leaf_neq_Scons]) 1);
+by (ALLGOALS (fast_tac (!claset addSEs [mp, pred_sexpE])));
 qed "wf_pred_sexp";
 
 (*** sexp_rec -- by wf recursion on pred_sexp ***)
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/Sum.ML
--- a/src/HOL/Sum.ML	Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/Sum.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -40,16 +40,13 @@
 by (rtac Inr_RepI 1);
 qed "Inl_not_Inr";
 
-bind_thm ("Inl_neq_Inr", (Inl_not_Inr RS notE));
-val Inr_neq_Inl = sym RS Inl_neq_Inr;
+bind_thm ("Inr_not_Inl", Inl_not_Inr RS not_sym);
+
+AddIffs [Inl_not_Inr, Inr_not_Inl];
 
-goal Sum.thy "(Inl(a)=Inr(b)) = False";
-by (simp_tac (!simpset addsimps [Inl_not_Inr]) 1);
-qed "Inl_Inr_eq";
+bind_thm ("Inl_neq_Inr", Inl_not_Inr RS notE);
 
-goal Sum.thy "(Inr(b)=Inl(a))  =  False";
-by (simp_tac (!simpset addsimps [Inl_not_Inr RS not_sym]) 1);
-qed "Inr_Inl_eq";
+val Inr_neq_Inl = sym RS Inl_neq_Inr;
 
 
 (** Injectiveness of Inl and Inr **)
@@ -88,16 +85,18 @@
 by (fast_tac (!claset addSEs [Inr_inject]) 1);
 qed "Inr_eq";
 
+AddIffs [Inl_eq, Inr_eq];
+
 (*** Rules for the disjoint sum of two SETS ***)
 
 (** Introduction rules for the injections **)
 
 goalw Sum.thy [sum_def] "!!a A B. a : A ==> Inl(a) : A plus B";
-by (REPEAT (ares_tac [UnI1,imageI] 1));
+by (Fast_tac 1);
 qed "InlI";
 
 goalw Sum.thy [sum_def] "!!b A B. b : B ==> Inr(b) : A plus B";
-by (REPEAT (ares_tac [UnI2,imageI] 1));
+by (Fast_tac 1);
 qed "InrI";
 
 (** Elimination rules **)
@@ -113,13 +112,8 @@
 qed "plusE";
 
 
-val sum_cs = set_cs addSIs [InlI, InrI] 
-                    addSEs [plusE, Inl_neq_Inr, Inr_neq_Inl]
-                    addSDs [Inl_inject, Inr_inject];
-
 AddSIs [InlI, InrI]; 
-AddSEs [plusE, Inl_neq_Inr, Inr_neq_Inl];
-AddSDs [Inl_inject, Inr_inject];
+AddSEs [plusE];
 
 
 (** sum_case -- the selection operator for sums **)
@@ -132,6 +126,8 @@
 by (fast_tac (!claset addIs [select_equality]) 1);
 qed "sum_case_Inr";
 
+Addsimps [sum_case_Inl, sum_case_Inr];
+
 (** Exhaustion rule for sums -- a degenerate form of induction **)
 
 val prems = goalw Sum.thy [Inl_def,Inr_def]
@@ -152,17 +148,10 @@
 
 goal Sum.thy "R(sum_case f g s) = \
 \             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
-by (rtac sumE 1);
-by (etac ssubst 1);
-by (stac sum_case_Inl 1);
-by (fast_tac (!claset addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
-by (etac ssubst 1);
-by (stac sum_case_Inr 1);
-by (fast_tac (!claset addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
+by (res_inst_tac [("s","s")] sumE 1);
+by (Auto_tac());
 qed "expand_sum_case";
 
-Addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq,  sum_case_Inl, sum_case_Inr];
-
 (*Prevents simplification of f and g: much faster*)
 qed_goal "sum_case_weak_cong" Sum.thy
   "s=t ==> sum_case f g s = sum_case f g t"
@@ -170,7 +159,6 @@
 
 
 
-
 (** Rules for the Part primitive **)
 
 goalw Sum.thy [Part_def]
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/Trancl.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -276,6 +276,3 @@
 by (fast_tac (!claset addSDs [lemma]) 1);
 qed "trancl_subset_Sigma";
 
-(* Don't add r_into_rtrancl: it messes up the proofs in Lambda *)
-val trancl_cs = rel_cs addIs [rtrancl_refl];
-
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/Univ.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -27,13 +27,13 @@
 
 (** Push -- an injection, analogous to Cons on lists **)
 
-val [major] = goalw Univ.thy [Push_def] "Push i f =Push j g  ==> i=j";
+val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g  ==> i=j";
 by (rtac (major RS fun_cong RS box_equals RS Suc_inject) 1);
 by (rtac nat_case_0 1);
 by (rtac nat_case_0 1);
 qed "Push_inject1";
 
-val [major] = goalw Univ.thy [Push_def] "Push i f =Push j g  ==> f=g";
+val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g  ==> f=g";
 by (rtac (major RS fun_cong RS ext RS box_equals) 1);
 by (rtac (nat_case_Suc RS ext) 1);
 by (rtac (nat_case_Suc RS ext) 1);
@@ -90,10 +90,8 @@
                           Pair_inject, sym RS Push_neq_K0] 1
      ORELSE resolve_tac [Node_K0_I, Rep_Node RS Node_Push_I] 1));
 qed "Scons_not_Atom";
-bind_thm ("Atom_not_Scons", (Scons_not_Atom RS not_sym));
+bind_thm ("Atom_not_Scons", Scons_not_Atom RS not_sym);
 
-bind_thm ("Scons_neq_Atom", (Scons_not_Atom RS notE));
-val Atom_neq_Scons = sym RS Scons_neq_Atom;
 
 (*** Injectiveness ***)
 
@@ -104,12 +102,18 @@
 qed "inj_Atom";
 val Atom_inject = inj_Atom RS injD;
 
+goal Univ.thy "(Atom(a)=Atom(b)) = (a=b)";
+by (fast_tac (!claset addSEs [Atom_inject]) 1);
+qed "Atom_Atom_eq";
+AddIffs [Atom_Atom_eq];
+
 goalw Univ.thy [Leaf_def,o_def] "inj(Leaf)";
 by (rtac injI 1);
 by (etac (Atom_inject RS Inl_inject) 1);
 qed "inj_Leaf";
 
 val Leaf_inject = inj_Leaf RS injD;
+AddSDs [Leaf_inject];
 
 goalw Univ.thy [Numb_def,o_def] "inj(Numb)";
 by (rtac injI 1);
@@ -117,6 +121,7 @@
 qed "inj_Numb";
 
 val Numb_inject = inj_Numb RS injD;
+AddSDs [Numb_inject];
 
 (** Injectiveness of Push_Node **)
 
@@ -131,7 +136,7 @@
 by (etac (Push_inject1 RS sym) 1);
 by (rtac (inj_Rep_Node RS injD) 1);
 by (etac trans 1);
-by (safe_tac (!claset addSEs [Pair_inject,Push_inject,sym]));
+by (safe_tac (!claset addSEs [Push_inject,sym]));
 qed "Push_Node_inject";
 
 
@@ -139,14 +144,12 @@
 
 val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> M<=M'";
 by (cut_facts_tac [major] 1);
-by (fast_tac (!claset addSDs [Suc_inject]
-                     addSEs [Push_Node_inject, Zero_neq_Suc]) 1);
+by (fast_tac (!claset addSEs [Push_Node_inject]) 1);
 qed "Scons_inject_lemma1";
 
 val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> N<=N'";
 by (cut_facts_tac [major] 1);
-by (fast_tac (!claset addSDs [Suc_inject]
-                     addSEs [Push_Node_inject, Suc_neq_Zero]) 1);
+by (fast_tac (!claset addSEs [Push_Node_inject]) 1);
 qed "Scons_inject_lemma2";
 
 val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
@@ -165,10 +168,7 @@
 by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
 qed "Scons_inject";
 
-(*rewrite rules*)
-goal Univ.thy "(Atom(a)=Atom(b)) = (a=b)";
-by (fast_tac (!claset addSEs [Atom_inject]) 1);
-qed "Atom_Atom_eq";
+AddSDs [Scons_inject];
 
 goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')";
 by (fast_tac (!claset addSEs [Scons_inject]) 1);
@@ -181,35 +181,35 @@
 goalw Univ.thy [Leaf_def,o_def] "(M$N) ~= Leaf(a)";
 by (rtac Scons_not_Atom 1);
 qed "Scons_not_Leaf";
-bind_thm ("Leaf_not_Scons", (Scons_not_Leaf RS not_sym));
+bind_thm ("Leaf_not_Scons", Scons_not_Leaf RS not_sym);
 
-bind_thm ("Scons_neq_Leaf", (Scons_not_Leaf RS notE));
-val Leaf_neq_Scons = sym RS Scons_neq_Leaf;
+AddIffs [Scons_not_Leaf, Leaf_not_Scons];
+
 
 (** Scons vs Numb **)
 
 goalw Univ.thy [Numb_def,o_def] "(M$N) ~= Numb(k)";
 by (rtac Scons_not_Atom 1);
 qed "Scons_not_Numb";
-bind_thm ("Numb_not_Scons", (Scons_not_Numb RS not_sym));
+bind_thm ("Numb_not_Scons", Scons_not_Numb RS not_sym);
 
-bind_thm ("Scons_neq_Numb", (Scons_not_Numb RS notE));
-val Numb_neq_Scons = sym RS Scons_neq_Numb;
+AddIffs [Scons_not_Numb, Numb_not_Scons];
+
 
 (** Leaf vs Numb **)
 
 goalw Univ.thy [Leaf_def,Numb_def] "Leaf(a) ~= Numb(k)";
-by (simp_tac (!simpset addsimps [Atom_Atom_eq,Inl_not_Inr]) 1);
+by (simp_tac (!simpset addsimps [Inl_not_Inr]) 1);
 qed "Leaf_not_Numb";
-bind_thm ("Numb_not_Leaf", (Leaf_not_Numb RS not_sym));
+bind_thm ("Numb_not_Leaf", Leaf_not_Numb RS not_sym);
 
-bind_thm ("Leaf_neq_Numb", (Leaf_not_Numb RS notE));
-val Numb_neq_Leaf = sym RS Leaf_neq_Numb;
+AddIffs [Leaf_not_Numb, Numb_not_Leaf];
 
 
 (*** ndepth -- the depth of a node ***)
 
-Addsimps [apfst_conv,Scons_not_Atom,Atom_not_Scons,Scons_Scons_eq];
+Addsimps [apfst_conv];
+AddIffs  [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq];
 
 
 goalw Univ.thy [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0";
@@ -244,13 +244,11 @@
 (*** ntrunc applied to the various node sets ***)
 
 goalw Univ.thy [ntrunc_def] "ntrunc 0 M = {}";
-by (safe_tac (!claset addSIs [equalityI] addSEs [less_zeroE]));
+by (Fast_tac 1);
 qed "ntrunc_0";
 
 goalw Univ.thy [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)";
-by (safe_tac (!claset addSIs [equalityI]));
-by (stac ndepth_K0 1);
-by (rtac zero_less_Suc 1);
+by (fast_tac (!claset addss (!simpset addsimps [ndepth_K0])) 1);
 qed "ntrunc_Atom";
 
 goalw Univ.thy [Leaf_def,o_def] "ntrunc (Suc k) (Leaf a) = Leaf(a)";
@@ -275,7 +273,7 @@
 goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
 by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
 by (rewtac Scons_def);
-by (safe_tac (!claset addSIs [equalityI]));
+by (Fast_tac 1);
 qed "ntrunc_one_In0";
 
 goalw Univ.thy [In0_def]
@@ -286,7 +284,7 @@
 goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
 by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
 by (rewtac Scons_def);
-by (safe_tac (!claset addSIs [equalityI]));
+by (Fast_tac 1);
 qed "ntrunc_one_In1";
 
 goalw Univ.thy [In1_def]
@@ -348,9 +346,9 @@
 by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1);
 qed "In0_not_In1";
 
-bind_thm ("In1_not_In0", (In0_not_In1 RS not_sym));
-bind_thm ("In0_neq_In1", (In0_not_In1 RS notE));
-val In1_neq_In0 = sym RS In0_neq_In1;
+bind_thm ("In1_not_In0", In0_not_In1 RS not_sym);
+
+AddIffs [In0_not_In1, In1_not_In0];
 
 val [major] = goalw Univ.thy [In0_def] "In0(M) = In0(N) ==>  M=N";
 by (rtac (major RS Scons_inject2) 1);
@@ -360,6 +358,7 @@
 by (rtac (major RS Scons_inject2) 1);
 qed "In1_inject";
 
+AddSDs [In0_inject, In1_inject];
 
 (*** proving equality of sets and functions using ntrunc ***)
 
@@ -414,17 +413,15 @@
 (*** Split and Case ***)
 
 goalw Univ.thy [Split_def] "Split c (M$N) = c M N";
-by (fast_tac (!claset addIs [select_equality] addEs [Scons_inject]) 1);
+by (fast_tac (!claset addIs [select_equality]) 1);
 qed "Split";
 
 goalw Univ.thy [Case_def] "Case c d (In0 M) = c(M)";
-by (fast_tac (!claset addIs [select_equality] 
-                     addEs [make_elim In0_inject, In0_neq_In1]) 1);
+by (fast_tac (!claset addIs [select_equality]) 1);
 qed "Case_In0";
 
 goalw Univ.thy [Case_def] "Case c d (In1 N) = d(N)";
-by (fast_tac (!claset addIs [select_equality] 
-                     addEs [make_elim In1_inject, In1_neq_In0]) 1);
+by (fast_tac (!claset addIs [select_equality]) 1);
 qed "Case_In1";
 
 (**** UN x. B(x) rules ****)
@@ -506,11 +503,6 @@
 qed "dsumE";
 
 
-val univ_cs =
-    prod_cs addSIs [diagI, uprodI, dprodI]
-            addIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I]
-            addSEs [diagE, uprodE, dprodE, usumE, dsumE];
-
 AddSIs [diagI, uprodI, dprodI];
 AddIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I];
 AddSEs [diagE, uprodE, dprodE, usumE, dsumE];
@@ -556,18 +548,15 @@
 (*** Domain ***)
 
 goal Univ.thy "fst `` diag(A) = A";
-by (fast_tac (!claset addIs [diagI] addSEs [diagE]) 1);
+by (Fast_tac 1);
 qed "fst_image_diag";
 
 goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
-by (fast_tac (!claset addIs [uprodI, dprodI]
-                     addSEs [uprodE, dprodE]) 1);
+by (Fast_tac 1);
 qed "fst_image_dprod";
 
 goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
-by (fast_tac (!claset addIs [usum_In0I, usum_In1I, 
-                             dsum_In0I, dsum_In1I]
-                     addSEs [usumE, dsumE]) 1);
+by (Fast_tac 1);
 qed "fst_image_dsum";
 
 Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum];
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/cladata.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/cladata.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -0,0 +1,63 @@
+(*  Title:      HOL/cladata.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1996  University of Cambridge
+
+Setting up the classical reasoner 
+*)
+
+
+(** Applying HypsubstFun to generate hyp_subst_tac **)
+section "Classical Reasoner";
+
+structure Hypsubst_Data =
+  struct
+  structure Simplifier = Simplifier
+  (*Take apart an equality judgement; otherwise raise Match!*)
+  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
+  val eq_reflection = eq_reflection
+  val imp_intr = impI
+  val rev_mp = rev_mp
+  val subst = subst
+  val sym = sym
+  end;
+
+structure Hypsubst = HypsubstFun(Hypsubst_Data);
+open Hypsubst;
+
+(*** Applying ClassicalFun to create a classical prover ***)
+structure Classical_Data = 
+  struct
+  val sizef     = size_of_thm
+  val mp        = mp
+  val not_elim  = notE
+  val classical = classical
+  val hyp_subst_tacs=[hyp_subst_tac]
+  end;
+
+structure Classical = ClassicalFun(Classical_Data);
+open Classical;
+
+(*Propositional rules*)
+val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
+                       addSEs [conjE,disjE,impCE,FalseE,iffE];
+
+(*Quantifier rules*)
+val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
+                     addSEs [exE,ex1E] addEs [allE];
+
+exception CS_DATA of claset;
+
+let fun merge [] = CS_DATA empty_cs
+      | merge cs = let val cs = map (fn CS_DATA x => x) cs;
+                   in CS_DATA (foldl merge_cs (hd cs, tl cs)) end;
+
+    fun put (CS_DATA cs) = claset := cs;
+
+    fun get () = CS_DATA (!claset);
+in add_thydata "HOL"
+     ("claset", ThyMethods {merge = merge, put = put, get = get})
+end;
+
+claset := HOL_cs;
+
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/ex/LList.ML
--- a/src/HOL/ex/LList.ML	Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/ex/LList.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -362,10 +362,10 @@
 by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1));
 qed "LCons_not_LNil";
 
-bind_thm ("LNil_not_LCons", (LCons_not_LNil RS not_sym));
+bind_thm ("LNil_not_LCons", LCons_not_LNil RS not_sym);
 
-bind_thm ("LCons_neq_LNil", (LCons_not_LNil RS notE));
-val LNil_neq_LCons = sym RS LCons_neq_LNil;
+AddIffs [LCons_not_LNil, LNil_not_LCons];
+
 
 (** llist constructors **)
 
@@ -392,14 +392,14 @@
 (*For reasoning about abstract llist constructors*)
 
 AddIs ([Rep_llist]@llist.intrs);
-AddSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject];
 AddSDs [inj_onto_Abs_llist RS inj_ontoD,
-                              inj_Rep_llist RS injD, Leaf_inject];
+	inj_Rep_llist RS injD, Leaf_inject];
 
 goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
 by (Fast_tac 1);
 qed "LCons_LCons_eq";
-bind_thm ("LCons_inject", (LCons_LCons_eq RS iffD1 RS conjE));
+
+AddIffs [LCons_LCons_eq];
 
 val [major] = goal LList.thy "CONS M N: llist(A) ==> M: A & N: llist(A)";
 by (rtac (major RS llist.elim) 1);
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/ex/SList.ML
--- a/src/HOL/ex/SList.ML	Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/ex/SList.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -74,10 +74,7 @@
 by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1));
 qed "Cons_not_Nil";
 
-bind_thm ("Nil_not_Cons", (Cons_not_Nil RS not_sym));
-
-bind_thm ("Cons_neq_Nil2", (Cons_not_Nil RS notE));
-val Nil_neq_Cons = sym RS Cons_neq_Nil2;
+bind_thm ("Nil_not_Cons", Cons_not_Nil RS not_sym);
 
 (** Injectiveness of CONS and Cons **)
 
@@ -85,11 +82,11 @@
 by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
 qed "CONS_CONS_eq";
 
-bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
-
 (*For reasoning about abstract list constructors*)
 AddIs ([Rep_list] @ list.intrs);
-AddSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject];
+
+AddIffs [CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq];
+
 AddSDs [inj_onto_Abs_list RS inj_ontoD,
         inj_Rep_list RS injD, Leaf_inject];
 
@@ -111,9 +108,10 @@
 qed "sexp_CONS_D";
 
 
-(*Basic ss with constructors and their freeness*)
-Addsimps ([Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq, CONS_not_NIL,
-           NIL_not_CONS, CONS_CONS_eq] @ list.intrs);
+(*Reasoning about constructors and their freeness*)
+Addsimps list.intrs;
+
+AddIffs [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq];
 
 goal SList.thy "!!N. N: list(A) ==> !M. N ~= CONS M N";
 by (etac list.induct 1);
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/ex/Simult.ML
--- a/src/HOL/ex/Simult.ML	Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/ex/Simult.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -64,7 +64,7 @@
 
 AddSIs [PartI];
 AddSDs [In0_inject, In1_inject];
-AddSEs [In0_neq_In1, In1_neq_In0, PartE];
+AddSEs [PartE];
 
 (*Could prove  ~ TCONS M N : Part (TF A) In1  etc. *)
 
diff -r 5cf82dc3ce67 -r 84cf16192e03 src/HOL/indrule.ML
--- a/src/HOL/indrule.ML	Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/indrule.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -165,7 +165,7 @@
 
 (*Simplification largely reduces the mutual induction rule to the 
   standard rule*)
-val mut_ss = min_ss addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq, split];
+val mut_ss = min_ss addsimps [Inl_not_Inr, Inr_not_Inl, Inl_eq, Inr_eq, split];
 
 val all_defs = [split RS eq_reflection] @ Inductive.con_defs @ part_rec_defs;