--- a/NEWS Sat Nov 21 20:44:16 2009 +0100
+++ b/NEWS Sun Nov 22 14:13:18 2009 +0100
@@ -1,8 +1,8 @@
Isabelle NEWS -- history user-relevant changes
==============================================
-New in this Isabelle version
-----------------------------
+New in Isabelle2009-1 (December 2009)
+-------------------------------------
*** General ***
@@ -19,74 +19,77 @@
The currently only available mixins are the equations used to map
local definitions to terms of the target domain of an interpretation.
-* Reactivated diagnositc command 'print_interps'. Use 'print_interps l'
-to print all interpretations of locale l in the theory. Interpretations
-in proofs are not shown.
+* Reactivated diagnostic command 'print_interps'. Use "print_interps
+loc" to print all interpretations of locale "loc" in the theory.
+Interpretations in proofs are not shown.
* Thoroughly revised locales tutorial. New section on conditional
interpretation.
-*** document preparation ***
-
-* New generalized style concept for printing terms:
-write @{foo (style) ...} instead of @{foo_style style ...}
-(old form is still retained for backward compatibility).
-Styles can be also applied for antiquotations prop, term_type and typeof.
+*** Document preparation ***
+
+* New generalized style concept for printing terms: @{foo (style) ...}
+instead of @{foo_style style ...} (old form is still retained for
+backward compatibility). Styles can be also applied for
+antiquotations prop, term_type and typeof.
*** HOL ***
-* A tabled implementation of the reflexive transitive closure
-
-* New commands "code_pred" and "values" to invoke the predicate compiler
-and to enumerate values of inductive predicates.
-
-* Combined former theories Divides and IntDiv to one theory Divides
-in the spirit of other number theory theories in HOL; some constants
-(and to a lesser extent also facts) have been suffixed with _nat und _int
+* A tabled implementation of the reflexive transitive closure.
+
+* New commands 'code_pred' and 'values' to invoke the predicate
+compiler and to enumerate values of inductive predicates.
+
+* Combined former theories Divides and IntDiv to one theory Divides in
+the spirit of other number theory theories in HOL; some constants (and
+to a lesser extent also facts) have been suffixed with _nat and _int
respectively. INCOMPATIBILITY.
-* Most rules produced by inductive and datatype package
-have mandatory prefixes.
-INCOMPATIBILITY.
-
-* New proof method "smt" for a combination of first-order logic
-with equality, linear and nonlinear (natural/integer/real)
-arithmetic, and fixed-size bitvectors; there is also basic
-support for higher-order features (esp. lambda abstractions).
-It is an incomplete decision procedure based on external SMT
-solvers using the oracle mechanism; for the SMT solver Z3,
-this method is proof-producing. Certificates are provided to
-avoid calling the external solvers solely for re-checking proofs.
-Due to a remote SMT service there is no need for installing SMT
-solvers locally.
-
-* New commands to load and prove verification conditions
-generated by the Boogie program verifier or derived systems
-(e.g. the Verifying C Compiler (VCC) or Spec#).
-
-* New counterexample generator tool "nitpick" based on the Kodkod
-relational model finder.
-
-* Reorganization of number theory:
- * former session NumberTheory now named Old_Number_Theory
- * new session Number_Theory by Jeremy Avigad; if possible, prefer this.
- * moved legacy theories Legacy_GCD and Primes from Library/ to Old_Number_Theory/;
- * moved theory Pocklington from Library/ to Old_Number_Theory/;
- * removed various references to Old_Number_Theory from HOL distribution.
-INCOMPATIBILITY.
+* Most rules produced by inductive and datatype package have mandatory
+prefixes. INCOMPATIBILITY.
+
+* New proof method "smt" for a combination of first-order logic with
+equality, linear and nonlinear (natural/integer/real) arithmetic, and
+fixed-size bitvectors; there is also basic support for higher-order
+features (esp. lambda abstractions). It is an incomplete decision
+procedure based on external SMT solvers using the oracle mechanism;
+for the SMT solver Z3, this method is proof-producing. Certificates
+are provided to avoid calling the external solvers solely for
+re-checking proofs. Due to a remote SMT service there is no need for
+installing SMT solvers locally. See src/HOL/SMT.
+
+* New commands to load and prove verification conditions generated by
+the Boogie program verifier or derived systems (e.g. the Verifying C
+Compiler (VCC) or Spec#). See src/HOL/Boogie.
+
+* New counterexample generator tool 'nitpick' based on the Kodkod
+relational model finder. See src/HOL/Tools/Nitpick and
+src/HOL/Nitpick_Examples.
+
+* Reorganization of number theory, INCOMPATIBILITY:
+ - former session NumberTheory now named Old_Number_Theory
+ - new session Number_Theory; prefer this, if possible
+ - moved legacy theories Legacy_GCD and Primes from src/HOL/Library
+ to src/HOL/Old_Number_Theory
+ - moved theory Pocklington from src/HOL/Library to
+ src/HOL/Old_Number_Theory
+ - removed various references to Old_Number_Theory from HOL
+ distribution
* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
of finite and infinite sets. It is shown that they form a complete
lattice.
-* New theory SupInf of the supremum and infimum operators for sets of reals.
-
-* New theory Probability, which contains a development of measure theory, eventually leading to Lebesgue integration and probability.
-
-* Split off prime number ingredients from theory GCD
-to theory Number_Theory/Primes;
+* Split off prime number ingredients from theory GCD to theory
+Number_Theory/Primes.
+
+* New theory SupInf of the supremum and infimum operators for sets of
+reals.
+
+* New theory Probability, which contains a development of measure
+theory, eventually leading to Lebesgue integration and probability.
* Class semiring_div requires superclass no_zero_divisors and proof of
div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
@@ -96,32 +99,33 @@
zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
INCOMPATIBILITY.
-* Extended Multivariate Analysis to include derivation and Brouwer's fixpoint
-theorem.
-
-* Removed predicate "M hassize n" (<--> card M = n & finite M). Was only used
-in Multivariate Analysis. Renamed vector_less_eq_def to vector_le_def, the
-more usual name.
+* Extended Multivariate Analysis to include derivation and Brouwer's
+fixpoint theorem.
+
+* Removed predicate "M hassize n" (<--> card M = n & finite M).
+INCOMPATIBILITY.
+
+* Renamed vector_less_eq_def to vector_le_def, the more usual name.
INCOMPATIBILITY.
-* Added theorem List.map_map as [simp]. Removed List.map_compose.
+* Added theorem List.map_map as [simp]. Removed List.map_compose.
INCOMPATIBILITY.
-* New testing tool "Mirabelle" for automated (proof) tools. Applies
+* New testing tool "Mirabelle" for automated proof tools. Applies
several tools and tactics like sledgehammer, metis, or quickcheck, to
-every proof step in a theory. To be used in batch mode via the
+every proof step in a theory. To be used in batch mode via the
"mirabelle" utility.
* New proof method "sos" (sum of squares) for nonlinear real
-arithmetic (originally due to John Harison). It requires
+arithmetic (originally due to John Harison). It requires theory
Library/Sum_Of_Squares. It is not a complete decision procedure but
works well in practice on quantifier-free real arithmetic with +, -,
*, ^, =, <= and <, i.e. boolean combinations of equalities and
-inequalities between polynomials. It makes use of external
-semidefinite programming solvers. Method "sos" generates a certificate
-that can be pasted into the proof thus avoiding the need to call an external
-tool every time the proof is checked.
-For more information and examples see src/HOL/Library/Sum_Of_Squares.
+inequalities between polynomials. It makes use of external
+semidefinite programming solvers. Method "sos" generates a
+certificate that can be pasted into the proof thus avoiding the need
+to call an external tool every time the proof is checked. See
+src/HOL/Library/Sum_Of_Squares.
* Code generator attributes follow the usual underscore convention:
code_unfold replaces code unfold
@@ -132,12 +136,15 @@
* Refinements to lattice classes and sets:
- less default intro/elim rules in locale variant, more default
intro/elim rules in class variant: more uniformity
- - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
- - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
+ - lemma ge_sup_conv renamed to le_sup_iff, in accordance with
+ le_inf_iff
+ - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and
+ sup_aci)
- renamed ACI to inf_sup_aci
- new class "boolean_algebra"
- - class "complete_lattice" moved to separate theory "complete_lattice";
- corresponding constants (and abbreviations) renamed and with authentic syntax:
+ - class "complete_lattice" moved to separate theory
+ "complete_lattice"; corresponding constants (and abbreviations)
+ renamed and with authentic syntax:
Set.Inf ~> Complete_Lattice.Inf
Set.Sup ~> Complete_Lattice.Sup
Set.INFI ~> Complete_Lattice.INFI
@@ -164,111 +171,101 @@
- object-logic definitions as far as appropriate
INCOMPATIBILITY. Care is required when theorems Int_subset_iff or
-Un_subset_iff are explicitly deleted as default simp rules; then
-also their lattice counterparts le_inf_iff and le_sup_iff have to be
+Un_subset_iff are explicitly deleted as default simp rules; then also
+their lattice counterparts le_inf_iff and le_sup_iff have to be
deleted to achieve the desired effect.
-* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no
-simp rules by default any longer. The same applies to
-min_max.inf_absorb1 etc.! INCOMPATIBILITY.
-
-* sup_Int_eq and sup_Un_eq are no default pred_set_conv rules any longer.
-INCOMPATIBILITY.
-
-* Power operations on relations and functions are now one dedicate
+* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp
+rules by default any longer; the same applies to min_max.inf_absorb1
+etc. INCOMPATIBILITY.
+
+* Rules sup_Int_eq and sup_Un_eq are no longer declared as
+pred_set_conv by default. INCOMPATIBILITY.
+
+* Power operations on relations and functions are now one dedicated
constant "compow" with infix syntax "^^". Power operation on
multiplicative monoids retains syntax "^" and is now defined generic
in class power. INCOMPATIBILITY.
-* Relation composition "R O S" now has a "more standard" argument
-order, i.e., "R O S = {(x,z). EX y. (x,y) : R & (y,z) : S }".
-INCOMPATIBILITY: Rewrite propositions with "S O R" --> "R O S". Proofs
-may occationally break, since the O_assoc rule was not rewritten like
-this. Fix using O_assoc[symmetric]. The same applies to the curried
-version "R OO S".
+* Relation composition "R O S" now has a more standard argument order:
+"R O S = {(x, z). EX y. (x, y) : R & (y, z) : S}". INCOMPATIBILITY,
+rewrite propositions with "S O R" --> "R O S". Proofs may occasionally
+break, since the O_assoc rule was not rewritten like this. Fix using
+O_assoc[symmetric]. The same applies to the curried version "R OO S".
* Function "Inv" is renamed to "inv_into" and function "inv" is now an
-abbreviation for "inv_into UNIV". Lemmas are renamed accordingly.
+abbreviation for "inv_into UNIV". Lemmas are renamed accordingly.
INCOMPATIBILITY.
* ML antiquotation @{code_datatype} inserts definition of a datatype
-generated by the code generator; see Predicate.thy for an example.
+generated by the code generator; e.g. see src/HOL/Predicate.thy.
* New method "linarith" invokes existing linear arithmetic decision
procedure only.
* New implementation of quickcheck uses generic code generator;
default generators are provided for all suitable HOL types, records
-and datatypes. Old quickcheck can be re-activated importing
-theory Library/SML_Quickcheck.
+and datatypes. Old quickcheck can be re-activated importing theory
+Library/SML_Quickcheck.
* Renamed theorems:
Suc_eq_add_numeral_1 -> Suc_eq_plus1
Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
Suc_plus1 -> Suc_eq_plus1
-* Moved theorems:
-Wellfounded.in_inv_image -> Relation.in_inv_image
-
* New sledgehammer option "Full Types" in Proof General settings menu.
Causes full type information to be output to the ATPs. This slows
ATPs down considerably but eliminates a source of unsound "proofs"
that fail later.
-* New method metisFT: A version of metis that uses full type information
-in order to avoid failures of proof reconstruction.
-
-* Discontinued ancient tradition to suffix certain ML module names
-with "_package", e.g.:
-
- DatatypePackage ~> Datatype
- InductivePackage ~> Inductive
-
-INCOMPATIBILITY.
-
-* Discontinued abbreviation "arbitrary" of constant
-"undefined". INCOMPATIBILITY, use "undefined" directly.
+* New method "metisFT": A version of metis that uses full type
+information in order to avoid failures of proof reconstruction.
+
+* Discontinued abbreviation "arbitrary" of constant "undefined".
+INCOMPATIBILITY, use "undefined" directly.
* New evaluator "approximate" approximates an real valued term using
the same method as the approximation method.
-* Method "approximate" supports now arithmetic expressions as
+* Method "approximate" now supports arithmetic expressions as
boundaries of intervals and implements interval splitting and Taylor
series expansion.
-* Changed DERIV_intros to a dynamic fact (via Named_Thms). Each of
-the theorems in DERIV_intros assumes composition with an additional
-function and matches a variable to the derivative, which has to be
-solved by the simplifier. Hence (auto intro!: DERIV_intros) computes
-the derivative of most elementary terms.
-
-* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are
-replaced by: (auto intro!: DERIV_intros). INCOMPATIBILITY.
+* Changed "DERIV_intros" to a dynamic fact, which can be augmented by
+the attribute of the same name. Each of the theorems in the list
+DERIV_intros assumes composition with an additional function and
+matches a variable to the derivative, which has to be solved by the
+Simplifier. Hence (auto intro!: DERIV_intros) computes the derivative
+of most elementary terms.
+
+* Former Maclauren.DERIV_tac and Maclauren.deriv_tac are superseded
+are replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY.
* Renamed methods:
sizechange -> size_change
induct_scheme -> induction_schema
* Lemma name change: replaced "anti_sym" by "antisym" everywhere.
+INCOMPATIBILITY.
*** HOLCF ***
-* Theory 'Representable.thy' defines a class 'rep' of domains that are
-representable (via an ep-pair) in the universal domain type 'udom'.
+* Theory Representable defines a class "rep" of domains that are
+representable (via an ep-pair) in the universal domain type "udom".
Instances are provided for all type constructors defined in HOLCF.
* The 'new_domain' command is a purely definitional version of the
domain package, for representable domains. Syntax is identical to the
old domain package. The 'new_domain' package also supports indirect
recursion using previously-defined type constructors. See
-HOLCF/ex/New_Domain.thy for examples.
-
-* Method 'fixrec_simp' unfolds one step of a fixrec-defined constant
+src/HOLCF/ex/New_Domain.thy for examples.
+
+* Method "fixrec_simp" unfolds one step of a fixrec-defined constant
on the left-hand side of an equation, and then performs
simplification. Rewriting is done using rules declared with the
-'fixrec_simp' attribute. The 'fixrec_simp' method is intended as a
-replacement for 'fixpat'; see HOLCF/ex/Fixrec_ex.thy for examples.
+"fixrec_simp" attribute. The "fixrec_simp" method is intended as a
+replacement for "fixpat"; see src/HOLCF/ex/Fixrec_ex.thy for examples.
* The pattern-match compiler in 'fixrec' can now handle constructors
with HOL function types. Pattern-match combinators for the Pair
@@ -280,13 +277,13 @@
* The constant "sq_le" (with infix syntax "<<" or "\<sqsubseteq>") has
been renamed to "below". The name "below" now replaces "less" in many
-theorem names. (Legacy theorem names using "less" are still
-supported as well.)
+theorem names. (Legacy theorem names using "less" are still supported
+as well.)
* The 'fixrec' package now supports "bottom patterns". Bottom
patterns can be used to generate strictness rules, or to make
functions more strict (much like the bang-patterns supported by the
-Glasgow Haskell Compiler). See HOLCF/ex/Fixrec_ex.thy for examples.
+Glasgow Haskell Compiler). See src/HOLCF/ex/Fixrec_ex.thy for examples.
*** ML ***
@@ -296,9 +293,6 @@
to be pure, but the old TheoryDataFun for mutable data (with explicit
copy operation) is still available for some time.
-* Removed some old-style infix operations using polymorphic equality.
-INCOMPATIBILITY.
-
* Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML)
provides a high-level programming interface to synchronized state
variables with atomic update. This works via pure function
@@ -330,8 +324,11 @@
* Renamed NamedThmsFun to Named_Thms. INCOMPATIBILITY.
+* Renamed several structures FooBar to Foo_Bar. Occasional,
+INCOMPATIBILITY.
+
* Eliminated old Attrib.add_attributes, Method.add_methods and related
-cominators for "args". INCOMPATIBILITY, need to use simplified
+combinators for "args". INCOMPATIBILITY, need to use simplified
Attrib/Method.setup introduced in Isabelle2009.
* Proper context for simpset_of, claset_of, clasimpset_of. May fall
@@ -347,29 +344,30 @@
Syntax.pretty_typ/term directly, preferably with proper context
instead of global theory.
-* Operations of structure Skip_Proof (formerly SkipProof) no longer
-require quick_and_dirty mode, which avoids critical setmp.
+* Operations of structure Skip_Proof no longer require quick_and_dirty
+mode, which avoids critical setmp.
*** System ***
+* Further fine tuning of parallel proof checking, scales up to 8 cores
+(max. speedup factor 5.0). See also Goal.parallel_proofs in ML and
+usedir option -q.
+
* Support for additional "Isabelle components" via etc/components, see
also the system manual.
* The isabelle makeall tool now operates on all components with
IsaMakefile, not just hardwired "logics".
-* New component "isabelle wwwfind [start|stop|status] [HEAP]"
-Provides web interface for find_theorems on HEAP. Depends on lighttpd
-webserver being installed. Currently supported on Linux only.
+* Removed "compress" option from isabelle-process and isabelle usedir;
+this is always enabled.
* Discontinued support for Poly/ML 4.x versions.
-* Removed "compress" option from isabelle-process and isabelle usedir;
-this is always enabled.
-
-* More fine-grained control of proof parallelism, cf.
-Goal.parallel_proofs in ML and usedir option -q LEVEL.
+* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
+on a given logic image. This requires the lighttpd webserver and is
+currently supported on Linux only.