Isabelle NEWS -- history user-relevant changes

==============================================

New in this Isabelle version

----------------------------

*** General ***

* Discontinued obsolete method fastsimp / tactic fast_simp_tac, which

is called fastforce / fast_force_tac already since Isabelle2011-1.

* Updated and extended "isar-ref" manual, reduced remaining material

in old "ref" manual.

*** Pure ***

* 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.

* Discontinued obsolete attribute "COMP".  Potential INCOMPATIBILITY,

use regular rule composition via "OF" / "THEN", or explicit proof

structure instead.  Note that Isabelle/ML provides a variety of

operators like COMP, INCR_COMP, COMP_INCR, which need to be applied

with some care where this is really required.

*** HOL ***

* Library/Debug.thy and Library/Parallel.thy: debugging and parallel

execution for code generated towards Isabelle/ML.

* Simproc "finite_Collect" 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.

  - Rationalized type encodings ("type_enc" option).

  - Renamed options:

      max_relevant ~> max_facts

      relevance_thresholds ~> fact_thresholds

*** Document preparation ***

* Default for \<euro> is now based on eurosym package, instead of

slightly exotic babel/greek.

*** System ***

* Discontinued support for Poly/ML 5.2.1, which was the last version

without exception positions and advanced ML compiler/toplevel

configuration.

New in Isabelle2012 (May 2012)

------------------------------

*** General ***

* Prover IDE (PIDE) improvements:

  - more robust Sledgehammer integration (as before the sledgehammer

    command-line needs to be typed into the source buffer)

  - markup for bound variables

  - markup for types of term variables (displayed as tooltips)

  - support for user-defined Isar commands within the running session

  - improved support for Unicode outside original 16bit range

    e.g. glyph for \<A> (thanks to jEdit 4.5.1)

* Forward declaration of outer syntax keywords within the theory

header -- minor INCOMPATIBILITY for user-defined commands.  Allow new

commands to be used in the same theory where defined.

* Auxiliary contexts indicate block structure for specifications with

additional parameters and assumptions.  Such unnamed contexts may be

nested within other targets, like 'theory', 'locale', 'class',

'instantiation' etc.  Results from the local context are generalized

accordingly and applied to the enclosing target context.  Example:

  context

    fixes x y z :: 'a

    assumes xy: "x = y" and yz: "y = z"

  begin

  lemma my_trans: "x = z" using xy yz by simp

  end

  thm my_trans

The most basic application is to factor-out context elements of

several fixes/assumes/shows theorem statements, e.g. see

~~/src/HOL/Isar_Examples/Group_Context.thy

Any other local theory specification element works within the "context

... begin ... end" block as well.

* Bundled declarations associate attributed fact expressions with a

given name in the context.  These may be later included in other

contexts.  This allows to manage context extensions casually, without

the logical dependencies of locales and locale interpretation.  See

commands 'bundle', 'include', 'including' etc. in the isar-ref manual.

* Commands 'lemmas' and 'theorems' allow local variables using 'for'

declaration, and results are standardized before being stored.  Thus

old-style "standard" after instantiation or composition of facts

becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of

indices of schematic variables.

* Rule attributes in local theory declarations (e.g. locale or class)

are now statically evaluated: the resulting theorem is stored instead

of the original expression.  INCOMPATIBILITY in rare situations, where

the historic accident of dynamic re-evaluation in interpretations

etc. was exploited.

* New tutorial "Programming and Proving in Isabelle/HOL"

("prog-prove").  It completely supersedes "A Tutorial Introduction to

Structured Isar Proofs" ("isar-overview"), which has been removed.  It

also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order

Logic" as the recommended beginners tutorial, but does not cover all

of the material of that old tutorial.

* Updated and extended reference manuals: "isar-ref",

"implementation", "system"; reduced remaining material in old "ref"

manual.

*** Pure ***

* Command 'definition' no longer exports the foundational "raw_def"

into the user context.  Minor INCOMPATIBILITY, may use the regular

"def" result with attribute "abs_def" to imitate the old version.

* Attribute "abs_def" turns an equation of the form "f x y == t" into

"f == %x y. t", which ensures that "simp" or "unfold" steps always

expand it.  This also works for object-logic equality.  (Formerly

undocumented feature.)

* Sort constraints are now propagated in simultaneous statements, just

like type constraints.  INCOMPATIBILITY in rare situations, where

distinct sorts used to be assigned accidentally.  For example:

  lemma "P (x::'a::foo)" and "Q (y::'a::bar)"  -- "now illegal"

  lemma "P (x::'a)" and "Q (y::'a::bar)"

    -- "now uniform 'a::bar instead of default sort for first occurrence (!)"

* Rule composition via attribute "OF" (or ML functions OF/MRS) is more

tolerant against multiple unifiers, as long as the final result is

unique.  (As before, rules are composed in canonical right-to-left

order to accommodate newly introduced premises.)

* Renamed some inner syntax categories:

    num ~> num_token

    xnum ~> xnum_token

    xstr ~> str_token

Minor INCOMPATIBILITY.  Note that in practice "num_const" or

"num_position" etc. are mainly used instead (which also include

position information via constraints).

* Simplified configuration options for syntax ambiguity: see

"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref

