Isabelle NEWS -- history user-relevant changes

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

New in this Isabelle version

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

*** HOL ***

* 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

  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

New in Isabelle2011-1 (October 2011)

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

*** General ***

* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as

"isabelle jedit" or "ISABELLE_HOME/Isabelle" on the command line.

  - Management of multiple theory files directly from the editor

    buffer store -- bypassing the file-system (no requirement to save

    files for checking).

  - Markup of formal entities within the text buffer, with semantic

    highlighting, tooltips and hyperlinks to jump to defining source

    positions.

  - Improved text rendering, with sub/superscripts in the source

    buffer (including support for copy/paste wrt. output panel, HTML

    theory output and other non-Isabelle text boxes).

  - Refined scheduling of proof checking and printing of results,

    based on interactive editor view.  (Note: jEdit folding and

    narrowing allows to restrict buffer perspectives explicitly.)

  - Reduced CPU performance requirements, usable on machines with few

    cores.

  - Reduced memory requirements due to pruning of unused document

    versions (garbage collection).

See also ~~/src/Tools/jEdit/README.html for further information,

including some remaining limitations.

* Theory loader: source files are exclusively located via the master

directory of each theory node (where the .thy file itself resides).

The global load path (such as src/HOL/Library) has been discontinued.

Note that the path element ~~ may be used to reference theories in the

Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet".

INCOMPATIBILITY.

* Theory loader: source files are identified by content via SHA1

digests.  Discontinued former path/modtime identification and optional

ISABELLE_FILE_IDENT plugin scripts.

* Parallelization of nested Isar proofs is subject to

Goal.parallel_proofs_threshold (default 100).  See also isabelle

usedir option -Q.

* Name space: former unsynchronized references are now proper

configuration options, with more conventional names:

  long_names   ~> names_long

  short_names  ~> names_short

  unique_names ~> names_unique

Minor INCOMPATIBILITY, need to declare options in context like this:

  declare [[names_unique = false]]

* Literal facts `prop` may contain dummy patterns, e.g. `_ = _`.  Note

that the result needs to be unique, which means fact specifications

may have to be refined after enriching a proof context.

* Attribute "case_names" has been refined: the assumptions in each case

can be named now by following the case name with [name1 name2 ...].

* Isabelle/Isar reference manual has been updated and extended:

  - "Synopsis" provides a catalog of main Isar language concepts.

  - Formal references in syntax diagrams, via @{rail} antiquotation.

  - Updated material from classic "ref" manual, notably about

    "Classical Reasoner".

*** HOL ***

* Class bot and top require underlying partial order rather than

preorder: uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.

* Class complete_lattice: generalized a couple of lemmas from sets;

generalized theorems INF_cong and SUP_cong.  New type classes for

complete boolean algebras and complete linear orders.  Lemmas

Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in

class complete_linorder.

Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def,

Sup_fun_def, Inf_apply, Sup_apply.

Removed redundant lemmas (the right hand side gives hints how to

replace them for (metis ...), or (simp only: ...) proofs):

  Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty inf_top_right]

  Sup_singleton ~> Sup_insert [where A="{}", unfolded Sup_empty sup_bot_right]

  Inf_binary ~> Inf_insert, Inf_empty, and inf_top_right

  Sup_binary ~> Sup_insert, Sup_empty, and sup_bot_right

  Int_eq_Inter ~> Inf_insert, Inf_empty, and inf_top_right

  Un_eq_Union ~> Sup_insert, Sup_empty, and sup_bot_right

  Inter_def ~> INF_def, image_def

  Union_def ~> SUP_def, image_def

  INT_eq ~> INF_def, and image_def

  UN_eq ~> SUP_def, and image_def

  INF_subset ~> INF_superset_mono [OF _ order_refl]

More consistent and comprehensive names:

  INTER_eq_Inter_image ~> INF_def

  UNION_eq_Union_image ~> SUP_def

  INFI_def ~> INF_def

  SUPR_def ~> SUP_def

  INF_leI ~> INF_lower

  INF_leI2 ~> INF_lower2

  le_INFI ~> INF_greatest

  le_SUPI ~> SUP_upper

  le_SUPI2 ~> SUP_upper2

  SUP_leI ~> SUP_least

  INFI_bool_eq ~> INF_bool_eq

  SUPR_bool_eq ~> SUP_bool_eq

  INFI_apply ~> INF_apply

  SUPR_apply ~> SUP_apply

  INTER_def ~> INTER_eq

  UNION_def ~> UNION_eq

INCOMPATIBILITY.

* Renamed theory Complete_Lattice to Complete_Lattices.

INCOMPATIBILITY.

* Theory Complete_Lattices: lemmas Inf_eq_top_iff, INF_eq_top_iff,

