Isabelle NEWS -- history user-relevant changes

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

New in Isabelle2009-2 (June 2010)

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

*** General ***

* Authentic syntax for *all* logical entities (type classes, type

constructors, term constants): provides simple and robust

correspondence between formal entities and concrete syntax.  Within

the parse tree / AST representations, "constants" are decorated by

their category (class, type, const) and spelled out explicitly with

their full internal name.

Substantial INCOMPATIBILITY concerning low-level syntax declarations

and translations (translation rules and translation functions in ML).

Some hints on upgrading:

  - Many existing uses of 'syntax' and 'translations' can be replaced

    by more modern 'type_notation', 'notation' and 'abbreviation',

    which are independent of this issue.

  - 'translations' require markup within the AST; the term syntax

    provides the following special forms:

      CONST c   -- produces syntax version of constant c from context

      XCONST c  -- literally c, checked as constant from context

      c         -- literally c, if declared by 'syntax'

    Plain identifiers are treated as AST variables -- occasionally the

    system indicates accidental variables via the error "rhs contains

    extra variables".

    Type classes and type constructors are marked according to their

    concrete syntax.  Some old translations rules need to be written

    for the "type" category, using type constructor application

    instead of pseudo-term application of the default category

    "logic".

  - 'parse_translation' etc. in ML may use the following

    antiquotations:

      @{class_syntax c}   -- type class c within parse tree / AST

      @{term_syntax c}    -- type constructor c within parse tree / AST

      @{const_syntax c}   -- ML version of "CONST c" above

      @{syntax_const c}   -- literally c (checked wrt. 'syntax' declarations)

  - Literal types within 'typed_print_translations', i.e. those *not*

    represented as pseudo-terms are represented verbatim.  Use @{class

    c} or @{type_name c} here instead of the above syntax

    antiquotations.

Note that old non-authentic syntax was based on unqualified base

names, so all of the above "constant" names would coincide.  Recall

that 'print_syntax' and ML_command "set Syntax.trace_ast" help to

diagnose syntax problems.

* Type constructors admit general mixfix syntax, not just infix.

* Concrete syntax may be attached to local entities without a proof

body, too.  This works via regular mixfix annotations for 'fix',

'def', 'obtain' etc. or via the explicit 'write' command, which is

similar to the 'notation' command in theory specifications.

* Discontinued unnamed infix syntax (legacy feature for many years) --

need to specify constant name and syntax separately.  Internal ML

datatype constructors have been renamed from InfixName to Infix etc.

Minor INCOMPATIBILITY.

* Schematic theorem statements need to be explicitly markup as such,

via commands 'schematic_lemma', 'schematic_theorem',

'schematic_corollary'.  Thus the relevance of the proof is made

syntactically clear, which impacts performance in a parallel or

asynchronous interactive environment.  Minor INCOMPATIBILITY.

* Use of cumulative prems via "!" in some proof methods has been

discontinued (old legacy feature).

* References 'trace_simp' and 'debug_simp' have been replaced by

configuration options stored in the context. Enabling tracing (the

case of debugging is similar) in proofs works via

  using [[trace_simp = true]]

Tracing is then active for all invocations of the simplifier in

subsequent goal refinement steps. Tracing may also still be enabled or

disabled via the ProofGeneral settings menu.

* Separate commands 'hide_class', 'hide_type', 'hide_const',

'hide_fact' replace the former 'hide' KIND command.  Minor

INCOMPATIBILITY.

* Improved parallelism of proof term normalization: usedir -p2 -q0 is

more efficient than combinations with -q1 or -q2.

*** Pure ***

* Proofterms record type-class reasoning explicitly, using the

"unconstrain" operation internally.  This eliminates all sort

constraints from a theorem and proof, introducing explicit

OFCLASS-premises.  On the proof term level, this operation is

automatically applied at theorem boundaries, such that closed proofs

are always free of sort constraints.  INCOMPATIBILITY for tools that

inspect proof terms.

* Local theory specifications may depend on extra type variables that