manual.  Minor INCOMPATIBILITY.

* Discontinued configuration option "syntax_positions": atomic terms

in parse trees are always annotated by position constraints.

* Old code generator for SML and its commands 'code_module',

'code_library', 'consts_code', 'types_code' have been discontinued.

Use commands of the generic code generator instead.  INCOMPATIBILITY.

* Redundant attribute "code_inline" has been discontinued. Use

"code_unfold" instead.  INCOMPATIBILITY.

* Dropped attribute "code_unfold_post" in favor of the its dual

"code_abbrev", which yields a common pattern in definitions like

  definition [code_abbrev]: "f = t"

INCOMPATIBILITY.

* Obsolete 'types' command has been discontinued.  Use 'type_synonym'

instead.  INCOMPATIBILITY.

* Discontinued old "prems" fact, which used to refer to the accidental

collection of foundational premises in the context (already marked as

legacy since Isabelle2011).

*** HOL ***

* Type 'a set is now a proper type constructor (just as before

Isabelle2008).  Definitions mem_def and Collect_def have disappeared.

Non-trivial INCOMPATIBILITY.  For developments keeping predicates and

sets separate, it is often sufficient to rephrase some set S that has

been accidentally used as predicates by "%x. x : S", and some

predicate P that has been accidentally used as set by "{x. P x}".

Corresponding proofs in a first step should be pruned from any

tinkering with former theorems mem_def and Collect_def as far as

possible.

For developments which deliberately mix predicates and sets, a

planning step is necessary to determine what should become a predicate

and what a set.  It can be helpful to carry out that step in

Isabelle2011-1 before jumping right into the current release.

* Code generation by default implements sets as container type rather

than predicates.  INCOMPATIBILITY.

* New type synonym 'a rel = ('a * 'a) set

* The representation of numerals has changed.  Datatype "num"

represents strictly positive binary numerals, along with functions

"numeral :: num => 'a" and "neg_numeral :: num => 'a" to represent

positive and negated numeric literals, respectively.  See also

definitions in ~~/src/HOL/Num.thy.  Potential INCOMPATIBILITY, some

user theories may require adaptations as follows:

  - Theorems with number_ring or number_semiring constraints: These

    classes are gone; use comm_ring_1 or comm_semiring_1 instead.

  - Theories defining numeric types: Remove number, number_semiring,

    and number_ring instances. Defer all theorems about numerals until

    after classes one and semigroup_add have been instantiated.

  - Numeral-only simp rules: Replace each rule having a "number_of v"

    pattern with two copies, one for numeral and one for neg_numeral.

  - Theorems about subclasses of semiring_1 or ring_1: These classes

    automatically support numerals now, so more simp rules and

    simprocs may now apply within the proof.

  - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:

    Redefine using other integer operations.

* Transfer: New package intended to generalize the existing

"descending" method and related theorem attributes from the Quotient

package.  (Not all functionality is implemented yet, but future

development will focus on Transfer as an eventual replacement for the

corresponding parts of the Quotient package.)

  - transfer_rule attribute: Maintains a collection of transfer rules,

    which relate constants at two different types. Transfer rules may

    relate different type instances of the same polymorphic constant,

    or they may relate an operation on a raw type to a corresponding

    operation on an abstract type (quotient or subtype). For example:

    ((A ===> B) ===> list_all2 A ===> list_all2 B) map map

    (cr_int ===> cr_int ===> cr_int) (%(x,y) (u,v). (x+u, y+v)) plus_int

  - transfer method: Replaces a subgoal on abstract types with an

    equivalent subgoal on the corresponding raw types. Constants are

    replaced with corresponding ones according to the transfer rules.

    Goals are generalized over all free variables by default; this is

    necessary for variables whose types change, but can be overridden

    for specific variables with e.g. "transfer fixing: x y z".  The

    variant transfer' method allows replacing a subgoal with one that

    is logically stronger (rather than equivalent).

  - relator_eq attribute: Collects identity laws for relators of

    various type constructors, e.g. "list_all2 (op =) = (op =)".  The

    transfer method uses these lemmas to infer transfer rules for

    non-polymorphic constants on the fly.

  - transfer_prover method: Assists with proving a transfer rule for a

    new constant, provided the constant is defined in terms of other

    constants that already have transfer rules. It should be applied

    after unfolding the constant definitions.

  - HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer

    from type nat to type int.

* Lifting: New package intended to generalize the quotient_definition

facility of the Quotient package; designed to work with Transfer.

  - lift_definition command: Defines operations on an abstract type in

    terms of a corresponding operation on a representation

    type.  Example syntax:

    lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist"

      is List.insert

    Users must discharge a respectfulness proof obligation when each

    constant is defined. (For a type copy, i.e. a typedef with UNIV,

    the proof is discharged automatically.) The obligation is

    presented in a user-friendly, readable form; a respectfulness

    theorem in the standard format and a transfer rule are generated

    by the package.

  - Integration with code_abstype: For typedefs (e.g. subtypes

    corresponding to a datatype invariant, such as dlist),

    lift_definition generates a code certificate theorem and sets up

    code generation for each constant.

  - setup_lifting command: Sets up the Lifting package to work with a

    user-defined type. The user must provide either a quotient theorem

    or a type_definition theorem.  The package configures transfer

    rules for equality and quantifiers on the type, and sets up the

    lift_definition command to work with the type.

  - Usage examples: See Quotient_Examples/Lift_DList.thy,

    Quotient_Examples/Lift_RBT.thy, Quotient_Examples/Lift_FSet.thy,

    Word/Word.thy and Library/Float.thy.

