Changes from version 5.
1. Updated Globals.version_number to 6.
2. Changed resituate_hol90 to be cleaner. Changed install.doc to give more
details on the use of make_hol, especially the d option (when necessary,
etc).
3. Added GEN_INDUCTION to mk_arithmetic at the request of Elsa Gunter.
4. Made the functions in File print out the path of files that they find,
but can not read.
5. Changed the way that the system builds. I now do an install at the end
of the build. This cleans up all the screwedup paths that people
were getting added to the theory path as a result of calling find_library
in 3/sys_lib.sml when rebuilding the system while reusing theories and
libraries.
6. In a related fix, when one loads a library, it is done relative to its
path. In version 5, that was true only for code and help. Now it is true for
theories. (When we do a new_parent, it is now done with an absolute path
derived from the path field of the library.) After the first parent is
found, new_parent ensures that further ancestors are found by unique
theory id.)
7. Changed the parsing of type specifications. The syntax of the hol88 version
is more subtle than I thought; it allows the defined constructor to be
curried or not. My boneheaded version in hol90.5 wouldn't allow type
constructors that took paired arguments. Now that has been fixed, at the
cost of some special syntax. A curried constructor has "=>" between its
arguments, while an uncurried constructor has just a single argument,
which can have the form of any type. The "=>" is merely a delimiter that
makes parsing simple, plus I hope that it has an intuitive reading
if one confuses the "=>" with ">".
8. Took some cruft out of hol_lex.
9. As part of the changes done in 7, the "arg_atom" type defined in
Parse_support has been changed to be "arg". As a result, the arguments to
dtype have changed:
 dtype;
