miz3/Samples/samples.ml

   1 horizon := 1;;
   2
   3 thm `;
   4   !R. (!x. R x x) /\ (!x y z. R x y /\ R y z ==> R x z)
   5        ==> ((!m n. m <= n ==> R m n) <=> (!n. R n (SUC n)))
   6   proof
   7    let R be num->num->bool;
   8    assume !x. R x x [1];
   9    assume !x y z. R x y /\ R y z ==> R x z [2];
  10    !n. n <= SUC n by ARITH_TAC;
  11    (!m n. m <= n ==> R m n) ==> (!n. R n (SUC n)) [3] by SIMP_TAC;
  12    now
  13     assume !n. R n (SUC n) [4];
  14     !m n d. n = m + d ==> R m (m + d)
  15     proof
  16      let m be num;
  17      R m m by MESON_TAC,1;
  18      R m (m + 0) [5] by REWRITE_TAC,ADD_CLAUSES;
  19      !d. R m (m + d) ==> R m (m + SUC d)
  20      proof
  21       let d be num;
  22       assume R m (m + d);
  23       R m (SUC (m + d)) by MESON_TAC,2,4;
  24      qed by REWRITE_TAC,ADD_CLAUSES;
  25      !d. R m (m + d) by INDUCT_TAC,5;
  26      !d n. n = m + d ==> R m (m + d)
  27       by REWRITE_TAC,LEFT_FORALL_IMP_THM,EXISTS_REFL,ADD_CLAUSES;
  28     qed by ONCE_REWRITE_TAC,SWAP_FORALL_THM;
  29     thus !m n. m <= n ==> R m n by SIMP_TAC,LE_EXISTS,LEFT_IMP_EXISTS_THM;
  30    end;
  31   qed by EQ_TAC,3`;;
  32
  33 thm `;
  34   !s. INFINITE s ==> ?x:A. x IN s
  35   proof
  36     let s be A->bool;
  37     assume INFINITE s;
  38     ~(s = {}) by INFINITE_NONEMPTY;
  39     consider x such that
  40       ~(x IN s <=> x IN {}) [1] by EXTENSION;
  41     take x;
  42     ~(x IN {}) by NOT_IN_EMPTY;
  43   qed by 1`;;
  44
  45 let NOT_EVEN = thm `;
  46   !n. ~EVEN n <=> ODD n
  47   proof
  48     ~EVEN 0 <=> ODD 0 [1] by EVEN,ODD;
  49     !n. (~EVEN n <=> ODD n) ==> (~EVEN (SUC n) <=> ODD (SUC n))
  50       by EVEN,ODD;
  51   qed by 1,INDUCT_TAC`;;
  52