summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

author | wenzelm |

Tue May 22 11:05:47 2018 +0200 (22 months ago) | |

changeset 68245 | 37974ddde928 |

parent 68219 | c0341c0080e2 |

child 68246 | b48bab511939 |

permissions | -rw-r--r-- |

merged

1 Isabelle NEWS -- history of user-relevant changes

2 =================================================

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

7 New in this Isabelle version

8 ----------------------------

10 *** General ***

12 * Marginal comments need to be written exclusively in the new-style form

13 "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer

14 supported. INCOMPATIBILITY, use the command-line tool "isabelle

15 update_comments" to update existing theory files.

17 * Old-style inner comments (* ... *) within the term language are legacy

18 and will be discontinued soon: use formal comments "\<comment> \<open>...\<close>" or "\<^cancel>\<open>...\<close>"

19 instead.

21 * The "op <infix-op>" syntax for infix operators has been replaced by

22 "(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to

23 be a space between the "*" and the corresponding parenthesis.

24 INCOMPATIBILITY.

25 There is an Isabelle tool "update_op" that converts theory and ML files

26 to the new syntax. Because it is based on regular expression matching,

27 the result may need a bit of manual postprocessing. Invoking "isabelle

28 update_op" converts all files in the current directory (recursively).

29 In case you want to exclude conversion of ML files (because the tool

30 frequently also converts ML's "op" syntax), use option "-m".

32 * The old 'def' command has been discontinued (legacy since

33 Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with

34 object-logic equality or equivalence.

36 * Session-qualified theory names are mandatory: it is no longer possible

37 to refer to unqualified theories from the parent session.

38 INCOMPATIBILITY for old developments that have not been updated to

39 Isabelle2017 yet (using the "isabelle imports" tool).

41 * Theory header 'abbrevs' specifications need to be separated by 'and'.

42 INCOMPATIBILITY.

44 * Only the most fundamental theory names are global, usually the entry

45 points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,

46 FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for

47 formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".

49 * Command 'external_file' declares the formal dependency on the given

50 file name, such that the Isabelle build process knows about it, but

51 without specific Prover IDE management.

53 * Session ROOT entries no longer allow specification of 'files'. Rare

54 INCOMPATIBILITY, use command 'external_file' within a proper theory

55 context.

57 * Session root directories may be specified multiple times: each

58 accessible ROOT file is processed only once. This facilitates

59 specification of $ISABELLE_HOME_USER/ROOTS or command-line options like

60 -d or -D for "isabelle build" and "isabelle jedit". Example:

62 isabelle build -D '~~/src/ZF'

64 * The command 'display_drafts' has been discontinued. INCOMPATIBILITY,

65 use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.

67 * Isabelle symbol "\<hyphen>" is rendered as explicit Unicode hyphen U+2010, to

68 avoid unclear meaning of the old "soft hyphen" U+00AD. Rare

69 INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML output.

72 *** Isabelle/jEdit Prover IDE ***

74 * The view title is set dynamically, according to the Isabelle

75 distribution and the logic session name. The user can override this via

76 set-view-title (stored persistently in $JEDIT_SETTINGS/perspective.xml).

78 * System options "spell_checker_include" and "spell_checker_exclude"

79 supersede former "spell_checker_elements" to determine regions of text

80 that are subject to spell-checking. Minor INCOMPATIBILITY.

82 * PIDE markup for session ROOT files: allows to complete session names,

83 follow links to theories and document files etc.

85 * Completion supports theory header imports, using theory base name.

86 E.g. "Prob" may be completed to "HOL-Probability.Probability".

88 * The command-line tool "isabelle jedit" provides more flexible options

89 for session selection:

90 - options -P opens the parent session image of -l

91 - options -A and -B modify the meaning of -l to produce a base

92 image on the spot, based on the specified ancestor (or parent)

93 - option -F focuses on the specified logic session

94 - option -R has changed: it only opens the session ROOT entry

95 - option -S sets up the development environment to edit the

96 specified session: it abbreviates -B -F -R -l

98 Examples:

99 isabelle jedit -d '$AFP' -S Formal_SSA -A HOL

100 isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis

102 * Named control symbols (without special Unicode rendering) are shown as

103 bold-italic keyword. This is particularly useful for the short form of

104 antiquotations with control symbol: \<^name>\<open>argument\<close>. The action

105 "isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1

106 arguments into this format.

108 * Completion provides templates for named symbols with arguments,

109 e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".

111 * Bibtex database files (.bib) are semantically checked.

113 * Action "isabelle.preview" is able to present more file formats,

114 notably bibtex database files and ML files.

116 * Action "isabelle.draft" is similar to "isabelle.preview", but shows a

117 plain-text document draft. Both are available via the menu "Plugins /

118 Isabelle".

120 * When loading text files, the Isabelle symbols encoding UTF-8-Isabelle

121 is only used if there is no conflict with existing Unicode sequences in

122 the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle

123 symbols remain in literal \<symbol> form. This avoids accidental loss of

124 Unicode content when saving the file.

126 * Update to jedit-5.5.0, the latest release.

129 *** Isabelle/VSCode Prover IDE ***

131 * HTML preview of theories and other file-formats similar to

132 Isabelle/jEdit.

135 *** Document preparation ***

137 * Formal comments work uniformly in outer syntax, inner syntax (term

138 language), Isabelle/ML and some other embedded languages of Isabelle.

139 See also "Document comments" in the isar-ref manual. The following forms

140 are supported:

142 - marginal text comment: \<comment> \<open>\<dots>\<close>

143 - canceled source: \<^cancel>\<open>\<dots>\<close>

144 - raw LaTeX: \<^latex>\<open>\<dots>\<close>

146 * Outside of the inner theory body, the default presentation context is

147 theory Pure. Thus elementary antiquotations may be used in markup

148 commands (e.g. 'chapter', 'section', 'text') and formal comments.

150 * System option "document_tags" specifies a default for otherwise

151 untagged commands. This is occasionally useful to control the global

152 visibility of commands via session options (e.g. in ROOT).

154 * Document markup commands ('section', 'text' etc.) are implicitly

155 tagged as "document" and visible by default. This avoids the application

156 of option "document_tags" to these commands.

158 * Isabelle names are mangled into LaTeX macro names to allow the full

159 identifier syntax with underscore, prime, digits. This is relevant for

160 antiquotations in control symbol notation, e.g. \<^const_name> becomes

161 \isactrlconstUNDERSCOREname.

163 * Document antiquotation @{cite} now checks the given Bibtex entries

164 against the Bibtex database files -- only in batch-mode session builds.

166 * Document antiquotation @{session name} checks and prints the given

167 session name verbatim.

169 * Document preparation with skip_proofs option now preserves the content

170 more accurately: only terminal proof steps ('by' etc.) are skipped.

172 * Command-line tool "isabelle document" has been re-implemented in

173 Isabelle/Scala, with simplified arguments and explicit errors from the

174 latex and bibtex process. Minor INCOMPATIBILITY.

177 *** Isar ***

179 * Command 'interpret' no longer exposes resulting theorems as literal

180 facts, notably for the \<open>prop\<close> notation or the "fact" proof method. This

181 improves modularity of proofs and scalability of locale interpretation.

182 Rare INCOMPATIBILITY, need to refer to explicitly named facts instead

183 (e.g. use 'find_theorems' or 'try' to figure this out).

185 * Rewrites clauses (keyword 'rewrites') were moved into the locale

186 expression syntax, where they are part of locale instances. In

187 interpretation commands rewrites clauses now need to occur before

188 'for' and 'defines'. Minor INCOMPATIBILITY.

190 * For rewrites clauses, if activating a locale instance fails, fall

191 back to reading the clause first. This helps avoid qualification of

192 locale instances where the qualifier's sole purpose is avoiding

193 duplicate constant declarations.

196 *** Pure ***

198 * The inner syntax category "sort" now includes notation "_" for the

199 dummy sort: it is effectively ignored in type-inference.

202 *** HOL ***

204 * Clarified relationship of characters, strings and code generation:

206 * Type "char" is now a proper datatype of 8-bit values.

208 * Conversions "nat_of_char" and "char_of_nat" are gone; use more

209 general conversions "of_char" and "char_of" with suitable

210 type constraints instead.

212 * The zero character is just written "CHR 0x00", not

213 "0" any longer.

215 * Type "String.literal" (for code generation) is now isomorphic

216 to lists of 7-bit (ASCII) values; concrete values can be written

217 as "STR ''...''" for sequences of printable characters and

218 "STR 0x..." for one single ASCII code point given

219 as hexadecimal numeral.

221 * Type "String.literal" supports concatenation "... + ..."

222 for all standard target languages.

224 * Theory Library/Code_Char is gone; study the explanations concerning

225 "String.literal" in the tutorial on code generation to get an idea

226 how target-language string literals can be converted to HOL string

227 values and vice versa.

229 * Imperative-HOL: operation "raise" directly takes a value of type

230 "String.literal" as argument, not type "string".

232 INCOMPATIBILITY.

234 * Abstract bit operations as part of Main: push_bit, take_bit,

235 drop_bit.

237 * New, more general, axiomatization of complete_distrib_lattice.

238 The former axioms:

239 "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"

240 are replaced by

241 "Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"

242 The instantiations of sets and functions as complete_distrib_lattice

243 are moved to Hilbert_Choice.thy because their proofs need the Hilbert

244 choice operator. The dual of this property is also proved in

245 Hilbert_Choice.thy.

247 * New syntax for the minimum/maximum of a function over a finite set:

248 MIN x\<in>A. B and even MIN x. B (only useful for finite types), also

249 MAX.

251 * Clarifed theorem names:

253 Min.antimono ~> Min.subset_imp

254 Max.antimono ~> Max.subset_imp

256 Minor INCOMPATIBILITY.

258 * A new command parametric_constant for proving parametricity of

259 non-recursive definitions. For constants that are not fully parametric

260 the command will infer conditions on relations (e.g., bi_unique,

261 bi_total, or type class conditions such as "respects 0") sufficient for

262 parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for

263 some examples.

265 * A new preprocessor for the code generator to generate code for algebraic

266 types with lazy evaluation semantics even in call-by-value target languages.

267 See theory HOL-Library.Code_Lazy for the implementation and

268 HOL-Codegenerator_Test.Code_Lazy_Test for examples.

270 * SMT module:

271 - The 'smt_oracle' option is now necessary when using the 'smt' method

272 with a solver other than Z3. INCOMPATIBILITY.

273 - The encoding to first-order logic is now more complete in the

274 presence of higher-order quantifiers. An 'smt_explicit_application'

275 option has been added to control this. INCOMPATIBILITY.

277 * Datatypes:

278 - The legacy command 'old_datatype', provided by

279 '~~/src/HOL/Library/Old_Datatype.thy', has been removed. INCOMPATIBILITY.

281 * Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide

282 instances of rat, real, complex as factorial rings etc. Import

283 HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.

284 INCOMPATIBILITY.

286 * Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to

287 sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on

288 interpretation of abstract locales. INCOMPATIBILITY.

290 * Predicate pairwise_coprime abolished, use "pairwise coprime" instead.

291 INCOMPATIBILITY.

293 * The relator rel_filter on filters has been strengthened to its

294 canonical categorical definition with better properties. INCOMPATIBILITY.

296 * Generalized linear algebra involving linear, span, dependent, dim

297 from type class real_vector to locales module and vector_space.

298 Renamed:

299 - span_inc ~> span_superset

300 - span_superset ~> span_base

301 - span_eq ~> span_eq_iff

302 INCOMPATIBILITY.

304 * HOL-Algebra: renamed (^) to [^]

306 * Session HOL-Analysis: Moebius functions, the Riemann mapping

307 theorem, the Vitali covering theorem, change-of-variables results for

308 integration and measures.

310 * Class linordered_semiring_1 covers zero_less_one also, ruling out

311 pathologic instances. Minor INCOMPATIBILITY.

313 * Theory List: functions "sorted_wrt" and "sorted" now compare every

314 element in a list to all following elements, not just the next one.

316 * Removed nat-int transfer machinery. Rare INCOMPATIBILITY.

318 * Predicate coprime is now a real definition, not a mere

319 abbreviation. INCOMPATIBILITY.

321 * Code generation: Code generation takes an explicit option

322 "case_insensitive" to accomodate case-insensitive file systems.

324 * Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid

325 clash with fact mod_mult_self4 (on more generic semirings).

326 INCOMPATIBILITY.

328 * Eliminated some theorem aliasses:

330 even_times_iff ~> even_mult_iff

331 mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1

332 even_of_nat ~> even_int_iff

334 INCOMPATIBILITY.

336 * Eliminated some theorem duplicate variations:

337 * dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0.

338 * mod_Suc_eq_Suc_mod can be replaced by mod_Suc.

339 * mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps.

340 * mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def.

341 * The witness of mod_eqD can be given directly as "_ div _".

343 INCOMPATIBILITY.

346 *** ML ***

348 * Operation Export.export emits theory exports (arbitrary blobs), which

349 are stored persistently in the session build database.

352 *** System ***

354 * Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:

355 heap images and session databases are always stored in

356 $ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or

357 $ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or

358 "isabelle jedit -s" or "isabelle build -s").

360 * The command-line tool retrieves theory exports from the session build

361 database.

363 * The command-line tools "isabelle server" and "isabelle client" provide

364 access to the Isabelle Server: it supports responsive session management

365 and concurrent use of theories, based on Isabelle/PIDE infrastructure.

366 See also the "system" manual.

368 * The command-line tool "isabelle update_comments" normalizes formal

369 comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to

370 approximate the appearance in document output). This is more specific

371 than former "isabelle update_cartouches -c": the latter tool option has

372 been discontinued.

374 * Session ROOT entry: empty 'document_files' means there is no document

375 for this session. There is no need to specify options [document = false]

376 anymore.

378 * The command-line tool "isabelle mkroot" now always produces a document

379 outline: its options have been adapted accordingly. INCOMPATIBILITY.

381 * The command-line tool "isabelle mkroot -I" initializes a Mercurial

382 repository for the generated session files.

384 * Linux and Windows/Cygwin is for x86_64 only. Old 32bit platform

385 support has been discontinued.

387 * Mac OS X 10.10 Yosemite is now the baseline version; Mavericks is no

388 longer supported.

390 * Java runtime is for x86_64 only. Corresponding Isabelle settings have

391 been renamed to ISABELLE_TOOL_JAVA_OPTIONS and JEDIT_JAVA_OPTIONS,

392 instead of former 32/64 variants. INCOMPATIBILITY.

394 * Old settings ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM should be

395 phased out due to unclear preference of 32bit vs. 64bit architecture.

396 Explicit GNU bash expressions are now preferred, for example (with

397 quotes):

399 #Posix executables (Unix or Cygwin), with preference for 64bit

400 "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"

402 #native Windows or Unix executables, with preference for 64bit

403 "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"

405 #native Windows (32bit) or Unix executables (preference for 64bit)

406 "${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}"

408 * Command-line tool "isabelle build" supports new options:

409 - option -B NAME: include session NAME and all descendants

410 - option -S: only observe changes of sources, not heap images

411 - option -f: forces a fresh build

413 * Command-line tool "isabelle build" takes "condition" options with the

414 corresponding environment values into account, when determining the

415 up-to-date status of a session.

417 * Command-line tool "isabelle imports -I" also reports actual session

418 imports. This helps to minimize the session dependency graph.

420 * Update to current Poly/ML 5.7.1 with slightly improved performance and

421 PIDE markup for identifier bindings.

423 * ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific

424 options for improved error reporting. Potential INCOMPATIBILITY with

425 unusual LaTeX installations, may have to adapt these settings.

427 * The bundled Poly/ML 5.7.1 now uses The GNU Multiple Precision

428 Arithmetic Library (libgmp) on all platforms, notably Mac OS X with

429 32/64 bit.

433 New in Isabelle2017 (October 2017)

434 ----------------------------------

436 *** General ***

438 * Experimental support for Visual Studio Code (VSCode) as alternative

439 Isabelle/PIDE front-end, see also

440 https://marketplace.visualstudio.com/items?itemName=makarius.Isabelle2017

442 VSCode is a new type of application that continues the concepts of

443 "programmer's editor" and "integrated development environment" towards

444 fully semantic editing and debugging -- in a relatively light-weight

445 manner. Thus it fits nicely on top of the Isabelle/PIDE infrastructure.

446 Technically, VSCode is based on the Electron application framework

447 (Node.js + Chromium browser + V8), which is implemented in JavaScript

448 and TypeScript, while Isabelle/VSCode mainly consists of Isabelle/Scala

449 modules around a Language Server implementation.

451 * Theory names are qualified by the session name that they belong to.

452 This affects imports, but not the theory name space prefix (which is

453 just the theory base name as before).

455 In order to import theories from other sessions, the ROOT file format

456 provides a new 'sessions' keyword. In contrast, a theory that is

457 imported in the old-fashioned manner via an explicit file-system path

458 belongs to the current session, and might cause theory name conflicts

459 later on. Theories that are imported from other sessions are excluded

460 from the current session document. The command-line tool "isabelle

461 imports" helps to update theory imports.

463 * The main theory entry points for some non-HOL sessions have changed,

464 to avoid confusion with the global name "Main" of the session HOL. This

465 leads to the follow renamings:

467 CTT/Main.thy ~> CTT/CTT.thy

468 ZF/Main.thy ~> ZF/ZF.thy

469 ZF/Main_ZF.thy ~> ZF/ZF.thy

470 ZF/Main_ZFC.thy ~> ZF/ZFC.thy

471 ZF/ZF.thy ~> ZF/ZF_Base.thy

473 INCOMPATIBILITY.

475 * Commands 'alias' and 'type_alias' introduce aliases for constants and

476 type constructors, respectively. This allows adhoc changes to name-space

477 accesses within global or local theory contexts, e.g. within a 'bundle'.

479 * Document antiquotations @{prf} and @{full_prf} output proof terms

480 (again) in the same way as commands 'prf' and 'full_prf'.

482 * Computations generated by the code generator can be embedded directly

483 into ML, alongside with @{code} antiquotations, using the following

484 antiquotations:

486 @{computation ... terms: ... datatypes: ...} :

487 ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a

488 @{computation_conv ... terms: ... datatypes: ...} :

489 (Proof.context -> 'ml -> conv) -> Proof.context -> conv

490 @{computation_check terms: ... datatypes: ...} : Proof.context -> conv

492 See src/HOL/ex/Computations.thy,

493 src/HOL/Decision_Procs/Commutative_Ring.thy and

494 src/HOL/Decision_Procs/Reflective_Field.thy for examples and the

495 tutorial on code generation.

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

500 * Session-qualified theory imports allow the Prover IDE to process

501 arbitrary theory hierarchies independently of the underlying logic

502 session image (e.g. option "isabelle jedit -l"), but the directory

503 structure needs to be known in advance (e.g. option "isabelle jedit -d"

504 or a line in the file $ISABELLE_HOME_USER/ROOTS).

506 * The PIDE document model maintains file content independently of the

507 status of jEdit editor buffers. Reloading jEdit buffers no longer causes

508 changes of formal document content. Theory dependencies are always

509 resolved internally, without the need for corresponding editor buffers.

510 The system option "jedit_auto_load" has been discontinued: it is

511 effectively always enabled.

513 * The Theories dockable provides a "Purge" button, in order to restrict

514 the document model to theories that are required for open editor

515 buffers.

517 * The Theories dockable indicates the overall status of checking of each

518 entry. When all forked tasks of a theory are finished, the border is

519 painted with thick lines; remaining errors in this situation are

520 represented by a different border color.

522 * Automatic indentation is more careful to avoid redundant spaces in

523 intermediate situations. Keywords are indented after input (via typed

524 characters or completion); see also option "jedit_indent_input".

526 * Action "isabelle.preview" opens an HTML preview of the current theory

527 document in the default web browser.

529 * Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT

530 entry of the specified logic session in the editor, while its parent is

531 used for formal checking.

533 * The main Isabelle/jEdit plugin may be restarted manually (using the

534 jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains

535 enabled at all times.

537 * Update to current jedit-5.4.0.

540 *** Pure ***

542 * Deleting the last code equations for a particular function using

543 [code del] results in function with no equations (runtime abort) rather

544 than an unimplemented function (generation time abort). Use explicit

545 [[code drop:]] to enforce the latter. Minor INCOMPATIBILITY.

547 * Proper concept of code declarations in code.ML:

548 - Regular code declarations act only on the global theory level, being

549 ignored with warnings if syntactically malformed.

550 - Explicitly global code declarations yield errors if syntactically

551 malformed.

552 - Default code declarations are silently ignored if syntactically

553 malformed.

554 Minor INCOMPATIBILITY.

556 * Clarified and standardized internal data bookkeeping of code

557 declarations: history of serials allows to track potentially

558 non-monotonous declarations appropriately. Minor INCOMPATIBILITY.

561 *** HOL ***

563 * The Nunchaku model finder is now part of "Main".

565 * SMT module:

566 - A new option, 'smt_nat_as_int', has been added to translate 'nat' to

567 'int' and benefit from the SMT solver's theory reasoning. It is

568 disabled by default.

569 - The legacy module "src/HOL/Library/Old_SMT.thy" has been removed.

570 - Several small issues have been rectified in the 'smt' command.

572 * (Co)datatype package: The 'size_gen_o_map' lemma is no longer

573 generated for datatypes with type class annotations. As a result, the

574 tactic that derives it no longer fails on nested datatypes. Slight

575 INCOMPATIBILITY.

577 * Command and antiquotation "value" with modified default strategy:

578 terms without free variables are always evaluated using plain evaluation

579 only, with no fallback on normalization by evaluation. Minor

580 INCOMPATIBILITY.

582 * Theories "GCD" and "Binomial" are already included in "Main" (instead

583 of "Complex_Main").

585 * Constant "surj" is a full input/output abbreviation (again).

586 Minor INCOMPATIBILITY.

588 * Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.

589 INCOMPATIBILITY.

591 * Renamed ii to imaginary_unit in order to free up ii as a variable

592 name. The syntax \<i> remains available. INCOMPATIBILITY.

594 * Dropped abbreviations transP, antisymP, single_valuedP; use constants

595 transp, antisymp, single_valuedp instead. INCOMPATIBILITY.

597 * Constant "subseq" in Topological_Spaces has been removed -- it is

598 subsumed by "strict_mono". Some basic lemmas specific to "subseq" have

599 been renamed accordingly, e.g. "subseq_o" -> "strict_mono_o" etc.

601 * Theory List: "sublist" renamed to "nths" in analogy with "nth", and

602 "sublisteq" renamed to "subseq". Minor INCOMPATIBILITY.

604 * Theory List: new generic function "sorted_wrt".

606 * Named theorems mod_simps covers various congruence rules concerning

607 mod, replacing former zmod_simps. INCOMPATIBILITY.

609 * Swapped orientation of congruence rules mod_add_left_eq,

610 mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,

611 mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,

612 mod_diff_eq. INCOMPATIBILITY.

614 * Generalized some facts:

615 measure_induct_rule

616 measure_induct

617 zminus_zmod ~> mod_minus_eq

618 zdiff_zmod_left ~> mod_diff_left_eq

619 zdiff_zmod_right ~> mod_diff_right_eq

620 zmod_eq_dvd_iff ~> mod_eq_dvd_iff

621 INCOMPATIBILITY.

623 * Algebraic type class hierarchy of euclidean (semi)rings in HOL:

624 euclidean_(semi)ring, euclidean_(semi)ring_cancel,

625 unique_euclidean_(semi)ring; instantiation requires provision of a

626 euclidean size.

628 * Theory "HOL-Number_Theory.Euclidean_Algorithm" has been reworked:

629 - Euclidean induction is available as rule eucl_induct.

630 - Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm,

631 Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow

632 easy instantiation of euclidean (semi)rings as GCD (semi)rings.

633 - Coefficients obtained by extended euclidean algorithm are

634 available as "bezout_coefficients".

635 INCOMPATIBILITY.

637 * Theory "Number_Theory.Totient" introduces basic notions about Euler's

638 totient function previously hidden as solitary example in theory

639 Residues. Definition changed so that "totient 1 = 1" in agreement with

640 the literature. Minor INCOMPATIBILITY.

642 * New styles in theory "HOL-Library.LaTeXsugar":

643 - "dummy_pats" for printing equations with "_" on the lhs;

644 - "eta_expand" for printing eta-expanded terms.

646 * Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has

647 been renamed to bij_swap_compose_bij. INCOMPATIBILITY.

649 * New theory "HOL-Library.Going_To_Filter" providing the "f going_to F"

650 filter for describing points x such that f(x) is in the filter F.

652 * Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been

653 renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name

654 space. INCOMPATIBILITY.

656 * Theory "HOL-Library.FinFun" has been moved to AFP (again).

657 INCOMPATIBILITY.

659 * Theory "HOL-Library.FuncSet": some old and rarely used ASCII

660 replacement syntax has been removed. INCOMPATIBILITY, standard syntax

661 with symbols should be used instead. The subsequent commands help to

662 reproduce the old forms, e.g. to simplify porting old theories:

664 syntax (ASCII)

665 "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3PIE _:_./ _)" 10)

666 "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3PI _:_./ _)" 10)

667 "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("(3%_:_./ _)" [0,0,3] 3)

669 * Theory "HOL-Library.Multiset": the simprocs on subsets operators of

670 multisets have been renamed:

672 msetless_cancel_numerals ~> msetsubset_cancel

673 msetle_cancel_numerals ~> msetsubset_eq_cancel

675 INCOMPATIBILITY.

677 * Theory "HOL-Library.Pattern_Aliases" provides input and output syntax

678 for pattern aliases as known from Haskell, Scala and ML.

680 * Theory "HOL-Library.Uprod" formalizes the type of unordered pairs.

682 * Session HOL-Analysis: more material involving arcs, paths, covering

683 spaces, innessential maps, retracts, infinite products, simplicial

684 complexes. Baire Category theorem. Major results include the Jordan

685 Curve Theorem and the Great Picard Theorem.

687 * Session HOL-Algebra has been extended by additional lattice theory:

688 the Knaster-Tarski fixed point theorem and Galois Connections.

690 * Sessions HOL-Computational_Algebra and HOL-Number_Theory: new notions

691 of squarefreeness, n-th powers, and prime powers.

693 * Session "HOL-Computional_Algebra" covers many previously scattered

694 theories, notably Euclidean_Algorithm, Factorial_Ring,

695 Formal_Power_Series, Fraction_Field, Fundamental_Theorem_Algebra,

696 Normalized_Fraction, Polynomial_FPS, Polynomial, Primes. Minor

697 INCOMPATIBILITY.

700 *** System ***

702 * Isabelle/Scala: the SQL module supports access to relational

703 databases, either as plain file (SQLite) or full-scale server

704 (PostgreSQL via local port or remote ssh connection).

