wenzelm@12360: (* Title: HOL/ex/Higher_Order_Logic.thy wenzelm@12360: Author: Gertrud Bauer and Markus Wenzel, TU Muenchen wenzelm@12360: *) wenzelm@12360: wenzelm@12360: header {* Foundations of HOL *} wenzelm@12360: wenzelm@26957: theory Higher_Order_Logic imports Pure begin wenzelm@12360: wenzelm@12360: text {* wenzelm@12360: The following theory development demonstrates Higher-Order Logic wenzelm@12360: itself, represented directly within the Pure framework of Isabelle. wenzelm@12360: The ``HOL'' logic given here is essentially that of Gordon wenzelm@12360: \cite{Gordon:1985:HOL}, although we prefer to present basic concepts wenzelm@12360: in a slightly more conventional manner oriented towards plain wenzelm@12360: Natural Deduction. wenzelm@12360: *} wenzelm@12360: wenzelm@12360: wenzelm@12360: subsection {* Pure Logic *} wenzelm@12360: wenzelm@14854: classes type wenzelm@36452: default_sort type wenzelm@12360: wenzelm@12360: typedecl o wenzelm@12360: arities wenzelm@12360: o :: type krauss@20523: "fun" :: (type, type) type wenzelm@12360: wenzelm@12360: wenzelm@12360: subsubsection {* Basic logical connectives *} wenzelm@12360: wenzelm@12360: judgment wenzelm@12360: Trueprop :: "o \ prop" ("_" 5) wenzelm@12360: wenzelm@23822: axiomatization wenzelm@23822: imp :: "o \ o \ o" (infixr "\" 25) and wenzelm@12360: All :: "('a \ o) \ o" (binder "\" 10) wenzelm@23822: where wenzelm@23822: impI [intro]: "(A \ B) \ A \ B" and wenzelm@23822: impE [dest, trans]: "A \ B \ A \ B" and wenzelm@23822: allI [intro]: "(\x. P x) \ \x. P x" and wenzelm@12360: allE [dest]: "\x. P x \ P a" wenzelm@12360: wenzelm@12360: wenzelm@12360: subsubsection {* Extensional equality *} wenzelm@12360: wenzelm@23822: axiomatization wenzelm@12360: equal :: "'a \ 'a \ o" (infixl "=" 50) wenzelm@23822: where wenzelm@23822: refl [intro]: "x = x" and wenzelm@23822: subst: "x = y \ P x \ P y" wenzelm@12360: wenzelm@23822: axiomatization where wenzelm@23822: ext [intro]: "(\x. f x = g x) \ f = g" and wenzelm@12360: iff [intro]: "(A \ B) \ (B \ A) \ A = B" wenzelm@12360: wenzelm@12394: theorem sym [sym]: "x = y \ y = x" wenzelm@12360: proof - wenzelm@12360: assume "x = y" wenzelm@23373: then show "y = x" by (rule subst) (rule refl) wenzelm@12360: qed wenzelm@12360: wenzelm@12360: lemma [trans]: "x = y \ P y \ P x" wenzelm@12360: by (rule subst) (rule sym) wenzelm@12360: wenzelm@12360: lemma [trans]: "P x \ x = y \ P y" wenzelm@12360: by (rule subst) wenzelm@12360: wenzelm@12360: theorem trans [trans]: "x = y \ y = z \ x = z" wenzelm@12360: by (rule subst) wenzelm@12360: wenzelm@12360: theorem iff1 [elim]: "A = B \ A \ B" wenzelm@12360: by (rule subst) wenzelm@12360: wenzelm@12360: theorem iff2 [elim]: "A = B \ B \ A" wenzelm@12360: by (rule subst) (rule sym) wenzelm@12360: wenzelm@12360: wenzelm@12360: subsubsection {* Derived connectives *} wenzelm@12360: wenzelm@19736: definition wenzelm@21404: false :: o ("\") where wenzelm@12360: "\ \ \A. A" wenzelm@21404: wenzelm@21404: definition wenzelm@21404: true :: o ("\") where wenzelm@12360: "\ \ \ \ \" wenzelm@21404: wenzelm@21404: definition wenzelm@21404: not :: "o \ o" ("\ _" [40] 40) where wenzelm@12360: "not \ \A. A \ \" wenzelm@21404: wenzelm@21404: definition wenzelm@21404: conj :: "o \ o \ o" (infixr "\" 35) where wenzelm@12360: "conj \ \A B. \C. (A \ B \ C) \ C" wenzelm@21404: wenzelm@21404: definition wenzelm@21404: disj :: "o \ o \ o" (infixr "\" 30) where wenzelm@12360: "disj \ \A B. \C. (A \ C) \ (B \ C) \ C" wenzelm@21404: wenzelm@21404: definition wenzelm@21404: Ex :: "('a \ o) \ o" (binder "\" 10) where wenzelm@23822: "\x. P x \ \C. (\x. P x \ C) \ C" wenzelm@12360: wenzelm@19380: abbreviation wenzelm@21404: not_equal :: "'a \ 'a \ o" (infixl "\" 50) where wenzelm@19380: "x \ y \ \ (x = y)" wenzelm@12360: wenzelm@12360: theorem falseE [elim]: "\ \ A" wenzelm@12360: proof (unfold false_def) wenzelm@12360: assume "\A. A" wenzelm@23373: then show A .. wenzelm@12360: qed wenzelm@12360: wenzelm@12360: theorem trueI [intro]: \ wenzelm@12360: proof (unfold true_def) wenzelm@12360: show "\ \ \" .. wenzelm@12360: qed wenzelm@12360: wenzelm@12360: theorem notI [intro]: "(A \ \) \ \ A" wenzelm@12360: proof (unfold not_def) wenzelm@12360: assume "A \ \" wenzelm@23373: then show "A \ \" .. wenzelm@12360: qed wenzelm@12360: wenzelm@12360: theorem notE [elim]: "\ A \ A \ B" wenzelm@12360: proof (unfold not_def) wenzelm@12360: assume "A \ \" wenzelm@12360: also assume A wenzelm@12360: finally have \ .. wenzelm@23373: then show B .. wenzelm@12360: qed wenzelm@12360: wenzelm@12360: lemma notE': "A \ \ A \ B" wenzelm@12360: by (rule notE) wenzelm@12360: wenzelm@12360: lemmas contradiction = notE notE' -- {* proof by contradiction in any order *} wenzelm@12360: wenzelm@12360: theorem conjI [intro]: "A \ B \ A \ B" wenzelm@12360: proof (unfold conj_def) wenzelm@12360: assume A and B wenzelm@12360: show "\C. (A \ B \ C) \ C" wenzelm@12360: proof wenzelm@12360: fix C show "(A \ B \ C) \ C" wenzelm@12360: proof wenzelm@12360: assume "A \ B \ C" wenzelm@23373: also note `A` wenzelm@23373: also note `B` wenzelm@12360: finally show C . wenzelm@12360: qed wenzelm@12360: qed wenzelm@12360: qed wenzelm@12360: wenzelm@12360: theorem conjE [elim]: "A \ B \ (A \ B \ C) \ C" wenzelm@12360: proof (unfold conj_def) wenzelm@12360: assume c: "\C. (A \ B \ C) \ C" wenzelm@12360: assume "A \ B \ C" wenzelm@12360: moreover { wenzelm@12360: from c have "(A \ B \ A) \ A" .. wenzelm@12360: also have "A \ B \ A" wenzelm@12360: proof wenzelm@12360: assume A wenzelm@23373: then show "B \ A" .. wenzelm@12360: qed wenzelm@12360: finally have A . wenzelm@12360: } moreover { wenzelm@12360: from c have "(A \ B \ B) \ B" .. wenzelm@12360: also have "A \ B \ B" wenzelm@12360: proof wenzelm@12360: show "B \ B" .. wenzelm@12360: qed wenzelm@12360: finally have B . wenzelm@12360: } ultimately show C . wenzelm@12360: qed wenzelm@12360: wenzelm@12360: theorem disjI1 [intro]: "A \ A \ B" wenzelm@12360: proof (unfold disj_def) wenzelm@12360: assume A wenzelm@12360: show "\C. (A \ C) \ (B \ C) \ C" wenzelm@12360: proof wenzelm@12360: fix C show "(A \ C) \ (B \ C) \ C" wenzelm@12360: proof wenzelm@12360: assume "A \ C" wenzelm@23373: also note `A` wenzelm@12360: finally have C . wenzelm@23373: then show "(B \ C) \ C" .. wenzelm@12360: qed wenzelm@12360: qed wenzelm@12360: qed wenzelm@12360: wenzelm@12360: theorem disjI2 [intro]: "B \ A \ B" wenzelm@12360: proof (unfold disj_def) wenzelm@12360: assume B wenzelm@12360: show "\C. (A \ C) \ (B \ C) \ C" wenzelm@12360: proof wenzelm@12360: fix C show "(A \ C) \ (B \ C) \ C" wenzelm@12360: proof wenzelm@12360: show "(B \ C) \ C" wenzelm@12360: proof wenzelm@12360: assume "B \ C" wenzelm@23373: also note `B` wenzelm@12360: finally show C . wenzelm@12360: qed wenzelm@12360: qed wenzelm@12360: qed wenzelm@12360: qed wenzelm@12360: wenzelm@12360: theorem disjE [elim]: "A \ B \ (A \ C) \ (B \ C) \ C" wenzelm@12360: proof (unfold disj_def) wenzelm@12360: assume c: "\C. (A \ C) \ (B \ C) \ C" wenzelm@12360: assume r1: "A \ C" and r2: "B \ C" wenzelm@12360: from c have "(A \ C) \ (B \ C) \ C" .. wenzelm@12360: also have "A \ C" wenzelm@12360: proof wenzelm@23373: assume A then show C by (rule r1) wenzelm@12360: qed wenzelm@12360: also have "B \ C" wenzelm@12360: proof wenzelm@23373: assume B then show C by (rule r2) wenzelm@12360: qed wenzelm@12360: finally show C . wenzelm@12360: qed wenzelm@12360: wenzelm@12360: theorem exI [intro]: "P a \ \x. P x" wenzelm@12360: proof (unfold Ex_def) wenzelm@12360: assume "P a" wenzelm@12360: show "\C. (\x. P x \ C) \ C" wenzelm@12360: proof wenzelm@12360: fix C show "(\x. P x \ C) \ C" wenzelm@12360: proof wenzelm@12360: assume "\x. P x \ C" wenzelm@23373: then have "P a \ C" .. wenzelm@23373: also note `P a` wenzelm@12360: finally show C . wenzelm@12360: qed wenzelm@12360: qed wenzelm@12360: qed wenzelm@12360: wenzelm@12360: theorem exE [elim]: "\x. P x \ (\x. P x \ C) \ C" wenzelm@12360: proof (unfold Ex_def) wenzelm@12360: assume c: "\C. (\x. P x \ C) \ C" wenzelm@12360: assume r: "\x. P x \ C" wenzelm@12360: from c have "(\x. P x \ C) \ C" .. wenzelm@12360: also have "\x. P x \ C" wenzelm@12360: proof wenzelm@12360: fix x show "P x \ C" wenzelm@12360: proof wenzelm@12360: assume "P x" wenzelm@23373: then show C by (rule r) wenzelm@12360: qed wenzelm@12360: qed wenzelm@12360: finally show C . wenzelm@12360: qed wenzelm@12360: wenzelm@12360: wenzelm@12360: subsection {* Classical logic *} wenzelm@12360: wenzelm@12360: locale classical = wenzelm@12360: assumes classical: "(\ A \ A) \ A" wenzelm@12360: wenzelm@12360: theorem (in classical) wenzelm@12360: Peirce's_Law: "((A \ B) \ A) \ A" wenzelm@12360: proof wenzelm@12360: assume a: "(A \ B) \ A" wenzelm@12360: show A wenzelm@12360: proof (rule classical) wenzelm@12360: assume "\ A" wenzelm@12360: have "A \ B" wenzelm@12360: proof wenzelm@12360: assume A wenzelm@23373: with `\ A` show B by (rule contradiction) wenzelm@12360: qed wenzelm@12360: with a show A .. wenzelm@12360: qed wenzelm@12360: qed wenzelm@12360: wenzelm@12360: theorem (in classical) wenzelm@12360: double_negation: "\ \ A \ A" wenzelm@12360: proof - wenzelm@12360: assume "\ \ A" wenzelm@12360: show A wenzelm@12360: proof (rule classical) wenzelm@12360: assume "\ A" wenzelm@23373: with `\ \ A` show ?thesis by (rule contradiction) wenzelm@12360: qed wenzelm@12360: qed wenzelm@12360: wenzelm@12360: theorem (in classical) wenzelm@12360: tertium_non_datur: "A \ \ A" wenzelm@12360: proof (rule double_negation) wenzelm@12360: show "\ \ (A \ \ A)" wenzelm@12360: proof wenzelm@12360: assume "\ (A \ \ A)" wenzelm@12360: have "\ A" wenzelm@12360: proof wenzelm@23373: assume A then have "A \ \ A" .. wenzelm@23373: with `\ (A \ \ A)` show \ by (rule contradiction) wenzelm@12360: qed wenzelm@23373: then have "A \ \ A" .. wenzelm@23373: with `\ (A \ \ A)` show \ by (rule contradiction) wenzelm@12360: qed wenzelm@12360: qed wenzelm@12360: wenzelm@12360: theorem (in classical) wenzelm@12360: classical_cases: "(A \ C) \ (\ A \ C) \ C" wenzelm@12360: proof - wenzelm@12360: assume r1: "A \ C" and r2: "\ A \ C" wenzelm@12360: from tertium_non_datur show C wenzelm@12360: proof wenzelm@12360: assume A wenzelm@23373: then show ?thesis by (rule r1) wenzelm@12360: next wenzelm@12360: assume "\ A" wenzelm@23373: then show ?thesis by (rule r2) wenzelm@12360: qed wenzelm@12360: qed wenzelm@12360: wenzelm@12573: lemma (in classical) "(\ A \ A) \ A" (* FIXME *) wenzelm@12573: proof - wenzelm@12573: assume r: "\ A \ A" wenzelm@12573: show A wenzelm@12573: proof (rule classical_cases) wenzelm@23373: assume A then show A . wenzelm@12573: next wenzelm@23373: assume "\ A" then show A by (rule r) wenzelm@12573: qed wenzelm@12573: qed wenzelm@12573: wenzelm@12360: end