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