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

NEWS

author | ballarin |

Wed Dec 11 10:12:48 2002 +0100 (2002-12-11) | |

changeset 13745 | a31e04831dd1 |

parent 13735 | 7de9342aca7a |

child 13781 | ecb2df44253e |

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

HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.

1 Isabelle NEWS -- history user-relevant changes

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

4 New in this Isabelle release

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

7 *** General ***

9 * Provers/linorder: New generic prover for transitivity reasoning over

10 linear orders. Note: this prover is not efficient!

12 * Provers/simplifier:

14 - Completely reimplemented Asm_full_simp_tac:

15 Assumptions are now subject to complete mutual simplification,

16 not just from left to right. The simplifier now preserves

17 the order of assumptions.

19 Potential INCOMPATIBILITY:

21 -- Asm_full_simp_tac sometimes diverges where the old version did

22 not, e.g. invoking Asm_full_simp_tac on the goal

24 [| P (f x); y = x; f x = f y |] ==> Q

26 now gives rise to the infinite reduction sequence

28 P (f x) --(f x = f y)--> P (f y) --(y = x)--> P (f x) --(f x = f y)--> ...

30 Using Asm_lr_simp_tac (or "simp (asm_lr)" in Isabelle/Isar) instead

31 often solves this kind of problem.

33 -- Tactics combining classical reasoner and simplification (such

34 as auto) are also affected by this change, because many of them

35 rely on Asm_full_simp_tac. They may sometimes diverge as well

36 or yield a different numbers of subgoals. Try to use e.g. force,

37 fastsimp, or safe instead of auto in case of problems. Sometimes

38 subsequent calls to the classical reasoner will fail because a

39 preceeding call to the simplifier too eagerly simplified the

40 goal, e.g. deleted redundant premises.

42 - The simplifier trace now shows the names of the applied rewrite rules

44 * Pure: new flag trace_unify_fail causes unification to print

45 diagnostic information (PG: in trace buffer) when it fails. This is

46 useful for figuring out why single step proofs like rule, erule or

47 assumption failed.

49 * Pure: you can find all matching introduction rules for subgoal 1,

50 i.e. all rules whose conclusion matches subgoal 1, by executing

51 ML"ProofGeneral.print_intros()"

52 The rules are ordered by how closely they match the subgoal.

53 In particular, rules that solve a subgoal outright are displayed first

54 (or rather last, the way it is printed).

55 TODO: integration with PG

57 * Pure: locale specifications now produce predicate definitions

58 according to the body of text (covering assumptions modulo local

59 definitions); predicate "loc_axioms" covers newly introduced text,

60 while "loc" is cumulative wrt. all included locale expressions; the

61 latter view is presented only on export into the global theory

62 context; potential INCOMPATIBILITY, use "(open)" option to fall back

63 on the old view without predicates;

65 * Pure: predefined locales "var" and "struct" are useful for sharing

66 parameters (as in CASL, for example); just specify something like

67 ``var x + var y + struct M'' as import;

69 * Pure: improved thms_containing: proper indexing of facts instead of

70 raw theorems; check validity of results wrt. current name space;

71 include local facts of proof configuration (also covers active

72 locales), cover fixed variables in index; may use "_" in term

73 specification; an optional limit for the number of printed facts may

74 be given (the default is 40);

76 * Pure: disallow duplicate fact bindings within new-style theory files

77 (batch-mode only);

79 * Provers: improved induct method: assumptions introduced by case

80 "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from

81 the goal statement); "foo" still refers to all facts collectively;

83 * Provers: the function blast.overloaded has been removed: all constants

84 are regarded as potentially overloaded, which improves robustness in exchange

85 for slight decrease in efficiency;

87 * Isar: preview of problems to finish 'show' now produce an error

88 rather than just a warning (in interactive mode);

91 *** HOL ***

93 * GroupTheory: new, experimental summation operator for abelian groups.

95 * New tactic "trans_tac" and method "trans" instantiate

96 Provers/linorder.ML for axclasses "order" and "linorder" (predicates

97 "<=", "<" and "=").

99 * function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main

100 HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp";

102 * 'typedef' command has new option "open" to suppress the set

103 definition;

105 * functions Min and Max on finite sets have been introduced (theory

106 Finite_Set);

108 * attribute [symmetric] now works for relations as well; it turns

109 (x,y) : R^-1 into (y,x) : R, and vice versa;

111 * arith(_tac) now produces a counter example if it cannot prove a theorem.

112 In ProofGeneral the counter example appears in the trace buffer.

114 * arith(_tac) does now know about div k and mod k where k is a numeral

115 of type nat or int. It can solve simple goals like

117 "0 < n ==> n div 2 < (n::nat)"

119 but fails if divisibility plays a role like in

121 "n div 2 + (n+1) div 2 = (n::nat)"

123 * simp's arithmetic capabilities have been enhanced a bit: it now

124 takes ~= in premises into account (by performing a case split);

126 * simp reduces "m*(n div m) + n mod m" to n, even if the two summands

127 are distributed over a sum of terms;

129 * induct over a !!-quantified statement (say !!x1..xn):

130 each "case" automatically performs "fix x1 .. xn" with exactly those names.

132 * GroupTheory: converted to Isar theories, using locales with implicit structures;

134 * Real/HahnBanach: updated and adapted to locales;

137 *** ZF ***

139 * ZF/Constructible: consistency proof for AC (Gödel's constructible

140 universe, etc.);

142 * Main ZF: many theories converted to new-style format;

145 *** ML ***

147 * Pure: Tactic.prove provides sane interface for internal proofs;

148 omits the infamous "standard" operation, so this is more appropriate

149 than prove_goalw_cterm in many situations (e.g. in simprocs);

151 * Pure: improved error reporting of simprocs;

153 * Provers: Simplifier.simproc(_i) provides sane interface for setting

154 up simprocs;

158 New in Isabelle2002 (March 2002)

159 --------------------------------

161 *** Document preparation ***

163 * greatly simplified document preparation setup, including more

164 graceful interpretation of isatool usedir -i/-d/-D options, and more

165 instructive isatool mkdir; users should basically be able to get

166 started with "isatool mkdir HOL Test && isatool make"; alternatively,

167 users may run a separate document processing stage manually like this:

168 "isatool usedir -D output HOL Test && isatool document Test/output";

170 * theory dependency graph may now be incorporated into documents;

171 isatool usedir -g true will produce session_graph.eps/.pdf for use

172 with \includegraphics of LaTeX;

174 * proper spacing of consecutive markup elements, especially text

175 blocks after section headings;

177 * support bold style (for single symbols only), input syntax is like

178 this: "\<^bold>\<alpha>" or "\<^bold>A";

180 * \<bullet> is now output as bold \cdot by default, which looks much

181 better in printed text;

183 * added default LaTeX bindings for \<tturnstile> and \<TTurnstile>;

184 note that these symbols are currently unavailable in Proof General /

185 X-Symbol; new symbols \<zero>, \<one>, ..., \<nine>, and \<euro>;

187 * isatool latex no longer depends on changed TEXINPUTS, instead

188 isatool document copies the Isabelle style files to the target

189 location;

192 *** Isar ***

194 * Pure/Provers: improved proof by cases and induction;

195 - 'case' command admits impromptu naming of parameters (such as

196 "case (Suc n)");

197 - 'induct' method divinates rule instantiation from the inductive

198 claim; no longer requires excessive ?P bindings for proper

199 instantiation of cases;

200 - 'induct' method properly enumerates all possibilities of set/type

201 rules; as a consequence facts may be also passed through *type*

202 rules without further ado;

203 - 'induct' method now derives symbolic cases from the *rulified*

204 rule (before it used to rulify cases stemming from the internal

205 atomized version); this means that the context of a non-atomic

206 statement becomes is included in the hypothesis, avoiding the

207 slightly cumbersome show "PROP ?case" form;

208 - 'induct' may now use elim-style induction rules without chaining

209 facts, using ``missing'' premises from the goal state; this allows

210 rules stemming from inductive sets to be applied in unstructured

211 scripts, while still benefitting from proper handling of non-atomic

212 statements; NB: major inductive premises need to be put first, all

213 the rest of the goal is passed through the induction;

214 - 'induct' proper support for mutual induction involving non-atomic

215 rule statements (uses the new concept of simultaneous goals, see

216 below);

217 - append all possible rule selections, but only use the first

218 success (no backtracking);

219 - removed obsolete "(simplified)" and "(stripped)" options of methods;

220 - undeclared rule case names default to numbers 1, 2, 3, ...;

221 - added 'print_induct_rules' (covered by help item in recent Proof

222 General versions);

223 - moved induct/cases attributes to Pure, methods to Provers;

224 - generic method setup instantiated for FOL and HOL;

226 * Pure: support multiple simultaneous goal statements, for example

227 "have a: A and b: B" (same for 'theorem' etc.); being a pure

228 meta-level mechanism, this acts as if several individual goals had

229 been stated separately; in particular common proof methods need to be

230 repeated in order to cover all claims; note that a single elimination

231 step is *not* sufficient to establish the two conjunctions, so this

232 fails:

234 assume "A & B" then have A and B .. (*".." fails*)

236 better use "obtain" in situations as above; alternative refer to

237 multi-step methods like 'auto', 'simp_all', 'blast+' etc.;

239 * Pure: proper integration with ``locales''; unlike the original

240 version by Florian Kammüller, Isar locales package high-level proof

241 contexts rather than raw logical ones (e.g. we admit to include

242 attributes everywhere); operations on locales include merge and

243 rename; support for implicit arguments (``structures''); simultaneous

244 type-inference over imports and text; see also HOL/ex/Locales.thy for

245 some examples;

247 * Pure: the following commands have been ``localized'', supporting a

248 target locale specification "(in name)": 'lemma', 'theorem',

249 'corollary', 'lemmas', 'theorems', 'declare'; the results will be

250 stored both within the locale and at the theory level (exported and

251 qualified by the locale name);

253 * Pure: theory goals may now be specified in ``long'' form, with

254 ad-hoc contexts consisting of arbitrary locale elements. for example

255 ``lemma foo: fixes x assumes "A x" shows "B x"'' (local syntax and

256 definitions may be given, too); the result is a meta-level rule with

257 the context elements being discharged in the obvious way;

259 * Pure: new proof command 'using' allows to augment currently used

