clasohm@1268: (* Title: FOL/IFOL.thy lcp@35: ID: $Id$ wenzelm@11677: Author: Lawrence C Paulson and Markus Wenzel wenzelm@11677: *) lcp@35: wenzelm@11677: header {* Intuitionistic first-order logic *} lcp@35: wenzelm@7355: theory IFOL = Pure wenzelm@7355: files ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML"): wenzelm@7355: clasohm@0: wenzelm@11677: subsection {* Syntax and axiomatic basis *} wenzelm@11677: wenzelm@3906: global wenzelm@3906: wenzelm@7355: classes "term" < logic wenzelm@7355: defaultsort "term" clasohm@0: wenzelm@7355: typedecl o wenzelm@79: wenzelm@11747: judgment wenzelm@11747: Trueprop :: "o => prop" ("(_)" 5) clasohm@0: wenzelm@11747: consts wenzelm@7355: True :: o wenzelm@7355: False :: o wenzelm@79: wenzelm@79: (* Connectives *) wenzelm@79: wenzelm@7355: "=" :: "['a, 'a] => o" (infixl 50) lcp@35: wenzelm@7355: Not :: "o => o" ("~ _" [40] 40) wenzelm@7355: & :: "[o, o] => o" (infixr 35) wenzelm@7355: "|" :: "[o, o] => o" (infixr 30) wenzelm@7355: --> :: "[o, o] => o" (infixr 25) wenzelm@7355: <-> :: "[o, o] => o" (infixr 25) wenzelm@79: wenzelm@79: (* Quantifiers *) wenzelm@79: wenzelm@7355: All :: "('a => o) => o" (binder "ALL " 10) wenzelm@7355: Ex :: "('a => o) => o" (binder "EX " 10) wenzelm@7355: Ex1 :: "('a => o) => o" (binder "EX! " 10) wenzelm@79: clasohm@0: lcp@928: syntax wenzelm@12662: "_not_equal" :: "['a, 'a] => o" (infixl "~=" 50) lcp@35: translations wenzelm@79: "x ~= y" == "~ (x = y)" wenzelm@79: wenzelm@12114: syntax (xsymbols) wenzelm@11677: Not :: "o => o" ("\ _" [40] 40) wenzelm@11677: "op &" :: "[o, o] => o" (infixr "\" 35) wenzelm@11677: "op |" :: "[o, o] => o" (infixr "\" 30) wenzelm@11677: "ALL " :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) wenzelm@11677: "EX " :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) wenzelm@11677: "EX! " :: "[idts, o] => o" ("(3\!_./ _)" [0, 10] 10) wenzelm@12662: "_not_equal" :: "['a, 'a] => o" (infixl "\" 50) wenzelm@11677: "op -->" :: "[o, o] => o" (infixr "\" 25) wenzelm@11677: "op <->" :: "[o, o] => o" (infixr "\" 25) lcp@35: wenzelm@6340: syntax (HTML output) wenzelm@11677: Not :: "o => o" ("\ _" [40] 40) wenzelm@6340: wenzelm@6340: wenzelm@3932: local wenzelm@3906: paulson@14236: finalconsts paulson@14236: False All Ex paulson@14236: "op =" paulson@14236: "op &" paulson@14236: "op |" paulson@14236: "op -->" paulson@14236: wenzelm@7355: axioms clasohm@0: wenzelm@79: (* Equality *) clasohm@0: wenzelm@7355: refl: "a=a" wenzelm@7355: subst: "[| a=b; P(a) |] ==> P(b)" clasohm@0: wenzelm@79: (* Propositional logic *) clasohm@0: wenzelm@7355: conjI: "[| P; Q |] ==> P&Q" wenzelm@7355: conjunct1: "P&Q ==> P" wenzelm@7355: conjunct2: "P&Q ==> Q" clasohm@0: wenzelm@7355: disjI1: "P ==> P|Q" wenzelm@7355: disjI2: "Q ==> P|Q" wenzelm@7355: disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" clasohm@0: wenzelm@7355: impI: "(P ==> Q) ==> P-->Q" wenzelm@7355: mp: "[| P-->Q; P |] ==> Q" clasohm@0: wenzelm@7355: FalseE: "False ==> P" wenzelm@7355: wenzelm@79: (* Quantifiers *) clasohm@0: wenzelm@7355: allI: "(!!x. P(x)) ==> (ALL x. P(x))" wenzelm@7355: spec: "(ALL x. P(x)) ==> P(x)" clasohm@0: wenzelm@7355: exI: "P(x) ==> (EX x. P(x))" wenzelm@7355: exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" clasohm@0: clasohm@0: (* Reflection *) clasohm@0: wenzelm@7355: eq_reflection: "(x=y) ==> (x==y)" wenzelm@7355: iff_reflection: "(P<->Q) ==> (P==Q)" clasohm@0: wenzelm@4092: paulson@14236: defs paulson@14236: (* Definitions *) paulson@14236: paulson@14236: True_def: "True == False-->False" paulson@14236: not_def: "~P == P-->False" paulson@14236: iff_def: "P<->Q == (P-->Q) & (Q-->P)" paulson@14236: paulson@14236: (* Unique existence *) paulson@14236: paulson@14236: ex1_def: "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)" paulson@14236: paulson@13779: wenzelm@11677: subsection {* Lemmas and proof tools *} wenzelm@11677: wenzelm@9886: setup Simplifier.setup wenzelm@9886: use "IFOL_lemmas.ML" wenzelm@11734: wenzelm@7355: use "fologic.ML" wenzelm@9886: use "hypsubstdata.ML" wenzelm@9886: setup hypsubst_setup wenzelm@7355: use "intprover.ML" wenzelm@7355: wenzelm@4092: wenzelm@12875: subsection {* Intuitionistic Reasoning *} wenzelm@12368: 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@12349: ML_setup {* wenzelm@12352: Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)); wenzelm@12349: *} wenzelm@12349: wenzelm@12349: wenzelm@12368: lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)" wenzelm@12368: by rules 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@12368: show "ALL x. P(x)" .. wenzelm@11677: next wenzelm@11677: assume "ALL x. P(x)" wenzelm@12368: thus "!!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@12368: thus "A --> B" .. wenzelm@11677: next wenzelm@11677: assume "A --> B" and A wenzelm@11677: thus 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@11677: show "x = y" by (unfold prems) (rule refl) wenzelm@11677: next wenzelm@11677: assume "x = y" wenzelm@11677: thus "x == y" by (rule eq_reflection) wenzelm@11677: qed wenzelm@11677: wenzelm@12875: lemma atomize_conj [atomize]: wenzelm@12875: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)" wenzelm@11976: proof wenzelm@11953: assume "!!C. (A ==> B ==> PROP C) ==> PROP C" wenzelm@11953: show "A & B" by (rule conjI) wenzelm@11953: next wenzelm@11953: fix C wenzelm@11953: assume "A & B" wenzelm@11953: assume "A ==> B ==> PROP C" wenzelm@11953: thus "PROP C" wenzelm@11953: proof this wenzelm@11953: show A by (rule conjunct1) wenzelm@11953: show B by (rule conjunct2) wenzelm@11953: qed wenzelm@11953: qed wenzelm@11953: wenzelm@12368: lemmas [symmetric, rulify] = atomize_all atomize_imp wenzelm@11771: wenzelm@11848: 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: paulson@13779: paulson@13779: subsection {* ``Let'' declarations *} paulson@13779: paulson@13779: nonterminals letbinds letbind paulson@13779: paulson@13779: constdefs paulson@13779: Let :: "['a::logic, 'a => 'b] => ('b::logic)" 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))" paulson@13779: "let x = a in e" == "Let(a, %x. e)" paulson@13779: paulson@13779: paulson@13779: lemma LetI: paulson@13779: assumes prem: "(!!x. x=t ==> P(u(x)))" paulson@13779: shows "P(let x=t in u(x))" paulson@13779: apply (unfold Let_def) paulson@13779: apply (rule refl [THEN prem]) paulson@13779: done paulson@13779: paulson@13779: ML paulson@13779: {* paulson@13779: val Let_def = thm "Let_def"; paulson@13779: val LetI = thm "LetI"; paulson@13779: *} paulson@13779: wenzelm@4854: end