author wenzelm Sat, 02 Jan 2016 16:32:36 +0100 changeset 62038 5651de00bca9 parent 62037 9bb80149dad9 child 62039 a77f4a9037d4
tuned;
```--- a/src/HOL/Isar_Examples/Cantor.thy	Sat Jan 02 16:15:28 2016 +0100
+++ b/src/HOL/Isar_Examples/Cantor.thy	Sat Jan 02 16:32:36 2016 +0100
@@ -17,7 +17,7 @@
\<^item> @{url "https://en.wikipedia.org/wiki/Cantor's_diagonal_argument"}
\<close>

-theorem Cantor: "\<not> (\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A :: 'a set. \<exists>x :: 'a. A = f x)"
+theorem Cantor: "\<not> (\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x)"
proof
assume "\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
then obtain f :: "'a \<Rightarrow> 'a set" where *: "\<forall>A. \<exists>x. A = f x" ..
@@ -63,14 +63,14 @@
with * show A ..
qed

-theorem Cantor': "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A :: 'a \<Rightarrow> bool. \<exists>x :: 'a. A = f x)"
+theorem Cantor': "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A. \<exists>x. A = f x)"
proof
-  assume "\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A :: 'a \<Rightarrow> bool. \<exists>x. A = f x"
+  assume "\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A. \<exists>x. A = f x"
then obtain f :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 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 have "?D a \<longleftrightarrow> f a a" by (rule arg_cong)
then show False by (rule iff_contradiction)
qed
```
```--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Sat Jan 02 16:15:28 2016 +0100
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Sat Jan 02 16:32:36 2016 +0100
@@ -274,7 +274,7 @@
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)"
+theorem Cantor: "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. 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" ..```