/usr/share/hol88-2.02.19940316/Library/reduce/reduce.ml is in hol88-library-source 2.02.19940316-15.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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;;
|