706 * Results of "isabelle build" are recorded as SQLite database (i.e.

707 "Application File Format" in the sense of

708 https://www.sqlite.org/appfileformat.html). This allows systematic

709 access via operations from module Sessions.Store in Isabelle/Scala.

711 * System option "parallel_proofs" is 1 by default (instead of more

712 aggressive 2). This requires less heap space and avoids burning parallel

713 CPU cycles, while full subproof parallelization is enabled for repeated

714 builds (according to parallel_subproofs_threshold).

716 * System option "record_proofs" allows to change the global

717 Proofterm.proofs variable for a session. Regular values are are 0, 1, 2;

718 a negative value means the current state in the ML heap image remains

719 unchanged.

721 * Isabelle settings variable ISABELLE_SCALA_BUILD_OPTIONS has been

722 renamed to ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY.

724 * Isabelle settings variables ISABELLE_WINDOWS_PLATFORM,

725 ISABELLE_WINDOWS_PLATFORM32, ISABELLE_WINDOWS_PLATFORM64 indicate the

726 native Windows platform (independently of the Cygwin installation). This

727 is analogous to ISABELLE_PLATFORM, ISABELLE_PLATFORM32,

728 ISABELLE_PLATFORM64.

730 * Command-line tool "isabelle build_docker" builds a Docker image from

731 the Isabelle application bundle for Linux. See also

732 https://hub.docker.com/r/makarius/isabelle

734 * Command-line tool "isabelle vscode_server" provides a Language Server

735 Protocol implementation, e.g. for the Visual Studio Code editor. It

736 serves as example for alternative PIDE front-ends.

738 * Command-line tool "isabelle imports" helps to maintain theory imports

739 wrt. session structure. Examples for the main Isabelle distribution:

741 isabelle imports -I -a

742 isabelle imports -U -a

743 isabelle imports -U -i -a

744 isabelle imports -M -a -d '~~/src/Benchmarks'

748 New in Isabelle2016-1 (December 2016)

749 -------------------------------------

751 *** General ***

753 * Splitter in proof methods "simp", "auto" and friends:

754 - The syntax "split add" has been discontinued, use plain "split",

755 INCOMPATIBILITY.

756 - For situations with many conditional or case expressions, there is

757 an alternative splitting strategy that can be much faster. It is

758 selected by writing "split!" instead of "split". It applies safe

759 introduction and elimination rules after each split rule. As a

760 result the subgoal may be split into several subgoals.

762 * Command 'bundle' provides a local theory target to define a bundle

763 from the body of specification commands (such as 'declare',

764 'declaration', 'notation', 'lemmas', 'lemma'). For example:

766 bundle foo

767 begin

768 declare a [simp]

769 declare b [intro]

770 end

772 * Command 'unbundle' is like 'include', but works within a local theory

773 context. Unlike "context includes ... begin", the effect of 'unbundle'

774 on the target context persists, until different declarations are given.

776 * Simplified outer syntax: uniform category "name" includes long

777 identifiers. Former "xname" / "nameref" / "name reference" has been

778 discontinued.

780 * Embedded content (e.g. the inner syntax of types, terms, props) may be

781 delimited uniformly via cartouches. This works better than old-fashioned

782 quotes when sub-languages are nested.

784 * Mixfix annotations support general block properties, with syntax

785 "(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",

786 "unbreakable", "markup". The existing notation "(DIGITS" is equivalent

787 to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks

788 is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY.

790 * Proof method "blast" is more robust wrt. corner cases of Pure

791 statements without object-logic judgment.

793 * Commands 'prf' and 'full_prf' are somewhat more informative (again):

794 proof terms are reconstructed and cleaned from administrative thm nodes.

796 * Code generator: config option "code_timing" triggers measurements of

797 different phases of code generation. See src/HOL/ex/Code_Timing.thy for

798 examples.

800 * Code generator: implicits in Scala (stemming from type class

801 instances) are generated into companion object of corresponding type

802 class, to resolve some situations where ambiguities may occur.

804 * Solve direct: option "solve_direct_strict_warnings" gives explicit

805 warnings for lemma statements with trivial proofs.

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

810 * More aggressive flushing of machine-generated input, according to

811 system option editor_generated_input_delay (in addition to existing

812 editor_input_delay for regular user edits). This may affect overall PIDE

813 reactivity and CPU usage.

815 * Syntactic indentation according to Isabelle outer syntax. Action

816 "indent-lines" (shortcut C+i) indents the current line according to

817 command keywords and some command substructure. Action

818 "isabelle.newline" (shortcut ENTER) indents the old and the new line

819 according to command keywords only; see also option

820 "jedit_indent_newline".

822 * Semantic indentation for unstructured proof scripts ('apply' etc.) via

823 number of subgoals. This requires information of ongoing document

824 processing and may thus lag behind, when the user is editing too

825 quickly; see also option "jedit_script_indent" and

826 "jedit_script_indent_limit".

828 * Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'

829 are treated as delimiters for fold structure; 'begin' and 'end'

830 structure of theory specifications is treated as well.

832 * Command 'proof' provides information about proof outline with cases,

833 e.g. for proof methods "cases", "induct", "goal_cases".

835 * Completion templates for commands involving "begin ... end" blocks,

836 e.g. 'context', 'notepad'.

838 * Sidekick parser "isabelle-context" shows nesting of context blocks

839 according to 'begin' and 'end' structure.

841 * Highlighting of entity def/ref positions wrt. cursor.

843 * Action "isabelle.select-entity" (shortcut CS+ENTER) selects all

844 occurrences of the formal entity at the caret position. This facilitates

845 systematic renaming.

847 * PIDE document markup works across multiple Isar commands, e.g. the

848 results established at the end of a proof are properly identified in the

849 theorem statement.

851 * Cartouche abbreviations work both for " and ` to accomodate typical

852 situations where old ASCII notation may be updated.

854 * Dockable window "Symbols" also provides access to 'abbrevs' from the

855 outer syntax of the current theory buffer. This provides clickable

856 syntax templates, including entries with empty abbrevs name (which are

857 inaccessible via keyboard completion).

859 * IDE support for the Isabelle/Pure bootstrap process, with the

860 following independent stages:

862 src/Pure/ROOT0.ML

863 src/Pure/ROOT.ML

864 src/Pure/Pure.thy

865 src/Pure/ML_Bootstrap.thy

867 The ML ROOT files act like quasi-theories in the context of theory

868 ML_Bootstrap: this allows continuous checking of all loaded ML files.

869 The theory files are presented with a modified header to import Pure

870 from the running Isabelle instance. Results from changed versions of

871 each stage are *not* propagated to the next stage, and isolated from the

872 actual Isabelle/Pure that runs the IDE itself. The sequential

873 dependencies of the above files are only observed for batch build.

875 * Isabelle/ML and Standard ML files are presented in Sidekick with the

876 tree structure of section headings: this special comment format is

877 described in "implementation" chapter 0, e.g. (*** section ***).

879 * Additional abbreviations for syntactic completion may be specified

880 within the theory header as 'abbrevs'. The theory syntax for 'keywords'

881 has been simplified accordingly: optional abbrevs need to go into the

882 new 'abbrevs' section.

884 * Global abbreviations via $ISABELLE_HOME/etc/abbrevs and

885 $ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor

886 INCOMPATIBILITY, use 'abbrevs' within theory header instead.

888 * Action "isabelle.keymap-merge" asks the user to resolve pending

889 Isabelle keymap changes that are in conflict with the current jEdit

890 keymap; non-conflicting changes are always applied implicitly. This

891 action is automatically invoked on Isabelle/jEdit startup and thus

892 increases chances that users see new keyboard shortcuts when re-using

893 old keymaps.

895 * ML and document antiquotations for file-systems paths are more uniform

896 and diverse:

898 @{path NAME} -- no file-system check

899 @{file NAME} -- check for plain file

900 @{dir NAME} -- check for directory

902 Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may

903 have to be changed.

906 *** Document preparation ***

908 * New symbol \<circle>, e.g. for temporal operator.

910 * New document and ML antiquotation @{locale} for locales, similar to

911 existing antiquotation @{class}.

913 * Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> --

914 this allows special forms of document output.

916 * Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control

917 symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its

918 derivatives.

920 * \<^raw:...> symbols are no longer supported.

922 * Old 'header' command is no longer supported (legacy since

923 Isabelle2015).

926 *** Isar ***

928 * Many specification elements support structured statements with 'if' /

929 'for' eigen-context, e.g. 'axiomatization', 'abbreviation',

930 'definition', 'inductive', 'function'.

932 * Toplevel theorem statements support eigen-context notation with 'if' /

933 'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the

934 traditional long statement form (in prefix). Local premises are called

935 "that" or "assms", respectively. Empty premises are *not* bound in the

936 context: INCOMPATIBILITY.

938 * Command 'define' introduces a local (non-polymorphic) definition, with

939 optional abstraction over local parameters. The syntax resembles

940 'definition' and 'obtain'. It fits better into the Isar language than

941 old 'def', which is now a legacy feature.

943 * Command 'obtain' supports structured statements with 'if' / 'for'

944 context.

946 * Command '\<proof>' is an alias for 'sorry', with different

947 typesetting. E.g. to produce proof holes in examples and documentation.

949 * The defining position of a literal fact \<open>prop\<close> is maintained more

950 carefully, and made accessible as hyperlink in the Prover IDE.

952 * Commands 'finally' and 'ultimately' used to expose the result as

953 literal fact: this accidental behaviour has been discontinued. Rare

954 INCOMPATIBILITY, use more explicit means to refer to facts in Isar.

956 * Command 'axiomatization' has become more restrictive to correspond

957 better to internal axioms as singleton facts with mandatory name. Minor

958 INCOMPATIBILITY.

960 * Proof methods may refer to the main facts via the dynamic fact

961 "method_facts". This is particularly useful for Eisbach method

962 definitions.

964 * Proof method "use" allows to modify the main facts of a given method

965 expression, e.g.

967 (use facts in simp)

968 (use facts in \<open>simp add: ...\<close>)

970 * The old proof method "default" has been removed (legacy since

971 Isabelle2016). INCOMPATIBILITY, use "standard" instead.

974 *** Pure ***

976 * Pure provides basic versions of proof methods "simp" and "simp_all"

977 that only know about meta-equality (==). Potential INCOMPATIBILITY in

978 theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order

979 is relevant to avoid confusion of Pure.simp vs. HOL.simp.

981 * The command 'unfolding' and proof method "unfold" include a second

982 stage where given equations are passed through the attribute "abs_def"

983 before rewriting. This ensures that definitions are fully expanded,

984 regardless of the actual parameters that are provided. Rare

985 INCOMPATIBILITY in some corner cases: use proof method (simp only:)

986 instead, or declare [[unfold_abs_def = false]] in the proof context.

988 * Type-inference improves sorts of newly introduced type variables for

989 the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).

990 Thus terms like "f x" or "\<And>x. P x" without any further syntactic context

991 produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare

992 INCOMPATIBILITY, need to provide explicit type constraints for Pure

993 types where this is really intended.

996 *** HOL ***

998 * New proof method "argo" using the built-in Argo solver based on SMT

999 technology. The method can be used to prove goals of quantifier-free

1000 propositional logic, goals based on a combination of quantifier-free

1001 propositional logic with equality, and goals based on a combination of

1002 quantifier-free propositional logic with linear real arithmetic

1003 including min/max/abs. See HOL/ex/Argo_Examples.thy for examples.

1005 * The new "nunchaku" command integrates the Nunchaku model finder. The

1006 tool is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details.

1008 * Metis: The problem encoding has changed very slightly. This might

1009 break existing proofs. INCOMPATIBILITY.

1011 * Sledgehammer:

1012 - The MaSh relevance filter is now faster than before.

1013 - Produce syntactically correct Vampire 4.0 problem files.

1015 * (Co)datatype package:

1016 - New commands for defining corecursive functions and reasoning about

1017 them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',

1018 'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof

1019 method. See 'isabelle doc corec'.

1020 - The predicator :: ('a \<Rightarrow> bool) \<Rightarrow> 'a F \<Rightarrow> bool is now a first-class

1021 citizen in bounded natural functors.

1022 - 'primrec' now allows nested calls through the predicator in addition

1023 to the map function.

1024 - 'bnf' automatically discharges reflexive proof obligations.

1025 - 'bnf' outputs a slightly modified proof obligation expressing rel in

1026 terms of map and set

1027 (not giving a specification for rel makes this one reflexive).

1028 - 'bnf' outputs a new proof obligation expressing pred in terms of set

1029 (not giving a specification for pred makes this one reflexive).

1030 INCOMPATIBILITY: manual 'bnf' declarations may need adjustment.

1031 - Renamed lemmas:

1032 rel_prod_apply ~> rel_prod_inject

1033 pred_prod_apply ~> pred_prod_inject

1034 INCOMPATIBILITY.

1035 - The "size" plugin has been made compatible again with locales.

1036 - The theorems about "rel" and "set" may have a slightly different (but

1037 equivalent) form.

1038 INCOMPATIBILITY.

1040 * The 'coinductive' command produces a proper coinduction rule for

1041 mutual coinductive predicates. This new rule replaces the old rule,

1042 which exposed details of the internal fixpoint construction and was

1043 hard to use. INCOMPATIBILITY.

1045 * New abbreviations for negated existence (but not bounded existence):

1047 \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)

1048 \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)

1050 * The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"

1051 has been removed for output. It is retained for input only, until it is

1052 eliminated altogether.

1054 * The unique existence quantifier no longer provides 'binder' syntax,

1055 but uses syntax translations (as for bounded unique existence). Thus

1056 iterated quantification \<exists>!x y. P x y with its slightly confusing

1057 sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead,

1058 pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y

1059 (analogous to existing notation \<exists>!(x, y)\<in>A. P x y). Potential

1060 INCOMPATIBILITY in rare situations.

1062 * Conventional syntax "%(). t" for unit abstractions. Slight syntactic

1063 INCOMPATIBILITY.

1065 * Renamed constants and corresponding theorems:

1067 setsum ~> sum

1068 setprod ~> prod

1069 listsum ~> sum_list

1070 listprod ~> prod_list

1072 INCOMPATIBILITY.

1074 * Sligthly more standardized theorem names:

1075 sgn_times ~> sgn_mult

1076 sgn_mult' ~> Real_Vector_Spaces.sgn_mult

1077 divide_zero_left ~> div_0

1078 zero_mod_left ~> mod_0

1079 divide_zero ~> div_by_0

1080 divide_1 ~> div_by_1

1081 nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left

1082 div_mult_self1_is_id ~> nonzero_mult_div_cancel_left

1083 nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right

1084 div_mult_self2_is_id ~> nonzero_mult_div_cancel_right

1085 is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left

1086 is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right

1087 mod_div_equality ~> div_mult_mod_eq

1088 mod_div_equality2 ~> mult_div_mod_eq

1089 mod_div_equality3 ~> mod_div_mult_eq

1090 mod_div_equality4 ~> mod_mult_div_eq

1091 minus_div_eq_mod ~> minus_div_mult_eq_mod

1092 minus_div_eq_mod2 ~> minus_mult_div_eq_mod

1093 minus_mod_eq_div ~> minus_mod_eq_div_mult

1094 minus_mod_eq_div2 ~> minus_mod_eq_mult_div

1095 div_mod_equality' ~> minus_mod_eq_div_mult [symmetric]

1096 mod_div_equality' ~> minus_div_mult_eq_mod [symmetric]

1097 zmod_zdiv_equality ~> mult_div_mod_eq [symmetric]

1098 zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric]

1099 Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]

1100 mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]

1101 zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric]

1102 div_1 ~> div_by_Suc_0

1103 mod_1 ~> mod_by_Suc_0

1104 INCOMPATIBILITY.

1106 * New type class "idom_abs_sgn" specifies algebraic properties

1107 of sign and absolute value functions. Type class "sgn_if" has

1108 disappeared. Slight INCOMPATIBILITY.