INF_image, Inf_insert, INF_top, Inf_top_conv, INF_top_conv, SUP_bot,

Sup_bot_conv, SUP_bot_conv, Sup_eq_top_iff, SUP_eq_top_iff, SUP_image,

Sup_insert are now declared as [simp].  INCOMPATIBILITY.

* Theory Lattice: lemmas compl_inf_bot, compl_le_comp_iff,

compl_sup_top, inf_idem, inf_left_idem, inf_sup_absorb, sup_idem,

sup_inf_absob, sup_left_idem are now declared as [simp].  Minor

INCOMPATIBILITY.

* Added syntactic classes "inf" and "sup" for the respective

constants.  INCOMPATIBILITY: Changes in the argument order of the

(mostly internal) locale predicates for some derived classes.

* Theorem collections ball_simps and bex_simps do not contain theorems

referring to UNION any longer; these have been moved to collection

UN_ball_bex_simps.  INCOMPATIBILITY.

* Theory Archimedean_Field: floor now is defined as parameter of a

separate type class floor_ceiling.

* Theory Finite_Set: more coherent development of fold_set locales:

    locale fun_left_comm ~> locale comp_fun_commute

    locale fun_left_comm_idem ~> locale comp_fun_idem

Both use point-free characterization; interpretation proofs may need

adjustment.  INCOMPATIBILITY.

* Theory Limits: Type "'a net" has been renamed to "'a filter", in

accordance with standard mathematical terminology. INCOMPATIBILITY.

* Theory Complex_Main: The locale interpretations for the

bounded_linear and bounded_bilinear locales have been removed, in

order to reduce the number of duplicate lemmas. Users must use the

original names for distributivity theorems, potential INCOMPATIBILITY.

  divide.add ~> add_divide_distrib

  divide.diff ~> diff_divide_distrib

  divide.setsum ~> setsum_divide_distrib

  mult.add_right ~> right_distrib

  mult.diff_right ~> right_diff_distrib

  mult_right.setsum ~> setsum_right_distrib

  mult_left.diff ~> left_diff_distrib

* Theory Complex_Main: Several redundant theorems have been removed or

replaced by more general versions. INCOMPATIBILITY.

  real_diff_def ~> minus_real_def

  real_divide_def ~> divide_real_def

  real_less_def ~> less_le

  real_abs_def ~> abs_real_def

  real_sgn_def ~> sgn_real_def

  real_mult_commute ~> mult_commute

  real_mult_assoc ~> mult_assoc

  real_mult_1 ~> mult_1_left

  real_add_mult_distrib ~> left_distrib

  real_zero_not_eq_one ~> zero_neq_one

  real_mult_inverse_left ~> left_inverse

  INVERSE_ZERO ~> inverse_zero

  real_le_refl ~> order_refl

  real_le_antisym ~> order_antisym

  real_le_trans ~> order_trans

  real_le_linear ~> linear

  real_le_eq_diff ~> le_iff_diff_le_0

  real_add_left_mono ~> add_left_mono

  real_mult_order ~> mult_pos_pos

  real_mult_less_mono2 ~> mult_strict_left_mono

  real_of_int_real_of_nat ~> real_of_int_of_nat_eq

  real_0_le_divide_iff ~> zero_le_divide_iff

  realpow_two_disj ~> power2_eq_iff

  real_squared_diff_one_factored ~> square_diff_one_factored

  realpow_two_diff ~> square_diff_square_factored

  reals_complete2 ~> complete_real

  real_sum_squared_expand ~> power2_sum

  exp_ln_eq ~> ln_unique

  expi_add ~> exp_add

  expi_zero ~> exp_zero

  lemma_DERIV_subst ~> DERIV_cong

  LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff

  LIMSEQ_const ~> tendsto_const

  LIMSEQ_norm ~> tendsto_norm

  LIMSEQ_add ~> tendsto_add

  LIMSEQ_minus ~> tendsto_minus

  LIMSEQ_minus_cancel ~> tendsto_minus_cancel

  LIMSEQ_diff ~> tendsto_diff

  bounded_linear.LIMSEQ ~> bounded_linear.tendsto

  bounded_bilinear.LIMSEQ ~> bounded_bilinear.tendsto

  LIMSEQ_mult ~> tendsto_mult

  LIMSEQ_inverse ~> tendsto_inverse

  LIMSEQ_divide ~> tendsto_divide

  LIMSEQ_pow ~> tendsto_power

  LIMSEQ_setsum ~> tendsto_setsum

  LIMSEQ_setprod ~> tendsto_setprod

  LIMSEQ_norm_zero ~> tendsto_norm_zero_iff

  LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff

  LIMSEQ_imp_rabs ~> tendsto_rabs

  LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]

  LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]

  LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]

  LIMSEQ_Complex ~> tendsto_Complex

  LIM_ident ~> tendsto_ident_at

  LIM_const ~> tendsto_const

  LIM_add ~> tendsto_add

  LIM_add_zero ~> tendsto_add_zero

  LIM_minus ~> tendsto_minus

  LIM_diff ~> tendsto_diff

  LIM_norm ~> tendsto_norm

  LIM_norm_zero ~> tendsto_norm_zero

  LIM_norm_zero_cancel ~> tendsto_norm_zero_cancel

  LIM_norm_zero_iff ~> tendsto_norm_zero_iff

  LIM_rabs ~> tendsto_rabs

  LIM_rabs_zero ~> tendsto_rabs_zero

  LIM_rabs_zero_cancel ~> tendsto_rabs_zero_cancel

  LIM_rabs_zero_iff ~> tendsto_rabs_zero_iff

  LIM_compose ~> tendsto_compose

  LIM_mult ~> tendsto_mult

  LIM_scaleR ~> tendsto_scaleR

  LIM_of_real ~> tendsto_of_real

  LIM_power ~> tendsto_power

  LIM_inverse ~> tendsto_inverse

  LIM_sgn ~> tendsto_sgn

  isCont_LIM_compose ~> isCont_tendsto_compose

  bounded_linear.LIM ~> bounded_linear.tendsto

  bounded_linear.LIM_zero ~> bounded_linear.tendsto_zero

  bounded_bilinear.LIM ~> bounded_bilinear.tendsto

  bounded_bilinear.LIM_prod_zero ~> bounded_bilinear.tendsto_zero

  bounded_bilinear.LIM_left_zero ~> bounded_bilinear.tendsto_left_zero

  bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero

  LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at]

