# HG changeset patch
# User wenzelm
# Date 1451155026 -3600
# Node ID c51ce9ed0b1c23eccda5f2cb6751eaf83ba245c6
# Parent  6512e84cc9f5d3d21bb5fc889a72904949bed120
more notation;
more examples;

diff -r 6512e84cc9f5 -r c51ce9ed0b1c src/HOL/Isar_Examples/Higher_Order_Logic.thy
--- 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>
+
+lemma iff_contradiction:
+  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>