1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
%******************************************************************************
** LIBRARY: reduce (part III) **
** **
** DESCRIPTION: Reduction tools using all the conversions in the library **
** **
** AUTHOR: John Harrison **
** University of Cambridge Computer Laboratory **
** New Museums Site **
** Pembroke Street **
** Cambridge CB2 3QG **
** England. **
** **
** jrh@cl.cam.ac.uk **
** **
** DATE: 18th May 1991 **
** REVISED: 8th July 1991 **
******************************************************************************%
%-----------------------------%
% Extend the help search path %
%-----------------------------%
tty_write `Extending help search path`;
let path = library_pathname()^`/reduce/help/entries/` in
set_help_search_path (union [path] (help_search_path()));;
%------------------------------%
% Load the boolean conversions %
%------------------------------%
tty_write `\
Loading boolean conversions`;
load (library_pathname()^`/reduce/boolconv`,get_flag_value `print_lib`);;
%---------------------------------%
% Load the arithmetic conversions %
%---------------------------------%
tty_write `\
Loading arithmetic conversions`;
load (library_pathname()^`/reduce/arithconv`,get_flag_value `print_lib`);;
tty_write `\
Loading general conversions, rule and tactic`;;
%-----------------------------------------------------------------------%
% RED_CONV - Try all the conversions in the library %
%-----------------------------------------------------------------------%
let RED_CONV =
let FAIL_CONV (s:string) (tm:term) = (failwith s) :thm in
itlist $ORELSEC
[ADD_CONV; AND_CONV; BEQ_CONV; COND_CONV;
DIV_CONV; EXP_CONV; GE_CONV; GT_CONV;
IMP_CONV; LE_CONV; LT_CONV; MOD_CONV;
MUL_CONV; NEQ_CONV; NOT_CONV; OR_CONV;
PRE_CONV; SBC_CONV; SUC_CONV] (FAIL_CONV `RED_CONV`);;
%-----------------------------------------------------------------------%
% REDUCE_CONV - Perform above reductions at any depth. %
%-----------------------------------------------------------------------%
let REDUCE_CONV = DEPTH_CONV RED_CONV;;
%-----------------------------------------------------------------------%
% REDUCE_RULE and REDUCE_TAC - Inference rule and tactic versions. %
%-----------------------------------------------------------------------%
let REDUCE_RULE = CONV_RULE REDUCE_CONV;;
let REDUCE_TAC = CONV_TAC REDUCE_CONV;;
|
