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