# HG changeset patch # User wenzelm # Date 909052015 -7200 # Node ID 5de7e399ec88f920a4cfd79c5c09468d83609f71 # Parent 26772f4543fc520e913a7916f1e945d641c2e5f8 tuned; record package; diff -r 26772f4543fc -r 5de7e399ec88 NEWS --- a/NEWS Thu Oct 22 11:09:43 1998 +0200 +++ b/NEWS Thu Oct 22 12:26:55 1998 +0200 @@ -1,3 +1,4 @@ + Isabelle NEWS -- history user-relevant changes ============================================== @@ -6,26 +7,26 @@ *** Overview of INCOMPATIBILITIES (see below for more details) *** -* several changes of proof tools; - -* HOL: new version of inductive and datatype; +* several changes of automated proof tools; -* HOL: major changes to the inductive and datatype packages; +* HOL: major changes to the inductive and datatype packages, including +some minor incompatibilities of theory syntax; -* HOL: renamed r^-1 to 'converse' from 'inverse'; `inj_onto' is now +* HOL: renamed r^-1 to 'converse' from 'inverse'; 'inj_onto' is now called `inj_on'; * HOL: removed duplicate thms in Arith: less_imp_add_less should be replaced by trans_less_add1 le_imp_add_le should be replaced by trans_le_add1 -* HOL: unary - is now overloaded (new type constraints may be required); +* HOL: unary minus is now overloaded (new type constraints may be +required); -* HOL and ZF: unary minus for integers is now #- instead of #~. In ZF, - expressions such as n#-1 must be changed to n#- 1, since #-1 is now taken - as an integer constant. +* HOL and ZF: unary minus for integers is now #- instead of #~. In +ZF, expressions such as n#-1 must be changed to n#- 1, since #-1 is +now taken as an integer constant. -* Pure: ML function 'theory_of' replaced by 'theory'; +* Pure: ML function 'theory_of' renamed to 'theory'; *** Proof tools *** @@ -53,44 +54,43 @@ getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; * Classical reasoner: addbefore/addSbefore now have APPEND/ORELSE - semantics; addbefore now affects only the unsafe part of step_tac - etc.; this affects addss/auto_tac/force_tac, so EXISTING PROOFS MAY - FAIL, but proofs should be fixable easily, e.g. by replacing - Auto_tac by Force_tac; +semantics; addbefore now affects only the unsafe part of step_tac +etc.; this affects addss/auto_tac/force_tac, so EXISTING PROOFS MAY +FAIL, but proofs should be fixable easily, e.g. by replacing Auto_tac +by Force_tac; -* Classical reasoner: setwrapper to setWrapper and compwrapper to compWrapper; - added safe wrapper (and access functions for it); +* Classical reasoner: setwrapper to setWrapper and compwrapper to +compWrapper; added safe wrapper (and access functions for it); * HOL/split_all_tac is now much faster and fails if there is nothing -to split. Existing (fragile) proofs may require adaption because the -order and the names of the automatically generated variables have -changed. split_all_tac has moved within claset() from unsafe wrappers -to safe wrappers, which means that !!-bound variables are split much -more aggressively, and safe_tac and clarify_tac now split such -variables. If this splitting is not appropriate, use delSWrapper -"split_all_tac". - -* HOL/Simplifier: +to split. Some EXISTING PROOFS MAY REQUIRE ADAPTION because the order +and the names of the automatically generated variables have changed. +split_all_tac has moved within claset() from unsafe wrappers to safe +wrappers, which means that !!-bound variables are split much more +aggressively, and safe_tac and clarify_tac now split such variables. +If this splitting is not appropriate, use delSWrapper "split_all_tac". +Note: the same holds for record_split_tac, which does the job of +split_all_tac for record fields. - - Rewrite rules for case distinctions can now be added permanently to - the default simpset using Addsplits just like Addsimps. They can be - removed via Delsplits just like Delsimps. Lower-case versions are - also available. +* HOL/Simplifier: Rewrite rules for case distinctions can now be added +permanently to the default simpset using Addsplits just like +Addsimps. They can be removed via Delsplits just like +Delsimps. Lower-case versions are also available. - - The rule split_if is now part of the default simpset. This means - that the simplifier will eliminate all occurrences of if-then-else - in the conclusion of a goal. To prevent this, you can either remove - split_if completely from the default simpset by `Delsplits - [split_if]' or remove it in a specific call of the simplifier using - `... delsplits [split_if]'. You can also add/delete other case - splitting rules to/from the default simpset: every datatype - generates suitable rules `split_t_case' and `split_t_case_asm' - (where t is the name of the datatype). +* HOL/Simplifier: The rule split_if is now part of the default +simpset. This means that the simplifier will eliminate all occurrences +of if-then-else in the conclusion of a goal. To prevent this, you can +either remove split_if completely from the default simpset by +`Delsplits [split_if]' or remove it in a specific call of the +simplifier using `... delsplits [split_if]'. You can also add/delete +other case splitting rules to/from the default simpset: every datatype +generates suitable rules `split_t_case' and `split_t_case_asm' (where +t is the name of the datatype). -* Classical reasoner - Simplifier combination: new force_tac (and +* Classical reasoner / Simplifier combination: new force_tac (and derivatives Force_tac, force) combines rewriting and classical reasoning (and whatever other tools) similarly to auto_tac, but is -aimed to solve the given subgoal completely; +aimed to solve the given subgoal completely. *** General *** @@ -123,6 +123,8 @@ * print mode 'emacs' reserved for Isamode; +* support multiple print (ast) translations per constant name; + *** HOL *** @@ -193,9 +195,33 @@ scripts to the new package (backup your sources first!). -* HOL/record package: now includes concrete syntax for record types, -terms, updates; still lacks important theorems, like surjective -pairing and split; +* HOL/record package: considerably improved implementation; now +includes concrete syntax for record types, terms, updates; theorems +for surjective pairing and splitting !!-bound record variables; proof +support is as follows: + + 1) standard conversions (selectors or updates applied to record +constructor terms) are part of the standard simpset; + + 2) inject equations of the form ((x, y) = (x', y')) == x=x' & y=y' are +made part of standard simpset and claset via addIffs; + + 3) a tactic for record field splitting (record_split_tac) is part of +the standard claset (addSWrapper); + +To get a better idea about these rules you may retrieve them via +something like 'thms "foo.simps"' or 'thms "foo.iffs"', where "foo" is +the name of your record type. + +The split tactic 3) conceptually simplifies by the following rule: + + "(!!x. PROP ?P x) == (!!a b. PROP ?P (a, b))" + +Thus any record variable that is bound by meta-all will automatically +blow up into some record constructor term, consequently the +simplifications of 1), 2) apply. Thus force_tac, auto_tac etc. shall +solve record problems automatically. + * reorganized the main HOL image: HOL/Integ and String loaded by default; theory Main includes everything; @@ -450,7 +476,7 @@ *** HOL *** -* HOL: there is a new splitter `split_asm_tac' that can be used e.g. +* HOL: there is a new splitter `split_asm_tac' that can be used e.g. with `addloop' of the simplifier to faciliate case splitting in premises. * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions; @@ -544,7 +570,7 @@ *** FOL and ZF *** -* FOL: there is a new splitter `split_asm_tac' that can be used e.g. +* FOL: there is a new splitter `split_asm_tac' that can be used e.g. with `addloop' of the simplifier to faciliate case splitting in premises. * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as @@ -602,7 +628,7 @@ some limitations. Blast_tac... + ignores addss, addbefore, addafter; this restriction is intrinsic + ignores elimination rules that don't have the correct format - (the conclusion MUST be a formula variable) + (the conclusion MUST be a formula variable) + ignores types, which can make HOL proofs fail + rules must not require higher-order unification, e.g. apply_type in ZF [message "Function Var's argument not a bound variable" relates to this] @@ -615,12 +641,12 @@ setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper (and access functions for it); -* improved combination of classical reasoner and simplifier: +* improved combination of classical reasoner and simplifier: + functions for handling clasimpsets + improvement of addss: now the simplifier is called _after_ the safe steps. + safe variant of addss called addSss: uses safe simplifications - _during_ the safe steps. It is more complete as it allows multiple + _during_ the safe steps. It is more complete as it allows multiple instantiations of unknowns (e.g. with slow_tac). *** Simplifier *** @@ -676,8 +702,8 @@ * HOLCF/IOA replaces old HOL/IOA; -* HOLCF changes: derived all rules and arities - + axiomatic type classes instead of classes +* HOLCF changes: derived all rules and arities + + axiomatic type classes instead of classes + typedef instead of faking type definitions + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc. + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po @@ -765,7 +791,7 @@ * theory files (.thy) no longer require \...\ escapes at line breaks; -* searchable theorem database (see the section "Retrieving theorems" on +* searchable theorem database (see the section "Retrieving theorems" on page 8 of the Reference Manual); * new examples, including Grabczewski's monumental case study of the @@ -773,7 +799,7 @@ * The previous version of HOL renamed to Old_HOL; -* The new version of HOL (previously called CHOL) uses a curried syntax +* The new version of HOL (previously called CHOL) uses a curried syntax for functions. Application looks like f a b instead of f(a,b); * Mutually recursive inductive definitions finally work in HOL; @@ -786,12 +812,12 @@ New in Isabelle94-3 ------------------- -* new infix operator, addss, allowing the classical reasoner to +* new infix operator, addss, allowing the classical reasoner to perform simplification at each step of its search. Example: - fast_tac (cs addss ss) + fast_tac (cs addss ss) -* a new logic, CHOL, the same as HOL, but with a curried syntax -for functions. Application looks like f a b instead of f(a,b). Also pairs +* a new logic, CHOL, the same as HOL, but with a curried syntax +for functions. Application looks like f a b instead of f(a,b). Also pairs look like (a,b) instead of ; * PLEASE NOTE: CHOL will eventually replace HOL! @@ -802,7 +828,7 @@ * In ZF, integer numerals now denote two's-complement binary integers. Arithmetic operations can be performed by rewriting. See ZF/ex/Bin.ML; -* Many new examples: I/O automata, Church-Rosser theorem, equivalents +* Many new examples: I/O automata, Church-Rosser theorem, equivalents of the Axiom of Choice; @@ -810,7 +836,7 @@ New in Isabelle94-2 ------------------- -* Significantly faster resolution; +* Significantly faster resolution; * the different sections in a .thy file can now be mixed and repeated freely;