Tidied many proofs, using AddIffs to let equivalences take
the place of separate Intr and Elim rules. Also deleted most named clasets.
--- /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!*)
--- /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
--- 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";
--- 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);
--- 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);
--- 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];
--- 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];
--- 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;
--- 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 ***)
--- 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]
--- 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];
-
--- 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];
--- /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;
+
--- 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);
--- 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);
--- 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. *)
--- 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;