NEWS
changeset 66472 1b7d66d62035
parent 66462 0a8277e9cfd6
child 66473 5928c6cc780f
     1.1 --- a/NEWS	Mon Aug 21 16:12:52 2017 +0200
     1.2 +++ b/NEWS	Mon Aug 21 16:55:26 2017 +0200
     1.3 @@ -4,8 +4,8 @@
     1.4  (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
     1.5  
     1.6  
     1.7 -New in this Isabelle version
     1.8 -----------------------------
     1.9 +New in Isabelle2017 (October 2017)
    1.10 +----------------------------------
    1.11  
    1.12  *** General ***
    1.13  
    1.14 @@ -29,17 +29,11 @@
    1.15  In order to import theories from other sessions, the ROOT file format
    1.16  provides a new 'sessions' keyword. In contrast, a theory that is
    1.17  imported in the old-fashioned manner via an explicit file-system path
    1.18 -belongs to the current session, and might cause theory name confusion
    1.19 +belongs to the current session, and might cause theory name conflicts
    1.20  later on. Theories that are imported from other sessions are excluded
    1.21  from the current session document. The command-line tool "isabelle
    1.22  imports" helps to update theory imports.
    1.23  
    1.24 -Properly qualified imports allow the Prover IDE to process arbitrary
    1.25 -theory hierarchies independently of the underlying logic session image
    1.26 -(e.g. option "isabelle jedit -l"), but the directory structure needs to
    1.27 -be known in advance (e.g. option "isabelle jedit -d" or a line in the
    1.28 -file $ISABELLE_HOME_USER/ROOTS).
    1.29 -
    1.30  * The main theory entry points for some non-HOL sessions have changed,
    1.31  to avoid confusion with the global name "Main" of the session HOL. This
    1.32  leads to the follow renamings:
    1.33 @@ -52,6 +46,10 @@
    1.34  
    1.35  INCOMPATIBILITY.
    1.36  
    1.37 +* Commands 'alias' and 'type_alias' introduce aliases for constants and
    1.38 +type constructors, respectively. This allows adhoc changes to name-space
    1.39 +accesses within global or local theory contexts, e.g. within a 'bundle'.
    1.40 +
    1.41  * Document antiquotations @{prf} and @{full_prf} output proof terms
    1.42  (again) in the same way as commands 'prf' and 'full_prf'.
    1.43  
    1.44 @@ -70,24 +68,14 @@
    1.45  src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
    1.46  tutorial on code generation.
    1.47  
    1.48 -* Commands 'alias' and 'type_alias' introduce aliases for constants and
    1.49 -type constructors, respectively. This allows adhoc changes to name-space
    1.50 -accesses within global or local theory contexts, e.g. within a 'bundle'.
    1.51 -
    1.52  
    1.53  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.54  
    1.55 -* Automatic indentation is more careful to avoid redundant spaces in
    1.56 -intermediate situations. Keywords are indented after input (via typed
    1.57 -characters or completion); see also option "jedit_indent_input".
    1.58 -
    1.59 -* Action "isabelle.preview" opens an HTML preview of the current theory
    1.60 -document in the default web browser.
    1.61 -
    1.62 -* Command-line invocation "isabelle jedit -R -l SESSION" uses the parent
    1.63 -image of the SESSION, with qualified theory imports restricted to that
    1.64 -portion of the session graph. Moreover, the ROOT entry of the SESSION is
    1.65 -opened in the editor.
    1.66 +* Session-qualified theory imports allow the Prover IDE to process
    1.67 +arbitrary theory hierarchies independently of the underlying logic
    1.68 +session image (e.g. option "isabelle jedit -l"), but the directory
    1.69 +structure needs to be known in advance (e.g. option "isabelle jedit -d"
    1.70 +or a line in the file $ISABELLE_HOME_USER/ROOTS).
    1.71  
    1.72  * The PIDE document model maintains file content independently of the
    1.73  status of jEdit editor buffers. Reloading jEdit buffers no longer causes
    1.74 @@ -105,122 +93,96 @@
    1.75  painted with thick lines; remaining errors in this situation are
    1.76  represented by a different border color.
    1.77  
    1.78 +* Automatic indentation is more careful to avoid redundant spaces in
    1.79 +intermediate situations. Keywords are indented after input (via typed
    1.80 +characters or completion); see also option "jedit_indent_input".
    1.81 +
    1.82 +* Action "isabelle.preview" opens an HTML preview of the current theory
    1.83 +document in the default web browser.
    1.84 +
    1.85 +* Command-line invocation "isabelle jedit -R -l SESSION" uses the parent
    1.86 +image of the SESSION, with qualified theory imports restricted to that
    1.87 +portion of the session graph. Moreover, the ROOT entry of the SESSION is
    1.88 +opened in the editor.
    1.89 +
    1.90  * The main Isabelle/jEdit plugin may be restarted manually (using the
    1.91  jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains
    1.92  enabled at all times.
    1.93  
    1.94 -* Update to jedit-5.4.0.
    1.95 +* Update to current jedit-5.4.0.
    1.96  
    1.97  
    1.98  *** Pure ***
    1.99  
   1.100  * Deleting the last code equations for a particular function using
   1.101  [code del] results in function with no equations (runtime abort) rather
   1.102 -than an unimplemented function (generation time abort).  Use explicit
   1.103 -[[code drop:]] to enforce the latter.  Minor INCOMPATIBILTIY.
   1.104 +than an unimplemented function (generation time abort). Use explicit
   1.105 +[[code drop:]] to enforce the latter. Minor INCOMPATIBILTIY.
   1.106  
   1.107  * Proper concept of code declarations in code.ML:
   1.108 -  - Regular code declarations act only on the global theory level,
   1.109 -    being ignored with warnings if syntactically malformed.
   1.110 -  - Explicitly global code declarations yield errors if syntactically malformed.
   1.111 -  - Default code declarations are silently ignored if syntactically malformed.
   1.112 +  - Regular code declarations act only on the global theory level, being
   1.113 +    ignored with warnings if syntactically malformed.
   1.114 +  - Explicitly global code declarations yield errors if syntactically
   1.115 +    malformed.
   1.116 +  - Default code declarations are silently ignored if syntactically
   1.117 +    malformed.
   1.118  Minor INCOMPATIBILITY.
   1.119  
   1.120 -* Clarified and standardized internal data bookkeeping of code declarations:
   1.121 -history of serials allows to track potentially non-monotonous declarations
   1.122 -appropriately.  Minor INCOMPATIBILITY.
   1.123 +* Clarified and standardized internal data bookkeeping of code
   1.124 +declarations: history of serials allows to track potentially
   1.125 +non-monotonous declarations appropriately. Minor INCOMPATIBILITY.
   1.126  
   1.127  
   1.128  *** HOL ***
   1.129  
   1.130 -* Theory Library/Pattern_Aliases provides input syntax for pattern
   1.131 -aliases as known from Haskell, Scala and ML.
   1.132 -
   1.133 -* Constant "subseq" in Topological_Spaces removed and subsumed by
   1.134 -"strict_mono". Some basic lemmas specific to "subseq" have been renamed
   1.135 -accordingly, e.g. "subseq_o" -> "strict_mono_o" etc.
   1.136 +* SMT module:
   1.137 +  - A new option, 'smt_nat_as_int', has been added to translate 'nat' to
   1.138 +    'int' and benefit from the SMT solver's theory reasoning. It is
   1.139 +    disabled by default.
   1.140 +  - The legacy module "src/HOL/Library/Old_SMT.thy" has been removed.
   1.141 +  - Several small issues have been rectified in the 'smt' command.
   1.142 +
   1.143 +* (Co)datatype package: The 'size_gen_o_map' lemma is no longer
   1.144 +generated for datatypes with type class annotations. As a result, the
   1.145 +tactic that derives it no longer fails on nested datatypes. Slight
   1.146 +INCOMPATIBILITY.
   1.147  
   1.148  * Command and antiquotation "value" with modified default strategy:
   1.149  terms without free variables are always evaluated using plain evaluation
   1.150 -only, with no fallback on normalization by evaluation.
   1.151 -Minor INCOMPATIBILITY.
   1.152 -
   1.153 -* Notions of squarefreeness, n-th powers, and prime powers in
   1.154 -HOL-Computational_Algebra and HOL-Number_Theory.
   1.155 -
   1.156 -* Material on infinite products in HOL-Analysis
   1.157 -
   1.158 -* Theory List:
   1.159 -  "sublist" renamed to "nths" in analogy with "nth".
   1.160 -  "sublisteq" renamed to "subseq".
   1.161 -  Minor INCOMPATIBILITY.
   1.162 -  New generic function "sorted_wrt"
   1.163 +only, with no fallback on normalization by evaluation. Minor
   1.164 +INCOMPATIBILITY.
   1.165  
   1.166  * Theories "GCD" and "Binomial" are already included in "Main" (instead
   1.167  of "Complex_Main").
   1.168  
   1.169 -* Constants E/L/F in Library/Formal_Power_Series were renamed to
   1.170 -fps_exp/fps_ln/fps_hypergeo to avoid polluting the name space.
   1.171 -INCOMPATIBILITY.
   1.172 -
   1.173 -* Theory Totient in session Number_Theory introduces basic notions
   1.174 -about Euler's totient function previously hidden as solitary example
   1.175 -in theory Residues. Definition changed so that "totient 1 = 1" in
   1.176 -agreement with the literature.  Minor INCOMPATIBILITY.
   1.177 -
   1.178 -* Session "Computional_Algebra" covers many previously scattered
   1.179 -theories, notably Euclidean_Algorithm, Factorial_Ring, Formal_Power_Series,
   1.180 -Fraction_Field, Fundamental_Theorem_Algebra, Normalized_Fraction,
   1.181 -Polynomial_FPS, Polynomial, Primes.  Minor INCOMPATIBILITY.
   1.182 -
   1.183  * Constant "surj" is a full input/output abbreviation (again).
   1.184  Minor INCOMPATIBILITY.
   1.185  
   1.186 -* Theory Library/FinFun has been moved to AFP (again).  INCOMPATIBILITY.
   1.187 -
   1.188 -* Some old and rarely used ASCII replacement syntax has been removed.
   1.189 -INCOMPATIBILITY, standard syntax with symbols should be used instead.
   1.190 -The subsequent commands help to reproduce the old forms, e.g. to
   1.191 -simplify porting old theories:
   1.192 -
   1.193 -syntax (ASCII)
   1.194 -  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
   1.195 -  "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
   1.196 -  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)
   1.197 -
   1.198  * Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
   1.199  INCOMPATIBILITY.
   1.200  
   1.201 -* Renamed ii to imaginary_unit in order to free up ii as a variable name.
   1.202 -The syntax \<i> remains available.
   1.203 -INCOMPATIBILITY.
   1.204 -
   1.205 -* Dropped abbreviations transP, antisymP, single_valuedP;
   1.206 -use constants transp, antisymp, single_valuedp instead.
   1.207 -INCOMPATIBILITY.
   1.208 -
   1.209 -* Algebraic type class hierarchy of euclidean (semi)rings in HOL:
   1.210 -euclidean_(semi)ring, euclidean_(semi)ring_cancel,
   1.211 -unique_euclidean_(semi)ring; instantiation requires
   1.212 -provision of a euclidean size.
   1.213 -
   1.214 -* Reworking of theory Euclidean_Algorithm in session HOL-Number_Theory:
   1.215 -  - Euclidean induction is available as rule eucl_induct;
   1.216 -  - Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm,
   1.217 -    Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow
   1.218 -    easy instantiation of euclidean (semi)rings as GCD (semi)rings.
   1.219 -  - Coefficients obtained by extended euclidean algorithm are
   1.220 -    available as "bezout_coefficients".
   1.221 -INCOMPATIBILITY.
   1.222 -
   1.223 -* Named collection mod_simps covers various congruence rules
   1.224 -concerning mod, replacing former zmod_simps.
   1.225 -INCOMPATIBILITY.
   1.226 +* Renamed ii to imaginary_unit in order to free up ii as a variable
   1.227 +name. The syntax \<i> remains available. INCOMPATIBILITY.
   1.228 +
   1.229 +* Dropped abbreviations transP, antisymP, single_valuedP; use constants
   1.230 +transp, antisymp, single_valuedp instead. INCOMPATIBILITY.
   1.231 +
   1.232 +* Constant "subseq" in Topological_Spaces has been removed -- it is
   1.233 +subsumed by "strict_mono". Some basic lemmas specific to "subseq" have
   1.234 +been renamed accordingly, e.g. "subseq_o" -> "strict_mono_o" etc.
   1.235 +
   1.236 +* Theory List: "sublist" renamed to "nths" in analogy with "nth", and
   1.237 +"sublisteq" renamed to "subseq". Minor INCOMPATIBILITY.
   1.238 +
   1.239 +* Theory List: new generic function "sorted_wrt".
   1.240 +
   1.241 +* Named theorems mod_simps covers various congruence rules concerning
   1.242 +mod, replacing former zmod_simps. INCOMPATIBILITY.
   1.243  
   1.244  * Swapped orientation of congruence rules mod_add_left_eq,
   1.245  mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
   1.246  mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
   1.247 -mod_diff_eq.  INCOMPATIBILITY.
   1.248 +mod_diff_eq. INCOMPATIBILITY.
   1.249  
   1.250  * Generalized some facts:
   1.251      measure_induct_rule
   1.252 @@ -231,45 +193,76 @@
   1.253      zmod_eq_dvd_iff ~> mod_eq_dvd_iff
   1.254  INCOMPATIBILITY.
   1.255  
   1.256 -* (Co)datatype package:
   1.257 -  - The 'size_gen_o_map' lemma is no longer generated for datatypes
   1.258 -    with type class annotations. As a result, the tactic that derives
   1.259 -    it no longer fails on nested datatypes. Slight INCOMPATIBILITY.
   1.260 -
   1.261 -* Session HOL-Algebra extended by additional lattice theory: the
   1.262 -Knaster-Tarski fixed point theorem and Galois Connections.
   1.263 -
   1.264 -* SMT module:
   1.265 -  - A new option, 'smt_nat_as_int', has been added to translate 'nat' to
   1.266 -    'int' and benefit from the SMT solver's theory reasoning. It is disabled
   1.267 -    by default.
   1.268 -  - The legacy module 'src/HOL/Library/Old_SMT.thy' has been removed.
   1.269 -  - Several small issues have been rectified in the 'smt' command.
   1.270 +* Algebraic type class hierarchy of euclidean (semi)rings in HOL:
   1.271 +euclidean_(semi)ring, euclidean_(semi)ring_cancel,
   1.272 +unique_euclidean_(semi)ring; instantiation requires provision of a
   1.273 +euclidean size.
   1.274 +
   1.275 +* Theory "HOL-Number_Theory.Euclidean_Algorithm" has been reworked:
   1.276 +  - Euclidean induction is available as rule eucl_induct.
   1.277 +  - Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm,
   1.278 +    Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow
   1.279 +    easy instantiation of euclidean (semi)rings as GCD (semi)rings.
   1.280 +  - Coefficients obtained by extended euclidean algorithm are
   1.281 +    available as "bezout_coefficients".
   1.282 +INCOMPATIBILITY.
   1.283 +
   1.284 +* Theory "Number_Theory.Totient" introduces basic notions about Euler's
   1.285 +totient function previously hidden as solitary example in theory
   1.286 +Residues. Definition changed so that "totient 1 = 1" in agreement with
   1.287 +the literature. Minor INCOMPATIBILITY.
   1.288 +
   1.289 +* Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
   1.290 +been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
   1.291 +
   1.292 +* Theory "HOL-Library.Formal_Power_Series": constants E/L/F have been
   1.293 +renamed to fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
   1.294 +space. INCOMPATIBILITY.
   1.295 +
   1.296 +* Theory "HOL-Library.FinFun" has been moved to AFP (again).
   1.297 +INCOMPATIBILITY.
   1.298 +
   1.299 +* Theory "HOL-Library.FuncSet": some old and rarely used ASCII
   1.300 +replacement syntax has been removed. INCOMPATIBILITY, standard syntax
   1.301 +with symbols should be used instead. The subsequent commands help to
   1.302 +reproduce the old forms, e.g. to simplify porting old theories:
   1.303 +
   1.304 +syntax (ASCII)
   1.305 +  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
   1.306 +  "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
   1.307 +  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)
   1.308 +
   1.309 +* Theory "HOL-Library.Multiset": the simprocs on subsets operators of
   1.310 +multisets have been renamed:
   1.311 +
   1.312 +  msetless_cancel_numerals ~> msetsubset_cancel
   1.313 +  msetle_cancel_numerals ~> msetsubset_eq_cancel
   1.314 +
   1.315 +INCOMPATIBILITY.
   1.316 +
   1.317 +* Theory "HOL-Library.Pattern_Aliases" provides input syntax for pattern
   1.318 +aliases as known from Haskell, Scala and ML.
   1.319  
   1.320  * Session HOL-Analysis: more material involving arcs, paths, covering
   1.321 -spaces, innessential maps, retracts. Major results include the Jordan
   1.322 -Curve Theorem and the Great Picard Theorem.
   1.323 -
   1.324 -* The theorem in Permutations has been renamed:
   1.325 -  bij_swap_ompose_bij ~> bij_swap_compose_bij
   1.326 -
   1.327 -* Session HOL-Library: The simprocs on subsets operators of multisets
   1.328 -have been renamed:
   1.329 -  msetless_cancel_numerals ~> msetsubset_cancel
   1.330 -  msetle_cancel_numerals ~> msetsubset_eq_cancel
   1.331 -INCOMPATIBILITY.
   1.332 -
   1.333 -* Session HOL-Library: The suffix _numerals has been removed from the
   1.334 -name of the simprocs on multisets. INCOMPATIBILITY.
   1.335 +spaces, innessential maps, retracts, material on infinite products.
   1.336 +Major results include the Jordan Curve Theorem and the Great Picard
   1.337 +Theorem.
   1.338 +
   1.339 +* Session HOL-Algebra has been extended by additional lattice theory:
   1.340 +the Knaster-Tarski fixed point theorem and Galois Connections.
   1.341 +
   1.342 +* Sessions HOL-Computational_Algebra and HOL-Number_Theory: new notions
   1.343 +of squarefreeness, n-th powers, and prime powers.
   1.344 +
   1.345 +* Session "HOL-Computional_Algebra" covers many previously scattered
   1.346 +theories, notably Euclidean_Algorithm, Factorial_Ring,
   1.347 +Formal_Power_Series, Fraction_Field, Fundamental_Theorem_Algebra,
   1.348 +Normalized_Fraction, Polynomial_FPS, Polynomial, Primes. Minor
   1.349 +INCOMPATIBILITY.
   1.350  
   1.351  
   1.352  *** System ***
   1.353  
   1.354 -* Option parallel_proofs is 1 by default (instead of more aggressive 2).
   1.355 -This requires less heap space and avoids burning parallel CPU cycles,
   1.356 -while full subproof parallelization is enabled for repeated builds
   1.357 -(according to parallel_subproofs_threshold).
   1.358 -
   1.359  * Prover IDE support for the Visual Studio Code editor and language
   1.360  server protocol, via the "isabelle vscode_server" tool (see also
   1.361  src/Tools/VSCode/README.md). The example application within the VS code
   1.362 @@ -277,27 +270,24 @@
   1.363  (the "Marketplace"). It serves as example for further potential IDE
   1.364  front-ends.
   1.365  
   1.366 -* ISABELLE_SCALA_BUILD_OPTIONS has been renamed to
   1.367 -ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY.
   1.368 -
   1.369 -* Isabelle settings ISABELLE_WINDOWS_PLATFORM,
   1.370 -ISABELLE_WINDOWS_PLATFORM32, ISABELLE_WINDOWS_PLATFORM64 indicate the
   1.371 -native Windows platform (independently of the Cygwin installation). This
   1.372 -is analogous to ISABELLE_PLATFORM, ISABELLE_PLATFORM32,
   1.373 -ISABELLE_PLATFORM64.
   1.374 +* System option "parallel_proofs" is 1 by default (instead of more
   1.375 +aggressive 2). This requires less heap space and avoids burning parallel
   1.376 +CPU cycles, while full subproof parallelization is enabled for repeated
   1.377 +builds (according to parallel_subproofs_threshold).
   1.378  
   1.379  * System option "record_proofs" allows to change the global
   1.380  Proofterm.proofs variable for a session. Regular values are are 0, 1, 2;
   1.381  a negative value means the current state in the ML heap image remains
   1.382  unchanged.
   1.383  
   1.384 -* Command-line tool "isabelle imports" helps to maintain theory imports
   1.385 -wrt. session structure. Examples:
   1.386 -
   1.387 -  isabelle imports -I -a
   1.388 -  isabelle imports -U -a
   1.389 -  isabelle imports -U -i -a
   1.390 -  isabelle imports -M -a -d '~~/src/Benchmarks'
   1.391 +* Isabelle settings variable ISABELLE_SCALA_BUILD_OPTIONS has been
   1.392 +renamed to ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY.
   1.393 +
   1.394 +* Isabelle settings variables ISABELLE_WINDOWS_PLATFORM,
   1.395 +ISABELLE_WINDOWS_PLATFORM32, ISABELLE_WINDOWS_PLATFORM64 indicate the
   1.396 +native Windows platform (independently of the Cygwin installation). This
   1.397 +is analogous to ISABELLE_PLATFORM, ISABELLE_PLATFORM32,
   1.398 +ISABELLE_PLATFORM64.
   1.399  
   1.400  * Isabelle/Scala: the SQL module supports access to relational
   1.401  databases, either as plain file (SQLite) or full-scale server
   1.402 @@ -308,6 +298,14 @@
   1.403  https://www.sqlite.org/appfileformat.html). This allows systematic
   1.404  access via operations from module Sessions.Store in Isabelle/Scala.
   1.405  
   1.406 +* Command-line tool "isabelle imports" helps to maintain theory imports
   1.407 +wrt. session structure. Examples:
   1.408 +
   1.409 +  isabelle imports -I -a
   1.410 +  isabelle imports -U -a
   1.411 +  isabelle imports -U -i -a
   1.412 +  isabelle imports -M -a -d '~~/src/Benchmarks'
   1.413 +
   1.414  
   1.415  New in Isabelle2016-1 (December 2016)
   1.416  -------------------------------------