Isabelle NEWS -- history user-relevant changes

==============================================

New in Isabelle2001 (?? 2001)

-----------------------------

*** Document preparation ***

* greatly simplified document preparation setup, including more

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

instructive isatool mkdir; users should basically be able to get

started with "isatool mkdir Test && isatool make";

* theory dependency graph may now be incorporated into documents;

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

with \includegraphics of LaTeX;

* proper spacing of consecutive markup elements, especially text

blocks after section headings;

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

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

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

better in printed text;

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

note that these symbols are currently unavailable in Proof General /

X-Symbol;

*** Isar ***

* improved proof by cases and induction:

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

  - added 'print_induct_rules' (covered by help item in Proof General > 3.3);

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

  - generic method setup instantiated for FOL and HOL;

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

"case (Suc n)");

  - 'induct' method divinates rule instantiation from the inductive

claim; no longer requires excessive ?P bindings for proper

instantiation of cases;

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

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

without further ado;

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

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

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

statement becomes is included in the hypothesis, avoiding the slightly

cumbersome show "PROP ?case" form;

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

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

rules stemming from inductive sets to be applied in unstructured

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

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

rest of the goal is passed through the induction;

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

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

below);

* Pure: support multiple simultaneous goal statements, for example

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

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

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

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

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

fails:

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

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

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

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

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

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

attributes everywhere);

* Pure: theory goals now support ad-hoc contexts, which are discharged

in the result, as in ``lemma (assumes A and B) K: A .''; syntax

coincides with that of a locale body;

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

* Pure: added 'corollary' command;

* Pure: fixed 'token_translation' command;

* Pure: removed obsolete 'exported' attribute;

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

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

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

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

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

rewrite rules declarations of 'atomize' attribute; example

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

proof *scripts*;

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

now consider the syntactic context of assumptions, giving a better

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

especially important for locales);

* Provers: 'simplified' attribute may refer to explicit rules instead

of full simplifier context; 'iff' attribute handles conditional rules;

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

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

"(permissive)" option to recover old behavior;

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

for 'intros' (was found too confusing);

*** HOL ***

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

follows:

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

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

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

  binary representation internally;

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

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

This change may cause significant INCOMPATIBILITIES; here are some

hints on converting existing sources:

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

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

  to be spaced properly;

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

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

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

  - remove all special provisions on numerals in proofs;

* HOL/record:

  - removed old "make" and "make_scheme" operations -- INCOMPATIBILITY;

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

  - provides cases/induct rules for use with corresponding Isar

    methods (for concrete records, record schemes, concrete more

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

  - new derived operations "make" (for adding fields of current

    record), "extend" to promote fixed record to record scheme, and

    "truncate" for the reverse; cf. theorems "derived_defs", which are

    *not* declared as simp by default;

  - internal definitions directly based on a light-weight abstract

    theory of product types over typedef rather than datatype;

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

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

(beware of argument permutation!);

* HOL: linorder_less_split superseded by linorder_cases;

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

to peripheral theory "Hilbert_Choice";

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

in this (rare) case use:

  delSWrapper "split_all_tac"

  addSbefore ("unsafe_split_all_tac", unsafe_split_all_tac)

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

MAY FAIL;

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

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

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

necessary to attach explicit type constraints;

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

expressions;

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

Florian Kammüller;

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

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

renamed "Product_Type.unit";

*** HOLCF ***

* proper rep_datatype lift (see theory Lift); use plain induct_tac

instead of former lift.induct_tac; always use UU instead of Undef;

* 'domain' package adapted to new-style theories, e.g. see

HOLCF/ex/Dnat.thy;

*** ZF ***

* ZF: new-style theory commands '(co)inductive', '(co)datatype',

'rep_datatype', 'inductive_cases'; also methods 'ind_cases',

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

* ZF: the integer library now covers quotients and remainders, with

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

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

including theory Multiset for multiset orderings;

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

typeless version of the formalism;

*** General ***

* kernel: meta-level proof terms (by Stefan Berghofer), see also ref

manual;

* Pure/axclass: removed obsolete ML interface goal_subclass/goal_arity;

* classical: renamed addaltern to addafter, addSaltern to addSafter;

* clasimp: ``iff'' declarations now handle conditional rules as well;

* syntax: new token syntax "num" for plain numerals (without "#" of

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

tokens, so expressions involving minus need to be spaced properly;

* syntax: support non-oriented infixes;

* syntax: print modes "type_brackets" and "no_type_brackets" control

output of nested => (types); the default behavior is "type_brackets";

* syntax: builtin parse translation for "_constify" turns valued

tokens into AST constants;

* syntax: prefer later print_translation functions; potential

INCOMPATIBILITY: need to reverse declarations of multiple translation

functions for same constant;

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

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

iso-latin characters may now be used;

* system: support Poly/ML 4.1.1 (now able to manage large heaps);

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

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

* system: smart selection of Isabelle process versus Isabelle

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

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

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

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

New in Isabelle99-2 (February 2001)

-----------------------------------

*** Overview of INCOMPATIBILITIES ***

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

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

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

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

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

format may be recovered via ML function complete_split_rule or attribute

'split_rule (complete)';

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

gfp_Tarski to gfp_unfold;

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

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

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

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

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

operation;

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

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

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

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

(which is now passed through the inductive cases);

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

\<gg> to \<ggreater>;

*** Document preparation ***

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

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

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

\isabellestyle command is given, output is according to slanted

type-writer);

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

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

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

the complete list of symbols defined in isabellesym.sty;

* improved isabelle style files; more abstract symbol implementation

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

definitions);

