imports Pure

(* Title: HOL/ex/Higher_Order_Logic.thy

Author: Gertrud Bauer and Markus Wenzel, TU Muenchen

*)

header {* Foundations of HOL *}

theory Higher_Order_Logic imports Pure begin

text {*

The following theory development demonstrates Higher-Order Logic

itself, represented directly within the Pure framework of Isabelle.

The ``HOL'' logic given here is essentially that of Gordon

\cite{Gordon:1985:HOL}, although we prefer to present basic concepts

in a slightly more conventional manner oriented towards plain

Natural Deduction.

*}

subsection {* Pure Logic *}

classes type

default_sort type

typedecl o

arities

o :: type

"fun" :: (type, type) type

subsubsection {* Basic logical connectives *}

judgment

Trueprop :: "o => prop" ("_" 5)

axiomatization

imp :: "o => o => o" (infixr "-->" 25) and

All :: "('a => o) => o" (binder "∀" 10)

where

impI [intro]: "(A ==> B) ==> A --> B" and

impE [dest, trans]: "A --> B ==> A ==> B" and

allI [intro]: "(!!x. P x) ==> ∀x. P x" and

allE [dest]: "∀x. P x ==> P a"

subsubsection {* Extensional equality *}

axiomatization

equal :: "'a => 'a => o" (infixl "=" 50)

where

refl [intro]: "x = x" and

subst: "x = y ==> P x ==> P y"

axiomatization where

ext [intro]: "(!!x. f x = g x) ==> f = g" and

iff [intro]: "(A ==> B) ==> (B ==> A) ==> A = B"

theorem sym [sym]: "x = y ==> y = x"

proof -

assume "x = y"

then show "y = x" by (rule subst) (rule refl)

qed

lemma [trans]: "x = y ==> P y ==> P x"

by (rule subst) (rule sym)

lemma [trans]: "P x ==> x = y ==> P y"

by (rule subst)

theorem trans [trans]: "x = y ==> y = z ==> x = z"

by (rule subst)

theorem iff1 [elim]: "A = B ==> A ==> B"

by (rule subst)

theorem iff2 [elim]: "A = B ==> B ==> A"

by (rule subst) (rule sym)

subsubsection {* Derived connectives *}

definition

false :: o ("⊥") where

"⊥ ≡ ∀A. A"

definition

true :: o ("\<top>") where

"\<top> ≡ ⊥ --> ⊥"

definition

not :: "o => o" ("¬ _" [40] 40) where

"not ≡ λA. A --> ⊥"

definition

conj :: "o => o => o" (infixr "∧" 35) where

"conj ≡ λA B. ∀C. (A --> B --> C) --> C"

definition

disj :: "o => o => o" (infixr "∨" 30) where

"disj ≡ λA B. ∀C. (A --> C) --> (B --> C) --> C"

definition

Ex :: "('a => o) => o" (binder "∃" 10) where

"∃x. P x ≡ ∀C. (∀x. P x --> C) --> C"

abbreviation

not_equal :: "'a => 'a => o" (infixl "≠" 50) where

"x ≠ y ≡ ¬ (x = y)"

theorem falseE [elim]: "⊥ ==> A"

proof (unfold false_def)

assume "∀A. A"

then show A ..

qed

theorem trueI [intro]: \<top>

proof (unfold true_def)

show "⊥ --> ⊥" ..

qed

theorem notI [intro]: "(A ==> ⊥) ==> ¬ A"

proof (unfold not_def)

assume "A ==> ⊥"

then show "A --> ⊥" ..

qed

theorem notE [elim]: "¬ A ==> A ==> B"

proof (unfold not_def)

assume "A --> ⊥"

also assume A

finally have ⊥ ..

then show B ..

qed

lemma notE': "A ==> ¬ A ==> B"

by (rule notE)

lemmas contradiction = notE notE' -- {* proof by contradiction in any order *}

theorem conjI [intro]: "A ==> B ==> A ∧ B"

proof (unfold conj_def)

assume A and B

show "∀C. (A --> B --> C) --> C"

proof

fix C show "(A --> B --> C) --> C"

proof

assume "A --> B --> C"

also note `A`

also note `B`

finally show C .

qed

qed

qed

theorem conjE [elim]: "A ∧ B ==> (A ==> B ==> C) ==> C"