260 facts after a goal statement ('using' is syntactically analogous to

261 'apply', but acts on the goal's facts only); this allows chained facts

262 to be separated into parts given before and after a claim, as in

263 ``from a and b have C using d and e <proof>'';

265 * Pure: renamed "antecedent" case to "rule_context";

267 * Pure: new 'judgment' command records explicit information about the

268 object-logic embedding (used by several tools internally); no longer

269 use hard-wired "Trueprop";

271 * Pure: added 'corollary' command;

273 * Pure: fixed 'token_translation' command;

275 * Pure: removed obsolete 'exported' attribute;

277 * Pure: dummy pattern "_" in is/let is now automatically lifted over

278 bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x")

279 supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");

281 * Pure: method 'atomize' presents local goal premises as object-level

282 statements (atomic meta-level propositions); setup controlled via

283 rewrite rules declarations of 'atomize' attribute; example

284 application: 'induct' method with proper rule statements in improper

285 proof *scripts*;

287 * Pure: emulation of instantiation tactics (rule_tac, cut_tac, etc.)

288 now consider the syntactic context of assumptions, giving a better

289 chance to get type-inference of the arguments right (this is

290 especially important for locales);

292 * Pure: "sorry" no longer requires quick_and_dirty in interactive

293 mode;

295 * Pure/obtain: the formal conclusion "thesis", being marked as

296 ``internal'', may no longer be reference directly in the text;

297 potential INCOMPATIBILITY, may need to use "?thesis" in rare

298 situations;

300 * Pure: generic 'sym' attribute which declares a rule both as pure

301 'elim?' and for the 'symmetric' operation;

303 * Pure: marginal comments ``--'' may now occur just anywhere in the

304 text; the fixed correlation with particular command syntax has been

305 discontinued;

307 * Pure: new method 'rules' is particularly well-suited for proof

308 search in intuitionistic logic; a bit slower than 'blast' or 'fast',

309 but often produces more compact proof terms with less detours;

311 * Pure/Provers/classical: simplified integration with pure rule

312 attributes and methods; the classical "intro?/elim?/dest?"

313 declarations coincide with the pure ones; the "rule" method no longer

314 includes classically swapped intros; "intro" and "elim" methods no

315 longer pick rules from the context; also got rid of ML declarations

316 AddXIs/AddXEs/AddXDs; all of this has some potential for

317 INCOMPATIBILITY;

319 * Provers/classical: attribute 'swapped' produces classical inversions

320 of introduction rules;

322 * Provers/simplifier: 'simplified' attribute may refer to explicit

323 rules instead of full simplifier context; 'iff' attribute handles

324 conditional rules;

326 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;

328 * HOL: 'recdef' now fails on unfinished automated proofs, use

329 "(permissive)" option to recover old behavior;

331 * HOL: 'inductive' no longer features separate (collective) attributes

332 for 'intros' (was found too confusing);

334 * HOL: properly declared induction rules less_induct and

335 wf_induct_rule;

338 *** HOL ***

340 * HOL: moved over to sane numeral syntax; the new policy is as

341 follows:

343 - 0 and 1 are polymorphic constants, which are defined on any

344 numeric type (nat, int, real etc.);

346 - 2, 3, 4, ... and -1, -2, -3, ... are polymorphic numerals, based

347 binary representation internally;

349 - type nat has special constructor Suc, and generally prefers Suc 0

350 over 1::nat and Suc (Suc 0) over 2::nat;

352 This change may cause significant problems of INCOMPATIBILITY; here

353 are some hints on converting existing sources:

355 - due to the new "num" token, "-0" and "-1" etc. are now atomic

356 entities, so expressions involving "-" (unary or binary minus) need

357 to be spaced properly;

359 - existing occurrences of "1" may need to be constraint "1::nat" or

360 even replaced by Suc 0; similar for old "2";

362 - replace "#nnn" by "nnn", and "#-nnn" by "-nnn";

364 - remove all special provisions on numerals in proofs;

366 * HOL: simp rules nat_number expand numerals on nat to Suc/0

367 representation (depends on bin_arith_simps in the default context);

369 * HOL: symbolic syntax for x^2 (numeral 2);

371 * HOL: the class of all HOL types is now called "type" rather than

372 "term"; INCOMPATIBILITY, need to adapt references to this type class

373 in axclass/classes, instance/arities, and (usually rare) occurrences

374 in typings (of consts etc.); internally the class is called

375 "HOL.type", ML programs should refer to HOLogic.typeS;

377 * HOL/record package improvements:

378 - new derived operations "fields" to build a partial record section,

379 "extend" to promote a fixed record to a record scheme, and

380 "truncate" for the reverse; cf. theorems "xxx.defs", which are *not*

381 declared as simp by default;

382 - shared operations ("more", "fields", etc.) now need to be always

383 qualified) --- potential INCOMPATIBILITY;

384 - removed "make_scheme" operations (use "make" with "extend") --

385 INCOMPATIBILITY;

386 - removed "more" class (simply use "term") -- INCOMPATIBILITY;

387 - provides cases/induct rules for use with corresponding Isar

388 methods (for concrete records, record schemes, concrete more

389 parts, and schematic more parts -- in that order);

390 - internal definitions directly based on a light-weight abstract

391 theory of product types over typedef rather than datatype;

393 * HOL: generic code generator for generating executable ML code from

394 specifications; specific support for HOL constructs such as inductive

395 datatypes and sets, as well as recursive functions; can be invoked

396 via 'generate_code' theory section;

398 * HOL: canonical cases/induct rules for n-tuples (n = 3..7);

400 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"

401 (beware of argument permutation!);

403 * HOL: linorder_less_split superseded by linorder_cases;

405 * HOL/List: "nodups" renamed to "distinct";

407 * HOL: added "The" definite description operator; move Hilbert's "Eps"

408 to peripheral theory "Hilbert_Choice";

410 * HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so

411 in this (rare) case use:

413 delSWrapper "split_all_tac"

414 addSbefore ("unsafe_split_all_tac", unsafe_split_all_tac)

416 * HOL: added safe wrapper "split_conv_tac" to claset; EXISTING PROOFS

417 MAY FAIL;

419 * HOL: introduced f^n = f o ... o f; warning: due to the limits of

420 Isabelle's type classes, ^ on functions and relations has too general

421 a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be

422 necessary to attach explicit type constraints;

424 * HOL/Relation: the prefix name of the infix "O" has been changed from

425 "comp" to "rel_comp"; INCOMPATIBILITY: a few theorems have been

426 renamed accordingly (eg "compI" -> "rel_compI").

428 * HOL: syntax translations now work properly with numerals and records

429 expressions;

431 * HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead

432 of "lam" -- INCOMPATIBILITY;

434 * HOL: got rid of some global declarations (potential INCOMPATIBILITY

435 for ML tools): const "()" renamed "Product_Type.Unity", type "unit"

436 renamed "Product_Type.unit";

438 * HOL: renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl

440 * HOL: removed obsolete theorem "optionE" (use "option.exhaust", or

441 the "cases" method);

443 * HOL/GroupTheory: group theory examples including Sylow's theorem (by

444 Florian Kammüller);

446 * HOL/IMP: updated and converted to new-style theory format; several

447 parts turned into readable document, with proper Isar proof texts and

448 some explanations (by Gerwin Klein);

450 * HOL-Real: added Complex_Numbers (by Gertrud Bauer);

452 * HOL-Hyperreal is now a logic image;

455 *** HOLCF ***

457 * Isar: consts/constdefs supports mixfix syntax for continuous

458 operations;

460 * Isar: domain package adapted to new-style theory format, e.g. see

461 HOLCF/ex/Dnat.thy;

463 * theory Lift: proper use of rep_datatype lift instead of ML hacks --

464 potential INCOMPATIBILITY; now use plain induct_tac instead of former

465 lift.induct_tac, always use UU instead of Undef;

467 * HOLCF/IMP: updated and converted to new-style theory;

470 *** ZF ***

472 * Isar: proper integration of logic-specific tools and packages,

473 including theory commands '(co)inductive', '(co)datatype',

474 'rep_datatype', 'inductive_cases', as well as methods 'ind_cases',

475 'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');

477 * theory Main no longer includes AC; for the Axiom of Choice, base

478 your theory on Main_ZFC;

480 * the integer library now covers quotients and remainders, with many

481 laws relating division to addition, multiplication, etc.;

483 * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a

484 typeless version of the formalism;

486 * ZF/AC, Coind, IMP, Resid: updated and converted to new-style theory

487 format;

489 * ZF/Induct: new directory for examples of inductive definitions,

490 including theory Multiset for multiset orderings; converted to

491 new-style theory format;

493 * ZF: many new theorems about lists, ordinals, etc.;

496 *** General ***

498 * Pure/kernel: meta-level proof terms (by Stefan Berghofer); reference

499 variable proof controls level of detail: 0 = no proofs (only oracle

500 dependencies), 1 = lemma dependencies, 2 = compact proof terms; see

501 also ref manual for further ML interfaces;

503 * Pure/axclass: removed obsolete ML interface

504 goal_subclass/goal_arity;

506 * Pure/syntax: new token syntax "num" for plain numerals (without "#"

507 of "xnum"); potential INCOMPATIBILITY, since -0, -1 etc. are now

508 separate tokens, so expressions involving minus need to be spaced

509 properly;

511 * Pure/syntax: support non-oriented infixes, using keyword "infix"

512 rather than "infixl" or "infixr";

514 * Pure/syntax: concrete syntax for dummy type variables admits genuine

515 sort constraint specifications in type inference; e.g. "x::_::foo"

516 ensures that the type of "x" is of sort "foo" (but not necessarily a

517 type variable);

519 * Pure/syntax: print modes "type_brackets" and "no_type_brackets"

520 control output of nested => (types); the default behavior is

521 "type_brackets";

523 * Pure/syntax: builtin parse translation for "_constify" turns valued

524 tokens into AST constants;

526 * Pure/syntax: prefer later declarations of translations and print

527 translation functions; potential INCOMPATIBILITY: need to reverse

528 multiple declarations for same syntax element constant;

530 * Pure/show_hyps reset by default (in accordance to existing Isar

531 practice);

533 * Provers/classical: renamed addaltern to addafter, addSaltern to

534 addSafter;

536 * Provers/clasimp: ``iff'' declarations now handle conditional rules

537 as well;

539 * system: tested support for MacOS X; should be able to get Isabelle +

540 Proof General to work in a plain Terminal after installing Poly/ML

541 (e.g. from the Isabelle distribution area) and GNU bash alone

