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

NEWS

author | blanchet |

Fri Jan 31 10:23:32 2014 +0100 (2014-01-31) | |

changeset 55198 | 7a538e58b64e |

parent 55183 | 17ec4a29ef71 |

child 55289 | 30d874dc7000 |

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

tuned ML file name

1 Isabelle NEWS -- history user-relevant changes

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

4 New in this Isabelle version

5 ----------------------------

7 *** General ***

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

10 which results in an active hyperlink within the text.

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

13 not check existence within the file-system.

15 * Discontinued legacy_isub_isup, which was a temporary Isabelle/ML

16 workaround in Isabelle2013-1. The prover process no longer accepts

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

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

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

21 string token. Minor INCOMPATIBILITY.

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

24 arbitrary nesting, and without escapes of quotes etc.

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

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

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

32 * Document panel: simplied interaction where every single mouse click

33 (re)opens document via desktop environment or as jEdit buffer.

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

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

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

38 "isabelle jedit -m MODE".

41 *** Pure ***

43 * Attributes "where" and "of" allow an optional context of local

44 variables ('for' declaration): these variables become schematic in the

45 instantiated theorem.

47 * Obsolete attribute "standard" has been discontinued (legacy since

48 Isabelle2012). Potential INCOMPATIBILITY, use explicit 'for' context

49 where instantiations with schematic variables are intended (for

50 declaration commands like 'lemmas' or attributes like "of"). The

51 following temporary definition may help to port old applications:

53 attribute_setup standard =

54 "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"

56 * More thorough check of proof context for goal statements and

57 attributed fact expressions (concerning background theory, declared

58 hyps). Potential INCOMPATIBILITY, tools need to observe standard

59 context discipline. See also Assumption.add_assumes and the more

60 primitive Thm.assume_hyps.

62 * Inner syntax token language allows regular quoted strings "..."

63 (only makes sense in practice, if outer syntax is delimited

64 differently).

67 *** HOL ***

69 * Simproc "finite_Collect" is no longer enabled by default, due to

70 spurious crashes and other surprises. Potential INCOMPATIBILITY.

72 * Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL".

73 The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",

74 "primrec_new", "primcorec", and "primcorecursive" command are now part of

75 "Main".

76 INCOMPATIBILITY.

77 Theory renamings:

78 FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)

79 Library/Wfrec.thy ~> Wfrec.thy

80 Library/Zorn.thy ~> Zorn.thy

81 Cardinals/Order_Relation.thy ~> Order_Relation.thy

82 Library/Order_Union.thy ~> Cardinals/Order_Union.thy

83 Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy

84 Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy

85 Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy

86 Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy

87 Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy

88 BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy

89 BNF/Basic_BNFs.thy ~> Basic_BNFs.thy

90 BNF/BNF_Comp.thy ~> BNF_Comp.thy

91 BNF/BNF_Def.thy ~> BNF_Def.thy

92 BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy

93 BNF/BNF_GFP.thy ~> BNF_GFP.thy

94 BNF/BNF_LFP.thy ~> BNF_LFP.thy

95 BNF/BNF_Util.thy ~> BNF_Util.thy

96 BNF/Coinduction.thy ~> Coinduction.thy

97 BNF/More_BNFs.thy ~> Library/More_BNFs.thy

98 BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy

