# HG changeset patch # User wenzelm # Date 1164581033 -3600 # Node ID c5cf9243ad625ecc4179477471866cc192134388 # Parent 678299eac351f0b87db06e4e8e8b56218998a67d converted legacy ML scripts; diff -r 678299eac351 -r c5cf9243ad62 src/FOL/FOL.ML --- a/src/FOL/FOL.ML Sun Nov 26 23:09:25 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ - -structure FOL = -struct - val thy = the_context (); - val classical = classical; -end; diff -r 678299eac351 -r c5cf9243ad62 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Sun Nov 26 23:09:25 2006 +0100 +++ b/src/FOL/FOL.thy Sun Nov 26 23:43:53 2006 +0100 @@ -7,7 +7,7 @@ theory FOL imports IFOL -uses ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") +uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") begin @@ -19,8 +19,151 @@ subsection {* Lemmas and proof tools *} -use "FOL_lemmas1.ML" -theorems case_split = case_split_thm [case_names True False, cases type: o] +lemma ccontr: "(\ P \ False) \ P" + by (erule FalseE [THEN classical]) + +(*** Classical introduction rules for | and EX ***) + +lemma disjCI: "(~Q ==> P) ==> P|Q" + apply (rule classical) + apply (assumption | erule meta_mp | rule disjI1 notI)+ + apply (erule notE disjI2)+ + done + +(*introduction rule involving only EX*) +lemma ex_classical: + assumes r: "~(EX x. P(x)) ==> P(a)" + shows "EX x. P(x)" + apply (rule classical) + apply (rule exI, erule r) + done + +(*version of above, simplifying ~EX to ALL~ *) +lemma exCI: + assumes r: "ALL x. ~P(x) ==> P(a)" + shows "EX x. P(x)" + apply (rule ex_classical) + apply (rule notI [THEN allI, THEN r]) + apply (erule notE) + apply (erule exI) + done + +lemma excluded_middle: "~P | P" + apply (rule disjCI) + apply assumption + done + +(*For disjunctive case analysis*) +ML {* + local + val excluded_middle = thm "excluded_middle" + val disjE = thm "disjE" + in + fun excluded_middle_tac sP = + res_inst_tac [("Q",sP)] (excluded_middle RS disjE) + end +*} + +lemma case_split_thm: + assumes r1: "P ==> Q" + and r2: "~P ==> Q" + shows Q + apply (rule excluded_middle [THEN disjE]) + apply (erule r2) + apply (erule r1) + done + +lemmas case_split = case_split_thm [case_names True False, cases type: o] + +(*HOL's more natural case analysis tactic*) +ML {* + local + val case_split_thm = thm "case_split_thm" + in + fun case_tac a = res_inst_tac [("P",a)] case_split_thm + end +*} + + +(*** Special elimination rules *) + + +(*Classical implies (-->) elimination. *) +lemma impCE: + assumes major: "P-->Q" + and r1: "~P ==> R" + and r2: "Q ==> R" + shows R + apply (rule excluded_middle [THEN disjE]) + apply (erule r1) + apply (rule r2) + apply (erule major [THEN mp]) + done + +(*This version of --> elimination works on Q before P. It works best for + those cases in which P holds "almost everywhere". Can't install as + default: would break old proofs.*) +lemma impCE': + assumes major: "P-->Q" + and r1: "Q ==> R" + and r2: "~P ==> R" + shows R + apply (rule excluded_middle [THEN disjE]) + apply (erule r2) + apply (rule r1) + apply (erule major [THEN mp]) + done + +(*Double negation law*) +lemma notnotD: "~~P ==> P" + apply (rule classical) + apply (erule notE) + apply assumption + done + +lemma contrapos2: "[| Q; ~ P ==> ~ Q |] ==> P" + apply (rule classical) + apply (drule (1) meta_mp) + apply (erule (1) notE) + done + +(*** Tactics for implication and contradiction ***) + +(*Classical <-> elimination. Proof substitutes P=Q in + ~P ==> ~Q and P ==> Q *) +lemma iffCE: + assumes major: "P<->Q" + and r1: "[| P; Q |] ==> R" + and r2: "[| ~P; ~Q |] ==> R" + shows R + apply (rule major [unfolded iff_def, THEN conjE]) + apply (elim impCE) + apply (erule (1) r2) + apply (erule (1) notE)+ + apply (erule (1) r1) + done + + +(*Better for fast_tac: needs no quantifier duplication!*) +lemma alt_ex1E: + assumes major: "EX! x. P(x)" + and r: "!!x. [| P(x); ALL y y'. P(y) & P(y') --> y=y' |] ==> R" + shows R + using major +proof (rule ex1E) + fix x + assume * : "\y. P(y) \ y = x" + assume "P(x)" + then show R + proof (rule r) + { fix y y' + assume "P(y)" and "P(y')" + with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac 1")+ + then have "y = y'" by (rule subst) + } note r' = this + show "\y y'. P(y) \ P(y') \ y = y'" by (intro strip, elim conjE) (rule r') + qed +qed use "cladata.ML" setup Cla.setup @@ -32,9 +175,7 @@ lemma ex1_functional: "[| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c" -by blast - -ML {* val ex1_functional = thm "ex1_functional" *} + by blast (* Elimination of True from asumptions: *) lemma True_implies_equals: "(True ==> PROP P) == PROP P" @@ -46,6 +187,19 @@ then show "PROP P" . qed +lemma uncurry: "P --> Q --> R ==> P & Q --> R" + by blast + +lemma iff_allI: "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))" + by blast + +lemma iff_exI: "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))" + by blast + +lemma all_comm: "(ALL x y. P(x,y)) <-> (ALL y x. P(x,y))" by blast + +lemma ex_comm: "(EX x y. P(x,y)) <-> (EX y x. P(x,y))" by blast + use "simpdata.ML" setup simpsetup setup "Simplifier.method_setup Splitter.split_modifiers" diff -r 678299eac351 -r c5cf9243ad62 src/FOL/FOL_lemmas1.ML --- a/src/FOL/FOL_lemmas1.ML Sun Nov 26 23:09:25 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,95 +0,0 @@ -(* Title: FOL/FOL_lemmas1.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge - -Tactics and lemmas for theory FOL (classical First-Order Logic). -*) - -val classical = thm "classical"; -bind_thm ("ccontr", FalseE RS classical); - - -(*** Classical introduction rules for | and EX ***) - -val prems = Goal "(~Q ==> P) ==> P|Q"; -by (rtac classical 1); -by (REPEAT (ares_tac (prems@[disjI1,notI]) 1)); -by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ; -qed "disjCI"; - -(*introduction rule involving only EX*) -val prems = Goal "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)"; -by (rtac classical 1); -by (eresolve_tac (prems RL [exI]) 1) ; -qed "ex_classical"; - -(*version of above, simplifying ~EX to ALL~ *) -val [prem]= Goal "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"; -by (rtac ex_classical 1); -by (resolve_tac [notI RS allI RS prem] 1); -by (etac notE 1); -by (etac exI 1) ; -qed "exCI"; - -Goal"~P | P"; -by (rtac disjCI 1); -by (assume_tac 1) ; -qed "excluded_middle"; - -(*For disjunctive case analysis*) -fun excluded_middle_tac sP = - res_inst_tac [("Q",sP)] (excluded_middle RS disjE); - -val [p1,p2] = Goal"[| P ==> Q; ~P ==> Q |] ==> Q"; -by (rtac (excluded_middle RS disjE) 1); -by (etac p2 1); -by (etac p1 1); -qed "case_split_thm"; - -(*HOL's more natural case analysis tactic*) -fun case_tac a = res_inst_tac [("P",a)] case_split_thm; - - -(*** Special elimination rules *) - - -(*Classical implies (-->) elimination. *) -val major::prems = Goal "[| P-->Q; ~P ==> R; Q ==> R |] ==> R"; -by (resolve_tac [excluded_middle RS disjE] 1); -by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ; -qed "impCE"; - -(*This version of --> elimination works on Q before P. It works best for - those cases in which P holds "almost everywhere". Can't install as - default: would break old proofs.*) -val major::prems = Goal "[| P-->Q; Q ==> R; ~P ==> R |] ==> R"; -by (resolve_tac [excluded_middle RS disjE] 1); -by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ; -qed "impCE'"; - -(*Double negation law*) -Goal"~~P ==> P"; -by (rtac classical 1); -by (etac notE 1); -by (assume_tac 1); -qed "notnotD"; - -val [p1,p2] = Goal"[| Q; ~ P ==> ~ Q |] ==> P"; -by (rtac classical 1); -by (dtac p2 1); -by (etac notE 1); -by (rtac p1 1); -qed "contrapos2"; - -(*** Tactics for implication and contradiction ***) - -(*Classical <-> elimination. Proof substitutes P=Q in - ~P ==> ~Q and P ==> Q *) -val major::prems = -Goalw [iff_def] "[| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R"; -by (rtac (major RS conjE) 1); -by (REPEAT_FIRST (etac impCE)); -by (REPEAT (DEPTH_SOLVE_1 (mp_tac 1 ORELSE ares_tac prems 1))); -qed "iffCE"; - diff -r 678299eac351 -r c5cf9243ad62 src/FOL/IFOL.ML --- a/src/FOL/IFOL.ML Sun Nov 26 23:09:25 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,26 +0,0 @@ - -structure IFOL = -struct - val thy = the_context (); - val refl = refl; - val subst = subst; - val conjI = conjI; - val conjunct1 = conjunct1; - val conjunct2 = conjunct2; - val disjI1 = disjI1; - val disjI2 = disjI2; - val disjE = disjE; - val impI = impI; - val mp = mp; - val FalseE = FalseE; - val True_def = True_def; - val not_def = not_def; - val iff_def = iff_def; - val ex1_def = ex1_def; - val allI = allI; - val spec = spec; - val exI = exI; - val exE = exE; - val eq_reflection = eq_reflection; - val iff_reflection = iff_reflection; -end; diff -r 678299eac351 -r c5cf9243ad62 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Sun Nov 26 23:09:25 2006 +0100 +++ b/src/FOL/IFOL.thy Sun Nov 26 23:43:53 2006 +0100 @@ -7,7 +7,7 @@ theory IFOL imports Pure -uses ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML") +uses ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML") begin @@ -55,22 +55,22 @@ not_equal (infixl "\" 50) notation (xsymbols) - Not ("\ _" [40] 40) and - "op &" (infixr "\" 35) and - "op |" (infixr "\" 30) and - All (binder "\" 10) and - Ex (binder "\" 10) and - Ex1 (binder "\!" 10) and + Not ("\ _" [40] 40) and + "op &" (infixr "\" 35) and + "op |" (infixr "\" 30) and + All (binder "\" 10) and + Ex (binder "\" 10) and + Ex1 (binder "\!" 10) and "op -->" (infixr "\" 25) and "op <->" (infixr "\" 25) notation (HTML output) - Not ("\ _" [40] 40) and - "op &" (infixr "\" 35) and - "op |" (infixr "\" 30) and - All (binder "\" 10) and - Ex (binder "\" 10) and - Ex1 (binder "\!" 10) + Not ("\ _" [40] 40) and + "op &" (infixr "\" 35) and + "op |" (infixr "\" 30) and + All (binder "\" 10) and + Ex (binder "\" 10) and + Ex1 (binder "\!" 10) local @@ -145,7 +145,471 @@ subsection {* Lemmas and proof tools *} -use "IFOL_lemmas.ML" +lemma TrueI: True + unfolding True_def by (rule impI) + + +(*** Sequent-style elimination rules for & --> and ALL ***) + +lemma conjE: + assumes major: "P & Q" + and r: "[| P; Q |] ==> R" + shows R + apply (rule r) + apply (rule major [THEN conjunct1]) + apply (rule major [THEN conjunct2]) + done + +lemma impE: + assumes major: "P --> Q" + and P + and r: "Q ==> R" + shows R + apply (rule r) + apply (rule major [THEN mp]) + apply (rule `P`) + done + +lemma allE: + assumes major: "ALL x. P(x)" + and r: "P(x) ==> R" + shows R + apply (rule r) + apply (rule major [THEN spec]) + done + +(*Duplicates the quantifier; for use with eresolve_tac*) +lemma all_dupE: + assumes major: "ALL x. P(x)" + and r: "[| P(x); ALL x. P(x) |] ==> R" + shows R + apply (rule r) + apply (rule major [THEN spec]) + apply (rule major) + done + + +(*** Negation rules, which translate between ~P and P-->False ***) + +lemma notI: "(P ==> False) ==> ~P" + unfolding not_def by (erule impI) + +lemma notE: "[| ~P; P |] ==> R" + unfolding not_def by (erule mp [THEN FalseE]) + +lemma rev_notE: "[| P; ~P |] ==> R" + by (erule notE) + +(*This is useful with the special implication rules for each kind of P. *) +lemma not_to_imp: + assumes "~P" + and r: "P --> False ==> Q" + shows Q + apply (rule r) + apply (rule impI) + apply (erule notE [OF `~P`]) + done + +(* For substitution into an assumption P, reduce Q to P-->Q, substitute into + this implication, then apply impI to move P back into the assumptions. + To specify P use something like + eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *) +lemma rev_mp: "[| P; P --> Q |] ==> Q" + by (erule mp) + +(*Contrapositive of an inference rule*) +lemma contrapos: + assumes major: "~Q" + and minor: "P ==> Q" + shows "~P" + apply (rule major [THEN notE, THEN notI]) + apply (erule minor) + done + + +(*** Modus Ponens Tactics ***) + +(*Finds P-->Q and P in the assumptions, replaces implication by Q *) +ML {* + local + val notE = thm "notE" + val impE = thm "impE" + in + fun mp_tac i = eresolve_tac [notE,impE] i THEN assume_tac i + fun eq_mp_tac i = eresolve_tac [notE,impE] i THEN eq_assume_tac i + end +*} + + +(*** If-and-only-if ***) + +lemma iffI: "[| P ==> Q; Q ==> P |] ==> P<->Q" + apply (unfold iff_def) + apply (rule conjI) + apply (erule impI) + apply (erule impI) + done + + +(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) +lemma iffE: + assumes major: "P <-> Q" + and r: "P-->Q ==> Q-->P ==> R" + shows R + apply (insert major, unfold iff_def) + apply (erule conjE) + apply (erule r) + apply assumption + done + +(* Destruct rules for <-> similar to Modus Ponens *) + +lemma iffD1: "[| P <-> Q; P |] ==> Q" + apply (unfold iff_def) + apply (erule conjunct1 [THEN mp]) + apply assumption + done + +lemma iffD2: "[| P <-> Q; Q |] ==> P" + apply (unfold iff_def) + apply (erule conjunct2 [THEN mp]) + apply assumption + done + +lemma rev_iffD1: "[| P; P <-> Q |] ==> Q" + apply (erule iffD1) + apply assumption + done + +lemma rev_iffD2: "[| Q; P <-> Q |] ==> P" + apply (erule iffD2) + apply assumption + done + +lemma iff_refl: "P <-> P" + by (rule iffI) + +lemma iff_sym: "Q <-> P ==> P <-> Q" + apply (erule iffE) + apply (rule iffI) + apply (assumption | erule mp)+ + done + +lemma iff_trans: "[| P <-> Q; Q<-> R |] ==> P <-> R" + apply (rule iffI) + apply (assumption | erule iffE | erule (1) notE impE)+ + done + + +(*** Unique existence. NOTE THAT the following 2 quantifications + EX!x such that [EX!y such that P(x,y)] (sequential) + EX!x,y such that P(x,y) (simultaneous) + do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. +***) + +lemma ex1I: + assumes "P(a)" + and "!!x. P(x) ==> x=a" + shows "EX! x. P(x)" + apply (unfold ex1_def) + apply (assumption | rule assms exI conjI allI impI)+ + done + +(*Sometimes easier to use: the premises have no shared variables. Safe!*) +lemma ex_ex1I: + assumes ex: "EX x. P(x)" + and eq: "!!x y. [| P(x); P(y) |] ==> x=y" + shows "EX! x. P(x)" + apply (rule ex [THEN exE]) + apply (assumption | rule ex1I eq)+ + done + +lemma ex1E: + assumes ex1: "EX! x. P(x)" + and r: "!!x. [| P(x); ALL y. P(y) --> y=x |] ==> R" + shows R + apply (insert ex1, unfold ex1_def) + apply (assumption | erule exE conjE)+ + done + + +(*** <-> congruence rules for simplification ***) + +(*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*) +ML {* + local + val iffE = thm "iffE" + val mp = thm "mp" + in + fun iff_tac prems i = + resolve_tac (prems RL [iffE]) i THEN + REPEAT1 (eresolve_tac [asm_rl, mp] i) + end +*} + +lemma conj_cong: + assumes "P <-> P'" + and "P' ==> Q <-> Q'" + shows "(P&Q) <-> (P'&Q')" + apply (insert assms) + apply (assumption | rule iffI conjI | erule iffE conjE mp | + tactic {* iff_tac (thms "assms") 1 *})+ + done + +(*Reversed congruence rule! Used in ZF/Order*) +lemma conj_cong2: + assumes "P <-> P'" + and "P' ==> Q <-> Q'" + shows "(Q&P) <-> (Q'&P')" + apply (insert assms) + apply (assumption | rule iffI conjI | erule iffE conjE mp | + tactic {* iff_tac (thms "assms") 1 *})+ + done + +lemma disj_cong: + assumes "P <-> P'" and "Q <-> Q'" + shows "(P|Q) <-> (P'|Q')" + apply (insert assms) + apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | erule (1) notE impE)+ + done + +lemma imp_cong: + assumes "P <-> P'" + and "P' ==> Q <-> Q'" + shows "(P-->Q) <-> (P'-->Q')" + apply (insert assms) + apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | + tactic {* iff_tac (thms "assms") 1 *})+ + done + +lemma iff_cong: "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')" + apply (erule iffE | assumption | rule iffI | erule (1) notE impE)+ + done + +lemma not_cong: "P <-> P' ==> ~P <-> ~P'" + apply (assumption | rule iffI notI | erule (1) notE impE | erule iffE notE)+ + done + +lemma all_cong: + assumes "!!x. P(x) <-> Q(x)" + shows "(ALL x. P(x)) <-> (ALL x. Q(x))" + apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | + tactic {* iff_tac (thms "assms") 1 *})+ + done + +lemma ex_cong: + assumes "!!x. P(x) <-> Q(x)" + shows "(EX x. P(x)) <-> (EX x. Q(x))" + apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | + tactic {* iff_tac (thms "assms") 1 *})+ + done + +lemma ex1_cong: + assumes "!!x. P(x) <-> Q(x)" + shows "(EX! x. P(x)) <-> (EX! x. Q(x))" + apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | + tactic {* iff_tac (thms "assms") 1 *})+ + done + +(*** Equality rules ***) + +lemma sym: "a=b ==> b=a" + apply (erule subst) + apply (rule refl) + done + +lemma trans: "[| a=b; b=c |] ==> a=c" + apply (erule subst, assumption) + done + +(** **) +lemma not_sym: "b ~= a ==> a ~= b" + apply (erule contrapos) + apply (erule sym) + done + +(* Two theorms for rewriting only one instance of a definition: + the first for definitions of formulae and the second for terms *) + +lemma def_imp_iff: "(A == B) ==> A <-> B" + apply unfold + apply (rule iff_refl) + done + +lemma meta_eq_to_obj_eq: "(A == B) ==> A = B" + apply unfold + apply (rule refl) + done + +lemma meta_eq_to_iff: "x==y ==> x<->y" + by unfold (rule iff_refl) + +(*substitution*) +lemma ssubst: "[| b = a; P(a) |] ==> P(b)" + apply (drule sym) + apply (erule (1) subst) + done + +(*A special case of ex1E that would otherwise need quantifier expansion*) +lemma ex1_equalsE: + "[| EX! x. P(x); P(a); P(b) |] ==> a=b" + apply (erule ex1E) + apply (rule trans) + apply (rule_tac [2] sym) + apply (assumption | erule spec [THEN mp])+ + done + +(** Polymorphic congruence rules **) + +lemma subst_context: "[| a=b |] ==> t(a)=t(b)" + apply (erule ssubst) + apply (rule refl) + done + +lemma subst_context2: "[| a=b; c=d |] ==> t(a,c)=t(b,d)" + apply (erule ssubst)+ + apply (rule refl) + done + +lemma subst_context3: "[| a=b; c=d; e=f |] ==> t(a,c,e)=t(b,d,f)" + apply (erule ssubst)+ + apply (rule refl) + done + +(*Useful with eresolve_tac for proving equalties from known equalities. + a = b + | | + c = d *) +lemma box_equals: "[| a=b; a=c; b=d |] ==> c=d" + apply (rule trans) + apply (rule trans) + apply (rule sym) + apply assumption+ + done + +(*Dual of box_equals: for proving equalities backwards*) +lemma simp_equals: "[| a=c; b=d; c=d |] ==> a=b" + apply (rule trans) + apply (rule trans) + apply assumption+ + apply (erule sym) + done + +(** Congruence rules for predicate letters **) + +lemma pred1_cong: "a=a' ==> P(a) <-> P(a')" + apply (rule iffI) + apply (erule (1) subst) + apply (erule (1) ssubst) + done + +lemma pred2_cong: "[| a=a'; b=b' |] ==> P(a,b) <-> P(a',b')" + apply (rule iffI) + apply (erule subst)+ + apply assumption + apply (erule ssubst)+ + apply assumption + done + +lemma pred3_cong: "[| a=a'; b=b'; c=c' |] ==> P(a,b,c) <-> P(a',b',c')" + apply (rule iffI) + apply (erule subst)+ + apply assumption + apply (erule ssubst)+ + apply assumption + done + +(*special cases for free variables P, Q, R, S -- up to 3 arguments*) + +ML {* +bind_thms ("pred_congs", + List.concat (map (fn c => + map (fn th => read_instantiate [("P",c)] th) + [thm "pred1_cong", thm "pred2_cong", thm "pred3_cong"]) + (explode"PQRS"))) +*} + +(*special case for the equality predicate!*) +lemma eq_cong: "[| a = a'; b = b' |] ==> a = b <-> a' = b'" + apply (erule (1) pred2_cong) + done + + +(*** Simplifications of assumed implications. + Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE + used with mp_tac (restricted to atomic formulae) is COMPLETE for + intuitionistic propositional logic. See + R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic + (preprint, University of St Andrews, 1991) ***) + +lemma conj_impE: + assumes major: "(P&Q)-->S" + and r: "P-->(Q-->S) ==> R" + shows R + by (assumption | rule conjI impI major [THEN mp] r)+ + +lemma disj_impE: + assumes major: "(P|Q)-->S" + and r: "[| P-->S; Q-->S |] ==> R" + shows R + by (assumption | rule disjI1 disjI2 impI major [THEN mp] r)+ + +(*Simplifies the implication. Classical version is stronger. + Still UNSAFE since Q must be provable -- backtracking needed. *) +lemma imp_impE: + assumes major: "(P-->Q)-->S" + and r1: "[| P; Q-->S |] ==> Q" + and r2: "S ==> R" + shows R + by (assumption | rule impI major [THEN mp] r1 r2)+ + +(*Simplifies the implication. Classical version is stronger. + Still UNSAFE since ~P must be provable -- backtracking needed. *) +lemma not_impE: + assumes major: "~P --> S" + and r1: "P ==> False" + and r2: "S ==> R" + shows R + apply (assumption | rule notI impI major [THEN mp] r1 r2)+ + done + +(*Simplifies the implication. UNSAFE. *) +lemma iff_impE: + assumes major: "(P<->Q)-->S" + and r1: "[| P; Q-->S |] ==> Q" + and r2: "[| Q; P-->S |] ==> P" + and r3: "S ==> R" + shows R + apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+ + done + +(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) +lemma all_impE: + assumes major: "(ALL x. P(x))-->S" + and r1: "!!x. P(x)" + and r2: "S ==> R" + shows R + apply (assumption | rule allI impI major [THEN mp] r1 r2)+ + done + +(*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) +lemma ex_impE: + assumes major: "(EX x. P(x))-->S" + and r: "P(x)-->S ==> R" + shows R + apply (assumption | rule exI impI major [THEN mp] r)+ + done + +(*** Courtesy of Krzysztof Grabczewski ***) + +lemma disj_imp_disj: + assumes major: "P|Q" + and "P==>R" and "Q==>S" + shows "R|S" + apply (rule disjE [OF major]) + apply (rule disjI1) apply assumption + apply (rule disjI2) apply assumption + done ML {* structure ProjectRule = ProjectRuleFun @@ -157,6 +621,9 @@ *} use "fologic.ML" + +lemma thin_refl: "!!X. [|x=x; PROP W|] ==> PROP W" . + use "hypsubstdata.ML" setup hypsubst_setup use "intprover.ML" @@ -314,16 +781,51 @@ lemma LetI: - assumes prem: "(!!x. x=t ==> P(u(x)))" - shows "P(let x=t in u(x))" -apply (unfold Let_def) -apply (rule refl [THEN prem]) -done + assumes "!!x. x=t ==> P(u(x))" + shows "P(let x=t in u(x))" + apply (unfold Let_def) + apply (rule refl [THEN assms]) + done + + +subsection {* ML bindings *} -ML -{* -val Let_def = thm "Let_def"; -val LetI = thm "LetI"; +ML {* +val refl = thm "refl" +val trans = thm "trans" +val sym = thm "sym" +val subst = thm "subst" +val ssubst = thm "ssubst" +val conjI = thm "conjI" +val conjE = thm "conjE" +val conjunct1 = thm "conjunct1" +val conjunct2 = thm "conjunct2" +val disjI1 = thm "disjI1" +val disjI2 = thm "disjI2" +val disjE = thm "disjE" +val impI = thm "impI" +val impE = thm "impE" +val mp = thm "mp" +val rev_mp = thm "rev_mp" +val TrueI = thm "TrueI" +val FalseE = thm "FalseE" +val iff_refl = thm "iff_refl" +val iff_trans = thm "iff_trans" +val iffI = thm "iffI" +val iffE = thm "iffE" +val iffD1 = thm "iffD1" +val iffD2 = thm "iffD2" +val notI = thm "notI" +val notE = thm "notE" +val allI = thm "allI" +val allE = thm "allE" +val spec = thm "spec" +val exI = thm "exI" +val exE = thm "exE" +val eq_reflection = thm "eq_reflection" +val iff_reflection = thm "iff_reflection" +val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq" +val meta_eq_to_iff = thm "meta_eq_to_iff" *} end diff -r 678299eac351 -r c5cf9243ad62 src/FOL/IFOL_lemmas.ML --- a/src/FOL/IFOL_lemmas.ML Sun Nov 26 23:09:25 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,451 +0,0 @@ -(* Title: FOL/IFOL_lemmas.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - -Tactics and lemmas for theory IFOL (intuitionistic first-order logic). -*) - -(* ML bindings *) - -val refl = thm "refl"; -val subst = thm "subst"; -val conjI = thm "conjI"; -val conjunct1 = thm "conjunct1"; -val conjunct2 = thm "conjunct2"; -val disjI1 = thm "disjI1"; -val disjI2 = thm "disjI2"; -val disjE = thm "disjE"; -val impI = thm "impI"; -val mp = thm "mp"; -val FalseE = thm "FalseE"; -val True_def = thm "True_def"; -val not_def = thm "not_def"; -val iff_def = thm "iff_def"; -val ex1_def = thm "ex1_def"; -val allI = thm "allI"; -val spec = thm "spec"; -val exI = thm "exI"; -val exE = thm "exE"; -val eq_reflection = thm "eq_reflection"; -val iff_reflection = thm "iff_reflection"; - -structure IFOL = -struct - val thy = the_context (); - val refl = refl; - val subst = subst; - val conjI = conjI; - val conjunct1 = conjunct1; - val conjunct2 = conjunct2; - val disjI1 = disjI1; - val disjI2 = disjI2; - val disjE = disjE; - val impI = impI; - val mp = mp; - val FalseE = FalseE; - val True_def = True_def; - val not_def = not_def; - val iff_def = iff_def; - val ex1_def = ex1_def; - val allI = allI; - val spec = spec; - val exI = exI; - val exE = exE; - val eq_reflection = eq_reflection; - val iff_reflection = iff_reflection; -end; - - -Goalw [True_def] "True"; -by (REPEAT (ares_tac [impI] 1)) ; -qed "TrueI"; - -(*** Sequent-style elimination rules for & --> and ALL ***) - -val major::prems = Goal - "[| P&Q; [| P; Q |] ==> R |] ==> R"; -by (resolve_tac prems 1); -by (rtac (major RS conjunct1) 1); -by (rtac (major RS conjunct2) 1); -qed "conjE"; - -val major::prems = Goal - "[| P-->Q; P; Q ==> R |] ==> R"; -by (resolve_tac prems 1); -by (rtac (major RS mp) 1); -by (resolve_tac prems 1); -qed "impE"; - -val major::prems = Goal - "[| ALL x. P(x); P(x) ==> R |] ==> R"; -by (resolve_tac prems 1); -by (rtac (major RS spec) 1); -qed "allE"; - -(*Duplicates the quantifier; for use with eresolve_tac*) -val major::prems = Goal - "[| ALL x. P(x); [| P(x); ALL x. P(x) |] ==> R \ -\ |] ==> R"; -by (resolve_tac prems 1); -by (rtac (major RS spec) 1); -by (rtac major 1); -qed "all_dupE"; - - -(*** Negation rules, which translate between ~P and P-->False ***) - -val prems = Goalw [not_def] "(P ==> False) ==> ~P"; -by (REPEAT (ares_tac (prems@[impI]) 1)) ; -qed "notI"; - -Goalw [not_def] "[| ~P; P |] ==> R"; -by (etac (mp RS FalseE) 1); -by (assume_tac 1); -qed "notE"; - -Goal "[| P; ~P |] ==> R"; -by (etac notE 1); -by (assume_tac 1); -qed "rev_notE"; - -(*This is useful with the special implication rules for each kind of P. *) -val prems = Goal - "[| ~P; (P-->False) ==> Q |] ==> Q"; -by (REPEAT (ares_tac (prems@[impI,notE]) 1)) ; -qed "not_to_imp"; - -(* For substitution into an assumption P, reduce Q to P-->Q, substitute into - this implication, then apply impI to move P back into the assumptions. - To specify P use something like - eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *) -Goal "[| P; P --> Q |] ==> Q"; -by (etac mp 1); -by (assume_tac 1); -qed "rev_mp"; - -(*Contrapositive of an inference rule*) -val [major,minor]= Goal "[| ~Q; P==>Q |] ==> ~P"; -by (rtac (major RS notE RS notI) 1); -by (etac minor 1) ; -qed "contrapos"; - - -(*** Modus Ponens Tactics ***) - -(*Finds P-->Q and P in the assumptions, replaces implication by Q *) -fun mp_tac i = eresolve_tac [notE,impE] i THEN assume_tac i; - -(*Like mp_tac but instantiates no variables*) -fun eq_mp_tac i = eresolve_tac [notE,impE] i THEN eq_assume_tac i; - - -(*** If-and-only-if ***) - -val prems = Goalw [iff_def] - "[| P ==> Q; Q ==> P |] ==> P<->Q"; -by (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ; -qed "iffI"; - - -(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) -val prems = Goalw [iff_def] - "[| P <-> Q; [| P-->Q; Q-->P |] ==> R |] ==> R"; -by (rtac conjE 1); -by (REPEAT (ares_tac prems 1)) ; -qed "iffE"; - -(* Destruct rules for <-> similar to Modus Ponens *) - -Goalw [iff_def] "[| P <-> Q; P |] ==> Q"; -by (etac (conjunct1 RS mp) 1); -by (assume_tac 1); -qed "iffD1"; - -val prems = Goalw [iff_def] "[| P <-> Q; Q |] ==> P"; -by (etac (conjunct2 RS mp) 1); -by (assume_tac 1); -qed "iffD2"; - -Goal "[| P; P <-> Q |] ==> Q"; -by (etac iffD1 1); -by (assume_tac 1); -qed "rev_iffD1"; - -Goal "[| Q; P <-> Q |] ==> P"; -by (etac iffD2 1); -by (assume_tac 1); -qed "rev_iffD2"; - -Goal "P <-> P"; -by (REPEAT (ares_tac [iffI] 1)) ; -qed "iff_refl"; - -Goal "Q <-> P ==> P <-> Q"; -by (etac iffE 1); -by (rtac iffI 1); -by (REPEAT (eresolve_tac [asm_rl,mp] 1)) ; -qed "iff_sym"; - -Goal "[| P <-> Q; Q<-> R |] ==> P <-> R"; -by (rtac iffI 1); -by (REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ; -qed "iff_trans"; - - -(*** Unique existence. NOTE THAT the following 2 quantifications - EX!x such that [EX!y such that P(x,y)] (sequential) - EX!x,y such that P(x,y) (simultaneous) - do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. -***) - -val prems = Goalw [ex1_def] - "[| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x)"; -by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ; -qed "ex1I"; - -(*Sometimes easier to use: the premises have no shared variables. Safe!*) -val [ex,eq] = Goal - "[| EX x. P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"; -by (rtac (ex RS exE) 1); -by (REPEAT (ares_tac [ex1I,eq] 1)) ; -qed "ex_ex1I"; - -val prems = Goalw [ex1_def] - "[| EX! x. P(x); !!x. [| P(x); ALL y. P(y) --> y=x |] ==> R |] ==> R"; -by (cut_facts_tac prems 1); -by (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ; -qed "ex1E"; - - -(*** <-> congruence rules for simplification ***) - -(*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*) -fun iff_tac prems i = - resolve_tac (prems RL [iffE]) i THEN - REPEAT1 (eresolve_tac [asm_rl,mp] i); - -val prems = Goal - "[| P <-> P'; P' ==> Q <-> Q' |] ==> (P&Q) <-> (P'&Q')"; -by (cut_facts_tac prems 1); -by (REPEAT (ares_tac [iffI,conjI] 1 - ORELSE eresolve_tac [iffE,conjE,mp] 1 - ORELSE iff_tac prems 1)) ; -qed "conj_cong"; - -(*Reversed congruence rule! Used in ZF/Order*) -val prems = Goal - "[| P <-> P'; P' ==> Q <-> Q' |] ==> (Q&P) <-> (Q'&P')"; -by (cut_facts_tac prems 1); -by (REPEAT (ares_tac [iffI,conjI] 1 - ORELSE eresolve_tac [iffE,conjE,mp] 1 ORELSE iff_tac prems 1)) ; -qed "conj_cong2"; - -val prems = Goal - "[| P <-> P'; Q <-> Q' |] ==> (P|Q) <-> (P'|Q')"; -by (cut_facts_tac prems 1); -by (REPEAT (eresolve_tac [iffE,disjE,disjI1,disjI2] 1 - ORELSE ares_tac [iffI] 1 ORELSE mp_tac 1)) ; -qed "disj_cong"; - -val prems = Goal - "[| P <-> P'; P' ==> Q <-> Q' |] ==> (P-->Q) <-> (P'-->Q')"; -by (cut_facts_tac prems 1); -by (REPEAT (ares_tac [iffI,impI] 1 - ORELSE etac iffE 1 ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ; -qed "imp_cong"; - -val prems = Goal - "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"; -by (cut_facts_tac prems 1); -by (REPEAT (etac iffE 1 ORELSE ares_tac [iffI] 1 ORELSE mp_tac 1)) ; -qed "iff_cong"; - -val prems = Goal - "P <-> P' ==> ~P <-> ~P'"; -by (cut_facts_tac prems 1); -by (REPEAT (ares_tac [iffI,notI] 1 - ORELSE mp_tac 1 ORELSE eresolve_tac [iffE,notE] 1)) ; -qed "not_cong"; - -val prems = Goal - "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"; -by (REPEAT (ares_tac [iffI,allI] 1 - ORELSE mp_tac 1 ORELSE etac allE 1 ORELSE iff_tac prems 1)) ; -qed "all_cong"; - -val prems = Goal - "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))"; -by (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1 - ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ; -qed "ex_cong"; - -val prems = Goal - "(!!x. P(x) <-> Q(x)) ==> (EX! x. P(x)) <-> (EX! x. Q(x))"; -by (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 - ORELSE ares_tac [iffI,ex1I] 1 ORELSE mp_tac 1 - ORELSE iff_tac prems 1)) ; -qed "ex1_cong"; - -(*** Equality rules ***) - -Goal "a=b ==> b=a"; -by (etac subst 1); -by (rtac refl 1) ; -qed "sym"; - -Goal "[| a=b; b=c |] ==> a=c"; -by (etac subst 1 THEN assume_tac 1) ; -qed "trans"; - -(** ~ b=a ==> ~ a=b **) -bind_thm ("not_sym", hd (compose(sym,2,contrapos))); - - -(* Two theorms for rewriting only one instance of a definition: - the first for definitions of formulae and the second for terms *) - -val prems = goal (the_context()) "(A == B) ==> A <-> B"; -by (rewrite_goals_tac prems); -by (rtac iff_refl 1); -qed "def_imp_iff"; - -val prems = goal (the_context()) "(A == B) ==> A = B"; -by (rewrite_goals_tac prems); -by (rtac refl 1); -qed "meta_eq_to_obj_eq"; - -(*substitution*) -bind_thm ("ssubst", sym RS subst); - -(*A special case of ex1E that would otherwise need quantifier expansion*) -val prems = Goal - "[| EX! x. P(x); P(a); P(b) |] ==> a=b"; -by (cut_facts_tac prems 1); -by (etac ex1E 1); -by (rtac trans 1); -by (rtac sym 2); -by (REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ; -qed "ex1_equalsE"; - -(** Polymorphic congruence rules **) - -Goal "[| a=b |] ==> t(a)=t(b)"; -by (etac ssubst 1); -by (rtac refl 1) ; -qed "subst_context"; - -Goal "[| a=b; c=d |] ==> t(a,c)=t(b,d)"; -by (REPEAT (etac ssubst 1)); -by (rtac refl 1) ; -qed "subst_context2"; - -Goal "[| a=b; c=d; e=f |] ==> t(a,c,e)=t(b,d,f)"; -by (REPEAT (etac ssubst 1)); -by (rtac refl 1) ; -qed "subst_context3"; - -(*Useful with eresolve_tac for proving equalties from known equalities. - a = b - | | - c = d *) -Goal "[| a=b; a=c; b=d |] ==> c=d"; -by (rtac trans 1); -by (rtac trans 1); -by (rtac sym 1); -by (REPEAT (assume_tac 1)); -qed "box_equals"; - -(*Dual of box_equals: for proving equalities backwards*) -Goal "[| a=c; b=d; c=d |] ==> a=b"; -by (rtac trans 1); -by (rtac trans 1); -by (REPEAT (assume_tac 1)); -by (etac sym 1); -qed "simp_equals"; - -(** Congruence rules for predicate letters **) - -Goal "a=a' ==> P(a) <-> P(a')"; -by (rtac iffI 1); -by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ; -qed "pred1_cong"; - -Goal "[| a=a'; b=b' |] ==> P(a,b) <-> P(a',b')"; -by (rtac iffI 1); -by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ; -qed "pred2_cong"; - -Goal "[| a=a'; b=b'; c=c' |] ==> P(a,b,c) <-> P(a',b',c')"; -by (rtac iffI 1); -by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ; -qed "pred3_cong"; - -(*special cases for free variables P, Q, R, S -- up to 3 arguments*) - -val pred_congs = - List.concat (map (fn c => - map (fn th => read_instantiate [("P",c)] th) - [pred1_cong,pred2_cong,pred3_cong]) - (explode"PQRS")); - -(*special case for the equality predicate!*) -bind_thm ("eq_cong", read_instantiate [("P","op =")] pred2_cong); - - -(*** Simplifications of assumed implications. - Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE - used with mp_tac (restricted to atomic formulae) is COMPLETE for - intuitionistic propositional logic. See - R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic - (preprint, University of St Andrews, 1991) ***) - -val major::prems= Goal - "[| (P&Q)-->S; P-->(Q-->S) ==> R |] ==> R"; -by (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ; -qed "conj_impE"; - -val major::prems= Goal - "[| (P|Q)-->S; [| P-->S; Q-->S |] ==> R |] ==> R"; -by (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ; -qed "disj_impE"; - -(*Simplifies the implication. Classical version is stronger. - Still UNSAFE since Q must be provable -- backtracking needed. *) -val major::prems= Goal - "[| (P-->Q)-->S; [| P; Q-->S |] ==> Q; S ==> R |] ==> R"; -by (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ; -qed "imp_impE"; - -(*Simplifies the implication. Classical version is stronger. - Still UNSAFE since ~P must be provable -- backtracking needed. *) -val major::prems= Goal - "[| ~P --> S; P ==> False; S ==> R |] ==> R"; -by (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ; -qed "not_impE"; - -(*Simplifies the implication. UNSAFE. *) -val major::prems= Goal - "[| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P; \ -\ S ==> R |] ==> R"; -by (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ; -qed "iff_impE"; - -(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) -val major::prems= Goal - "[| (ALL x. P(x))-->S; !!x. P(x); S ==> R |] ==> R"; -by (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ; -qed "all_impE"; - -(*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) -val major::prems= Goal - "[| (EX x. P(x))-->S; P(x)-->S ==> R |] ==> R"; -by (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ; -qed "ex_impE"; - -(*** Courtesy of Krzysztof Grabczewski ***) - -val major::prems = Goal "[| P|Q; P==>R; Q==>S |] ==> R|S"; -by (rtac (major RS disjE) 1); -by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1)); -qed "disj_imp_disj"; diff -r 678299eac351 -r c5cf9243ad62 src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Sun Nov 26 23:09:25 2006 +0100 +++ b/src/FOL/IsaMakefile Sun Nov 26 23:43:53 2006 +0100 @@ -37,8 +37,7 @@ $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \ $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \ $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \ - $(SRC)/Provers/splitter.ML FOL.ML FOL.thy FOL_lemmas1.ML IFOL.ML \ - IFOL.thy IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML \ + $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML blastdata.ML cladata.ML \ document/root.tex fologic.ML hypsubstdata.ML intprover.ML simpdata.ML @$(ISATOOL) usedir -p 2 -b $(OUT)/Pure FOL diff -r 678299eac351 -r c5cf9243ad62 src/FOL/ROOT.ML --- a/src/FOL/ROOT.ML Sun Nov 26 23:09:25 2006 +0100 +++ b/src/FOL/ROOT.ML Sun Nov 26 23:43:53 2006 +0100 @@ -24,3 +24,13 @@ use "~~/src/Provers/project_rule.ML"; use_thy "FOL"; + +structure IFOL = +struct + val thy = theory "IFOL"; +end; + +structure FOL = +struct + val thy = theory "FOL"; +end; diff -r 678299eac351 -r c5cf9243ad62 src/FOL/blastdata.ML --- a/src/FOL/blastdata.ML Sun Nov 26 23:09:25 2006 +0100 +++ b/src/FOL/blastdata.ML Sun Nov 26 23:43:53 2006 +0100 @@ -1,3 +1,5 @@ + +val ccontr = thm "ccontr"; (*** Applying BlastFun to create Blast_tac ***) structure Blast_Data = diff -r 678299eac351 -r c5cf9243ad62 src/FOL/cladata.ML --- a/src/FOL/cladata.ML Sun Nov 26 23:09:25 2006 +0100 +++ b/src/FOL/cladata.ML Sun Nov 26 23:43:53 2006 +0100 @@ -13,7 +13,7 @@ struct val mp = mp val not_elim = notE - val classical = classical + val classical = thm "classical" val sizef = size_of_thm val hyp_subst_tacs=[hyp_subst_tac] end; @@ -22,25 +22,15 @@ structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical; -(*Better for fast_tac: needs no quantifier duplication!*) -qed_goal "alt_ex1E" IFOL.thy - "[| EX! x. P(x); \ -\ !!x. [| P(x); ALL y y'. P(y) & P(y') --> y=y' |] ==> R \ -\ |] ==> R" - (fn major::prems => - [ (rtac (major RS ex1E) 1), - (REPEAT (ares_tac (allI::prems) 1)), - (etac (dup_elim allE) 1), - (IntPr.fast_tac 1)]); - (*Propositional rules*) -val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] - addSEs [conjE,disjE,impCE,FalseE,iffCE]; +val prop_cs = empty_cs + addSIs [refl, TrueI, conjI, thm "disjCI", impI, notI, iffI] + addSEs [conjE, disjE, thm "impCE", FalseE, thm "iffCE"]; (*Quantifier rules*) -val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] - addSEs [exE,alt_ex1E] addEs [allE]; +val FOL_cs = prop_cs addSIs [allI, thm "ex_ex1I"] addIs [exI] + addSEs [exE, thm "alt_ex1E"] addEs [allE]; val cla_setup = (fn thy => (change_claset_of thy (fn _ => FOL_cs); thy)); diff -r 678299eac351 -r c5cf9243ad62 src/FOL/hypsubstdata.ML --- a/src/FOL/hypsubstdata.ML Sun Nov 26 23:09:25 2006 +0100 +++ b/src/FOL/hypsubstdata.ML Sun Nov 26 23:43:53 2006 +0100 @@ -6,13 +6,13 @@ val dest_eq = FOLogic.dest_eq val dest_Trueprop = FOLogic.dest_Trueprop val dest_imp = FOLogic.dest_imp - val eq_reflection = eq_reflection - val rev_eq_reflection = meta_eq_to_obj_eq - val imp_intr = impI - val rev_mp = rev_mp - val subst = subst - val sym = sym - val thin_refl = prove_goal (the_context ()) "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]); + val eq_reflection = thm "eq_reflection" + val rev_eq_reflection = thm "meta_eq_to_obj_eq" + val imp_intr = thm "impI" + val rev_mp = thm "rev_mp" + val subst = thm "subst" + val sym = thm "sym" + val thin_refl = thm "thin_refl" end; structure Hypsubst = HypsubstFun(Hypsubst_Data); diff -r 678299eac351 -r c5cf9243ad62 src/FOL/intprover.ML --- a/src/FOL/intprover.ML Sun Nov 26 23:09:25 2006 +0100 +++ b/src/FOL/intprover.ML Sun Nov 26 23:43:53 2006 +0100 @@ -41,22 +41,22 @@ step of an intuitionistic proof. *) val safe_brls = sort (make_ord lessb) - [ (true,FalseE), (false,TrueI), (false,refl), - (false,impI), (false,notI), (false,allI), - (true,conjE), (true,exE), - (false,conjI), (true,conj_impE), - (true,disj_impE), (true,disjE), - (false,iffI), (true,iffE), (true,not_to_imp) ]; + [ (true, thm "FalseE"), (false, thm "TrueI"), (false, thm "refl"), + (false, thm "impI"), (false, thm "notI"), (false, thm "allI"), + (true, thm "conjE"), (true, thm "exE"), + (false, thm "conjI"), (true, thm "conj_impE"), + (true, thm "disj_impE"), (true, thm "disjE"), + (false, thm "iffI"), (true, thm "iffE"), (true, thm "not_to_imp") ]; val haz_brls = - [ (false,disjI1), (false,disjI2), (false,exI), - (true,allE), (true,not_impE), (true,imp_impE), (true,iff_impE), - (true,all_impE), (true,ex_impE), (true,impE) ]; + [ (false, thm "disjI1"), (false, thm "disjI2"), (false, thm "exI"), + (true, thm "allE"), (true, thm "not_impE"), (true, thm "imp_impE"), (true, thm "iff_impE"), + (true, thm "all_impE"), (true, thm "ex_impE"), (true, thm "impE") ]; val haz_dup_brls = - [ (false,disjI1), (false,disjI2), (false,exI), - (true,all_dupE), (true,not_impE), (true,imp_impE), (true,iff_impE), - (true,all_impE), (true,ex_impE), (true,impE) ]; + [ (false, thm "disjI1"), (false, thm "disjI2"), (false, thm "exI"), + (true, thm "all_dupE"), (true, thm "not_impE"), (true, thm "imp_impE"), (true, thm "iff_impE"), + (true, thm "all_impE"), (true, thm "ex_impE"), (true, thm "impE") ]; (*0 subgoals vs 1 or more: the p in safep is for positive*) val (safe0_brls, safep_brls) = diff -r 678299eac351 -r c5cf9243ad62 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Sun Nov 26 23:09:25 2006 +0100 +++ b/src/FOL/simpdata.ML Sun Nov 26 23:43:53 2006 +0100 @@ -6,16 +6,11 @@ Simplification data for FOL. *) -val ex1_functional = thm "ex1_functional"; -val True_implies_equals = thm "True_implies_equals"; - - - (*** Rewrite rules ***) fun int_prove_fun s = (writeln s; - prove_goal IFOL.thy s + prove_goal (theory "IFOL") s (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ])); @@ -88,7 +83,7 @@ (*Replace premises x=y, X<->Y by X==Y*) val mk_meta_prems = rule_by_tactic - (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff])); + (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, thm "def_imp_iff"])); (*Congruence rules for = or <-> (instead of ==)*) fun mk_meta_cong rl = @@ -169,7 +164,7 @@ (*** Named rewrite rules proved for IFOL ***) -fun int_prove nm thm = qed_goal nm IFOL.thy thm +fun int_prove nm thm = qed_goal nm (theory "IFOL") thm (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ]); @@ -213,23 +208,6 @@ "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))"; -local -val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R" - (fn prems => [cut_facts_tac prems 1, Blast_tac 1]); - -val iff_allI = allI RS - prove_goal (the_context()) "ALL x. P(x) <-> Q(x) ==> (ALL x. P(x)) <-> (ALL x. Q(x))" - (fn prems => [cut_facts_tac prems 1, Blast_tac 1]) -val iff_exI = allI RS - prove_goal (the_context()) "ALL x. P(x) <-> Q(x) ==> (EX x. P(x)) <-> (EX x. Q(x))" - (fn prems => [cut_facts_tac prems 1, Blast_tac 1]) - -val all_comm = prove_goal (the_context()) "(ALL x y. P(x,y)) <-> (ALL y x. P(x,y))" - (fn _ => [Blast_tac 1]) -val ex_comm = prove_goal (the_context()) "(EX x y. P(x,y)) <-> (EX y x. P(x,y))" - (fn _ => [Blast_tac 1]) -in - (** make simplification procedures for quantifier elimination **) structure Quantifier1 = Quantifier1Fun( struct @@ -250,17 +228,15 @@ val conjE= conjE val impI = impI val mp = mp - val uncurry = uncurry + val uncurry = thm "uncurry" val exI = exI val exE = exE - val iff_allI = iff_allI - val iff_exI = iff_exI - val all_comm = all_comm - val ex_comm = ex_comm + val iff_allI = thm "iff_allI" + val iff_exI = thm "iff_exI" + val all_comm = thm "all_comm" + val ex_comm = thm "ex_comm" end); -end; - val defEX_regroup = Simplifier.simproc (the_context ()) "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex; @@ -272,9 +248,6 @@ (*** Case splitting ***) -bind_thm ("meta_eq_to_iff", prove_goal IFOL.thy "x==y ==> x<->y" - (fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1])); - structure SplitterData = struct structure Simplifier = Simplifier @@ -284,9 +257,9 @@ val disjE = disjE val conjE = conjE val exE = exE - val contrapos = contrapos - val contrapos2 = contrapos2 - val notnotD = notnotD + val contrapos = thm "contrapos" + val contrapos2 = thm "contrapos2" + val notnotD = thm "notnotD" end; structure Splitter = SplitterFun(SplitterData); @@ -302,21 +275,22 @@ (*** Standard simpsets ***) -structure Induction = InductionFun(struct val spec=IFOL.spec end); +structure Induction = InductionFun(struct val spec = spec end); open Induction; bind_thms ("meta_simps", [triv_forall_equality, (* prunes params *) - True_implies_equals]); (* prune asms `True' *) + thm "True_implies_equals"]); (* prune asms `True' *) bind_thms ("IFOL_simps", [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ imp_simps @ iff_simps @ quant_simps); bind_thm ("notFalseI", int_prove_fun "~False"); -bind_thms ("triv_rls", [TrueI,refl,reflexive_thm,iff_refl,notFalseI]); +bind_thms ("triv_rls", + [TrueI, refl, reflexive_thm, iff_refl, thm "notFalseI"]); fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems), atac, etac FalseE]; @@ -339,10 +313,11 @@ (*intuitionistic simprules only*) -val IFOL_ss = FOL_basic_ss +val IFOL_ss = + FOL_basic_ss addsimps (meta_simps @ IFOL_simps @ int_ex_simps @ int_all_simps) addsimprocs [defALL_regroup, defEX_regroup] - addcongs [imp_cong]; + addcongs [thm "imp_cong"]; bind_thms ("cla_simps", [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, diff -r 678299eac351 -r c5cf9243ad62 src/ZF/Integ/int_arith.ML --- a/src/ZF/Integ/int_arith.ML Sun Nov 26 23:09:25 2006 +0100 +++ b/src/ZF/Integ/int_arith.ML Sun Nov 26 23:43:53 2006 +0100 @@ -20,7 +20,7 @@ AddIffs [inst "y" "integ_of(?w)" zminus_zle, inst "x" "integ_of(?w)" zle_zminus]; -Addsimps [inst "s" "integ_of(?w)" Let_def]; +Addsimps [inst "s" "integ_of(?w)" (thm "Let_def")]; (*** Simprocs for numeric literals ***) diff -r 678299eac351 -r c5cf9243ad62 src/ZF/ind_syntax.ML --- a/src/ZF/ind_syntax.ML Sun Nov 26 23:09:25 2006 +0100 +++ b/src/ZF/ind_syntax.ML Sun Nov 26 23:43:53 2006 +0100 @@ -136,20 +136,20 @@ (*Could go to FOL, but it's hardly general*) -val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b" - (fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]); +val def_swap_iff = prove_goal (the_context ()) "a==b ==> a=c <-> c=b" + (fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]); -val def_trans = prove_goal IFOL.thy "[| f==g; g(a)=b |] ==> f(a)=b" +val def_trans = prove_goal (the_context ()) "[| f==g; g(a)=b |] ==> f(a)=b" (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]); (*Delete needless equality assumptions*) -val refl_thin = prove_goal IFOL.thy "!!P. [| a=a; P |] ==> P" +val refl_thin = prove_goal (the_context ()) "!!P. [| a=a; P |] ==> P" (fn _ => [assume_tac 1]); (*Includes rules for succ and Pair since they are common constructions*) -val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, - Pair_neq_0, sym RS Pair_neq_0, Pair_inject, - make_elim succ_inject, +val elim_rls = [asm_rl, FalseE, thm "succ_neq_0", sym RS thm "succ_neq_0", + thm "Pair_neq_0", sym RS thm "Pair_neq_0", thm "Pair_inject", + make_elim (thm "succ_inject"), refl_thin, conjE, exE, disjE]; @@ -163,7 +163,6 @@ (*Turns iff rules into safe elimination rules*) fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]); - end;