Isabelle NEWS -- history of user-relevant changes

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

(Note: Isabelle/jEdit shows a tree-view of this file in Sidekick.)

New in this Isabelle version

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

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Improved scheduling for urgent print tasks (e.g. command state output,

interactive queries) wrt. long-running background tasks.

* IDE support for the source-level debugger of Poly/ML, to work with

Isabelle/ML and official Standard ML. Configuration option "ML_debugger"

and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',

'SML_file_no_debug' control compilation of sources with debugging

information. The Debugger panel allows to set breakpoints (via context

menu), step through stopped threads, evaluate local ML expressions etc.

At least one Debugger view needs to be active to have any effect on the

running ML program.

*** Isar ***

* Command 'obtain' binds term abbreviations (via 'is' patterns) in the

proof body as well, abstracted over relevant parameters.

* Improved type-inference for theorem statement 'obtains': separate

parameter scope for of each clause.

* Term abbreviations via 'is' patterns also work for schematic

statements: result is abstracted over unknowns.

* Local goals ('have', 'show', 'hence', 'thus') allow structured

statements like fixes/assumes/shows in theorem specifications, but the

notation is postfix with keywords 'if' (or 'when') and 'for'. For

example:

  have result: "C x y"

    if "A x" and "B y"

    for x :: 'a and y :: 'a

    <proof>

The local assumptions are bound to the name "that". The result is

exported from context of the statement as usual. The above roughly

corresponds to a raw proof block like this:

  {

    fix x :: 'a and y :: 'a

    assume that: "A x" "B y"

    have "C x y" <proof>

  }

  note result = this

The keyword 'when' may be used instead of 'if', to indicate 'presume'

instead of 'assume' above.

* The meaning of 'show' with Pure rule statements has changed: premises

are treated in the sense of 'assume', instead of 'presume'. This means,

a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as follows:

  show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"

or:

  show "C x" if "A x" "B x" for x

Rare INCOMPATIBILITY, the old behaviour may be recovered as follows:

  show "C x" when "A x" "B x" for x

* New command 'supply' supports fact definitions during goal refinement

('apply' scripts).

* New command 'consider' states rules for generalized elimination and

case splitting. This is like a toplevel statement "theorem obtains" used

within a proof body; or like a multi-branch 'obtain' without activation

of the local context elements yet.

* Proof method "cases" allows to specify the rule as first entry of

chained facts.  This is particularly useful with 'consider':

  consider (a) A | (b) B | (c) C <proof>

  then have something

  proof cases

    case a

    then show ?thesis <proof>

  next

    case b

    then show ?thesis <proof>

  next

    case c

    then show ?thesis <proof>

  qed

* Command 'case' allows fact name and attribute specification like this:

  case a: (c xs)

  case a [attributes]: (c xs)

Facts that are introduced by invoking the case context are uniformly

qualified by "a"; the same name is used for the cumulative fact. The old

form "case (c xs) [attributes]" is no longer supported. Rare

INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,

and always put attributes in front.

* The standard proof method of commands 'proof' and '..' is now called

"standard" to make semantically clear what it is; the old name "default"

is still available as legacy for some time. Documentation now explains

'..' more accurately as "by standard" instead of "by rule".

* Command 'subgoal' allows to impose some structure on backward

refinements, to avoid proof scripts degenerating into long of 'apply'

sequences. Further explanations and examples are given in the isar-ref

manual.

* Proof method "goals" turns the current subgoals into cases within the

context; the conclusion is bound to variable ?case in each case.

For example:

lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"

  and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"

proof goals

  case (1 x)

  then show ?case using \<open>A x\<close> \<open>B x\<close> sorry

next

  case (2 y z)

  then show ?case using \<open>U y\<close> \<open>V z\<close> sorry

qed

lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"

  and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"

proof goals

  case prems: 1

  then show ?case using prems sorry

next

  case prems: 2

  then show ?case using prems sorry

qed

* The undocumented feature of implicit cases goal1, goal2, goal3, etc.

is marked as legacy, and will be removed eventually. The proof method

"goals" achieves a similar effect within regular Isar; often it can be

done more adequately by other means (e.g. 'consider').

* Nesting of Isar goal structure has been clarified: the context after

the initial backwards refinement is retained for the whole proof, within

all its context sections (as indicated via 'next'). This is e.g.

relevant for 'using', 'including', 'supply':

  have "A \<and> A" if a: A for A

    supply [simp] = a

  proof

    show A by simp

  next

    show A by simp

  qed