are not present in the result type -- arguments TYPE('a) :: 'a itself

are added internally.  For example:

  definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"

* Predicates of locales introduced by classes carry a mandatory

"class" prefix.  INCOMPATIBILITY.

* Vacuous class specifications observe default sort.  INCOMPATIBILITY.

* Old 'axclass' command has been discontinued.  INCOMPATIBILITY, use

'class' instead.

* Command 'code_reflect' allows to incorporate generated ML code into

runtime environment; replaces immature code_datatype antiquotation.

INCOMPATIBILITY.

* Code generator: simple concept for abstract datatypes obeying

invariants.

* Code generator: details of internal data cache have no impact on the

user space functionality any longer.

* Methods "unfold_locales" and "intro_locales" ignore non-locale

subgoals.  This is more appropriate for interpretations with 'where'.

INCOMPATIBILITY.

* Command 'example_proof' opens an empty proof body.  This allows to

experiment with Isar, without producing any persistent result.

* Commands 'type_notation' and 'no_type_notation' declare type syntax

within a local theory context, with explicit checking of the

constructors involved (in contrast to the raw 'syntax' versions).

* Commands 'types' and 'typedecl' now work within a local theory

context -- without introducing dependencies on parameters or

assumptions, which is not possible in Isabelle/Pure.

* Command 'defaultsort' has been renamed to 'default_sort', it works

within a local theory context.  Minor INCOMPATIBILITY.

*** HOL ***

* Command 'typedef' now works within a local theory context -- without

introducing dependencies on parameters or assumptions, which is not

possible in Isabelle/Pure/HOL.  Note that the logical environment may

contain multiple interpretations of local typedefs (with different

non-emptiness proofs), even in a global theory context.

* New package for quotient types.  Commands 'quotient_type' and

'quotient_definition' may be used for defining types and constants by

quotient constructions.  An example is the type of integers created by

quotienting pairs of natural numbers:

  fun

    intrel :: "(nat * nat) => (nat * nat) => bool" 

  where

    "intrel (x, y) (u, v) = (x + v = u + y)"

  quotient_type int = "nat × nat" / intrel

    by (auto simp add: equivp_def expand_fun_eq)

  quotient_definition

    "0::int" is "(0::nat, 0::nat)"

The method "lifting" can be used to lift of theorems from the

underlying "raw" type to the quotient type.  The example

src/HOL/Quotient_Examples/FSet.thy includes such a quotient

construction and provides a reasoning infrastructure for finite sets.

* Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid

clash with new theory Quotient in Main HOL.

* Moved the SMT binding into the main HOL session, eliminating

separate HOL-SMT session.

* List membership infix mem operation is only an input abbreviation.

INCOMPATIBILITY.

* Theory Library/Word.thy has been removed.  Use library Word/Word.thy

for future developements; former Library/Word.thy is still present in

the AFP entry RSAPPS.

* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no

longer shadowed.  INCOMPATIBILITY.

* Dropped theorem duplicate comp_arith; use semiring_norm instead.

INCOMPATIBILITY.

* Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.

INCOMPATIBILITY.

* Dropped normalizing_semiring etc; use the facts in semiring classes

instead.  INCOMPATIBILITY.

* Dropped several real-specific versions of lemmas about floor and

ceiling; use the generic lemmas from theory "Archimedean_Field"

instead.  INCOMPATIBILITY.

  floor_number_of_eq         ~> floor_number_of

  le_floor_eq_number_of      ~> number_of_le_floor

  le_floor_eq_zero           ~> zero_le_floor

  le_floor_eq_one            ~> one_le_floor

  floor_less_eq_number_of    ~> floor_less_number_of

  floor_less_eq_zero         ~> floor_less_zero

  floor_less_eq_one          ~> floor_less_one

  less_floor_eq_number_of    ~> number_of_less_floor

  less_floor_eq_zero         ~> zero_less_floor

  less_floor_eq_one          ~> one_less_floor

  floor_le_eq_number_of      ~> floor_le_number_of

  floor_le_eq_zero           ~> floor_le_zero

  floor_le_eq_one            ~> floor_le_one

  floor_subtract_number_of   ~> floor_diff_number_of

  floor_subtract_one         ~> floor_diff_one

  ceiling_number_of_eq       ~> ceiling_number_of

  ceiling_le_eq_number_of    ~> ceiling_le_number_of

  ceiling_le_zero_eq         ~> ceiling_le_zero

  ceiling_le_eq_one          ~> ceiling_le_one

  less_ceiling_eq_number_of  ~> number_of_less_ceiling

  less_ceiling_eq_zero       ~> zero_less_ceiling

  less_ceiling_eq_one        ~> one_less_ceiling

  ceiling_less_eq_number_of  ~> ceiling_less_number_of

  ceiling_less_eq_zero       ~> ceiling_less_zero

  ceiling_less_eq_one        ~> ceiling_less_one

  le_ceiling_eq_number_of    ~> number_of_le_ceiling

  le_ceiling_eq_zero         ~> zero_le_ceiling

  le_ceiling_eq_one          ~> one_le_ceiling

  ceiling_subtract_number_of ~> ceiling_diff_number_of

  ceiling_subtract_one       ~> ceiling_diff_one

* Theory "Finite_Set": various folding_XXX locales facilitate the

application of the various fold combinators on finite sets.

* Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"

provides abstract red-black tree type which is backed by "RBT_Impl" as

implementation.  INCOMPATIBILTY.

* Theory Library/Coinductive_List has been removed -- superseded by

AFP/thys/Coinductive.

* Theory PReal, including the type "preal" and related operations, has

been removed.  INCOMPATIBILITY.

* Split off theory "Big_Operators" containing setsum, setprod,

Inf_fin, Sup_fin, Min, Max from theory Finite_Set.  INCOMPATIBILITY.

* Theory "Rational" renamed to "Rat", for consistency with "Nat",

"Int" etc.  INCOMPATIBILITY.

* Constant Rat.normalize needs to be qualified.  INCOMPATIBILITY.

* New set of rules "ac_simps" provides combined assoc / commute

rewrites for all interpretations of the appropriate generic locales.

* Renamed theory "OrderedGroup" to "Groups" and split theory

"Ring_and_Field" into theories "Rings" and "Fields"; for more

appropriate and more consistent names suitable for name prefixes

within the HOL theories.  INCOMPATIBILITY.

* Some generic constants have been put to appropriate theories:

  - less_eq, less: Orderings

  - zero, one, plus, minus, uminus, times, abs, sgn: Groups

  - inverse, divide: Rings

INCOMPATIBILITY.

* More consistent naming of type classes involving orderings (and

lattices):

    lower_semilattice                   ~> semilattice_inf

    upper_semilattice                   ~> semilattice_sup

    dense_linear_order                  ~> dense_linorder

    pordered_ab_group_add               ~> ordered_ab_group_add

    pordered_ab_group_add_abs           ~> ordered_ab_group_add_abs

    pordered_ab_semigroup_add           ~> ordered_ab_semigroup_add

    pordered_ab_semigroup_add_imp_le    ~> ordered_ab_semigroup_add_imp_le

    pordered_cancel_ab_semigroup_add    ~> ordered_cancel_ab_semigroup_add

    pordered_cancel_comm_semiring       ~> ordered_cancel_comm_semiring

    pordered_cancel_semiring            ~> ordered_cancel_semiring

    pordered_comm_monoid_add            ~> ordered_comm_monoid_add

    pordered_comm_ring                  ~> ordered_comm_ring

    pordered_comm_semiring              ~> ordered_comm_semiring

    pordered_ring                       ~> ordered_ring

    pordered_ring_abs                   ~> ordered_ring_abs

    pordered_semiring                   ~> ordered_semiring

    ordered_ab_group_add                ~> linordered_ab_group_add

    ordered_ab_semigroup_add            ~> linordered_ab_semigroup_add

    ordered_cancel_ab_semigroup_add     ~> linordered_cancel_ab_semigroup_add

    ordered_comm_semiring_strict        ~> linordered_comm_semiring_strict

    ordered_field                       ~> linordered_field

    ordered_field_no_lb                 ~> linordered_field_no_lb

    ordered_field_no_ub                 ~> linordered_field_no_ub

    ordered_field_dense_linear_order    ~> dense_linordered_field

    ordered_idom                        ~> linordered_idom

    ordered_ring                        ~> linordered_ring

    ordered_ring_le_cancel_factor       ~> linordered_ring_le_cancel_factor

    ordered_ring_less_cancel_factor     ~> linordered_ring_less_cancel_factor

    ordered_ring_strict                 ~> linordered_ring_strict

    ordered_semidom                     ~> linordered_semidom

    ordered_semiring                    ~> linordered_semiring

    ordered_semiring_1                  ~> linordered_semiring_1

    ordered_semiring_1_strict           ~> linordered_semiring_1_strict

    ordered_semiring_strict             ~> linordered_semiring_strict

  The following slightly odd type classes have been moved to a

  separate theory Library/Lattice_Algebras:

    lordered_ab_group_add               ~> lattice_ab_group_add

    lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs

    lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add

    lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add

    lordered_ring                       ~> lattice_ring

INCOMPATIBILITY.

* Refined field classes:

  - classes division_ring_inverse_zero, field_inverse_zero,

    linordered_field_inverse_zero include rule inverse 0 = 0 --

    subsumes former division_by_zero class;

  - numerous lemmas have been ported from field to division_ring.

INCOMPATIBILITY.

* Refined algebra theorem collections:

  - dropped theorem group group_simps, use algebra_simps instead;

  - dropped theorem group ring_simps, use field_simps instead;

  - proper theorem collection field_simps subsumes former theorem

    groups field_eq_simps and field_simps;

  - dropped lemma eq_minus_self_iff which is a duplicate for

    equal_neg_zero.

INCOMPATIBILITY.

* Theory Finite_Set and List: some lemmas have been generalized from

sets to lattices:

  fun_left_comm_idem_inter      ~> fun_left_comm_idem_inf

  fun_left_comm_idem_union      ~> fun_left_comm_idem_sup

  inter_Inter_fold_inter        ~> inf_Inf_fold_inf

  union_Union_fold_union        ~> sup_Sup_fold_sup

  Inter_fold_inter              ~> Inf_fold_inf

  Union_fold_union              ~> Sup_fold_sup

  inter_INTER_fold_inter        ~> inf_INFI_fold_inf

  union_UNION_fold_union        ~> sup_SUPR_fold_sup

  INTER_fold_inter              ~> INFI_fold_inf

  UNION_fold_union              ~> SUPR_fold_sup

* Theory "Complete_Lattice": lemmas top_def and bot_def have been

replaced by the more convenient lemmas Inf_empty and Sup_empty.

Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed

by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace

former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right

subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.

* Reorganized theory Multiset: swapped notation of pointwise and

multiset order:

  - pointwise ordering is instance of class order with standard syntax

    <= and <;

  - multiset ordering has syntax <=# and <#; partial order properties

    are provided by means of interpretation with prefix

    multiset_order;

  - less duplication, less historical organization of sections,

    conversion from associations lists to multisets, rudimentary code

    generation;

  - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,

    if needed.

Renamed:

  multiset_eq_conv_count_eq  ~>  multiset_ext_iff

  multi_count_ext  ~>  multiset_ext

  diff_union_inverse2  ~>  diff_union_cancelR

INCOMPATIBILITY.

* Theory Permutation: replaced local "remove" by List.remove1.

* Code generation: ML and OCaml code is decorated with signatures.

* Theory List: added transpose.

* Library/Nat_Bijection.thy is a collection of bijective functions

between nat and other types, which supersedes the older libraries

Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy.  INCOMPATIBILITY.

  Constants:

  Nat_Int_Bij.nat2_to_nat         ~> prod_encode

  Nat_Int_Bij.nat_to_nat2         ~> prod_decode

  Nat_Int_Bij.int_to_nat_bij      ~> int_encode

  Nat_Int_Bij.nat_to_int_bij      ~> int_decode

  Countable.pair_encode           ~> prod_encode

  NatIso.prod2nat                 ~> prod_encode

  NatIso.nat2prod                 ~> prod_decode

  NatIso.sum2nat                  ~> sum_encode

  NatIso.nat2sum                  ~> sum_decode

  NatIso.list2nat                 ~> list_encode

  NatIso.nat2list                 ~> list_decode

  NatIso.set2nat                  ~> set_encode

  NatIso.nat2set                  ~> set_decode

  Lemmas:

  Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_decode

  Nat_Int_Bij.nat2_to_nat_inj     ~> inj_prod_encode

  Nat_Int_Bij.nat2_to_nat_surj    ~> surj_prod_encode

  Nat_Int_Bij.nat_to_nat2_inj     ~> inj_prod_decode

  Nat_Int_Bij.nat_to_nat2_surj    ~> surj_prod_decode

  Nat_Int_Bij.i2n_n2i_id          ~> int_encode_inverse

  Nat_Int_Bij.n2i_i2n_id          ~> int_decode_inverse

  Nat_Int_Bij.surj_nat_to_int_bij ~> surj_int_encode

  Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode

  Nat_Int_Bij.inj_nat_to_int_bij  ~> inj_int_encode

  Nat_Int_Bij.inj_int_to_nat_bij  ~> inj_int_decode

  Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_encode

  Nat_Int_Bij.bij_int_to_nat_bij  ~> bij_int_decode

* Sledgehammer:

  - Renamed ATP commands:

    atp_info     ~> sledgehammer running_atps

    atp_kill     ~> sledgehammer kill_atps

    atp_messages ~> sledgehammer messages

    atp_minimize ~> sledgehammer minimize

    print_atps   ~> sledgehammer available_atps

    INCOMPATIBILITY.

  - Added user's manual ("isabelle doc sledgehammer").

  - Added option syntax and "sledgehammer_params" to customize

    Sledgehammer's behavior.  See the manual for details.

  - Modified the Isar proof reconstruction code so that it produces

    direct proofs rather than proofs by contradiction.  (This feature

    is still experimental.)

  - Made Isar proof reconstruction work for SPASS, remote ATPs, and in

    full-typed mode.

  - Added support for TPTP syntax for SPASS via the "spass_tptp" ATP.

* Nitpick:

  - Added and implemented "binary_ints" and "bits" options.

  - Added "std" option and implemented support for nonstandard models.

  - Added and implemented "finitize" option to improve the precision

    of infinite datatypes based on a monotonicity analysis.

  - Added support for quotient types.

  - Added support for "specification" and "ax_specification"

    constructs.

  - Added support for local definitions (for "function" and

    "termination" proofs).

  - Added support for term postprocessors.

  - Optimized "Multiset.multiset" and "FinFun.finfun".

  - Improved efficiency of "destroy_constrs" optimization.

  - Fixed soundness bugs related to "destroy_constrs" optimization and

    record getters.

  - Fixed soundness bug related to higher-order constructors.

  - Fixed soundness bug when "full_descrs" is enabled.

  - Improved precision of set constructs.

  - Added "atoms" option.

  - Added cache to speed up repeated Kodkod invocations on the same

    problems.

  - Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and

    "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and

    "SAT4J_Light".  INCOMPATIBILITY.

  - Removed "skolemize", "uncurry", "sym_break", "flatten_prop",

    "sharing_depth", and "show_skolems" options.  INCOMPATIBILITY.

  - Removed "nitpick_intro" attribute.  INCOMPATIBILITY.

*** HOLCF ***

* Variable names in lemmas generated by the domain package have

changed; the naming scheme is now consistent with the HOL datatype

package.  Some proof scripts may be affected, INCOMPATIBILITY.

* The domain package no longer defines the function "foo_copy" for

recursive domain "foo".  The reach lemma is now stated directly in

terms of "foo_take".  Lemmas and proofs that mention "foo_copy" must

be reformulated in terms of "foo_take", INCOMPATIBILITY.

* Most definedness lemmas generated by the domain package (previously

of the form "x ~= UU ==> foo$x ~= UU") now have an if-and-only-if form

like "foo$x = UU <-> x = UU", which works better as a simp rule.

Proofs that used definedness lemmas as intro rules may break,

potential INCOMPATIBILITY.

* Induction and casedist rules generated by the domain package now

declare proper case_names (one called "bottom", and one named for each

constructor).  INCOMPATIBILITY.

* For mutually-recursive domains, separate "reach" and "take_lemma"

rules are generated for each domain, INCOMPATIBILITY.

  foo_bar.reach       ~> foo.reach  bar.reach

  foo_bar.take_lemmas ~> foo.take_lemma  bar.take_lemma

* Some lemmas generated by the domain package have been renamed for

consistency with the datatype package, INCOMPATIBILITY.

  foo.ind        ~> foo.induct

  foo.finite_ind ~> foo.finite_induct

  foo.coind      ~> foo.coinduct

  foo.casedist   ~> foo.exhaust

  foo.exhaust    ~> foo.nchotomy

* For consistency with other definition packages, the fixrec package

now generates qualified theorem names, INCOMPATIBILITY.

  foo_simps  ~> foo.simps

  foo_unfold ~> foo.unfold

  foo_induct ~> foo.induct

* The "fixrec_simp" attribute has been removed.  The "fixrec_simp"

method and internal fixrec proofs now use the default simpset instead.

INCOMPATIBILITY.

* The "contlub" predicate has been removed.  Proof scripts should use

lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY.

* The "admw" predicate has been removed, INCOMPATIBILITY.

* The constants cpair, cfst, and csnd have been removed in favor of

Pair, fst, and snd from Isabelle/HOL, INCOMPATIBILITY.

*** ML ***

* Antiquotations for basic formal entities:

    @{class NAME}         -- type class

    @{class_syntax NAME}  -- syntax representation of the above

    @{type_name NAME}     -- logical type

    @{type_abbrev NAME}   -- type abbreviation

    @{nonterminal NAME}   -- type of concrete syntactic category

    @{type_syntax NAME}   -- syntax representation of any of the above

    @{const_name NAME}    -- logical constant (INCOMPATIBILITY)

    @{const_abbrev NAME}  -- abbreviated constant

    @{const_syntax NAME}  -- syntax representation of any of the above

* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw

syntax constant (cf. 'syntax' command).

* Antiquotation @{make_string} inlines a function to print arbitrary

values similar to the ML toplevel.  The result is compiler dependent

and may fall back on "?" in certain situations.

* Diagnostic commands 'ML_val' and 'ML_command' may refer to

antiquotations @{Isar.state} and @{Isar.goal}.  This replaces impure

Isar.state() and Isar.goal(), which belong to the old TTY loop and do

not work with the asynchronous Isar document model.

* Configuration options now admit dynamic default values, depending on

the context or even global references.

* SHA1.digest digests strings according to SHA-1 (see RFC 3174).  It

uses an efficient external library if available (for Poly/ML).

* Renamed some important ML structures, while keeping the old names

for some time as aliases within the structure Legacy:

  OuterKeyword  ~>  Keyword

  OuterLex      ~>  Token

  OuterParse    ~>  Parse

  OuterSyntax   ~>  Outer_Syntax

  PrintMode     ~>  Print_Mode

  SpecParse     ~>  Parse_Spec

  ThyInfo       ~>  Thy_Info

  ThyLoad       ~>  Thy_Load

  ThyOutput     ~>  Thy_Output

  TypeInfer     ~>  Type_Infer

Note that "open Legacy" simplifies porting of sources, but forgetting

to remove it again will complicate porting again in the future.

* Most operations that refer to a global context are named

accordingly, e.g. Simplifier.global_context or

ProofContext.init_global.  There are some situations where a global

context actually works, but under normal circumstances one needs to

pass the proper local context through the code!

* Discontinued old TheoryDataFun with its copy/init operation -- data

needs to be pure.  Functor Theory_Data_PP retains the traditional

Pretty.pp argument to merge, which is absent in the standard

Theory_Data version.

* Sorts.certify_sort and derived "cert" operations for types and terms

no longer minimize sorts.  Thus certification at the boundary of the

inference kernel becomes invariant under addition of class relations,

which is an important monotonicity principle.  Sorts are now minimized

in the syntax layer only, at the boundary between the end-user and the

system.  Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort

explicitly in rare situations.

* Renamed old-style Drule.standard to Drule.export_without_context, to

emphasize that this is in no way a standard operation.

INCOMPATIBILITY.

* Subgoal.FOCUS (and variants): resulting goal state is normalized as

usual for resolution.  Rare INCOMPATIBILITY.

* Renamed varify/unvarify operations to varify_global/unvarify_global

to emphasize that these only work in a global situation (which is

quite rare).

* Curried take and drop in library.ML; negative length is interpreted

as infinity (as in chop).  Subtle INCOMPATIBILITY.

* Proof terms: type substitutions on proof constants now use canonical

order of type variables.  INCOMPATIBILITY for tools working with proof

terms.

* Raw axioms/defs may no longer carry sort constraints, and raw defs

may no longer carry premises.  User-level specifications are

transformed accordingly by Thm.add_axiom/add_def.

*** System ***

* Discontinued special HOL_USEDIR_OPTIONS for the main HOL image;

ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions.  Note that

proof terms are enabled unconditionally in the new HOL-Proofs image.

* Discontinued old ISABELLE and ISATOOL environment settings (legacy

feature since Isabelle2009).  Use ISABELLE_PROCESS and ISABELLE_TOOL,

respectively.

* Old lib/scripts/polyml-platform is superseded by the

ISABELLE_PLATFORM setting variable, which defaults to the 32 bit

variant, even on a 64 bit machine.  The following example setting

prefers 64 bit if available:

  ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"

* The preliminary Isabelle/jEdit application demonstrates the emerging

Isabelle/Scala layer for advanced prover interaction and integration.

See src/Tools/jEdit or "isabelle jedit" provided by the properly built

component.

New in Isabelle2009-1 (December 2009)

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

*** General ***

* Discontinued old form of "escaped symbols" such as \\<forall>.  Only

one backslash should be used, even in ML sources.

*** Pure ***

* Locale interpretation propagates mixins along the locale hierarchy.

The currently only available mixins are the equations used to map

local definitions to terms of the target domain of an interpretation.

* Reactivated diagnostic command 'print_interps'.  Use "print_interps

loc" to print all interpretations of locale "loc" in the theory.

Interpretations in proofs are not shown.

* Thoroughly revised locales tutorial.  New section on conditional

interpretation.

* On instantiation of classes, remaining undefined class parameters

are formally declared.  INCOMPATIBILITY.

*** Document preparation ***

* New generalized style concept for printing terms: @{foo (style) ...}

instead of @{foo_style style ...}  (old form is still retained for

backward compatibility).  Styles can be also applied for

antiquotations prop, term_type and typeof.

*** HOL ***

* New proof method "smt" for a combination of first-order logic with

equality, linear and nonlinear (natural/integer/real) arithmetic, and

fixed-size bitvectors; there is also basic support for higher-order

features (esp. lambda abstractions).  It is an incomplete decision

procedure based on external SMT solvers using the oracle mechanism;

for the SMT solver Z3, this method is proof-producing.  Certificates

are provided to avoid calling the external solvers solely for

re-checking proofs.  Due to a remote SMT service there is no need for

installing SMT solvers locally.  See src/HOL/SMT.

* New commands to load and prove verification conditions generated by

the Boogie program verifier or derived systems (e.g. the Verifying C

Compiler (VCC) or Spec#).  See src/HOL/Boogie.

* New counterexample generator tool 'nitpick' based on the Kodkod

relational model finder.  See src/HOL/Tools/Nitpick and

src/HOL/Nitpick_Examples.

* New commands 'code_pred' and 'values' to invoke the predicate

compiler and to enumerate values of inductive predicates.

* A tabled implementation of the reflexive transitive closure.

* New implementation of quickcheck uses generic code generator;

default generators are provided for all suitable HOL types, records

and datatypes.  Old quickcheck can be re-activated importing theory

Library/SML_Quickcheck.

* New testing tool Mirabelle for automated proof tools.  Applies

several tools and tactics like sledgehammer, metis, or quickcheck, to

every proof step in a theory.  To be used in batch mode via the

"mirabelle" utility.

* New proof method "sos" (sum of squares) for nonlinear real

arithmetic (originally due to John Harison). It requires theory

Library/Sum_Of_Squares.  It is not a complete decision procedure but

works well in practice on quantifier-free real arithmetic with +, -,

*, ^, =, <= and <, i.e. boolean combinations of equalities and

inequalities between polynomials.  It makes use of external

semidefinite programming solvers.  Method "sos" generates a

certificate that can be pasted into the proof thus avoiding the need

to call an external tool every time the proof is checked.  See

src/HOL/Library/Sum_Of_Squares.

* New method "linarith" invokes existing linear arithmetic decision

procedure only.

* New command 'atp_minimal' reduces result produced by Sledgehammer.

* New Sledgehammer option "Full Types" in Proof General settings menu.

Causes full type information to be output to the ATPs.  This slows

ATPs down considerably but eliminates a source of unsound "proofs"

that fail later.

* New method "metisFT": A version of metis that uses full type

information in order to avoid failures of proof reconstruction.

* New evaluator "approximate" approximates an real valued term using

the same method as the approximation method.

* Method "approximate" now supports arithmetic expressions as

boundaries of intervals and implements interval splitting and Taylor

series expansion.

* ML antiquotation @{code_datatype} inserts definition of a datatype

generated by the code generator; e.g. see src/HOL/Predicate.thy.

* New theory SupInf of the supremum and infimum operators for sets of

reals.

* New theory Probability, which contains a development of measure

theory, eventually leading to Lebesgue integration and probability.

* Extended Multivariate Analysis to include derivation and Brouwer's

fixpoint theorem.

* Reorganization of number theory, INCOMPATIBILITY:

  - new number theory development for nat and int, in theories Divides

    and GCD as well as in new session Number_Theory

  - some constants and facts now suffixed with _nat and _int

    accordingly

  - former session NumberTheory now named Old_Number_Theory, including

    theories Legacy_GCD and Primes (prefer Number_Theory if possible)

  - moved theory Pocklington from src/HOL/Library to

    src/HOL/Old_Number_Theory

* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and

lcm of finite and infinite sets. It is shown that they form a complete

lattice.

* Class semiring_div requires superclass no_zero_divisors and proof of

div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,

div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been

generalized to class semiring_div, subsuming former theorems

zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and

zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.

INCOMPATIBILITY.

* Refinements to lattice classes and sets:

  - less default intro/elim rules in locale variant, more default

    intro/elim rules in class variant: more uniformity

  - lemma ge_sup_conv renamed to le_sup_iff, in accordance with

    le_inf_iff

  - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and

    sup_aci)

  - renamed ACI to inf_sup_aci

  - new class "boolean_algebra"

  - class "complete_lattice" moved to separate theory

    "Complete_Lattice"; corresponding constants (and abbreviations)

    renamed and with authentic syntax:

    Set.Inf ~>    Complete_Lattice.Inf

    Set.Sup ~>    Complete_Lattice.Sup

    Set.INFI ~>   Complete_Lattice.INFI

    Set.SUPR ~>   Complete_Lattice.SUPR

    Set.Inter ~>  Complete_Lattice.Inter

    Set.Union ~>  Complete_Lattice.Union

    Set.INTER ~>  Complete_Lattice.INTER

    Set.UNION ~>  Complete_Lattice.UNION

  - authentic syntax for

    Set.Pow

    Set.image

  - mere abbreviations:

    Set.empty               (for bot)

    Set.UNIV                (for top)

    Set.inter               (for inf, formerly Set.Int)

    Set.union               (for sup, formerly Set.Un)

    Complete_Lattice.Inter  (for Inf)

    Complete_Lattice.Union  (for Sup)

    Complete_Lattice.INTER  (for INFI)

    Complete_Lattice.UNION  (for SUPR)

  - object-logic definitions as far as appropriate

INCOMPATIBILITY.  Care is required when theorems Int_subset_iff or

Un_subset_iff are explicitly deleted as default simp rules; then also

their lattice counterparts le_inf_iff and le_sup_iff have to be

deleted to achieve the desired effect.

* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp

rules by default any longer; the same applies to min_max.inf_absorb1

etc.  INCOMPATIBILITY.

* Rules sup_Int_eq and sup_Un_eq are no longer declared as

pred_set_conv by default.  INCOMPATIBILITY.

* Power operations on relations and functions are now one dedicated

constant "compow" with infix syntax "^^".  Power operation on

multiplicative monoids retains syntax "^" and is now defined generic

in class power.  INCOMPATIBILITY.

* Relation composition "R O S" now has a more standard argument order:

"R O S = {(x, z). EX y. (x, y) : R & (y, z) : S}".  INCOMPATIBILITY,

rewrite propositions with "S O R" --> "R O S". Proofs may occasionally

break, since the O_assoc rule was not rewritten like this.  Fix using

O_assoc[symmetric].  The same applies to the curried version "R OO S".

* Function "Inv" is renamed to "inv_into" and function "inv" is now an

abbreviation for "inv_into UNIV".  Lemmas are renamed accordingly.

INCOMPATIBILITY.

* Most rules produced by inductive and datatype package have mandatory

prefixes.  INCOMPATIBILITY.

* Changed "DERIV_intros" to a dynamic fact, which can be augmented by

the attribute of the same name.  Each of the theorems in the list

DERIV_intros assumes composition with an additional function and

matches a variable to the derivative, which has to be solved by the

Simplifier.  Hence (auto intro!: DERIV_intros) computes the derivative

of most elementary terms.  Former Maclauren.DERIV_tac and

Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros).

