--- 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))) ]);
-
--- 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
--- /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))) ]);
--- /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";
--- 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;
--- 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 ("\\<not> _" [40] 40)
- "op &" :: [o, o] => o (infixr "\\<and>" 35)
- "op |" :: [o, o] => o (infixr "\\<or>" 30)
- "op -->" :: [o, o] => o (infixr "\\<midarrow>\\<rightarrow>" 25)
- "op <->" :: [o, o] => o (infixr "\\<leftarrow>\\<rightarrow>" 25)
- "ALL " :: [idts, o] => o ("(3\\<forall>_./ _)" [0, 10] 10)
- "EX " :: [idts, o] => o ("(3\\<exists>_./ _)" [0, 10] 10)
- "EX! " :: [idts, o] => o ("(3\\<exists>!_./ _)" [0, 10] 10)
- "op ~=" :: ['a, 'a] => o (infixl "\\<noteq>" 50)
+ Not :: "o => o" ("\\<not> _" [40] 40)
+ "op &" :: "[o, o] => o" (infixr "\\<and>" 35)
+ "op |" :: "[o, o] => o" (infixr "\\<or>" 30)
+ "op -->" :: "[o, o] => o" (infixr "\\<midarrow>\\<rightarrow>" 25)
+ "op <->" :: "[o, o] => o" (infixr "\\<leftarrow>\\<rightarrow>" 25)
+ "ALL " :: "[idts, o] => o" ("(3\\<forall>_./ _)" [0, 10] 10)
+ "EX " :: "[idts, o] => o" ("(3\\<exists>_./ _)" [0, 10] 10)
+ "EX! " :: "[idts, o] => o" ("(3\\<exists>!_./ _)" [0, 10] 10)
+ "op ~=" :: "['a, 'a] => o" (infixl "\\<noteq>" 50)
syntax (xsymbols)
- "op -->" :: [o, o] => o (infixr "\\<longrightarrow>" 25)
- "op <->" :: [o, o] => o (infixr "\\<longleftrightarrow>" 25)
+ "op -->" :: "[o, o] => o" (infixr "\\<longrightarrow>" 25)
+ "op <->" :: "[o, o] => o" (infixr "\\<longleftrightarrow>" 25)
syntax (HTML output)
- Not :: o => o ("\\<not> _" [40] 40)
+ Not :: "o => o" ("\\<not> _" [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
--- /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;
--- 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
--- 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;
--- /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;
--- 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)];
--- /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;
--- 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 ***)