* Method "sleep" succeeds after a real-time delay (in seconds). This is

occasionally useful for demonstration and testing purposes.

*** Pure ***

* The vacuous fact "TERM x" may be established "by fact" or as `TERM x`

as well, not just "by this" or "." as before.

* Configuration option rule_insts_schematic has been discontinued

(intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.

* Abbreviations in type classes now carry proper sort constraint.

Rare INCOMPATIBILITY in situations where the previous misbehaviour

has been exploited previously.

* Refinement of user-space type system in type classes: pseudo-local

operations behave more similar to abbreviations.  Potential

INCOMPATIBILITY in exotic situations.

*** HOL ***

* Qualification of various formal entities in the libraries is done more

uniformly via "context begin qualified definition ... end" instead of

old-style "hide_const (open) ...". Consequently, both the defined

constant and its defining fact become qualified, e.g. Option.is_none and

Option.is_none_def. Occasional INCOMPATIBILITY in applications.

* Combinator to represent case distinction on products is named "uncurry",

with "split" and "prod_case" retained as input abbreviations.

Partially applied occurences of "uncurry" with eta-contracted body

terms are not printed with special syntax, to provide a compact

notation and getting rid of a special-case print translation.

Hence, the "uncurry"-expressions are printed the following way:

a) fully applied "uncurry f p": explicit case-expression;

b) partially applied with explicit double lambda abstraction in

the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;

c) partially applied with eta-contracted body term "uncurry f":

no special syntax, plain "uncurry" combinator.

This aims for maximum readability in a given subterm.

INCOMPATIBILITY.

* Some old and rarely used ASCII replacement syntax has been removed.

INCOMPATIBILITY, standard syntax with symbols should be used instead.

The subsequent commands help to reproduce the old forms, e.g. to

simplify porting old theories:

  type_notation Map.map  (infixr "~=>" 0)

  notation Map.map_comp  (infixl "o'_m" 55)

* Case combinator "prod_case" with eta-contracted body functions

has explicit "uncurry" notation, to provide a compact notation while

getting ride of a special case translation.  Slight syntactic

INCOMPATIBILITY.

* Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has

been removed. INCOMPATIBILITY.

* Quickcheck setup for finite sets.

* Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.

* Sledgehammer:

  - Proof reconstruction has been improved, to minimize the incidence of

    cases where Sledgehammer gives a proof that does not work.

  - Auto Sledgehammer now minimizes and preplays the results.

  - Handle Vampire 4.0 proof output without raising exception.

  - Eliminated "MASH" environment variable. Use the "MaSh" option in

    Isabelle/jEdit instead. INCOMPATIBILITY.

* Nitpick:

  - Removed "check_potential" and "check_genuine" options.

* New commands lift_bnf and copy_bnf for lifting (copying) a BNF structure

  on the raw type to an abstract type defined using typedef.

* Division on integers is bootstrapped directly from division on

naturals and uses generic numeral algorithm for computations.

Slight INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes

former simprocs binary_int_div and binary_int_mod

* Tightened specification of class semiring_no_zero_divisors.  Slight

INCOMPATIBILITY.

* Class algebraic_semidom introduces common algebraic notions of

integral (semi)domains, particularly units.  Although

logically subsumed by fields, is is not a super class of these

in order not to burden fields with notions that are trivial there.

* Class normalization_semidom specifies canonical representants

for equivalence classes of associated elements in an integral

(semi)domain.  This formalizes associated elements as well.

* Abstract specification of gcd/lcm operations in classes semiring_gcd,

semiring_Gcd, semiring_Lcd.  Minor INCOMPATIBILITY: facts gcd_nat.commute

and gcd_int.commute are subsumed by gcd.commute, as well as gcd_nat.assoc

and gcd_int.assoc by gcd.assoc.

* Former constants Fields.divide (_ / _) and Divides.div (_ div _)

are logically unified to Rings.divide in syntactic type class

Rings.divide, with infix syntax (_ div _).  Infix syntax (_ / _)

for field division is added later as abbreviation in class Fields.inverse.

INCOMPATIBILITY,  instantiations must refer to Rings.divide rather

than the former separate constants, hence infix syntax (_ / _) is usually

not available during instantiation.

