# HG changeset patch # User wenzelm # Date 1477389338 -7200 # Node ID ad2c5f37f6590e1d261d0ec32298af95500e8534 # Parent 6273d4c8325be9e28b18c495f5e5f052e479ed07 misc tuning for release; diff -r 6273d4c8325b -r ad2c5f37f659 NEWS --- a/NEWS Mon Oct 24 22:42:07 2016 +0200 +++ b/NEWS Tue Oct 25 11:55:38 2016 +0200 @@ -9,6 +9,15 @@ *** General *** +* Splitter in proof methods "simp", "auto" and friends: + - The syntax "split add" has been discontinued, use plain "split", + INCOMPATIBILITY. + - For situations with many conditional or case expressions, there is + an alternative splitting strategy that can be much faster. It is + selected by writing "split!" instead of "split". It applies safe + introduction and elimination rules after each split rule. As a + result the subgoal may be split into several subgoals. + * Command 'bundle' provides a local theory target to define a bundle from the body of specification commands (such as 'declare', 'declaration', 'notation', 'lemmas', 'lemma'). For example: @@ -51,21 +60,38 @@ instances) are generated into companion object of corresponding type class, to resolve some situations where ambiguities may occur. -* Splitter in simp, auto and friends: - - The syntax "split add" has been discontinued, use plain "split", - INCOMPATIBILITY. - - For situations with many conditional or case expressions, there is - an alternative splitting strategy that can be much faster. It is - selected by writing "split!" instead of "split". It applies safe - introduction and elimination rules after each split rule. As a - result the subgoal may be split into several subgoals. - -* Solve direct: option 'solve_direct_strict_warnings' gives explicit - warnings for lemma statements with trivial proofs. +* Solve direct: option "solve_direct_strict_warnings" gives explicit +warnings for lemma statements with trivial proofs. *** Prover IDE -- Isabelle/Scala/jEdit *** +* Syntactic indentation according to Isabelle outer syntax. Action +"indent-lines" (shortcut C+i) indents the current line according to +command keywords and some command substructure. Action +"isabelle.newline" (shortcut ENTER) indents the old and the new line +according to command keywords only; see also option +"jedit_indent_newline". + +* Semantic indentation for unstructured proof scripts ('apply' etc.) via +number of subgoals. This requires information of ongoing document +processing and may thus lag behind, when the user is editing too +quickly; see also option "jedit_script_indent" and +"jedit_script_indent_limit". + +* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed' +are treated as delimiters for fold structure; 'begin' and 'end' +structure of theory specifications is treated as well. + +* Command 'proof' provides information about proof outline with cases, +e.g. for proof methods "cases", "induct", "goal_cases". + +* Completion templates for commands involving "begin ... end" blocks, +e.g. 'context', 'notepad'. + +* Sidekick parser "isabelle-context" shows nesting of context blocks +according to 'begin' and 'end' structure. + * Highlighting of entity def/ref positions wrt. cursor. * Action "isabelle.select-entity" (shortcut CS+ENTER) selects all @@ -104,39 +130,6 @@ tree structure of section headings: this special comment format is described in "implementation" chapter 0, e.g. (*** section ***). -* Sidekick parser "isabelle-context" shows nesting of context blocks -according to 'begin' and 'end' structure. - -* Syntactic indentation according to Isabelle outer syntax. Action -"indent-lines" (shortcut C+i) indents the current line according to -command keywords and some command substructure. Action -"isabelle.newline" (shortcut ENTER) indents the old and the new line -according to command keywords only; see also option -"jedit_indent_newline". - -* Semantic indentation for unstructured proof scripts ('apply' etc.) via -number of subgoals. This requires information of ongoing document -processing and may thus lag behind, when the user is editing too -quickly; see also option "jedit_script_indent" and -"jedit_script_indent_limit". - -* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed' -are treated as delimiters for fold structure; 'begin' and 'end' -structure of theory specifications is treated as well. - -* Action "isabelle.keymap-merge" asks the user to resolve pending -Isabelle keymap changes that are in conflict with the current jEdit -keymap; non-conflicting changes are always applied implicitly. This -action is automatically invoked on Isabelle/jEdit startup and thus -increases chances that users see new keyboard shortcuts when re-using -old keymaps. - -* Command 'proof' provides information about proof outline with cases, -e.g. for proof methods "cases", "induct", "goal_cases". - -* Completion templates for commands involving "begin ... end" blocks, -e.g. 'context', 'notepad'. - * Additional abbreviations for syntactic completion may be specified within the theory header as 'abbrevs'. The theory syntax for 'keywords' has been simplified accordingly: optional abbrevs need to go into the @@ -146,6 +139,13 @@ $ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor INCOMPATIBILITY, use 'abbrevs' within theory header instead. +* Action "isabelle.keymap-merge" asks the user to resolve pending +Isabelle keymap changes that are in conflict with the current jEdit +keymap; non-conflicting changes are always applied implicitly. This +action is automatically invoked on Isabelle/jEdit startup and thus +increases chances that users see new keyboard shortcuts when re-using +old keymaps. + * ML and document antiquotations for file-systems paths are more uniform and diverse: @@ -249,49 +249,6 @@ *** HOL *** -* Ported remaining theories of Old_Number_Theory and removed Old_Number_Theory. - -* Sligthly more standardized theorem names: - sgn_times ~> sgn_mult - sgn_mult' ~> Real_Vector_Spaces.sgn_mult - divide_zero_left ~> div_0 - zero_mod_left ~> mod_0 - divide_zero ~> div_by_0 - divide_1 ~> div_by_1 - nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left - div_mult_self1_is_id ~> nonzero_mult_div_cancel_left - nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right - div_mult_self2_is_id ~> nonzero_mult_div_cancel_right - is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left - is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right - mod_div_equality ~> div_mult_mod_eq - mod_div_equality2 ~> mult_div_mod_eq - mod_div_equality3 ~> mod_div_mult_eq - mod_div_equality4 ~> mod_mult_div_eq - minus_div_eq_mod ~> minus_div_mult_eq_mod - minus_div_eq_mod2 ~> minus_mult_div_eq_mod - minus_mod_eq_div ~> minus_mod_eq_div_mult - minus_mod_eq_div2 ~> minus_mod_eq_mult_div - div_mod_equality' ~> minus_mod_eq_div_mult [symmetric] - mod_div_equality' ~> minus_div_mult_eq_mod [symmetric] - zmod_zdiv_equality ~> mult_div_mod_eq [symmetric] - zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric] - Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] - mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] - zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric] - div_1 ~> div_by_Suc_0 - mod_1 ~> mod_by_Suc_0 -INCOMPATIBILITY. - -* Renamed constants "setsum" ~> "sum" and "setprod" ~> "prod". - Corresponding renaming of theorems. - -* New type class "idom_abs_sgn" specifies algebraic properties -of sign and absolute value functions. Type class "sgn_if" has -disappeared. Slight INCOMPATIBILITY. - -* Dedicated syntax LENGTH('a) for length of types. - * New proof method "argo" using the built-in Argo solver based on SMT technology. The method can be used to prove goals of quantifier-free propositional logic, goals based on a combination of quantifier-free @@ -299,6 +256,9 @@ quantifier-free propositional logic with linear real arithmetic including min/max/abs. See HOL/ex/Argo_Examples.thy for examples. +* The new "nunchaku" program integrates the Nunchaku model finder. The +tool is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details. + * Metis: The problem encoding has changed very slightly. This might break existing proofs. INCOMPATIBILITY. @@ -356,6 +316,53 @@ * Conventional syntax "%(). t" for unit abstractions. Slight syntactic INCOMPATIBILITY. +* Renamed constants and corresponding theorems: + + setsum ~> sum + setprod ~> prod + listsum ~> sum_list + listprod ~> prod_list + +INCOMPATIBILITY. + +* Sligthly more standardized theorem names: + sgn_times ~> sgn_mult + sgn_mult' ~> Real_Vector_Spaces.sgn_mult + divide_zero_left ~> div_0 + zero_mod_left ~> mod_0 + divide_zero ~> div_by_0 + divide_1 ~> div_by_1 + nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left + div_mult_self1_is_id ~> nonzero_mult_div_cancel_left + nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right + div_mult_self2_is_id ~> nonzero_mult_div_cancel_right + is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left + is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right + mod_div_equality ~> div_mult_mod_eq + mod_div_equality2 ~> mult_div_mod_eq + mod_div_equality3 ~> mod_div_mult_eq + mod_div_equality4 ~> mod_mult_div_eq + minus_div_eq_mod ~> minus_div_mult_eq_mod + minus_div_eq_mod2 ~> minus_mult_div_eq_mod + minus_mod_eq_div ~> minus_mod_eq_div_mult + minus_mod_eq_div2 ~> minus_mod_eq_mult_div + div_mod_equality' ~> minus_mod_eq_div_mult [symmetric] + mod_div_equality' ~> minus_div_mult_eq_mod [symmetric] + zmod_zdiv_equality ~> mult_div_mod_eq [symmetric] + zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric] + Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] + mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] + zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric] + div_1 ~> div_by_Suc_0 + mod_1 ~> mod_by_Suc_0 +INCOMPATIBILITY. + +* New type class "idom_abs_sgn" specifies algebraic properties +of sign and absolute value functions. Type class "sgn_if" has +disappeared. Slight INCOMPATIBILITY. + +* Dedicated syntax LENGTH('a) for length of types. + * Characters (type char) are modelled as finite algebraic type corresponding to {0..255}. @@ -406,14 +413,11 @@ * Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on explicitly provided auxiliary definitions for required type class -dictionaries rather than half-working magic. INCOMPATIBILITY, see -the tutorial on code generation for details. - -* Theory Set_Interval.thy: substantial new theorems on indexed sums -and products. - -* Theory List.thy: ranaming of listsum ~> sum_list, listprod ~> -prod_list, INCOMPATIBILITY. +dictionaries rather than half-working magic. INCOMPATIBILITY, see the +tutorial on code generation for details. + +* Theory Set_Interval: substantial new theorems on indexed sums and +products. * Locale bijection establishes convenient default simp rules such as "inv f (f a) = a" for total bijections. @@ -466,354 +470,6 @@ * Added class topological_monoid. -* HOL-Library: theory FinFun bundles "finfun_syntax" and -"no_finfun_syntax" allow to control optional syntax in local contexts; -this supersedes former theory FinFun_Syntax. INCOMPATIBILITY, e.g. use -"unbundle finfun_syntax" to imitate import of -"~~/src/HOL/Library/FinFun_Syntax". - -* HOL-Library: theory Multiset_Permutations (executably) defines the set of -permutations of a given set or multiset, i.e. the set of all lists that -contain every element of the carrier (multi-)set exactly once. - -* HOL-Library: multiset membership is now expressed using set_mset -rather than count. - - - Expressions "count M a > 0" and similar simplify to membership - by default. - - - Converting between "count M a = 0" and non-membership happens using - equations count_eq_zero_iff and not_in_iff. - - - Rules count_inI and in_countE obtain facts of the form - "count M a = n" from membership. - - - Rules count_in_diffI and in_diff_countE obtain facts of the form - "count M a = n + count N a" from membership on difference sets. - -INCOMPATIBILITY. - -* HOL-Library: theory LaTeXsugar uses new-style "dummy_pats" for -displaying equations in functional programming style --- variables -present on the left-hand but not on the righ-hand side are replaced by -underscores. - -* HOL-Library: theory Combinator_PER provides combinator to build -partial equivalence relations from a predicate and an equivalence -relation. - -* HOL-Library: theory Perm provides basic facts about almost everywhere -fix bijections. - -* HOL-Library: theory Normalized_Fraction allows viewing an element of a -field of fractions as a normalized fraction (i.e. a pair of numerator -and denominator such that the two are coprime and the denominator is -normalized wrt. unit factors). - -* Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis. - -* Session HOL-Multivariate_Analysis has been renamed to HOL-Analysis. - -* HOL-Analysis: measure theory has been moved here from HOL-Probability. -When importing HOL-Analysis some theorems need additional name spaces -prefixes due to name clashes. INCOMPATIBILITY. - -* HOL-Analysis: more complex analysis including Cauchy's inequality, -Liouville theorem, open mapping theorem, maximum modulus principle, -Residue theorem, Schwarz Lemma. - -* HOL-Analysis: Theory of polyhedra: faces, extreme points, polytopes, -and the Krein–Milman Minkowski theorem. - -* HOL-Analysis: Numerous results ported from the HOL Light libraries: -homeomorphisms, continuous function extensions, invariance of domain. - -* HOL-Probability: the type of emeasure and nn_integral was changed from -ereal to ennreal, INCOMPATIBILITY. - - emeasure :: 'a measure \ 'a set \ ennreal - nn_integral :: 'a measure \ ('a \ ennreal) \ ennreal - -* HOL-Probability: Code generation and QuickCheck for Probability Mass -Functions. - -* HOL-Probability: theory Random_Permutations contains some theory about -choosing a permutation of a set uniformly at random and folding over a -list in random order. - -* HOL-Probability: theory SPMF formalises discrete subprobability -distributions. - -* HOL-Number_Theory: algebraic foundation for primes: Generalisation of -predicate "prime" and introduction of predicates "prime_elem", -"irreducible", a "prime_factorization" function, and the -"factorial_ring" typeclass with instance proofs for nat, int, poly. Some -theorems now have different names, most notably "prime_def" is now -"prime_nat_iff". INCOMPATIBILITY. - -* HOL-Library: the names of multiset theorems have been normalised to -distinguish which ordering the theorems are about - - mset_less_eqI ~> mset_subset_eqI - mset_less_insertD ~> mset_subset_insertD - mset_less_eq_count ~> mset_subset_eq_count - mset_less_diff_self ~> mset_subset_diff_self - mset_le_exists_conv ~> mset_subset_eq_exists_conv - mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel - mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel - mset_le_mono_add ~> mset_subset_eq_mono_add - mset_le_add_left ~> mset_subset_eq_add_left - mset_le_add_right ~> mset_subset_eq_add_right - mset_le_single ~> mset_subset_eq_single - mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute - diff_le_self ~> diff_subset_eq_self - mset_leD ~> mset_subset_eqD - mset_lessD ~> mset_subsetD - mset_le_insertD ~> mset_subset_eq_insertD - mset_less_of_empty ~> mset_subset_of_empty - mset_less_size ~> mset_subset_size - wf_less_mset_rel ~> wf_subset_mset_rel - count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq - mset_remdups_le ~> mset_remdups_subset_eq - ms_lesseq_impl ~> subset_eq_mset_impl - -Some functions have been renamed: - ms_lesseq_impl -> subset_eq_mset_impl - -* HOL-Library: multisets are now ordered with the multiset ordering - #\# ~> \ - #\# ~> < - le_multiset ~> less_eq_multiset - less_multiset ~> le_multiset -INCOMPATIBILITY. - -* HOL-Library: the prefix multiset_order has been discontinued: the -theorems can be directly accessed. As a consequence, the lemmas -"order_multiset" and "linorder_multiset" have been discontinued, and the -interpretations "multiset_linorder" and "multiset_wellorder" have been -replaced by instantiations. INCOMPATIBILITY. - -* HOL-Library: some theorems about the multiset ordering have been -renamed: - - le_multiset_def ~> less_eq_multiset_def - less_multiset_def ~> le_multiset_def - less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset - mult_less_not_refl ~> mset_le_not_refl - mult_less_trans ~> mset_le_trans - mult_less_not_sym ~> mset_le_not_sym - mult_less_asym ~> mset_le_asym - mult_less_irrefl ~> mset_le_irrefl - union_less_mono2{,1,2} ~> union_le_mono2{,1,2} - - le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O - le_multiset_total ~> less_eq_multiset_total - less_multiset_right_total ~> subset_eq_imp_le_multiset - le_multiset_empty_left ~> less_eq_multiset_empty_left - le_multiset_empty_right ~> less_eq_multiset_empty_right - less_multiset_empty_right ~> le_multiset_empty_left - less_multiset_empty_left ~> le_multiset_empty_right - union_less_diff_plus ~> union_le_diff_plus - ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset - less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty - le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty -INCOMPATIBILITY. - -* HOL-Library: the lemma mset_map has now the attribute [simp]. -INCOMPATIBILITY. - -* HOL-Library: some theorems about multisets have been removed. -INCOMPATIBILITY, use the following replacements: - - le_multiset_plus_plus_left_iff ~> add_less_cancel_right - less_multiset_plus_plus_left_iff ~> add_less_cancel_right - le_multiset_plus_plus_right_iff ~> add_less_cancel_left - less_multiset_plus_plus_right_iff ~> add_less_cancel_left - add_eq_self_empty_iff ~> add_cancel_left_right - mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right - mset_less_add_bothsides ~> subset_mset.add_less_cancel_right - mset_le_add_bothsides ~> subset_mset.add_less_cancel_right - empty_inter ~> subset_mset.inf_bot_left - inter_empty ~> subset_mset.inf_bot_right - empty_sup ~> subset_mset.sup_bot_left - sup_empty ~> subset_mset.sup_bot_right - bdd_below_multiset ~> subset_mset.bdd_above_bot - subset_eq_empty ~> subset_mset.le_zero_eq - le_empty ~> subset_mset.le_zero_eq - mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero - mset_less_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero - -* HOL-Library: some typeclass constraints about multisets have been -reduced from ordered or linordered to preorder. Multisets have the -additional typeclasses order_bot, no_top, -ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add, -linordered_cancel_ab_semigroup_add, and -ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY. - -* HOL-Library: there are some new simplification rules about multisets, -the multiset ordering, and the subset ordering on multisets. -INCOMPATIBILITY. - -* HOL-Library: the subset ordering on multisets has now the -interpretations ordered_ab_semigroup_monoid_add_imp_le and -bounded_lattice_bot. INCOMPATIBILITY. - -* HOL-Library/Multiset: single has been removed in favor of add_mset -that roughly corresponds to Set.insert. Some theorems have removed or -changed: - - single_not_empty ~> add_mset_not_empty or empty_not_add_mset - fold_mset_insert ~> fold_mset_add_mset - image_mset_insert ~> image_mset_add_mset - union_single_eq_diff - multi_self_add_other_not_self - diff_single_eq_union -INCOMPATIBILITY. - -* HOL-Library/Multiset: some theorems have been changed to use add_mset -instead of single: - - mset_add - multi_self_add_other_not_self - diff_single_eq_union - union_single_eq_diff - union_single_eq_member - add_eq_conv_diff - insert_noteq_member - add_eq_conv_ex - multi_member_split - multiset_add_sub_el_shuffle - mset_subset_eq_insertD - mset_subset_insertD - insert_subset_eq_iff - insert_union_subset_iff - multi_psub_of_add_self - inter_add_left1 - inter_add_left2 - inter_add_right1 - inter_add_right2 - sup_union_left1 - sup_union_left2 - sup_union_right1 - sup_union_right2 - size_eq_Suc_imp_eq_union - multi_nonempty_split - mset_insort - mset_update - mult1I - less_add - mset_zip_take_Cons_drop_twice - rel_mset_Zero - msed_map_invL - msed_map_invR - msed_rel_invL - msed_rel_invR - le_multiset_right_total - multiset_induct - multiset_induct2_size - multiset_induct2 -INCOMPATIBILITY. - -* HOL-Library/Multiset. The definitions of some constants have changed -to use add_mset instead of adding a single element: - image_mset - mset - replicate_mset - mult1 - pred_mset - rel_mset' - mset_insort -INCOMPATIBILITY. - -* HOL-Library/Multiset. Due to the above changes, the attributes of some -multiset theorems have been changed: - insert_DiffM [] ~> [simp] - insert_DiffM2 [simp] ~> [] - diff_add_mset_swap [simp] - fold_mset_add_mset [simp] - diff_diff_add [simp] (for multisets only) - diff_cancel [simp] ~> [] - count_single [simp] ~> [] - set_mset_single [simp] ~> [] - size_multiset_single [simp] ~> [] - size_single [simp] ~> [] - image_mset_single [simp] ~> [] - mset_subset_eq_mono_add_right_cancel [simp] ~> [] - mset_subset_eq_mono_add_left_cancel [simp] ~> [] - fold_mset_single [simp] ~> [] - subset_eq_empty [simp] ~> [] - empty_sup [simp] ~> [] - sup_empty [simp] ~> [] - inter_empty [simp] ~> [] - empty_inter [simp] ~> [] -INCOMPATIBILITY. - -* HOL-Library/Multiset. The order of the variables in the second cases -of multiset_induct, multiset_induct2_size, multiset_induct2 has been -changed (e.g. Add A a ~> Add a A). INCOMPATIBILITY. - -* HOL-Library/Multiset. There is now a simplification procedure on -multisets. It mimics the behavior of the procedure on natural numbers. -INCOMPATIBILITY. - -* HOL-Library/Multiset. Renamed sums and products of multisets: - msetsum ~> sum_mset - msetprod ~> prod_mset - -* HOL-Library/Multiset. The notation for intersection and union of -multisets have been changed: - #\ ~> \# - #\ ~> \# -INCOMPATIBILITY. - -* HOL-Library/Multiset. The lemma one_step_implies_mult_aux on multisets -has been removed, use one_step_implies_mult instead. INCOMPATIBILITY. - -* The following theorems have been renamed: - setsum_left_distrib ~> setsum_distrib_right - setsum_right_distrib ~> setsum_distrib_left -INCOMPATIBILITY. - -* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. -INCOMPATIBILITY. - -* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional -comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` A)". - -* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. - -* The type class ordered_comm_monoid_add is now called -ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add -is introduced as the combination of ordered_ab_semigroup_add + -comm_monoid_add. INCOMPATIBILITY. - -* Introduced the type classes canonically_ordered_comm_monoid_add and -dioid. - -* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When -instantiating linordered_semiring_strict and ordered_ab_group_add, an -explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might -be required. INCOMPATIBILITY. - -* HOL-Library: theory Complete_Partial_Order2 provides reasoning support -for monotonicity and continuity in chain-complete partial orders and -about admissibility conditions for fixpoint inductions. - -* HOL-Library: theory Polynomial contains also derivation of polynomials -but not gcd/lcm on polynomials over fields. This has been moved to a -separate theory Library/Polynomial_GCD_euclidean.thy, to pave way for a -possible future different type class instantiation for polynomials over -factorial rings. INCOMPATIBILITY. - -* HOL-Library: theory Sublist.thy provides function "prefixes" with the -following renaming - - prefixeq -> prefix - prefix -> strict_prefix - suffixeq -> suffix - suffix -> strict_suffix - -Added theory of longest common prefixes. * Dropped various legacy fact bindings, whose replacements are often of a more general type also: @@ -910,15 +566,376 @@ * Renamed HOL/Quotient_Examples/FSet.thy to HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY. -* The "nunchaku" program integrates the Nunchaku model finder. The tool -is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details. +* Session HOL-Library: theory FinFun bundles "finfun_syntax" and +"no_finfun_syntax" allow to control optional syntax in local contexts; +this supersedes former theory FinFun_Syntax. INCOMPATIBILITY, e.g. use +"unbundle finfun_syntax" to imitate import of +"~~/src/HOL/Library/FinFun_Syntax". + +* Session HOL-Library: theory Multiset_Permutations (executably) defines +the set of permutations of a given set or multiset, i.e. the set of all +lists that contain every element of the carrier (multi-)set exactly +once. + +* Session HOL-Library: multiset membership is now expressed using +set_mset rather than count. + + - Expressions "count M a > 0" and similar simplify to membership + by default. + + - Converting between "count M a = 0" and non-membership happens using + equations count_eq_zero_iff and not_in_iff. + + - Rules count_inI and in_countE obtain facts of the form + "count M a = n" from membership. + + - Rules count_in_diffI and in_diff_countE obtain facts of the form + "count M a = n + count N a" from membership on difference sets. + +INCOMPATIBILITY. + +* Session HOL-Library: theory LaTeXsugar uses new-style "dummy_pats" for +displaying equations in functional programming style --- variables +present on the left-hand but not on the righ-hand side are replaced by +underscores. + +* Session HOL-Library: theory Combinator_PER provides combinator to +build partial equivalence relations from a predicate and an equivalence +relation. + +* Session HOL-Library: theory Perm provides basic facts about almost +everywhere fix bijections. + +* Session HOL-Library: theory Normalized_Fraction allows viewing an +element of a field of fractions as a normalized fraction (i.e. a pair of +numerator and denominator such that the two are coprime and the +denominator is normalized wrt. unit factors). + +* Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis. + +* Session HOL-Multivariate_Analysis has been renamed to HOL-Analysis. + +* Session HOL-Analysis: measure theory has been moved here from +HOL-Probability. When importing HOL-Analysis some theorems need +additional name spaces prefixes due to name clashes. INCOMPATIBILITY. + +* Session HOL-Analysis: more complex analysis including Cauchy's +inequality, Liouville theorem, open mapping theorem, maximum modulus +principle, Residue theorem, Schwarz Lemma. + +* Session HOL-Analysis: Theory of polyhedra: faces, extreme points, +polytopes, and the Krein–Milman Minkowski theorem. + +* Session HOL-Analysis: Numerous results ported from the HOL Light +libraries: homeomorphisms, continuous function extensions, invariance of +domain. + +* Session HOL-Probability: the type of emeasure and nn_integral was +changed from ereal to ennreal, INCOMPATIBILITY. + + emeasure :: 'a measure \ 'a set \ ennreal + nn_integral :: 'a measure \ ('a \ ennreal) \ ennreal + +* Session HOL-Probability: Code generation and QuickCheck for +Probability Mass Functions. + +* Session HOL-Probability: theory Random_Permutations contains some +theory about choosing a permutation of a set uniformly at random and +folding over a list in random order. + +* Session HOL-Probability: theory SPMF formalises discrete +subprobability distributions. + +* Session HOL-Number_Theory: algebraic foundation for primes: +Generalisation of predicate "prime" and introduction of predicates +"prime_elem", "irreducible", a "prime_factorization" function, and the +"factorial_ring" typeclass with instance proofs for nat, int, poly. Some +theorems now have different names, most notably "prime_def" is now +"prime_nat_iff". INCOMPATIBILITY. + +* Session Old_Number_Theory has been removed, after porting remaining +theories. + +* Session HOL-Library: the names of multiset theorems have been +normalised to distinguish which ordering the theorems are about + + mset_less_eqI ~> mset_subset_eqI + mset_less_insertD ~> mset_subset_insertD + mset_less_eq_count ~> mset_subset_eq_count + mset_less_diff_self ~> mset_subset_diff_self + mset_le_exists_conv ~> mset_subset_eq_exists_conv + mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel + mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel + mset_le_mono_add ~> mset_subset_eq_mono_add + mset_le_add_left ~> mset_subset_eq_add_left + mset_le_add_right ~> mset_subset_eq_add_right + mset_le_single ~> mset_subset_eq_single + mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute + diff_le_self ~> diff_subset_eq_self + mset_leD ~> mset_subset_eqD + mset_lessD ~> mset_subsetD + mset_le_insertD ~> mset_subset_eq_insertD + mset_less_of_empty ~> mset_subset_of_empty + mset_less_size ~> mset_subset_size + wf_less_mset_rel ~> wf_subset_mset_rel + count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq + mset_remdups_le ~> mset_remdups_subset_eq + ms_lesseq_impl ~> subset_eq_mset_impl + +Some functions have been renamed: + ms_lesseq_impl -> subset_eq_mset_impl + +* The following theorems have been renamed: + + setsum_left_distrib ~> setsum_distrib_right + setsum_right_distrib ~> setsum_distrib_left + +INCOMPATIBILITY. + +* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. +INCOMPATIBILITY. + +* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional +comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` +A)". + +* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. + +* The type class ordered_comm_monoid_add is now called +ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add +is introduced as the combination of ordered_ab_semigroup_add + +comm_monoid_add. INCOMPATIBILITY. + +* Introduced the type classes canonically_ordered_comm_monoid_add and +dioid. + +* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When +instantiating linordered_semiring_strict and ordered_ab_group_add, an +explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might +be required. INCOMPATIBILITY. + +* HOL-Library: multisets are now ordered with the multiset ordering + #\# ~> \ + #\# ~> < + le_multiset ~> less_eq_multiset + less_multiset ~> le_multiset +INCOMPATIBILITY. + +* Session HOL-Library: the prefix multiset_order has been discontinued: +the theorems can be directly accessed. As a consequence, the lemmas +"order_multiset" and "linorder_multiset" have been discontinued, and the +interpretations "multiset_linorder" and "multiset_wellorder" have been +replaced by instantiations. INCOMPATIBILITY. + +* Session HOL-Library: some theorems about the multiset ordering have +been renamed: + + le_multiset_def ~> less_eq_multiset_def + less_multiset_def ~> le_multiset_def + less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset + mult_less_not_refl ~> mset_le_not_refl + mult_less_trans ~> mset_le_trans + mult_less_not_sym ~> mset_le_not_sym + mult_less_asym ~> mset_le_asym + mult_less_irrefl ~> mset_le_irrefl + union_less_mono2{,1,2} ~> union_le_mono2{,1,2} + + le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O + le_multiset_total ~> less_eq_multiset_total + less_multiset_right_total ~> subset_eq_imp_le_multiset + le_multiset_empty_left ~> less_eq_multiset_empty_left + le_multiset_empty_right ~> less_eq_multiset_empty_right + less_multiset_empty_right ~> le_multiset_empty_left + less_multiset_empty_left ~> le_multiset_empty_right + union_less_diff_plus ~> union_le_diff_plus + ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset + less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty + le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty +INCOMPATIBILITY. + +* Session HOL-Library: the lemma mset_map has now the attribute [simp]. +INCOMPATIBILITY. + +* Session HOL-Library: some theorems about multisets have been removed. +INCOMPATIBILITY, use the following replacements: + + le_multiset_plus_plus_left_iff ~> add_less_cancel_right + less_multiset_plus_plus_left_iff ~> add_less_cancel_right + le_multiset_plus_plus_right_iff ~> add_less_cancel_left + less_multiset_plus_plus_right_iff ~> add_less_cancel_left + add_eq_self_empty_iff ~> add_cancel_left_right + mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right + mset_less_add_bothsides ~> subset_mset.add_less_cancel_right + mset_le_add_bothsides ~> subset_mset.add_less_cancel_right + empty_inter ~> subset_mset.inf_bot_left + inter_empty ~> subset_mset.inf_bot_right + empty_sup ~> subset_mset.sup_bot_left + sup_empty ~> subset_mset.sup_bot_right + bdd_below_multiset ~> subset_mset.bdd_above_bot + subset_eq_empty ~> subset_mset.le_zero_eq + le_empty ~> subset_mset.le_zero_eq + mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero + mset_less_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero + +* Session HOL-Library: some typeclass constraints about multisets have +been reduced from ordered or linordered to preorder. Multisets have the +additional typeclasses order_bot, no_top, +ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add, +linordered_cancel_ab_semigroup_add, and +ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY. + +* Session HOL-Library: there are some new simplification rules about +multisets, the multiset ordering, and the subset ordering on multisets. +INCOMPATIBILITY. + +* Session HOL-Library: the subset ordering on multisets has now the +interpretations ordered_ab_semigroup_monoid_add_imp_le and +bounded_lattice_bot. INCOMPATIBILITY. + +* Session HOL-Library, theory Multiset: single has been removed in favor +of add_mset that roughly corresponds to Set.insert. Some theorems have +removed or changed: + + single_not_empty ~> add_mset_not_empty or empty_not_add_mset + fold_mset_insert ~> fold_mset_add_mset + image_mset_insert ~> image_mset_add_mset + union_single_eq_diff + multi_self_add_other_not_self + diff_single_eq_union +INCOMPATIBILITY. + +* Session HOL-Library, theory Multiset: some theorems have been changed +to use add_mset instead of single: + + mset_add + multi_self_add_other_not_self + diff_single_eq_union + union_single_eq_diff + union_single_eq_member + add_eq_conv_diff + insert_noteq_member + add_eq_conv_ex + multi_member_split + multiset_add_sub_el_shuffle + mset_subset_eq_insertD + mset_subset_insertD + insert_subset_eq_iff + insert_union_subset_iff + multi_psub_of_add_self + inter_add_left1 + inter_add_left2 + inter_add_right1 + inter_add_right2 + sup_union_left1 + sup_union_left2 + sup_union_right1 + sup_union_right2 + size_eq_Suc_imp_eq_union + multi_nonempty_split + mset_insort + mset_update + mult1I + less_add + mset_zip_take_Cons_drop_twice + rel_mset_Zero + msed_map_invL + msed_map_invR + msed_rel_invL + msed_rel_invR + le_multiset_right_total + multiset_induct + multiset_induct2_size + multiset_induct2 +INCOMPATIBILITY. + +* Session HOL-Library, theory Multiset: the definitions of some +constants have changed to use add_mset instead of adding a single +element: + + image_mset + mset + replicate_mset + mult1 + pred_mset + rel_mset' + mset_insort + +INCOMPATIBILITY. + +* Session HOL-Library, theory Multiset: due to the above changes, the +attributes of some multiset theorems have been changed: + + insert_DiffM [] ~> [simp] + insert_DiffM2 [simp] ~> [] + diff_add_mset_swap [simp] + fold_mset_add_mset [simp] + diff_diff_add [simp] (for multisets only) + diff_cancel [simp] ~> [] + count_single [simp] ~> [] + set_mset_single [simp] ~> [] + size_multiset_single [simp] ~> [] + size_single [simp] ~> [] + image_mset_single [simp] ~> [] + mset_subset_eq_mono_add_right_cancel [simp] ~> [] + mset_subset_eq_mono_add_left_cancel [simp] ~> [] + fold_mset_single [simp] ~> [] + subset_eq_empty [simp] ~> [] + empty_sup [simp] ~> [] + sup_empty [simp] ~> [] + inter_empty [simp] ~> [] + empty_inter [simp] ~> [] +INCOMPATIBILITY. + +* Session HOL-Library, theory Multiset: The order of the variables in +the second cases of multiset_induct, multiset_induct2_size, +multiset_induct2 has been changed (e.g. Add A a ~> Add a A). +INCOMPATIBILITY. + +* Session HOL-Library, theory Multiset: there is now a simplification +procedure on multisets. It mimics the behavior of the procedure on +natural numbers. INCOMPATIBILITY. + +* Session HOL-Library, theory Multiset: renamed sums and products of +multisets: + + msetsum ~> sum_mset + msetprod ~> prod_mset + +* Session HOL-Library, theory Multiset: the notation for intersection +and union of multisets have been changed: + + #\ ~> \# + #\ ~> \# + +INCOMPATIBILITY. + +* Session HOL-Library, theory Multiset: the lemma +one_step_implies_mult_aux on multisets has been removed, use +one_step_implies_mult instead. INCOMPATIBILITY. + +* Session HOL-Library: theory Complete_Partial_Order2 provides reasoning +support for monotonicity and continuity in chain-complete partial orders +and about admissibility conditions for fixpoint inductions. + +* Session HOL-Library: theory Polynomial contains also derivation of +polynomials but not gcd/lcm on polynomials over fields. This has been +moved to a separate theory Library/Polynomial_GCD_euclidean.thy, to pave +way for a possible future different type class instantiation for +polynomials over factorial rings. INCOMPATIBILITY. + +* Session HOL-Library: theory Sublist provides function "prefixes" with +the following renaming + + prefixeq -> prefix + prefix -> strict_prefix + suffixeq -> suffix + suffix -> strict_suffix + +Added theory of longest common prefixes. *** ML *** -* ML antiquotation @{path} is superseded by @{file}, which ensures that -the argument is a plain file. Minor INCOMPATIBILITY. - * Integer.gcd and Integer.lcm use efficient operations from the Poly/ML library (notably for big integers). Subtle change of semantics: Integer.gcd and Integer.lcm both normalize the sign, results are never @@ -933,16 +950,19 @@ use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been superseded by General.Div. +* ML antiquotation @{path} is superseded by @{file}, which ensures that +the argument is a plain file. Minor INCOMPATIBILITY. + +* Antiquotation @{make_string} is available during Pure bootstrap -- +with approximative output quality. + +* Low-level ML system structures (like PolyML and RunCall) are no longer +exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY. + * The ML function "ML" provides easy access to run-time compilation. This is particularly useful for conditional compilation, without requiring separate files. -* Low-level ML system structures (like PolyML and RunCall) are no longer -exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY. - -* Antiquotation @{make_string} is available during Pure bootstrap -- -with approximative output quality. - * Option ML_exception_debugger controls detailed exception trace via the Poly/ML debugger. Relevant ML modules need to be compiled beforehand with ML_file_debug, or with ML_file and option ML_debugger enabled. Note @@ -972,31 +992,10 @@ *** System *** -* Isabelle/Scala: the SSH module supports ssh and sftp connections, for -remote command-execution and file-system access. This resembles -operations from module File and Isabelle_System to some extent. Note -that Path specifications need to be resolved remotely via -ssh.remote_path instead of File.standard_path: the implicit process -environment is different, Isabelle settings are not available remotely. - -* Isabelle/Scala: the Mercurial module supports repositories via the -regular hg command-line interface. The repositroy clone and working -directory may reside on a local or remote file-system (via ssh -connection). - -* Many Isabelle tools that require a Java runtime system refer to the -settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64, -depending on the underlying platform. The settings for "isabelle build" -ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been -discontinued. Potential INCOMPATIBILITY. - -* The Isabelle system environment always ensures that the main -executables are found within the shell search $PATH: "isabelle" and -"isabelle_scala_script". - -* Isabelle tools may consist of .scala files: the Scala compiler is -invoked on the spot. The source needs to define some object that extends -Isabelle_Tool.Body. +* SML/NJ and old versions of Poly/ML are no longer supported. + +* Poly/ML heaps now follow the hierarchy of sessions, and thus require +much less disk space. * The Isabelle ML process is now managed directly by Isabelle/Scala, and shell scripts merely provide optional command-line access. In @@ -1016,30 +1015,14 @@ given heap image. Errors lead to premature exit of the ML process with return code 1. -* The system option "threads" (for the size of the Isabelle/ML thread -farm) is also passed to the underlying ML runtime system as --gcthreads, +* The command-line tool "isabelle build" supports option -N for cyclic +shuffling of NUMA CPU nodes. This may help performance tuning on Linux +servers with separate CPU/memory modules. + +* System option "threads" (for the size of the Isabelle/ML thread farm) +is also passed to the underlying ML runtime system as --gcthreads, unless there is already a default provided via ML_OPTIONS settings. -* Command-line tool "isabelle console" provides option -r to help to -bootstrapping Isabelle/Pure interactively. - -* Command-line tool "isabelle yxml" has been discontinued. -INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in -Isabelle/ML or Isabelle/Scala. - -* File.bash_string, File.bash_path etc. represent Isabelle/ML and -Isabelle/Scala strings authentically within GNU bash. This is useful to -produce robust shell scripts under program control, without worrying -about spaces or special characters. Note that user output works via -Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and -less versatile) operations File.shell_quote, File.shell_path etc. have -been discontinued. - -* SML/NJ and old versions of Poly/ML are no longer supported. - -* Poly/ML heaps now follow the hierarchy of sessions, and thus require -much less disk space. - * System option "checkpoint" helps to fine-tune the global heap space management of isabelle build. This is relevant for big sessions that may exhaust the small 32-bit address space of the ML process (which is used @@ -1055,13 +1038,50 @@ multiprocessor systems. The "isabelle jedit" tool allows to override the implicit default via option -p. +* Command-line tool "isabelle console" provides option -r to help to +bootstrapping Isabelle/Pure interactively. + +* Command-line tool "isabelle yxml" has been discontinued. +INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in +Isabelle/ML or Isabelle/Scala. + +* Many Isabelle tools that require a Java runtime system refer to the +settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64, +depending on the underlying platform. The settings for "isabelle build" +ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been +discontinued. Potential INCOMPATIBILITY. + +* The Isabelle system environment always ensures that the main +executables are found within the shell search $PATH: "isabelle" and +"isabelle_scala_script". + +* Isabelle tools may consist of .scala files: the Scala compiler is +invoked on the spot. The source needs to define some object that extends +Isabelle_Tool.Body. + +* File.bash_string, File.bash_path etc. represent Isabelle/ML and +Isabelle/Scala strings authentically within GNU bash. This is useful to +produce robust shell scripts under program control, without worrying +about spaces or special characters. Note that user output works via +Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and +less versatile) operations File.shell_quote, File.shell_path etc. have +been discontinued. + * The isabelle_java executable allows to run a Java process within the name space of Java and Scala components that are bundled with Isabelle, but without the Isabelle settings environment. -* The command-line tool "isabelle build" supports option -N for cyclic -shuffling of NUMA CPU nodes. This may help performance tuning on Linux -servers with separate CPU/memory modules. +* Isabelle/Scala: the SSH module supports ssh and sftp connections, for +remote command-execution and file-system access. This resembles +operations from module File and Isabelle_System to some extent. Note +that Path specifications need to be resolved remotely via +ssh.remote_path instead of File.standard_path: the implicit process +environment is different, Isabelle settings are not available remotely. + +* Isabelle/Scala: the Mercurial module supports repositories via the +regular hg command-line interface. The repositroy clone and working +directory may reside on a local or remote file-system (via ssh +connection).