INCOMPATIBILITY.

* Code generator attributes follow the usual underscore convention:

    code_unfold     replaces    code unfold

    code_post       replaces    code post

    etc.

  INCOMPATIBILITY.

* Renamed methods:

    sizechange -> size_change

    induct_scheme -> induction_schema

  INCOMPATIBILITY.

* Discontinued abbreviation "arbitrary" of constant "undefined".

INCOMPATIBILITY, use "undefined" directly.

* Renamed theorems:

    Suc_eq_add_numeral_1 -> Suc_eq_plus1

    Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left

    Suc_plus1 -> Suc_eq_plus1

    *anti_sym -> *antisym*

    vector_less_eq_def -> vector_le_def

  INCOMPATIBILITY.

* Added theorem List.map_map as [simp].  Removed List.map_compose.

INCOMPATIBILITY.

* Removed predicate "M hassize n" (<--> card M = n & finite M).

INCOMPATIBILITY.

*** HOLCF ***

* Theory Representable defines a class "rep" of domains that are

representable (via an ep-pair) in the universal domain type "udom".

Instances are provided for all type constructors defined in HOLCF.

* The 'new_domain' command is a purely definitional version of the

domain package, for representable domains.  Syntax is identical to the

old domain package.  The 'new_domain' package also supports indirect

