src/HOL/Isar_examples/Cantor.thy
changeset 7982 d534b897ce39
parent 7955 f30e08579481
child 9474 b0ce3b7c9c26
equal deleted inserted replaced
7981:5120a2a15d06 7982:d534b897ce39
    28   
    28   
    29  \bigskip We first consider a slightly awkward version of the proof,
    29  \bigskip We first consider a slightly awkward version of the proof,
    30  with the innermost reasoning expressed quite naively.
    30  with the innermost reasoning expressed quite naively.
    31 *};
    31 *};
    32 
    32 
    33 theorem "EX S. S ~: range(f :: 'a => 'a set)";
    33 theorem "EX S. S ~: range (f :: 'a => 'a set)";
    34 proof;
    34 proof;
    35   let ?S = "{x. x ~: f x}";
    35   let ?S = "{x. x ~: f x}";
    36   show "?S ~: range f";
    36   show "?S ~: range f";
    37   proof;
    37   proof;
    38     assume "?S : range f";
    38     assume "?S : range f";
    67  basic logical structure has to be left intact, though.  In
    67  basic logical structure has to be left intact, though.  In
    68  particular, assumptions ``belonging'' to some goal have to be
    68  particular, assumptions ``belonging'' to some goal have to be
    69  introduced \emph{before} its corresponding \isacommand{show}.}
    69  introduced \emph{before} its corresponding \isacommand{show}.}
    70 *};
    70 *};
    71 
    71 
    72 theorem "EX S. S ~: range(f :: 'a => 'a set)";
    72 theorem "EX S. S ~: range (f :: 'a => 'a set)";
    73 proof;
    73 proof;
    74   let ?S = "{x. x ~: f x}";
    74   let ?S = "{x. x ~: f x}";
    75   show "?S ~: range f";
    75   show "?S ~: range f";
    76   proof;
    76   proof;
    77     assume "?S : range f";
    77     assume "?S : range f";
    93   qed;
    93   qed;
    94 qed;
    94 qed;
    95 
    95 
    96 text {*
    96 text {*
    97  How much creativity is required?  As it happens, Isabelle can prove
    97  How much creativity is required?  As it happens, Isabelle can prove
    98  this theorem automatically.  The default context of the Isabelle's
    98  this theorem automatically.  The context of Isabelle's classical
    99  classical prover contains rules for most of the constructs of HOL's
    99  prover contains rules for most of the constructs of HOL's set theory.
   100  set theory.  We must augment it with \name{equalityCE} to break up
   100  We must augment it with \name{equalityCE} to break up set equalities,
   101  set equalities, and then apply best-first search.  Depth-first search
   101  and then apply best-first search.  Depth-first search would diverge,
   102  would diverge, but best-first search successfully navigates through
   102  but best-first search successfully navigates through the large search
   103  the large search space.
   103  space.
   104 *};
   104 *};
   105 
   105 
   106 theorem "EX S. S ~: range(f :: 'a => 'a set)";
   106 theorem "EX S. S ~: range (f :: 'a => 'a set)";
   107   by (best elim: equalityCE);
   107   by (best elim: equalityCE);
   108 
   108 
   109 text {*
   109 text {*
   110  While this establishes the same theorem internally, we do not get any
   110  While this establishes the same theorem internally, we do not get any
   111  idea of how the proof actually works.  There is currently no way to
   111  idea of how the proof actually works.  There is currently no way to
   112  transform internal system-level representations of Isabelle proofs
   112  transform internal system-level representations of Isabelle proofs
   113  back into Isar documents.  Writing intelligible proof documents
   113  back into Isar text.  Writing intelligible proof documents
   114  really is a creative process, after all.
   114  really is a creative process, after all.
   115 *};
   115 *};
   116 
   116 
   117 end;
   117 end;