src/HOL/Isar_examples/Cantor.thy
 author wenzelm Fri Apr 23 11:50:35 1999 +0200 (1999-04-23) changeset 6494 ab1442d2e4e1 parent 6444 2ebe9e630cab child 6505 2863855a6902 permissions -rw-r--r--
detailed proofs;
 wenzelm@6444 ` 1` ```(* Title: HOL/Isar_examples/Cantor.thy ``` wenzelm@6444 ` 2` ``` ID: \$Id\$ ``` wenzelm@6444 ` 3` ``` Author: Markus Wenzel, TU Muenchen ``` wenzelm@6444 ` 4` wenzelm@6444 ` 5` ```Cantor's theorem (see also 'Isabelle's Object-Logics'). ``` wenzelm@6444 ` 6` ```*) ``` wenzelm@6444 ` 7` wenzelm@6444 ` 8` ```theory Cantor = Main:; ``` wenzelm@6444 ` 9` wenzelm@6494 ` 10` wenzelm@6494 ` 11` ```theorem "EX S. S ~: range(f :: 'a => 'a set)"; ``` wenzelm@6494 ` 12` ```proof; ``` wenzelm@6494 ` 13` ``` let ??S = "{x. x ~: f x}"; ``` wenzelm@6494 ` 14` ``` show "??S ~: range f"; ``` wenzelm@6494 ` 15` ``` proof; ``` wenzelm@6494 ` 16` ``` assume "??S : range f"; ``` wenzelm@6494 ` 17` ``` then; show False; ``` wenzelm@6494 ` 18` ``` proof; ``` wenzelm@6494 ` 19` ``` fix y; ``` wenzelm@6494 ` 20` ``` assume "??S = f y"; ``` wenzelm@6494 ` 21` ``` then; show ??thesis; ``` wenzelm@6494 ` 22` ``` proof (rule equalityCE); ``` wenzelm@6494 ` 23` ``` assume y_in_S: "y : ??S"; ``` wenzelm@6494 ` 24` ``` assume y_in_fy: "y : f y"; ``` wenzelm@6494 ` 25` ``` from y_in_S; have y_notin_fy: "y ~: f y"; ..; ``` wenzelm@6494 ` 26` ``` from y_notin_fy y_in_fy; show ??thesis; ..; ``` wenzelm@6494 ` 27` ``` next; ``` wenzelm@6494 ` 28` ``` assume y_notin_S: "y ~: ??S"; ``` wenzelm@6494 ` 29` ``` assume y_notin_fy: "y ~: f y"; ``` wenzelm@6494 ` 30` ``` from y_notin_S; have y_in_fy: "y : f y"; ..; ``` wenzelm@6494 ` 31` ``` from y_notin_fy y_in_fy; show ??thesis; ..; ``` wenzelm@6494 ` 32` ``` qed; ``` wenzelm@6494 ` 33` ``` qed; ``` wenzelm@6494 ` 34` ``` qed; ``` wenzelm@6494 ` 35` ```qed; ``` wenzelm@6494 ` 36` wenzelm@6494 ` 37` wenzelm@6494 ` 38` ```theorem "EX S. S ~: range(f :: 'a => 'a set)"; ``` wenzelm@6494 ` 39` ```proof; ``` wenzelm@6494 ` 40` ``` let ??S = "{x. x ~: f x}"; ``` wenzelm@6494 ` 41` ``` show "??S ~: range f"; ``` wenzelm@6494 ` 42` ``` proof; ``` wenzelm@6494 ` 43` ``` assume "??S : range f"; ``` wenzelm@6494 ` 44` ``` then; show False; ``` wenzelm@6494 ` 45` ``` proof; ``` wenzelm@6494 ` 46` ``` fix y; ``` wenzelm@6494 ` 47` ``` assume "??S = f y"; ``` wenzelm@6494 ` 48` ``` then; show ??thesis; ``` wenzelm@6494 ` 49` ``` proof (rule equalityCE); ``` wenzelm@6494 ` 50` ``` assume "y : ??S"; then; have y_notin_fy: "y ~: f y"; ..; ``` wenzelm@6494 ` 51` ``` assume "y : f y"; ``` wenzelm@6494 ` 52` ``` from y_notin_fy it; show ??thesis; ..; ``` wenzelm@6494 ` 53` ``` next; ``` wenzelm@6494 ` 54` ``` assume "y ~: ??S"; then; have y_in_fy: "y : f y"; ..; ``` wenzelm@6494 ` 55` ``` assume "y ~: f y"; ``` wenzelm@6494 ` 56` ``` from it y_in_fy; show ??thesis; ..; ``` wenzelm@6494 ` 57` ``` qed; ``` wenzelm@6494 ` 58` ``` qed; ``` wenzelm@6494 ` 59` ``` qed; ``` wenzelm@6494 ` 60` ```qed; ``` wenzelm@6494 ` 61` wenzelm@6494 ` 62` wenzelm@6494 ` 63` ```theorem "EX S. S ~: range(f :: 'a => 'a set)"; ``` wenzelm@6494 ` 64` ``` by (best elim: equalityCE); ``` wenzelm@6494 ` 65` wenzelm@6444 ` 66` wenzelm@6444 ` 67` ```end; ```