recursion using previously-defined type constructors.  See

src/HOLCF/ex/New_Domain.thy for examples.

* Method "fixrec_simp" unfolds one step of a fixrec-defined constant

on the left-hand side of an equation, and then performs

simplification.  Rewriting is done using rules declared with the

"fixrec_simp" attribute.  The "fixrec_simp" method is intended as a

replacement for "fixpat"; see src/HOLCF/ex/Fixrec_ex.thy for examples.

* The pattern-match compiler in 'fixrec' can now handle constructors

with HOL function types.  Pattern-match combinators for the Pair

constructor are pre-configured.

* The 'fixrec' package now produces better fixed-point induction rules

for mutually-recursive definitions:  Induction rules have conclusions

of the form "P foo bar" instead of "P <foo, bar>".

* The constant "sq_le" (with infix syntax "<<" or "\<sqsubseteq>") has

been renamed to "below".  The name "below" now replaces "less" in many

theorem names.  (Legacy theorem names using "less" are still supported

as well.)

* The 'fixrec' package now supports "bottom patterns".  Bottom

patterns can be used to generate strictness rules, or to make

functions more strict (much like the bang-patterns supported by the

Glasgow Haskell Compiler).  See src/HOLCF/ex/Fixrec_ex.thy for

examples.

*** ML ***