* antiquotation @{goals} and @{subgoals} 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!

* proper indentation of antiquoted output with proportional LaTeX

fonts;

* no_document ML operator temporarily disables LaTeX document

generation;

* isatool unsymbolize tunes sources for plain ASCII communication;

*** Isar ***

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

schematic variables (this does not conform to actual readable proof

documents, due to unpredictable outcome and non-compositional proof

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

for Prolog-style synthesis of proven results;

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

rules as well;

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

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

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

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

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

instance proofs may be performed by "..";

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

statements as well;

* Pure: more robust selection of calculational rules;

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

rule (as well as the assumption rule);

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

lemmas, using the graph browser tool;

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

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

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

(potential INCOMPATIBILITY); tuned error handling;

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

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

any remaining facts are inserted into the goal verbatim;

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

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

the result to be shown in each case;

* HOL: added 'recdef_tc' command;

* isatool convert assists in eliminating legacy ML scripts;

*** HOL ***

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

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

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

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

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

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

modelling and verification task performed in Isabelle/HOL +

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

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

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

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

'domain', this makes the theory consistent with mathematical

literature;

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

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

operator \<Sum>;

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

HOL/subset.thy);

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

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

require atomize_strip_tac to cope with non-atomic premises);

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

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

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

rules with string literals);

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

 and Fleuriot's mechanization of analysis, including the transcendental

 functions for the reals;

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

*** CTT ***

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

"lam" is displayed as TWO lambda-symbols

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

and Arith);

*** General ***

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

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

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

the Isabelle inference kernel has been greatly improved;

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

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

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

as assumptions as well;

* system: support Poly/ML 4.0;

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

New in Isabelle99-1 (October 2000)

----------------------------------

*** Overview of INCOMPATIBILITIES ***

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

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

issue the following ML commands:

  Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;

  Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];

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

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

* HOL: nat_less_induct renamed to less_induct;

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

fixsome to patch .thy and .ML sources automatically;

  select_equality  -> some_equality

  select_eq_Ex     -> some_eq_ex

  selectI2EX       -> someI2_ex

  selectI2         -> someI2

  selectI          -> someI

  select1_equality -> some1_equality

  Eps_sym_eq       -> some_sym_eq_trivial

  Eps_eq           -> some_eq_trivial

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

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

instead);

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

f.simps instead of f.rules;

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

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

sometimes be needed;

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

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

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

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

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

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

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

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

the old syntax may be recovered as follows:

  syntax (symbols)

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

      (infixl "\\<oplus>" 100)

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

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

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

internally;

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

changed from A/r to A//r;

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

proofs;

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

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

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

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

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

"rule del";

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

* Provers: strengthened force_tac by using new first_best_tac;

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

lib/texinputs);

*** Document preparation ***

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

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

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

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

* isatool mkdir provides easy setup of Isabelle session directories,

including proper document sources;

* generated LaTeX sources are now deleted after successful run

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

of isatool usedir;

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

style files, achieving self-contained LaTeX sources and simplifying

LaTeX debugging;

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

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

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

graph for 'all sessions';

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

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

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

*** Isar ***

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

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

accommodates incremental type-inference very nicely;

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

generalized existence reasoning;

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

support accumulation of results, without applying any rules yet;

useful to collect intermediate results without explicit name

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

premises;

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

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

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

to theorems as "tags";

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

class/type/const name spaces;

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

