Isabelle NEWS -- history user-relevant changes

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

New in this Isabelle version

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

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

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

discontinued (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.

*** Pure ***

* Code generator: simple concept for abstract datatypes obeying invariants.

* 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)"

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

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

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

* Command 'typedecl' now works within a local theory context --

without introducing dependencies on parameters or assumptions, which

is not possible in Isabelle/Pure.

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

order of type variables. INCOMPATIBILITY: Tools working with proof

terms may need to be adapted.

*** HOL ***

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

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

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

AFP/thys/Coinductive.

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

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

* Class division_ring also requires proof of fact divide_inverse.  However instantiation

of parameter divide has also been required previously.  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.thy:

    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.

* HOLogic.strip_psplit: types are returned in syntactic order, similar

to other strip and tuple operations.  INCOMPATIBILITY.

* Various old-style primrec specifications in the HOL theories have been

replaced by new-style primrec, especially in theory List.  The corresponding

constants now have authentic syntax.  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.

INCOMPATIBILITY.

* Reorganized theory Sum_Type; Inl and Inr now have authentic syntax.

INCOMPATIBILITY.

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

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

* 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 List: added transpose.

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

clash with new theory Quotient in Main HOL.

* 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

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

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

emphasize that this is in no way a standard operation.

INCOMPATIBILITY.

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

as infinity (as in chop).  INCOMPATIBILITY.

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

usual for resolution.  Rare INCOMPATIBILITY.

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

* Renamed varify/unvarify operations to varify_global/unvarify_global

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

quite rare).

* Configuration options now admit dynamic default values, depending on

the context or even global references.

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

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.

* Support for additional "Isabelle components" via etc/components, see

also the system manual.

* The isabelle makeall tool now operates on all components with

IsaMakefile, not just hardwired "logics".

* Removed "compress" option from isabelle-process and isabelle usedir;

this is always enabled.

* Discontinued support for Poly/ML 4.x versions.

* Isabelle tool "wwwfind" provides web interface for 'find_theorems'

on a given logic image.  This requires the lighttpd webserver and is

currently supported on Linux only.

New in Isabelle2009 (April 2009)

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

*** General ***

* Simplified main Isabelle executables, with less surprises on

case-insensitive file-systems (such as Mac OS).

  - The main Isabelle tool wrapper is now called "isabelle" instead of

    "isatool."

  - The former "isabelle" alias for "isabelle-process" has been

    removed (should rarely occur to regular users).

  - The former "isabelle-interface" and its alias "Isabelle" have been

    removed (interfaces are now regular Isabelle tools).

Within scripts and make files, the Isabelle environment variables

ISABELLE_TOOL and ISABELLE_PROCESS replace old ISATOOL and ISABELLE,

respectively.  (The latter are still available as legacy feature.)

The old isabelle-interface wrapper could react in confusing ways if

the interface was uninstalled or changed otherwise.  Individual

interface tool configuration is now more explicit, see also the

Isabelle system manual.  In particular, Proof General is now available

via "isabelle emacs".

INCOMPATIBILITY, need to adapt derivative scripts.  Users may need to

purge installed copies of Isabelle executables and re-run "isabelle

install -p ...", or use symlinks.

* The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the

old ~/isabelle, which was slightly non-standard and apt to cause

surprises on case-insensitive file-systems (such as Mac OS).

INCOMPATIBILITY, need to move existing ~/isabelle/etc,

~/isabelle/heaps, ~/isabelle/browser_info to the new place.  Special

care is required when using older releases of Isabelle.  Note that

ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any

Isabelle distribution, in order to use the new ~/.isabelle uniformly.

* Proofs of fully specified statements are run in parallel on

multi-core systems.  A speedup factor of 2.5 to 3.2 can be expected on

a regular 4-core machine, if the initial heap space is made reasonably

large (cf. Poly/ML option -H).  (Requires Poly/ML 5.2.1 or later.)

* The main reference manuals ("isar-ref", "implementation", and

"system") have been updated and extended.  Formally checked references

as hyperlinks are now available uniformly.

*** Pure ***

* Complete re-implementation of locales.  INCOMPATIBILITY in several

respects.  The most important changes are listed below.  See the

Tutorial on Locales ("locales" manual) for details.

- In locale expressions, instantiation replaces renaming.  Parameters

must be declared in a for clause.  To aid compatibility with previous

