(* Title: HOL/ex/Higher_Order_Logic.thy
Author: Gertrud Bauer and Markus Wenzel, TU Muenchen
*)
section \<open>Foundations of HOL\<close>
theory Higher_Order_Logic imports Pure begin
text \<open>
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.
\<close>
subsection \<open>Pure Logic\<close>
class type
default_sort type
typedecl o
instance o :: type ..
instance "fun" :: (type, type) type ..
subsubsection \<open>Basic logical connectives\<close>
judgment
Trueprop :: "o \<Rightarrow> prop" ("_" 5)
axiomatization
imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25) and
All :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10)
where
impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and
impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" and
allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" and
allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
subsubsection \<open>Extensional equality\<close>
axiomatization
equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "=" 50)
where
refl [intro]: "x = x" and
subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
axiomatization where
ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g" and
iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
theorem sym [sym]: "x = y \<Longrightarrow> y = x"
proof -
assume "x = y"
then show "y = x" by (rule subst) (rule refl)
qed
lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
by (rule subst) (rule sym)
lemma [trans]: "P x \<Longrightarrow> x = y \<Longrightarrow> P y"
by (rule subst)
theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
by (rule subst)
theorem iff1 [elim]: "A = B \<Longrightarrow> A \<Longrightarrow> B"
by (rule subst)
theorem iff2 [elim]: "A = B \<Longrightarrow> B \<Longrightarrow> A"
by (rule subst) (rule sym)
subsubsection \<open>Derived connectives\<close>
definition false :: o ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A"
definition true :: o ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
definition not :: "o \<Rightarrow> o" ("\<not> _" [40] 40)
where "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
definition conj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<and>" 35)
where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
definition disj :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<or>" 30)
where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10)
where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50)
where "x \<noteq> y \<equiv> \<not> (x = y)"
theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
proof (unfold false_def)
assume "\<forall>A. A"
then show A ..
qed
theorem trueI [intro]: \<top>
proof (unfold true_def)
show "\<bottom> \<longrightarrow> \<bottom>" ..
qed
theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
proof (unfold not_def)
assume "A \<Longrightarrow> \<bottom>"
then show "A \<longrightarrow> \<bottom>" ..
qed
theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
proof (unfold not_def)
assume "A \<longrightarrow> \<bottom>"
also assume A
finally have \<bottom> ..
then show B ..
qed
lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
by (rule notE)
lemmas contradiction = notE notE' -- \<open>proof by contradiction in any order\<close>
theorem conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
proof (unfold conj_def)
assume A and B
show "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
proof
fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
proof
assume "A \<longrightarrow> B \<longrightarrow> C"
also note \<open>A\<close>
also note \<open>B\<close>
finally show C .
qed
qed
qed
theorem conjE [elim]: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
proof (unfold conj_def)
assume c: "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
assume "A \<Longrightarrow> B \<Longrightarrow> C"
moreover {
from c have "(A \<longrightarrow> B \<longrightarrow> A) \<longrightarrow> A" ..
also have "A \<longrightarrow> B \<longrightarrow> A"
proof
assume A
then show "B \<longrightarrow> A" ..
qed
finally have A .
} moreover {
from c have "(A \<longrightarrow> B \<longrightarrow> B) \<longrightarrow> B" ..
also have "A \<longrightarrow> B \<longrightarrow> B"
proof
show "B \<longrightarrow> B" ..
qed
finally have B .
} ultimately show C .
qed
theorem disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
proof (unfold disj_def)
assume A
show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
proof
fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
proof
assume "A \<longrightarrow> C"
also note \<open>A\<close>
finally have C .
then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
qed
qed
qed
theorem disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
proof (unfold disj_def)
assume B
show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
proof
fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
proof
show "(B \<longrightarrow> C) \<longrightarrow> C"
proof
assume "B \<longrightarrow> C"
also note \<open>B\<close>
finally show C .
qed
qed
qed
qed
theorem disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
proof (unfold disj_def)
assume c: "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
assume r1: "A \<Longrightarrow> C" and r2: "B \<Longrightarrow> C"
from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..
also have "A \<longrightarrow> C"
proof
assume A then show C by (rule r1)
qed
also have "B \<longrightarrow> C"
proof
assume B then show C by (rule r2)
qed
finally show C .
qed
theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
proof (unfold Ex_def)
assume "P a"
show "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
proof
fix C show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
proof
assume "\<forall>x. P x \<longrightarrow> C"
then have "P a \<longrightarrow> C" ..
also note \<open>P a\<close>
finally show C .
qed
qed
qed
theorem exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
proof (unfold Ex_def)
assume c: "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
assume r: "\<And>x. P x \<Longrightarrow> C"
from c have "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" ..
also have "\<forall>x. P x \<longrightarrow> C"
proof
fix x show "P x \<longrightarrow> C"
proof
assume "P x"
then show C by (rule r)
qed
qed
finally show C .
qed
subsection \<open>Classical logic\<close>
locale classical =
assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
theorem (in classical)
Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
proof
assume a: "(A \<longrightarrow> B) \<longrightarrow> A"
show A
proof (rule classical)
assume "\<not> A"
have "A \<longrightarrow> B"
proof
assume A
with \<open>\<not> A\<close> show B by (rule contradiction)
qed
with a show A ..
qed
qed
theorem (in classical)
double_negation: "\<not> \<not> A \<Longrightarrow> A"
proof -
assume "\<not> \<not> A"
show A
proof (rule classical)
assume "\<not> A"
with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
qed
qed
theorem (in classical)
tertium_non_datur: "A \<or> \<not> A"
proof (rule double_negation)
show "\<not> \<not> (A \<or> \<not> A)"
proof
assume "\<not> (A \<or> \<not> A)"
have "\<not> A"
proof
assume A then have "A \<or> \<not> A" ..
with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction)
qed
then have "A \<or> \<not> A" ..
with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction)
qed
qed
theorem (in classical)
classical_cases: "(A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
proof -
assume r1: "A \<Longrightarrow> C" and r2: "\<not> A \<Longrightarrow> C"
from tertium_non_datur show C
proof
assume A
then show ?thesis by (rule r1)
next
assume "\<not> A"
then show ?thesis by (rule r2)
qed
qed
lemma (in classical) "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A" (* FIXME *)
proof -
assume r: "\<not> A \<Longrightarrow> A"
show A
proof (rule classical_cases)
assume A then show A .
next
assume "\<not> A" then show A by (rule r)
qed
qed
end