* Theory Complex_Main: The definition of infinite series was

generalized.  Now it is defined on the type class {topological_space,

comm_monoid_add}.  Hence it is useable also for extended real numbers.

* Theory Complex_Main: The complex exponential function "expi" is now

a type-constrained abbreviation for "exp :: complex => complex"; thus

several polymorphic lemmas about "exp" are now applicable to "expi".

* Code generation:

  - Theory Library/Code_Char_ord provides native ordering of

    characters in the target language.

  - Commands code_module and code_library are legacy, use export_code

    instead.

  - Method "evaluation" is legacy, use method "eval" instead.

  - Legacy evaluator "SML" is deactivated by default.  May be

    reactivated by the following theory command:

      setup {* Value.add_evaluator ("SML", Codegen.eval_term) *}

* Declare ext [intro] by default.  Rare INCOMPATIBILITY.

* New proof method "induction" that gives induction hypotheses the

name "IH", thus distinguishing them from further hypotheses that come

from rule induction.  The latter are still called "hyps".  Method

"induction" is a thin wrapper around "induct" and follows the same

syntax.

* Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is

still available as a legacy feature for some time.

* Nitpick:

  - Added "need" and "total_consts" options.

  - Reintroduced "show_skolems" option by popular demand.

  - Renamed attribute: nitpick_def ~> nitpick_unfold.

    INCOMPATIBILITY.

* Sledgehammer:

  - Use quasi-sound (and efficient) translations by default.

  - Added support for the following provers: E-ToFoF, LEO-II,

    Satallax, SNARK, Waldmeister, and Z3 with TPTP syntax.

  - Automatically preplay and minimize proofs before showing them if

    this can be done within reasonable time.

  - sledgehammer available_provers ~> sledgehammer supported_provers.

    INCOMPATIBILITY.

  - Added "preplay_timeout", "slicing", "type_enc", "sound",

    "max_mono_iters", and "max_new_mono_instances" options.

  - Removed "explicit_apply" and "full_types" options as well as "Full

    Types" Proof General menu item. INCOMPATIBILITY.

* Metis:

  - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY.

  - Obsoleted "metisFT" -- use "metis (full_types)" instead.

    INCOMPATIBILITY.

* Command 'try':

  - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and

    "elim:" options. INCOMPATIBILITY.

  - Introduced 'try' that not only runs 'try_methods' but also

    'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'.

* Quickcheck:

  - Added "eval" option to evaluate terms for the found counterexample

    (currently only supported by the default (exhaustive) tester).

  - Added post-processing of terms to obtain readable counterexamples

    (currently only supported by the default (exhaustive) tester).

  - New counterexample generator quickcheck[narrowing] enables

    narrowing-based testing.  Requires the Glasgow Haskell compiler

    with its installation location defined in the Isabelle settings

    environment as ISABELLE_GHC.

  - Removed quickcheck tester "SML" based on the SML code generator

    (formly in HOL/Library).

* Function package: discontinued option "tailrec".  INCOMPATIBILITY,

use 'partial_function' instead.