parameter inheritance, in locale declarations, parameters that are not

'touched' (instantiation position "_" or omitted) are implicitly added

with their syntax at the beginning of the for clause.

- Syntax from abbreviations and definitions in locales is available in

locale expressions and context elements.  The latter is particularly

useful in locale declarations.

- More flexible mechanisms to qualify names generated by locale

expressions.  Qualifiers (prefixes) may be specified in locale

expressions, and can be marked as mandatory (syntax: "name!:") or

optional (syntax "name?:").  The default depends for plain "name:"

depends on the situation where a locale expression is used: in

commands 'locale' and 'sublocale' prefixes are optional, in

'interpretation' and 'interpret' prefixes are mandatory.  The old

implicit qualifiers derived from the parameter names of a locale are

no longer generated.

- Command "sublocale l < e" replaces "interpretation l < e".  The

instantiation clause in "interpretation" and "interpret" (square

brackets) is no longer available.  Use locale expressions.

- When converting proof scripts, mandatory qualifiers in

'interpretation' and 'interpret' should be retained by default, even

if this is an INCOMPATIBILITY compared to former behavior.  In the

worst case, use the "name?:" form for non-mandatory ones.  Qualifiers

in locale expressions range over a single locale instance only.

- Dropped locale element "includes".  This is a major INCOMPATIBILITY.

In existing theorem specifications replace the includes element by the

respective context elements of the included locale, omitting those

that are already present in the theorem specification.  Multiple

assume elements of a locale should be replaced by a single one

involving the locale predicate.  In the proof body, declarations (most

notably theorems) may be regained by interpreting the respective

locales in the proof context as required (command "interpret").

If using "includes" in replacement of a target solely because the

parameter types in the theorem are not as general as in the target,

consider declaring a new locale with additional type constraints on

the parameters (context element "constrains").

- Discontinued "locale (open)".  INCOMPATIBILITY.

- Locale interpretation commands no longer attempt to simplify goal.

INCOMPATIBILITY: in rare situations the generated goal differs.  Use

methods intro_locales and unfold_locales to clarify.

- Locale interpretation commands no longer accept interpretation

attributes.  INCOMPATIBILITY.

* Class declaration: so-called "base sort" must not be given in import

list any longer, but is inferred from the specification.  Particularly

in HOL, write

    class foo = ...

instead of

    class foo = type + ...

* Class target: global versions of theorems stemming do not carry a

parameter prefix any longer.  INCOMPATIBILITY.

* Class 'instance' command no longer accepts attached definitions.

INCOMPATIBILITY, use proper 'instantiation' target instead.

* Recovered hiding of consts, which was accidentally broken in

Isabelle2007.  Potential INCOMPATIBILITY, ``hide const c'' really

makes c inaccessible; consider using ``hide (open) const c'' instead.

* Slightly more coherent Pure syntax, with updated documentation in

isar-ref manual.  Removed locales meta_term_syntax and

meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent,

INCOMPATIBILITY in rare situations.  Note that &&& should not be used

directly in regular applications.

* There is a new syntactic category "float_const" for signed decimal

fractions (e.g. 123.45 or -123.45).

* Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML

interface with 'setup' command instead.

* Command 'local_setup' is similar to 'setup', but operates on a local

theory context.

* The 'axiomatization' command now only works within a global theory

context.  INCOMPATIBILITY.

* Goal-directed proof now enforces strict proof irrelevance wrt. sort

hypotheses.  Sorts required in the course of reasoning need to be

covered by the constraints in the initial statement, completed by the

type instance information of the background theory.  Non-trivial sort

hypotheses, which rarely occur in practice, may be specified via

vacuous propositions of the form SORT_CONSTRAINT('a::c).  For example:

  lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ...

The result contains an implicit sort hypotheses as before --

SORT_CONSTRAINT premises are eliminated as part of the canonical rule

normalization.

* Generalized Isar history, with support for linear undo, direct state

addressing etc.

* Changed defaults for unify configuration options:

  unify_trace_bound = 50 (formerly 25)

  unify_search_bound = 60 (formerly 30)

* Different bookkeeping for code equations (INCOMPATIBILITY):

  a) On theory merge, the last set of code equations for a particular

     constant is taken (in accordance with the policy applied by other

     parts of the code generator framework).

  b) Code equations stemming from explicit declarations (e.g. code

     attribute) gain priority over default code equations stemming

     from definition, primrec, fun etc.

* Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.

* Unified theorem tables for both code generators.  Thus [code

func] has disappeared and only [code] remains.  INCOMPATIBILITY.

* Command 'find_consts' searches for constants based on type and name

patterns, e.g.

    find_consts "_ => bool"

By default, matching is against subtypes, but it may be restricted to

the whole type.  Searching by name is possible.  Multiple queries are

conjunctive and queries may be negated by prefixing them with a

hyphen:

    find_consts strict: "_ => bool" name: "Int" -"int => int"

* New 'find_theorems' criterion "solves" matches theorems that

directly solve the current goal (modulo higher-order unification).

* Auto solve feature for main theorem statements: whenever a new goal

is stated, "find_theorems solves" is called; any theorems that could

solve the lemma directly are listed as part of the goal state.

Cf. associated options in Proof General Isabelle settings menu,

enabled by default, with reasonable timeout for pathological cases of

higher-order unification.

*** Document preparation ***

* Antiquotation @{lemma} now imitates a regular terminal proof,

demanding keyword 'by' and supporting the full method expression

syntax just like the Isar command 'by'.

*** HOL ***

* Integrated main parts of former image HOL-Complex with HOL.  Entry

points Main and Complex_Main remain as before.

* Logic image HOL-Plain provides a minimal HOL with the most important

tools available (inductive, datatype, primrec, ...).  This facilitates

experimentation and tool development.  Note that user applications

(and library theories) should never refer to anything below theory

Main, as before.

* Logic image HOL-Main stops at theory Main, and thus facilitates

experimentation due to shorter build times.

* Logic image HOL-NSA contains theories of nonstandard analysis which

were previously part of former HOL-Complex.  Entry point Hyperreal

remains valid, but theories formerly using Complex_Main should now use

new entry point Hypercomplex.

* Generic ATP manager for Sledgehammer, based on ML threads instead of

Posix processes.  Avoids potentially expensive forking of the ML

process.  New thread-based implementation also works on non-Unix

platforms (Cygwin).  Provers are no longer hardwired, but defined

within the theory via plain ML wrapper functions.  Basic Sledgehammer

commands are covered in the isar-ref manual.

* Wrapper scripts for remote SystemOnTPTP service allows to use

sledgehammer without local ATP installation (Vampire etc.). Other

provers may be included via suitable ML wrappers, see also

src/HOL/ATP_Linkup.thy.

* ATP selection (E/Vampire/Spass) is now via Proof General's settings

menu.

* The metis method no longer fails because the theorem is too trivial

(contains the empty clause).

* The metis method now fails in the usual manner, rather than raising

an exception, if it determines that it cannot prove the theorem.

* Method "coherent" implements a prover for coherent logic (see also

src/Tools/coherent.ML).

* Constants "undefined" and "default" replace "arbitrary".  Usually

"undefined" is the right choice to replace "arbitrary", though

logically there is no difference.  INCOMPATIBILITY.

* Command "value" now integrates different evaluation mechanisms.  The

result of the first successful evaluation mechanism is printed.  In

square brackets a particular named evaluation mechanisms may be

specified (currently, [SML], [code] or [nbe]).  See further

src/HOL/ex/Eval_Examples.thy.

* Normalization by evaluation now allows non-leftlinear equations.

Declare with attribute [code nbe].

* Methods "case_tac" and "induct_tac" now refer to the very same rules

as the structured Isar versions "cases" and "induct", cf. the

corresponding "cases" and "induct" attributes.  Mutual induction rules

are now presented as a list of individual projections

(e.g. foo_bar.inducts for types foo and bar); the old format with

explicit HOL conjunction is no longer supported.  INCOMPATIBILITY, in

rare situations a different rule is selected --- notably nested tuple

elimination instead of former prod.exhaust: use explicit (case_tac t

rule: prod.exhaust) here.

* Attributes "cases", "induct", "coinduct" support "del" option.

* Removed fact "case_split_thm", which duplicates "case_split".

* The option datatype has been moved to a new theory Option.  Renamed

option_map to Option.map, and o2s to Option.set, INCOMPATIBILITY.

* New predicate "strict_mono" classifies strict functions on partial

orders.  With strict functions on linear orders, reasoning about

(in)equalities is facilitated by theorems "strict_mono_eq",

"strict_mono_less_eq" and "strict_mono_less".