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