# HG changeset patch # User wenzelm # Date 935606719 -7200 # Node ID 4c43090659cad83eb7c572e802f44fc412a15cdf # Parent 358b1c5391f0c3c417f9713a376d94b40605034b proper bootstrap of IFOL/FOL theories and packages; diff -r 358b1c5391f0 -r 4c43090659ca src/FOL/FOL.ML --- a/src/FOL/FOL.ML Wed Aug 25 20:42:01 1999 +0200 +++ b/src/FOL/FOL.ML Wed Aug 25 20:45:19 1999 +0200 @@ -1,94 +1,8 @@ -(* Title: FOL/FOL.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge -Tactics and lemmas for FOL.thy (classical First-Order Logic) -*) +structure FOL = +struct + val thy = the_context (); + val classical = classical; +end; open FOL; - - -val ccontr = FalseE RS classical; - -(*** Classical introduction rules for | and EX ***) - -qed_goal "disjCI" FOL.thy - "(~Q ==> P) ==> P|Q" - (fn prems=> - [ (rtac classical 1), - (REPEAT (ares_tac (prems@[disjI1,notI]) 1)), - (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]); - -(*introduction rule involving only EX*) -qed_goal "ex_classical" FOL.thy - "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)" - (fn prems=> - [ (rtac classical 1), - (eresolve_tac (prems RL [exI]) 1) ]); - -(*version of above, simplifying ~EX to ALL~ *) -qed_goal "exCI" FOL.thy - "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)" - (fn [prem]=> - [ (rtac ex_classical 1), - (resolve_tac [notI RS allI RS prem] 1), - (etac notE 1), - (etac exI 1) ]); - -qed_goal "excluded_middle" FOL.thy "~P | P" - (fn _=> [ rtac disjCI 1, assume_tac 1 ]); - -(*For disjunctive case analysis*) -fun excluded_middle_tac sP = - res_inst_tac [("Q",sP)] (excluded_middle RS disjE); - -qed_goal "case_split_thm" FOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q" - (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1, - etac p2 1, etac p1 1]); - -(*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. *) -qed_goal "impCE" FOL.thy - "[| P-->Q; ~P ==> R; Q ==> R |] ==> R" - (fn major::prems=> - [ (resolve_tac [excluded_middle RS disjE] 1), - (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]); - -(*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.*) -qed_goal "impCE'" thy - "[| P-->Q; Q ==> R; ~P ==> R |] ==> R" - (fn major::prems=> - [ (resolve_tac [excluded_middle RS disjE] 1), - (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]); - -(*Double negation law*) -qed_goal "notnotD" FOL.thy "~~P ==> P" - (fn [major]=> - [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]); - -qed_goal "contrapos2" FOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [ - rtac classical 1, - dtac p2 1, - etac notE 1, - rtac p1 1]); - -(*** Tactics for implication and contradiction ***) - -(*Classical <-> elimination. Proof substitutes P=Q in - ~P ==> ~Q and P ==> Q *) -qed_goalw "iffCE" FOL.thy [iff_def] - "[| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R" - (fn prems => - [ (rtac conjE 1), - (REPEAT (DEPTH_SOLVE_1 - (etac impCE 1 ORELSE mp_tac 1 ORELSE ares_tac prems 1))) ]); - diff -r 358b1c5391f0 -r 4c43090659ca src/FOL/FOL.thy --- a/src/FOL/FOL.thy Wed Aug 25 20:42:01 1999 +0200 +++ b/src/FOL/FOL.thy Wed Aug 25 20:45:19 1999 +0200 @@ -1,10 +1,14 @@ -FOL = IFOL + +theory FOL = IFOL +files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("FOL_lemmas2.ML"): -rules - classical "(~P ==> P) ==> P" +axioms + classical: "(~P ==> P) ==> P" -setup ClasetThyData.setup -setup attrib_setup (* FIXME move to IFOL.thy *) +use "FOL_lemmas1.ML" +use "cladata.ML" setup Cla.setup setup clasetup +use "blastdata.ML" setup Blast.setup +use "FOL_lemmas2.ML" +use "simpdata.ML" setup simpsetup setup Clasimp.setup end diff -r 358b1c5391f0 -r 4c43090659ca src/FOL/FOL_lemmas1.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/FOL/FOL_lemmas1.ML Wed Aug 25 20:45:19 1999 +0200 @@ -0,0 +1,92 @@ +(* 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"; +val ccontr = FalseE RS classical; + + +(*** Classical introduction rules for | and EX ***) + +qed_goal "disjCI" (the_context ()) + "(~Q ==> P) ==> P|Q" + (fn prems=> + [ (rtac classical 1), + (REPEAT (ares_tac (prems@[disjI1,notI]) 1)), + (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]); + +(*introduction rule involving only EX*) +qed_goal "ex_classical" (the_context ()) + "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)" + (fn prems=> + [ (rtac classical 1), + (eresolve_tac (prems RL [exI]) 1) ]); + +(*version of above, simplifying ~EX to ALL~ *) +qed_goal "exCI" (the_context ()) + "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)" + (fn [prem]=> + [ (rtac ex_classical 1), + (resolve_tac [notI RS allI RS prem] 1), + (etac notE 1), + (etac exI 1) ]); + +qed_goal "excluded_middle" (the_context ()) "~P | P" + (fn _=> [ rtac disjCI 1, assume_tac 1 ]); + +(*For disjunctive case analysis*) +fun excluded_middle_tac sP = + res_inst_tac [("Q",sP)] (excluded_middle RS disjE); + +qed_goal "case_split_thm" (the_context ()) "[| P ==> Q; ~P ==> Q |] ==> Q" + (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1, + etac p2 1, etac p1 1]); + +(*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. *) +qed_goal "impCE" (the_context ()) + "[| P-->Q; ~P ==> R; Q ==> R |] ==> R" + (fn major::prems=> + [ (resolve_tac [excluded_middle RS disjE] 1), + (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]); + +(*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.*) +qed_goal "impCE'" (the_context ()) + "[| P-->Q; Q ==> R; ~P ==> R |] ==> R" + (fn major::prems=> + [ (resolve_tac [excluded_middle RS disjE] 1), + (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]); + +(*Double negation law*) +qed_goal "notnotD" (the_context ()) "~~P ==> P" + (fn [major]=> + [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]); + +qed_goal "contrapos2" (the_context ()) "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [ + rtac classical 1, + dtac p2 1, + etac notE 1, + rtac p1 1]); + +(*** Tactics for implication and contradiction ***) + +(*Classical <-> elimination. Proof substitutes P=Q in + ~P ==> ~Q and P ==> Q *) +qed_goalw "iffCE" (the_context ()) [iff_def] + "[| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R" + (fn prems => + [ (rtac conjE 1), + (REPEAT (DEPTH_SOLVE_1 + (etac impCE 1 ORELSE mp_tac 1 ORELSE ares_tac prems 1))) ]); diff -r 358b1c5391f0 -r 4c43090659ca src/FOL/FOL_lemmas2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/FOL/FOL_lemmas2.ML Wed Aug 25 20:45:19 1999 +0200 @@ -0,0 +1,4 @@ + +Goal "!!a b c. [| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c"; + by (Blast_tac 1); +qed "ex1_functional"; diff -r 358b1c5391f0 -r 4c43090659ca src/FOL/IFOL.ML --- a/src/FOL/IFOL.ML Wed Aug 25 20:42:01 1999 +0200 +++ b/src/FOL/IFOL.ML Wed Aug 25 20:45:19 1999 +0200 @@ -1,454 +1,28 @@ -(* Title: FOL/IFOL.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge -Tactics and lemmas for IFOL.thy (intuitionistic first-order logic) -*) - -qed_goalw "TrueI" IFOL.thy [True_def] "True" - (fn _ => [ (REPEAT (ares_tac [impI] 1)) ]); - -(*** Sequent-style elimination rules for & --> and ALL ***) - -qed_goal "conjE" IFOL.thy - "[| P&Q; [| P; Q |] ==> R |] ==> R" - (fn prems=> - [ (REPEAT (resolve_tac prems 1 - ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN - resolve_tac prems 1))) ]); - -qed_goal "impE" IFOL.thy - "[| P-->Q; P; Q ==> R |] ==> R" - (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); - -qed_goal "allE" IFOL.thy - "[| ALL x. P(x); P(x) ==> R |] ==> R" - (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); - -(*Duplicates the quantifier; for use with eresolve_tac*) -qed_goal "all_dupE" IFOL.thy - "[| ALL x. P(x); [| P(x); ALL x. P(x) |] ==> R \ -\ |] ==> R" - (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); - - -(*** Negation rules, which translate between ~P and P-->False ***) - -qed_goalw "notI" IFOL.thy [not_def] "(P ==> False) ==> ~P" - (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]); - -qed_goalw "notE" IFOL.thy [not_def] "[| ~P; P |] ==> R" - (fn prems=> - [ (resolve_tac [mp RS FalseE] 1), - (REPEAT (resolve_tac prems 1)) ]); - -qed_goal "rev_notE" IFOL.thy "!!P R. [| P; ~P |] ==> R" - (fn _ => [REPEAT (ares_tac [notE] 1)]); - -(*This is useful with the special implication rules for each kind of P. *) -qed_goal "not_to_imp" IFOL.thy - "[| ~P; (P-->False) ==> Q |] ==> Q" - (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]); - -(* 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 *) -qed_goal "rev_mp" IFOL.thy "[| P; P --> Q |] ==> Q" - (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); - -(*Contrapositive of an inference rule*) -qed_goal "contrapos" IFOL.thy "[| ~Q; P==>Q |] ==> ~P" - (fn [major,minor]=> - [ (rtac (major RS notE RS notI) 1), - (etac minor 1) ]); - - -(*** 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 ***) - -qed_goalw "iffI" IFOL.thy [iff_def] - "[| P ==> Q; Q ==> P |] ==> P<->Q" - (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]); - - -(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) -qed_goalw "iffE" IFOL.thy [iff_def] - "[| P <-> Q; [| P-->Q; Q-->P |] ==> R |] ==> R" - (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]); - -(* Destruct rules for <-> similar to Modus Ponens *) - -qed_goalw "iffD1" IFOL.thy [iff_def] "[| P <-> Q; P |] ==> Q" - (fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); - -qed_goalw "iffD2" IFOL.thy [iff_def] "[| P <-> Q; Q |] ==> P" - (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); - -qed_goal "rev_iffD1" IFOL.thy "!!P. [| P; P <-> Q |] ==> Q" - (fn _ => [etac iffD1 1, assume_tac 1]); - -qed_goal "rev_iffD2" IFOL.thy "!!P. [| Q; P <-> Q |] ==> P" - (fn _ => [etac iffD2 1, assume_tac 1]); - -qed_goal "iff_refl" IFOL.thy "P <-> P" - (fn _ => [ (REPEAT (ares_tac [iffI] 1)) ]); - -qed_goal "iff_sym" IFOL.thy "Q <-> P ==> P <-> Q" - (fn [major] => - [ (rtac (major RS iffE) 1), - (rtac iffI 1), - (REPEAT (eresolve_tac [asm_rl,mp] 1)) ]); - -qed_goal "iff_trans" IFOL.thy - "!!P Q R. [| P <-> Q; Q<-> R |] ==> P <-> R" - (fn _ => - [ (rtac iffI 1), - (REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ]); - - -(*** 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. -***) - -qed_goalw "ex1I" IFOL.thy [ex1_def] - "[| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x)" - (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]); - -(*Sometimes easier to use: the premises have no shared variables. Safe!*) -qed_goal "ex_ex1I" IFOL.thy - "[| EX x. P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)" - (fn [ex,eq] => [ (rtac (ex RS exE) 1), - (REPEAT (ares_tac [ex1I,eq] 1)) ]); - -qed_goalw "ex1E" IFOL.thy [ex1_def] - "[| EX! x. P(x); !!x. [| P(x); ALL y. P(y) --> y=x |] ==> R |] ==> R" - (fn prems => - [ (cut_facts_tac prems 1), - (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]); - - -(*** <-> 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); - -qed_goal "conj_cong" IFOL.thy - "[| P <-> P'; P' ==> Q <-> Q' |] ==> (P&Q) <-> (P'&Q')" - (fn prems => - [ (cut_facts_tac prems 1), - (REPEAT (ares_tac [iffI,conjI] 1 - ORELSE eresolve_tac [iffE,conjE,mp] 1 - ORELSE iff_tac prems 1)) ]); - -(*Reversed congruence rule! Used in ZF/Order*) -qed_goal "conj_cong2" IFOL.thy - "[| P <-> P'; P' ==> Q <-> Q' |] ==> (Q&P) <-> (Q'&P')" - (fn prems => - [ (cut_facts_tac prems 1), - (REPEAT (ares_tac [iffI,conjI] 1 - ORELSE eresolve_tac [iffE,conjE,mp] 1 - ORELSE iff_tac prems 1)) ]); - -qed_goal "disj_cong" IFOL.thy - "[| P <-> P'; Q <-> Q' |] ==> (P|Q) <-> (P'|Q')" - (fn prems => - [ (cut_facts_tac prems 1), - (REPEAT (eresolve_tac [iffE,disjE,disjI1,disjI2] 1 - ORELSE ares_tac [iffI] 1 - ORELSE mp_tac 1)) ]); - -qed_goal "imp_cong" IFOL.thy - "[| P <-> P'; P' ==> Q <-> Q' |] ==> (P-->Q) <-> (P'-->Q')" - (fn prems => - [ (cut_facts_tac prems 1), - (REPEAT (ares_tac [iffI,impI] 1 - ORELSE etac iffE 1 - ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]); - -qed_goal "iff_cong" IFOL.thy - "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')" - (fn prems => - [ (cut_facts_tac prems 1), - (REPEAT (etac iffE 1 - ORELSE ares_tac [iffI] 1 - ORELSE mp_tac 1)) ]); - -qed_goal "not_cong" IFOL.thy - "P <-> P' ==> ~P <-> ~P'" - (fn prems => - [ (cut_facts_tac prems 1), - (REPEAT (ares_tac [iffI,notI] 1 - ORELSE mp_tac 1 - ORELSE eresolve_tac [iffE,notE] 1)) ]); - -qed_goal "all_cong" IFOL.thy - "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))" - (fn prems => - [ (REPEAT (ares_tac [iffI,allI] 1 - ORELSE mp_tac 1 - ORELSE etac allE 1 ORELSE iff_tac prems 1)) ]); - -qed_goal "ex_cong" IFOL.thy - "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))" - (fn prems => - [ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1 - ORELSE mp_tac 1 - ORELSE iff_tac prems 1)) ]); - -qed_goal "ex1_cong" IFOL.thy - "(!!x. P(x) <-> Q(x)) ==> (EX! x. P(x)) <-> (EX! x. Q(x))" - (fn prems => - [ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1 - ORELSE mp_tac 1 - ORELSE iff_tac prems 1)) ]); - -(*** Equality rules ***) - -qed_goal "sym" IFOL.thy "a=b ==> b=a" - (fn [major] => [ (rtac (major RS subst) 1), (rtac refl 1) ]); - -qed_goal "trans" IFOL.thy "[| a=b; b=c |] ==> a=c" - (fn [prem1,prem2] => [ (rtac (prem2 RS subst) 1), (rtac prem1 1) ]); - -(** ~ b=a ==> ~ a=b **) -val [not_sym] = 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 IFOL.thy "(A == B) ==> A <-> B"; -by (rewrite_goals_tac prems); -by (rtac iff_refl 1); -qed "def_imp_iff"; - -val prems = goal IFOL.thy "(A == B) ==> A = B"; -by (rewrite_goals_tac prems); -by (rtac refl 1); -qed "meta_eq_to_obj_eq"; - - -(*Substitution: rule and tactic*) -bind_thm ("ssubst", sym RS subst); - -(*Apply an equality or definition ONCE. - Fails unless the substitution has an effect*) -fun stac th = - let val th' = th RS meta_eq_to_obj_eq handle THM _ => th - in CHANGED_GOAL (rtac (th' RS ssubst)) - end; - -(*A special case of ex1E that would otherwise need quantifier expansion*) -qed_goal "ex1_equalsE" IFOL.thy - "[| EX! x. P(x); P(a); P(b) |] ==> a=b" - (fn prems => - [ (cut_facts_tac prems 1), - (etac ex1E 1), - (rtac trans 1), - (rtac sym 2), - (REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ]); - -(** Polymorphic congruence rules **) - -qed_goal "subst_context" IFOL.thy - "[| a=b |] ==> t(a)=t(b)" - (fn prems=> - [ (resolve_tac (prems RL [ssubst]) 1), - (rtac refl 1) ]); - -qed_goal "subst_context2" IFOL.thy - "[| a=b; c=d |] ==> t(a,c)=t(b,d)" - (fn prems=> - [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]); - -qed_goal "subst_context3" IFOL.thy - "[| a=b; c=d; e=f |] ==> t(a,c,e)=t(b,d,f)" - (fn prems=> - [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]); - -(*Useful with eresolve_tac for proving equalties from known equalities. - a = b - | | - c = d *) -qed_goal "box_equals" IFOL.thy - "[| a=b; a=c; b=d |] ==> c=d" - (fn prems=> - [ (rtac trans 1), - (rtac trans 1), - (rtac sym 1), - (REPEAT (resolve_tac prems 1)) ]); - -(*Dual of box_equals: for proving equalities backwards*) -qed_goal "simp_equals" IFOL.thy - "[| a=c; b=d; c=d |] ==> a=b" - (fn prems=> - [ (rtac trans 1), - (rtac trans 1), - (REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]); - -(** Congruence rules for predicate letters **) - -qed_goal "pred1_cong" IFOL.thy - "a=a' ==> P(a) <-> P(a')" - (fn prems => - [ (cut_facts_tac prems 1), - (rtac iffI 1), - (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); - -qed_goal "pred2_cong" IFOL.thy - "[| a=a'; b=b' |] ==> P(a,b) <-> P(a',b')" - (fn prems => - [ (cut_facts_tac prems 1), - (rtac iffI 1), - (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); - -qed_goal "pred3_cong" IFOL.thy - "[| a=a'; b=b'; c=c' |] ==> P(a,b,c) <-> P(a',b',c')" - (fn prems => - [ (cut_facts_tac prems 1), - (rtac iffI 1), - (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); - -(*special cases for free variables P, Q, R, S -- up to 3 arguments*) - -val pred_congs = - flat (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!*) -val 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) ***) - -qed_goal "conj_impE" IFOL.thy - "[| (P&Q)-->S; P-->(Q-->S) ==> R |] ==> R" - (fn major::prems=> - [ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]); - -qed_goal "disj_impE" IFOL.thy - "[| (P|Q)-->S; [| P-->S; Q-->S |] ==> R |] ==> R" - (fn major::prems=> - [ (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ]); - -(*Simplifies the implication. Classical version is stronger. - Still UNSAFE since Q must be provable -- backtracking needed. *) -qed_goal "imp_impE" IFOL.thy - "[| (P-->Q)-->S; [| P; Q-->S |] ==> Q; S ==> R |] ==> R" - (fn major::prems=> - [ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]); - -(*Simplifies the implication. Classical version is stronger. - Still UNSAFE since ~P must be provable -- backtracking needed. *) -qed_goal "not_impE" IFOL.thy - "[| ~P --> S; P ==> False; S ==> R |] ==> R" - (fn major::prems=> - [ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]); - -(*Simplifies the implication. UNSAFE. *) -qed_goal "iff_impE" IFOL.thy - "[| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P; \ -\ S ==> R |] ==> R" - (fn major::prems=> - [ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]); - -(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) -qed_goal "all_impE" IFOL.thy - "[| (ALL x. P(x))-->S; !!x. P(x); S ==> R |] ==> R" - (fn major::prems=> - [ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]); - -(*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) -qed_goal "ex_impE" IFOL.thy - "[| (EX x. P(x))-->S; P(x)-->S ==> R |] ==> R" - (fn major::prems=> - [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]); - -(*** Courtesy of Krzysztof Grabczewski ***) - -val major::prems = goal IFOL.thy "[| 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"; - - -(** strip ALL and --> from proved goal while preserving ALL-bound var names **) - -fun make_new_spec rl = - (* Use a crazy name to avoid forall_intr failing because of - duplicate variable name *) - let val myspec = read_instantiate [("P","?wlzickd")] rl - val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec; - val cvx = cterm_of (#sign(rep_thm myspec)) vx - in (vxT, forall_intr cvx myspec) end; - -local - -val (specT, spec') = make_new_spec spec - -in - -fun RSspec th = - (case concl_of th of - _ $ (Const("All",_) $ Abs(a,_,_)) => - let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),specT)) - in th RS forall_elim ca spec' end - | _ => raise THM("RSspec",0,[th])); - -fun RSmp th = - (case concl_of th of - _ $ (Const("op -->",_)$_$_) => th RS mp - | _ => raise THM("RSmp",0,[th])); - -fun normalize_thm funs = - let fun trans [] th = th - | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th - in trans funs end; - -fun qed_spec_mp name = - let val thm = normalize_thm [RSspec,RSmp] (result()) - in bind_thm(name, thm) end; - -fun qed_goal_spec_mp name thy s p = - bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p)); - -fun qed_goalw_spec_mp name thy defs s p = - bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p)); - +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; - -(* attributes *) - -local - -fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x; - -in - -val attrib_setup = - [Attrib.add_attributes - [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]]; - -end; +open IFOL; diff -r 358b1c5391f0 -r 4c43090659ca src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Wed Aug 25 20:42:01 1999 +0200 +++ b/src/FOL/IFOL.thy Wed Aug 25 20:45:19 1999 +0200 @@ -6,120 +6,121 @@ Intuitionistic first-order logic. *) -IFOL = Pure + +theory IFOL = Pure +files ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML"): + global -classes - term < logic - -default - term +classes "term" < logic +defaultsort "term" -types - o - -arities - o :: logic - +typedecl o consts - Trueprop :: o => prop ("(_)" 5) - True, False :: o + Trueprop :: "o => prop" ("(_)" 5) + True :: o + False :: o (* Connectives *) - "=" :: ['a, 'a] => o (infixl 50) + "=" :: "['a, 'a] => o" (infixl 50) - Not :: o => o ("~ _" [40] 40) - "&" :: [o, o] => o (infixr 35) - "|" :: [o, o] => o (infixr 30) - "-->" :: [o, o] => o (infixr 25) - "<->" :: [o, o] => o (infixr 25) + Not :: "o => o" ("~ _" [40] 40) + & :: "[o, o] => o" (infixr 35) + "|" :: "[o, o] => o" (infixr 30) + --> :: "[o, o] => o" (infixr 25) + <-> :: "[o, o] => o" (infixr 25) (* Quantifiers *) - All :: ('a => o) => o (binder "ALL " 10) - Ex :: ('a => o) => o (binder "EX " 10) - Ex1 :: ('a => o) => o (binder "EX! " 10) + All :: "('a => o) => o" (binder "ALL " 10) + Ex :: "('a => o) => o" (binder "EX " 10) + Ex1 :: "('a => o) => o" (binder "EX! " 10) syntax - "~=" :: ['a, 'a] => o (infixl 50) + "~=" :: "['a, 'a] => o" (infixl 50) translations "x ~= y" == "~ (x = y)" syntax (symbols) - Not :: o => o ("\\ _" [40] 40) - "op &" :: [o, o] => o (infixr "\\" 35) - "op |" :: [o, o] => o (infixr "\\" 30) - "op -->" :: [o, o] => o (infixr "\\\\" 25) - "op <->" :: [o, o] => o (infixr "\\\\" 25) - "ALL " :: [idts, o] => o ("(3\\_./ _)" [0, 10] 10) - "EX " :: [idts, o] => o ("(3\\_./ _)" [0, 10] 10) - "EX! " :: [idts, o] => o ("(3\\!_./ _)" [0, 10] 10) - "op ~=" :: ['a, 'a] => o (infixl "\\" 50) + Not :: "o => o" ("\\ _" [40] 40) + "op &" :: "[o, o] => o" (infixr "\\" 35) + "op |" :: "[o, o] => o" (infixr "\\" 30) + "op -->" :: "[o, o] => o" (infixr "\\\\" 25) + "op <->" :: "[o, o] => o" (infixr "\\\\" 25) + "ALL " :: "[idts, o] => o" ("(3\\_./ _)" [0, 10] 10) + "EX " :: "[idts, o] => o" ("(3\\_./ _)" [0, 10] 10) + "EX! " :: "[idts, o] => o" ("(3\\!_./ _)" [0, 10] 10) + "op ~=" :: "['a, 'a] => o" (infixl "\\" 50) syntax (xsymbols) - "op -->" :: [o, o] => o (infixr "\\" 25) - "op <->" :: [o, o] => o (infixr "\\" 25) + "op -->" :: "[o, o] => o" (infixr "\\" 25) + "op <->" :: "[o, o] => o" (infixr "\\" 25) syntax (HTML output) - Not :: o => o ("\\ _" [40] 40) + Not :: "o => o" ("\\ _" [40] 40) local -rules +axioms (* Equality *) - refl "a=a" - subst "[| a=b; P(a) |] ==> P(b)" + refl: "a=a" + subst: "[| a=b; P(a) |] ==> P(b)" (* Propositional logic *) - conjI "[| P; Q |] ==> P&Q" - conjunct1 "P&Q ==> P" - conjunct2 "P&Q ==> Q" + conjI: "[| P; Q |] ==> P&Q" + conjunct1: "P&Q ==> P" + conjunct2: "P&Q ==> Q" - disjI1 "P ==> P|Q" - disjI2 "Q ==> P|Q" - disjE "[| P|Q; P ==> R; Q ==> R |] ==> R" + disjI1: "P ==> P|Q" + disjI2: "Q ==> P|Q" + disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" - impI "(P ==> Q) ==> P-->Q" - mp "[| P-->Q; P |] ==> Q" + impI: "(P ==> Q) ==> P-->Q" + mp: "[| P-->Q; P |] ==> Q" - FalseE "False ==> P" + FalseE: "False ==> P" + (* Definitions *) - True_def "True == False-->False" - not_def "~P == P-->False" - iff_def "P<->Q == (P-->Q) & (Q-->P)" + True_def: "True == False-->False" + not_def: "~P == P-->False" + iff_def: "P<->Q == (P-->Q) & (Q-->P)" (* Unique existence *) - ex1_def "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)" + ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)" + (* Quantifiers *) - allI "(!!x. P(x)) ==> (ALL x. P(x))" - spec "(ALL x. P(x)) ==> P(x)" + allI: "(!!x. P(x)) ==> (ALL x. P(x))" + spec: "(ALL x. P(x)) ==> P(x)" - exI "P(x) ==> (EX x. P(x))" - exE "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" + exI: "P(x) ==> (EX x. P(x))" + exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" (* Reflection *) - eq_reflection "(x=y) ==> (x==y)" - iff_reflection "(P<->Q) ==> (P==Q)" + eq_reflection: "(x=y) ==> (x==y)" + iff_reflection: "(P<->Q) ==> (P==Q)" -setup - Simplifier.setup + setup Simplifier.setup +use "IFOL_lemmas.ML" setup attrib_setup +use "fologic.ML" +use "hypsubstdata.ML" +use "intprover.ML" + end diff -r 358b1c5391f0 -r 4c43090659ca src/FOL/IFOL_lemmas.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/FOL/IFOL_lemmas.ML Wed Aug 25 20:45:19 1999 +0200 @@ -0,0 +1,480 @@ +(* 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"; + + + +qed_goalw "TrueI" (the_context ()) [True_def] "True" + (fn _ => [ (REPEAT (ares_tac [impI] 1)) ]); + +(*** Sequent-style elimination rules for & --> and ALL ***) + +qed_goal "conjE" (the_context ()) + "[| P&Q; [| P; Q |] ==> R |] ==> R" + (fn prems=> + [ (REPEAT (resolve_tac prems 1 + ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN + resolve_tac prems 1))) ]); + +qed_goal "impE" (the_context ()) + "[| P-->Q; P; Q ==> R |] ==> R" + (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); + +qed_goal "allE" (the_context ()) + "[| ALL x. P(x); P(x) ==> R |] ==> R" + (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); + +(*Duplicates the quantifier; for use with eresolve_tac*) +qed_goal "all_dupE" (the_context ()) + "[| ALL x. P(x); [| P(x); ALL x. P(x) |] ==> R \ +\ |] ==> R" + (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); + + +(*** Negation rules, which translate between ~P and P-->False ***) + +qed_goalw "notI" (the_context ()) [not_def] "(P ==> False) ==> ~P" + (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]); + +qed_goalw "notE" (the_context ()) [not_def] "[| ~P; P |] ==> R" + (fn prems=> + [ (resolve_tac [mp RS FalseE] 1), + (REPEAT (resolve_tac prems 1)) ]); + +qed_goal "rev_notE" (the_context ()) "!!P R. [| P; ~P |] ==> R" + (fn _ => [REPEAT (ares_tac [notE] 1)]); + +(*This is useful with the special implication rules for each kind of P. *) +qed_goal "not_to_imp" (the_context ()) + "[| ~P; (P-->False) ==> Q |] ==> Q" + (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]); + +(* 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 *) +qed_goal "rev_mp" (the_context ()) "[| P; P --> Q |] ==> Q" + (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); + +(*Contrapositive of an inference rule*) +qed_goal "contrapos" (the_context ()) "[| ~Q; P==>Q |] ==> ~P" + (fn [major,minor]=> + [ (rtac (major RS notE RS notI) 1), + (etac minor 1) ]); + + +(*** 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 ***) + +qed_goalw "iffI" (the_context ()) [iff_def] + "[| P ==> Q; Q ==> P |] ==> P<->Q" + (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]); + + +(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) +qed_goalw "iffE" (the_context ()) [iff_def] + "[| P <-> Q; [| P-->Q; Q-->P |] ==> R |] ==> R" + (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]); + +(* Destruct rules for <-> similar to Modus Ponens *) + +qed_goalw "iffD1" (the_context ()) [iff_def] "[| P <-> Q; P |] ==> Q" + (fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); + +qed_goalw "iffD2" (the_context ()) [iff_def] "[| P <-> Q; Q |] ==> P" + (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); + +qed_goal "rev_iffD1" (the_context ()) "!!P. [| P; P <-> Q |] ==> Q" + (fn _ => [etac iffD1 1, assume_tac 1]); + +qed_goal "rev_iffD2" (the_context ()) "!!P. [| Q; P <-> Q |] ==> P" + (fn _ => [etac iffD2 1, assume_tac 1]); + +qed_goal "iff_refl" (the_context ()) "P <-> P" + (fn _ => [ (REPEAT (ares_tac [iffI] 1)) ]); + +qed_goal "iff_sym" (the_context ()) "Q <-> P ==> P <-> Q" + (fn [major] => + [ (rtac (major RS iffE) 1), + (rtac iffI 1), + (REPEAT (eresolve_tac [asm_rl,mp] 1)) ]); + +qed_goal "iff_trans" (the_context ()) + "!!P Q R. [| P <-> Q; Q<-> R |] ==> P <-> R" + (fn _ => + [ (rtac iffI 1), + (REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ]); + + +(*** 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. +***) + +qed_goalw "ex1I" (the_context ()) [ex1_def] + "[| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x)" + (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]); + +(*Sometimes easier to use: the premises have no shared variables. Safe!*) +qed_goal "ex_ex1I" (the_context ()) + "[| EX x. P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)" + (fn [ex,eq] => [ (rtac (ex RS exE) 1), + (REPEAT (ares_tac [ex1I,eq] 1)) ]); + +qed_goalw "ex1E" (the_context ()) [ex1_def] + "[| EX! x. P(x); !!x. [| P(x); ALL y. P(y) --> y=x |] ==> R |] ==> R" + (fn prems => + [ (cut_facts_tac prems 1), + (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]); + + +(*** <-> 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); + +qed_goal "conj_cong" (the_context ()) + "[| P <-> P'; P' ==> Q <-> Q' |] ==> (P&Q) <-> (P'&Q')" + (fn prems => + [ (cut_facts_tac prems 1), + (REPEAT (ares_tac [iffI,conjI] 1 + ORELSE eresolve_tac [iffE,conjE,mp] 1 + ORELSE iff_tac prems 1)) ]); + +(*Reversed congruence rule! Used in ZF/Order*) +qed_goal "conj_cong2" (the_context ()) + "[| P <-> P'; P' ==> Q <-> Q' |] ==> (Q&P) <-> (Q'&P')" + (fn prems => + [ (cut_facts_tac prems 1), + (REPEAT (ares_tac [iffI,conjI] 1 + ORELSE eresolve_tac [iffE,conjE,mp] 1 + ORELSE iff_tac prems 1)) ]); + +qed_goal "disj_cong" (the_context ()) + "[| P <-> P'; Q <-> Q' |] ==> (P|Q) <-> (P'|Q')" + (fn prems => + [ (cut_facts_tac prems 1), + (REPEAT (eresolve_tac [iffE,disjE,disjI1,disjI2] 1 + ORELSE ares_tac [iffI] 1 + ORELSE mp_tac 1)) ]); + +qed_goal "imp_cong" (the_context ()) + "[| P <-> P'; P' ==> Q <-> Q' |] ==> (P-->Q) <-> (P'-->Q')" + (fn prems => + [ (cut_facts_tac prems 1), + (REPEAT (ares_tac [iffI,impI] 1 + ORELSE etac iffE 1 + ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]); + +qed_goal "iff_cong" (the_context ()) + "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')" + (fn prems => + [ (cut_facts_tac prems 1), + (REPEAT (etac iffE 1 + ORELSE ares_tac [iffI] 1 + ORELSE mp_tac 1)) ]); + +qed_goal "not_cong" (the_context ()) + "P <-> P' ==> ~P <-> ~P'" + (fn prems => + [ (cut_facts_tac prems 1), + (REPEAT (ares_tac [iffI,notI] 1 + ORELSE mp_tac 1 + ORELSE eresolve_tac [iffE,notE] 1)) ]); + +qed_goal "all_cong" (the_context ()) + "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))" + (fn prems => + [ (REPEAT (ares_tac [iffI,allI] 1 + ORELSE mp_tac 1 + ORELSE etac allE 1 ORELSE iff_tac prems 1)) ]); + +qed_goal "ex_cong" (the_context ()) + "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))" + (fn prems => + [ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1 + ORELSE mp_tac 1 + ORELSE iff_tac prems 1)) ]); + +qed_goal "ex1_cong" (the_context ()) + "(!!x. P(x) <-> Q(x)) ==> (EX! x. P(x)) <-> (EX! x. Q(x))" + (fn prems => + [ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1 + ORELSE mp_tac 1 + ORELSE iff_tac prems 1)) ]); + +(*** Equality rules ***) + +qed_goal "sym" (the_context ()) "a=b ==> b=a" + (fn [major] => [ (rtac (major RS subst) 1), (rtac refl 1) ]); + +qed_goal "trans" (the_context ()) "[| a=b; b=c |] ==> a=c" + (fn [prem1,prem2] => [ (rtac (prem2 RS subst) 1), (rtac prem1 1) ]); + +(** ~ b=a ==> ~ a=b **) +val [not_sym] = 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: rule and tactic*) +bind_thm ("ssubst", sym RS subst); + +(*Apply an equality or definition ONCE. + Fails unless the substitution has an effect*) +fun stac th = + let val th' = th RS meta_eq_to_obj_eq handle THM _ => th + in CHANGED_GOAL (rtac (th' RS ssubst)) + end; + +(*A special case of ex1E that would otherwise need quantifier expansion*) +qed_goal "ex1_equalsE" (the_context ()) + "[| EX! x. P(x); P(a); P(b) |] ==> a=b" + (fn prems => + [ (cut_facts_tac prems 1), + (etac ex1E 1), + (rtac trans 1), + (rtac sym 2), + (REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ]); + +(** Polymorphic congruence rules **) + +qed_goal "subst_context" (the_context ()) + "[| a=b |] ==> t(a)=t(b)" + (fn prems=> + [ (resolve_tac (prems RL [ssubst]) 1), + (rtac refl 1) ]); + +qed_goal "subst_context2" (the_context ()) + "[| a=b; c=d |] ==> t(a,c)=t(b,d)" + (fn prems=> + [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]); + +qed_goal "subst_context3" (the_context ()) + "[| a=b; c=d; e=f |] ==> t(a,c,e)=t(b,d,f)" + (fn prems=> + [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]); + +(*Useful with eresolve_tac for proving equalties from known equalities. + a = b + | | + c = d *) +qed_goal "box_equals" (the_context ()) + "[| a=b; a=c; b=d |] ==> c=d" + (fn prems=> + [ (rtac trans 1), + (rtac trans 1), + (rtac sym 1), + (REPEAT (resolve_tac prems 1)) ]); + +(*Dual of box_equals: for proving equalities backwards*) +qed_goal "simp_equals" (the_context ()) + "[| a=c; b=d; c=d |] ==> a=b" + (fn prems=> + [ (rtac trans 1), + (rtac trans 1), + (REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]); + +(** Congruence rules for predicate letters **) + +qed_goal "pred1_cong" (the_context ()) + "a=a' ==> P(a) <-> P(a')" + (fn prems => + [ (cut_facts_tac prems 1), + (rtac iffI 1), + (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); + +qed_goal "pred2_cong" (the_context ()) + "[| a=a'; b=b' |] ==> P(a,b) <-> P(a',b')" + (fn prems => + [ (cut_facts_tac prems 1), + (rtac iffI 1), + (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); + +qed_goal "pred3_cong" (the_context ()) + "[| a=a'; b=b'; c=c' |] ==> P(a,b,c) <-> P(a',b',c')" + (fn prems => + [ (cut_facts_tac prems 1), + (rtac iffI 1), + (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); + +(*special cases for free variables P, Q, R, S -- up to 3 arguments*) + +val pred_congs = + flat (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!*) +val 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) ***) + +qed_goal "conj_impE" (the_context ()) + "[| (P&Q)-->S; P-->(Q-->S) ==> R |] ==> R" + (fn major::prems=> + [ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]); + +qed_goal "disj_impE" (the_context ()) + "[| (P|Q)-->S; [| P-->S; Q-->S |] ==> R |] ==> R" + (fn major::prems=> + [ (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ]); + +(*Simplifies the implication. Classical version is stronger. + Still UNSAFE since Q must be provable -- backtracking needed. *) +qed_goal "imp_impE" (the_context ()) + "[| (P-->Q)-->S; [| P; Q-->S |] ==> Q; S ==> R |] ==> R" + (fn major::prems=> + [ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]); + +(*Simplifies the implication. Classical version is stronger. + Still UNSAFE since ~P must be provable -- backtracking needed. *) +qed_goal "not_impE" (the_context ()) + "[| ~P --> S; P ==> False; S ==> R |] ==> R" + (fn major::prems=> + [ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]); + +(*Simplifies the implication. UNSAFE. *) +qed_goal "iff_impE" (the_context ()) + "[| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P; \ +\ S ==> R |] ==> R" + (fn major::prems=> + [ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]); + +(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) +qed_goal "all_impE" (the_context ()) + "[| (ALL x. P(x))-->S; !!x. P(x); S ==> R |] ==> R" + (fn major::prems=> + [ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]); + +(*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) +qed_goal "ex_impE" (the_context ()) + "[| (EX x. P(x))-->S; P(x)-->S ==> R |] ==> R" + (fn major::prems=> + [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]); + +(*** Courtesy of Krzysztof Grabczewski ***) + +val major::prems = goal (the_context ()) "[| 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"; + + +(** strip ALL and --> from proved goal while preserving ALL-bound var names **) + +fun make_new_spec rl = + (* Use a crazy name to avoid forall_intr failing because of + duplicate variable name *) + let val myspec = read_instantiate [("P","?wlzickd")] rl + val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec; + val cvx = cterm_of (#sign(rep_thm myspec)) vx + in (vxT, forall_intr cvx myspec) end; + +local + +val (specT, spec') = make_new_spec spec + +in + +fun RSspec th = + (case concl_of th of + _ $ (Const("All",_) $ Abs(a,_,_)) => + let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),specT)) + in th RS forall_elim ca spec' end + | _ => raise THM("RSspec",0,[th])); + +fun RSmp th = + (case concl_of th of + _ $ (Const("op -->",_)$_$_) => th RS mp + | _ => raise THM("RSmp",0,[th])); + +fun normalize_thm funs = + let fun trans [] th = th + | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th + in trans funs end; + +fun qed_spec_mp name = + let val thm = normalize_thm [RSspec,RSmp] (result()) + in bind_thm(name, thm) end; + +fun qed_goal_spec_mp name thy s p = + bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p)); + +fun qed_goalw_spec_mp name thy defs s p = + bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p)); + +end; + + +(* attributes *) + +local + +fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x; + +in + +val attrib_setup = + [Attrib.add_attributes + [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]]; + +end; diff -r 358b1c5391f0 -r 4c43090659ca src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Wed Aug 25 20:42:01 1999 +0200 +++ b/src/FOL/IsaMakefile Wed Aug 25 20:45:19 1999 +0200 @@ -30,8 +30,9 @@ $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML \ $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML FOL.ML \ - FOL.thy IFOL.ML IFOL.thy ROOT.ML cladata.ML fologic.ML intprover.ML \ - simpdata.ML + FOL.thy FOL_lemmas1.ML FOL_lemmas2.ML IFOL.ML IFOL.thy \ + IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML fologic.ML \ + hypsubstdata.ML intprover.ML simpdata.ML @$(ISATOOL) usedir -b $(OUT)/Pure FOL diff -r 358b1c5391f0 -r 4c43090659ca src/FOL/ROOT.ML --- a/src/FOL/ROOT.ML Wed Aug 25 20:42:01 1999 +0200 +++ b/src/FOL/ROOT.ML Wed Aug 25 20:45:19 1999 +0200 @@ -1,10 +1,9 @@ -(* Title: FOL/ROOT +(* Title: FOL/ROOT.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -Adds First-Order Logic to a database containing pure Isabelle. -Should be executed in the subdirectory FOL. +First-Order Logic. *) val banner = "First-Order Logic with Natural Deduction"; @@ -23,39 +22,6 @@ use "~~/src/Provers/quantifier1.ML"; use_thy "IFOL"; -use "fologic.ML"; - -(** Applying HypsubstFun to generate hyp_subst_tac **) -structure Hypsubst_Data = - struct - structure Simplifier = Simplifier - (*These destructors Match!*) - fun dest_eq (Const("op =",T) $ t $ u) = (t, u, domain_type T) - val dest_Trueprop = FOLogic.dest_Trueprop - val dest_imp = FOLogic.dest_imp - val eq_reflection = eq_reflection - val imp_intr = impI - val rev_mp = rev_mp - val subst = subst - val sym = sym - val thin_refl = prove_goal IFOL.thy - "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]); - end; - -structure Hypsubst = HypsubstFun(Hypsubst_Data); -open Hypsubst; - - -use "intprover.ML"; - use_thy "FOL"; -use "cladata.ML"; -use "simpdata.ML"; - -qed_goal "ex1_functional" FOL.thy - "!!a b c. [| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c" - (fn _ => [ (Blast_tac 1) ]); - - print_depth 8; diff -r 358b1c5391f0 -r 4c43090659ca src/FOL/blastdata.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/FOL/blastdata.ML Wed Aug 25 20:45:19 1999 +0200 @@ -0,0 +1,20 @@ + +(*** Applying BlastFun to create Blast_tac ***) +structure Blast_Data = + struct + type claset = Cla.claset + val notE = notE + val ccontr = ccontr + val contr_tac = Cla.contr_tac + val dup_intr = Cla.dup_intr + val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac + val claset = Cla.claset + val rep_cs = Cla.rep_cs + val cla_modifiers = Cla.cla_modifiers; + val cla_meth' = Cla.cla_meth' + end; + +structure Blast = BlastFun(Blast_Data); + +val Blast_tac = Blast.Blast_tac +and blast_tac = Blast.blast_tac; diff -r 358b1c5391f0 -r 4c43090659ca src/FOL/cladata.ML --- a/src/FOL/cladata.ML Wed Aug 25 20:42:01 1999 +0200 +++ b/src/FOL/cladata.ML Wed Aug 25 20:45:19 1999 +0200 @@ -3,10 +3,9 @@ Author: Tobias Nipkow Copyright 1996 University of Cambridge -Setting up the classical reasoner +Setting up the classical reasoner. *) - section "Classical Reasoner"; @@ -24,6 +23,7 @@ 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); \ @@ -44,25 +44,4 @@ val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] addSEs [exE,alt_ex1E] addEs [allE]; -claset_ref() := FOL_cs; - - -(*** Applying BlastFun to create Blast_tac ***) -structure Blast_Data = - struct - type claset = Cla.claset - val notE = notE - val ccontr = ccontr - val contr_tac = Cla.contr_tac - val dup_intr = Cla.dup_intr - val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac - val claset = Cla.claset - val rep_cs = Cla.rep_cs - val cla_modifiers = Cla.cla_modifiers; - val cla_meth' = Cla.cla_meth' - end; - -structure Blast = BlastFun(Blast_Data); - -val Blast_tac = Blast.Blast_tac -and blast_tac = Blast.blast_tac; +val clasetup = [fn thy => (claset_ref_of thy := FOL_cs; thy)]; diff -r 358b1c5391f0 -r 4c43090659ca src/FOL/hypsubstdata.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/FOL/hypsubstdata.ML Wed Aug 25 20:45:19 1999 +0200 @@ -0,0 +1,20 @@ + +(** Applying HypsubstFun to generate hyp_subst_tac **) +structure Hypsubst_Data = + struct + structure Simplifier = Simplifier + (*These destructors Match!*) + fun dest_eq (Const("op =",T) $ t $ u) = (t, u, domain_type T) + val dest_Trueprop = FOLogic.dest_Trueprop + val dest_imp = FOLogic.dest_imp + val eq_reflection = eq_reflection + 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]); + end; + +structure Hypsubst = HypsubstFun(Hypsubst_Data); +open Hypsubst; diff -r 358b1c5391f0 -r 4c43090659ca src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Wed Aug 25 20:42:01 1999 +0200 +++ b/src/FOL/simpdata.ML Wed Aug 25 20:45:19 1999 +0200 @@ -127,7 +127,7 @@ fun prove_fun s = (writeln s; - prove_goal FOL.thy s + prove_goal (the_context ()) s (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOL_cs 1) ])); @@ -177,7 +177,7 @@ (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ]); -fun prove nm thm = qed_goal nm FOL.thy thm (fn _ => [Blast_tac 1]); +fun prove nm thm = qed_goal nm (the_context ()) thm (fn _ => [Blast_tac 1]); int_prove "conj_commute" "P&Q <-> Q&P"; int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)"; @@ -242,11 +242,12 @@ end); local + val ex_pattern = - read_cterm (Theory.sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT) + read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)", FOLogic.oT) val all_pattern = - read_cterm (Theory.sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT) + read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT) in val defEX_regroup = @@ -348,8 +349,7 @@ (*classical simprules too*) val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps); -simpset_ref() := FOL_ss; - +val simpsetup = [fn thy => (simpset_ref_of thy := FOL_ss; thy)]; (*** integration of simplifier with classical reasoner ***)