--- 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