* Quotient package:

  - The 'quotient_type' command now supports a 'morphisms' option with

    rep and abs functions, similar to typedef.

  - 'quotient_type' sets up new types to work with the Lifting and

    Transfer packages, as with 'setup_lifting'.

  - The 'quotient_definition' command now requires the user to prove a

    respectfulness property at the point where the constant is

    defined, similar to lift_definition; INCOMPATIBILITY.

  - Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems

    accordingly, INCOMPATIBILITY.

* New diagnostic command 'find_unused_assms' to find potentially

superfluous assumptions in theorems using Quickcheck.

* Quickcheck:

  - Quickcheck returns variable assignments as counterexamples, which

    allows to reveal the underspecification of functions under test.

    For example, refuting "hd xs = x", it presents the variable

    assignment xs = [] and x = a1 as a counterexample, assuming that

    any property is false whenever "hd []" occurs in it.

    These counterexample are marked as potentially spurious, as

    Quickcheck also returns "xs = []" as a counterexample to the

    obvious theorem "hd xs = hd xs".

    After finding a potentially spurious counterexample, Quickcheck

    continues searching for genuine ones.

    By default, Quickcheck shows potentially spurious and genuine

    counterexamples. The option "genuine_only" sets quickcheck to only

    show genuine counterexamples.

  - The command 'quickcheck_generator' creates random and exhaustive

    value generators for a given type and operations.

    It generates values by using the operations as if they were

    constructors of that type.

  - Support for multisets.

  - Added "use_subtype" options.

  - Added "quickcheck_locale" configuration to specify how to process

    conjectures in a locale context.

* Nitpick: Fixed infinite loop caused by the 'peephole_optim' option

and affecting 'rat' and 'real'.

* Sledgehammer:

  - Integrated more tightly with SPASS, as described in the ITP 2012

    paper "More SPASS with Isabelle".

  - Made it try "smt" as a fallback if "metis" fails or times out.

  - Added support for the following provers: Alt-Ergo (via Why3 and

    TFF1), iProver, iProver-Eq.

  - Sped up the minimizer.

  - Added "lam_trans", "uncurry_aliases", and "minimize" options.

  - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").

  - Renamed "sound" option to "strict".

* Metis: Added possibility to specify lambda translations scheme as a

parenthesized argument (e.g., "by (metis (lifting) ...)").

* SMT: Renamed "smt_fixed" option to "smt_read_only_certificates".

* Command 'try0': Renamed from 'try_methods'. INCOMPATIBILITY.

* New "case_product" attribute to generate a case rule doing multiple

case distinctions at the same time.  E.g.

  list.exhaust [case_product nat.exhaust]

produces a rule which can be used to perform case distinction on both

a list and a nat.

* New "eventually_elim" method as a generalized variant of the

eventually_elim* rules.  Supports structured proofs.

* Typedef with implicit set definition is considered legacy.  Use

"typedef (open)" form instead, which will eventually become the

default.

* Record: code generation can be switched off manually with

  declare [[record_coden = false]]  -- "default true"

* Datatype: type parameters allow explicit sort constraints.

* Concrete syntax for case expressions includes constraints for source

positions, and thus produces Prover IDE markup for its bindings.

INCOMPATIBILITY for old-style syntax translations that augment the

pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of

one_case.

* Clarified attribute "mono_set": pure declaration without modifying

the result of the fact expression.

* More default pred/set conversions on a couple of relation operations

and predicates.  Added powers of predicate relations.  Consolidation

of some relation theorems:

  converse_def ~> converse_unfold

  rel_comp_def ~> relcomp_unfold

  symp_def ~> (modified, use symp_def and sym_def instead)

  transp_def ~> transp_trans

  Domain_def ~> Domain_unfold

  Range_def ~> Domain_converse [symmetric]

Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2.

See theory "Relation" for examples for making use of pred/set

conversions by means of attributes "to_set" and "to_pred".

INCOMPATIBILITY.

* Renamed facts about the power operation on relations, i.e., relpow

to match the constant's name:

  rel_pow_1 ~> relpow_1

  rel_pow_0_I ~> relpow_0_I

  rel_pow_Suc_I ~> relpow_Suc_I

  rel_pow_Suc_I2 ~> relpow_Suc_I2

  rel_pow_0_E ~> relpow_0_E

  rel_pow_Suc_E ~> relpow_Suc_E

  rel_pow_E ~> relpow_E

  rel_pow_Suc_D2 ~> relpow_Suc_D2

  rel_pow_Suc_E2 ~> relpow_Suc_E2

  rel_pow_Suc_D2' ~> relpow_Suc_D2'

  rel_pow_E2 ~> relpow_E2

  rel_pow_add ~> relpow_add

  rel_pow_commute ~> relpow

  rel_pow_empty ~> relpow_empty:

  rtrancl_imp_UN_rel_pow ~> rtrancl_imp_UN_relpow

  rel_pow_imp_rtrancl ~> relpow_imp_rtrancl

  rtrancl_is_UN_rel_pow ~> rtrancl_is_UN_relpow

  rtrancl_imp_rel_pow ~> rtrancl_imp_relpow

  rel_pow_fun_conv ~> relpow_fun_conv

  rel_pow_finite_bounded1 ~> relpow_finite_bounded1

  rel_pow_finite_bounded ~> relpow_finite_bounded

  rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow

  trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow

  single_valued_rel_pow ~> single_valued_relpow