542 (e.g. from http://www.apple.com); full X11, XEmacs and X-Symbol

543 support requires further installations, e.g. from

544 http://fink.sourceforge.net/);

546 * system: support Poly/ML 4.1.1 (able to manage larger heaps);

548 * system: reduced base memory usage by Poly/ML (approx. 20 MB instead

549 of 40 MB), cf. ML_OPTIONS;

551 * system: Proof General keywords specification is now part of the

552 Isabelle distribution (see etc/isar-keywords.el);

554 * system: support for persistent Proof General sessions (refrain from

555 outdating all loaded theories on startup); user may create writable

556 logic images like this: ``isabelle -q HOL Test'';

558 * system: smart selection of Isabelle process versus Isabelle

559 interface, accommodates case-insensitive file systems (e.g. HFS+); may

560 run both "isabelle" and "Isabelle" even if file names are badly

561 damaged (executable inspects the case of the first letter of its own

562 name); added separate "isabelle-process" and "isabelle-interface";

564 * system: refrain from any attempt at filtering input streams; no

565 longer support ``8bit'' encoding of old isabelle font, instead proper

566 iso-latin characters may now be used; the related isatools

567 "symbolinput" and "nonascii" have disappeared as well;

569 * system: removed old "xterm" interface (the print modes "xterm" and

570 "xterm_color" are still available for direct use in a suitable

571 terminal);

575 New in Isabelle99-2 (February 2001)

576 -----------------------------------

578 *** Overview of INCOMPATIBILITIES ***

580 * HOL: please note that theories in the Library and elsewhere often use the

581 new-style (Isar) format; to refer to their theorems in an ML script you must

582 bind them to ML identifers by e.g. val thm_name = thm "thm_name";

584 * HOL: inductive package no longer splits induction rule aggressively,

585 but only as far as specified by the introductions given; the old

586 format may be recovered via ML function complete_split_rule or attribute

587 'split_rule (complete)';

589 * HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold,

590 gfp_Tarski to gfp_unfold;

592 * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;

594 * HOL: infix "dvd" now has priority 50 rather than 70 (because it is a

595 relation); infix "^^" has been renamed "``"; infix "``" has been

596 renamed "`"; "univalent" has been renamed "single_valued";

598 * HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse"

599 operation;

601 * HOLCF: infix "`" has been renamed "$"; the symbol syntax is \<cdot>;

603 * Isar: 'obtain' no longer declares "that" fact as simp/intro;

605 * Isar/HOL: method 'induct' now handles non-atomic goals; as a

606 consequence, it is no longer monotonic wrt. the local goal context

607 (which is now passed through the inductive cases);

609 * Document preparation: renamed standard symbols \<ll> to \<lless> and

610 \<gg> to \<ggreater>;

613 *** Document preparation ***

615 * \isabellestyle{NAME} selects version of Isabelle output (currently

616 available: are "it" for near math-mode best-style output, "sl" for

617 slanted text style, and "tt" for plain type-writer; if no

618 \isabellestyle command is given, output is according to slanted

619 type-writer);

621 * support sub/super scripts (for single symbols only), input syntax is

622 like this: "A\<^sup>*" or "A\<^sup>\<star>";

624 * some more standard symbols; see Appendix A of the system manual for

625 the complete list of symbols defined in isabellesym.sty;

627 * improved isabelle style files; more abstract symbol implementation

628 (should now use \isamath{...} and \isatext{...} in custom symbol

629 definitions);

631 * antiquotation @{goals} and @{subgoals} for output of *dynamic* goals

632 state; Note that presentation of goal states does not conform to

633 actual human-readable proof documents. Please do not include goal

634 states into document output unless you really know what you are doing!

636 * proper indentation of antiquoted output with proportional LaTeX

637 fonts;

639 * no_document ML operator temporarily disables LaTeX document

640 generation;

642 * isatool unsymbolize tunes sources for plain ASCII communication;

645 *** Isar ***

647 * Pure: Isar now suffers initial goal statements to contain unbound

648 schematic variables (this does not conform to actual readable proof

649 documents, due to unpredictable outcome and non-compositional proof

650 checking); users who know what they are doing may use schematic goals

651 for Prolog-style synthesis of proven results;

653 * Pure: assumption method (an implicit finishing) now handles actual

654 rules as well;

656 * Pure: improved 'obtain' --- moved to Pure, insert "that" into

657 initial goal, declare "that" only as Pure intro (only for single

658 steps); the "that" rule assumption may now be involved in implicit

659 finishing, thus ".." becomes a feasible for trivial obtains;

661 * Pure: default proof step now includes 'intro_classes'; thus trivial

662 instance proofs may be performed by "..";

664 * Pure: ?thesis / ?this / "..." now work for pure meta-level

665 statements as well;

667 * Pure: more robust selection of calculational rules;

669 * Pure: the builtin notion of 'finished' goal now includes the ==-refl

670 rule (as well as the assumption rule);

672 * Pure: 'thm_deps' command visualizes dependencies of theorems and

673 lemmas, using the graph browser tool;

675 * Pure: predict failure of "show" in interactive mode;

677 * Pure: 'thms_containing' now takes actual terms as arguments;

679 * HOL: improved method 'induct' --- now handles non-atomic goals

680 (potential INCOMPATIBILITY); tuned error handling;

682 * HOL: cases and induct rules now provide explicit hints about the

683 number of facts to be consumed (0 for "type" and 1 for "set" rules);

684 any remaining facts are inserted into the goal verbatim;

686 * HOL: local contexts (aka cases) may now contain term bindings as

687 well; the 'cases' and 'induct' methods new provide a ?case binding for

688 the result to be shown in each case;

690 * HOL: added 'recdef_tc' command;

692 * isatool convert assists in eliminating legacy ML scripts;

695 *** HOL ***

697 * HOL/Library: a collection of generic theories to be used together

698 with main HOL; the theory loader path already includes this directory

699 by default; the following existing theories have been moved here:

700 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While

701 (as While_Combinator), HOL/Lex/Prefix (as List_Prefix);

703 * HOL/Unix: "Some aspects of Unix file-system security", a typical

704 modelling and verification task performed in Isabelle/HOL +

705 Isabelle/Isar + Isabelle document preparation (by Markus Wenzel).

707 * HOL/Algebra: special summation operator SUM no longer exists, it has

708 been replaced by setsum; infix 'assoc' now has priority 50 (like

709 'dvd'); axiom 'one_not_zero' has been moved from axclass 'ring' to

710 'domain', this makes the theory consistent with mathematical

711 literature;

713 * HOL basics: added overloaded operations "inverse" and "divide"

714 (infix "/"), syntax for generic "abs" operation, generic summation

715 operator \<Sum>;

717 * HOL/typedef: simplified package, provide more useful rules (see also

718 HOL/subset.thy);

720 * HOL/datatype: induction rule for arbitrarily branching datatypes is

721 now expressed as a proper nested rule (old-style tactic scripts may

722 require atomize_strip_tac to cope with non-atomic premises);

724 * HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule

725 to "split_conv" (old name still available for compatibility);

727 * HOL: improved concrete syntax for strings (e.g. allows translation

728 rules with string literals);

730 * HOL-Real-Hyperreal: this extends HOL-Real with the hyperreals

731 and Fleuriot's mechanization of analysis, including the transcendental

732 functions for the reals;

734 * HOL/Real, HOL/Hyperreal: improved arithmetic simplification;

737 *** CTT ***

739 * CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that

740 "lam" is displayed as TWO lambda-symbols

742 * CTT: theory Main now available, containing everything (that is, Bool

743 and Arith);

746 *** General ***

748 * Pure: the Simplifier has been implemented properly as a derived rule

749 outside of the actual kernel (at last!); the overall performance

750 penalty in practical applications is about 50%, while reliability of

751 the Isabelle inference kernel has been greatly improved;

753 * print modes "brackets" and "no_brackets" control output of nested =>

754 (types) and ==> (props); the default behaviour is "brackets";

756 * Provers: fast_tac (and friends) now handle actual object-logic rules

757 as assumptions as well;

759 * system: support Poly/ML 4.0;

761 * system: isatool install handles KDE version 1 or 2;

765 New in Isabelle99-1 (October 2000)

766 ----------------------------------

768 *** Overview of INCOMPATIBILITIES ***

770 * HOL: simplification of natural numbers is much changed; to partly

771 recover the old behaviour (e.g. to prevent n+n rewriting to #2*n)

772 issue the following ML commands:

774 Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;

775 Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];

777 * HOL: simplification no longer dives into case-expressions; this is

778 controlled by "t.weak_case_cong" for each datatype t;

780 * HOL: nat_less_induct renamed to less_induct;

782 * HOL: systematic renaming of the SOME (Eps) rules, may use isatool

783 fixsome to patch .thy and .ML sources automatically;

785 select_equality -> some_equality

786 select_eq_Ex -> some_eq_ex

787 selectI2EX -> someI2_ex

788 selectI2 -> someI2

789 selectI -> someI

790 select1_equality -> some1_equality

791 Eps_sym_eq -> some_sym_eq_trivial

792 Eps_eq -> some_eq_trivial

794 * HOL: exhaust_tac on datatypes superceded by new generic case_tac;

796 * HOL: removed obsolete theorem binding expand_if (refer to split_if

797 instead);

799 * HOL: the recursion equations generated by 'recdef' are now called

800 f.simps instead of f.rules;

802 * HOL: qed_spec_mp now also handles bounded ALL as well;

804 * HOL: 0 is now overloaded, so the type constraint ":: nat" may

805 sometimes be needed;

807 * HOL: the constant for "f``x" is now "image" rather than "op ``";

809 * HOL: the constant for "f-``x" is now "vimage" rather than "op -``";

811 * HOL: the disjoint sum is now "<+>" instead of "Plus"; the cartesian

812 product is now "<*>" instead of "Times"; the lexicographic product is

813 now "<*lex*>" instead of "**";

815 * HOL: theory Sexp is now in HOL/Induct examples (it used to be part

816 of main HOL, but was unused); better use HOL's datatype package;

818 * HOL: removed "symbols" syntax for constant "override" of theory Map;

819 the old syntax may be recovered as follows:

821 syntax (symbols)

822 override :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"

823 (infixl "\\<oplus>" 100)

825 * HOL/Real: "rabs" replaced by overloaded "abs" function;

827 * HOL/ML: even fewer consts are declared as global (see theories Ord,

828 Lfp, Gfp, WF); this only affects ML packages that refer to const names

829 internally;

831 * HOL and ZF: syntax for quotienting wrt an equivalence relation

832 changed from A/r to A//r;

834 * ZF: new treatment of arithmetic (nat & int) may break some old

835 proofs;

837 * Isar: renamed some attributes (RS -> THEN, simplify -> simplified,

838 rulify -> rule_format, elimify -> elim_format, ...);

840 * Isar/Provers: intro/elim/dest attributes changed; renamed

841 intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one

842 should have to change intro!! to intro? only); replaced "delrule" by

843 "rule del";

845 * Isar/HOL: renamed "intrs" to "intros" in inductive definitions;

847 * Provers: strengthened force_tac by using new first_best_tac;

849 * LaTeX document preparation: several changes of isabelle.sty (see

850 lib/texinputs);

853 *** Document preparation ***

855 * formal comments (text blocks etc.) in new-style theories may now

856 contain antiquotations of thm/prop/term/typ/text to be presented

857 according to latex print mode; concrete syntax is like this:

858 @{term[show_types] "f(x) = a + x"};

860 * isatool mkdir provides easy setup of Isabelle session directories,

861 including proper document sources;

863 * generated LaTeX sources are now deleted after successful run

864 (isatool document -c); may retain a copy somewhere else via -D option

865 of isatool usedir;

867 * isatool usedir -D now lets isatool latex -o sty update the Isabelle

868 style files, achieving self-contained LaTeX sources and simplifying

869 LaTeX debugging;

871 * old-style theories now produce (crude) LaTeX output as well;

873 * browser info session directories are now self-contained (may be put

874 on WWW server seperately); improved graphs of nested sessions; removed

875 graph for 'all sessions';

877 * several improvements in isabelle style files; \isabellestyle{it}

878 produces fake math mode output; \isamarkupheader is now \section by

879 default; see lib/texinputs/isabelle.sty etc.;

882 *** Isar ***

884 * Isar/Pure: local results and corresponding term bindings are now

885 subject to Hindley-Milner polymorphism (similar to ML); this

886 accommodates incremental type-inference very nicely;

888 * Isar/Pure: new derived language element 'obtain' supports

889 generalized existence reasoning;

891 * Isar/Pure: new calculational elements 'moreover' and 'ultimately'

892 support accumulation of results, without applying any rules yet;

893 useful to collect intermediate results without explicit name

894 references, and for use with transitivity rules with more than 2

895 premises;

897 * Isar/Pure: scalable support for case-analysis type proofs: new

898 'case' language element refers to local contexts symbolically, as

899 produced by certain proof methods; internally, case names are attached

