NEWS
changeset 5726 5de7e399ec88
parent 5722 c669e2161b08
child 5731 f84dc3b811e9
     1.1 --- a/NEWS	Thu Oct 22 11:09:43 1998 +0200
     1.2 +++ b/NEWS	Thu Oct 22 12:26:55 1998 +0200
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 @@ -6,26 +7,26 @@
     1.9  
    1.10  *** Overview of INCOMPATIBILITIES (see below for more details) ***
    1.11  
    1.12 -* several changes of proof tools;
    1.13 -
    1.14 -* HOL: new version of inductive and datatype;
    1.15 +* several changes of automated proof tools;
    1.16  
    1.17 -* HOL: major changes to the inductive and datatype packages;
    1.18 +* HOL: major changes to the inductive and datatype packages, including
    1.19 +some minor incompatibilities of theory syntax;
    1.20  
    1.21 -* HOL: renamed r^-1 to 'converse' from 'inverse'; `inj_onto' is now
    1.22 +* HOL: renamed r^-1 to 'converse' from 'inverse'; 'inj_onto' is now
    1.23  called `inj_on';
    1.24  
    1.25  * HOL: removed duplicate thms in Arith:
    1.26    less_imp_add_less  should be replaced by  trans_less_add1
    1.27    le_imp_add_le      should be replaced by  trans_le_add1
    1.28  
    1.29 -* HOL: unary - is now overloaded (new type constraints may be required);
    1.30 +* HOL: unary minus is now overloaded (new type constraints may be
    1.31 +required);
    1.32  
    1.33 -* HOL and ZF: unary minus for integers is now #- instead of #~.  In ZF, 
    1.34 -  expressions such as n#-1 must be changed to n#- 1, since #-1 is now taken
    1.35 -  as an integer constant.
    1.36 +* HOL and ZF: unary minus for integers is now #- instead of #~.  In
    1.37 +ZF, expressions such as n#-1 must be changed to n#- 1, since #-1 is
    1.38 +now taken as an integer constant.
    1.39  
    1.40 -* Pure: ML function 'theory_of' replaced by 'theory';
    1.41 +* Pure: ML function 'theory_of' renamed to 'theory';
    1.42  
    1.43  
    1.44  *** Proof tools ***
    1.45 @@ -53,44 +54,43 @@
    1.46    getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
    1.47  
    1.48  * Classical reasoner: addbefore/addSbefore now have APPEND/ORELSE
    1.49 -  semantics; addbefore now affects only the unsafe part of step_tac
    1.50 -  etc.; this affects addss/auto_tac/force_tac, so EXISTING PROOFS MAY
    1.51 -  FAIL, but proofs should be fixable easily, e.g. by replacing
    1.52 -  Auto_tac by Force_tac;
    1.53 +semantics; addbefore now affects only the unsafe part of step_tac
    1.54 +etc.; this affects addss/auto_tac/force_tac, so EXISTING PROOFS MAY
    1.55 +FAIL, but proofs should be fixable easily, e.g. by replacing Auto_tac
    1.56 +by Force_tac;
    1.57  
    1.58 -* Classical reasoner: setwrapper to setWrapper and compwrapper to compWrapper; 
    1.59 -  added safe wrapper (and access functions for it);
    1.60 +* Classical reasoner: setwrapper to setWrapper and compwrapper to
    1.61 +compWrapper; added safe wrapper (and access functions for it);
    1.62  
    1.63  * HOL/split_all_tac is now much faster and fails if there is nothing
    1.64 -to split.  Existing (fragile) proofs may require adaption because the
    1.65 -order and the names of the automatically generated variables have
    1.66 -changed.  split_all_tac has moved within claset() from unsafe wrappers
    1.67 -to safe wrappers, which means that !!-bound variables are split much
    1.68 -more aggressively, and safe_tac and clarify_tac now split such
    1.69 -variables.  If this splitting is not appropriate, use delSWrapper
    1.70 -"split_all_tac".
    1.71 -
    1.72 -* HOL/Simplifier:
    1.73 +to split.  Some EXISTING PROOFS MAY REQUIRE ADAPTION because the order
    1.74 +and the names of the automatically generated variables have changed.
    1.75 +split_all_tac has moved within claset() from unsafe wrappers to safe
    1.76 +wrappers, which means that !!-bound variables are split much more
    1.77 +aggressively, and safe_tac and clarify_tac now split such variables.
    1.78 +If this splitting is not appropriate, use delSWrapper "split_all_tac".
    1.79 +Note: the same holds for record_split_tac, which does the job of
    1.80 +split_all_tac for record fields.
    1.81  
    1.82 - - Rewrite rules for case distinctions can now be added permanently to
    1.83 -   the default simpset using Addsplits just like Addsimps. They can be
    1.84 -   removed via Delsplits just like Delsimps. Lower-case versions are
    1.85 -   also available.
    1.86 +* HOL/Simplifier: Rewrite rules for case distinctions can now be added
    1.87 +permanently to the default simpset using Addsplits just like
    1.88 +Addsimps. They can be removed via Delsplits just like
    1.89 +Delsimps. Lower-case versions are also available.
    1.90  
    1.91 - - The rule split_if is now part of the default simpset. This means
    1.92 -   that the simplifier will eliminate all occurrences of if-then-else
    1.93 -   in the conclusion of a goal. To prevent this, you can either remove
    1.94 -   split_if completely from the default simpset by `Delsplits
    1.95 -   [split_if]' or remove it in a specific call of the simplifier using
    1.96 -   `... delsplits [split_if]'.  You can also add/delete other case
    1.97 -   splitting rules to/from the default simpset: every datatype
    1.98 -   generates suitable rules `split_t_case' and `split_t_case_asm'
    1.99 -   (where t is the name of the datatype).
   1.100 +* HOL/Simplifier: The rule split_if is now part of the default
   1.101 +simpset. This means that the simplifier will eliminate all occurrences
   1.102 +of if-then-else in the conclusion of a goal. To prevent this, you can
   1.103 +either remove split_if completely from the default simpset by
   1.104 +`Delsplits [split_if]' or remove it in a specific call of the
   1.105 +simplifier using `... delsplits [split_if]'.  You can also add/delete
   1.106 +other case splitting rules to/from the default simpset: every datatype
   1.107 +generates suitable rules `split_t_case' and `split_t_case_asm' (where
   1.108 +t is the name of the datatype).
   1.109  
   1.110 -* Classical reasoner - Simplifier combination: new force_tac (and
   1.111 +* Classical reasoner / Simplifier combination: new force_tac (and
   1.112  derivatives Force_tac, force) combines rewriting and classical
   1.113  reasoning (and whatever other tools) similarly to auto_tac, but is
   1.114 -aimed to solve the given subgoal completely;
   1.115 +aimed to solve the given subgoal completely.
   1.116  
   1.117  
   1.118  *** General ***
   1.119 @@ -123,6 +123,8 @@
   1.120  
   1.121  * print mode 'emacs' reserved for Isamode;
   1.122  
   1.123 +* support multiple print (ast) translations per constant name;
   1.124 +
   1.125  
   1.126  *** HOL ***
   1.127  
   1.128 @@ -193,9 +195,33 @@
   1.129  scripts to the new package (backup your sources first!).
   1.130  
   1.131  
   1.132 -* HOL/record package: now includes concrete syntax for record types,
   1.133 -terms, updates; still lacks important theorems, like surjective
   1.134 -pairing and split;
   1.135 +* HOL/record package: considerably improved implementation; now
   1.136 +includes concrete syntax for record types, terms, updates; theorems
   1.137 +for surjective pairing and splitting !!-bound record variables; proof
   1.138 +support is as follows:
   1.139 +
   1.140 +  1) standard conversions (selectors or updates applied to record
   1.141 +constructor terms) are part of the standard simpset;
   1.142 +
   1.143 +  2) inject equations of the form ((x, y) = (x', y')) == x=x' & y=y' are
   1.144 +made part of standard simpset and claset via addIffs;
   1.145 +
   1.146 +  3) a tactic for record field splitting (record_split_tac) is part of
   1.147 +the standard claset (addSWrapper);
   1.148 +
   1.149 +To get a better idea about these rules you may retrieve them via
   1.150 +something like 'thms "foo.simps"' or 'thms "foo.iffs"', where "foo" is
   1.151 +the name of your record type.
   1.152 +
   1.153 +The split tactic 3) conceptually simplifies by the following rule:
   1.154 +
   1.155 +  "(!!x. PROP ?P x) == (!!a b. PROP ?P (a, b))"
   1.156 +
   1.157 +Thus any record variable that is bound by meta-all will automatically
   1.158 +blow up into some record constructor term, consequently the
   1.159 +simplifications of 1), 2) apply.  Thus force_tac, auto_tac etc. shall
   1.160 +solve record problems automatically.
   1.161 +
   1.162  
   1.163  * reorganized the main HOL image: HOL/Integ and String loaded by
   1.164  default; theory Main includes everything;
   1.165 @@ -450,7 +476,7 @@
   1.166  
   1.167  *** HOL ***
   1.168  
   1.169 -* HOL: there is a new splitter `split_asm_tac' that can be used e.g. 
   1.170 +* HOL: there is a new splitter `split_asm_tac' that can be used e.g.
   1.171    with `addloop' of the simplifier to faciliate case splitting in premises.
   1.172  
   1.173  * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
   1.174 @@ -544,7 +570,7 @@
   1.175  
   1.176  *** FOL and ZF ***
   1.177  
   1.178 -* FOL: there is a new splitter `split_asm_tac' that can be used e.g. 
   1.179 +* FOL: there is a new splitter `split_asm_tac' that can be used e.g.
   1.180    with `addloop' of the simplifier to faciliate case splitting in premises.
   1.181  
   1.182  * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as
   1.183 @@ -602,7 +628,7 @@
   1.184  some limitations.  Blast_tac...
   1.185    + ignores addss, addbefore, addafter; this restriction is intrinsic
   1.186    + ignores elimination rules that don't have the correct format
   1.187 -	(the conclusion MUST be a formula variable)
   1.188 +        (the conclusion MUST be a formula variable)
   1.189    + ignores types, which can make HOL proofs fail
   1.190    + rules must not require higher-order unification, e.g. apply_type in ZF
   1.191      [message "Function Var's argument not a bound variable" relates to this]
   1.192 @@ -615,12 +641,12 @@
   1.193  setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper
   1.194  (and access functions for it);
   1.195  
   1.196 -* improved combination of classical reasoner and simplifier: 
   1.197 +* improved combination of classical reasoner and simplifier:
   1.198    + functions for handling clasimpsets
   1.199    + improvement of addss: now the simplifier is called _after_ the
   1.200      safe steps.
   1.201    + safe variant of addss called addSss: uses safe simplifications
   1.202 -    _during_ the safe steps. It is more complete as it allows multiple 
   1.203 +    _during_ the safe steps. It is more complete as it allows multiple
   1.204      instantiations of unknowns (e.g. with slow_tac).
   1.205  
   1.206  *** Simplifier ***
   1.207 @@ -676,8 +702,8 @@
   1.208  
   1.209  * HOLCF/IOA replaces old HOL/IOA;
   1.210  
   1.211 -* HOLCF changes: derived all rules and arities 
   1.212 -  + axiomatic type classes instead of classes 
   1.213 +* HOLCF changes: derived all rules and arities
   1.214 +  + axiomatic type classes instead of classes
   1.215    + typedef instead of faking type definitions
   1.216    + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
   1.217    + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po
   1.218 @@ -765,7 +791,7 @@
   1.219  
   1.220  * theory files (.thy) no longer require \...\ escapes at line breaks;
   1.221  
   1.222 -* searchable theorem database (see the section "Retrieving theorems" on 
   1.223 +* searchable theorem database (see the section "Retrieving theorems" on
   1.224  page 8 of the Reference Manual);
   1.225  
   1.226  * new examples, including Grabczewski's monumental case study of the
   1.227 @@ -773,7 +799,7 @@
   1.228  
   1.229  * The previous version of HOL renamed to Old_HOL;
   1.230  
   1.231 -* The new version of HOL (previously called CHOL) uses a curried syntax 
   1.232 +* The new version of HOL (previously called CHOL) uses a curried syntax
   1.233  for functions.  Application looks like f a b instead of f(a,b);
   1.234  
   1.235  * Mutually recursive inductive definitions finally work in HOL;
   1.236 @@ -786,12 +812,12 @@
   1.237  New in Isabelle94-3
   1.238  -------------------
   1.239  
   1.240 -* new infix operator, addss, allowing the classical reasoner to 
   1.241 +* new infix operator, addss, allowing the classical reasoner to
   1.242  perform simplification at each step of its search.  Example:
   1.243 -	fast_tac (cs addss ss)
   1.244 +        fast_tac (cs addss ss)
   1.245  
   1.246 -* a new logic, CHOL, the same as HOL, but with a curried syntax 
   1.247 -for functions.  Application looks like f a b instead of f(a,b).  Also pairs 
   1.248 +* a new logic, CHOL, the same as HOL, but with a curried syntax
   1.249 +for functions.  Application looks like f a b instead of f(a,b).  Also pairs
   1.250  look like (a,b) instead of <a,b>;
   1.251  
   1.252  * PLEASE NOTE: CHOL will eventually replace HOL!
   1.253 @@ -802,7 +828,7 @@
   1.254  * In ZF, integer numerals now denote two's-complement binary integers.
   1.255  Arithmetic operations can be performed by rewriting.  See ZF/ex/Bin.ML;
   1.256  
   1.257 -* Many new examples: I/O automata, Church-Rosser theorem, equivalents 
   1.258 +* Many new examples: I/O automata, Church-Rosser theorem, equivalents
   1.259  of the Axiom of Choice;
   1.260  
   1.261  
   1.262 @@ -810,7 +836,7 @@
   1.263  New in Isabelle94-2
   1.264  -------------------
   1.265  
   1.266 -* Significantly faster resolution;  
   1.267 +* Significantly faster resolution;
   1.268  
   1.269  * the different sections in a .thy file can now be mixed and repeated
   1.270  freely;