INCOMPATIBILITY.

* Theory Relation: Consolidated constant name for relation composition

and corresponding theorem names:

  - Renamed constant rel_comp to relcomp.

  - Dropped abbreviation pred_comp. Use relcompp instead.

  - Renamed theorems:

    rel_compI ~> relcompI

    rel_compEpair ~> relcompEpair

    rel_compE ~> relcompE

    pred_comp_rel_comp_eq ~> relcompp_relcomp_eq

    rel_comp_empty1 ~> relcomp_empty1

    rel_comp_mono ~> relcomp_mono

    rel_comp_subset_Sigma ~> relcomp_subset_Sigma

    rel_comp_distrib ~> relcomp_distrib

    rel_comp_distrib2 ~> relcomp_distrib2

    rel_comp_UNION_distrib ~> relcomp_UNION_distrib

    rel_comp_UNION_distrib2 ~> relcomp_UNION_distrib2

    single_valued_rel_comp ~> single_valued_relcomp

    rel_comp_def ~> relcomp_unfold

    converse_rel_comp ~> converse_relcomp

    pred_compI ~> relcomppI

    pred_compE ~> relcomppE

    pred_comp_bot1 ~> relcompp_bot1

    pred_comp_bot2 ~> relcompp_bot2

    transp_pred_comp_less_eq ~> transp_relcompp_less_eq

    pred_comp_mono ~> relcompp_mono

    pred_comp_distrib ~> relcompp_distrib

    pred_comp_distrib2 ~> relcompp_distrib2

    converse_pred_comp ~> converse_relcompp

    finite_rel_comp ~> finite_relcomp

    set_rel_comp ~> set_relcomp

INCOMPATIBILITY.

* Theory Divides: Discontinued redundant theorems about div and mod.

INCOMPATIBILITY, use the corresponding generic theorems instead.

  DIVISION_BY_ZERO ~> div_by_0, mod_by_0

  zdiv_self ~> div_self

  zmod_self ~> mod_self

  zdiv_zero ~> div_0

  zmod_zero ~> mod_0

  zdiv_zmod_equality ~> div_mod_equality2

  zdiv_zmod_equality2 ~> div_mod_equality

  zmod_zdiv_trivial ~> mod_div_trivial

  zdiv_zminus_zminus ~> div_minus_minus

  zmod_zminus_zminus ~> mod_minus_minus

  zdiv_zminus2 ~> div_minus_right

  zmod_zminus2 ~> mod_minus_right

  zdiv_minus1_right ~> div_minus1_right

  zmod_minus1_right ~> mod_minus1_right

  zdvd_mult_div_cancel ~> dvd_mult_div_cancel

  zmod_zmult1_eq ~> mod_mult_right_eq

  zpower_zmod ~> power_mod

  zdvd_zmod ~> dvd_mod

  zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd

  mod_mult_distrib ~> mult_mod_left

  mod_mult_distrib2 ~> mult_mod_right

* Removed redundant theorems nat_mult_2 and nat_mult_2_right; use

generic mult_2 and mult_2_right instead. INCOMPATIBILITY.

* Finite_Set.fold now qualified.  INCOMPATIBILITY.

* Consolidated theorem names concerning fold combinators:

  inf_INFI_fold_inf ~> inf_INF_fold_inf

  sup_SUPR_fold_sup ~> sup_SUP_fold_sup

  INFI_fold_inf ~> INF_fold_inf

  SUPR_fold_sup ~> SUP_fold_sup

  union_set ~> union_set_fold

  minus_set ~> minus_set_fold

  INFI_set_fold ~> INF_set_fold

  SUPR_set_fold ~> SUP_set_fold

  INF_code ~> INF_set_foldr

  SUP_code ~> SUP_set_foldr

  foldr.simps ~> foldr.simps (in point-free formulation)

  foldr_fold_rev ~> foldr_conv_fold

  foldl_fold ~> foldl_conv_fold

  foldr_foldr ~> foldr_conv_foldl

  foldl_foldr ~> foldl_conv_foldr

  fold_set_remdups ~> fold_set_fold_remdups

  fold_set ~> fold_set_fold

  fold1_set ~> fold1_set_fold

INCOMPATIBILITY.

* Dropped rarely useful theorems concerning fold combinators:

foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant,

rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,

concat_conv_foldl, foldl_weak_invariant, foldl_invariant,

foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,

listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc,

foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv.

INCOMPATIBILITY.  For the common phrases "%xs. List.foldr plus xs 0"

and "List.foldl plus 0", prefer "List.listsum".  Otherwise it can be

useful to boil down "List.foldr" and "List.foldl" to "List.fold" by

