# HG changeset patch # User wenzelm # Date 1356955717 -3600 # Node ID c02e6a75aa3f9c7ee048386581e15e2612c09a26 # Parent cb8f93361e865f3cc99d50bc78746ed33403de47 misc tuning for release; diff -r cb8f93361e86 -r c02e6a75aa3f NEWS --- a/NEWS Mon Dec 31 12:25:11 2012 +0100 +++ b/NEWS Mon Dec 31 13:08:37 2012 +0100 @@ -102,17 +102,12 @@ *** Pure *** -* Dropped legacy antiquotations "term_style" and "thm_style", since -styles may be given as arguments to "term" and "thm" already. Dropped -legacy styles "prem1" .. "prem19". INCOMPATIBILITY. - * Code generation for Haskell: restrict unqualified imports from Haskell Prelude to a small set of fundamental operations. -* Command "export_code": relative file names are interpreted -relatively to master directory of current theory rather than -the rather arbitrary current working directory. -INCOMPATIBILITY. +* Command 'export_code': relative file names are interpreted +relatively to master directory of current theory rather than the +rather arbitrary current working directory. INCOMPATIBILITY. * Discontinued obsolete attribute "COMP". Potential INCOMPATIBILITY, use regular rule composition via "OF" / "THEN", or explicit proof @@ -129,11 +124,34 @@ *** HOL *** -* Removed constant "chars". Prefer "Enum.enum" on type "char" -directly. INCOMPATIBILITY. - -* Moved operation product, sublists and n_lists from Enum.thy -to List.thy. INCOMPATIBILITY. +* Sledgehammer: + + - Added MaSh relevance filter based on machine-learning; see the + Sledgehammer manual for details. + - Polished Isar proofs generated with "isar_proofs" option. + - Rationalized type encodings ("type_enc" option). + - Renamed "kill_provers" subcommand to "kill". + - Renamed options: + isar_proof ~> isar_proofs + isar_shrink_factor ~> isar_shrink + max_relevant ~> max_facts + relevance_thresholds ~> fact_thresholds + +* Quickcheck: added an optimisation for equality premises. It is +switched on by default, and can be switched off by setting the +configuration quickcheck_optimise_equality to false. + +* Simproc "finite_Collect" rewrites set comprehensions into pointfree +expressions. + +* Preprocessing of the code generator rewrites set comprehensions into +pointfree expressions. + +* The SMT solver Z3 has now by default a restricted set of directly +supported features. For the full set of features (div/mod, nonlinear +arithmetic, datatypes/records) with potential proof reconstruction +failures, enable the configuration option "z3_with_extensions". Minor +INCOMPATIBILITY. * Simplified 'typedef' specifications: historical options for implicit set definition and alternative name have been discontinued. The @@ -141,51 +159,84 @@ written just "typedef t = A". INCOMPATIBILITY, need to adapt theories accordingly. -* Theory "Library/Multiset": - - - Renamed constants - fold_mset ~> Multiset.fold -- for coherence with other fold combinators - - - Renamed facts - fold_mset_commute ~> fold_mset_comm -- for coherence with fold_comm - -INCOMPATIBILITY. +* Removed constant "chars"; prefer "Enum.enum" on type "char" +directly. INCOMPATIBILITY. + +* Moved operation product, sublists and n_lists from theory Enum to +List. INCOMPATIBILITY. * Theorem UN_o generalized to SUP_comp. INCOMPATIBILITY. * Class "comm_monoid_diff" formalises properties of bounded subtraction, with natural numbers and multisets as typical instances. -* Theory "Library/Option_ord" provides instantiation of option type -to lattice type classes. - -* New combinator "Option.these" with type "'a option set => 'a set". - -* Renamed theory Library/List_Prefix to Library/Sublist. -INCOMPATIBILITY. Related changes are: - - - Renamed constants: +* Added combinator "Option.these" with type "'a option set => 'a set". + +* Theory "Transitive_Closure": renamed lemmas + + reflcl_tranclp -> reflclp_tranclp + rtranclp_reflcl -> rtranclp_reflclp + +INCOMPATIBILITY. + +* Theory "Rings": renamed lemmas (in class semiring) + + left_distrib ~> distrib_right + right_distrib ~> distrib_left + +INCOMPATIBILITY. + +* Generalized the definition of limits: + + - Introduced the predicate filterlim (LIM x F. f x :> G) which + expresses that when the input values x converge to F then the + output f x converges to G. + + - Added filters for convergence to positive (at_top) and negative + infinity (at_bot). + + - Moved infinity in the norm (at_infinity) from + Multivariate_Analysis to Complex_Main. + + - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :> + at_top". + +INCOMPATIBILITY. + +* Theory "Library/Option_ord" provides instantiation of option type to +lattice type classes. + +* Theory "Library/Multiset": renamed + + constant fold_mset ~> Multiset.fold + fact fold_mset_commute ~> fold_mset_comm + +INCOMPATIBILITY. + +* Renamed theory Library/List_Prefix to Library/Sublist, with related +changes as follows. + + - Renamed constants (and related lemmas) prefix ~> prefixeq strict_prefix ~> prefix - Renamed lemmas accordingly, INCOMPATIBILITY. - - - Replaced constant "postfix" by "suffixeq" with swapped argument order - (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped old infix - syntax "xs >>= ys"; use "suffixeq ys xs" instead. Renamed lemmas - accordingly. INCOMPATIBILITY. - - - New constant "list_hembeq" for homeomorphic embedding on lists. New - abbreviation "sublisteq" for special case "list_hembeq (op =)". - - - Library/Sublist does no longer provide "order" and "bot" type class - instances for the prefix order (merely corresponding locale - interpretations). The type class instances are to be found in - Library/Prefix_Order. INCOMPATIBILITY. - - - The sublist relation from Library/Sublist_Order is now based on - "Sublist.sublisteq". Replaced lemmas: + - Replaced constant "postfix" by "suffixeq" with swapped argument + order (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped + old infix syntax "xs >>= ys"; use "suffixeq ys xs" instead. + Renamed lemmas accordingly. + + - Added constant "list_hembeq" for homeomorphic embedding on + lists. Added abbreviation "sublisteq" for special case + "list_hembeq (op =)". + + - Theory Library/Sublist no longer provides "order" and "bot" type + class instances for the prefix order (merely corresponding locale + interpretations). The type class instances are now in theory + Library/Prefix_Order. + + - The sublist relation of theory Library/Sublist_Order is now based + on "Sublist.sublisteq". Renamed lemmas accordingly: le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff le_list_append_mono ~> Sublist.list_hembeq_append_mono @@ -204,148 +255,110 @@ less_eq_list.induct ~> less_eq_list_induct not_le_list_length ~> Sublist.not_sublisteq_length - INCOMPATIBILITY. - -* Further generalized the definition of limits: - - - Introduced the predicate filterlim (LIM x F. f x :> G) which expresses that - when the input values x converge to F then the output f x converges to G. - - - Added filters for convergence to positive (at_top) and negative infinity (at_bot). - Moved infinity in the norm (at_infinity) from Multivariate_Analysis to Complex_Main. - - - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :> at_top". - INCOMPATIBILITY - -* HOL/Transitive_Closure: renamed lemmas - reflcl_tranclp -> reflclp_tranclp - rtranclp_reflcl -> rtranclp_reflclp - -* HOL/Rings: renamed lemmas - -left_distrib ~> distrib_right -right_distrib ~> distrib_left - -in class semiring. INCOMPATIBILITY. - -* HOL/BNF: New (co)datatype package based on bounded natural -functors with support for mixed, nested recursion and interesting -non-free datatypes. - -* HOL/Cardinals: Theories of ordinals and cardinals -(supersedes the AFP entry "Ordinals_and_Cardinals"). - -* HOL/Multivariate_Analysis: - Replaced "basis :: 'a::euclidean_space => nat => real" and - "\\ :: (nat => real) => 'a::euclidean_space" on euclidean spaces by - using the inner product "_ \ _" with vectors from the Basis set. - "\\ i. f i" is replaced by "SUM i : Basis. f i *r i". - - With this change the following constants are also chanegd or removed: - - DIM('a) :: nat ~> card (Basis :: 'a set) (is an abbreviation) - a $$ i ~> inner a i (where i : Basis) - cart_base i removed - \, \' removed +INCOMPATIBILITY. + + +* New theory Library/Countable_Set. + +* Theory Library/Debug and Library/Parallel provide debugging and +parallel execution for code generated towards Isabelle/ML. + +* Theory Library/FuncSet: Extended support for Pi and extensional and +introduce the extensional dependent function space "PiE". Replaced +extensional_funcset by an abbreviation, and renamed lemmas from +extensional_funcset to PiE as follows: + + extensional_empty ~> PiE_empty + extensional_funcset_empty_domain ~> PiE_empty_domain + extensional_funcset_empty_range ~> PiE_empty_range + extensional_funcset_arb ~> PiE_arb + extensional_funcset_mem ~> PiE_mem + extensional_funcset_extend_domainI ~> PiE_fun_upd + extensional_funcset_restrict_domain ~> fun_upd_in_PiE + extensional_funcset_extend_domain_eq ~> PiE_insert_eq + card_extensional_funcset ~> card_PiE + finite_extensional_funcset ~> finite_PiE + +INCOMPATIBILITY. + +* Theory Library/FinFun: theory of almost everywhere constant +functions (supersedes the AFP entry "Code Generation for Functions as +Data"). + +* Theory Library/Phantom: generic phantom type to make a type +parameter appear in a constant's type. This alternative to adding +TYPE('a) as another parameter avoids unnecessary closures in generated +code. + +* Theory Library/RBT_Impl: efficient construction of red-black trees +from sorted associative lists. Merging two trees with rbt_union may +return a structurally different tree than before. Potential +INCOMPATIBILITY. + +* Theory Library/IArray: immutable arrays with code generation. + +* Theory Library/Finite_Lattice: theory of finite lattices. + +* HOL/Multivariate_Analysis: replaced + + "basis :: 'a::euclidean_space => nat => real" + "\\ :: (nat => real) => 'a::euclidean_space" + +on euclidean spaces by using the inner product "_ \ _" with +vectors from the Basis set: "\\ i. f i" is superseded by +"SUM i : Basis. f i * r i". + + With this change the following constants are also changed or removed: + + DIM('a) :: nat ~> card (Basis :: 'a set) (is an abbreviation) + a $$ i ~> inner a i (where i : Basis) + cart_base i removed + \, \' removed Theorems about these constants where removed. Renamed lemmas: - component_le_norm ~> Basis_le_norm - euclidean_eq ~> euclidean_eq_iff - differential_zero_maxmin_component ~> differential_zero_maxmin_cart - euclidean_simps ~> inner_simps - independent_basis ~> independent_Basis - span_basis ~> span_Basis - in_span_basis ~> in_span_Basis - norm_bound_component_le ~> norm_boound_Basis_le - norm_bound_component_lt ~> norm_boound_Basis_lt - component_le_infnorm ~> Basis_le_infnorm - - INCOMPATIBILITY. + component_le_norm ~> Basis_le_norm + euclidean_eq ~> euclidean_eq_iff + differential_zero_maxmin_component ~> differential_zero_maxmin_cart + euclidean_simps ~> inner_simps + independent_basis ~> independent_Basis + span_basis ~> span_Basis + in_span_basis ~> in_span_Basis + norm_bound_component_le ~> norm_boound_Basis_le + norm_bound_component_lt ~> norm_boound_Basis_lt + component_le_infnorm ~> Basis_le_infnorm + +INCOMPATIBILITY. * HOL/Probability: - - Add simproc "measurable" to automatically prove measurability - - - Add induction rules for sigma sets with disjoint union (sigma_sets_induct_disjoint) - and for Borel-measurable functions (borel_measurable_induct). - - - The Daniell-Kolmogorov theorem (the existence the limit of a projective family) - -* Library/Countable_Set.thy: Theory of countable sets. - -* Library/Debug.thy and Library/Parallel.thy: debugging and parallel -execution for code generated towards Isabelle/ML. - -* Library/FuncSet.thy: Extended support for Pi and extensional and introduce the -extensional dependent function space "PiE". Replaces extensional_funcset by an -abbreviation, rename a couple of lemmas from extensional_funcset to PiE: - - extensional_empty ~> PiE_empty - extensional_funcset_empty_domain ~> PiE_empty_domain - extensional_funcset_empty_range ~> PiE_empty_range - extensional_funcset_arb ~> PiE_arb - extensional_funcset_mem > PiE_mem - extensional_funcset_extend_domainI ~> PiE_fun_upd - extensional_funcset_restrict_domain ~> fun_upd_in_PiE - extensional_funcset_extend_domain_eq ~> PiE_insert_eq - card_extensional_funcset ~> card_PiE - finite_extensional_funcset ~> finite_PiE - - INCOMPATIBILITY. - -* Library/FinFun.thy: theory of almost everywhere constant functions -(supersedes the AFP entry "Code Generation for Functions as Data"). - -* Library/Phantom.thy: generic phantom type to make a type parameter -appear in a constant's type. This alternative to adding TYPE('a) as -another parameter avoids unnecessary closures in generated code. - -* Library/RBT_Impl.thy: efficient construction of red-black trees -from sorted associative lists. Merging two trees with rbt_union may -return a structurally different tree than before. MINOR INCOMPATIBILITY. - -* Library/IArray.thy: immutable arrays with code generation. - -* Library/Finite_Lattice.thy: theory of finite lattices - -* Simproc "finite_Collect" rewrites set comprehensions into pointfree -expressions. - -* Preprocessing of the code generator rewrites set comprehensions into -pointfree expressions. - -* Quickcheck: - - - added an optimisation for equality premises. - It is switched on by default, and can be switched off by setting - the configuration quickcheck_optimise_equality to false. - -* The SMT solver Z3 has now by default a restricted set of directly -supported features. For the full set of features (div/mod, nonlinear -arithmetic, datatypes/records) with potential proof reconstruction -failures, enable the configuration option "z3_with_extensions". -Minor INCOMPATIBILITY. - -* Sledgehammer: - - - Added MaSh relevance filter based on machine-learning; see the - Sledgehammer manual for details. - - Polished Isar proofs generated with "isar_proofs" option. - - Rationalized type encodings ("type_enc" option). - - Renamed "kill_provers" subcommand to "kill". - - Renamed options: - isar_proof ~> isar_proofs - isar_shrink_factor ~> isar_shrink - max_relevant ~> max_facts - relevance_thresholds ~> fact_thresholds + + - Added simproc "measurable" to automatically prove measurability. + + - Added induction rules for sigma sets with disjoint union + (sigma_sets_induct_disjoint) and for Borel-measurable functions + (borel_measurable_induct). + + - Added the Daniell-Kolmogorov theorem (the existence the limit of a + projective family). + +* HOL/Cardinals: Theories of ordinals and cardinals (supersedes the +AFP entry "Ordinals_and_Cardinals"). + +* HOL/BNF: New (co)datatype package based on bounded natural functors +with support for mixed, nested recursion and interesting non-free +datatypes. *** Document preparation *** -* Default for \ is now based on eurosym package, instead of -slightly exotic babel/greek. +* Dropped legacy antiquotations "term_style" and "thm_style", since +styles may be given as arguments to "term" and "thm" already. +Discontinued legacy styles "prem1" .. "prem19". + +* Default LaTeX rendering for \ is now based on eurosym package, +instead of slightly exotic babel/greek. * Document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists, instead of the common @@ -357,6 +370,10 @@ *** ML *** +* The default limit for maximum number of worker threads is now 8, +instead of 4, in correspondence to capabilities of contemporary +hardware and Poly/ML runtime system. + * Type Seq.results and related operations support embedded error messages within lazy enumerations, and thus allow to provide informative errors in the absence of any usable results. @@ -368,16 +385,6 @@ *** System *** -* The default limit for maximum number of worker threads is now 8, -instead of 4. - -* The ML system is configured as regular component, and no longer -picked up from some surrounding directory. Potential INCOMPATIBILITY -for home-made configurations. - -* The "isabelle logo" tool produces EPS and PDF format simultaneously. -Minor INCOMPATIBILITY in command-line options. - * Advanced support for Isabelle sessions and build management, see "system" manual for the chapter of that name, especially the "isabelle build" tool and its examples. INCOMPATIBILITY, isabelle usedir / @@ -403,12 +410,22 @@ with "isabelle build", similar to former "isabelle mkdir" for "isabelle usedir". +* The "isabelle logo" tool produces EPS and PDF format simultaneously. +Minor INCOMPATIBILITY in command-line options. + +* The "isabelle install" tool has now a simpler command-line. Minor +INCOMPATIBILITY. + * The "isabelle components" tool helps to resolve add-on components that are not bundled, or referenced from a bare-bones repository version of Isabelle. -* The "isabelle install" tool has now a simpler command-line. Minor -INCOMPATIBILITY. +* Settings variable ISABELLE_PLATFORM_FAMILY refers to the general +platform family: "linux", "macos", "windows". + +* The ML system is configured as regular component, and no longer +picked up from some surrounding directory. Potential INCOMPATIBILITY +for home-made settings. * Discontinued support for Poly/ML 5.2.1, which was the last version without exception positions and advanced ML compiler/toplevel @@ -420,8 +437,6 @@ settings manually, or use a Proof General version that has been bundled as Isabelle component. -* Settings variable ISABELLE_PLATFORM_FAMILY refers to the general -platform family: "linux", "macos", "windows". New in Isabelle2012 (May 2012)