* Support for Poly/ML 5.3.0, with improved reporting of compiler

errors and run-time exceptions, including detailed source positions.

* Structure Name_Space (formerly NameSpace) now manages uniquely

identified entries, with some additional information such as source

position, logical grouping etc.

* Theory and context data is now introduced by the simplified and

modernized functors Theory_Data, Proof_Data, Generic_Data.  Data needs

to be pure, but the old TheoryDataFun for mutable data (with explicit

copy operation) is still available for some time.

* Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML)

provides a high-level programming interface to synchronized state

variables with atomic update.  This works via pure function

application within a critical section -- its runtime should be as

short as possible; beware of deadlocks if critical code is nested,

either directly or indirectly via other synchronized variables!

* Structure Unsynchronized (cf. src/Pure/ML-Systems/unsynchronized.ML)

wraps raw ML references, explicitly indicating their non-thread-safe

behaviour.  The Isar toplevel keeps this structure open, to

accommodate Proof General as well as quick and dirty interactive

experiments with references.

* PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for

parallel tactical reasoning.

* Tacticals Subgoal.FOCUS, Subgoal.FOCUS_PREMS, Subgoal.FOCUS_PARAMS

are similar to SUBPROOF, but are slightly more flexible: only the

specified parts of the subgoal are imported into the context, and the