unfolding "foldr_conv_fold" and "foldl_conv_fold".

* Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr,

inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr,

Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr,

INF_set_foldr, SUP_set_foldr.  INCOMPATIBILITY.  Prefer corresponding

lemmas over fold rather than foldr, or make use of lemmas

fold_conv_foldr and fold_rev.

* Congruence rules Option.map_cong and Option.bind_cong for recursion

through option types.

* "Transitive_Closure.ntrancl": bounded transitive closure on

relations.

* Constant "Set.not_member" now qualified.  INCOMPATIBILITY.

* Theory Int: Discontinued many legacy theorems specific to type int.

INCOMPATIBILITY, use the corresponding generic theorems instead.

  zminus_zminus ~> minus_minus

  zminus_0 ~> minus_zero

  zminus_zadd_distrib ~> minus_add_distrib

  zadd_commute ~> add_commute

  zadd_assoc ~> add_assoc

  zadd_left_commute ~> add_left_commute

  zadd_ac ~> add_ac

  zmult_ac ~> mult_ac

  zadd_0 ~> add_0_left

  zadd_0_right ~> add_0_right

  zadd_zminus_inverse2 ~> left_minus

  zmult_zminus ~> mult_minus_left

  zmult_commute ~> mult_commute

  zmult_assoc ~> mult_assoc

  zadd_zmult_distrib ~> left_distrib

  zadd_zmult_distrib2 ~> right_distrib

  zdiff_zmult_distrib ~> left_diff_distrib

  zdiff_zmult_distrib2 ~> right_diff_distrib

  zmult_1 ~> mult_1_left

  zmult_1_right ~> mult_1_right

  zle_refl ~> order_refl

  zle_trans ~> order_trans

  zle_antisym ~> order_antisym

  zle_linear ~> linorder_linear

  zless_linear ~> linorder_less_linear

  zadd_left_mono ~> add_left_mono

  zadd_strict_right_mono ~> add_strict_right_mono

  zadd_zless_mono ~> add_less_le_mono

  int_0_less_1 ~> zero_less_one

  int_0_neq_1 ~> zero_neq_one

  zless_le ~> less_le

  zpower_zadd_distrib ~> power_add

  zero_less_zpower_abs_iff ~> zero_less_power_abs_iff

  zero_le_zpower_abs ~> zero_le_power_abs

* Theory Deriv: Renamed

  DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing

* Theory Library/Multiset: Improved code generation of multisets.

* Theory HOL/Library/Set_Algebras: Addition and multiplication on sets

are expressed via type classes again. The special syntax