1110 * Dedicated syntax LENGTH('a) for length of types.

1112 * Characters (type char) are modelled as finite algebraic type

1113 corresponding to {0..255}.

1115 - Logical representation:

1116 * 0 is instantiated to the ASCII zero character.

1117 * All other characters are represented as "Char n"

1118 with n being a raw numeral expression less than 256.

1119 * Expressions of the form "Char n" with n greater than 255

1120 are non-canonical.

1121 - Printing and parsing:

1122 * Printable characters are printed and parsed as "CHR ''\<dots>''"

1123 (as before).

1124 * The ASCII zero character is printed and parsed as "0".

1125 * All other canonical characters are printed as "CHR 0xXX"

1126 with XX being the hexadecimal character code. "CHR n"

1127 is parsable for every numeral expression n.

1128 * Non-canonical characters have no special syntax and are

1129 printed as their logical representation.

1130 - Explicit conversions from and to the natural numbers are

1131 provided as char_of_nat, nat_of_char (as before).

1132 - The auxiliary nibble type has been discontinued.

1134 INCOMPATIBILITY.

1136 * Type class "div" with operation "mod" renamed to type class "modulo"

1137 with operation "modulo", analogously to type class "divide". This

1138 eliminates the need to qualify any of those names in the presence of

1139 infix "mod" syntax. INCOMPATIBILITY.

1141 * Statements and proofs of Knaster-Tarski fixpoint combinators lfp/gfp

1142 have been clarified. The fixpoint properties are lfp_fixpoint, its

1143 symmetric lfp_unfold (as before), and the duals for gfp. Auxiliary items

1144 for the proof (lfp_lemma2 etc.) are no longer exported, but can be

1145 easily recovered by composition with eq_refl. Minor INCOMPATIBILITY.

1147 * Constant "surj" is a mere input abbreviation, to avoid hiding an

1148 equation in term output. Minor INCOMPATIBILITY.

1150 * Command 'code_reflect' accepts empty constructor lists for datatypes,

1151 which renders those abstract effectively.

1153 * Command 'export_code' checks given constants for abstraction

1154 violations: a small guarantee that given constants specify a safe

1155 interface for the generated code.

1157 * Code generation for Scala: ambiguous implicts in class diagrams are

1158 spelt out explicitly.

1160 * Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on

1161 explicitly provided auxiliary definitions for required type class

1162 dictionaries rather than half-working magic. INCOMPATIBILITY, see the

1163 tutorial on code generation for details.

1165 * Theory Set_Interval: substantial new theorems on indexed sums and

1166 products.

1168 * Locale bijection establishes convenient default simp rules such as

1169 "inv f (f a) = a" for total bijections.

1171 * Abstract locales semigroup, abel_semigroup, semilattice,

1172 semilattice_neutr, ordering, ordering_top, semilattice_order,

1173 semilattice_neutr_order, comm_monoid_set, semilattice_set,

1174 semilattice_neutr_set, semilattice_order_set,

1175 semilattice_order_neutr_set monoid_list, comm_monoid_list,

1176 comm_monoid_list_set, comm_monoid_mset, comm_monoid_fun use boldified

1177 syntax uniformly that does not clash with corresponding global syntax.

1178 INCOMPATIBILITY.

1180 * Former locale lifting_syntax is now a bundle, which is easier to

1181 include in a local context or theorem statement, e.g. "context includes

1182 lifting_syntax begin ... end". Minor INCOMPATIBILITY.

1184 * Some old / obsolete theorems have been renamed / removed, potential

1185 INCOMPATIBILITY.

1187 nat_less_cases -- removed, use linorder_cases instead

1188 inv_image_comp -- removed, use image_inv_f_f instead

1189 image_surj_f_inv_f ~> image_f_inv_f

1191 * Some theorems about groups and orders have been generalised from

1192 groups to semi-groups that are also monoids:

1193 le_add_same_cancel1

1194 le_add_same_cancel2

1195 less_add_same_cancel1

1196 less_add_same_cancel2

1197 add_le_same_cancel1

1198 add_le_same_cancel2

1199 add_less_same_cancel1

1200 add_less_same_cancel2

1202 * Some simplifications theorems about rings have been removed, since

1203 superseeded by a more general version:

1204 less_add_cancel_left_greater_zero ~> less_add_same_cancel1

1205 less_add_cancel_right_greater_zero ~> less_add_same_cancel2

1206 less_eq_add_cancel_left_greater_eq_zero ~> le_add_same_cancel1

1207 less_eq_add_cancel_right_greater_eq_zero ~> le_add_same_cancel2

1208 less_eq_add_cancel_left_less_eq_zero ~> add_le_same_cancel1

1209 less_eq_add_cancel_right_less_eq_zero ~> add_le_same_cancel2

1210 less_add_cancel_left_less_zero ~> add_less_same_cancel1

1211 less_add_cancel_right_less_zero ~> add_less_same_cancel2

1212 INCOMPATIBILITY.

1214 * Renamed split_if -> if_split and split_if_asm -> if_split_asm to

1215 resemble the f.split naming convention, INCOMPATIBILITY.

1217 * Added class topological_monoid.

1219 * The following theorems have been renamed:

1221 setsum_left_distrib ~> sum_distrib_right

1222 setsum_right_distrib ~> sum_distrib_left

1224 INCOMPATIBILITY.

1226 * Compound constants INFIMUM and SUPREMUM are mere abbreviations now.

1227 INCOMPATIBILITY.

1229 * "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional

1230 comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f `

1231 A)".

1233 * Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY.

1235 * The type class ordered_comm_monoid_add is now called

1236 ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add

1237 is introduced as the combination of ordered_ab_semigroup_add +

1238 comm_monoid_add. INCOMPATIBILITY.

1240 * Introduced the type classes canonically_ordered_comm_monoid_add and

1241 dioid.

1243 * Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When

1244 instantiating linordered_semiring_strict and ordered_ab_group_add, an

1245 explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might

1246 be required. INCOMPATIBILITY.

1248 * Dropped various legacy fact bindings, whose replacements are often

1249 of a more general type also:

1250 lcm_left_commute_nat ~> lcm.left_commute

1251 lcm_left_commute_int ~> lcm.left_commute

1252 gcd_left_commute_nat ~> gcd.left_commute

1253 gcd_left_commute_int ~> gcd.left_commute

1254 gcd_greatest_iff_nat ~> gcd_greatest_iff

1255 gcd_greatest_iff_int ~> gcd_greatest_iff

1256 coprime_dvd_mult_nat ~> coprime_dvd_mult

1257 coprime_dvd_mult_int ~> coprime_dvd_mult

1258 zpower_numeral_even ~> power_numeral_even

1259 gcd_mult_cancel_nat ~> gcd_mult_cancel

1260 gcd_mult_cancel_int ~> gcd_mult_cancel

1261 div_gcd_coprime_nat ~> div_gcd_coprime

1262 div_gcd_coprime_int ~> div_gcd_coprime

1263 zpower_numeral_odd ~> power_numeral_odd

1264 zero_less_int_conv ~> of_nat_0_less_iff

1265 gcd_greatest_nat ~> gcd_greatest

1266 gcd_greatest_int ~> gcd_greatest

1267 coprime_mult_nat ~> coprime_mult

1268 coprime_mult_int ~> coprime_mult

1269 lcm_commute_nat ~> lcm.commute

1270 lcm_commute_int ~> lcm.commute

1271 int_less_0_conv ~> of_nat_less_0_iff

1272 gcd_commute_nat ~> gcd.commute

1273 gcd_commute_int ~> gcd.commute

1274 Gcd_insert_nat ~> Gcd_insert

1275 Gcd_insert_int ~> Gcd_insert

1276 of_int_int_eq ~> of_int_of_nat_eq

1277 lcm_least_nat ~> lcm_least

1278 lcm_least_int ~> lcm_least

1279 lcm_assoc_nat ~> lcm.assoc

1280 lcm_assoc_int ~> lcm.assoc

1281 int_le_0_conv ~> of_nat_le_0_iff

1282 int_eq_0_conv ~> of_nat_eq_0_iff

1283 Gcd_empty_nat ~> Gcd_empty

1284 Gcd_empty_int ~> Gcd_empty

1285 gcd_assoc_nat ~> gcd.assoc

1286 gcd_assoc_int ~> gcd.assoc

1287 zero_zle_int ~> of_nat_0_le_iff

1288 lcm_dvd2_nat ~> dvd_lcm2

1289 lcm_dvd2_int ~> dvd_lcm2

1290 lcm_dvd1_nat ~> dvd_lcm1

1291 lcm_dvd1_int ~> dvd_lcm1

1292 gcd_zero_nat ~> gcd_eq_0_iff

1293 gcd_zero_int ~> gcd_eq_0_iff

1294 gcd_dvd2_nat ~> gcd_dvd2

1295 gcd_dvd2_int ~> gcd_dvd2

1296 gcd_dvd1_nat ~> gcd_dvd1

1297 gcd_dvd1_int ~> gcd_dvd1

1298 int_numeral ~> of_nat_numeral

1299 lcm_ac_nat ~> ac_simps

1300 lcm_ac_int ~> ac_simps

1301 gcd_ac_nat ~> ac_simps

1302 gcd_ac_int ~> ac_simps

1303 abs_int_eq ~> abs_of_nat

1304 zless_int ~> of_nat_less_iff

1305 zdiff_int ~> of_nat_diff

1306 zadd_int ~> of_nat_add

1307 int_mult ~> of_nat_mult

1308 int_Suc ~> of_nat_Suc

1309 inj_int ~> inj_of_nat

1310 int_1 ~> of_nat_1

1311 int_0 ~> of_nat_0

1312 Lcm_empty_nat ~> Lcm_empty

1313 Lcm_empty_int ~> Lcm_empty

1314 Lcm_insert_nat ~> Lcm_insert

1315 Lcm_insert_int ~> Lcm_insert

1316 comp_fun_idem_gcd_nat ~> comp_fun_idem_gcd

1317 comp_fun_idem_gcd_int ~> comp_fun_idem_gcd

1318 comp_fun_idem_lcm_nat ~> comp_fun_idem_lcm

1319 comp_fun_idem_lcm_int ~> comp_fun_idem_lcm

1320 Lcm_eq_0 ~> Lcm_eq_0_I

1321 Lcm0_iff ~> Lcm_0_iff

1322 Lcm_dvd_int ~> Lcm_least

1323 divides_mult_nat ~> divides_mult

1324 divides_mult_int ~> divides_mult

1325 lcm_0_nat ~> lcm_0_right

1326 lcm_0_int ~> lcm_0_right

1327 lcm_0_left_nat ~> lcm_0_left

1328 lcm_0_left_int ~> lcm_0_left

1329 dvd_gcd_D1_nat ~> dvd_gcdD1

1330 dvd_gcd_D1_int ~> dvd_gcdD1

1331 dvd_gcd_D2_nat ~> dvd_gcdD2

1332 dvd_gcd_D2_int ~> dvd_gcdD2

1333 coprime_dvd_mult_iff_nat ~> coprime_dvd_mult_iff

1334 coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff

1335 realpow_minus_mult ~> power_minus_mult

1336 realpow_Suc_le_self ~> power_Suc_le_self

1337 dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest

1338 INCOMPATIBILITY.

1340 * Renamed HOL/Quotient_Examples/FSet.thy to

1341 HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY.

1343 * Session HOL-Library: theory FinFun bundles "finfun_syntax" and

1344 "no_finfun_syntax" allow to control optional syntax in local contexts;

1345 this supersedes former theory FinFun_Syntax. INCOMPATIBILITY, e.g. use

1346 "unbundle finfun_syntax" to imitate import of

1347 "~~/src/HOL/Library/FinFun_Syntax".

1349 * Session HOL-Library: theory Multiset_Permutations (executably) defines

1350 the set of permutations of a given set or multiset, i.e. the set of all

1351 lists that contain every element of the carrier (multi-)set exactly

1352 once.

1354 * Session HOL-Library: multiset membership is now expressed using

1355 set_mset rather than count.

1357 - Expressions "count M a > 0" and similar simplify to membership

1358 by default.

1360 - Converting between "count M a = 0" and non-membership happens using

1361 equations count_eq_zero_iff and not_in_iff.

1363 - Rules count_inI and in_countE obtain facts of the form

1364 "count M a = n" from membership.

1366 - Rules count_in_diffI and in_diff_countE obtain facts of the form

1367 "count M a = n + count N a" from membership on difference sets.

1369 INCOMPATIBILITY.

1371 * Session HOL-Library: theory LaTeXsugar uses new-style "dummy_pats" for

1372 displaying equations in functional programming style --- variables

1373 present on the left-hand but not on the righ-hand side are replaced by

1374 underscores.

1376 * Session HOL-Library: theory Combinator_PER provides combinator to

1377 build partial equivalence relations from a predicate and an equivalence

1378 relation.

1380 * Session HOL-Library: theory Perm provides basic facts about almost

1381 everywhere fix bijections.

1383 * Session HOL-Library: theory Normalized_Fraction allows viewing an

1384 element of a field of fractions as a normalized fraction (i.e. a pair of

1385 numerator and denominator such that the two are coprime and the

1386 denominator is normalized wrt. unit factors).

1388 * Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis.

1390 * Session HOL-Multivariate_Analysis has been renamed to HOL-Analysis.

1392 * Session HOL-Analysis: measure theory has been moved here from

1393 HOL-Probability. When importing HOL-Analysis some theorems need

1394 additional name spaces prefixes due to name clashes. INCOMPATIBILITY.

1396 * Session HOL-Analysis: more complex analysis including Cauchy's

1397 inequality, Liouville theorem, open mapping theorem, maximum modulus

1398 principle, Residue theorem, Schwarz Lemma.

1400 * Session HOL-Analysis: Theory of polyhedra: faces, extreme points,

1401 polytopes, and the Krein–Milman Minkowski theorem.

1403 * Session HOL-Analysis: Numerous results ported from the HOL Light

1404 libraries: homeomorphisms, continuous function extensions, invariance of

1405 domain.

1407 * Session HOL-Probability: the type of emeasure and nn_integral was

1408 changed from ereal to ennreal, INCOMPATIBILITY.

1410 emeasure :: 'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal

1411 nn_integral :: 'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal

1413 * Session HOL-Probability: Code generation and QuickCheck for

1414 Probability Mass Functions.

1416 * Session HOL-Probability: theory Random_Permutations contains some

1417 theory about choosing a permutation of a set uniformly at random and

1418 folding over a list in random order.

1420 * Session HOL-Probability: theory SPMF formalises discrete

1421 subprobability distributions.

1423 * Session HOL-Library: the names of multiset theorems have been

1424 normalised to distinguish which ordering the theorems are about

1426 mset_less_eqI ~> mset_subset_eqI

1427 mset_less_insertD ~> mset_subset_insertD

1428 mset_less_eq_count ~> mset_subset_eq_count

1429 mset_less_diff_self ~> mset_subset_diff_self

1430 mset_le_exists_conv ~> mset_subset_eq_exists_conv

1431 mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel

1432 mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel

1433 mset_le_mono_add ~> mset_subset_eq_mono_add

1434 mset_le_add_left ~> mset_subset_eq_add_left

1435 mset_le_add_right ~> mset_subset_eq_add_right

1436 mset_le_single ~> mset_subset_eq_single

1437 mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute

1438 diff_le_self ~> diff_subset_eq_self

1439 mset_leD ~> mset_subset_eqD

1440 mset_lessD ~> mset_subsetD

1441 mset_le_insertD ~> mset_subset_eq_insertD

1442 mset_less_of_empty ~> mset_subset_of_empty

1443 mset_less_size ~> mset_subset_size

1444 wf_less_mset_rel ~> wf_subset_mset_rel

1445 count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq

1446 mset_remdups_le ~> mset_remdups_subset_eq

1447 ms_lesseq_impl ~> subset_eq_mset_impl

1449 Some functions have been renamed:

1450 ms_lesseq_impl -> subset_eq_mset_impl

1452 * HOL-Library: multisets are now ordered with the multiset ordering

1453 #\<subseteq># ~> \<le>

1454 #\<subset># ~> <

1455 le_multiset ~> less_eq_multiset

1456 less_multiset ~> le_multiset

1457 INCOMPATIBILITY.

1459 * Session HOL-Library: the prefix multiset_order has been discontinued:

1460 the theorems can be directly accessed. As a consequence, the lemmas

1461 "order_multiset" and "linorder_multiset" have been discontinued, and the

1462 interpretations "multiset_linorder" and "multiset_wellorder" have been

1463 replaced by instantiations. INCOMPATIBILITY.

1465 * Session HOL-Library: some theorems about the multiset ordering have

1466 been renamed:

1468 le_multiset_def ~> less_eq_multiset_def

1469 less_multiset_def ~> le_multiset_def

1470 less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset

1471 mult_less_not_refl ~> mset_le_not_refl

1472 mult_less_trans ~> mset_le_trans

1473 mult_less_not_sym ~> mset_le_not_sym

1474 mult_less_asym ~> mset_le_asym

1475 mult_less_irrefl ~> mset_le_irrefl

1476 union_less_mono2{,1,2} ~> union_le_mono2{,1,2}

1478 le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O

1479 le_multiset_total ~> less_eq_multiset_total

1480 less_multiset_right_total ~> subset_eq_imp_le_multiset

1481 le_multiset_empty_left ~> less_eq_multiset_empty_left

1482 le_multiset_empty_right ~> less_eq_multiset_empty_right

1483 less_multiset_empty_right ~> le_multiset_empty_left

1484 less_multiset_empty_left ~> le_multiset_empty_right

1485 union_less_diff_plus ~> union_le_diff_plus

1486 ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset

1487 less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty

1488 le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty

1489 INCOMPATIBILITY.

1491 * Session HOL-Library: the lemma mset_map has now the attribute [simp].

1492 INCOMPATIBILITY.

1494 * Session HOL-Library: some theorems about multisets have been removed.

1495 INCOMPATIBILITY, use the following replacements:

1497 le_multiset_plus_plus_left_iff ~> add_less_cancel_right

1498 less_multiset_plus_plus_left_iff ~> add_less_cancel_right

1499 le_multiset_plus_plus_right_iff ~> add_less_cancel_left

1500 less_multiset_plus_plus_right_iff ~> add_less_cancel_left

1501 add_eq_self_empty_iff ~> add_cancel_left_right

1502 mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right

1503 mset_less_add_bothsides ~> subset_mset.add_less_cancel_right

1504 mset_le_add_bothsides ~> subset_mset.add_less_cancel_right

1505 empty_inter ~> subset_mset.inf_bot_left

1506 inter_empty ~> subset_mset.inf_bot_right

1507 empty_sup ~> subset_mset.sup_bot_left

1508 sup_empty ~> subset_mset.sup_bot_right

1509 bdd_below_multiset ~> subset_mset.bdd_above_bot

1510 subset_eq_empty ~> subset_mset.le_zero_eq

1511 le_empty ~> subset_mset.le_zero_eq

1512 mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero

1513 mset_less_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero

1515 * Session HOL-Library: some typeclass constraints about multisets have

1516 been reduced from ordered or linordered to preorder. Multisets have the

1517 additional typeclasses order_bot, no_top,

1518 ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add,

1519 linordered_cancel_ab_semigroup_add, and

1520 ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY.

1522 * Session HOL-Library: there are some new simplification rules about

1523 multisets, the multiset ordering, and the subset ordering on multisets.

1524 INCOMPATIBILITY.

1526 * Session HOL-Library: the subset ordering on multisets has now the

1527 interpretations ordered_ab_semigroup_monoid_add_imp_le and

1528 bounded_lattice_bot. INCOMPATIBILITY.

1530 * Session HOL-Library, theory Multiset: single has been removed in favor

1531 of add_mset that roughly corresponds to Set.insert. Some theorems have

1532 removed or changed:

1534 single_not_empty ~> add_mset_not_empty or empty_not_add_mset

1535 fold_mset_insert ~> fold_mset_add_mset

1536 image_mset_insert ~> image_mset_add_mset

1537 union_single_eq_diff

1538 multi_self_add_other_not_self

1539 diff_single_eq_union

1540 INCOMPATIBILITY.

1542 * Session HOL-Library, theory Multiset: some theorems have been changed

1543 to use add_mset instead of single:

1545 mset_add

1546 multi_self_add_other_not_self

1547 diff_single_eq_union

1548 union_single_eq_diff

1549 union_single_eq_member

1550 add_eq_conv_diff

1551 insert_noteq_member

1552 add_eq_conv_ex

1553 multi_member_split

1554 multiset_add_sub_el_shuffle

1555 mset_subset_eq_insertD

1556 mset_subset_insertD

1557 insert_subset_eq_iff

1558 insert_union_subset_iff

1559 multi_psub_of_add_self

1560 inter_add_left1

1561 inter_add_left2

1562 inter_add_right1

1563 inter_add_right2

1564 sup_union_left1

1565 sup_union_left2

1566 sup_union_right1

1567 sup_union_right2

1568 size_eq_Suc_imp_eq_union

1569 multi_nonempty_split

1570 mset_insort

1571 mset_update

1572 mult1I

1573 less_add

1574 mset_zip_take_Cons_drop_twice

1575 rel_mset_Zero

1576 msed_map_invL

1577 msed_map_invR

1578 msed_rel_invL

1579 msed_rel_invR

1580 le_multiset_right_total

1581 multiset_induct

1582 multiset_induct2_size

1583 multiset_induct2

1584 INCOMPATIBILITY.

1586 * Session HOL-Library, theory Multiset: the definitions of some

1587 constants have changed to use add_mset instead of adding a single

1588 element:

1590 image_mset

1591 mset

1592 replicate_mset

1593 mult1

1594 pred_mset

1595 rel_mset'

1596 mset_insort

1598 INCOMPATIBILITY.

1600 * Session HOL-Library, theory Multiset: due to the above changes, the

1601 attributes of some multiset theorems have been changed:

1603 insert_DiffM [] ~> [simp]

1604 insert_DiffM2 [simp] ~> []

1605 diff_add_mset_swap [simp]

1606 fold_mset_add_mset [simp]

1607 diff_diff_add [simp] (for multisets only)

1608 diff_cancel [simp] ~> []

1609 count_single [simp] ~> []

1610 set_mset_single [simp] ~> []

1611 size_multiset_single [simp] ~> []

1612 size_single [simp] ~> []

1613 image_mset_single [simp] ~> []

1614 mset_subset_eq_mono_add_right_cancel [simp] ~> []

1615 mset_subset_eq_mono_add_left_cancel [simp] ~> []

1616 fold_mset_single [simp] ~> []

1617 subset_eq_empty [simp] ~> []

1618 empty_sup [simp] ~> []

1619 sup_empty [simp] ~> []

1620 inter_empty [simp] ~> []

1621 empty_inter [simp] ~> []

1622 INCOMPATIBILITY.

1624 * Session HOL-Library, theory Multiset: the order of the variables in

1625 the second cases of multiset_induct, multiset_induct2_size,

1626 multiset_induct2 has been changed (e.g. Add A a ~> Add a A).

1627 INCOMPATIBILITY.

1629 * Session HOL-Library, theory Multiset: there is now a simplification

1630 procedure on multisets. It mimics the behavior of the procedure on

1631 natural numbers. INCOMPATIBILITY.

1633 * Session HOL-Library, theory Multiset: renamed sums and products of

1634 multisets:

1636 msetsum ~> sum_mset

1637 msetprod ~> prod_mset

1639 * Session HOL-Library, theory Multiset: the notation for intersection

1640 and union of multisets have been changed:

1642 #\<inter> ~> \<inter>#

1643 #\<union> ~> \<union>#

1645 INCOMPATIBILITY.

1647 * Session HOL-Library, theory Multiset: the lemma

1648 one_step_implies_mult_aux on multisets has been removed, use

1649 one_step_implies_mult instead. INCOMPATIBILITY.

1651 * Session HOL-Library: theory Complete_Partial_Order2 provides reasoning

1652 support for monotonicity and continuity in chain-complete partial orders

1653 and about admissibility conditions for fixpoint inductions.

1655 * Session HOL-Library: theory Library/Polynomial contains also

1656 derivation of polynomials (formerly in Library/Poly_Deriv) but not

1657 gcd/lcm on polynomials over fields. This has been moved to a separate

1658 theory Library/Polynomial_GCD_euclidean.thy, to pave way for a possible

1659 future different type class instantiation for polynomials over factorial

1660 rings. INCOMPATIBILITY.

1662 * Session HOL-Library: theory Sublist provides function "prefixes" with

1663 the following renaming

1665 prefixeq -> prefix

1666 prefix -> strict_prefix

1667 suffixeq -> suffix

1668 suffix -> strict_suffix

1670 Added theory of longest common prefixes.

1672 * Session HOL-Number_Theory: algebraic foundation for primes:

1673 Generalisation of predicate "prime" and introduction of predicates

1674 "prime_elem", "irreducible", a "prime_factorization" function, and the

1675 "factorial_ring" typeclass with instance proofs for nat, int, poly. Some

1676 theorems now have different names, most notably "prime_def" is now

1677 "prime_nat_iff". INCOMPATIBILITY.

1679 * Session Old_Number_Theory has been removed, after porting remaining

1680 theories.

1682 * Session HOL-Types_To_Sets provides an experimental extension of

1683 Higher-Order Logic to allow translation of types to sets.

1686 *** ML ***

1688 * Integer.gcd and Integer.lcm use efficient operations from the Poly/ML

1689 library (notably for big integers). Subtle change of semantics:

1690 Integer.gcd and Integer.lcm both normalize the sign, results are never

1691 negative. This coincides with the definitions in HOL/GCD.thy.

1692 INCOMPATIBILITY.

1694 * Structure Rat for rational numbers is now an integral part of

1695 Isabelle/ML, with special notation @int/nat or @int for numerals (an

1696 abbreviation for antiquotation @{Pure.rat argument}) and ML pretty

1697 printing. Standard operations on type Rat.rat are provided via ad-hoc

1698 overloading of + - * / < <= > >= ~ abs. INCOMPATIBILITY, need to

1699 use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been

1700 superseded by General.Div.

1702 * ML antiquotation @{path} is superseded by @{file}, which ensures that

1703 the argument is a plain file. Minor INCOMPATIBILITY.

1705 * Antiquotation @{make_string} is available during Pure bootstrap --

1706 with approximative output quality.

1708 * Low-level ML system structures (like PolyML and RunCall) are no longer

1709 exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY.

1711 * The ML function "ML" provides easy access to run-time compilation.

1712 This is particularly useful for conditional compilation, without

1713 requiring separate files.

1715 * Option ML_exception_debugger controls detailed exception trace via the

1716 Poly/ML debugger. Relevant ML modules need to be compiled beforehand

1717 with ML_file_debug, or with ML_file and option ML_debugger enabled. Note

1718 debugger information requires consirable time and space: main

1719 Isabelle/HOL with full debugger support may need ML_system_64.

1721 * Local_Theory.restore has been renamed to Local_Theory.reset to

1722 emphasize its disruptive impact on the cumulative context, notably the

1723 scope of 'private' or 'qualified' names. Note that Local_Theory.reset is

1724 only appropriate when targets are managed, e.g. starting from a global

1725 theory and returning to it. Regular definitional packages should use

1726 balanced blocks of Local_Theory.open_target versus

1727 Local_Theory.close_target instead. Rare INCOMPATIBILITY.

1729 * Structure TimeLimit (originally from the SML/NJ library) has been

1730 replaced by structure Timeout, with slightly different signature.

1731 INCOMPATIBILITY.

1733 * Discontinued cd and pwd operations, which are not well-defined in a

1734 multi-threaded environment. Note that files are usually located

1735 relatively to the master directory of a theory (see also

1736 File.full_path). Potential INCOMPATIBILITY.

1738 * Binding.empty_atts supersedes Thm.empty_binding and

1739 Attrib.empty_binding. Minor INCOMPATIBILITY.

1742 *** System ***

1744 * SML/NJ and old versions of Poly/ML are no longer supported.

1746 * Poly/ML heaps now follow the hierarchy of sessions, and thus require

1747 much less disk space.

1749 * The Isabelle ML process is now managed directly by Isabelle/Scala, and

1750 shell scripts merely provide optional command-line access. In

1751 particular:

1753 . Scala module ML_Process to connect to the raw ML process,

1754 with interaction via stdin/stdout/stderr or in batch mode;

1755 . command-line tool "isabelle console" as interactive wrapper;

1756 . command-line tool "isabelle process" as batch mode wrapper.

1758 * The executable "isabelle_process" has been discontinued. Tools and

1759 prover front-ends should use ML_Process or Isabelle_Process in

1760 Isabelle/Scala. INCOMPATIBILITY.

1762 * New command-line tool "isabelle process" supports ML evaluation of

1763 literal expressions (option -e) or files (option -f) in the context of a

1764 given heap image. Errors lead to premature exit of the ML process with

1765 return code 1.

1767 * The command-line tool "isabelle build" supports option -N for cyclic

1768 shuffling of NUMA CPU nodes. This may help performance tuning on Linux

1769 servers with separate CPU/memory modules.

1771 * System option "threads" (for the size of the Isabelle/ML thread farm)

1772 is also passed to the underlying ML runtime system as --gcthreads,

1773 unless there is already a default provided via ML_OPTIONS settings.

1775 * System option "checkpoint" helps to fine-tune the global heap space

1776 management of isabelle build. This is relevant for big sessions that may

1777 exhaust the small 32-bit address space of the ML process (which is used

1778 by default).

1780 * System option "profiling" specifies the mode for global ML profiling

1781 in "isabelle build". Possible values are "time", "allocations". The

1782 command-line tool "isabelle profiling_report" helps to digest the

1783 resulting log files.

1785 * System option "ML_process_policy" specifies an optional command prefix

1786 for the underlying ML process, e.g. to control CPU affinity on

1787 multiprocessor systems. The "isabelle jedit" tool allows to override the

1788 implicit default via option -p.

1790 * Command-line tool "isabelle console" provides option -r to help to

1791 bootstrapping Isabelle/Pure interactively.

1793 * Command-line tool "isabelle yxml" has been discontinued.

1794 INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in

1795 Isabelle/ML or Isabelle/Scala.

1797 * Many Isabelle tools that require a Java runtime system refer to the

1798 settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64,

1799 depending on the underlying platform. The settings for "isabelle build"

1800 ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been

1801 discontinued. Potential INCOMPATIBILITY.

1803 * The Isabelle system environment always ensures that the main

1804 executables are found within the shell search $PATH: "isabelle" and

1805 "isabelle_scala_script".

1807 * Isabelle tools may consist of .scala files: the Scala compiler is

1808 invoked on the spot. The source needs to define some object that extends

1809 Isabelle_Tool.Body.

1811 * File.bash_string, File.bash_path etc. represent Isabelle/ML and

1812 Isabelle/Scala strings authentically within GNU bash. This is useful to

1813 produce robust shell scripts under program control, without worrying

1814 about spaces or special characters. Note that user output works via

1815 Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and

1816 less versatile) operations File.shell_quote, File.shell_path etc. have

1817 been discontinued.

1819 * The isabelle_java executable allows to run a Java process within the

1820 name space of Java and Scala components that are bundled with Isabelle,

1821 but without the Isabelle settings environment.

1823 * Isabelle/Scala: the SSH module supports ssh and sftp connections, for

1824 remote command-execution and file-system access. This resembles

1825 operations from module File and Isabelle_System to some extent. Note

1826 that Path specifications need to be resolved remotely via

1827 ssh.remote_path instead of File.standard_path: the implicit process

1828 environment is different, Isabelle settings are not available remotely.

1830 * Isabelle/Scala: the Mercurial module supports repositories via the

1831 regular hg command-line interface. The repositroy clone and working

1832 directory may reside on a local or remote file-system (via ssh

1833 connection).

1837 New in Isabelle2016 (February 2016)

1838 -----------------------------------

1840 *** General ***

1842 * Eisbach is now based on Pure instead of HOL. Objects-logics may import

1843 either the theory ~~/src/HOL/Eisbach/Eisbach (for HOL etc.) or

1844 ~~/src/HOL/Eisbach/Eisbach_Old_Appl_Syntax (for FOL, ZF etc.). Note that

1845 the HOL-Eisbach session located in ~~/src/HOL/Eisbach/ contains further

1846 examples that do require HOL.

1848 * Better resource usage on all platforms (Linux, Windows, Mac OS X) for

1849 both Isabelle/ML and Isabelle/Scala. Slightly reduced heap space usage.

1851 * Former "xsymbols" syntax with Isabelle symbols is used by default,

1852 without any special print mode. Important ASCII replacement syntax

1853 remains available under print mode "ASCII", but less important syntax

1854 has been removed (see below).

1856 * Support for more arrow symbols, with rendering in LaTeX and Isabelle

1857 fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>.

1859 * Special notation \<struct> for the first implicit 'structure' in the

1860 context has been discontinued. Rare INCOMPATIBILITY, use explicit

1861 structure name instead, notably in indexed notation with block-subscript

1862 (e.g. \<odot>\<^bsub>A\<^esub>).

1864 * The glyph for \<diamond> in the IsabelleText font now corresponds better to its

1865 counterpart \<box> as quantifier-like symbol. A small diamond is available as

1866 \<diamondop>; the old symbol \<struct> loses this rendering and any special

1867 meaning.

1869 * Syntax for formal comments "-- text" now also supports the symbolic

1870 form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps

1871 to update old sources.

1873 * Toplevel theorem statements have been simplified as follows:

1875 theorems ~> lemmas

1876 schematic_lemma ~> schematic_goal

1877 schematic_theorem ~> schematic_goal

1878 schematic_corollary ~> schematic_goal

1880 Command-line tool "isabelle update_theorems" updates theory sources

1881 accordingly.

1883 * Toplevel theorem statement 'proposition' is another alias for

1884 'theorem'.

1886 * The old 'defs' command has been removed (legacy since Isabelle2014).

1887 INCOMPATIBILITY, use regular 'definition' instead. Overloaded and/or

1888 deferred definitions require a surrounding 'overloading' block.

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

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

1894 Isabelle/ML and official Standard ML. Option "ML_debugger" and commands

1895 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',

1896 'SML_file_no_debug' control compilation of sources with or without

1897 debugging information. The Debugger panel allows to set breakpoints (via

1898 context menu), step through stopped threads, evaluate local ML

1899 expressions etc. At least one Debugger view needs to be active to have

1900 any effect on the running ML program.

1902 * The State panel manages explicit proof state output, with dynamic

1903 auto-update according to cursor movement. Alternatively, the jEdit

1904 action "isabelle.update-state" (shortcut S+ENTER) triggers manual

1905 update.

1907 * The Output panel no longer shows proof state output by default, to

1908 avoid GUI overcrowding. INCOMPATIBILITY, use the State panel instead or

1909 enable option "editor_output_state".

1911 * The text overview column (status of errors, warnings etc.) is updated

1912 asynchronously, leading to much better editor reactivity. Moreover, the

1913 full document node content is taken into account. The width of the

1914 column is scaled according to the main text area font, for improved

1915 visibility.

1917 * The main text area no longer changes its color hue in outdated

1918 situations. The text overview column takes over the role to indicate

1919 unfinished edits in the PIDE pipeline. This avoids flashing text display

1920 due to ad-hoc updates by auxiliary GUI components, such as the State

1921 panel.

1923 * Slightly improved scheduling for urgent print tasks (e.g. command

1924 state output, interactive queries) wrt. long-running background tasks.

1926 * Completion of symbols via prefix of \<name> or \<^name> or \name is

1927 always possible, independently of the language context. It is never

1928 implicit: a popup will show up unconditionally.

1930 * Additional abbreviations for syntactic completion may be specified in

1931 $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with

1932 support for simple templates using ASCII 007 (bell) as placeholder.

1934 * Symbols \<oplus>, \<Oplus>, \<otimes>, \<Otimes>, \<odot>, \<Odot>, \<ominus>, \<oslash> no longer provide abbreviations for

1935 completion like "+o", "*o", ".o" etc. -- due to conflicts with other

1936 ASCII syntax. INCOMPATIBILITY, use plain backslash-completion or define

1937 suitable abbreviations in $ISABELLE_HOME_USER/etc/abbrevs.

1939 * Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls

1940 emphasized text style; the effect is visible in document output, not in

1941 the editor.

1943 * Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE,

1944 instead of former C+e LEFT.

1946 * The command-line tool "isabelle jedit" and the isabelle.Main

1947 application wrapper treat the default $USER_HOME/Scratch.thy more

1948 uniformly, and allow the dummy file argument ":" to open an empty buffer

1949 instead.

1951 * New command-line tool "isabelle jedit_client" allows to connect to an

1952 already running Isabelle/jEdit process. This achieves the effect of

1953 single-instance applications seen on common GUI desktops.

1955 * The default look-and-feel for Linux is the traditional "Metal", which

1956 works better with GUI scaling for very high-resolution displays (e.g.

1957 4K). Moreover, it is generally more robust than "Nimbus".

1959 * Update to jedit-5.3.0, with improved GUI scaling and support of

1960 high-resolution displays (e.g. 4K).

1962 * The main Isabelle executable is managed as single-instance Desktop

1963 application uniformly on all platforms: Linux, Windows, Mac OS X.

1966 *** Document preparation ***

1968 * Commands 'paragraph' and 'subparagraph' provide additional section

1969 headings. Thus there are 6 levels of standard headings, as in HTML.

1971 * Command 'text_raw' has been clarified: input text is processed as in

1972 'text' (with antiquotations and control symbols). The key difference is

1973 the lack of the surrounding isabelle markup environment in output.

1975 * Text is structured in paragraphs and nested lists, using notation that

1976 is similar to Markdown. The control symbols for list items are as

1977 follows:

1979 \<^item> itemize

1980 \<^enum> enumerate

1981 \<^descr> description

1983 * There is a new short form for antiquotations with a single argument

1984 that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and

1985 \<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}.

1986 \<^name> without following cartouche is equivalent to @{name}. The

1987 standard Isabelle fonts provide glyphs to render important control

1988 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".

1990 * Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with

1991 corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using

1992 standard LaTeX macros of the same names.

1994 * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.

1995 Consequently, \<open>...\<close> without any decoration prints literal quasi-formal

1996 text. Command-line tool "isabelle update_cartouches -t" helps to update

1997 old sources, by approximative patching of the content of string and

1998 cartouche tokens seen in theory sources.

2000 * The @{text} antiquotation now ignores the antiquotation option

2001 "source". The given text content is output unconditionally, without any

2002 surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the

2003 argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial

2004 or terminal spaces are ignored.

2006 * Antiquotations @{emph} and @{bold} output LaTeX source recursively,

2007 adding appropriate text style markup. These may be used in the short

2008 form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>.

2010 * Document antiquotation @{footnote} outputs LaTeX source recursively,

2011 marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>.

2013 * Antiquotation @{verbatim [display]} supports option "indent".

2015 * Antiquotation @{theory_text} prints uninterpreted theory source text

2016 (Isar outer syntax with command keywords etc.). This may be used in the

2017 short form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent".

2019 * Antiquotation @{doc ENTRY} provides a reference to the given

2020 documentation, with a hyperlink in the Prover IDE.

2022 * Antiquotations @{command}, @{method}, @{attribute} print checked

2023 entities of the Isar language.

2025 * HTML presentation uses the standard IsabelleText font and Unicode

2026 rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former

2027 print mode "HTML" loses its special meaning.

2030 *** Isar ***

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

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

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

2035 example:

2037 have result: "C x y"

2038 if "A x" and "B y"

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

2040 <proof>

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

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

2044 corresponds to a raw proof block like this:

2046 {

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

2048 assume that: "A x" "B y"

2049 have "C x y" <proof>

2050 }

2051 note result = this

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

2054 instead of 'assume' above.

2056 * Assumptions ('assume', 'presume') allow structured rule statements

2057 using 'if' and 'for', similar to 'have' etc. above. For example:

2059 assume result: "C x y"

2060 if "A x" and "B y"

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

2063 This assumes "\<And>x y::'a. A x \<Longrightarrow> B y \<Longrightarrow> C x y" and produces a general

2064 result as usual: "A ?x \<Longrightarrow> B ?y \<Longrightarrow> C ?x ?y".

2066 Vacuous quantification in assumptions is omitted, i.e. a for-context

2067 only effects propositions according to actual use of variables. For

2068 example:

2070 assume "A x" and "B y" for x and y

2072 is equivalent to:

2074 assume "\<And>x. A x" and "\<And>y. B y"

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

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

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

2079 follows:

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

2083 or:

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

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

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

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

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

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

2094 of the local context elements yet.

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

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

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

2100 then have something

2101 proof cases

2102 case a

2103 then show ?thesis <proof>

2104 next

2105 case b

2106 then show ?thesis <proof>

2107 next

2108 case c

2109 then show ?thesis <proof>

2110 qed

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

2114 case a: (c xs)

2115 case a [attributes]: (c xs)

2117 Facts that are introduced by invoking the case context are uniformly

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

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

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

2121 and always put attributes in front.

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

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

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

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

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

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

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

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

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

2134 supply [simp] = a

2135 proof

2136 show A by simp

2137 next

2138 show A by simp

2139 qed

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

2142 proof body as well, abstracted over relevant parameters.

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

2145 parameter scope for of each clause.

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

2148 statements: result is abstracted over unknowns.

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

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

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

2153 manual.

2155 * Command 'supply' supports fact definitions during goal refinement

2156 ('apply' scripts).

2158 * Proof method "goal_cases" turns the current subgoals into cases within

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

2160 example:

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

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

2164 proof goal_cases

2165 case (1 x)

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

2167 next

2168 case (2 y z)

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

2170 qed

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

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

2174 proof goal_cases

2175 case prems: 1

2176 then show ?case using prems sorry

2177 next

2178 case prems: 2

2179 then show ?case using prems sorry

2180 qed

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

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

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

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

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

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

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

2191 occasionally useful for demonstration and testing purposes.

2194 *** Pure ***

2196 * Qualifiers in locale expressions default to mandatory ('!') regardless

2197 of the command. Previously, for 'locale' and 'sublocale' the default was

2198 optional ('?'). The old synatx '!' has been discontinued.

2199 INCOMPATIBILITY, remove '!' and add '?' as required.

2201 * Keyword 'rewrites' identifies rewrite morphisms in interpretation

2202 commands. Previously, the keyword was 'where'. INCOMPATIBILITY.

2204 * More gentle suppression of syntax along locale morphisms while

2205 printing terms. Previously 'abbreviation' and 'notation' declarations

2206 would be suppressed for morphisms except term identity. Now

2207 'abbreviation' is also kept for morphims that only change the involved

2208 parameters, and only 'notation' is suppressed. This can be of great help

2209 when working with complex locale hierarchies, because proof states are

2210 displayed much more succinctly. It also means that only notation needs

2211 to be redeclared if desired, as illustrated by this example:

2213 locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\<cdot>" 65)

2214 begin

2215 definition derived (infixl "\<odot>" 65) where ...

2216 end

2218 locale morphism =

2219 left: struct composition + right: struct composition'

2220 for composition (infix "\<cdot>" 65) and composition' (infix "\<cdot>''" 65)

2221 begin

2222 notation right.derived ("\<odot>''")

2223 end

2225 * Command 'global_interpretation' issues interpretations into global

2226 theories, with optional rewrite definitions following keyword 'defines'.

2228 * Command 'sublocale' accepts optional rewrite definitions after keyword

2229 'defines'.

2231 * Command 'permanent_interpretation' has been discontinued. Use

2232 'global_interpretation' or 'sublocale' instead. INCOMPATIBILITY.

2234 * Command 'print_definitions' prints dependencies of definitional

2235 specifications. This functionality used to be part of 'print_theory'.

2237 * Configuration option rule_insts_schematic has been discontinued

2238 (intermediate legacy feature in Isabelle2015). INCOMPATIBILITY.

2240 * Abbreviations in type classes now carry proper sort constraint. Rare

2241 INCOMPATIBILITY in situations where the previous misbehaviour has been

2242 exploited.

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

2245 operations behave more similar to abbreviations. Potential

2246 INCOMPATIBILITY in exotic situations.

2249 *** HOL ***

2251 * The 'typedef' command has been upgraded from a partially checked

2252 "axiomatization", to a full definitional specification that takes the

2253 global collection of overloaded constant / type definitions into

2254 account. Type definitions with open dependencies on overloaded

2255 definitions need to be specified as "typedef (overloaded)". This

2256 provides extra robustness in theory construction. Rare INCOMPATIBILITY.

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

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

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

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

2262 Option.is_none_def. Occasional INCOMPATIBILITY in applications.

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

2265 INCOMPATIBILITY, standard syntax with symbols should be used instead.

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

2267 simplify porting old theories:

2269 notation iff (infixr "<->" 25)

2271 notation Times (infixr "<*>" 80)

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

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

2276 type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21)

2278 notation FuncSet.funcset (infixr "->" 60)

2279 notation FuncSet.extensional_funcset (infixr "->\<^sub>E" 60)

2281 notation Omega_Words_Fun.conc (infixr "conc" 65)

2283 notation Preorder.equiv ("op ~~")

2284 and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50)

2286 notation (in topological_space) tendsto (infixr "--->" 55)

2287 notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)

2288 notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)

2290 notation NSA.approx (infixl "@=" 50)

2291 notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60)

2292 notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)

2294 * The alternative notation "\<Colon>" for type and sort constraints has been

2295 removed: in LaTeX document output it looks the same as "::".

2296 INCOMPATIBILITY, use plain "::" instead.

2298 * Commands 'inductive' and 'inductive_set' work better when names for

2299 intro rules are omitted: the "cases" and "induct" rules no longer

2300 declare empty case_names, but no case_names at all. This allows to use

2301 numbered cases in proofs, without requiring method "goal_cases".

2303 * Inductive definitions ('inductive', 'coinductive', etc.) expose

2304 low-level facts of the internal construction only if the option

2305 "inductive_internals" is enabled. This refers to the internal predicate

2306 definition and its monotonicity result. Rare INCOMPATIBILITY.

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

2309 expose low-level facts of the internal construction only if the option

2310 "function_internals" is enabled. Its internal inductive definition is

2311 also subject to "inductive_internals". Rare INCOMPATIBILITY.

2313 * BNF datatypes ('datatype', 'codatatype', etc.) expose low-level facts

2314 of the internal construction only if the option "bnf_internals" is

2315 enabled. This supersedes the former option "bnf_note_all". Rare

2316 INCOMPATIBILITY.

2318 * Combinator to represent case distinction on products is named

2319 "case_prod", uniformly, discontinuing any input aliasses. Very popular

2320 theorem aliasses have been retained.

2322 Consolidated facts:

2323 PairE ~> prod.exhaust

2324 Pair_eq ~> prod.inject

2325 pair_collapse ~> prod.collapse

2326 Pair_fst_snd_eq ~> prod_eq_iff

2327 split_twice ~> prod.case_distrib

2328 split_weak_cong ~> prod.case_cong_weak

2329 split_split ~> prod.split

2330 split_split_asm ~> prod.split_asm

2331 splitI ~> case_prodI

2332 splitD ~> case_prodD

2333 splitI2 ~> case_prodI2

2334 splitI2' ~> case_prodI2'

2335 splitE ~> case_prodE

2336 splitE' ~> case_prodE'

2337 split_pair ~> case_prod_Pair

2338 split_eta ~> case_prod_eta

2339 split_comp ~> case_prod_comp

2340 mem_splitI ~> mem_case_prodI

2341 mem_splitI2 ~> mem_case_prodI2

2342 mem_splitE ~> mem_case_prodE

2343 The_split ~> The_case_prod

2344 cond_split_eta ~> cond_case_prod_eta

2345 Collect_split_in_rel_leE ~> Collect_case_prod_in_rel_leE

2346 Collect_split_in_rel_leI ~> Collect_case_prod_in_rel_leI

2347 in_rel_Collect_split_eq ~> in_rel_Collect_case_prod_eq

2348 Collect_split_Grp_eqD ~> Collect_case_prod_Grp_eqD

2349 Collect_split_Grp_inD ~> Collect_case_prod_Grp_in

2350 Domain_Collect_split ~> Domain_Collect_case_prod

2351 Image_Collect_split ~> Image_Collect_case_prod

2352 Range_Collect_split ~> Range_Collect_case_prod

2353 Eps_split ~> Eps_case_prod

2354 Eps_split_eq ~> Eps_case_prod_eq

2355 split_rsp ~> case_prod_rsp

2356 curry_split ~> curry_case_prod

2357 split_curry ~> case_prod_curry

2359 Changes in structure HOLogic:

2360 split_const ~> case_prod_const

2361 mk_split ~> mk_case_prod

2362 mk_psplits ~> mk_ptupleabs

2363 strip_psplits ~> strip_ptupleabs

2365 INCOMPATIBILITY.

2367 * The coercions to type 'real' have been reorganised. The function

2368 'real' is no longer overloaded, but has type 'nat => real' and

2369 abbreviates of_nat for that type. Also 'real_of_int :: int => real'

2370 abbreviates of_int for that type. Other overloaded instances of 'real'

2371 have been replaced by 'real_of_ereal' and 'real_of_float'.

2373 Consolidated facts (among others):

2374 real_of_nat_le_iff -> of_nat_le_iff

2375 real_of_nat_numeral of_nat_numeral

2376 real_of_int_zero of_int_0

2377 real_of_nat_zero of_nat_0

2378 real_of_one of_int_1

2379 real_of_int_add of_int_add

2380 real_of_nat_add of_nat_add

2381 real_of_int_diff of_int_diff

2382 real_of_nat_diff of_nat_diff

2383 floor_subtract floor_diff_of_int

2384 real_of_int_inject of_int_eq_iff

2385 real_of_int_gt_zero_cancel_iff of_int_0_less_iff

2386 real_of_int_ge_zero_cancel_iff of_int_0_le_iff

2387 real_of_nat_ge_zero of_nat_0_le_iff

2388 real_of_int_ceiling_ge le_of_int_ceiling

2389 ceiling_less_eq ceiling_less_iff

2390 ceiling_le_eq ceiling_le_iff

2391 less_floor_eq less_floor_iff

2392 floor_less_eq floor_less_iff

2393 floor_divide_eq_div floor_divide_of_int_eq

2394 real_of_int_zero_cancel of_nat_eq_0_iff

2395 ceiling_real_of_int ceiling_of_int

2397 INCOMPATIBILITY.

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

2400 been removed. INCOMPATIBILITY.

2402 * Quickcheck setup for finite sets.

2404 * Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.

2406 * Sledgehammer:

2407 - The MaSh relevance filter has been sped up.

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

2409 cases where Sledgehammer gives a proof that does not work.

2410 - Auto Sledgehammer now minimizes and preplays the results.

2411 - Handle Vampire 4.0 proof output without raising exception.

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

2413 Isabelle/jEdit instead. INCOMPATIBILITY.

2414 - Eliminated obsolete "blocking" option and related subcommands.

2416 * Nitpick:

2417 - Fixed soundness bug in translation of "finite" predicate.

2418 - Fixed soundness bug in "destroy_constrs" optimization.

2419 - Fixed soundness bug in translation of "rat" type.

2420 - Removed "check_potential" and "check_genuine" options.

2421 - Eliminated obsolete "blocking" option.

2423 * (Co)datatype package:

2424 - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF

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

2426 - Always generate "case_transfer" theorem.

2427 - For mutual types, generate slightly stronger "rel_induct",

2428 "rel_coinduct", and "coinduct" theorems. INCOMPATIBILITY.

2429 - Allow discriminators and selectors with the same name as the type

2430 being defined.

2431 - Avoid various internal name clashes (e.g., 'datatype f = f').

2433 * Transfer: new methods for interactive debugging of 'transfer' and

2434 'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',

2435 'transfer_prover_start' and 'transfer_prover_end'.

2437 * New diagnostic command print_record for displaying record definitions.

2439 * Division on integers is bootstrapped directly from division on

2440 naturals and uses generic numeral algorithm for computations. Slight

2441 INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes former

2442 simprocs binary_int_div and binary_int_mod

2444 * Tightened specification of class semiring_no_zero_divisors. Minor

2445 INCOMPATIBILITY.

2447 * Class algebraic_semidom introduces common algebraic notions of

2448 integral (semi)domains, particularly units. Although logically subsumed

2449 by fields, is is not a super class of these in order not to burden

2450 fields with notions that are trivial there.

2452 * Class normalization_semidom specifies canonical representants for

2453 equivalence classes of associated elements in an integral (semi)domain.

2454 This formalizes associated elements as well.

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

2457 semiring_Gcd, semiring_Lcd. Minor INCOMPATIBILITY: facts gcd_nat.commute

2458 and gcd_int.commute are subsumed by gcd.commute, as well as

2459 gcd_nat.assoc and gcd_int.assoc by gcd.assoc.

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

2462 logically unified to Rings.divide in syntactic type class Rings.divide,

2463 with infix syntax (_ div _). Infix syntax (_ / _) for field division is

2464 added later as abbreviation in class Fields.inverse. INCOMPATIBILITY,

2465 instantiations must refer to Rings.divide rather than the former

2466 separate constants, hence infix syntax (_ / _) is usually not available

2467 during instantiation.

2469 * New cancellation simprocs for boolean algebras to cancel complementary

2470 terms for sup and inf. For example, "sup x (sup y (- x))" simplifies to

2471 "top". INCOMPATIBILITY.

2473 * Class uniform_space introduces uniform spaces btw topological spaces

2474 and metric spaces. Minor INCOMPATIBILITY: open_<type>_def needs to be

2475 introduced in the form of an uniformity. Some constants are more general

2476 now, it may be necessary to add type class constraints.

2478 open_real_def \<leadsto> open_dist

2479 open_complex_def \<leadsto> open_dist

2481 * Library/Monad_Syntax: notation uses symbols \<bind> and \<then>. INCOMPATIBILITY.

2483 * Library/Multiset:

2484 - Renamed multiset inclusion operators:

2485 < ~> <#

2486 > ~> >#

2487 <= ~> <=#

2488 >= ~> >=#

2489 \<le> ~> \<le>#

2490 \<ge> ~> \<ge>#

2491 INCOMPATIBILITY.

2492 - Added multiset inclusion operator syntax:

2493 \<subset>#

2494 \<subseteq>#

2495 \<supset>#

2496 \<supseteq>#

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

2498 "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",

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

2500 previously provided by these type classes (directly or indirectly)

2501 are now available through the "subset_mset" interpretation

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

2503 INCOMPATIBILITY.

2504 - Renamed conversions:

2505 multiset_of ~> mset

2506 multiset_of_set ~> mset_set

2507 set_of ~> set_mset

2508 INCOMPATIBILITY

2509 - Renamed lemmas:

2510 mset_le_def ~> subseteq_mset_def

2511 mset_less_def ~> subset_mset_def

2512 less_eq_multiset.rep_eq ~> subseteq_mset_def

2513 INCOMPATIBILITY

2514 - Removed lemmas generated by lift_definition:

2515 less_eq_multiset.abs_eq, less_eq_multiset.rsp,

2516 less_eq_multiset.transfer, less_eq_multiset_def

2517 INCOMPATIBILITY

2519 * Library/Omega_Words_Fun: Infinite words modeled as functions nat \<Rightarrow> 'a.

2521 * Library/Bourbaki_Witt_Fixpoint: Added formalisation of the

2522 Bourbaki-Witt fixpoint theorem for increasing functions in

2523 chain-complete partial orders.

2525 * Library/Old_Recdef: discontinued obsolete 'defer_recdef' command.

2526 Minor INCOMPATIBILITY, use 'function' instead.

2528 * Library/Periodic_Fun: a locale that provides convenient lemmas for

2529 periodic functions.

2531 * Library/Formal_Power_Series: proper definition of division (with

2532 remainder) for formal power series; instances for Euclidean Ring and

2533 GCD.

2535 * HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.

2537 * HOL-Statespace: command 'statespace' uses mandatory qualifier for

2538 import of parent, as for general 'locale' expressions. INCOMPATIBILITY,

2539 remove '!' and add '?' as required.

2541 * HOL-Decision_Procs: The "approximation" method works with "powr"

2542 (exponentiation on real numbers) again.

2544 * HOL-Multivariate_Analysis: theory Cauchy_Integral_Thm with Contour

2545 integrals (= complex path integrals), Cauchy's integral theorem, winding

2546 numbers and Cauchy's integral formula, Liouville theorem, Fundamental

2547 Theorem of Algebra. Ported from HOL Light.

2549 * HOL-Multivariate_Analysis: topological concepts such as connected

2550 components, homotopic paths and the inside or outside of a set.

2552 * HOL-Multivariate_Analysis: radius of convergence of power series and

2553 various summability tests; Harmonic numbers and the Euler–Mascheroni

2554 constant; the Generalised Binomial Theorem; the complex and real

2555 Gamma/log-Gamma/Digamma/ Polygamma functions and their most important

2556 properties.

2558 * HOL-Probability: The central limit theorem based on Levy's uniqueness

2559 and continuity theorems, weak convergence, and characterisitc functions.

2561 * HOL-Data_Structures: new and growing session of standard data

2562 structures.

2565 *** ML ***

2567 * The following combinators for low-level profiling of the ML runtime

2568 system are available:

2570 profile_time (*CPU time*)

2571 profile_time_thread (*CPU time on this thread*)

2572 profile_allocations (*overall heap allocations*)

2574 * Antiquotation @{undefined} or \<^undefined> inlines (raise Match).

2576 * Antiquotation @{method NAME} inlines the (checked) name of the given

2577 Isar proof method.

2579 * Pretty printing of Poly/ML compiler output in Isabelle has been

2580 improved: proper treatment of break offsets and blocks with consistent

2581 breaks.

2583 * The auxiliary module Pure/display.ML has been eliminated. Its

2584 elementary thm print operations are now in Pure/more_thm.ML and thus

2585 called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY.

2587 * Simproc programming interfaces have been simplified:

2588 Simplifier.make_simproc and Simplifier.define_simproc supersede various

2589 forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that

2590 term patterns for the left-hand sides are specified with implicitly

2591 fixed variables, like top-level theorem statements. INCOMPATIBILITY.

2593 * Instantiation rules have been re-organized as follows:

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

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

2598 Drule.infer_instantiate (*instantiation with type inference*)

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

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

2602 Old cterm_instantiate is superseded by infer_instantiate.

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

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

2606 discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.

2607 instead (with proper context).

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

2610 instantiation to be certified: plain variables are given directly.

2612 * Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous

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

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

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

2616 the proof context discipline.

2618 * Isar proof methods are based on a slightly more general type

2619 context_tactic, which allows to change the proof context dynamically

2620 (e.g. to update cases) and indicate explicit Seq.Error results. Former

2621 METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are

2622 provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY.

2625 *** System ***

2627 * Command-line tool "isabelle console" enables print mode "ASCII".

2629 * Command-line tool "isabelle update_then" expands old Isar command

2630 conflations:

2632 hence ~> then have

2633 thus ~> then show

2635 This syntax is more orthogonal and improves readability and

2636 maintainability of proofs.

2638 * Global session timeout is multiplied by timeout_scale factor. This

2639 allows to adjust large-scale tests (e.g. AFP) to overall hardware

2640 performance.

2642 * Property values in etc/symbols may contain spaces, if written with the

2643 replacement character "␣" (Unicode point 0x2324). For example:

2645 \<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono

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

2648 space.

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

2651 platforms as follows.

2653 - Isabelle desktop application: platform-specific files that are

2654 associated with the main app bundle

2656 - isabelle jedit: settings

2657 JEDIT_JAVA_SYSTEM_OPTIONS

2658 JEDIT_JAVA_OPTIONS32 vs. JEDIT_JAVA_OPTIONS64

2660 - isabelle build: settings

2661 ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64

2663 * Bash shell function "jvmpath" has been renamed to "platform_path": it

2664 is relevant both for Poly/ML and JVM processes.

2666 * Poly/ML default platform architecture may be changed from 32bit to

2667 64bit via system option ML_system_64. A system restart (and rebuild) is

2668 required after change.

2670 * Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which

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

2673 * Heap images are 10-15% smaller due to less wasteful persistent theory

2674 content (using ML type theory_id instead of theory);

2678 New in Isabelle2015 (May 2015)

2679 ------------------------------

2681 *** General ***

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

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

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

2687 context

2688 begin

2690 private definition ...

2691 private lemma ...

2693 qualified definition ...

2694 qualified lemma ...

2696 lemma ...

2697 theorem ...

2699 end

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

2702 naming policy.

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

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

2706 INCOMPATIBILITY, use 'sorry' instead.

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

2709 together with an attribute to maintain the content incrementally. This

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

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

2713 * 'find_theorems': search patterns which are abstractions are

2714 schematically expanded before search. Search results match the naive

2715 expectation more closely, particularly wrt. abbreviations.

2716 INCOMPATIBILITY.

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

2719 theory context.

2721 * Outer syntax commands are managed authentically within the theory

2722 context, without implicit global state. Potential for accidental

2723 INCOMPATIBILITY, make sure that required theories are really imported.

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

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

2727 update_semicolons" to remove obsolete semicolons from old theory

2728 sources.

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

2731 corresponds to (tac1 THEN_ALL_NEW tac2) in ML.

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

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

2735 method provides basic fact/term matching in addition to

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

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

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

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

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

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

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

2747 * Extended bracket matching based on Isar language structure. System

2748 option jedit_structure_limit determines maximum number of lines to scan

2749 in the buffer.

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

2752 marker, SideKick parser.

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

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

2756 the editor (hyperlinks, completion etc.).

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

2759 Options / Text Area).

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

2762 display of 'thy_deps', 'class_deps' etc.

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

2765 restrict the visualized hierarchy.

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

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

2771 *** Document preparation ***

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

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

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

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

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

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

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

2780 update_header"). Minor INCOMPATIBILITY.

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

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

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

2785 as argument to other macros (such as footnotes).

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

2788 style.

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

2791 produced unconditionally for HTML browser_info and PDF-LaTeX document.

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

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

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

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

2797 tags. Potential INCOMPATIBILITY in exotic situations.

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

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

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

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

2803 dynamically in GUI front-ends. Implementations of document

2804 antiquotations need to observe the margin explicitly according to

2805 Thy_Output.string_of_margin. Minor INCOMPATIBILITY.

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

2808 mandatory for document preparation. The legacy mode with implicit

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

2810 INCOMPATIBILITY.

2813 *** Pure ***

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

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

2817 these variables become schematic in the instantiated theorem; this

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

2819 Configuration option rule_insts_schematic (default false) controls use

2820 of schematic variables outside the context. Minor INCOMPATIBILITY,

2821 declare rule_insts_schematic = true temporarily and update to use local

2822 variable declarations or dummy patterns instead.

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

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

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

2828 * Generated schematic variables in standard format of exported facts are

2829 incremented to avoid material in the proof context. Rare

2830 INCOMPATIBILITY, explicit instantiation sometimes needs to refer to

2831 different index.

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

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

2835 of numeral signs, particularly in expressions involving infix syntax

2836 like "(- 1) ^ n".

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

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

2840 token category instead.

2843 *** HOL ***

2845 * New (co)datatype package:

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

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

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

2849 'isabelle doc datatypes' for information on porting.

2850 INCOMPATIBILITY.

2851 - Renamed theorems:

2852 disc_corec ~> corec_disc

2853 disc_corec_iff ~> corec_disc_iff

2854 disc_exclude ~> distinct_disc

2855 disc_exhaust ~> exhaust_disc

2856 disc_map_iff ~> map_disc_iff

2857 sel_corec ~> corec_sel

2858 sel_exhaust ~> exhaust_sel

2859 sel_map ~> map_sel

2860 sel_set ~> set_sel

2861 sel_split ~> split_sel

2862 sel_split_asm ~> split_sel_asm

2863 strong_coinduct ~> coinduct_strong

2864 weak_case_cong ~> case_cong_weak

2865 INCOMPATIBILITY.

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

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

2868 INCOMPATIBILITY.

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

2870 consequences of other set rules "by auto".

2871 INCOMPATIBILITY.

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

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

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

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

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

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

2878 INCOMPATIBILITY.

2879 - Renamed theories:

2880 BNF_Comp ~> BNF_Composition

2881 BNF_FP_Base ~> BNF_Fixpoint_Base

2882 BNF_GFP ~> BNF_Greatest_Fixpoint

2883 BNF_LFP ~> BNF_Least_Fixpoint

2884 BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions

2885 Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions

2886 INCOMPATIBILITY.

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

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

2889 Lifting_Product and Lifting_Option from Main became obsolete and

2890 were removed. Changed definitions of the relators rel_prod and

2891 rel_sum (using inductive).

2892 INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead

2893 of rel_prod_def and rel_sum_def.

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

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

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

2897 constructors, case combinators, discriminators, selectors and

2898 (co)recursors are automatically proved and registered as transfer

2899 rules.

2901 * Old datatype package:

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

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

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

2905 'isabelle doc datatypes' for information on porting.

2906 INCOMPATIBILITY.

2907 - Renamed theorems:

2908 weak_case_cong ~> case_cong_weak

2909 INCOMPATIBILITY.

2910 - Renamed theory:

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

2912 INCOMPATIBILITY.

2914 * Nitpick:

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

2916 operations.

2918 * Sledgehammer:

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

2920 default.

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

2922 source. The "z3_non_commercial" option is discontinued.

2923 - Minimization is now always enabled by default.

2924 Removed sub-command:

2925 min

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

2927 dramatically improved.

2928 - Improved support for CVC4 and veriT.

2930 * Old and new SMT modules:

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

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

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

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

2935 be installed, and the environment variable "OLD_Z3_SOLVER" must

2936 point to it.

2937 INCOMPATIBILITY.

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

2939 INCOMPATIBILITY.

2940 - New option 'smt_reconstruction_step_timeout' to limit the

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

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

2943 method, especially runtime statistics of Z3 proof reconstruction.

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

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

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

2948 lifting, and avoids tedious workarounds.

2950 * Command and antiquotation "value" provide different evaluation slots

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

2952 Minor INCOMPATIBILITY.

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

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

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

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

2959 add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY.

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

2962 algebraic semiring_no_zero_divisors. INCOMPATIBILITY.

2964 * Class linordered_semidom really requires no zero divisors.

2965 INCOMPATIBILITY.

2967 * Classes division_ring, field and linordered_field always demand

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

2969 field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY.

2971 * Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit

2972 additive inverse operation. INCOMPATIBILITY.

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

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

2976 INCOMPATIBILITY: type constraints may be necessary.

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

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

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

2981 needed.

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

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

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

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

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

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

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

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

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

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

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

2996 "nat_floor"/"nat_ceiling".

2998 * Qualified some duplicated fact names required for boostrapping the

2999 type class hierarchy:

3000 ab_add_uminus_conv_diff ~> diff_conv_add_uminus

3001 field_inverse_zero ~> inverse_zero

3002 field_divide_inverse ~> divide_inverse

3003 field_inverse ~> left_inverse

3004 Minor INCOMPATIBILITY.

3006 * Eliminated fact duplicates:

3007 mult_less_imp_less_right ~> mult_right_less_imp_less

3008 mult_less_imp_less_left ~> mult_left_less_imp_less

3009 Minor INCOMPATIBILITY.

3011 * Fact consolidation: even_less_0_iff is subsumed by

3012 double_add_less_zero_iff_single_add_less_zero (simp by default anyway).

3014 * Generalized and consolidated some theorems concerning divsibility:

3015 dvd_reduce ~> dvd_add_triv_right_iff

3016 dvd_plus_eq_right ~> dvd_add_right_iff

3017 dvd_plus_eq_left ~> dvd_add_left_iff

3018 Minor INCOMPATIBILITY.

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

3021 and part of theory Main.

3022 even_def ~> even_iff_mod_2_eq_zero

3023 INCOMPATIBILITY.

3025 * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor

3026 INCOMPATIBILITY.

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

3029 Fact rename:

3030 listsum_def ~> listsum.eq_foldr

3031 INCOMPATIBILITY.

3033 * Product over lists via constant "listprod".

3035 * Theory List: renamed drop_Suc_conv_tl and nth_drop' to

3036 Cons_nth_drop_Suc.

3038 * New infrastructure for compiling, running, evaluating and testing

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

3040 HOL/Codegenerator_Test/Code_Test* for examples.

3042 * Library/Multiset:

3043 - Introduced "replicate_mset" operation.

3044 - Introduced alternative characterizations of the multiset ordering in

3045 "Library/Multiset_Order".

3046 - Renamed multiset ordering:

3047 <# ~> #<#

3048 <=# ~> #<=#

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

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

3051 INCOMPATIBILITY.

3052 - Introduced abbreviations for ill-named multiset operations:

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

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

3055 INCOMPATIBILITY.

3056 - Renamed

3057 in_multiset_of ~> in_multiset_in_set

3058 Multiset.fold ~> fold_mset

3059 Multiset.filter ~> filter_mset

3060 INCOMPATIBILITY.

3061 - Removed mcard, is equal to size.

3062 - Added attributes:

3063 image_mset.id [simp]

3064 image_mset_id [simp]

3065 elem_multiset_of_set [simp, intro]

3066 comp_fun_commute_plus_mset [simp]

3067 comp_fun_commute.fold_mset_insert [OF comp_fun_commute_plus_mset, simp]

3068 in_mset_fold_plus_iff [iff]

3069 set_of_Union_mset [simp]

3070 in_Union_mset_iff [iff]

3071 INCOMPATIBILITY.

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

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

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

3076 argument. Minor INCOMPATIBILITY.

3078 * HOL-Decision_Procs: New counterexample generator quickcheck

3079 [approximation] for inequalities of transcendental functions. Uses

3080 hardware floating point arithmetic to randomly discover potential

3081 counterexamples. Counterexamples are certified with the "approximation"

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

3083 examples.

3085 * HOL-Probability: Reworked measurability prover

3086 - applies destructor rules repeatedly

3087 - removed application splitting (replaced by destructor rule)

3088 - added congruence rules to rewrite measure spaces under the sets

3089 projection

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

3092 single-step rewriting with subterm selection based on patterns.

3095 *** ML ***

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

3098 considered inaccessible, instead of accessible via the fully-qualified

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

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

3101 contemporary applications use the strict Name_Space.check (and

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

3103 INCOMPATIBILITY in rare applications of Name_Space.intern.

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

3106 ERROR instead of internal Toplevel.UNDEF.

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

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

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

3112 INCOMPATIBILITY.

3114 * Former combinators NAMED_CRITICAL and CRITICAL for central critical

3115 sections have been discontinued, in favour of the more elementary

3116 Multithreading.synchronized and its high-level derivative

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

3118 INCOMPATIBILITY: synchronized access needs to be atomic and cannot be

3119 nested.

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

3122 change of semantics with minimal potential for INCOMPATIBILITY.

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

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

3126 available as Thm.global_ctyp_of and Thm.global_cterm_of.

3127 INCOMPATIBILITY.

3129 * Elementary operations in module Thm are no longer pervasive.

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

3131 Thm.term_of etc.

3133 * Proper context for various elementary tactics: assume_tac,

3134 resolve_tac, eresolve_tac, dresolve_tac, forward_tac, match_tac,

3135 compose_tac, Splitter.split_tac etc. INCOMPATIBILITY.

3137 * Tactical PARALLEL_ALLGOALS is the most common way to refer to

3138 PARALLEL_GOALS.

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

3141 which also allows to specify a fork priority.

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

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

3145 markup). Minor INCOMPATIBILITY.

3147 * Cartouches within ML sources are turned into values of type

3148 Input.source (with formal position information).

3151 *** System ***

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

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

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

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

3159 be externally triggered using an appropriate ROOT file plus a

3160 corresponding theory. Parametrization is possible using environment

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

3162 INCOMPATIBILITY.

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

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

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

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

3169 menu Global Options / Appearance.

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

3172 Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.

3176 New in Isabelle2014 (August 2014)

3177 ---------------------------------

3179 *** General ***

3181 * Support for official Standard ML within the Isabelle context.

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

3183 Toplevel bindings are stored within the theory context; the initial

3184 environment is restricted to the Standard ML implementation of

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

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

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

3188 some examples.

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

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

3192 variable. Locale assumptions and chained facts containing "x"

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

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

3195 restore the previous behavior. INCOMPATIBILITY, especially where

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

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

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

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

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

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

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

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

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

3206 exception. Potential INCOMPATIBILITY for non-conformant tactical

3207 proof tools.

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

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

3211 supports input via ` (backquote).

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

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

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

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

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

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

3220 Minor INCOMPATIBILITY.

3222 * Discontinued legacy_isub_isup, which was a temporary workaround for

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

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

3225 INCOMPATIBILITY.

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

3228 which results in an active hyperlink within the text.

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

3231 not check existence within the file-system.

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

3234 isar-ref, jedit, system.

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

3239 * Improved Document panel: simplified interaction where every single

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

3241 buffer.

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

3244 to PIDE hyperlinks.

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

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

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

3250 auxiliary ML files.

3252 * Improved syntactic and semantic completion mechanism, with simple

3253 templates, completion language context, name-space completion,

3254 file-name completion, spell-checker completion.

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

3257 handling and propagation to enclosing text area -- avoid loosing

3258 keystrokes with slow / remote graphics displays.

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

3261 item, depending on Isabelle options.

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

3264 selections, rectangular selections, rectangular selection as "tall

3265 caret".

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

3268 completion popup and context-menu.

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

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

3272 operations for the context. Minor incompatibility in keyboard

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

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

3276 to highlight text via regular expression.

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

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

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

3281 "isabelle jedit -m MODE".

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

3284 networking operations instead of jEdit virtual file-systems.

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

3287 imports) are automatically removed from the document model.