* Theory Library/Extended_Reals replaces now the positive extended

reals found in probability theory. This file is extended by

Multivariate_Analysis/Extended_Real_Limits.

* Theory Library/Old_Recdef: old 'recdef' package has been moved here,

from where it must be imported explicitly if it is really required.

INCOMPATIBILITY.

* Theory Library/Wfrec: well-founded recursion combinator "wfrec" has

been moved here.  INCOMPATIBILITY.

* Theory Library/Saturated provides type of numbers with saturated

arithmetic.

* Theory Library/Product_Lattice defines a pointwise ordering for the

product type 'a * 'b, and provides instance proofs for various order

and lattice type classes.

* Theory Library/Countable now provides the "countable_datatype" proof

method for proving "countable" class instances for datatypes.

* Theory Library/Cset_Monad allows do notation for computable sets

(cset) via the generic monad ad-hoc overloading facility.

* Library: Theories of common data structures are split into theories

for implementation, an invariant-ensuring type, and connection to an

abstract type. INCOMPATIBILITY.

  - RBT is split into RBT and RBT_Mapping.

  - AssocList is split and renamed into AList and AList_Mapping.

  - DList is split into DList_Impl, DList, and DList_Cset.

  - Cset is split into Cset and List_Cset.

* Theory Library/Nat_Infinity has been renamed to

Library/Extended_Nat, with name changes of the following types and

constants:

  type inat   ~> type enat

  Fin         ~> enat

  Infty       ~> infinity (overloaded)

  iSuc        ~> eSuc

  the_Fin     ~> the_enat

Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has

been renamed accordingly. INCOMPATIBILITY.

* Session Multivariate_Analysis: The euclidean_space type class now

fixes a constant "Basis :: 'a set" consisting of the standard

orthonormal basis for the type. Users now have the option of

quantifying over this set instead of using the "basis" function, e.g.

"ALL x:Basis. P x" vs "ALL i<DIM('a). P (basis i)".

* Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed

to "('a, 'b) vec" (the syntax "'a ^ 'b" remains unaffected). Constants

"Cart_nth" and "Cart_lambda" have been respectively renamed to

"vec_nth" and "vec_lambda"; theorems mentioning those names have

changed to match. Definition theorems for overloaded constants now use

the standard "foo_vec_def" naming scheme. A few other theorems have

been renamed as follows (INCOMPATIBILITY):

  Cart_eq          ~> vec_eq_iff

  dist_nth_le_cart ~> dist_vec_nth_le

  tendsto_vector   ~> vec_tendstoI

  Cauchy_vector    ~> vec_CauchyI

* Session Multivariate_Analysis: Several duplicate theorems have been

removed, and other theorems have been renamed or replaced with more

general versions. INCOMPATIBILITY.

  finite_choice ~> finite_set_choice

  eventually_conjI ~> eventually_conj

  eventually_and ~> eventually_conj_iff

  eventually_false ~> eventually_False

  setsum_norm ~> norm_setsum

  Lim_sequentially ~> LIMSEQ_def

  Lim_ident_at ~> LIM_ident

  Lim_const ~> tendsto_const

  Lim_cmul ~> tendsto_scaleR [OF tendsto_const]

  Lim_neg ~> tendsto_minus

  Lim_add ~> tendsto_add

  Lim_sub ~> tendsto_diff

  Lim_mul ~> tendsto_scaleR

  Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const]

  Lim_null_norm ~> tendsto_norm_zero_iff [symmetric]

  Lim_linear ~> bounded_linear.tendsto

  Lim_component ~> tendsto_euclidean_component

  Lim_component_cart ~> tendsto_vec_nth

  Lim_inner ~> tendsto_inner [OF tendsto_const]

  dot_lsum ~> inner_setsum_left

  dot_rsum ~> inner_setsum_right

  continuous_cmul ~> continuous_scaleR [OF continuous_const]

  continuous_neg ~> continuous_minus

  continuous_sub ~> continuous_diff

  continuous_vmul ~> continuous_scaleR [OF _ continuous_const]

  continuous_mul ~> continuous_scaleR

  continuous_inv ~> continuous_inverse

  continuous_at_within_inv ~> continuous_at_within_inverse

  continuous_at_inv ~> continuous_at_inverse

  continuous_at_norm ~> continuous_norm [OF continuous_at_id]

  continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id]

  continuous_at_component ~> continuous_component [OF continuous_at_id]

  continuous_on_neg ~> continuous_on_minus

  continuous_on_sub ~> continuous_on_diff

  continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const]

  continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const]

  continuous_on_mul ~> continuous_on_scaleR

  continuous_on_mul_real ~> continuous_on_mult

  continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]

  continuous_on_norm ~> continuous_on_norm [OF continuous_on_id]

  continuous_on_inverse ~> continuous_on_inv

  uniformly_continuous_on_neg ~> uniformly_continuous_on_minus

  uniformly_continuous_on_sub ~> uniformly_continuous_on_diff

  subset_interior ~> interior_mono

  subset_closure ~> closure_mono

  closure_univ ~> closure_UNIV

  real_arch_lt ~> reals_Archimedean2

  real_arch ~> reals_Archimedean3

  real_abs_norm ~> abs_norm_cancel

  real_abs_sub_norm ~> norm_triangle_ineq3

  norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2

