src/HOL/Isar_examples/Cantor.thy
 changeset 10007 64bf7da1994a parent 9474 b0ce3b7c9c26 child 12388 c845fec1ac94
     1.1 --- a/src/HOL/Isar_examples/Cantor.thy	Sun Sep 17 22:15:08 2000 +0200
1.2 +++ b/src/HOL/Isar_examples/Cantor.thy	Sun Sep 17 22:19:02 2000 +0200
1.3 @@ -3,14 +3,14 @@
1.4      Author:     Markus Wenzel, TU Muenchen
1.5  *)
1.6
1.7 -header {* Cantor's Theorem *};
1.8 +header {* Cantor's Theorem *}
1.9
1.10 -theory Cantor = Main:;
1.11 +theory Cantor = Main:
1.12
1.13  text_raw {*
1.14   \footnote{This is an Isar version of the final example of the
1.15   Isabelle/HOL manual \cite{isabelle-HOL}.}
1.16 -*};
1.17 +*}
1.18
1.19  text {*
1.20   Cantor's Theorem states that every set has more subsets than it has
1.21 @@ -28,33 +28,33 @@
1.22
1.23   \bigskip We first consider a slightly awkward version of the proof,
1.24   with the innermost reasoning expressed quite naively.
1.25 -*};
1.26 +*}
1.27
1.28 -theorem "EX S. S ~: range (f :: 'a => 'a set)";
1.29 -proof;
1.30 -  let ?S = "{x. x ~: f x}";
1.31 -  show "?S ~: range f";
1.32 -  proof;
1.33 -    assume "?S : range f";
1.34 -    thus False;
1.35 -    proof;
1.36 -      fix y;
1.37 -      assume "?S = f y";
1.38 -      thus ?thesis;
1.39 -      proof (rule equalityCE);
1.40 -        assume in_S: "y : ?S";
1.41 -        assume in_fy: "y : f y";
1.42 -        from in_S; have notin_fy: "y ~: f y"; ..;
1.43 -        from notin_fy in_fy; show ?thesis; by contradiction;
1.44 -      next;
1.45 -        assume notin_S: "y ~: ?S";
1.46 -        assume notin_fy: "y ~: f y";
1.47 -        from notin_S; have in_fy: "y : f y"; ..;
1.48 -        from notin_fy in_fy; show ?thesis; by contradiction;
1.49 -      qed;
1.50 -    qed;
1.51 -  qed;
1.52 -qed;
1.53 +theorem "EX S. S ~: range (f :: 'a => 'a set)"
1.54 +proof
1.55 +  let ?S = "{x. x ~: f x}"
1.56 +  show "?S ~: range f"
1.57 +  proof
1.58 +    assume "?S : range f"
1.59 +    thus False
1.60 +    proof
1.61 +      fix y
1.62 +      assume "?S = f y"
1.63 +      thus ?thesis
1.64 +      proof (rule equalityCE)
1.65 +        assume in_S: "y : ?S"
1.66 +        assume in_fy: "y : f y"
1.67 +        from in_S have notin_fy: "y ~: f y" ..
1.68 +        from notin_fy in_fy show ?thesis by contradiction
1.69 +      next
1.70 +        assume notin_S: "y ~: ?S"
1.71 +        assume notin_fy: "y ~: f y"
1.72 +        from notin_S have in_fy: "y : f y" ..
1.73 +        from notin_fy in_fy show ?thesis by contradiction
1.74 +      qed
1.75 +    qed
1.76 +  qed
1.77 +qed
1.78
1.79  text {*
1.80   The following version of the proof essentially does the same
1.81 @@ -67,31 +67,31 @@
1.82   basic logical structure has to be left intact, though.  In
1.83   particular, assumptions belonging'' to some goal have to be
1.84   introduced \emph{before} its corresponding \isacommand{show}.}
1.85 -*};
1.86 +*}
1.87
1.88 -theorem "EX S. S ~: range (f :: 'a => 'a set)";
1.89 -proof;
1.90 -  let ?S = "{x. x ~: f x}";
1.91 -  show "?S ~: range f";
1.92 -  proof;
1.93 -    assume "?S : range f";
1.94 -    thus False;
1.95 -    proof;
1.96 -      fix y;
1.97 -      assume "?S = f y";
1.98 -      thus ?thesis;
1.99 -      proof (rule equalityCE);
1.100 -        assume "y : f y";
1.101 -        assume "y : ?S"; hence "y ~: f y"; ..;
1.102 -        thus ?thesis; by contradiction;
1.103 -      next;
1.104 -        assume "y ~: f y";
1.105 -        assume "y ~: ?S"; hence "y : f y"; ..;
1.106 -        thus ?thesis; by contradiction;
1.107 -      qed;
1.108 -    qed;
1.109 -  qed;
1.110 -qed;
1.111 +theorem "EX S. S ~: range (f :: 'a => 'a set)"
1.112 +proof
1.113 +  let ?S = "{x. x ~: f x}"
1.114 +  show "?S ~: range f"
1.115 +  proof
1.116 +    assume "?S : range f"
1.117 +    thus False
1.118 +    proof
1.119 +      fix y
1.120 +      assume "?S = f y"
1.121 +      thus ?thesis
1.122 +      proof (rule equalityCE)
1.123 +        assume "y : f y"
1.124 +        assume "y : ?S" hence "y ~: f y" ..
1.125 +        thus ?thesis by contradiction
1.126 +      next
1.127 +        assume "y ~: f y"
1.128 +        assume "y ~: ?S" hence "y : f y" ..
1.129 +        thus ?thesis by contradiction
1.130 +      qed
1.131 +    qed
1.132 +  qed
1.133 +qed
1.134
1.135  text {*
1.136   How much creativity is required?  As it happens, Isabelle can prove
1.137 @@ -100,10 +100,10 @@
1.138   through the large search space.  The context of Isabelle's classical
1.139   prover contains rules for the relevant constructs of HOL's set
1.140   theory.
1.141 -*};
1.142 +*}
1.143
1.144 -theorem "EX S. S ~: range (f :: 'a => 'a set)";
1.145 -  by best;
1.146 +theorem "EX S. S ~: range (f :: 'a => 'a set)"
1.147 +  by best
1.148
1.149  text {*
1.150   While this establishes the same theorem internally, we do not get any
1.151 @@ -111,6 +111,6 @@
1.152   transform internal system-level representations of Isabelle proofs
1.153   back into Isar text.  Writing intelligible proof documents
1.154   really is a creative process, after all.
1.155 -*};
1.156 +*}
1.157
1.158 -end;
1.159 +end