* Library/Multiset:

  - Renamed multiset inclusion operators:

      < ~> <#

      \<subset> ~> \<subset>#

      <= ~> <=#

      \<le> ~> \<le>#

      \<subseteq> ~> \<subseteq>#

    INCOMPATIBILITY.

  - "'a multiset" is no longer an instance of the "order",

    "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",

    "semilattice_inf", and "semilattice_sup" type classes. The theorems

    previously provided by these type classes (directly or indirectly)

    are now available through the "subset_mset" interpretation

    (e.g. add_mono ~> subset_mset.add_mono).

    INCOMPATIBILITY.

  - Renamed conversions:

      multiset_of ~> mset

      multiset_of_set ~> mset_set

      set_of ~> set_mset

    INCOMPATIBILITY

  - Renamed lemmas:

      mset_le_def ~> subseteq_mset_def

      mset_less_def ~> subset_mset_def

      less_eq_multiset.rep_eq ~> subseteq_mset_def

    INCOMPATIBILITY

  - Removed lemmas generated by lift_definition:

    less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer

    less_eq_multiset_def

    INCOMPATIBILITY

* Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals and Cauchy's integral theorem,

    ported from HOL Light

* Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'

command. Minor INCOMPATIBILITY, use 'function' instead.

* Recursive function definitions ('fun', 'function', 'partial_function')

no longer expose the low-level "_def" facts of the internal

construction. INCOMPATIBILITY, enable option "function_defs" in the

context for rare situations where these facts are really needed.

* Imperative_HOL: obsolete theory Legacy_Mrec has been removed.

*** ML ***

* Instantiation rules have been re-organized as follows:

  Thm.instantiate  (*low-level instantiation with named arguments*)

  Thm.instantiate' (*version with positional arguments*)

  Drule.infer_instantiate  (*instantiation with type inference*)

  Drule.infer_instantiate'  (*version with positional arguments*)

The LHS only requires variable specifications, instead of full terms.

Old cterm_instantiate is superseded by infer_instantiate.

INCOMPATIBILITY, need to re-adjust some ML names and types accordingly.

* Old tactic shorthands atac, rtac, etac, dtac, ftac have been

discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.

instead (with proper context).

* Thm.instantiate (and derivatives) no longer require the LHS of the

instantiation to be certified: plain variables are given directly.

* Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous

quasi-bound variables (like the Simplifier), instead of accidentally

named local fixes. This has the potential to improve stability of proof

tools, but can also cause INCOMPATIBILITY for tools that don't observe

the proof context discipline.

*** System ***

* Poly/ML 5.5.3 runs natively on x86-windows and x86_64-windows,

which both allow larger heap space than former x86-cygwin.

* Java runtime environment for x86_64-windows allows to use larger heap

space.

* Java runtime options are determined separately for 32bit vs. 64bit

platforms as follows.

  - Isabelle desktop application: platform-specific files that are

    associated with the main app bundle

  - isabelle jedit: settings

    JEDIT_JAVA_SYSTEM_OPTIONS

    JEDIT_JAVA_OPTIONS32 vs. JEDIT_JAVA_OPTIONS64

  - isabelle build: settings

    ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64

New in Isabelle2015 (May 2015)

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

*** General ***

* Local theory specification commands may have a 'private' or

'qualified' modifier to restrict name space accesses to the local scope,

as provided by some "context begin ... end" block. For example:

  context

  begin

  private definition ...

  private lemma ...

  qualified definition ...

  qualified lemma ...

  lemma ...

  theorem ...

  end

* Command 'experiment' opens an anonymous locale context with private

naming policy.

* Command 'notepad' requires proper nesting of begin/end and its proof

structure in the body: 'oops' is no longer supported here. Minor

INCOMPATIBILITY, use 'sorry' instead.

* Command 'named_theorems' declares a dynamic fact within the context,

together with an attribute to maintain the content incrementally. This

supersedes functor Named_Thms in Isabelle/ML, but with a subtle change

of semantics due to external visual order vs. internal reverse order.

* 'find_theorems': search patterns which are abstractions are

schematically expanded before search. Search results match the naive

expectation more closely, particularly wrt. abbreviations.

INCOMPATIBILITY.

* Commands 'method_setup' and 'attribute_setup' now work within a local

theory context.

* Outer syntax commands are managed authentically within the theory

context, without implicit global state. Potential for accidental

INCOMPATIBILITY, make sure that required theories are really imported.

* Historical command-line terminator ";" is no longer accepted (and

already used differently in Isar). Minor INCOMPATIBILITY, use "isabelle

update_semicolons" to remove obsolete semicolons from old theory

sources.