900 to theorems as "tags";

902 * Isar/Pure: theory command 'hide' removes declarations from

903 class/type/const name spaces;

905 * Isar/Pure: theory command 'defs' supports option "(overloaded)" to

906 indicate potential overloading;

908 * Isar/Pure: changed syntax of local blocks from {{ }} to { };

910 * Isar/Pure: syntax of sorts made 'inner', i.e. have to write

911 "{a,b,c}" instead of {a,b,c};

913 * Isar/Pure now provides its own version of intro/elim/dest

914 attributes; useful for building new logics, but beware of confusion

915 with the version in Provers/classical;

917 * Isar/Pure: the local context of (non-atomic) goals is provided via

918 case name 'antecedent';

920 * Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms

921 to the current context is now done automatically);

923 * Isar/Pure: theory command 'method_setup' provides a simple interface

924 for definining proof methods in ML;

926 * Isar/Provers: intro/elim/dest attributes changed; renamed

927 intro/intro!/intro!! flags to intro!/intro/intro? (INCOMPATIBILITY, in

928 most cases, one should have to change intro!! to intro? only);

929 replaced "delrule" by "rule del";

931 * Isar/Provers: new 'hypsubst' method, plain 'subst' method and

932 'symmetric' attribute (the latter supercedes [RS sym]);

934 * Isar/Provers: splitter support (via 'split' attribute and 'simp'

935 method modifier); 'simp' method: 'only:' modifier removes loopers as

936 well (including splits);

938 * Isar/Provers: Simplifier and Classical methods now support all kind

939 of modifiers used in the past, including 'cong', 'iff', etc.

941 * Isar/Provers: added 'fastsimp' and 'clarsimp' methods (combination

942 of Simplifier and Classical reasoner);

944 * Isar/HOL: new proof method 'cases' and improved version of 'induct'

945 now support named cases; major packages (inductive, datatype, primrec,

946 recdef) support case names and properly name parameters;

948 * Isar/HOL: new transitivity rules for substitution in inequalities --

949 monotonicity conditions are extracted to be proven at end of

950 calculations;

952 * Isar/HOL: removed 'case_split' thm binding, should use 'cases' proof

953 method anyway;

955 * Isar/HOL: removed old expand_if = split_if; theorems if_splits =

956 split_if split_if_asm; datatype package provides theorems foo.splits =

957 foo.split foo.split_asm for each datatype;

959 * Isar/HOL: tuned inductive package, rename "intrs" to "intros"

960 (potential INCOMPATIBILITY), emulation of mk_cases feature for proof

961 scripts: new 'inductive_cases' command and 'ind_cases' method; (Note:

962 use "(cases (simplified))" method in proper proof texts);

964 * Isar/HOL: added global 'arith_split' attribute for 'arith' method;

966 * Isar: names of theorems etc. may be natural numbers as well;

968 * Isar: 'pr' command: optional arguments for goals_limit and

969 ProofContext.prems_limit; no longer prints theory contexts, but only

970 proof states;

972 * Isar: diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit

973 additional print modes to be specified; e.g. "pr(latex)" will print

974 proof state according to the Isabelle LaTeX style;

976 * Isar: improved support for emulating tactic scripts, including proof

977 methods 'rule_tac' etc., 'cut_tac', 'thin_tac', 'subgoal_tac',

978 'rename_tac', 'rotate_tac', 'tactic', and 'case_tac' / 'induct_tac'

979 (for HOL datatypes);

981 * Isar: simplified (more robust) goal selection of proof methods: 1st

982 goal, all goals, or explicit goal specifier (tactic emulation); thus

983 'proof method scripts' have to be in depth-first order;

985 * Isar: tuned 'let' syntax: replaced 'as' keyword by 'and';

987 * Isar: removed 'help' command, which hasn't been too helpful anyway;

988 should instead use individual commands for printing items

989 (print_commands, print_methods etc.);

991 * Isar: added 'nothing' --- the empty list of theorems;

994 *** HOL ***

996 * HOL/MicroJava: formalization of a fragment of Java, together with a

997 corresponding virtual machine and a specification of its bytecode

998 verifier and a lightweight bytecode verifier, including proofs of

999 type-safety; by Gerwin Klein, Tobias Nipkow, David von Oheimb, and

