author wenzelm Sat, 26 Dec 2015 19:37:06 +0100 changeset 61936 c51ce9ed0b1c parent 61935 6512e84cc9f5 child 61937 2a9bed6cd6e5
more notation; more examples;
```--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Sat Dec 26 19:27:46 2015 +0100
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Sat Dec 26 19:37:06 2015 +0100
@@ -46,9 +46,12 @@
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 = B"
+    and iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<longleftrightarrow> B"

theorem sym [sym]:
assumes "x = y"
@@ -64,10 +67,10 @@
theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
by (rule subst)

-theorem iff1 [elim]: "A = B \<Longrightarrow> A \<Longrightarrow> B"
+theorem iff1 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
by (rule subst)

-theorem iff2 [elim]: "A = B \<Longrightarrow> B \<Longrightarrow> A"
+theorem iff2 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> B \<Longrightarrow> A"
by (rule subst) (rule sym)

@@ -250,6 +253,39 @@
qed

+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>
+
+  assumes *: "\<not> A \<longleftrightarrow> A"
+  shows C
+proof (rule notE)
+  show "\<not> A"
+  proof
+    assume A
+    with * have "\<not> A" ..
+    from this and \<open>A\<close> show \<bottom> ..
+  qed
+  with * show A ..
+qed
+
+theorem Cantor: "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A :: 'a \<Rightarrow> o. \<exists>x :: 'a. A = f x)"
+proof
+  assume "\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. A = f x"
+  then obtain f :: "'a \<Rightarrow> 'a \<Rightarrow> o" where *: "\<forall>A. \<exists>x. A = f x" ..
+  let ?D = "\<lambda>x. \<not> f x x"
+  from * have "\<exists>x. ?D = f x" ..
+  then obtain a where "?D = f a" ..
+  then have "?D a \<longleftrightarrow> f a a" using refl by (rule subst)
+  then show \<bottom> by (rule iff_contradiction)
+qed
+
+
subsection \<open>Classical logic\<close>

text \<open>```