* Session HOL-Probability:

  - Caratheodory's extension lemma is now proved for ring_of_sets.

  - Infinite products of probability measures are now available.

  - Sigma closure is independent, if the generator is independent

  - Use extended reals instead of positive extended

    reals. INCOMPATIBILITY.

* Session HOLCF: Discontinued legacy theorem names, INCOMPATIBILITY.

  expand_fun_below ~> fun_below_iff

  below_fun_ext ~> fun_belowI

  expand_cfun_eq ~> cfun_eq_iff

  ext_cfun ~> cfun_eqI

  expand_cfun_below ~> cfun_below_iff

  below_cfun_ext ~> cfun_belowI

  monofun_fun_fun ~> fun_belowD

  monofun_fun_arg ~> monofunE

  monofun_lub_fun ~> adm_monofun [THEN admD]

  cont_lub_fun ~> adm_cont [THEN admD]

  cont2cont_Rep_CFun ~> cont2cont_APP

  cont_Rep_CFun_app ~> cont_APP_app

  cont_Rep_CFun_app_app ~> cont_APP_app_app

  cont_cfun_fun ~> cont_Rep_cfun1 [THEN contE]

  cont_cfun_arg ~> cont_Rep_cfun2 [THEN contE]

  contlub_cfun ~> lub_APP [symmetric]

  contlub_LAM ~> lub_LAM [symmetric]

  thelubI ~> lub_eqI

  UU_I ~> bottomI

  lift_distinct1 ~> lift.distinct(1)

  lift_distinct2 ~> lift.distinct(2)

  Def_not_UU ~> lift.distinct(2)

  Def_inject ~> lift.inject

  below_UU_iff ~> below_bottom_iff

  eq_UU_iff ~> eq_bottom_iff

*** Document preparation ***

* Antiquotation @{rail} layouts railroad syntax diagrams, see also

isar-ref manual, both for description and actual application of the

same.

* Antiquotation @{value} evaluates the given term and presents its

result.

* Antiquotations: term style "isub" provides ad-hoc conversion of

variables x1, y23 into subscripted form x\<^isub>1,

y\<^isub>2\<^isub>3.

* Predefined LaTeX macros for Isabelle symbols \<bind> and \<then>

(e.g. see ~~/src/HOL/Library/Monad_Syntax.thy).

* Localized \isabellestyle switch can be used within blocks or groups

like this:

  \isabellestyle{it}  %preferred default

  {\isabellestylett @{text "typewriter stuff"}}

* Discontinued special treatment of hard tabulators.  Implicit

tab-width is now defined as 1.  Potential INCOMPATIBILITY for visual

layouts.

*** ML ***

* The inner syntax of sort/type/term/prop supports inlined YXML

representations within quoted string tokens.  By encoding logical

entities via Term_XML (in ML or Scala) concrete syntax can be

bypassed, which is particularly useful for producing bits of text

under external program control.

* Antiquotations for ML and document preparation are managed as theory

data, which requires explicit setup.

* Isabelle_Process.is_active allows tools to check if the official

process wrapper is running (Isabelle/Scala/jEdit) or the old TTY loop

(better known as Proof General).

* Structure Proof_Context follows standard naming scheme.  Old

ProofContext is still available for some time as legacy alias.

* Structure Timing provides various operations for timing; supersedes

former start_timing/end_timing etc.

* Path.print is the official way to show file-system paths to users

(including quotes etc.).

* Inner syntax: identifiers in parse trees of generic categories

"logic", "aprop", "idt" etc. carry position information (disguised as

type constraints).  Occasional INCOMPATIBILITY with non-compliant

translations that choke on unexpected type constraints.  Positions can

be stripped in ML translations via Syntax.strip_positions /

Syntax.strip_positions_ast, or via the syntax constant

"_strip_positions" within parse trees.  As last resort, positions can

be disabled via the configuration option Syntax.positions, which is

called "syntax_positions" in Isar attribute syntax.

* Discontinued special status of various ML structures that contribute

to structure Syntax (Ast, Lexicon, Mixfix, Parser, Printer etc.): less

pervasive content, no inclusion in structure Syntax.  INCOMPATIBILITY,

