1\DOC EVAL_RULE 2 3\TYPE {EVAL_RULE : thm -> thm} 4 5\SYNOPSIS 6Evaluate conclusion of a theorem. 7 8\KEYWORDS 9evaluation. 10 11\DESCRIBE 12 13An invocation {EVAL_RULE th} symbolically evaluates the 14conclusion of {th} by applying the defining equations of constants 15which occur in the conclusion of {th}. These equations are held in a 16mutable datastructure that is automatically added to by {Hol_datatype}, 17{Define}, and {tprove}. The underlying algorithm is call-by-value with a 18few differences, see the entry for {CBV_CONV} for details. 19 20\FAILURE 21Never fails, but may diverge. 22 23\EXAMPLE 24{ 25- val th = ASSUME(Term `x = MAP FACT (REVERSE [1;2;3;4;5;6;7;8;9;10])`); 26> val th = [.] |- x = MAP FACT (REVERSE [1; 2; 3; 4; 5; 6; 7; 8; 9; 10]) 27 28- EVAL_RULE th; 29> val it = [.] |- x = [3628800; 362880; 40320; 5040; 720; 120; 24; 6; 2; 1] 30 31- hyp it; 32> val it = [`x = MAP FACT (REVERSE [1; 2; 3; 4; 5; 6; 7; 8; 9; 10])`] 33} 34 35\COMMENTS 36In order for recursive functions over numbers to be applied by {EVAL_RULE}, 37pattern matching over {SUC} and {0} needs to be replaced by destructors. 38For example, the equations for {FACT} would have to be rephrased 39as {FACT n = if n = 0 then 1 else n * FACT (n-1)}. 40 41\SEEALSO 42bossLib.EVAL, bossLib.EVAL_TAC, computeLib.CBV_CONV. 43 44\ENDDOC 45