* Structural composition of proof methods (meth1; meth2) in Isar

corresponds to (tac1 THEN_ALL_NEW tac2) in ML.

* The Eisbach proof method language allows to define new proof methods

by combining existing ones with their usual syntax. The "match" proof

method provides basic fact/term matching in addition to

premise/conclusion matching through Subgoal.focus, and binds fact names

from matches as well as term patterns within matches. The Isabelle

documentation provides an entry "eisbach" for the Eisbach User Manual.

Sources and various examples are in ~~/src/HOL/Eisbach/.

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Improved folding mode "isabelle" based on Isar syntax. Alternatively,

the "sidekick" mode may be used for document structure.

* Extended bracket matching based on Isar language structure. System

option jedit_structure_limit determines maximum number of lines to scan

in the buffer.

* Support for BibTeX files: context menu, context-sensitive token

marker, SideKick parser.

* Document antiquotation @{cite} provides formal markup, which is

interpreted semi-formally based on .bib files that happen to be open in

the editor (hyperlinks, completion etc.).

* Less waste of vertical space via negative line spacing (see Global

Options / Text Area).

* Improved graphview panel with optional output of PNG or PDF, for

display of 'thy_deps', 'class_deps' etc.

* The commands 'thy_deps' and 'class_deps' allow optional bounds to

restrict the visualized hierarchy.

* Improved scheduling for asynchronous print commands (e.g. provers

managed by the Sledgehammer panel) wrt. ongoing document processing.

*** Document preparation ***

* Document markup commands 'chapter', 'section', 'subsection',

'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any

context, even before the initial 'theory' command. Obsolete proof

commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been

discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw'

instead. The old 'header' command is still retained for some time, but

should be replaced by 'chapter', 'section' etc. (using "isabelle

update_header"). Minor INCOMPATIBILITY.

* Official support for "tt" style variants, via \isatt{...} or

\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or

verbatim environment of LaTeX is no longer used. This allows @{ML} etc.

as argument to other macros (such as footnotes).

* Document antiquotation @{verbatim} prints ASCII text literally in "tt"

style.

* Discontinued obsolete option "document_graph": session_graph.pdf is

produced unconditionally for HTML browser_info and PDF-LaTeX document.

* Diagnostic commands and document markup commands within a proof do not

affect the command tag for output. Thus commands like 'thm' are subject

to proof document structure, and no longer "stick out" accidentally.

Commands 'text' and 'txt' merely differ in the LaTeX style, not their

tags. Potential INCOMPATIBILITY in exotic situations.

* System option "pretty_margin" is superseded by "thy_output_margin",

which is also accessible via document antiquotation option "margin".

Only the margin for document output may be changed, but not the global

pretty printing: that is 76 for plain console output, and adapted

dynamically in GUI front-ends. Implementations of document

antiquotations need to observe the margin explicitly according to

Thy_Output.string_of_margin. Minor INCOMPATIBILITY.

* Specification of 'document_files' in the session ROOT file is

mandatory for document preparation. The legacy mode with implicit

copying of the document/ directory is no longer supported. Minor

INCOMPATIBILITY.

*** Pure ***

* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"

etc.) allow an optional context of local variables ('for' declaration):

these variables become schematic in the instantiated theorem; this

behaviour is analogous to 'for' in attributes "where" and "of".

Configuration option rule_insts_schematic (default false) controls use

of schematic variables outside the context. Minor INCOMPATIBILITY,

declare rule_insts_schematic = true temporarily and update to use local

variable declarations or dummy patterns instead.

* Explicit instantiation via attributes "where", "of", and proof methods

"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns

("_") that stand for anonymous local variables.

* Generated schematic variables in standard format of exported facts are

incremented to avoid material in the proof context. Rare

INCOMPATIBILITY, explicit instantiation sometimes needs to refer to

different index.

* Lexical separation of signed and unsigned numerals: categories "num"

and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence

of numeral signs, particularly in expressions involving infix syntax

like "(- 1) ^ n".

* Old inner token category "xnum" has been discontinued.  Potential

INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num"

token category instead.

*** HOL ***

