Up to index of Isabelle/FOL
theory IFOL(* Title: FOL/IFOL.thy ID: $Id: IFOL.thy,v 1.49 2005/09/28 22:58:55 wenzelm Exp $ Author: Lawrence C Paulson and Markus Wenzel *) header {* Intuitionistic first-order logic *} theory IFOL imports Pure uses ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML") begin subsection {* Syntax and axiomatic basis *} global classes "term" final_consts term_class defaultsort "term" typedecl o judgment Trueprop :: "o => prop" ("(_)" 5) consts True :: o False :: o (* Connectives *) "op =" :: "['a, 'a] => o" (infixl "=" 50) Not :: "o => o" ("~ _" [40] 40) "op &" :: "[o, o] => o" (infixr "&" 35) "op |" :: "[o, o] => o" (infixr "|" 30) "op -->" :: "[o, o] => o" (infixr "-->" 25) "op <->" :: "[o, o] => o" (infixr "<->" 25) (* Quantifiers *) All :: "('a => o) => o" (binder "ALL " 10) Ex :: "('a => o) => o" (binder "EX " 10) Ex1 :: "('a => o) => o" (binder "EX! " 10) syntax "_not_equal" :: "['a, 'a] => o" (infixl "~=" 50) translations "x ~= y" == "~ (x = y)" syntax (xsymbols) Not :: "o => o" ("¬ _" [40] 40) "op &" :: "[o, o] => o" (infixr "∧" 35) "op |" :: "[o, o] => o" (infixr "∨" 30) "ALL " :: "[idts, o] => o" ("(3∀_./ _)" [0, 10] 10) "EX " :: "[idts, o] => o" ("(3∃_./ _)" [0, 10] 10) "EX! " :: "[idts, o] => o" ("(3∃!_./ _)" [0, 10] 10) "_not_equal" :: "['a, 'a] => o" (infixl "≠" 50) "op -->" :: "[o, o] => o" (infixr "-->" 25) "op <->" :: "[o, o] => o" (infixr "<->" 25) syntax (HTML output) Not :: "o => o" ("¬ _" [40] 40) "op &" :: "[o, o] => o" (infixr "∧" 35) "op |" :: "[o, o] => o" (infixr "∨" 30) "ALL " :: "[idts, o] => o" ("(3∀_./ _)" [0, 10] 10) "EX " :: "[idts, o] => o" ("(3∃_./ _)" [0, 10] 10) "EX! " :: "[idts, o] => o" ("(3∃!_./ _)" [0, 10] 10) "_not_equal" :: "['a, 'a] => o" (infixl "≠" 50) local finalconsts False All Ex "op =" "op &" "op |" "op -->" axioms (* Equality *) refl: "a=a" (* Propositional logic *) conjI: "[| P; Q |] ==> P&Q" conjunct1: "P&Q ==> P" conjunct2: "P&Q ==> Q" disjI1: "P ==> P|Q" disjI2: "Q ==> P|Q" disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" impI: "(P ==> Q) ==> P-->Q" mp: "[| P-->Q; P |] ==> Q" FalseE: "False ==> P" (* Quantifiers *) allI: "(!!x. P(x)) ==> (ALL x. P(x))" spec: "(ALL x. P(x)) ==> P(x)" exI: "P(x) ==> (EX x. P(x))" exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" (* Reflection *) eq_reflection: "(x=y) ==> (x==y)" iff_reflection: "(P<->Q) ==> (P==Q)" text{*Thanks to Stephan Merz*} theorem subst: assumes eq: "a = b" and p: "P(a)" shows "P(b)" proof - from eq have meta: "a ≡ b" by (rule eq_reflection) from p show ?thesis by (unfold meta) qed defs (* Definitions *) True_def: "True == False-->False" not_def: "~P == P-->False" iff_def: "P<->Q == (P-->Q) & (Q-->P)" (* Unique existence *) ex1_def: "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)" subsection {* Lemmas and proof tools *} use "IFOL_lemmas.ML" use "fologic.ML" use "hypsubstdata.ML" setup hypsubst_setup use "intprover.ML" subsection {* Intuitionistic Reasoning *} lemma impE': assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P" shows R proof - from 3 and 1 have P . with 1 have Q by (rule impE) with 2 show R . qed lemma allE': assumes 1: "ALL x. P(x)" and 2: "P(x) ==> ALL x. P(x) ==> Q" shows Q proof - from 1 have "P(x)" by (rule spec) from this and 1 show Q by (rule 2) qed lemma notE': assumes 1: "~ P" and 2: "~ P ==> P" shows R proof - from 2 and 1 have P . with 1 show R by (rule notE) qed lemmas [Pure.elim!] = disjE iffE FalseE conjE exE and [Pure.intro!] = iffI conjI impI TrueI notI allI refl and [Pure.elim 2] = allE notE' impE' and [Pure.intro] = exI disjI2 disjI1 setup {* [ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)] *} lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)" by iprover lemmas [sym] = sym iff_sym not_sym iff_not_sym and [Pure.elim?] = iffD1 iffD2 impE lemma eq_commute: "a=b <-> b=a" apply (rule iffI) apply (erule sym)+ done subsection {* Atomizing meta-level rules *} lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" proof assume "!!x. P(x)" show "ALL x. P(x)" .. next assume "ALL x. P(x)" thus "!!x. P(x)" .. qed lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)" proof assume "A ==> B" thus "A --> B" .. next assume "A --> B" and A thus B by (rule mp) qed lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" proof assume "x == y" show "x = y" by (unfold prems) (rule refl) next assume "x = y" thus "x == y" by (rule eq_reflection) qed lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)" proof assume "!!C. (A ==> B ==> PROP C) ==> PROP C" show "A & B" by (rule conjI) next fix C assume "A & B" assume "A ==> B ==> PROP C" thus "PROP C" proof this show A by (rule conjunct1) show B by (rule conjunct2) qed qed lemmas [symmetric, rulify] = atomize_all atomize_imp subsection {* Calculational rules *} lemma forw_subst: "a = b ==> P(b) ==> P(a)" by (rule ssubst) lemma back_subst: "P(a) ==> a = b ==> P(b)" by (rule subst) text {* Note that this list of rules is in reverse order of priorities. *} lemmas basic_trans_rules [trans] = forw_subst back_subst rev_mp mp trans subsection {* ``Let'' declarations *} nonterminals letbinds letbind constdefs Let :: "['a::{}, 'a => 'b] => ('b::{})" "Let(s, f) == f(s)" syntax "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) "" :: "letbind => letbinds" ("_") "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) translations "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" "let x = a in e" == "Let(a, %x. e)" 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 ML {* val Let_def = thm "Let_def"; val LetI = thm "LetI"; *} end
theorem subst:
[| a = b; P(a) |] ==> P(b)
theorem TrueI:
True
theorem conjE:
[| P ∧ Q; [| P; Q |] ==> R |] ==> R
theorem impE:
[| P --> Q; P; Q ==> R |] ==> R
theorem allE:
[| ∀x. P(x); P(x) ==> R |] ==> R
theorem all_dupE:
[| ∀x. P(x); [| P(x); ∀x. P(x) |] ==> R |] ==> R
theorem notI:
(P ==> False) ==> ¬ P
theorem notE:
[| ¬ P; P |] ==> R
theorem rev_notE:
[| P; ¬ P |] ==> R
theorem not_to_imp:
[| ¬ P; P --> False ==> Q |] ==> Q
theorem rev_mp:
[| P; P --> Q |] ==> Q
theorem contrapos:
[| ¬ Q; P ==> Q |] ==> ¬ P
theorem iffI:
[| P ==> Q; Q ==> P |] ==> P <-> Q
theorem iffE:
[| P <-> Q; [| P --> Q; Q --> P |] ==> R |] ==> R
theorem iffD1:
[| P <-> Q; P |] ==> Q
theorem iffD2:
[| P <-> Q; Q |] ==> P
theorem rev_iffD1:
[| P; P <-> Q |] ==> Q
theorem rev_iffD2:
[| Q; P <-> Q |] ==> P
theorem iff_refl:
P <-> P
theorem iff_sym:
Q <-> P ==> P <-> Q
theorem iff_trans:
[| P <-> Q; Q <-> R |] ==> P <-> R
theorem ex1I:
[| P(a); !!x. P(x) ==> x = a |] ==> ∃!x. P(x)
theorem ex_ex1I:
[| ∃x. P(x); !!x y. [| P(x); P(y) |] ==> x = y |] ==> ∃!x. P(x)
theorem ex1E:
[| ∃!x. P(x); !!x. [| P(x); ∀y. P(y) --> y = x |] ==> R |] ==> R
theorem conj_cong:
[| P <-> P'; P' ==> Q <-> Q' |] ==> P ∧ Q <-> P' ∧ Q'
theorem conj_cong2:
[| P <-> P'; P' ==> Q <-> Q' |] ==> Q ∧ P <-> Q' ∧ P'
theorem disj_cong:
[| P <-> P'; Q <-> Q' |] ==> P ∨ Q <-> P' ∨ Q'
theorem imp_cong:
[| P <-> P'; P' ==> Q <-> Q' |] ==> (P --> Q) <-> P' --> Q'
theorem iff_cong:
[| P <-> P'; Q <-> Q' |] ==> (P <-> Q) <-> P' <-> Q'
theorem not_cong:
P <-> P' ==> ¬ P <-> ¬ P'
theorem all_cong:
(!!x. P(x) <-> Q(x)) ==> (∀x. P(x)) <-> (∀x. Q(x))
theorem ex_cong:
(!!x. P(x) <-> Q(x)) ==> (∃x. P(x)) <-> (∃x. Q(x))
theorem ex1_cong:
(!!x. P(x) <-> Q(x)) ==> (∃!x. P(x)) <-> (∃!x. Q(x))
theorem sym:
a = b ==> b = a
theorem trans:
[| a = b; b = c |] ==> a = c
theorem not_sym:
b ≠ a ==> a ≠ b
theorem def_imp_iff:
A == B ==> A <-> B
theorem meta_eq_to_obj_eq:
A == B ==> A = B
theorem ssubst:
[| b = a; P(a) |] ==> P(b)
theorem ex1_equalsE:
[| ∃!x. P(x); P(a); P(b) |] ==> a = b
theorem subst_context:
a = b ==> t(a) = t(b)
theorem subst_context2:
[| a = b; c = d |] ==> t(a, c) = t(b, d)
theorem subst_context3:
[| a = b; c = d; e = f |] ==> t(a, c, e) = t(b, d, f)
theorem box_equals:
[| a = b; a = c; b = d |] ==> c = d
theorem simp_equals:
[| a = c; b = d; c = d |] ==> a = b
theorem pred1_cong:
a = a' ==> P(a) <-> P(a')
theorem pred2_cong:
[| a = a'; b = b' |] ==> P(a, b) <-> P(a', b')
theorem pred3_cong:
[| a = a'; b = b'; c = c' |] ==> P(a, b, c) <-> P(a', b', c')
theorem eq_cong:
[| a = a'; b = b' |] ==> a = b <-> a' = b'
theorem conj_impE:
[| P ∧ Q --> S; P --> Q --> S ==> R |] ==> R
theorem disj_impE:
[| P ∨ Q --> S; [| P --> S; Q --> S |] ==> R |] ==> R
theorem imp_impE:
[| (P --> Q) --> S; [| P; Q --> S |] ==> Q; S ==> R |] ==> R
theorem not_impE:
[| ¬ P --> S; P ==> False; S ==> R |] ==> R
theorem iff_impE:
[| (P <-> Q) --> S; [| P; Q --> S |] ==> Q; [| Q; P --> S |] ==> P; S ==> R |] ==> R
theorem all_impE:
[| (∀x. P(x)) --> S; !!x. P(x); S ==> R |] ==> R
theorem ex_impE:
[| (∃x. P(x)) --> S; P(x) --> S ==> R |] ==> R
theorem disj_imp_disj:
[| P ∨ Q; P ==> R; Q ==> S |] ==> R ∨ S
lemma impE':
[| P --> Q; Q ==> R; P --> Q ==> P |] ==> R
lemma allE':
[| ∀x. P(x); [| P(x); ∀x. P(x) |] ==> Q |] ==> Q
lemma notE':
[| ¬ P; ¬ P ==> P |] ==> R
lemmas
[| P ∨ Q; P ==> R; Q ==> R |] ==> R
[| P <-> Q; [| P --> Q; Q --> P |] ==> R |] ==> R
False ==> P
[| P ∧ Q; [| P; Q |] ==> R |] ==> R
[| ∃x. P(x); !!x. P(x) ==> R |] ==> R
and
[| P ==> Q; Q ==> P |] ==> P <-> Q
[| P; Q |] ==> P ∧ Q
(P ==> Q) ==> P --> Q
True
(P ==> False) ==> ¬ P
(!!x. P(x)) ==> ∀x. P(x)
a = a
and
[| ∀x. P(x); P(x) ==> R |] ==> R
[| ¬ P; ¬ P ==> P |] ==> R
[| P --> Q; Q ==> R; P --> Q ==> P |] ==> R
and
P(x) ==> ∃x. P(x)
Q ==> P ∨ Q
P ==> P ∨ Q
lemmas
[| P ∨ Q; P ==> R; Q ==> R |] ==> R
[| P <-> Q; [| P --> Q; Q --> P |] ==> R |] ==> R
False ==> P
[| P ∧ Q; [| P; Q |] ==> R |] ==> R
[| ∃x. P(x); !!x. P(x) ==> R |] ==> R
and
[| P ==> Q; Q ==> P |] ==> P <-> Q
[| P; Q |] ==> P ∧ Q
(P ==> Q) ==> P --> Q
True
(P ==> False) ==> ¬ P
(!!x. P(x)) ==> ∀x. P(x)
a = a
and
[| ∀x. P(x); P(x) ==> R |] ==> R
[| ¬ P; ¬ P ==> P |] ==> R
[| P --> Q; Q ==> R; P --> Q ==> P |] ==> R
and
P(x) ==> ∃x. P(x)
Q ==> P ∨ Q
P ==> P ∨ Q
lemma iff_not_sym:
¬ (Q <-> P) ==> ¬ (P <-> Q)
lemmas
a = b ==> b = a
Q <-> P ==> P <-> Q
b ≠ a ==> a ≠ b
¬ (Q <-> P) ==> ¬ (P <-> Q)
and
[| P <-> Q; P |] ==> Q
[| P <-> Q; Q |] ==> P
[| P --> Q; P; Q ==> R |] ==> R
lemmas
a = b ==> b = a
Q <-> P ==> P <-> Q
b ≠ a ==> a ≠ b
¬ (Q <-> P) ==> ¬ (P <-> Q)
and
[| P <-> Q; P |] ==> Q
[| P <-> Q; Q |] ==> P
[| P --> Q; P; Q ==> R |] ==> R
lemma eq_commute:
a = b <-> b = a
lemma atomize_all:
(!!x. P(x)) == ∀x. P(x)
lemma atomize_imp:
(A ==> B) == A --> B
lemma atomize_eq:
(x == y) == x = y
lemma atomize_conj:
(A && B) == A ∧ B
lemmas
∀x. P1(x) == (!!x. P1(x))
A1 --> B1 == (A1 ==> B1)
lemmas
∀x. P1(x) == (!!x. P1(x))
A1 --> B1 == (A1 ==> B1)
lemma forw_subst:
[| a = b; P(b) |] ==> P(a)
lemma back_subst:
[| P(a); a = b |] ==> P(b)
lemmas basic_trans_rules:
[| a = b; P(b) |] ==> P(a)
[| P(a); a = b |] ==> P(b)
[| P; P --> Q |] ==> Q
[| P --> Q; P |] ==> Q
[| a = b; b = c |] ==> a = c
lemmas basic_trans_rules:
[| a = b; P(b) |] ==> P(a)
[| P(a); a = b |] ==> P(b)
[| P; P --> Q |] ==> Q
[| P --> Q; P |] ==> Q
[| a = b; b = c |] ==> a = c
lemma LetI:
(!!x. x = t ==> P(u(x))) ==> P(Let(t, u))