author | wenzelm |

Fri Jan 19 22:31:17 2007 +0100 (2007-01-19) | |

changeset 22126 | 420b7b102acc |

parent 22125 | cc35c948f6c5 |

child 22127 | 025dfa637f78 |

tuned;

1.1 --- a/NEWS Fri Jan 19 22:14:23 2007 +0100 1.2 +++ b/NEWS Fri Jan 19 22:31:17 2007 +0100 1.3 @@ -302,21 +302,21 @@ 1.4 1.5 * Isar/locales: changed the way locales with predicates are defined. 1.6 Instead of accumulating the specification, the imported expression is 1.7 -now an interpretation. 1.8 -INCOMPATIBILITY: different normal form of locale expressions. 1.9 -In particular, in interpretations of locales with predicates, 1.10 -goals repesenting already interpreted fragments are not removed 1.11 -automatically. Use methods `intro_locales' and `unfold_locales'; see below. 1.12 - 1.13 -* Isar/locales: new methods `intro_locales' and `unfold_locales' provide 1.14 -backward reasoning on locales predicates. The methods are aware of 1.15 -interpretations and discharge corresponding goals. `intro_locales' is 1.16 -less aggressive then `unfold_locales' and does not unfold predicates to 1.17 -assumptions. 1.18 +now an interpretation. INCOMPATIBILITY: different normal form of 1.19 +locale expressions. In particular, in interpretations of locales with 1.20 +predicates, goals repesenting already interpreted fragments are not 1.21 +removed automatically. Use methods `intro_locales' and 1.22 +`unfold_locales'; see below. 1.23 + 1.24 +* Isar/locales: new methods `intro_locales' and `unfold_locales' 1.25 +provide backward reasoning on locales predicates. The methods are 1.26 +aware of interpretations and discharge corresponding goals. 1.27 +`intro_locales' is less aggressive then `unfold_locales' and does not 1.28 +unfold predicates to assumptions. 1.29 1.30 * Isar/locales: the order in which locale fragments are accumulated 1.31 -has changed. This enables to override declarations from fragments 1.32 -due to interpretations -- for example, unwanted simp rules. 1.33 +has changed. This enables to override declarations from fragments due 1.34 +to interpretations -- for example, unwanted simp rules. 1.35 1.36 * Provers/induct: improved internal context management to support 1.37 local fixes and defines on-the-fly. Thus explicit meta-level 1.38 @@ -469,10 +469,10 @@ 1.39 * Attribute "symmetric" produces result with standardized schematic 1.40 variables (index 0). Potential INCOMPATIBILITY. 1.41 1.42 -* Simplifier: by default the simplifier trace only shows top level rewrites 1.43 -now. That is, trace_simp_depth_limit is set to 1 by default. Thus there is 1.44 -less danger of being flooded by the trace. The trace indicates where parts 1.45 -have been suppressed. 1.46 +* Simplifier: by default the simplifier trace only shows top level 1.47 +rewrites now. That is, trace_simp_depth_limit is set to 1 by 1.48 +default. Thus there is less danger of being flooded by the trace. The 1.49 +trace indicates where parts have been suppressed. 1.50 1.51 * Provers/classical: removed obsolete classical version of elim_format 1.52 attribute; classical elim/dest rules are now treated uniformly when 1.53 @@ -507,80 +507,53 @@ 1.54 1.55 *** HOL *** 1.56 1.57 -* New syntactic class "size"; overloaded constant "size" now 1.58 -has type "'a::size ==> bool" 1.59 - 1.60 -* Constants "Divides.op div", "Divides.op mod" and "Divides.op dvd" no named 1.61 - "Divides.div", "Divides.mod" and "Divides.dvd" 1.62 - INCOMPATIBILITY for ML code directly refering to constant names. 1.63 - 1.64 -* Replaced "auto_term" by the conceptually simpler method "relation", 1.65 -which just applies the instantiated termination rule with no further 1.66 -simplifications. 1.67 -INCOMPATIBILITY: 1.68 -Replace 1.69 - termination by (auto_term "MYREL") 1.70 -with 1.71 - termination by (relation "MYREL") auto 1.72 - 1.73 -* Automated termination proofs "by lexicographic_order" are now 1.74 -included in the abbreviated function command "fun". No explicit 1.75 -"termination" command is necessary anymore. 1.76 -INCOMPATIBILITY: If a "fun"-definition cannot be proved terminating by 1.77 -a lexicographic size order, then the command fails. Use the expanded 1.78 -version "function" for these cases. 1.79 - 1.80 -* New method "lexicographic_order" automatically synthesizes 1.81 -termination relations as lexicographic combinations of size measures. 1.82 -Usage for (function package) termination proofs: 1.83 - 1.84 -termination 1.85 -by lexicographic_order 1.86 - 1.87 -* Records: generalised field-update to take a function on the field 1.88 -rather than the new value: r(|A := x|) is translated to A_update (K x) r 1.89 -The K-combinator that is internally used is called K_record. 1.90 +* Added syntactic class "size"; overloaded constant "size" now has 1.91 +type "'a::size ==> bool" 1.92 + 1.93 +* Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op 1.94 +dvd" to "Divides.div", "Divides.mod" and 1.95 +"Divides.dvd". INCOMPATIBILITY. 1.96 + 1.97 +* Added method "lexicographic_order" automatically synthesizes 1.98 +termination relations as lexicographic combinations of size measures 1.99 +-- 'function' package. 1.100 + 1.101 +* HOL/records: generalised field-update to take a function on the 1.102 +field rather than the new value: r(|A := x|) is translated to A_update 1.103 +(K x) r The K-combinator that is internally used is called K_record. 1.104 INCOMPATIBILITY: Usage of the plain update functions has to be 1.105 adapted. 1.106 1.107 -* axclass "semiring_0" now contains annihilation axioms 1.108 -("x * 0 = 0","0 * x = 0"), which are required for a semiring. Richer 1.109 -structures do not inherit from semiring_0 anymore, because this property 1.110 -is a theorem there, not an axiom. 1.111 -INCOMPATIBILITY: In instances of semiring_0, there is more to prove, but 1.112 -this is mostly trivial. 1.113 - 1.114 -* axclass "recpower" was generalized to arbitrary monoids, not just 1.115 -commutative semirings. 1.116 -INCOMPATIBILITY: If you use recpower and need commutativity or a semiring 1.117 -property, add the corresponding classes. 1.118 - 1.119 -* Locale Lattic_Locales.partial_order changed (to achieve consistency with 1.120 -axclass order): 1.121 -- moved to Orderings.partial_order 1.122 -- additional parameter ``less'' 1.123 -INCOMPATIBILITY. 1.124 +* axclass "semiring_0" now contains annihilation axioms x * 0 = 0 and 1.125 +0 * x = 0, which are required for a semiring. Richer structures do 1.126 +not inherit from semiring_0 anymore, because this property is a 1.127 +theorem there, not an axiom. INCOMPATIBILITY: In instances of 1.128 +semiring_0, there is more to prove, but this is mostly trivial. 1.129 + 1.130 +* axclass "recpower" was generalized to arbitrary monoids, not just 1.131 +commutative semirings. INCOMPATIBILITY: If you use recpower and need 1.132 +commutativity or a semiring property, add the corresponding classes. 1.133 + 1.134 +* Unified locale partial_order with class definition (cf. theory 1.135 +Orderings), added parameter ``less''. INCOMPATIBILITY. 1.136 1.137 * Constant "List.list_all2" in List.thy now uses authentic syntax. 1.138 -INCOMPATIBILITY: translations containing list_all2 may go wrong. On Isar 1.139 -level, use abbreviations instead. 1.140 - 1.141 -* Constant "List.op mem" in List.thy now has proper name: "List.memberl" 1.142 -INCOMPATIBILITY: rarely occuring name references (e.g. ``List.op mem.simps'') 1.143 -require renaming (e.g. ``List.memberl.simps''). 1.144 - 1.145 -* Renamed constants in HOL.thy: 1.146 - 0 ~> HOL.zero 1.147 - 1 ~> HOL.one 1.148 -INCOMPATIBILITY: ML code directly refering to constant names may need adaption 1.149 -This in general only affects hand-written proof tactics, simprocs and so on. 1.150 - 1.151 -* New theory Code_Generator providing class 'eq', 1.152 -allowing for code generation with polymorphic equality. 1.153 - 1.154 -* Numeral syntax: type 'bin' which was a mere type copy of 'int' has been 1.155 -abandoned in favour of plain 'int'. INCOMPATIBILITY -- Significant changes 1.156 -for setting up numeral syntax for types: 1.157 +INCOMPATIBILITY: translations containing list_all2 may go wrong. On 1.158 +Isar level, use abbreviations instead. 1.159 + 1.160 +* Renamed constant "List.op mem" to "List.memberl" INCOMPATIBILITY: 1.161 +rarely occuring name references (e.g. ``List.op mem.simps'') require 1.162 +renaming (e.g. ``List.memberl.simps''). 1.163 + 1.164 +* Renamed constants "0" to "HOL.zero" and "1" to "HOL.one". 1.165 +INCOMPATIBILITY. 1.166 + 1.167 +* Added theory Code_Generator providing class 'eq', allowing for code 1.168 +generation with polymorphic equality. 1.169 + 1.170 +* Numeral syntax: type 'bin' which was a mere type copy of 'int' has 1.171 +been abandoned in favour of plain 'int'. INCOMPATIBILITY -- 1.172 +significant changes for setting up numeral syntax for types: 1.173 1.174 - new constants Numeral.pred and Numeral.succ instead 1.175 of former Numeral.bin_pred and Numeral.bin_succ. 1.176 @@ -590,12 +563,11 @@ 1.177 1.178 See HOL/Integ/IntArith.thy for an example setup. 1.179 1.180 -* New top level command 'normal_form' computes the normal form of a term 1.181 -that may contain free variables. For example 'normal_form "rev[a,b,c]"' 1.182 -prints '[b,c,a]'. This command is suitable for heavy-duty computations 1.183 -because the functions are compiled to ML first. 1.184 -INCOMPATIBILITY: new keywords 'normal_form' must quoted when used as 1.185 -an identifier. 1.186 +* New top level command 'normal_form' computes the normal form of a 1.187 +term that may contain free variables. For example ``normal_form 1.188 +"rev[a,b,c]"'' produces ``[b,c,a]'' (without proof). This command is 1.189 +suitable for heavy-duty computations because the functions are 1.190 +compiled to ML first. 1.191 1.192 * Alternative iff syntax "A <-> B" for equality on bool (with priority 1.193 25 like -->); output depends on the "iff" print_mode, the default is 1.194 @@ -639,34 +611,37 @@ 1.195 * Relation composition operator "op O" now has precedence 75 and binds 1.196 stronger than union and intersection. INCOMPATIBILITY. 1.197 1.198 -* The old set interval syntax "{m..n(}" (and relatives) has been removed. 1.199 - Use "{m..<n}" (and relatives) instead. 1.200 +* The old set interval syntax "{m..n(}" (and relatives) has been 1.201 +removed. Use "{m..<n}" (and relatives) instead. 1.202 1.203 * In the context of the assumption "~(s = t)" the Simplifier rewrites 1.204 "t = s" to False (by simproc "neq_simproc"). For backward 1.205 compatibility this can be disabled by ML "reset use_neq_simproc". 1.206 1.207 -* "m dvd n" where m and n are numbers is evaluated to True/False by simp. 1.208 - 1.209 -* Theorem Cons_eq_map_conv no longer has attribute `simp'. 1.210 +* "m dvd n" where m and n are numbers is evaluated to True/False by 1.211 +simp. 1.212 + 1.213 +* Theorem Cons_eq_map_conv no longer declared as ``simp''. 1.214 1.215 * Theorem setsum_mult renamed to setsum_right_distrib. 1.216 1.217 * Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the 1.218 -'rule' method. 1.219 - 1.220 -* Tactics 'sat' and 'satx' reimplemented, several improvements: goals 1.221 -no longer need to be stated as "<prems> ==> False", equivalences (i.e. 1.222 -"=" on type bool) are handled, variable names of the form "lit_<n>" 1.223 -are no longer reserved, significant speedup. 1.224 - 1.225 -* Tactics 'sat' and 'satx' can now replay MiniSat proof traces. zChaff is 1.226 -still supported as well. 1.227 - 1.228 -* inductive and datatype: provide projections of mutual rules, bundled 1.229 -as foo_bar.inducts; 1.230 - 1.231 -* Library: moved theories Parity, GCD, Binomial, Infinite_Set to Library. 1.232 +``rule'' method. 1.233 + 1.234 +* Reimplemented methods ``sat'' and ``satx'', with several 1.235 +improvements: goals no longer need to be stated as "<prems> ==> 1.236 +False", equivalences (i.e. "=" on type bool) are handled, variable 1.237 +names of the form "lit_<n>" are no longer reserved, significant 1.238 +speedup. 1.239 + 1.240 +* Methods ``sat'' and ``satx'' can now replay MiniSat proof traces. 1.241 +zChaff is still supported as well. 1.242 + 1.243 +* 'inductive' and 'datatype': provide projections of mutual rules, 1.244 +bundled as foo_bar.inducts; 1.245 + 1.246 +* Library: moved theories Parity, GCD, Binomial, Infinite_Set to 1.247 +Library. 1.248 1.249 * Library: moved theory Accessible_Part to main HOL. 1.250 1.251 @@ -676,16 +651,16 @@ 1.252 * Library: added theory AssocList which implements (finite) maps as 1.253 association lists. 1.254 1.255 -* New proof method "evaluation" for efficiently solving a goal (i.e. a 1.256 -boolean expression) by compiling it to ML. The goal is "proved" (via 1.257 -the oracle "Evaluation") if it evaluates to True. 1.258 +* Added proof method ``evaluation'' for efficiently solving a goal 1.259 +(i.e. a boolean expression) by compiling it to ML. The goal is 1.260 +"proved" (via an oracle) if it evaluates to True. 1.261 1.262 * Linear arithmetic now splits certain operators (e.g. min, max, abs) 1.263 also when invoked by the simplifier. This results in the simplifier 1.264 being more powerful on arithmetic goals. INCOMPATIBILITY. Set 1.265 fast_arith_split_limit to 0 to obtain the old behavior. 1.266 1.267 -* Support for hex (0x20) and binary (0b1001) numerals. 1.268 +* Support for hex (0x20) and binary (0b1001) numerals. 1.269 1.270 * New method: reify eqs (t), where eqs are equations for an 1.271 interpretation I :: 'a list => 'b => 'c and t::'c is an optional 1.272 @@ -713,14 +688,14 @@ 1.273 * Order and lattice theory no longer based on records. 1.274 INCOMPATIBILITY. 1.275 1.276 -* Renamed lemmas least_carrier -> least_closed and 1.277 -greatest_carrier -> greatest_closed. INCOMPATIBILITY. 1.278 +* Renamed lemmas least_carrier -> least_closed and greatest_carrier -> 1.279 +greatest_closed. INCOMPATIBILITY. 1.280 1.281 * Method algebra is now set up via an attribute. For examples see 1.282 Ring.thy. INCOMPATIBILITY: the method is now weaker on combinations 1.283 of algebraic structures. 1.284 1.285 -* Renamed `CRing.thy' to `Ring.thy'. INCOMPATIBILITY. 1.286 +* Renamed theory CRing to Ring. 1.287 1.288 1.289 *** HOL-Complex *** 1.290 @@ -734,13 +709,14 @@ 1.291 algebras, using new overloaded constants scaleR :: real => 'a => 'a 1.292 and norm :: 'a => real. 1.293 1.294 -* Real: New constant of_real :: real => 'a::real_algebra_1 injects from 1.295 -reals into other types. The overloaded constant Reals :: 'a set is now 1.296 -defined as range of_real; potential INCOMPATIBILITY. 1.297 - 1.298 -* Hyperreal: Several constants that previously worked only for the reals 1.299 -have been generalized, so they now work over arbitrary vector spaces. Type 1.300 -annotations may need to be added in some cases; potential INCOMPATIBILITY. 1.301 +* Real: New constant of_real :: real => 'a::real_algebra_1 injects 1.302 +from reals into other types. The overloaded constant Reals :: 'a set 1.303 +is now defined as range of_real; potential INCOMPATIBILITY. 1.304 + 1.305 +* Hyperreal: Several constants that previously worked only for the 1.306 +reals have been generalized, so they now work over arbitrary vector 1.307 +spaces. Type annotations may need to be added in some cases; potential 1.308 +INCOMPATIBILITY. 1.309 1.310 Infinitesimal :: ('a::real_normed_vector) star set" 1.311 HFinite :: ('a::real_normed_vector) star set" 1.312 @@ -757,9 +733,9 @@ 1.313 deriv :: ['a::real_normed_field => 'a, 'a, 'a] => bool 1.314 1.315 * Complex: Some complex-specific constants are now abbreviations for 1.316 -overloaded ones: complex_of_real = of_real, cmod = norm, hcmod = hnorm. 1.317 -Other constants have been entirely removed in favor of the polymorphic 1.318 -versions (INCOMPATIBILITY): 1.319 +overloaded ones: complex_of_real = of_real, cmod = norm, hcmod = 1.320 +hnorm. Other constants have been entirely removed in favor of the 1.321 +polymorphic versions (INCOMPATIBILITY): 1.322 1.323 approx <-- capprox 1.324 HFinite <-- CFinite 1.325 @@ -774,33 +750,6 @@ 1.326 1.327 *** ML *** 1.328 1.329 -* Pure/table: 1.330 - 1.331 -Function `...tab.foldl` removed. 1.332 -INCOMPATIBILITY: use `...tabfold` instead 1.333 - 1.334 -* Pure/library: 1.335 - 1.336 -`gen_rem(s)` abandoned in favour of `remove` / `subtract`. 1.337 -INCOMPATIBILITY: 1.338 -rewrite "gen_rem eq (xs, x)" to "remove (eq o swap) x xs" 1.339 -rewrite "gen_rems eq (xs, ys)" to "subtract (eq o swap) ys xs" 1.340 -drop "swap" if "eq" is symmetric. 1.341 - 1.342 -* Pure/library: 1.343 - 1.344 -infixes `ins` `ins_string` `ins_int` have been abandoned in favour of `insert`. 1.345 -INCOMPATIBILITY: rewrite "x ins(_...) xs" to "insert (op =) x xs" 1.346 - 1.347 -* Pure/General/susp.ML: 1.348 - 1.349 -New module for delayed evaluations. 1.350 - 1.351 -* Pure/library: 1.352 - 1.353 -Semantically identical functions "equal_list" and "eq_list" have been 1.354 -unified to "eq_list". 1.355 - 1.356 * Pure/library: 1.357 1.358 val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list 1.359 @@ -808,12 +757,9 @@ 1.360 1.361 The semantics of "burrow" is: "take a function with *simulatanously* 1.362 transforms a list of value, and apply it *simulatanously* to a list of 1.363 -list of values of the appropriate type". Confer this with "map" which 1.364 +list of values of the appropriate type". Compare this with "map" which 1.365 would *not* apply its argument function simulatanously but in 1.366 -sequence. "fold_burrow" has an additional context. 1.367 - 1.368 -Both actually avoid the usage of "unflat" since they hide away 1.369 -"unflat" from the user. 1.370 +sequence; "fold_burrow" has an additional context. 1.371 1.372 * Pure/library: functions map2 and fold2 with curried syntax for 1.373 simultanous mapping and folding: 1.374 @@ -833,12 +779,8 @@ 1.375 Note that fold_index starts counting at index 0, not 1 like foldln 1.376 used to. 1.377 1.378 -* Pure/library: general ``divide_and_conquer'' combinator on lists. 1.379 - 1.380 -* Pure/General/name_mangler.ML provides a functor for generic name 1.381 -mangling (bijective mapping from expression values to strings). 1.382 - 1.383 -* Pure/General/rat.ML implements rational numbers. 1.384 +* Pure/library: added general ``divide_and_conquer'' combinator on 1.385 +lists. 1.386 1.387 * Pure/General/table.ML: the join operations now works via exceptions 1.388 DUP/SAME instead of type option. This is simpler in simple cases, and 1.389 @@ -862,7 +804,8 @@ 1.390 1.391 * Pure/kernel: consts certification ignores sort constraints given in 1.392 signature declarations. (This information is not relevant to the 1.393 -logic, but only for type inference.) IMPORTANT INTERNAL CHANGE. 1.394 +logic, but only for type inference.) IMPORTANT INTERNAL CHANGE, 1.395 +potential INCOMPATIBILITY. 1.396 1.397 * Pure: axiomatic type classes are now purely definitional, with 1.398 explicit proofs of class axioms and super class relations performed