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 -* HOL/record: now includes concrete syntax for record terms (still
1.112 -lacks important theorems, like surjective pairing and split);
1.113 +* added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset;
1.114
1.115 -* Inductive definition package: Mutually recursive definitions such as
1.116 +* many new identities for unions, intersections, set difference, etc.;
1.117 +
1.118 +* expand_if, expand_split, expand_sum_case and expand_nat_case are now
1.119 +called split_if, split_split, split_sum_case and split_nat_case (to go
1.120 +with add/delsplits);
1.121 +
1.122 +* HOL/Prod introduces simplification procedure unit_eq_proc rewriting
1.123 +(?x::unit) = (); this is made part of the default simpset, which COULD
1.124 +MAKE EXISTING PROOFS FAIL under rare circumstances (consider
1.125 +'Delsimprocs [unit_eq_proc];' as last resort);
1.126 +
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 +new component "elims" of the structure created by the package contains
1.145 +an elimination rule for each of the recursive sets; requires
1.146 +Inductive.thy as an ancestor; component "mutual_induct" no longer
1.147 +exists - the induction rule is always contained in "induct"; inductive
1.148 +definitions now handle disjunctive premises correctly (also ZF);
1.149
1.150 -* simplification procedure unit_eq_proc rewrites (?x::unit) = (); this
1.151 -is made part of the default simpset of Prod.thy, which COULD MAKE
1.152 -EXISTING PROOFS FAIL (consider 'Delsimprocs [unit_eq_proc];' as last
1.153 -resort);
1.154 +* HOL/recdef can now declare non-recursive functions, with {} supplied as
1.155 +the well-founded relation;
1.156
1.157 -* new force_tac (and its derivations Force_tac, force): combines
1.158 -rewriting and classical reasoning (and whatever other tools) similarly
1.159 -to auto_tac, but is aimed to solve the given subgoal totally;
1.160 +* HOL/Update: new theory of function updates:
1.161 + f(a:=b) == %x. if x=a then b else f x
1.162 +may also be iterated as in f(a:=b,c:=d,...);
1.163
1.164 -* added option_map_eq_Some to simpset() and claset();
1.165 -
1.166 -* New directory HOL/UNITY: Chandy and Misra's UNITY formalism;
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 +* directory HOL/Real: a construction of the reals using Dedekind cuts
1.206 +(not included by default);
1.207
1.208 -* expand_if, expand_split, expand_sum_case and expand_nat_case are now called
1.209 - split_if, split_split, split_sum_case and split_nat_case
1.210 - (to go with add/delsplits).
1.211 -
1.212 -* Simplifier:
1.213 -
1.214 - -Rewrite rules for case distinctions can now be added permanently to the
1.215 - default simpset using Addsplits just like Addsimps. They can be removed via
1.216 - Delsplits just like Delsimps. Lower-case versions are also available.
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)