refer directly to Ast.Constant, Lexicon.is_identifier,

Syntax_Trans.mk_binder_tr etc.

* Typed print translation: discontinued show_sorts argument, which is

already available via context of "advanced" translation.

* Refined PARALLEL_GOALS tactical: degrades gracefully for schematic

goal states; body tactic needs to address all subgoals uniformly.

* Slightly more special eq_list/eq_set, with shortcut involving

pointer equality (assumes that eq relation is reflexive).

* Classical tactics use proper Proof.context instead of historic types

claset/clasimpset.  Old-style declarations like addIs, addEs, addDs

operate directly on Proof.context.  Raw type claset retains its use as

snapshot of the classical context, which can be recovered via

(put_claset HOL_cs) etc.  Type clasimpset has been discontinued.

INCOMPATIBILITY, classical tactics and derived proof methods require

proper Proof.context.

*** System ***

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

without proper multithreading and TimeLimit implementation.

* Discontinued old lib/scripts/polyml-platform, which has been

obsolete since Isabelle2009-2.

* Various optional external tools are referenced more robustly and

uniformly by explicit Isabelle settings as follows:

  ISABELLE_CSDP   (formerly CSDP_EXE)

  ISABELLE_GHC    (formerly EXEC_GHC or GHC_PATH)

  ISABELLE_OCAML  (formerly EXEC_OCAML)

  ISABELLE_SWIPL  (formerly EXEC_SWIPL)

  ISABELLE_YAP    (formerly EXEC_YAP)

Note that automated detection from the file-system or search path has

been discontinued.  INCOMPATIBILITY.

* Scala layer provides JVM method invocation service for static

methods of type (String)String, see Invoke_Scala.method in ML.  For

example:

  Invoke_Scala.method "java.lang.System.getProperty" "java.home"

Together with YXML.string_of_body/parse_body and XML.Encode/Decode

this allows to pass structured values between ML and Scala.

* The IsabelleText fonts includes some further glyphs to support the

Prover IDE.  Potential INCOMPATIBILITY: users who happen to have

installed a local copy (which is normally *not* required) need to

delete or update it from ~~/lib/fonts/.

New in Isabelle2011 (January 2011)

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

*** General ***

* Experimental Prover IDE based on Isabelle/Scala and jEdit (see

src/Tools/jEdit).  This also serves as IDE for Isabelle/ML, with

useful tooltips and hyperlinks produced from its static analysis.  The

bundled component provides an executable Isabelle tool that can be run

like this:

  Isabelle2011/bin/isabelle jedit

* Significantly improved Isabelle/Isar implementation manual.

* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER

(and thus refers to something like $HOME/.isabelle/Isabelle2011),

while the default heap location within that directory lacks that extra

suffix.  This isolates multiple Isabelle installations from each

other, avoiding problems with old settings in new versions.

INCOMPATIBILITY, need to copy/upgrade old user settings manually.

* Source files are always encoded as UTF-8, instead of old-fashioned

ISO-Latin-1.  INCOMPATIBILITY.  Isabelle LaTeX documents might require

the following package declarations:

  \usepackage[utf8]{inputenc}

  \usepackage{textcomp}

* Explicit treatment of UTF-8 sequences as Isabelle symbols, such that

a Unicode character is treated as a single symbol, not a sequence of

non-ASCII bytes as before.  Since Isabelle/ML string literals may

contain symbols without further backslash escapes, Unicode can now be

used here as well.  Recall that Symbol.explode in ML provides a

consistent view on symbols, while raw explode (or String.explode)

merely give a byte-oriented representation.

* Theory loader: source files are primarily located via the master

directory of each theory node (where the .thy file itself resides).

The global load path is still partially available as legacy feature.

Minor INCOMPATIBILITY due to subtle change in file lookup: use

explicit paths, relatively to the theory.

* Special treatment of ML file names has been discontinued.

Historically, optional extensions .ML or .sml were added on demand --

at the cost of clarity of file dependencies.  Recall that Isabelle/ML

files exclusively use the .ML extension.  Minor INCOMPATIBILTY.

* Various options that affect pretty printing etc. are now properly

handled within the context via configuration options, instead of

unsynchronized references or print modes.  There are both ML Config.T

entities and Isar declaration attributes to access these.

  ML (Config.T)                 Isar (attribute)

  eta_contract                  eta_contract

  show_brackets                 show_brackets

  show_sorts                    show_sorts

  show_types                    show_types

  show_question_marks           show_question_marks

  show_consts                   show_consts

  show_abbrevs                  show_abbrevs

  Syntax.ast_trace              syntax_ast_trace

  Syntax.ast_stat               syntax_ast_stat

  Syntax.ambiguity_level        syntax_ambiguity_level

  Goal_Display.goals_limit      goals_limit

  Goal_Display.show_main_goal   show_main_goal

  Method.rule_trace             rule_trace

  Thy_Output.display            thy_output_display

  Thy_Output.quotes             thy_output_quotes

  Thy_Output.indent             thy_output_indent

  Thy_Output.source             thy_output_source

  Thy_Output.break              thy_output_break

