# 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 = 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 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 m m Suc(m) < Suc(n)"; -by (subgoal_tac "m Suc(m) < Suc(n)" 1); -by (fast_tac (!claset addIs prems) 1); +goal Nat.thy "!!m n. m 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;