author | wenzelm |

Thu Oct 22 12:26:55 1998 +0200 (1998-10-22) | |

changeset 5726 | 5de7e399ec88 |

parent 5725 | 26772f4543fc |

child 5727 | 1b708bfb0c1e |

tuned;

record package;

record package;

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;