summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/FOL/IFOL.thy

changeset 21539 | c5cf9243ad62 |

parent 21524 | 7843e2fd14a9 |

child 22139 | 539a63b98f76 |

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