1000 Cornelia Pusch (see also the homepage of project Bali at

1001 http://isabelle.in.tum.de/Bali/);

1003 * HOL/Algebra: new theory of rings and univariate polynomials, by

1004 Clemens Ballarin;

1006 * HOL/NumberTheory: fundamental Theorem of Arithmetic, Chinese

1007 Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, by Thomas M

1008 Rasmussen;

1010 * HOL/Lattice: fundamental concepts of lattice theory and order

1011 structures, including duals, properties of bounds versus algebraic

1012 laws, lattice operations versus set-theoretic ones, the Knaster-Tarski

1013 Theorem for complete lattices etc.; may also serve as a demonstration

1014 for abstract algebraic reasoning using axiomatic type classes, and

1015 mathematics-style proof in Isabelle/Isar; by Markus Wenzel;

1017 * HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog, by David

1018 von Oheimb;

1020 * HOL/IMPP: extension of IMP with local variables and mutually

1021 recursive procedures, by David von Oheimb;

1023 * HOL/Lambda: converted into new-style theory and document;

1025 * HOL/ex/Multiquote: example of multiple nested quotations and

1026 anti-quotations -- basically a generalized version of de-Bruijn

1027 representation; very useful in avoiding lifting of operations;

1029 * HOL/record: added general record equality rule to simpset; fixed

1030 select-update simplification procedure to handle extended records as

1031 well; admit "r" as field name;

1033 * HOL: 0 is now overloaded over the new sort "zero", allowing its use with

1034 other numeric types and also as the identity of groups, rings, etc.;

1036 * HOL: new axclass plus_ac0 for addition with the AC-laws and 0 as identity.

1037 Types nat and int belong to this axclass;

1039 * HOL: greatly improved simplification involving numerals of type nat, int, real:

1040 (i + #8 + j) = Suc k simplifies to #7 + (i + j) = k

1041 i*j + k + j*#3*i simplifies to #4*(i*j) + k

1042 two terms #m*u and #n*u are replaced by #(m+n)*u

1043 (where #m, #n and u can implicitly be 1; this is simproc combine_numerals)

1044 and the term/formula #m*u+x ~~ #n*u+y simplifies simplifies to #(m-n)+x ~~ y

1045 or x ~~ #(n-m)+y, where ~~ is one of = < <= or - (simproc cancel_numerals);

1047 * HOL: meson_tac is available (previously in ex/meson.ML); it is a

1048 powerful prover for predicate logic but knows nothing of clasets; see

1049 ex/mesontest.ML and ex/mesontest2.ML for example applications;

1051 * HOL: new version of "case_tac" subsumes both boolean case split and

1052 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer

1053 exists, may define val exhaust_tac = case_tac for ad-hoc portability;

1055 * HOL: simplification no longer dives into case-expressions: only the

1056 selector expression is simplified, but not the remaining arms; to

1057 enable full simplification of case-expressions for datatype t, you may

1058 remove t.weak_case_cong from the simpset, either globally (Delcongs

1059 [thm"t.weak_case_cong"];) or locally (delcongs [...]).

1061 * HOL/recdef: the recursion equations generated by 'recdef' for

1062 function 'f' are now called f.simps instead of f.rules; if all

1063 termination conditions are proved automatically, these simplification

1064 rules are added to the simpset, as in primrec; rules may be named

1065 individually as well, resulting in a separate list of theorems for

1066 each equation;

1068 * HOL/While is a new theory that provides a while-combinator. It

1069 permits the definition of tail-recursive functions without the

1070 provision of a termination measure. The latter is necessary once the

1071 invariant proof rule for while is applied.

1073 * HOL: new (overloaded) notation for the set of elements below/above

1074 some element: {..u}, {..u(}, {l..}, {)l..}. See theory SetInterval.

1076 * HOL: theorems impI, allI, ballI bound as "strip";

1078 * HOL: new tactic induct_thm_tac: thm -> string -> int -> tactic

1079 induct_tac th "x1 ... xn" expects th to have a conclusion of the form

1080 P v1 ... vn and abbreviates res_inst_tac [("v1","x1"),...,("vn","xn")] th;

1082 * HOL/Real: "rabs" replaced by overloaded "abs" function;

1084 * HOL: theory Sexp now in HOL/Induct examples (it used to be part of

1085 main HOL, but was unused);

1087 * HOL: fewer consts declared as global (e.g. have to refer to

1088 "Lfp.lfp" instead of "lfp" internally; affects ML packages only);

1090 * HOL: tuned AST representation of nested pairs, avoiding bogus output

1091 in case of overlap with user translations (e.g. judgements over

1092 tuples); (note that the underlying logical represenation is still

1093 bogus);

1096 *** ZF ***

1098 * ZF: simplification automatically cancels common terms in arithmetic

1099 expressions over nat and int;

1101 * ZF: new treatment of nat to minimize type-checking: all operators

1102 coerce their operands to a natural number using the function natify,

1103 making the algebraic laws unconditional;

1105 * ZF: as above, for int: operators coerce their operands to an integer

1106 using the function intify;

1108 * ZF: the integer library now contains many of the usual laws for the

1109 orderings, including $<=, and monotonicity laws for $+ and $*;

1111 * ZF: new example ZF/ex/NatSum to demonstrate integer arithmetic

1112 simplification;

1114 * FOL and ZF: AddIffs now available, giving theorems of the form P<->Q

1115 to the simplifier and classical reasoner simultaneously;

1118 *** General ***

1120 * Provers: blast_tac now handles actual object-logic rules as

1121 assumptions; note that auto_tac uses blast_tac internally as well;

1123 * Provers: new functions rulify/rulify_no_asm: thm -> thm for turning

1124 outer -->/All/Ball into ==>/!!; qed_spec_mp now uses rulify_no_asm;

1126 * Provers: delrules now handles destruct rules as well (no longer need

1127 explicit make_elim);

1129 * Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g.

1130 [| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W

1131 use instead the strong form,

1132 [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W

1133 in HOL, FOL and ZF the function cla_make_elim will create such rules

1134 from destruct-rules;

1136 * Provers: Simplifier.easy_setup provides a fast path to basic

1137 Simplifier setup for new object-logics;

1139 * Pure: AST translation rules no longer require constant head on LHS;

1141 * Pure: improved name spaces: ambiguous output is qualified; support

1142 for hiding of names;

1144 * system: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, and

1145 XSYMBOL_HOME; no longer need to do manual configuration in most

1146 situations;

1148 * system: compression of ML heaps images may now be controlled via -c

1149 option of isabelle and isatool usedir (currently only observed by

1150 Poly/ML);

1152 * system: isatool installfonts may handle X-Symbol fonts as well (very

1153 useful for remote X11);

1155 * system: provide TAGS file for Isabelle sources;

1157 * ML: infix 'OF' is a version of 'MRS' with more appropriate argument

1158 order;

1160 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global

1161 timing flag supersedes proof_timing and Toplevel.trace;

1163 * ML: new combinators |>> and |>>> for incremental transformations

1164 with secondary results (e.g. certain theory extensions):

1166 * ML: PureThy.add_defs gets additional argument to indicate potential

1167 overloading (usually false);

1169 * ML: PureThy.add_thms/add_axioms/add_defs now return theorems as

1170 results;

1174 New in Isabelle99 (October 1999)

1175 --------------------------------

1177 *** Overview of INCOMPATIBILITIES (see below for more details) ***

1179 * HOL: The THEN and ELSE parts of conditional expressions (if P then x else y)

1180 are no longer simplified. (This allows the simplifier to unfold recursive

1181 functional programs.) To restore the old behaviour, declare

1183 Delcongs [if_weak_cong];

1185 * HOL: Removed the obsolete syntax "Compl A"; use -A for set

1186 complement;

1188 * HOL: the predicate "inj" is now defined by translation to "inj_on";

1190 * HOL/datatype: mutual_induct_tac no longer exists --

1191 use induct_tac "x_1 ... x_n" instead of mutual_induct_tac ["x_1", ..., "x_n"]

1193 * HOL/typedef: fixed type inference for representing set; type

1194 arguments now have to occur explicitly on the rhs as type constraints;

1196 * ZF: The con_defs part of an inductive definition may no longer refer

1197 to constants declared in the same theory;

1199 * HOL, ZF: the function mk_cases, generated by the inductive

1200 definition package, has lost an argument. To simplify its result, it

1201 uses the default simpset instead of a supplied list of theorems.

1203 * HOL/List: the constructors of type list are now Nil and Cons;

1205 * Simplifier: the type of the infix ML functions

1206 setSSolver addSSolver setSolver addSolver

1207 is now simpset * solver -> simpset where `solver' is a new abstract type

1208 for packaging solvers. A solver is created via

1209 mk_solver: string -> (thm list -> int -> tactic) -> solver

1210 where the string argument is only a comment.

1213 *** Proof tools ***

1215 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a

1216 decision procedure for linear arithmetic. Currently it is used for

1217 types `nat', `int', and `real' in HOL (see below); it can, should and

1218 will be instantiated for other types and logics as well.

1220 * The simplifier now accepts rewrite rules with flexible heads, eg

1221 hom ?f ==> ?f(?x+?y) = ?f ?x + ?f ?y

1222 They are applied like any rule with a non-pattern lhs, i.e. by first-order

1223 matching.

1226 *** General ***

1228 * New Isabelle/Isar subsystem provides an alternative to traditional

1229 tactical theorem proving; together with the ProofGeneral/isar user

1230 interface it offers an interactive environment for developing human

1231 readable proof documents (Isar == Intelligible semi-automated

1232 reasoning); for further information see isatool doc isar-ref,

1233 src/HOL/Isar_examples and http://isabelle.in.tum.de/Isar/

1235 * improved and simplified presentation of theories: better HTML markup

1236 (including colors), graph views in several sizes; isatool usedir now

1237 provides a proper interface for user theories (via -P option); actual

1238 document preparation based on (PDF)LaTeX is available as well (for

1239 new-style theories only); see isatool doc system for more information;

1241 * native support for Proof General, both for classic Isabelle and

1242 Isabelle/Isar;

1244 * ML function thm_deps visualizes dependencies of theorems and lemmas,

1245 using the graph browser tool;

1247 * Isabelle manuals now also available as PDF;

1249 * theory loader rewritten from scratch (may not be fully

1250 bug-compatible); old loadpath variable has been replaced by show_path,

1251 add_path, del_path, reset_path functions; new operations such as

1252 update_thy, touch_thy, remove_thy, use/update_thy_only (see also

1253 isatool doc ref);

1255 * improved isatool install: option -k creates KDE application icon,

1256 option -p DIR installs standalone binaries;

1258 * added ML_PLATFORM setting (useful for cross-platform installations);

1259 more robust handling of platform specific ML images for SML/NJ;

1261 * the settings environment is now statically scoped, i.e. it is never

1262 created again in sub-processes invoked from isabelle, isatool, or

1263 Isabelle;

1265 * path element specification '~~' refers to '$ISABELLE_HOME';

1267 * in locales, the "assumes" and "defines" parts may be omitted if

1268 empty;

1270 * new print_mode "xsymbols" for extended symbol support (e.g. genuine

1271 long arrows);

1273 * new print_mode "HTML";

1275 * new flag show_tags controls display of tags of theorems (which are

1276 basically just comments that may be attached by some tools);

1278 * Isamode 2.6 requires patch to accomodate change of Isabelle font

1279 mode and goal output format:

1281 diff -r Isamode-2.6/elisp/isa-load.el Isamode/elisp/isa-load.el

1282 244c244

1283 < (list (isa-getenv "ISABELLE") "-msymbols" logic-name)

1284 ---

1285 > (list (isa-getenv "ISABELLE") "-misabelle_font" "-msymbols" logic-name)

1286 diff -r Isabelle-2.6/elisp/isa-proofstate.el Isamode/elisp/isa-proofstate.el

1287 181c181

1288 < (defconst proofstate-proofstart-regexp "^Level [0-9]+$"

1289 ---

1290 > (defconst proofstate-proofstart-regexp "^Level [0-9]+"

1292 * function bind_thms stores lists of theorems (cf. bind_thm);

1294 * new shorthand tactics ftac, eatac, datac, fatac;

1296 * qed (and friends) now accept "" as result name; in that case the

1297 theorem is not stored, but proper checks and presentation of the

1298 result still apply;

1300 * theorem database now also indexes constants "Trueprop", "all",

1301 "==>", "=="; thus thms_containing, findI etc. may retrieve more rules;

1304 *** HOL ***

1306 ** HOL arithmetic **

1308 * There are now decision procedures for linear arithmetic over nat and

1309 int:

1311 1. arith_tac copes with arbitrary formulae involving `=', `<', `<=',

1312 `+', `-', `Suc', `min', `max' and numerical constants; other subterms

1313 are treated as atomic; subformulae not involving type `nat' or `int'

1314 are ignored; quantified subformulae are ignored unless they are

1315 positive universal or negative existential. The tactic has to be

1316 invoked by hand and can be a little bit slow. In particular, the

1317 running time is exponential in the number of occurrences of `min' and

1318 `max', and `-' on `nat'.

1320 2. fast_arith_tac is a cut-down version of arith_tac: it only takes

1321 (negated) (in)equalities among the premises and the conclusion into

1322 account (i.e. no compound formulae) and does not know about `min' and

1323 `max', and `-' on `nat'. It is fast and is used automatically by the

1324 simplifier.

1326 NB: At the moment, these decision procedures do not cope with mixed

1327 nat/int formulae where the two parts interact, such as `m < n ==>

1328 int(m) < int(n)'.

1330 * HOL/Numeral provides a generic theory of numerals (encoded

1331 efficiently as bit strings); setup for types nat/int/real is in place;

1332 INCOMPATIBILITY: since numeral syntax is now polymorphic, rather than

1333 int, existing theories and proof scripts may require a few additional

1334 type constraints;

1336 * integer division and remainder can now be performed on constant

1337 arguments;

1339 * many properties of integer multiplication, division and remainder

1340 are now available;

1342 * An interface to the Stanford Validity Checker (SVC) is available through the

1343 tactic svc_tac. Propositional tautologies and theorems of linear arithmetic

1344 are proved automatically. SVC must be installed separately, and its results

1345 must be TAKEN ON TRUST (Isabelle does not check the proofs, but tags any

1346 invocation of the underlying oracle). For SVC see

1347 http://verify.stanford.edu/SVC

1349 * IsaMakefile: the HOL-Real target now builds an actual image;

1352 ** HOL misc **

1354 * HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces

1355 (in Isabelle/Isar) -- by Gertrud Bauer;

1357 * HOL/BCV: generic model of bytecode verification, i.e. data-flow

1358 analysis for assembly languages with subtypes;

1360 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization

1361 -- avoids syntactic ambiguities and treats state, transition, and

1362 temporal levels more uniformly; introduces INCOMPATIBILITIES due to

1363 changed syntax and (many) tactics;

1365 * HOL/inductive: Now also handles more general introduction rules such

1366 as "ALL y. (y, x) : r --> y : acc r ==> x : acc r"; monotonicity

1367 theorems are now maintained within the theory (maintained via the

1368 "mono" attribute);

1370 * HOL/datatype: Now also handles arbitrarily branching datatypes

1371 (using function types) such as

1373 datatype 'a tree = Atom 'a | Branch "nat => 'a tree"

1375 * HOL/record: record_simproc (part of the default simpset) takes care

1376 of selectors applied to updated records; record_split_tac is no longer

1377 part of the default claset; update_defs may now be removed from the

1378 simpset in many cases; COMPATIBILITY: old behavior achieved by

1380 claset_ref () := claset() addSWrapper record_split_wrapper;

1381 Delsimprocs [record_simproc]

1383 * HOL/typedef: fixed type inference for representing set; type

1384 arguments now have to occur explicitly on the rhs as type constraints;

1386 * HOL/recdef (TFL): 'congs' syntax now expects comma separated list of theorem

1387 names rather than an ML expression;

1389 * HOL/defer_recdef (TFL): like recdef but the well-founded relation can be

1390 supplied later. Program schemes can be defined, such as

1391 "While B C s = (if B s then While B C (C s) else s)"

1392 where the well-founded relation can be chosen after B and C have been given.

1394 * HOL/List: the constructors of type list are now Nil and Cons;

1395 INCOMPATIBILITY: while [] and infix # syntax is still there, of

1396 course, ML tools referring to List.list.op # etc. have to be adapted;

1398 * HOL_quantifiers flag superseded by "HOL" print mode, which is

1399 disabled by default; run isabelle with option -m HOL to get back to

1400 the original Gordon/HOL-style output;

1402 * HOL/Ord.thy: new bounded quantifier syntax (input only): ALL x<y. P,

1403 ALL x<=y. P, EX x<y. P, EX x<=y. P;

1405 * HOL basic syntax simplified (more orthogonal): all variants of

1406 All/Ex now support plain / symbolic / HOL notation; plain syntax for

1407 Eps operator is provided as well: "SOME x. P[x]";

1409 * HOL/Sum.thy: sum_case has been moved to HOL/Datatype;

1411 * HOL/Univ.thy: infix syntax <*>, <+>, <**>, <+> eliminated and made

1412 thus available for user theories;

1414 * HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with

1415 HOL/List; hardly an INCOMPATIBILITY since '>>' syntax is used all the

1416 time;

1418 * HOL: new tactic smp_tac: int -> int -> tactic, which applies spec

1419 several times and then mp;

1422 *** LK ***

1424 * the notation <<...>> is now available as a notation for sequences of

1425 formulas;

1427 * the simplifier is now installed

1429 * the axiom system has been generalized (thanks to Soren Heilmann)

1431 * the classical reasoner now has a default rule database

1434 *** ZF ***

1436 * new primrec section allows primitive recursive functions to be given

1437 directly (as in HOL) over datatypes and the natural numbers;

1439 * new tactics induct_tac and exhaust_tac for induction (or case

1440 analysis) over datatypes and the natural numbers;

1442 * the datatype declaration of type T now defines the recursor T_rec;

1444 * simplification automatically does freeness reasoning for datatype

1445 constructors;

1447 * automatic type-inference, with AddTCs command to insert new

1448 type-checking rules;

1450 * datatype introduction rules are now added as Safe Introduction rules

1451 to the claset;

1453 * the syntax "if P then x else y" is now available in addition to

1454 if(P,x,y);

1457 *** Internal programming interfaces ***

1459 * tuned simplifier trace output; new flag debug_simp;

1461 * structures Vartab / Termtab (instances of TableFun) offer efficient

1462 tables indexed by indexname_ord / term_ord (compatible with aconv);

1464 * AxClass.axclass_tac lost the theory argument;

1466 * tuned current_goals_markers semantics: begin / end goal avoids

1467 printing empty lines;

1469 * removed prs and prs_fn hook, which was broken because it did not

1470 include \n in its semantics, forcing writeln to add one

1471 uncoditionally; replaced prs_fn by writeln_fn; consider std_output:

1472 string -> unit if you really want to output text without newline;

1474 * Symbol.output subject to print mode; INCOMPATIBILITY: defaults to

1475 plain output, interface builders may have to enable 'isabelle_font'

1476 mode to get Isabelle font glyphs as before;

1478 * refined token_translation interface; INCOMPATIBILITY: output length

1479 now of type real instead of int;

1481 * theory loader actions may be traced via new ThyInfo.add_hook

1482 interface (see src/Pure/Thy/thy_info.ML); example application: keep

1483 your own database of information attached to *whole* theories -- as

1484 opposed to intra-theory data slots offered via TheoryDataFun;

1486 * proper handling of dangling sort hypotheses (at last!);

1487 Thm.strip_shyps and Drule.strip_shyps_warning take care of removing

1488 extra sort hypotheses that can be witnessed from the type signature;

1489 the force_strip_shyps flag is gone, any remaining shyps are simply

1490 left in the theorem (with a warning issued by strip_shyps_warning);

1494 New in Isabelle98-1 (October 1998)

1495 ----------------------------------

1497 *** Overview of INCOMPATIBILITIES (see below for more details) ***

1499 * several changes of automated proof tools;

1501 * HOL: major changes to the inductive and datatype packages, including

1502 some minor incompatibilities of theory syntax;

1504 * HOL: renamed r^-1 to 'converse' from 'inverse'; 'inj_onto' is now

1505 called `inj_on';

1507 * HOL: removed duplicate thms in Arith:

1508 less_imp_add_less should be replaced by trans_less_add1

1509 le_imp_add_le should be replaced by trans_le_add1

1511 * HOL: unary minus is now overloaded (new type constraints may be

1512 required);

1514 * HOL and ZF: unary minus for integers is now #- instead of #~. In

1515 ZF, expressions such as n#-1 must be changed to n#- 1, since #-1 is

1516 now taken as an integer constant.

1518 * Pure: ML function 'theory_of' renamed to 'theory';

1521 *** Proof tools ***

1523 * Simplifier:

1524 1. Asm_full_simp_tac is now more aggressive.

1525 1. It will sometimes reorient premises if that increases their power to

1526 simplify.

1527 2. It does no longer proceed strictly from left to right but may also

1528 rotate premises to achieve further simplification.

1529 For compatibility reasons there is now Asm_lr_simp_tac which is like the

1530 old Asm_full_simp_tac in that it does not rotate premises.

1531 2. The simplifier now knows a little bit about nat-arithmetic.

1533 * Classical reasoner: wrapper mechanism for the classical reasoner now

1534 allows for selected deletion of wrappers, by introduction of names for

1535 wrapper functionals. This implies that addbefore, addSbefore,

1536 addaltern, and addSaltern now take a pair (name, tactic) as argument,

1537 and that adding two tactics with the same name overwrites the first

1538 one (emitting a warning).

1539 type wrapper = (int -> tactic) -> (int -> tactic)

1540 setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by

1541 addWrapper, addSWrapper: claset * (string * wrapper) -> claset

1542 delWrapper, delSWrapper: claset * string -> claset

1543 getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;

1545 * Classical reasoner: addbefore/addSbefore now have APPEND/ORELSE

1546 semantics; addbefore now affects only the unsafe part of step_tac

1547 etc.; this affects addss/auto_tac/force_tac, so EXISTING PROOFS MAY

1548 FAIL, but proofs should be fixable easily, e.g. by replacing Auto_tac

1549 by Force_tac;

1551 * Classical reasoner: setwrapper to setWrapper and compwrapper to

1552 compWrapper; added safe wrapper (and access functions for it);

1554 * HOL/split_all_tac is now much faster and fails if there is nothing

1555 to split. Some EXISTING PROOFS MAY REQUIRE ADAPTION because the order

1556 and the names of the automatically generated variables have changed.

1557 split_all_tac has moved within claset() from unsafe wrappers to safe

1558 wrappers, which means that !!-bound variables are split much more

1559 aggressively, and safe_tac and clarify_tac now split such variables.

1560 If this splitting is not appropriate, use delSWrapper "split_all_tac".

1561 Note: the same holds for record_split_tac, which does the job of

1562 split_all_tac for record fields.

1564 * HOL/Simplifier: Rewrite rules for case distinctions can now be added

1565 permanently to the default simpset using Addsplits just like

1566 Addsimps. They can be removed via Delsplits just like

1567 Delsimps. Lower-case versions are also available.

1569 * HOL/Simplifier: The rule split_if is now part of the default

1570 simpset. This means that the simplifier will eliminate all occurrences

1571 of if-then-else in the conclusion of a goal. To prevent this, you can

1572 either remove split_if completely from the default simpset by

1573 `Delsplits [split_if]' or remove it in a specific call of the

1574 simplifier using `... delsplits [split_if]'. You can also add/delete

1575 other case splitting rules to/from the default simpset: every datatype

1576 generates suitable rules `split_t_case' and `split_t_case_asm' (where

1577 t is the name of the datatype).

1579 * Classical reasoner / Simplifier combination: new force_tac (and

1580 derivatives Force_tac, force) combines rewriting and classical

1581 reasoning (and whatever other tools) similarly to auto_tac, but is

1582 aimed to solve the given subgoal completely.

1585 *** General ***

1587 * new top-level commands `Goal' and `Goalw' that improve upon `goal'

1588 and `goalw': the theory is no longer needed as an explicit argument -

1589 the current theory context is used; assumptions are no longer returned

1590 at the ML-level unless one of them starts with ==> or !!; it is

1591 recommended to convert to these new commands using isatool fixgoal

1592 (backup your sources first!);

1594 * new top-level commands 'thm' and 'thms' for retrieving theorems from

1595 the current theory context, and 'theory' to lookup stored theories;

1597 * new theory section 'locale' for declaring constants, assumptions and

1598 definitions that have local scope;

1600 * new theory section 'nonterminals' for purely syntactic types;

1602 * new theory section 'setup' for generic ML setup functions

1603 (e.g. package initialization);

1605 * the distribution now includes Isabelle icons: see

1606 lib/logo/isabelle-{small,tiny}.xpm;

1608 * isatool install - install binaries with absolute references to

1609 ISABELLE_HOME/bin;

1611 * isatool logo -- create instances of the Isabelle logo (as EPS);

1613 * print mode 'emacs' reserved for Isamode;

1615 * support multiple print (ast) translations per constant name;

1617 * theorems involving oracles are now printed with a suffixed [!];

1620 *** HOL ***

1622 * there is now a tutorial on Isabelle/HOL (do 'isatool doc tutorial');

1624 * HOL/inductive package reorganized and improved: now supports mutual

1625 definitions such as

1627 inductive EVEN ODD

1628 intrs

1629 null "0 : EVEN"

1630 oddI "n : EVEN ==> Suc n : ODD"

1631 evenI "n : ODD ==> Suc n : EVEN"

1633 new theorem list "elims" contains an elimination rule for each of the

1634 recursive sets; inductive definitions now handle disjunctive premises

1635 correctly (also ZF);

1637 INCOMPATIBILITIES: requires Inductive as an ancestor; component

1638 "mutual_induct" no longer exists - the induction rule is always

1639 contained in "induct";

1642 * HOL/datatype package re-implemented and greatly improved: now

1643 supports mutually recursive datatypes such as

1645 datatype

1646 'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp)

1647 | SUM ('a aexp) ('a aexp)

1648 | DIFF ('a aexp) ('a aexp)

1649 | NUM 'a

1650 and

1651 'a bexp = LESS ('a aexp) ('a aexp)

1652 | AND ('a bexp) ('a bexp)

1653 | OR ('a bexp) ('a bexp)

1655 as well as indirectly recursive datatypes such as

1657 datatype

1658 ('a, 'b) term = Var 'a

1659 | App 'b ((('a, 'b) term) list)

1661 The new tactic mutual_induct_tac [<var_1>, ..., <var_n>] i performs

1662 induction on mutually / indirectly recursive datatypes.

1664 Primrec equations are now stored in theory and can be accessed via

1665 <function_name>.simps.

1667 INCOMPATIBILITIES:

1669 - Theories using datatypes must now have theory Datatype as an

1670 ancestor.

1671 - The specific <typename>.induct_tac no longer exists - use the

1672 generic induct_tac instead.

1673 - natE has been renamed to nat.exhaust - use exhaust_tac

1674 instead of res_inst_tac ... natE. Note that the variable

1675 names in nat.exhaust differ from the names in natE, this

1676 may cause some "fragile" proofs to fail.

1677 - The theorems split_<typename>_case and split_<typename>_case_asm

1678 have been renamed to <typename>.split and <typename>.split_asm.

1679 - Since default sorts of type variables are now handled correctly,

1680 some datatype definitions may have to be annotated with explicit

1681 sort constraints.

1682 - Primrec definitions no longer require function name and type

1683 of recursive argument.

1685 Consider using isatool fixdatatype to adapt your theories and proof

1686 scripts to the new package (backup your sources first!).

1689 * HOL/record package: considerably improved implementation; now

1690 includes concrete syntax for record types, terms, updates; theorems

1691 for surjective pairing and splitting !!-bound record variables; proof

1692 support is as follows:

1694 1) standard conversions (selectors or updates applied to record

1695 constructor terms) are part of the standard simpset;

1697 2) inject equations of the form ((x, y) = (x', y')) == x=x' & y=y' are

1698 made part of standard simpset and claset via addIffs;

1700 3) a tactic for record field splitting (record_split_tac) is part of

1701 the standard claset (addSWrapper);

1703 To get a better idea about these rules you may retrieve them via

1704 something like 'thms "foo.simps"' or 'thms "foo.iffs"', where "foo" is

1705 the name of your record type.

1707 The split tactic 3) conceptually simplifies by the following rule:

1709 "(!!x. PROP ?P x) == (!!a b. PROP ?P (a, b))"

1711 Thus any record variable that is bound by meta-all will automatically

1712 blow up into some record constructor term, consequently the

1713 simplifications of 1), 2) apply. Thus force_tac, auto_tac etc. shall

1714 solve record problems automatically.

1717 * reorganized the main HOL image: HOL/Integ and String loaded by

1718 default; theory Main includes everything;

1720 * automatic simplification of integer sums and comparisons, using cancellation;

1722 * added option_map_eq_Some and not_Some_eq to the default simpset and claset;

1724 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset;

1726 * many new identities for unions, intersections, set difference, etc.;

1728 * expand_if, expand_split, expand_sum_case and expand_nat_case are now

1729 called split_if, split_split, split_sum_case and split_nat_case (to go

1730 with add/delsplits);

1732 * HOL/Prod introduces simplification procedure unit_eq_proc rewriting

1733 (?x::unit) = (); this is made part of the default simpset, which COULD

1734 MAKE EXISTING PROOFS FAIL under rare circumstances (consider

1735 'Delsimprocs [unit_eq_proc];' as last resort); also note that

1736 unit_abs_eta_conv is added in order to counter the effect of

1737 unit_eq_proc on (%u::unit. f u), replacing it by f rather than by

1738 %u.f();

1740 * HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which

1741 makes more sense);

1743 * HOL/Set INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;

1744 It and 'sym RS equals0D' are now in the default claset, giving automatic

1745 disjointness reasoning but breaking a few old proofs.

1747 * HOL/Relation INCOMPATIBILITY: renamed the relational operator r^-1

1748 to 'converse' from 'inverse' (for compatibility with ZF and some

1749 literature);

1751 * HOL/recdef can now declare non-recursive functions, with {} supplied as

1752 the well-founded relation;

1754 * HOL/Set INCOMPATIBILITY: the complement of set A is now written -A instead of

1755 Compl A. The "Compl" syntax remains available as input syntax for this

1756 release ONLY.

1758 * HOL/Update: new theory of function updates:

1759 f(a:=b) == %x. if x=a then b else f x

1760 may also be iterated as in f(a:=b,c:=d,...);

1762 * HOL/Vimage: new theory for inverse image of a function, syntax f-``B;

1764 * HOL/List:

1765 - new function list_update written xs[i:=v] that updates the i-th

1766 list position. May also be iterated as in xs[i:=a,j:=b,...].

1767 - new function `upt' written [i..j(] which generates the list

1768 [i,i+1,...,j-1], i.e. the upper bound is excluded. To include the upper

1769 bound write [i..j], which is a shorthand for [i..j+1(].

1770 - new lexicographic orderings and corresponding wellfoundedness theorems.

1772 * HOL/Arith:

1773 - removed 'pred' (predecessor) function;

1774 - generalized some theorems about n-1;

1775 - many new laws about "div" and "mod";

1776 - new laws about greatest common divisors (see theory ex/Primes);

1778 * HOL/Relation: renamed the relational operator r^-1 "converse"

1779 instead of "inverse";

1781 * HOL/Induct/Multiset: a theory of multisets, including the wellfoundedness

1782 of the multiset ordering;

1784 * directory HOL/Real: a construction of the reals using Dedekind cuts

1785 (not included by default);

1787 * directory HOL/UNITY: Chandy and Misra's UNITY formalism;

1789 * directory HOL/Hoare: a new version of Hoare logic which permits many-sorted

1790 programs, i.e. different program variables may have different types.

1792 * calling (stac rew i) now fails if "rew" has no effect on the goal

1793 [previously, this check worked only if the rewrite rule was unconditional]

1794 Now rew can involve either definitions or equalities (either == or =).

1797 *** ZF ***

1799 * theory Main includes everything; INCOMPATIBILITY: theory ZF.thy contains

1800 only the theorems proved on ZF.ML;

1802 * ZF INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;

1803 It and 'sym RS equals0D' are now in the default claset, giving automatic

1804 disjointness reasoning but breaking a few old proofs.

1806 * ZF/Update: new theory of function updates

1807 with default rewrite rule f(x:=y) ` z = if(z=x, y, f`z)

1808 may also be iterated as in f(a:=b,c:=d,...);

1810 * in let x=t in u(x), neither t nor u(x) has to be an FOL term.

1812 * calling (stac rew i) now fails if "rew" has no effect on the goal

1813 [previously, this check worked only if the rewrite rule was unconditional]

1814 Now rew can involve either definitions or equalities (either == or =).

1816 * case_tac provided for compatibility with HOL

1817 (like the old excluded_middle_tac, but with subgoals swapped)

1820 *** Internal programming interfaces ***

1822 * Pure: several new basic modules made available for general use, see

1823 also src/Pure/README;

1825 * improved the theory data mechanism to support encapsulation (data

1826 kind name replaced by private Object.kind, acting as authorization

1827 key); new type-safe user interface via functor TheoryDataFun; generic

1828 print_data function becomes basically useless;

1830 * removed global_names compatibility flag -- all theory declarations

1831 are qualified by default;

1833 * module Pure/Syntax now offers quote / antiquote translation

1834 functions (useful for Hoare logic etc. with implicit dependencies);

1835 see HOL/ex/Antiquote for an example use;

1837 * Simplifier now offers conversions (asm_)(full_)rewrite: simpset ->

1838 cterm -> thm;

1840 * new tactical CHANGED_GOAL for checking that a tactic modifies a

1841 subgoal;

1843 * Display.print_goals function moved to Locale.print_goals;

1845 * standard print function for goals supports current_goals_markers

1846 variable for marking begin of proof, end of proof, start of goal; the

1847 default is ("", "", ""); setting current_goals_markers := ("<proof>",

1848 "</proof>", "<goal>") causes SGML like tagged proof state printing,

1849 for example;

1853 New in Isabelle98 (January 1998)

1854 --------------------------------

1856 *** Overview of INCOMPATIBILITIES (see below for more details) ***

1858 * changed lexical syntax of terms / types: dots made part of long

1859 identifiers, e.g. "%x.x" no longer possible, should be "%x. x";

1861 * simpset (and claset) reference variable replaced by functions

1862 simpset / simpset_ref;

1864 * no longer supports theory aliases (via merge) and non-trivial

1865 implicit merge of thms' signatures;

1867 * most internal names of constants changed due to qualified names;

1869 * changed Pure/Sequence interface (see Pure/seq.ML);

1872 *** General Changes ***

1874 * hierachically structured name spaces (for consts, types, axms, thms

1875 etc.); new lexical class 'longid' (e.g. Foo.bar.x) may render much of

1876 old input syntactically incorrect (e.g. "%x.x"); COMPATIBILITY:

1877 isatool fixdots ensures space after dots (e.g. "%x. x"); set

1878 long_names for fully qualified output names; NOTE: ML programs

1879 (special tactics, packages etc.) referring to internal names may have

1880 to be adapted to cope with fully qualified names; in case of severe

1881 backward campatibility problems try setting 'global_names' at compile

1882 time to have enrything declared within a flat name space; one may also

1883 fine tune name declarations in theories via the 'global' and 'local'

1884 section;

1886 * reimplemented the implicit simpset and claset using the new anytype

1887 data filed in signatures; references simpset:simpset ref etc. are

1888 replaced by functions simpset:unit->simpset and

1889 simpset_ref:unit->simpset ref; COMPATIBILITY: use isatool fixclasimp

1890 to patch your ML files accordingly;

1892 * HTML output now includes theory graph data for display with Java

1893 applet or isatool browser; data generated automatically via isatool

1894 usedir (see -i option, ISABELLE_USEDIR_OPTIONS);

1896 * defs may now be conditional; improved rewrite_goals_tac to handle

1897 conditional equations;

1899 * defs now admits additional type arguments, using TYPE('a) syntax;

1901 * theory aliases via merge (e.g. M=A+B+C) no longer supported, always

1902 creates a new theory node; implicit merge of thms' signatures is

1903 restricted to 'trivial' ones; COMPATIBILITY: one may have to use

1904 transfer:theory->thm->thm in (rare) cases;

1906 * improved handling of draft signatures / theories; draft thms (and

1907 ctyps, cterms) are automatically promoted to real ones;

1909 * slightly changed interfaces for oracles: admit many per theory, named

1910 (e.g. oracle foo = mlfun), additional name argument for invoke_oracle;

1912 * print_goals: optional output of const types (set show_consts and

1913 show_types);

1915 * improved output of warnings (###) and errors (***);

1917 * subgoal_tac displays a warning if the new subgoal has type variables;

1919 * removed old README and Makefiles;

1921 * replaced print_goals_ref hook by print_current_goals_fn and result_error_fn;

1923 * removed obsolete init_pps and init_database;

1925 * deleted the obsolete tactical STATE, which was declared by

1926 fun STATE tacfun st = tacfun st st;

1928 * cd and use now support path variables, e.g. $ISABELLE_HOME, or ~

1929 (which abbreviates $HOME);

1931 * changed Pure/Sequence interface (see Pure/seq.ML); COMPATIBILITY:

1932 use isatool fixseq to adapt your ML programs (this works for fully

1933 qualified references to the Sequence structure only!);

1935 * use_thy no longer requires writable current directory; it always

1936 reloads .ML *and* .thy file, if either one is out of date;

1939 *** Classical Reasoner ***

1941 * Clarify_tac, clarify_tac, clarify_step_tac, Clarify_step_tac: new

1942 tactics that use classical reasoning to simplify a subgoal without

1943 splitting it into several subgoals;

1945 * Safe_tac: like safe_tac but uses the default claset;

1948 *** Simplifier ***

1950 * added simplification meta rules:

1951 (asm_)(full_)simplify: simpset -> thm -> thm;

1953 * simplifier.ML no longer part of Pure -- has to be loaded by object

1954 logics (again);

1956 * added prems argument to simplification procedures;

1958 * HOL, FOL, ZF: added infix function `addsplits':

1959 instead of `<simpset> setloop (split_tac <thms>)'

1960 you can simply write `<simpset> addsplits <thms>'

1963 *** Syntax ***

1965 * TYPE('a) syntax for type reflection terms;

1967 * no longer handles consts with name "" -- declare as 'syntax' instead;

1969 * pretty printer: changed order of mixfix annotation preference (again!);

1971 * Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;

1974 *** HOL ***

1976 * HOL: there is a new splitter `split_asm_tac' that can be used e.g.

1977 with `addloop' of the simplifier to faciliate case splitting in premises.

1979 * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;

1981 * HOL/Auth: new protocol proofs including some for the Internet

1982 protocol TLS;

1984 * HOL/Map: new theory of `maps' a la VDM;

1986 * HOL/simplifier: simplification procedures nat_cancel_sums for

1987 cancelling out common nat summands from =, <, <= (in)equalities, or

1988 differences; simplification procedures nat_cancel_factor for

1989 cancelling common factor from =, <, <= (in)equalities over natural

1990 sums; nat_cancel contains both kinds of procedures, it is installed by

1991 default in Arith.thy -- this COULD MAKE EXISTING PROOFS FAIL;

1993 * HOL/simplifier: terms of the form

1994 `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x)

1995 are rewritten to

1996 `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)',

1997 and those of the form

1998 `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)' (or t=x)

1999 are rewritten to

2000 `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) --> R(t)',

2002 * HOL/datatype

2003 Each datatype `t' now comes with a theorem `split_t_case' of the form

2005 P(t_case f1 ... fn x) =

2006 ( (!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1)) &

2007 ...

2008 (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))

2009 )

2011 and a theorem `split_t_case_asm' of the form

2013 P(t_case f1 ... fn x) =

2014 ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |

2015 ...

2016 (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))

2017 )

2018 which can be added to a simpset via `addsplits'. The existing theorems

2019 expand_list_case and expand_option_case have been renamed to

2020 split_list_case and split_option_case.

2022 * HOL/Arithmetic:

2023 - `pred n' is automatically converted to `n-1'.

2024 Users are strongly encouraged not to use `pred' any longer,

2025 because it will disappear altogether at some point.

2026 - Users are strongly encouraged to write "0 < n" rather than

2027 "n ~= 0". Theorems and proof tools have been modified towards this

2028 `standard'.

2030 * HOL/Lists:

2031 the function "set_of_list" has been renamed "set" (and its theorems too);

2032 the function "nth" now takes its arguments in the reverse order and

2033 has acquired the infix notation "!" as in "xs!n".

2035 * HOL/Set: UNIV is now a constant and is no longer translated to Compl{};

2037 * HOL/Set: The operator (UN x.B x) now abbreviates (UN x:UNIV. B x) and its

2038 specialist theorems (like UN1_I) are gone. Similarly for (INT x.B x);

2040 * HOL/record: extensible records with schematic structural subtyping

2041 (single inheritance); EXPERIMENTAL version demonstrating the encoding,

2042 still lacks various theorems and concrete record syntax;

2045 *** HOLCF ***

2047 * removed "axioms" and "generated by" sections;

2049 * replaced "ops" section by extended "consts" section, which is capable of

2050 handling the continuous function space "->" directly;

2052 * domain package:

2053 . proves theorems immediately and stores them in the theory,

2054 . creates hierachical name space,

2055 . now uses normal mixfix annotations (instead of cinfix...),

2056 . minor changes to some names and values (for consistency),

2057 . e.g. cases -> casedist, dists_eq -> dist_eqs, [take_lemma] -> take_lemmas,

2058 . separator between mutual domain defs: changed "," to "and",

2059 . improved handling of sort constraints; now they have to

2060 appear on the left-hand side of the equations only;

2062 * fixed LAM <x,y,zs>.b syntax;

2064 * added extended adm_tac to simplifier in HOLCF -- can now discharge

2065 adm (%x. P (t x)), where P is chainfinite and t continuous;

2068 *** FOL and ZF ***

2070 * FOL: there is a new splitter `split_asm_tac' that can be used e.g.

2071 with `addloop' of the simplifier to faciliate case splitting in premises.

2073 * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as

2074 in HOL, they strip ALL and --> from proved theorems;

2078 New in Isabelle94-8 (May 1997)

2079 ------------------------------

2081 *** General Changes ***

2083 * new utilities to build / run / maintain Isabelle etc. (in parts

2084 still somewhat experimental); old Makefiles etc. still functional;

2086 * new 'Isabelle System Manual';

2088 * INSTALL text, together with ./configure and ./build scripts;

2090 * reimplemented type inference for greater efficiency, better error

2091 messages and clean internal interface;

2093 * prlim command for dealing with lots of subgoals (an easier way of

2094 setting goals_limit);

2097 *** Syntax ***

2099 * supports alternative (named) syntax tables (parser and pretty

2100 printer); internal interface is provided by add_modesyntax(_i);

2102 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to

2103 be used in conjunction with the Isabelle symbol font; uses the

2104 "symbols" syntax table;

2106 * added token_translation interface (may translate name tokens in

2107 arbitrary ways, dependent on their type (free, bound, tfree, ...) and

2108 the current print_mode); IMPORTANT: user print translation functions

2109 are responsible for marking newly introduced bounds

2110 (Syntax.mark_boundT);

2112 * token translations for modes "xterm" and "xterm_color" that display

2113 names in bold, underline etc. or colors (which requires a color

2114 version of xterm);

2116 * infixes may now be declared with names independent of their syntax;

2118 * added typed_print_translation (like print_translation, but may

2119 access type of constant);

2122 *** Classical Reasoner ***

2124 Blast_tac: a new tactic! It is often more powerful than fast_tac, but has

2125 some limitations. Blast_tac...

2126 + ignores addss, addbefore, addafter; this restriction is intrinsic

2127 + ignores elimination rules that don't have the correct format

2128 (the conclusion MUST be a formula variable)

2129 + ignores types, which can make HOL proofs fail

2130 + rules must not require higher-order unification, e.g. apply_type in ZF

2131 [message "Function Var's argument not a bound variable" relates to this]

2132 + its proof strategy is more general but can actually be slower

2134 * substitution with equality assumptions no longer permutes other

2135 assumptions;

2137 * minor changes in semantics of addafter (now called addaltern); renamed

2138 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper

2139 (and access functions for it);

2141 * improved combination of classical reasoner and simplifier:

2142 + functions for handling clasimpsets

2143 + improvement of addss: now the simplifier is called _after_ the

2144 safe steps.

2145 + safe variant of addss called addSss: uses safe simplifications

2146 _during_ the safe steps. It is more complete as it allows multiple

2147 instantiations of unknowns (e.g. with slow_tac).

2149 *** Simplifier ***

2151 * added interface for simplification procedures (functions that

2152 produce *proven* rewrite rules on the fly, depending on current

2153 redex);

2155 * ordering on terms as parameter (used for ordered rewriting);

2157 * new functions delcongs, deleqcongs, and Delcongs. richer rep_ss;

2159 * the solver is now split into a safe and an unsafe part.

2160 This should be invisible for the normal user, except that the

2161 functions setsolver and addsolver have been renamed to setSolver and

2162 addSolver; added safe_asm_full_simp_tac;

2165 *** HOL ***

2167 * a generic induction tactic `induct_tac' which works for all datatypes and

2168 also for type `nat';

2170 * a generic case distinction tactic `exhaust_tac' which works for all

2171 datatypes and also for type `nat';

2173 * each datatype comes with a function `size';

2175 * patterns in case expressions allow tuple patterns as arguments to

2176 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...';

2178 * primrec now also works with type nat;

2180 * recdef: a new declaration form, allows general recursive functions to be

2181 defined in theory files. See HOL/ex/Fib, HOL/ex/Primes, HOL/Subst/Unify.

2183 * the constant for negation has been renamed from "not" to "Not" to

2184 harmonize with FOL, ZF, LK, etc.;

2186 * HOL/ex/LFilter theory of a corecursive "filter" functional for

2187 infinite lists;

2189 * HOL/Modelcheck demonstrates invocation of model checker oracle;

2191 * HOL/ex/Ring.thy declares cring_simp, which solves equational

2192 problems in commutative rings, using axiomatic type classes for + and *;

2194 * more examples in HOL/MiniML and HOL/Auth;

2196 * more default rewrite rules for quantifiers, union/intersection;

2198 * a new constant `arbitrary == @x.False';

2200 * HOLCF/IOA replaces old HOL/IOA;

2202 * HOLCF changes: derived all rules and arities

2203 + axiomatic type classes instead of classes

2204 + typedef instead of faking type definitions

2205 + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.

2206 + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po

2207 + eliminated the types void, one, tr

2208 + use unit lift and bool lift (with translations) instead of one and tr

2209 + eliminated blift from Lift3.thy (use Def instead of blift)

2210 all eliminated rules are derived as theorems --> no visible changes ;

2213 *** ZF ***

2215 * ZF now has Fast_tac, Simp_tac and Auto_tac. Union_iff is a now a default

2216 rewrite rule; this may affect some proofs. eq_cs is gone but can be put back

2217 as ZF_cs addSIs [equalityI];

2221 New in Isabelle94-7 (November 96)

2222 ---------------------------------

2224 * allowing negative levels (as offsets) in prlev and choplev;

2226 * super-linear speedup for large simplifications;

2228 * FOL, ZF and HOL now use miniscoping: rewriting pushes

2229 quantifications in as far as possible (COULD MAKE EXISTING PROOFS

2230 FAIL); can suppress it using the command Delsimps (ex_simps @

2231 all_simps); De Morgan laws are also now included, by default;

2233 * improved printing of ==> : ~:

2235 * new object-logic "Sequents" adds linear logic, while replacing LK

2236 and Modal (thanks to Sara Kalvala);

2238 * HOL/Auth: correctness proofs for authentication protocols;

2240 * HOL: new auto_tac combines rewriting and classical reasoning (many

2241 examples on HOL/Auth);

2243 * HOL: new command AddIffs for declaring theorems of the form P=Q to

2244 the rewriter and classical reasoner simultaneously;

2246 * function uresult no longer returns theorems in "standard" format;

2247 regain previous version by: val uresult = standard o uresult;

2251 New in Isabelle94-6

2252 -------------------

2254 * oracles -- these establish an interface between Isabelle and trusted

2255 external reasoners, which may deliver results as theorems;

2257 * proof objects (in particular record all uses of oracles);

2259 * Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;

2261 * "constdefs" section in theory files;

2263 * "primrec" section (HOL) no longer requires names;

2265 * internal type "tactic" now simply "thm -> thm Sequence.seq";

2269 New in Isabelle94-5

2270 -------------------

2272 * reduced space requirements;

2274 * automatic HTML generation from theories;

2276 * theory files no longer require "..." (quotes) around most types;

2278 * new examples, including two proofs of the Church-Rosser theorem;

2280 * non-curried (1994) version of HOL is no longer distributed;

2284 New in Isabelle94-4

2285 -------------------

2287 * greatly reduced space requirements;

2289 * theory files (.thy) no longer require \...\ escapes at line breaks;

2291 * searchable theorem database (see the section "Retrieving theorems" on

2292 page 8 of the Reference Manual);

2294 * new examples, including Grabczewski's monumental case study of the

2295 Axiom of Choice;

2297 * The previous version of HOL renamed to Old_HOL;

2299 * The new version of HOL (previously called CHOL) uses a curried syntax

2300 for functions. Application looks like f a b instead of f(a,b);

2302 * Mutually recursive inductive definitions finally work in HOL;

2304 * In ZF, pattern-matching on tuples is now available in all abstractions and

2305 translates to the operator "split";

2309 New in Isabelle94-3

2310 -------------------

2312 * new infix operator, addss, allowing the classical reasoner to

2313 perform simplification at each step of its search. Example:

2314 fast_tac (cs addss ss)

2316 * a new logic, CHOL, the same as HOL, but with a curried syntax

2317 for functions. Application looks like f a b instead of f(a,b). Also pairs

2318 look like (a,b) instead of <a,b>;

2320 * PLEASE NOTE: CHOL will eventually replace HOL!

2322 * In CHOL, pattern-matching on tuples is now available in all abstractions.

2323 It translates to the operator "split". A new theory of integers is available;

2325 * In ZF, integer numerals now denote two's-complement binary integers.

2326 Arithmetic operations can be performed by rewriting. See ZF/ex/Bin.ML;

2328 * Many new examples: I/O automata, Church-Rosser theorem, equivalents

2329 of the Axiom of Choice;

2333 New in Isabelle94-2

2334 -------------------

2336 * Significantly faster resolution;

2338 * the different sections in a .thy file can now be mixed and repeated

2339 freely;

2341 * Database of theorems for FOL, HOL and ZF. New

2342 commands including qed, qed_goal and bind_thm store theorems in the database.

2344 * Simple database queries: return a named theorem (get_thm) or all theorems of

2345 a given theory (thms_of), or find out what theory a theorem was proved in

2346 (theory_of_thm);

2348 * Bugs fixed in the inductive definition and datatype packages;

2350 * The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs

2351 and HOL_dup_cs obsolete;

2353 * Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1

2354 have been removed;

2356 * Simpler definition of function space in ZF;

2358 * new results about cardinal and ordinal arithmetic in ZF;

2360 * 'subtype' facility in HOL for introducing new types as subsets of existing

2361 types;

2364 $Id$