3289 * Improved monitor panel.

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

3292 more robust treatment of threads and interrupts.

3294 * Improved management of dockable windows: clarified keyboard focus

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

3296 "Detach" a copy where this makes sense.

3298 * New Simplifier Trace panel provides an interactive view of the

3299 simplification process, enabled by the "simp_trace_new" attribute

3300 within the context.

3303 *** Pure ***

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

3306 been discontinued to avoid the danger of non-trivial axiomatization

3307 that is not immediately visible. INCOMPATIBILITY, use regular

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

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

3310 finished trivially if the underlying class definition is made vacuous

3311 (without any assumptions). See also Isabelle/ML operations

3312 Axclass.class_axiomatization, Axclass.classrel_axiomatization,

3313 Axclass.arity_axiomatization.

3315 * Basic constants of Pure use more conventional names and are always

3316 qualified. Rare INCOMPATIBILITY, but with potentially serious

3317 consequences, notably for tools in Isabelle/ML. The following

3318 renaming needs to be applied:

3320 == ~> Pure.eq

3321 ==> ~> Pure.imp

3322 all ~> Pure.all

3323 TYPE ~> Pure.type

3324 dummy_pattern ~> Pure.dummy_pattern

3326 Systematic porting works by using the following theory setup on a

3327 *previous* Isabelle version to introduce the new name accesses for the

3328 old constants:

3330 setup {*

3331 fn thy => thy

3332 |> Sign.root_path

3333 |> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "=="

3334 |> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>"

3335 |> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all"

3336 |> Sign.restore_naming thy

3337 *}

3339 Thus ML antiquotations like @{const_name Pure.eq} may be used already.

3340 Later the application is moved to the current Isabelle version, and

3341 the auxiliary aliases are deleted.

3343 * Attributes "where" and "of" allow an optional context of local

3344 variables ('for' declaration): these variables become schematic in the

3345 instantiated theorem.

3347 * Obsolete attribute "standard" has been discontinued (legacy since

3348 Isabelle2012). Potential INCOMPATIBILITY, use explicit 'for' context

3349 where instantiations with schematic variables are intended (for

3350 declaration commands like 'lemmas' or attributes like "of"). The

3351 following temporary definition may help to port old applications:

3353 attribute_setup standard =

3354 "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"

3356 * More thorough check of proof context for goal statements and

3357 attributed fact expressions (concerning background theory, declared

3358 hyps). Potential INCOMPATIBILITY, tools need to observe standard

3359 context discipline. See also Assumption.add_assumes and the more

3360 primitive Thm.assume_hyps.

3362 * Inner syntax token language allows regular quoted strings "..."

3363 (only makes sense in practice, if outer syntax is delimited

3364 differently, e.g. via cartouches).

3366 * Command 'print_term_bindings' supersedes 'print_binds' for clarity,

