Isabelle NEWS -- history user-relevant changes

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

New in Isabelle2001 (?? 2001)

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

*** Document preparation ***

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

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

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

better in printed text;

*** Isar ***

* renamed "antecedent" case to "rule_context";

* improved proof by cases and induction:

  - moved induct/cases attributes to Pure;

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

  - generic setup instantiated for FOL and HOL;

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

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

"(permissive)" option to recover old behavior;

* HOL: 'inductive' now longer features separate (collective)

attributes for 'intros';

*** HOL ***

* 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: eliminated global items

  const "()" -> "Product_Type.Unity"

  type "unit" -> "Product_Type.unit"

*** ZF ***

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

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

*** General ***

* Meta-level proof terms (by Stefan Berghofer), see also ref manual;

* 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;

* Classical reasoner: renamed addaltern to addafter, addSaltern to

addSafter;

* syntax: support non-oriented infixes;

* print modes "type_brackets" and "no_type_brackets" control output of

nested => (types); the default behavior is "brackets";

* 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-Hyperreal: a new target, extending HOL-Real with the hyperreals

and Fleuriot's mechanization of analysis;

* 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

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

result still apply;

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

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

*** HOL ***

** HOL arithmetic **

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

int:

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

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

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

are ignored; quantified subformulae are ignored unless they are

positive universal or negative existential. The tactic has to be

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

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

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

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

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

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

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

simplifier.

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

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

int(m) < int(n)'.

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

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

INCOMPATIBILITY: since numeral syntax is now polymorphic, rather than

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

type constraints;

* integer division and remainder can now be performed on constant

arguments;

* many properties of integer multiplication, division and remainder

are now available;

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

tactic svc_tac.  Propositional tautologies and theorems of linear arithmetic

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

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

invocation of the underlying oracle).  For SVC see

  http://verify.stanford.edu/SVC

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

** HOL misc **

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

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

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

analysis for assembly languages with subtypes;

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

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

temporal levels more uniformly; introduces INCOMPATIBILITIES due to

changed syntax and (many) tactics;

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

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

  theorems are now maintained within the theory (maintained via the

  "mono" attribute);

* HOL/datatype: Now also handles arbitrarily branching datatypes

  (using function types) such as

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

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

of selectors applied to updated records; record_split_tac is no longer

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

simpset in many cases; COMPATIBILITY: old behavior achieved by

  claset_ref () := claset() addSWrapper record_split_wrapper;

  Delsimprocs [record_simproc]

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

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

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

names rather than an ML expression;

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

supplied later.  Program schemes can be defined, such as

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

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

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

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

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

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

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

the original Gordon/HOL-style output;

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

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

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

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

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

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

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

thus available for user theories;

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

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

time;

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

several times and then mp;

*** LK ***

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

formulas;

* the simplifier is now installed

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

* the classical reasoner now has a default rule database

*** ZF ***

* new primrec section allows primitive recursive functions to be given

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

* new tactics induct_tac and exhaust_tac for induction (or case

analysis) over datatypes and the natural numbers;

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

* simplification automatically does freeness reasoning for datatype

constructors;

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

type-checking rules;

* datatype introduction rules are now added as Safe Introduction rules

to the claset;

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

if(P,x,y);

*** Internal programming interfaces ***

* tuned simplifier trace output; new flag debug_simp;

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

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

* AxClass.axclass_tac lost the theory argument;

* tuned current_goals_markers semantics: begin / end goal avoids

printing empty lines;