Note that corresponding "..._default" references in ML may only be

changed globally at the ROOT session setup, but *not* within a theory.

The option "show_abbrevs" supersedes the former print mode

"no_abbrevs" with inverted meaning.

* More systematic naming of some configuration options.

INCOMPATIBILITY.

  trace_simp  ~>  simp_trace

  debug_simp  ~>  simp_debug

* Support for real valued configuration options, using simplistic

floating-point notation that coincides with the inner syntax for

float_token.

* Support for real valued preferences (with approximative PGIP type):

front-ends need to accept "pgint" values in float notation.

INCOMPATIBILITY.

* The IsabelleText font now includes Cyrillic, Hebrew, Arabic from

DejaVu Sans.

* Discontinued support for Poly/ML 5.0 and 5.1 versions.

*** Pure ***

* Command 'type_synonym' (with single argument) replaces somewhat

outdated 'types', which is still available as legacy feature for some

time.

* Command 'nonterminal' (with 'and' separated list of arguments)

replaces somewhat outdated 'nonterminals'.  INCOMPATIBILITY.

* Command 'notepad' replaces former 'example_proof' for

experimentation in Isar without any result.  INCOMPATIBILITY.

* Locale interpretation commands 'interpret' and 'sublocale' accept

lists of equations to map definitions in a locale to appropriate

entities in the context of the interpretation.  The 'interpretation'

command already provided this functionality.

* Diagnostic command 'print_dependencies' prints the locale instances

that would be activated if the specified expression was interpreted in

the current context.  Variant "print_dependencies!" assumes a context

without interpretations.

* Diagnostic command 'print_interps' prints interpretations in proofs

in addition to interpretations in theories.

* Discontinued obsolete 'global' and 'local' commands to manipulate

the theory name space.  Rare INCOMPATIBILITY.  The ML functions

Sign.root_path and Sign.local_path may be applied directly where this

feature is still required for historical reasons.

* Discontinued obsolete 'constdefs' command.  INCOMPATIBILITY, use

'definition' instead.

* The "prems" fact, which refers to the accidental collection of

foundational premises in the context, is now explicitly marked as

legacy feature and will be discontinued soon.  Consider using "assms"

of the head statement or reference facts by explicit names.

* Document antiquotations @{class} and @{type} print classes and type

constructors.

* Document antiquotation @{file} checks file/directory entries within

the local file system.

*** HOL ***

* Coercive subtyping: functions can be declared as coercions and type

inference will add them as necessary upon input of a term.  Theory

Complex_Main declares real :: nat => real and real :: int => real as

coercions. A coercion function f is declared like this:

  declare [[coercion f]]

To lift coercions through type constructors (e.g. from nat => real to

nat list => real list), map functions can be declared, e.g.

  declare [[coercion_map map]]

Currently coercion inference is activated only in theories including

real numbers, i.e. descendants of Complex_Main.  This is controlled by

the configuration option "coercion_enabled", e.g. it can be enabled in

other theories like this:

  declare [[coercion_enabled]]

* Command 'partial_function' provides basic support for recursive

function definitions over complete partial orders.  Concrete instances

are provided for i) the option type, ii) tail recursion on arbitrary

types, and iii) the heap monad of Imperative_HOL.  See

src/HOL/ex/Fundefs.thy and src/HOL/Imperative_HOL/ex/Linked_Lists.thy

for examples.

* Function package: f.psimps rules are no longer implicitly declared

as [simp].  INCOMPATIBILITY.

* Datatype package: theorems generated for executable equality (class

"eq") carry proper names and are treated as default code equations.

* Inductive package: now offers command 'inductive_simps' to

automatically derive instantiated and simplified equations for

inductive predicates, similar to 'inductive_cases'.

* Command 'enriched_type' allows to register properties of the

functorial structure of types.

* Improved infrastructure for term evaluation using code generator

techniques, in particular static evaluation conversions.

* Code generator: Scala (2.8 or higher) has been added to the target

languages.

* Code generator: globbing constant expressions "*" and "Theory.*"

have been replaced by the more idiomatic "_" and "Theory._".

INCOMPATIBILITY.

* Code generator: export_code without explicit file declaration prints

to standard output.  INCOMPATIBILITY.

* Code generator: do not print function definitions for case

combinators any longer.

* Code generator: simplification with rules determined with

src/Tools/Code/code_simp.ML and method "code_simp".

* Code generator for records: more idiomatic representation of record

