Unity/mk_gen_induct.ml

   1 (* -*- Emacs Mode: sml -*- *)
   2
   3 (*---------------------------------------------------------------------------*)
   4 (*
   5    File:         mk_gen_induct.sml
   6
   7    Description:  This file proves the theorem of general induction on natural
   8                  numbers by using the theorem of primitive recursion.
   9
  10    Author:       (c) Copyright 1990-2008 by Flemming Andersen
  11                  Modified by John Harrison to just pick up num_WF instead
  12    Date:         June 7. 1990
  13    Last Update:  January 18, 2008
  14 *)
  15 (*---------------------------------------------------------------------------*)
  16
  17 (*
  18         !P. (!(m:num). (!n. n < m ==> (P n)) ==> (P m)) ==> (!m. P m)
  19 *)
  20 let GEN_INDUCT_thm = prove_thm
  21   ("GEN_INDUCT_thm",
  22    (`!P. (!(m:num). (!n. n < m ==> (P n)) ==> (P m)) ==> (!m. P m)`),
  23     MATCH_ACCEPT_TAC num_WF);;
  24
  25 (* Emacs editor information
  26 |  Local variables:
  27 |  mode:sml
  28 |  sml-prog-name:"hol90"
  29 |  End:
  30 *)