* New (co)datatype package:

  - The 'datatype_new' command has been renamed 'datatype'. The old

    command of that name is now called 'old_datatype' and is provided

    by "~~/src/HOL/Library/Old_Datatype.thy". See

    'isabelle doc datatypes' for information on porting.

    INCOMPATIBILITY.

  - Renamed theorems:

      disc_corec ~> corec_disc

      disc_corec_iff ~> corec_disc_iff

      disc_exclude ~> distinct_disc

      disc_exhaust ~> exhaust_disc

      disc_map_iff ~> map_disc_iff

      sel_corec ~> corec_sel

      sel_exhaust ~> exhaust_sel

      sel_map ~> map_sel

      sel_set ~> set_sel

      sel_split ~> split_sel

      sel_split_asm ~> split_sel_asm

      strong_coinduct ~> coinduct_strong

      weak_case_cong ~> case_cong_weak

    INCOMPATIBILITY.

  - The "no_code" option to "free_constructors", "datatype_new", and

    "codatatype" has been renamed "plugins del: code".

    INCOMPATIBILITY.

  - The rules "set_empty" have been removed. They are easy

    consequences of other set rules "by auto".

    INCOMPATIBILITY.

  - The rule "set_cases" is now registered with the "[cases set]"

    attribute. This can influence the behavior of the "cases" proof

    method when more than one case rule is applicable (e.g., an

    assumption is of the form "w : set ws" and the method "cases w"

    is invoked). The solution is to specify the case rule explicitly

    (e.g. "cases w rule: widget.exhaust").

    INCOMPATIBILITY.

  - Renamed theories:

      BNF_Comp ~> BNF_Composition

      BNF_FP_Base ~> BNF_Fixpoint_Base

      BNF_GFP ~> BNF_Greatest_Fixpoint

      BNF_LFP ~> BNF_Least_Fixpoint

      BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions

      Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions

    INCOMPATIBILITY.

  - Lifting and Transfer setup for basic HOL types sum and prod (also

    option) is now performed by the BNF package. Theories Lifting_Sum,

    Lifting_Product and Lifting_Option from Main became obsolete and

    were removed. Changed definitions of the relators rel_prod and

    rel_sum (using inductive).

    INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead

    of rel_prod_def and rel_sum_def.

    Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names

    changed (e.g. map_prod_transfer ~> prod.map_transfer).

  - Parametricity theorems for map functions, relators, set functions,

    constructors, case combinators, discriminators, selectors and

    (co)recursors are automatically proved and registered as transfer

    rules.

* Old datatype package:

  - The old 'datatype' command has been renamed 'old_datatype', and

    'rep_datatype' has been renamed 'old_rep_datatype'. They are

    provided by "~~/src/HOL/Library/Old_Datatype.thy". See

    'isabelle doc datatypes' for information on porting.

    INCOMPATIBILITY.

  - Renamed theorems:

      weak_case_cong ~> case_cong_weak

    INCOMPATIBILITY.

  - Renamed theory:

      ~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy

    INCOMPATIBILITY.

* Nitpick:

  - Fixed soundness bug related to the strict and non-strict subset

    operations.

* Sledgehammer:

  - CVC4 is now included with Isabelle instead of CVC3 and run by

    default.

  - Z3 is now always enabled by default, now that it is fully open

    source. The "z3_non_commercial" option is discontinued.

  - Minimization is now always enabled by default.

    Removed sub-command:

      min

  - Proof reconstruction, both one-liners and Isar, has been

    dramatically improved.

  - Improved support for CVC4 and veriT.

* Old and new SMT modules:

  - The old 'smt' method has been renamed 'old_smt' and moved to

    'src/HOL/Library/Old_SMT.thy'. It is provided for compatibility,

    until applications have been ported to use the new 'smt' method. For

    the method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must

    be installed, and the environment variable "OLD_Z3_SOLVER" must

    point to it.

    INCOMPATIBILITY.

  - The 'smt2' method has been renamed 'smt'.

    INCOMPATIBILITY.

  - New option 'smt_reconstruction_step_timeout' to limit the

    reconstruction time of Z3 proof steps in the new 'smt' method.

  - New option 'smt_statistics' to display statistics of the new 'smt'

    method, especially runtime statistics of Z3 proof reconstruction.

* Lifting: command 'lift_definition' allows to execute lifted constants

that have as a return type a datatype containing a subtype. This

overcomes long-time limitations in the area of code generation and

lifting, and avoids tedious workarounds.

* Command and antiquotation "value" provide different evaluation slots

(again), where the previous strategy (NBE after ML) serves as default.

Minor INCOMPATIBILITY.

* Add NO_MATCH-simproc, allows to check for syntactic non-equality.

* field_simps: Use NO_MATCH-simproc for distribution rules, to avoid

non-termination in case of distributing a division. With this change