val it = fn
: {clauses:{constructor:string, args:Parse_support.arg list,
fixity:fixity} list,
save_name:string, ty_name:string}
> thm
As a result of the change to the concrete syntax of type specifications,
I changed the "define_type" invocations in the string library (mk_ascii and
mk_string) and in the "examples" directory of the "ind_def" library.
10. Moved "sed_hol_yak" and its bretheren to the tools directory. Added a
comment (some code) to the end of parse_support.sml that shows how to
make an MLYacc produce files that when compiled will give an hol parser
(types,terms,and type specs).
11. Changed SPEC to TY_SPEC in the datatype Parse_support.parse. When
Parse_support was "open"ed, the rule of inference "SPEC" would no longer
be accessible, thus other libraries and code that used "SPEC" wouldn't
load. This is an instance of a general problem. This ought to partially
go away when library code is loadable in binary format.
12. Changed hol_lex and hol_yak to depend solely on publically available
functions.
13. Fixed a prettyprinting bug in hol_pp. The bug is manifested in the
following example from David Shephard:
`let a=1 and b=2 in a+b`;
val it = (`let a = 1 and b = 2 in (b + a)`) : term
14. Added a function "const_decl" to Theory:
val const_decl : string > {const:Thm.Term.term,
theory : string,
place: Term.fixity}
It gives the information given when the constant was put in the symbol
table.
15. Fixed a bug in the prettyprinting of HOL theories, which was pointed out
by Ralph Reetz.
16. Jim Grundy's library of pairs has been ported to hol90 by David Shepherd.
17. Added a new theory "restr_binder", with definitions for
"RES_ABSTRACT", "RES_FORALL", "RES_EXISTS" and "RES_SELECT".
"restr_binder" has "bool" as its (only) parent, and is a parent of
"HOL". Added restricted quantification to the parser and prettyprinter.
As in hol88, users can define their own restricted binders. The interface
to this is in Dsyntax:
val binder_restrictions :unit > (string * string) list
val associate_restriction :(string*string) > unit
val delete_restriction :string > unit
There is also a new addition to allow users to control the style of
prettyprinting. Globals.pp_flags will eventually encapsulate all the
flags used to control the prettyprinter. Currently, the only field in
Globals.pp_flags is for restrictions:
val pp_flags : {restrict:bool ref}
I also took this opportunity to rewrite and document some of the
prettyprinting code.
18. Documentation has been added to help/90 for the restricted binder functions
"associate_restriction", "binder_restrictions", and "delete_restriction".
19. Added documentation for "union"  its specification is slightly different
than that of hol88.
20. Added the combinators, "W","CB","KI","oo", "Co", and the functions
"funpow", "butlast", and "replicate" to the Compat structure found in the
hol88 library.
21. Fixed the definition of "Lib.front_n_back" so that it handles singleton
lists. Now Compat.last and Compat.butlast are just the second and first
projections of the result of "front_n_back"
22. The "real" library has been ported to hol90 by its author John Harrison.
23. The "wellorder" library has been ported to hol90 by its author John
Harrison.
24. Added "CHANGED_TAC" to Tacticals.
25. Added "tryfind" to Lib.
26. Fixed an installation bug in the "HOL_lib" description (in 3/sys_lib.sml).
When building the system in the "reusingtheories" mode,
"find_library" is used to get the library description from disk. We
then have to do a "move_library" so that the internal description
has the correct path. I wasn't doing that in the case of "HOL_lib",
although I was doing it for "PRIM_HOL" and "BASIC_HOL". Beats me why
I wasn't consistent. This caused installation problems for Paul Curzon
and Ching Tsun.
27. Fixed a bug in the pairs library, reported by Ching Tsun. Both
CURRY_FORALL_CONV and CURRY_EXISTS_CONV needed a list_mk_pforall,
instead of a list_mk_forall.
28. Added a new entry to Globals. It identifies the keywords in the HOL
language, i.e., those "apparently OK identifiers" that are not able to
be used as variable or constant names. This is experimental; in particular
it is not clear how this interacts with Globals.tilde_symbols.
val reserved_identifiers = {symbolic = ["\\", ";", "=>", "", ":" ],
alphanumeric = ["let", "in", "and", "of"]}
29. Added CCONTR_TAC, from an old infohol message from Paul Loewenstein.
30. Made a slight change in Conv.SUB_QCONV. It might make things faster:
else if (is_abs tm)
then let val {Bvar,Body} = dest_abs tm
val bodyth = conv Body
in MK_ABS (GEN Bvar bodyth)
end
else ALL_QCONV tm;
is now
else if (is_abs tm)
then let val {Bvar,Body} = dest_abs tm
in ABS Bvar (conv Body)
end
else ALL_QCONV tm;
The reasoning is that "MK_ABS o GEN Bvar" is equivalent to "ABS Bvar".
31. Fixed a minor bug in SUBST: the "var" part of a replacement record
was not being checked to make sure that it was actually a var.
32. Changed line 194 of contrib/mutrec/mut_rec_ty.sml from
arg = map change_arg arg_info,
to
args = map change_arg arg_info,
33. Made changes to SUB_QCONV that affect rewriting. These required
various changes to proofs in the reals library and Paul Loewenstein's
automata library. I should probably include an upwardcompatibility
modification.
34. Fix to the abs_theory package.
The fix is to the function "new_abstract_entity". Replace the lines
val type_string = (type_to_string o type_of o list_mk_pair) ops
val rep_type_string = (name ^ " = " ^ name ^ " of " ^ type_string)
val rep_type = define_type{name=name,
type_spec = [QUOTE rep_type_string],
fixities = [Prefix]}
with
val rep_type = dtype
{save_name = name,
ty_name = name,
clauses = [{constructor = name,
args = map (Parse_support.Hty o type_of) ops,
fixity = Prefix}]}
35. Added global variable to Globals:
val goal_line = ref "____________________________";
36. Fixed a bug in the goalstack: backing up past the initial goal is not
allowed. Rewrote the goalstack implementation: it is now much cleaner.
37. Added a new structure "PP", that represents System.PrettyPrint in SML/NJ.
A few extra prettyprinting routines are thrown in too. In time, this
might grow into a useful library of prettyprinting routines.
38. Fixed a bug, reported by Paul Curzon, in the prettyprinter.
Nonsymbolic binders would not put a space between themselves and
the bound variable. The output could not therefore be reparsed.
39. Fixed a bug, reported by Paul Curzon, in the code that installs an
axiom/theorem/definition in the current theory. It allowed an empty
name to be given, e.g., save_thm("",TRUTH). This case now raises an
exception. (It might be argued that hol90 should read the empty name
off the theory file; this is possible, and add_theory_to_sml and its
ilk will properly handle the attempt to bind in ML the empty string
to the theorem (by giving a warning message, not making the binding,
and continuing), but if a theorem is important enough to save on a
theory file, it is important enough to name.)
40. Fixed a bug in SELECT_CONV. It wasn't using aconv to check equality
of terms. Bug reported by Chris Toshok.
41. Chris Toshok at UIdaho sent me the hol90 conversion of Mike Gordon's
fixpoint library.
42. Fixed a bug in the prettyprinter, noticed by Brian Graham:
c (\(x,y).M) N
would print out as
c \(x,y).M N
and so wouldn't be reparsable.
43. Added a feature to the pretty printer: infixes can now be stipulated to
print at the beginning or end of a line: after
#infix_at_front pp_flags := true
then A B C ... D can pretty print as
A
B
C
.
.
.
D
Otherwise, we get the usual, default, behaviour:
A
B
C
.
.
.
D
44. Changed the structure "Goal_stack" and the signature "Goal_stack_sig" to
"Goalstack" and "Goalstack_sig". Also, the Goalstack structure is not
open when the system starts up. This is to allow experimenting with a new
proof interface.
45. Added a new field to Globals.pp_flag : stack_infixes: bool ref. This
provides another control on how infixes get printed. The default is to
stack them, as shown above in 43. However, for long formulas, or formulas
with a large number of short identifiers being the "atoms" of the infix
expression, this can be unsightly. "stack_infixes" is initially true, and
we would observe one of the formats in 43. If "stack_infixes" is false,
we might see
A B C ... F
G ...
46. The treatment in 45 has been extended to application, the invisible infix.
47. Fixed a bug in "subst", noticed by Klaus Schneider. The simplest example
demonstrating the bug is
val tm = `\(p:'a) (q:'a). f (x:'a) (y:'a) : 'a`;
val theta = [{redex = `x:'a`, residue = `q:'a`},
{redex = `y:'a`, residue = `p:'a`}];
subst theta tm;
The answer should be the term
\p' q'. f q p
but hol90.6 fails with a CLASH error. This bug is "conservative", in that
it can not be used to prove  F; it just raises an exception in a case
where it ought to rename and proceed.
48. Fixed a bug in Rec_type_support.prove_induction_thm, noticed by La
Bella Maurizio. Frustratingly, this bug had been fixed in hol88, but
not recorded on the Versions file. Anyway, at approximately line 310 of
src/2/rec_type_support.sml, there is a function "mk_fn" defined. This is
a local function to the function "prove_induction_thm". Replace the
definition of "mk_fn" with the following:
fun mk_fn P ty tm =
let val {lhs,rhs} = dest_eq(snd(strip_forall tm))
val c = rand lhs
val args = snd(strip_comb rhs)
val vars = filter is_var args
val n = length(filter (fn t => type_of t = ty) vars)
in if (n=0)
then list_mk_abs (vars, tr)
else let val bools = gen n
val term = mk_disj{disj1 = list_mk_conj bools,
disj2 = mk_comb{Rator = P, Rand = c}}
in list_mk_abs((bools@vars),term)
end
end
49. Theorems with assumptions are now allowed to be stored and retrieved
from theory files. Also, the variable: "allow_theorems_with_assumptions"
in declared in Globals is now initialized to true.
50. Fixed a bug in CONTR noticed by David Shephard;
 CONTR(`1`)(ASSUME(`F`));
