# HG changeset patch # User wenzelm # Date 1258895598 -3600 # Node ID efa1b89c79e09da80ae98bb4e2f45c0584395148 # Parent 6508d0e8bb19c133fba5a993d48092fff31ca117 misc tuning and updates for official release; diff -r 6508d0e8bb19 -r efa1b89c79e0 ANNOUNCE --- a/ANNOUNCE Sat Nov 21 20:44:16 2009 +0100 +++ b/ANNOUNCE Sun Nov 22 14:13:18 2009 +0100 @@ -1,40 +1,16 @@ -Subject: Announcing Isabelle2009 +Subject: Announcing Isabelle2009-1 To: isabelle-users@cl.cam.ac.uk -Isabelle2009 is now available. +Isabelle2009-1 is now available. -This release significantly improves upon Isabelle2008, see the NEWS +This release improves upon Isabelle2009 in many ways, see the NEWS file in the distribution for more details. Some important changes are: -* Complete re-implementation of locales, with proper support for local -syntax, and more general locale expressions. - -* New 'find_consts' and 'find_theorems' facilities, together with -"auto solve" feature of toplevel goal statements. - -* HOL: reorganization of main logic images. - -* HOL: improved implementation of Sledgehammer, based on generic ATP -manager; support for remote ATPs. - -* HOL: numerous library improvements. - -* Updated and extended versions of main reference manuals. - -* Simplified arrangement of Isabelle startup scripts and settings -directory. - -* Simplified programming interfaces for all Isar language elements. - -* General high-level support for concurrent ML programming. - -* Parallel proof checking within Isar theories. - -* Haskabelle importer from Haskell source files to Isar theories. +* FIXME -You may get Isabelle2009 from the following mirror sites: +You may get Isabelle2009-1 from the following mirror sites: Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Munich (Germany) http://isabelle.in.tum.de/ diff -r 6508d0e8bb19 -r efa1b89c79e0 CONTRIBUTORS --- a/CONTRIBUTORS Sat Nov 21 20:44:16 2009 +0100 +++ b/CONTRIBUTORS Sun Nov 22 14:13:18 2009 +0100 @@ -4,23 +4,24 @@ distribution. -Contributions to this Isabelle version --------------------------------------- +Contributions to Isabelle2009-1 +------------------------------- * November 2009: Robert Himmelmann, TUM Derivation and Brouwer's fixpoint theorem in Multivariate Analysis -* November 2009: Stefan Berghofer, Lukas Bulwahn, TUM - A tabled implementation of the reflexive transitive closure +* November 2009: Stefan Berghofer and Lukas Bulwahn, TUM + A tabled implementation of the reflexive transitive closure. * November 2009: Lukas Bulwahn, TUM - Predicate Compiler: a compiler for inductive predicates to equational specfications + Predicate Compiler: a compiler for inductive predicates to + equational specfications. * November 2009: Sascha Boehme, TUM - HOL-Boogie: an interactive prover back-end for Boogie and VCC + HOL-Boogie: an interactive prover back-end for Boogie and VCC. * October 2009: Jasmin Blanchette, TUM - Nitpick: yet another counterexample generator for Isabelle/HOL + Nitpick: yet another counterexample generator for Isabelle/HOL. * October 2009: Sascha Boehme, TUM Extension of SMT method: proof-reconstruction for the SMT solver Z3. diff -r 6508d0e8bb19 -r efa1b89c79e0 NEWS --- 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 "\") 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. diff -r 6508d0e8bb19 -r efa1b89c79e0 README --- a/README Sat Nov 21 20:44:16 2009 +0100 +++ b/README Sun Nov 22 14:13:18 2009 +0100 @@ -11,11 +11,11 @@ Isabelle requires a regular Unix platform (e.g. GNU Linux) with the following additional software: - * A full Standard ML Compiler (works best with Poly/ML 5.2.1). + + * A full Standard ML Compiler (works best with Poly/ML 5.3.0). * The GNU bash shell (version 3.x or 2.x). * Perl (version 5.x). - * GNU Emacs (version 21, 22, 23) or XEmacs (version 21.4.x) - -- for the Proof General interface. + * GNU Emacs (version 22 or 23) -- for the Proof General interface. * A complete LaTeX installation -- for document preparation. Installation