# HG changeset patch # User wenzelm # Date 969047394 -7200 # Node ID bd2ef19a0275c55b91fbe4e999ab3750d89eda01 # Parent aaaca09b18de6a8346b3ab28baa4eab763491bc8 cleaned up and prepared for Isabelle99-1; diff -r aaaca09b18de -r bd2ef19a0275 NEWS --- a/NEWS Fri Sep 15 20:47:06 2000 +0200 +++ b/NEWS Fri Sep 15 21:49:54 2000 +0200 @@ -2,10 +2,10 @@ Isabelle NEWS -- history user-relevant changes ============================================== -New in this Isabelle version ----------------------------- +New in Isabelle99-1 (September 2000) +------------------------------------ -*** Overview of INCOMPATIBILITIES (see below for more details) *** +*** 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) @@ -14,40 +14,43 @@ Delsimprocs Nat_Numeral_Simprocs.cancel_numerals; Delsimprocs [Nat_Numeral_Simprocs.combine_numerals]; -* HOL: 0 is now overloaded, so the type constraint ::nat may sometimes be -needed; +* HOL: simplification no longer dives into case-expressions; + +* 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; -* HOL: the constant for f``x is now "image" rather than "op ``"; + 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 disjoint sum is now "<+>" instead of "Plus"; the cartesian product is now "<*>" instead of "Times"; the lexicographic product is now "<*lex*>" instead of "**"; -* HOL: exhaust_tac on datatypes superceded by new generic case_tac; - -* HOL: simplification no longer dives into case-expressions; - -* HOL: the recursion equations generated by 'recdef' are now called -f.simps instead of f.rules; - -* HOL: theory Sexp now in HOL/Induct examples (it used to be part of -main HOL, but was unused); it is better to use HOL's datatype package -anyway; - -* HOL: removed obsolete theorem binding expand_if (refer to split_if -instead); - -* HOL: less_induct is renamed nat_less_induct - -* HOL: systematic renaming of the @-rules: - selectI -> someI - selectI2 -> someI2 - selectI2EX -> someI2_ex - select_equality -> some_equality - select1_equality -> some1_equality - select_eq_Ex -> some_eq_ex - Eps_eq -> some_eq_trivial - Eps_sym_eq -> some_sym_eq_trivial +* 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/Real: "rabs" replaced by overloaded "abs" function; @@ -55,48 +58,26 @@ Lfp, Gfp, WF); this only affects ML packages that refer to const names internally; -* HOL, ZF: syntax for quotienting wrt an equivalence relation changed -from A/r to A//r; +* HOL and ZF: syntax for quotienting wrt an equivalence relation +changed from A/r to A//r; -* HOL: qed_spec_mp now also removes bounded ALL; +* ZF: new treatment of arithmetic (nat & int) may break some old +proofs; -* 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: changed syntax of local blocks from {{ }} to { }; - -* Isar: renamed 'RS' attribute to 'THEN'; - -* Isar: renamed some attributes (rulify -> rule_format, elimify -> elim_format, ...); - * Isar/HOL: renamed "intrs" to "intros" in inductive definitions; * Provers: strengthened force_tac by using new first_best_tac; -* 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: safe_asm_full_simp_tac is no longer in the simplifier signature. Use - val safe_asm_full_simp_tac = generic_simp_tac true (true,true,true); - if required. - -* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global -timing flag supersedes proof_timing and Toplevel.trace; - -* ML: PureThy.add_thms/add_axioms/add_defs return theorems as well; - -* ML: PureThy.add_defs gets additional argument to indicate potential -overloading (usually false); - -* LaTeX: several changes of isabelle.sty; +* LaTeX document preparation: several changes of isabelle.sty (see +lib/texinputs); *** Document preparation *** @@ -114,7 +95,8 @@ of isatool usedir; * isatool usedir -D now lets isatool latex -o sty update the Isabelle -style files, achieving self-contained LaTeX sources; +style files, achieving self-contained LaTeX sources and simplifying +LaTeX debugging; * old-style theories now produce (crude) LaTeX output as well; @@ -122,139 +104,140 @@ on WWW server seperately); improved graphs of nested sessions; removed graph for 'all sessions'; -* several improvements in isabelle.sty; \isabellestyle{it} produces -near math mode output; \isamarkupheader is now \section by default; +* 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 *** -* Pure: local results and corresponding term bindings are now subject -to Hindley-Milner polymorphism (similar to ML); this accommodates -incremental type-inference nicely; +* 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; -* Pure: new derived language element 'obtain' supports generalized -existence reasoning; +* Isar/Pure: new derived language element 'obtain' supports +generalized existence reasoning; -* Pure: new calculational elements 'moreover' and 'ultimately' support -accumulation of results, without applying any rules yet; +* 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; -* 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: 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"; -* Pure: theory command 'hide' removes declarations from +* Isar/Pure: theory command 'hide' removes declarations from class/type/const name spaces; -* Pure: theory command 'defs' supports option "(overloaded)" to +* Isar/Pure: theory command 'defs' supports option "(overloaded)" to indicate potential overloading; -* Pure: changed syntax of local blocks from {{ }} to { }; - -* Pure: renamed 'RS' attribute to 'THEN'; - -* Pure: syntax of sorts made 'inner', i.e. have to write "{a, b, c}" -instead of {a, b, c}; - -* 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: changed syntax of local blocks from {{ }} to { }; -* Pure: the local context of (non-atomic) goals is provided via case -name 'antecedent'; - -* Pure: removed obsolete 'transfer' attribute (transfer of thms to the -current context is now done automatically); +* Isar/Pure: syntax of sorts made 'inner', i.e. have to write +"{a,b,c}" instead of {a,b,c}; -* Pure: theory command 'method_setup' provides a simple interface for -definining proof methods in ML; - -* Provers: 'simp' method now supports 'cong' modifiers; - -* Provers: hypsubst support; also plain subst and symmetric attribute -(the latter supercedes [RS sym]); +* 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; -* Provers: splitter support (via 'split' attribute and 'simp' method -modifier); 'simp' method: 'only:' modifier removes loopers as well -(including splits); - -* Provers: added 'fastsimp' and 'clarsimp' methods (combination of -Simplifier and Classical reasoner); - -* Provers: added 'arith_split' attribute; - -* 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/Pure: the local context of (non-atomic) goals is provided via +case name 'antecedent'; -* HOL: removed 'case_split' thm binding, should use 'cases' proof -method anyway; - -* HOL: removed obsolete 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/Pure: removed obsolete 'transfer' attribute (transfer of thms +to the current context is now done automatically); -* HOL/Calculation: new rules for substitution in inequalities -(monotonicity conditions are extracted to be proven at end); +* Isar/Pure: theory command 'method_setup' provides a simple interface +for definining proof methods in ML; -* HOL/inductive: rename "intrs" to "intros" (potential -INCOMPATIBILITY); emulation of mk_cases feature for proof scripts: -'inductive_cases' command and 'ind_cases' method; NOTE: use (cases -(simplified)) method in proper proofs; - -* Provers: intro/elim/dest attributes changed; renamed +* 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"; -* names of theorems etc. may be natural numbers as well; +* 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; -* 'pr' command: optional arguments for goals_limit and +* 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; -* diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit +* 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; -* improved support for emulating tactic scripts, including proof +* 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); -* 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: 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; -* tuned 'let' syntax: replaced 'as' keyword by 'and'; +* Isar: tuned 'let' syntax: replaced 'as' keyword by 'and'; -* removed 'help' command, which hasn't been too helpful anyway; should -instead use individual commands for printing items (print_commands, -print_methods etc.); +* Isar: removed 'help' command, which hasn't been too helpful anyway; +should instead use individual commands for printing items +(print_commands, print_methods etc.); -* added 'nothing' --- the empty list of theorems; +* Isar: added 'nothing' --- the empty list of theorems; *** HOL *** -* HOL/Lambda: converted into new-style theory and document; - * HOL/Algebra: new theory of rings and univariate polynomials, by Clemens Ballarin; -* HOL/ex: new theory Factorization proving the Fundamental Theorem of -Arithmetic, by Thomas M Rasmussen; - -* HOL/ex/Multiquote: multiple nested quotations and anti-quotations -- -basically a generalized version of de-Bruijn representation; very -useful in avoiding lifting of operations; +* HOL/NumberTheory: Fundamental Theorem of Arithmetic, Chinese +Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, by Thomas M +Rasmussen; -* HOL/NumberTheory: Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's -Theorem, by Thomas M Rasmussen; +* HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog, by David +von Oheimb; -* HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog; +* HOL/Lambda: converted into new-style theory and document; -* HOL/Real: "rabs" replaced by overloaded "abs" function; +* 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 @@ -266,7 +249,7 @@ * HOL: new axclass plus_ac0 for addition with the AC-laws and 0 as identity. Types nat and int belong to this axclass; -* greatly improved simplification involving numerals of type nat, int, real: +* 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 @@ -274,9 +257,9 @@ 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. For examples of - what it can do, see ex/mesontest.ML and ex/mesontest2.ML; +* 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 @@ -286,7 +269,7 @@ selector expression is simplified, but not the remaining arms. To enable full simplification of case-expressions for datatype t, you need to remove t.weak_case_cong from the simpset, either permanently -(Delcongs[thm"t.weak_case_cong"];) or locally (delcongs [...]). +(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 @@ -300,58 +283,68 @@ 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: 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"; -* new tactic induct_thm_tac: thm -> string -> int -> tactic +* 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; -* new functions rulify/rulify_no_asm: thm -> thm for turning outer --->/All/Ball into ==>/!!; qed_spec_mp now uses rulify_no_asm; +* HOL/Real: "rabs" replaced by overloaded "abs" function; -* theory Sexp now in HOL/Induct examples (it used to be part of main -HOL, but was unused); +* HOL: theory Sexp now in HOL/Induct examples (it used to be part of +main HOL, but was unused); -* fewer consts declared as global (e.g. have to refer to "Lfp.lfp" -instead of "lfp" internally; affects ML packages only); +* HOL: fewer consts declared as global (e.g. have to refer to +"Lfp.lfp" instead of "lfp" internally; affects ML packages only); -* tuned AST representation of nested pairs, avoiding bogus output in -case of overlap with user translations (e.g. judgements over tuples); +* 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 *** -* simplification automatically cancels common terms in arithmetic expressions -over nat and int; +* ZF: simplification automatically cancels common terms in arithmetic +expressions over nat and int; -* 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; - -* as above, for int: operators coerce their operands to an integer using the -function intify; +* 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; -* the integer library now contains many of the usual laws for the orderings, -including $<=, and monotonicity laws for $+ and $*; +* ZF: as above, for int: operators coerce their operands to an integer +using the function intify; -* new example ZF/ex/NatSum to demonstrate integer arithmetic simplification; +* ZF: the integer library now contains many of the usual laws for the +orderings, including $<=, and monotonicity laws for $+ and $*; -*** FOL & ZF *** +* ZF: new example ZF/ex/NatSum to demonstrate integer arithmetic +simplification; -* AddIffs now available, giving theorems of the form P<->Q to the -simplifier and classical reasoner simultaneously; +* 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 handles actual object-logic rules as -assumptions; note that auto(_tac) uses blast(_tac) internally as well; +* 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; @@ -361,6 +354,10 @@ * 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); @@ -370,21 +367,20 @@ * system: provide TAGS file for Isabelle sources; -* settings: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, and -XSYMBOL_HOME; no longer need to do manual configuration in most -situations; - * 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: new combinators |>> and |>>> for incremental transformations -with secondary results (e.g. certain theory extensions): +* ML: PureThy.add_thms/add_axioms/add_defs now return theorems as +results;