field_simps is in some cases slightly less powerful, if it fails try to

add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY.

* Separate class no_zero_divisors has been given up in favour of fully

algebraic semiring_no_zero_divisors. INCOMPATIBILITY.

* Class linordered_semidom really requires no zero divisors.

INCOMPATIBILITY.

* Classes division_ring, field and linordered_field always demand

"inverse 0 = 0". Given up separate classes division_ring_inverse_zero,

field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY.

* Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit

additive inverse operation. INCOMPATIBILITY.

* Complex powers and square roots. The functions "ln" and "powr" are now

overloaded for types real and complex, and 0 powr y = 0 by definition.

INCOMPATIBILITY: type constraints may be necessary.

* The functions "sin" and "cos" are now defined for any type of sort

"{real_normed_algebra_1,banach}" type, so in particular on "real" and

"complex" uniformly. Minor INCOMPATIBILITY: type constraints may be

needed.

* New library of properties of the complex transcendental functions sin,

cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light.

* The factorial function, "fact", now has type "nat => 'a" (of a sort

that admits numeric types including nat, int, real and complex.

INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type

constraint, and the combination "real (fact k)" is likely to be

unsatisfactory. If a type conversion is still necessary, then use

"of_nat (fact k)" or "real_of_nat (fact k)".

* Removed functions "natfloor" and "natceiling", use "nat o floor" and

"nat o ceiling" instead. A few of the lemmas have been retained and

adapted: in their names "natfloor"/"natceiling" has been replaced by

"nat_floor"/"nat_ceiling".

* Qualified some duplicated fact names required for boostrapping the

type class hierarchy:

  ab_add_uminus_conv_diff ~> diff_conv_add_uminus

  field_inverse_zero ~> inverse_zero

  field_divide_inverse ~> divide_inverse

  field_inverse ~> left_inverse

Minor INCOMPATIBILITY.

* Eliminated fact duplicates:

  mult_less_imp_less_right ~> mult_right_less_imp_less

  mult_less_imp_less_left ~> mult_left_less_imp_less

Minor INCOMPATIBILITY.

* Fact consolidation: even_less_0_iff is subsumed by

double_add_less_zero_iff_single_add_less_zero (simp by default anyway).

* Generalized and consolidated some theorems concerning divsibility:

  dvd_reduce ~> dvd_add_triv_right_iff

  dvd_plus_eq_right ~> dvd_add_right_iff

  dvd_plus_eq_left ~> dvd_add_left_iff

Minor INCOMPATIBILITY.

* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _"

and part of theory Main.

  even_def ~> even_iff_mod_2_eq_zero

INCOMPATIBILITY.

* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor

INCOMPATIBILITY.

* Bootstrap of listsum as special case of abstract product over lists.

Fact rename:

    listsum_def ~> listsum.eq_foldr

INCOMPATIBILITY.

* Product over lists via constant "listprod".

* Theory List: renamed drop_Suc_conv_tl and nth_drop' to

Cons_nth_drop_Suc.

* New infrastructure for compiling, running, evaluating and testing

generated code in target languages in HOL/Library/Code_Test. See

HOL/Codegenerator_Test/Code_Test* for examples.

* Library/Multiset:

  - Introduced "replicate_mset" operation.

  - Introduced alternative characterizations of the multiset ordering in

    "Library/Multiset_Order".

  - Renamed multiset ordering:

      <# ~> #<#

      <=# ~> #<=#

      \<subset># ~> #\<subset>#

      \<subseteq># ~> #\<subseteq>#

    INCOMPATIBILITY.

  - Introduced abbreviations for ill-named multiset operations:

      <#, \<subset># abbreviate < (strict subset)

      <=#, \<le>#, \<subseteq># abbreviate <= (subset or equal)

    INCOMPATIBILITY.

  - Renamed

      in_multiset_of ~> in_multiset_in_set

      Multiset.fold ~> fold_mset

      Multiset.filter ~> filter_mset

    INCOMPATIBILITY.

  - Removed mcard, is equal to size.

  - Added attributes:

      image_mset.id [simp]

      image_mset_id [simp]

      elem_multiset_of_set [simp, intro]

      comp_fun_commute_plus_mset [simp]

      comp_fun_commute.fold_mset_insert [OF comp_fun_commute_plus_mset, simp]

      in_mset_fold_plus_iff [iff]

      set_of_Union_mset [simp]

      in_Union_mset_iff [iff]

    INCOMPATIBILITY.

* Library/Sum_of_Squares: simplified and improved "sos" method. Always

use local CSDP executable, which is much faster than the NEOS server.

The "sos_cert" functionality is invoked as "sos" with additional

argument. Minor INCOMPATIBILITY.

* HOL-Decision_Procs: New counterexample generator quickcheck

[approximation] for inequalities of transcendental functions. Uses

hardware floating point arithmetic to randomly discover potential

counterexamples. Counterexamples are certified with the "approximation"

method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for

examples.

* HOL-Probability: Reworked measurability prover

  - applies destructor rules repeatedly

  - removed application splitting (replaced by destructor rule)

  - added congruence rules to rewrite measure spaces under the sets

    projection

* New proof method "rewrite" (in theory ~~/src/HOL/Library/Rewrite) for

single-step rewriting with subterm selection based on patterns.

*** ML ***

* Subtle change of name space policy: undeclared entries are now

considered inaccessible, instead of accessible via the fully-qualified

internal name. This mainly affects Name_Space.intern (and derivatives),

which may produce an unexpected Long_Name.hidden prefix. Note that

contemporary applications use the strict Name_Space.check (and

derivatives) instead, which is not affected by the change. Potential

INCOMPATIBILITY in rare applications of Name_Space.intern.

* Subtle change of error semantics of Toplevel.proof_of: regular user

ERROR instead of internal Toplevel.UNDEF.

* Basic combinators map, fold, fold_map, split_list, apply are available

as parameterized antiquotations, e.g. @{map 4} for lists of quadruples.

* Renamed "pairself" to "apply2", in accordance to @{apply 2}.

INCOMPATIBILITY.

* Former combinators NAMED_CRITICAL and CRITICAL for central critical

sections have been discontinued, in favour of the more elementary

Multithreading.synchronized and its high-level derivative

Synchronized.var (which is usually sufficient in applications). Subtle

INCOMPATIBILITY: synchronized access needs to be atomic and cannot be

nested.

* Synchronized.value (ML) is actually synchronized (as in Scala): subtle

change of semantics with minimal potential for INCOMPATIBILITY.

* The main operations to certify logical entities are Thm.ctyp_of and

Thm.cterm_of with a local context; old-style global theory variants are

available as Thm.global_ctyp_of and Thm.global_cterm_of.

INCOMPATIBILITY.

* Elementary operations in module Thm are no longer pervasive.

INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of,

Thm.term_of etc.

* Proper context for various elementary tactics: assume_tac,

resolve_tac, eresolve_tac, dresolve_tac, forward_tac, match_tac,

compose_tac, Splitter.split_tac etc. INCOMPATIBILITY.

* Tactical PARALLEL_ALLGOALS is the most common way to refer to

PARALLEL_GOALS.

* Goal.prove_multi is superseded by the fully general Goal.prove_common,

which also allows to specify a fork priority.

* Antiquotation @{command_spec "COMMAND"} is superseded by

@{command_keyword COMMAND} (usually without quotes and with PIDE

markup). Minor INCOMPATIBILITY.

* Cartouches within ML sources are turned into values of type

Input.source (with formal position information).

*** System ***

* The Isabelle tool "update_cartouches" changes theory files to use

cartouches instead of old-style {* verbatim *} or `alt_string` tokens.

* The Isabelle tool "build" provides new options -X, -k, -x.

* Discontinued old-fashioned "codegen" tool. Code generation can always

be externally triggered using an appropriate ROOT file plus a

corresponding theory. Parametrization is possible using environment

variables, or ML snippets in the most extreme cases. Minor

INCOMPATIBILITY.

* JVM system property "isabelle.threads" determines size of Scala thread

pool, like Isabelle system option "threads" for ML.

* JVM system property "isabelle.laf" determines the default Swing

look-and-feel, via internal class name or symbolic name as in the jEdit

menu Global Options / Appearance.

* Support for Proof General and Isar TTY loop has been discontinued.

Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.

New in Isabelle2014 (August 2014)

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

*** General ***

* Support for official Standard ML within the Isabelle context.

Command 'SML_file' reads and evaluates the given Standard ML file.

Toplevel bindings are stored within the theory context; the initial

environment is restricted to the Standard ML implementation of

Poly/ML, without the add-ons of Isabelle/ML.  Commands 'SML_import'

and 'SML_export' allow to exchange toplevel bindings between the two

separate environments.  See also ~~/src/Tools/SML/Examples.thy for

some examples.

* Standard tactics and proof methods such as "clarsimp", "auto" and

"safe" now preserve equality hypotheses "x = expr" where x is a free

variable.  Locale assumptions and chained facts containing "x"

continue to be useful.  The new method "hypsubst_thin" and the

configuration option "hypsubst_thin" (within the attribute name space)

restore the previous behavior.  INCOMPATIBILITY, especially where

induction is done after these methods or when the names of free and

bound variables clash.  As first approximation, old proofs may be

repaired by "using [[hypsubst_thin = true]]" in the critical spot.

* More static checking of proof methods, which allows the system to

form a closure over the concrete syntax.  Method arguments should be

processed in the original proof context as far as possible, before

operating on the goal state.  In any case, the standard discipline for

subgoal-addressing needs to be observed: no subgoals or a subgoal

number that is out of range produces an empty result sequence, not an

exception.  Potential INCOMPATIBILITY for non-conformant tactical

proof tools.

* Lexical syntax (inner and outer) supports text cartouches with

arbitrary nesting, and without escapes of quotes etc.  The Prover IDE

supports input via ` (backquote).

* The outer syntax categories "text" (for formal comments and document

markup commands) and "altstring" (for literal fact references) allow

cartouches as well, in addition to the traditional mix of quotations.

* Syntax of document antiquotation @{rail} now uses \<newline> instead

of "\\", to avoid the optical illusion of escaped backslash within

string token.  General renovation of its syntax using text cartouches.

Minor INCOMPATIBILITY.

* Discontinued legacy_isub_isup, which was a temporary workaround for

Isabelle/ML in Isabelle2013-1.  The prover process no longer accepts

old identifier syntax with \<^isub> or \<^isup>.  Potential

INCOMPATIBILITY.

* Document antiquotation @{url} produces markup for the given URL,

which results in an active hyperlink within the text.

* Document antiquotation @{file_unchecked} is like @{file}, but does

not check existence within the file-system.

* Updated and extended manuals: codegen, datatypes, implementation,

isar-ref, jedit, system.

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Improved Document panel: simplified interaction where every single

mouse click (re)opens document via desktop environment or as jEdit

buffer.

* Support for Navigator plugin (with toolbar buttons), with connection

to PIDE hyperlinks.

* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.

Open text buffers take precedence over copies within the file-system.

* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for

auxiliary ML files.

* Improved syntactic and semantic completion mechanism, with simple

templates, completion language context, name-space completion,

file-name completion, spell-checker completion.

* Refined GUI popup for completion: more robust key/mouse event

handling and propagation to enclosing text area -- avoid loosing

keystrokes with slow / remote graphics displays.

* Completion popup supports both ENTER and TAB (default) to select an

item, depending on Isabelle options.

* Refined insertion of completion items wrt. jEdit text: multiple

selections, rectangular selections, rectangular selection as "tall

caret".

* Integrated spell-checker for document text, comments etc. with

completion popup and context-menu.

* More general "Query" panel supersedes "Find" panel, with GUI access

to commands 'find_theorems' and 'find_consts', as well as print

operations for the context.  Minor incompatibility in keyboard

shortcuts etc.: replace action isabelle-find by isabelle-query.

* Search field for all output panels ("Output", "Query", "Info" etc.)

to highlight text via regular expression.

* Option "jedit_print_mode" (see also "Plugin Options / Isabelle /

General") allows to specify additional print modes for the prover

process, without requiring old-fashioned command-line invocation of

"isabelle jedit -m MODE".

* More support for remote files (e.g. http) using standard Java

networking operations instead of jEdit virtual file-systems.

* Empty editors buffers that are no longer required (e.g.\ via theory

imports) are automatically removed from the document model.

* Improved monitor panel.

* Improved Console/Scala plugin: more uniform scala.Console output,

more robust treatment of threads and interrupts.

* Improved management of dockable windows: clarified keyboard focus

and window placement wrt. main editor view; optional menu item to

"Detach" a copy where this makes sense.

* New Simplifier Trace panel provides an interactive view of the

simplification process, enabled by the "simp_trace_new" attribute

within the context.

*** Pure ***

* Low-level type-class commands 'classes', 'classrel', 'arities' have

been discontinued to avoid the danger of non-trivial axiomatization

that is not immediately visible.  INCOMPATIBILITY, use regular

'instance' command with proof.  The required OFCLASS(...) theorem

might be postulated via 'axiomatization' beforehand, or the proof