summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 19 Jan 2007 22:31:17 +0100 | |

changeset 22126 | 420b7b102acc |

parent 22125 | cc35c948f6c5 |

child 22127 | 025dfa637f78 |

tuned;

--- a/NEWS Fri Jan 19 22:14:23 2007 +0100 +++ b/NEWS Fri Jan 19 22:31:17 2007 +0100 @@ -302,21 +302,21 @@ * Isar/locales: changed the way locales with predicates are defined. Instead of accumulating the specification, the imported expression is -now an interpretation. -INCOMPATIBILITY: different normal form of locale expressions. -In particular, in interpretations of locales with predicates, -goals repesenting already interpreted fragments are not removed -automatically. Use methods `intro_locales' and `unfold_locales'; see below. - -* Isar/locales: new methods `intro_locales' and `unfold_locales' provide -backward reasoning on locales predicates. The methods are aware of -interpretations and discharge corresponding goals. `intro_locales' is -less aggressive then `unfold_locales' and does not unfold predicates to -assumptions. +now an interpretation. INCOMPATIBILITY: different normal form of +locale expressions. In particular, in interpretations of locales with +predicates, goals repesenting already interpreted fragments are not +removed automatically. Use methods `intro_locales' and +`unfold_locales'; see below. + +* Isar/locales: new methods `intro_locales' and `unfold_locales' +provide backward reasoning on locales predicates. The methods are +aware of interpretations and discharge corresponding goals. +`intro_locales' is less aggressive then `unfold_locales' and does not +unfold predicates to assumptions. * Isar/locales: the order in which locale fragments are accumulated -has changed. This enables to override declarations from fragments -due to interpretations -- for example, unwanted simp rules. +has changed. This enables to override declarations from fragments due +to interpretations -- for example, unwanted simp rules. * Provers/induct: improved internal context management to support local fixes and defines on-the-fly. Thus explicit meta-level @@ -469,10 +469,10 @@ * Attribute "symmetric" produces result with standardized schematic variables (index 0). Potential INCOMPATIBILITY. -* Simplifier: by default the simplifier trace only shows top level rewrites -now. That is, trace_simp_depth_limit is set to 1 by default. Thus there is -less danger of being flooded by the trace. The trace indicates where parts -have been suppressed. +* Simplifier: by default the simplifier trace only shows top level +rewrites now. That is, trace_simp_depth_limit is set to 1 by +default. Thus there is less danger of being flooded by the trace. The +trace indicates where parts have been suppressed. * Provers/classical: removed obsolete classical version of elim_format attribute; classical elim/dest rules are now treated uniformly when @@ -507,80 +507,53 @@ *** HOL *** -* New syntactic class "size"; overloaded constant "size" now -has type "'a::size ==> bool" - -* Constants "Divides.op div", "Divides.op mod" and "Divides.op dvd" no named - "Divides.div", "Divides.mod" and "Divides.dvd" - INCOMPATIBILITY for ML code directly refering to constant names. - -* Replaced "auto_term" by the conceptually simpler method "relation", -which just applies the instantiated termination rule with no further -simplifications. -INCOMPATIBILITY: -Replace - termination by (auto_term "MYREL") -with - termination by (relation "MYREL") auto - -* Automated termination proofs "by lexicographic_order" are now -included in the abbreviated function command "fun". No explicit -"termination" command is necessary anymore. -INCOMPATIBILITY: If a "fun"-definition cannot be proved terminating by -a lexicographic size order, then the command fails. Use the expanded -version "function" for these cases. - -* New method "lexicographic_order" automatically synthesizes -termination relations as lexicographic combinations of size measures. -Usage for (function package) termination proofs: - -termination -by lexicographic_order - -* Records: generalised field-update to take a function on the field -rather than the new value: r(|A := x|) is translated to A_update (K x) r -The K-combinator that is internally used is called K_record. +* Added syntactic class "size"; overloaded constant "size" now has +type "'a::size ==> bool" + +* Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op +dvd" to "Divides.div", "Divides.mod" and +"Divides.dvd". INCOMPATIBILITY. + +* Added method "lexicographic_order" automatically synthesizes +termination relations as lexicographic combinations of size measures +-- 'function' package. + +* HOL/records: generalised field-update to take a function on the +field rather than the new value: r(|A := x|) is translated to A_update +(K x) r The K-combinator that is internally used is called K_record. INCOMPATIBILITY: Usage of the plain update functions has to be adapted. -* axclass "semiring_0" now contains annihilation axioms -("x * 0 = 0","0 * x = 0"), which are required for a semiring. Richer -structures do not inherit from semiring_0 anymore, because this property -is a theorem there, not an axiom. -INCOMPATIBILITY: In instances of semiring_0, there is more to prove, but -this is mostly trivial. - -* axclass "recpower" was generalized to arbitrary monoids, not just -commutative semirings. -INCOMPATIBILITY: If you use recpower and need commutativity or a semiring -property, add the corresponding classes. - -* Locale Lattic_Locales.partial_order changed (to achieve consistency with -axclass order): -- moved to Orderings.partial_order -- additional parameter ``less'' -INCOMPATIBILITY. +* axclass "semiring_0" now contains annihilation axioms x * 0 = 0 and +0 * x = 0, which are required for a semiring. Richer structures do +not inherit from semiring_0 anymore, because this property is a +theorem there, not an axiom. INCOMPATIBILITY: In instances of +semiring_0, there is more to prove, but this is mostly trivial. + +* axclass "recpower" was generalized to arbitrary monoids, not just +commutative semirings. INCOMPATIBILITY: If you use recpower and need +commutativity or a semiring property, add the corresponding classes. + +* Unified locale partial_order with class definition (cf. theory +Orderings), added parameter ``less''. INCOMPATIBILITY. * Constant "List.list_all2" in List.thy now uses authentic syntax. -INCOMPATIBILITY: translations containing list_all2 may go wrong. On Isar -level, use abbreviations instead. - -* Constant "List.op mem" in List.thy now has proper name: "List.memberl" -INCOMPATIBILITY: rarely occuring name references (e.g. ``List.op mem.simps'') -require renaming (e.g. ``List.memberl.simps''). - -* Renamed constants in HOL.thy: - 0 ~> HOL.zero - 1 ~> HOL.one -INCOMPATIBILITY: ML code directly refering to constant names may need adaption -This in general only affects hand-written proof tactics, simprocs and so on. - -* New theory Code_Generator providing class 'eq', -allowing for code generation with polymorphic equality. - -* Numeral syntax: type 'bin' which was a mere type copy of 'int' has been -abandoned in favour of plain 'int'. INCOMPATIBILITY -- Significant changes -for setting up numeral syntax for types: +INCOMPATIBILITY: translations containing list_all2 may go wrong. On +Isar level, use abbreviations instead. + +* Renamed constant "List.op mem" to "List.memberl" INCOMPATIBILITY: +rarely occuring name references (e.g. ``List.op mem.simps'') require +renaming (e.g. ``List.memberl.simps''). + +* Renamed constants "0" to "HOL.zero" and "1" to "HOL.one". +INCOMPATIBILITY. + +* Added theory Code_Generator providing class 'eq', allowing for code +generation with polymorphic equality. + +* Numeral syntax: type 'bin' which was a mere type copy of 'int' has +been abandoned in favour of plain 'int'. INCOMPATIBILITY -- +significant changes for setting up numeral syntax for types: - new constants Numeral.pred and Numeral.succ instead of former Numeral.bin_pred and Numeral.bin_succ. @@ -590,12 +563,11 @@ See HOL/Integ/IntArith.thy for an example setup. -* New top level command 'normal_form' computes the normal form of a term -that may contain free variables. For example 'normal_form "rev[a,b,c]"' -prints '[b,c,a]'. This command is suitable for heavy-duty computations -because the functions are compiled to ML first. -INCOMPATIBILITY: new keywords 'normal_form' must quoted when used as -an identifier. +* New top level command 'normal_form' computes the normal form of a +term that may contain free variables. For example ``normal_form +"rev[a,b,c]"'' produces ``[b,c,a]'' (without proof). This command is +suitable for heavy-duty computations because the functions are +compiled to ML first. * Alternative iff syntax "A <-> B" for equality on bool (with priority 25 like -->); output depends on the "iff" print_mode, the default is @@ -639,34 +611,37 @@ * Relation composition operator "op O" now has precedence 75 and binds stronger than union and intersection. INCOMPATIBILITY. -* The old set interval syntax "{m..n(}" (and relatives) has been removed. - Use "{m..<n}" (and relatives) instead. +* The old set interval syntax "{m..n(}" (and relatives) has been +removed. Use "{m..<n}" (and relatives) instead. * In the context of the assumption "~(s = t)" the Simplifier rewrites "t = s" to False (by simproc "neq_simproc"). For backward compatibility this can be disabled by ML "reset use_neq_simproc". -* "m dvd n" where m and n are numbers is evaluated to True/False by simp. - -* Theorem Cons_eq_map_conv no longer has attribute `simp'. +* "m dvd n" where m and n are numbers is evaluated to True/False by +simp. + +* Theorem Cons_eq_map_conv no longer declared as ``simp''. * Theorem setsum_mult renamed to setsum_right_distrib. * Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the -'rule' method. - -* Tactics 'sat' and 'satx' reimplemented, several improvements: goals -no longer need to be stated as "<prems> ==> False", equivalences (i.e. -"=" on type bool) are handled, variable names of the form "lit_<n>" -are no longer reserved, significant speedup. - -* Tactics 'sat' and 'satx' can now replay MiniSat proof traces. zChaff is -still supported as well. - -* inductive and datatype: provide projections of mutual rules, bundled -as foo_bar.inducts; - -* Library: moved theories Parity, GCD, Binomial, Infinite_Set to Library. +``rule'' method. + +* Reimplemented methods ``sat'' and ``satx'', with several +improvements: goals no longer need to be stated as "<prems> ==> +False", equivalences (i.e. "=" on type bool) are handled, variable +names of the form "lit_<n>" are no longer reserved, significant +speedup. + +* Methods ``sat'' and ``satx'' can now replay MiniSat proof traces. +zChaff is still supported as well. + +* 'inductive' and 'datatype': provide projections of mutual rules, +bundled as foo_bar.inducts; + +* Library: moved theories Parity, GCD, Binomial, Infinite_Set to +Library. * Library: moved theory Accessible_Part to main HOL. @@ -676,16 +651,16 @@ * Library: added theory AssocList which implements (finite) maps as association lists. -* New proof method "evaluation" for efficiently solving a goal (i.e. a -boolean expression) by compiling it to ML. The goal is "proved" (via -the oracle "Evaluation") if it evaluates to True. +* Added proof method ``evaluation'' for efficiently solving a goal +(i.e. a boolean expression) by compiling it to ML. The goal is +"proved" (via an oracle) if it evaluates to True. * Linear arithmetic now splits certain operators (e.g. min, max, abs) also when invoked by the simplifier. This results in the simplifier being more powerful on arithmetic goals. INCOMPATIBILITY. Set fast_arith_split_limit to 0 to obtain the old behavior. -* Support for hex (0x20) and binary (0b1001) numerals. +* Support for hex (0x20) and binary (0b1001) numerals. * New method: reify eqs (t), where eqs are equations for an interpretation I :: 'a list => 'b => 'c and t::'c is an optional @@ -713,14 +688,14 @@ * Order and lattice theory no longer based on records. INCOMPATIBILITY. -* Renamed lemmas least_carrier -> least_closed and -greatest_carrier -> greatest_closed. INCOMPATIBILITY. +* Renamed lemmas least_carrier -> least_closed and greatest_carrier -> +greatest_closed. INCOMPATIBILITY. * Method algebra is now set up via an attribute. For examples see Ring.thy. INCOMPATIBILITY: the method is now weaker on combinations of algebraic structures. -* Renamed `CRing.thy' to `Ring.thy'. INCOMPATIBILITY. +* Renamed theory CRing to Ring. *** HOL-Complex *** @@ -734,13 +709,14 @@ algebras, using new overloaded constants scaleR :: real => 'a => 'a and norm :: 'a => real. -* Real: New constant of_real :: real => 'a::real_algebra_1 injects from -reals into other types. The overloaded constant Reals :: 'a set is now -defined as range of_real; potential INCOMPATIBILITY. - -* Hyperreal: Several constants that previously worked only for the reals -have been generalized, so they now work over arbitrary vector spaces. Type -annotations may need to be added in some cases; potential INCOMPATIBILITY. +* Real: New constant of_real :: real => 'a::real_algebra_1 injects +from reals into other types. The overloaded constant Reals :: 'a set +is now defined as range of_real; potential INCOMPATIBILITY. + +* Hyperreal: Several constants that previously worked only for the +reals have been generalized, so they now work over arbitrary vector +spaces. Type annotations may need to be added in some cases; potential +INCOMPATIBILITY. Infinitesimal :: ('a::real_normed_vector) star set" HFinite :: ('a::real_normed_vector) star set" @@ -757,9 +733,9 @@ deriv :: ['a::real_normed_field => 'a, 'a, 'a] => bool * Complex: Some complex-specific constants are now abbreviations for -overloaded ones: complex_of_real = of_real, cmod = norm, hcmod = hnorm. -Other constants have been entirely removed in favor of the polymorphic -versions (INCOMPATIBILITY): +overloaded ones: complex_of_real = of_real, cmod = norm, hcmod = +hnorm. Other constants have been entirely removed in favor of the +polymorphic versions (INCOMPATIBILITY): approx <-- capprox HFinite <-- CFinite @@ -774,33 +750,6 @@ *** ML *** -* Pure/table: - -Function `...tab.foldl` removed. -INCOMPATIBILITY: use `...tabfold` instead - -* Pure/library: - -`gen_rem(s)` abandoned in favour of `remove` / `subtract`. -INCOMPATIBILITY: -rewrite "gen_rem eq (xs, x)" to "remove (eq o swap) x xs" -rewrite "gen_rems eq (xs, ys)" to "subtract (eq o swap) ys xs" -drop "swap" if "eq" is symmetric. - -* Pure/library: - -infixes `ins` `ins_string` `ins_int` have been abandoned in favour of `insert`. -INCOMPATIBILITY: rewrite "x ins(_...) xs" to "insert (op =) x xs" - -* Pure/General/susp.ML: - -New module for delayed evaluations. - -* Pure/library: - -Semantically identical functions "equal_list" and "eq_list" have been -unified to "eq_list". - * Pure/library: val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list @@ -808,12 +757,9 @@ The semantics of "burrow" is: "take a function with *simulatanously* transforms a list of value, and apply it *simulatanously* to a list of -list of values of the appropriate type". Confer this with "map" which +list of values of the appropriate type". Compare this with "map" which would *not* apply its argument function simulatanously but in -sequence. "fold_burrow" has an additional context. - -Both actually avoid the usage of "unflat" since they hide away -"unflat" from the user. +sequence; "fold_burrow" has an additional context. * Pure/library: functions map2 and fold2 with curried syntax for simultanous mapping and folding: @@ -833,12 +779,8 @@ Note that fold_index starts counting at index 0, not 1 like foldln used to. -* Pure/library: general ``divide_and_conquer'' combinator on lists. - -* Pure/General/name_mangler.ML provides a functor for generic name -mangling (bijective mapping from expression values to strings). - -* Pure/General/rat.ML implements rational numbers. +* Pure/library: added general ``divide_and_conquer'' combinator on +lists. * Pure/General/table.ML: the join operations now works via exceptions DUP/SAME instead of type option. This is simpler in simple cases, and @@ -862,7 +804,8 @@ * Pure/kernel: consts certification ignores sort constraints given in signature declarations. (This information is not relevant to the -logic, but only for type inference.) IMPORTANT INTERNAL CHANGE. +logic, but only for type inference.) IMPORTANT INTERNAL CHANGE, +potential INCOMPATIBILITY. * Pure: axiomatic type classes are now purely definitional, with explicit proofs of class axioms and super class relations performed