99 BNF/Examples/* ~> BNF_Examples/*

100 New theories:

101 List_Prefix.thy (split from Library/Sublist.thy)

102 Wellorder_Extension.thy (split from Zorn.thy)

103 Library/Cardinal_Notations.thy

104 Library/BNF_Decl.thy

105 BNF_Examples/Misc_Primcorec.thy

106 BNF_Examples/Stream_Processor.thy

107 Discontinued theory:

108 BNF/BNF.thy

109 BNF/Equiv_Relations_More.thy

111 * New theory:

112 Cardinals/Ordinal_Arithmetic.thy

114 * Theory reorganizations:

115 * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy

117 * Sledgehammer:

118 - Renamed options:

119 isar_compress ~> compress_isar

120 isar_try0 ~> try0_isar

121 INCOMPATIBILITY.

123 * Try0: Added 'algebra' and 'meson' to the set of proof methods.

125 * The symbol "\<newline>" may be used within char or string literals

126 to represent (Char Nibble0 NibbleA), i.e. ASCII newline.

128 * Activation of Z3 now works via "z3_non_commercial" system option

129 (without requiring restart), instead of former settings variable

130 "Z3_NON_COMMERCIAL". The option can be edited in Isabelle/jEdit menu

131 Plugin Options / Isabelle / General.

133 * "declare [[code abort: ...]]" replaces "code_abort ...".

134 INCOMPATIBILITY.

136 * "declare [[code drop: ...]]" drops all code equations associated

137 with the given constants.

139 * Abolished slightly odd global lattice interpretation for min/max.

141 Fact consolidations:

142 min_max.inf_assoc ~> min.assoc

143 min_max.inf_commute ~> min.commute

144 min_max.inf_left_commute ~> min.left_commute

145 min_max.inf_idem ~> min.idem

146 min_max.inf_left_idem ~> min.left_idem

147 min_max.inf_right_idem ~> min.right_idem

148 min_max.sup_assoc ~> max.assoc

149 min_max.sup_commute ~> max.commute

150 min_max.sup_left_commute ~> max.left_commute

151 min_max.sup_idem ~> max.idem

152 min_max.sup_left_idem ~> max.left_idem

153 min_max.sup_inf_distrib1 ~> max_min_distrib2

154 min_max.sup_inf_distrib2 ~> max_min_distrib1

155 min_max.inf_sup_distrib1 ~> min_max_distrib2

156 min_max.inf_sup_distrib2 ~> min_max_distrib1

157 min_max.distrib ~> min_max_distribs

158 min_max.inf_absorb1 ~> min.absorb1

159 min_max.inf_absorb2 ~> min.absorb2

160 min_max.sup_absorb1 ~> max.absorb1

161 min_max.sup_absorb2 ~> max.absorb2

162 min_max.le_iff_inf ~> min.absorb_iff1

163 min_max.le_iff_sup ~> max.absorb_iff2

164 min_max.inf_le1 ~> min.cobounded1

165 min_max.inf_le2 ~> min.cobounded2

166 le_maxI1, min_max.sup_ge1 ~> max.cobounded1

167 le_maxI2, min_max.sup_ge2 ~> max.cobounded2

168 min_max.le_infI1 ~> min.coboundedI1

169 min_max.le_infI2 ~> min.coboundedI2

170 min_max.le_supI1 ~> max.coboundedI1

171 min_max.le_supI2 ~> max.coboundedI2

172 min_max.less_infI1 ~> min.strict_coboundedI1

173 min_max.less_infI2 ~> min.strict_coboundedI2

174 min_max.less_supI1 ~> max.strict_coboundedI1

175 min_max.less_supI2 ~> max.strict_coboundedI2

176 min_max.inf_mono ~> min.mono

177 min_max.sup_mono ~> max.mono

178 min_max.le_infI, min_max.inf_greatest ~> min.boundedI

179 min_max.le_supI, min_max.sup_least ~> max.boundedI

180 min_max.le_inf_iff ~> min.bounded_iff

181 min_max.le_sup_iff ~> max.bounded_iff

183 For min_max.inf_sup_aci, prefer (one of) min.commute, min.assoc,

184 min.left_commute, min.left_idem, max.commute, max.assoc,

185 max.left_commute, max.left_idem directly.

187 For min_max.inf_sup_ord, prefer (one of) min.cobounded1, min.cobounded2,

188 max.cobounded1m max.cobounded2 directly.

190 For min_ac or max_ac, prefor more general collection ac_simps.

192 INCOMPATBILITY.

194 * Word library: bit representations prefer type bool over type bit.

195 INCOMPATIBILITY.

197 * Theorem disambiguation Inf_le_Sup (on finite sets) ~> Inf_fin_le_Sup_fin.

198 INCOMPATIBILITY.

200 * Code generations are provided for make, fields, extend and truncate

201 operations on records.

203 * Qualified constant names Wellfounded.acc, Wellfounded.accp.

204 INCOMPATIBILITY.

206 * Fact generalization and consolidation:

207 neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1

208 INCOMPATIBILITY.

210 * Purely algebraic definition of even. Fact generalization and consolidation:

211 nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd

212 even_zero_(nat|int) ~> even_zero

213 INCOMPATIBILITY.

215 * Abolished neg_numeral.

216 * Canonical representation for minus one is "- 1".

217 * Canonical representation for other negative numbers is "- (numeral _)".

218 * When devising rule sets for number calculation, consider the

219 following canonical cases: 0, 1, numeral _, - 1, - numeral _.

220 * HOLogic.dest_number also recognizes numerals in non-canonical forms

221 like "numeral One", "- numeral One", "- 0" and even "- ... - _".

222 * Syntax for negative numerals is mere input syntax.

223 INCOMPATBILITY.

225 * Elimination of fact duplicates:

226 equals_zero_I ~> minus_unique

227 diff_eq_0_iff_eq ~> right_minus_eq

228 nat_infinite ~> infinite_UNIV_nat

229 int_infinite ~> infinite_UNIV_int

230 INCOMPATIBILITY.

232 * Fact name consolidation:

233 diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus

234 minus_le_self_iff ~> neg_less_eq_nonneg

235 le_minus_self_iff ~> less_eq_neg_nonpos

236 neg_less_nonneg ~> neg_less_pos

237 less_minus_self_iff ~> less_neg_neg [simp]

238 INCOMPATIBILITY.

240 * More simplification rules on unary and binary minus:

241 add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1,

242 add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,

243 add_minus_cancel, diff_add_cancel, le_add_same_cancel1,

244 le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,

245 minus_add_cancel, uminus_add_conv_diff. These correspondingly

246 have been taken away from fact collections algebra_simps and

247 field_simps. INCOMPATIBILITY.

249 To restore proofs, the following patterns are helpful:

251 a) Arbitrary failing proof not involving "diff_def":

252 Consider simplification with algebra_simps or field_simps.

254 b) Lifting rules from addition to subtraction:

255 Try with "using <rule for addition> of [... "- _" ...]" by simp".

257 c) Simplification with "diff_def": just drop "diff_def".

258 Consider simplification with algebra_simps or field_simps;

259 or the brute way with

260 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff".

262 * SUP and INF generalized to conditionally_complete_lattice

264 * Theory Lubs moved HOL image to HOL-Library. It is replaced by

265 Conditionally_Complete_Lattices. INCOMPATIBILITY.

267 * Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them

268 instead of explicitly stating boundedness of sets.

270 * ccpo.admissible quantifies only over non-empty chains to allow

271 more syntax-directed proof rules; the case of the empty chain

272 shows up as additional case in fixpoint induction proofs.

273 INCOMPATIBILITY

275 * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.

277 * Nitpick:

278 - Fixed soundness bug whereby mutually recursive datatypes could take

279 infinite values.

281 * HOL-Multivariate_Analysis:

282 - type class ordered_real_vector for ordered vector spaces

283 - changed order of ordered_euclidean_space to be compatible with

284 pointwise ordering on products. Therefore instance of

285 conditionally_complete_lattice and ordered_real_vector.

286 INCOMPATIBILITY: use box instead of greaterThanLessThan or

287 explicit set-comprehensions with eucl_less for other (half-) open

288 intervals.

291 *** ML ***

293 * Proper context discipline for read_instantiate and instantiate_tac:

294 variables that are meant to become schematic need to be given as

295 fixed, and are generalized by the explicit context of local variables.

296 This corresponds to Isar attributes "where" and "of" with 'for'

297 declaration. INCOMPATIBILITY, also due to potential change of indices

298 of schematic variables.

300 * Toplevel function "use" refers to raw ML bootstrap environment,

301 without Isar context nor antiquotations. Potential INCOMPATIBILITY.

302 Note that 'ML_file' is the canonical command to load ML files into the

303 formal context.

305 * Proper context for basic Simplifier operations: rewrite_rule,

306 rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to

307 pass runtime Proof.context (and ensure that the simplified entity

308 actually belongs to it).

311 *** System ***

313 * Simplified "isabelle display" tool. Settings variables DVI_VIEWER

314 and PDF_VIEWER now refer to the actual programs, not shell

315 command-lines. Discontinued option -c: invocation may be asynchronous

316 via desktop environment, without any special precautions. Potential

317 INCOMPATIBILITY with ambitious private settings.

319 * Improved 'display_drafts' concerning desktop integration and

320 repeated invocation in PIDE front-end: re-use single file

321 $ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views.

325 New in Isabelle2013-2 (December 2013)

326 -------------------------------------

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

330 * More robust editing of running commands with internal forks,

331 e.g. non-terminating 'by' steps.

333 * More relaxed Sledgehammer panel: avoid repeated application of query

334 after edits surrounding the command location.

336 * More status information about commands that are interrupted

337 accidentally (via physical event or Poly/ML runtime system signal,

338 e.g. out-of-memory).

341 *** System ***

343 * More robust termination of external processes managed by

344 Isabelle/ML: support cancellation of tasks within the range of

345 milliseconds, as required for PIDE document editing with automatically

346 tried tools (e.g. Sledgehammer).

348 * Reactivated Isabelle/Scala kill command for external processes on

349 Mac OS X, which was accidentally broken in Isabelle2013-1 due to a

350 workaround for some Debian/Ubuntu Linux versions from 2013.

354 New in Isabelle2013-1 (November 2013)

355 -------------------------------------

357 *** General ***

359 * Discontinued obsolete 'uses' within theory header. Note that

360 commands like 'ML_file' work without separate declaration of file

361 dependencies. Minor INCOMPATIBILITY.

363 * Discontinued redundant 'use' command, which was superseded by

364 'ML_file' in Isabelle2013. Minor INCOMPATIBILITY.

366 * Simplified subscripts within identifiers, using plain \<^sub>

367 instead of the second copy \<^isub> and \<^isup>. Superscripts are

368 only for literal tokens within notation; explicit mixfix annotations

369 for consts or fixed variables may be used as fall-back for unusual

370 names. Obsolete \<twosuperior> has been expanded to \<^sup>2 in

371 Isabelle/HOL. INCOMPATIBILITY, use "isabelle update_sub_sup" to

372 standardize symbols as a starting point for further manual cleanup.

373 The ML reference variable "legacy_isub_isup" may be set as temporary

374 workaround, to make the prover accept a subset of the old identifier

375 syntax.

377 * Document antiquotations: term style "isub" has been renamed to

378 "sub". Minor INCOMPATIBILITY.

380 * Uniform management of "quick_and_dirty" as system option (see also

381 "isabelle options"), configuration option within the context (see also

382 Config.get in Isabelle/ML), and attribute in Isabelle/Isar. Minor

383 INCOMPATIBILITY, need to use more official Isabelle means to access

384 quick_and_dirty, instead of historical poking into mutable reference.

386 * Renamed command 'print_configs' to 'print_options'. Minor

387 INCOMPATIBILITY.

389 * Proper diagnostic command 'print_state'. Old 'pr' (with its

390 implicit change of some global references) is retained for now as

391 control command, e.g. for ProofGeneral 3.7.x.

393 * Discontinued 'print_drafts' command with its old-fashioned PS output

394 and Unix command-line print spooling. Minor INCOMPATIBILITY: use

395 'display_drafts' instead and print via the regular document viewer.

397 * Updated and extended "isar-ref" and "implementation" manual,

398 eliminated old "ref" manual.

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

403 * New manual "jedit" for Isabelle/jEdit, see isabelle doc or

404 Documentation panel.

406 * Dockable window "Documentation" provides access to Isabelle

407 documentation.

409 * Dockable window "Find" provides query operations for formal entities

410 (GUI front-end to 'find_theorems' command).

412 * Dockable window "Sledgehammer" manages asynchronous / parallel

413 sledgehammer runs over existing document sources, independently of

414 normal editing and checking process.

416 * Dockable window "Timing" provides an overview of relevant command

417 timing information, depending on option jedit_timing_threshold. The

418 same timing information is shown in the extended tooltip of the

419 command keyword, when hovering the mouse over it while the CONTROL or

420 COMMAND modifier is pressed.

422 * Improved dockable window "Theories": Continuous checking of proof

423 document (visible and required parts) may be controlled explicitly,

424 using check box or shortcut "C+e ENTER". Individual theory nodes may

425 be marked explicitly as required and checked in full, using check box

426 or shortcut "C+e SPACE".

428 * Improved completion mechanism, which is now managed by the

429 Isabelle/jEdit plugin instead of SideKick. Refined table of Isabelle

430 symbol abbreviations (see $ISABELLE_HOME/etc/symbols).

432 * Standard jEdit keyboard shortcut C+b complete-word is remapped to

433 isabelle.complete for explicit completion in Isabelle sources.

434 INCOMPATIBILITY wrt. jEdit defaults, may have to invent new shortcuts

435 to resolve conflict.

437 * Improved support of various "minor modes" for Isabelle NEWS,

438 options, session ROOT etc., with completion and SideKick tree view.

440 * Strictly monotonic document update, without premature cancellation of

441 running transactions that are still needed: avoid reset/restart of

442 such command executions while editing.

444 * Support for asynchronous print functions, as overlay to existing

445 document content.

447 * Support for automatic tools in HOL, which try to prove or disprove

448 toplevel theorem statements.

450 * Action isabelle.reset-font-size resets main text area font size

451 according to Isabelle/Scala plugin option "jedit_font_reset_size" (see

452 also "Plugin Options / Isabelle / General"). It can be bound to some

453 keyboard shortcut by the user (e.g. C+0 and/or C+NUMPAD0).

455 * File specifications in jEdit (e.g. file browser) may refer to

456 $ISABELLE_HOME and $ISABELLE_HOME_USER on all platforms. Discontinued

457 obsolete $ISABELLE_HOME_WINDOWS variable.

459 * Improved support for Linux look-and-feel "GTK+", see also "Utilities

460 / Global Options / Appearance".

462 * Improved support of native Mac OS X functionality via "MacOSX"

463 plugin, which is now enabled by default.

466 *** Pure ***

468 * Commands 'interpretation' and 'sublocale' are now target-sensitive.

469 In particular, 'interpretation' allows for non-persistent

470 interpretation within "context ... begin ... end" blocks offering a

471 light-weight alternative to 'sublocale'. See "isar-ref" manual for

472 details.

474 * Improved locales diagnostic command 'print_dependencies'.

476 * Discontinued obsolete 'axioms' command, which has been marked as

477 legacy since Isabelle2009-2. INCOMPATIBILITY, use 'axiomatization'

478 instead, while observing its uniform scope for polymorphism.

480 * Discontinued empty name bindings in 'axiomatization'.

481 INCOMPATIBILITY.

483 * System option "proofs" has been discontinued. Instead the global

484 state of Proofterm.proofs is persistently compiled into logic images

485 as required, notably HOL-Proofs. Users no longer need to change

486 Proofterm.proofs dynamically. Minor INCOMPATIBILITY.

488 * Syntax translation functions (print_translation etc.) always depend

489 on Proof.context. Discontinued former "(advanced)" option -- this is

490 now the default. Minor INCOMPATIBILITY.

492 * Former global reference trace_unify_fail is now available as

493 configuration option "unify_trace_failure" (global context only).

495 * SELECT_GOAL now retains the syntactic context of the overall goal

496 state (schematic variables etc.). Potential INCOMPATIBILITY in rare

497 situations.

500 *** HOL ***

502 * Stronger precedence of syntax for big intersection and union on

503 sets, in accordance with corresponding lattice operations.

504 INCOMPATIBILITY.

506 * Notation "{p:A. P}" now allows tuple patterns as well.

508 * Nested case expressions are now translated in a separate check phase

509 rather than during parsing. The data for case combinators is separated

510 from the datatype package. The declaration attribute

511 "case_translation" can be used to register new case combinators:

513 declare [[case_translation case_combinator constructor1 ... constructorN]]

515 * Code generator:

516 - 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' /

517 'code_instance'.

518 - 'code_identifier' declares name hints for arbitrary identifiers in

519 generated code, subsuming 'code_modulename'.

521 See the isar-ref manual for syntax diagrams, and the HOL theories for

522 examples.

524 * Attibute 'code': 'code' now declares concrete and abstract code

525 equations uniformly. Use explicit 'code equation' and 'code abstract'

526 to distinguish both when desired.

528 * Discontinued theories Code_Integer and Efficient_Nat by a more

529 fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,

530 Code_Target_Nat and Code_Target_Numeral. See the tutorial on code

531 generation for details. INCOMPATIBILITY.

533 * Numeric types are mapped by default to target language numerals:

534 natural (replaces former code_numeral) and integer (replaces former

535 code_int). Conversions are available as integer_of_natural /

536 natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and

537 Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in

538 ML). INCOMPATIBILITY.

540 * Function package: For mutually recursive functions f and g, separate

541 cases rules f.cases and g.cases are generated instead of unusable

542 f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY,

543 in the case that the unusable rule was used nevertheless.

545 * Function package: For each function f, new rules f.elims are

546 generated, which eliminate equalities of the form "f x = t".

548 * New command 'fun_cases' derives ad-hoc elimination rules for

549 function equations as simplified instances of f.elims, analogous to

550 inductive_cases. See ~~/src/HOL/ex/Fundefs.thy for some examples.

552 * Lifting:

553 - parametrized correspondence relations are now supported:

554 + parametricity theorems for the raw term can be specified in

555 the command lift_definition, which allow us to generate stronger

556 transfer rules

557 + setup_lifting generates stronger transfer rules if parametric

558 correspondence relation can be generated

559 + various new properties of the relator must be specified to support

560 parametricity

561 + parametricity theorem for the Quotient relation can be specified

562 - setup_lifting generates domain rules for the Transfer package

563 - stronger reflexivity prover of respectfulness theorems for type

564 copies

565 - ===> and --> are now local. The symbols can be introduced

566 by interpreting the locale lifting_syntax (typically in an

567 anonymous context)

568 - Lifting/Transfer relevant parts of Library/Quotient_* are now in

569 Main. Potential INCOMPATIBILITY

570 - new commands for restoring and deleting Lifting/Transfer context:

571 lifting_forget, lifting_update

572 - the command print_quotmaps was renamed to print_quot_maps.

573 INCOMPATIBILITY

575 * Transfer:

576 - better support for domains in Transfer: replace Domainp T

577 by the actual invariant in a transferred goal

578 - transfer rules can have as assumptions other transfer rules

579 - Experimental support for transferring from the raw level to the

580 abstract level: Transfer.transferred attribute

581 - Attribute version of the transfer method: untransferred attribute

583 * Reification and reflection:

584 - Reification is now directly available in HOL-Main in structure

585 "Reification".

586 - Reflection now handles multiple lists with variables also.

587 - The whole reflection stack has been decomposed into conversions.

588 INCOMPATIBILITY.

590 * Revised devices for recursive definitions over finite sets:

591 - Only one fundamental fold combinator on finite set remains:

592 Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b

593 This is now identity on infinite sets.

594 - Locales ("mini packages") for fundamental definitions with

595 Finite_Set.fold: folding, folding_idem.

596 - Locales comm_monoid_set, semilattice_order_set and

597 semilattice_neutr_order_set for big operators on sets.

598 See theory Big_Operators for canonical examples.

599 Note that foundational constants comm_monoid_set.F and

600 semilattice_set.F correspond to former combinators fold_image

601 and fold1 respectively. These are now gone. You may use

602 those foundational constants as substitutes, but it is

603 preferable to interpret the above locales accordingly.

604 - Dropped class ab_semigroup_idem_mult (special case of lattice,

605 no longer needed in connection with Finite_Set.fold etc.)

606 - Fact renames:

607 card.union_inter ~> card_Un_Int [symmetric]

608 card.union_disjoint ~> card_Un_disjoint

609 INCOMPATIBILITY.

611 * Locale hierarchy for abstract orderings and (semi)lattices.

613 * Complete_Partial_Order.admissible is defined outside the type class

614 ccpo, but with mandatory prefix ccpo. Admissibility theorems lose the

615 class predicate assumption or sort constraint when possible.

616 INCOMPATIBILITY.

618 * Introduce type class "conditionally_complete_lattice": Like a

619 complete lattice but does not assume the existence of the top and

620 bottom elements. Allows to generalize some lemmas about reals and

621 extended reals. Removed SupInf and replaced it by the instantiation

622 of conditionally_complete_lattice for real. Renamed lemmas about

623 conditionally-complete lattice from Sup_... to cSup_... and from

624 Inf_... to cInf_... to avoid hidding of similar complete lattice

625 lemmas.

627 * Introduce type class linear_continuum as combination of

628 conditionally-complete lattices and inner dense linorders which have

629 more than one element. INCOMPATIBILITY.

631 * Introduced type classes order_top and order_bot. The old classes top

632 and bot only contain the syntax without assumptions. INCOMPATIBILITY:

633 Rename bot -> order_bot, top -> order_top

635 * Introduce type classes "no_top" and "no_bot" for orderings without

636 top and bottom elements.

638 * Split dense_linorder into inner_dense_order and no_top, no_bot.

640 * Complex_Main: Unify and move various concepts from

641 HOL-Multivariate_Analysis to HOL-Complex_Main.

643 - Introduce type class (lin)order_topology and

644 linear_continuum_topology. Allows to generalize theorems about

645 limits and order. Instances are reals and extended reals.

647 - continuous and continuos_on from Multivariate_Analysis:

648 "continuous" is the continuity of a function at a filter. "isCont"

649 is now an abbrevitation: "isCont x f == continuous (at _) f".

651 Generalized continuity lemmas from isCont to continuous on an

652 arbitrary filter.

654 - compact from Multivariate_Analysis. Use Bolzano's lemma to prove

655 compactness of closed intervals on reals. Continuous functions

656 attain infimum and supremum on compact sets. The inverse of a

657 continuous function is continuous, when the function is continuous

658 on a compact set.

660 - connected from Multivariate_Analysis. Use it to prove the

661 intermediate value theorem. Show connectedness of intervals on

662 linear_continuum_topology).

664 - first_countable_topology from Multivariate_Analysis. Is used to

665 show equivalence of properties on the neighbourhood filter of x and

666 on all sequences converging to x.

668 - FDERIV: Definition of has_derivative moved to Deriv.thy. Moved

669 theorems from Library/FDERIV.thy to Deriv.thy and base the

670 definition of DERIV on FDERIV. Add variants of DERIV and FDERIV

671 which are restricted to sets, i.e. to represent derivatives from

672 left or right.

674 - Removed the within-filter. It is replaced by the principal filter:

676 F within X = inf F (principal X)

678 - Introduce "at x within U" as a single constant, "at x" is now an

679 abbreviation for "at x within UNIV"

681 - Introduce named theorem collections tendsto_intros,

682 continuous_intros, continuous_on_intros and FDERIV_intros. Theorems

683 in tendsto_intros (or FDERIV_intros) are also available as

684 tendsto_eq_intros (or FDERIV_eq_intros) where the right-hand side

685 is replaced by a congruence rule. This allows to apply them as

686 intro rules and then proving equivalence by the simplifier.

688 - Restructured theories in HOL-Complex_Main:

690 + Moved RealDef and RComplete into Real

692 + Introduced Topological_Spaces and moved theorems about

693 topological spaces, filters, limits and continuity to it

695 + Renamed RealVector to Real_Vector_Spaces

697 + Split Lim, SEQ, Series into Topological_Spaces,

698 Real_Vector_Spaces, and Limits

700 + Moved Ln and Log to Transcendental

702 + Moved theorems about continuity from Deriv to Topological_Spaces

704 - Remove various auxiliary lemmas.

706 INCOMPATIBILITY.

708 * Nitpick:

709 - Added option "spy"

710 - Reduce incidence of "too high arity" errors

712 * Sledgehammer:

713 - Renamed option:

714 isar_shrink ~> isar_compress

715 INCOMPATIBILITY.

716 - Added options "isar_try0", "spy"

717 - Better support for "isar_proofs"

718 - MaSh has been fined-tuned and now runs as a local server

720 * Improved support for ad hoc overloading of constants (see also

721 isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).

723 * Library/Polynomial.thy:

724 - Use lifting for primitive definitions.

725 - Explicit conversions from and to lists of coefficients, used for

726 generated code.

727 - Replaced recursion operator poly_rec by fold_coeffs.

728 - Prefer pre-existing gcd operation for gcd.

729 - Fact renames:

730 poly_eq_iff ~> poly_eq_poly_eq_iff

731 poly_ext ~> poly_eqI

732 expand_poly_eq ~> poly_eq_iff

733 IMCOMPATIBILITY.

735 * New Library/Simps_Case_Conv.thy: Provides commands simps_of_case and

736 case_of_simps to convert function definitions between a list of

737 equations with patterns on the lhs and a single equation with case

738 expressions on the rhs. See also Ex/Simps_Case_Conv_Examples.thy.

740 * New Library/FSet.thy: type of finite sets defined as a subtype of

741 sets defined by Lifting/Transfer.

743 * Discontinued theory src/HOL/Library/Eval_Witness. INCOMPATIBILITY.

745 * Consolidation of library theories on product orders:

747 Product_Lattice ~> Product_Order -- pointwise order on products

748 Product_ord ~> Product_Lexorder -- lexicographic order on products

750 INCOMPATIBILITY.

752 * Imperative-HOL: The MREC combinator is considered legacy and no

753 longer included by default. INCOMPATIBILITY, use partial_function

754 instead, or import theory Legacy_Mrec as a fallback.

756 * HOL-Algebra: Discontinued theories ~~/src/HOL/Algebra/abstract and

757 ~~/src/HOL/Algebra/poly. Existing theories should be based on

758 ~~/src/HOL/Library/Polynomial instead. The latter provides

759 integration with HOL's type classes for rings. INCOMPATIBILITY.

761 * HOL-BNF:

762 - Various improvements to BNF-based (co)datatype package, including

763 new commands "primrec_new", "primcorec", and

764 "datatype_new_compat", as well as documentation. See

765 "datatypes.pdf" for details.

766 - New "coinduction" method to avoid some boilerplate (compared to

767 coinduct).

768 - Renamed keywords:

769 data ~> datatype_new

770 codata ~> codatatype

771 bnf_def ~> bnf

772 - Renamed many generated theorems, including

773 discs ~> disc

774 map_comp' ~> map_comp

775 map_id' ~> map_id

776 sels ~> sel

777 set_map' ~> set_map

778 sets ~> set

779 IMCOMPATIBILITY.

782 *** ML ***

784 * Spec_Check is a Quickcheck tool for Isabelle/ML. The ML function

785 "check_property" allows to check specifications of the form "ALL x y

786 z. prop x y z". See also ~~/src/Tools/Spec_Check/ with its

787 Examples.thy in particular.

789 * Improved printing of exception trace in Poly/ML 5.5.1, with regular

790 tracing output in the command transaction context instead of physical

791 stdout. See also Toplevel.debug, Toplevel.debugging and

792 ML_Compiler.exn_trace.

794 * ML type "theory" is now immutable, without any special treatment of

795 drafts or linear updates (which could lead to "stale theory" errors in

796 the past). Discontinued obsolete operations like Theory.copy,

797 Theory.checkpoint, and the auxiliary type theory_ref. Minor

798 INCOMPATIBILITY.

800 * More uniform naming of goal functions for skipped proofs:

802 Skip_Proof.prove ~> Goal.prove_sorry

803 Skip_Proof.prove_global ~> Goal.prove_sorry_global

805 Minor INCOMPATIBILITY.

807 * Simplifier tactics and tools use proper Proof.context instead of

808 historic type simpset. Old-style declarations like addsimps,

809 addsimprocs etc. operate directly on Proof.context. Raw type simpset

810 retains its use as snapshot of the main Simplifier context, using

811 simpset_of and put_simpset on Proof.context. INCOMPATIBILITY -- port

812 old tools by making them depend on (ctxt : Proof.context) instead of

813 (ss : simpset), then turn (simpset_of ctxt) into ctxt.

815 * Modifiers for classical wrappers (e.g. addWrapper, delWrapper)

816 operate on Proof.context instead of claset, for uniformity with addIs,

817 addEs, addDs etc. Note that claset_of and put_claset allow to manage

818 clasets separately from the context.

820 * Discontinued obsolete ML antiquotations @{claset} and @{simpset}.

821 INCOMPATIBILITY, use @{context} instead.

823 * Antiquotation @{theory_context A} is similar to @{theory A}, but

824 presents the result as initial Proof.context.

827 *** System ***

829 * Discontinued obsolete isabelle usedir, mkdir, make -- superseded by

830 "isabelle build" in Isabelle2013. INCOMPATIBILITY.

832 * Discontinued obsolete isabelle-process options -f and -u (former

833 administrative aliases of option -e). Minor INCOMPATIBILITY.

835 * Discontinued obsolete isabelle print tool, and PRINT_COMMAND

836 settings variable.

838 * Discontinued ISABELLE_DOC_FORMAT settings variable and historic

839 document formats: dvi.gz, ps, ps.gz -- the default document format is

840 always pdf.

842 * Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to

843 specify global resources of the JVM process run by isabelle build.

845 * Toplevel executable $ISABELLE_HOME/bin/isabelle_scala_script allows

846 to run Isabelle/Scala source files as standalone programs.

848 * Improved "isabelle keywords" tool (for old-style ProofGeneral

849 keyword tables): use Isabelle/Scala operations, which inspect outer

850 syntax without requiring to build sessions first.

852 * Sessions may be organized via 'chapter' specifications in the ROOT

853 file, which determines a two-level hierarchy of browser info. The old

854 tree-like organization via implicit sub-session relation (with its

855 tendency towards erratic fluctuation of URLs) has been discontinued.

856 The default chapter is called "Unsorted". Potential INCOMPATIBILITY

857 for HTML presentation of theories.

861 New in Isabelle2013 (February 2013)

862 -----------------------------------

864 *** General ***

866 * Theorem status about oracles and unfinished/failed future proofs is

867 no longer printed by default, since it is incompatible with

868 incremental / parallel checking of the persistent document model. ML

869 function Thm.peek_status may be used to inspect a snapshot of the

870 ongoing evaluation process. Note that in batch mode --- notably

871 isabelle build --- the system ensures that future proofs of all

872 accessible theorems in the theory context are finished (as before).

874 * Configuration option show_markup controls direct inlining of markup

875 into the printed representation of formal entities --- notably type

876 and sort constraints. This enables Prover IDE users to retrieve that

877 information via tooltips in the output window, for example.

879 * Command 'ML_file' evaluates ML text from a file directly within the

880 theory, without any predeclaration via 'uses' in the theory header.

882 * Old command 'use' command and corresponding keyword 'uses' in the

883 theory header are legacy features and will be discontinued soon.

884 Tools that load their additional source files may imitate the

885 'ML_file' implementation, such that the system can take care of

886 dependencies properly.

888 * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which

889 is called fastforce / fast_force_tac already since Isabelle2011-1.

891 * Updated and extended "isar-ref" and "implementation" manual, reduced

892 remaining material in old "ref" manual.

894 * Improved support for auxiliary contexts that indicate block structure

895 for specifications. Nesting of "context fixes ... context assumes ..."

896 and "class ... context ...".

898 * Attribute "consumes" allows a negative value as well, which is

899 interpreted relatively to the total number of premises of the rule in

900 the target context. This form of declaration is stable when exported

901 from a nested 'context' with additional assumptions. It is the

902 preferred form for definitional packages, notably cases/rules produced

903 in HOL/inductive and HOL/function.

905 * More informative error messages for Isar proof commands involving

906 lazy enumerations (method applications etc.).

908 * Refined 'help' command to retrieve outer syntax commands according

909 to name patterns (with clickable results).

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

914 * Parallel terminal proofs ('by') are enabled by default, likewise

915 proofs that are built into packages like 'datatype', 'function'. This

916 allows to "run ahead" checking the theory specifications on the

917 surface, while the prover is still crunching on internal

918 justifications. Unfinished / cancelled proofs are restarted as

919 required to complete full proof checking eventually.

921 * Improved output panel with tooltips, hyperlinks etc. based on the

922 same Rich_Text_Area as regular Isabelle/jEdit buffers. Activation of

923 tooltips leads to some window that supports the same recursively,

924 which can lead to stacks of tooltips as the semantic document content

925 is explored. ESCAPE closes the whole stack, individual windows may be

926 closed separately, or detached to become independent jEdit dockables.

928 * Improved support for commands that produce graph output: the text

929 message contains a clickable area to open a new instance of the graph

930 browser on demand.

932 * More robust incremental parsing of outer syntax (partial comments,

933 malformed symbols). Changing the balance of open/close quotes and

934 comment delimiters works more conveniently with unfinished situations

935 that frequently occur in user interaction.

937 * More efficient painting and improved reactivity when editing large

938 files. More scalable management of formal document content.

940 * Smarter handling of tracing messages: prover process pauses after

941 certain number of messages per command transaction, with some user

942 dialog to stop or continue. This avoids swamping the front-end with

943 potentially infinite message streams.

945 * More plugin options and preferences, based on Isabelle/Scala. The

946 jEdit plugin option panel provides access to some Isabelle/Scala

947 options, including tuning parameters for editor reactivity and color

948 schemes.

950 * Dockable window "Symbols" provides some editing support for Isabelle

951 symbols.

953 * Dockable window "Monitor" shows ML runtime statistics. Note that

954 continuous display of the chart slows down the system.

956 * Improved editing support for control styles: subscript, superscript,

957 bold, reset of style -- operating on single symbols or text

958 selections. Cf. keyboard shortcuts C+e DOWN/UP/RIGHT/LEFT.

960 * Actions isabelle.increase-font-size and isabelle.decrease-font-size

961 adjust the main text area font size, and its derivatives for output,

962 tooltips etc. Cf. keyboard shortcuts C-PLUS and C-MINUS, which often

963 need to be adapted to local keyboard layouts.

965 * More reactive completion popup by default: use \t (TAB) instead of

966 \n (NEWLINE) to minimize intrusion into regular flow of editing. See

967 also "Plugin Options / SideKick / General / Code Completion Options".

969 * Implicit check and build dialog of the specified logic session

970 image. For example, HOL, HOLCF, HOL-Nominal can be produced on

971 demand, without bundling big platform-dependent heap images in the

972 Isabelle distribution.

974 * Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates

975 from Oracle provide better multi-platform experience. This version is

976 now bundled exclusively with Isabelle.

979 *** Pure ***

981 * Code generation for Haskell: restrict unqualified imports from

982 Haskell Prelude to a small set of fundamental operations.

984 * Command 'export_code': relative file names are interpreted

985 relatively to master directory of current theory rather than the

986 rather arbitrary current working directory. INCOMPATIBILITY.

988 * Discontinued obsolete attribute "COMP". Potential INCOMPATIBILITY,

989 use regular rule composition via "OF" / "THEN", or explicit proof

990 structure instead. Note that Isabelle/ML provides a variety of

991 operators like COMP, INCR_COMP, COMP_INCR, which need to be applied

992 with some care where this is really required.

994 * Command 'typ' supports an additional variant with explicit sort

995 constraint, to infer and check the most general type conforming to a

996 given sort. Example (in HOL):

998 typ "_ * _ * bool * unit" :: finite

1000 * Command 'locale_deps' visualizes all locales and their relations as

1001 a Hasse diagram.

1004 *** HOL ***

1006 * Sledgehammer:

1008 - Added MaSh relevance filter based on machine-learning; see the

1009 Sledgehammer manual for details.

1010 - Polished Isar proofs generated with "isar_proofs" option.

1011 - Rationalized type encodings ("type_enc" option).

1012 - Renamed "kill_provers" subcommand to "kill_all".

1013 - Renamed options:

1014 isar_proof ~> isar_proofs

1015 isar_shrink_factor ~> isar_shrink

1016 max_relevant ~> max_facts

1017 relevance_thresholds ~> fact_thresholds

1019 * Quickcheck: added an optimisation for equality premises. It is

1020 switched on by default, and can be switched off by setting the

1021 configuration quickcheck_optimise_equality to false.

1023 * Quotient: only one quotient can be defined by quotient_type

1024 INCOMPATIBILITY.

1026 * Lifting:

1027 - generation of an abstraction function equation in lift_definition

1028 - quot_del attribute

1029 - renamed no_abs_code -> no_code (INCOMPATIBILITY.)

1031 * Simproc "finite_Collect" rewrites set comprehensions into pointfree

1032 expressions.

1034 * Preprocessing of the code generator rewrites set comprehensions into

1035 pointfree expressions.

1037 * The SMT solver Z3 has now by default a restricted set of directly

1038 supported features. For the full set of features (div/mod, nonlinear

1039 arithmetic, datatypes/records) with potential proof reconstruction

1040 failures, enable the configuration option "z3_with_extensions". Minor

1041 INCOMPATIBILITY.

1043 * Simplified 'typedef' specifications: historical options for implicit

1044 set definition and alternative name have been discontinued. The

1045 former behavior of "typedef (open) t = A" is now the default, but

1046 written just "typedef t = A". INCOMPATIBILITY, need to adapt theories

1047 accordingly.

1049 * Removed constant "chars"; prefer "Enum.enum" on type "char"

1050 directly. INCOMPATIBILITY.

1052 * Moved operation product, sublists and n_lists from theory Enum to

1053 List. INCOMPATIBILITY.

1055 * Theorem UN_o generalized to SUP_comp. INCOMPATIBILITY.

1057 * Class "comm_monoid_diff" formalises properties of bounded

1058 subtraction, with natural numbers and multisets as typical instances.

1060 * Added combinator "Option.these" with type "'a option set => 'a set".

1062 * Theory "Transitive_Closure": renamed lemmas

1064 reflcl_tranclp -> reflclp_tranclp

1065 rtranclp_reflcl -> rtranclp_reflclp

1067 INCOMPATIBILITY.

1069 * Theory "Rings": renamed lemmas (in class semiring)

1071 left_distrib ~> distrib_right

1072 right_distrib ~> distrib_left

1074 INCOMPATIBILITY.

1076 * Generalized the definition of limits:

1078 - Introduced the predicate filterlim (LIM x F. f x :> G) which

1079 expresses that when the input values x converge to F then the

1080 output f x converges to G.

1082 - Added filters for convergence to positive (at_top) and negative

1083 infinity (at_bot).

1085 - Moved infinity in the norm (at_infinity) from

1086 Multivariate_Analysis to Complex_Main.

1088 - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :>

1089 at_top".

1091 INCOMPATIBILITY.

1093 * Theory "Library/Option_ord" provides instantiation of option type to

1094 lattice type classes.

1096 * Theory "Library/Multiset": renamed

1098 constant fold_mset ~> Multiset.fold

1099 fact fold_mset_commute ~> fold_mset_comm

1101 INCOMPATIBILITY.

1103 * Renamed theory Library/List_Prefix to Library/Sublist, with related

1104 changes as follows.

1106 - Renamed constants (and related lemmas)

1108 prefix ~> prefixeq

1109 strict_prefix ~> prefix

1111 - Replaced constant "postfix" by "suffixeq" with swapped argument

1112 order (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped

1113 old infix syntax "xs >>= ys"; use "suffixeq ys xs" instead.

1114 Renamed lemmas accordingly.

1116 - Added constant "list_hembeq" for homeomorphic embedding on

1117 lists. Added abbreviation "sublisteq" for special case

1118 "list_hembeq (op =)".

1120 - Theory Library/Sublist no longer provides "order" and "bot" type

1121 class instances for the prefix order (merely corresponding locale

1122 interpretations). The type class instances are now in theory

1123 Library/Prefix_Order.

1125 - The sublist relation of theory Library/Sublist_Order is now based

1126 on "Sublist.sublisteq". Renamed lemmas accordingly:

1128 le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff

1129 le_list_append_mono ~> Sublist.list_hembeq_append_mono

1130 le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2

1131 le_list_Cons_EX ~> Sublist.list_hembeq_ConsD

1132 le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2'

1133 le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq

1134 le_list_drop_Cons ~> Sublist.sublisteq_Cons'

1135 le_list_drop_many ~> Sublist.sublisteq_drop_many

1136 le_list_filter_left ~> Sublist.sublisteq_filter_left

1137 le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many

1138 le_list_rev_take_iff ~> Sublist.sublisteq_append

1139 le_list_same_length ~> Sublist.sublisteq_same_length

1140 le_list_take_many_iff ~> Sublist.sublisteq_append'

1141 less_eq_list.drop ~> less_eq_list_drop

1142 less_eq_list.induct ~> less_eq_list_induct

1143 not_le_list_length ~> Sublist.not_sublisteq_length

1145 INCOMPATIBILITY.

1147 * New theory Library/Countable_Set.

1149 * Theory Library/Debug and Library/Parallel provide debugging and

1150 parallel execution for code generated towards Isabelle/ML.

1152 * Theory Library/FuncSet: Extended support for Pi and extensional and

1153 introduce the extensional dependent function space "PiE". Replaced

1154 extensional_funcset by an abbreviation, and renamed lemmas from

1155 extensional_funcset to PiE as follows:

1157 extensional_empty ~> PiE_empty

1158 extensional_funcset_empty_domain ~> PiE_empty_domain

1159 extensional_funcset_empty_range ~> PiE_empty_range

1160 extensional_funcset_arb ~> PiE_arb

1161 extensional_funcset_mem ~> PiE_mem

1162 extensional_funcset_extend_domainI ~> PiE_fun_upd

1163 extensional_funcset_restrict_domain ~> fun_upd_in_PiE

1164 extensional_funcset_extend_domain_eq ~> PiE_insert_eq

1165 card_extensional_funcset ~> card_PiE

1166 finite_extensional_funcset ~> finite_PiE

1168 INCOMPATIBILITY.

1170 * Theory Library/FinFun: theory of almost everywhere constant

1171 functions (supersedes the AFP entry "Code Generation for Functions as

1172 Data").

1174 * Theory Library/Phantom: generic phantom type to make a type

1175 parameter appear in a constant's type. This alternative to adding

1176 TYPE('a) as another parameter avoids unnecessary closures in generated

1177 code.

1179 * Theory Library/RBT_Impl: efficient construction of red-black trees

1180 from sorted associative lists. Merging two trees with rbt_union may

1181 return a structurally different tree than before. Potential

1182 INCOMPATIBILITY.

1184 * Theory Library/IArray: immutable arrays with code generation.

1186 * Theory Library/Finite_Lattice: theory of finite lattices.

1188 * HOL/Multivariate_Analysis: replaced

1190 "basis :: 'a::euclidean_space => nat => real"

1191 "\<Chi>\<Chi> :: (nat => real) => 'a::euclidean_space"

1193 on euclidean spaces by using the inner product "_ \<bullet> _" with

1194 vectors from the Basis set: "\<Chi>\<Chi> i. f i" is superseded by

1195 "SUM i : Basis. f i * r i".

1197 With this change the following constants are also changed or removed:

1199 DIM('a) :: nat ~> card (Basis :: 'a set) (is an abbreviation)

1200 a $$ i ~> inner a i (where i : Basis)

1201 cart_base i removed

1202 \<pi>, \<pi>' removed

1204 Theorems about these constants where removed.

1206 Renamed lemmas:

1208 component_le_norm ~> Basis_le_norm

1209 euclidean_eq ~> euclidean_eq_iff

1210 differential_zero_maxmin_component ~> differential_zero_maxmin_cart

1211 euclidean_simps ~> inner_simps

1212 independent_basis ~> independent_Basis

1213 span_basis ~> span_Basis

1214 in_span_basis ~> in_span_Basis

1215 norm_bound_component_le ~> norm_boound_Basis_le

1216 norm_bound_component_lt ~> norm_boound_Basis_lt

1217 component_le_infnorm ~> Basis_le_infnorm

1219 INCOMPATIBILITY.

1221 * HOL/Probability:

1223 - Added simproc "measurable" to automatically prove measurability.

1225 - Added induction rules for sigma sets with disjoint union

1226 (sigma_sets_induct_disjoint) and for Borel-measurable functions

1227 (borel_measurable_induct).

1229 - Added the Daniell-Kolmogorov theorem (the existence the limit of a

1230 projective family).

1232 * HOL/Cardinals: Theories of ordinals and cardinals (supersedes the

1233 AFP entry "Ordinals_and_Cardinals").

1235 * HOL/BNF: New (co)datatype package based on bounded natural functors

1236 with support for mixed, nested recursion and interesting non-free

1237 datatypes.

1239 * HOL/Finite_Set and Relation: added new set and relation operations

1240 expressed by Finite_Set.fold.

1242 * New theory HOL/Library/RBT_Set: implementation of sets by red-black

1243 trees for the code generator.

1245 * HOL/Library/RBT and HOL/Library/Mapping have been converted to

1246 Lifting/Transfer.

1247 possible INCOMPATIBILITY.

1249 * HOL/Set: renamed Set.project -> Set.filter

1250 INCOMPATIBILITY.

1253 *** Document preparation ***

1255 * Dropped legacy antiquotations "term_style" and "thm_style", since

1256 styles may be given as arguments to "term" and "thm" already.

1257 Discontinued legacy styles "prem1" .. "prem19".

1259 * Default LaTeX rendering for \<euro> is now based on eurosym package,

1260 instead of slightly exotic babel/greek.

1262 * Document variant NAME may use different LaTeX entry point

1263 document/root_NAME.tex if that file exists, instead of the common

1264 document/root.tex.

1266 * Simplified custom document/build script, instead of old-style

1267 document/IsaMakefile. Minor INCOMPATIBILITY.

1270 *** ML ***

1272 * The default limit for maximum number of worker threads is now 8,

1273 instead of 4, in correspondence to capabilities of contemporary

1274 hardware and Poly/ML runtime system.

1276 * Type Seq.results and related operations support embedded error

1277 messages within lazy enumerations, and thus allow to provide

1278 informative errors in the absence of any usable results.

1280 * Renamed Position.str_of to Position.here to emphasize that this is a

1281 formal device to inline positions into message text, but not

1282 necessarily printing visible text.

1285 *** System ***

1287 * Advanced support for Isabelle sessions and build management, see

1288 "system" manual for the chapter of that name, especially the "isabelle

1289 build" tool and its examples. The "isabelle mkroot" tool prepares

1290 session root directories for use with "isabelle build", similar to

1291 former "isabelle mkdir" for "isabelle usedir". Note that this affects

1292 document preparation as well. INCOMPATIBILITY, isabelle usedir /

1293 mkdir / make are rendered obsolete.

1295 * Discontinued obsolete Isabelle/build script, it is superseded by the

1296 regular isabelle build tool. For example:

1298 isabelle build -s -b HOL

1300 * Discontinued obsolete "isabelle makeall".

1302 * Discontinued obsolete IsaMakefile and ROOT.ML files from the

1303 Isabelle distribution, except for rudimentary src/HOL/IsaMakefile that

1304 provides some traditional targets that invoke "isabelle build". Note

1305 that this is inefficient! Applications of Isabelle/HOL involving

1306 "isabelle make" should be upgraded to use "isabelle build" directly.

1308 * The "isabelle options" tool prints Isabelle system options, as

1309 required for "isabelle build", for example.

1311 * The "isabelle logo" tool produces EPS and PDF format simultaneously.

1312 Minor INCOMPATIBILITY in command-line options.

1314 * The "isabelle install" tool has now a simpler command-line. Minor

1315 INCOMPATIBILITY.

1317 * The "isabelle components" tool helps to resolve add-on components

1318 that are not bundled, or referenced from a bare-bones repository

1319 version of Isabelle.

1321 * Settings variable ISABELLE_PLATFORM_FAMILY refers to the general

1322 platform family: "linux", "macos", "windows".

1324 * The ML system is configured as regular component, and no longer

1325 picked up from some surrounding directory. Potential INCOMPATIBILITY

1326 for home-made settings.

1328 * Improved ML runtime statistics (heap, threads, future tasks etc.).

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

1331 without exception positions and advanced ML compiler/toplevel

1332 configuration.

1334 * Discontinued special treatment of Proof General -- no longer guess

1335 PROOFGENERAL_HOME based on accidental file-system layout. Minor

1336 INCOMPATIBILITY: provide PROOFGENERAL_HOME and PROOFGENERAL_OPTIONS

1337 settings manually, or use a Proof General version that has been

1338 bundled as Isabelle component.

1342 New in Isabelle2012 (May 2012)

1343 ------------------------------

1345 *** General ***

1347 * Prover IDE (PIDE) improvements:

1349 - more robust Sledgehammer integration (as before the sledgehammer

1350 command-line needs to be typed into the source buffer)

1351 - markup for bound variables

1352 - markup for types of term variables (displayed as tooltips)

1353 - support for user-defined Isar commands within the running session

1354 - improved support for Unicode outside original 16bit range

1355 e.g. glyph for \<A> (thanks to jEdit 4.5.1)

1357 * Forward declaration of outer syntax keywords within the theory

1358 header -- minor INCOMPATIBILITY for user-defined commands. Allow new

1359 commands to be used in the same theory where defined.

1361 * Auxiliary contexts indicate block structure for specifications with

1362 additional parameters and assumptions. Such unnamed contexts may be

1363 nested within other targets, like 'theory', 'locale', 'class',

1364 'instantiation' etc. Results from the local context are generalized

1365 accordingly and applied to the enclosing target context. Example:

1367 context

1368 fixes x y z :: 'a

1369 assumes xy: "x = y" and yz: "y = z"

1370 begin

1372 lemma my_trans: "x = z" using xy yz by simp

1374 end

1376 thm my_trans

1378 The most basic application is to factor-out context elements of

1379 several fixes/assumes/shows theorem statements, e.g. see

1380 ~~/src/HOL/Isar_Examples/Group_Context.thy

1382 Any other local theory specification element works within the "context

1383 ... begin ... end" block as well.

1385 * Bundled declarations associate attributed fact expressions with a

1386 given name in the context. These may be later included in other

1387 contexts. This allows to manage context extensions casually, without

1388 the logical dependencies of locales and locale interpretation. See

1389 commands 'bundle', 'include', 'including' etc. in the isar-ref manual.

1391 * Commands 'lemmas' and 'theorems' allow local variables using 'for'

1392 declaration, and results are standardized before being stored. Thus

1393 old-style "standard" after instantiation or composition of facts

1394 becomes obsolete. Minor INCOMPATIBILITY, due to potential change of

1395 indices of schematic variables.

1397 * Rule attributes in local theory declarations (e.g. locale or class)

1398 are now statically evaluated: the resulting theorem is stored instead

1399 of the original expression. INCOMPATIBILITY in rare situations, where

1400 the historic accident of dynamic re-evaluation in interpretations

1401 etc. was exploited.

1403 * New tutorial "Programming and Proving in Isabelle/HOL"

1404 ("prog-prove"). It completely supersedes "A Tutorial Introduction to

1405 Structured Isar Proofs" ("isar-overview"), which has been removed. It

1406 also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order

1407 Logic" as the recommended beginners tutorial, but does not cover all

1408 of the material of that old tutorial.

1410 * Updated and extended reference manuals: "isar-ref",

1411 "implementation", "system"; reduced remaining material in old "ref"

1412 manual.

1415 *** Pure ***

1417 * Command 'definition' no longer exports the foundational "raw_def"

1418 into the user context. Minor INCOMPATIBILITY, may use the regular

1419 "def" result with attribute "abs_def" to imitate the old version.

1421 * Attribute "abs_def" turns an equation of the form "f x y == t" into

1422 "f == %x y. t", which ensures that "simp" or "unfold" steps always

1423 expand it. This also works for object-logic equality. (Formerly

1424 undocumented feature.)

1426 * Sort constraints are now propagated in simultaneous statements, just

1427 like type constraints. INCOMPATIBILITY in rare situations, where

1428 distinct sorts used to be assigned accidentally. For example:

1430 lemma "P (x::'a::foo)" and "Q (y::'a::bar)" -- "now illegal"

1432 lemma "P (x::'a)" and "Q (y::'a::bar)"

1433 -- "now uniform 'a::bar instead of default sort for first occurrence (!)"

1435 * Rule composition via attribute "OF" (or ML functions OF/MRS) is more

1436 tolerant against multiple unifiers, as long as the final result is

1437 unique. (As before, rules are composed in canonical right-to-left

1438 order to accommodate newly introduced premises.)

1440 * Renamed some inner syntax categories:

1442 num ~> num_token

1443 xnum ~> xnum_token

1444 xstr ~> str_token

1446 Minor INCOMPATIBILITY. Note that in practice "num_const" or

1447 "num_position" etc. are mainly used instead (which also include

1448 position information via constraints).

1450 * Simplified configuration options for syntax ambiguity: see

1451 "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref

1452 manual. Minor INCOMPATIBILITY.

1454 * Discontinued configuration option "syntax_positions": atomic terms

1455 in parse trees are always annotated by position constraints.

1457 * Old code generator for SML and its commands 'code_module',

1458 'code_library', 'consts_code', 'types_code' have been discontinued.

1459 Use commands of the generic code generator instead. INCOMPATIBILITY.

1461 * Redundant attribute "code_inline" has been discontinued. Use

1462 "code_unfold" instead. INCOMPATIBILITY.

1464 * Dropped attribute "code_unfold_post" in favor of the its dual

1465 "code_abbrev", which yields a common pattern in definitions like

1467 definition [code_abbrev]: "f = t"

1469 INCOMPATIBILITY.

1471 * Obsolete 'types' command has been discontinued. Use 'type_synonym'

1472 instead. INCOMPATIBILITY.

1474 * Discontinued old "prems" fact, which used to refer to the accidental

1475 collection of foundational premises in the context (already marked as

1476 legacy since Isabelle2011).

1479 *** HOL ***

1481 * Type 'a set is now a proper type constructor (just as before

1482 Isabelle2008). Definitions mem_def and Collect_def have disappeared.

1483 Non-trivial INCOMPATIBILITY. For developments keeping predicates and

1484 sets separate, it is often sufficient to rephrase some set S that has

1485 been accidentally used as predicates by "%x. x : S", and some

1486 predicate P that has been accidentally used as set by "{x. P x}".

1487 Corresponding proofs in a first step should be pruned from any

1488 tinkering with former theorems mem_def and Collect_def as far as

1489 possible.

1491 For developments which deliberately mix predicates and sets, a

1492 planning step is necessary to determine what should become a predicate

1493 and what a set. It can be helpful to carry out that step in

1494 Isabelle2011-1 before jumping right into the current release.

1496 * Code generation by default implements sets as container type rather

1497 than predicates. INCOMPATIBILITY.

1499 * New type synonym 'a rel = ('a * 'a) set

1501 * The representation of numerals has changed. Datatype "num"

1502 represents strictly positive binary numerals, along with functions

1503 "numeral :: num => 'a" and "neg_numeral :: num => 'a" to represent

1504 positive and negated numeric literals, respectively. See also

1505 definitions in ~~/src/HOL/Num.thy. Potential INCOMPATIBILITY, some

1506 user theories may require adaptations as follows:

1508 - Theorems with number_ring or number_semiring constraints: These

1509 classes are gone; use comm_ring_1 or comm_semiring_1 instead.

1511 - Theories defining numeric types: Remove number, number_semiring,

1512 and number_ring instances. Defer all theorems about numerals until

1513 after classes one and semigroup_add have been instantiated.

1515 - Numeral-only simp rules: Replace each rule having a "number_of v"

1516 pattern with two copies, one for numeral and one for neg_numeral.

1518 - Theorems about subclasses of semiring_1 or ring_1: These classes

1519 automatically support numerals now, so more simp rules and

1520 simprocs may now apply within the proof.

1522 - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:

1523 Redefine using other integer operations.

1525 * Transfer: New package intended to generalize the existing

1526 "descending" method and related theorem attributes from the Quotient

1527 package. (Not all functionality is implemented yet, but future

1528 development will focus on Transfer as an eventual replacement for the

1529 corresponding parts of the Quotient package.)

1531 - transfer_rule attribute: Maintains a collection of transfer rules,

1532 which relate constants at two different types. Transfer rules may

1533 relate different type instances of the same polymorphic constant,

1534 or they may relate an operation on a raw type to a corresponding

1535 operation on an abstract type (quotient or subtype). For example:

1537 ((A ===> B) ===> list_all2 A ===> list_all2 B) map map

1538 (cr_int ===> cr_int ===> cr_int) (%(x,y) (u,v). (x+u, y+v)) plus_int

1540 - transfer method: Replaces a subgoal on abstract types with an

1541 equivalent subgoal on the corresponding raw types. Constants are

1542 replaced with corresponding ones according to the transfer rules.

1543 Goals are generalized over all free variables by default; this is

1544 necessary for variables whose types change, but can be overridden

1545 for specific variables with e.g. "transfer fixing: x y z". The

1546 variant transfer' method allows replacing a subgoal with one that

1547 is logically stronger (rather than equivalent).

1549 - relator_eq attribute: Collects identity laws for relators of

1550 various type constructors, e.g. "list_all2 (op =) = (op =)". The

1551 transfer method uses these lemmas to infer transfer rules for

1552 non-polymorphic constants on the fly.

1554 - transfer_prover method: Assists with proving a transfer rule for a

1555 new constant, provided the constant is defined in terms of other

1556 constants that already have transfer rules. It should be applied

1557 after unfolding the constant definitions.

1559 - HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer

1560 from type nat to type int.

1562 * Lifting: New package intended to generalize the quotient_definition

1563 facility of the Quotient package; designed to work with Transfer.

1565 - lift_definition command: Defines operations on an abstract type in

1566 terms of a corresponding operation on a representation

1567 type. Example syntax:

1569 lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist"

1570 is List.insert

1572 Users must discharge a respectfulness proof obligation when each

1573 constant is defined. (For a type copy, i.e. a typedef with UNIV,

1574 the proof is discharged automatically.) The obligation is

1575 presented in a user-friendly, readable form; a respectfulness

1576 theorem in the standard format and a transfer rule are generated

1577 by the package.

1579 - Integration with code_abstype: For typedefs (e.g. subtypes

1580 corresponding to a datatype invariant, such as dlist),

1581 lift_definition generates a code certificate theorem and sets up

1582 code generation for each constant.

1584 - setup_lifting command: Sets up the Lifting package to work with a

1585 user-defined type. The user must provide either a quotient theorem

1586 or a type_definition theorem. The package configures transfer

1587 rules for equality and quantifiers on the type, and sets up the

1588 lift_definition command to work with the type.

1590 - Usage examples: See Quotient_Examples/Lift_DList.thy,

1591 Quotient_Examples/Lift_RBT.thy, Quotient_Examples/Lift_FSet.thy,

1592 Word/Word.thy and Library/Float.thy.

1594 * Quotient package:

1596 - The 'quotient_type' command now supports a 'morphisms' option with

1597 rep and abs functions, similar to typedef.

1599 - 'quotient_type' sets up new types to work with the Lifting and

1600 Transfer packages, as with 'setup_lifting'.

1602 - The 'quotient_definition' command now requires the user to prove a

1603 respectfulness property at the point where the constant is

1604 defined, similar to lift_definition; INCOMPATIBILITY.

1606 - Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems

1607 accordingly, INCOMPATIBILITY.

1609 * New diagnostic command 'find_unused_assms' to find potentially

1610 superfluous assumptions in theorems using Quickcheck.

1612 * Quickcheck:

1614 - Quickcheck returns variable assignments as counterexamples, which

1615 allows to reveal the underspecification of functions under test.

1616 For example, refuting "hd xs = x", it presents the variable

1617 assignment xs = [] and x = a1 as a counterexample, assuming that

1618 any property is false whenever "hd []" occurs in it.

1620 These counterexample are marked as potentially spurious, as

1621 Quickcheck also returns "xs = []" as a counterexample to the

1622 obvious theorem "hd xs = hd xs".

1624 After finding a potentially spurious counterexample, Quickcheck

1625 continues searching for genuine ones.

1627 By default, Quickcheck shows potentially spurious and genuine

1628 counterexamples. The option "genuine_only" sets quickcheck to only

1629 show genuine counterexamples.

1631 - The command 'quickcheck_generator' creates random and exhaustive

1632 value generators for a given type and operations.

1634 It generates values by using the operations as if they were

1635 constructors of that type.

1637 - Support for multisets.

1639 - Added "use_subtype" options.

1641 - Added "quickcheck_locale" configuration to specify how to process

1642 conjectures in a locale context.

1644 * Nitpick: Fixed infinite loop caused by the 'peephole_optim' option

1645 and affecting 'rat' and 'real'.

1647 * Sledgehammer:

1648 - Integrated more tightly with SPASS, as described in the ITP 2012

1649 paper "More SPASS with Isabelle".

1650 - Made it try "smt" as a fallback if "metis" fails or times out.

1651 - Added support for the following provers: Alt-Ergo (via Why3 and

1652 TFF1), iProver, iProver-Eq.

1653 - Sped up the minimizer.

1654 - Added "lam_trans", "uncurry_aliases", and "minimize" options.

1655 - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").

1656 - Renamed "sound" option to "strict".

1658 * Metis: Added possibility to specify lambda translations scheme as a

1659 parenthesized argument (e.g., "by (metis (lifting) ...)").

1661 * SMT: Renamed "smt_fixed" option to "smt_read_only_certificates".

1663 * Command 'try0': Renamed from 'try_methods'. INCOMPATIBILITY.

1665 * New "case_product" attribute to generate a case rule doing multiple

1666 case distinctions at the same time. E.g.

1668 list.exhaust [case_product nat.exhaust]

1670 produces a rule which can be used to perform case distinction on both

1671 a list and a nat.

1673 * New "eventually_elim" method as a generalized variant of the

1674 eventually_elim* rules. Supports structured proofs.

1676 * Typedef with implicit set definition is considered legacy. Use

1677 "typedef (open)" form instead, which will eventually become the

1678 default.

1680 * Record: code generation can be switched off manually with

1682 declare [[record_coden = false]] -- "default true"

1684 * Datatype: type parameters allow explicit sort constraints.

1686 * Concrete syntax for case expressions includes constraints for source

1687 positions, and thus produces Prover IDE markup for its bindings.

1688 INCOMPATIBILITY for old-style syntax translations that augment the

1689 pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of

1690 one_case.

1692 * Clarified attribute "mono_set": pure declaration without modifying

1693 the result of the fact expression.

1695 * More default pred/set conversions on a couple of relation operations

1696 and predicates. Added powers of predicate relations. Consolidation

1697 of some relation theorems:

1699 converse_def ~> converse_unfold

1700 rel_comp_def ~> relcomp_unfold

1701 symp_def ~> (modified, use symp_def and sym_def instead)

1702 transp_def ~> transp_trans

1703 Domain_def ~> Domain_unfold

1704 Range_def ~> Domain_converse [symmetric]

1706 Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2.

1708 See theory "Relation" for examples for making use of pred/set

1709 conversions by means of attributes "to_set" and "to_pred".

1711 INCOMPATIBILITY.

1713 * Renamed facts about the power operation on relations, i.e., relpow

1714 to match the constant's name:

1716 rel_pow_1 ~> relpow_1

1717 rel_pow_0_I ~> relpow_0_I

1718 rel_pow_Suc_I ~> relpow_Suc_I

1719 rel_pow_Suc_I2 ~> relpow_Suc_I2

1720 rel_pow_0_E ~> relpow_0_E

1721 rel_pow_Suc_E ~> relpow_Suc_E

1722 rel_pow_E ~> relpow_E

1723 rel_pow_Suc_D2 ~> relpow_Suc_D2

1724 rel_pow_Suc_E2 ~> relpow_Suc_E2

1725 rel_pow_Suc_D2' ~> relpow_Suc_D2'

1726 rel_pow_E2 ~> relpow_E2

1727 rel_pow_add ~> relpow_add

1728 rel_pow_commute ~> relpow

1729 rel_pow_empty ~> relpow_empty:

1730 rtrancl_imp_UN_rel_pow ~> rtrancl_imp_UN_relpow

1731 rel_pow_imp_rtrancl ~> relpow_imp_rtrancl

1732 rtrancl_is_UN_rel_pow ~> rtrancl_is_UN_relpow

1733 rtrancl_imp_rel_pow ~> rtrancl_imp_relpow

1734 rel_pow_fun_conv ~> relpow_fun_conv

1735 rel_pow_finite_bounded1 ~> relpow_finite_bounded1

1736 rel_pow_finite_bounded ~> relpow_finite_bounded

1737 rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow

1738 trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow

1739 single_valued_rel_pow ~> single_valued_relpow

1741 INCOMPATIBILITY.

1743 * Theory Relation: Consolidated constant name for relation composition

1744 and corresponding theorem names:

1746 - Renamed constant rel_comp to relcomp.

1748 - Dropped abbreviation pred_comp. Use relcompp instead.

1750 - Renamed theorems:

1752 rel_compI ~> relcompI

1753 rel_compEpair ~> relcompEpair

1754 rel_compE ~> relcompE

1755 pred_comp_rel_comp_eq ~> relcompp_relcomp_eq

1756 rel_comp_empty1 ~> relcomp_empty1

1757 rel_comp_mono ~> relcomp_mono

1758 rel_comp_subset_Sigma ~> relcomp_subset_Sigma

1759 rel_comp_distrib ~> relcomp_distrib

1760 rel_comp_distrib2 ~> relcomp_distrib2

1761 rel_comp_UNION_distrib ~> relcomp_UNION_distrib

1762 rel_comp_UNION_distrib2 ~> relcomp_UNION_distrib2

1763 single_valued_rel_comp ~> single_valued_relcomp

1764 rel_comp_def ~> relcomp_unfold

1765 converse_rel_comp ~> converse_relcomp

1766 pred_compI ~> relcomppI

1767 pred_compE ~> relcomppE

1768 pred_comp_bot1 ~> relcompp_bot1

1769 pred_comp_bot2 ~> relcompp_bot2

1770 transp_pred_comp_less_eq ~> transp_relcompp_less_eq

1771 pred_comp_mono ~> relcompp_mono

1772 pred_comp_distrib ~> relcompp_distrib

1773 pred_comp_distrib2 ~> relcompp_distrib2

1774 converse_pred_comp ~> converse_relcompp

1776 finite_rel_comp ~> finite_relcomp

1778 set_rel_comp ~> set_relcomp

1780 INCOMPATIBILITY.

1782 * Theory Divides: Discontinued redundant theorems about div and mod.

1783 INCOMPATIBILITY, use the corresponding generic theorems instead.

1785 DIVISION_BY_ZERO ~> div_by_0, mod_by_0

1786 zdiv_self ~> div_self

1787 zmod_self ~> mod_self

1788 zdiv_zero ~> div_0

1789 zmod_zero ~> mod_0

1790 zdiv_zmod_equality ~> div_mod_equality2

1791 zdiv_zmod_equality2 ~> div_mod_equality

1792 zmod_zdiv_trivial ~> mod_div_trivial

1793 zdiv_zminus_zminus ~> div_minus_minus

1794 zmod_zminus_zminus ~> mod_minus_minus

1795 zdiv_zminus2 ~> div_minus_right

1796 zmod_zminus2 ~> mod_minus_right

1797 zdiv_minus1_right ~> div_minus1_right

1798 zmod_minus1_right ~> mod_minus1_right

1799 zdvd_mult_div_cancel ~> dvd_mult_div_cancel

1800 zmod_zmult1_eq ~> mod_mult_right_eq

1801 zpower_zmod ~> power_mod

1802 zdvd_zmod ~> dvd_mod

1803 zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd

1804 mod_mult_distrib ~> mult_mod_left

1805 mod_mult_distrib2 ~> mult_mod_right

1807 * Removed redundant theorems nat_mult_2 and nat_mult_2_right; use

1808 generic mult_2 and mult_2_right instead. INCOMPATIBILITY.

1810 * Finite_Set.fold now qualified. INCOMPATIBILITY.

1812 * Consolidated theorem names concerning fold combinators:

1814 inf_INFI_fold_inf ~> inf_INF_fold_inf

1815 sup_SUPR_fold_sup ~> sup_SUP_fold_sup

1816 INFI_fold_inf ~> INF_fold_inf

1817 SUPR_fold_sup ~> SUP_fold_sup

1818 union_set ~> union_set_fold

1819 minus_set ~> minus_set_fold

1820 INFI_set_fold ~> INF_set_fold

1821 SUPR_set_fold ~> SUP_set_fold

1822 INF_code ~> INF_set_foldr

1823 SUP_code ~> SUP_set_foldr

1824 foldr.simps ~> foldr.simps (in point-free formulation)

1825 foldr_fold_rev ~> foldr_conv_fold

1826 foldl_fold ~> foldl_conv_fold

1827 foldr_foldr ~> foldr_conv_foldl

1828 foldl_foldr ~> foldl_conv_foldr

1829 fold_set_remdups ~> fold_set_fold_remdups

1830 fold_set ~> fold_set_fold

1831 fold1_set ~> fold1_set_fold

1833 INCOMPATIBILITY.

1835 * Dropped rarely useful theorems concerning fold combinators:

1836 foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant,

1837 rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,

1838 concat_conv_foldl, foldl_weak_invariant, foldl_invariant,

1839 foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,

1840 listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc,

1841 foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv.

1842 INCOMPATIBILITY. For the common phrases "%xs. List.foldr plus xs 0"

1843 and "List.foldl plus 0", prefer "List.listsum". Otherwise it can be

1844 useful to boil down "List.foldr" and "List.foldl" to "List.fold" by

1845 unfolding "foldr_conv_fold" and "foldl_conv_fold".

1847 * Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr,

1848 inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr,

1849 Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr,

1850 INF_set_foldr, SUP_set_foldr. INCOMPATIBILITY. Prefer corresponding

1851 lemmas over fold rather than foldr, or make use of lemmas

1852 fold_conv_foldr and fold_rev.

1854 * Congruence rules Option.map_cong and Option.bind_cong for recursion

1855 through option types.

1857 * "Transitive_Closure.ntrancl": bounded transitive closure on

1858 relations.

1860 * Constant "Set.not_member" now qualified. INCOMPATIBILITY.

1862 * Theory Int: Discontinued many legacy theorems specific to type int.

1863 INCOMPATIBILITY, use the corresponding generic theorems instead.

1865 zminus_zminus ~> minus_minus

1866 zminus_0 ~> minus_zero

1867 zminus_zadd_distrib ~> minus_add_distrib

1868 zadd_commute ~> add_commute

1869 zadd_assoc ~> add_assoc

1870 zadd_left_commute ~> add_left_commute

1871 zadd_ac ~> add_ac

1872 zmult_ac ~> mult_ac

1873 zadd_0 ~> add_0_left

1874 zadd_0_right ~> add_0_right

1875 zadd_zminus_inverse2 ~> left_minus

1876 zmult_zminus ~> mult_minus_left

1877 zmult_commute ~> mult_commute

1878 zmult_assoc ~> mult_assoc

1879 zadd_zmult_distrib ~> left_distrib

1880 zadd_zmult_distrib2 ~> right_distrib

1881 zdiff_zmult_distrib ~> left_diff_distrib

1882 zdiff_zmult_distrib2 ~> right_diff_distrib

1883 zmult_1 ~> mult_1_left

1884 zmult_1_right ~> mult_1_right

1885 zle_refl ~> order_refl

1886 zle_trans ~> order_trans

1887 zle_antisym ~> order_antisym

1888 zle_linear ~> linorder_linear

1889 zless_linear ~> linorder_less_linear

1890 zadd_left_mono ~> add_left_mono

1891 zadd_strict_right_mono ~> add_strict_right_mono

1892 zadd_zless_mono ~> add_less_le_mono

1893 int_0_less_1 ~> zero_less_one

1894 int_0_neq_1 ~> zero_neq_one

1895 zless_le ~> less_le

1896 zpower_zadd_distrib ~> power_add

1897 zero_less_zpower_abs_iff ~> zero_less_power_abs_iff

1898 zero_le_zpower_abs ~> zero_le_power_abs

1900 * Theory Deriv: Renamed

1902 DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing

1904 * Theory Library/Multiset: Improved code generation of multisets.

1906 * Theory HOL/Library/Set_Algebras: Addition and multiplication on sets

1907 are expressed via type classes again. The special syntax

1908 \<oplus>/\<otimes> has been replaced by plain +/*. Removed constant

1909 setsum_set, which is now subsumed by Big_Operators.setsum.

1910 INCOMPATIBILITY.

1912 * Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,

1913 use theory HOL/Library/Nat_Bijection instead.

1915 * Theory HOL/Library/RBT_Impl: Backing implementation of red-black

1916 trees is now inside a type class context. Names of affected

1917 operations and lemmas have been prefixed by rbt_. INCOMPATIBILITY for

1918 theories working directly with raw red-black trees, adapt the names as

1919 follows:

1921 Operations:

1922 bulkload -> rbt_bulkload

1923 del_from_left -> rbt_del_from_left

1924 del_from_right -> rbt_del_from_right

1925 del -> rbt_del

1926 delete -> rbt_delete

1927 ins -> rbt_ins

1928 insert -> rbt_insert

1929 insertw -> rbt_insert_with

1930 insert_with_key -> rbt_insert_with_key

1931 map_entry -> rbt_map_entry

1932 lookup -> rbt_lookup

1933 sorted -> rbt_sorted

1934 tree_greater -> rbt_greater

1935 tree_less -> rbt_less

1936 tree_less_symbol -> rbt_less_symbol

1937 union -> rbt_union

1938 union_with -> rbt_union_with

1939 union_with_key -> rbt_union_with_key

1941 Lemmas:

1942 balance_left_sorted -> balance_left_rbt_sorted

1943 balance_left_tree_greater -> balance_left_rbt_greater

1944 balance_left_tree_less -> balance_left_rbt_less

1945 balance_right_sorted -> balance_right_rbt_sorted

1946 balance_right_tree_greater -> balance_right_rbt_greater

1947 balance_right_tree_less -> balance_right_rbt_less

1948 balance_sorted -> balance_rbt_sorted

1949 balance_tree_greater -> balance_rbt_greater

1950 balance_tree_less -> balance_rbt_less

1951 bulkload_is_rbt -> rbt_bulkload_is_rbt

1952 combine_sorted -> combine_rbt_sorted

1953 combine_tree_greater -> combine_rbt_greater

1954 combine_tree_less -> combine_rbt_less

1955 delete_in_tree -> rbt_delete_in_tree

1956 delete_is_rbt -> rbt_delete_is_rbt

1957 del_from_left_tree_greater -> rbt_del_from_left_rbt_greater

1958 del_from_left_tree_less -> rbt_del_from_left_rbt_less

1959 del_from_right_tree_greater -> rbt_del_from_right_rbt_greater

1960 del_from_right_tree_less -> rbt_del_from_right_rbt_less

1961 del_in_tree -> rbt_del_in_tree

1962 del_inv1_inv2 -> rbt_del_inv1_inv2

1963 del_sorted -> rbt_del_rbt_sorted

1964 del_tree_greater -> rbt_del_rbt_greater

1965 del_tree_less -> rbt_del_rbt_less

1966 dom_lookup_Branch -> dom_rbt_lookup_Branch

1967 entries_lookup -> entries_rbt_lookup

1968 finite_dom_lookup -> finite_dom_rbt_lookup

1969 insert_sorted -> rbt_insert_rbt_sorted

1970 insertw_is_rbt -> rbt_insertw_is_rbt

1971 insertwk_is_rbt -> rbt_insertwk_is_rbt

1972 insertwk_sorted -> rbt_insertwk_rbt_sorted

1973 insertw_sorted -> rbt_insertw_rbt_sorted

1974 ins_sorted -> ins_rbt_sorted

1975 ins_tree_greater -> ins_rbt_greater

1976 ins_tree_less -> ins_rbt_less

1977 is_rbt_sorted -> is_rbt_rbt_sorted

1978 lookup_balance -> rbt_lookup_balance

1979 lookup_bulkload -> rbt_lookup_rbt_bulkload

1980 lookup_delete -> rbt_lookup_rbt_delete

1981 lookup_Empty -> rbt_lookup_Empty

1982 lookup_from_in_tree -> rbt_lookup_from_in_tree

1983 lookup_in_tree -> rbt_lookup_in_tree

1984 lookup_ins -> rbt_lookup_ins

1985 lookup_insert -> rbt_lookup_rbt_insert

1986 lookup_insertw -> rbt_lookup_rbt_insertw

1987 lookup_insertwk -> rbt_lookup_rbt_insertwk

1988 lookup_keys -> rbt_lookup_keys

1989 lookup_map -> rbt_lookup_map

1990 lookup_map_entry -> rbt_lookup_rbt_map_entry

1991 lookup_tree_greater -> rbt_lookup_rbt_greater

1992 lookup_tree_less -> rbt_lookup_rbt_less

1993 lookup_union -> rbt_lookup_rbt_union

1994 map_entry_color_of -> rbt_map_entry_color_of

1995 map_entry_inv1 -> rbt_map_entry_inv1

1996 map_entry_inv2 -> rbt_map_entry_inv2

1997 map_entry_is_rbt -> rbt_map_entry_is_rbt

1998 map_entry_sorted -> rbt_map_entry_rbt_sorted

1999 map_entry_tree_greater -> rbt_map_entry_rbt_greater

2000 map_entry_tree_less -> rbt_map_entry_rbt_less

2001 map_tree_greater -> map_rbt_greater

2002 map_tree_less -> map_rbt_less

2003 map_sorted -> map_rbt_sorted

2004 paint_sorted -> paint_rbt_sorted

2005 paint_lookup -> paint_rbt_lookup

2006 paint_tree_greater -> paint_rbt_greater

2007 paint_tree_less -> paint_rbt_less

2008 sorted_entries -> rbt_sorted_entries

2009 tree_greater_eq_trans -> rbt_greater_eq_trans

2010 tree_greater_nit -> rbt_greater_nit

2011 tree_greater_prop -> rbt_greater_prop

2012 tree_greater_simps -> rbt_greater_simps

2013 tree_greater_trans -> rbt_greater_trans

2014 tree_less_eq_trans -> rbt_less_eq_trans

2015 tree_less_nit -> rbt_less_nit

2016 tree_less_prop -> rbt_less_prop

2017 tree_less_simps -> rbt_less_simps

2018 tree_less_trans -> rbt_less_trans

2019 tree_ord_props -> rbt_ord_props

2020 union_Branch -> rbt_union_Branch

2021 union_is_rbt -> rbt_union_is_rbt

2022 unionw_is_rbt -> rbt_unionw_is_rbt

2023 unionwk_is_rbt -> rbt_unionwk_is_rbt

2024 unionwk_sorted -> rbt_unionwk_rbt_sorted

2026 * Theory HOL/Library/Float: Floating point numbers are now defined as

2027 a subset of the real numbers. All operations are defined using the

2028 lifing-framework and proofs use the transfer method. INCOMPATIBILITY.

2030 Changed Operations:

2031 float_abs -> abs

2032 float_nprt -> nprt

2033 float_pprt -> pprt

2034 pow2 -> use powr

2035 round_down -> float_round_down

2036 round_up -> float_round_up

2037 scale -> exponent

2039 Removed Operations:

2040 ceiling_fl, lb_mult, lb_mod, ub_mult, ub_mod

2042 Renamed Lemmas:

2043 abs_float_def -> Float.compute_float_abs

2044 bitlen_ge0 -> bitlen_nonneg

2045 bitlen.simps -> Float.compute_bitlen

2046 float_components -> Float_mantissa_exponent

2047 float_divl.simps -> Float.compute_float_divl

2048 float_divr.simps -> Float.compute_float_divr

2049 float_eq_odd -> mult_powr_eq_mult_powr_iff

2050 float_power -> real_of_float_power

2051 lapprox_posrat_def -> Float.compute_lapprox_posrat

2052 lapprox_rat.simps -> Float.compute_lapprox_rat

2053 le_float_def' -> Float.compute_float_le

2054 le_float_def -> less_eq_float.rep_eq

2055 less_float_def' -> Float.compute_float_less

2056 less_float_def -> less_float.rep_eq

2057 normfloat_def -> Float.compute_normfloat

2058 normfloat_imp_odd_or_zero -> mantissa_not_dvd and mantissa_noteq_0

2059 normfloat -> normfloat_def

2060 normfloat_unique -> use normfloat_def

2061 number_of_float_Float -> Float.compute_float_numeral, Float.compute_float_neg_numeral

2062 one_float_def -> Float.compute_float_one

2063 plus_float_def -> Float.compute_float_plus

2064 rapprox_posrat_def -> Float.compute_rapprox_posrat

2065 rapprox_rat.simps -> Float.compute_rapprox_rat

2066 real_of_float_0 -> zero_float.rep_eq

2067 real_of_float_1 -> one_float.rep_eq

2068 real_of_float_abs -> abs_float.rep_eq

2069 real_of_float_add -> plus_float.rep_eq

2070 real_of_float_minus -> uminus_float.rep_eq

2071 real_of_float_mult -> times_float.rep_eq

2072 real_of_float_simp -> Float.rep_eq

2073 real_of_float_sub -> minus_float.rep_eq

2074 round_down.simps -> Float.compute_float_round_down

2075 round_up.simps -> Float.compute_float_round_up

2076 times_float_def -> Float.compute_float_times

2077 uminus_float_def -> Float.compute_float_uminus

2078 zero_float_def -> Float.compute_float_zero

2080 Lemmas not necessary anymore, use the transfer method:

2081 bitlen_B0, bitlen_B1, bitlen_ge1, bitlen_Min, bitlen_Pls, float_divl,

2082 float_divr, float_le_simp, float_less1_mantissa_bound,

2083 float_less_simp, float_less_zero, float_le_zero,

2084 float_pos_less1_e_neg, float_pos_m_pos, float_split, float_split2,

2085 floor_pos_exp, lapprox_posrat, lapprox_posrat_bottom, lapprox_rat,

2086 lapprox_rat_bottom, normalized_float, rapprox_posrat,

2087 rapprox_posrat_le1, rapprox_rat, real_of_float_ge0_exp,

2088 real_of_float_neg_exp, real_of_float_nge0_exp, round_down floor_fl,

2089 round_up, zero_le_float, zero_less_float

2091 * New theory HOL/Library/DAList provides an abstract type for

2092 association lists with distinct keys.

2094 * Session HOL/IMP: Added new theory of abstract interpretation of

2095 annotated commands.

2097 * Session HOL-Import: Re-implementation from scratch is faster,

2098 simpler, and more scalable. Requires a proof bundle, which is

2099 available as an external component. Discontinued old (and mostly

2100 dead) Importer for HOL4 and HOL Light. INCOMPATIBILITY.

2102 * Session HOL-Word: Discontinued many redundant theorems specific to

2103 type 'a word. INCOMPATIBILITY, use the corresponding generic theorems

2104 instead.

2106 word_sub_alt ~> word_sub_wi

2107 word_add_alt ~> word_add_def

2108 word_mult_alt ~> word_mult_def

2109 word_minus_alt ~> word_minus_def

2110 word_0_alt ~> word_0_wi

2111 word_1_alt ~> word_1_wi

2112 word_add_0 ~> add_0_left

2113 word_add_0_right ~> add_0_right

2114 word_mult_1 ~> mult_1_left

2115 word_mult_1_right ~> mult_1_right

2116 word_add_commute ~> add_commute

2117 word_add_assoc ~> add_assoc

2118 word_add_left_commute ~> add_left_commute

2119 word_mult_commute ~> mult_commute

2120 word_mult_assoc ~> mult_assoc

2121 word_mult_left_commute ~> mult_left_commute

2122 word_left_distrib ~> left_distrib

2123 word_right_distrib ~> right_distrib

2124 word_left_minus ~> left_minus

2125 word_diff_0_right ~> diff_0_right

2126 word_diff_self ~> diff_self

2127 word_sub_def ~> diff_minus

2128 word_diff_minus ~> diff_minus

2129 word_add_ac ~> add_ac

2130 word_mult_ac ~> mult_ac

2131 word_plus_ac0 ~> add_0_left add_0_right add_ac

2132 word_times_ac1 ~> mult_1_left mult_1_right mult_ac

2133 word_order_trans ~> order_trans

2134 word_order_refl ~> order_refl

2135 word_order_antisym ~> order_antisym

2136 word_order_linear ~> linorder_linear

2137 lenw1_zero_neq_one ~> zero_neq_one

2138 word_number_of_eq ~> number_of_eq

2139 word_of_int_add_hom ~> wi_hom_add

2140 word_of_int_sub_hom ~> wi_hom_sub

2141 word_of_int_mult_hom ~> wi_hom_mult

2142 word_of_int_minus_hom ~> wi_hom_neg

2143 word_of_int_succ_hom ~> wi_hom_succ

2144 word_of_int_pred_hom ~> wi_hom_pred

2145 word_of_int_0_hom ~> word_0_wi

2146 word_of_int_1_hom ~> word_1_wi

2148 * Session HOL-Word: New proof method "word_bitwise" for splitting

2149 machine word equalities and inequalities into logical circuits,

2150 defined in HOL/Word/WordBitwise.thy. Supports addition, subtraction,

2151 multiplication, shifting by constants, bitwise operators and numeric

2152 constants. Requires fixed-length word types, not 'a word. Solves

2153 many standard word identities outright and converts more into first

2154 order problems amenable to blast or similar. See also examples in

2155 HOL/Word/Examples/WordExamples.thy.

2157 * Session HOL-Probability: Introduced the type "'a measure" to

2158 represent measures, this replaces the records 'a algebra and 'a

2159 measure_space. The locales based on subset_class now have two

2160 locale-parameters the space \<Omega> and the set of measurable sets M.

2161 The product of probability spaces uses now the same constant as the

2162 finite product of sigma-finite measure spaces "PiM :: ('i => 'a)

2163 measure". Most constants are defined now outside of locales and gain

2164 an additional parameter, like null_sets, almost_eventually or \<mu>'.

2165 Measure space constructions for distributions and densities now got

2166 their own constants distr and density. Instead of using locales to

2167 describe measure spaces with a finite space, the measure count_space

2168 and point_measure is introduced. INCOMPATIBILITY.

2170 Renamed constants:

2171 measure -> emeasure

2172 finite_measure.\<mu>' -> measure

2173 product_algebra_generator -> prod_algebra

2174 product_prob_space.emb -> prod_emb

2175 product_prob_space.infprod_algebra -> PiM

2177 Removed locales:

2178 completeable_measure_space

2179 finite_measure_space

2180 finite_prob_space

2181 finite_product_finite_prob_space

2182 finite_product_sigma_algebra

2183 finite_sigma_algebra

2184 measure_space

2185 pair_finite_prob_space

2186 pair_finite_sigma_algebra

2187 pair_finite_space

2188 pair_sigma_algebra

2189 product_sigma_algebra

2191 Removed constants:

2192 conditional_space

2193 distribution -> use distr measure, or distributed predicate

2194 image_space

2195 joint_distribution -> use distr measure, or distributed predicate

2196 pair_measure_generator

2197 product_prob_space.infprod_algebra -> use PiM

2198 subvimage

2200 Replacement theorems:

2201 finite_additivity_sufficient -> ring_of_sets.countably_additiveI_finite

2202 finite_measure.empty_measure -> measure_empty

2203 finite_measure.finite_continuity_from_above -> finite_measure.finite_Lim_measure_decseq

2204 finite_measure.finite_continuity_from_below -> finite_measure.finite_Lim_measure_incseq

2205 finite_measure.finite_measure_countably_subadditive -> finite_measure.finite_measure_subadditive_countably

2206 finite_measure.finite_measure_eq -> finite_measure.emeasure_eq_measure

2207 finite_measure.finite_measure -> finite_measure.emeasure_finite

2208 finite_measure.finite_measure_finite_singleton -> finite_measure.finite_measure_eq_setsum_singleton

2209 finite_measure.positive_measure' -> measure_nonneg

2210 finite_measure.real_measure -> finite_measure.emeasure_real

2211 finite_product_prob_space.finite_measure_times -> finite_product_prob_space.finite_measure_PiM_emb

2212 finite_product_sigma_algebra.in_P -> sets_PiM_I_finite

2213 finite_product_sigma_algebra.P_empty -> space_PiM_empty, sets_PiM_empty

2214 information_space.conditional_entropy_eq -> information_space.conditional_entropy_simple_distributed

2215 information_space.conditional_entropy_positive -> information_space.conditional_entropy_nonneg_simple

2216 information_space.conditional_mutual_information_eq_mutual_information -> information_space.conditional_mutual_information_eq_mutual_information_simple

2217 information_space.conditional_mutual_information_generic_positive -> information_space.conditional_mutual_information_nonneg_simple

2218 information_space.conditional_mutual_information_positive -> information_space.conditional_mutual_information_nonneg_simple

2219 information_space.entropy_commute -> information_space.entropy_commute_simple

2220 information_space.entropy_eq -> information_space.entropy_simple_distributed

2221 information_space.entropy_generic_eq -> information_space.entropy_simple_distributed

2222 information_space.entropy_positive -> information_space.entropy_nonneg_simple

2223 information_space.entropy_uniform_max -> information_space.entropy_uniform

2224 information_space.KL_eq_0_imp -> information_space.KL_eq_0_iff_eq

2225 information_space.KL_eq_0 -> information_space.KL_same_eq_0

2226 information_space.KL_ge_0 -> information_space.KL_nonneg

2227 information_space.mutual_information_eq -> information_space.mutual_information_simple_distributed

2228 information_space.mutual_information_positive -> information_space.mutual_information_nonneg_simple

2229 Int_stable_cuboids -> Int_stable_atLeastAtMost

2230 Int_stable_product_algebra_generator -> positive_integral

2231 measure_preserving -> equality "distr M N f = N" "f : measurable M N"

2232 measure_space.additive -> emeasure_additive

2233 measure_space.AE_iff_null_set -> AE_iff_null

2234 measure_space.almost_everywhere_def -> eventually_ae_filter

2235 measure_space.almost_everywhere_vimage -> AE_distrD

2236 measure_space.continuity_from_above -> INF_emeasure_decseq

2237 measure_space.continuity_from_above_Lim -> Lim_emeasure_decseq

2238 measure_space.continuity_from_below_Lim -> Lim_emeasure_incseq

2239 measure_space.continuity_from_below -> SUP_emeasure_incseq

2240 measure_space_density -> emeasure_density

2241 measure_space.density_is_absolutely_continuous -> absolutely_continuousI_density

2242 measure_space.integrable_vimage -> integrable_distr

2243 measure_space.integral_translated_density -> integral_density

2244 measure_space.integral_vimage -> integral_distr

2245 measure_space.measure_additive -> plus_emeasure

2246 measure_space.measure_compl -> emeasure_compl

2247 measure_space.measure_countable_increasing -> emeasure_countable_increasing

2248 measure_space.measure_countably_subadditive -> emeasure_subadditive_countably

2249 measure_space.measure_decseq -> decseq_emeasure

2250 measure_space.measure_Diff -> emeasure_Diff

2251 measure_space.measure_Diff_null_set -> emeasure_Diff_null_set

2252 measure_space.measure_eq_0 -> emeasure_eq_0

2253 measure_space.measure_finitely_subadditive -> emeasure_subadditive_finite

2254 measure_space.measure_finite_singleton -> emeasure_eq_setsum_singleton

2255 measure_space.measure_incseq -> incseq_emeasure

2256 measure_space.measure_insert -> emeasure_insert

2257 measure_space.measure_mono -> emeasure_mono

2258 measure_space.measure_not_negative -> emeasure_not_MInf

2259 measure_space.measure_preserving_Int_stable -> measure_eqI_generator_eq

2260 measure_space.measure_setsum -> setsum_emeasure

2261 measure_space.measure_setsum_split -> setsum_emeasure_cover

2262 measure_space.measure_space_vimage -> emeasure_distr

2263 measure_space.measure_subadditive_finite -> emeasure_subadditive_finite

2264 measure_space.measure_subadditive -> subadditive

2265 measure_space.measure_top -> emeasure_space

2266 measure_space.measure_UN_eq_0 -> emeasure_UN_eq_0

2267 measure_space.measure_Un_null_set -> emeasure_Un_null_set

2268 measure_space.positive_integral_translated_density -> positive_integral_density

2269 measure_space.positive_integral_vimage -> positive_integral_distr

2270 measure_space.real_continuity_from_above -> Lim_measure_decseq

2271 measure_space.real_continuity_from_below -> Lim_measure_incseq

2272 measure_space.real_measure_countably_subadditive -> measure_subadditive_countably

2273 measure_space.real_measure_Diff -> measure_Diff

2274 measure_space.real_measure_finite_Union -> measure_finite_Union

2275 measure_space.real_measure_setsum_singleton -> measure_eq_setsum_singleton

2276 measure_space.real_measure_subadditive -> measure_subadditive

2277 measure_space.real_measure_Union -> measure_Union

2278 measure_space.real_measure_UNION -> measure_UNION

2279 measure_space.simple_function_vimage -> simple_function_comp

2280 measure_space.simple_integral_vimage -> simple_integral_distr

2281 measure_space.simple_integral_vimage -> simple_integral_distr

2282 measure_unique_Int_stable -> measure_eqI_generator_eq

2283 measure_unique_Int_stable_vimage -> measure_eqI_generator_eq

2284 pair_sigma_algebra.measurable_cut_fst -> sets_Pair1

2285 pair_sigma_algebra.measurable_cut_snd -> sets_Pair2

2286 pair_sigma_algebra.measurable_pair_image_fst -> measurable_Pair1

2287 pair_sigma_algebra.measurable_pair_image_snd -> measurable_Pair2

2288 pair_sigma_algebra.measurable_product_swap -> measurable_pair_swap_iff

2289 pair_sigma_algebra.pair_sigma_algebra_measurable -> measurable_pair_swap

2290 pair_sigma_algebra.pair_sigma_algebra_swap_measurable -> measurable_pair_swap'

2291 pair_sigma_algebra.sets_swap -> sets_pair_swap

2292 pair_sigma_finite.measure_cut_measurable_fst -> pair_sigma_finite.measurable_emeasure_Pair1

2293 pair_sigma_finite.measure_cut_measurable_snd -> pair_sigma_finite.measurable_emeasure_Pair2

2294 pair_sigma_finite.measure_preserving_swap -> pair_sigma_finite.distr_pair_swap

2295 pair_sigma_finite.pair_measure_alt2 -> pair_sigma_finite.emeasure_pair_measure_alt2

2296 pair_sigma_finite.pair_measure_alt -> pair_sigma_finite.emeasure_pair_measure_alt

2297 pair_sigma_finite.pair_measure_times -> pair_sigma_finite.emeasure_pair_measure_Times

2298 prob_space.indep_distribution_eq_measure -> prob_space.indep_vars_iff_distr_eq_PiM

2299 prob_space.indep_var_distributionD -> prob_space.indep_var_distribution_eq

2300 prob_space.measure_space_1 -> prob_space.emeasure_space_1

2301 prob_space.prob_space_vimage -> prob_space_distr

2302 prob_space.random_variable_restrict -> measurable_restrict

2303 prob_space_unique_Int_stable -> measure_eqI_prob_space

2304 product_algebraE -> prod_algebraE_all

2305 product_algebra_generator_der -> prod_algebra_eq_finite

2306 product_algebra_generator_into_space -> prod_algebra_sets_into_space

2307 product_algebraI -> sets_PiM_I_finite

2308 product_measure_exists -> product_sigma_finite.sigma_finite

2309 product_prob_space.finite_index_eq_finite_product -> product_prob_space.sets_PiM_generator

2310 product_prob_space.finite_measure_infprod_emb_Pi -> product_prob_space.measure_PiM_emb

2311 product_prob_space.infprod_spec -> product_prob_space.emeasure_PiM_emb_not_empty

2312 product_prob_space.measurable_component -> measurable_component_singleton

2313 product_prob_space.measurable_emb -> measurable_prod_emb

2314 product_prob_space.measurable_into_infprod_algebra -> measurable_PiM_single

2315 product_prob_space.measurable_singleton_infprod -> measurable_component_singleton

2316 product_prob_space.measure_emb -> emeasure_prod_emb

2317 product_prob_space.measure_preserving_restrict -> product_prob_space.distr_restrict

2318 product_sigma_algebra.product_algebra_into_space -> space_closed

2319 product_sigma_finite.measure_fold -> product_sigma_finite.distr_merge

2320 product_sigma_finite.measure_preserving_component_singelton -> product_sigma_finite.distr_singleton

2321 product_sigma_finite.measure_preserving_merge -> product_sigma_finite.distr_merge

2322 sequence_space.measure_infprod -> sequence_space.measure_PiM_countable

2323 sets_product_algebra -> sets_PiM

2324 sigma_algebra.measurable_sigma -> measurable_measure_of

2325 sigma_finite_measure.disjoint_sigma_finite -> sigma_finite_disjoint

2326 sigma_finite_measure.RN_deriv_vimage -> sigma_finite_measure.RN_deriv_distr

2327 sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq

2328 space_product_algebra -> space_PiM

2330 * Session HOL-TPTP: support to parse and import TPTP problems (all

2331 languages) into Isabelle/HOL.

2334 *** FOL ***

2336 * New "case_product" attribute (see HOL).

2339 *** ZF ***

2341 * Greater support for structured proofs involving induction or case

2342 analysis.

2344 * Much greater use of mathematical symbols.

2346 * Removal of many ML theorem bindings. INCOMPATIBILITY.

2349 *** ML ***

2351 * Antiquotation @{keyword "name"} produces a parser for outer syntax

2352 from a minor keyword introduced via theory header declaration.

2354 * Antiquotation @{command_spec "name"} produces the

2355 Outer_Syntax.command_spec from a major keyword introduced via theory

2356 header declaration; it can be passed to Outer_Syntax.command etc.

2358 * Local_Theory.define no longer hard-wires default theorem name

2359 "foo_def", but retains the binding as given. If that is Binding.empty

2360 / Attrib.empty_binding, the result is not registered as user-level

2361 fact. The Local_Theory.define_internal variant allows to specify a

2362 non-empty name (used for the foundation in the background theory),

2363 while omitting the fact binding in the user-context. Potential

2364 INCOMPATIBILITY for derived definitional packages: need to specify

2365 naming policy for primitive definitions more explicitly.

2367 * Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in

2368 conformance with similar operations in structure Term and Logic.

2370 * Antiquotation @{attributes [...]} embeds attribute source

2371 representation into the ML text, which is particularly useful with

2372 declarations like Local_Theory.note.

2374 * Structure Proof_Context follows standard naming scheme. Old

2375 ProofContext has been discontinued. INCOMPATIBILITY.

2377 * Refined Local_Theory.declaration {syntax, pervasive}, with subtle

2378 change of semantics: update is applied to auxiliary local theory

2379 context as well.

2381 * Modernized some old-style infix operations:

2383 addeqcongs ~> Simplifier.add_eqcong

2384 deleqcongs ~> Simplifier.del_eqcong

2385 addcongs ~> Simplifier.add_cong

2386 delcongs ~> Simplifier.del_cong

2387 setmksimps ~> Simplifier.set_mksimps

2388 setmkcong ~> Simplifier.set_mkcong

2389 setmksym ~> Simplifier.set_mksym

2390 setmkeqTrue ~> Simplifier.set_mkeqTrue

2391 settermless ~> Simplifier.set_termless

2392 setsubgoaler ~> Simplifier.set_subgoaler

2393 addsplits ~> Splitter.add_split

2394 delsplits ~> Splitter.del_split

2397 *** System ***

2399 * USER_HOME settings variable points to cross-platform user home

2400 directory, which coincides with HOME on POSIX systems only. Likewise,

2401 the Isabelle path specification "~" now expands to $USER_HOME, instead

2402 of former $HOME. A different default for USER_HOME may be set

2403 explicitly in shell environment, before Isabelle settings are

2404 evaluated. Minor INCOMPATIBILITY: need to adapt Isabelle path where

2405 the generic user home was intended.

2407 * ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name

2408 notation, which is useful for the jEdit file browser, for example.

2410 * ISABELLE_JDK_HOME settings variable points to JDK with javac and jar

2411 (not just JRE).

2415 New in Isabelle2011-1 (October 2011)

2416 ------------------------------------

2418 *** General ***

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

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

2423 - Management of multiple theory files directly from the editor

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

2425 files for checking).

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

2428 highlighting, tooltips and hyperlinks to jump to defining source

2429 positions.

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

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

2433 theory output and other non-Isabelle text boxes).

2435 - Refined scheduling of proof checking and printing of results,

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

2437 narrowing allows to restrict buffer perspectives explicitly.)

2439 - Reduced CPU performance requirements, usable on machines with few

2440 cores.

2442 - Reduced memory requirements due to pruning of unused document

2443 versions (garbage collection).

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

2446 including some remaining limitations.

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

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

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

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

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

2453 INCOMPATIBILITY.

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

2456 digests. Discontinued former path/modtime identification and optional

2457 ISABELLE_FILE_IDENT plugin scripts.

2459 * Parallelization of nested Isar proofs is subject to

2460 Goal.parallel_proofs_threshold (default 100). See also isabelle

2461 usedir option -Q.

2463 * Name space: former unsynchronized references are now proper

2464 configuration options, with more conventional names:

2466 long_names ~> names_long

2467 short_names ~> names_short

2468 unique_names ~> names_unique

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

2472 declare [[names_unique = false]]

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

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

2476 may have to be refined after enriching a proof context.

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

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

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

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

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

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

2485 "Classical Reasoner".

2488 *** HOL ***

2490 * Class bot and top require underlying partial order rather than

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

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

2494 generalized theorems INF_cong and SUP_cong. New type classes for

2495 complete boolean algebras and complete linear orders. Lemmas

2496 Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in

2497 class complete_linorder.

2499 Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def,

2500 Sup_fun_def, Inf_apply, Sup_apply.

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

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

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

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

2507 Inf_binary ~> Inf_insert, Inf_empty, and inf_top_right

2508 Sup_binary ~> Sup_insert, Sup_empty, and sup_bot_right

2509 Int_eq_Inter ~> Inf_insert, Inf_empty, and inf_top_right

2510 Un_eq_Union ~> Sup_insert, Sup_empty, and sup_bot_right

2511 Inter_def ~> INF_def, image_def

2512 Union_def ~> SUP_def, image_def

2513 INT_eq ~> INF_def, and image_def

2514 UN_eq ~> SUP_def, and image_def

2515 INF_subset ~> INF_superset_mono [OF _ order_refl]

2517 More consistent and comprehensive names:

2519 INTER_eq_Inter_image ~> INF_def

2520 UNION_eq_Union_image ~> SUP_def

2521 INFI_def ~> INF_def

2522 SUPR_def ~> SUP_def

2523 INF_leI ~> INF_lower

2524 INF_leI2 ~> INF_lower2

2525 le_INFI ~> INF_greatest

2526 le_SUPI ~> SUP_upper

2527 le_SUPI2 ~> SUP_upper2

2528 SUP_leI ~> SUP_least

2529 INFI_bool_eq ~> INF_bool_eq

2530 SUPR_bool_eq ~> SUP_bool_eq

2531 INFI_apply ~> INF_apply

2532 SUPR_apply ~> SUP_apply

2533 INTER_def ~> INTER_eq

2534 UNION_def ~> UNION_eq

2536 INCOMPATIBILITY.

2538 * Renamed theory Complete_Lattice to Complete_Lattices.

2539 INCOMPATIBILITY.

2541 * Theory Complete_Lattices: lemmas Inf_eq_top_iff, INF_eq_top_iff,

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

2543 Sup_bot_conv, SUP_bot_conv, Sup_eq_top_iff, SUP_eq_top_iff, SUP_image,

2544 Sup_insert are now declared as [simp]. INCOMPATIBILITY.

2546 * Theory Lattice: lemmas compl_inf_bot, compl_le_comp_iff,

2547 compl_sup_top, inf_idem, inf_left_idem, inf_sup_absorb, sup_idem,

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

2549 INCOMPATIBILITY.

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

2552 constants. INCOMPATIBILITY: Changes in the argument order of the

2553 (mostly internal) locale predicates for some derived classes.

2555 * Theorem collections ball_simps and bex_simps do not contain theorems

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

2557 UN_ball_bex_simps. INCOMPATIBILITY.

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

2560 separate type class floor_ceiling.

2562 * Theory Finite_Set: more coherent development of fold_set locales:

2564 locale fun_left_comm ~> locale comp_fun_commute

2565 locale fun_left_comm_idem ~> locale comp_fun_idem

2567 Both use point-free characterization; interpretation proofs may need

2568 adjustment. INCOMPATIBILITY.

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

2571 accordance with standard mathematical terminology. INCOMPATIBILITY.

2573 * Theory Complex_Main: The locale interpretations for the

2574 bounded_linear and bounded_bilinear locales have been removed, in

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

2576 original names for distributivity theorems, potential INCOMPATIBILITY.

2578 divide.add ~> add_divide_distrib

2579 divide.diff ~> diff_divide_distrib

2580 divide.setsum ~> setsum_divide_distrib

2581 mult.add_right ~> right_distrib

2582 mult.diff_right ~> right_diff_distrib

2583 mult_right.setsum ~> setsum_right_distrib

2584 mult_left.diff ~> left_diff_distrib

2586 * Theory Complex_Main: Several redundant theorems have been removed or

2587 replaced by more general versions. INCOMPATIBILITY.

2589 real_diff_def ~> minus_real_def

2590 real_divide_def ~> divide_real_def

2591 real_less_def ~> less_le

2592 real_abs_def ~> abs_real_def

2593 real_sgn_def ~> sgn_real_def

2594 real_mult_commute ~> mult_commute

2595 real_mult_assoc ~> mult_assoc

2596 real_mult_1 ~> mult_1_left

2597 real_add_mult_distrib ~> left_distrib

2598 real_zero_not_eq_one ~> zero_neq_one

2599 real_mult_inverse_left ~> left_inverse

2600 INVERSE_ZERO ~> inverse_zero

2601 real_le_refl ~> order_refl

2602 real_le_antisym ~> order_antisym

2603 real_le_trans ~> order_trans

2604 real_le_linear ~> linear

2605 real_le_eq_diff ~> le_iff_diff_le_0

2606 real_add_left_mono ~> add_left_mono

2607 real_mult_order ~> mult_pos_pos

2608 real_mult_less_mono2 ~> mult_strict_left_mono

2609 real_of_int_real_of_nat ~> real_of_int_of_nat_eq

2610 real_0_le_divide_iff ~> zero_le_divide_iff

2611 realpow_two_disj ~> power2_eq_iff

2612 real_squared_diff_one_factored ~> square_diff_one_factored

2613 realpow_two_diff ~> square_diff_square_factored

2614 reals_complete2 ~> complete_real

2615 real_sum_squared_expand ~> power2_sum

2616 exp_ln_eq ~> ln_unique

2617 expi_add ~> exp_add

2618 expi_zero ~> exp_zero

2619 lemma_DERIV_subst ~> DERIV_cong

2620 LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff

2621 LIMSEQ_const ~> tendsto_const

2622 LIMSEQ_norm ~> tendsto_norm

2623 LIMSEQ_add ~> tendsto_add

2624 LIMSEQ_minus ~> tendsto_minus

2625 LIMSEQ_minus_cancel ~> tendsto_minus_cancel

2626 LIMSEQ_diff ~> tendsto_diff

2627 bounded_linear.LIMSEQ ~> bounded_linear.tendsto

2628 bounded_bilinear.LIMSEQ ~> bounded_bilinear.tendsto

2629 LIMSEQ_mult ~> tendsto_mult

2630 LIMSEQ_inverse ~> tendsto_inverse

2631 LIMSEQ_divide ~> tendsto_divide

2632 LIMSEQ_pow ~> tendsto_power

2633 LIMSEQ_setsum ~> tendsto_setsum

2634 LIMSEQ_setprod ~> tendsto_setprod

2635 LIMSEQ_norm_zero ~> tendsto_norm_zero_iff

2636 LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff

2637 LIMSEQ_imp_rabs ~> tendsto_rabs

2638 LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]

2639 LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]

2640 LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]

2641 LIMSEQ_Complex ~> tendsto_Complex

2642 LIM_ident ~> tendsto_ident_at

2643 LIM_const ~> tendsto_const

2644 LIM_add ~> tendsto_add

2645 LIM_add_zero ~> tendsto_add_zero

2646 LIM_minus ~> tendsto_minus

2647 LIM_diff ~> tendsto_diff

2648 LIM_norm ~> tendsto_norm

2649 LIM_norm_zero ~> tendsto_norm_zero

2650 LIM_norm_zero_cancel ~> tendsto_norm_zero_cancel

2651 LIM_norm_zero_iff ~> tendsto_norm_zero_iff

2652 LIM_rabs ~> tendsto_rabs

2653 LIM_rabs_zero ~> tendsto_rabs_zero

2654 LIM_rabs_zero_cancel ~> tendsto_rabs_zero_cancel

2655 LIM_rabs_zero_iff ~> tendsto_rabs_zero_iff

2656 LIM_compose ~> tendsto_compose

2657 LIM_mult ~> tendsto_mult

2658 LIM_scaleR ~> tendsto_scaleR

2659 LIM_of_real ~> tendsto_of_real

2660 LIM_power ~> tendsto_power

2661 LIM_inverse ~> tendsto_inverse

2662 LIM_sgn ~> tendsto_sgn

2663 isCont_LIM_compose ~> isCont_tendsto_compose

2664 bounded_linear.LIM ~> bounded_linear.tendsto

2665 bounded_linear.LIM_zero ~> bounded_linear.tendsto_zero

2666 bounded_bilinear.LIM ~> bounded_bilinear.tendsto

2667 bounded_bilinear.LIM_prod_zero ~> bounded_bilinear.tendsto_zero

2668 bounded_bilinear.LIM_left_zero ~> bounded_bilinear.tendsto_left_zero

2669 bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero

2670 LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at]

2672 * Theory Complex_Main: The definition of infinite series was

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

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

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

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

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

2680 * Code generation:

2682 - Theory Library/Code_Char_ord provides native ordering of

2683 characters in the target language.

2685 - Commands code_module and code_library are legacy, use export_code

2686 instead.

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

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

2691 reactivated by the following theory command:

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

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

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

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

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

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

2701 syntax.

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

2704 still available as a legacy feature for some time.

2706 * Nitpick:

2707 - Added "need" and "total_consts" options.

2708 - Reintroduced "show_skolems" option by popular demand.

2709 - Renamed attribute: nitpick_def ~> nitpick_unfold.

2710 INCOMPATIBILITY.

2712 * Sledgehammer:

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

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

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

2716 - Automatically preplay and minimize proofs before showing them if

2717 this can be done within reasonable time.

2718 - sledgehammer available_provers ~> sledgehammer supported_provers.

2719 INCOMPATIBILITY.

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

2721 "max_mono_iters", and "max_new_mono_instances" options.

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

2723 Types" Proof General menu item. INCOMPATIBILITY.

2725 * Metis:

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

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

2728 INCOMPATIBILITY.

2730 * Command 'try':

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

2732 "elim:" options. INCOMPATIBILITY.

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

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

2736 * Quickcheck:

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

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

2739 - Added post-processing of terms to obtain readable counterexamples

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

2741 - New counterexample generator quickcheck[narrowing] enables

2742 narrowing-based testing. Requires the Glasgow Haskell compiler

2743 with its installation location defined in the Isabelle settings

2744 environment as ISABELLE_GHC.

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

2746 (formly in HOL/Library).

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

2749 use 'partial_function' instead.

2751 * Theory Library/Extended_Reals replaces now the positive extended

2752 reals found in probability theory. This file is extended by

2753 Multivariate_Analysis/Extended_Real_Limits.

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

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

2757 INCOMPATIBILITY.

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

2760 been moved here. INCOMPATIBILITY.

2762 * Theory Library/Saturated provides type of numbers with saturated

2763 arithmetic.

2765 * Theory Library/Product_Lattice defines a pointwise ordering for the

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

2767 and lattice type classes.

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

2770 method for proving "countable" class instances for datatypes.

2772 * Theory Library/Cset_Monad allows do notation for computable sets

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

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

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

2777 abstract type. INCOMPATIBILITY.

2779 - RBT is split into RBT and RBT_Mapping.

2780 - AssocList is split and renamed into AList and AList_Mapping.

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

2782 - Cset is split into Cset and List_Cset.

2784 * Theory Library/Nat_Infinity has been renamed to

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

2786 constants:

2788 type inat ~> type enat

2789 Fin ~> enat

2790 Infty ~> infinity (overloaded)

2791 iSuc ~> eSuc

2792 the_Fin ~> the_enat

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

2795 been renamed accordingly. INCOMPATIBILITY.

2797 * Session Multivariate_Analysis: The euclidean_space type class now

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

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

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

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

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

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

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

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

2807 changed to match. Definition theorems for overloaded constants now use

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

2809 been renamed as follows (INCOMPATIBILITY):

2811 Cart_eq ~> vec_eq_iff

2812 dist_nth_le_cart ~> dist_vec_nth_le

2813 tendsto_vector ~> vec_tendstoI

2814 Cauchy_vector ~> vec_CauchyI

2816 * Session Multivariate_Analysis: Several duplicate theorems have been

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

2818 general versions. INCOMPATIBILITY.

2820 finite_choice ~> finite_set_choice

2821 eventually_conjI ~> eventually_conj

2822 eventually_and ~> eventually_conj_iff

2823 eventually_false ~> eventually_False

2824 setsum_norm ~> norm_setsum

2825 Lim_sequentially ~> LIMSEQ_def

2826 Lim_ident_at ~> LIM_ident

2827 Lim_const ~> tendsto_const

2828 Lim_cmul ~> tendsto_scaleR [OF tendsto_const]

2829 Lim_neg ~> tendsto_minus

2830 Lim_add ~> tendsto_add

2831 Lim_sub ~> tendsto_diff

2832 Lim_mul ~> tendsto_scaleR

2833 Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const]

2834 Lim_null_norm ~> tendsto_norm_zero_iff [symmetric]

2835 Lim_linear ~> bounded_linear.tendsto

2836 Lim_component ~> tendsto_euclidean_component

2837 Lim_component_cart ~> tendsto_vec_nth

2838 Lim_inner ~> tendsto_inner [OF tendsto_const]

2839 dot_lsum ~> inner_setsum_left

2840 dot_rsum ~> inner_setsum_right

2841 continuous_cmul ~> continuous_scaleR [OF continuous_const]

2842 continuous_neg ~> continuous_minus

2843 continuous_sub ~> continuous_diff

2844 continuous_vmul ~> continuous_scaleR [OF _ continuous_const]

2845 continuous_mul ~> continuous_scaleR

2846 continuous_inv ~> continuous_inverse

2847 continuous_at_within_inv ~> continuous_at_within_inverse

2848 continuous_at_inv ~> continuous_at_inverse

2849 continuous_at_norm ~> continuous_norm [OF continuous_at_id]

2850 continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id]

2851 continuous_at_component ~> continuous_component [OF continuous_at_id]

2852 continuous_on_neg ~> continuous_on_minus

2853 continuous_on_sub ~> continuous_on_diff

2854 continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const]

2855 continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const]

2856 continuous_on_mul ~> continuous_on_scaleR

2857 continuous_on_mul_real ~> continuous_on_mult

2858 continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]

2859 continuous_on_norm ~> continuous_on_norm [OF continuous_on_id]

2860 continuous_on_inverse ~> continuous_on_inv

2861 uniformly_continuous_on_neg ~> uniformly_continuous_on_minus

2862 uniformly_continuous_on_sub ~> uniformly_continuous_on_diff

2863 subset_interior ~> interior_mono

2864 subset_closure ~> closure_mono

2865 closure_univ ~> closure_UNIV

2866 real_arch_lt ~> reals_Archimedean2

2867 real_arch ~> reals_Archimedean3

2868 real_abs_norm ~> abs_norm_cancel

2869 real_abs_sub_norm ~> norm_triangle_ineq3

2870 norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2

2872 * Session HOL-Probability:

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

2874 - Infinite products of probability measures are now available.

2875 - Sigma closure is independent, if the generator is independent

2876 - Use extended reals instead of positive extended

2877 reals. INCOMPATIBILITY.

2879 * Session HOLCF: Discontinued legacy theorem names, INCOMPATIBILITY.

2881 expand_fun_below ~> fun_below_iff

2882 below_fun_ext ~> fun_belowI

2883 expand_cfun_eq ~> cfun_eq_iff

2884 ext_cfun ~> cfun_eqI

2885 expand_cfun_below ~> cfun_below_iff

2886 below_cfun_ext ~> cfun_belowI

2887 monofun_fun_fun ~> fun_belowD

2888 monofun_fun_arg ~> monofunE

2889 monofun_lub_fun ~> adm_monofun [THEN admD]

2890 cont_lub_fun ~> adm_cont [THEN admD]

2891 cont2cont_Rep_CFun ~> cont2cont_APP

2892 cont_Rep_CFun_app ~> cont_APP_app

2893 cont_Rep_CFun_app_app ~> cont_APP_app_app

2894 cont_cfun_fun ~> cont_Rep_cfun1 [THEN contE]

2895 cont_cfun_arg ~> cont_Rep_cfun2 [THEN contE]

2896 contlub_cfun ~> lub_APP [symmetric]

2897 contlub_LAM ~> lub_LAM [symmetric]

2898 thelubI ~> lub_eqI

2899 UU_I ~> bottomI

2900 lift_distinct1 ~> lift.distinct(1)

2901 lift_distinct2 ~> lift.distinct(2)

2902 Def_not_UU ~> lift.distinct(2)

2903 Def_inject ~> lift.inject

2904 below_UU_iff ~> below_bottom_iff

2905 eq_UU_iff ~> eq_bottom_iff

2908 *** Document preparation ***

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

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

2912 same.

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

2915 result.

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

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

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

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

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

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

2925 like this:

2927 \isabellestyle{it} %preferred default

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

2930 * Discontinued special treatment of hard tabulators. Implicit

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

2932 layouts.

2935 *** ML ***

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

2938 representations within quoted string tokens. By encoding logical

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

2940 bypassed, which is particularly useful for producing bits of text

2941 under external program control.

2943 * Antiquotations for ML and document preparation are managed as theory

2944 data, which requires explicit setup.

2946 * Isabelle_Process.is_active allows tools to check if the official

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

2948 (better known as Proof General).

2950 * Structure Proof_Context follows standard naming scheme. Old

2951 ProofContext is still available for some time as legacy alias.

2953 * Structure Timing provides various operations for timing; supersedes

2954 former start_timing/end_timing etc.

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

2957 (including quotes etc.).

2959 * Inner syntax: identifiers in parse trees of generic categories

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

2961 type constraints). Occasional INCOMPATIBILITY with non-compliant

2962 translations that choke on unexpected type constraints. Positions can

2963 be stripped in ML translations via Syntax.strip_positions /

2964 Syntax.strip_positions_ast, or via the syntax constant

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

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

2967 called "syntax_positions" in Isar attribute syntax.

2969 * Discontinued special status of various ML structures that contribute

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

2971 pervasive content, no inclusion in structure Syntax. INCOMPATIBILITY,

2972 refer directly to Ast.Constant, Lexicon.is_identifier,

2973 Syntax_Trans.mk_binder_tr etc.

2975 * Typed print translation: discontinued show_sorts argument, which is

2976 already available via context of "advanced" translation.

2978 * Refined PARALLEL_GOALS tactical: degrades gracefully for schematic

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

2981 * Slightly more special eq_list/eq_set, with shortcut involving

2982 pointer equality (assumes that eq relation is reflexive).

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

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

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

2987 snapshot of the classical context, which can be recovered via

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

2989 INCOMPATIBILITY, classical tactics and derived proof methods require

2990 proper Proof.context.

2993 *** System ***

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

2996 without proper multithreading and TimeLimit implementation.

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

2999 obsolete since Isabelle2009-2.

3001 * Various optional external tools are referenced more robustly and

3002 uniformly by explicit Isabelle settings as follows:

3004 ISABELLE_CSDP (formerly CSDP_EXE)

3005 ISABELLE_GHC (formerly EXEC_GHC or GHC_PATH)

3006 ISABELLE_OCAML (formerly EXEC_OCAML)

3007 ISABELLE_SWIPL (formerly EXEC_SWIPL)

3008 ISABELLE_YAP (formerly EXEC_YAP)

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

3011 been discontinued. INCOMPATIBILITY.

3013 * Scala layer provides JVM method invocation service for static

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

3015 example:

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

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

3020 this allows to pass structured values between ML and Scala.

3022 * The IsabelleText fonts includes some further glyphs to support the

3023 Prover IDE. Potential INCOMPATIBILITY: users who happen to have

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

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

3029 New in Isabelle2011 (January 2011)

3030 ----------------------------------

3032 *** General ***

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

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

3036 useful tooltips and hyperlinks produced from its static analysis. The

3037 bundled component provides an executable Isabelle tool that can be run

3038 like this:

3040 Isabelle2011/bin/isabelle jedit

3042 * Significantly improved Isabelle/Isar implementation manual.

3044 * System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER

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

3046 while the default heap location within that directory lacks that extra

3047 suffix. This isolates multiple Isabelle installations from each

3048 other, avoiding problems with old settings in new versions.

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

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

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

3053 the following package declarations:

3055 \usepackage[utf8]{inputenc}

3056 \usepackage{textcomp}

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

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

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

3061 contain symbols without further backslash escapes, Unicode can now be

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

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

3064 merely give a byte-oriented representation.

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

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

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

3069 Minor INCOMPATIBILITY due to subtle change in file lookup: use

3070 explicit paths, relatively to the theory.

3072 * Special treatment of ML file names has been discontinued.

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

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

3075 files exclusively use the .ML extension. Minor INCOMPATIBILTY.

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

3078 handled within the context via configuration options, instead of

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

3080 entities and Isar declaration attributes to access these.

3082 ML (Config.T) Isar (attribute)

3084 eta_contract eta_contract

3085 show_brackets show_brackets

3086 show_sorts show_sorts

3087 show_types show_types

3088 show_question_marks show_question_marks

3089 show_consts show_consts

3090 show_abbrevs show_abbrevs

3092 Syntax.ast_trace syntax_ast_trace

3093 Syntax.ast_stat syntax_ast_stat

3094 Syntax.ambiguity_level syntax_ambiguity_level

3096 Goal_Display.goals_limit goals_limit

3097 Goal_Display.show_main_goal show_main_goal

3099 Method.rule_trace rule_trace

3101 Thy_Output.display thy_output_display

3102 Thy_Output.quotes thy_output_quotes

3103 Thy_Output.indent thy_output_indent

3104 Thy_Output.source thy_output_source

3105 Thy_Output.break thy_output_break

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

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

3109 The option "show_abbrevs" supersedes the former print mode

3110 "no_abbrevs" with inverted meaning.

3112 * More systematic naming of some configuration options.

3113 INCOMPATIBILITY.

3115 trace_simp ~> simp_trace

3116 debug_simp ~> simp_debug

3118 * Support for real valued configuration options, using simplistic

3119 floating-point notation that coincides with the inner syntax for

3120 float_token.

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

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

3124 INCOMPATIBILITY.

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

3127 DejaVu Sans.

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

3132 *** Pure ***

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

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

3136 time.

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

3139 replaces somewhat outdated 'nonterminals'. INCOMPATIBILITY.

3141 * Command 'notepad' replaces former 'example_proof' for

3142 experimentation in Isar without any result. INCOMPATIBILITY.

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

3145 lists of equations to map definitions in a locale to appropriate

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

3147 command already provided this functionality.

3149 * Diagnostic command 'print_dependencies' prints the locale instances

3150 that would be activated if the specified expression was interpreted in

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

3152 without interpretations.

3154 * Diagnostic command 'print_interps' prints interpretations in proofs

3155 in addition to interpretations in theories.

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

3158 the theory name space. Rare INCOMPATIBILITY. The ML functions

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

3160 feature is still required for historical reasons.

3162 * Discontinued obsolete 'constdefs' command. INCOMPATIBILITY, use

3163 'definition' instead.

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

3166 foundational premises in the context, is now explicitly marked as

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

3168 of the head statement or reference facts by explicit names.

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

3171 constructors.

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

3174 the local file system.

3177 *** HOL ***

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

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

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

3182 coercions. A coercion function f is declared like this:

3184 declare [[coercion f]]

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

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

3189 declare [[coercion_map map]]

3191 Currently coercion inference is activated only in theories including

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

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

3194 other theories like this:

3196 declare [[coercion_enabled]]

3198 * Command 'partial_function' provides basic support for recursive

3199 function definitions over complete partial orders. Concrete instances

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

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

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

3203 for examples.

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

3206 as [simp]. INCOMPATIBILITY.

3208 * Datatype package: theorems generated for executable equality (class

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

3211 * Inductive package: now offers command 'inductive_simps' to

3212 automatically derive instantiated and simplified equations for

3213 inductive predicates, similar to 'inductive_cases'.

3215 * Command 'enriched_type' allows to register properties of the

3216 functorial structure of types.

3218 * Improved infrastructure for term evaluation using code generator

3219 techniques, in particular static evaluation conversions.

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

3222 languages.

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

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

3226 INCOMPATIBILITY.

3228 * Code generator: export_code without explicit file declaration prints

3229 to standard output. INCOMPATIBILITY.

3231 * Code generator: do not print function definitions for case

3232 combinators any longer.

3234 * Code generator: simplification with rules determined with

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

3237 * Code generator for records: more idiomatic representation of record

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

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

3240 rep_datatype declaration helps to succeed then:

3242 record 'a foo = ...

3243 ...

3244 rep_datatype foo_ext ...

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

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

3248 INCOMPATIBILITY.

3250 * Quickcheck now by default uses exhaustive testing instead of random

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

3252 exhaustive testing by "quickcheck [exhaustive]".

3254 * Quickcheck instantiates polymorphic types with small finite

3255 datatypes by default. This enables a simple execution mechanism to

3256 handle quantifiers and function equality over the finite datatypes.

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

3259 "random". INCOMPATIBILITY.

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

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

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

3264 independently.

3266 * Quickcheck in locales considers interpretations of that locale for

3267 counter example search.

3269 * Sledgehammer:

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

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

3272 sledgehammer").

3273 - Renamed commands:

3274 sledgehammer atp_info ~> sledgehammer running_provers

3275 sledgehammer atp_kill ~> sledgehammer kill_provers

3276 sledgehammer available_atps ~> sledgehammer available_provers

3277 INCOMPATIBILITY.

3278 - Renamed options:

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

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

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

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

3283 INCOMPATIBILITY.

3285 * Nitpick:

3286 - Renamed options:

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

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

3289 INCOMPATIBILITY.

3290 - Added support for partial quotient types.

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

3292 - Added "whack" option.

3293 - Allow registration of quotient types as codatatypes.

3294 - Improved "merge_type_vars" option to merge more types.

3295 - Removed unsound "fast_descrs" option.

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

3297 higher cardinalities.

3298 - Prevent the expansion of too large definitions.

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

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

3302 to diagnose these tools. E.g.

3304 using [[metis_trace = true]]

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

3307 manually as command 'solve_direct'.

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

3310 licensing issues) by setting the environment variable

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

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

3313 changing the SMT solver is done via the configuration option

3314 "smt_solver".

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

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

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

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

3321 in exchange (pass theorems fst_conv snd_conv pair_collapse to the SMT

3322 support for a similar behavior). Minor INCOMPATIBILITY.

3324 * Changed SMT configuration options:

3325 - Renamed:

3326 z3_proofs ~> smt_oracle (with inverted meaning)

3327 z3_trace_assms ~> smt_trace_used_facts

3328 INCOMPATIBILITY.

3329 - Added:

3330 smt_verbose

3331 smt_random_seed

3332 smt_datatypes

3333 smt_infer_triggers

3334 smt_monomorph_limit

3335 cvc3_options

3336 remote_cvc3_options

3337 remote_z3_options

3338 yices_options

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

3341 header.

3343 * Simplification procedure "list_to_set_comprehension" rewrites list

3344 comprehensions applied to List.set to set comprehensions. Occasional

3345 INCOMPATIBILITY, may be deactivated like this:

3347 declare [[simproc del: list_to_set_comprehension]]

3349 * Removed old version of primrec package. INCOMPATIBILITY.

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

3352 been the case with "split". INCOMPATIBILITY.

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

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

3357 [split_format]. Potential INCOMPATIBILITY.

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

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

3362 * Constant "contents" renamed to "the_elem", to free the generic name

3363 contents for other uses. INCOMPATIBILITY.

3365 * Renamed class eq and constant eq (for code generation) to class

3366 equal and constant equal, plus renaming of related facts and various

3367 tuning. INCOMPATIBILITY.

3369 * Dropped type classes mult_mono and mult_mono1. INCOMPATIBILITY.

3371 * Removed output syntax "'a ~=> 'b" for "'a => 'b option".

3372 INCOMPATIBILITY.

3374 * Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to

3375 avoid confusion with finite sets. INCOMPATIBILITY.

3377 * Abandoned locales equiv, congruent and congruent2 for equivalence

3378 relations. INCOMPATIBILITY: use equivI rather than equiv_intro (same

3379 for congruent(2)).

3381 * Some previously unqualified names have been qualified:

3383 types

3384 bool ~> HOL.bool

3385 nat ~> Nat.nat

3387 constants

3388 Trueprop ~> HOL.Trueprop

3389 True ~> HOL.True

3390 False ~> HOL.False

3391 op & ~> HOL.conj

3392 op | ~> HOL.disj

3393 op --> ~> HOL.implies

3394 op = ~> HOL.eq

3395 Not ~> HOL.Not

3396 The ~> HOL.The

3397 All ~> HOL.All

3398 Ex ~> HOL.Ex

3399 Ex1 ~> HOL.Ex1

3400 Let ~> HOL.Let

3401 If ~> HOL.If

3402 Ball ~> Set.Ball

3403 Bex ~> Set.Bex

3404 Suc ~> Nat.Suc

3405 Pair ~> Product_Type.Pair

3406 fst ~> Product_Type.fst

3407 snd ~> Product_Type.snd

3408 curry ~> Product_Type.curry

3409 op : ~> Set.member

3410 Collect ~> Set.Collect

3412 INCOMPATIBILITY.

3414 * More canonical naming convention for some fundamental definitions:

3416 bot_bool_eq ~> bot_bool_def

3417 top_bool_eq ~> top_bool_def

3418 inf_bool_eq ~> inf_bool_def

3419 sup_bool_eq ~> sup_bool_def

3420 bot_fun_eq ~> bot_fun_def

3421 top_fun_eq ~> top_fun_def

3422 inf_fun_eq ~> inf_fun_def

3423 sup_fun_eq ~> sup_fun_def

3425 INCOMPATIBILITY.

3427 * More stylized fact names:

3429 expand_fun_eq ~> fun_eq_iff

3430 expand_set_eq ~> set_eq_iff

3431 set_ext ~> set_eqI

3432 nat_number ~> eval_nat_numeral

3434 INCOMPATIBILITY.

3436 * Refactoring of code-generation specific operations in theory List:

3438 constants

3439 null ~> List.null

3441 facts

3442 mem_iff ~> member_def

3443 null_empty ~> null_def

3445 INCOMPATIBILITY. Note that these were not supposed to be used

3446 regularly unless for striking reasons; their main purpose was code

3447 generation.

3449 Various operations from the Haskell prelude are used for generating

3450 Haskell code.

3452 * Term "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". Term

3453 "surj f" is now an abbreviation of "range f = UNIV". The theorems

3454 bij_def and surj_def are unchanged. INCOMPATIBILITY.

3456 * Abolished some non-alphabetic type names: "prod" and "sum" replace

3457 "*" and "+" respectively. INCOMPATIBILITY.

3459 * Name "Plus" of disjoint sum operator "<+>" is now hidden. Write

3460 "Sum_Type.Plus" instead.

3462 * Constant "split" has been merged with constant "prod_case"; names of

3463 ML functions, facts etc. involving split have been retained so far,

3464 though. INCOMPATIBILITY.

3466 * Dropped old infix syntax "_ mem _" for List.member; use "_ : set _"

3467 instead. INCOMPATIBILITY.

3469 * Removed lemma "Option.is_none_none" which duplicates "is_none_def".

3470 INCOMPATIBILITY.

3472 * Former theory Library/Enum is now part of the HOL-Main image.

3473 INCOMPATIBILITY: all constants of the Enum theory now have to be

3474 referred to by its qualified name.

3476 enum ~> Enum.enum

3477 nlists ~> Enum.nlists

3478 product ~> Enum.product

3480 * Theory Library/Monad_Syntax provides do-syntax for monad types.

3481 Syntax in Library/State_Monad has been changed to avoid ambiguities.

3482 INCOMPATIBILITY.

3484 * Theory Library/SetsAndFunctions has been split into

3485 Library/Function_Algebras and Library/Set_Algebras; canonical names

3486 for instance definitions for functions; various improvements.

3487 INCOMPATIBILITY.

3489 * Theory Library/Multiset provides stable quicksort implementation of

3490 sort_key.

3492 * Theory Library/Multiset: renamed empty_idemp ~> empty_neutral.

3493 INCOMPATIBILITY.

3495 * Session Multivariate_Analysis: introduced a type class for euclidean

3496 space. Most theorems are now stated in terms of euclidean spaces

3497 instead of finite cartesian products.

3499 types

3500 real ^ 'n ~> 'a::real_vector

3501 ~> 'a::euclidean_space

3502 ~> 'a::ordered_euclidean_space

3503 (depends on your needs)

3505 constants

3506 _ $ _ ~> _ $$ _

3507 \<chi> x. _ ~> \<chi>\<chi> x. _

3508 CARD('n) ~> DIM('a)

3510 Also note that the indices are now natural numbers and not from some

3511 finite type. Finite cartesian products of euclidean spaces, products

3512 of euclidean spaces the real and complex numbers are instantiated to

3513 be euclidean_spaces. INCOMPATIBILITY.

3515 * Session Probability: introduced pextreal as positive extended real

3516 numbers. Use pextreal as value for measures. Introduce the

3517 Radon-Nikodym derivative, product spaces and Fubini's theorem for

3518 arbitrary sigma finite measures. Introduces Lebesgue measure based on

3519 the integral in Multivariate Analysis. INCOMPATIBILITY.

3521 * Session Imperative_HOL: revamped, corrected dozens of inadequacies.

3522 INCOMPATIBILITY.

3524 * Session SPARK (with image HOL-SPARK) provides commands to load and

3525 prove verification conditions generated by the SPARK Ada program

3526 verifier. See also src/HOL/SPARK and src/HOL/SPARK/Examples.

3529 *** HOL-Algebra ***

3531 * Theorems for additive ring operations (locale abelian_monoid and

3532 descendants) are generated by interpretation from their multiplicative

3533 counterparts. Names (in particular theorem names) have the mandatory

3534 qualifier 'add'. Previous theorem names are redeclared for

3535 compatibility.

3537 * Structure "int_ring" is now an abbreviation (previously a

3538 definition). This fits more natural with advanced interpretations.

3541 *** HOLCF ***

3543 * The domain package now runs in definitional mode by default: The

3544 former command 'new_domain' is now called 'domain'. To use the domain

3545 package in its original axiomatic mode, use 'domain (unsafe)'.

3546 INCOMPATIBILITY.

3548 * The new class "domain" is now the default sort. Class "predomain"

3549 is an unpointed version of "domain". Theories can be updated by

3550 replacing sort annotations as shown below. INCOMPATIBILITY.

3552 'a::type ~> 'a::countable

3553 'a::cpo ~> 'a::predomain

3554 'a::pcpo ~> 'a::domain

3556 * The old type class "rep" has been superseded by class "domain".

3557 Accordingly, users of the definitional package must remove any

3558 "default_sort rep" declarations. INCOMPATIBILITY.

3560 * The domain package (definitional mode) now supports unpointed

3561 predomain argument types, as long as they are marked 'lazy'. (Strict

3562 arguments must be in class "domain".) For example, the following

3563 domain definition now works:

3565 domain natlist = nil | cons (lazy "nat discr") (lazy "natlist")

3567 * Theory HOLCF/Library/HOL_Cpo provides cpo and predomain class

3568 instances for types from main HOL: bool, nat, int, char, 'a + 'b,

3569 'a option, and 'a list. Additionally, it configures fixrec and the

3570 domain package to work with these types. For example:

3572 fixrec isInl :: "('a + 'b) u -> tr"

3573 where "isInl$(up$(Inl x)) = TT" | "isInl$(up$(Inr y)) = FF"

3575 domain V = VFun (lazy "V -> V") | VCon (lazy "nat") (lazy "V list")

3577 * The "(permissive)" option of fixrec has been replaced with a

3578 per-equation "(unchecked)" option. See

3579 src/HOL/HOLCF/Tutorial/Fixrec_ex.thy for examples. INCOMPATIBILITY.

3581 * The "bifinite" class no longer fixes a constant "approx"; the class

3582 now just asserts that such a function exists. INCOMPATIBILITY.

3584 * Former type "alg_defl" has been renamed to "defl". HOLCF no longer

3585 defines an embedding of type 'a defl into udom by default; instances

3586 of "bifinite" and "domain" classes are available in

3587 src/HOL/HOLCF/Library/Defl_Bifinite.thy.

3589 * The syntax "REP('a)" has been replaced with "DEFL('a)".

3591 * The predicate "directed" has been removed. INCOMPATIBILITY.

3593 * The type class "finite_po" has been removed. INCOMPATIBILITY.

3595 * The function "cprod_map" has been renamed to "prod_map".

3596 INCOMPATIBILITY.

3598 * The monadic bind operator on each powerdomain has new binder syntax

3599 similar to sets, e.g. "\<Union>\<sharp>x\<in>xs. t" represents

3600 "upper_bind\<cdot>xs\<cdot>(\<Lambda> x. t)".

3602 * The infix syntax for binary union on each powerdomain has changed

3603 from e.g. "+\<sharp>" to "\<union>\<sharp>", for consistency with set

3604 syntax. INCOMPATIBILITY.

3606 * The constant "UU" has been renamed to "bottom". The syntax "UU" is

3607 still supported as an input translation.

3609 * Renamed some theorems (the original names are also still available).

3611 expand_fun_below ~> fun_below_iff

3612 below_fun_ext ~> fun_belowI

3613 expand_cfun_eq ~> cfun_eq_iff

3614 ext_cfun ~> cfun_eqI

3615 expand_cfun_below ~> cfun_below_iff

3616 below_cfun_ext ~> cfun_belowI

3617 cont2cont_Rep_CFun ~> cont2cont_APP

3619 * The Abs and Rep functions for various types have changed names.

3620 Related theorem names have also changed to match. INCOMPATIBILITY.

3622 Rep_CFun ~> Rep_cfun

3623 Abs_CFun ~> Abs_cfun

3624 Rep_Sprod ~> Rep_sprod

3625 Abs_Sprod ~> Abs_sprod

3626 Rep_Ssum ~> Rep_ssum

3627 Abs_Ssum ~> Abs_ssum

3629 * Lemmas with names of the form *_defined_iff or *_strict_iff have

3630 been renamed to *_bottom_iff. INCOMPATIBILITY.

3632 * Various changes to bisimulation/coinduction with domain package:

3634 - Definitions of "bisim" constants no longer mention definedness.

3635 - With mutual recursion, "bisim" predicate is now curried.

3636 - With mutual recursion, each type gets a separate coind theorem.

3637 - Variable names in bisim_def and coinduct rules have changed.

3639 INCOMPATIBILITY.

3641 * Case combinators generated by the domain package for type "foo" are

3642 now named "foo_case" instead of "foo_when". INCOMPATIBILITY.

3644 * Several theorems have been renamed to more accurately reflect the

3645 names of constants and types involved. INCOMPATIBILITY.

3647 thelub_const ~> lub_const

3648 lub_const ~> is_lub_const

3649 thelubI ~> lub_eqI

3650 is_lub_lub ~> is_lubD2

3651 lubI ~> is_lub_lub

3652 unique_lub ~> is_lub_unique

3653 is_ub_lub ~> is_lub_rangeD1

3654 lub_bin_chain ~> is_lub_bin_chain

3655 lub_fun ~> is_lub_fun

3656 thelub_fun ~> lub_fun

3657 thelub_cfun ~> lub_cfun

3658 thelub_Pair ~> lub_Pair

3659 lub_cprod ~> is_lub_prod

3660 thelub_cprod ~> lub_prod

3661 minimal_cprod ~> minimal_prod

3662 inst_cprod_pcpo ~> inst_prod_pcpo

3663 UU_I ~> bottomI

3664 compact_UU ~> compact_bottom

3665 deflation_UU ~> deflation_bottom

3666 finite_deflation_UU ~> finite_deflation_bottom

3668 * Many legacy theorem names have been discontinued. INCOMPATIBILITY.

3670 sq_ord_less_eq_trans ~> below_eq_trans

3671 sq_ord_eq_less_trans ~> eq_below_trans

3672 refl_less ~> below_refl

3673 trans_less ~> below_trans

3674 antisym_less ~> below_antisym

3675 antisym_less_inverse ~> po_eq_conv [THEN iffD1]

3676 box_less ~> box_below

3677 rev_trans_less ~> rev_below_trans

3678 not_less2not_eq ~> not_below2not_eq

3679 less_UU_iff ~> below_UU_iff

3680 flat_less_iff ~> flat_below_iff

3681 adm_less ~> adm_below

3682 adm_not_less ~> adm_not_below

3683 adm_compact_not_less ~> adm_compact_not_below

3684 less_fun_def ~> below_fun_def

3685 expand_fun_less ~> fun_below_iff

3686 less_fun_ext ~> fun_belowI

3687 less_discr_def ~> below_discr_def

3688 discr_less_eq ~> discr_below_eq

3689 less_unit_def ~> below_unit_def

3690 less_cprod_def ~> below_prod_def

3691 prod_lessI ~> prod_belowI

3692 Pair_less_iff ~> Pair_below_iff

3693 fst_less_iff ~> fst_below_iff

3694 snd_less_iff ~> snd_below_iff

3695 expand_cfun_less ~> cfun_below_iff

3696 less_cfun_ext ~> cfun_belowI

3697 injection_less ~> injection_below

3698 less_up_def ~> below_up_def

3699 not_Iup_less ~> not_Iup_below

3700 Iup_less ~> Iup_below

3701 up_less ~> up_below

3702 Def_inject_less_eq ~> Def_below_Def

3703 Def_less_is_eq ~> Def_below_iff

3704 spair_less_iff ~> spair_below_iff

3705 less_sprod ~> below_sprod

3706 spair_less ~> spair_below

3707 sfst_less_iff ~> sfst_below_iff

3708 ssnd_less_iff ~> ssnd_below_iff

3709 fix_least_less ~> fix_least_below

3710 dist_less_one ~> dist_below_one

3711 less_ONE ~> below_ONE

3712 ONE_less_iff ~> ONE_below_iff

3713 less_sinlD ~> below_sinlD

3714 less_sinrD ~> below_sinrD

3717 *** FOL and ZF ***

3719 * All constant names are now qualified internally and use proper

3720 identifiers, e.g. "IFOL.eq" instead of "op =". INCOMPATIBILITY.

3723 *** ML ***

3725 * Antiquotation @{assert} inlines a function bool -> unit that raises

3726 Fail if the argument is false. Due to inlining the source position of

3727 failed assertions is included in the error output.

3729 * Discontinued antiquotation @{theory_ref}, which is obsolete since ML

3730 text is in practice always evaluated with a stable theory checkpoint.

3731 Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.

3733 * Antiquotation @{theory A} refers to theory A from the ancestry of

3734 the current context, not any accidental theory loader state as before.

3735 Potential INCOMPATIBILITY, subtle change in semantics.

3737 * Syntax.pretty_priority (default 0) configures the required priority

3738 of pretty-printed output and thus affects insertion of parentheses.

3740 * Syntax.default_root (default "any") configures the inner syntax

3741 category (nonterminal symbol) for parsing of terms.

3743 * Former exception Library.UnequalLengths now coincides with

3744 ListPair.UnequalLengths.

3746 * Renamed structure MetaSimplifier to Raw_Simplifier. Note that the

3747 main functionality is provided by structure Simplifier.

3749 * Renamed raw "explode" function to "raw_explode" to emphasize its

3750 meaning. Note that internally to Isabelle, Symbol.explode is used in

3751 almost all situations.

3753 * Discontinued obsolete function sys_error and exception SYS_ERROR.

3754 See implementation manual for further details on exceptions in

3755 Isabelle/ML.

3757 * Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its

3758 meaning.

3760 * Renamed structure PureThy to Pure_Thy and moved most of its

3761 operations to structure Global_Theory, to emphasize that this is

3762 rarely-used global-only stuff.

3764 * Discontinued Output.debug. Minor INCOMPATIBILITY, use plain writeln

3765 instead (or tracing for high-volume output).

3767 * Configuration option show_question_marks only affects regular pretty

3768 printing of types and terms, not raw Term.string_of_vname.

3770 * ML_Context.thm and ML_Context.thms are no longer pervasive. Rare

3771 INCOMPATIBILITY, superseded by static antiquotations @{thm} and

3772 @{thms} for most purposes.

3774 * ML structure Unsynchronized is never opened, not even in Isar

3775 interaction mode as before. Old Unsynchronized.set etc. have been

3776 discontinued -- use plain := instead. This should be *rare* anyway,

3777 since modern tools always work via official context data, notably

3778 configuration options.

3780 * Parallel and asynchronous execution requires special care concerning

3781 interrupts. Structure Exn provides some convenience functions that

3782 avoid working directly with raw Interrupt. User code must not absorb

3783 interrupts -- intermediate handling (for cleanup etc.) needs to be

3784 followed by re-raising of the original exception. Another common

3785 source of mistakes are "handle _" patterns, which make the meaning of

3786 the program subject to physical effects of the environment.

3790 New in Isabelle2009-2 (June 2010)

3791 ---------------------------------

3793 *** General ***

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

3796 constructors, term constants): provides simple and robust

3797 correspondence between formal entities and concrete syntax. Within

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

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

3800 their full internal name.

3802 Substantial INCOMPATIBILITY concerning low-level syntax declarations

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

3804 Some hints on upgrading:

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

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

3808 which are independent of this issue.

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

3811 provides the following special forms:

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

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

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

3817 Plain identifiers are treated as AST variables -- occasionally the

3818 system indicates accidental variables via the error "rhs contains

3819 extra variables".

3821 Type classes and type constructors are marked according to their

3822 concrete syntax. Some old translations rules need to be written

3823 for the "type" category, using type constructor application

3824 instead of pseudo-term application of the default category

3825 "logic".

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

3828 antiquotations:

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

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

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

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

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

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

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

3838 antiquotations.

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

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

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

3843 diagnose syntax problems.

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

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

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

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

3850 similar to the 'notation' command in theory specifications.

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

3853 need to specify constant name and syntax separately. Internal ML

3854 datatype constructors have been renamed from InfixName to Infix etc.

3855 Minor INCOMPATIBILITY.

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

3858 via commands 'schematic_lemma', 'schematic_theorem',

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

3860 syntactically clear, which impacts performance in a parallel or

3861 asynchronous interactive environment. Minor INCOMPATIBILITY.

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

3864 discontinued (old legacy feature).

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

3867 configuration options stored in the context. Enabling tracing (the

3868 case of debugging is similar) in proofs works via

3870 using [[trace_simp = true]]

3872 Tracing is then active for all invocations of the simplifier in

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

3874 disabled via the ProofGeneral settings menu.

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

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

3878 INCOMPATIBILITY.

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

3881 more efficient than combinations with -q1 or -q2.

3884 *** Pure ***

3886 * Proofterms record type-class reasoning explicitly, using the

3887 "unconstrain" operation internally. This eliminates all sort

3888 constraints from a theorem and proof, introducing explicit

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

3890 automatically applied at theorem boundaries, such that closed proofs

3891 are always free of sort constraints. INCOMPATIBILITY for tools that

3892 inspect proof terms.

3894 * Local theory specifications may depend on extra type variables that

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

3896 are added internally. For example:

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

3900 * Predicates of locales introduced by classes carry a mandatory

3901 "class" prefix. INCOMPATIBILITY.

3903 * Vacuous class specifications observe default sort. INCOMPATIBILITY.

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

3906 'class' instead.

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

3909 runtime environment; replaces immature code_datatype antiquotation.

3910 INCOMPATIBILITY.

3912 * Code generator: simple concept for abstract datatypes obeying

3913 invariants.

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

3916 user space functionality any longer.

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

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

3920 INCOMPATIBILITY.

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

3923 experiment with Isar, without producing any persistent result.

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

3926 within a local theory context, with explicit checking of the

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

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

3930 context -- without introducing dependencies on parameters or

3931 assumptions, which is not possible in Isabelle/Pure.

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

3934 within a local theory context. Minor INCOMPATIBILITY.

3937 *** HOL ***

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

3940 introducing dependencies on parameters or assumptions, which is not

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

3942 contain multiple interpretations of local typedefs (with different

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

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

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

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

3948 quotienting pairs of natural numbers:

3950 fun

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

3952 where

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

3955 quotient_type int = "nat * nat" / intrel

3956 by (auto simp add: equivp_def expand_fun_eq)

3958 quotient_definition

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

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

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

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

3964 construction and provides a reasoning infrastructure for finite sets.

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

3967 clash with new theory Quotient in Main HOL.

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

3970 separate HOL-SMT session.

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

3973 INCOMPATIBILITY.

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

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

3977 the AFP entry RSAPPS.

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

3980 longer shadowed. INCOMPATIBILITY.

3982 * Dropped theorem duplicate comp_arith; use semiring_norm instead.

3983 INCOMPATIBILITY.

3985 * Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.

3986 INCOMPATIBILITY.

3988 * Dropped normalizing_semiring etc; use the facts in semiring classes

3989 instead. INCOMPATIBILITY.

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

3992 ceiling; use the generic lemmas from theory "Archimedean_Field"

3993 instead. INCOMPATIBILITY.

3995 floor_number_of_eq ~> floor_number_of

3996 le_floor_eq_number_of ~> number_of_le_floor

3997 le_floor_eq_zero ~> zero_le_floor

3998 le_floor_eq_one ~> one_le_floor

3999 floor_less_eq_number_of ~> floor_less_number_of

4000 floor_less_eq_zero ~> floor_less_zero

4001 floor_less_eq_one ~> floor_less_one

4002 less_floor_eq_number_of ~> number_of_less_floor

4003 less_floor_eq_zero ~> zero_less_floor

4004 less_floor_eq_one ~> one_less_floor

4005 floor_le_eq_number_of ~> floor_le_number_of

4006 floor_le_eq_zero ~> floor_le_zero

4007 floor_le_eq_one ~> floor_le_one

4008 floor_subtract_number_of ~> floor_diff_number_of

4009 floor_subtract_one ~> floor_diff_one

4010 ceiling_number_of_eq ~> ceiling_number_of

4011 ceiling_le_eq_number_of ~> ceiling_le_number_of

4012 ceiling_le_zero_eq ~> ceiling_le_zero

4013 ceiling_le_eq_one ~> ceiling_le_one

4014 less_ceiling_eq_number_of ~> number_of_less_ceiling

4015 less_ceiling_eq_zero ~> zero_less_ceiling

4016 less_ceiling_eq_one ~> one_less_ceiling

4017 ceiling_less_eq_number_of ~> ceiling_less_number_of

4018 ceiling_less_eq_zero ~> ceiling_less_zero

4019 ceiling_less_eq_one ~> ceiling_less_one

4020 le_ceiling_eq_number_of ~> number_of_le_ceiling

4021 le_ceiling_eq_zero ~> zero_le_ceiling

4022 le_ceiling_eq_one ~> one_le_ceiling

4023 ceiling_subtract_number_of ~> ceiling_diff_number_of

4024 ceiling_subtract_one ~> ceiling_diff_one

4026 * Theory "Finite_Set": various folding_XXX locales facilitate the

4027 application of the various fold combinators on finite sets.

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

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

4031 implementation. INCOMPATIBILTY.

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

4034 AFP/thys/Coinductive.

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

4037 been removed. INCOMPATIBILITY.

4039 * Real: new development using Cauchy Sequences.

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

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

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

4045 "Int" etc. INCOMPATIBILITY.

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

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

4050 rewrites for all interpretations of the appropriate generic locales.

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

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

4054 appropriate and more consistent names suitable for name prefixes

4055 within the HOL theories. INCOMPATIBILITY.

4057 * Some generic constants have been put to appropriate theories:

4058 - less_eq, less: Orderings

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

4060 - inverse, divide: Rings

4061 INCOMPATIBILITY.

4063 * More consistent naming of type classes involving orderings (and

4064 lattices):

4066 lower_semilattice ~> semilattice_inf

4067 upper_semilattice ~> semilattice_sup

4069 dense_linear_order ~> dense_linorder

4071 pordered_ab_group_add ~> ordered_ab_group_add

4072 pordered_ab_group_add_abs ~> ordered_ab_group_add_abs

4073 pordered_ab_semigroup_add ~> ordered_ab_semigroup_add

4074 pordered_ab_semigroup_add_imp_le ~> ordered_ab_semigroup_add_imp_le

4075 pordered_cancel_ab_semigroup_add ~> ordered_cancel_ab_semigroup_add

4076 pordered_cancel_comm_semiring ~> ordered_cancel_comm_semiring

4077 pordered_cancel_semiring ~> ordered_cancel_semiring

4078 pordered_comm_monoid_add ~> ordered_comm_monoid_add

4079 pordered_comm_ring ~> ordered_comm_ring

4080 pordered_comm_semiring ~> ordered_comm_semiring

4081 pordered_ring ~> ordered_ring

4082 pordered_ring_abs ~> ordered_ring_abs

4083 pordered_semiring ~> ordered_semiring

4085 ordered_ab_group_add ~> linordered_ab_group_add

4086 ordered_ab_semigroup_add ~> linordered_ab_semigroup_add

4087 ordered_cancel_ab_semigroup_add ~> linordered_cancel_ab_semigroup_add

4088 ordered_comm_semiring_strict ~> linordered_comm_semiring_strict

4089 ordered_field ~> linordered_field

4090 ordered_field_no_lb ~> linordered_field_no_lb

4091 ordered_field_no_ub ~> linordered_field_no_ub

4092 ordered_field_dense_linear_order ~> dense_linordered_field

4093 ordered_idom ~> linordered_idom

4094 ordered_ring ~> linordered_ring

4095 ordered_ring_le_cancel_factor ~> linordered_ring_le_cancel_factor

4096 ordered_ring_less_cancel_factor ~> linordered_ring_less_cancel_factor

4097 ordered_ring_strict ~> linordered_ring_strict

4098 ordered_semidom ~> linordered_semidom

4099 ordered_semiring ~> linordered_semiring

4100 ordered_semiring_1 ~> linordered_semiring_1

4101 ordered_semiring_1_strict ~> linordered_semiring_1_strict

4102 ordered_semiring_strict ~> linordered_semiring_strict

4104 The following slightly odd type classes have been moved to a

4105 separate theory Library/Lattice_Algebras:

4107 lordered_ab_group_add ~> lattice_ab_group_add

4108 lordered_ab_group_add_abs ~> lattice_ab_group_add_abs

4109 lordered_ab_group_add_meet ~> semilattice_inf_ab_group_add

4110 lordered_ab_group_add_join ~> semilattice_sup_ab_group_add

4111 lordered_ring ~> lattice_ring

4113 INCOMPATIBILITY.

4115 * Refined field classes:

4116 - classes division_ring_inverse_zero, field_inverse_zero,

4117 linordered_field_inverse_zero include rule inverse 0 = 0 --

4118 subsumes former division_by_zero class;

4119 - numerous lemmas have been ported from field to division_ring.

4120 INCOMPATIBILITY.

4122 * Refined algebra theorem collections:

4123 - dropped theorem group group_simps, use algebra_simps instead;

4124 - dropped theorem group ring_simps, use field_simps instead;

4125 - proper theorem collection field_simps subsumes former theorem

4126 groups field_eq_simps and field_simps;

4127 - dropped lemma eq_minus_self_iff which is a duplicate for

4128 equal_neg_zero.

4129 INCOMPATIBILITY.

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

4132 sets to lattices:

4134 fun_left_comm_idem_inter ~> fun_left_comm_idem_inf

4135 fun_left_comm_idem_union ~> fun_left_comm_idem_sup

4136 inter_Inter_fold_inter ~> inf_Inf_fold_inf

4137 union_Union_fold_union ~> sup_Sup_fold_sup

4138 Inter_fold_inter ~> Inf_fold_inf

4139 Union_fold_union ~> Sup_fold_sup

4140 inter_INTER_fold_inter ~> inf_INFI_fold_inf

4141 union_UNION_fold_union ~> sup_SUPR_fold_sup

4142 INTER_fold_inter ~> INFI_fold_inf

4143 UNION_fold_union ~> SUPR_fold_sup

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

4146 replaced by the more convenient lemmas Inf_empty and Sup_empty.

4147 Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed

4148 by Inf_insert and Sup_insert. Lemmas Inf_UNIV and Sup_UNIV replace

4149 former Inf_Univ and Sup_Univ. Lemmas inf_top_right and sup_bot_right

4150 subsume inf_top and sup_bot respectively. INCOMPATIBILITY.

4152 * Reorganized theory Multiset: swapped notation of pointwise and

4153 multiset order:

4155 - pointwise ordering is instance of class order with standard syntax

4156 <= and <;

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

4158 are provided by means of interpretation with prefix

4159 multiset_order;

4160 - less duplication, less historical organization of sections,

4161 conversion from associations lists to multisets, rudimentary code

4162 generation;

4163 - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,

4164 if needed.

4166 Renamed:

4168 multiset_eq_conv_count_eq ~> multiset_ext_iff

4169 multi_count_ext ~> multiset_ext

4170 diff_union_inverse2 ~> diff_union_cancelR

4172 INCOMPATIBILITY.

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

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

4178 * Theory List: added transpose.

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

4181 between nat and other types, which supersedes the older libraries

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

4184 Constants:

4185 Nat_Int_Bij.nat2_to_nat ~> prod_encode

4186 Nat_Int_Bij.nat_to_nat2 ~> prod_decode

4187 Nat_Int_Bij.int_to_nat_bij ~> int_encode

4188 Nat_Int_Bij.nat_to_int_bij ~> int_decode

4189 Countable.pair_encode ~> prod_encode

4190 NatIso.prod2nat ~> prod_encode

4191 NatIso.nat2prod ~> prod_decode

4192 NatIso.sum2nat ~> sum_encode

4193 NatIso.nat2sum ~> sum_decode

4194 NatIso.list2nat ~> list_encode

4195 NatIso.nat2list ~> list_decode

4196 NatIso.set2nat ~> set_encode

4197 NatIso.nat2set ~> set_decode

4199 Lemmas:

4200 Nat_Int_Bij.bij_nat_to_int_bij ~> bij_int_decode

4201 Nat_Int_Bij.nat2_to_nat_inj ~> inj_prod_encode

4202 Nat_Int_Bij.nat2_to_nat_surj ~> surj_prod_encode

4203 Nat_Int_Bij.nat_to_nat2_inj ~> inj_prod_decode

4204 Nat_Int_Bij.nat_to_nat2_surj ~> surj_prod_decode

4205 Nat_Int_Bij.i2n_n2i_id ~> int_encode_inverse

4206 Nat_Int_Bij.n2i_i2n_id ~> int_decode_inverse

4207 Nat_Int_Bij.surj_nat_to_int_bij ~> surj_int_encode

4208 Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode

4209 Nat_Int_Bij.inj_nat_to_int_bij ~> inj_int_encode

4210 Nat_Int_Bij.inj_int_to_nat_bij ~> inj_int_decode

4211 Nat_Int_Bij.bij_nat_to_int_bij ~> bij_int_encode

4212 Nat_Int_Bij.bij_int_to_nat_bij ~> bij_int_decode

4214 * Sledgehammer:

4215 - Renamed ATP commands:

4216 atp_info ~> sledgehammer running_atps

4217 atp_kill ~> sledgehammer kill_atps

4218 atp_messages ~> sledgehammer messages

4219 atp_minimize ~> sledgehammer minimize

4220 print_atps ~> sledgehammer available_atps

4221 INCOMPATIBILITY.

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

4223 - Added option syntax and "sledgehammer_params" to customize

4224 Sledgehammer's behavior. See the manual for details.

4225 - Modified the Isar proof reconstruction code so that it produces

4226 direct proofs rather than proofs by contradiction. (This feature

4227 is still experimental.)

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

4229 full-typed mode.

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

4232 * Nitpick:

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

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

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

4236 of infinite datatypes based on a monotonicity analysis.

4237 - Added support for quotient types.

4238 - Added support for "specification" and "ax_specification"

4239 constructs.

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

4241 "termination" proofs).

4242 - Added support for term postprocessors.

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

4244 - Improved efficiency of "destroy_constrs" optimization.

4245 - Fixed soundness bugs related to "destroy_constrs" optimization and

4246 record getters.

4247 - Fixed soundness bug related to higher-order constructors.

4248 - Fixed soundness bug when "full_descrs" is enabled.

4249 - Improved precision of set constructs.

4250 - Added "atoms" option.

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

4252 problems.

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

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

4255 "SAT4J_Light". INCOMPATIBILITY.

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

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

4258 - Removed "nitpick_intro" attribute. INCOMPATIBILITY.

4260 * Method "induct" now takes instantiations of the form t, where t is not

4261 a variable, as a shorthand for "x == t", where x is a fresh variable.

4262 If this is not intended, t has to be enclosed in parentheses.

4263 By default, the equalities generated by definitional instantiations

4264 are pre-simplified, which may cause parameters of inductive cases

4265 to disappear, or may even delete some of the inductive cases.

4266 Use "induct (no_simp)" instead of "induct" to restore the old

4267 behaviour. The (no_simp) option is also understood by the "cases"

4268 and "nominal_induct" methods, which now perform pre-simplification, too.

4269 INCOMPATIBILITY.

4272 *** HOLCF ***

4274 * Variable names in lemmas generated by the domain package have

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

4276 package. Some proof scripts may be affected, INCOMPATIBILITY.

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

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

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

4281 be reformulated in terms of "foo_take", INCOMPATIBILITY.

4283 * Most definedness lemmas generated by the domain package (previously

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

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

4286 Proofs that used definedness lemmas as intro rules may break,

4287 potential INCOMPATIBILITY.

4289 * Induction and casedist rules generated by the domain package now

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

4291 constructor). INCOMPATIBILITY.

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

4294 rules are generated for each domain, INCOMPATIBILITY.

4296 foo_bar.reach ~> foo.reach bar.reach

4297 foo_bar.take_lemmas ~> foo.take_lemma bar.take_lemma

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

4300 consistency with the datatype package, INCOMPATIBILITY.

4302 foo.ind ~> foo.induct

4303 foo.finite_ind ~> foo.finite_induct

4304 foo.coind ~> foo.coinduct

4305 foo.casedist ~> foo.exhaust

4306 foo.exhaust ~> foo.nchotomy

4308 * For consistency with other definition packages, the fixrec package

4309 now generates qualified theorem names, INCOMPATIBILITY.

4311 foo_simps ~> foo.simps

4312 foo_unfold ~> foo.unfold

4313 foo_induct ~> foo.induct

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

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

4317 INCOMPATIBILITY.

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

4320 lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY.

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

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

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

4328 *** ML ***

4330 * Antiquotations for basic formal entities:

4332 @{class NAME} -- type class

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

4335 @{type_name NAME} -- logical type

4336 @{type_abbrev NAME} -- type abbreviation

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

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

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

4341 @{const_abbrev NAME} -- abbreviated constant

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

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

4345 syntax constant (cf. 'syntax' command).

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

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

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

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

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

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

4354 not work with the asynchronous Isar document model.

4356 * Configuration options now admit dynamic default values, depending on

4357 the context or even global references.

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

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

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

4363 for some time as aliases within the structure Legacy:

4365 OuterKeyword ~> Keyword

4366 OuterLex ~> Token

4367 OuterParse ~> Parse

4368 OuterSyntax ~> Outer_Syntax

4369 PrintMode ~> Print_Mode

4370 SpecParse ~> Parse_Spec

4371 ThyInfo ~> Thy_Info

4372 ThyLoad ~> Thy_Load

4373 ThyOutput ~> Thy_Output

4374 TypeInfer ~> Type_Infer

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

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

4379 * Most operations that refer to a global context are named

4380 accordingly, e.g. Simplifier.global_context or

4381 ProofContext.init_global. There are some situations where a global

4382 context actually works, but under normal circumstances one needs to

4383 pass the proper local context through the code!

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

4386 needs to be pure. Functor Theory_Data_PP retains the traditional

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

4388 Theory_Data version.

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

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

4392 inference kernel becomes invariant under addition of class relations,

4393 which is an important monotonicity principle. Sorts are now minimized

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

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

4396 explicitly in rare situations.

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

4399 emphasize that this is in no way a standard operation.

4400 INCOMPATIBILITY.

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

4403 usual for resolution. Rare INCOMPATIBILITY.

4405 * Renamed varify/unvarify operations to varify_global/unvarify_global

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

4407 quite rare).

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

4410 as infinity (as in chop). Subtle INCOMPATIBILITY.

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

4413 order of type variables. INCOMPATIBILITY for tools working with proof

4414 terms.

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

4417 may no longer carry premises. User-level specifications are

4418 transformed accordingly by Thm.add_axiom/add_def.

4421 *** System ***

4423 * Discontinued special HOL_USEDIR_OPTIONS for the main HOL image;

4424 ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions. Note that

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

4427 * Discontinued old ISABELLE and ISATOOL environment settings (legacy

4428 feature since Isabelle2009). Use ISABELLE_PROCESS and ISABELLE_TOOL,

4429 respectively.

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

4432 ISABELLE_PLATFORM setting variable, which defaults to the 32 bit

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

4434 prefers 64 bit if available:

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

4438 * The preliminary Isabelle/jEdit application demonstrates the emerging

4439 Isabelle/Scala layer for advanced prover interaction and integration.

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

4441 component.

4443 * "IsabelleText" is a Unicode font derived from Bitstream Vera Mono

4444 and Bluesky TeX fonts. It provides the usual Isabelle symbols,

4445 similar to the default assignment of the document preparation system

4446 (cf. isabellesym.sty). The Isabelle/Scala class Isabelle_System

4447 provides some operations for direct access to the font without asking

4448 the user for manual installation.

4452 New in Isabelle2009-1 (December 2009)

4453 -------------------------------------

4455 *** General ***

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

4458 one backslash should be used, even in ML sources.

4461 *** Pure ***

4463 * Locale interpretation propagates mixins along the locale hierarchy.

4464 The currently only available mixins are the equations used to map

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

4467 * Reactivated diagnostic command 'print_interps'. Use "print_interps

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

4469 Interpretations in proofs are not shown.

4471 * Thoroughly revised locales tutorial. New section on conditional

4472 interpretation.

4474 * On instantiation of classes, remaining undefined class parameters

4475 are formally declared. INCOMPATIBILITY.

4478 *** Document preparation ***

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

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

4482 backward compatibility). Styles can be also applied for

4483 antiquotations prop, term_type and typeof.

4486 *** HOL ***

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

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

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

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

4492 procedure based on external SMT solvers using the oracle mechanism;

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

4494 are provided to avoid calling the external solvers solely for

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

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

4498 * New commands to load and prove verification conditions generated by

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

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

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

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

4504 src/HOL/Nitpick_Examples.

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

4507 compiler and to enumerate values of inductive predicates.

4509 * A tabled implementation of the reflexive transitive closure.

4511 * New implementation of quickcheck uses generic code generator;

4512 default generators are provided for all suitable HOL types, records

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

4514 Library/SML_Quickcheck.

4516 * New testing tool Mirabelle for automated proof tools. Applies

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

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

4519 "mirabelle" utility.

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

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

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

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

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

4526 inequalities between polynomials. It makes use of external

4527 semidefinite programming solvers. Method "sos" generates a

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

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

4530 src/HOL/Library/Sum_Of_Squares.

4532 * New method "linarith" invokes existing linear arithmetic decision

4533 procedure only.

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

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

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

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

4540 that fail later.

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

4543 information in order to avoid failures of proof reconstruction.

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

4546 the same method as the approximation method.

4548 * Method "approximate" now supports arithmetic expressions as

4549 boundaries of intervals and implements interval splitting and Taylor

4550 series expansion.

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

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

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

4556 reals.

4558 * New theory Probability, which contains a development of measure

4559 theory, eventually leading to Lebesgue integration and probability.

4561 * Extended Multivariate Analysis to include derivation and Brouwer's

4562 fixpoint theorem.

4564 * Reorganization of number theory, INCOMPATIBILITY:

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

4566 and GCD as well as in new session Number_Theory

4567 - some constants and facts now suffixed with _nat and _int

4568 accordingly

4569 - former session NumberTheory now named Old_Number_Theory, including

4570 theories Legacy_GCD and Primes (prefer Number_Theory if possible)

4571 - moved theory Pocklington from src/HOL/Library to

4572 src/HOL/Old_Number_Theory

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

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

4576 lattice.

4578 * Class semiring_div requires superclass no_zero_divisors and proof of

4579 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,

4580 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been

4581 generalized to class semiring_div, subsuming former theorems

4582 zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and

4583 zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.

4584 INCOMPATIBILITY.

4586 * Refinements to lattice classes and sets:

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

4588 intro/elim rules in class variant: more uniformity

4589 - lemma ge_sup_conv renamed to le_sup_iff, in accordance with

4590 le_inf_iff

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

4592 sup_aci)

4593 - renamed ACI to inf_sup_aci

4594 - new class "boolean_algebra"

4595 - class "complete_lattice" moved to separate theory

4596 "Complete_Lattice"; corresponding constants (and abbreviations)

4597 renamed and with authentic syntax:

4598 Set.Inf ~> Complete_Lattice.Inf

4599 Set.Sup ~> Complete_Lattice.Sup

4600 Set.INFI ~> Complete_Lattice.INFI

4601 Set.SUPR ~> Complete_Lattice.SUPR

4602 Set.Inter ~> Complete_Lattice.Inter

4603 Set.Union ~> Complete_Lattice.Union

4604 Set.INTER ~> Complete_Lattice.INTER

4605 Set.UNION ~> Complete_Lattice.UNION

4606 - authentic syntax for

4607 Set.Pow

4608 Set.image

4609 - mere abbreviations:

4610 Set.empty (for bot)

4611 Set.UNIV (for top)

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

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

4614 Complete_Lattice.Inter (for Inf)

4615 Complete_Lattice.Union (for Sup)

4616 Complete_Lattice.INTER (for INFI)

4617 Complete_Lattice.UNION (for SUPR)

4618 - object-logic definitions as far as appropriate

4620 INCOMPATIBILITY. Care is required when theorems Int_subset_iff or

4621 Un_subset_iff are explicitly deleted as default simp rules; then also

4622 their lattice counterparts le_inf_iff and le_sup_iff have to be

4623 deleted to achieve the desired effect.

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

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

4627 etc. INCOMPATIBILITY.

4629 * Rules sup_Int_eq and sup_Un_eq are no longer declared as

4630 pred_set_conv by default. INCOMPATIBILITY.

4632 * Power operations on relations and functions are now one dedicated

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

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

4635 in class power. INCOMPATIBILITY.

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

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

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

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

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

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

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

4645 INCOMPATIBILITY.

4647 * Most rules produced by inductive and datatype package have mandatory

4648 prefixes. INCOMPATIBILITY.

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

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

4652 DERIV_intros assumes composition with an additional function and

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

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

4655 of most elementary terms. Former Maclauren.DERIV_tac and

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

4657 INCOMPATIBILITY.

4659 * Code generator attributes follow the usual underscore convention:

4660 code_unfold replaces code unfold

4661 code_post replaces code post

4662 etc.

4663 INCOMPATIBILITY.

4665 * Renamed methods:

4666 sizechange -> size_change

4667 induct_scheme -> induction_schema

4668 INCOMPATIBILITY.

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

4671 INCOMPATIBILITY, use "undefined" directly.

4673 * Renamed theorems:

4674 Suc_eq_add_numeral_1 -> Suc_eq_plus1

4675 Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left

4676 Suc_plus1 -> Suc_eq_plus1

4677 *anti_sym -> *antisym*

4678 vector_less_eq_def -> vector_le_def

4679 INCOMPATIBILITY.

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

4682 INCOMPATIBILITY.

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

4685 INCOMPATIBILITY.

4688 *** HOLCF ***

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

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

4692 Instances are provided for all type constructors defined in HOLCF.

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

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

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

4697 recursion using previously-defined type constructors. See

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

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

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

4702 simplification. Rewriting is done using rules declared with the

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

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

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

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

4708 constructor are pre-configured.

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

4711 for mutually-recursive definitions: Induction rules have conclusions

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

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

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

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

4717 as well.)

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

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

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

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

4723 examples.

4726 *** ML ***

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

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

4731 * Structure Name_Space (formerly NameSpace) now manages uniquely

4732 identified entries, with some additional information such as source

4733 position, logical grouping etc.

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

4736 modernized functors Theory_Data, Proof_Data, Generic_Data. Data needs

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

4738 copy operation) is still available for some time.

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

4741 provides a high-level programming interface to synchronized state

4742 variables with atomic update. This works via pure function

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

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

4745 either directly or indirectly via other synchronized variables!

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

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

4749 behaviour. The Isar toplevel keeps this structure open, to

4750 accommodate Proof General as well as quick and dirty interactive

4751 experiments with references.

4753 * PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for

4754 parallel tactical reasoning.

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

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

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

4759 body tactic may introduce new subgoals and schematic variables.

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

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

4763 or Subgoal.FOCUS etc.

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

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

4767 separately.) Minor INCOMPATIBILITY.

4769 * Renamed NamedThmsFun to Named_Thms. INCOMPATIBILITY.

4771 * Renamed several structures FooBar to Foo_Bar. Occasional,

4772 INCOMPATIBILITY.

4774 * Operations of structure Skip_Proof no longer require quick_and_dirty

4775 mode, which avoids critical setmp.

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

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

4779 Attrib/Method.setup introduced in Isabelle2009.

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

4782 back on global_simpset_of, global_claset_of, global_clasimpset_of as

4783 last resort. INCOMPATIBILITY.

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

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

4787 or even Display.pretty_thm_without_context as last resort.

4788 INCOMPATIBILITY.

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

4791 Syntax.pretty_typ/term directly, preferably with proper context

4792 instead of global theory.

4795 *** System ***

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

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

4799 usedir option -q.

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

4802 also the system manual.

4804 * The isabelle makeall tool now operates on all components with

4805 IsaMakefile, not just hardwired "logics".

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

4808 this is always enabled.

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

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

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

4814 currently supported on Linux only.

4818 New in Isabelle2009 (April 2009)

4819 --------------------------------

4821 *** General ***

4823 * Simplified main Isabelle executables, with less surprises on

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

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

4827 "isatool."

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

4830 removed (should rarely occur to regular users).

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

4833 removed (interfaces are now regular Isabelle tools).

4835 Within scripts and make files, the Isabelle environment variables

4836 ISABELLE_TOOL and ISABELLE_PROCESS replace old ISATOOL and ISABELLE,

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

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

4840 the interface was uninstalled or changed otherwise. Individual

4841 interface tool configuration is now more explicit, see also the

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

4843 via "isabelle emacs".

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

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

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

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

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

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

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

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

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

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

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

4859 * Proofs of fully specified statements are run in parallel on

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

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

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

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

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

4866 as hyperlinks are now available uniformly.

4869 *** Pure ***

4871 * Complete re-implementation of locales. INCOMPATIBILITY in several

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

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

4875 - In locale expressions, instantiation replaces renaming. Parameters

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

4877 parameter inheritance, in locale declarations, parameters that are not

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

4879 with their syntax at the beginning of the for clause.

4881 - Syntax from abbreviations and definitions in locales is available in

4882 locale expressions and context elements. The latter is particularly

4883 useful in locale declarations.

4885 - More flexible mechanisms to qualify names generated by locale

4886 expressions. Qualifiers (prefixes) may be specified in locale

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

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

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

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

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

4892 implicit qualifiers derived from the parameter names of a locale are

4893 no longer generated.

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

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

4897 brackets) is no longer available. Use locale expressions.

4899 - When converting proof scripts, mandatory qualifiers in

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

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

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

4903 in locale expressions range over a single locale instance only.

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

4906 In existing theorem specifications replace the includes element by the

4907 respective context elements of the included locale, omitting those

4908 that are already present in the theorem specification. Multiple

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

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

4911 notably theorems) may be regained by interpreting the respective

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

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

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

4916 consider declaring a new locale with additional type constraints on

4917 the parameters (context element "constrains").

4919 - Discontinued "locale (open)". INCOMPATIBILITY.

4921 - Locale interpretation commands no longer attempt to simplify goal.

4922 INCOMPATIBILITY: in rare situations the generated goal differs. Use

4923 methods intro_locales and unfold_locales to clarify.

4925 - Locale interpretation commands no longer accept interpretation

4926 attributes. INCOMPATIBILITY.

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

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

4930 in HOL, write

4932 class foo = ...

4934 instead of

4936 class foo = type + ...

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

4939 parameter prefix any longer. INCOMPATIBILITY.

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

4942 INCOMPATIBILITY, use proper 'instantiation' target instead.

4944 * Recovered hiding of consts, which was accidentally broken in

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

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

4948 * Slightly more coherent Pure syntax, with updated documentation in

4949 isar-ref manual. Removed locales meta_term_syntax and

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

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

4952 directly in regular applications.

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

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

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

4958 interface with 'setup' command instead.

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

4961 theory context.

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

4964 context. INCOMPATIBILITY.

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

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

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

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

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

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

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

4975 The result contains an implicit sort hypotheses as before --

4976 SORT_CONSTRAINT premises are eliminated as part of the canonical rule

4977 normalization.

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

4980 addressing etc.

4982 * Changed defaults for unify configuration options:

4984 unify_trace_bound = 50 (formerly 25)

4985 unify_search_bound = 60 (formerly 30)

4987 * Different bookkeeping for code equations (INCOMPATIBILITY):

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

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

4991 parts of the code generator framework).

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

4994 attribute) gain priority over default code equations stemming

4995 from definition, primrec, fun etc.

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

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

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

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

5003 patterns, e.g.

5005 find_consts "_ => bool"

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

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

5009 conjunctive and queries may be negated by prefixing them with a

5010 hyphen:

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

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

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

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

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

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

5020 Cf. associated options in Proof General Isabelle settings menu,

5021 enabled by default, with reasonable timeout for pathological cases of

5022 higher-order unification.

5025 *** Document preparation ***

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

5028 demanding keyword 'by' and supporting the full method expression

5029 syntax just like the Isar command 'by'.

5032 *** HOL ***

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

5035 points Main and Complex_Main remain as before.

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

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

5039 experimentation and tool development. Note that user applications

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

5041 Main, as before.

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

5044 experimentation due to shorter build times.

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

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

5048 remains valid, but theories formerly using Complex_Main should now use

5049 new entry point Hypercomplex.

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

5052 Posix processes. Avoids potentially expensive forking of the ML

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

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

5055 within the theory via plain ML wrapper functions. Basic Sledgehammer

5056 commands are covered in the isar-ref manual.

5058 * Wrapper scripts for remote SystemOnTPTP service allows to use

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

5060 provers may be included via suitable ML wrappers, see also

5061 src/HOL/ATP_Linkup.thy.

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

5064 menu.

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

5067 (contains the empty clause).

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

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

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

5073 src/Tools/coherent.ML).

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

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

5077 logically there is no difference. INCOMPATIBILITY.

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

5080 result of the first successful evaluation mechanism is printed. In

5081 square brackets a particular named evaluation mechanisms may be

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

5083 src/HOL/ex/Eval_Examples.thy.

5085 * Normalization by evaluation now allows non-leftlinear equations.

5086 Declare with attribute [code nbe].

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

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

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

5091 are now presented as a list of individual projections

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

5093 explicit HOL conjunction is no longer supported. INCOMPATIBILITY, in

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

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

5096 rule: prod.exhaust) here.

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

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

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

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

5105 * New predicate "strict_mono" classifies strict functions on partial

5106 orders. With strict functions on linear orders, reasoning about

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

5108 "strict_mono_less_eq" and "strict_mono_less".

5110 * Some set operations are now proper qualified constants with

5111 authentic syntax. INCOMPATIBILITY:

5113 op Int ~> Set.Int

5114 op Un ~> Set.Un

5115 INTER ~> Set.INTER

5116 UNION ~> Set.UNION

5117 Inter ~> Set.Inter

5118 Union ~> Set.Union

5119 {} ~> Set.empty

5120 UNIV ~> Set.UNIV

5122 * Class complete_lattice with operations Inf, Sup, INFI, SUPR now in

5123 theory Set.

5125 * Auxiliary class "itself" has disappeared -- classes without any

5126 parameter are treated as expected by the 'class' command.

5128 * Leibnitz's Series for Pi and the arcus tangens and logarithm series.

5130 * Common decision procedures (Cooper, MIR, Ferrack, Approximation,

5131 Dense_Linear_Order) are now in directory HOL/Decision_Procs.

5133 * Theory src/HOL/Decision_Procs/Approximation provides the new proof

5134 method "approximation". It proves formulas on real values by using

5135 interval arithmetic. In the formulas are also the transcendental

5136 functions sin, cos, tan, atan, ln, exp and the constant pi are

5137 allowed. For examples see

5138 src/HOL/Descision_Procs/ex/Approximation_Ex.thy.

5140 * Theory "Reflection" now resides in HOL/Library.

5142 * Entry point to Word library now simply named "Word".

5143 INCOMPATIBILITY.

5145 * Made source layout more coherent with logical distribution

5146 structure:

5148 src/HOL/Library/RType.thy ~> src/HOL/Typerep.thy

5149 src/HOL/Library/Code_Message.thy ~> src/HOL/

5150 src/HOL/Library/GCD.thy ~> src/HOL/

5151 src/HOL/Library/Order_Relation.thy ~> src/HOL/

5152 src/HOL/Library/Parity.thy ~> src/HOL/

5153 src/HOL/Library/Univ_Poly.thy ~> src/HOL/

5154 src/HOL/Real/ContNotDenum.thy ~> src/HOL/Library/

5155 src/HOL/Real/Lubs.thy ~> src/HOL/

5156 src/HOL/Real/PReal.thy ~> src/HOL/

5157 src/HOL/Real/Rational.thy ~> src/HOL/

5158 src/HOL/Real/RComplete.thy ~> src/HOL/

5159 src/HOL/Real/RealDef.thy ~> src/HOL/

5160 src/HOL/Real/RealPow.thy ~> src/HOL/

5161 src/HOL/Real/Real.thy ~> src/HOL/

5162 src/HOL/Complex/Complex_Main.thy ~> src/HOL/

5163 src/HOL/Complex/Complex.thy ~> src/HOL/

5164 src/HOL/Complex/FrechetDeriv.thy ~> src/HOL/Library/

5165 src/HOL/Complex/Fundamental_Theorem_Algebra.thy ~> src/HOL/Library/

5166 src/HOL/Hyperreal/Deriv.thy ~> src/HOL/

5167 src/HOL/Hyperreal/Fact.thy ~> src/HOL/

5168 src/HOL/Hyperreal/Integration.thy ~> src/HOL/

5169 src/HOL/Hyperreal/Lim.thy ~> src/HOL/

5170 src/HOL/Hyperreal/Ln.thy ~> src/HOL/

5171 src/HOL/Hyperreal/Log.thy ~> src/HOL/

5172 src/HOL/Hyperreal/MacLaurin.thy ~> src/HOL/

5173 src/HOL/Hyperreal/NthRoot.thy ~> src/HOL/

5174 src/HOL/Hyperreal/Series.thy ~> src/HOL/

5175 src/HOL/Hyperreal/SEQ.thy ~> src/HOL/

5176 src/HOL/Hyperreal/Taylor.thy ~> src/HOL/

5177 src/HOL/Hyperreal/Transcendental.thy ~> src/HOL/

5178 src/HOL/Real/Float ~> src/HOL/Library/

5179 src/HOL/Real/HahnBanach ~> src/HOL/HahnBanach

5180 src/HOL/Real/RealVector.thy ~> src/HOL/

5182 src/HOL/arith_data.ML ~> src/HOL/Tools

5183 src/HOL/hologic.ML ~> src/HOL/Tools

5184 src/HOL/simpdata.ML ~> src/HOL/Tools

5185 src/HOL/int_arith1.ML ~> src/HOL/Tools/int_arith.ML

5186 src/HOL/int_factor_simprocs.ML ~> src/HOL/Tools

5187 src/HOL/nat_simprocs.ML ~> src/HOL/Tools

5188 src/HOL/Real/float_arith.ML ~> src/HOL/Tools

5189 src/HOL/Real/float_syntax.ML ~> src/HOL/Tools

5190 src/HOL/Real/rat_arith.ML ~> src/HOL/Tools

5191 src/HOL/Real/real_arith.ML ~> src/HOL/Tools

5193 src/HOL/Library/Array.thy ~> src/HOL/Imperative_HOL

5194 src/HOL/Library/Heap_Monad.thy ~> src/HOL/Imperative_HOL

5195 src/HOL/Library/Heap.thy ~> src/HOL/Imperative_HOL

5196 src/HOL/Library/Imperative_HOL.thy ~> src/HOL/Imperative_HOL

5197 src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL

5198 src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL

5200 * If methods "eval" and "evaluation" encounter a structured proof

5201 state with !!/==>, only the conclusion is evaluated to True (if

5202 possible), avoiding strange error messages.

5204 * Method "sizechange" automates termination proofs using (a

5205 modification of) the size-change principle. Requires SAT solver. See

5206 src/HOL/ex/Termination.thy for examples.

5208 * Simplifier: simproc for let expressions now unfolds if bound

5209 variable occurs at most once in let expression body. INCOMPATIBILITY.

5211 * Method "arith": Linear arithmetic now ignores all inequalities when

5212 fast_arith_neq_limit is exceeded, instead of giving up entirely.

5214 * New attribute "arith" for facts that should always be used

5215 automatically by arithmetic. It is intended to be used locally in

5216 proofs, e.g.

5218 assumes [arith]: "x > 0"

5220 Global usage is discouraged because of possible performance impact.

5222 * New classes "top" and "bot" with corresponding operations "top" and

5223 "bot" in theory Orderings; instantiation of class "complete_lattice"

5224 requires instantiation of classes "top" and "bot". INCOMPATIBILITY.

5226 * Changed definition lemma "less_fun_def" in order to provide an

5227 instance for preorders on functions; use lemma "less_le" instead.

5228 INCOMPATIBILITY.

5230 * Theory Orderings: class "wellorder" moved here, with explicit

5231 induction rule "less_induct" as assumption. For instantiation of

5232 "wellorder" by means of predicate "wf", use rule wf_wellorderI.

5233 INCOMPATIBILITY.

5235 * Theory Orderings: added class "preorder" as superclass of "order".

5236 INCOMPATIBILITY: Instantiation proofs for order, linorder

5237 etc. slightly changed. Some theorems named order_class.* now named

5238 preorder_class.*.

5240 * Theory Relation: renamed "refl" to "refl_on", "reflexive" to "refl,

5241 "diag" to "Id_on".

5243 * Theory Finite_Set: added a new fold combinator of type

5245 ('a => 'b => 'b) => 'b => 'a set => 'b

5247 Occasionally this is more convenient than the old fold combinator

5248 which is now defined in terms of the new one and renamed to

5249 fold_image.

5251 * Theories Ring_and_Field and OrderedGroup: The lemmas "group_simps"

5252 and "ring_simps" have been replaced by "algebra_simps" (which can be

5253 extended with further lemmas!). At the moment both still exist but

5254 the former will disappear at some point.

5256 * Theory Power: Lemma power_Suc is now declared as a simp rule in

5257 class recpower. Type-specific simp rules for various recpower types

5258 have been removed. INCOMPATIBILITY, rename old lemmas as follows:

5260 rat_power_0 -> power_0

5261 rat_power_Suc -> power_Suc

5262 realpow_0 -> power_0

5263 realpow_Suc -> power_Suc

5264 complexpow_0 -> power_0

5265 complexpow_Suc -> power_Suc

5266 power_poly_0 -> power_0

5267 power_poly_Suc -> power_Suc

5269 * Theories Ring_and_Field and Divides: Definition of "op dvd" has been

5270 moved to separate class dvd in Ring_and_Field; a couple of lemmas on

5271 dvd has been generalized to class comm_semiring_1. Likewise a bunch

5272 of lemmas from Divides has been generalized from nat to class

5273 semiring_div. INCOMPATIBILITY. This involves the following theorem

5274 renames resulting from duplicate elimination:

5276 dvd_def_mod ~> dvd_eq_mod_eq_0

5277 zero_dvd_iff ~> dvd_0_left_iff

5278 dvd_0 ~> dvd_0_right

5279 DIVISION_BY_ZERO_DIV ~> div_by_0

5280 DIVISION_BY_ZERO_MOD ~> mod_by_0

5281 mult_div ~> div_mult_self2_is_id

5282 mult_mod ~> mod_mult_self2_is_0

5284 * Theory IntDiv: removed many lemmas that are instances of class-based

5285 generalizations (from Divides and Ring_and_Field). INCOMPATIBILITY,

5286 rename old lemmas as follows:

5288 dvd_diff -> nat_dvd_diff

5289 dvd_zminus_iff -> dvd_minus_iff

5290 mod_add1_eq -> mod_add_eq

5291 mod_mult1_eq -> mod_mult_right_eq

5292 mod_mult1_eq' -> mod_mult_left_eq

5293 mod_mult_distrib_mod -> mod_mult_eq

5294 nat_mod_add_left_eq -> mod_add_left_eq

5295 nat_mod_add_right_eq -> mod_add_right_eq

5296 nat_mod_div_trivial -> mod_div_trivial

5297 nat_mod_mod_trivial -> mod_mod_trivial

5298 zdiv_zadd_self1 -> div_add_self1

5299 zdiv_zadd_self2 -> div_add_self2

5300 zdiv_zmult_self1 -> div_mult_self2_is_id

5301 zdiv_zmult_self2 -> div_mult_self1_is_id

5302 zdvd_triv_left -> dvd_triv_left

5303 zdvd_triv_right -> dvd_triv_right

5304 zdvd_zmult_cancel_disj -> dvd_mult_cancel_left

5305 zmod_eq0_zdvd_iff -> dvd_eq_mod_eq_0[symmetric]

5306 zmod_zadd_left_eq -> mod_add_left_eq

5307 zmod_zadd_right_eq -> mod_add_right_eq

5308 zmod_zadd_self1 -> mod_add_self1

5309 zmod_zadd_self2 -> mod_add_self2

5310 zmod_zadd1_eq -> mod_add_eq

5311 zmod_zdiff1_eq -> mod_diff_eq

5312 zmod_zdvd_zmod -> mod_mod_cancel

5313 zmod_zmod_cancel -> mod_mod_cancel

5314 zmod_zmult_self1 -> mod_mult_self2_is_0

5315 zmod_zmult_self2 -> mod_mult_self1_is_0

5316 zmod_1 -> mod_by_1

5317 zdiv_1 -> div_by_1

5318 zdvd_abs1 -> abs_dvd_iff

5319 zdvd_abs2 -> dvd_abs_iff

5320 zdvd_refl -> dvd_refl

5321 zdvd_trans -> dvd_trans

5322 zdvd_zadd -> dvd_add

5323 zdvd_zdiff -> dvd_diff

5324 zdvd_zminus_iff -> dvd_minus_iff

5325 zdvd_zminus2_iff -> minus_dvd_iff

5326 zdvd_zmultD -> dvd_mult_right

5327 zdvd_zmultD2 -> dvd_mult_left

5328 zdvd_zmult_mono -> mult_dvd_mono

5329 zdvd_0_right -> dvd_0_right

5330 zdvd_0_left -> dvd_0_left_iff

5331 zdvd_1_left -> one_dvd

5332 zminus_dvd_iff -> minus_dvd_iff

5334 * Theory Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY.

5336 * The real numbers offer decimal input syntax: 12.34 is translated

5337 into 1234/10^2. This translation is not reversed upon output.

5339 * Theory Library/Polynomial defines an abstract type 'a poly of

5340 univariate polynomials with coefficients of type 'a. In addition to

5341 the standard ring operations, it also supports div and mod. Code

5342 generation is also supported, using list-style constructors.

5344 * Theory Library/Inner_Product defines a class of real_inner for real

5345 inner product spaces, with an overloaded operation inner :: 'a => 'a

5346 => real. Class real_inner is a subclass of real_normed_vector from

5347 theory RealVector.

5349 * Theory Library/Product_Vector provides instances for the product

5350 type 'a * 'b of several classes from RealVector and Inner_Product.

5351 Definitions of addition, subtraction, scalar multiplication, norms,

5352 and inner products are included.

5354 * Theory Library/Bit defines the field "bit" of integers modulo 2. In

5355 addition to the field operations, numerals and case syntax are also

5356 supported.

5358 * Theory Library/Diagonalize provides constructive version of Cantor's

5359 first diagonalization argument.

5361 * Theory Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,

5362 zlcm (for int); carried together from various gcd/lcm developements in

5363 the HOL Distribution. Constants zgcd and zlcm replace former igcd and

5364 ilcm; corresponding theorems renamed accordingly. INCOMPATIBILITY,

5365 may recover tupled syntax as follows:

5367 hide (open) const gcd

5368 abbreviation gcd where

5369 "gcd == (%(a, b). GCD.gcd a b)"

5370 notation (output)

5371 GCD.gcd ("gcd '(_, _')")

5373 The same works for lcm, zgcd, zlcm.

5375 * Theory Library/Nat_Infinity: added addition, numeral syntax and more

5376 instantiations for algebraic structures. Removed some duplicate

5377 theorems. Changes in simp rules. INCOMPATIBILITY.

5379 * ML antiquotation @{code} takes a constant as argument and generates

5380 corresponding code in background and inserts name of the corresponding

5381 resulting ML value/function/datatype constructor binding in place.

5382 All occurrences of @{code} with a single ML block are generated

5383 simultaneously. Provides a generic and safe interface for

5384 instrumentalizing code generation. See

5385 src/HOL/Decision_Procs/Ferrack.thy for a more ambitious application.

5386 In future you ought to refrain from ad-hoc compiling generated SML

5387 code on the ML toplevel. Note that (for technical reasons) @{code}

5388 cannot refer to constants for which user-defined serializations are

5389 set. Refer to the corresponding ML counterpart directly in that

5390 cases.

5392 * Command 'rep_datatype': instead of theorem names the command now

5393 takes a list of terms denoting the constructors of the type to be

5394 represented as datatype. The characteristic theorems have to be

5395 proven. INCOMPATIBILITY. Also observe that the following theorems

5396 have disappeared in favour of existing ones:

5398 unit_induct ~> unit.induct

5399 prod_induct ~> prod.induct

5400 sum_induct ~> sum.induct

5401 Suc_Suc_eq ~> nat.inject

5402 Suc_not_Zero Zero_not_Suc ~> nat.distinct

5405 *** HOL-Algebra ***

5407 * New locales for orders and lattices where the equivalence relation

5408 is not restricted to equality. INCOMPATIBILITY: all order and lattice

5409 locales use a record structure with field eq for the equivalence.

5411 * New theory of factorial domains.

5413 * Units_l_inv and Units_r_inv are now simp rules by default.

5414 INCOMPATIBILITY. Simplifier proof that require deletion of l_inv

5415 and/or r_inv will now also require deletion of these lemmas.

5417 * Renamed the following theorems, INCOMPATIBILITY:

5419 UpperD ~> Upper_memD

5420 LowerD ~> Lower_memD

5421 least_carrier ~> least_closed

5422 greatest_carrier ~> greatest_closed

5423 greatest_Lower_above ~> greatest_Lower_below

5424 one_zero ~> carrier_one_zero

5425 one_not_zero ~> carrier_one_not_zero (collision with assumption)

5428 *** HOL-Nominal ***

5430 * Nominal datatypes can now contain type-variables.

5432 * Commands 'nominal_inductive' and 'equivariance' work with local

5433 theory targets.

5435 * Nominal primrec can now works with local theory targets and its

5436 specification syntax now conforms to the general format as seen in

5437 'inductive' etc.

5439 * Method "perm_simp" honours the standard simplifier attributes

5440 (no_asm), (no_asm_use) etc.

5442 * The new predicate #* is defined like freshness, except that on the

5443 left hand side can be a set or list of atoms.

5445 * Experimental command 'nominal_inductive2' derives strong induction

5446 principles for inductive definitions. In contrast to

5447 'nominal_inductive', which can only deal with a fixed number of

5448 binders, it can deal with arbitrary expressions standing for sets of

5449 atoms to be avoided. The only inductive definition we have at the

5450 moment that needs this generalisation is the typing rule for Lets in

5451 the algorithm W:

5453 Gamma |- t1 : T1 (x,close Gamma T1)::Gamma |- t2 : T2 x#Gamma

5454 -----------------------------------------------------------------

5455 Gamma |- Let x be t1 in t2 : T2

5457 In this rule one wants to avoid all the binders that are introduced by

5458 "close Gamma T1". We are looking for other examples where this

5459 feature might be useful. Please let us know.

5462 *** HOLCF ***

5464 * Reimplemented the simplification procedure for proving continuity

5465 subgoals. The new simproc is extensible; users can declare additional

5466 continuity introduction rules with the attribute [cont2cont].

5468 * The continuity simproc now uses a different introduction rule for

5469 solving continuity subgoals on terms with lambda abstractions. In

5470 some rare cases the new simproc may fail to solve subgoals that the

5471 old one could solve, and "simp add: cont2cont_LAM" may be necessary.

5472 Potential INCOMPATIBILITY.

5474 * Command 'fixrec': specification syntax now conforms to the general

5475 format as seen in 'inductive' etc. See src/HOLCF/ex/Fixrec_ex.thy for

5476 examples. INCOMPATIBILITY.

5479 *** ZF ***

5481 * Proof of Zorn's Lemma for partial orders.

5484 *** ML ***

5486 * Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for

5487 Poly/ML 5.2.1 or later. Important note: the TimeLimit facility

5488 depends on multithreading, so timouts will not work before Poly/ML

5489 5.2.1!

5491 * High-level support for concurrent ML programming, see

5492 src/Pure/Cuncurrent. The data-oriented model of "future values" is

5493 particularly convenient to organize independent functional

5494 computations. The concept of "synchronized variables" provides a

5495 higher-order interface for components with shared state, avoiding the

5496 delicate details of mutexes and condition variables. (Requires

5497 Poly/ML 5.2.1 or later.)

5499 * ML bindings produced via Isar commands are stored within the Isar

5500 context (theory or proof). Consequently, commands like 'use' and 'ML'

5501 become thread-safe and work with undo as expected (concerning

5502 top-level bindings, not side-effects on global references).

5503 INCOMPATIBILITY, need to provide proper Isar context when invoking the

5504 compiler at runtime; really global bindings need to be given outside a

5505 theory. (Requires Poly/ML 5.2 or later.)

5507 * Command 'ML_prf' is analogous to 'ML' but works within a proof

5508 context. Top-level ML bindings are stored within the proof context in

5509 a purely sequential fashion, disregarding the nested proof structure.

5510 ML bindings introduced by 'ML_prf' are discarded at the end of the

5511 proof. (Requires Poly/ML 5.2 or later.)

5513 * Simplified ML attribute and method setup, cf. functions Attrib.setup

5514 and Method.setup, as well as Isar commands 'attribute_setup' and

5515 'method_setup'. INCOMPATIBILITY for 'method_setup', need to simplify

5516 existing code accordingly, or use plain 'setup' together with old

5517 Method.add_method.

5519 * Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm

5520 to 'a -> thm, while results are always tagged with an authentic oracle

5521 name. The Isar command 'oracle' is now polymorphic, no argument type

5522 is specified. INCOMPATIBILITY, need to simplify existing oracle code

5523 accordingly. Note that extra performance may be gained by producing

5524 the cterm carefully, avoiding slow Thm.cterm_of.

5526 * Simplified interface for defining document antiquotations via

5527 ThyOutput.antiquotation, ThyOutput.output, and optionally

5528 ThyOutput.maybe_pretty_source. INCOMPATIBILITY, need to simplify user

5529 antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common

5530 examples.

5532 * More systematic treatment of long names, abstract name bindings, and

5533 name space operations. Basic operations on qualified names have been

5534 move from structure NameSpace to Long_Name, e.g. Long_Name.base_name,

5535 Long_Name.append. Old type bstring has been mostly replaced by

5536 abstract type binding (see structure Binding), which supports precise

5537 qualification by packages and local theory targets, as well as proper

5538 tracking of source positions. INCOMPATIBILITY, need to wrap old

5539 bstring values into Binding.name, or better pass through abstract

5540 bindings everywhere. See further src/Pure/General/long_name.ML,

5541 src/Pure/General/binding.ML and src/Pure/General/name_space.ML

5543 * Result facts (from PureThy.note_thms, ProofContext.note_thms,

5544 LocalTheory.note etc.) now refer to the *full* internal name, not the

5545 bstring as before. INCOMPATIBILITY, not detected by ML type-checking!

5547 * Disposed old type and term read functions (Sign.read_def_typ,

5548 Sign.read_typ, Sign.read_def_terms, Sign.read_term,

5549 Thm.read_def_cterms, Thm.read_cterm etc.). INCOMPATIBILITY, should

5550 use regular Syntax.read_typ, Syntax.read_term, Syntax.read_typ_global,

5551 Syntax.read_term_global etc.; see also OldGoals.read_term as last

5552 resort for legacy applications.

5554 * Disposed old declarations, tactics, tactic combinators that refer to

5555 the simpset or claset of an implicit theory (such as Addsimps,

5556 Simp_tac, SIMPSET). INCOMPATIBILITY, should use @{simpset} etc. in

5557 embedded ML text, or local_simpset_of with a proper context passed as

5558 explicit runtime argument.

5560 * Rules and tactics that read instantiations (read_instantiate,

5561 res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof

5562 context, which is required for parsing and type-checking. Moreover,

5563 the variables are specified as plain indexnames, not string encodings

5564 thereof. INCOMPATIBILITY.

5566 * Generic Toplevel.add_hook interface allows to analyze the result of

5567 transactions. E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML

5568 for theorem dependency output of transactions resulting in a new

5569 theory state.

5571 * ML antiquotations: block-structured compilation context indicated by

5572 \<lbrace> ... \<rbrace>; additional antiquotation forms:

5574 @{binding name} - basic name binding

5575 @{let ?pat = term} - term abbreviation (HO matching)

5576 @{note name = fact} - fact abbreviation

5577 @{thm fact} - singleton fact (with attributes)

5578 @{thms fact} - general fact (with attributes)

5579 @{lemma prop by method} - singleton goal

5580 @{lemma prop by meth1 meth2} - singleton goal

5581 @{lemma prop1 ... propN by method} - general goal

5582 @{lemma prop1 ... propN by meth1 meth2} - general goal

5583 @{lemma (open) ...} - open derivation

5586 *** System ***

5588 * The Isabelle "emacs" tool provides a specific interface to invoke

5589 Proof General / Emacs, with more explicit failure if that is not

5590 installed (the old isabelle-interface script silently falls back on

5591 isabelle-process). The PROOFGENERAL_HOME setting determines the

5592 installation location of the Proof General distribution.

5594 * Isabelle/lib/classes/Pure.jar provides basic support to integrate

5595 the Isabelle process into a JVM/Scala application. See

5596 Isabelle/lib/jedit/plugin for a minimal example. (The obsolete Java

5597 process wrapper has been discontinued.)

5599 * Added homegrown Isabelle font with unicode layout, see lib/fonts.

5601 * Various status messages (with exact source position information) are

5602 emitted, if proper markup print mode is enabled. This allows

5603 user-interface components to provide detailed feedback on internal

5604 prover operations.

5608 New in Isabelle2008 (June 2008)

5609 -------------------------------

5611 *** General ***

5613 * The Isabelle/Isar Reference Manual (isar-ref) has been reorganized

5614 and updated, with formally checked references as hyperlinks.

5616 * Theory loader: use_thy (and similar operations) no longer set the

5617 implicit ML context, which was occasionally hard to predict and in

5618 conflict with concurrency. INCOMPATIBILITY, use ML within Isar which

5619 provides a proper context already.

5621 * Theory loader: old-style ML proof scripts being *attached* to a thy

5622 file are no longer supported. INCOMPATIBILITY, regular 'uses' and

5623 'use' within a theory file will do the job.

5625 * Name space merge now observes canonical order, i.e. the second space

5626 is inserted into the first one, while existing entries in the first

5627 space take precedence. INCOMPATIBILITY in rare situations, may try to

5628 swap theory imports.

5630 * Syntax: symbol \<chi> is now considered a letter. Potential

5631 INCOMPATIBILITY in identifier syntax etc.

5633 * Outer syntax: string tokens no longer admit escaped white space,

5634 which was an accidental (undocumented) feature. INCOMPATIBILITY, use

5635 white space without escapes.

5637 * Outer syntax: string tokens may contain arbitrary character codes

5638 specified via 3 decimal digits (as in SML). E.g. "foo\095bar" for

5639 "foo_bar".

5642 *** Pure ***

5644 * Context-dependent token translations. Default setup reverts locally

5645 fixed variables, and adds hilite markup for undeclared frees.

5647 * Unused theorems can be found using the new command 'unused_thms'.

5648 There are three ways of invoking it:

5650 (1) unused_thms

5651 Only finds unused theorems in the current theory.

5653 (2) unused_thms thy_1 ... thy_n -

5654 Finds unused theorems in the current theory and all of its ancestors,

5655 excluding the theories thy_1 ... thy_n and all of their ancestors.

5657 (3) unused_thms thy_1 ... thy_n - thy'_1 ... thy'_m

5658 Finds unused theorems in the theories thy'_1 ... thy'_m and all of

5659 their ancestors, excluding the theories thy_1 ... thy_n and all of

5660 their ancestors.

5662 In order to increase the readability of the list produced by

5663 unused_thms, theorems that have been created by a particular instance

5664 of a theory command such as 'inductive' or 'function' are considered

5665 to belong to the same "group", meaning that if at least one theorem in

5666 this group is used, the other theorems in the same group are no longer

5667 reported as unused. Moreover, if all theorems in the group are

5668 unused, only one theorem in the group is displayed.

5670 Note that proof objects have to be switched on in order for

5671 unused_thms to work properly (i.e. !proofs must be >= 1, which is

5672 usually the case when using Proof General with the default settings).

5674 * Authentic naming of facts disallows ad-hoc overwriting of previous

5675 theorems within the same name space. INCOMPATIBILITY, need to remove

5676 duplicate fact bindings, or even accidental fact duplications. Note

5677 that tools may maintain dynamically scoped facts systematically, using

5678 PureThy.add_thms_dynamic.

5680 * Command 'hide' now allows to hide from "fact" name space as well.

5682 * Eliminated destructive theorem database, simpset, claset, and

5683 clasimpset. Potential INCOMPATIBILITY, really need to observe linear

5684 update of theories within ML code.

5686 * Eliminated theory ProtoPure and CPure, leaving just one Pure theory.

5687 INCOMPATIBILITY, object-logics depending on former Pure require

5688 additional setup PureThy.old_appl_syntax_setup; object-logics

5689 depending on former CPure need to refer to Pure.

5691 * Commands 'use' and 'ML' are now purely functional, operating on

5692 theory/local_theory. Removed former 'ML_setup' (on theory), use 'ML'

5693 instead. Added 'ML_val' as mere diagnostic replacement for 'ML'.

5694 INCOMPATIBILITY.

5696 * Command 'setup': discontinued implicit version with ML reference.

5698 * Instantiation target allows for simultaneous specification of class

5699 instance operations together with an instantiation proof.

5700 Type-checking phase allows to refer to class operations uniformly.

5701 See src/HOL/Complex/Complex.thy for an Isar example and

5702 src/HOL/Library/Eval.thy for an ML example.

5704 * Indexing of literal facts: be more serious about including only

5705 facts from the visible specification/proof context, but not the

5706 background context (locale etc.). Affects `prop` notation and method

5707 "fact". INCOMPATIBILITY: need to name facts explicitly in rare

5708 situations.

5710 * Method "cases", "induct", "coinduct": removed obsolete/undocumented

5711 "(open)" option, which used to expose internal bound variables to the

5712 proof text.

5714 * Isar statements: removed obsolete case "rule_context".

5715 INCOMPATIBILITY, better use explicit fixes/assumes.

5717 * Locale proofs: default proof step now includes 'unfold_locales';

5718 hence 'proof' without argument may be used to unfold locale

5719 predicates.

5722 *** Document preparation ***

5724 * Simplified pdfsetup.sty: color/hyperref is used unconditionally for

5725 both pdf and dvi (hyperlinks usually work in xdvi as well); removed

5726 obsolete thumbpdf setup (contemporary PDF viewers do this on the

5727 spot); renamed link color from "darkblue" to "linkcolor" (default

5728 value unchanged, can be redefined via \definecolor); no longer sets

5729 "a4paper" option (unnecessary or even intrusive).

5731 * Antiquotation @{lemma A method} proves proposition A by the given

5732 method (either a method name or a method name plus (optional) method

5733 arguments in parentheses) and prints A just like @{prop A}.

5736 *** HOL ***

5738 * New primrec package. Specification syntax conforms in style to

5739 definition/function/.... No separate induction rule is provided. The

5740 "primrec" command distinguishes old-style and new-style specifications

5741 by syntax. The former primrec package is now named OldPrimrecPackage.

5742 When adjusting theories, beware: constants stemming from new-style

5743 primrec specifications have authentic syntax.

5745 * Metis prover is now an order of magnitude faster, and also works

5746 with multithreading.

5748 * Metis: the maximum number of clauses that can be produced from a

5749 theorem is now given by the attribute max_clauses. Theorems that

5750 exceed this number are ignored, with a warning printed.

5752 * Sledgehammer no longer produces structured proofs by default. To

5753 enable, declare [[sledgehammer_full = true]]. Attributes

5754 reconstruction_modulus, reconstruction_sorts renamed

5755 sledgehammer_modulus, sledgehammer_sorts. INCOMPATIBILITY.

5757 * Method "induct_scheme" derives user-specified induction rules

5758 from well-founded induction and completeness of patterns. This factors

5759 out some operations that are done internally by the function package

5760 and makes them available separately. See

5761 src/HOL/ex/Induction_Scheme.thy for examples.

5763 * More flexible generation of measure functions for termination

5764 proofs: Measure functions can be declared by proving a rule of the

5765 form "is_measure f" and giving it the [measure_function] attribute.

5766 The "is_measure" predicate is logically meaningless (always true), and

5767 just guides the heuristic. To find suitable measure functions, the

5768 termination prover sets up the goal "is_measure ?f" of the appropriate

5769 type and generates all solutions by prolog-style backwards proof using

5770 the declared rules.

5772 This setup also deals with rules like

5774 "is_measure f ==> is_measure (list_size f)"

5776 which accommodates nested datatypes that recurse through lists.

5777 Similar rules are predeclared for products and option types.

5779 * Turned the type of sets "'a set" into an abbreviation for "'a => bool"

5781 INCOMPATIBILITIES:

5783 - Definitions of overloaded constants on sets have to be replaced by

5784 definitions on => and bool.

5786 - Some definitions of overloaded operators on sets can now be proved

5787 using the definitions of the operators on => and bool. Therefore,

5788 the following theorems have been renamed:

5790 subset_def -> subset_eq

5791 psubset_def -> psubset_eq

5792 set_diff_def -> set_diff_eq

5793 Compl_def -> Compl_eq

5794 Sup_set_def -> Sup_set_eq

5795 Inf_set_def -> Inf_set_eq

5796 sup_set_def -> sup_set_eq

5797 inf_set_def -> inf_set_eq

5799 - Due to the incompleteness of the HO unification algorithm, some

5800 rules such as subst may require manual instantiation, if some of

5801 the unknowns in the rule is a set.

5803 - Higher order unification and forward proofs:

5804 The proof pattern

5806 have "P (S::'a set)" <...>

5807 then have "EX S. P S" ..

5809 no longer works (due to the incompleteness of the HO unification

5810 algorithm) and must be replaced by the pattern

5812 have "EX S. P S"

5813 proof

5814 show "P S" <...>

5815 qed

5817 - Calculational reasoning with subst (or similar rules):

5818 The proof pattern

5820 have "P (S::'a set)" <...>

5821 also have "S = T" <...>

5822 finally have "P T" .

5824 no longer works (for similar reasons as the previous example) and

5825 must be replaced by something like

5827 have "P (S::'a set)" <...>

5828 moreover have "S = T" <...>

5829 ultimately have "P T" by simp

5831 - Tactics or packages written in ML code:

5832 Code performing pattern matching on types via

5834 Type ("set", [T]) => ...

5836 must be rewritten. Moreover, functions like strip_type or

5837 binder_types no longer return the right value when applied to a

5838 type of the form

5840 T1 => ... => Tn => U => bool

5842 rather than

5844 T1 => ... => Tn => U set

5846 * Merged theories Wellfounded_Recursion, Accessible_Part and

5847 Wellfounded_Relations to theory Wellfounded.

5849 * Explicit class "eq" for executable equality. INCOMPATIBILITY.

5851 * Class finite no longer treats UNIV as class parameter. Use class

5852 enum from theory Library/Enum instead to achieve a similar effect.

5853 INCOMPATIBILITY.

5855 * Theory List: rule list_induct2 now has explicitly named cases "Nil"

5856 and "Cons". INCOMPATIBILITY.

5858 * HOL (and FOL): renamed variables in rules imp_elim and swap.

5859 Potential INCOMPATIBILITY.

5861 * Theory Product_Type: duplicated lemmas split_Pair_apply and

5862 injective_fst_snd removed, use split_eta and prod_eqI instead.

5863 Renamed upd_fst to apfst and upd_snd to apsnd. INCOMPATIBILITY.

5865 * Theory Nat: removed redundant lemmas that merely duplicate lemmas of

5866 the same name in theory Orderings:

5868 less_trans

5869 less_linear

5870 le_imp_less_or_eq

5871 le_less_trans

5872 less_le_trans

5873 less_not_sym

5874 less_asym

5876 Renamed less_imp_le to less_imp_le_nat, and less_irrefl to

5877 less_irrefl_nat. Potential INCOMPATIBILITY due to more general types

5878 and different variable names.

5880 * Library/Option_ord.thy: Canonical order on option type.

5882 * Library/RBT.thy: Red-black trees, an efficient implementation of

5883 finite maps.

5885 * Library/Countable.thy: Type class for countable types.

5887 * Theory Int: The representation of numerals has changed. The infix

5888 operator BIT and the bit datatype with constructors B0 and B1 have

5889 disappeared. INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in

5890 place of "x BIT bit.B0" and "y BIT bit.B1", respectively. Theorems

5891 involving BIT, B0, or B1 have been renamed with "Bit0" or "Bit1"

5892 accordingly.

5894 * Theory Nat: definition of <= and < on natural numbers no longer

5895 depend on well-founded relations. INCOMPATIBILITY. Definitions

5896 le_def and less_def have disappeared. Consider lemmas not_less

5897 [symmetric, where ?'a = nat] and less_eq [symmetric] instead.

5899 * Theory Finite_Set: locales ACf, ACe, ACIf, ACIfSL and ACIfSLlin

5900 (whose purpose mainly is for various fold_set functionals) have been

5901 abandoned in favor of the existing algebraic classes

5902 ab_semigroup_mult, comm_monoid_mult, ab_semigroup_idem_mult,

5903 lower_semilattice (resp. upper_semilattice) and linorder.

5904 INCOMPATIBILITY.

5906 * Theory Transitive_Closure: induct and cases rules now declare proper

5907 case_names ("base" and "step"). INCOMPATIBILITY.

5909 * Theorem Inductive.lfp_ordinal_induct generalized to complete

5910 lattices. The form set-specific version is available as

5911 Inductive.lfp_ordinal_induct_set.

5913 * Renamed theorems "power.simps" to "power_int.simps".

5914 INCOMPATIBILITY.

5916 * Class semiring_div provides basic abstract properties of semirings

5917 with division and modulo operations. Subsumes former class dvd_mod.

5919 * Merged theories IntDef, Numeral and IntArith into unified theory

5920 Int. INCOMPATIBILITY.

5922 * Theory Library/Code_Index: type "index" now represents natural

5923 numbers rather than integers. INCOMPATIBILITY.

5925 * New class "uminus" with operation "uminus" (split of from class

5926 "minus" which now only has operation "minus", binary).

5927 INCOMPATIBILITY.

5929 * Constants "card", "internal_split", "option_map" now with authentic

5930 syntax. INCOMPATIBILITY.

5932 * Definitions subset_def, psubset_def, set_diff_def, Compl_def,

5933 le_bool_def, less_bool_def, le_fun_def, less_fun_def, inf_bool_def,

5934 sup_bool_def, Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def,

5935 Inf_fun_def, Sup_fun_def, inf_set_def, sup_set_def, Inf_set_def,

5936 Sup_set_def, le_def, less_def, option_map_def now with object

5937 equality. INCOMPATIBILITY.

5939 * Records. Removed K_record, and replaced it by pure lambda term

5940 %x. c. The simplifier setup is now more robust against eta expansion.

5941 INCOMPATIBILITY: in cases explicitly referring to K_record.

5943 * Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}.

5945 * Library/ListVector: new theory of arithmetic vector operations.

5947 * Library/Order_Relation: new theory of various orderings as sets of

5948 pairs. Defines preorders, partial orders, linear orders and

5949 well-orders on sets and on types.

5952 *** ZF ***

5954 * Renamed some theories to allow to loading both ZF and HOL in the

5955 same session:

5957 Datatype -> Datatype_ZF

5958 Inductive -> Inductive_ZF

5959 Int -> Int_ZF

5960 IntDiv -> IntDiv_ZF

5961 Nat -> Nat_ZF

5962 List -> List_ZF

5963 Main -> Main_ZF

5965 INCOMPATIBILITY: ZF theories that import individual theories below

5966 Main might need to be adapted. Regular theory Main is still

5967 available, as trivial extension of Main_ZF.

5970 *** ML ***

5972 * ML within Isar: antiquotation @{const name} or @{const

5973 name(typargs)} produces statically-checked Const term.

5975 * Functor NamedThmsFun: data is available to the user as dynamic fact

5976 (of the same name). Removed obsolete print command.

5978 * Removed obsolete "use_legacy_bindings" function.

5980 * The ``print mode'' is now a thread-local value derived from a global

5981 template (the former print_mode reference), thus access becomes

5982 non-critical. The global print_mode reference is for session

5983 management only; user-code should use print_mode_value,

5984 print_mode_active, PrintMode.setmp etc. INCOMPATIBILITY.

5986 * Functions system/system_out provide a robust way to invoke external

5987 shell commands, with propagation of interrupts (requires Poly/ML

5988 5.2.1). Do not use OS.Process.system etc. from the basis library!

5991 *** System ***

5993 * Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs ---

5994 in accordance with Proof General 3.7, which prefers GNU emacs.

5996 * isatool tty runs Isabelle process with plain tty interaction;

5997 optional line editor may be specified via ISABELLE_LINE_EDITOR

5998 setting, the default settings attempt to locate "ledit" and "rlwrap".

6000 * isatool browser now works with Cygwin as well, using general

6001 "javapath" function defined in Isabelle process environment.

6003 * YXML notation provides a simple and efficient alternative to

6004 standard XML transfer syntax. See src/Pure/General/yxml.ML and

6005 isatool yxml as described in the Isabelle system manual.

6007 * JVM class isabelle.IsabelleProcess (located in Isabelle/lib/classes)

6008 provides general wrapper for managing an Isabelle process in a robust

6009 fashion, with ``cooked'' output from stdin/stderr.

6011 * Rudimentary Isabelle plugin for jEdit (see Isabelle/lib/jedit),

6012 based on Isabelle/JVM process wrapper (see Isabelle/lib/classes).

6014 * Removed obsolete THIS_IS_ISABELLE_BUILD feature. NB: the documented

6015 way of changing the user's settings is via

6016 ISABELLE_HOME_USER/etc/settings, which is a fully featured bash

6017 script.

6019 * Multithreading.max_threads := 0 refers to the number of actual CPU

6020 cores of the underlying machine, which is a good starting point for

6021 optimal performance tuning. The corresponding usedir option -M allows

6022 "max" as an alias for "0". WARNING: does not work on certain versions

6023 of Mac OS (with Poly/ML 5.1).

6025 * isabelle-process: non-ML sessions are run with "nice", to reduce the

6026 adverse effect of Isabelle flooding interactive front-ends (notably

6027 ProofGeneral / XEmacs).

6031 New in Isabelle2007 (November 2007)

6032 -----------------------------------

6034 *** General ***

6036 * More uniform information about legacy features, notably a

6037 warning/error of "Legacy feature: ...", depending on the state of the

6038 tolerate_legacy_features flag (default true). FUTURE INCOMPATIBILITY:

6039 legacy features will disappear eventually.

6041 * Theory syntax: the header format ``theory A = B + C:'' has been

6042 discontinued in favour of ``theory A imports B C begin''. Use isatool

6043 fixheaders to convert existing theory files. INCOMPATIBILITY.

6045 * Theory syntax: the old non-Isar theory file format has been

6046 discontinued altogether. Note that ML proof scripts may still be used

6047 with Isar theories; migration is usually quite simple with the ML

6048 function use_legacy_bindings. INCOMPATIBILITY.

6050 * Theory syntax: some popular names (e.g. 'class', 'declaration',

6051 'fun', 'help', 'if') are now keywords. INCOMPATIBILITY, use double

6052 quotes.

6054 * Theory loader: be more serious about observing the static theory

6055 header specifications (including optional directories), but not the

6056 accidental file locations of previously successful loads. The strict

6057 update policy of former update_thy is now already performed by

6058 use_thy, so the former has been removed; use_thys updates several

6059 theories simultaneously, just as 'imports' within a theory header

6060 specification, but without merging the results. Potential

6061 INCOMPATIBILITY: may need to refine theory headers and commands

6062 ROOT.ML which depend on load order.

6064 * Theory loader: optional support for content-based file

6065 identification, instead of the traditional scheme of full physical

6066 path plus date stamp; configured by the ISABELLE_FILE_IDENT setting

6067 (cf. the system manual). The new scheme allows to work with

6068 non-finished theories in persistent session images, such that source

6069 files may be moved later on without requiring reloads.

6071 * Theory loader: old-style ML proof scripts being *attached* to a thy

6072 file (with the same base name as the theory) are considered a legacy

6073 feature, which will disappear eventually. Even now, the theory loader

6074 no longer maintains dependencies on such files.

6076 * Syntax: the scope for resolving ambiguities via type-inference is

6077 now limited to individual terms, instead of whole simultaneous

6078 specifications as before. This greatly reduces the complexity of the

6079 syntax module and improves flexibility by separating parsing and

6080 type-checking. INCOMPATIBILITY: additional type-constraints (explicit

6081 'fixes' etc.) are required in rare situations.

6083 * Syntax: constants introduced by new-style packages ('definition',

6084 'abbreviation' etc.) are passed through the syntax module in

6085 ``authentic mode''. This means that associated mixfix annotations

6086 really stick to such constants, independently of potential name space

6087 ambiguities introduced later on. INCOMPATIBILITY: constants in parse

6088 trees are represented slightly differently, may need to adapt syntax

6089 translations accordingly. Use CONST marker in 'translations' and

6090 @{const_syntax} antiquotation in 'parse_translation' etc.

6092 * Legacy goal package: reduced interface to the bare minimum required

6093 to keep existing proof scripts running. Most other user-level

6094 functions are now part of the OldGoals structure, which is *not* open

6095 by default (consider isatool expandshort before open OldGoals).

6096 Removed top_sg, prin, printyp, pprint_term/typ altogether, because

6097 these tend to cause confusion about the actual goal (!) context being

6098 used here, which is not necessarily the same as the_context().

6100 * Command 'find_theorems': supports "*" wild-card in "name:"

6101 criterion; "with_dups" option. Certain ProofGeneral versions might

6102 support a specific search form (see ProofGeneral/CHANGES).

6104 * The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1

6105 by default, which means that "prems" (and also "fixed variables") are

6106 suppressed from proof state output. Note that the ProofGeneral

6107 settings mechanism allows to change and save options persistently, but

6108 older versions of Isabelle will fail to start up if a negative prems

6109 limit is imposed.

6111 * Local theory targets may be specified by non-nested blocks of

6112 ``context/locale/class ... begin'' followed by ``end''. The body may

6113 contain definitions, theorems etc., including any derived mechanism

6114 that has been implemented on top of these primitives. This concept

6115 generalizes the existing ``theorem (in ...)'' towards more versatility

6116 and scalability.

6118 * Proof General interface: proper undo of final 'end' command;

6119 discontinued Isabelle/classic mode (ML proof scripts).

6122 *** Document preparation ***

6124 * Added antiquotation @{theory name} which prints the given name,

6125 after checking that it refers to a valid ancestor theory in the

6126 current context.

6128 * Added antiquotations @{ML_type text} and @{ML_struct text} which

6129 check the given source text as ML type/structure, printing verbatim.

6131 * Added antiquotation @{abbrev "c args"} which prints the abbreviation

6132 "c args == rhs" given in the current context. (Any number of

6133 arguments may be given on the LHS.)

6136 *** Pure ***

6138 * The 'class' package offers a combination of axclass and locale to

6139 achieve Haskell-like type classes in Isabelle. Definitions and

6140 theorems within a class context produce both relative results (with

6141 implicit parameters according to the locale context), and polymorphic

6142 constants with qualified polymorphism (according to the class

6143 context). Within the body context of a 'class' target, a separate

6144 syntax layer ("user space type system") takes care of converting

6145 between global polymorphic consts and internal locale representation.

6146 See src/HOL/ex/Classpackage.thy for examples (as well as main HOL).

6147 "isatool doc classes" provides a tutorial.

6149 * Generic code generator framework allows to generate executable

6150 code for ML and Haskell (including Isabelle classes). A short usage

6151 sketch:

6153 internal compilation:

6154 export_code <list of constants (term syntax)> in SML

6155 writing SML code to a file:

6156 export_code <list of constants (term syntax)> in SML <filename>

6157 writing OCaml code to a file:

6158 export_code <list of constants (term syntax)> in OCaml <filename>

6159 writing Haskell code to a bunch of files:

6160 export_code <list of constants (term syntax)> in Haskell <filename>

6162 evaluating closed propositions to True/False using code generation:

6163 method ``eval''

6165 Reasonable default setup of framework in HOL.

6167 Theorem attributs for selecting and transforming function equations theorems:

6169 [code fun]: select a theorem as function equation for a specific constant

6170 [code fun del]: deselect a theorem as function equation for a specific constant

6171 [code inline]: select an equation theorem for unfolding (inlining) in place

6172 [code inline del]: deselect an equation theorem for unfolding (inlining) in place

6174 User-defined serializations (target in {SML, OCaml, Haskell}):

6176 code_const <and-list of constants (term syntax)>

6177 {(target) <and-list of const target syntax>}+

6179 code_type <and-list of type constructors>

6180 {(target) <and-list of type target syntax>}+

6182 code_instance <and-list of instances>

6183 {(target)}+

6184 where instance ::= <type constructor> :: <class>

6186 code_class <and_list of classes>

6187 {(target) <and-list of class target syntax>}+

6188 where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}?

6190 code_instance and code_class only are effective to target Haskell.

6192 For example usage see src/HOL/ex/Codegenerator.thy and

6193 src/HOL/ex/Codegenerator_Pretty.thy. A separate tutorial on code

6194 generation from Isabelle/HOL theories is available via "isatool doc

6195 codegen".

6197 * Code generator: consts in 'consts_code' Isar commands are now

6198 referred to by usual term syntax (including optional type

6199 annotations).

6201 * Command 'no_translations' removes translation rules from theory

6202 syntax.

6204 * Overloaded definitions are now actually checked for acyclic

6205 dependencies. The overloading scheme is slightly more general than

6206 that of Haskell98, although Isabelle does not demand an exact

6207 correspondence to type class and instance declarations.

6208 INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to admit more

6209 exotic versions of overloading -- at the discretion of the user!

6211 Polymorphic constants are represented via type arguments, i.e. the

6212 instantiation that matches an instance against the most general

6213 declaration given in the signature. For example, with the declaration

6214 c :: 'a => 'a => 'a, an instance c :: nat => nat => nat is represented

6215 as c(nat). Overloading is essentially simultaneous structural

6216 recursion over such type arguments. Incomplete specification patterns

6217 impose global constraints on all occurrences, e.g. c('a * 'a) on the

6218 LHS means that more general c('a * 'b) will be disallowed on any RHS.

6219 Command 'print_theory' outputs the normalized system of recursive

6220 equations, see section "definitions".

6222 * Configuration options are maintained within the theory or proof

6223 context (with name and type bool/int/string), providing a very simple

6224 interface to a poor-man's version of general context data. Tools may

6225 declare options in ML (e.g. using Attrib.config_int) and then refer to

6226 these values using Config.get etc. Users may change options via an

6227 associated attribute of the same name. This form of context

6228 declaration works particularly well with commands 'declare' or

6229 'using', for example ``declare [[foo = 42]]''. Thus it has become

6230 very easy to avoid global references, which would not observe Isar

6231 toplevel undo/redo and fail to work with multithreading.

6233 Various global ML references of Pure and HOL have been turned into

6234 configuration options:

6236 Unify.search_bound unify_search_bound

6237 Unify.trace_bound unify_trace_bound

6238 Unify.trace_simp unify_trace_simp

6239 Unify.trace_types unify_trace_types

6240 Simplifier.simp_depth_limit simp_depth_limit

6241 Blast.depth_limit blast_depth_limit

6242 DatatypeProp.dtK datatype_distinctness_limit

6243 fast_arith_neq_limit fast_arith_neq_limit

6244 fast_arith_split_limit fast_arith_split_limit

6246 * Named collections of theorems may be easily installed as context

6247 data using the functor NamedThmsFun (see also

6248 src/Pure/Tools/named_thms.ML). The user may add or delete facts via

6249 attributes; there is also a toplevel print command. This facility is

6250 just a common case of general context data, which is the preferred way

6251 for anything more complex than just a list of facts in canonical

6252 order.

6254 * Isar: command 'declaration' augments a local theory by generic

6255 declaration functions written in ML. This enables arbitrary content

6256 being added to the context, depending on a morphism that tells the

6257 difference of the original declaration context wrt. the application

6258 context encountered later on.

6260 * Isar: proper interfaces for simplification procedures. Command

6261 'simproc_setup' declares named simprocs (with match patterns, and body

6262 text in ML). Attribute "simproc" adds/deletes simprocs in the current

6263 context. ML antiquotation @{simproc name} retrieves named simprocs.

6265 * Isar: an extra pair of brackets around attribute declarations

6266 abbreviates a theorem