miz3/Samples/drinker.ml

   1 horizon := 0;;
   2
   3 thm `;
   4   assume ?x:A. T [1];
   5   let P be A->bool;
   6   thus ?x. P x ==> !y. P y
   7   proof
   8     (?x. ~P x) \/ ~(?x. ~P x);  // LEM
   9     cases by -;                 // \/E
  10     suppose ?x. ~P x;
  11       consider x such that
  12         ~P x [2] by -;          // ?E
  13       take x;                   // ?I
  14       assume P x;               // ==>I
  15       F by 2,-;                 // ~E
  16     qed by -;                   // FE
  17     suppose ~(?x. ~P x) [3];
  18       consider x such that
  19         (\x:A. T) x by 1;       // ?E
  20       take x;                   // ?I
  21       assume P x;               // ==>I
  22       let y be A;               // !I
  23       P y \/ ~P y;              // LEM
  24       cases by -;               // \/E
  25       suppose P y;
  26       qed by -;                 //
  27       suppose ~P y;
  28         ?y. ~P y
  29         proof
  30           take y;               // ?I
  31         qed by -;               //
  32         F by 3,-;               // ~E
  33       qed by -;                 // FE
  34     end;
  35   end`;;
  36