3367 but the latter is retained some time as Proof General legacy.

3369 * Code generator preprocessor: explicit control of simp tracing on a

3370 per-constant basis. See attribute "code_preproc".

3373 *** HOL ***

3375 * Code generator: enforce case of identifiers only for strict target

3376 language requirements. INCOMPATIBILITY.

3378 * Code generator: explicit proof contexts in many ML interfaces.

3379 INCOMPATIBILITY.

3381 * Code generator: minimize exported identifiers by default. Minor

3382 INCOMPATIBILITY.

3384 * Code generation for SML and OCaml: dropped arcane "no_signatures"

3385 option. Minor INCOMPATIBILITY.

3387 * "declare [[code abort: ...]]" replaces "code_abort ...".

3388 INCOMPATIBILITY.

3390 * "declare [[code drop: ...]]" drops all code equations associated

3391 with the given constants.

3393 * Code generations are provided for make, fields, extend and truncate

3394 operations on records.

3396 * Command and antiquotation "value" are now hardcoded against nbe and

3397 ML. Minor INCOMPATIBILITY.

3399 * Renamed command 'enriched_type' to 'functor'. INCOMPATIBILITY.

3401 * The symbol "\<newline>" may be used within char or string literals

3402 to represent (Char Nibble0 NibbleA), i.e. ASCII newline.

3404 * Qualified String.implode and String.explode. INCOMPATIBILITY.

3406 * Simplifier: Enhanced solver of preconditions of rewrite rules can

3407 now deal with conjunctions. For help with converting proofs, the old

3408 behaviour of the simplifier can be restored like this: declare/using

3409 [[simp_legacy_precond]]. This configuration option will disappear

3410 again in the future. INCOMPATIBILITY.

3412 * Simproc "finite_Collect" is no longer enabled by default, due to

3413 spurious crashes and other surprises. Potential INCOMPATIBILITY.

3415 * Moved new (co)datatype package and its dependencies from session

3416 "HOL-BNF" to "HOL". The commands 'bnf', 'wrap_free_constructors',

3417 'datatype_new', 'codatatype', 'primcorec', 'primcorecursive' are now

3418 part of theory "Main".

3420 Theory renamings:

3421 FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)

3422 Library/Wfrec.thy ~> Wfrec.thy

3423 Library/Zorn.thy ~> Zorn.thy

3424 Cardinals/Order_Relation.thy ~> Order_Relation.thy

3425 Library/Order_Union.thy ~> Cardinals/Order_Union.thy

3426 Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy

3427 Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy

3428 Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy

3429 Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy

3430 Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy

3431 BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy

3432 BNF/Basic_BNFs.thy ~> Basic_BNFs.thy

3433 BNF/BNF_Comp.thy ~> BNF_Comp.thy

3434 BNF/BNF_Def.thy ~> BNF_Def.thy

3435 BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy

3436 BNF/BNF_GFP.thy ~> BNF_GFP.thy

3437 BNF/BNF_LFP.thy ~> BNF_LFP.thy

3438 BNF/BNF_Util.thy ~> BNF_Util.thy

3439 BNF/Coinduction.thy ~> Coinduction.thy

3440 BNF/More_BNFs.thy ~> Library/More_BNFs.thy

3441 BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy

3442 BNF/Examples/* ~> BNF_Examples/*

3444 New theories:

3445 Wellorder_Extension.thy (split from Zorn.thy)

3446 Library/Cardinal_Notations.thy

3447 Library/BNF_Axomatization.thy

3448 BNF_Examples/Misc_Primcorec.thy

3449 BNF_Examples/Stream_Processor.thy

3451 Discontinued theories:

3452 BNF/BNF.thy

3453 BNF/Equiv_Relations_More.thy

3455 INCOMPATIBILITY.

3457 * New (co)datatype package:

3458 - Command 'primcorec' is fully implemented.

3459 - Command 'datatype_new' generates size functions ("size_xxx" and

3460 "size") as required by 'fun'.

3461 - BNFs are integrated with the Lifting tool and new-style

3462 (co)datatypes with Transfer.

3463 - Renamed commands:

3464 datatype_new_compat ~> datatype_compat

3465 primrec_new ~> primrec

3466 wrap_free_constructors ~> free_constructors

3467 INCOMPATIBILITY.

3468 - The generated constants "xxx_case" and "xxx_rec" have been renamed

3469 "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").

3470 INCOMPATIBILITY.

3471 - The constant "xxx_(un)fold" and related theorems are no longer

3472 generated. Use "xxx_(co)rec" or define "xxx_(un)fold" manually

3473 using "prim(co)rec".

3474 INCOMPATIBILITY.

3475 - No discriminators are generated for nullary constructors by

3476 default, eliminating the need for the odd "=:" syntax.

3477 INCOMPATIBILITY.

3478 - No discriminators or selectors are generated by default by

3479 "datatype_new", unless custom names are specified or the new

3480 "discs_sels" option is passed.

3481 INCOMPATIBILITY.

3483 * Old datatype package:

3484 - The generated theorems "xxx.cases" and "xxx.recs" have been

3485 renamed "xxx.case" and "xxx.rec" (e.g., "sum.cases" ->

3486 "sum.case"). INCOMPATIBILITY.

3487 - The generated constants "xxx_case", "xxx_rec", and "xxx_size" have

3488 been renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g.,

3489 "prod_case" ~> "case_prod"). INCOMPATIBILITY.

3491 * The types "'a list" and "'a option", their set and map functions,

3492 their relators, and their selectors are now produced using the new

3493 BNF-based datatype package.

3495 Renamed constants:

3496 Option.set ~> set_option

3497 Option.map ~> map_option

3498 option_rel ~> rel_option

3500 Renamed theorems:

3501 set_def ~> set_rec[abs_def]

3502 map_def ~> map_rec[abs_def]

3503 Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")

3504 option.recs ~> option.rec

3505 list_all2_def ~> list_all2_iff

3506 set.simps ~> set_simps (or the slightly different "list.set")

3507 map.simps ~> list.map

3508 hd.simps ~> list.sel(1)

3509 tl.simps ~> list.sel(2-3)

3510 the.simps ~> option.sel

3512 INCOMPATIBILITY.

3514 * The following map functions and relators have been renamed:

3515 sum_map ~> map_sum

3516 map_pair ~> map_prod

3517 prod_rel ~> rel_prod

3518 sum_rel ~> rel_sum

3519 fun_rel ~> rel_fun

3520 set_rel ~> rel_set

3521 filter_rel ~> rel_filter

3522 fset_rel ~> rel_fset (in "src/HOL/Library/FSet.thy")

3523 cset_rel ~> rel_cset (in "src/HOL/Library/Countable_Set_Type.thy")

3524 vset ~> rel_vset (in "src/HOL/Library/Quotient_Set.thy")

3526 INCOMPATIBILITY.

3528 * Lifting and Transfer:

3529 - a type variable as a raw type is supported

3530 - stronger reflexivity prover

3531 - rep_eq is always generated by lift_definition

3532 - setup for Lifting/Transfer is now automated for BNFs

3533 + holds for BNFs that do not contain a dead variable

3534 + relator_eq, relator_mono, relator_distr, relator_domain,

3535 relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total,

3536 right_unique, right_total, left_unique, left_total are proved

3537 automatically

3538 + definition of a predicator is generated automatically

3539 + simplification rules for a predicator definition are proved

3540 automatically for datatypes

3541 - consolidation of the setup of Lifting/Transfer

3542 + property that a relator preservers reflexivity is not needed any

3543 more

3544 Minor INCOMPATIBILITY.

3545 + left_total and left_unique rules are now transfer rules

3546 (reflexivity_rule attribute not needed anymore)

3547 INCOMPATIBILITY.

3548 + Domainp does not have to be a separate assumption in

3549 relator_domain theorems (=> more natural statement)

3550 INCOMPATIBILITY.

3551 - registration of code equations is more robust

3552 Potential INCOMPATIBILITY.

3553 - respectfulness proof obligation is preprocessed to a more readable

3554 form

3555 Potential INCOMPATIBILITY.

3556 - eq_onp is always unfolded in respectfulness proof obligation

3557 Potential INCOMPATIBILITY.

3558 - unregister lifting setup for Code_Numeral.integer and

3559 Code_Numeral.natural

3560 Potential INCOMPATIBILITY.

3561 - Lifting.invariant -> eq_onp

3562 INCOMPATIBILITY.

3564 * New internal SAT solver "cdclite" that produces models and proof

3565 traces. This solver replaces the internal SAT solvers "enumerate" and

3566 "dpll". Applications that explicitly used one of these two SAT

3567 solvers should use "cdclite" instead. In addition, "cdclite" is now

3568 the default SAT solver for the "sat" and "satx" proof methods and

3569 corresponding tactics; the old default can be restored using "declare

3570 [[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY.

3572 * SMT module: A new version of the SMT module, temporarily called

3573 "SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g.,

3574 4.3). The new proof method is called "smt2". CVC3 and CVC4 are also

3575 supported as oracles. Yices is no longer supported, because no version

3576 of the solver can handle both SMT-LIB 2 and quantifiers.

3578 * Activation of Z3 now works via "z3_non_commercial" system option

3579 (without requiring restart), instead of former settings variable

3580 "Z3_NON_COMMERCIAL". The option can be edited in Isabelle/jEdit menu

3581 Plugin Options / Isabelle / General.

3583 * Sledgehammer:

3584 - Z3 can now produce Isar proofs.

3585 - MaSh overhaul:

3586 . New SML-based learning algorithms eliminate the dependency on

3587 Python and increase performance and reliability.

3588 . MaSh and MeSh are now used by default together with the

3589 traditional MePo (Meng-Paulson) relevance filter. To disable

3590 MaSh, set the "MaSh" system option in Isabelle/jEdit Plugin

3591 Options / Isabelle / General to "none".

3592 - New option:

3593 smt_proofs

3594 - Renamed options:

3595 isar_compress ~> compress

3596 isar_try0 ~> try0

3598 INCOMPATIBILITY.

3600 * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.

3602 * Nitpick:

3603 - Fixed soundness bug whereby mutually recursive datatypes could

3604 take infinite values.

3605 - Fixed soundness bug with low-level number functions such as

3606 "Abs_Integ" and "Rep_Integ".

3607 - Removed "std" option.

3608 - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to

3609 "hide_types".

3611 * Metis: Removed legacy proof method 'metisFT'. Use 'metis

3612 (full_types)' instead. INCOMPATIBILITY.

3614 * Try0: Added 'algebra' and 'meson' to the set of proof methods.

3616 * Adjustion of INF and SUP operations:

3617 - Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.

3618 - Consolidated theorem names containing INFI and SUPR: have INF and

3619 SUP instead uniformly.

3620 - More aggressive normalization of expressions involving INF and Inf

3621 or SUP and Sup.

3622 - INF_image and SUP_image do not unfold composition.

3623 - Dropped facts INF_comp, SUP_comp.

3624 - Default congruence rules strong_INF_cong and strong_SUP_cong, with

3625 simplifier implication in premises. Generalize and replace former

3626 INT_cong, SUP_cong

3628 INCOMPATIBILITY.

3630 * SUP and INF generalized to conditionally_complete_lattice.

3632 * Swapped orientation of facts image_comp and vimage_comp:

3634 image_compose ~> image_comp [symmetric]

3635 image_comp ~> image_comp [symmetric]

3636 vimage_compose ~> vimage_comp [symmetric]

3637 vimage_comp ~> vimage_comp [symmetric]

3639 INCOMPATIBILITY.

3641 * Theory reorganization: split of Big_Operators.thy into

3642 Groups_Big.thy and Lattices_Big.thy.

3644 * Consolidated some facts about big group operators:

3646 setsum_0' ~> setsum.neutral

3647 setsum_0 ~> setsum.neutral_const

3648 setsum_addf ~> setsum.distrib

3649 setsum_cartesian_product ~> setsum.cartesian_product

3650 setsum_cases ~> setsum.If_cases

3651 setsum_commute ~> setsum.commute

3652 setsum_cong ~> setsum.cong

3653 setsum_delta ~> setsum.delta

3654 setsum_delta' ~> setsum.delta'

3655 setsum_diff1' ~> setsum.remove

3656 setsum_empty ~> setsum.empty

3657 setsum_infinite ~> setsum.infinite

3658 setsum_insert ~> setsum.insert

3659 setsum_inter_restrict'' ~> setsum.inter_filter

3660 setsum_mono_zero_cong_left ~> setsum.mono_neutral_cong_left

3661 setsum_mono_zero_cong_right ~> setsum.mono_neutral_cong_right

3662 setsum_mono_zero_left ~> setsum.mono_neutral_left

3663 setsum_mono_zero_right ~> setsum.mono_neutral_right

3664 setsum_reindex ~> setsum.reindex

3665 setsum_reindex_cong ~> setsum.reindex_cong

3666 setsum_reindex_nonzero ~> setsum.reindex_nontrivial

3667 setsum_restrict_set ~> setsum.inter_restrict

3668 setsum_Plus ~> setsum.Plus

3669 setsum_setsum_restrict ~> setsum.commute_restrict

3670 setsum_Sigma ~> setsum.Sigma

3671 setsum_subset_diff ~> setsum.subset_diff

3672 setsum_Un_disjoint ~> setsum.union_disjoint

3673 setsum_UN_disjoint ~> setsum.UNION_disjoint

3674 setsum_Un_Int ~> setsum.union_inter

3675 setsum_Union_disjoint ~> setsum.Union_disjoint

3676 setsum_UNION_zero ~> setsum.Union_comp

3677 setsum_Un_zero ~> setsum.union_inter_neutral

3678 strong_setprod_cong ~> setprod.strong_cong

3679 strong_setsum_cong ~> setsum.strong_cong

3680 setprod_1' ~> setprod.neutral

3681 setprod_1 ~> setprod.neutral_const

3682 setprod_cartesian_product ~> setprod.cartesian_product

3683 setprod_cong ~> setprod.cong

3684 setprod_delta ~> setprod.delta

3685 setprod_delta' ~> setprod.delta'

3686 setprod_empty ~> setprod.empty

3687 setprod_infinite ~> setprod.infinite

3688 setprod_insert ~> setprod.insert

3689 setprod_mono_one_cong_left ~> setprod.mono_neutral_cong_left

3690 setprod_mono_one_cong_right ~> setprod.mono_neutral_cong_right

3691 setprod_mono_one_left ~> setprod.mono_neutral_left

3692 setprod_mono_one_right ~> setprod.mono_neutral_right

3693 setprod_reindex ~> setprod.reindex

3694 setprod_reindex_cong ~> setprod.reindex_cong

3695 setprod_reindex_nonzero ~> setprod.reindex_nontrivial

3696 setprod_Sigma ~> setprod.Sigma

3697 setprod_subset_diff ~> setprod.subset_diff

3698 setprod_timesf ~> setprod.distrib

3699 setprod_Un2 ~> setprod.union_diff2

3700 setprod_Un_disjoint ~> setprod.union_disjoint

3701 setprod_UN_disjoint ~> setprod.UNION_disjoint

3702 setprod_Un_Int ~> setprod.union_inter

3703 setprod_Union_disjoint ~> setprod.Union_disjoint

3704 setprod_Un_one ~> setprod.union_inter_neutral

3706 Dropped setsum_cong2 (simple variant of setsum.cong).

3707 Dropped setsum_inter_restrict' (simple variant of setsum.inter_restrict)

3708 Dropped setsum_reindex_id, setprod_reindex_id

3709 (simple variants of setsum.reindex [symmetric], setprod.reindex [symmetric]).

3711 INCOMPATIBILITY.

3713 * Abolished slightly odd global lattice interpretation for min/max.

3715 Fact consolidations:

3716 min_max.inf_assoc ~> min.assoc

3717 min_max.inf_commute ~> min.commute

3718 min_max.inf_left_commute ~> min.left_commute

3719 min_max.inf_idem ~> min.idem

3720 min_max.inf_left_idem ~> min.left_idem

3721 min_max.inf_right_idem ~> min.right_idem

3722 min_max.sup_assoc ~> max.assoc

3723 min_max.sup_commute ~> max.commute

3724 min_max.sup_left_commute ~> max.left_commute

3725 min_max.sup_idem ~> max.idem

3726 min_max.sup_left_idem ~> max.left_idem

3727 min_max.sup_inf_distrib1 ~> max_min_distrib2

3728 min_max.sup_inf_distrib2 ~> max_min_distrib1

3729 min_max.inf_sup_distrib1 ~> min_max_distrib2

3730 min_max.inf_sup_distrib2 ~> min_max_distrib1

3731 min_max.distrib ~> min_max_distribs

3732 min_max.inf_absorb1 ~> min.absorb1

3733 min_max.inf_absorb2 ~> min.absorb2

3734 min_max.sup_absorb1 ~> max.absorb1

3735 min_max.sup_absorb2 ~> max.absorb2

3736 min_max.le_iff_inf ~> min.absorb_iff1

3737 min_max.le_iff_sup ~> max.absorb_iff2

3738 min_max.inf_le1 ~> min.cobounded1

3739 min_max.inf_le2 ~> min.cobounded2

3740 le_maxI1, min_max.sup_ge1 ~> max.cobounded1

3741 le_maxI2, min_max.sup_ge2 ~> max.cobounded2

3742 min_max.le_infI1 ~> min.coboundedI1

3743 min_max.le_infI2 ~> min.coboundedI2

3744 min_max.le_supI1 ~> max.coboundedI1

3745 min_max.le_supI2 ~> max.coboundedI2

3746 min_max.less_infI1 ~> min.strict_coboundedI1

3747 min_max.less_infI2 ~> min.strict_coboundedI2

3748 min_max.less_supI1 ~> max.strict_coboundedI1

3749 min_max.less_supI2 ~> max.strict_coboundedI2

3750 min_max.inf_mono ~> min.mono

3751 min_max.sup_mono ~> max.mono

3752 min_max.le_infI, min_max.inf_greatest ~> min.boundedI

3753 min_max.le_supI, min_max.sup_least ~> max.boundedI

3754 min_max.le_inf_iff ~> min.bounded_iff

3755 min_max.le_sup_iff ~> max.bounded_iff

3757 For min_max.inf_sup_aci, prefer (one of) min.commute, min.assoc,

3758 min.left_commute, min.left_idem, max.commute, max.assoc,

3759 max.left_commute, max.left_idem directly.

3761 For min_max.inf_sup_ord, prefer (one of) min.cobounded1,

3762 min.cobounded2, max.cobounded1m max.cobounded2 directly.

3764 For min_ac or max_ac, prefer more general collection ac_simps.

3766 INCOMPATIBILITY.

3768 * Theorem disambiguation Inf_le_Sup (on finite sets) ~>

3769 Inf_fin_le_Sup_fin. INCOMPATIBILITY.

3771 * Qualified constant names Wellfounded.acc, Wellfounded.accp.

3772 INCOMPATIBILITY.

3774 * Fact generalization and consolidation:

3775 neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1

3777 INCOMPATIBILITY.

3779 * Purely algebraic definition of even. Fact generalization and

3780 consolidation:

3781 nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd

3782 even_zero_(nat|int) ~> even_zero

3784 INCOMPATIBILITY.

3786 * Abolished neg_numeral.

3787 - Canonical representation for minus one is "- 1".

3788 - Canonical representation for other negative numbers is "- (numeral _)".

3789 - When devising rule sets for number calculation, consider the

3790 following canonical cases: 0, 1, numeral _, - 1, - numeral _.

3791 - HOLogic.dest_number also recognizes numerals in non-canonical forms

3792 like "numeral One", "- numeral One", "- 0" and even "- ... - _".

3793 - Syntax for negative numerals is mere input syntax.

3795 INCOMPATIBILITY.

3797 * Reduced name variants for rules on associativity and commutativity:

3799 add_assoc ~> add.assoc

3800 add_commute ~> add.commute

3801 add_left_commute ~> add.left_commute

3802 mult_assoc ~> mult.assoc

3803 mult_commute ~> mult.commute

3804 mult_left_commute ~> mult.left_commute

3805 nat_add_assoc ~> add.assoc

3806 nat_add_commute ~> add.commute

3807 nat_add_left_commute ~> add.left_commute

3808 nat_mult_assoc ~> mult.assoc

3809 nat_mult_commute ~> mult.commute

3810 eq_assoc ~> iff_assoc

3811 eq_left_commute ~> iff_left_commute

3813 INCOMPATIBILITY.

3815 * Fact collections add_ac and mult_ac are considered old-fashioned.

3816 Prefer ac_simps instead, or specify rules

3817 (add|mult).(assoc|commute|left_commute) individually.

3819 * Elimination of fact duplicates:

3820 equals_zero_I ~> minus_unique

3821 diff_eq_0_iff_eq ~> right_minus_eq

3822 nat_infinite ~> infinite_UNIV_nat

3823 int_infinite ~> infinite_UNIV_int

3825 INCOMPATIBILITY.

3827 * Fact name consolidation:

3828 diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus

3829 minus_le_self_iff ~> neg_less_eq_nonneg

3830 le_minus_self_iff ~> less_eq_neg_nonpos

3831 neg_less_nonneg ~> neg_less_pos

3832 less_minus_self_iff ~> less_neg_neg [simp]

3834 INCOMPATIBILITY.

3836 * More simplification rules on unary and binary minus:

3837 add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1,

3838 add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,

3839 add_minus_cancel, diff_add_cancel, le_add_same_cancel1,

3840 le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,

3841 minus_add_cancel, uminus_add_conv_diff. These correspondingly have

3842 been taken away from fact collections algebra_simps and field_simps.

3843 INCOMPATIBILITY.

3845 To restore proofs, the following patterns are helpful:

3847 a) Arbitrary failing proof not involving "diff_def":

3848 Consider simplification with algebra_simps or field_simps.

3850 b) Lifting rules from addition to subtraction:

3851 Try with "using <rule for addition> of [... "- _" ...]" by simp".

3853 c) Simplification with "diff_def": just drop "diff_def".

3854 Consider simplification with algebra_simps or field_simps;

3855 or the brute way with

3856 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff".

3858 * Introduce bdd_above and bdd_below in theory

3859 Conditionally_Complete_Lattices, use them instead of explicitly

3860 stating boundedness of sets.

3862 * ccpo.admissible quantifies only over non-empty chains to allow more

3863 syntax-directed proof rules; the case of the empty chain shows up as

3864 additional case in fixpoint induction proofs. INCOMPATIBILITY.

3866 * Removed and renamed theorems in Series:

3867 summable_le ~> suminf_le

3868 suminf_le ~> suminf_le_const

3869 series_pos_le ~> setsum_le_suminf

3870 series_pos_less ~> setsum_less_suminf

3871 suminf_ge_zero ~> suminf_nonneg

3872 suminf_gt_zero ~> suminf_pos

3873 suminf_gt_zero_iff ~> suminf_pos_iff

3874 summable_sumr_LIMSEQ_suminf ~> summable_LIMSEQ

3875 suminf_0_le ~> suminf_nonneg [rotate]

3876 pos_summable ~> summableI_nonneg_bounded

3877 ratio_test ~> summable_ratio_test

3879 removed series_zero, replaced by sums_finite

3881 removed auxiliary lemmas:

3883 sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group,

3884 half, le_Suc_ex_iff, lemma_realpow_diff_sumr,

3885 real_setsum_nat_ivl_bounded, summable_le2, ratio_test_lemma2,

3886 sumr_minus_one_realpow_zerom, sumr_one_lb_realpow_zero,

3887 summable_convergent_sumr_iff, sumr_diff_mult_const

3889 INCOMPATIBILITY.

3891 * Replace (F)DERIV syntax by has_derivative:

3892 - "(f has_derivative f') (at x within s)" replaces "FDERIV f x : s : f'"

3894 - "(f has_field_derivative f') (at x within s)" replaces "DERIV f x : s : f'"

3896 - "f differentiable at x within s" replaces "_ differentiable _ in _" syntax

3898 - removed constant isDiff

3900 - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as

3901 input syntax.

3903 - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed.

3905 - Renamed FDERIV_... lemmas to has_derivative_...

3907 - renamed deriv (the syntax constant used for "DERIV _ _ :> _") to DERIV

3909 - removed DERIV_intros, has_derivative_eq_intros

3911 - introduced derivative_intros and deriative_eq_intros which

3912 includes now rules for DERIV, has_derivative and

3913 has_vector_derivative.

3915 - Other renamings:

3916 differentiable_def ~> real_differentiable_def

3917 differentiableE ~> real_differentiableE

3918 fderiv_def ~> has_derivative_at

3919 field_fderiv_def ~> field_has_derivative_at

3920 isDiff_der ~> differentiable_def

3921 deriv_fderiv ~> has_field_derivative_def

3922 deriv_def ~> DERIV_def

3924 INCOMPATIBILITY.

3926 * Include more theorems in continuous_intros. Remove the

3927 continuous_on_intros, isCont_intros collections, these facts are now

3928 in continuous_intros.

3930 * Theorems about complex numbers are now stated only using Re and Im,

3931 the Complex constructor is not used anymore. It is possible to use

3932 primcorec to defined the behaviour of a complex-valued function.

3934 Removed theorems about the Complex constructor from the simpset, they

3935 are available as the lemma collection legacy_Complex_simps. This

3936 especially removes

3938 i_complex_of_real: "ii * complex_of_real r = Complex 0 r".

3940 Instead the reverse direction is supported with

3941 Complex_eq: "Complex a b = a + \<i> * b"

3943 Moved csqrt from Fundamental_Algebra_Theorem to Complex.

3945 Renamings:

3946 Re/Im ~> complex.sel

3947 complex_Re/Im_zero ~> zero_complex.sel

3948 complex_Re/Im_add ~> plus_complex.sel

3949 complex_Re/Im_minus ~> uminus_complex.sel

3950 complex_Re/Im_diff ~> minus_complex.sel

3951 complex_Re/Im_one ~> one_complex.sel

3952 complex_Re/Im_mult ~> times_complex.sel

3953 complex_Re/Im_inverse ~> inverse_complex.sel

3954 complex_Re/Im_scaleR ~> scaleR_complex.sel

3955 complex_Re/Im_i ~> ii.sel

3956 complex_Re/Im_cnj ~> cnj.sel

3957 Re/Im_cis ~> cis.sel

3959 complex_divide_def ~> divide_complex_def

3960 complex_norm_def ~> norm_complex_def

3961 cmod_def ~> norm_complex_de

3963 Removed theorems:

3964 complex_zero_def

3965 complex_add_def

3966 complex_minus_def

3967 complex_diff_def

3968 complex_one_def

3969 complex_mult_def

3970 complex_inverse_def

3971 complex_scaleR_def

3973 INCOMPATIBILITY.

3975 * Theory Lubs moved HOL image to HOL-Library. It is replaced by

3976 Conditionally_Complete_Lattices. INCOMPATIBILITY.

3978 * HOL-Library: new theory src/HOL/Library/Tree.thy.

3980 * HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it

3981 is subsumed by session Kleene_Algebra in AFP.

3983 * HOL-Library / theory RBT: various constants and facts are hidden;

3984 lifting setup is unregistered. INCOMPATIBILITY.

3986 * HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.

3988 * HOL-Word: bit representations prefer type bool over type bit.

3989 INCOMPATIBILITY.

3991 * HOL-Word:

3992 - Abandoned fact collection "word_arith_alts", which is a duplicate

3993 of "word_arith_wis".

3994 - Dropped first (duplicated) element in fact collections

3995 "sint_word_ariths", "word_arith_alts", "uint_word_ariths",

3996 "uint_word_arith_bintrs".

3998 * HOL-Number_Theory:

3999 - consolidated the proofs of the binomial theorem

4000 - the function fib is again of type nat => nat and not overloaded

4001 - no more references to Old_Number_Theory in the HOL libraries

4002 (except the AFP)

4004 INCOMPATIBILITY.

4006 * HOL-Multivariate_Analysis:

4007 - Type class ordered_real_vector for ordered vector spaces.

4008 - New theory Complex_Basic_Analysis defining complex derivatives,

4009 holomorphic functions, etc., ported from HOL Light's canal.ml.

4010 - Changed order of ordered_euclidean_space to be compatible with

4011 pointwise ordering on products. Therefore instance of

4012 conditionally_complete_lattice and ordered_real_vector.

4013 INCOMPATIBILITY: use box instead of greaterThanLessThan or

4014 explicit set-comprehensions with eucl_less for other (half-)open

4015 intervals.

4016 - removed dependencies on type class ordered_euclidean_space with

4017 introduction of "cbox" on euclidean_space

4018 - renamed theorems:

4019 interval ~> box

4020 mem_interval ~> mem_box

4021 interval_eq_empty ~> box_eq_empty

4022 interval_ne_empty ~> box_ne_empty

4023 interval_sing(1) ~> cbox_sing

4024 interval_sing(2) ~> box_sing

4025 subset_interval_imp ~> subset_box_imp

4026 subset_interval ~> subset_box

4027 open_interval ~> open_box

4028 closed_interval ~> closed_cbox

4029 interior_closed_interval ~> interior_cbox

4030 bounded_closed_interval ~> bounded_cbox

4031 compact_interval ~> compact_cbox

4032 bounded_subset_closed_interval_symmetric ~> bounded_subset_cbox_symmetric

4033 bounded_subset_closed_interval ~> bounded_subset_cbox

4034 mem_interval_componentwiseI ~> mem_box_componentwiseI

4035 convex_box ~> convex_prod

4036 rel_interior_real_interval ~> rel_interior_real_box

4037 convex_interval ~> convex_box

4038 convex_hull_eq_real_interval ~> convex_hull_eq_real_cbox

4039 frechet_derivative_within_closed_interval ~> frechet_derivative_within_cbox

4040 content_closed_interval' ~> content_cbox'

4041 elementary_subset_interval ~> elementary_subset_box

4042 diameter_closed_interval ~> diameter_cbox

4043 frontier_closed_interval ~> frontier_cbox

4044 frontier_open_interval ~> frontier_box

4045 bounded_subset_open_interval_symmetric ~> bounded_subset_box_symmetric

4046 closure_open_interval ~> closure_box

4047 open_closed_interval_convex ~> open_cbox_convex

4048 open_interval_midpoint ~> box_midpoint

4049 content_image_affinity_interval ~> content_image_affinity_cbox

4050 is_interval_interval ~> is_interval_cbox + is_interval_box + is_interval_closed_interval

4051 bounded_interval ~> bounded_closed_interval + bounded_boxes

4053 - respective theorems for intervals over the reals:

4054 content_closed_interval + content_cbox

4055 has_integral + has_integral_real

4056 fine_division_exists + fine_division_exists_real

4057 has_integral_null + has_integral_null_real

4058 tagged_division_union_interval + tagged_division_union_interval_real

4059 has_integral_const + has_integral_const_real

4060 integral_const + integral_const_real

4061 has_integral_bound + has_integral_bound_real

4062 integrable_continuous + integrable_continuous_real

4063 integrable_subinterval + integrable_subinterval_real

4064 has_integral_reflect_lemma + has_integral_reflect_lemma_real

4065 integrable_reflect + integrable_reflect_real

4066 integral_reflect + integral_reflect_real

4067 image_affinity_interval + image_affinity_cbox

4068 image_smult_interval + image_smult_cbox

4069 integrable_const + integrable_const_ivl

4070 integrable_on_subinterval + integrable_on_subcbox

4072 - renamed theorems:

4073 derivative_linear ~> has_derivative_bounded_linear

4074 derivative_is_linear ~> has_derivative_linear

4075 bounded_linear_imp_linear ~> bounded_linear.linear

4077 * HOL-Probability:

4078 - Renamed positive_integral to nn_integral:

4080 . Renamed all lemmas "*positive_integral*" to *nn_integral*"

4081 positive_integral_positive ~> nn_integral_nonneg

4083 . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.

4085 - replaced the Lebesgue integral on real numbers by the more general

4086 Bochner integral for functions into a real-normed vector space.

4088 integral_zero ~> integral_zero / integrable_zero

4089 integral_minus ~> integral_minus / integrable_minus

4090 integral_add ~> integral_add / integrable_add

4091 integral_diff ~> integral_diff / integrable_diff

4092 integral_setsum ~> integral_setsum / integrable_setsum

4093 integral_multc ~> integral_mult_left / integrable_mult_left

4094 integral_cmult ~> integral_mult_right / integrable_mult_right

4095 integral_triangle_inequality~> integral_norm_bound

4096 integrable_nonneg ~> integrableI_nonneg

4097 integral_positive ~> integral_nonneg_AE

4098 integrable_abs_iff ~> integrable_abs_cancel

4099 positive_integral_lim_INF ~> nn_integral_liminf

4100 lebesgue_real_affine ~> lborel_real_affine

4101 borel_integral_has_integral ~> has_integral_lebesgue_integral

4102 integral_indicator ~>

4103 integral_real_indicator / integrable_real_indicator

4104 positive_integral_fst ~> nn_integral_fst'

4105 positive_integral_fst_measurable ~> nn_integral_fst

4106 positive_integral_snd_measurable ~> nn_integral_snd

4108 integrable_fst_measurable ~>

4109 integral_fst / integrable_fst / AE_integrable_fst

4111 integrable_snd_measurable ~>

4112 integral_snd / integrable_snd / AE_integrable_snd

4114 integral_monotone_convergence ~>

4115 integral_monotone_convergence / integrable_monotone_convergence

4117 integral_monotone_convergence_at_top ~>

4118 integral_monotone_convergence_at_top /

4119 integrable_monotone_convergence_at_top

4121 has_integral_iff_positive_integral_lebesgue ~>

4122 has_integral_iff_has_bochner_integral_lebesgue_nonneg

4124 lebesgue_integral_has_integral ~>

4125 has_integral_integrable_lebesgue_nonneg

4127 positive_integral_lebesgue_has_integral ~>

4128 integral_has_integral_lebesgue_nonneg /

4129 integrable_has_integral_lebesgue_nonneg

4131 lebesgue_integral_real_affine ~>

4132 nn_integral_real_affine

4134 has_integral_iff_positive_integral_lborel ~>

4135 integral_has_integral_nonneg / integrable_has_integral_nonneg

4137 The following theorems where removed:

4139 lebesgue_integral_nonneg

4140 lebesgue_integral_uminus

4141 lebesgue_integral_cmult

4142 lebesgue_integral_multc

4143 lebesgue_integral_cmult_nonneg

4144 integral_cmul_indicator

4145 integral_real

4147 - Formalized properties about exponentially, Erlang, and normal

4148 distributed random variables.

4150 * HOL-Decision_Procs: Separate command 'approximate' for approximative

4151 computation in src/HOL/Decision_Procs/Approximation. Minor

4152 INCOMPATIBILITY.

4155 *** Scala ***

4157 * The signature and semantics of Document.Snapshot.cumulate_markup /

4158 select_markup have been clarified. Markup is now traversed in the

4159 order of reports given by the prover: later markup is usually more

4160 specific and may override results accumulated so far. The elements

4161 guard is mandatory and checked precisely. Subtle INCOMPATIBILITY.

4163 * Substantial reworking of internal PIDE protocol communication

4164 channels. INCOMPATIBILITY.

4167 *** ML ***

4169 * Subtle change of semantics of Thm.eq_thm: theory stamps are not

4170 compared (according to Thm.thm_ord), but assumed to be covered by the

4171 current background theory. Thus equivalent data produced in different

4172 branches of the theory graph usually coincides (e.g. relevant for

4173 theory merge). Note that the softer Thm.eq_thm_prop is often more

4174 appropriate than Thm.eq_thm.

4176 * Proper context for basic Simplifier operations: rewrite_rule,

4177 rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to

4178 pass runtime Proof.context (and ensure that the simplified entity

4179 actually belongs to it).

4181 * Proper context discipline for read_instantiate and instantiate_tac:

4182 variables that are meant to become schematic need to be given as

4183 fixed, and are generalized by the explicit context of local variables.

4184 This corresponds to Isar attributes "where" and "of" with 'for'

4185 declaration. INCOMPATIBILITY, also due to potential change of indices

4186 of schematic variables.

4188 * Moved ML_Compiler.exn_trace and other operations on exceptions to

4189 structure Runtime. Minor INCOMPATIBILITY.

4191 * Discontinued old Toplevel.debug in favour of system option

4192 "ML_exception_trace", which may be also declared within the context

4193 via "declare [[ML_exception_trace = true]]". Minor INCOMPATIBILITY.

4195 * Renamed configuration option "ML_trace" to "ML_source_trace". Minor

4196 INCOMPATIBILITY.

4198 * Configuration option "ML_print_depth" controls the pretty-printing

4199 depth of the ML compiler within the context. The old print_depth in

4200 ML is still available as default_print_depth, but rarely used. Minor

4201 INCOMPATIBILITY.

4203 * Toplevel function "use" refers to raw ML bootstrap environment,

4204 without Isar context nor antiquotations. Potential INCOMPATIBILITY.

4205 Note that 'ML_file' is the canonical command to load ML files into the

4206 formal context.

4208 * Simplified programming interface to define ML antiquotations, see

4209 structure ML_Antiquotation. Minor INCOMPATIBILITY.

4211 * ML antiquotation @{here} refers to its source position, which is

4212 occasionally useful for experimentation and diagnostic purposes.

4214 * ML antiquotation @{path} produces a Path.T value, similarly to

4215 Path.explode, but with compile-time check against the file-system and

4216 some PIDE markup. Note that unlike theory source, ML does not have a

4217 well-defined master directory, so an absolute symbolic path

4218 specification is usually required, e.g. "~~/src/HOL".

4220 * ML antiquotation @{print} inlines a function to print an arbitrary

4221 ML value, which is occasionally useful for diagnostic or demonstration

4222 purposes.

4225 *** System ***

4227 * Proof General with its traditional helper scripts is now an optional

4228 Isabelle component, e.g. see ProofGeneral-4.2-2 from the Isabelle

4229 component repository http://isabelle.in.tum.de/components/. Note that

4230 the "system" manual provides general explanations about add-on

4231 components, especially those that are not bundled with the release.

4233 * The raw Isabelle process executable has been renamed from

4234 "isabelle-process" to "isabelle_process", which conforms to common

4235 shell naming conventions, and allows to define a shell function within

4236 the Isabelle environment to avoid dynamic path lookup. Rare

4237 incompatibility for old tools that do not use the ISABELLE_PROCESS

4238 settings variable.

4240 * Former "isabelle tty" has been superseded by "isabelle console",

4241 with implicit build like "isabelle jedit", and without the mostly

4242 obsolete Isar TTY loop.

4244 * Simplified "isabelle display" tool. Settings variables DVI_VIEWER

4245 and PDF_VIEWER now refer to the actual programs, not shell

4246 command-lines. Discontinued option -c: invocation may be asynchronous

4247 via desktop environment, without any special precautions. Potential

4248 INCOMPATIBILITY with ambitious private settings.

4250 * Removed obsolete "isabelle unsymbolize". Note that the usual format

4251 for email communication is the Unicode rendering of Isabelle symbols,

4252 as produced by Isabelle/jEdit, for example.

4254 * Removed obsolete tool "wwwfind". Similar functionality may be

4255 integrated into Isabelle/jEdit eventually.

4257 * Improved 'display_drafts' concerning desktop integration and

4258 repeated invocation in PIDE front-end: re-use single file

4259 $ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views.

4261 * Session ROOT specifications require explicit 'document_files' for

4262 robust dependencies on LaTeX sources. Only these explicitly given

4263 files are copied to the document output directory, before document

4264 processing is started.

4266 * Windows: support for regular TeX installation (e.g. MiKTeX) instead

4267 of TeX Live from Cygwin.

4271 New in Isabelle2013-2 (December 2013)

4272 -------------------------------------

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

4276 * More robust editing of running commands with internal forks,

4277 e.g. non-terminating 'by' steps.

4279 * More relaxed Sledgehammer panel: avoid repeated application of query

4280 after edits surrounding the command location.

4282 * More status information about commands that are interrupted

4283 accidentally (via physical event or Poly/ML runtime system signal,

4284 e.g. out-of-memory).

4287 *** System ***

4289 * More robust termination of external processes managed by

4290 Isabelle/ML: support cancellation of tasks within the range of

4291 milliseconds, as required for PIDE document editing with automatically

4292 tried tools (e.g. Sledgehammer).

4294 * Reactivated Isabelle/Scala kill command for external processes on

4295 Mac OS X, which was accidentally broken in Isabelle2013-1 due to a

4296 workaround for some Debian/Ubuntu Linux versions from 2013.

4300 New in Isabelle2013-1 (November 2013)

4301 -------------------------------------

4303 *** General ***

4305 * Discontinued obsolete 'uses' within theory header. Note that

4306 commands like 'ML_file' work without separate declaration of file

4307 dependencies. Minor INCOMPATIBILITY.

4309 * Discontinued redundant 'use' command, which was superseded by

4310 'ML_file' in Isabelle2013. Minor INCOMPATIBILITY.

4312 * Simplified subscripts within identifiers, using plain \<^sub>

4313 instead of the second copy \<^isub> and \<^isup>. Superscripts are

4314 only for literal tokens within notation; explicit mixfix annotations

4315 for consts or fixed variables may be used as fall-back for unusual

4316 names. Obsolete \<twosuperior> has been expanded to \<^sup>2 in

4317 Isabelle/HOL. INCOMPATIBILITY, use "isabelle update_sub_sup" to

4318 standardize symbols as a starting point for further manual cleanup.

4319 The ML reference variable "legacy_isub_isup" may be set as temporary

4320 workaround, to make the prover accept a subset of the old identifier

4321 syntax.

4323 * Document antiquotations: term style "isub" has been renamed to

4324 "sub". Minor INCOMPATIBILITY.

4326 * Uniform management of "quick_and_dirty" as system option (see also

4327 "isabelle options"), configuration option within the context (see also

4328 Config.get in Isabelle/ML), and attribute in Isabelle/Isar. Minor

4329 INCOMPATIBILITY, need to use more official Isabelle means to access

4330 quick_and_dirty, instead of historical poking into mutable reference.

4332 * Renamed command 'print_configs' to 'print_options'. Minor

4333 INCOMPATIBILITY.

4335 * Proper diagnostic command 'print_state'. Old 'pr' (with its

4336 implicit change of some global references) is retained for now as

4337 control command, e.g. for ProofGeneral 3.7.x.

4339 * Discontinued 'print_drafts' command with its old-fashioned PS output

4340 and Unix command-line print spooling. Minor INCOMPATIBILITY: use

4341 'display_drafts' instead and print via the regular document viewer.

4343 * Updated and extended "isar-ref" and "implementation" manual,

4344 eliminated old "ref" manual.

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

4349 * New manual "jedit" for Isabelle/jEdit, see isabelle doc or

4350 Documentation panel.

4352 * Dockable window "Documentation" provides access to Isabelle

4353 documentation.

4355 * Dockable window "Find" provides query operations for formal entities

4356 (GUI front-end to 'find_theorems' command).

4358 * Dockable window "Sledgehammer" manages asynchronous / parallel

4359 sledgehammer runs over existing document sources, independently of

4360 normal editing and checking process.

4362 * Dockable window "Timing" provides an overview of relevant command

4363 timing information, depending on option jedit_timing_threshold. The

4364 same timing information is shown in the extended tooltip of the

4365 command keyword, when hovering the mouse over it while the CONTROL or

4366 COMMAND modifier is pressed.

4368 * Improved dockable window "Theories": Continuous checking of proof

4369 document (visible and required parts) may be controlled explicitly,

4370 using check box or shortcut "C+e ENTER". Individual theory nodes may

4371 be marked explicitly as required and checked in full, using check box

4372 or shortcut "C+e SPACE".

4374 * Improved completion mechanism, which is now managed by the

4375 Isabelle/jEdit plugin instead of SideKick. Refined table of Isabelle

4376 symbol abbreviations (see $ISABELLE_HOME/etc/symbols).

4378 * Standard jEdit keyboard shortcut C+b complete-word is remapped to

4379 isabelle.complete for explicit completion in Isabelle sources.

4380 INCOMPATIBILITY wrt. jEdit defaults, may have to invent new shortcuts

4381 to resolve conflict.

4383 * Improved support of various "minor modes" for Isabelle NEWS,

4384 options, session ROOT etc., with completion and SideKick tree view.

4386 * Strictly monotonic document update, without premature cancellation of

4387 running transactions that are still needed: avoid reset/restart of

4388 such command executions while editing.

4390 * Support for asynchronous print functions, as overlay to existing

4391 document content.

4393 * Support for automatic tools in HOL, which try to prove or disprove

4394 toplevel theorem statements.

4396 * Action isabelle.reset-font-size resets main text area font size

4397 according to Isabelle/Scala plugin option "jedit_font_reset_size" (see

4398 also "Plugin Options / Isabelle / General"). It can be bound to some

4399 keyboard shortcut by the user (e.g. C+0 and/or C+NUMPAD0).

4401 * File specifications in jEdit (e.g. file browser) may refer to

4402 $ISABELLE_HOME and $ISABELLE_HOME_USER on all platforms. Discontinued

4403 obsolete $ISABELLE_HOME_WINDOWS variable.

4405 * Improved support for Linux look-and-feel "GTK+", see also "Utilities

4406 / Global Options / Appearance".

4408 * Improved support of native Mac OS X functionality via "MacOSX"

4409 plugin, which is now enabled by default.

4412 *** Pure ***

4414 * Commands 'interpretation' and 'sublocale' are now target-sensitive.

4415 In particular, 'interpretation' allows for non-persistent

4416 interpretation within "context ... begin ... end" blocks offering a

4417 light-weight alternative to 'sublocale'. See "isar-ref" manual for

4418 details.

4420 * Improved locales diagnostic command 'print_dependencies'.

4422 * Discontinued obsolete 'axioms' command, which has been marked as

4423 legacy since Isabelle2009-2. INCOMPATIBILITY, use 'axiomatization'

4424 instead, while observing its uniform scope for polymorphism.

4426 * Discontinued empty name bindings in 'axiomatization'.

4427 INCOMPATIBILITY.

4429 * System option "proofs" has been discontinued. Instead the global

4430 state of Proofterm.proofs is persistently compiled into logic images

4431 as required, notably HOL-Proofs. Users no longer need to change

4432 Proofterm.proofs dynamically. Minor INCOMPATIBILITY.

4434 * Syntax translation functions (print_translation etc.) always depend

4435 on Proof.context. Discontinued former "(advanced)" option -- this is

4436 now the default. Minor INCOMPATIBILITY.

4438 * Former global reference trace_unify_fail is now available as

4439 configuration option "unify_trace_failure" (global context only).

4441 * SELECT_GOAL now retains the syntactic context of the overall goal

4442 state (schematic variables etc.). Potential INCOMPATIBILITY in rare

4443 situations.

4446 *** HOL ***

4448 * Stronger precedence of syntax for big intersection and union on

4449 sets, in accordance with corresponding lattice operations.

4450 INCOMPATIBILITY.

4452 * Notation "{p:A. P}" now allows tuple patterns as well.

4454 * Nested case expressions are now translated in a separate check phase

4455 rather than during parsing. The data for case combinators is separated

4456 from the datatype package. The declaration attribute

4457 "case_translation" can be used to register new case combinators:

4459 declare [[case_translation case_combinator constructor1 ... constructorN]]

4461 * Code generator:

4462 - 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' /

4463 'code_instance'.

4464 - 'code_identifier' declares name hints for arbitrary identifiers in

4465 generated code, subsuming 'code_modulename'.

4467 See the isar-ref manual for syntax diagrams, and the HOL theories for

4468 examples.

4470 * Attibute 'code': 'code' now declares concrete and abstract code

4471 equations uniformly. Use explicit 'code equation' and 'code abstract'

4472 to distinguish both when desired.

4474 * Discontinued theories Code_Integer and Efficient_Nat by a more

4475 fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,

4476 Code_Target_Nat and Code_Target_Numeral. See the tutorial on code

4477 generation for details. INCOMPATIBILITY.

4479 * Numeric types are mapped by default to target language numerals:

4480 natural (replaces former code_numeral) and integer (replaces former

4481 code_int). Conversions are available as integer_of_natural /

4482 natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and

4483 Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in

4484 ML). INCOMPATIBILITY.

4486 * Function package: For mutually recursive functions f and g, separate

4487 cases rules f.cases and g.cases are generated instead of unusable

4488 f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY,

4489 in the case that the unusable rule was used nevertheless.

4491 * Function package: For each function f, new rules f.elims are

4492 generated, which eliminate equalities of the form "f x = t".

4494 * New command 'fun_cases' derives ad-hoc elimination rules for

4495 function equations as simplified instances of f.elims, analogous to

4496 inductive_cases. See ~~/src/HOL/ex/Fundefs.thy for some examples.

4498 * Lifting:

4499 - parametrized correspondence relations are now supported:

4500 + parametricity theorems for the raw term can be specified in

4501 the command lift_definition, which allow us to generate stronger

4502 transfer rules

4503 + setup_lifting generates stronger transfer rules if parametric

4504 correspondence relation can be generated

4505 + various new properties of the relator must be specified to support

4506 parametricity

4507 + parametricity theorem for the Quotient relation can be specified

4508 - setup_lifting generates domain rules for the Transfer package

4509 - stronger reflexivity prover of respectfulness theorems for type

4510 copies

4511 - ===> and --> are now local. The symbols can be introduced

4512 by interpreting the locale lifting_syntax (typically in an

4513 anonymous context)

4514 - Lifting/Transfer relevant parts of Library/Quotient_* are now in

4515 Main. Potential INCOMPATIBILITY

4516 - new commands for restoring and deleting Lifting/Transfer context:

4517 lifting_forget, lifting_update

4518 - the command print_quotmaps was renamed to print_quot_maps.

4519 INCOMPATIBILITY

4521 * Transfer:

4522 - better support for domains in Transfer: replace Domainp T

4523 by the actual invariant in a transferred goal

4524 - transfer rules can have as assumptions other transfer rules

4525 - Experimental support for transferring from the raw level to the

4526 abstract level: Transfer.transferred attribute

4527 - Attribute version of the transfer method: untransferred attribute

4529 * Reification and reflection:

4530 - Reification is now directly available in HOL-Main in structure

4531 "Reification".

4532 - Reflection now handles multiple lists with variables also.

4533 - The whole reflection stack has been decomposed into conversions.

4534 INCOMPATIBILITY.

4536 * Revised devices for recursive definitions over finite sets:

4537 - Only one fundamental fold combinator on finite set remains:

4538 Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b

4539 This is now identity on infinite sets.

4540 - Locales ("mini packages") for fundamental definitions with

4541 Finite_Set.fold: folding, folding_idem.

4542 - Locales comm_monoid_set, semilattice_order_set and

4543 semilattice_neutr_order_set for big operators on sets.

4544 See theory Big_Operators for canonical examples.

4545 Note that foundational constants comm_monoid_set.F and

4546 semilattice_set.F correspond to former combinators fold_image

4547 and fold1 respectively. These are now gone. You may use

4548 those foundational constants as substitutes, but it is

4549 preferable to interpret the above locales accordingly.

4550 - Dropped class ab_semigroup_idem_mult (special case of lattice,

4551 no longer needed in connection with Finite_Set.fold etc.)

4552 - Fact renames:

4553 card.union_inter ~> card_Un_Int [symmetric]

4554 card.union_disjoint ~> card_Un_disjoint

4555 INCOMPATIBILITY.

4557 * Locale hierarchy for abstract orderings and (semi)lattices.

4559 * Complete_Partial_Order.admissible is defined outside the type class

4560 ccpo, but with mandatory prefix ccpo. Admissibility theorems lose the

4561 class predicate assumption or sort constraint when possible.

4562 INCOMPATIBILITY.

4564 * Introduce type class "conditionally_complete_lattice": Like a

4565 complete lattice but does not assume the existence of the top and

4566 bottom elements. Allows to generalize some lemmas about reals and

4567 extended reals. Removed SupInf and replaced it by the instantiation

4568 of conditionally_complete_lattice for real. Renamed lemmas about

4569 conditionally-complete lattice from Sup_... to cSup_... and from

4570 Inf_... to cInf_... to avoid hidding of similar complete lattice

4571 lemmas.

4573 * Introduce type class linear_continuum as combination of

4574 conditionally-complete lattices and inner dense linorders which have

4575 more than one element. INCOMPATIBILITY.

4577 * Introduced type classes order_top and order_bot. The old classes top

4578 and bot only contain the syntax without assumptions. INCOMPATIBILITY:

4579 Rename bot -> order_bot, top -> order_top

4581 * Introduce type classes "no_top" and "no_bot" for orderings without

4582 top and bottom elements.

4584 * Split dense_linorder into inner_dense_order and no_top, no_bot.

4586 * Complex_Main: Unify and move various concepts from

4587 HOL-Multivariate_Analysis to HOL-Complex_Main.

4589 - Introduce type class (lin)order_topology and

4590 linear_continuum_topology. Allows to generalize theorems about

4591 limits and order. Instances are reals and extended reals.

4593 - continuous and continuos_on from Multivariate_Analysis:

4594 "continuous" is the continuity of a function at a filter. "isCont"

4595 is now an abbrevitation: "isCont x f == continuous (at _) f".

4597 Generalized continuity lemmas from isCont to continuous on an

4598 arbitrary filter.

4600 - compact from Multivariate_Analysis. Use Bolzano's lemma to prove

4601 compactness of closed intervals on reals. Continuous functions

4602 attain infimum and supremum on compact sets. The inverse of a

4603 continuous function is continuous, when the function is continuous

4604 on a compact set.

4606 - connected from Multivariate_Analysis. Use it to prove the

4607 intermediate value theorem. Show connectedness of intervals on

4608 linear_continuum_topology).

4610 - first_countable_topology from Multivariate_Analysis. Is used to

4611 show equivalence of properties on the neighbourhood filter of x and

4612 on all sequences converging to x.

4614 - FDERIV: Definition of has_derivative moved to Deriv.thy. Moved

4615 theorems from Library/FDERIV.thy to Deriv.thy and base the

4616 definition of DERIV on FDERIV. Add variants of DERIV and FDERIV

4617 which are restricted to sets, i.e. to represent derivatives from

4618 left or right.

4620 - Removed the within-filter. It is replaced by the principal filter:

4622 F within X = inf F (principal X)

4624 - Introduce "at x within U" as a single constant, "at x" is now an

4625 abbreviation for "at x within UNIV"

4627 - Introduce named theorem collections tendsto_intros,

4628 continuous_intros, continuous_on_intros and FDERIV_intros. Theorems

4629 in tendsto_intros (or FDERIV_intros) are also available as

4630 tendsto_eq_intros (or FDERIV_eq_intros) where the right-hand side

4631 is replaced by a congruence rule. This allows to apply them as

4632 intro rules and then proving equivalence by the simplifier.

4634 - Restructured theories in HOL-Complex_Main:

4636 + Moved RealDef and RComplete into Real

4638 + Introduced Topological_Spaces and moved theorems about

4639 topological spaces, filters, limits and continuity to it

4641 + Renamed RealVector to Real_Vector_Spaces

4643 + Split Lim, SEQ, Series into Topological_Spaces,

4644 Real_Vector_Spaces, and Limits

4646 + Moved Ln and Log to Transcendental

4648 + Moved theorems about continuity from Deriv to Topological_Spaces

4650 - Remove various auxiliary lemmas.

4652 INCOMPATIBILITY.

4654 * Nitpick:

4655 - Added option "spy".

4656 - Reduce incidence of "too high arity" errors.

4658 * Sledgehammer:

4659 - Renamed option:

4660 isar_shrink ~> isar_compress

4661 INCOMPATIBILITY.

4662 - Added options "isar_try0", "spy".

4663 - Better support for "isar_proofs".

4664 - MaSh has been fined-tuned and now runs as a local server.

4666 * Improved support for ad hoc overloading of constants (see also

4667 isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).

4669 * Library/Polynomial.thy:

4670 - Use lifting for primitive definitions.

4671 - Explicit conversions from and to lists of coefficients, used for

4672 generated code.

4673 - Replaced recursion operator poly_rec by fold_coeffs.

4674 - Prefer pre-existing gcd operation for gcd.

4675 - Fact renames:

4676 poly_eq_iff ~> poly_eq_poly_eq_iff

4677 poly_ext ~> poly_eqI

4678 expand_poly_eq ~> poly_eq_iff

4679 IMCOMPATIBILITY.

4681 * New Library/Simps_Case_Conv.thy: Provides commands simps_of_case and

4682 case_of_simps to convert function definitions between a list of

4683 equations with patterns on the lhs and a single equation with case

4684 expressions on the rhs. See also Ex/Simps_Case_Conv_Examples.thy.

4686 * New Library/FSet.thy: type of finite sets defined as a subtype of

4687 sets defined by Lifting/Transfer.

4689 * Discontinued theory src/HOL/Library/Eval_Witness. INCOMPATIBILITY.

4691 * Consolidation of library theories on product orders:

4693 Product_Lattice ~> Product_Order -- pointwise order on products

4694 Product_ord ~> Product_Lexorder -- lexicographic order on products

4696 INCOMPATIBILITY.

4698 * Imperative-HOL: The MREC combinator is considered legacy and no

4699 longer included by default. INCOMPATIBILITY, use partial_function

4700 instead, or import theory Legacy_Mrec as a fallback.

4702 * HOL-Algebra: Discontinued theories ~~/src/HOL/Algebra/abstract and

4703 ~~/src/HOL/Algebra/poly. Existing theories should be based on

4704 ~~/src/HOL/Library/Polynomial instead. The latter provides

4705 integration with HOL's type classes for rings. INCOMPATIBILITY.

4707 * HOL-BNF:

4708 - Various improvements to BNF-based (co)datatype package, including

4709 new commands "primrec_new", "primcorec", and

4710 "datatype_new_compat", as well as documentation. See

4711 "datatypes.pdf" for details.

4712 - New "coinduction" method to avoid some boilerplate (compared to

4713 coinduct).

4714 - Renamed keywords:

4715 data ~> datatype_new

4716 codata ~> codatatype

4717 bnf_def ~> bnf

4718 - Renamed many generated theorems, including

4719 discs ~> disc

4720 map_comp' ~> map_comp

4721 map_id' ~> map_id

4722 sels ~> sel

4723 set_map' ~> set_map

4724 sets ~> set

4725 IMCOMPATIBILITY.

4728 *** ML ***

4730 * Spec_Check is a Quickcheck tool for Isabelle/ML. The ML function

4731 "check_property" allows to check specifications of the form "ALL x y

4732 z. prop x y z". See also ~~/src/Tools/Spec_Check/ with its

4733 Examples.thy in particular.

4735 * Improved printing of exception trace in Poly/ML 5.5.1, with regular

4736 tracing output in the command transaction context instead of physical

4737 stdout. See also Toplevel.debug, Toplevel.debugging and

4738 ML_Compiler.exn_trace.

4740 * ML type "theory" is now immutable, without any special treatment of

4741 drafts or linear updates (which could lead to "stale theory" errors in

4742 the past). Discontinued obsolete operations like Theory.copy,

4743 Theory.checkpoint, and the auxiliary type theory_ref. Minor

4744 INCOMPATIBILITY.

4746 * More uniform naming of goal functions for skipped proofs:

4748 Skip_Proof.prove ~> Goal.prove_sorry

4749 Skip_Proof.prove_global ~> Goal.prove_sorry_global

4751 Minor INCOMPATIBILITY.

4753 * Simplifier tactics and tools use proper Proof.context instead of

4754 historic type simpset. Old-style declarations like addsimps,

4755 addsimprocs etc. operate directly on Proof.context. Raw type simpset

4756 retains its use as snapshot of the main Simplifier context, using

4757 simpset_of and put_simpset on Proof.context. INCOMPATIBILITY -- port

4758 old tools by making them depend on (ctxt : Proof.context) instead of

4759 (ss : simpset), then turn (simpset_of ctxt) into ctxt.

4761 * Modifiers for classical wrappers (e.g. addWrapper, delWrapper)

4762 operate on Proof.context instead of claset, for uniformity with addIs,

4763 addEs, addDs etc. Note that claset_of and put_claset allow to manage

4764 clasets separately from the context.

4766 * Discontinued obsolete ML antiquotations @{claset} and @{simpset}.

4767 INCOMPATIBILITY, use @{context} instead.

4769 * Antiquotation @{theory_context A} is similar to @{theory A}, but

4770 presents the result as initial Proof.context.

4773 *** System ***

4775 * Discontinued obsolete isabelle usedir, mkdir, make -- superseded by

4776 "isabelle build" in Isabelle2013. INCOMPATIBILITY.

4778 * Discontinued obsolete isabelle-process options -f and -u (former

4779 administrative aliases of option -e). Minor INCOMPATIBILITY.

4781 * Discontinued obsolete isabelle print tool, and PRINT_COMMAND

4782 settings variable.

4784 * Discontinued ISABELLE_DOC_FORMAT settings variable and historic

4785 document formats: dvi.gz, ps, ps.gz -- the default document format is

4786 always pdf.

4788 * Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to

4789 specify global resources of the JVM process run by isabelle build.

4791 * Toplevel executable $ISABELLE_HOME/bin/isabelle_scala_script allows

4792 to run Isabelle/Scala source files as standalone programs.

4794 * Improved "isabelle keywords" tool (for old-style ProofGeneral

4795 keyword tables): use Isabelle/Scala operations, which inspect outer

4796 syntax without requiring to build sessions first.

4798 * Sessions may be organized via 'chapter' specifications in the ROOT

4799 file, which determines a two-level hierarchy of browser info. The old

4800 tree-like organization via implicit sub-session relation (with its

4801 tendency towards erratic fluctuation of URLs) has been discontinued.

4802 The default chapter is called "Unsorted". Potential INCOMPATIBILITY

4803 for HTML presentation of theories.

4807 New in Isabelle2013 (February 2013)

4808 -----------------------------------

4810 *** General ***

4812 * Theorem status about oracles and unfinished/failed future proofs is

4813 no longer printed by default, since it is incompatible with

4814 incremental / parallel checking of the persistent document model. ML

4815 function Thm.peek_status may be used to inspect a snapshot of the

4816 ongoing evaluation process. Note that in batch mode --- notably

4817 isabelle build --- the system ensures that future proofs of all

4818 accessible theorems in the theory context are finished (as before).

4820 * Configuration option show_markup controls direct inlining of markup

4821 into the printed representation of formal entities --- notably type

4822 and sort constraints. This enables Prover IDE users to retrieve that

4823 information via tooltips in the output window, for example.

4825 * Command 'ML_file' evaluates ML text from a file directly within the

4826 theory, without any predeclaration via 'uses' in the theory header.

4828 * Old command 'use' command and corresponding keyword 'uses' in the

4829 theory header are legacy features and will be discontinued soon.

4830 Tools that load their additional source files may imitate the

4831 'ML_file' implementation, such that the system can take care of

4832 dependencies properly.

4834 * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which

4835 is called fastforce / fast_force_tac already since Isabelle2011-1.

4837 * Updated and extended "isar-ref" and "implementation" manual, reduced

4838 remaining material in old "ref" manual.

4840 * Improved support for auxiliary contexts that indicate block structure

4841 for specifications. Nesting of "context fixes ... context assumes ..."

4842 and "class ... context ...".

4844 * Attribute "consumes" allows a negative value as well, which is

4845 interpreted relatively to the total number of premises of the rule in

4846 the target context. This form of declaration is stable when exported

4847 from a nested 'context' with additional assumptions. It is the

4848 preferred form for definitional packages, notably cases/rules produced

4849 in HOL/inductive and HOL/function.

4851 * More informative error messages for Isar proof commands involving

4852 lazy enumerations (method applications etc.).

4854 * Refined 'help' command to retrieve outer syntax commands according

4855 to name patterns (with clickable results).

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

4860 * Parallel terminal proofs ('by') are enabled by default, likewise

4861 proofs that are built into packages like 'datatype', 'function'. This

4862 allows to "run ahead" checking the theory specifications on the

4863 surface, while the prover is still crunching on internal

4864 justifications. Unfinished / cancelled proofs are restarted as

4865 required to complete full proof checking eventually.

4867 * Improved output panel with tooltips, hyperlinks etc. based on the

4868 same Rich_Text_Area as regular Isabelle/jEdit buffers. Activation of

4869 tooltips leads to some window that supports the same recursively,

4870 which can lead to stacks of tooltips as the semantic document content

4871 is explored. ESCAPE closes the whole stack, individual windows may be

4872 closed separately, or detached to become independent jEdit dockables.

4874 * Improved support for commands that produce graph output: the text

4875 message contains a clickable area to open a new instance of the graph

4876 browser on demand.

4878 * More robust incremental parsing of outer syntax (partial comments,

4879 malformed symbols). Changing the balance of open/close quotes and

4880 comment delimiters works more conveniently with unfinished situations

4881 that frequently occur in user interaction.

4883 * More efficient painting and improved reactivity when editing large

4884 files. More scalable management of formal document content.

4886 * Smarter handling of tracing messages: prover process pauses after

4887 certain number of messages per command transaction, with some user

4888 dialog to stop or continue. This avoids swamping the front-end with

4889 potentially infinite message streams.

4891 * More plugin options and preferences, based on Isabelle/Scala. The

4892 jEdit plugin option panel provides access to some Isabelle/Scala

4893 options, including tuning parameters for editor reactivity and color

4894 schemes.

4896 * Dockable window "Symbols" provides some editing support for Isabelle

4897 symbols.

4899 * Dockable window "Monitor" shows ML runtime statistics. Note that

4900 continuous display of the chart slows down the system.

4902 * Improved editing support for control styles: subscript, superscript,

4903 bold, reset of style -- operating on single symbols or text

4904 selections. Cf. keyboard shortcuts C+e DOWN/UP/RIGHT/LEFT.

4906 * Actions isabelle.increase-font-size and isabelle.decrease-font-size

4907 adjust the main text area font size, and its derivatives for output,

4908 tooltips etc. Cf. keyboard shortcuts C-PLUS and C-MINUS, which often

4909 need to be adapted to local keyboard layouts.

4911 * More reactive completion popup by default: use \t (TAB) instead of

4912 \n (NEWLINE) to minimize intrusion into regular flow of editing. See

4913 also "Plugin Options / SideKick / General / Code Completion Options".

4915 * Implicit check and build dialog of the specified logic session

4916 image. For example, HOL, HOLCF, HOL-Nominal can be produced on

4917 demand, without bundling big platform-dependent heap images in the

4918 Isabelle distribution.

4920 * Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates

4921 from Oracle provide better multi-platform experience. This version is

4922 now bundled exclusively with Isabelle.

4925 *** Pure ***

4927 * Code generation for Haskell: restrict unqualified imports from

4928 Haskell Prelude to a small set of fundamental operations.

4930 * Command 'export_code': relative file names are interpreted

4931 relatively to master directory of current theory rather than the

4932 rather arbitrary current working directory. INCOMPATIBILITY.

4934 * Discontinued obsolete attribute "COMP". Potential INCOMPATIBILITY,

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

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

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

4938 with some care where this is really required.

4940 * Command 'typ' supports an additional variant with explicit sort

4941 constraint, to infer and check the most general type conforming to a

4942 given sort. Example (in HOL):

4944 typ "_ * _ * bool * unit" :: finite

4946 * Command 'locale_deps' visualizes all locales and their relations as

4947 a Hasse diagram.

4950 *** HOL ***

4952 * Sledgehammer:

4954 - Added MaSh relevance filter based on machine-learning; see the

4955 Sledgehammer manual for details.

4956 - Polished Isar proofs generated with "isar_proofs" option.

4957 - Rationalized type encodings ("type_enc" option).

4958 - Renamed "kill_provers" subcommand to "kill_all".

4959 - Renamed options:

4960 isar_proof ~> isar_proofs

4961 isar_shrink_factor ~> isar_shrink

4962 max_relevant ~> max_facts

4963 relevance_thresholds ~> fact_thresholds

4965 * Quickcheck: added an optimisation for equality premises. It is

4966 switched on by default, and can be switched off by setting the

4967 configuration quickcheck_optimise_equality to false.

4969 * Quotient: only one quotient can be defined by quotient_type

4970 INCOMPATIBILITY.

4972 * Lifting:

4973 - generation of an abstraction function equation in lift_definition

4974 - quot_del attribute

4975 - renamed no_abs_code -> no_code (INCOMPATIBILITY.)

4977 * Simproc "finite_Collect" rewrites set comprehensions into pointfree

4978 expressions.

4980 * Preprocessing of the code generator rewrites set comprehensions into

4981 pointfree expressions.

4983 * The SMT solver Z3 has now by default a restricted set of directly

4984 supported features. For the full set of features (div/mod, nonlinear

4985 arithmetic, datatypes/records) with potential proof reconstruction

4986 failures, enable the configuration option "z3_with_extensions". Minor

4987 INCOMPATIBILITY.

4989 * Simplified 'typedef' specifications: historical options for implicit

4990 set definition and alternative name have been discontinued. The

4991 former behavior of "typedef (open) t = A" is now the default, but

4992 written just "typedef t = A". INCOMPATIBILITY, need to adapt theories

4993 accordingly.

4995 * Removed constant "chars"; prefer "Enum.enum" on type "char"

4996 directly. INCOMPATIBILITY.

4998 * Moved operation product, sublists and n_lists from theory Enum to

4999 List. INCOMPATIBILITY.

5001 * Theorem UN_o generalized to SUP_comp. INCOMPATIBILITY.

5003 * Class "comm_monoid_diff" formalises properties of bounded

5004 subtraction, with natural numbers and multisets as typical instances.

5006 * Added combinator "Option.these" with type "'a option set => 'a set".

5008 * Theory "Transitive_Closure": renamed lemmas

5010 reflcl_tranclp -> reflclp_tranclp

5011 rtranclp_reflcl -> rtranclp_reflclp

5013 INCOMPATIBILITY.

5015 * Theory "Rings": renamed lemmas (in class semiring)

5017 left_distrib ~> distrib_right

5018 right_distrib ~> distrib_left

5020 INCOMPATIBILITY.

5022 * Generalized the definition of limits:

5024 - Introduced the predicate filterlim (LIM x F. f x :> G) which

5025 expresses that when the input values x converge to F then the

5026 output f x converges to G.

5028 - Added filters for convergence to positive (at_top) and negative

5029 infinity (at_bot).

5031 - Moved infinity in the norm (at_infinity) from

5032 Multivariate_Analysis to Complex_Main.

5034 - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :>

5035 at_top".

5037 INCOMPATIBILITY.

5039 * Theory "Library/Option_ord" provides instantiation of option type to

5040 lattice type classes.

5042 * Theory "Library/Multiset": renamed

5044 constant fold_mset ~> Multiset.fold

5045 fact fold_mset_commute ~> fold_mset_comm

5047 INCOMPATIBILITY.

5049 * Renamed theory Library/List_Prefix to Library/Sublist, with related

5050 changes as follows.

5052 - Renamed constants (and related lemmas)

5054 prefix ~> prefixeq

5055 strict_prefix ~> prefix

5057 - Replaced constant "postfix" by "suffixeq" with swapped argument

5058 order (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped

5059 old infix syntax "xs >>= ys"; use "suffixeq ys xs" instead.

5060 Renamed lemmas accordingly.

5062 - Added constant "list_hembeq" for homeomorphic embedding on

5063 lists. Added abbreviation "sublisteq" for special case

5064 "list_hembeq (op =)".

5066 - Theory Library/Sublist no longer provides "order" and "bot" type

5067 class instances for the prefix order (merely corresponding locale

5068 interpretations). The type class instances are now in theory

5069 Library/Prefix_Order.

5071 - The sublist relation of theory Library/Sublist_Order is now based

5072 on "Sublist.sublisteq". Renamed lemmas accordingly:

5074 le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff

5075 le_list_append_mono ~> Sublist.list_hembeq_append_mono

5076 le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2

5077 le_list_Cons_EX ~> Sublist.list_hembeq_ConsD

5078 le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2'

5079 le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq

5080 le_list_drop_Cons ~> Sublist.sublisteq_Cons'

5081 le_list_drop_many ~> Sublist.sublisteq_drop_many

5082 le_list_filter_left ~> Sublist.sublisteq_filter_left

5083 le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many

5084 le_list_rev_take_iff ~> Sublist.sublisteq_append

5085 le_list_same_length ~> Sublist.sublisteq_same_length

5086 le_list_take_many_iff ~> Sublist.sublisteq_append'

5087 less_eq_list.drop ~> less_eq_list_drop

5088 less_eq_list.induct ~> less_eq_list_induct

5089 not_le_list_length ~> Sublist.not_sublisteq_length

5091 INCOMPATIBILITY.

5093 * New theory Library/Countable_Set.

5095 * Theory Library/Debug and Library/Parallel provide debugging and

5096 parallel execution for code generated towards Isabelle/ML.

5098 * Theory Library/FuncSet: Extended support for Pi and extensional and

5099 introduce the extensional dependent function space "PiE". Replaced

5100 extensional_funcset by an abbreviation, and renamed lemmas from

5101 extensional_funcset to PiE as follows:

5103 extensional_empty ~> PiE_empty

5104 extensional_funcset_empty_domain ~> PiE_empty_domain

5105 extensional_funcset_empty_range ~> PiE_empty_range

5106 extensional_funcset_arb ~> PiE_arb

5107 extensional_funcset_mem ~> PiE_mem

5108 extensional_funcset_extend_domainI ~> PiE_fun_upd

5109 extensional_funcset_restrict_domain ~> fun_upd_in_PiE

5110 extensional_funcset_extend_domain_eq ~> PiE_insert_eq

5111 card_extensional_funcset ~> card_PiE

5112 finite_extensional_funcset ~> finite_PiE

5114 INCOMPATIBILITY.

5116 * Theory Library/FinFun: theory of almost everywhere constant

5117 functions (supersedes the AFP entry "Code Generation for Functions as

5118 Data").

5120 * Theory Library/Phantom: generic phantom type to make a type

5121 parameter appear in a constant's type. This alternative to adding

5122 TYPE('a) as another parameter avoids unnecessary closures in generated

5123 code.

5125 * Theory Library/RBT_Impl: efficient construction of red-black trees

5126 from sorted associative lists. Merging two trees with rbt_union may

5127 return a structurally different tree than before. Potential

5128 INCOMPATIBILITY.

5130 * Theory Library/IArray: immutable arrays with code generation.

5132 * Theory Library/Finite_Lattice: theory of finite lattices.

5134 * HOL/Multivariate_Analysis: replaced

5136 "basis :: 'a::euclidean_space => nat => real"

5137 "\<Chi>\<Chi> :: (nat => real) => 'a::euclidean_space"

5139 on euclidean spaces by using the inner product "_ \<bullet> _" with

5140 vectors from the Basis set: "\<Chi>\<Chi> i. f i" is superseded by

5141 "SUM i : Basis. f i * r i".

5143 With this change the following constants are also changed or removed:

5145 DIM('a) :: nat ~> card (Basis :: 'a set) (is an abbreviation)

5146 a $$ i ~> inner a i (where i : Basis)

5147 cart_base i removed

5148 \<pi>, \<pi>' removed

5150 Theorems about these constants where removed.

5152 Renamed lemmas:

5154 component_le_norm ~> Basis_le_norm

5155 euclidean_eq ~> euclidean_eq_iff

5156 differential_zero_maxmin_component ~> differential_zero_maxmin_cart

5157 euclidean_simps ~> inner_simps

5158 independent_basis ~> independent_Basis

5159 span_basis ~> span_Basis

5160 in_span_basis ~> in_span_Basis

5161 norm_bound_component_le ~> norm_boound_Basis_le

5162 norm_bound_component_lt ~> norm_boound_Basis_lt

5163 component_le_infnorm ~> Basis_le_infnorm

5165 INCOMPATIBILITY.

5167 * HOL/Probability:

5169 - Added simproc "measurable" to automatically prove measurability.

5171 - Added induction rules for sigma sets with disjoint union

5172 (sigma_sets_induct_disjoint) and for Borel-measurable functions

5173 (borel_measurable_induct).

5175 - Added the Daniell-Kolmogorov theorem (the existence the limit of a

5176 projective family).

5178 * HOL/Cardinals: Theories of ordinals and cardinals (supersedes the

5179 AFP entry "Ordinals_and_Cardinals").

5181 * HOL/BNF: New (co)datatype package based on bounded natural functors

5182 with support for mixed, nested recursion and interesting non-free

5183 datatypes.

5185 * HOL/Finite_Set and Relation: added new set and relation operations

5186 expressed by Finite_Set.fold.

5188 * New theory HOL/Library/RBT_Set: implementation of sets by red-black

5189 trees for the code generator.

5191 * HOL/Library/RBT and HOL/Library/Mapping have been converted to

5192 Lifting/Transfer.

5193 possible INCOMPATIBILITY.

5195 * HOL/Set: renamed Set.project -> Set.filter

5196 INCOMPATIBILITY.

5199 *** Document preparation ***

5201 * Dropped legacy antiquotations "term_style" and "thm_style", since

5202 styles may be given as arguments to "term" and "thm" already.

5203 Discontinued legacy styles "prem1" .. "prem19".

5205 * Default LaTeX rendering for \<euro> is now based on eurosym package,

5206 instead of slightly exotic babel/greek.

5208 * Document variant NAME may use different LaTeX entry point

5209 document/root_NAME.tex if that file exists, instead of the common

5210 document/root.tex.

5212 * Simplified custom document/build script, instead of old-style

5213 document/IsaMakefile. Minor INCOMPATIBILITY.

5216 *** ML ***

5218 * The default limit for maximum number of worker threads is now 8,

5219 instead of 4, in correspondence to capabilities of contemporary

5220 hardware and Poly/ML runtime system.

5222 * Type Seq.results and related operations support embedded error

5223 messages within lazy enumerations, and thus allow to provide

5224 informative errors in the absence of any usable results.

5226 * Renamed Position.str_of to Position.here to emphasize that this is a

5227 formal device to inline positions into message text, but not

5228 necessarily printing visible text.

5231 *** System ***

5233 * Advanced support for Isabelle sessions and build management, see

5234 "system" manual for the chapter of that name, especially the "isabelle

5235 build" tool and its examples. The "isabelle mkroot" tool prepares

5236 session root directories for use with "isabelle build", similar to

5237 former "isabelle mkdir" for "isabelle usedir". Note that this affects

5238 document preparation as well. INCOMPATIBILITY, isabelle usedir /

5239 mkdir / make are rendered obsolete.

5241 * Discontinued obsolete Isabelle/build script, it is superseded by the

5242 regular isabelle build tool. For example:

5244 isabelle build -s -b HOL

5246 * Discontinued obsolete "isabelle makeall".

5248 * Discontinued obsolete IsaMakefile and ROOT.ML files from the

5249 Isabelle distribution, except for rudimentary src/HOL/IsaMakefile that

5250 provides some traditional targets that invoke "isabelle build". Note

5251 that this is inefficient! Applications of Isabelle/HOL involving

5252 "isabelle make" should be upgraded to use "isabelle build" directly.

5254 * The "isabelle options" tool prints Isabelle system options, as

5255 required for "isabelle build", for example.

5257 * The "isabelle logo" tool produces EPS and PDF format simultaneously.

5258 Minor INCOMPATIBILITY in command-line options.

5260 * The "isabelle install" tool has now a simpler command-line. Minor

5261 INCOMPATIBILITY.

5263 * The "isabelle components" tool helps to resolve add-on components

5264 that are not bundled, or referenced from a bare-bones repository

5265 version of Isabelle.

5267 * Settings variable ISABELLE_PLATFORM_FAMILY refers to the general

5268 platform family: "linux", "macos", "windows".

5270 * The ML system is configured as regular component, and no longer

5271 picked up from some surrounding directory. Potential INCOMPATIBILITY

5272 for home-made settings.

5274 * Improved ML runtime statistics (heap, threads, future tasks etc.).

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

5277 without exception positions and advanced ML compiler/toplevel

5278 configuration.

5280 * Discontinued special treatment of Proof General -- no longer guess

5281 PROOFGENERAL_HOME based on accidental file-system layout. Minor

5282 INCOMPATIBILITY: provide PROOFGENERAL_HOME and PROOFGENERAL_OPTIONS

5283 settings manually, or use a Proof General version that has been

5284 bundled as Isabelle component.

5288 New in Isabelle2012 (May 2012)

5289 ------------------------------

5291 *** General ***

5293 * Prover IDE (PIDE) improvements:

5295 - more robust Sledgehammer integration (as before the sledgehammer

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

5297 - markup for bound variables

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

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

5300 - improved support for Unicode outside original 16bit range

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

5303 * Forward declaration of outer syntax keywords within the theory

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

5305 commands to be used in the same theory where defined.

5307 * Auxiliary contexts indicate block structure for specifications with

5308 additional parameters and assumptions. Such unnamed contexts may be

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

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

5311 accordingly and applied to the enclosing target context. Example:

5313 context

5314 fixes x y z :: 'a

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

5316 begin

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

5320 end

5322 thm my_trans

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

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

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

5328 Any other local theory specification element works within the "context

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

5331 * Bundled declarations associate attributed fact expressions with a

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

5333 contexts. This allows to manage context extensions casually, without

5334 the logical dependencies of locales and locale interpretation. See

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

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

5338 declaration, and results are standardized before being stored. Thus

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

5340 becomes obsolete. Minor INCOMPATIBILITY, due to potential change of

5341 indices of schematic variables.

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

5344 are now statically evaluated: the resulting theorem is stored instead

5345 of the original expression. INCOMPATIBILITY in rare situations, where

5346 the historic accident of dynamic re-evaluation in interpretations

5347 etc. was exploited.

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

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

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

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

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

5354 of the material of that old tutorial.

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

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

5358 manual.

5361 *** Pure ***

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

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

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

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

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

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

5370 undocumented feature.)

5372 * Sort constraints are now propagated in simultaneous statements, just

5373 like type constraints. INCOMPATIBILITY in rare situations, where

5374 distinct sorts used to be assigned accidentally. For example:

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

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

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

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

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

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

5384 order to accommodate newly introduced premises.)

5386 * Renamed some inner syntax categories:

5388 num ~> num_token

5389 xnum ~> xnum_token

5390 xstr ~> str_token

5392 Minor INCOMPATIBILITY. Note that in practice "num_const" or

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

5394 position information via constraints).

5396 * Simplified configuration options for syntax ambiguity: see

5397 "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref

5398 manual. Minor INCOMPATIBILITY.

5400 * Discontinued configuration option "syntax_positions": atomic terms

5401 in parse trees are always annotated by position constraints.

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

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

5405 Use commands of the generic code generator instead. INCOMPATIBILITY.

5407 * Redundant attribute "code_inline" has been discontinued. Use

5408 "code_unfold" instead. INCOMPATIBILITY.

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

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

5413 definition [code_abbrev]: "f = t"

5415 INCOMPATIBILITY.

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

5418 instead. INCOMPATIBILITY.

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

5421 collection of foundational premises in the context (already marked as

5422 legacy since Isabelle2011).

5425 *** HOL ***

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

5428 Isabelle2008). Definitions mem_def and Collect_def have disappeared.

5429 Non-trivial INCOMPATIBILITY. For developments keeping predicates and

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

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

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

5433 Corresponding proofs in a first step should be pruned from any

5434 tinkering with former theorems mem_def and Collect_def as far as

5435 possible.

5437 For developments which deliberately mix predicates and sets, a

5438 planning step is necessary to determine what should become a predicate

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

5440 Isabelle2011-1 before jumping right into the current release.

5442 * Code generation by default implements sets as container type rather

5443 than predicates. INCOMPATIBILITY.

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

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

5448 represents strictly positive binary numerals, along with functions

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

5450 positive and negated numeric literals, respectively. See also

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

5452 user theories may require adaptations as follows:

5454 - Theorems with number_ring or number_semiring constraints: These

5455 classes are gone; use comm_ring_1 or comm_semiring_1 instead.

5457 - Theories defining numeric types: Remove number, number_semiring,

5458 and number_ring instances. Defer all theorems about numerals until

5459 after classes one and semigroup_add have been instantiated.

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

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

5464 - Theorems about subclasses of semiring_1 or ring_1: These classes

5465 automatically support numerals now, so more simp rules and

5466 simprocs may now apply within the proof.

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

5469 Redefine using other integer operations.

5471 * Transfer: New package intended to generalize the existing

5472 "descending" method and related theorem attributes from the Quotient

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

5474 development will focus on Transfer as an eventual replacement for the

5475 corresponding parts of the Quotient package.)

5477 - transfer_rule attribute: Maintains a collection of transfer rules,

5478 which relate constants at two different types. Transfer rules may

5479 relate different type instances of the same polymorphic constant,

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

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

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

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

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

5487 equivalent subgoal on the corresponding raw types. Constants are

5488 replaced with corresponding ones according to the transfer rules.

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

5490 necessary for variables whose types change, but can be overridden

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

5492 variant transfer' method allows replacing a subgoal with one that

5493 is logically stronger (rather than equivalent).

5495 - relator_eq attribute: Collects identity laws for relators of

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

5497 transfer method uses these lemmas to infer transfer rules for

5498 non-polymorphic constants on the fly.

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

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

5502 constants that already have transfer rules. It should be applied

5503 after unfolding the constant definitions.

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

5506 from type nat to type int.

5508 * Lifting: New package intended to generalize the quotient_definition

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

5511 - lift_definition command: Defines operations on an abstract type in

5512 terms of a corresponding operation on a representation

5513 type. Example syntax:

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

5516 is List.insert

5518 Users must discharge a respectfulness proof obligation when each

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

5520 the proof is discharged automatically.) The obligation is

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

5522 theorem in the standard format and a transfer rule are generated

5523 by the package.

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

5526 corresponding to a datatype invariant, such as dlist),

5527 lift_definition generates a code certificate theorem and sets up

5528 code generation for each constant.

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

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

5532 or a type_definition theorem. The package configures transfer

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

5534 lift_definition command to work with the type.

5536 - Usage examples: See Quotient_Examples/Lift_DList.thy,

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

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

5540 * Quotient package:

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

5543 rep and abs functions, similar to typedef.

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

5546 Transfer packages, as with 'setup_lifting'.

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

5549 respectfulness property at the point where the constant is

5550 defined, similar to lift_definition; INCOMPATIBILITY.

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

5553 accordingly, INCOMPATIBILITY.

5555 * New diagnostic command 'find_unused_assms' to find potentially

5556 superfluous assumptions in theorems using Quickcheck.

5558 * Quickcheck:

5560 - Quickcheck returns variable assignments as counterexamples, which

5561 allows to reveal the underspecification of functions under test.

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

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

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

5566 These counterexample are marked as potentially spurious, as

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

5568 obvious theorem "hd xs = hd xs".

5570 After finding a potentially spurious counterexample, Quickcheck

5571 continues searching for genuine ones.

5573 By default, Quickcheck shows potentially spurious and genuine

5574 counterexamples. The option "genuine_only" sets quickcheck to only

5575 show genuine counterexamples.

5577 - The command 'quickcheck_generator' creates random and exhaustive

5578 value generators for a given type and operations.

5580 It generates values by using the operations as if they were

5581 constructors of that type.

5583 - Support for multisets.

5585 - Added "use_subtype" options.

5587 - Added "quickcheck_locale" configuration to specify how to process

5588 conjectures in a locale context.

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

5591 and affecting 'rat' and 'real'.

5593 * Sledgehammer:

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

5595 paper "More SPASS with Isabelle".

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

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

5598 TFF1), iProver, iProver-Eq.

5599 - Sped up the minimizer.

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

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

5602 - Renamed "sound" option to "strict".

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

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

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

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

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

5612 case distinctions at the same time. E.g.

5614 list.exhaust [case_product nat.exhaust]

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

5617 a list and a nat.

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

5620 eventually_elim* rules. Supports structured proofs.

5622 * Typedef with implicit set definition is considered legacy. Use

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

5624 default.

5626 * Record: code generation can be switched off manually with

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

5630 * Datatype: type parameters allow explicit sort constraints.

5632 * Concrete syntax for case expressions includes constraints for source

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

5634 INCOMPATIBILITY for old-style syntax translations that augment the

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

5636 one_case.

5638 * Clarified attribute "mono_set": pure declaration without modifying

5639 the result of the fact expression.

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

5642 and predicates. Added powers of predicate relations. Consolidation

5643 of some relation theorems:

5645 converse_def ~> converse_unfold

5646 rel_comp_def ~> relcomp_unfold

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

5648 transp_def ~> transp_trans

5649 Domain_def ~> Domain_unfold

5650 Range_def ~> Domain_converse [symmetric]

5652 Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2.

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

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

5657 INCOMPATIBILITY.

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

5660 to match the constant's name:

5662 rel_pow_1 ~> relpow_1

5663 rel_pow_0_I ~> relpow_0_I

5664 rel_pow_Suc_I ~> relpow_Suc_I

5665 rel_pow_Suc_I2 ~> relpow_Suc_I2

5666 rel_pow_0_E ~> relpow_0_E

5667 rel_pow_Suc_E ~> relpow_Suc_E

5668 rel_pow_E ~> relpow_E

5669 rel_pow_Suc_D2 ~> relpow_Suc_D2

5670 rel_pow_Suc_E2 ~> relpow_Suc_E2

5671 rel_pow_Suc_D2' ~> relpow_Suc_D2'

5672 rel_pow_E2 ~> relpow_E2

5673 rel_pow_add ~> relpow_add

5674 rel_pow_commute ~> relpow

5675 rel_pow_empty ~> relpow_empty:

5676 rtrancl_imp_UN_rel_pow ~> rtrancl_imp_UN_relpow

5677 rel_pow_imp_rtrancl ~> relpow_imp_rtrancl

5678 rtrancl_is_UN_rel_pow ~> rtrancl_is_UN_relpow

5679 rtrancl_imp_rel_pow ~> rtrancl_imp_relpow

5680 rel_pow_fun_conv ~> relpow_fun_conv

5681 rel_pow_finite_bounded1 ~> relpow_finite_bounded1

5682 rel_pow_finite_bounded ~> relpow_finite_bounded

5683 rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow

5684 trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow

5685 single_valued_rel_pow ~> single_valued_relpow

5687 INCOMPATIBILITY.

5689 * Theory Relation: Consolidated constant name for relation composition

5690 and corresponding theorem names:

5692 - Renamed constant rel_comp to relcomp.

5694 - Dropped abbreviation pred_comp. Use relcompp instead.

5696 - Renamed theorems:

5698 rel_compI ~> relcompI

5699 rel_compEpair ~> relcompEpair

5700 rel_compE ~> relcompE

5701 pred_comp_rel_comp_eq ~> relcompp_relcomp_eq

5702 rel_comp_empty1 ~> relcomp_empty1

5703 rel_comp_mono ~> relcomp_mono

5704 rel_comp_subset_Sigma ~> relcomp_subset_Sigma

5705 rel_comp_distrib ~> relcomp_distrib

5706 rel_comp_distrib2 ~> relcomp_distrib2

5707 rel_comp_UNION_distrib ~> relcomp_UNION_distrib

5708 rel_comp_UNION_distrib2 ~> relcomp_UNION_distrib2

5709 single_valued_rel_comp ~> single_valued_relcomp

5710 rel_comp_def ~> relcomp_unfold

5711 converse_rel_comp ~> converse_relcomp

5712 pred_compI ~> relcomppI

5713 pred_compE ~> relcomppE

5714 pred_comp_bot1 ~> relcompp_bot1

5715 pred_comp_bot2 ~> relcompp_bot2

5716 transp_pred_comp_less_eq ~> transp_relcompp_less_eq

5717 pred_comp_mono ~> relcompp_mono

5718 pred_comp_distrib ~> relcompp_distrib

5719 pred_comp_distrib2 ~> relcompp_distrib2

5720 converse_pred_comp ~> converse_relcompp

5722 finite_rel_comp ~> finite_relcomp

5724 set_rel_comp ~> set_relcomp

5726 INCOMPATIBILITY.

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

5729 INCOMPATIBILITY, use the corresponding generic theorems instead.

5731 DIVISION_BY_ZERO ~> div_by_0, mod_by_0

5732 zdiv_self ~> div_self

5733 zmod_self ~> mod_self

5734 zdiv_zero ~> div_0

5735 zmod_zero ~> mod_0

5736 zdiv_zmod_equality ~> div_mod_equality2

5737 zdiv_zmod_equality2 ~> div_mod_equality

5738 zmod_zdiv_trivial ~> mod_div_trivial

5739 zdiv_zminus_zminus ~> div_minus_minus

5740 zmod_zminus_zminus ~> mod_minus_minus

5741 zdiv_zminus2 ~> div_minus_right

5742 zmod_zminus2 ~> mod_minus_right

5743 zdiv_minus1_right ~> div_minus1_right

5744 zmod_minus1_right ~> mod_minus1_right

5745 zdvd_mult_div_cancel ~> dvd_mult_div_cancel

5746 zmod_zmult1_eq ~> mod_mult_right_eq

5747 zpower_zmod ~> power_mod

5748 zdvd_zmod ~> dvd_mod

5749 zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd

5750 mod_mult_distrib ~> mult_mod_left

5751 mod_mult_distrib2 ~> mult_mod_right

5753 * Removed redundant theorems nat_mult_2 and nat_mult_2_right; use

5754 generic mult_2 and mult_2_right instead. INCOMPATIBILITY.

5756 * Finite_Set.fold now qualified. INCOMPATIBILITY.

5758 * Consolidated theorem names concerning fold combinators:

5760 inf_INFI_fold_inf ~> inf_INF_fold_inf

5761 sup_SUPR_fold_sup ~> sup_SUP_fold_sup

5762 INFI_fold_inf ~> INF_fold_inf

5763 SUPR_fold_sup ~> SUP_fold_sup

5764 union_set ~> union_set_fold

5765 minus_set ~> minus_set_fold

5766 INFI_set_fold ~> INF_set_fold

5767 SUPR_set_fold ~> SUP_set_fold

5768 INF_code ~> INF_set_foldr

5769 SUP_code ~> SUP_set_foldr

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

5771 foldr_fold_rev ~> foldr_conv_fold

5772 foldl_fold ~> foldl_conv_fold

5773 foldr_foldr ~> foldr_conv_foldl

5774 foldl_foldr ~> foldl_conv_foldr

5775 fold_set_remdups ~> fold_set_fold_remdups

5776 fold_set ~> fold_set_fold

5777 fold1_set ~> fold1_set_fold

5779 INCOMPATIBILITY.

5781 * Dropped rarely useful theorems concerning fold combinators:

5782 foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant,

5783 rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,

5784 concat_conv_foldl, foldl_weak_invariant, foldl_invariant,

5785 foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,

5786 listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc,

5787 foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv.

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

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

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

5791 unfolding "foldr_conv_fold" and "foldl_conv_fold".

5793 * Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr,

5794 inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr,

5795 Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr,

5796 INF_set_foldr, SUP_set_foldr. INCOMPATIBILITY. Prefer corresponding

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

5798 fold_conv_foldr and fold_rev.

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

5801 through option types.

5803 * "Transitive_Closure.ntrancl": bounded transitive closure on

5804 relations.

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

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

5809 INCOMPATIBILITY, use the corresponding generic theorems instead.

5811 zminus_zminus ~> minus_minus

5812 zminus_0 ~> minus_zero

5813 zminus_zadd_distrib ~> minus_add_distrib

5814 zadd_commute ~> add_commute

5815 zadd_assoc ~> add_assoc

5816 zadd_left_commute ~> add_left_commute

5817 zadd_ac ~> add_ac

5818 zmult_ac ~> mult_ac

5819 zadd_0 ~> add_0_left

5820 zadd_0_right ~> add_0_right

5821 zadd_zminus_inverse2 ~> left_minus

5822 zmult_zminus ~> mult_minus_left

5823 zmult_commute ~> mult_commute

5824 zmult_assoc ~> mult_assoc

5825 zadd_zmult_distrib ~> left_distrib

5826 zadd_zmult_distrib2 ~> right_distrib

5827 zdiff_zmult_distrib ~> left_diff_distrib

5828 zdiff_zmult_distrib2 ~> right_diff_distrib

5829 zmult_1 ~> mult_1_left

5830 zmult_1_right ~> mult_1_right

5831 zle_refl ~> order_refl

5832 zle_trans ~> order_trans

5833 zle_antisym ~> order_antisym

5834 zle_linear ~> linorder_linear

5835 zless_linear ~> linorder_less_linear

5836 zadd_left_mono ~> add_left_mono

5837 zadd_strict_right_mono ~> add_strict_right_mono

5838 zadd_zless_mono ~> add_less_le_mono

5839 int_0_less_1 ~> zero_less_one

5840 int_0_neq_1 ~> zero_neq_one

5841 zless_le ~> less_le

5842 zpower_zadd_distrib ~> power_add

5843 zero_less_zpower_abs_iff ~> zero_less_power_abs_iff

5844 zero_le_zpower_abs ~> zero_le_power_abs

5846 * Theory Deriv: Renamed

5848 DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing

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

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

5853 are expressed via type classes again. The special syntax

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

5855 setsum_set, which is now subsumed by Big_Operators.setsum.

5856 INCOMPATIBILITY.

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

5859 use theory HOL/Library/Nat_Bijection instead.

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

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

5863 operations and lemmas have been prefixed by rbt_. INCOMPATIBILITY for

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

5865 follows:

5867 Operations:

5868 bulkload -> rbt_bulkload

5869 del_from_left -> rbt_del_from_left

5870 del_from_right -> rbt_del_from_right

5871 del -> rbt_del

5872 delete -> rbt_delete

5873 ins -> rbt_ins

5874 insert -> rbt_insert

5875 insertw -> rbt_insert_with

5876 insert_with_key -> rbt_insert_with_key

5877 map_entry -> rbt_map_entry

5878 lookup -> rbt_lookup

5879 sorted -> rbt_sorted

5880 tree_greater -> rbt_greater

5881 tree_less -> rbt_less

5882 tree_less_symbol -> rbt_less_symbol

5883 union -> rbt_union

5884 union_with -> rbt_union_with

5885 union_with_key -> rbt_union_with_key

5887 Lemmas:

5888 balance_left_sorted -> balance_left_rbt_sorted

5889 balance_left_tree_greater -> balance_left_rbt_greater

5890 balance_left_tree_less -> balance_left_rbt_less

5891 balance_right_sorted -> balance_right_rbt_sorted

5892 balance_right_tree_greater -> balance_right_rbt_greater

5893 balance_right_tree_less -> balance_right_rbt_less

5894 balance_sorted -> balance_rbt_sorted

5895 balance_tree_greater -> balance_rbt_greater

5896 balance_tree_less -> balance_rbt_less

5897 bulkload_is_rbt -> rbt_bulkload_is_rbt

5898 combine_sorted -> combine_rbt_sorted

5899 combine_tree_greater -> combine_rbt_greater

5900 combine_tree_less -> combine_rbt_less

5901 delete_in_tree -> rbt_delete_in_tree

5902 delete_is_rbt -> rbt_delete_is_rbt

5903 del_from_left_tree_greater -> rbt_del_from_left_rbt_greater

5904 del_from_left_tree_less -> rbt_del_from_left_rbt_less

5905 del_from_right_tree_greater -> rbt_del_from_right_rbt_greater

5906 del_from_right_tree_less -> rbt_del_from_right_rbt_less

5907 del_in_tree -> rbt_del_in_tree

5908 del_inv1_inv2 -> rbt_del_inv1_inv2

5909 del_sorted -> rbt_del_rbt_sorted

5910 del_tree_greater -> rbt_del_rbt_greater

5911 del_tree_less -> rbt_del_rbt_less

5912 dom_lookup_Branch -> dom_rbt_lookup_Branch

5913 entries_lookup -> entries_rbt_lookup

5914 finite_dom_lookup -> finite_dom_rbt_lookup

5915 insert_sorted -> rbt_insert_rbt_sorted

5916 insertw_is_rbt -> rbt_insertw_is_rbt

5917 insertwk_is_rbt -> rbt_insertwk_is_rbt

5918 insertwk_sorted -> rbt_insertwk_rbt_sorted

5919 insertw_sorted -> rbt_insertw_rbt_sorted

5920 ins_sorted -> ins_rbt_sorted

5921 ins_tree_greater -> ins_rbt_greater

5922 ins_tree_less -> ins_rbt_less

5923 is_rbt_sorted -> is_rbt_rbt_sorted

5924 lookup_balance -> rbt_lookup_balance

5925 lookup_bulkload -> rbt_lookup_rbt_bulkload

5926 lookup_delete -> rbt_lookup_rbt_delete

5927 lookup_Empty -> rbt_lookup_Empty

5928 lookup_from_in_tree -> rbt_lookup_from_in_tree

5929 lookup_in_tree -> rbt_lookup_in_tree

5930 lookup_ins -> rbt_lookup_ins

5931 lookup_insert -> rbt_lookup_rbt_insert

5932 lookup_insertw -> rbt_lookup_rbt_insertw

5933 lookup_insertwk -> rbt_lookup_rbt_insertwk

5934 lookup_keys -> rbt_lookup_keys

5935 lookup_map -> rbt_lookup_map

5936 lookup_map_entry -> rbt_lookup_rbt_map_entry

5937 lookup_tree_greater -> rbt_lookup_rbt_greater

5938 lookup_tree_less -> rbt_lookup_rbt_less

5939 lookup_union -> rbt_lookup_rbt_union

5940 map_entry_color_of -> rbt_map_entry_color_of

5941 map_entry_inv1 -> rbt_map_entry_inv1

5942 map_entry_inv2 -> rbt_map_entry_inv2

5943 map_entry_is_rbt -> rbt_map_entry_is_rbt

5944 map_entry_sorted -> rbt_map_entry_rbt_sorted

5945 map_entry_tree_greater -> rbt_map_entry_rbt_greater

5946 map_entry_tree_less -> rbt_map_entry_rbt_less

5947 map_tree_greater -> map_rbt_greater

5948 map_tree_less -> map_rbt_less

5949 map_sorted -> map_rbt_sorted

5950 paint_sorted -> paint_rbt_sorted

5951 paint_lookup -> paint_rbt_lookup

5952 paint_tree_greater -> paint_rbt_greater

5953 paint_tree_less -> paint_rbt_less

5954 sorted_entries -> rbt_sorted_entries

5955 tree_greater_eq_trans -> rbt_greater_eq_trans

5956 tree_greater_nit -> rbt_greater_nit

5957 tree_greater_prop -> rbt_greater_prop

5958 tree_greater_simps -> rbt_greater_simps

5959 tree_greater_trans -> rbt_greater_trans

5960 tree_less_eq_trans -> rbt_less_eq_trans

5961 tree_less_nit -> rbt_less_nit

5962 tree_less_prop -> rbt_less_prop

5963 tree_less_simps -> rbt_less_simps

5964 tree_less_trans -> rbt_less_trans

5965 tree_ord_props -> rbt_ord_props

5966 union_Branch -> rbt_union_Branch

5967 union_is_rbt -> rbt_union_is_rbt

5968 unionw_is_rbt -> rbt_unionw_is_rbt

5969 unionwk_is_rbt -> rbt_unionwk_is_rbt

5970 unionwk_sorted -> rbt_unionwk_rbt_sorted

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

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

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

5976 Changed Operations:

5977 float_abs -> abs

5978 float_nprt -> nprt

5979 float_pprt -> pprt

5980 pow2 -> use powr

5981 round_down -> float_round_down

5982 round_up -> float_round_up

5983 scale -> exponent

5985 Removed Operations:

5986 ceiling_fl, lb_mult, lb_mod, ub_mult, ub_mod

5988 Renamed Lemmas:

5989 abs_float_def -> Float.compute_float_abs

5990 bitlen_ge0 -> bitlen_nonneg

5991 bitlen.simps -> Float.compute_bitlen

5992 float_components -> Float_mantissa_exponent

5993 float_divl.simps -> Float.compute_float_divl

5994 float_divr.simps -> Float.compute_float_divr

5995 float_eq_odd -> mult_powr_eq_mult_powr_iff

5996 float_power -> real_of_float_power

5997 lapprox_posrat_def -> Float.compute_lapprox_posrat

5998 lapprox_rat.simps -> Float.compute_lapprox_rat

5999 le_float_def' -> Float.compute_float_le

6000 le_float_def -> less_eq_float.rep_eq

6001 less_float_def' -> Float.compute_float_less

6002 less_float_def -> less_float.rep_eq

6003 normfloat_def -> Float.compute_normfloat

6004 normfloat_imp_odd_or_zero -> mantissa_not_dvd and mantissa_noteq_0

6005 normfloat -> normfloat_def

6006 normfloat_unique -> use normfloat_def

6007 number_of_float_Float -> Float.compute_float_numeral, Float.compute_float_neg_numeral

6008 one_float_def -> Float.compute_float_one

6009 plus_float_def -> Float.compute_float_plus

6010 rapprox_posrat_def -> Float.compute_rapprox_posrat

6011 rapprox_rat.simps -> Float.compute_rapprox_rat

6012 real_of_float_0 -> zero_float.rep_eq

6013 real_of_float_1 -> one_float.rep_eq

6014 real_of_float_abs -> abs_float.rep_eq

6015 real_of_float_add -> plus_float.rep_eq

6016 real_of_float_minus -> uminus_float.rep_eq

6017 real_of_float_mult -> times_float.rep_eq

6018 real_of_float_simp -> Float.rep_eq

6019 real_of_float_sub -> minus_float.rep_eq

6020 round_down.simps -> Float.compute_float_round_down

6021 round_up.simps -> Float.compute_float_round_up

6022 times_float_def -> Float.compute_float_times

6023 uminus_float_def -> Float.compute_float_uminus

6024 zero_float_def -> Float.compute_float_zero

6026 Lemmas not necessary anymore, use the transfer method:

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

6028 float_divr, float_le_simp, float_less1_mantissa_bound,

6029 float_less_simp, float_less_zero, float_le_zero,

6030 float_pos_less1_e_neg, float_pos_m_pos, float_split, float_split2,

6031 floor_pos_exp, lapprox_posrat, lapprox_posrat_bottom, lapprox_rat,

6032 lapprox_rat_bottom, normalized_float, rapprox_posrat,

6033 rapprox_posrat_le1, rapprox_rat, real_of_float_ge0_exp,

6034 real_of_float_neg_exp, real_of_float_nge0_exp, round_down floor_fl,

6035 round_up, zero_le_float, zero_less_float

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

6038 association lists with distinct keys.

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

6041 annotated commands.

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

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

6045 available as an external component. Discontinued old (and mostly

6046 dead) Importer for HOL4 and HOL Light. INCOMPATIBILITY.

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

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

6050 instead.

6052 word_sub_alt ~> word_sub_wi

6053 word_add_alt ~> word_add_def

6054 word_mult_alt ~> word_mult_def

6055 word_minus_alt ~> word_minus_def

6056 word_0_alt ~> word_0_wi

6057 word_1_alt ~> word_1_wi

6058 word_add_0 ~> add_0_left

6059 word_add_0_right ~> add_0_right

6060 word_mult_1 ~> mult_1_left

6061 word_mult_1_right ~> mult_1_right

6062 word_add_commute ~> add_commute

6063 word_add_assoc ~> add_assoc

6064 word_add_left_commute ~> add_left_commute

6065 word_mult_commute ~> mult_commute

6066 word_mult_assoc ~> mult_assoc

6067 word_mult_left_commute ~> mult_left_commute

6068 word_left_distrib ~> left_distrib

6069 word_right_distrib ~> right_distrib

6070 word_left_minus ~> left_minus

6071 word_diff_0_right ~> diff_0_right

6072 word_diff_self ~> diff_self

6073 word_sub_def ~> diff_minus

6074 word_diff_minus ~> diff_minus

6075 word_add_ac ~> add_ac

6076 word_mult_ac ~> mult_ac

6077 word_plus_ac0 ~> add_0_left add_0_right add_ac

6078 word_times_ac1 ~> mult_1_left mult_1_right mult_ac

6079 word_order_trans ~> order_trans

6080 word_order_refl ~> order_refl

6081 word_order_antisym ~> order_antisym

6082 word_order_linear ~> linorder_linear

6083 lenw1_zero_neq_one ~> zero_neq_one

6084 word_number_of_eq ~> number_of_eq

6085 word_of_int_add_hom ~> wi_hom_add

6086 word_of_int_sub_hom ~> wi_hom_sub

6087 word_of_int_mult_hom ~> wi_hom_mult

6088 word_of_int_minus_hom ~> wi_hom_neg

6089 word_of_int_succ_hom ~> wi_hom_succ

6090 word_of_int_pred_hom ~> wi_hom_pred

6091 word_of_int_0_hom ~> word_0_wi

6092 word_of_int_1_hom ~> word_1_wi

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

6095 machine word equalities and inequalities into logical circuits,

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

6097 multiplication, shifting by constants, bitwise operators and numeric

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

6099 many standard word identities outright and converts more into first

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

6101 HOL/Word/Examples/WordExamples.thy.

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

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

6105 measure_space. The locales based on subset_class now have two

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

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

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

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

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

6111 Measure space constructions for distributions and densities now got

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

6113 describe measure spaces with a finite space, the measure count_space

6114 and point_measure is introduced. INCOMPATIBILITY.

6116 Renamed constants:

6117 measure -> emeasure

6118 finite_measure.\<mu>' -> measure

6119 product_algebra_generator -> prod_algebra

6120 product_prob_space.emb -> prod_emb

6121 product_prob_space.infprod_algebra -> PiM

6123 Removed locales:

6124 completeable_measure_space

6125 finite_measure_space

6126 finite_prob_space

6127 finite_product_finite_prob_space

6128 finite_product_sigma_algebra

6129 finite_sigma_algebra

6130 measure_space

6131 pair_finite_prob_space

6132 pair_finite_sigma_algebra

6133 pair_finite_space

6134 pair_sigma_algebra

6135 product_sigma_algebra

6137 Removed constants:

6138 conditional_space

6139 distribution -> use distr measure, or distributed predicate

6140 image_space

6141 joint_distribution -> use distr measure, or distributed predicate

6142 pair_measure_generator

6143 product_prob_space.infprod_algebra -> use PiM

6144 subvimage

6146 Replacement theorems:

6147 finite_additivity_sufficient -> ring_of_sets.countably_additiveI_finite

6148 finite_measure.empty_measure -> measure_empty

6149 finite_measure.finite_continuity_from_above -> finite_measure.finite_Lim_measure_decseq

6150 finite_measure.finite_continuity_from_below -> finite_measure.finite_Lim_measure_incseq

6151 finite_measure.finite_measure_countably_subadditive -> finite_measure.finite_measure_subadditive_countably

6152 finite_measure.finite_measure_eq -> finite_measure.emeasure_eq_measure

6153 finite_measure.finite_measure -> finite_measure.emeasure_finite

6154 finite_measure.finite_measure_finite_singleton -> finite_measure.finite_measure_eq_setsum_singleton

6155 finite_measure.positive_measure' -> measure_nonneg

6156 finite_measure.real_measure -> finite_measure.emeasure_real

6157 finite_product_prob_space.finite_measure_times -> finite_product_prob_space.finite_measure_PiM_emb

6158 finite_product_sigma_algebra.in_P -> sets_PiM_I_finite

6159 finite_product_sigma_algebra.P_empty -> space_PiM_empty, sets_PiM_empty

6160 information_space.conditional_entropy_eq -> information_space.conditional_entropy_simple_distributed

6161 information_space.conditional_entropy_positive -> information_space.conditional_entropy_nonneg_simple

6162 information_space.conditional_mutual_information_eq_mutual_information -> information_space.conditional_mutual_information_eq_mutual_information_simple

6163 information_space.conditional_mutual_information_generic_positive -> information_space.conditional_mutual_information_nonneg_simple

6164 information_space.conditional_mutual_information_positive -> information_space.conditional_mutual_information_nonneg_simple

6165 information_space.entropy_commute -> information_space.entropy_commute_simple

6166 information_space.entropy_eq -> information_space.entropy_simple_distributed

6167 information_space.entropy_generic_eq -> information_space.entropy_simple_distributed

6168 information_space.entropy_positive -> information_space.entropy_nonneg_simple

6169 information_space.entropy_uniform_max -> information_space.entropy_uniform

6170 information_space.KL_eq_0_imp -> information_space.KL_eq_0_iff_eq

6171 information_space.KL_eq_0 -> information_space.KL_same_eq_0

6172 information_space.KL_ge_0 -> information_space.KL_nonneg

6173 information_space.mutual_information_eq -> information_space.mutual_information_simple_distributed

6174 information_space.mutual_information_positive -> information_space.mutual_information_nonneg_simple

6175 Int_stable_cuboids -> Int_stable_atLeastAtMost

6176 Int_stable_product_algebra_generator -> positive_integral

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

6178 measure_space.additive -> emeasure_additive

6179 measure_space.AE_iff_null_set -> AE_iff_null

6180 measure_space.almost_everywhere_def -> eventually_ae_filter

6181 measure_space.almost_everywhere_vimage -> AE_distrD

6182 measure_space.continuity_from_above -> INF_emeasure_decseq

6183 measure_space.continuity_from_above_Lim -> Lim_emeasure_decseq

6184 measure_space.continuity_from_below_Lim -> Lim_emeasure_incseq

6185 measure_space.continuity_from_below -> SUP_emeasure_incseq

6186 measure_space_density -> emeasure_density

6187 measure_space.density_is_absolutely_continuous -> absolutely_continuousI_density

6188 measure_space.integrable_vimage -> integrable_distr

6189 measure_space.integral_translated_density -> integral_density

6190 measure_space.integral_vimage -> integral_distr

6191 measure_space.measure_additive -> plus_emeasure

6192 measure_space.measure_compl -> emeasure_compl

6193 measure_space.measure_countable_increasing -> emeasure_countable_increasing

6194 measure_space.measure_countably_subadditive -> emeasure_subadditive_countably

6195 measure_space.measure_decseq -> decseq_emeasure

6196 measure_space.measure_Diff -> emeasure_Diff

6197 measure_space.measure_Diff_null_set -> emeasure_Diff_null_set

6198 measure_space.measure_eq_0 -> emeasure_eq_0

6199 measure_space.measure_finitely_subadditive -> emeasure_subadditive_finite

6200 measure_space.measure_finite_singleton -> emeasure_eq_setsum_singleton

6201 measure_space.measure_incseq -> incseq_emeasure

6202 measure_space.measure_insert -> emeasure_insert

6203 measure_space.measure_mono -> emeasure_mono

6204 measure_space.measure_not_negative -> emeasure_not_MInf

6205 measure_space.measure_preserving_Int_stable -> measure_eqI_generator_eq

6206 measure_space.measure_setsum -> setsum_emeasure

6207 measure_space.measure_setsum_split -> setsum_emeasure_cover

6208 measure_space.measure_space_vimage -> emeasure_distr

6209 measure_space.measure_subadditive_finite -> emeasure_subadditive_finite

6210 measure_space.measure_subadditive -> subadditive

6211 measure_space.measure_top -> emeasure_space

6212 measure_space.measure_UN_eq_0 -> emeasure_UN_eq_0

6213 measure_space.measure_Un_null_set -> emeasure_Un_null_set

6214 measure_space.positive_integral_translated_density -> positive_integral_density

6215 measure_space.positive_integral_vimage -> positive_integral_distr

6216 measure_space.real_continuity_from_above -> Lim_measure_decseq

6217 measure_space.real_continuity_from_below -> Lim_measure_incseq

6218 measure_space.real_measure_countably_subadditive -> measure_subadditive_countably

6219 measure_space.real_measure_Diff -> measure_Diff

6220 measure_space.real_measure_finite_Union -> measure_finite_Union

6221 measure_space.real_measure_setsum_singleton -> measure_eq_setsum_singleton

6222 measure_space.real_measure_subadditive -> measure_subadditive

6223 measure_space.real_measure_Union -> measure_Union

6224 measure_space.real_measure_UNION -> measure_UNION

6225 measure_space.simple_function_vimage -> simple_function_comp

6226 measure_space.simple_integral_vimage -> simple_integral_distr

6227 measure_space.simple_integral_vimage -> simple_integral_distr

6228 measure_unique_Int_stable -> measure_eqI_generator_eq

6229 measure_unique_Int_stable_vimage -> measure_eqI_generator_eq

6230 pair_sigma_algebra.measurable_cut_fst -> sets_Pair1

6231 pair_sigma_algebra.measurable_cut_snd -> sets_Pair2

6232 pair_sigma_algebra.measurable_pair_image_fst -> measurable_Pair1

6233 pair_sigma_algebra.measurable_pair_image_snd -> measurable_Pair2

6234 pair_sigma_algebra.measurable_product_swap -> measurable_pair_swap_iff

6235 pair_sigma_algebra.pair_sigma_algebra_measurable -> measurable_pair_swap

6236 pair_sigma_algebra.pair_sigma_algebra_swap_measurable -> measurable_pair_swap'

6237 pair_sigma_algebra.sets_swap -> sets_pair_swap

6238 pair_sigma_finite.measure_cut_measurable_fst -> pair_sigma_finite.measurable_emeasure_Pair1

6239 pair_sigma_finite.measure_cut_measurable_snd -> pair_sigma_finite.measurable_emeasure_Pair2

6240 pair_sigma_finite.measure_preserving_swap -> pair_sigma_finite.distr_pair_swap

6241 pair_sigma_finite.pair_measure_alt2 -> pair_sigma_finite.emeasure_pair_measure_alt2

6242 pair_sigma_finite.pair_measure_alt -> pair_sigma_finite.emeasure_pair_measure_alt

6243 pair_sigma_finite.pair_measure_times -> pair_sigma_finite.emeasure_pair_measure_Times

6244 prob_space.indep_distribution_eq_measure -> prob_space.indep_vars_iff_distr_eq_PiM

6245 prob_space.indep_var_distributionD -> prob_space.indep_var_distribution_eq

6246 prob_space.measure_space_1 -> prob_space.emeasure_space_1

6247 prob_space.prob_space_vimage -> prob_space_distr

6248 prob_space.random_variable_restrict -> measurable_restrict

6249 prob_space_unique_Int_stable -> measure_eqI_prob_space

6250 product_algebraE -> prod_algebraE_all

6251 product_algebra_generator_der -> prod_algebra_eq_finite

6252 product_algebra_generator_into_space -> prod_algebra_sets_into_space

6253 product_algebraI -> sets_PiM_I_finite

6254 product_measure_exists -> product_sigma_finite.sigma_finite

6255 product_prob_space.finite_index_eq_finite_product -> product_prob_space.sets_PiM_generator

6256 product_prob_space.finite_measure_infprod_emb_Pi -&g