(* Title: Pure/Examples/Higher_Order_Logic.thy
Author: Makarius
*)
section \<open>Foundations of HOL\<close>
theory Higher_Order_Logic
imports Pure
begin
text \<open>
The following theory development illustrates the foundations of Higher-Order
Logic. The ``HOL'' logic that is given here resembles @{cite
"Gordon:1985:HOL"} and its predecessor @{cite "church40"}, but the order of
axiomatizations and defined connectives has be adapted to modern
presentations of \<open>\<lambda>\<close>-calculus and Constructive Type Theory. Thus it fits
nicely to the underlying Natural Deduction framework of Isabelle/Pure and
Isabelle/Isar.
\<close>
section \<open>HOL syntax within Pure\<close>
class type
default_sort type
typedecl o
instance o :: type ..
instance "fun" :: (type, type) type ..
judgment Trueprop :: "o \ prop" ("_" 5)
section \<open>Minimal logic (axiomatization)\<close>
axiomatization imp :: "o \ o \ o" (infixr "\" 25)
where impI [intro]: "(A \ B) \ A \ B"
and impE [dest, trans]: "A \ B \ A \ B"
axiomatization All :: "('a \ o) \ o" (binder "\" 10)
where allI [intro]: "(\x. P x) \ \x. P x"
and allE [dest]: "\x. P x \ P a"
lemma atomize_imp [atomize]: "(A \ B) \ Trueprop (A \ B)"
by standard (fact impI, fact impE)
lemma atomize_all [atomize]: "(\x. P x) \ Trueprop (\x. P x)"
by standard (fact allI, fact allE)
subsubsection \<open>Derived connectives\<close>
definition False :: o
where "False \ \A. A"
lemma FalseE [elim]:
assumes "False"
shows A
proof -
from \<open>False\<close> have "\<forall>A. A" by (simp only: False_def)
then show A ..
qed
definition True :: o
where "True \ False \ False"
lemma TrueI [intro]: True
unfolding True_def ..
definition not :: "o \ o" ("\ _" [40] 40)
where "not \ \A. A \ False"
lemma notI [intro]:
assumes "A \ False"
shows "\ A"
using assms unfolding not_def ..
lemma notE [elim]:
assumes "\ A" and A
shows B
proof -
from \<open>\<not> A\<close> have "A \<longrightarrow> False" by (simp only: not_def)
from this and \<open>A\<close> have "False" ..
then show B ..
qed
lemma notE': "A \ \ A \ B"
by (rule notE)
lemmas contradiction = notE notE' \ \proof by contradiction in any order\
definition conj :: "o \ o \ o" (infixr "\" 35)
where "A \ B \ \C. (A \ B \ C) \ C"
lemma conjI [intro]:
assumes A and B
shows "A \ B"
unfolding conj_def
proof
fix C
show "(A \ B \ C) \ C"
proof
assume "A \ B \ C"
also note \<open>A\<close>
also note \<open>B\<close>
finally show C .
qed
qed
lemma conjE [elim]:
assumes "A \ B"
obtains A and B
proof
from \<open>A \<and> B\<close> have *: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" for C
unfolding conj_def ..
show A
proof -
note * [of A]
also have "A \ B \ A"
proof
assume A
then show "B \ A" ..
qed
finally show ?thesis .
qed
show B
proof -
note * [of B]
also have "A \ B \ B"
proof
show "B \ B" ..
qed
finally show ?thesis .
qed
qed
definition disj :: "o \ o \ o" (infixr "\" 30)
where "A \ B \ \C. (A \ C) \ (B \ C) \ C"
lemma disjI1 [intro]:
assumes A
shows "A \ B"
unfolding disj_def
proof
fix C
show "(A \ C) \ (B \ C) \ C"
proof
assume "A \ C"
from this and \<open>A\<close> have C ..
then show "(B \ C) \ C" ..
qed
qed
lemma disjI2 [intro]:
assumes B
shows "A \ B"
unfolding disj_def
proof
fix C
show "(A \ C) \ (B \ C) \ C"
proof
show "(B \ C) \ C"
proof
assume "B \ C"
from this and \<open>B\<close> show C ..
qed
qed
qed
lemma disjE [elim]:
assumes "A \ B"
obtains (a) A | (b) B
proof -
from \<open>A \<or> B\<close> have "(A \<longrightarrow> thesis) \<longrightarrow> (B \<longrightarrow> thesis) \<longrightarrow> thesis"
unfolding disj_def ..
also have "A \ thesis"
proof
assume A
then show thesis by (rule a)
qed
also have "B \ thesis"
proof
assume B
then show thesis by (rule b)
qed
finally show thesis .
qed
definition Ex :: "('a \ o) \ o" (binder "\" 10)
where "\x. P x \ \C. (\x. P x \ C) \ C"
lemma exI [intro]: "P a \ \x. P x"
unfolding Ex_def
proof
fix C
assume "P a"
show "(\x. P x \ C) \ C"
proof
assume "\x. P x \ C"
then have "P a \ C" ..
from this and \<open>P a\<close> show C ..
qed
qed
lemma exE [elim]:
assumes "\x. P x"
obtains (that) x where "P x"
proof -
from \<open>\<exists>x. P x\<close> have "(\<forall>x. P x \<longrightarrow> thesis) \<longrightarrow> thesis"
unfolding Ex_def ..
also have "\x. P x \ thesis"
proof
fix x
show "P x \ thesis"
proof
assume "P x"
then show thesis by (rule that)
qed
qed
finally show thesis .
qed
subsubsection \<open>Extensional equality\<close>
axiomatization equal :: "'a \ 'a \ o" (infixl "=" 50)
where refl [intro]: "x = x"
and subst: "x = y \ P x \ P y"
abbreviation not_equal :: "'a \ 'a \ o" (infixl "\" 50)
where "x \ y \ \ (x = y)"
abbreviation iff :: "o \ o \ o" (infixr "\" 25)
where "A \ B \ A = B"
axiomatization
where ext [intro]: "(\x. f x = g x) \ f = g"
and iff [intro]: "(A \ B) \ (B \ A) \ A \ B"
for f g :: "'a \ 'b"
lemma sym [sym]: "y = x" if "x = y"
using that by (rule subst) (rule refl)
lemma [trans]: "x = y \ P y \ P x"
by (rule subst) (rule sym)
lemma [trans]: "P x \ x = y \ P y"
by (rule subst)
lemma arg_cong: "f x = f y" if "x = y"
using that by (rule subst) (rule refl)
lemma fun_cong: "f x = g x" if "f = g"
using that by (rule subst) (rule refl)
lemma trans [trans]: "x = y \ y = z \ x = z"
by (rule subst)
lemma iff1 [elim]: "A \ B \ A \ B"
by (rule subst)
lemma iff2 [elim]: "A \ B \ B \ A"
by (rule subst) (rule sym)
subsection \<open>Cantor's Theorem\<close>
text \<open>
Cantor's Theorem states that there is no surjection from a set to its
powerset. The subsequent formulation uses elementary \<open>\<lambda>\<close>-calculus and
predicate logic, with standard introduction and elimination rules.
\<close>
lemma iff_contradiction:
assumes *: "\ A \ A"
shows C
proof (rule notE)
show "\ A"
proof
assume A
with * have "\ A" ..
from this and \<open>A\<close> show False ..
qed
with * show A ..
qed
theorem Cantor: "\ (\f :: 'a \ 'a \ o. \A. \x. A = f x)"
proof
assume "\f :: 'a \ 'a \ o. \A. \x. A = f x"
then obtain f :: "'a \ 'a \ o" where *: "\A. \x. A = f x" ..
let ?D = "\x. \ f x x"
from * have "\x. ?D = f x" ..
then obtain a where "?D = f a" ..
then have "?D a \ f a a" using refl by (rule subst)
then have "\ f a a \ f a a" .
then show False by (rule iff_contradiction)
qed
subsection \<open>Characterization of Classical Logic\<close>
text \<open>
The subsequent rules of classical reasoning are all equivalent.
\<close>
locale classical =
assumes classical: "(\ A \ A) \ A"
\<comment> \<open>predicate definition and hypothetical context\<close>
begin
lemma classical_contradiction:
assumes "\ A \ False"
shows A
proof (rule classical)
assume "\ A"
then have False by (rule assms)
then show A ..
qed
lemma double_negation:
assumes "\ \ A"
shows A
proof (rule classical_contradiction)
assume "\ A"
with \<open>\<not> \<not> A\<close> show False by (rule contradiction)
qed
lemma 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 \<open>\<not> (A \<or> \<not> A)\<close> show False by (rule contradiction)
qed
then have "A \ \ A" ..
with \<open>\<not> (A \<or> \<not> A)\<close> show False by (rule contradiction)
qed
qed
lemma classical_cases:
obtains A | "\ A"
using tertium_non_datur
proof
assume A
then show thesis ..
next
assume "\ A"
then show thesis ..
qed
end
lemma classical_if_cases: classical
if cases: "\A C. (A \ C) \ (\ A \ C) \ C"
proof
fix A
assume *: "\ A \ A"
show A
proof (rule cases)
assume A
then show A .
next
assume "\ A"
then show A by (rule *)
qed
qed
section \<open>Peirce's Law\<close>
text \<open>
Peirce's Law is another characterization of classical reasoning. Its
statement only requires implication.
\<close>
theorem (in classical) Peirce's_Law: "((A \ B) \ A) \ A"
proof
assume *: "(A \ B) \ A"
show A
proof (rule classical)
assume "\ A"
have "A \ B"
proof
assume A
with \<open>\<not> A\<close> show B by (rule contradiction)
qed
with * show A ..
qed
qed
section \<open>Hilbert's choice operator (axiomatization)\<close>
axiomatization Eps :: "('a \ o) \ 'a"
where someI: "P x \ P (Eps P)"
syntax "_Eps" :: "pttrn \ o \ 'a" ("(3SOME _./ _)" [0, 10] 10)
translations "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
text \<open>
\<^medskip>
It follows a derivation of the classical law of tertium-non-datur by
means of Hilbert's choice operator (due to Berghofer, Beeson, Harrison,
based on a proof by Diaconescu).
\<^medskip>
\<close>
theorem Diaconescu: "A \ \ A"
proof -
let ?P = "\x. (A \ x) \ \ x"
let ?Q = "\x. (A \ \ x) \ x"
have a: "?P (Eps ?P)"
proof (rule someI)
have "\ False" ..
then show "?P False" ..
qed
have b: "?Q (Eps ?Q)"
proof (rule someI)
have True ..
then show "?Q True" ..
qed
from a show ?thesis
proof
assume "A \ Eps ?P"
then have A ..
then show ?thesis ..
next
assume "\ Eps ?P"
from b show ?thesis
proof
assume "A \ \ Eps ?Q"
then have A ..
then show ?thesis ..
next
assume "Eps ?Q"
have neq: "?P \ ?Q"
proof
assume "?P = ?Q"
then have "Eps ?P \ Eps ?Q" by (rule arg_cong)
also note \<open>Eps ?Q\<close>
finally have "Eps ?P" .
with \<open>\<not> Eps ?P\<close> show False by (rule contradiction)
qed
have "\ A"
proof
assume A
have "?P = ?Q"
proof (rule ext)
show "?P x \ ?Q x" for x
proof
assume "?P x"
then show "?Q x"
proof
assume "\ x"
with \<open>A\<close> have "A \<and> \<not> x" ..
then show ?thesis ..
next
assume "A \ x"
then have x ..
then show ?thesis ..
qed
next
assume "?Q x"
then show "?P x"
proof
assume "A \ \ x"
then have "\ x" ..
then show ?thesis ..
next
assume x
with \<open>A\<close> have "A \<and> x" ..
then show ?thesis ..
qed
qed
qed
with neq show False by (rule contradiction)
qed
then show ?thesis ..
qed
qed
qed
text \<open>
This means, the hypothetical predicate \<^const>\<open>classical\<close> always holds
unconditionally (with all consequences).
\<close>
interpretation classical
proof (rule classical_if_cases)
fix A C
assume *: "A \ C"
and **: "\ A \ C"
from Diaconescu [of A] show C
proof
assume A
then show C by (rule *)
next
assume "\ A"
then show C by (rule **)
qed
qed
thm classical
classical_contradiction
double_negation
tertium_non_datur
classical_cases
Peirce's_Law
end
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
