summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 5127 | ef467e05da61 |

parent 5125 | 463a0e9df5b5 |

child 5128 | 66c4d554e93f |

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)