clasohm@1268: (* Title: FOL/IFOL.thy wenzelm@11677: Author: Lawrence C Paulson and Markus Wenzel wenzelm@11677: *) lcp@35: wenzelm@11677: header {* Intuitionistic first-order logic *} lcp@35: paulson@15481: theory IFOL paulson@15481: imports Pure paulson@15481: begin wenzelm@7355: wenzelm@48891: ML_file "~~/src/Tools/misc_legacy.ML" wenzelm@48891: ML_file "~~/src/Provers/splitter.ML" wenzelm@48891: ML_file "~~/src/Provers/hypsubst.ML" wenzelm@48891: ML_file "~~/src/Tools/IsaPlanner/zipper.ML" wenzelm@48891: ML_file "~~/src/Tools/IsaPlanner/isand.ML" wenzelm@48891: ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML" wenzelm@48891: ML_file "~~/src/Provers/quantifier1.ML" wenzelm@48891: ML_file "~~/src/Tools/intuitionistic.ML" wenzelm@48891: ML_file "~~/src/Tools/project_rule.ML" wenzelm@48891: ML_file "~~/src/Tools/atomize_elim.ML" wenzelm@48891: clasohm@0: wenzelm@11677: subsection {* Syntax and axiomatic basis *} wenzelm@11677: wenzelm@39557: setup Pure_Thy.old_appl_syntax_setup wenzelm@26956: wenzelm@55380: class "term" wenzelm@36452: default_sort "term" clasohm@0: wenzelm@7355: typedecl o wenzelm@79: wenzelm@11747: judgment wenzelm@11747: Trueprop :: "o => prop" ("(_)" 5) clasohm@0: wenzelm@79: wenzelm@46972: subsubsection {* Equality *} lcp@35: wenzelm@46972: axiomatization wenzelm@46972: eq :: "['a, 'a] => o" (infixl "=" 50) wenzelm@46972: where wenzelm@46972: refl: "a=a" and wenzelm@46972: subst: "a=b \ P(a) \ P(b)" wenzelm@79: clasohm@0: wenzelm@46972: subsubsection {* Propositional logic *} wenzelm@46972: wenzelm@46972: axiomatization wenzelm@46972: False :: o and wenzelm@46972: conj :: "[o, o] => o" (infixr "&" 35) and wenzelm@46972: disj :: "[o, o] => o" (infixr "|" 30) and wenzelm@46972: imp :: "[o, o] => o" (infixr "-->" 25) wenzelm@46972: where wenzelm@46972: conjI: "[| P; Q |] ==> P&Q" and wenzelm@46972: conjunct1: "P&Q ==> P" and wenzelm@46972: conjunct2: "P&Q ==> Q" and wenzelm@46972: wenzelm@46972: disjI1: "P ==> P|Q" and wenzelm@46972: disjI2: "Q ==> P|Q" and wenzelm@46972: disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" and wenzelm@46972: wenzelm@46972: impI: "(P ==> Q) ==> P-->Q" and wenzelm@46972: mp: "[| P-->Q; P |] ==> Q" and wenzelm@46972: wenzelm@46972: FalseE: "False ==> P" wenzelm@46972: wenzelm@46972: wenzelm@46972: subsubsection {* Quantifiers *} wenzelm@46972: wenzelm@46972: axiomatization wenzelm@46972: All :: "('a => o) => o" (binder "ALL " 10) and wenzelm@46972: Ex :: "('a => o) => o" (binder "EX " 10) wenzelm@46972: where wenzelm@46972: allI: "(!!x. P(x)) ==> (ALL x. P(x))" and wenzelm@46972: spec: "(ALL x. P(x)) ==> P(x)" and wenzelm@46972: exI: "P(x) ==> (EX x. P(x))" and wenzelm@46972: exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" wenzelm@46972: wenzelm@46972: wenzelm@46972: subsubsection {* Definitions *} wenzelm@46972: wenzelm@46972: definition "True == False-->False" wenzelm@46972: definition Not ("~ _" [40] 40) where not_def: "~P == P-->False" wenzelm@46972: definition iff (infixr "<->" 25) where "P<->Q == (P-->Q) & (Q-->P)" wenzelm@46972: wenzelm@46972: definition Ex1 :: "('a => o) => o" (binder "EX! " 10) wenzelm@46972: where ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)" wenzelm@46972: wenzelm@46972: axiomatization where -- {* Reflection, admissible *} wenzelm@46972: eq_reflection: "(x=y) ==> (x==y)" and wenzelm@46972: iff_reflection: "(P<->Q) ==> (P==Q)" wenzelm@46972: wenzelm@46972: wenzelm@46972: subsubsection {* Additional notation *} wenzelm@46972: wenzelm@46972: abbreviation not_equal :: "['a, 'a] => o" (infixl "~=" 50) wenzelm@46972: where "x ~= y == ~ (x = y)" wenzelm@79: wenzelm@21210: notation (xsymbols) wenzelm@19656: not_equal (infixl "\" 50) wenzelm@19363: wenzelm@21210: notation (HTML output) wenzelm@19656: not_equal (infixl "\" 50) wenzelm@19363: wenzelm@21524: notation (xsymbols) wenzelm@46972: Not ("\ _" [40] 40) and wenzelm@46972: conj (infixr "\" 35) and wenzelm@46972: disj (infixr "\" 30) and wenzelm@46972: All (binder "\" 10) and wenzelm@46972: Ex (binder "\" 10) and wenzelm@46972: Ex1 (binder "\!" 10) and wenzelm@46972: imp (infixr "\" 25) and wenzelm@46972: iff (infixr "\" 25) lcp@35: wenzelm@21524: notation (HTML output) wenzelm@46972: Not ("\ _" [40] 40) and wenzelm@46972: conj (infixr "\" 35) and wenzelm@46972: disj (infixr "\" 30) and wenzelm@46972: All (binder "\" 10) and wenzelm@46972: Ex (binder "\" 10) and wenzelm@46972: Ex1 (binder "\!" 10) paulson@14236: paulson@13779: wenzelm@11677: subsection {* Lemmas and proof tools *} wenzelm@11677: wenzelm@46972: lemmas strip = impI allI wenzelm@46972: wenzelm@21539: lemma TrueI: True wenzelm@21539: unfolding True_def by (rule impI) wenzelm@21539: wenzelm@21539: wenzelm@21539: (*** Sequent-style elimination rules for & --> and ALL ***) wenzelm@21539: wenzelm@21539: lemma conjE: wenzelm@21539: assumes major: "P & Q" wenzelm@21539: and r: "[| P; Q |] ==> R" wenzelm@21539: shows R wenzelm@21539: apply (rule r) wenzelm@21539: apply (rule major [THEN conjunct1]) wenzelm@21539: apply (rule major [THEN conjunct2]) wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma impE: wenzelm@21539: assumes major: "P --> Q" wenzelm@21539: and P wenzelm@21539: and r: "Q ==> R" wenzelm@21539: shows R wenzelm@21539: apply (rule r) wenzelm@21539: apply (rule major [THEN mp]) wenzelm@21539: apply (rule `P`) wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma allE: wenzelm@21539: assumes major: "ALL x. P(x)" wenzelm@21539: and r: "P(x) ==> R" wenzelm@21539: shows R wenzelm@21539: apply (rule r) wenzelm@21539: apply (rule major [THEN spec]) wenzelm@21539: done wenzelm@21539: wenzelm@21539: (*Duplicates the quantifier; for use with eresolve_tac*) wenzelm@21539: lemma all_dupE: wenzelm@21539: assumes major: "ALL x. P(x)" wenzelm@21539: and r: "[| P(x); ALL x. P(x) |] ==> R" wenzelm@21539: shows R wenzelm@21539: apply (rule r) wenzelm@21539: apply (rule major [THEN spec]) wenzelm@21539: apply (rule major) wenzelm@21539: done wenzelm@21539: wenzelm@21539: wenzelm@21539: (*** Negation rules, which translate between ~P and P-->False ***) wenzelm@21539: wenzelm@21539: lemma notI: "(P ==> False) ==> ~P" wenzelm@21539: unfolding not_def by (erule impI) wenzelm@21539: wenzelm@21539: lemma notE: "[| ~P; P |] ==> R" wenzelm@21539: unfolding not_def by (erule mp [THEN FalseE]) wenzelm@21539: wenzelm@21539: lemma rev_notE: "[| P; ~P |] ==> R" wenzelm@21539: by (erule notE) wenzelm@21539: wenzelm@21539: (*This is useful with the special implication rules for each kind of P. *) wenzelm@21539: lemma not_to_imp: wenzelm@21539: assumes "~P" wenzelm@21539: and r: "P --> False ==> Q" wenzelm@21539: shows Q wenzelm@21539: apply (rule r) wenzelm@21539: apply (rule impI) wenzelm@21539: apply (erule notE [OF `~P`]) wenzelm@21539: done wenzelm@21539: wenzelm@21539: (* For substitution into an assumption P, reduce Q to P-->Q, substitute into wenzelm@27150: this implication, then apply impI to move P back into the assumptions.*) wenzelm@21539: lemma rev_mp: "[| P; P --> Q |] ==> Q" wenzelm@21539: by (erule mp) wenzelm@21539: wenzelm@21539: (*Contrapositive of an inference rule*) wenzelm@21539: lemma contrapos: wenzelm@21539: assumes major: "~Q" wenzelm@21539: and minor: "P ==> Q" wenzelm@21539: shows "~P" wenzelm@21539: apply (rule major [THEN notE, THEN notI]) wenzelm@21539: apply (erule minor) wenzelm@21539: done wenzelm@21539: wenzelm@21539: wenzelm@21539: (*** Modus Ponens Tactics ***) wenzelm@21539: wenzelm@21539: (*Finds P-->Q and P in the assumptions, replaces implication by Q *) wenzelm@21539: ML {* wenzelm@22139: fun mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN assume_tac i wenzelm@22139: fun eq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN eq_assume_tac i wenzelm@21539: *} wenzelm@21539: wenzelm@21539: wenzelm@21539: (*** If-and-only-if ***) wenzelm@21539: wenzelm@21539: lemma iffI: "[| P ==> Q; Q ==> P |] ==> P<->Q" wenzelm@21539: apply (unfold iff_def) wenzelm@21539: apply (rule conjI) wenzelm@21539: apply (erule impI) wenzelm@21539: apply (erule impI) wenzelm@21539: done wenzelm@21539: wenzelm@21539: wenzelm@21539: lemma iffE: wenzelm@21539: assumes major: "P <-> Q" wenzelm@21539: and r: "P-->Q ==> Q-->P ==> R" wenzelm@21539: shows R wenzelm@21539: apply (insert major, unfold iff_def) wenzelm@21539: apply (erule conjE) wenzelm@21539: apply (erule r) wenzelm@21539: apply assumption wenzelm@21539: done wenzelm@21539: wenzelm@21539: (* Destruct rules for <-> similar to Modus Ponens *) wenzelm@21539: wenzelm@21539: lemma iffD1: "[| P <-> Q; P |] ==> Q" wenzelm@21539: apply (unfold iff_def) wenzelm@21539: apply (erule conjunct1 [THEN mp]) wenzelm@21539: apply assumption wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma iffD2: "[| P <-> Q; Q |] ==> P" wenzelm@21539: apply (unfold iff_def) wenzelm@21539: apply (erule conjunct2 [THEN mp]) wenzelm@21539: apply assumption wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma rev_iffD1: "[| P; P <-> Q |] ==> Q" wenzelm@21539: apply (erule iffD1) wenzelm@21539: apply assumption wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma rev_iffD2: "[| Q; P <-> Q |] ==> P" wenzelm@21539: apply (erule iffD2) wenzelm@21539: apply assumption wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma iff_refl: "P <-> P" wenzelm@21539: by (rule iffI) wenzelm@21539: wenzelm@21539: lemma iff_sym: "Q <-> P ==> P <-> Q" wenzelm@21539: apply (erule iffE) wenzelm@21539: apply (rule iffI) wenzelm@21539: apply (assumption | erule mp)+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma iff_trans: "[| P <-> Q; Q<-> R |] ==> P <-> R" wenzelm@21539: apply (rule iffI) wenzelm@21539: apply (assumption | erule iffE | erule (1) notE impE)+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: wenzelm@21539: (*** Unique existence. NOTE THAT the following 2 quantifications wenzelm@21539: EX!x such that [EX!y such that P(x,y)] (sequential) wenzelm@21539: EX!x,y such that P(x,y) (simultaneous) wenzelm@21539: do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. wenzelm@21539: ***) wenzelm@21539: wenzelm@21539: lemma ex1I: wenzelm@23393: "P(a) \ (!!x. P(x) ==> x=a) \ EX! x. P(x)" wenzelm@21539: apply (unfold ex1_def) wenzelm@23393: apply (assumption | rule exI conjI allI impI)+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: (*Sometimes easier to use: the premises have no shared variables. Safe!*) wenzelm@21539: lemma ex_ex1I: wenzelm@23393: "EX x. P(x) \ (!!x y. [| P(x); P(y) |] ==> x=y) \ EX! x. P(x)" wenzelm@23393: apply (erule exE) wenzelm@23393: apply (rule ex1I) wenzelm@23393: apply assumption wenzelm@23393: apply assumption wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma ex1E: wenzelm@23393: "EX! x. P(x) \ (!!x. [| P(x); ALL y. P(y) --> y=x |] ==> R) \ R" wenzelm@23393: apply (unfold ex1_def) wenzelm@21539: apply (assumption | erule exE conjE)+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: wenzelm@21539: (*** <-> congruence rules for simplification ***) wenzelm@21539: wenzelm@21539: (*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*) wenzelm@21539: ML {* wenzelm@22139: fun iff_tac prems i = wenzelm@22139: resolve_tac (prems RL @{thms iffE}) i THEN wenzelm@22139: REPEAT1 (eresolve_tac [@{thm asm_rl}, @{thm mp}] i) wenzelm@21539: *} wenzelm@21539: wenzelm@21539: lemma conj_cong: wenzelm@21539: assumes "P <-> P'" wenzelm@21539: and "P' ==> Q <-> Q'" wenzelm@21539: shows "(P&Q) <-> (P'&Q')" wenzelm@21539: apply (insert assms) wenzelm@21539: apply (assumption | rule iffI conjI | erule iffE conjE mp | wenzelm@39159: tactic {* iff_tac @{thms assms} 1 *})+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: (*Reversed congruence rule! Used in ZF/Order*) wenzelm@21539: lemma conj_cong2: wenzelm@21539: assumes "P <-> P'" wenzelm@21539: and "P' ==> Q <-> Q'" wenzelm@21539: shows "(Q&P) <-> (Q'&P')" wenzelm@21539: apply (insert assms) wenzelm@21539: apply (assumption | rule iffI conjI | erule iffE conjE mp | wenzelm@39159: tactic {* iff_tac @{thms assms} 1 *})+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma disj_cong: wenzelm@21539: assumes "P <-> P'" and "Q <-> Q'" wenzelm@21539: shows "(P|Q) <-> (P'|Q')" wenzelm@21539: apply (insert assms) wenzelm@21539: apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | erule (1) notE impE)+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma imp_cong: wenzelm@21539: assumes "P <-> P'" wenzelm@21539: and "P' ==> Q <-> Q'" wenzelm@21539: shows "(P-->Q) <-> (P'-->Q')" wenzelm@21539: apply (insert assms) wenzelm@21539: apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | wenzelm@39159: tactic {* iff_tac @{thms assms} 1 *})+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma iff_cong: "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')" wenzelm@21539: apply (erule iffE | assumption | rule iffI | erule (1) notE impE)+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma not_cong: "P <-> P' ==> ~P <-> ~P'" wenzelm@21539: apply (assumption | rule iffI notI | erule (1) notE impE | erule iffE notE)+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma all_cong: wenzelm@21539: assumes "!!x. P(x) <-> Q(x)" wenzelm@21539: shows "(ALL x. P(x)) <-> (ALL x. Q(x))" wenzelm@21539: apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | wenzelm@39159: tactic {* iff_tac @{thms assms} 1 *})+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma ex_cong: wenzelm@21539: assumes "!!x. P(x) <-> Q(x)" wenzelm@21539: shows "(EX x. P(x)) <-> (EX x. Q(x))" wenzelm@21539: apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | wenzelm@39159: tactic {* iff_tac @{thms assms} 1 *})+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma ex1_cong: wenzelm@21539: assumes "!!x. P(x) <-> Q(x)" wenzelm@21539: shows "(EX! x. P(x)) <-> (EX! x. Q(x))" wenzelm@21539: apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | wenzelm@39159: tactic {* iff_tac @{thms assms} 1 *})+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: (*** Equality rules ***) wenzelm@21539: wenzelm@21539: lemma sym: "a=b ==> b=a" wenzelm@21539: apply (erule subst) wenzelm@21539: apply (rule refl) wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma trans: "[| a=b; b=c |] ==> a=c" wenzelm@21539: apply (erule subst, assumption) wenzelm@21539: done wenzelm@21539: wenzelm@21539: (** **) wenzelm@21539: lemma not_sym: "b ~= a ==> a ~= b" wenzelm@21539: apply (erule contrapos) wenzelm@21539: apply (erule sym) wenzelm@21539: done wenzelm@21539: wenzelm@21539: (* Two theorms for rewriting only one instance of a definition: wenzelm@21539: the first for definitions of formulae and the second for terms *) wenzelm@21539: wenzelm@21539: lemma def_imp_iff: "(A == B) ==> A <-> B" wenzelm@21539: apply unfold wenzelm@21539: apply (rule iff_refl) wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma meta_eq_to_obj_eq: "(A == B) ==> A = B" wenzelm@21539: apply unfold wenzelm@21539: apply (rule refl) wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma meta_eq_to_iff: "x==y ==> x<->y" wenzelm@21539: by unfold (rule iff_refl) wenzelm@21539: wenzelm@21539: (*substitution*) wenzelm@21539: lemma ssubst: "[| b = a; P(a) |] ==> P(b)" wenzelm@21539: apply (drule sym) wenzelm@21539: apply (erule (1) subst) wenzelm@21539: done wenzelm@21539: wenzelm@21539: (*A special case of ex1E that would otherwise need quantifier expansion*) wenzelm@21539: lemma ex1_equalsE: wenzelm@21539: "[| EX! x. P(x); P(a); P(b) |] ==> a=b" wenzelm@21539: apply (erule ex1E) wenzelm@21539: apply (rule trans) wenzelm@21539: apply (rule_tac [2] sym) wenzelm@21539: apply (assumption | erule spec [THEN mp])+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: (** Polymorphic congruence rules **) wenzelm@21539: wenzelm@21539: lemma subst_context: "[| a=b |] ==> t(a)=t(b)" wenzelm@21539: apply (erule ssubst) wenzelm@21539: apply (rule refl) wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma subst_context2: "[| a=b; c=d |] ==> t(a,c)=t(b,d)" wenzelm@21539: apply (erule ssubst)+ wenzelm@21539: apply (rule refl) wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma subst_context3: "[| a=b; c=d; e=f |] ==> t(a,c,e)=t(b,d,f)" wenzelm@21539: apply (erule ssubst)+ wenzelm@21539: apply (rule refl) wenzelm@21539: done wenzelm@21539: wenzelm@21539: (*Useful with eresolve_tac for proving equalties from known equalities. wenzelm@21539: a = b wenzelm@21539: | | wenzelm@21539: c = d *) wenzelm@21539: lemma box_equals: "[| a=b; a=c; b=d |] ==> c=d" wenzelm@21539: apply (rule trans) wenzelm@21539: apply (rule trans) wenzelm@21539: apply (rule sym) wenzelm@21539: apply assumption+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: (*Dual of box_equals: for proving equalities backwards*) wenzelm@21539: lemma simp_equals: "[| a=c; b=d; c=d |] ==> a=b" wenzelm@21539: apply (rule trans) wenzelm@21539: apply (rule trans) wenzelm@21539: apply assumption+ wenzelm@21539: apply (erule sym) wenzelm@21539: done wenzelm@21539: wenzelm@21539: (** Congruence rules for predicate letters **) wenzelm@21539: wenzelm@21539: lemma pred1_cong: "a=a' ==> P(a) <-> P(a')" wenzelm@21539: apply (rule iffI) wenzelm@21539: apply (erule (1) subst) wenzelm@21539: apply (erule (1) ssubst) wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma pred2_cong: "[| a=a'; b=b' |] ==> P(a,b) <-> P(a',b')" wenzelm@21539: apply (rule iffI) wenzelm@21539: apply (erule subst)+ wenzelm@21539: apply assumption wenzelm@21539: apply (erule ssubst)+ wenzelm@21539: apply assumption wenzelm@21539: done wenzelm@21539: wenzelm@21539: lemma pred3_cong: "[| a=a'; b=b'; c=c' |] ==> P(a,b,c) <-> P(a',b',c')" wenzelm@21539: apply (rule iffI) wenzelm@21539: apply (erule subst)+ wenzelm@21539: apply assumption wenzelm@21539: apply (erule ssubst)+ wenzelm@21539: apply assumption wenzelm@21539: done wenzelm@21539: wenzelm@21539: (*special case for the equality predicate!*) wenzelm@21539: lemma eq_cong: "[| a = a'; b = b' |] ==> a = b <-> a' = b'" wenzelm@21539: apply (erule (1) pred2_cong) wenzelm@21539: done wenzelm@21539: wenzelm@21539: wenzelm@21539: (*** Simplifications of assumed implications. wenzelm@21539: Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE wenzelm@21539: used with mp_tac (restricted to atomic formulae) is COMPLETE for wenzelm@21539: intuitionistic propositional logic. See wenzelm@21539: R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic wenzelm@21539: (preprint, University of St Andrews, 1991) ***) wenzelm@21539: wenzelm@21539: lemma conj_impE: wenzelm@21539: assumes major: "(P&Q)-->S" wenzelm@21539: and r: "P-->(Q-->S) ==> R" wenzelm@21539: shows R wenzelm@21539: by (assumption | rule conjI impI major [THEN mp] r)+ wenzelm@21539: wenzelm@21539: lemma disj_impE: wenzelm@21539: assumes major: "(P|Q)-->S" wenzelm@21539: and r: "[| P-->S; Q-->S |] ==> R" wenzelm@21539: shows R wenzelm@21539: by (assumption | rule disjI1 disjI2 impI major [THEN mp] r)+ wenzelm@21539: wenzelm@21539: (*Simplifies the implication. Classical version is stronger. wenzelm@21539: Still UNSAFE since Q must be provable -- backtracking needed. *) wenzelm@21539: lemma imp_impE: wenzelm@21539: assumes major: "(P-->Q)-->S" wenzelm@21539: and r1: "[| P; Q-->S |] ==> Q" wenzelm@21539: and r2: "S ==> R" wenzelm@21539: shows R wenzelm@21539: by (assumption | rule impI major [THEN mp] r1 r2)+ wenzelm@21539: wenzelm@21539: (*Simplifies the implication. Classical version is stronger. wenzelm@21539: Still UNSAFE since ~P must be provable -- backtracking needed. *) wenzelm@21539: lemma not_impE: wenzelm@23393: "~P --> S \ (P ==> False) \ (S ==> R) \ R" wenzelm@23393: apply (drule mp) wenzelm@23393: apply (rule notI) wenzelm@23393: apply assumption wenzelm@23393: apply assumption wenzelm@21539: done wenzelm@21539: wenzelm@21539: (*Simplifies the implication. UNSAFE. *) wenzelm@21539: lemma iff_impE: wenzelm@21539: assumes major: "(P<->Q)-->S" wenzelm@21539: and r1: "[| P; Q-->S |] ==> Q" wenzelm@21539: and r2: "[| Q; P-->S |] ==> P" wenzelm@21539: and r3: "S ==> R" wenzelm@21539: shows R wenzelm@21539: apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) wenzelm@21539: lemma all_impE: wenzelm@21539: assumes major: "(ALL x. P(x))-->S" wenzelm@21539: and r1: "!!x. P(x)" wenzelm@21539: and r2: "S ==> R" wenzelm@21539: shows R wenzelm@23393: apply (rule allI impI major [THEN mp] r1 r2)+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: (*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) wenzelm@21539: lemma ex_impE: wenzelm@21539: assumes major: "(EX x. P(x))-->S" wenzelm@21539: and r: "P(x)-->S ==> R" wenzelm@21539: shows R wenzelm@21539: apply (assumption | rule exI impI major [THEN mp] r)+ wenzelm@21539: done wenzelm@21539: wenzelm@21539: (*** Courtesy of Krzysztof Grabczewski ***) wenzelm@21539: wenzelm@21539: lemma disj_imp_disj: wenzelm@23393: "P|Q \ (P==>R) \ (Q==>S) \ R|S" wenzelm@23393: apply (erule disjE) wenzelm@21539: apply (rule disjI1) apply assumption wenzelm@21539: apply (rule disjI2) apply assumption wenzelm@21539: done wenzelm@11734: wenzelm@18481: ML {* wenzelm@32172: structure Project_Rule = Project_Rule wenzelm@32172: ( wenzelm@22139: val conjunct1 = @{thm conjunct1} wenzelm@22139: val conjunct2 = @{thm conjunct2} wenzelm@22139: val mp = @{thm mp} wenzelm@32172: ) wenzelm@18481: *} wenzelm@18481: wenzelm@48891: ML_file "fologic.ML" wenzelm@21539: wenzelm@42303: lemma thin_refl: "[|x=x; PROP W|] ==> PROP W" . wenzelm@21539: wenzelm@42799: ML {* wenzelm@42799: structure Hypsubst = Hypsubst wenzelm@42799: ( wenzelm@42799: val dest_eq = FOLogic.dest_eq wenzelm@42799: val dest_Trueprop = FOLogic.dest_Trueprop wenzelm@42799: val dest_imp = FOLogic.dest_imp wenzelm@42799: val eq_reflection = @{thm eq_reflection} wenzelm@42799: val rev_eq_reflection = @{thm meta_eq_to_obj_eq} wenzelm@42799: val imp_intr = @{thm impI} wenzelm@42799: val rev_mp = @{thm rev_mp} wenzelm@42799: val subst = @{thm subst} wenzelm@42799: val sym = @{thm sym} wenzelm@42799: val thin_refl = @{thm thin_refl} wenzelm@42799: ); wenzelm@42799: open Hypsubst; wenzelm@42799: *} wenzelm@42799: wenzelm@9886: setup hypsubst_setup wenzelm@48891: ML_file "intprover.ML" wenzelm@7355: wenzelm@4092: wenzelm@12875: subsection {* Intuitionistic Reasoning *} wenzelm@12368: wenzelm@31299: setup {* Intuitionistic.method_setup @{binding iprover} *} wenzelm@30165: wenzelm@12349: lemma impE': wenzelm@12937: assumes 1: "P --> Q" wenzelm@12937: and 2: "Q ==> R" wenzelm@12937: and 3: "P --> Q ==> P" wenzelm@12937: shows R wenzelm@12349: proof - wenzelm@12349: from 3 and 1 have P . wenzelm@12368: with 1 have Q by (rule impE) wenzelm@12349: with 2 show R . wenzelm@12349: qed wenzelm@12349: wenzelm@12349: lemma allE': wenzelm@12937: assumes 1: "ALL x. P(x)" wenzelm@12937: and 2: "P(x) ==> ALL x. P(x) ==> Q" wenzelm@12937: shows Q wenzelm@12349: proof - wenzelm@12349: from 1 have "P(x)" by (rule spec) wenzelm@12349: from this and 1 show Q by (rule 2) wenzelm@12349: qed wenzelm@12349: wenzelm@12937: lemma notE': wenzelm@12937: assumes 1: "~ P" wenzelm@12937: and 2: "~ P ==> P" wenzelm@12937: shows R wenzelm@12349: proof - wenzelm@12349: from 2 and 1 have P . wenzelm@12349: with 1 show R by (rule notE) wenzelm@12349: qed wenzelm@12349: wenzelm@12349: lemmas [Pure.elim!] = disjE iffE FalseE conjE exE wenzelm@12349: and [Pure.intro!] = iffI conjI impI TrueI notI allI refl wenzelm@12349: and [Pure.elim 2] = allE notE' impE' wenzelm@12349: and [Pure.intro] = exI disjI2 disjI1 wenzelm@12349: wenzelm@51798: setup {* Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac) *} wenzelm@12349: wenzelm@12349: wenzelm@12368: lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)" nipkow@17591: by iprover wenzelm@12368: wenzelm@12368: lemmas [sym] = sym iff_sym not_sym iff_not_sym wenzelm@12368: and [Pure.elim?] = iffD1 iffD2 impE wenzelm@12368: wenzelm@12368: paulson@13435: lemma eq_commute: "a=b <-> b=a" paulson@13435: apply (rule iffI) paulson@13435: apply (erule sym)+ paulson@13435: done paulson@13435: paulson@13435: wenzelm@11677: subsection {* Atomizing meta-level rules *} wenzelm@11677: wenzelm@11747: lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" wenzelm@11976: proof wenzelm@11677: assume "!!x. P(x)" wenzelm@22931: then show "ALL x. P(x)" .. wenzelm@11677: next wenzelm@11677: assume "ALL x. P(x)" wenzelm@22931: then show "!!x. P(x)" .. wenzelm@11677: qed wenzelm@11677: wenzelm@11747: lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)" wenzelm@11976: proof wenzelm@12368: assume "A ==> B" wenzelm@22931: then show "A --> B" .. wenzelm@11677: next wenzelm@11677: assume "A --> B" and A wenzelm@22931: then show B by (rule mp) wenzelm@11677: qed wenzelm@11677: wenzelm@11747: lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" wenzelm@11976: proof wenzelm@11677: assume "x == y" wenzelm@22931: show "x = y" unfolding `x == y` by (rule refl) wenzelm@11677: next wenzelm@11677: assume "x = y" wenzelm@22931: then show "x == y" by (rule eq_reflection) wenzelm@11677: qed wenzelm@11677: wenzelm@18813: lemma atomize_iff [atomize]: "(A == B) == Trueprop (A <-> B)" wenzelm@18813: proof wenzelm@18813: assume "A == B" wenzelm@22931: show "A <-> B" unfolding `A == B` by (rule iff_refl) wenzelm@18813: next wenzelm@18813: assume "A <-> B" wenzelm@22931: then show "A == B" by (rule iff_reflection) wenzelm@18813: qed wenzelm@18813: wenzelm@28856: lemma atomize_conj [atomize]: "(A &&& B) == Trueprop (A & B)" wenzelm@11976: proof wenzelm@28856: assume conj: "A &&& B" wenzelm@19120: show "A & B" wenzelm@19120: proof (rule conjI) wenzelm@19120: from conj show A by (rule conjunctionD1) wenzelm@19120: from conj show B by (rule conjunctionD2) wenzelm@19120: qed wenzelm@11953: next wenzelm@19120: assume conj: "A & B" wenzelm@28856: show "A &&& B" wenzelm@19120: proof - wenzelm@19120: from conj show A .. wenzelm@19120: from conj show B .. wenzelm@11953: qed wenzelm@11953: qed wenzelm@11953: wenzelm@12368: lemmas [symmetric, rulify] = atomize_all atomize_imp wenzelm@18861: and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff wenzelm@11771: wenzelm@11848: krauss@26580: subsection {* Atomizing elimination rules *} krauss@26580: krauss@26580: lemma atomize_exL[atomize_elim]: "(!!x. P(x) ==> Q) == ((EX x. P(x)) ==> Q)" wenzelm@57948: by rule iprover+ krauss@26580: krauss@26580: lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)" wenzelm@57948: by rule iprover+ krauss@26580: krauss@26580: lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A | B ==> C) ==> C)" wenzelm@57948: by rule iprover+ krauss@26580: krauss@26580: lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop(A)" .. krauss@26580: krauss@26580: wenzelm@11848: subsection {* Calculational rules *} wenzelm@11848: wenzelm@11848: lemma forw_subst: "a = b ==> P(b) ==> P(a)" wenzelm@11848: by (rule ssubst) wenzelm@11848: wenzelm@11848: lemma back_subst: "P(a) ==> a = b ==> P(b)" wenzelm@11848: by (rule subst) wenzelm@11848: wenzelm@11848: text {* wenzelm@11848: Note that this list of rules is in reverse order of priorities. wenzelm@11848: *} wenzelm@11848: wenzelm@12019: lemmas basic_trans_rules [trans] = wenzelm@11848: forw_subst wenzelm@11848: back_subst wenzelm@11848: rev_mp wenzelm@11848: mp wenzelm@11848: trans wenzelm@11848: paulson@13779: subsection {* ``Let'' declarations *} paulson@13779: wenzelm@41229: nonterminal letbinds and letbind paulson@13779: haftmann@35416: definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where paulson@13779: "Let(s, f) == f(s)" paulson@13779: paulson@13779: syntax paulson@13779: "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) paulson@13779: "" :: "letbind => letbinds" ("_") paulson@13779: "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") paulson@13779: "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) paulson@13779: paulson@13779: translations paulson@13779: "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" wenzelm@35054: "let x = a in e" == "CONST Let(a, %x. e)" paulson@13779: paulson@13779: paulson@13779: lemma LetI: wenzelm@21539: assumes "!!x. x=t ==> P(u(x))" wenzelm@21539: shows "P(let x=t in u(x))" wenzelm@21539: apply (unfold Let_def) wenzelm@21539: apply (rule refl [THEN assms]) wenzelm@21539: done wenzelm@21539: wenzelm@21539: wenzelm@26286: subsection {* Intuitionistic simplification rules *} wenzelm@26286: wenzelm@26286: lemma conj_simps: wenzelm@26286: "P & True <-> P" wenzelm@26286: "True & P <-> P" wenzelm@26286: "P & False <-> False" wenzelm@26286: "False & P <-> False" wenzelm@26286: "P & P <-> P" wenzelm@26286: "P & P & Q <-> P & Q" wenzelm@26286: "P & ~P <-> False" wenzelm@26286: "~P & P <-> False" wenzelm@26286: "(P & Q) & R <-> P & (Q & R)" wenzelm@26286: by iprover+ wenzelm@26286: wenzelm@26286: lemma disj_simps: wenzelm@26286: "P | True <-> True" wenzelm@26286: "True | P <-> True" wenzelm@26286: "P | False <-> P" wenzelm@26286: "False | P <-> P" wenzelm@26286: "P | P <-> P" wenzelm@26286: "P | P | Q <-> P | Q" wenzelm@26286: "(P | Q) | R <-> P | (Q | R)" wenzelm@26286: by iprover+ wenzelm@26286: wenzelm@26286: lemma not_simps: wenzelm@26286: "~(P|Q) <-> ~P & ~Q" wenzelm@26286: "~ False <-> True" wenzelm@26286: "~ True <-> False" wenzelm@26286: by iprover+ wenzelm@26286: wenzelm@26286: lemma imp_simps: wenzelm@26286: "(P --> False) <-> ~P" wenzelm@26286: "(P --> True) <-> True" wenzelm@26286: "(False --> P) <-> True" wenzelm@26286: "(True --> P) <-> P" wenzelm@26286: "(P --> P) <-> True" wenzelm@26286: "(P --> ~P) <-> ~P" wenzelm@26286: by iprover+ wenzelm@26286: wenzelm@26286: lemma iff_simps: wenzelm@26286: "(True <-> P) <-> P" wenzelm@26286: "(P <-> True) <-> P" wenzelm@26286: "(P <-> P) <-> True" wenzelm@26286: "(False <-> P) <-> ~P" wenzelm@26286: "(P <-> False) <-> ~P" wenzelm@26286: by iprover+ wenzelm@26286: wenzelm@26286: (*The x=t versions are needed for the simplification procedures*) wenzelm@26286: lemma quant_simps: wenzelm@26286: "!!P. (ALL x. P) <-> P" wenzelm@26286: "(ALL x. x=t --> P(x)) <-> P(t)" wenzelm@26286: "(ALL x. t=x --> P(x)) <-> P(t)" wenzelm@26286: "!!P. (EX x. P) <-> P" wenzelm@26286: "EX x. x=t" wenzelm@26286: "EX x. t=x" wenzelm@26286: "(EX x. x=t & P(x)) <-> P(t)" wenzelm@26286: "(EX x. t=x & P(x)) <-> P(t)" wenzelm@26286: by iprover+ wenzelm@26286: wenzelm@26286: (*These are NOT supplied by default!*) wenzelm@26286: lemma distrib_simps: wenzelm@26286: "P & (Q | R) <-> P&Q | P&R" wenzelm@26286: "(Q | R) & P <-> Q&P | R&P" wenzelm@26286: "(P | Q --> R) <-> (P --> R) & (Q --> R)" wenzelm@26286: by iprover+ wenzelm@26286: wenzelm@26286: wenzelm@26286: text {* Conversion into rewrite rules *} wenzelm@26286: wenzelm@26286: lemma P_iff_F: "~P ==> (P <-> False)" by iprover wenzelm@26286: lemma iff_reflection_F: "~P ==> (P == False)" by (rule P_iff_F [THEN iff_reflection]) wenzelm@26286: wenzelm@26286: lemma P_iff_T: "P ==> (P <-> True)" by iprover wenzelm@26286: lemma iff_reflection_T: "P ==> (P == True)" by (rule P_iff_T [THEN iff_reflection]) wenzelm@26286: wenzelm@26286: wenzelm@26286: text {* More rewrite rules *} wenzelm@26286: wenzelm@26286: lemma conj_commute: "P&Q <-> Q&P" by iprover wenzelm@26286: lemma conj_left_commute: "P&(Q&R) <-> Q&(P&R)" by iprover wenzelm@26286: lemmas conj_comms = conj_commute conj_left_commute wenzelm@26286: wenzelm@26286: lemma disj_commute: "P|Q <-> Q|P" by iprover wenzelm@26286: lemma disj_left_commute: "P|(Q|R) <-> Q|(P|R)" by iprover wenzelm@26286: lemmas disj_comms = disj_commute disj_left_commute wenzelm@26286: wenzelm@26286: lemma conj_disj_distribL: "P&(Q|R) <-> (P&Q | P&R)" by iprover wenzelm@26286: lemma conj_disj_distribR: "(P|Q)&R <-> (P&R | Q&R)" by iprover wenzelm@26286: wenzelm@26286: lemma disj_conj_distribL: "P|(Q&R) <-> (P|Q) & (P|R)" by iprover wenzelm@26286: lemma disj_conj_distribR: "(P&Q)|R <-> (P|R) & (Q|R)" by iprover wenzelm@26286: wenzelm@26286: lemma imp_conj_distrib: "(P --> (Q&R)) <-> (P-->Q) & (P-->R)" by iprover wenzelm@26286: lemma imp_conj: "((P&Q)-->R) <-> (P --> (Q --> R))" by iprover wenzelm@26286: lemma imp_disj: "(P|Q --> R) <-> (P-->R) & (Q-->R)" by iprover wenzelm@26286: wenzelm@26286: lemma de_Morgan_disj: "(~(P | Q)) <-> (~P & ~Q)" by iprover wenzelm@26286: wenzelm@26286: lemma not_ex: "(~ (EX x. P(x))) <-> (ALL x.~P(x))" by iprover wenzelm@26286: lemma imp_ex: "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)" by iprover wenzelm@26286: wenzelm@26286: lemma ex_disj_distrib: wenzelm@26286: "(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))" by iprover wenzelm@26286: wenzelm@26286: lemma all_conj_distrib: wenzelm@26286: "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))" by iprover wenzelm@26286: wenzelm@4854: end