1% Release notes for HOL4, Kananaskis-11
2
3<!-- search and replace ?????? strings corresponding to release name -->
4<!-- indent code within bulleted lists to column 11 -->
5
6(Released: 3 March 2017)
7
8We are pleased to announce the Kananaskis-11 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-   [Examples](#examples)
18-   [Incompatibilities](#incompatibilities)
19
20New features:
21-------------
22
23- We have ported HOL Light���s `PAT_CONV` and `PATH_CONV` ���conversionals���, providing nice machinery for applying conversions to specific sub-terms.
24
25- The tactic `PAT_ABBREV_TAC` (also available in the `Q` module) can now use patterns that are more polymorphic than the sub-term in the goal that is ultimately matched. ([Github issue](http://github.com/HOL-Theorem-Prover/HOL/issues/252))
26
27- We have implemented the rule for constant specification described by Rob Arthan in [HOL Constant Definition Done Right](http://www.lemma-one.com/papers/hcddr.pdf).
28  The new primitive `gen_prim_specification` in the kernel is used to implement the new rule, `gen_new_specification`, and is also used to re-implement `new_definition` and `new_specification`.
29  We removed `prim_constant_definition` from the kernel, but kept `prim_specification` because the new derivation of `new_specification` uses pairs.
30  ([Github pull-req](https://github.com/HOL-Theorem-Prover/HOL/pull/201))
31
32- Various commands for moving over and selecting HOL tactics in the emacs mode have been improved.
33  We have also added a new command `hol-find-eval-next-tactic` (bound to `M-h M-e` by default), which selects and highlights the next tactic in the source text, and then applies it to the current goal in the `*HOL*` buffer.
34  This shortcuts the current idiom, which requires the tactic to be highlighted manually, and then applied *via* `M-h e`.
35  (The advantage of the latter is that one can select specific tactic sequences to be applied all at once.)
36
37-   Record updates can now be more polymorphic. For example, if one defined
38
39           Datatype`rcd = <| myset : �� -> bool ; size : num |>`
40
41    one used to get back an update constant for the `myset` field:
42
43           rcd_myset_fupd : ((�� -> bool) -> (�� -> bool)) -> �� rcd -> �� rcd
44
45    Now, the same constant is
46
47           rcd_myset_fupd : ((�� -> bool) -> (�� -> bool)) -> �� rcd -> �� rcd
48
49    One might use this to define
50
51           Define`img (f:��->��) r = r with myset updated_by IMAGE f`
52
53    This definition would have previously been rejected.  ([Github issue](https://github.com/HOL-Theorem-Prover/HOL/issues/173))
54
55    This change can cause **incompatibilities**.
56    If one wants the old behaviour, it should suffice to overload the record update syntax to use a more specific type.
57    For example:
58
59           val _ = gen_remove_ovl_mapping
60                     (GrammarSpecials.recfupd_special ^ "myset")
61                     ``��f x. rcd_myset_fupd f x``
62
63           val _ = Parse.add_record_fupdate(
64                 "myset", Term.inst[beta |-> alpha] ``rcd_myset_fupd``);
65
66-   PolyML ���heaps��� are now implemented with its `SaveState` technology, used hierarchically.
67    This should make heaps smaller as they now only save deltas over the last used heap.
68
69Bugs fixed:
70-----------
71
72- An embarrassing infinite loop bug in the integration of the integer decision procedures (the Omega test, Cooper���s algorithm) into the simplifier was fixed.
73
74- Theorems can now have names that are the same as SML constructor names (*e.g.*, `Empty`).  ([Github issue](http://github.com/HOL-Theorem-Prover/HOL/issues/225))
75
76- `Holmake` will now follow `INCLUDES` specifications from `Holmakefiles` when given ���phony��� targets to build on the command-line.  (A typical phony target is `all`.) As in the past, it will still act only locally if given just a clean target (`clean`, `cleanDeps` or `cleanAll`).  To clean recursively, you must also pass the `-r` flag to `Holmake`.  ([Github issue](http://github.com/HOL-Theorem-Prover/HOL/issues/145))
77
78-   We fixed three problems with `Datatype`. Thanks to Ramana Kumar for the reports.
79    [First](http://github.com/HOL-Theorem-Prover/HOL/issues/257), `Datatype` will no longer create a recursive type if the recursive instance  is qualified with a theory name other than the current one.
80    In other words,
81
82            Datatype`num = C1 num$num | C2`
83
84    won���t create a recursive type (assuming this is not called in theory `num`).
85    (`Hol_datatype` had the same problem.)
86
87    [Second](http://github.com/HOL-Theorem-Prover/HOL/issues/258), `Datatype` will handle antiquotations in its input properly (`Hol_datatype` already did).
88
89    [Third](http://github.com/HOL-Theorem-Prover/HOL/issues/260), `Datatype` (and `Hol_datatype`) allows the definition of identical record types in different theories.
90
91-   Attempts to define constants or types with invalid names are now caught much earlier.
92    An invalid name is one that contains ���non-graphical��� characters (as *per* SML���s `Char.isGraph`) or parentheses.
93    This means that Unicode cannot be used in the kernel���s name for a constant, but certainly doesn���t prevent Unicode being used in overloaded notation.
94    Functions such as `overload_on`, `add_rule` and `set_mapped_fixity` can still be used to create pretty notation with as many Unicode characters included as desired.
95
96-   Loading theories under Poly/ML would fail unnecessarily if the current directory was unwritable.
97    Working in such directories will likely cause problems when and if an `export_theory` call is made, so there is a warning emitted in this situation, but the `load` now succeeds.
98    Thanks to Narges Khakpour for the bug report.
99
100-   The function `thm_to_string` was creating ugly strings full of special codes (encoding type information) rather than using the ���raw��� backend.
101
102-   Bare record operations (*e.g.*, `rcdtype_field`, the function that accesses `field` of type `rcdtype`) would occasionally pretty-print badly.  ([Github issue](http://github.com/HOL-Theorem-Prover/HOL/issues/150))
103
104New theories:
105-------------
106
107New tools:
108----------
109
110-   **Holyhammer:** A method for automatically finding relevant theorems for Metis.
111    Given a term, the procedure selects a large number of lemmas through different predictors such as KNN or Mepo.
112    These lemmas are given to the external provers E-prover (1.9), Vampire (2.6) or Z3 (4.0).
113    The necessary lemmas  in the provers' proofs are then returned to the user.
114    Modifications to the kernels to track dependencies between theorems allow predictors to learn from the induced relation improving future predictions.
115    The build of the source directory `src/holyhammer` needs ocaml (> 3.12.1) installed as well as a recent version of g++ that supports the C++11 standard.
116    The three ATPs have to be installed independently.
117    At least one of them should be present, preferably E-prover (1.9).
118
119    Thanks to Thibault Gauthier for this tool.
120
121-   A principle for making coinductive definitions, `Hol_coreln`.
122    The input syntax is the same as for `Hol_reln`, that is: a conjunction of introduction rules.
123    For example, if one is representing coalgebraic lists as a subset of the type `:num ��� �� option`, the coinductive predicate specifying the subset would be given as
124
125           val (lrep_ok_rules, lrep_ok_coind, lrep_ok_cases) = Hol_coreln`
126             lrep_ok (��n. NONE)
127                 ���
128             ���h t.
129               lrep_ok t
130                   ���
131               lrep_ok (��n. if n = 0 then SOME h else t(n - 1))
132           `;
133
134    as is now done in `src/llist/llistScript.sml`.
135
136    Thanks to Andrea Condoluci for this tool.
137
138New examples:
139---------
140
141- A theory of balanced binary trees (`examples/balanced_bst`), based on Haskell code by Leijen and Palamarchuk, and mechanised by Scott Owens.  The type supports operations such as `insert`, `union`, `delete`, filters and folds.  Operations are parameterised by comparison operators for comparing keys.  Balanced trees can themselves be compared.
142
143-  A formalisation of pattern matches (`examples/pattern_matches`).
144   Pattern matching is not directly supported by higher-order logic.
145   HOL4���s parser therefore compiles case-expressions (`case x of ...`) to decision trees based on case constants.
146   For non-trivial case expressions, there is a big discrepancy between the user���s view and this internal representation.
147   The `pattern_matches` example defines a new general-purpose representation for case expressions that mirrors the input syntax in the internal representation closely.
148   Because of this close connection, the new representation is more intuitive and often much more compact.
149   Complicated parsers and pretty-printers are no longer required.
150   Proofs can more closely follow the user���s intentions, and code generators (like CakeML) can produce better code.
151   Moreover, the new representation is strictly more general than the currently used representation.
152   The new representation allows for guards, patterns with multiple occurrences of the same bound variable, unbound variables, arithmetic expressions in patterns, and more.
153   The example provides the definitions as well as tools to work with the new case-expressions.
154   These tools include support for evaluating and simplifying them, a highly configurable pattern compilation algorithm inside the logic, and optimisations like detecting redundant rows and eliminating them.
155
156
157Incompatibilities:
158------------------
159
160- The function `optionSyntax.dest_none` will now unwrap the type of its result, *e.g.*, returning `:��` rather than `:�� option` when applied to `NONE : �� option`.  This brings it into line with the behaviour of `listSyntax.dest_nil`.  See [this github issue](https://github.com/HOL-Theorem-Prover/HOL/issues/215).
161
162- The functions `Q.MATCH_RENAME_TAC` and `Q.MATCH_ASSUM_RENAME_TAC` have been adjusted to lose their second arguments (the list of variable names that are not to be bound).  For example, applying ``Q.MATCH_RENAME_TAC `(f x = Pair c1 c2) ��� X` ["X"]`` to the goal
163
164           ?- (f x = Pair C'' C0') ��� (f C'' = f C0')
165
166    used to result in the renamed goal
167
168           ?- (f x = Pair c1 c2) ��� (f c1 = f c2)
169
170    where the `X` in the pattern was ignored.
171    The interface now achieves the same end by simply allowing the user to write underscores in the pattern.
172    Thus, the tactic would become ``Q.MATCH_RENAME_TAC `(f x = Pair c1 c2) ��� _` ``.
173    Multiple underscores can be used to ignore multiple sub-terms.
174
175    Of course, the `qmatch_rename_tac` and `qmatch_assum_rename_tac` names for these tactics in `bossLib` have changed types as well.
176    The new `Q.MATCH_GOALSUB_RENAME_TAC` and `Q.MATCH_ASMSUB_RENAME_TAC` (and their lower-case versions) have similar types, without explicit lists of variable names to ignore.
177
178-   The theory `state_option` was removed.
179    The better-developed `errorStateMonad` theory should be used instead.
180
181* * * * *
182
183<div class="footer">
184*[HOL4, Kananaskis-11](http://hol-theorem-prover.org)*
185
186[Release notes for the previous version](kananaskis-10.release.html)
187
188</div>
189