val it = .  1 : thm
51. Changed several small SML parsing bugs (due to SML/NJ or Poplog SML,
I'm not sure which). Thanks to Robin Popplestone for pointing them out.
52. Fixed a bug in the prettyprinter, reported by Brian Graham.
 %`!x y. !a::($> x). !b::($> y). (x > y) ==> (a > b)`;
val it = (`!x y. !a b ::($> x). x > y ==> a > b`) : term
Showing the dB structure and the restricted quantifiers, this is
 %`!x y. !a::($> x). !b::($> y). (x > y) ==> (a > b)`;
val it =
`!x y. RES_FORALL ($> (1))
(\a. RES_FORALL ($> (1)) (\b. (3) > (2) ==> (1) > (0)))`
Notice that the "x" in "($> x)" is one away from its binder, as is the
"y" in "($> y)". Hence, just testing with aconv, as I was, is not correct.
Changes to hol_pp.sml
53. Augmented Globals.pp_flags. Now it has the fields
val pp_flags : {infix_at_front:bool ref,
show_dB: bool ref,
show_restrict:bool ref,
show_types: bool ref,
stack_infixes :bool ref}
and also provides the variables
val show_restrict : bool ref
val show_types : bool ref
val show_dB : bool ref
Only show_restrict is new.
54. Change to Globals.output_HOL_ERR. I didn't understand the check for
origin_structure = "" in the following, so I am getting rid of it.
OLD:
val output_HOL_ERR =
ref (fn {message,origin_function,origin_structure} =>
(output(std_out,("\nException raised at "^origin_structure^"."^
origin_function^
(if (origin_structure="") then "" else ":\n")^
message^"\n"));
flush_out std_out));
NEW:
val output_HOL_ERR =
ref (fn {message,origin_function,origin_structure} =>
(output(std_out,("\nException raised at "^origin_structure^"."^
origin_function^":\n"^message^"\n"));
flush_out std_out));
55. Richard Boulton has modified the prettyprinter so that it is extensible.
The structure Extend_hol_pp in hol90 contains functions for incrementally
extending the system prettyprinters for HOL types and terms, and for
resetting them to their original state. The signature of this structure is:
sig
datatype gravity = TOP  APPL  INFIX of int  WEAK  BOTTOM
val gravity_geq : gravity > gravity > bool
val extend_pp_type :
(({depth:int, gravity:gravity} >
Term.Type.hol_type > PP.ppstream > unit) >
({depth:int, gravity:gravity} >
Term.Type.hol_type > PP.ppstream > unit)) > unit
val reset_pp_type : unit > unit
val extend_pp_term :
(({boundvars:Term.term list, depth:int, gravity:gravity} >
Term.term > PP.ppstream > unit) >
({boundvars:Term.term list, depth:int, gravity:gravity} >
Term.term > PP.ppstream > unit)) > unit
val reset_pp_term : unit > unit
end
Considering terms (and by analogy, types), there are two functions: one to
extend the printer; the other to reset it to the startup state. Users can
provide a prettyprinting function for whatever special features they
require. Such a function will be tried first on each call (toplevel and
recursive) to the prettyprinter. If it fails for any reason, the original
printer is called (or the previously extended version of it).
The usersupplied function takes a print function as its first argument.
When the user function is installed in the system using extend_pp_term,
this argument is instantiated with the currently active printer for terms.
Thus, if the user function makes calls to this argument in order to
process subterms, the new printing will be tried at each level without
cutting the old printer out of the loop.
The depth argument to the print functions is the print depth; it
should be decremented on each recursive call. When it reaches zero,
the subterm is elided. Starting with a negative value prevents elision
from occurring regardless of how deep the term is. The boundvars
argument is a list of the bound variables of the abstractions passed
through in descending the term. The list is accessed by the de Bruijn
number when a bound variable is encountered.
The datatype for precedence (called gravity) is available to the
user. There are five constructors. TOP is the highest (mosttightly
binding) precedence; APPL is for applications, INFIX is for the infix
operators and takes an integer argument; WEAK is used for bindings and
for mixfixes such as conditional expressions; and BOTTOM is the lowest
precedence value.
Example:
The use of the extensibility functions is illustrated in the session
below in which a function to print conditional expressions as "if
... then ... else ..." instead of as "... => ...  ..." is
installed. Note that the call to dest_cond fails if the term is not a
conditional expression and so forces the original printer to be used.
 val tm = (`APPEND ((n = 0) => []  [n]) [1;2;3]`);
val tm = (`APPEND ((n = 0) => []  [n]) [1; 2; 3]`) : term
 local
= open PP Extend_HOL_PP
= in
= fun pp_ite pp_tm {boundvars:term list,depth,gravity} tm ppstrm =
= if (depth = 0)
= then raise Fail "pp_ite"
= else let val {cond,larm,rarm} = dest_cond tm
= val parenth = gravity_geq gravity WEAK
= val params = {boundvars=boundvars,depth=depth1,gravity=TOP}
= in (if parenth then add_string ppstrm "(" else ();
= begin_block ppstrm CONSISTENT 0;
= add_string ppstrm "if ";
= (pp_tm params cond ppstrm : unit);
= add_break ppstrm (1,0);
= add_string ppstrm "then ";
= pp_tm params larm ppstrm;
= add_break ppstrm (1,0);
= add_string ppstrm "else ";
= pp_tm params rarm ppstrm;
= end_block ppstrm;
= if parenth then add_string ppstrm ")" else ())
= end
= end;
val pp_ite = fn
: ({boundvars:term list, depth:int, gravity:Extend_HOL_PP.gravity}
> term > PP.ppstream > unit)
> {boundvars:term list, depth:int, gravity:Extend_HOL_PP.gravity}
> term > PP.ppstream > unit
 tm;
val it = (`APPEND ((n = 0) => []  [n]) [1; 2; 3]`) : term
 Extend_HOL_PP.extend_pp_term pp_ite;
val it = () : unit
 tm;
val it = (`APPEND (if (n = 0) then [] else [n]) [1; 2; 3]`) : term
 Extend_HOL_PP.reset_pp_term ();
val it = () : unit
 tm;
val it = (`APPEND ((n = 0) => []  [n]) [1; 2; 3]`) : term

56. Momentarily took the new prettyprinter stuff out until I can understand
it better. Then put it back.
57. Fixed a bug, reported by Brian Graham, in the way "tilde_symbols" are
lexed. Example:
 Globals.tilde_symbols := ["~<"];
val it = () : unit
 new_theory"foo";
...
 val bug = new_infix_definition
("bug", `~< a b = ~(a < b)`, 200);
= val bug =  !a b. a ~< b = ~(a < b) : thm
 `~<`; (* OK, as before *)
val it = (`$~<`) : term
 `$~<`; (* OK, not as before *)
val it = (`$~<`) : term
 `2:num ~< 3`; (* This also used to fail *)
val it = (`2 ~< 3`) : term
58. Change to the definition of "EXISTS", so as to avoid variable
capture from dest_abs.
(* Old
* fun EXISTS (w,t) th =
* let val {Bvar,Body} = dest_exists w
* in
* if (aconv (subst [{redex = Bvar, residue = t}] Body)
* (concl th))
* then mk_thm(hyp th, w)
* else raise DRULE_ERR{function = "EXISTS",message = ""}
* end
* handle _ => raise DRULE_ERR{function = "EXISTS",message = ""};
*******************************************************************)
fun EXISTS (w,t) th =
let val {Rator,Rand} = dest_comb w
in
if (#Name(dest_const Rator) = "?")
then if (aconv (Term.beta_conv(mk_comb{Rator=Rand, Rand=t})) (concl th))
then mk_thm(hyp th, w)
else raise DRULE_ERR{function = "EXISTS",
message = "incompatible structure"}
else raise DRULE_ERR{function = "EXISTS",message = "not an existential"}
end;
59. Changed definition of REWR_CONV to localize (and rationalize!) the
exception handling. Did the same for RAND_CONV, RATOR_CONV, ABS_CONV, and
ORELSEQC. The general aim should be to replace instances of
handle _ => ...
with
handle (HOL_ERR _) =>
so that an occurrence of a nonHOL exception can propagate to where it
should.
60. Added funpow to the basic system.
fun funpow n f x =
let fun it (0,res) = res
 it (n,res) = it (n1, f res)
in it(n,x)
end;
61. Added Psyntax and Rsyntax to the system (in 3/{psyntax.sig,rsyntax.sig,
psyntax.sml,rsyntax.sml}). This should clean up hol88 a bit.
62. Added a new implementation of Goalstack to the system. This is still
cleaner than the previous clean version, since it uses the "history"
abstype, and the interface now provides reasonable access to a list of
proofs.
63. Changed ALPHA_CONV to be more efficient:
New.
fun ALPHA_CONV x t =
ALPHA t (mk_abs{Bvar = x,
Body = Term.beta_conv(mk_comb{Rator = t,Rand = x})})
Old.
fun ALPHA_CONV x t =
let val x' = variant (free_vars t) x
val cmb = mk_comb{Rator = t, Rand = x'}
val th1 = SYM(ETA_CONV(mk_abs{Bvar = x', Body = cmb}))
and th2 = ABS x' (BETA_CONV cmb)
in
TRANS th1 th2
end
handle _ => raise DRULE_ERR{function = "ALPHA_CONV",message = ""};
64. Fixed bug spotted by Richard Boulton in "is_infix": it shouldn't
fail when applied to a string that is not the name of a constant.
66. Added the MATCH_MP by John Harrison. It is much more robust than
the previous version.
67. Made a slight change to EXISTS_TAC, so that it takes advantage of
betaconversion (safer than using dest_exists followed by a subst
of the term for the bvar).
68. Made a slight change to the semantics of the "loaded_func" of the
library package. It now gets compiled after the library is loaded,
rather than when the library is declared.
69. Made a new library: goalstack_lib. The goalstack is no longer an
integral part of the hol90 distribution. This is intended to pave
the way for other proof managers to be set up as libraries. And it
makes it easier to experiment with the current goalstack
implementation.
70. Fixed a bug in substitution, reported by Elsa Gunter. Falsity was
not derivable; it's just that a replacement would not happen because
a certain renaming would not happen.
71. Changed the implementation of rewriting to use an abstract type of
`rewrites'. A value of type `rewrites' is a "compiled" set of rewrite
rules (what used to be a "conv net ref" before (ugh!)). Many rewriting
operations (the ones that don't start with "PURE_", for instance)
automatically use a base set of useful simplifications. Before the
introduction of the type of `rewrites', the interface to this base
set was poor. Now people can install their own base set of rewrites,
augment the existing set, or get the current value of the base rewrites.
The functions "empty_rewrites" and "add_rewrites", provide a simple
means for interested users to build their own rewrite rule sets.
A simple prettyprinter ("pp_rewrites") has been installed in the
system prettyprinter tables to enable the viewing of rewrite rule
sets.
type rewrites
val empty_rewrites : rewrites
val add_rewrites : rewrites > Base_logic.Thm.thm list > rewrites
val set_base_rewrites : rewrites > unit
val base_rewrites : unit > rewrites
val add_base_rewrites : Base_logic.Thm.thm list > unit
val pp_rewrites : PP.ppstream > rewrites > unit
Preexisting functions whose type has changed are:
val REWRITES_CONV :rewrites > conv
val GEN_REWRITE_CONV :(conv > conv)
> rewrites > Base_logic.Thm.thm list > conv
val GEN_REWRITE_RULE :(conv > conv)
> rewrites > Base_logic.Thm.thm list
> Base_logic.Thm.thm > Base_logic.Thm.thm
val GEN_REWRITE_TAC :(conv > conv)
> rewrites > Base_logic.Thm.thm list > tactic
Examples of prettyprinter.
 base_rewrites();
val it =
 (x = x) = T;  (T = t) = t;  (t = T) = t;  (F = t) = ~t;
 (t = F) = ~t;  ~~t = t;  ~T = F;  ~F = T;  T /\ t = t;
 t /\ T = t;  F /\ t = F;  t /\ F = F;  t /\ t = t;
 T \/ t = T;  t \/ T = T;  F \/ t = t;  t \/ F = t;
 t \/ t = t;  T ==> t = t;  t ==> T = T;  F ==> t = T;
 t ==> t = T;  t ==> F = ~t;  (T => t1  t2) = t1;
 (F => t1  t2) = t2;  (!x. t) = t;  (?x. t) = t;
 (\x. t1) t2 = t1;  (FST x,SND x) = x;  FST (x,y) = x;
 SND (x,y) = y
Number of rewrite rules = 31
: rewrites
 empty_rewrites;
val it =
Number of rewrite rules = 0
: rewrites
72. Modified the abs_theory library to depend on the goalstack
library. Also modified the description of the goalstack library so
that it depends on "basic_hol_lib", rather than "hol_lib". Edited
various files in the abs_theory library sources so that they reflect the
fact that abs_theory is a library (for example, examples/abs_theory.tex
was out of date).
73. The hol88 library has been reduced, since now Psyntax and Rsyntax are
part of the core. Various libraries, such as the reals and wellordering
have been modified in minor ways to build under this new regime. For users,
a simple invocation of (one of)
open Psyntax; (* gives paired syntax *)
open Rsyntax; (* gives record syntax *)
is all that is necessary to put one in a "paired" environment or a
"record" environment.
74. The libraries "fixpoint" and "prog_logic" both declare the constant
"ITER" in their theories. Therefore a person wishing to use both
libraries simultaneously would not be able to. I have changed the name
"ITER" in the fixpoint library to be "FUNPOW". Likewise, I have changed
"LUB" in the fixpoint library to "SUP".
75. Added a new directory, called "examples", at the top level of the hol90
directory hierarchy. This is for quick access to the various
examples that are available throughout the system. Currently, there are
entries for the following libraries:
abs_theory
inductive_def
unity
bmark
Also, there is John Harrison's proof of the n=4 case of Fermat's
Last Theorem.
76. Removed Parse.p and Parse.ps; added Parse.preterm_parser and
Parse.string_to_preterm.
77. Added better "theoremcounting" functionality. The interface is as
before, except that "thm_count" is much more accurate. Up until now,
"mk_thm" covered a mixture of undifferentiated sins and necessities. Now,
accurate counts are kept for each primitive rule; for the derived rules
(as a whole); for when definitions and axioms are built; when a theorem
is loaded in from disk; when mk_thm is called in checking for validity
of tactics; and finally for anytime the user just makes a theorem.
val reset_thm_count : unit > unit
(* Toggles switch that says whether to count inferences or not. *)
val counting_thms : bool > unit
val thm_count : unit > {ASSUME : int, REFL : int, BETA_CONV : int,
SUBST : int, ABS : int, DISCH : int,
MP : int, INST_TYPE : int, drule : int,
definition : int, axiom : int,
from_disk : int, valid_tac : int, other : int}
Thm_sig now supplies corresponding calls to invoke these different
varieties of mk_thm. The system has not become more unsafe, just
more accurate. However, it would be nice to remove some of these
entrypoints.
val mk_axiom_thm : (Term.term list * Term.term) > thm
val mk_definition_thm : (Term.term list * Term.term) > thm
val mk_drule_thm : (Term.term list * Term.term) > thm
val mk_disk_thm : (Term.term list * Term.term) > thm
val mk_tac_thm : (Term.term list * Term.term) > thm
val mk_thm : (Term.term list * Term.term) > thm
How should one compute inference totals? Here's one example:
let val {ABS,ASSUME,BETA_CONV,DISCH,INST_TYPE,MP,
REFL,SUBST,drule,other,...} = thm_count()
in
Lib.say("Total inferences = "
^Lib.int_to_string(ABS + ASSUME + BETA_CONV + DISCH +
INST_TYPE + MP + REFL + SUBST + drule + other))
end;
This computes all primitive and "extendedprimitive" inferences, plus
miscellaneous others (such as arise when axiom schemes like "num_CONV"
are applied). Invoking "counting_thms true" slows the implementation
down about 5%.
78. Added some infix notation for elements of a substitution:
A > B = {redex = A, residue = B}
This makes writing "substitutionheavy" code a bit pleasanter. Changes to
src/0/lib.{sig,sml}. ">" is polymorphic and so it works for both type
and term substitutions.
79. Fixed a bug in prettyprinting, reported by Einar Snekkenes. The problem
manifested itself as
`let a = 1 and (b,c) = (2,3) in (a,b,c)`;
val it = (`let a = 1 and b,c = (2,3) in (b,c,a)`) : term
Environments weren't being put together properly.
80. Added the "list" library of Wai Wong and Paul Curzon. This provides
a theory "List", in which the major definitions of the theory "list"
have been loaded and bound as theorems. Users of the type "list"
should therefore be able to load this theory and use the associated
reasoning facilities without stooping to the original theory of lists.
The auxiliary theory "fun" has been renamed "operator" and made local
to this library. Note: the library takes a lot of time and space to load,
even on a 64 Meg. SPARC2.
81. Removed the functions found in "src/3/list_conv.{sig,sml}" from the
system, as they are replicated in the "list" library. This
require minor changes to the libraries "unity" (which used
LIST_INDUCT_TAC) and "prog_logic" (which used
"new_list_rec_definition", a derived form of "new_recursive_definition").
82. Moved the "fixpoint" library to contrib, as it is very small and has
no documentation.
83. Added the "CSP" library of Albert Camillieri to "contrib". This library
was translated to hol90 by Brian Graham.
84. Changed the semantics of "load_library" so that the "theory" argument, if
not the name of the current theory, will be used to make a new theory,
i.e., to put the system into draft mode. Before, if all the theories
needed to build the library were already in the ancestry, the new theory
would not get declared. Now the new theory gets declared, regardless.
In other words, only when the "theory" argument equals the current theory
will new_theory not get called. One consequence of this is that
"load_library_in_place" is now a derived form:
fun load_library_in_place lib = load_library{lib = lib, theory = ""}
85. Arbitrarily replaced the name "load" from src/0/lib.{sig,sml} with the
name "interpret". I think it is more intuitive this way. I also
fixed up the exception handling in Lib.compile and Lib.interpret: if
they raise an error during loading, the original setting of the
"System.Control.interp" flag is restored.
86. Added a function "prim_load_library" to src/0/library/lib.{sig,sml}
of type
(string > unit) > {lib:lib, theory:string} > unit
The first string is a "code_loader" function  it is invoked on each file
in the "code" section of a library. Two possible ways to use
this are to: compile code or intepret code. The first option is already
provided in the functionality of the derived form "load_library", i.e.,
val load_library = prim_load_library Lib.compile
Another specialization of "prim_load_library" would load the code quickly,
but execution of that code would be slow. It would be appropriate for
small memory machines and it would be defined:
val fast_load_library = prim_load_library Lib.interpret
This has not, however, been installed in the system.
87. In hopefully the last chapter of the goalstack hegira, the goalstack
library has been moved back into the core of the system. It is now
in the structure Goalstack, which is already open when the system
starts up.
88. Added a new type "lambda" to term.sml. The declaration is
datatype lambda = VAR of {Name : string, Ty : Type.hol_type}
 CONST of {Name : string, Ty : Type.hol_type}
 COMB of {Rator : term, Rand : term}
 LAMB of {Bvar : term, Body : term};
Also added a new function "dest_term" of type "term > lambda". This
is for taking apart an arbitrary term in one step. These additions are
the suggestion of Morten Welinder; analogous proposals have been made
in the past by Elsa Gunter. This type is currently for experimental
purposes only and could be withdrawn at any moment since it provides
already existing functionality. Some changes using this type have
already been applied to rewriting (it didn't apparently help much).
89. Some internal changes have been made: the Symtab structure has been
removed; its functionality has been dispersed to Type and Term. One
consequence of this is that "mk_type" is now found in Type, instead
of Dsyntax.
90. Added the "window" library of Jim Grundy.
91. Added the libraries "res_quan", and "word", thanks to Wai Wong and
Paul Curzon.
92. As a result of (89), "variant" now has the right behaviour when the
argument variable has a name equal to that of a constant, i.e., it
returns a variable with a name different than that of any (term)
constant in the signature at the time of call.
93. Added a function "Theory.html_theory : string > unit", which takes
a string (s), looks up the theory with name "s" (it must be in
the ancestry), and prints the theory out in HTML format to file
"s.html". The parent theories are linked to, but not themselves printed
out, i.e., the function does not call itself recursively. "html_theory"
is a simple modification of "print_theory". It is easy to extend this
function to operate over parts of the ancestry. For example, to get
a hypertext version of the entire current theory graph, one might
do something like
map html_theory (current_theory()::ancestry"");
if one had a lot of memory available. A simple utility that one
could write using "html_theory" would be
fun html_ancestry{theory, until} =
let val A = theory::ancestry theory
val stoppers = Lib.U (map ancestry until)
val remains = Lib.set_diff A stoppers
in
map Theory.html_theory remains
end;
94. Fixed a bug in "new_parent". Suppose we have made a theory "A" with
parent "B" in a session. In a different session, we do a
new_theory "B";
new_parent "A";
This should not be allowed; otherwise various theory operations would
become ambiguous (which B is being referred to, for instance). This bug
is a problem in hol90 because we are using unique identifiers for
security: two theories with different unique ids could have the same name,
but that should not be allowed, if both are in the same theory graph.
95. Added the library "orsml" of Leonid Libkin and Elsa Gunter to contrib.
This library applies a sophisticated database query language to the
problem of searching for various HOL objects, e.g., all the rewrites
possible throughout a given term, all theorems involving a
certain term, etc.
96. Added the libraries "mutrec" and "nested_rec" to contrib. These
libraries were authored by Elsa Gunter, Healfdene Goguen, and Myra
VanInwegen. They provide functionality to define logical datatypes
with mutual recursion and nested recursion.
97. Added a bugfix (from Tom Melham) to num_EQ_CONV, in num_lib. Now the
following works, whereas it didn't earlier:
 num_EQ_CONV (`3 = SUC(SUC(SUC 1))`);
val it =  (3 = SUC (SUC (SUC 1))) = F : thm
98. Another name clash, this time in the contrib directory. Again, it involves
the theory of fixpoints. The clash is the constant "MONO", which is also
used in CSP. Solution: the "MONO" in "fixpoint" has now been renamed to
"MONOTONE". Other clashes and their resolutions (CSP is unaltered  all
changes were made in "fixpoint"):
CONTINUOUS > CONTINUOUSF
CHAIN > CHAINF
<< > <<<.
99. Simplified the installation procedure. Now hol90 includes the hol88 help
files. As a result, the hol88 help files don't have to be separately
fetched from elsewhere. I hope that, over time, the hol88 help files
will be replaced by their hol90 translations.
100. Added a link from the hol90 manual to Kathi Finsler's Beginner's
Guide for hol90.
101. Removed Globals.backup_limit. This is a variable that controls how
many "past states" of the goalstack are kept. Setting the limit is
now done by
set_backup: int > unit
The initial limit is 15. Note that setting the limit smaller than the
current limit will immediately truncate the past states to the new
limit.
102. Added "type_decl : string > {tyc:hol_type, arity :int, theory:string}"
to Type, at the request of Ralph Reetz.
103. Improved the basic Lexis functions and Lib.int_to_string and
Lib.string_to_int so that they are more efficient. For example, they
don't use "explode" anymore. The implementation follows that of "charset"
in the SML/NJ library, due to John Reppy.
104. Installed the library "part_fun" in contrib. This presents support for
partial functions and is due to Elsa Gunter.
105. Installed the library "holML" in contrib. This is an extensive
development of the dynamic semantics of Standard ML. It is due to
Elsa Gunter, Myra VanInwegen, and Savi Maharaj. The Core and Module
systems are covered, along with extensions to a higherorder module
system. Building this library requires *serious* resources  it
prostrated a 64 M. Sparc10!
106. Added a contrib directory "map", which contains a rudimentary HTML
map of the theories of the hol90 distribution. The "top" point of the
map can be accessed via the file "MAP.html"
106. Changed the theories in the "real" library to use nicerlooking
(symbolic) infixes. The changes are as follows:
Before After
 
real_add +
real_mul *
real_lt <
real_gt >
real_le <=
real_ge >=