# Theory Higher_Order_Logic

theory Higher_Order_Logic
imports Pure
```(*  Title:      HOL/ex/Higher_Order_Logic.thy
Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
*)

section ‹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›

class type
default_sort type

typedecl o
instance o :: type ..
instance "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
```