\<oplus>/\<otimes> has been replaced by plain +/*. Removed constant

setsum_set, which is now subsumed by Big_Operators.setsum.

INCOMPATIBILITY.

* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,

use theory HOL/Library/Nat_Bijection instead.

* Theory HOL/Library/RBT_Impl: Backing implementation of red-black

trees is now inside a type class context.  Names of affected

operations and lemmas have been prefixed by rbt_.  INCOMPATIBILITY for

theories working directly with raw red-black trees, adapt the names as

follows:

  Operations:

  bulkload -> rbt_bulkload

  del_from_left -> rbt_del_from_left

  del_from_right -> rbt_del_from_right

  del -> rbt_del

  delete -> rbt_delete

  ins -> rbt_ins

  insert -> rbt_insert

  insertw -> rbt_insert_with

  insert_with_key -> rbt_insert_with_key

  map_entry -> rbt_map_entry

  lookup -> rbt_lookup

  sorted -> rbt_sorted

  tree_greater -> rbt_greater

  tree_less -> rbt_less

  tree_less_symbol -> rbt_less_symbol

  union -> rbt_union

  union_with -> rbt_union_with

  union_with_key -> rbt_union_with_key

  Lemmas:

  balance_left_sorted -> balance_left_rbt_sorted

  balance_left_tree_greater -> balance_left_rbt_greater

  balance_left_tree_less -> balance_left_rbt_less

  balance_right_sorted -> balance_right_rbt_sorted

  balance_right_tree_greater -> balance_right_rbt_greater

  balance_right_tree_less -> balance_right_rbt_less

  balance_sorted -> balance_rbt_sorted

  balance_tree_greater -> balance_rbt_greater

  balance_tree_less -> balance_rbt_less

  bulkload_is_rbt -> rbt_bulkload_is_rbt

  combine_sorted -> combine_rbt_sorted

  combine_tree_greater -> combine_rbt_greater

  combine_tree_less -> combine_rbt_less

  delete_in_tree -> rbt_delete_in_tree

  delete_is_rbt -> rbt_delete_is_rbt

  del_from_left_tree_greater -> rbt_del_from_left_rbt_greater

  del_from_left_tree_less -> rbt_del_from_left_rbt_less

  del_from_right_tree_greater -> rbt_del_from_right_rbt_greater

  del_from_right_tree_less -> rbt_del_from_right_rbt_less

  del_in_tree -> rbt_del_in_tree

  del_inv1_inv2 -> rbt_del_inv1_inv2

  del_sorted -> rbt_del_rbt_sorted

  del_tree_greater -> rbt_del_rbt_greater

  del_tree_less -> rbt_del_rbt_less

  dom_lookup_Branch -> dom_rbt_lookup_Branch

  entries_lookup -> entries_rbt_lookup

  finite_dom_lookup -> finite_dom_rbt_lookup

  insert_sorted -> rbt_insert_rbt_sorted

  insertw_is_rbt -> rbt_insertw_is_rbt

  insertwk_is_rbt -> rbt_insertwk_is_rbt

  insertwk_sorted -> rbt_insertwk_rbt_sorted

  insertw_sorted -> rbt_insertw_rbt_sorted

  ins_sorted -> ins_rbt_sorted

  ins_tree_greater -> ins_rbt_greater

  ins_tree_less -> ins_rbt_less

  is_rbt_sorted -> is_rbt_rbt_sorted

  lookup_balance -> rbt_lookup_balance

  lookup_bulkload -> rbt_lookup_rbt_bulkload

  lookup_delete -> rbt_lookup_rbt_delete

  lookup_Empty -> rbt_lookup_Empty

  lookup_from_in_tree -> rbt_lookup_from_in_tree

  lookup_in_tree -> rbt_lookup_in_tree

  lookup_ins -> rbt_lookup_ins

  lookup_insert -> rbt_lookup_rbt_insert

  lookup_insertw -> rbt_lookup_rbt_insertw

  lookup_insertwk -> rbt_lookup_rbt_insertwk

  lookup_keys -> rbt_lookup_keys

  lookup_map -> rbt_lookup_map

  lookup_map_entry -> rbt_lookup_rbt_map_entry

  lookup_tree_greater -> rbt_lookup_rbt_greater

  lookup_tree_less -> rbt_lookup_rbt_less

  lookup_union -> rbt_lookup_rbt_union

  map_entry_color_of -> rbt_map_entry_color_of

  map_entry_inv1 -> rbt_map_entry_inv1

  map_entry_inv2 -> rbt_map_entry_inv2

  map_entry_is_rbt -> rbt_map_entry_is_rbt

  map_entry_sorted -> rbt_map_entry_rbt_sorted

  map_entry_tree_greater -> rbt_map_entry_rbt_greater

  map_entry_tree_less -> rbt_map_entry_rbt_less

  map_tree_greater -> map_rbt_greater

  map_tree_less -> map_rbt_less

  map_sorted -> map_rbt_sorted

  paint_sorted -> paint_rbt_sorted

  paint_lookup -> paint_rbt_lookup

  paint_tree_greater -> paint_rbt_greater

  paint_tree_less -> paint_rbt_less

  sorted_entries -> rbt_sorted_entries

  tree_greater_eq_trans -> rbt_greater_eq_trans

  tree_greater_nit -> rbt_greater_nit

  tree_greater_prop -> rbt_greater_prop

  tree_greater_simps -> rbt_greater_simps

  tree_greater_trans -> rbt_greater_trans

  tree_less_eq_trans -> rbt_less_eq_trans

  tree_less_nit -> rbt_less_nit

  tree_less_prop -> rbt_less_prop

  tree_less_simps -> rbt_less_simps

  tree_less_trans -> rbt_less_trans

  tree_ord_props -> rbt_ord_props

  union_Branch -> rbt_union_Branch

  union_is_rbt -> rbt_union_is_rbt

  unionw_is_rbt -> rbt_unionw_is_rbt

  unionwk_is_rbt -> rbt_unionwk_is_rbt

  unionwk_sorted -> rbt_unionwk_rbt_sorted

* Theory HOL/Library/Float: Floating point numbers are now defined as

a subset of the real numbers.  All operations are defined using the

lifing-framework and proofs use the transfer method.  INCOMPATIBILITY.

  Changed Operations:

  float_abs -> abs

  float_nprt -> nprt

  float_pprt -> pprt

  pow2 -> use powr

  round_down -> float_round_down

  round_up -> float_round_up

  scale -> exponent

  Removed Operations:

  ceiling_fl, lb_mult, lb_mod, ub_mult, ub_mod

  Renamed Lemmas:

  abs_float_def -> Float.compute_float_abs

  bitlen_ge0 -> bitlen_nonneg

  bitlen.simps -> Float.compute_bitlen

  float_components -> Float_mantissa_exponent

  float_divl.simps -> Float.compute_float_divl

  float_divr.simps -> Float.compute_float_divr

  float_eq_odd -> mult_powr_eq_mult_powr_iff

  float_power -> real_of_float_power

  lapprox_posrat_def -> Float.compute_lapprox_posrat

  lapprox_rat.simps -> Float.compute_lapprox_rat

  le_float_def' -> Float.compute_float_le

  le_float_def -> less_eq_float.rep_eq

  less_float_def' -> Float.compute_float_less

  less_float_def -> less_float.rep_eq

  normfloat_def -> Float.compute_normfloat

  normfloat_imp_odd_or_zero -> mantissa_not_dvd and mantissa_noteq_0

  normfloat -> normfloat_def

  normfloat_unique -> use normfloat_def

  number_of_float_Float -> Float.compute_float_numeral, Float.compute_float_neg_numeral

  one_float_def -> Float.compute_float_one

  plus_float_def -> Float.compute_float_plus

  rapprox_posrat_def -> Float.compute_rapprox_posrat

  rapprox_rat.simps -> Float.compute_rapprox_rat

  real_of_float_0 -> zero_float.rep_eq

  real_of_float_1 -> one_float.rep_eq

  real_of_float_abs -> abs_float.rep_eq

  real_of_float_add -> plus_float.rep_eq

  real_of_float_minus -> uminus_float.rep_eq

  real_of_float_mult -> times_float.rep_eq

  real_of_float_simp -> Float.rep_eq

  real_of_float_sub -> minus_float.rep_eq

  round_down.simps -> Float.compute_float_round_down

  round_up.simps -> Float.compute_float_round_up

  times_float_def -> Float.compute_float_times

  uminus_float_def -> Float.compute_float_uminus

  zero_float_def -> Float.compute_float_zero

  Lemmas not necessary anymore, use the transfer method:

  bitlen_B0, bitlen_B1, bitlen_ge1, bitlen_Min, bitlen_Pls, float_divl,

  float_divr, float_le_simp, float_less1_mantissa_bound,

  float_less_simp, float_less_zero, float_le_zero,

  float_pos_less1_e_neg, float_pos_m_pos, float_split, float_split2,

  floor_pos_exp, lapprox_posrat, lapprox_posrat_bottom, lapprox_rat,

  lapprox_rat_bottom, normalized_float, rapprox_posrat,

  rapprox_posrat_le1, rapprox_rat, real_of_float_ge0_exp,

  real_of_float_neg_exp, real_of_float_nge0_exp, round_down floor_fl,

  round_up, zero_le_float, zero_less_float

* New theory HOL/Library/DAList provides an abstract type for

association lists with distinct keys.

* Session HOL/IMP: Added new theory of abstract interpretation of

annotated commands.

* Session HOL-Import: Re-implementation from scratch is faster,

simpler, and more scalable.  Requires a proof bundle, which is

available as an external component.  Discontinued old (and mostly

dead) Importer for HOL4 and HOL Light.  INCOMPATIBILITY.

* Session HOL-Word: Discontinued many redundant theorems specific to

type 'a word. INCOMPATIBILITY, use the corresponding generic theorems

instead.

  word_sub_alt ~> word_sub_wi

  word_add_alt ~> word_add_def

  word_mult_alt ~> word_mult_def

  word_minus_alt ~> word_minus_def

  word_0_alt ~> word_0_wi

  word_1_alt ~> word_1_wi

  word_add_0 ~> add_0_left

  word_add_0_right ~> add_0_right

  word_mult_1 ~> mult_1_left

  word_mult_1_right ~> mult_1_right

  word_add_commute ~> add_commute

  word_add_assoc ~> add_assoc

  word_add_left_commute ~> add_left_commute

  word_mult_commute ~> mult_commute

  word_mult_assoc ~> mult_assoc

  word_mult_left_commute ~> mult_left_commute

  word_left_distrib ~> left_distrib

  word_right_distrib ~> right_distrib

  word_left_minus ~> left_minus

  word_diff_0_right ~> diff_0_right

  word_diff_self ~> diff_self

  word_sub_def ~> diff_minus

  word_diff_minus ~> diff_minus

  word_add_ac ~> add_ac

  word_mult_ac ~> mult_ac

  word_plus_ac0 ~> add_0_left add_0_right add_ac

  word_times_ac1 ~> mult_1_left mult_1_right mult_ac

  word_order_trans ~> order_trans

  word_order_refl ~> order_refl

  word_order_antisym ~> order_antisym

  word_order_linear ~> linorder_linear

  lenw1_zero_neq_one ~> zero_neq_one

  word_number_of_eq ~> number_of_eq

  word_of_int_add_hom ~> wi_hom_add

  word_of_int_sub_hom ~> wi_hom_sub

  word_of_int_mult_hom ~> wi_hom_mult

  word_of_int_minus_hom ~> wi_hom_neg

  word_of_int_succ_hom ~> wi_hom_succ

  word_of_int_pred_hom ~> wi_hom_pred

  word_of_int_0_hom ~> word_0_wi

  word_of_int_1_hom ~> word_1_wi

* Session HOL-Word: New proof method "word_bitwise" for splitting

machine word equalities and inequalities into logical circuits,

defined in HOL/Word/WordBitwise.thy.  Supports addition, subtraction,

multiplication, shifting by constants, bitwise operators and numeric

constants.  Requires fixed-length word types, not 'a word.  Solves

many standard word identities outright and converts more into first

order problems amenable to blast or similar.  See also examples in

HOL/Word/Examples/WordExamples.thy.

* Session HOL-Probability: Introduced the type "'a measure" to

represent measures, this replaces the records 'a algebra and 'a

measure_space.  The locales based on subset_class now have two

locale-parameters the space \<Omega> and the set of measurable sets M.

The product of probability spaces uses now the same constant as the

finite product of sigma-finite measure spaces "PiM :: ('i => 'a)

measure".  Most constants are defined now outside of locales and gain

an additional parameter, like null_sets, almost_eventually or \<mu>'.

Measure space constructions for distributions and densities now got

their own constants distr and density.  Instead of using locales to

describe measure spaces with a finite space, the measure count_space

and point_measure is introduced.  INCOMPATIBILITY.

  Renamed constants:

  measure -> emeasure

  finite_measure.\<mu>' -> measure

  product_algebra_generator -> prod_algebra

  product_prob_space.emb -> prod_emb

  product_prob_space.infprod_algebra -> PiM

  Removed locales:

  completeable_measure_space

  finite_measure_space

  finite_prob_space

  finite_product_finite_prob_space

  finite_product_sigma_algebra

  finite_sigma_algebra

  measure_space

  pair_finite_prob_space

  pair_finite_sigma_algebra

  pair_finite_space

  pair_sigma_algebra

  product_sigma_algebra

  Removed constants:

  conditional_space

  distribution -> use distr measure, or distributed predicate

  image_space

  joint_distribution -> use distr measure, or distributed predicate

  pair_measure_generator

  product_prob_space.infprod_algebra -> use PiM

  subvimage

  Replacement theorems:

  finite_additivity_sufficient -> ring_of_sets.countably_additiveI_finite

  finite_measure.empty_measure -> measure_empty

  finite_measure.finite_continuity_from_above -> finite_measure.finite_Lim_measure_decseq

  finite_measure.finite_continuity_from_below -> finite_measure.finite_Lim_measure_incseq

  finite_measure.finite_measure_countably_subadditive -> finite_measure.finite_measure_subadditive_countably

  finite_measure.finite_measure_eq -> finite_measure.emeasure_eq_measure

  finite_measure.finite_measure -> finite_measure.emeasure_finite

  finite_measure.finite_measure_finite_singleton -> finite_measure.finite_measure_eq_setsum_singleton

  finite_measure.positive_measure' -> measure_nonneg

  finite_measure.real_measure -> finite_measure.emeasure_real

  finite_product_prob_space.finite_measure_times -> finite_product_prob_space.finite_measure_PiM_emb

  finite_product_sigma_algebra.in_P -> sets_PiM_I_finite

  finite_product_sigma_algebra.P_empty -> space_PiM_empty, sets_PiM_empty

  information_space.conditional_entropy_eq -> information_space.conditional_entropy_simple_distributed

  information_space.conditional_entropy_positive -> information_space.conditional_entropy_nonneg_simple

  information_space.conditional_mutual_information_eq_mutual_information -> information_space.conditional_mutual_information_eq_mutual_information_simple

  information_space.conditional_mutual_information_generic_positive -> information_space.conditional_mutual_information_nonneg_simple

  information_space.conditional_mutual_information_positive -> information_space.conditional_mutual_information_nonneg_simple

  information_space.entropy_commute -> information_space.entropy_commute_simple

  information_space.entropy_eq -> information_space.entropy_simple_distributed

  information_space.entropy_generic_eq -> information_space.entropy_simple_distributed

  information_space.entropy_positive -> information_space.entropy_nonneg_simple

  information_space.entropy_uniform_max -> information_space.entropy_uniform

  information_space.KL_eq_0_imp -> information_space.KL_eq_0_iff_eq

  information_space.KL_eq_0 -> information_space.KL_same_eq_0

  information_space.KL_ge_0 -> information_space.KL_nonneg

  information_space.mutual_information_eq -> information_space.mutual_information_simple_distributed

  information_space.mutual_information_positive -> information_space.mutual_information_nonneg_simple

  Int_stable_cuboids -> Int_stable_atLeastAtMost

  Int_stable_product_algebra_generator -> positive_integral

  measure_preserving -> equality "distr M N f = N" "f : measurable M N"

  measure_space.additive -> emeasure_additive

  measure_space.AE_iff_null_set -> AE_iff_null

  measure_space.almost_everywhere_def -> eventually_ae_filter

  measure_space.almost_everywhere_vimage -> AE_distrD

  measure_space.continuity_from_above -> INF_emeasure_decseq

  measure_space.continuity_from_above_Lim -> Lim_emeasure_decseq

  measure_space.continuity_from_below_Lim -> Lim_emeasure_incseq

  measure_space.continuity_from_below -> SUP_emeasure_incseq

  measure_space_density -> emeasure_density

  measure_space.density_is_absolutely_continuous -> absolutely_continuousI_density

  measure_space.integrable_vimage -> integrable_distr

  measure_space.integral_translated_density -> integral_density

  measure_space.integral_vimage -> integral_distr

  measure_space.measure_additive -> plus_emeasure

  measure_space.measure_compl -> emeasure_compl

  measure_space.measure_countable_increasing -> emeasure_countable_increasing

  measure_space.measure_countably_subadditive -> emeasure_subadditive_countably

  measure_space.measure_decseq -> decseq_emeasure

  measure_space.measure_Diff -> emeasure_Diff

  measure_space.measure_Diff_null_set -> emeasure_Diff_null_set

  measure_space.measure_eq_0 -> emeasure_eq_0

  measure_space.measure_finitely_subadditive -> emeasure_subadditive_finite

  measure_space.measure_finite_singleton -> emeasure_eq_setsum_singleton

  measure_space.measure_incseq -> incseq_emeasure

  measure_space.measure_insert -> emeasure_insert

  measure_space.measure_mono -> emeasure_mono

  measure_space.measure_not_negative -> emeasure_not_MInf