cleaned up;
authorwenzelm
Fri Jul 03 18:53:02 1998 +0200 (1998-07-03)
changeset 5127ef467e05da61
parent 5126 01cbf154d926
child 5128 66c4d554e93f
cleaned up;
NEWS
     1.1 --- a/NEWS	Fri Jul 03 18:05:03 1998 +0200
     1.2 +++ b/NEWS	Fri Jul 03 18:53:02 1998 +0200
     1.3 @@ -1,17 +1,16 @@
     1.4 +
     1.5  Isabelle NEWS -- history of user-visible changes
     1.6  ================================================
     1.7  
     1.8  New in this Isabelle version
     1.9  ----------------------------
    1.10  
    1.11 -*** General Changes ***
    1.12 +*** Overview of INCOMPATIBILITIES (see below for more details) ***
    1.13  
    1.14 -* new toplevel commands `Goal' and `Goalw' that improve upon `goal'
    1.15 -and `goalw': the theory is no longer needed as an explicit argument -
    1.16 -the current theory is used; assumptions are no longer returned at the
    1.17 -ML-level unless one of them starts with ==> or !!; it is recommended
    1.18 -to convert to these new commands using isatool fixgoal (as usual,
    1.19 -backup your sources first!);
    1.20 +* HOL/inductive requires Inductive.thy as an ancestor;
    1.21 +
    1.22 +
    1.23 +*** Proof tools ***
    1.24  
    1.25  * Simplifier: Asm_full_simp_tac is now more aggressive.
    1.26    1. It will sometimes reorient premises if that increases their power to
    1.27 @@ -21,27 +20,66 @@
    1.28    For compatibility reasons there is now Asm_lr_simp_tac which is like the
    1.29    old Asm_full_simp_tac in that it does not rotate premises.
    1.30  
    1.31 -* Changed wrapper mechanism for the classical reasoner now allows for
    1.32 -selected deletion of wrappers, by introduction of names for wrapper
    1.33 -functionals.  This implies that addbefore, addSbefore, addaltern, and
    1.34 -addSaltern now take a pair (name, tactic) as argument, and that adding
    1.35 -two tactics with the same name overwrites the first one (emitting a
    1.36 -warning).
    1.37 +* Classical reasoner: wrapper mechanism for the classical reasoner now
    1.38 +allows for selected deletion of wrappers, by introduction of names for
    1.39 +wrapper functionals.  This implies that addbefore, addSbefore,
    1.40 +addaltern, and addSaltern now take a pair (name, tactic) as argument,
    1.41 +and that adding two tactics with the same name overwrites the first
    1.42 +one (emitting a warning).
    1.43    type wrapper = (int -> tactic) -> (int -> tactic)
    1.44    setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by
    1.45    addWrapper, addSWrapper: claset * (string * wrapper) -> claset
    1.46    delWrapper, delSWrapper: claset *  string            -> claset
    1.47    getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
    1.48  
    1.49 -* inductive definitions now handle disjunctive premises correctly (HOL
    1.50 -and ZF);
    1.51 +* HOL/split_all_tac is now much faster and fails if there is nothing
    1.52 +to split.  Existing (fragile) proofs may require adaption because the
    1.53 +order and the names of the automatically generated variables have
    1.54 +changed.  split_all_tac has moved within claset() from unsafe wrappers
    1.55 +to safe wrappers, which means that !!-bound variables are split much
    1.56 +more aggressively, and safe_tac and clarify_tac now split such
    1.57 +variables.  If this splitting is not appropriate, use delSWrapper
    1.58 +"split_all_tac".
    1.59 +
    1.60 +* HOL/Simplifier:
    1.61 +
    1.62 + - Rewrite rules for case distinctions can now be added permanently to
    1.63 +   the default simpset using Addsplits just like Addsimps. They can be
    1.64 +   removed via Delsplits just like Delsimps. Lower-case versions are
    1.65 +   also available.
    1.66 +
    1.67 + - The rule split_if is now part of the default simpset. This means
    1.68 +   that the simplifier will eliminate all occurrences of if-then-else
    1.69 +   in the conclusion of a goal. To prevent this, you can either remove
    1.70 +   split_if completely from the default simpset by `Delsplits
    1.71 +   [split_if]' or remove it in a specific call of the simplifier using
    1.72 +   `... delsplits [split_if]'.  You can also add/delete other case
    1.73 +   splitting rules to/from the default simpset: every datatype
    1.74 +   generates suitable rules `split_t_case' and `split_t_case_asm'
    1.75 +   (where t is the name of the datatype).
    1.76 +
    1.77 +* Classical reasoner - Simplifier combination: new force_tac (and
    1.78 +derivatives Force_tac, force) combines rewriting and classical
    1.79 +reasoning (and whatever other tools) similarly to auto_tac, but is
    1.80 +aimed to solve the given subgoal completely;
    1.81 +
    1.82 +
    1.83 +*** General ***
    1.84 +
    1.85 +* new toplevel commands `Goal' and `Goalw' that improve upon `goal'
    1.86 +and `goalw': the theory is no longer needed as an explicit argument -
    1.87 +the current theory context is used; assumptions are no longer returned
    1.88 +at the ML-level unless one of them starts with ==> or !!; it is
    1.89 +recommended to convert to these new commands using isatool fixgoal (as
    1.90 +usual, backup your sources first!);
    1.91  
    1.92  * new toplevel commands 'thm' and 'thms' for retrieving theorems from
    1.93  the current theory context;
    1.94  
    1.95 -* new theory section 'nonterminals';
    1.96 +* new theory section 'nonterminals' for purely syntactic types;
    1.97  
    1.98 -* new theory section 'setup';
    1.99 +* new theory section 'setup' for generic ML setup functions
   1.100 +(e.g. package initialization);
   1.101  
   1.102  
   1.103  *** HOL ***
   1.104 @@ -49,12 +87,26 @@
   1.105  * reorganized the main HOL image: HOL/Integ and String loaded by
   1.106  default; theory Main includes everything;
   1.107  
   1.108 -* HOL/Real: a construction of the reals using Dedekind cuts;
   1.109 +* added option_map_eq_Some to the default simpset claset;
   1.110 +
   1.111 +* added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset;
   1.112 +
   1.113 +* many new identities for unions, intersections, set difference, etc.;
   1.114 +
   1.115 +* expand_if, expand_split, expand_sum_case and expand_nat_case are now
   1.116 +called split_if, split_split, split_sum_case and split_nat_case (to go
   1.117 +with add/delsplits);
   1.118  
   1.119 -* HOL/record: now includes concrete syntax for record terms (still
   1.120 -lacks important theorems, like surjective pairing and split);
   1.121 +* HOL/Prod introduces simplification procedure unit_eq_proc rewriting
   1.122 +(?x::unit) = (); this is made part of the default simpset, which COULD
   1.123 +MAKE EXISTING PROOFS FAIL under rare circumstances (consider
   1.124 +'Delsimprocs [unit_eq_proc];' as last resort);
   1.125  
   1.126 -* Inductive definition package: Mutually recursive definitions such as
   1.127 +* HOL/record package: now includes concrete syntax for record terms
   1.128 +(still lacks important theorems, like surjective pairing and split);
   1.129 +
   1.130 +* HOL/inductive package reorganized and improved: now supports mutual
   1.131 +definitions such as
   1.132  
   1.133    inductive EVEN ODD
   1.134      intrs
   1.135 @@ -62,79 +114,37 @@
   1.136        oddI "n : EVEN ==> Suc n : ODD"
   1.137        evenI "n : ODD ==> Suc n : EVEN"
   1.138  
   1.139 -  are now possible. Theories containing (co)inductive definitions must now
   1.140 -  have theory "Inductive" as an ancestor. The new component "elims" of the
   1.141 -  structure created by the package contains an elimination rule for each of
   1.142 -  the recursive sets. Note that the component "mutual_induct" no longer
   1.143 -  exists - the induction rule is always contained in "induct".
   1.144 -
   1.145 -* simplification procedure unit_eq_proc rewrites (?x::unit) = (); this
   1.146 -is made part of the default simpset of Prod.thy, which COULD MAKE
   1.147 -EXISTING PROOFS FAIL (consider 'Delsimprocs [unit_eq_proc];' as last
   1.148 -resort);
   1.149 +new component "elims" of the structure created by the package contains
   1.150 +an elimination rule for each of the recursive sets; requires
   1.151 +Inductive.thy as an ancestor; component "mutual_induct" no longer
   1.152 +exists - the induction rule is always contained in "induct"; inductive
   1.153 +definitions now handle disjunctive premises correctly (also ZF);
   1.154  
   1.155 -* new force_tac (and its derivations Force_tac, force): combines
   1.156 -rewriting and classical reasoning (and whatever other tools) similarly
   1.157 -to auto_tac, but is aimed to solve the given subgoal totally;
   1.158 -
   1.159 -* added option_map_eq_Some to simpset() and claset();
   1.160 +* HOL/recdef can now declare non-recursive functions, with {} supplied as
   1.161 +the well-founded relation;
   1.162  
   1.163 -* New directory HOL/UNITY: Chandy and Misra's UNITY formalism;
   1.164 +* HOL/Update: new theory of function updates:
   1.165 +    f(a:=b) == %x. if x=a then b else f x
   1.166 +may also be iterated as in f(a:=b,c:=d,...);
   1.167  
   1.168 -* New theory HOL/Update of function updates:
   1.169 -  f(a:=b) == %x. if x=a then b else f x
   1.170 -  May also be iterated as in f(a:=b,c:=d,...).
   1.171 +* HOL/Vimage: new theory for inverse image of a function, syntax f-``B;
   1.172  
   1.173  * HOL/List: new function list_update written xs[i:=v] that updates the i-th
   1.174    list position. May also be iterated as in xs[i:=a,j:=b,...].
   1.175  
   1.176 -* split_all_tac is now much faster and fails if there is nothing to
   1.177 -split.  Existing (fragile) proofs may require adaption because the
   1.178 -order and the names of the automatically generated variables have
   1.179 -changed.  split_all_tac has moved within claset() from usafe wrappers
   1.180 -to safe wrappers, which means that !!-bound variables are splitted
   1.181 -much more aggressively, and safe_tac and clarify_tac now split such
   1.182 -variables.  If this splitting is not appropriate, use delSWrapper
   1.183 -"split_all_tac".
   1.184 +* HOL/Arith:
   1.185 +  - removed 'pred' (predecessor) function;
   1.186 +  - generalized some theorems about n-1;
   1.187 +  - many new laws about "div" and "mod";
   1.188 +  - new laws about greatest common divisors (see theory ex/Primes);
   1.189  
   1.190 -* added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset;
   1.191 -
   1.192 -* HOL/Arithmetic:
   1.193 -  
   1.194 -  - removed 'pred' (predecessor) function
   1.195 -  - generalized some theorems about n-1
   1.196 -  - Many new laws about "div" and "mod"
   1.197 -  - New laws about greatest common divisors (see theory ex/Primes)
   1.198 -
   1.199 -* HOL/Relation: renamed the relational operatotr r^-1 "converse"
   1.200 +* HOL/Relation: renamed the relational operator r^-1 "converse"
   1.201  instead of "inverse";
   1.202  
   1.203 -* recdef can now declare non-recursive functions, with {} supplied as
   1.204 -the well-founded relation;
   1.205 -
   1.206 -* expand_if, expand_split, expand_sum_case and expand_nat_case are now called
   1.207 -  split_if, split_split, split_sum_case and split_nat_case
   1.208 -  (to go with add/delsplits).
   1.209 -
   1.210 -* Simplifier:
   1.211 -
   1.212 - -Rewrite rules for case distinctions can now be added permanently to the
   1.213 -  default simpset using Addsplits just like Addsimps. They can be removed via
   1.214 -  Delsplits just like Delsimps. Lower-case versions are also available.
   1.215 +* directory HOL/Real: a construction of the reals using Dedekind cuts
   1.216 +(not included by default);
   1.217  
   1.218 - -The rule split_if is now part of the default simpset. This means that
   1.219 -  the simplifier will eliminate all ocurrences of if-then-else in the
   1.220 -  conclusion of a goal. To prevent this, you can either remove split_if
   1.221 -  completely from the default simpset by `Delsplits [split_if]' or
   1.222 -  remove it in a specific call of the simplifier using
   1.223 -  `... delsplits [split_if]'.
   1.224 -  You can also add/delete other case splitting rules to/from the default
   1.225 -  simpset: every datatype generates suitable rules `split_t_case' and
   1.226 -  `split_t_case_asm' (where t is the name of the datatype).
   1.227 -
   1.228 -* new theory Vimage (inverse image of a function, syntax f-``B);
   1.229 -
   1.230 -* many new identities for unions, intersections, set difference, etc.;
   1.231 +* directory HOL/UNITY: Chandy and Misra's UNITY formalism;
   1.232  
   1.233  
   1.234  *** ZF ***
   1.235 @@ -142,7 +152,7 @@
   1.236  * in  let x=t in u(x), neither t nor u(x) has to be an FOL term.
   1.237  
   1.238  
   1.239 -*** Internal changes ***
   1.240 +*** Internal programming interfaces ***
   1.241  
   1.242  * improved the theory data mechanism to support encapsulation (data
   1.243  kind name replaced by private Object.kind, acting as authorization
   1.244 @@ -151,6 +161,9 @@
   1.245  * module Pure/Syntax now offers quote / antiquote translation
   1.246  functions (useful for Hoare logic etc. with implicit dependencies);
   1.247  
   1.248 +* Simplifier now offers conversions (asm_)(full_)rewrite: simpset ->
   1.249 +cterm -> thm;
   1.250 +
   1.251  
   1.252  
   1.253  New in Isabelle98 (January 1998)