types.  Warning: records are not covered by ancient SML code

generation any longer.  INCOMPATIBILITY.  In cases of need, a suitable

rep_datatype declaration helps to succeed then:

  record 'a foo = ...

  ...

  rep_datatype foo_ext ...

* Records: logical foundation type for records does not carry a

'_type' suffix any longer (obsolete due to authentic syntax).

INCOMPATIBILITY.

* Quickcheck now by default uses exhaustive testing instead of random

testing.  Random testing can be invoked by "quickcheck [random]",

exhaustive testing by "quickcheck [exhaustive]".

* Quickcheck instantiates polymorphic types with small finite

datatypes by default. This enables a simple execution mechanism to

handle quantifiers and function equality over the finite datatypes.

* Quickcheck random generator has been renamed from "code" to

"random".  INCOMPATIBILITY.

* Quickcheck now has a configurable time limit which is set to 30

seconds by default. This can be changed by adding [timeout = n] to the

quickcheck command. The time limit for Auto Quickcheck is still set

independently.

* Quickcheck in locales considers interpretations of that locale for

counter example search.

* Sledgehammer:

  - Added "smt" and "remote_smt" provers based on the "smt" proof

    method. See the Sledgehammer manual for details ("isabelle doc

    sledgehammer").

  - Renamed commands:

    sledgehammer atp_info ~> sledgehammer running_provers

    sledgehammer atp_kill ~> sledgehammer kill_provers

    sledgehammer available_atps ~> sledgehammer available_provers

    INCOMPATIBILITY.

  - Renamed options:

    sledgehammer [atps = ...] ~> sledgehammer [provers = ...]

    sledgehammer [atp = ...] ~> sledgehammer [prover = ...]

    sledgehammer [timeout = 77 s] ~> sledgehammer [timeout = 77]

    (and "ms" and "min" are no longer supported)

    INCOMPATIBILITY.

* Nitpick:

  - Renamed options:

    nitpick [timeout = 77 s] ~> nitpick [timeout = 77]

    nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777]

    INCOMPATIBILITY.

  - Added support for partial quotient types.

  - Added local versions of the "Nitpick.register_xxx" functions.

  - Added "whack" option.

  - Allow registration of quotient types as codatatypes.

  - Improved "merge_type_vars" option to merge more types.

  - Removed unsound "fast_descrs" option.

  - Added custom symmetry breaking for datatypes, making it possible to reach

    higher cardinalities.

  - Prevent the expansion of too large definitions.

* Proof methods "metis" and "meson" now have configuration options

"meson_trace", "metis_trace", and "metis_verbose" that can be enabled

to diagnose these tools. E.g.

    using [[metis_trace = true]]

* Auto Solve: Renamed "Auto Solve Direct".  The tool is now available

manually as command 'solve_direct'.

* The default SMT solver Z3 must be enabled explicitly (due to

licensing issues) by setting the environment variable

Z3_NON_COMMERCIAL in etc/settings of the component, for example.  For

commercial applications, the SMT solver CVC3 is provided as fall-back;

changing the SMT solver is done via the configuration option

"smt_solver".

* Remote SMT solvers need to be referred to by the "remote_" prefix,

i.e. "remote_cvc3" and "remote_z3".

* Added basic SMT support for datatypes, records, and typedefs using

the oracle mode (no proofs).  Direct support of pairs has been dropped

in exchange (pass theorems fst_conv snd_conv pair_collapse to the SMT

support for a similar behavior).  Minor INCOMPATIBILITY.

* Changed SMT configuration options:

  - Renamed:

    z3_proofs ~> smt_oracle (with inverted meaning)

    z3_trace_assms ~> smt_trace_used_facts

    INCOMPATIBILITY.

  - Added:

    smt_verbose

    smt_random_seed

    smt_datatypes

    smt_infer_triggers

    smt_monomorph_limit

    cvc3_options

    remote_cvc3_options

    remote_z3_options

    yices_options

* Boogie output files (.b2i files) need to be declared in the theory

header.

* Simplification procedure "list_to_set_comprehension" rewrites list

comprehensions applied to List.set to set comprehensions.  Occasional

INCOMPATIBILITY, may be deactivated like this:

  declare [[simproc del: list_to_set_comprehension]]

* Removed old version of primrec package.  INCOMPATIBILITY.

* Removed simplifier congruence rule of "prod_case", as has for long

been the case with "split".  INCOMPATIBILITY.

* String.literal is a type, but not a datatype.  INCOMPATIBILITY.

* Removed [split_format ... and ... and ...] version of

[split_format].  Potential INCOMPATIBILITY.

* Predicate "sorted" now defined inductively, with nice induction

rules.  INCOMPATIBILITY: former sorted.simps now named sorted_simps.