body tactic may introduce new subgoals and schematic variables.

* Old tactical METAHYPS, which does not observe the proof context, has

been renamed to Old_Goals.METAHYPS and awaits deletion.  Use SUBPROOF

or Subgoal.FOCUS etc.

* Renamed functor TableFun to Table, and GraphFun to Graph.  (Since

functors have their own ML name space there is no point to mark them

separately.)  Minor INCOMPATIBILITY.

* Renamed NamedThmsFun to Named_Thms.  INCOMPATIBILITY.

* Renamed several structures FooBar to Foo_Bar.  Occasional,

INCOMPATIBILITY.

* Operations of structure Skip_Proof no longer require quick_and_dirty

mode, which avoids critical setmp.

* Eliminated old Attrib.add_attributes, Method.add_methods and related

combinators for "args".  INCOMPATIBILITY, need to use simplified

Attrib/Method.setup introduced in Isabelle2009.

* Proper context for simpset_of, claset_of, clasimpset_of.  May fall

back on global_simpset_of, global_claset_of, global_clasimpset_of as

last resort.  INCOMPATIBILITY.

* Display.pretty_thm now requires a proper context (cf. former

ProofContext.pretty_thm).  May fall back on Display.pretty_thm_global

or even Display.pretty_thm_without_context as last resort.

INCOMPATIBILITY.

* Discontinued Display.pretty_ctyp/cterm etc.  INCOMPATIBILITY, use

Syntax.pretty_typ/term directly, preferably with proper context

instead of global theory.

*** System ***

* Further fine tuning of parallel proof checking, scales up to 8 cores

(max. speedup factor 5.0).  See also Goal.parallel_proofs in ML and

usedir option -q.