1% Release notes for HOL4, ??????
2
3<!-- search and replace ?????? strings corresponding to release name -->
4<!-- indent code within bulleted lists to column 11 -->
5
6(Released: )
7
8We are pleased to announce the ?????? release of HOL 4.
9
10Contents
11--------
12
13-   [New features](#new-features)
14-   [Bugs fixed](#bugs-fixed)
15-   [New theories](#new-theories)
16-   [New tools](#new-tools)
17-   [New Examples](#new-examples)
18-   [Incompatibilities](#incompatibilities)
19
20New features:
21-------------
22
23*   The special `Type` syntax for making type abbreviations can now
24    map to `temp_type_abbrev` (or `temp_type_abbrev_pp`) by adding the
25    `local` attribute to the name of the abbreviation.
26
27    For example
28
29           Type foo[local] = ���:num -> bool # num���
30
31    or
32
33           Type foo[local,pp] = ���:num -> bool # num���
34
35    Thanks to Magnus Myreen for the feature suggestion.
36
37*   We have added a special syntactic form `Overload` to replace
38    various flavours of `overload_on` calls. The core syntax is
39    exemplified by
40
41           Overload foo = ���myterm���
42
43    Attributes can be added after the name. Possible attributes are
44    `local` (for overloads that won���t be exported) and `inferior` to
45    cause a call `inferior_overload_on` (which makes the overload the
46    pretty-printer���s last choice).
47
48    Thanks to Magnus Myreen for the feature suggestion.
49
50*   The `Holmake` tool will now build multiple targets across multiple
51    directories in parallel. Previously, directories were attacked one
52    at a time, and parallelisation only happened within those
53    directories. Now everything is done at once. The existing `-r`
54    option takes on a new meaning as part of this change: it now
55    causes `Holmake` to build all targets in all directories
56    accessible through `INCLUDES` directives. Without `-r`, `Holmake`
57    will build just those dependencies necessary for the current set
58    of targets (likely files/theories in the current directory).
59
60*   It is now possible to write `let`-expressions more smoothly inside
61    monadic `do`-`od` blocks. Rather than have to write something like
62
63           do
64             x <- M1;
65             let y = E
66             in
67               do
68                 z <- M2 x y;
69                 return (f z);
70               od
71           od
72
73    one can replace the `let`-bindings with uses of the `<<-` arrow:
74
75           do
76             x <- M1;
77             y <<- E;
78             z <- M2 x y;
79             return (f z)
80           od
81
82    (The `<<-` line above is semantically identical to writing
83    `y <- return E`, but is nonetheless syntactic sugar for a
84    `let`-expression.)
85
86    The pretty-printer reverses this transformation.
87
88    Thanks to Hrutvik Kanabar for the implementation of this feature.
89
90Bugs fixed:
91-----------
92
93*   In `extrealTheory`: the old definition of `extreal_add` wrongly
94    allowed `PosInf + NegInf = PosInf`, while the definition of
95    `extreal_sub` wrongly allows `PosInf - PosInf = PosInf` and
96    `NegInf - NegInf = PosInf`. Now these cases are unspecified, as is
97    division-by-zero (which is indeed allowed for reals in
98    `realTheory`). As a consequence, now all `EXTREAL_SUM_IAMGE`-
99    related theorems require that there must be no mixing of `PosInf`
100    and `NegInf` in the sum elements. A bug in `ext_suminf` with
101    non-positive functions is also fixed.
102
103    There is a minor backwards-incompatibility: the above changes may
104    lead to more complicated proofs when using extreals, while better
105    alignments with textbook proofs are achieved, on the other hand.
106
107*   Fix soundness bug in the HolyHammer translations to first-order.
108    Lambda-lifting definitions were stated as local hypothesis but
109    were printed in the TPTP format as global definitions. In a few
110    cases, the global definition captured some type variables causing
111    a soundness issue. Now, local hypothesis are printed locally under
112    the quantification of type variables in the translated formula.
113
114New theories:
115-------------
116
117*   Univariate differential and integral calculus (based on
118    Henstock-Kurzweil Integral, or gauge integral) in
119    `derivativeTheory` and `integrationTheory`. Ported by Muhammad
120    Qasim and Osman Hasan from HOL Light (up to 2015).
121
122*   Measure and probability theories based on extended real numbers,
123    *i.e.*, the type of measure (probability) is `�� set -> extreal`.
124    The following new (or updated) theories are provided:
125
126    `sigma_algebraTheory`
127      ~ Sigma-algebra and other system of sets
128
129    `measureTheory`
130      ~ Measure Theory defined on extended reals
131
132    `real_borelTheory`
133      ~ Borel-measurable sets generated from reals
134
135    `borelTheory`
136      ~ Borel sets (on extended reals) and Borel-measurable functions
137
138    `lebesgueTheory`
139      ~ Lebesgue integration theory
140
141    `martingaleTheory`
142      ~ Martingales based on sigma-finite filtered measure space
143
144    `probabilityTheory`
145      ~ Probability theory based on extended reals
146
147    Notable theorems include: Carath��odory's Extension Theorem (for
148    semirings), the construction of 1-dimensional Borel and Lebesgue
149    measure spaces, Radon-Nikodym theorem, Tonelli and Fubini's
150    theorems (product measures), Bayes' Rule (Conditional
151    Probability), Kolmogorov 0-1 Law, Borel-Cantelli Lemma,
152    Markov/Chebyshev's inequalities, convergence concepts of random
153    sequences, and simple versions of the Law(s) of Large Numbers.
154
155    There is a major backwards-incompatibility: old proof scripts
156    based on real-valued measure and probability theories should now
157    open the following legacy theories instead: `sigma_algebraTheory`,
158    `real_measureTheory`, `real_borelTheory`, `real_lebesgueTheory`
159    and `real_probabilityTheory`. These legacy theories are stil
160    maintained to support `examples/miller` and
161    `examples/diningcryptos`, etc.
162
163    Thanks to Muhammad Qasim, Osman Hasan, Liya Liu and Waqar Ahmad *et
164    al.* for the original work, and Chun Tian for the integration and
165    further extension.
166
167New tools:
168----------
169
170*   `holwrap.py`: a simple python script that 'wraps' hol in a similar
171    fashion to rlwrap. Features include multiline input, history and
172    basic StandardML syntax highlighting. See the comments at the head
173    of the script for usage instructions.
174
175New examples:
176-------------
177
178*   __algebra__: an abstract algebra library for HOL4. The algebraic
179    types are generic, so the library is useful in general. The
180    algebraic structures consist of `monoidTheory` for monoids with
181    identity, `groupTheory` for groups, `ringTheory` for commutative
182    rings, `fieldTheory` for fields, `polynomialTheory` for
183    polynomials with coefficients from rings or fields, `linearTheory`
184    for vector spaces, including linear independence, and
185    `finitefieldTheory` for finite fields, including existence and
186    uniqueness.
187
188*   __simple_complexity__: a simple theory of recurrence loops to
189    assist the computational complexity analysis of algorithms. The
190    ingredients are `bitsizeTheory` for the complexity measure using
191    binary bits, `complexityTheory` for the big-O complexity class,
192    and `loopTheory` for various recurrence loop patterns of iteration
193    steps.
194
195*   __AKS__: a mechanisation of the AKS algorithm, contributed by
196    Hing Lun Chan from his PhD work.
197
198    The theory behind the AKS algorithm is delivered in
199    __AKS/theories__, starting with `AKSintroTheory`, the
200    introspective relation, culminating in `AKSimprovedTheory`,
201    proving that the AKS algorithm is a primality test. The underlying
202    theories are based on finite fields, hence making use of
203    `finitefieldTheory` in __algebra__.
204
205    An implementation of the AKS algorithm is shown to execute in
206    polynomial-time: the pseudo-codes of subroutines are given in
207    __AKS/compute__, and the corresponding implementations in monadic
208    style are given in __AKS/machine__, which includes a simple
209    machine model outlined in `countMonadTheory` and
210    `countMacroTheory`. Run-time analysis of subroutines is based on
211    `loopTheory` in __simple_complexity__.
212
213    The AKS main theorems and proofs have been cleaned up in
214    `AKScleanTheory`. For details, please refer to his [PhD
215    thesis](http://hdl.handle.net/1885/177195).
216
217*   The code for training tree neural networks using
218    `mlTreeNeuralNetwork` on datasets of arithmetical and
219    propositional formulas is located in __AI_TNN__.
220
221*   A demonstration of the reinforcement learning algorithm
222    `mlReinforce` on the tasks of synthesizing combinators and
223    Diophantine equations can be found in __AI_tasks__.
224
225*   __bootstrap__: a minimalistic verified bootstrapped compiler.
226    By bootstrapped, we mean that the compiler is applied to itself
227    inside the logic. We evaluate (using EVAL) this self-application
228    to arrive at an x86-64 assembly implementation of the compiler
229    function.
230
231*   __Hoare-for-divergence__: a Hoare logic for proving properties
232    of (the output behaviour of) diverging programs. This Hoare
233    logic has been proved sound and complete. The same directory also
234    includes soundness and completeness proofs for a standard
235    total-correctness Hoare logic.
236
237Incompatibilities:
238------------------
239
240*   The treatment of abbreviations (introduced with `qabbrev_tac` for
241    example), has changed slightly. The system tries harder to prevent
242    abbreviation assumptions from changing in form; they should stay
243    as `Abbrev(v = e)`, with `v` a variable, for longer. Further, the
244    tactic `VAR_EQ_TAC` which eliminates equalities in assumptions and
245    does some other forms of cleanup, and which is called as part of
246    the action of `rw`, `SRW_TAC` and others, now eliminates
247    ���malformed��� abbreviations. To restore the old behaviours, two
248    steps are required:
249
250           val _ = diminish_srw_ss ["ABBREV"]
251           val _ = set_trace "BasicProvers.var_eq_old" 1
252
253    which invocation can be made at the head of script files.
254
255*   The theorem `rich_listTheory.REVERSE` (alias of
256    `listTheory.REVERSE_SNOC_DEF`) has been removed because `REVERSE`
257    is also a tactical (`Tactical.REVERSE`).
258
259*   `listTheory` and `rich_listTheory`: Some theorems have been
260    generalized.
261
262    For example, `EVERY_{TAKE, DROP, BUTLASTN, LASTN}` had unnecessary
263    preconditions. As a result of some theorems being generalized,
264    some `_IMP` versions of the same theorems have been dropped, as
265    they are now special cases of the non-`_IMP` versions.
266
267    Also, `DROP_NIL` has been renamed to `DROP_EQ_NIL`, to avoid
268    having both `DROP_nil` and `DROP_NIL` around. Furthermore, `>=` in
269    the theorem statement has been replaced with `<=`.
270
271*   Renamed theorems in `pred_setTheory`: `SUBSET_SUBSET_EQ` became
272    `SUBSET_ANTISYM_EQ` (compatible with HOL Light).
273
274*   The theorem `SORTED_APPEND_trans_IFF` has been moved from
275    `alist_treeTheory` into `sortingTheory`. The moved theorem is now
276    available as `SORTED_APPEND`, and the old `SORTED_APPEND` is now
277    available as `SORTED_APPEND_IMP`. To avoid confusion, as
278    `SORTED_APPEND` is now an (conditional) equality,
279    `SORTED_APPEND_IFF` has been renamed to `SORTED_APPEND_GEN`.
280
281*   The definition `SORTED_DEF` is now an automatic rewrite, meaning
282    that terms of the form `SORTED R (h1::h2::t)` will now rewrite to
283    `R h1 h2 /\ SORTED (h2::t)` (in addition to the existing automatic
284    rewrites for `SORTED R []` and `SORTED R [x]`). To restore the old
285    behaviour it is necessary to exclude `SORTED_DEF` (use
286    `temp_delsimps`), and reinstate `SORTED_NIL` and `SORTED_SING`
287    (use `augment_srw_ss [rewrites [thmnames]]`).
288
289*   The syntax for *greater than* in `intSyntax` and `realSyntax` is
290    consistently named as in `numSyntax`: The functions
291    `great_tm`,`dest_great` and `mk_great` become `greater_tm`,
292    `dest_greater` and `mk_greater`, respectively. Additionally,
293    `int_arithTheory.add_to_great` is renamed to
294    `int_arithTheory.add_to_greater`.
295
296*   Two theorems about `list$nub` (the constant that removes
297    duplicates in a list), have been made automatic:
298    `listTheory.nub_NIL` (`��� nub [] = []`) and
299    `listTheory.all_distinct_nub` (`��� ���l. ALL_DISTINCT (nub l)`).
300    Calls to `temp_delsimps` can be used to remove automatic rewrites
301    as necessary.
302
303*   The SML API for `ThmSetData` has changed; user-provided call-backs that apply set-changes (additions and removals of theorems) are only ever called with single changes at once rather than lists, so the required types for these call-backs has changed to reflect this.
304
305*   Parsing of `~x` has been changed so that this is always preferentially interpreted as being a boolean operation.
306    This may break proofs over types with a numeric negation that use expressions such as
307
308           SPEC ���~x��� some_theorem
309
310    It is much better style to use `Q.SPEC ���~x��� some_theorem`; and indeed one can also use `-` as a unary operator, so that `Q.SPEC ���-x��� some_theorem` will also work.
311
312    If a big script is broken by this, one can reinstate the old behaviour by changing the grammar locally with
313
314           Overload "~"[local] = ���numeric_negation_operator���
315
316    where the appropriate negation operator might be, *e.g.*, `���$real_neg���`.
317
318* * * * *
319
320<div class="footer">
321*[HOL4, ??????](http://hol-theorem-prover.org)*
322
323[Release notes for the previous version](kananaskis-13.release.html)
324
325</div>
326