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