NEWS
author wenzelm
Mon Nov 12 23:25:25 2001 +0100 (2001-11-12)
changeset 12163 04c98351f9af
parent 12159 b3a708ddedf8
child 12177 b1c16d685a99
permissions -rw-r--r--
Isar: 'induct' proper support for mutual induction involving
non-atomic rule statements;
Isar/Pure: support multiple simultaneous goal statements;
     1 
     2 Isabelle NEWS -- history user-relevant changes
     3 ==============================================
     4 
     5 New in Isabelle2001 (?? 2001)
     6 -----------------------------
     7 
     8 *** Document preparation ***
     9 
    10 * greatly simplified document preparation setup, including more
    11 graceful interpretation of isatool usedir -i/-d/-D options, and more
    12 instructive isatool mkdir; users should basically be able to get
    13 started with "isatool mkdir Test && isatool make";
    14 
    15 * theory dependency graph may now be incorporated into documents;
    16 isatool usedir -g true will produce session_graph.eps/.pdf for use
    17 with \includegraphics of LaTeX;
    18 
    19 * proper spacing of consecutive markup elements, especially text
    20 blocks after section headings;
    21 
    22 * support bold style (for single symbols only), input syntax is like
    23 this: "\<^bold>\<alpha>" or "\<^bold>A";
    24 
    25 * \<bullet> is now output as bold \cdot by default, which looks much
    26 better in printed text;
    27 
    28 * added default LaTeX bindings for \<tturnstile> and \<TTurnstile>;
    29 note that these symbols are currently unavailable in Proof General /
    30 X-Symbol;
    31 
    32 
    33 *** Isar ***
    34 
    35 * improved proof by cases and induction:
    36   - removed obsolete "(simplified)" and "(stripped)" options of methods;
    37   - added 'print_induct_rules' (covered by help item in Proof General > 3.3);
    38   - moved induct/cases attributes to Pure, methods to Provers;
    39   - generic method setup instantiated for FOL and HOL;
    40 
    41   - 'case' command admits impromptu naming of parameters (such as
    42 "case (Suc n)");
    43 
    44   - 'induct' method divinates rule instantiation from the inductive
    45 claim; no longer requires excessive ?P bindings for proper
    46 instantiation of cases;
    47 
    48   - 'induct' method properly enumerates all possibilities of set/type
    49 rules; as a consequence facts may be also passed through *type* rules
    50 without further ado;
    51 
    52   - 'induct' method now derives symbolic cases from the *rulified*
    53 rule (before it used to rulify cases stemming from the internal
    54 atomized version); this means that the context of a non-atomic
    55 statement becomes is included in the hypothesis, avoiding the slightly
    56 cumbersome show "PROP ?case" form;
    57 
    58   - 'induct' may now use elim-style induction rules without chaining
    59 facts, using ``missing'' premises from the goal state; this allows
    60 rules stemming from inductive sets to be applied in unstructured
    61 scripts, while still benefitting from proper handling of non-atomic
    62 statements; NB: major inductive premises need to be put first, all the
    63 rest of the goal is passed through the induction;
    64 
    65 - 'induct' proper support for mutual induction involving non-atomic
    66 rule statements (uses the new concept of simultaneous goals, see
    67 below);
    68 
    69 * Pure: support multiple simultaneous goal statements, for example
    70 "have a: A and b: B" (same for 'theorem' etc.); being a pure
    71 meta-level mechanism, this acts as if several individual goals had
    72 been stated separately; in particular common proof methods need to be
    73 repeated in order to cover all claims; note that a single elimination
    74 step is *not* sufficient to establish the two conjunctions, so this
    75 fails:
    76 
    77   assume "A & B" then have A and B ..   (*".." fails*)
    78 
    79 better use "obtain" in situations as above; alternative refer to
    80 multi-step methods like 'auto', 'simp_all', 'blast+' etc.;
    81 
    82 * Pure: proper integration with ``locales''; unlike the original
    83 version by Florian Kammueller, Isar locales package high-level proof
    84 contexts rather than raw logical ones (e.g. we admit to include
    85 attributes everywhere);
    86 
    87 * Pure: theory goals now support ad-hoc contexts, which are discharged
    88 in the result, as in ``lemma (assumes A and B) K: A .''; syntax
    89 coincides with that of a locale body;
    90 
    91 * Pure: renamed "antecedent" case to "rule_context";
    92 
    93 * Pure: added 'corollary' command;
    94 
    95 * Pure: fixed 'token_translation' command;
    96 
    97 * Pure: removed obsolete 'exported' attribute;
    98 
    99 * Pure: dummy pattern "_" in is/let is now automatically lifted over
   100 bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x")
   101 supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");
   102 
   103 * Pure: method 'atomize' presents local goal premises as object-level
   104 statements (atomic meta-level propositions); setup controlled via
   105 rewrite rules declarations of 'atomize' attribute; example
   106 application: 'induct' method with proper rule statements in improper
   107 proof *scripts*;
   108 
   109 * Pure: emulation of instantiation tactics (rule_tac, cut_tac, etc.)
   110 now consider the syntactic context of assumptions, giving a better
   111 chance to get type-inference of the arguments right (this is
   112 especially important for locales);
   113 
   114 * Provers: 'simplified' attribute may refer to explicit rules instead
   115 of full simplifier context; 'iff' attribute handles conditional rules;
   116 
   117 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
   118 
   119 * HOL: 'recdef' now fails on unfinished automated proofs, use
   120 "(permissive)" option to recover old behavior;
   121 
   122 * HOL: 'inductive' no longer features separate (collective) attributes
   123 for 'intros' (was found too confusing);
   124 
   125 
   126 
   127 *** HOL ***
   128 
   129 * HOL: moved over to sane numeral syntax; the new policy is as
   130 follows:
   131 
   132   - 0 and 1 are polymorphic constants, which are defined on any
   133   numeric type (nat, int, real etc.);
   134 
   135   - 2, 3, 4, ... and -1, -2, -3, ... are polymorphic numerals, based
   136   binary representation internally;
   137 
   138   - type nat has special constructor Suc, and generally prefers Suc 0
   139   over 1::nat and Suc (Suc 0) over 2::nat;
   140 
   141 This change may cause significant INCOMPATIBILITIES; here are some
   142 hints on converting existing sources:
   143 
   144   - due to the new "num" token, "-0" and "-1" etc. are now atomic
   145   entities, so expressions involving "-" (unary or binary minus) need
   146   to be spaced properly;
   147 
   148   - existing occurrences of "1" may need to be constraint "1::nat" or
   149   even replaced by Suc 0; similar for old "2";
   150 
   151   - replace "#nnn" by "nnn", and "#-nnn" by "-nnn";
   152 
   153   - remove all special provisions on numerals in proofs;
   154 
   155 * HOL/record:
   156   - removed old "make" and "make_scheme" operations -- INCOMPATIBILITY;
   157   - removed "more" class (simply use "term") -- INCOMPATIBILITY;
   158   - provides cases/induct rules for use with corresponding Isar methods;
   159   - new derived operations "make" (for adding fields of current
   160     record), "extend" to promote fixed record to record scheme, and
   161     "truncate" for the reverse; cf. theorems "derived_defs", which are
   162     *not* declared as simp by default;
   163   - internal definitions directly based on a light-weight abstract
   164     theory of product types over typedef rather than datatype;
   165 
   166 * HOL: canonical cases/induct rules for n-tuples (n = 3..7);
   167 
   168 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
   169 (beware of argument permutation!);
   170 
   171 * HOL: linorder_less_split superseded by linorder_cases;
   172 
   173 * HOL: added "The" definite description operator; move Hilbert's "Eps"
   174 to peripheral theory "Hilbert_Choice";
   175 
   176 * HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so
   177 in this (rare) case use:
   178 
   179   delSWrapper "split_all_tac"
   180   addSbefore ("unsafe_split_all_tac", unsafe_split_all_tac)
   181 
   182 * HOL: added safe wrapper "split_conv_tac" to claset; EXISTING PROOFS
   183 MAY FAIL;
   184 
   185 * HOL: introduced f^n = f o ... o f; warning: due to the limits of
   186 Isabelle's type classes, ^ on functions and relations has too general
   187 a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be
   188 necessary to attach explicit type constraints;
   189 
   190 * HOL: syntax translations now work properly with numerals and records
   191 expressions;
   192 
   193 * HOL/GroupTheory: group theory examples including Sylow's theorem, by
   194 Florian Kammüller;
   195 
   196 * HOL: got rid of some global declarations (potential INCOMPATIBILITY
   197 for ML tools): const "()" renamed "Product_Type.Unity", type "unit"
   198 renamed "Product_Type.unit";
   199 
   200 
   201 *** HOLCF ***
   202 
   203 * proper rep_datatype lift (see theory Lift); use plain induct_tac
   204 instead of former lift.induct_tac; always use UU instead of Undef;
   205 
   206 * 'domain' package adapted to new-style theories, e.g. see
   207 HOLCF/ex/Dnat.thy;
   208 
   209 
   210 *** ZF ***
   211 
   212 * ZF: the integer library now covers quotients and remainders, with
   213 many laws relating division to addition, multiplication, etc.;
   214 
   215 * ZF/Induct: new directory for examples of inductive definitions, including theory
   216 Multiset for multiset orderings;
   217 
   218 * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a typeless
   219 version of the formalism;
   220 
   221 
   222 *** General ***
   223 
   224 * kernel: meta-level proof terms (by Stefan Berghofer), see also ref
   225 manual;
   226 
   227 * Pure/axclass: removed obsolete ML interface goal_subclass/goal_arity;
   228 
   229 * classical: renamed addaltern to addafter, addSaltern to addSafter;
   230 
   231 * clasimp: ``iff'' declarations now handle conditional rules as well;
   232 
   233 * syntax: new token syntax "num" for plain numerals (without "#" of
   234 "xnum"); potential INCOMPATIBILITY, since -0, -1 etc. are now separate
   235 tokens, so expressions involving minus need to be spaced properly;
   236 
   237 * syntax: support non-oriented infixes;
   238 
   239 * syntax: print modes "type_brackets" and "no_type_brackets" control
   240 output of nested => (types); the default behavior is "type_brackets";
   241 
   242 * syntax: builtin parse translation for "_constify" turns valued
   243 tokens into AST constants;
   244 
   245 * system: refrain from any attempt at filtering input streams; no
   246 longer support ``8bit'' encoding of old isabelle font, instead proper
   247 iso-latin characters may now be used;
   248 
   249 * system: support Poly/ML 4.1.1 (now able to manage large heaps);
   250 
   251 * system: Proof General keywords specification is now part of the
   252 Isabelle distribution (see etc/isar-keywords.el);
   253 
   254 * system: smart selection of Isabelle process versus Isabelle
   255 interface, accommodates case-insensitive file systems (e.g. HFS+); may
   256 run both "isabelle" and "Isabelle" even if file names are badly
   257 damaged (executable inspects the case of the first letter of its own
   258 name); added separate "isabelle-process" and "isabelle-interface";
   259 
   260 
   261 
   262 New in Isabelle99-2 (February 2001)
   263 -----------------------------------
   264 
   265 *** Overview of INCOMPATIBILITIES ***
   266 
   267 * HOL: please note that theories in the Library and elsewhere often use the
   268 new-style (Isar) format; to refer to their theorems in an ML script you must
   269 bind them to ML identifers by e.g.	val thm_name = thm "thm_name";
   270 
   271 * HOL: inductive package no longer splits induction rule aggressively,
   272 but only as far as specified by the introductions given; the old
   273 format may be recovered via ML function complete_split_rule or attribute
   274 'split_rule (complete)';
   275 
   276 * HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold,
   277 gfp_Tarski to gfp_unfold;
   278 
   279 * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;
   280 
   281 * HOL: infix "dvd" now has priority 50 rather than 70 (because it is a
   282 relation); infix "^^" has been renamed "``"; infix "``" has been
   283 renamed "`"; "univalent" has been renamed "single_valued";
   284 
   285 * HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse"
   286 operation;
   287 
   288 * HOLCF: infix "`" has been renamed "$"; the symbol syntax is \<cdot>;
   289 
   290 * Isar: 'obtain' no longer declares "that" fact as simp/intro;
   291 
   292 * Isar/HOL: method 'induct' now handles non-atomic goals; as a
   293 consequence, it is no longer monotonic wrt. the local goal context
   294 (which is now passed through the inductive cases);
   295 
   296 * Document preparation: renamed standard symbols \<ll> to \<lless> and
   297 \<gg> to \<ggreater>;
   298 
   299 
   300 *** Document preparation ***
   301 
   302 * \isabellestyle{NAME} selects version of Isabelle output (currently
   303 available: are "it" for near math-mode best-style output, "sl" for
   304 slanted text style, and "tt" for plain type-writer; if no
   305 \isabellestyle command is given, output is according to slanted
   306 type-writer);
   307 
   308 * support sub/super scripts (for single symbols only), input syntax is
   309 like this: "A\<^sup>*" or "A\<^sup>\<star>";
   310 
   311 * some more standard symbols; see Appendix A of the system manual for
   312 the complete list of symbols defined in isabellesym.sty;
   313 
   314 * improved isabelle style files; more abstract symbol implementation
   315 (should now use \isamath{...} and \isatext{...} in custom symbol
   316 definitions);
   317 
   318 * antiquotation @{goals} and @{subgoals} for output of *dynamic* goals
   319 state; Note that presentation of goal states does not conform to
   320 actual human-readable proof documents.  Please do not include goal
   321 states into document output unless you really know what you are doing!
   322 
   323 * proper indentation of antiquoted output with proportional LaTeX
   324 fonts;
   325 
   326 * no_document ML operator temporarily disables LaTeX document
   327 generation;
   328 
   329 * isatool unsymbolize tunes sources for plain ASCII communication;
   330 
   331 
   332 *** Isar ***
   333 
   334 * Pure: Isar now suffers initial goal statements to contain unbound
   335 schematic variables (this does not conform to actual readable proof
   336 documents, due to unpredictable outcome and non-compositional proof
   337 checking); users who know what they are doing may use schematic goals
   338 for Prolog-style synthesis of proven results;
   339 
   340 * Pure: assumption method (an implicit finishing) now handles actual
   341 rules as well;
   342 
   343 * Pure: improved 'obtain' --- moved to Pure, insert "that" into
   344 initial goal, declare "that" only as Pure intro (only for single
   345 steps); the "that" rule assumption may now be involved in implicit
   346 finishing, thus ".." becomes a feasible for trivial obtains;
   347 
   348 * Pure: default proof step now includes 'intro_classes'; thus trivial
   349 instance proofs may be performed by "..";
   350 
   351 * Pure: ?thesis / ?this / "..." now work for pure meta-level
   352 statements as well;
   353 
   354 * Pure: more robust selection of calculational rules;
   355 
   356 * Pure: the builtin notion of 'finished' goal now includes the ==-refl
   357 rule (as well as the assumption rule);
   358 
   359 * Pure: 'thm_deps' command visualizes dependencies of theorems and
   360 lemmas, using the graph browser tool;
   361 
   362 * Pure: predict failure of "show" in interactive mode;
   363 
   364 * Pure: 'thms_containing' now takes actual terms as arguments;
   365 
   366 * HOL: improved method 'induct' --- now handles non-atomic goals
   367 (potential INCOMPATIBILITY); tuned error handling;
   368 
   369 * HOL: cases and induct rules now provide explicit hints about the
   370 number of facts to be consumed (0 for "type" and 1 for "set" rules);
   371 any remaining facts are inserted into the goal verbatim;
   372 
   373 * HOL: local contexts (aka cases) may now contain term bindings as
   374 well; the 'cases' and 'induct' methods new provide a ?case binding for
   375 the result to be shown in each case;
   376 
   377 * HOL: added 'recdef_tc' command;
   378 
   379 * isatool convert assists in eliminating legacy ML scripts;
   380 
   381 
   382 *** HOL ***
   383 
   384 * HOL/Library: a collection of generic theories to be used together
   385 with main HOL; the theory loader path already includes this directory
   386 by default; the following existing theories have been moved here:
   387 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
   388 (as While_Combinator), HOL/Lex/Prefix (as List_Prefix);
   389 
   390 * HOL/Unix: "Some aspects of Unix file-system security", a typical
   391 modelling and verification task performed in Isabelle/HOL +
   392 Isabelle/Isar + Isabelle document preparation (by Markus Wenzel).
   393 
   394 * HOL/Algebra: special summation operator SUM no longer exists, it has
   395 been replaced by setsum; infix 'assoc' now has priority 50 (like
   396 'dvd'); axiom 'one_not_zero' has been moved from axclass 'ring' to
   397 'domain', this makes the theory consistent with mathematical
   398 literature;
   399 
   400 * HOL basics: added overloaded operations "inverse" and "divide"
   401 (infix "/"), syntax for generic "abs" operation, generic summation
   402 operator \<Sum>;
   403 
   404 * HOL/typedef: simplified package, provide more useful rules (see also
   405 HOL/subset.thy);
   406 
   407 * HOL/datatype: induction rule for arbitrarily branching datatypes is
   408 now expressed as a proper nested rule (old-style tactic scripts may
   409 require atomize_strip_tac to cope with non-atomic premises);
   410 
   411 * HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule
   412 to "split_conv" (old name still available for compatibility);
   413 
   414 * HOL: improved concrete syntax for strings (e.g. allows translation
   415 rules with string literals);
   416 
   417 * HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals
   418 and Fleuriot's mechanization of analysis;
   419 
   420 * HOL/Real, HOL/Hyperreal: improved arithmetic simplification;
   421 
   422 
   423 *** CTT ***
   424 
   425 * CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that
   426 "lam" is displayed as TWO lambda-symbols
   427 
   428 * CTT: theory Main now available, containing everything (that is, Bool
   429 and Arith);
   430 
   431 
   432 *** General ***
   433 
   434 * Pure: the Simplifier has been implemented properly as a derived rule
   435 outside of the actual kernel (at last!); the overall performance
   436 penalty in practical applications is about 50%, while reliability of
   437 the Isabelle inference kernel has been greatly improved;
   438 
   439 * print modes "brackets" and "no_brackets" control output of nested =>
   440 (types) and ==> (props); the default behaviour is "brackets";
   441 
   442 * Provers: fast_tac (and friends) now handle actual object-logic rules
   443 as assumptions as well;
   444 
   445 * system: support Poly/ML 4.0;
   446 
   447 * system: isatool install handles KDE version 1 or 2;
   448 
   449 
   450 
   451 New in Isabelle99-1 (October 2000)
   452 ----------------------------------
   453 
   454 *** Overview of INCOMPATIBILITIES ***
   455 
   456 * HOL: simplification of natural numbers is much changed; to partly
   457 recover the old behaviour (e.g. to prevent n+n rewriting to #2*n)
   458 issue the following ML commands:
   459 
   460   Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
   461   Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
   462 
   463 * HOL: simplification no longer dives into case-expressions; this is
   464 controlled by "t.weak_case_cong" for each datatype t;
   465 
   466 * HOL: nat_less_induct renamed to less_induct;
   467 
   468 * HOL: systematic renaming of the SOME (Eps) rules, may use isatool
   469 fixsome to patch .thy and .ML sources automatically;
   470 
   471   select_equality  -> some_equality
   472   select_eq_Ex     -> some_eq_ex
   473   selectI2EX       -> someI2_ex
   474   selectI2         -> someI2
   475   selectI          -> someI
   476   select1_equality -> some1_equality
   477   Eps_sym_eq       -> some_sym_eq_trivial
   478   Eps_eq           -> some_eq_trivial
   479 
   480 * HOL: exhaust_tac on datatypes superceded by new generic case_tac;
   481 
   482 * HOL: removed obsolete theorem binding expand_if (refer to split_if
   483 instead);
   484 
   485 * HOL: the recursion equations generated by 'recdef' are now called
   486 f.simps instead of f.rules;
   487 
   488 * HOL: qed_spec_mp now also handles bounded ALL as well;
   489 
   490 * HOL: 0 is now overloaded, so the type constraint ":: nat" may
   491 sometimes be needed;
   492 
   493 * HOL: the constant for "f``x" is now "image" rather than "op ``";
   494 
   495 * HOL: the constant for "f-``x" is now "vimage" rather than "op -``";
   496 
   497 * HOL: the disjoint sum is now "<+>" instead of "Plus"; the cartesian
   498 product is now "<*>" instead of "Times"; the lexicographic product is
   499 now "<*lex*>" instead of "**";
   500 
   501 * HOL: theory Sexp is now in HOL/Induct examples (it used to be part
   502 of main HOL, but was unused); better use HOL's datatype package;
   503 
   504 * HOL: removed "symbols" syntax for constant "override" of theory Map;
   505 the old syntax may be recovered as follows:
   506 
   507   syntax (symbols)
   508     override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
   509       (infixl "\\<oplus>" 100)
   510 
   511 * HOL/Real: "rabs" replaced by overloaded "abs" function;
   512 
   513 * HOL/ML: even fewer consts are declared as global (see theories Ord,
   514 Lfp, Gfp, WF); this only affects ML packages that refer to const names
   515 internally;
   516 
   517 * HOL and ZF: syntax for quotienting wrt an equivalence relation
   518 changed from A/r to A//r;
   519 
   520 * ZF: new treatment of arithmetic (nat & int) may break some old
   521 proofs;
   522 
   523 * Isar: renamed some attributes (RS -> THEN, simplify -> simplified,
   524 rulify -> rule_format, elimify -> elim_format, ...);
   525 
   526 * Isar/Provers: intro/elim/dest attributes changed; renamed
   527 intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one
   528 should have to change intro!! to intro? only); replaced "delrule" by
   529 "rule del";
   530 
   531 * Isar/HOL: renamed "intrs" to "intros" in inductive definitions;
   532 
   533 * Provers: strengthened force_tac by using new first_best_tac;
   534 
   535 * LaTeX document preparation: several changes of isabelle.sty (see
   536 lib/texinputs);
   537 
   538 
   539 *** Document preparation ***
   540 
   541 * formal comments (text blocks etc.) in new-style theories may now
   542 contain antiquotations of thm/prop/term/typ/text to be presented
   543 according to latex print mode; concrete syntax is like this:
   544 @{term[show_types] "f(x) = a + x"};
   545 
   546 * isatool mkdir provides easy setup of Isabelle session directories,
   547 including proper document sources;
   548 
   549 * generated LaTeX sources are now deleted after successful run
   550 (isatool document -c); may retain a copy somewhere else via -D option
   551 of isatool usedir;
   552 
   553 * isatool usedir -D now lets isatool latex -o sty update the Isabelle
   554 style files, achieving self-contained LaTeX sources and simplifying
   555 LaTeX debugging;
   556 
   557 * old-style theories now produce (crude) LaTeX output as well;
   558 
   559 * browser info session directories are now self-contained (may be put
   560 on WWW server seperately); improved graphs of nested sessions; removed
   561 graph for 'all sessions';
   562 
   563 * several improvements in isabelle style files; \isabellestyle{it}
   564 produces fake math mode output; \isamarkupheader is now \section by
   565 default; see lib/texinputs/isabelle.sty etc.;
   566 
   567 
   568 *** Isar ***
   569 
   570 * Isar/Pure: local results and corresponding term bindings are now
   571 subject to Hindley-Milner polymorphism (similar to ML); this
   572 accommodates incremental type-inference very nicely;
   573 
   574 * Isar/Pure: new derived language element 'obtain' supports
   575 generalized existence reasoning;
   576 
   577 * Isar/Pure: new calculational elements 'moreover' and 'ultimately'
   578 support accumulation of results, without applying any rules yet;
   579 useful to collect intermediate results without explicit name
   580 references, and for use with transitivity rules with more than 2
   581 premises;
   582 
   583 * Isar/Pure: scalable support for case-analysis type proofs: new
   584 'case' language element refers to local contexts symbolically, as
   585 produced by certain proof methods; internally, case names are attached
   586 to theorems as "tags";
   587 
   588 * Isar/Pure: theory command 'hide' removes declarations from
   589 class/type/const name spaces;
   590 
   591 * Isar/Pure: theory command 'defs' supports option "(overloaded)" to
   592 indicate potential overloading;
   593 
   594 * Isar/Pure: changed syntax of local blocks from {{ }} to { };
   595 
   596 * Isar/Pure: syntax of sorts made 'inner', i.e. have to write
   597 "{a,b,c}" instead of {a,b,c};
   598 
   599 * Isar/Pure now provides its own version of intro/elim/dest
   600 attributes; useful for building new logics, but beware of confusion
   601 with the version in Provers/classical;
   602 
   603 * Isar/Pure: the local context of (non-atomic) goals is provided via
   604 case name 'antecedent';
   605 
   606 * Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms
   607 to the current context is now done automatically);
   608 
   609 * Isar/Pure: theory command 'method_setup' provides a simple interface
   610 for definining proof methods in ML;
   611 
   612 * Isar/Provers: intro/elim/dest attributes changed; renamed
   613 intro/intro!/intro!! flags to intro!/intro/intro? (INCOMPATIBILITY, in
   614 most cases, one should have to change intro!! to intro? only);
   615 replaced "delrule" by "rule del";
   616 
   617 * Isar/Provers: new 'hypsubst' method, plain 'subst' method and
   618 'symmetric' attribute (the latter supercedes [RS sym]);
   619 
   620 * Isar/Provers: splitter support (via 'split' attribute and 'simp'
   621 method modifier); 'simp' method: 'only:' modifier removes loopers as
   622 well (including splits);
   623 
   624 * Isar/Provers: Simplifier and Classical methods now support all kind
   625 of modifiers used in the past, including 'cong', 'iff', etc.
   626 
   627 * Isar/Provers: added 'fastsimp' and 'clarsimp' methods (combination
   628 of Simplifier and Classical reasoner);
   629 
   630 * Isar/HOL: new proof method 'cases' and improved version of 'induct'
   631 now support named cases; major packages (inductive, datatype, primrec,
   632 recdef) support case names and properly name parameters;
   633 
   634 * Isar/HOL: new transitivity rules for substitution in inequalities --
   635 monotonicity conditions are extracted to be proven at end of
   636 calculations;
   637 
   638 * Isar/HOL: removed 'case_split' thm binding, should use 'cases' proof
   639 method anyway;
   640 
   641 * Isar/HOL: removed old expand_if = split_if; theorems if_splits =
   642 split_if split_if_asm; datatype package provides theorems foo.splits =
   643 foo.split foo.split_asm for each datatype;
   644 
   645 * Isar/HOL: tuned inductive package, rename "intrs" to "intros"
   646 (potential INCOMPATIBILITY), emulation of mk_cases feature for proof
   647 scripts: new 'inductive_cases' command and 'ind_cases' method; (Note:
   648 use "(cases (simplified))" method in proper proof texts);
   649 
   650 * Isar/HOL: added global 'arith_split' attribute for 'arith' method;
   651 
   652 * Isar: names of theorems etc. may be natural numbers as well;
   653 
   654 * Isar: 'pr' command: optional arguments for goals_limit and
   655 ProofContext.prems_limit; no longer prints theory contexts, but only
   656 proof states;
   657 
   658 * Isar: diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit
   659 additional print modes to be specified; e.g. "pr(latex)" will print
   660 proof state according to the Isabelle LaTeX style;
   661 
   662 * Isar: improved support for emulating tactic scripts, including proof
   663 methods 'rule_tac' etc., 'cut_tac', 'thin_tac', 'subgoal_tac',
   664 'rename_tac', 'rotate_tac', 'tactic', and 'case_tac' / 'induct_tac'
   665 (for HOL datatypes);
   666 
   667 * Isar: simplified (more robust) goal selection of proof methods: 1st
   668 goal, all goals, or explicit goal specifier (tactic emulation); thus
   669 'proof method scripts' have to be in depth-first order;
   670 
   671 * Isar: tuned 'let' syntax: replaced 'as' keyword by 'and';
   672 
   673 * Isar: removed 'help' command, which hasn't been too helpful anyway;
   674 should instead use individual commands for printing items
   675 (print_commands, print_methods etc.);
   676 
   677 * Isar: added 'nothing' --- the empty list of theorems;
   678 
   679 
   680 *** HOL ***
   681 
   682 * HOL/MicroJava: formalization of a fragment of Java, together with a
   683 corresponding virtual machine and a specification of its bytecode
   684 verifier and a lightweight bytecode verifier, including proofs of
   685 type-safety; by Gerwin Klein, Tobias Nipkow, David von Oheimb, and
   686 Cornelia Pusch (see also the homepage of project Bali at
   687 http://isabelle.in.tum.de/Bali/);
   688 
   689 * HOL/Algebra: new theory of rings and univariate polynomials, by
   690 Clemens Ballarin;
   691 
   692 * HOL/NumberTheory: fundamental Theorem of Arithmetic, Chinese
   693 Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, by Thomas M
   694 Rasmussen;
   695 
   696 * HOL/Lattice: fundamental concepts of lattice theory and order
   697 structures, including duals, properties of bounds versus algebraic
   698 laws, lattice operations versus set-theoretic ones, the Knaster-Tarski
   699 Theorem for complete lattices etc.; may also serve as a demonstration
   700 for abstract algebraic reasoning using axiomatic type classes, and
   701 mathematics-style proof in Isabelle/Isar; by Markus Wenzel;
   702 
   703 * HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog, by David
   704 von Oheimb;
   705 
   706 * HOL/IMPP: extension of IMP with local variables and mutually
   707 recursive procedures, by David von Oheimb;
   708 
   709 * HOL/Lambda: converted into new-style theory and document;
   710 
   711 * HOL/ex/Multiquote: example of multiple nested quotations and
   712 anti-quotations -- basically a generalized version of de-Bruijn
   713 representation; very useful in avoiding lifting of operations;
   714 
   715 * HOL/record: added general record equality rule to simpset; fixed
   716 select-update simplification procedure to handle extended records as
   717 well; admit "r" as field name;
   718 
   719 * HOL: 0 is now overloaded over the new sort "zero", allowing its use with
   720 other numeric types and also as the identity of groups, rings, etc.;
   721 
   722 * HOL: new axclass plus_ac0 for addition with the AC-laws and 0 as identity.
   723 Types nat and int belong to this axclass;
   724 
   725 * HOL: greatly improved simplification involving numerals of type nat, int, real:
   726    (i + #8 + j) = Suc k simplifies to  #7 + (i + j) = k
   727    i*j + k + j*#3*i     simplifies to  #4*(i*j) + k
   728   two terms #m*u and #n*u are replaced by #(m+n)*u
   729     (where #m, #n and u can implicitly be 1; this is simproc combine_numerals)
   730   and the term/formula #m*u+x ~~ #n*u+y simplifies simplifies to #(m-n)+x ~~ y
   731     or x ~~ #(n-m)+y, where ~~ is one of = < <= or - (simproc cancel_numerals);
   732 
   733 * HOL: meson_tac is available (previously in ex/meson.ML); it is a
   734 powerful prover for predicate logic but knows nothing of clasets; see
   735 ex/mesontest.ML and ex/mesontest2.ML for example applications;
   736 
   737 * HOL: new version of "case_tac" subsumes both boolean case split and
   738 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
   739 exists, may define val exhaust_tac = case_tac for ad-hoc portability;
   740 
   741 * HOL: simplification no longer dives into case-expressions: only the
   742 selector expression is simplified, but not the remaining arms; to
   743 enable full simplification of case-expressions for datatype t, you may
   744 remove t.weak_case_cong from the simpset, either globally (Delcongs
   745 [thm"t.weak_case_cong"];) or locally (delcongs [...]).
   746 
   747 * HOL/recdef: the recursion equations generated by 'recdef' for
   748 function 'f' are now called f.simps instead of f.rules; if all
   749 termination conditions are proved automatically, these simplification
   750 rules are added to the simpset, as in primrec; rules may be named
   751 individually as well, resulting in a separate list of theorems for
   752 each equation;
   753 
   754 * HOL/While is a new theory that provides a while-combinator. It
   755 permits the definition of tail-recursive functions without the
   756 provision of a termination measure. The latter is necessary once the
   757 invariant proof rule for while is applied.
   758 
   759 * HOL: new (overloaded) notation for the set of elements below/above
   760 some element: {..u}, {..u(}, {l..}, {)l..}. See theory SetInterval.
   761 
   762 * HOL: theorems impI, allI, ballI bound as "strip";
   763 
   764 * HOL: new tactic induct_thm_tac: thm -> string -> int -> tactic
   765 induct_tac th "x1 ... xn" expects th to have a conclusion of the form
   766 P v1 ... vn and abbreviates res_inst_tac [("v1","x1"),...,("vn","xn")] th;
   767 
   768 * HOL/Real: "rabs" replaced by overloaded "abs" function;
   769 
   770 * HOL: theory Sexp now in HOL/Induct examples (it used to be part of
   771 main HOL, but was unused);
   772 
   773 * HOL: fewer consts declared as global (e.g. have to refer to
   774 "Lfp.lfp" instead of "lfp" internally; affects ML packages only);
   775 
   776 * HOL: tuned AST representation of nested pairs, avoiding bogus output
   777 in case of overlap with user translations (e.g. judgements over
   778 tuples); (note that the underlying logical represenation is still
   779 bogus);
   780 
   781 
   782 *** ZF ***
   783 
   784 * ZF: simplification automatically cancels common terms in arithmetic
   785 expressions over nat and int;
   786 
   787 * ZF: new treatment of nat to minimize type-checking: all operators
   788 coerce their operands to a natural number using the function natify,
   789 making the algebraic laws unconditional;
   790 
   791 * ZF: as above, for int: operators coerce their operands to an integer
   792 using the function intify;
   793 
   794 * ZF: the integer library now contains many of the usual laws for the
   795 orderings, including $<=, and monotonicity laws for $+ and $*;
   796 
   797 * ZF: new example ZF/ex/NatSum to demonstrate integer arithmetic
   798 simplification;
   799 
   800 * FOL and ZF: AddIffs now available, giving theorems of the form P<->Q
   801 to the simplifier and classical reasoner simultaneously;
   802 
   803 
   804 *** General ***
   805 
   806 * Provers: blast_tac now handles actual object-logic rules as
   807 assumptions; note that auto_tac uses blast_tac internally as well;
   808 
   809 * Provers: new functions rulify/rulify_no_asm: thm -> thm for turning
   810 outer -->/All/Ball into ==>/!!; qed_spec_mp now uses rulify_no_asm;
   811 
   812 * Provers: delrules now handles destruct rules as well (no longer need
   813 explicit make_elim);
   814 
   815 * Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g.
   816   [| inj ?f;          ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
   817 use instead the strong form,
   818   [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
   819 in HOL, FOL and ZF the function cla_make_elim will create such rules
   820 from destruct-rules;
   821 
   822 * Provers: Simplifier.easy_setup provides a fast path to basic
   823 Simplifier setup for new object-logics;
   824 
   825 * Pure: AST translation rules no longer require constant head on LHS;
   826 
   827 * Pure: improved name spaces: ambiguous output is qualified; support
   828 for hiding of names;
   829 
   830 * system: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, and
   831 XSYMBOL_HOME; no longer need to do manual configuration in most
   832 situations;
   833 
   834 * system: compression of ML heaps images may now be controlled via -c
   835 option of isabelle and isatool usedir (currently only observed by
   836 Poly/ML);
   837 
   838 * system: isatool installfonts may handle X-Symbol fonts as well (very
   839 useful for remote X11);
   840 
   841 * system: provide TAGS file for Isabelle sources;
   842 
   843 * ML: infix 'OF' is a version of 'MRS' with more appropriate argument
   844 order;
   845 
   846 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
   847 timing flag supersedes proof_timing and Toplevel.trace;
   848 
   849 * ML: new combinators |>> and |>>> for incremental transformations
   850 with secondary results (e.g. certain theory extensions):
   851 
   852 * ML: PureThy.add_defs gets additional argument to indicate potential
   853 overloading (usually false);
   854 
   855 * ML: PureThy.add_thms/add_axioms/add_defs now return theorems as
   856 results;
   857 
   858 
   859 
   860 New in Isabelle99 (October 1999)
   861 --------------------------------
   862 
   863 *** Overview of INCOMPATIBILITIES (see below for more details) ***
   864 
   865 * HOL: The THEN and ELSE parts of conditional expressions (if P then x else y)
   866 are no longer simplified.  (This allows the simplifier to unfold recursive
   867 functional programs.)  To restore the old behaviour, declare
   868 
   869     Delcongs [if_weak_cong];
   870 
   871 * HOL: Removed the obsolete syntax "Compl A"; use -A for set
   872 complement;
   873 
   874 * HOL: the predicate "inj" is now defined by translation to "inj_on";
   875 
   876 * HOL/datatype: mutual_induct_tac no longer exists --
   877   use induct_tac "x_1 ... x_n" instead of mutual_induct_tac ["x_1", ..., "x_n"]
   878 
   879 * HOL/typedef: fixed type inference for representing set; type
   880 arguments now have to occur explicitly on the rhs as type constraints;
   881 
   882 * ZF: The con_defs part of an inductive definition may no longer refer
   883 to constants declared in the same theory;
   884 
   885 * HOL, ZF: the function mk_cases, generated by the inductive
   886 definition package, has lost an argument.  To simplify its result, it
   887 uses the default simpset instead of a supplied list of theorems.
   888 
   889 * HOL/List: the constructors of type list are now Nil and Cons;
   890 
   891 * Simplifier: the type of the infix ML functions
   892         setSSolver addSSolver setSolver addSolver
   893 is now  simpset * solver -> simpset  where `solver' is a new abstract type
   894 for packaging solvers. A solver is created via
   895         mk_solver: string -> (thm list -> int -> tactic) -> solver
   896 where the string argument is only a comment.
   897 
   898 
   899 *** Proof tools ***
   900 
   901 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a
   902 decision procedure for linear arithmetic. Currently it is used for
   903 types `nat', `int', and `real' in HOL (see below); it can, should and
   904 will be instantiated for other types and logics as well.
   905 
   906 * The simplifier now accepts rewrite rules with flexible heads, eg
   907      hom ?f ==> ?f(?x+?y) = ?f ?x + ?f ?y
   908   They are applied like any rule with a non-pattern lhs, i.e. by first-order
   909   matching.
   910 
   911 
   912 *** General ***
   913 
   914 * New Isabelle/Isar subsystem provides an alternative to traditional
   915 tactical theorem proving; together with the ProofGeneral/isar user
   916 interface it offers an interactive environment for developing human
   917 readable proof documents (Isar == Intelligible semi-automated
   918 reasoning); for further information see isatool doc isar-ref,
   919 src/HOL/Isar_examples and http://isabelle.in.tum.de/Isar/
   920 
   921 * improved and simplified presentation of theories: better HTML markup
   922 (including colors), graph views in several sizes; isatool usedir now
   923 provides a proper interface for user theories (via -P option); actual
   924 document preparation based on (PDF)LaTeX is available as well (for
   925 new-style theories only); see isatool doc system for more information;
   926 
   927 * native support for Proof General, both for classic Isabelle and
   928 Isabelle/Isar;
   929 
   930 * ML function thm_deps visualizes dependencies of theorems and lemmas,
   931 using the graph browser tool;
   932 
   933 * Isabelle manuals now also available as PDF;
   934 
   935 * theory loader rewritten from scratch (may not be fully
   936 bug-compatible); old loadpath variable has been replaced by show_path,
   937 add_path, del_path, reset_path functions; new operations such as
   938 update_thy, touch_thy, remove_thy, use/update_thy_only (see also
   939 isatool doc ref);
   940 
   941 * improved isatool install: option -k creates KDE application icon,
   942 option -p DIR installs standalone binaries;
   943 
   944 * added ML_PLATFORM setting (useful for cross-platform installations);
   945 more robust handling of platform specific ML images for SML/NJ;
   946 
   947 * the settings environment is now statically scoped, i.e. it is never
   948 created again in sub-processes invoked from isabelle, isatool, or
   949 Isabelle;
   950 
   951 * path element specification '~~' refers to '$ISABELLE_HOME';
   952 
   953 * in locales, the "assumes" and "defines" parts may be omitted if
   954 empty;
   955 
   956 * new print_mode "xsymbols" for extended symbol support (e.g. genuine
   957 long arrows);
   958 
   959 * new print_mode "HTML";
   960 
   961 * new flag show_tags controls display of tags of theorems (which are
   962 basically just comments that may be attached by some tools);
   963 
   964 * Isamode 2.6 requires patch to accomodate change of Isabelle font
   965 mode and goal output format:
   966 
   967 diff -r Isamode-2.6/elisp/isa-load.el Isamode/elisp/isa-load.el
   968 244c244
   969 <       (list (isa-getenv "ISABELLE") "-msymbols" logic-name)
   970 ---
   971 >       (list (isa-getenv "ISABELLE") "-misabelle_font" "-msymbols" logic-name)
   972 diff -r Isabelle-2.6/elisp/isa-proofstate.el Isamode/elisp/isa-proofstate.el
   973 181c181
   974 < (defconst proofstate-proofstart-regexp "^Level [0-9]+$"
   975 ---
   976 > (defconst proofstate-proofstart-regexp "^Level [0-9]+"
   977 
   978 * function bind_thms stores lists of theorems (cf. bind_thm);
   979 
   980 * new shorthand tactics ftac, eatac, datac, fatac;
   981 
   982 * qed (and friends) now accept "" as result name; in that case the
   983 theorem is not stored, but proper checks and presentation of the
   984 result still apply;
   985 
   986 * theorem database now also indexes constants "Trueprop", "all",
   987 "==>", "=="; thus thms_containing, findI etc. may retrieve more rules;
   988 
   989 
   990 *** HOL ***
   991 
   992 ** HOL arithmetic **
   993 
   994 * There are now decision procedures for linear arithmetic over nat and
   995 int:
   996 
   997 1. arith_tac copes with arbitrary formulae involving `=', `<', `<=',
   998 `+', `-', `Suc', `min', `max' and numerical constants; other subterms
   999 are treated as atomic; subformulae not involving type `nat' or `int'
  1000 are ignored; quantified subformulae are ignored unless they are
  1001 positive universal or negative existential. The tactic has to be
  1002 invoked by hand and can be a little bit slow. In particular, the
  1003 running time is exponential in the number of occurrences of `min' and
  1004 `max', and `-' on `nat'.
  1005 
  1006 2. fast_arith_tac is a cut-down version of arith_tac: it only takes
  1007 (negated) (in)equalities among the premises and the conclusion into
  1008 account (i.e. no compound formulae) and does not know about `min' and
  1009 `max', and `-' on `nat'. It is fast and is used automatically by the
  1010 simplifier.
  1011 
  1012 NB: At the moment, these decision procedures do not cope with mixed
  1013 nat/int formulae where the two parts interact, such as `m < n ==>
  1014 int(m) < int(n)'.
  1015 
  1016 * HOL/Numeral provides a generic theory of numerals (encoded
  1017 efficiently as bit strings); setup for types nat/int/real is in place;
  1018 INCOMPATIBILITY: since numeral syntax is now polymorphic, rather than
  1019 int, existing theories and proof scripts may require a few additional
  1020 type constraints;
  1021 
  1022 * integer division and remainder can now be performed on constant
  1023 arguments;
  1024 
  1025 * many properties of integer multiplication, division and remainder
  1026 are now available;
  1027 
  1028 * An interface to the Stanford Validity Checker (SVC) is available through the
  1029 tactic svc_tac.  Propositional tautologies and theorems of linear arithmetic
  1030 are proved automatically.  SVC must be installed separately, and its results
  1031 must be TAKEN ON TRUST (Isabelle does not check the proofs, but tags any
  1032 invocation of the underlying oracle).  For SVC see
  1033   http://verify.stanford.edu/SVC
  1034 
  1035 * IsaMakefile: the HOL-Real target now builds an actual image;
  1036 
  1037 
  1038 ** HOL misc **
  1039 
  1040 * HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces
  1041 (in Isabelle/Isar) -- by Gertrud Bauer;
  1042 
  1043 * HOL/BCV: generic model of bytecode verification, i.e. data-flow
  1044 analysis for assembly languages with subtypes;
  1045 
  1046 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
  1047 -- avoids syntactic ambiguities and treats state, transition, and
  1048 temporal levels more uniformly; introduces INCOMPATIBILITIES due to
  1049 changed syntax and (many) tactics;
  1050 
  1051 * HOL/inductive: Now also handles more general introduction rules such
  1052   as "ALL y. (y, x) : r --> y : acc r ==> x : acc r"; monotonicity
  1053   theorems are now maintained within the theory (maintained via the
  1054   "mono" attribute);
  1055 
  1056 * HOL/datatype: Now also handles arbitrarily branching datatypes
  1057   (using function types) such as
  1058 
  1059   datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
  1060 
  1061 * HOL/record: record_simproc (part of the default simpset) takes care
  1062 of selectors applied to updated records; record_split_tac is no longer
  1063 part of the default claset; update_defs may now be removed from the
  1064 simpset in many cases; COMPATIBILITY: old behavior achieved by
  1065 
  1066   claset_ref () := claset() addSWrapper record_split_wrapper;
  1067   Delsimprocs [record_simproc]
  1068 
  1069 * HOL/typedef: fixed type inference for representing set; type
  1070 arguments now have to occur explicitly on the rhs as type constraints;
  1071 
  1072 * HOL/recdef (TFL): 'congs' syntax now expects comma separated list of theorem
  1073 names rather than an ML expression;
  1074 
  1075 * HOL/defer_recdef (TFL): like recdef but the well-founded relation can be
  1076 supplied later.  Program schemes can be defined, such as
  1077     "While B C s = (if B s then While B C (C s) else s)"
  1078 where the well-founded relation can be chosen after B and C have been given.
  1079 
  1080 * HOL/List: the constructors of type list are now Nil and Cons;
  1081 INCOMPATIBILITY: while [] and infix # syntax is still there, of
  1082 course, ML tools referring to List.list.op # etc. have to be adapted;
  1083 
  1084 * HOL_quantifiers flag superseded by "HOL" print mode, which is
  1085 disabled by default; run isabelle with option -m HOL to get back to
  1086 the original Gordon/HOL-style output;
  1087 
  1088 * HOL/Ord.thy: new bounded quantifier syntax (input only): ALL x<y. P,
  1089 ALL x<=y. P, EX x<y. P, EX x<=y. P;
  1090 
  1091 * HOL basic syntax simplified (more orthogonal): all variants of
  1092 All/Ex now support plain / symbolic / HOL notation; plain syntax for
  1093 Eps operator is provided as well: "SOME x. P[x]";
  1094 
  1095 * HOL/Sum.thy: sum_case has been moved to HOL/Datatype;
  1096 
  1097 * HOL/Univ.thy: infix syntax <*>, <+>, <**>, <+> eliminated and made
  1098 thus available for user theories;
  1099 
  1100 * HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with
  1101 HOL/List; hardly an INCOMPATIBILITY since '>>' syntax is used all the
  1102 time;
  1103 
  1104 * HOL: new tactic smp_tac: int -> int -> tactic, which applies spec
  1105 several times and then mp;
  1106 
  1107 
  1108 *** LK ***
  1109 
  1110 * the notation <<...>> is now available as a notation for sequences of
  1111 formulas;
  1112 
  1113 * the simplifier is now installed
  1114 
  1115 * the axiom system has been generalized (thanks to Soren Heilmann)
  1116 
  1117 * the classical reasoner now has a default rule database
  1118 
  1119 
  1120 *** ZF ***
  1121 
  1122 * new primrec section allows primitive recursive functions to be given
  1123 directly (as in HOL) over datatypes and the natural numbers;
  1124 
  1125 * new tactics induct_tac and exhaust_tac for induction (or case
  1126 analysis) over datatypes and the natural numbers;
  1127 
  1128 * the datatype declaration of type T now defines the recursor T_rec;
  1129 
  1130 * simplification automatically does freeness reasoning for datatype
  1131 constructors;
  1132 
  1133 * automatic type-inference, with AddTCs command to insert new
  1134 type-checking rules;
  1135 
  1136 * datatype introduction rules are now added as Safe Introduction rules
  1137 to the claset;
  1138 
  1139 * the syntax "if P then x else y" is now available in addition to
  1140 if(P,x,y);
  1141 
  1142 
  1143 *** Internal programming interfaces ***
  1144 
  1145 * tuned simplifier trace output; new flag debug_simp;
  1146 
  1147 * structures Vartab / Termtab (instances of TableFun) offer efficient
  1148 tables indexed by indexname_ord / term_ord (compatible with aconv);
  1149 
  1150 * AxClass.axclass_tac lost the theory argument;
  1151 
  1152 * tuned current_goals_markers semantics: begin / end goal avoids
  1153 printing empty lines;
  1154 
  1155 * removed prs and prs_fn hook, which was broken because it did not
  1156 include \n in its semantics, forcing writeln to add one
  1157 uncoditionally; replaced prs_fn by writeln_fn; consider std_output:
  1158 string -> unit if you really want to output text without newline;
  1159 
  1160 * Symbol.output subject to print mode; INCOMPATIBILITY: defaults to
  1161 plain output, interface builders may have to enable 'isabelle_font'
  1162 mode to get Isabelle font glyphs as before;
  1163 
  1164 * refined token_translation interface; INCOMPATIBILITY: output length
  1165 now of type real instead of int;
  1166 
  1167 * theory loader actions may be traced via new ThyInfo.add_hook
  1168 interface (see src/Pure/Thy/thy_info.ML); example application: keep
  1169 your own database of information attached to *whole* theories -- as
  1170 opposed to intra-theory data slots offered via TheoryDataFun;
  1171 
  1172 * proper handling of dangling sort hypotheses (at last!);
  1173 Thm.strip_shyps and Drule.strip_shyps_warning take care of removing
  1174 extra sort hypotheses that can be witnessed from the type signature;
  1175 the force_strip_shyps flag is gone, any remaining shyps are simply
  1176 left in the theorem (with a warning issued by strip_shyps_warning);
  1177 
  1178 
  1179 
  1180 New in Isabelle98-1 (October 1998)
  1181 ----------------------------------
  1182 
  1183 *** Overview of INCOMPATIBILITIES (see below for more details) ***
  1184 
  1185 * several changes of automated proof tools;
  1186 
  1187 * HOL: major changes to the inductive and datatype packages, including
  1188 some minor incompatibilities of theory syntax;
  1189 
  1190 * HOL: renamed r^-1 to 'converse' from 'inverse'; 'inj_onto' is now
  1191 called `inj_on';
  1192 
  1193 * HOL: removed duplicate thms in Arith:
  1194   less_imp_add_less  should be replaced by  trans_less_add1
  1195   le_imp_add_le      should be replaced by  trans_le_add1
  1196 
  1197 * HOL: unary minus is now overloaded (new type constraints may be
  1198 required);
  1199 
  1200 * HOL and ZF: unary minus for integers is now #- instead of #~.  In
  1201 ZF, expressions such as n#-1 must be changed to n#- 1, since #-1 is
  1202 now taken as an integer constant.
  1203 
  1204 * Pure: ML function 'theory_of' renamed to 'theory';
  1205 
  1206 
  1207 *** Proof tools ***
  1208 
  1209 * Simplifier:
  1210   1. Asm_full_simp_tac is now more aggressive.
  1211      1. It will sometimes reorient premises if that increases their power to
  1212         simplify.
  1213      2. It does no longer proceed strictly from left to right but may also
  1214         rotate premises to achieve further simplification.
  1215      For compatibility reasons there is now Asm_lr_simp_tac which is like the
  1216      old Asm_full_simp_tac in that it does not rotate premises.
  1217   2. The simplifier now knows a little bit about nat-arithmetic.
  1218 
  1219 * Classical reasoner: wrapper mechanism for the classical reasoner now
  1220 allows for selected deletion of wrappers, by introduction of names for
  1221 wrapper functionals.  This implies that addbefore, addSbefore,
  1222 addaltern, and addSaltern now take a pair (name, tactic) as argument,
  1223 and that adding two tactics with the same name overwrites the first
  1224 one (emitting a warning).
  1225   type wrapper = (int -> tactic) -> (int -> tactic)
  1226   setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by
  1227   addWrapper, addSWrapper: claset * (string * wrapper) -> claset
  1228   delWrapper, delSWrapper: claset *  string            -> claset
  1229   getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
  1230 
  1231 * Classical reasoner: addbefore/addSbefore now have APPEND/ORELSE
  1232 semantics; addbefore now affects only the unsafe part of step_tac
  1233 etc.; this affects addss/auto_tac/force_tac, so EXISTING PROOFS MAY
  1234 FAIL, but proofs should be fixable easily, e.g. by replacing Auto_tac
  1235 by Force_tac;
  1236 
  1237 * Classical reasoner: setwrapper to setWrapper and compwrapper to
  1238 compWrapper; added safe wrapper (and access functions for it);
  1239 
  1240 * HOL/split_all_tac is now much faster and fails if there is nothing
  1241 to split.  Some EXISTING PROOFS MAY REQUIRE ADAPTION because the order
  1242 and the names of the automatically generated variables have changed.
  1243 split_all_tac has moved within claset() from unsafe wrappers to safe
  1244 wrappers, which means that !!-bound variables are split much more
  1245 aggressively, and safe_tac and clarify_tac now split such variables.
  1246 If this splitting is not appropriate, use delSWrapper "split_all_tac".
  1247 Note: the same holds for record_split_tac, which does the job of
  1248 split_all_tac for record fields.
  1249 
  1250 * HOL/Simplifier: Rewrite rules for case distinctions can now be added
  1251 permanently to the default simpset using Addsplits just like
  1252 Addsimps. They can be removed via Delsplits just like
  1253 Delsimps. Lower-case versions are also available.
  1254 
  1255 * HOL/Simplifier: The rule split_if is now part of the default
  1256 simpset. This means that the simplifier will eliminate all occurrences
  1257 of if-then-else in the conclusion of a goal. To prevent this, you can
  1258 either remove split_if completely from the default simpset by
  1259 `Delsplits [split_if]' or remove it in a specific call of the
  1260 simplifier using `... delsplits [split_if]'.  You can also add/delete
  1261 other case splitting rules to/from the default simpset: every datatype
  1262 generates suitable rules `split_t_case' and `split_t_case_asm' (where
  1263 t is the name of the datatype).
  1264 
  1265 * Classical reasoner / Simplifier combination: new force_tac (and
  1266 derivatives Force_tac, force) combines rewriting and classical
  1267 reasoning (and whatever other tools) similarly to auto_tac, but is
  1268 aimed to solve the given subgoal completely.
  1269 
  1270 
  1271 *** General ***
  1272 
  1273 * new top-level commands `Goal' and `Goalw' that improve upon `goal'
  1274 and `goalw': the theory is no longer needed as an explicit argument -
  1275 the current theory context is used; assumptions are no longer returned
  1276 at the ML-level unless one of them starts with ==> or !!; it is
  1277 recommended to convert to these new commands using isatool fixgoal
  1278 (backup your sources first!);
  1279 
  1280 * new top-level commands 'thm' and 'thms' for retrieving theorems from
  1281 the current theory context, and 'theory' to lookup stored theories;
  1282 
  1283 * new theory section 'locale' for declaring constants, assumptions and
  1284 definitions that have local scope;
  1285 
  1286 * new theory section 'nonterminals' for purely syntactic types;
  1287 
  1288 * new theory section 'setup' for generic ML setup functions
  1289 (e.g. package initialization);
  1290 
  1291 * the distribution now includes Isabelle icons: see
  1292 lib/logo/isabelle-{small,tiny}.xpm;
  1293 
  1294 * isatool install - install binaries with absolute references to
  1295 ISABELLE_HOME/bin;
  1296 
  1297 * isatool logo -- create instances of the Isabelle logo (as EPS);
  1298 
  1299 * print mode 'emacs' reserved for Isamode;
  1300 
  1301 * support multiple print (ast) translations per constant name;
  1302 
  1303 * theorems involving oracles are now printed with a suffixed [!];
  1304 
  1305 
  1306 *** HOL ***
  1307 
  1308 * there is now a tutorial on Isabelle/HOL (do 'isatool doc tutorial');
  1309 
  1310 * HOL/inductive package reorganized and improved: now supports mutual
  1311 definitions such as
  1312 
  1313   inductive EVEN ODD
  1314     intrs
  1315       null "0 : EVEN"
  1316       oddI "n : EVEN ==> Suc n : ODD"
  1317       evenI "n : ODD ==> Suc n : EVEN"
  1318 
  1319 new theorem list "elims" contains an elimination rule for each of the
  1320 recursive sets; inductive definitions now handle disjunctive premises
  1321 correctly (also ZF);
  1322 
  1323 INCOMPATIBILITIES: requires Inductive as an ancestor; component
  1324 "mutual_induct" no longer exists - the induction rule is always
  1325 contained in "induct";
  1326 
  1327 
  1328 * HOL/datatype package re-implemented and greatly improved: now
  1329 supports mutually recursive datatypes such as
  1330 
  1331   datatype
  1332     'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp)
  1333             | SUM ('a aexp) ('a aexp)
  1334             | DIFF ('a aexp) ('a aexp)
  1335             | NUM 'a
  1336   and
  1337     'a bexp = LESS ('a aexp) ('a aexp)
  1338             | AND ('a bexp) ('a bexp)
  1339             | OR ('a bexp) ('a bexp)
  1340 
  1341 as well as indirectly recursive datatypes such as
  1342 
  1343   datatype
  1344     ('a, 'b) term = Var 'a
  1345                   | App 'b ((('a, 'b) term) list)
  1346 
  1347 The new tactic  mutual_induct_tac [<var_1>, ..., <var_n>] i  performs
  1348 induction on mutually / indirectly recursive datatypes.
  1349 
  1350 Primrec equations are now stored in theory and can be accessed via
  1351 <function_name>.simps.
  1352 
  1353 INCOMPATIBILITIES:
  1354 
  1355   - Theories using datatypes must now have theory Datatype as an
  1356     ancestor.
  1357   - The specific <typename>.induct_tac no longer exists - use the
  1358     generic induct_tac instead.
  1359   - natE has been renamed to nat.exhaust - use exhaust_tac
  1360     instead of res_inst_tac ... natE. Note that the variable
  1361     names in nat.exhaust differ from the names in natE, this
  1362     may cause some "fragile" proofs to fail.
  1363   - The theorems split_<typename>_case and split_<typename>_case_asm
  1364     have been renamed to <typename>.split and <typename>.split_asm.
  1365   - Since default sorts of type variables are now handled correctly,
  1366     some datatype definitions may have to be annotated with explicit
  1367     sort constraints.
  1368   - Primrec definitions no longer require function name and type
  1369     of recursive argument.
  1370 
  1371 Consider using isatool fixdatatype to adapt your theories and proof
  1372 scripts to the new package (backup your sources first!).
  1373 
  1374 
  1375 * HOL/record package: considerably improved implementation; now
  1376 includes concrete syntax for record types, terms, updates; theorems
  1377 for surjective pairing and splitting !!-bound record variables; proof
  1378 support is as follows:
  1379 
  1380   1) standard conversions (selectors or updates applied to record
  1381 constructor terms) are part of the standard simpset;
  1382 
  1383   2) inject equations of the form ((x, y) = (x', y')) == x=x' & y=y' are
  1384 made part of standard simpset and claset via addIffs;
  1385 
  1386   3) a tactic for record field splitting (record_split_tac) is part of
  1387 the standard claset (addSWrapper);
  1388 
  1389 To get a better idea about these rules you may retrieve them via
  1390 something like 'thms "foo.simps"' or 'thms "foo.iffs"', where "foo" is
  1391 the name of your record type.
  1392 
  1393 The split tactic 3) conceptually simplifies by the following rule:
  1394 
  1395   "(!!x. PROP ?P x) == (!!a b. PROP ?P (a, b))"
  1396 
  1397 Thus any record variable that is bound by meta-all will automatically
  1398 blow up into some record constructor term, consequently the
  1399 simplifications of 1), 2) apply.  Thus force_tac, auto_tac etc. shall
  1400 solve record problems automatically.
  1401 
  1402 
  1403 * reorganized the main HOL image: HOL/Integ and String loaded by
  1404 default; theory Main includes everything;
  1405 
  1406 * automatic simplification of integer sums and comparisons, using cancellation;
  1407 
  1408 * added option_map_eq_Some and not_Some_eq to the default simpset and claset;
  1409 
  1410 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset;
  1411 
  1412 * many new identities for unions, intersections, set difference, etc.;
  1413 
  1414 * expand_if, expand_split, expand_sum_case and expand_nat_case are now
  1415 called split_if, split_split, split_sum_case and split_nat_case (to go
  1416 with add/delsplits);
  1417 
  1418 * HOL/Prod introduces simplification procedure unit_eq_proc rewriting
  1419 (?x::unit) = (); this is made part of the default simpset, which COULD
  1420 MAKE EXISTING PROOFS FAIL under rare circumstances (consider
  1421 'Delsimprocs [unit_eq_proc];' as last resort); also note that
  1422 unit_abs_eta_conv is added in order to counter the effect of
  1423 unit_eq_proc on (%u::unit. f u), replacing it by f rather than by
  1424 %u.f();
  1425 
  1426 * HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which
  1427 makes more sense);
  1428 
  1429 * HOL/Set INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
  1430   It and 'sym RS equals0D' are now in the default  claset, giving automatic
  1431   disjointness reasoning but breaking a few old proofs.
  1432 
  1433 * HOL/Relation INCOMPATIBILITY: renamed the relational operator r^-1
  1434 to 'converse' from 'inverse' (for compatibility with ZF and some
  1435 literature);
  1436 
  1437 * HOL/recdef can now declare non-recursive functions, with {} supplied as
  1438 the well-founded relation;
  1439 
  1440 * HOL/Set INCOMPATIBILITY: the complement of set A is now written -A instead of
  1441     Compl A.  The "Compl" syntax remains available as input syntax for this
  1442     release ONLY.
  1443 
  1444 * HOL/Update: new theory of function updates:
  1445     f(a:=b) == %x. if x=a then b else f x
  1446 may also be iterated as in f(a:=b,c:=d,...);
  1447 
  1448 * HOL/Vimage: new theory for inverse image of a function, syntax f-``B;
  1449 
  1450 * HOL/List:
  1451   - new function list_update written xs[i:=v] that updates the i-th
  1452     list position. May also be iterated as in xs[i:=a,j:=b,...].
  1453   - new function `upt' written [i..j(] which generates the list
  1454     [i,i+1,...,j-1], i.e. the upper bound is excluded. To include the upper
  1455     bound write [i..j], which is a shorthand for [i..j+1(].
  1456   - new lexicographic orderings and corresponding wellfoundedness theorems.
  1457 
  1458 * HOL/Arith:
  1459   - removed 'pred' (predecessor) function;
  1460   - generalized some theorems about n-1;
  1461   - many new laws about "div" and "mod";
  1462   - new laws about greatest common divisors (see theory ex/Primes);
  1463 
  1464 * HOL/Relation: renamed the relational operator r^-1 "converse"
  1465 instead of "inverse";
  1466 
  1467 * HOL/Induct/Multiset: a theory of multisets, including the wellfoundedness
  1468   of the multiset ordering;
  1469 
  1470 * directory HOL/Real: a construction of the reals using Dedekind cuts
  1471   (not included by default);
  1472 
  1473 * directory HOL/UNITY: Chandy and Misra's UNITY formalism;
  1474 
  1475 * directory HOL/Hoare: a new version of Hoare logic which permits many-sorted
  1476   programs, i.e. different program variables may have different types.
  1477 
  1478 * calling (stac rew i) now fails if "rew" has no effect on the goal
  1479   [previously, this check worked only if the rewrite rule was unconditional]
  1480   Now rew can involve either definitions or equalities (either == or =).
  1481 
  1482 
  1483 *** ZF ***
  1484 
  1485 * theory Main includes everything; INCOMPATIBILITY: theory ZF.thy contains
  1486   only the theorems proved on ZF.ML;
  1487 
  1488 * ZF INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
  1489   It and 'sym RS equals0D' are now in the default  claset, giving automatic
  1490   disjointness reasoning but breaking a few old proofs.
  1491 
  1492 * ZF/Update: new theory of function updates
  1493     with default rewrite rule  f(x:=y) ` z = if(z=x, y, f`z)
  1494   may also be iterated as in f(a:=b,c:=d,...);
  1495 
  1496 * in  let x=t in u(x), neither t nor u(x) has to be an FOL term.
  1497 
  1498 * calling (stac rew i) now fails if "rew" has no effect on the goal
  1499   [previously, this check worked only if the rewrite rule was unconditional]
  1500   Now rew can involve either definitions or equalities (either == or =).
  1501 
  1502 * case_tac provided for compatibility with HOL
  1503     (like the old excluded_middle_tac, but with subgoals swapped)
  1504 
  1505 
  1506 *** Internal programming interfaces ***
  1507 
  1508 * Pure: several new basic modules made available for general use, see
  1509 also src/Pure/README;
  1510 
  1511 * improved the theory data mechanism to support encapsulation (data
  1512 kind name replaced by private Object.kind, acting as authorization
  1513 key); new type-safe user interface via functor TheoryDataFun; generic
  1514 print_data function becomes basically useless;
  1515 
  1516 * removed global_names compatibility flag -- all theory declarations
  1517 are qualified by default;
  1518 
  1519 * module Pure/Syntax now offers quote / antiquote translation
  1520 functions (useful for Hoare logic etc. with implicit dependencies);
  1521 see HOL/ex/Antiquote for an example use;
  1522 
  1523 * Simplifier now offers conversions (asm_)(full_)rewrite: simpset ->
  1524 cterm -> thm;
  1525 
  1526 * new tactical CHANGED_GOAL for checking that a tactic modifies a
  1527 subgoal;
  1528 
  1529 * Display.print_goals function moved to Locale.print_goals;
  1530 
  1531 * standard print function for goals supports current_goals_markers
  1532 variable for marking begin of proof, end of proof, start of goal; the
  1533 default is ("", "", ""); setting current_goals_markers := ("<proof>",
  1534 "</proof>", "<goal>") causes SGML like tagged proof state printing,
  1535 for example;
  1536 
  1537 
  1538 
  1539 New in Isabelle98 (January 1998)
  1540 --------------------------------
  1541 
  1542 *** Overview of INCOMPATIBILITIES (see below for more details) ***
  1543 
  1544 * changed lexical syntax of terms / types: dots made part of long
  1545 identifiers, e.g. "%x.x" no longer possible, should be "%x. x";
  1546 
  1547 * simpset (and claset) reference variable replaced by functions
  1548 simpset / simpset_ref;
  1549 
  1550 * no longer supports theory aliases (via merge) and non-trivial
  1551 implicit merge of thms' signatures;
  1552 
  1553 * most internal names of constants changed due to qualified names;
  1554 
  1555 * changed Pure/Sequence interface (see Pure/seq.ML);
  1556 
  1557 
  1558 *** General Changes ***
  1559 
  1560 * hierachically structured name spaces (for consts, types, axms, thms
  1561 etc.); new lexical class 'longid' (e.g. Foo.bar.x) may render much of
  1562 old input syntactically incorrect (e.g. "%x.x"); COMPATIBILITY:
  1563 isatool fixdots ensures space after dots (e.g. "%x. x"); set
  1564 long_names for fully qualified output names; NOTE: ML programs
  1565 (special tactics, packages etc.) referring to internal names may have
  1566 to be adapted to cope with fully qualified names; in case of severe
  1567 backward campatibility problems try setting 'global_names' at compile
  1568 time to have enrything declared within a flat name space; one may also
  1569 fine tune name declarations in theories via the 'global' and 'local'
  1570 section;
  1571 
  1572 * reimplemented the implicit simpset and claset using the new anytype
  1573 data filed in signatures; references simpset:simpset ref etc. are
  1574 replaced by functions simpset:unit->simpset and
  1575 simpset_ref:unit->simpset ref; COMPATIBILITY: use isatool fixclasimp
  1576 to patch your ML files accordingly;
  1577 
  1578 * HTML output now includes theory graph data for display with Java
  1579 applet or isatool browser; data generated automatically via isatool
  1580 usedir (see -i option, ISABELLE_USEDIR_OPTIONS);
  1581 
  1582 * defs may now be conditional; improved rewrite_goals_tac to handle
  1583 conditional equations;
  1584 
  1585 * defs now admits additional type arguments, using TYPE('a) syntax;
  1586 
  1587 * theory aliases via merge (e.g. M=A+B+C) no longer supported, always
  1588 creates a new theory node; implicit merge of thms' signatures is
  1589 restricted to 'trivial' ones; COMPATIBILITY: one may have to use
  1590 transfer:theory->thm->thm in (rare) cases;
  1591 
  1592 * improved handling of draft signatures / theories; draft thms (and
  1593 ctyps, cterms) are automatically promoted to real ones;
  1594 
  1595 * slightly changed interfaces for oracles: admit many per theory, named
  1596 (e.g. oracle foo = mlfun), additional name argument for invoke_oracle;
  1597 
  1598 * print_goals: optional output of const types (set show_consts and
  1599 show_types);
  1600 
  1601 * improved output of warnings (###) and errors (***);
  1602 
  1603 * subgoal_tac displays a warning if the new subgoal has type variables;
  1604 
  1605 * removed old README and Makefiles;
  1606 
  1607 * replaced print_goals_ref hook by print_current_goals_fn and result_error_fn;
  1608 
  1609 * removed obsolete init_pps and init_database;
  1610 
  1611 * deleted the obsolete tactical STATE, which was declared by
  1612     fun STATE tacfun st = tacfun st st;
  1613 
  1614 * cd and use now support path variables, e.g. $ISABELLE_HOME, or ~
  1615 (which abbreviates $HOME);
  1616 
  1617 * changed Pure/Sequence interface (see Pure/seq.ML); COMPATIBILITY:
  1618 use isatool fixseq to adapt your ML programs (this works for fully
  1619 qualified references to the Sequence structure only!);
  1620 
  1621 * use_thy no longer requires writable current directory; it always
  1622 reloads .ML *and* .thy file, if either one is out of date;
  1623 
  1624 
  1625 *** Classical Reasoner ***
  1626 
  1627 * Clarify_tac, clarify_tac, clarify_step_tac, Clarify_step_tac: new
  1628 tactics that use classical reasoning to simplify a subgoal without
  1629 splitting it into several subgoals;
  1630 
  1631 * Safe_tac: like safe_tac but uses the default claset;
  1632 
  1633 
  1634 *** Simplifier ***
  1635 
  1636 * added simplification meta rules:
  1637     (asm_)(full_)simplify: simpset -> thm -> thm;
  1638 
  1639 * simplifier.ML no longer part of Pure -- has to be loaded by object
  1640 logics (again);
  1641 
  1642 * added prems argument to simplification procedures;
  1643 
  1644 * HOL, FOL, ZF: added infix function `addsplits':
  1645   instead of `<simpset> setloop (split_tac <thms>)'
  1646   you can simply write `<simpset> addsplits <thms>'
  1647 
  1648 
  1649 *** Syntax ***
  1650 
  1651 * TYPE('a) syntax for type reflection terms;
  1652 
  1653 * no longer handles consts with name "" -- declare as 'syntax' instead;
  1654 
  1655 * pretty printer: changed order of mixfix annotation preference (again!);
  1656 
  1657 * Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
  1658 
  1659 
  1660 *** HOL ***
  1661 
  1662 * HOL: there is a new splitter `split_asm_tac' that can be used e.g.
  1663   with `addloop' of the simplifier to faciliate case splitting in premises.
  1664 
  1665 * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
  1666 
  1667 * HOL/Auth: new protocol proofs including some for the Internet
  1668   protocol TLS;
  1669 
  1670 * HOL/Map: new theory of `maps' a la VDM;
  1671 
  1672 * HOL/simplifier: simplification procedures nat_cancel_sums for
  1673 cancelling out common nat summands from =, <, <= (in)equalities, or
  1674 differences; simplification procedures nat_cancel_factor for
  1675 cancelling common factor from =, <, <= (in)equalities over natural
  1676 sums; nat_cancel contains both kinds of procedures, it is installed by
  1677 default in Arith.thy -- this COULD MAKE EXISTING PROOFS FAIL;
  1678 
  1679 * HOL/simplifier: terms of the form
  1680   `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)'  (or t=x)
  1681   are rewritten to
  1682   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)',
  1683   and those of the form
  1684   `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)'  (or t=x)
  1685   are rewritten to
  1686   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) --> R(t)',
  1687 
  1688 * HOL/datatype
  1689   Each datatype `t' now comes with a theorem `split_t_case' of the form
  1690 
  1691   P(t_case f1 ... fn x) =
  1692      ( (!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1)) &
  1693         ...
  1694        (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
  1695      )
  1696 
  1697   and a theorem `split_t_case_asm' of the form
  1698 
  1699   P(t_case f1 ... fn x) =
  1700     ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
  1701         ...
  1702        (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
  1703      )
  1704   which can be added to a simpset via `addsplits'. The existing theorems
  1705   expand_list_case and expand_option_case have been renamed to
  1706   split_list_case and split_option_case.
  1707 
  1708 * HOL/Arithmetic:
  1709   - `pred n' is automatically converted to `n-1'.
  1710     Users are strongly encouraged not to use `pred' any longer,
  1711     because it will disappear altogether at some point.
  1712   - Users are strongly encouraged to write "0 < n" rather than
  1713     "n ~= 0". Theorems and proof tools have been modified towards this
  1714     `standard'.
  1715 
  1716 * HOL/Lists:
  1717   the function "set_of_list" has been renamed "set" (and its theorems too);
  1718   the function "nth" now takes its arguments in the reverse order and
  1719   has acquired the infix notation "!" as in "xs!n".
  1720 
  1721 * HOL/Set: UNIV is now a constant and is no longer translated to Compl{};
  1722 
  1723 * HOL/Set: The operator (UN x.B x) now abbreviates (UN x:UNIV. B x) and its
  1724   specialist theorems (like UN1_I) are gone.  Similarly for (INT x.B x);
  1725 
  1726 * HOL/record: extensible records with schematic structural subtyping
  1727 (single inheritance); EXPERIMENTAL version demonstrating the encoding,
  1728 still lacks various theorems and concrete record syntax;
  1729 
  1730 
  1731 *** HOLCF ***
  1732 
  1733 * removed "axioms" and "generated by" sections;
  1734 
  1735 * replaced "ops" section by extended "consts" section, which is capable of
  1736   handling the continuous function space "->" directly;
  1737 
  1738 * domain package:
  1739   . proves theorems immediately and stores them in the theory,
  1740   . creates hierachical name space,
  1741   . now uses normal mixfix annotations (instead of cinfix...),
  1742   . minor changes to some names and values (for consistency),
  1743   . e.g. cases -> casedist, dists_eq -> dist_eqs, [take_lemma] -> take_lemmas,
  1744   . separator between mutual domain defs: changed "," to "and",
  1745   . improved handling of sort constraints;  now they have to
  1746     appear on the left-hand side of the equations only;
  1747 
  1748 * fixed LAM <x,y,zs>.b syntax;
  1749 
  1750 * added extended adm_tac to simplifier in HOLCF -- can now discharge
  1751 adm (%x. P (t x)), where P is chainfinite and t continuous;
  1752 
  1753 
  1754 *** FOL and ZF ***
  1755 
  1756 * FOL: there is a new splitter `split_asm_tac' that can be used e.g.
  1757   with `addloop' of the simplifier to faciliate case splitting in premises.
  1758 
  1759 * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as
  1760 in HOL, they strip ALL and --> from proved theorems;
  1761 
  1762 
  1763 
  1764 New in Isabelle94-8 (May 1997)
  1765 ------------------------------
  1766 
  1767 *** General Changes ***
  1768 
  1769 * new utilities to build / run / maintain Isabelle etc. (in parts
  1770 still somewhat experimental); old Makefiles etc. still functional;
  1771 
  1772 * new 'Isabelle System Manual';
  1773 
  1774 * INSTALL text, together with ./configure and ./build scripts;
  1775 
  1776 * reimplemented type inference for greater efficiency, better error
  1777 messages and clean internal interface;
  1778 
  1779 * prlim command for dealing with lots of subgoals (an easier way of
  1780 setting goals_limit);
  1781 
  1782 
  1783 *** Syntax ***
  1784 
  1785 * supports alternative (named) syntax tables (parser and pretty
  1786 printer); internal interface is provided by add_modesyntax(_i);
  1787 
  1788 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
  1789 be used in conjunction with the Isabelle symbol font; uses the
  1790 "symbols" syntax table;
  1791 
  1792 * added token_translation interface (may translate name tokens in
  1793 arbitrary ways, dependent on their type (free, bound, tfree, ...) and
  1794 the current print_mode); IMPORTANT: user print translation functions
  1795 are responsible for marking newly introduced bounds
  1796 (Syntax.mark_boundT);
  1797 
  1798 * token translations for modes "xterm" and "xterm_color" that display
  1799 names in bold, underline etc. or colors (which requires a color
  1800 version of xterm);
  1801 
  1802 * infixes may now be declared with names independent of their syntax;
  1803 
  1804 * added typed_print_translation (like print_translation, but may
  1805 access type of constant);
  1806 
  1807 
  1808 *** Classical Reasoner ***
  1809 
  1810 Blast_tac: a new tactic!  It is often more powerful than fast_tac, but has
  1811 some limitations.  Blast_tac...
  1812   + ignores addss, addbefore, addafter; this restriction is intrinsic
  1813   + ignores elimination rules that don't have the correct format
  1814         (the conclusion MUST be a formula variable)
  1815   + ignores types, which can make HOL proofs fail
  1816   + rules must not require higher-order unification, e.g. apply_type in ZF
  1817     [message "Function Var's argument not a bound variable" relates to this]
  1818   + its proof strategy is more general but can actually be slower
  1819 
  1820 * substitution with equality assumptions no longer permutes other
  1821 assumptions;
  1822 
  1823 * minor changes in semantics of addafter (now called addaltern); renamed
  1824 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper
  1825 (and access functions for it);
  1826 
  1827 * improved combination of classical reasoner and simplifier:
  1828   + functions for handling clasimpsets
  1829   + improvement of addss: now the simplifier is called _after_ the
  1830     safe steps.
  1831   + safe variant of addss called addSss: uses safe simplifications
  1832     _during_ the safe steps. It is more complete as it allows multiple
  1833     instantiations of unknowns (e.g. with slow_tac).
  1834 
  1835 *** Simplifier ***
  1836 
  1837 * added interface for simplification procedures (functions that
  1838 produce *proven* rewrite rules on the fly, depending on current
  1839 redex);
  1840 
  1841 * ordering on terms as parameter (used for ordered rewriting);
  1842 
  1843 * new functions delcongs, deleqcongs, and Delcongs. richer rep_ss;
  1844 
  1845 * the solver is now split into a safe and an unsafe part.
  1846 This should be invisible for the normal user, except that the
  1847 functions setsolver and addsolver have been renamed to setSolver and
  1848 addSolver; added safe_asm_full_simp_tac;
  1849 
  1850 
  1851 *** HOL ***
  1852 
  1853 * a generic induction tactic `induct_tac' which works for all datatypes and
  1854 also for type `nat';
  1855 
  1856 * a generic case distinction tactic `exhaust_tac' which works for all
  1857 datatypes and also for type `nat';
  1858 
  1859 * each datatype comes with a function `size';
  1860 
  1861 * patterns in case expressions allow tuple patterns as arguments to
  1862 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...';
  1863 
  1864 * primrec now also works with type nat;
  1865 
  1866 * recdef: a new declaration form, allows general recursive functions to be
  1867 defined in theory files.  See HOL/ex/Fib, HOL/ex/Primes, HOL/Subst/Unify.
  1868 
  1869 * the constant for negation has been renamed from "not" to "Not" to
  1870 harmonize with FOL, ZF, LK, etc.;
  1871 
  1872 * HOL/ex/LFilter theory of a corecursive "filter" functional for
  1873 infinite lists;
  1874 
  1875 * HOL/Modelcheck demonstrates invocation of model checker oracle;
  1876 
  1877 * HOL/ex/Ring.thy declares cring_simp, which solves equational
  1878 problems in commutative rings, using axiomatic type classes for + and *;
  1879 
  1880 * more examples in HOL/MiniML and HOL/Auth;
  1881 
  1882 * more default rewrite rules for quantifiers, union/intersection;
  1883 
  1884 * a new constant `arbitrary == @x.False';
  1885 
  1886 * HOLCF/IOA replaces old HOL/IOA;
  1887 
  1888 * HOLCF changes: derived all rules and arities
  1889   + axiomatic type classes instead of classes
  1890   + typedef instead of faking type definitions
  1891   + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
  1892   + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po
  1893   + eliminated the types void, one, tr
  1894   + use unit lift and bool lift (with translations) instead of one and tr
  1895   + eliminated blift from Lift3.thy (use Def instead of blift)
  1896   all eliminated rules are derived as theorems --> no visible changes ;
  1897 
  1898 
  1899 *** ZF ***
  1900 
  1901 * ZF now has Fast_tac, Simp_tac and Auto_tac.  Union_iff is a now a default
  1902 rewrite rule; this may affect some proofs.  eq_cs is gone but can be put back
  1903 as ZF_cs addSIs [equalityI];
  1904 
  1905 
  1906 
  1907 New in Isabelle94-7 (November 96)
  1908 ---------------------------------
  1909 
  1910 * allowing negative levels (as offsets) in prlev and choplev;
  1911 
  1912 * super-linear speedup for large simplifications;
  1913 
  1914 * FOL, ZF and HOL now use miniscoping: rewriting pushes
  1915 quantifications in as far as possible (COULD MAKE EXISTING PROOFS
  1916 FAIL); can suppress it using the command Delsimps (ex_simps @
  1917 all_simps); De Morgan laws are also now included, by default;
  1918 
  1919 * improved printing of ==>  :  ~:
  1920 
  1921 * new object-logic "Sequents" adds linear logic, while replacing LK
  1922 and Modal (thanks to Sara Kalvala);
  1923 
  1924 * HOL/Auth: correctness proofs for authentication protocols;
  1925 
  1926 * HOL: new auto_tac combines rewriting and classical reasoning (many
  1927 examples on HOL/Auth);
  1928 
  1929 * HOL: new command AddIffs for declaring theorems of the form P=Q to
  1930 the rewriter and classical reasoner simultaneously;
  1931 
  1932 * function uresult no longer returns theorems in "standard" format;
  1933 regain previous version by: val uresult = standard o uresult;
  1934 
  1935 
  1936 
  1937 New in Isabelle94-6
  1938 -------------------
  1939 
  1940 * oracles -- these establish an interface between Isabelle and trusted
  1941 external reasoners, which may deliver results as theorems;
  1942 
  1943 * proof objects (in particular record all uses of oracles);
  1944 
  1945 * Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;
  1946 
  1947 * "constdefs" section in theory files;
  1948 
  1949 * "primrec" section (HOL) no longer requires names;
  1950 
  1951 * internal type "tactic" now simply "thm -> thm Sequence.seq";
  1952 
  1953 
  1954 
  1955 New in Isabelle94-5
  1956 -------------------
  1957 
  1958 * reduced space requirements;
  1959 
  1960 * automatic HTML generation from theories;
  1961 
  1962 * theory files no longer require "..." (quotes) around most types;
  1963 
  1964 * new examples, including two proofs of the Church-Rosser theorem;
  1965 
  1966 * non-curried (1994) version of HOL is no longer distributed;
  1967 
  1968 
  1969 
  1970 New in Isabelle94-4
  1971 -------------------
  1972 
  1973 * greatly reduced space requirements;
  1974 
  1975 * theory files (.thy) no longer require \...\ escapes at line breaks;
  1976 
  1977 * searchable theorem database (see the section "Retrieving theorems" on
  1978 page 8 of the Reference Manual);
  1979 
  1980 * new examples, including Grabczewski's monumental case study of the
  1981 Axiom of Choice;
  1982 
  1983 * The previous version of HOL renamed to Old_HOL;
  1984 
  1985 * The new version of HOL (previously called CHOL) uses a curried syntax
  1986 for functions.  Application looks like f a b instead of f(a,b);
  1987 
  1988 * Mutually recursive inductive definitions finally work in HOL;
  1989 
  1990 * In ZF, pattern-matching on tuples is now available in all abstractions and
  1991 translates to the operator "split";
  1992 
  1993 
  1994 
  1995 New in Isabelle94-3
  1996 -------------------
  1997 
  1998 * new infix operator, addss, allowing the classical reasoner to
  1999 perform simplification at each step of its search.  Example:
  2000         fast_tac (cs addss ss)
  2001 
  2002 * a new logic, CHOL, the same as HOL, but with a curried syntax
  2003 for functions.  Application looks like f a b instead of f(a,b).  Also pairs
  2004 look like (a,b) instead of <a,b>;
  2005 
  2006 * PLEASE NOTE: CHOL will eventually replace HOL!
  2007 
  2008 * In CHOL, pattern-matching on tuples is now available in all abstractions.
  2009 It translates to the operator "split".  A new theory of integers is available;
  2010 
  2011 * In ZF, integer numerals now denote two's-complement binary integers.
  2012 Arithmetic operations can be performed by rewriting.  See ZF/ex/Bin.ML;
  2013 
  2014 * Many new examples: I/O automata, Church-Rosser theorem, equivalents
  2015 of the Axiom of Choice;
  2016 
  2017 
  2018 
  2019 New in Isabelle94-2
  2020 -------------------
  2021 
  2022 * Significantly faster resolution;
  2023 
  2024 * the different sections in a .thy file can now be mixed and repeated
  2025 freely;
  2026 
  2027 * Database of theorems for FOL, HOL and ZF.  New
  2028 commands including qed, qed_goal and bind_thm store theorems in the database.
  2029 
  2030 * Simple database queries: return a named theorem (get_thm) or all theorems of
  2031 a given theory (thms_of), or find out what theory a theorem was proved in
  2032 (theory_of_thm);
  2033 
  2034 * Bugs fixed in the inductive definition and datatype packages;
  2035 
  2036 * The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs
  2037 and HOL_dup_cs obsolete;
  2038 
  2039 * Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1
  2040 have been removed;
  2041 
  2042 * Simpler definition of function space in ZF;
  2043 
  2044 * new results about cardinal and ordinal arithmetic in ZF;
  2045 
  2046 * 'subtype' facility in HOL for introducing new types as subsets of existing
  2047 types;
  2048 
  2049 
  2050 $Id$