--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy Mon Jan 16 16:12:29 2017 +0100
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy Mon Jan 16 21:20:30 2017 +0100
@@ -9,15 +9,17 @@
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.
+ 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>
-subsection \<open>Pure Logic\<close>
+section \<open>HOL syntax within Pure\<close>
class type
default_sort type
@@ -26,10 +28,10 @@
instance o :: type ..
instance "fun" :: (type, type) type ..
+judgment Trueprop :: "o \<Rightarrow> prop" ("_" 5)
-subsubsection \<open>Basic logical connectives\<close>
-judgment Trueprop :: "o \<Rightarrow> prop" ("_" 5)
+section \<open>Minimal logic (axiomatization)\<close>
axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25)
where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
@@ -39,79 +41,48 @@
where 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"
-
-abbreviation iff :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longleftrightarrow>" 25)
- where "A \<longleftrightarrow> B \<equiv> A = B"
-
-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 \<longleftrightarrow> B"
+lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)"
+ by standard (fact impI, fact impE)
-theorem sym [sym]:
- assumes "x = y"
- shows "y = x"
- using assms by (rule subst) (rule refl)
-
-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 \<longleftrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
- by (rule subst)
-
-theorem iff2 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> B \<Longrightarrow> A"
- by (rule subst) (rule sym)
+lemma atomize_all [atomize]: "(\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x)"
+ by standard (fact allI, fact allE)
subsubsection \<open>Derived connectives\<close>
-definition false :: o ("\<bottom>")
- where "\<bottom> \<equiv> \<forall>A. A"
+definition False :: o
+ where "False \<equiv> \<forall>A. A"
-theorem falseE [elim]:
- assumes "\<bottom>"
+lemma FalseE [elim]:
+ assumes "False"
shows A
proof -
- from \<open>\<bottom>\<close> have "\<forall>A. A" by (simp only: false_def)
+ from \<open>False\<close> have "\<forall>A. A" by (simp only: False_def)
then show A ..
qed
-definition true :: o ("\<top>")
- where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
+definition True :: o
+ where "True \<equiv> False \<longrightarrow> False"
-theorem trueI [intro]: \<top>
- unfolding true_def ..
+lemma TrueI [intro]: True
+ unfolding True_def ..
definition not :: "o \<Rightarrow> o" ("\<not> _" [40] 40)
- where "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
+ where "not \<equiv> \<lambda>A. A \<longrightarrow> False"
-abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50)
- where "x \<noteq> y \<equiv> \<not> (x = y)"
-
-theorem notI [intro]:
- assumes "A \<Longrightarrow> \<bottom>"
+lemma notI [intro]:
+ assumes "A \<Longrightarrow> False"
shows "\<not> A"
using assms unfolding not_def ..
-theorem notE [elim]:
+lemma notE [elim]:
assumes "\<not> A" and A
shows B
proof -
- from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" by (simp only: not_def)
- from this and \<open>A\<close> have "\<bottom>" ..
+ 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
@@ -122,9 +93,9 @@
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"
+ where "A \<and> B \<equiv> \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
-theorem conjI [intro]:
+lemma conjI [intro]:
assumes A and B
shows "A \<and> B"
unfolding conj_def
@@ -139,7 +110,7 @@
qed
qed
-theorem conjE [elim]:
+lemma conjE [elim]:
assumes "A \<and> B"
obtains A and B
proof
@@ -168,9 +139,9 @@
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"
+ where "A \<or> B \<equiv> \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
-theorem disjI1 [intro]:
+lemma disjI1 [intro]:
assumes A
shows "A \<or> B"
unfolding disj_def
@@ -184,7 +155,7 @@
qed
qed
-theorem disjI2 [intro]:
+lemma disjI2 [intro]:
assumes B
shows "A \<or> B"
unfolding disj_def
@@ -200,7 +171,7 @@
qed
qed
-theorem disjE [elim]:
+lemma disjE [elim]:
assumes "A \<or> B"
obtains (a) A | (b) B
proof -
@@ -223,7 +194,7 @@
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"
-theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
+lemma exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
unfolding Ex_def
proof
fix C
@@ -236,7 +207,7 @@
qed
qed
-theorem exE [elim]:
+lemma exE [elim]:
assumes "\<exists>x. P x"
obtains (that) x where "P x"
proof -
@@ -255,6 +226,47 @@
qed
+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"
+
+abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o" (infixl "\<noteq>" 50)
+ where "x \<noteq> y \<equiv> \<not> (x = y)"
+
+abbreviation iff :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longleftrightarrow>" 25)
+ where "A \<longleftrightarrow> B \<equiv> A = B"
+
+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 \<longleftrightarrow> B"
+
+lemma sym [sym]: "y = x" if "x = y"
+ using that by (rule subst) (rule refl)
+
+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)
+
+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 \<Longrightarrow> y = z \<Longrightarrow> x = z"
+ by (rule subst)
+
+lemma iff1 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
+ by (rule subst)
+
+lemma iff2 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> B \<Longrightarrow> A"
+ by (rule subst) (rule sym)
+
+
subsection \<open>Cantor's Theorem\<close>
text \<open>
@@ -271,7 +283,7 @@
proof
assume A
with * have "\<not> A" ..
- from this and \<open>A\<close> show \<bottom> ..
+ from this and \<open>A\<close> show False ..
qed
with * show A ..
qed
@@ -285,11 +297,11 @@
then obtain a where "?D = f a" ..
then have "?D a \<longleftrightarrow> f a a" using refl by (rule subst)
then have "\<not> f a a \<longleftrightarrow> f a a" .
- then show \<bottom> by (rule iff_contradiction)
+ then show False by (rule iff_contradiction)
qed
-subsection \<open>Classical logic\<close>
+subsection \<open>Characterization of Classical Logic\<close>
text \<open>
The subsequent rules of classical reasoning are all equivalent.
@@ -297,8 +309,10 @@
locale classical =
assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
+ \<comment> \<open>predicate definition and hypothetical context\<close>
+begin
-theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
+theorem Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
proof
assume *: "(A \<longrightarrow> B) \<longrightarrow> A"
show A
@@ -313,7 +327,7 @@
qed
qed
-theorem (in classical) double_negation:
+lemma double_negation:
assumes "\<not> \<not> A"
shows A
proof (rule classical)
@@ -321,7 +335,7 @@
with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
qed
-theorem (in classical) tertium_non_datur: "A \<or> \<not> A"
+lemma tertium_non_datur: "A \<or> \<not> A"
proof (rule double_negation)
show "\<not> \<not> (A \<or> \<not> A)"
proof
@@ -329,14 +343,14 @@
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)
+ with \<open>\<not> (A \<or> \<not> A)\<close> show False by (rule contradiction)
qed
then have "A \<or> \<not> A" ..
- with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction)
+ with \<open>\<not> (A \<or> \<not> A)\<close> show False by (rule contradiction)
qed
qed
-theorem (in classical) classical_cases:
+lemma classical_cases:
obtains A | "\<not> A"
using tertium_non_datur
proof
@@ -347,14 +361,15 @@
then show thesis ..
qed
-lemma
- assumes classical_cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
- shows "PROP classical"
+end
+
+lemma classical_if_cases: classical
+ if cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
proof
fix A
assume *: "\<not> A \<Longrightarrow> A"
show A
- proof (rule classical_cases)
+ proof (rule cases)
assume A
then show A .
next
@@ -363,4 +378,124 @@
qed
qed
+
+section \<open>Hilbert's choice operator (axiomatization)\<close>
+
+axiomatization Eps :: "('a \<Rightarrow> o) \<Rightarrow> 'a"
+ where someI: "P x \<Longrightarrow> P (Eps P)"
+
+syntax "_Eps" :: "pttrn \<Rightarrow> o \<Rightarrow> '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 \<or> \<not> A"
+proof -
+ let ?P = "\<lambda>x. (A \<and> x) \<or> \<not> x"
+ let ?Q = "\<lambda>x. (A \<and> \<not> x) \<or> x"
+
+ have a: "?P (Eps ?P)"
+ proof (rule someI)
+ have "\<not> 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 \<and> Eps ?P"
+ then have A ..
+ then show ?thesis ..
+ next
+ assume "\<not> Eps ?P"
+ from b show ?thesis
+ proof
+ assume "A \<and> \<not> Eps ?Q"
+ then have A ..
+ then show ?thesis ..
+ next
+ assume "Eps ?Q"
+ have neq: "?P \<noteq> ?Q"
+ proof
+ assume "?P = ?Q"
+ then have "Eps ?P \<longleftrightarrow> 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 "\<not> A"
+ proof
+ assume A
+ have "?P = ?Q"
+ proof (rule ext)
+ show "?P x \<longleftrightarrow> ?Q x" for x
+ proof
+ assume "?P x"
+ then show "?Q x"
+ proof
+ assume "\<not> x"
+ with \<open>A\<close> have "A \<and> \<not> x" ..
+ then show ?thesis ..
+ next
+ assume "A \<and> x"
+ then have x ..
+ then show ?thesis ..
+ qed
+ next
+ assume "?Q x"
+ then show "?P x"
+ proof
+ assume "A \<and> \<not> x"
+ then have "\<not> 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 classical} always holds
+ unconditionally (with all consequences).
+\<close>
+
+interpretation classical
+proof (rule classical_if_cases)
+ fix A C
+ assume *: "A \<Longrightarrow> C"
+ and **: "\<not> A \<Longrightarrow> C"
+ from Diaconescu [of A] show C
+ proof
+ assume A
+ then show C by (rule *)
+ next
+ assume "\<not> A"
+ then show C by (rule **)
+ qed
+qed
+
+thm classical
+ Peirce's_Law
+ double_negation
+ tertium_non_datur
+ classical_cases
+
end
--- a/src/HOL/Isar_Examples/document/root.bib Mon Jan 16 16:12:29 2017 +0100
+++ b/src/HOL/Isar_Examples/document/root.bib Mon Jan 16 21:20:30 2017 +0100
@@ -4,6 +4,14 @@
@string{Springer="Springer-Verlag"}
@string{TUM="TU Munich"}
+@article{church40,
+ author = "Alonzo Church",
+ title = "A Formulation of the Simple Theory of Types",
+ journal = "Journal of Symbolic Logic",
+ year = 1940,
+ volume = 5,
+ pages = "56-68"}
+
@Book{Concrete-Math,
author = {R. L. Graham and D. E. Knuth and O. Patashnik},
title = {Concrete Mathematics},