--- a/src/HOL/ex/Higher_Order_Logic.thy Mon Nov 30 15:23:02 2015 +0100
+++ b/src/HOL/ex/Higher_Order_Logic.thy Mon Nov 30 19:12:08 2015 +0100
@@ -1,5 +1,5 @@
(* Title: HOL/ex/Higher_Order_Logic.thy
- Author: Gertrud Bauer and Markus Wenzel, TU Muenchen
+ Author: Makarius
*)
section \<open>Foundations of HOL\<close>
@@ -9,12 +9,11 @@
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 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>
@@ -30,35 +29,31 @@
subsubsection \<open>Basic logical connectives\<close>
-judgment Trueprop :: "o \<Rightarrow> prop" ("_" 5)
+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"
+axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o" (infixr "\<longrightarrow>" 25)
+ where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
+ and impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
+
+axiomatization All :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10)
+ 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"
+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"
+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
+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)
@@ -80,173 +75,187 @@
definition false :: o ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A"
+theorem falseE [elim]:
+ assumes "\<bottom>"
+ shows A
+proof -
+ from \<open>\<bottom>\<close> have "\<forall>A. A" unfolding false_def .
+ then show A ..
+qed
+
+
definition true :: o ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
+theorem trueI [intro]: \<top>
+ unfolding true_def ..
+
+
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]:
+ assumes "A \<Longrightarrow> \<bottom>"
+ shows "\<not> A"
+ using assms unfolding not_def ..
-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>" and A
- then have \<bottom> ..
+theorem notE [elim]:
+ assumes "\<not> A" and A
+ shows B
+proof -
+ from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" unfolding not_def .
+ from this and \<open>A\<close> 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>
+lemmas contradiction = notE notE' \<comment> \<open>proof by contradiction in any order\<close>
+
+
+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"
-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"
+theorem conjI [intro]:
+ assumes A and B
+ shows "A \<and> B"
+ unfolding conj_def
+proof
+ fix C
+ show "(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
+ assume "A \<longrightarrow> B \<longrightarrow> C"
+ also note \<open>A\<close>
+ also note \<open>B\<close>
+ finally show C .
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" ..
+theorem conjE [elim]:
+ assumes "A \<and> 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 \<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" ..
+ finally show ?thesis .
+ qed
+ show B
+ proof -
+ note * [of 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
+ finally show ?thesis .
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"
+
+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"
+
+theorem disjI1 [intro]:
+ assumes A
+ shows "A \<or> B"
+ unfolding disj_def
+proof
+ fix C
+ show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
proof
- fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+ assume "A \<longrightarrow> C"
+ from this and \<open>A\<close> have C ..
+ then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
+ qed
+qed
+
+theorem disjI2 [intro]:
+ assumes B
+ shows "A \<or> B"
+ unfolding disj_def
+proof
+ fix C
+ show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+ proof
+ show "(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
+ assume "B \<longrightarrow> C"
+ from this and \<open>B\<close> show C ..
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"
+theorem disjE [elim]:
+ assumes "A \<or> 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 \<longrightarrow> thesis"
proof
assume A
- then show C by (rule r1)
+ then show thesis by (rule a)
qed
- also have "B \<longrightarrow> C"
+ also have "B \<longrightarrow> thesis"
proof
assume B
- then show C by (rule r2)
+ then show thesis by (rule b)
qed
- finally show C .
+ finally show thesis .
qed
+
+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"
-proof (unfold Ex_def)
+ unfolding Ex_def
+proof
+ fix C
assume "P a"
- show "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
+ show "(\<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
+ assume "\<forall>x. P x \<longrightarrow> C"
+ then have "P a \<longrightarrow> C" ..
+ from this and \<open>P a\<close> show C ..
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"
+theorem exE [elim]:
+ assumes "\<exists>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 "\<forall>x. P x \<longrightarrow> thesis"
proof
- fix x show "P x \<longrightarrow> C"
+ fix x
+ show "P x \<longrightarrow> thesis"
proof
assume "P x"
- then show C by (rule r)
+ then show thesis by (rule that)
qed
qed
- finally show C .
+ finally show thesis .
qed
subsection \<open>Classical logic\<close>
+text \<open>
+ The subsequent rules of classical reasoning are all equivalent.
+\<close>
+
locale classical =
assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
@@ -265,14 +274,12 @@
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
+theorem (in classical) double_negation:
+ assumes "\<not> \<not> A"
+ shows A
+proof (rule classical)
+ assume "\<not> A"
+ with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
qed
theorem (in classical) tertium_non_datur: "A \<or> \<not> A"
@@ -290,27 +297,30 @@
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
+theorem (in classical) classical_cases:
+ obtains A | "\<not> A"
+ using tertium_non_datur
+proof
+ assume A
+ then show thesis ..
+next
+ assume "\<not> A"
+ then show thesis ..
+qed
+
+lemma
+ assumes classical_cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
+ shows "PROP classical"
+proof
+ fix A
+ assume *: "\<not> A \<Longrightarrow> A"
+ show A
+ proof (rule classical_cases)
assume A
- then show ?thesis by (rule r1)
+ then show A .
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)
+ then show A by (rule *)
qed
qed