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