NEWS
author paulson
Tue Jan 19 11:18:11 1999 +0100 (1999-01-19)
changeset 6141 a6922171b396
parent 6131 2d9e609abcdb
child 6155 e387d188d0ca
permissions -rw-r--r--
removal of the (thm list) argument of mk_cases
     1 Isabelle NEWS -- history user-relevant changes
     2 ==============================================
     3 
     4 New in this Isabelle version
     5 ----------------------------
     6 
     7 *** Overview of INCOMPATIBILITIES (see below for more details) ***
     8 
     9 * HOL: Removed the obsolete syntax "Compl A"; use -A for set complement
    10 
    11 * ZF: The con_defs part of an inductive definition may no longer refer to 
    12   constants declared in the same theory;
    13 
    14 * HOL, ZF: the function mk_cases, generated by the inductive definition 
    15   package, has lost an argument.  To simplify its result, it uses the default
    16   simpset instead of a supplied list of theorems.
    17 
    18 
    19 *** Proof tools ***
    20 
    21 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a decision
    22 procedure for linear arithmetic. Currently it is used for types `nat' and
    23 `int' in HOL (see below) but can, should and will be instantiated for other
    24 types and logics as well.
    25 
    26 
    27 *** General ***
    28 
    29 * in locales, the "assumes" and "defines" parts may be omitted if empty;
    30 
    31 * new print_mode "xsymbols" for extended symbol support 
    32   (e.g. genuiely long arrows)
    33 
    34 *** HOL ***
    35 
    36 * There are now decision procedures for linear arithmetic over nat and int:
    37 
    38 1. arith_tac copes with arbitrary formulae involving `=', `<', `<=', `+',
    39 `-', `Suc' and numerical constants; other subterms are treated as atomic;
    40 subformulae not involving type `nat' or `int' are ignored; quantified
    41 subformulae are ignored unless they are positive universal or negative
    42 existential. The tactic has to be invoked by hand and can be a little bit
    43 slow. In particular, the running time is exponential in the number of
    44 occurrences of `-' on `nat'.
    45 
    46 2. fast_arith_tac is a cut-down version of arith_tac: it only takes (negated)
    47 (in)equalities among the premises and the conclusion into account (i.e. no
    48 compound formulae) and does not know about `-' on `nat'. It is fast and is
    49 used automatically by the simplifier.
    50 
    51 NB: At the moment, these decision procedures do not cope with mixed nat/int
    52 formulae where the two parts interact, such as `m < n ==> int(m) < int(n)'.
    53 
    54 *** Internal programming interfaces ***
    55 
    56 * tuned current_goals_markers semantics: begin / end goal avoids
    57 printing empty lines;
    58 
    59 * removed prs and prs_fn hook, which was broken because it did not
    60 include \n in its semantics, forcing writeln to add one
    61 uncoditionally; replaced prs_fn by writeln_fn; consider std_output:
    62 string -> unit if you really want to output text without newline;
    63 
    64 
    65 *** ZF ***
    66 
    67 * new primrec section allows primitive recursive functions to be given
    68   directly (as in HOL) over datatypes and the natural numbers;
    69 
    70 * new tactics induct_tac and exhaust_tac for induction (or case analysis)
    71   over datatypes and the natural numbers;
    72 
    73 * the datatype declaration of type T now defines the recursor T_rec;
    74 
    75 * simplification automatically does freeness reasoning for datatype
    76   constructors;
    77 
    78 * The syntax "if P then x else y" is now available in addition to if(P,x,y).
    79 
    80 
    81 New in Isabelle98-1 (October 1998)
    82 ----------------------------------
    83 
    84 *** Overview of INCOMPATIBILITIES (see below for more details) ***
    85 
    86 * several changes of automated proof tools;
    87 
    88 * HOL: major changes to the inductive and datatype packages, including
    89 some minor incompatibilities of theory syntax;
    90 
    91 * HOL: renamed r^-1 to 'converse' from 'inverse'; 'inj_onto' is now
    92 called `inj_on';
    93 
    94 * HOL: removed duplicate thms in Arith:
    95   less_imp_add_less  should be replaced by  trans_less_add1
    96   le_imp_add_le      should be replaced by  trans_le_add1
    97 
    98 * HOL: unary minus is now overloaded (new type constraints may be
    99 required);
   100 
   101 * HOL and ZF: unary minus for integers is now #- instead of #~.  In
   102 ZF, expressions such as n#-1 must be changed to n#- 1, since #-1 is
   103 now taken as an integer constant.
   104 
   105 * Pure: ML function 'theory_of' renamed to 'theory';
   106 
   107 
   108 *** Proof tools ***
   109 
   110 * Simplifier:
   111   1. Asm_full_simp_tac is now more aggressive.
   112      1. It will sometimes reorient premises if that increases their power to
   113         simplify.
   114      2. It does no longer proceed strictly from left to right but may also
   115         rotate premises to achieve further simplification.
   116      For compatibility reasons there is now Asm_lr_simp_tac which is like the
   117      old Asm_full_simp_tac in that it does not rotate premises.
   118   2. The simplifier now knows a little bit about nat-arithmetic.
   119 
   120 * Classical reasoner: wrapper mechanism for the classical reasoner now
   121 allows for selected deletion of wrappers, by introduction of names for
   122 wrapper functionals.  This implies that addbefore, addSbefore,
   123 addaltern, and addSaltern now take a pair (name, tactic) as argument,
   124 and that adding two tactics with the same name overwrites the first
   125 one (emitting a warning).
   126   type wrapper = (int -> tactic) -> (int -> tactic)
   127   setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by
   128   addWrapper, addSWrapper: claset * (string * wrapper) -> claset
   129   delWrapper, delSWrapper: claset *  string            -> claset
   130   getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
   131 
   132 * Classical reasoner: addbefore/addSbefore now have APPEND/ORELSE
   133 semantics; addbefore now affects only the unsafe part of step_tac
   134 etc.; this affects addss/auto_tac/force_tac, so EXISTING PROOFS MAY
   135 FAIL, but proofs should be fixable easily, e.g. by replacing Auto_tac
   136 by Force_tac;
   137 
   138 * Classical reasoner: setwrapper to setWrapper and compwrapper to
   139 compWrapper; added safe wrapper (and access functions for it);
   140 
   141 * HOL/split_all_tac is now much faster and fails if there is nothing
   142 to split.  Some EXISTING PROOFS MAY REQUIRE ADAPTION because the order
   143 and the names of the automatically generated variables have changed.
   144 split_all_tac has moved within claset() from unsafe wrappers to safe
   145 wrappers, which means that !!-bound variables are split much more
   146 aggressively, and safe_tac and clarify_tac now split such variables.
   147 If this splitting is not appropriate, use delSWrapper "split_all_tac".
   148 Note: the same holds for record_split_tac, which does the job of
   149 split_all_tac for record fields.
   150 
   151 * HOL/Simplifier: Rewrite rules for case distinctions can now be added
   152 permanently to the default simpset using Addsplits just like
   153 Addsimps. They can be removed via Delsplits just like
   154 Delsimps. Lower-case versions are also available.
   155 
   156 * HOL/Simplifier: The rule split_if is now part of the default
   157 simpset. This means that the simplifier will eliminate all occurrences
   158 of if-then-else in the conclusion of a goal. To prevent this, you can
   159 either remove split_if completely from the default simpset by
   160 `Delsplits [split_if]' or remove it in a specific call of the
   161 simplifier using `... delsplits [split_if]'.  You can also add/delete
   162 other case splitting rules to/from the default simpset: every datatype
   163 generates suitable rules `split_t_case' and `split_t_case_asm' (where
   164 t is the name of the datatype).
   165 
   166 * Classical reasoner / Simplifier combination: new force_tac (and
   167 derivatives Force_tac, force) combines rewriting and classical
   168 reasoning (and whatever other tools) similarly to auto_tac, but is
   169 aimed to solve the given subgoal completely.
   170 
   171 
   172 *** General ***
   173 
   174 * new top-level commands `Goal' and `Goalw' that improve upon `goal'
   175 and `goalw': the theory is no longer needed as an explicit argument -
   176 the current theory context is used; assumptions are no longer returned
   177 at the ML-level unless one of them starts with ==> or !!; it is
   178 recommended to convert to these new commands using isatool fixgoal
   179 (backup your sources first!);
   180 
   181 * new top-level commands 'thm' and 'thms' for retrieving theorems from
   182 the current theory context, and 'theory' to lookup stored theories;
   183 
   184 * new theory section 'locale' for declaring constants, assumptions and
   185 definitions that have local scope;
   186 
   187 * new theory section 'nonterminals' for purely syntactic types;
   188 
   189 * new theory section 'setup' for generic ML setup functions
   190 (e.g. package initialization);
   191 
   192 * the distribution now includes Isabelle icons: see
   193 lib/logo/isabelle-{small,tiny}.xpm;
   194 
   195 * isatool install - install binaries with absolute references to
   196 ISABELLE_HOME/bin;
   197 
   198 * isatool logo -- create instances of the Isabelle logo (as EPS);
   199 
   200 * print mode 'emacs' reserved for Isamode;
   201 
   202 * support multiple print (ast) translations per constant name;
   203 
   204 
   205 *** HOL ***
   206 
   207 * there is now a tutorial on Isabelle/HOL (do 'isatool doc tutorial');
   208 
   209 * HOL/inductive package reorganized and improved: now supports mutual
   210 definitions such as
   211 
   212   inductive EVEN ODD
   213     intrs
   214       null "0 : EVEN"
   215       oddI "n : EVEN ==> Suc n : ODD"
   216       evenI "n : ODD ==> Suc n : EVEN"
   217 
   218 new theorem list "elims" contains an elimination rule for each of the
   219 recursive sets; inductive definitions now handle disjunctive premises
   220 correctly (also ZF);
   221 
   222 INCOMPATIBILITIES: requires Inductive as an ancestor; component
   223 "mutual_induct" no longer exists - the induction rule is always
   224 contained in "induct";
   225 
   226 
   227 * HOL/datatype package re-implemented and greatly improved: now
   228 supports mutually recursive datatypes such as
   229 
   230   datatype
   231     'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp)
   232             | SUM ('a aexp) ('a aexp)
   233             | DIFF ('a aexp) ('a aexp)
   234             | NUM 'a
   235   and
   236     'a bexp = LESS ('a aexp) ('a aexp)
   237             | AND ('a bexp) ('a bexp)
   238             | OR ('a bexp) ('a bexp)
   239 
   240 as well as indirectly recursive datatypes such as
   241 
   242   datatype
   243     ('a, 'b) term = Var 'a
   244                   | App 'b ((('a, 'b) term) list)
   245 
   246 The new tactic  mutual_induct_tac [<var_1>, ..., <var_n>] i  performs
   247 induction on mutually / indirectly recursive datatypes.
   248 
   249 Primrec equations are now stored in theory and can be accessed via
   250 <function_name>.simps.
   251 
   252 INCOMPATIBILITIES:
   253 
   254   - Theories using datatypes must now have theory Datatype as an
   255     ancestor.
   256   - The specific <typename>.induct_tac no longer exists - use the
   257     generic induct_tac instead.
   258   - natE has been renamed to nat.exhaust - use exhaust_tac
   259     instead of res_inst_tac ... natE. Note that the variable
   260     names in nat.exhaust differ from the names in natE, this
   261     may cause some "fragile" proofs to fail.
   262   - The theorems split_<typename>_case and split_<typename>_case_asm
   263     have been renamed to <typename>.split and <typename>.split_asm.
   264   - Since default sorts of type variables are now handled correctly,
   265     some datatype definitions may have to be annotated with explicit
   266     sort constraints.
   267   - Primrec definitions no longer require function name and type
   268     of recursive argument.
   269 
   270 Consider using isatool fixdatatype to adapt your theories and proof
   271 scripts to the new package (backup your sources first!).
   272 
   273 
   274 * HOL/record package: considerably improved implementation; now
   275 includes concrete syntax for record types, terms, updates; theorems
   276 for surjective pairing and splitting !!-bound record variables; proof
   277 support is as follows:
   278 
   279   1) standard conversions (selectors or updates applied to record
   280 constructor terms) are part of the standard simpset;
   281 
   282   2) inject equations of the form ((x, y) = (x', y')) == x=x' & y=y' are
   283 made part of standard simpset and claset via addIffs;
   284 
   285   3) a tactic for record field splitting (record_split_tac) is part of
   286 the standard claset (addSWrapper);
   287 
   288 To get a better idea about these rules you may retrieve them via
   289 something like 'thms "foo.simps"' or 'thms "foo.iffs"', where "foo" is
   290 the name of your record type.
   291 
   292 The split tactic 3) conceptually simplifies by the following rule:
   293 
   294   "(!!x. PROP ?P x) == (!!a b. PROP ?P (a, b))"
   295 
   296 Thus any record variable that is bound by meta-all will automatically
   297 blow up into some record constructor term, consequently the
   298 simplifications of 1), 2) apply.  Thus force_tac, auto_tac etc. shall
   299 solve record problems automatically.
   300 
   301 
   302 * reorganized the main HOL image: HOL/Integ and String loaded by
   303 default; theory Main includes everything;
   304 
   305 * automatic simplification of integer sums and comparisons, using cancellation;
   306 
   307 * added option_map_eq_Some and not_Some_eq to the default simpset and claset;
   308 
   309 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset;
   310 
   311 * many new identities for unions, intersections, set difference, etc.;
   312 
   313 * expand_if, expand_split, expand_sum_case and expand_nat_case are now
   314 called split_if, split_split, split_sum_case and split_nat_case (to go
   315 with add/delsplits);
   316 
   317 * HOL/Prod introduces simplification procedure unit_eq_proc rewriting
   318 (?x::unit) = (); this is made part of the default simpset, which COULD
   319 MAKE EXISTING PROOFS FAIL under rare circumstances (consider
   320 'Delsimprocs [unit_eq_proc];' as last resort); also note that
   321 unit_abs_eta_conv is added in order to counter the effect of
   322 unit_eq_proc on (%u::unit. f u), replacing it by f rather than by
   323 %u.f();
   324 
   325 * HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which
   326 makes more sense);
   327 
   328 * HOL/Set INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
   329   It and 'sym RS equals0D' are now in the default  claset, giving automatic
   330   disjointness reasoning but breaking a few old proofs.
   331 
   332 * HOL/Relation INCOMPATIBILITY: renamed the relational operator r^-1
   333 to 'converse' from 'inverse' (for compatibility with ZF and some
   334 literature);
   335 
   336 * HOL/recdef can now declare non-recursive functions, with {} supplied as
   337 the well-founded relation;
   338 
   339 * HOL/Set INCOMPATIBILITY: the complement of set A is now written -A instead of
   340     Compl A.  The "Compl" syntax remains available as input syntax for this
   341     release ONLY.
   342 
   343 * HOL/Update: new theory of function updates:
   344     f(a:=b) == %x. if x=a then b else f x
   345 may also be iterated as in f(a:=b,c:=d,...);
   346 
   347 * HOL/Vimage: new theory for inverse image of a function, syntax f-``B;
   348 
   349 * HOL/List:
   350   - new function list_update written xs[i:=v] that updates the i-th
   351     list position. May also be iterated as in xs[i:=a,j:=b,...].
   352   - new function `upt' written [i..j(] which generates the list
   353     [i,i+1,...,j-1], i.e. the upper bound is excluded. To include the upper
   354     bound write [i..j], which is a shorthand for [i..j+1(].
   355   - new lexicographic orderings and corresponding wellfoundedness theorems.
   356 
   357 * HOL/Arith:
   358   - removed 'pred' (predecessor) function;
   359   - generalized some theorems about n-1;
   360   - many new laws about "div" and "mod";
   361   - new laws about greatest common divisors (see theory ex/Primes);
   362 
   363 * HOL/Relation: renamed the relational operator r^-1 "converse"
   364 instead of "inverse";
   365 
   366 * HOL/Induct/Multiset: a theory of multisets, including the wellfoundedness
   367   of the multiset ordering;
   368 
   369 * directory HOL/Real: a construction of the reals using Dedekind cuts
   370   (not included by default);
   371 
   372 * directory HOL/UNITY: Chandy and Misra's UNITY formalism;
   373 
   374 * directory HOL/Hoare: a new version of Hoare logic which permits many-sorted
   375   programs, i.e. different program variables may have different types.
   376 
   377 * calling (stac rew i) now fails if "rew" has no effect on the goal
   378   [previously, this check worked only if the rewrite rule was unconditional]
   379   Now rew can involve either definitions or equalities (either == or =).
   380 
   381 
   382 *** ZF ***
   383 
   384 * theory Main includes everything; INCOMPATIBILITY: theory ZF.thy contains
   385   only the theorems proved on ZF.ML;
   386 
   387 * ZF INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
   388   It and 'sym RS equals0D' are now in the default  claset, giving automatic
   389   disjointness reasoning but breaking a few old proofs.
   390 
   391 * ZF/Update: new theory of function updates
   392     with default rewrite rule  f(x:=y) ` z = if(z=x, y, f`z)
   393   may also be iterated as in f(a:=b,c:=d,...);
   394 
   395 * in  let x=t in u(x), neither t nor u(x) has to be an FOL term.
   396 
   397 * calling (stac rew i) now fails if "rew" has no effect on the goal
   398   [previously, this check worked only if the rewrite rule was unconditional]
   399   Now rew can involve either definitions or equalities (either == or =).
   400 
   401 * case_tac provided for compatibility with HOL
   402     (like the old excluded_middle_tac, but with subgoals swapped)
   403 
   404 
   405 *** Internal programming interfaces ***
   406 
   407 * Pure: several new basic modules made available for general use, see
   408 also src/Pure/README;
   409 
   410 * improved the theory data mechanism to support encapsulation (data
   411 kind name replaced by private Object.kind, acting as authorization
   412 key); new type-safe user interface via functor TheoryDataFun; generic
   413 print_data function becomes basically useless;
   414 
   415 * removed global_names compatibility flag -- all theory declarations
   416 are qualified by default;
   417 
   418 * module Pure/Syntax now offers quote / antiquote translation
   419 functions (useful for Hoare logic etc. with implicit dependencies);
   420 see HOL/ex/Antiquote for an example use;
   421 
   422 * Simplifier now offers conversions (asm_)(full_)rewrite: simpset ->
   423 cterm -> thm;
   424 
   425 * new tactical CHANGED_GOAL for checking that a tactic modifies a
   426 subgoal;
   427 
   428 * Display.print_goals function moved to Locale.print_goals;
   429 
   430 * standard print function for goals supports current_goals_markers
   431 variable for marking begin of proof, end of proof, start of goal; the
   432 default is ("", "", ""); setting current_goals_markers := ("<proof>",
   433 "</proof>", "<goal>") causes SGML like tagged proof state printing,
   434 for example;
   435 
   436 
   437 
   438 New in Isabelle98 (January 1998)
   439 --------------------------------
   440 
   441 *** Overview of INCOMPATIBILITIES (see below for more details) ***
   442 
   443 * changed lexical syntax of terms / types: dots made part of long
   444 identifiers, e.g. "%x.x" no longer possible, should be "%x. x";
   445 
   446 * simpset (and claset) reference variable replaced by functions
   447 simpset / simpset_ref;
   448 
   449 * no longer supports theory aliases (via merge) and non-trivial
   450 implicit merge of thms' signatures;
   451 
   452 * most internal names of constants changed due to qualified names;
   453 
   454 * changed Pure/Sequence interface (see Pure/seq.ML);
   455 
   456 
   457 *** General Changes ***
   458 
   459 * hierachically structured name spaces (for consts, types, axms, thms
   460 etc.); new lexical class 'longid' (e.g. Foo.bar.x) may render much of
   461 old input syntactically incorrect (e.g. "%x.x"); COMPATIBILITY:
   462 isatool fixdots ensures space after dots (e.g. "%x. x"); set
   463 long_names for fully qualified output names; NOTE: ML programs
   464 (special tactics, packages etc.) referring to internal names may have
   465 to be adapted to cope with fully qualified names; in case of severe
   466 backward campatibility problems try setting 'global_names' at compile
   467 time to have enrything declared within a flat name space; one may also
   468 fine tune name declarations in theories via the 'global' and 'local'
   469 section;
   470 
   471 * reimplemented the implicit simpset and claset using the new anytype
   472 data filed in signatures; references simpset:simpset ref etc. are
   473 replaced by functions simpset:unit->simpset and
   474 simpset_ref:unit->simpset ref; COMPATIBILITY: use isatool fixclasimp
   475 to patch your ML files accordingly;
   476 
   477 * HTML output now includes theory graph data for display with Java
   478 applet or isatool browser; data generated automatically via isatool
   479 usedir (see -i option, ISABELLE_USEDIR_OPTIONS);
   480 
   481 * defs may now be conditional; improved rewrite_goals_tac to handle
   482 conditional equations;
   483 
   484 * defs now admits additional type arguments, using TYPE('a) syntax;
   485 
   486 * theory aliases via merge (e.g. M=A+B+C) no longer supported, always
   487 creates a new theory node; implicit merge of thms' signatures is
   488 restricted to 'trivial' ones; COMPATIBILITY: one may have to use
   489 transfer:theory->thm->thm in (rare) cases;
   490 
   491 * improved handling of draft signatures / theories; draft thms (and
   492 ctyps, cterms) are automatically promoted to real ones;
   493 
   494 * slightly changed interfaces for oracles: admit many per theory, named
   495 (e.g. oracle foo = mlfun), additional name argument for invoke_oracle;
   496 
   497 * print_goals: optional output of const types (set show_consts and
   498 show_types);
   499 
   500 * improved output of warnings (###) and errors (***);
   501 
   502 * subgoal_tac displays a warning if the new subgoal has type variables;
   503 
   504 * removed old README and Makefiles;
   505 
   506 * replaced print_goals_ref hook by print_current_goals_fn and result_error_fn;
   507 
   508 * removed obsolete init_pps and init_database;
   509 
   510 * deleted the obsolete tactical STATE, which was declared by
   511     fun STATE tacfun st = tacfun st st;
   512 
   513 * cd and use now support path variables, e.g. $ISABELLE_HOME, or ~
   514 (which abbreviates $HOME);
   515 
   516 * changed Pure/Sequence interface (see Pure/seq.ML); COMPATIBILITY:
   517 use isatool fixseq to adapt your ML programs (this works for fully
   518 qualified references to the Sequence structure only!);
   519 
   520 * use_thy no longer requires writable current directory; it always
   521 reloads .ML *and* .thy file, if either one is out of date;
   522 
   523 
   524 *** Classical Reasoner ***
   525 
   526 * Clarify_tac, clarify_tac, clarify_step_tac, Clarify_step_tac: new
   527 tactics that use classical reasoning to simplify a subgoal without
   528 splitting it into several subgoals;
   529 
   530 * Safe_tac: like safe_tac but uses the default claset;
   531 
   532 
   533 *** Simplifier ***
   534 
   535 * added simplification meta rules:
   536     (asm_)(full_)simplify: simpset -> thm -> thm;
   537 
   538 * simplifier.ML no longer part of Pure -- has to be loaded by object
   539 logics (again);
   540 
   541 * added prems argument to simplification procedures;
   542 
   543 * HOL, FOL, ZF: added infix function `addsplits':
   544   instead of `<simpset> setloop (split_tac <thms>)'
   545   you can simply write `<simpset> addsplits <thms>'
   546 
   547 
   548 *** Syntax ***
   549 
   550 * TYPE('a) syntax for type reflection terms;
   551 
   552 * no longer handles consts with name "" -- declare as 'syntax' instead;
   553 
   554 * pretty printer: changed order of mixfix annotation preference (again!);
   555 
   556 * Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
   557 
   558 
   559 *** HOL ***
   560 
   561 * HOL: there is a new splitter `split_asm_tac' that can be used e.g.
   562   with `addloop' of the simplifier to faciliate case splitting in premises.
   563 
   564 * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
   565 
   566 * HOL/Auth: new protocol proofs including some for the Internet
   567   protocol TLS;
   568 
   569 * HOL/Map: new theory of `maps' a la VDM;
   570 
   571 * HOL/simplifier: simplification procedures nat_cancel_sums for
   572 cancelling out common nat summands from =, <, <= (in)equalities, or
   573 differences; simplification procedures nat_cancel_factor for
   574 cancelling common factor from =, <, <= (in)equalities over natural
   575 sums; nat_cancel contains both kinds of procedures, it is installed by
   576 default in Arith.thy -- this COULD MAKE EXISTING PROOFS FAIL;
   577 
   578 * HOL/simplifier: terms of the form
   579   `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)'  (or t=x)
   580   are rewritten to
   581   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)',
   582   and those of the form
   583   `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)'  (or t=x)
   584   are rewritten to
   585   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) --> R(t)',
   586 
   587 * HOL/datatype
   588   Each datatype `t' now comes with a theorem `split_t_case' of the form
   589 
   590   P(t_case f1 ... fn x) =
   591      ( (!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1)) &
   592         ...
   593        (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
   594      )
   595 
   596   and a theorem `split_t_case_asm' of the form
   597 
   598   P(t_case f1 ... fn x) =
   599     ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
   600         ...
   601        (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
   602      )
   603   which can be added to a simpset via `addsplits'. The existing theorems
   604   expand_list_case and expand_option_case have been renamed to
   605   split_list_case and split_option_case.
   606 
   607 * HOL/Arithmetic:
   608   - `pred n' is automatically converted to `n-1'.
   609     Users are strongly encouraged not to use `pred' any longer,
   610     because it will disappear altogether at some point.
   611   - Users are strongly encouraged to write "0 < n" rather than
   612     "n ~= 0". Theorems and proof tools have been modified towards this
   613     `standard'.
   614 
   615 * HOL/Lists:
   616   the function "set_of_list" has been renamed "set" (and its theorems too);
   617   the function "nth" now takes its arguments in the reverse order and
   618   has acquired the infix notation "!" as in "xs!n".
   619 
   620 * HOL/Set: UNIV is now a constant and is no longer translated to Compl{};
   621 
   622 * HOL/Set: The operator (UN x.B x) now abbreviates (UN x:UNIV. B x) and its
   623   specialist theorems (like UN1_I) are gone.  Similarly for (INT x.B x);
   624 
   625 * HOL/record: extensible records with schematic structural subtyping
   626 (single inheritance); EXPERIMENTAL version demonstrating the encoding,
   627 still lacks various theorems and concrete record syntax;
   628 
   629 
   630 *** HOLCF ***
   631 
   632 * removed "axioms" and "generated by" sections;
   633 
   634 * replaced "ops" section by extended "consts" section, which is capable of
   635   handling the continuous function space "->" directly;
   636 
   637 * domain package:
   638   . proves theorems immediately and stores them in the theory,
   639   . creates hierachical name space,
   640   . now uses normal mixfix annotations (instead of cinfix...),
   641   . minor changes to some names and values (for consistency),
   642   . e.g. cases -> casedist, dists_eq -> dist_eqs, [take_lemma] -> take_lemmas,
   643   . separator between mutual domain defs: changed "," to "and",
   644   . improved handling of sort constraints;  now they have to
   645     appear on the left-hand side of the equations only;
   646 
   647 * fixed LAM <x,y,zs>.b syntax;
   648 
   649 * added extended adm_tac to simplifier in HOLCF -- can now discharge
   650 adm (%x. P (t x)), where P is chainfinite and t continuous;
   651 
   652 
   653 *** FOL and ZF ***
   654 
   655 * FOL: there is a new splitter `split_asm_tac' that can be used e.g.
   656   with `addloop' of the simplifier to faciliate case splitting in premises.
   657 
   658 * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as
   659 in HOL, they strip ALL and --> from proved theorems;
   660 
   661 
   662 
   663 New in Isabelle94-8 (May 1997)
   664 ------------------------------
   665 
   666 *** General Changes ***
   667 
   668 * new utilities to build / run / maintain Isabelle etc. (in parts
   669 still somewhat experimental); old Makefiles etc. still functional;
   670 
   671 * new 'Isabelle System Manual';
   672 
   673 * INSTALL text, together with ./configure and ./build scripts;
   674 
   675 * reimplemented type inference for greater efficiency, better error
   676 messages and clean internal interface;
   677 
   678 * prlim command for dealing with lots of subgoals (an easier way of
   679 setting goals_limit);
   680 
   681 
   682 *** Syntax ***
   683 
   684 * supports alternative (named) syntax tables (parser and pretty
   685 printer); internal interface is provided by add_modesyntax(_i);
   686 
   687 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
   688 be used in conjunction with the Isabelle symbol font; uses the
   689 "symbols" syntax table;
   690 
   691 * added token_translation interface (may translate name tokens in
   692 arbitrary ways, dependent on their type (free, bound, tfree, ...) and
   693 the current print_mode); IMPORTANT: user print translation functions
   694 are responsible for marking newly introduced bounds
   695 (Syntax.mark_boundT);
   696 
   697 * token translations for modes "xterm" and "xterm_color" that display
   698 names in bold, underline etc. or colors (which requires a color
   699 version of xterm);
   700 
   701 * infixes may now be declared with names independent of their syntax;
   702 
   703 * added typed_print_translation (like print_translation, but may
   704 access type of constant);
   705 
   706 
   707 *** Classical Reasoner ***
   708 
   709 Blast_tac: a new tactic!  It is often more powerful than fast_tac, but has
   710 some limitations.  Blast_tac...
   711   + ignores addss, addbefore, addafter; this restriction is intrinsic
   712   + ignores elimination rules that don't have the correct format
   713         (the conclusion MUST be a formula variable)
   714   + ignores types, which can make HOL proofs fail
   715   + rules must not require higher-order unification, e.g. apply_type in ZF
   716     [message "Function Var's argument not a bound variable" relates to this]
   717   + its proof strategy is more general but can actually be slower
   718 
   719 * substitution with equality assumptions no longer permutes other
   720 assumptions;
   721 
   722 * minor changes in semantics of addafter (now called addaltern); renamed
   723 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper
   724 (and access functions for it);
   725 
   726 * improved combination of classical reasoner and simplifier:
   727   + functions for handling clasimpsets
   728   + improvement of addss: now the simplifier is called _after_ the
   729     safe steps.
   730   + safe variant of addss called addSss: uses safe simplifications
   731     _during_ the safe steps. It is more complete as it allows multiple
   732     instantiations of unknowns (e.g. with slow_tac).
   733 
   734 *** Simplifier ***
   735 
   736 * added interface for simplification procedures (functions that
   737 produce *proven* rewrite rules on the fly, depending on current
   738 redex);
   739 
   740 * ordering on terms as parameter (used for ordered rewriting);
   741 
   742 * new functions delcongs, deleqcongs, and Delcongs. richer rep_ss;
   743 
   744 * the solver is now split into a safe and an unsafe part.
   745 This should be invisible for the normal user, except that the
   746 functions setsolver and addsolver have been renamed to setSolver and
   747 addSolver; added safe_asm_full_simp_tac;
   748 
   749 
   750 *** HOL ***
   751 
   752 * a generic induction tactic `induct_tac' which works for all datatypes and
   753 also for type `nat';
   754 
   755 * a generic case distinction tactic `exhaust_tac' which works for all
   756 datatypes and also for type `nat';
   757 
   758 * each datatype comes with a function `size';
   759 
   760 * patterns in case expressions allow tuple patterns as arguments to
   761 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...';
   762 
   763 * primrec now also works with type nat;
   764 
   765 * recdef: a new declaration form, allows general recursive functions to be
   766 defined in theory files.  See HOL/ex/Fib, HOL/ex/Primes, HOL/Subst/Unify.
   767 
   768 * the constant for negation has been renamed from "not" to "Not" to
   769 harmonize with FOL, ZF, LK, etc.;
   770 
   771 * HOL/ex/LFilter theory of a corecursive "filter" functional for
   772 infinite lists;
   773 
   774 * HOL/Modelcheck demonstrates invocation of model checker oracle;
   775 
   776 * HOL/ex/Ring.thy declares cring_simp, which solves equational
   777 problems in commutative rings, using axiomatic type classes for + and *;
   778 
   779 * more examples in HOL/MiniML and HOL/Auth;
   780 
   781 * more default rewrite rules for quantifiers, union/intersection;
   782 
   783 * a new constant `arbitrary == @x.False';
   784 
   785 * HOLCF/IOA replaces old HOL/IOA;
   786 
   787 * HOLCF changes: derived all rules and arities
   788   + axiomatic type classes instead of classes
   789   + typedef instead of faking type definitions
   790   + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
   791   + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po
   792   + eliminated the types void, one, tr
   793   + use unit lift and bool lift (with translations) instead of one and tr
   794   + eliminated blift from Lift3.thy (use Def instead of blift)
   795   all eliminated rules are derived as theorems --> no visible changes ;
   796 
   797 
   798 *** ZF ***
   799 
   800 * ZF now has Fast_tac, Simp_tac and Auto_tac.  Union_iff is a now a default
   801 rewrite rule; this may affect some proofs.  eq_cs is gone but can be put back
   802 as ZF_cs addSIs [equalityI];
   803 
   804 
   805 
   806 New in Isabelle94-7 (November 96)
   807 ---------------------------------
   808 
   809 * allowing negative levels (as offsets) in prlev and choplev;
   810 
   811 * super-linear speedup for large simplifications;
   812 
   813 * FOL, ZF and HOL now use miniscoping: rewriting pushes
   814 quantifications in as far as possible (COULD MAKE EXISTING PROOFS
   815 FAIL); can suppress it using the command Delsimps (ex_simps @
   816 all_simps); De Morgan laws are also now included, by default;
   817 
   818 * improved printing of ==>  :  ~:
   819 
   820 * new object-logic "Sequents" adds linear logic, while replacing LK
   821 and Modal (thanks to Sara Kalvala);
   822 
   823 * HOL/Auth: correctness proofs for authentication protocols;
   824 
   825 * HOL: new auto_tac combines rewriting and classical reasoning (many
   826 examples on HOL/Auth);
   827 
   828 * HOL: new command AddIffs for declaring theorems of the form P=Q to
   829 the rewriter and classical reasoner simultaneously;
   830 
   831 * function uresult no longer returns theorems in "standard" format;
   832 regain previous version by: val uresult = standard o uresult;
   833 
   834 
   835 
   836 New in Isabelle94-6
   837 -------------------
   838 
   839 * oracles -- these establish an interface between Isabelle and trusted
   840 external reasoners, which may deliver results as theorems;
   841 
   842 * proof objects (in particular record all uses of oracles);
   843 
   844 * Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;
   845 
   846 * "constdefs" section in theory files;
   847 
   848 * "primrec" section (HOL) no longer requires names;
   849 
   850 * internal type "tactic" now simply "thm -> thm Sequence.seq";
   851 
   852 
   853 
   854 New in Isabelle94-5
   855 -------------------
   856 
   857 * reduced space requirements;
   858 
   859 * automatic HTML generation from theories;
   860 
   861 * theory files no longer require "..." (quotes) around most types;
   862 
   863 * new examples, including two proofs of the Church-Rosser theorem;
   864 
   865 * non-curried (1994) version of HOL is no longer distributed;
   866 
   867 
   868 
   869 New in Isabelle94-4
   870 -------------------
   871 
   872 * greatly reduced space requirements;
   873 
   874 * theory files (.thy) no longer require \...\ escapes at line breaks;
   875 
   876 * searchable theorem database (see the section "Retrieving theorems" on
   877 page 8 of the Reference Manual);
   878 
   879 * new examples, including Grabczewski's monumental case study of the
   880 Axiom of Choice;
   881 
   882 * The previous version of HOL renamed to Old_HOL;
   883 
   884 * The new version of HOL (previously called CHOL) uses a curried syntax
   885 for functions.  Application looks like f a b instead of f(a,b);
   886 
   887 * Mutually recursive inductive definitions finally work in HOL;
   888 
   889 * In ZF, pattern-matching on tuples is now available in all abstractions and
   890 translates to the operator "split";
   891 
   892 
   893 
   894 New in Isabelle94-3
   895 -------------------
   896 
   897 * new infix operator, addss, allowing the classical reasoner to
   898 perform simplification at each step of its search.  Example:
   899         fast_tac (cs addss ss)
   900 
   901 * a new logic, CHOL, the same as HOL, but with a curried syntax
   902 for functions.  Application looks like f a b instead of f(a,b).  Also pairs
   903 look like (a,b) instead of <a,b>;
   904 
   905 * PLEASE NOTE: CHOL will eventually replace HOL!
   906 
   907 * In CHOL, pattern-matching on tuples is now available in all abstractions.
   908 It translates to the operator "split".  A new theory of integers is available;
   909 
   910 * In ZF, integer numerals now denote two's-complement binary integers.
   911 Arithmetic operations can be performed by rewriting.  See ZF/ex/Bin.ML;
   912 
   913 * Many new examples: I/O automata, Church-Rosser theorem, equivalents
   914 of the Axiom of Choice;
   915 
   916 
   917 
   918 New in Isabelle94-2
   919 -------------------
   920 
   921 * Significantly faster resolution;
   922 
   923 * the different sections in a .thy file can now be mixed and repeated
   924 freely;
   925 
   926 * Database of theorems for FOL, HOL and ZF.  New
   927 commands including qed, qed_goal and bind_thm store theorems in the database.
   928 
   929 * Simple database queries: return a named theorem (get_thm) or all theorems of
   930 a given theory (thms_of), or find out what theory a theorem was proved in
   931 (theory_of_thm);
   932 
   933 * Bugs fixed in the inductive definition and datatype packages;
   934 
   935 * The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs
   936 and HOL_dup_cs obsolete;
   937 
   938 * Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1
   939 have been removed;
   940 
   941 * Simpler definition of function space in ZF;
   942 
   943 * new results about cardinal and ordinal arithmetic in ZF;
   944 
   945 * 'subtype' facility in HOL for introducing new types as subsets of existing
   946 types;
   947 
   948 
   949 $Id$