proof (unfold conj_def)

assume c: "∀C. (A --> B --> C) --> C"

assume "A ==> B ==> C"

moreover {

from c have "(A --> B --> A) --> A" ..

also have "A --> B --> A"

proof

assume A

then show "B --> A" ..

qed

finally have A .

} moreover {

from c have "(A --> B --> B) --> B" ..

also have "A --> B --> B"

proof

show "B --> B" ..

qed

finally have B .

} ultimately show C .

qed

theorem disjI1 [intro]: "A ==> A ∨ B"

proof (unfold disj_def)

assume A

show "∀C. (A --> C) --> (B --> C) --> C"

proof

fix C show "(A --> C) --> (B --> C) --> C"

proof

assume "A --> C"

also note `A`

finally have C .

then show "(B --> C) --> C" ..

qed

qed

qed

theorem disjI2 [intro]: "B ==> A ∨ B"

proof (unfold disj_def)

assume B

show "∀C. (A --> C) --> (B --> C) --> C"

proof

fix C show "(A --> C) --> (B --> C) --> C"

proof

show "(B --> C) --> C"

proof

assume "B --> C"

also note `B`

finally show C .

qed

qed

qed

qed

theorem disjE [elim]: "A ∨ B ==> (A ==> C) ==> (B ==> C) ==> C"

proof (unfold disj_def)

assume c: "∀C. (A --> C) --> (B --> C) --> C"

assume r1: "A ==> C" and r2: "B ==> C"

from c have "(A --> C) --> (B --> C) --> C" ..

also have "A --> C"

proof

assume A then show C by (rule r1)

qed

also have "B --> C"

proof

assume B then show C by (rule r2)

qed

finally show C .

qed

theorem exI [intro]: "P a ==> ∃x. P x"

proof (unfold Ex_def)

assume "P a"

show "∀C. (∀x. P x --> C) --> C"

proof

fix C show "(∀x. P x --> C) --> C"

proof

assume "∀x. P x --> C"

then have "P a --> C" ..

also note `P a`

finally show C .

qed

qed

qed

theorem exE [elim]: "∃x. P x ==> (!!x. P x ==> C) ==> C"

proof (unfold Ex_def)

assume c: "∀C. (∀x. P x --> C) --> C"

assume r: "!!x. P x ==> C"

from c have "(∀x. P x --> C) --> C" ..

also have "∀x. P x --> C"

proof

fix x show "P x --> C"

proof

assume "P x"

then show C by (rule r)

qed

qed

finally show C .

qed

subsection {* Classical logic *}

locale classical =

assumes classical: "(¬ A ==> A) ==> A"

theorem (in classical)

Peirce's_Law: "((A --> B) --> A) --> A"

proof

assume a: "(A --> B) --> A"

show A

proof (rule classical)

assume "¬ A"

have "A --> B"

proof

assume A

with `¬ A` show B by (rule contradiction)

qed

with a show A ..

qed

qed

theorem (in classical)

double_negation: "¬ ¬ A ==> A"

proof -

assume "¬ ¬ A"

show A

proof (rule classical)

assume "¬ A"

with `¬ ¬ A` show ?thesis by (rule contradiction)

qed

qed

theorem (in classical)

tertium_non_datur: "A ∨ ¬ A"

proof (rule double_negation)

show "¬ ¬ (A ∨ ¬ A)"

proof

assume "¬ (A ∨ ¬ A)"

have "¬ A"

proof

assume A then have "A ∨ ¬ A" ..

with `¬ (A ∨ ¬ A)` show ⊥ by (rule contradiction)

qed

then have "A ∨ ¬ A" ..

with `¬ (A ∨ ¬ A)` show ⊥ by (rule contradiction)

qed

qed

theorem (in classical)

classical_cases: "(A ==> C) ==> (¬ A ==> C) ==> C"

proof -

assume r1: "A ==> C" and r2: "¬ A ==> C"

from tertium_non_datur show C

proof

assume A

then show ?thesis by (rule r1)

next

assume "¬ A"

then show ?thesis by (rule r2)

qed

qed

lemma (in classical) "(¬ A ==> A) ==> A" (* FIXME *)

proof -

assume r: "¬ A ==> A"

show A

proof (rule classical_cases)

assume A then show A .

next

assume "¬ A" then show A by (rule r)

qed

qed

end