indicate potential overloading;

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

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

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

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

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

with the version in Provers/classical;

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

case name 'antecedent';

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

to the current context is now done automatically);

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

for definining proof methods in ML;

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

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

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

replaced "delrule" by "rule del";

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

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

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

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

well (including splits);

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

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

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

of Simplifier and Classical reasoner);

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

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

recdef) support case names and properly name parameters;

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

monotonicity conditions are extracted to be proven at end of

calculations;

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

method anyway;

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

split_if split_if_asm; datatype package provides theorems foo.splits =

foo.split foo.split_asm for each datatype;

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

(potential INCOMPATIBILITY), emulation of mk_cases feature for proof

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

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

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

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

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

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

proof states;

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

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

proof state according to the Isabelle LaTeX style;

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

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

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

(for HOL datatypes);

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

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

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

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

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

should instead use individual commands for printing items

(print_commands, print_methods etc.);

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

*** HOL ***

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

corresponding virtual machine and a specification of its bytecode

verifier and a lightweight bytecode verifier, including proofs of

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

Cornelia Pusch (see also the homepage of project Bali at

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

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

Clemens Ballarin;

* HOL/NumberTheory: fundamental Theorem of Arithmetic, Chinese

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

Rasmussen;

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

structures, including duals, properties of bounds versus algebraic

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

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

for abstract algebraic reasoning using axiomatic type classes, and

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

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

von Oheimb;

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

recursive procedures, by David von Oheimb;

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

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

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

representation; very useful in avoiding lifting of operations;

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

select-update simplification procedure to handle extended records as

well; admit "r" as field name;

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

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

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

Types nat and int belong to this axclass;

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

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

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

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

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

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

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

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

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

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

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

"exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer

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

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

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

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

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

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

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

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

termination conditions are proved automatically, these simplification

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

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

each equation;

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

permits the definition of tail-recursive functions without the

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

invariant proof rule for while is applied.

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

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

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

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

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

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

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

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

main HOL, but was unused);

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

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

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

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

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

bogus);

*** ZF ***

* ZF: simplification automatically cancels common terms in arithmetic

expressions over nat and int;

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

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

making the algebraic laws unconditional;

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

using the function intify;

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

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

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

simplification;

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

to the simplifier and classical reasoner simultaneously;

*** General ***

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

assumptions; note that auto_tac uses blast_tac internally as well;

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

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

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

explicit make_elim);

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

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

use instead the strong form,

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

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

from destruct-rules;

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

Simplifier setup for new object-logics;

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

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

for hiding of names;

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

XSYMBOL_HOME; no longer need to do manual configuration in most

situations;

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

option of isabelle and isatool usedir (currently only observed by

Poly/ML);

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

useful for remote X11);

* system: provide TAGS file for Isabelle sources;

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

order;

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

timing flag supersedes proof_timing and Toplevel.trace;

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

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

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

overloading (usually false);

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

results;

New in Isabelle99 (October 1999)

--------------------------------

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

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

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

functional programs.)  To restore the old behaviour, declare

    Delcongs [if_weak_cong];

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

complement;

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

* HOL/datatype: mutual_induct_tac no longer exists --

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

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

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

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

to constants declared in the same theory;

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

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

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

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

* Simplifier: the type of the infix ML functions

        setSSolver addSSolver setSolver addSolver

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

for packaging solvers. A solver is created via

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

where the string argument is only a comment.

*** Proof tools ***

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

decision procedure for linear arithmetic. Currently it is used for

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

will be instantiated for other types and logics as well.

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

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

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

  matching.

*** General ***

* New Isabelle/Isar subsystem provides an alternative to traditional

tactical theorem proving; together with the ProofGeneral/isar user

interface it offers an interactive environment for developing human

readable proof documents (Isar == Intelligible semi-automated

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

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

* improved and simplified presentation of theories: better HTML markup

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

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

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

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

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

Isabelle/Isar;

* ML function thm_deps visualizes dependencies of theorems and lemmas,

using the graph browser tool;

* Isabelle manuals now also available as PDF;

* theory loader rewritten from scratch (may not be fully

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

add_path, del_path, reset_path functions; new operations such as

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

isatool doc ref);

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

option -p DIR installs standalone binaries;

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

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

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

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

Isabelle;

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

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

empty;

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

long arrows);

* new print_mode "HTML";

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

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

* Isamode 2.6 requires patch to accomodate change of Isabelle font

mode and goal output format:

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

244c244

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

---

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

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

181c181

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

---

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

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

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

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