miz3/Samples/sample.ml

   1 horizon := 1;;
   2
   3 thm `;
   4 let R be num->num->bool;
   5 assume !x. R x x [1];
   6 assume !x y z. R x y /\ R y z ==> R x z [2];
   7 thus (!m n. m <= n ==> R m n) <=> (!n. R n (SUC n))
   8 proof
   9  now [3] // back direction first
  10   assume !n. R n (SUC n);
  11   let m n be num;
  12   !d. R m (m + d) ==> R m (m + SUC d) [4] by 2,ADD_CLAUSES;
  13   R m (m + 0) by 1,ADD_CLAUSES;
  14   !d. R m (m + d) by 4,INDUCT_TAC;
  15   thus m <= n ==> R m n by LE_EXISTS;
  16  end;
  17  !n. n <= SUC n;
  18 qed by 3`;;
  19