author wenzelm Sat, 05 Mar 2016 21:23:28 +0100 changeset 62523 5335e5c53312 parent 62522 d32c23d29968 child 62524 bf9a024ca238
tuned;
 src/HOL/Isar_Examples/Cantor.thy file | annotate | diff | comparison | revisions src/HOL/Isar_Examples/Drinker.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Isar_Examples/Cantor.thy	Sat Mar 05 20:47:31 2016 +0100
+++ b/src/HOL/Isar_Examples/Cantor.thy	Sat Mar 05 21:23:28 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. \<exists>x. A = f x)"
+theorem Cantor: "\<nexists>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" ..
@@ -35,10 +35,10 @@
works.
\<close>

-theorem "\<not> (\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. f x = A)"
+theorem "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. f x = A"
by best

-theorem "\<not> (\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. f x = A)"
+theorem "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. f x = A"
by force

@@ -63,7 +63,7 @@
with * show A ..
qed

-theorem Cantor': "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A. \<exists>x. A = f x)"
+theorem Cantor': "\<nexists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A. \<exists>x. A = f x"
proof
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" ..```
```--- a/src/HOL/Isar_Examples/Drinker.thy	Sat Mar 05 20:47:31 2016 +0100
+++ b/src/HOL/Isar_Examples/Drinker.thy	Sat Mar 05 21:23:28 2016 +0100
@@ -19,14 +19,14 @@
assumes "\<not> (\<forall>x. P x)"
shows "\<exists>x. \<not> P x"
proof (rule classical)
-  assume "\<not> (\<exists>x. \<not> P x)"
+  assume "\<nexists>x. \<not> P x"
have "\<forall>x. P x"
proof
fix x show "P x"
proof (rule classical)
assume "\<not> P x"
then have "\<exists>x. \<not> P x" ..
-      with \<open>\<not> (\<exists>x. \<not> P x)\<close> show ?thesis by contradiction
+      with \<open>\<nexists>x. \<not> P x\<close> show ?thesis by contradiction
qed
qed
with \<open>\<not> (\<forall>x. P x)\<close> show ?thesis by contradiction```