This file contains a theory I defined while learning the system.  It
contains some sample definitions and stored proofs.  My goal in this
theory was to define the factorial function in both tail-recursive
(RFACT) and non-tail-recursive (IFACT) forms, and prove that the two
computed the same function under initialization conditions.
<P>

Of course, there are probably better ways to do the proofs and
definitions in this file.  Keep in mind that they were done by someone
with only a week's experience with the system.  I've provided the file
because I personally could have benefitted from a small example to
study when I started. <P>

<PRE>
new_theory "facts"; 

new_parent "arithmetic"; 

val num_Axiom = theorem "prim_rec" "num_Axiom";                     

add_theory_to_sml "arithmetic" ;

val RFACT = new_recursive_definition
   {name = "RFACT",
    fixity = Prefix,
    rec_axiom = num_Axiom, 
    def = --`($RFACT 0 = 1) /\
             ($RFACT (SUC n) = (SUC n) * ($RFACT n))`--};

val IFACT = new_recursive_definition
   {name = "IFACT",
    fixity = Prefix,
    rec_axiom = num_Axiom,
    def = --`($IFACT 0 a = a) /\
             ($IFACT (SUC n) a = ($IFACT n (a * (SUC n))))`--};

close_theory(); 

val IFACT_lemma = store_thm ("IFACT_lemma",
   --`!n . !a . IFACT n a = a * IFACT n 1`--,
   INDUCT_TAC
     THEN GEN_TAC
     THEN REWRITE_TAC[IFACT, MULT_RIGHT_1] 
     THEN REWRITE_TAC[MULT_LEFT_1]
     THEN ONCE_ASM_REWRITE_TAC[] 
     THEN REWRITE_TAC[MULT_ASSOC]);

val RFACT_IFACT = store_thm ("RFACT_IFACT",
   --`! n . RFACT n = IFACT n 1`--,
   INDUCT_TAC
     THEN REWRITE_TAC[RFACT, IFACT]
     THEN REWRITE_TAC[MULT_LEFT_1]
     THEN ASSUME_TAC IFACT_lemma
     THEN ONCE_ASM_REWRITE_TAC[]
     THEN REWRITE_TAC[]);

export_theory(); 
</PRE>