# HG changeset patch # User haftmann # Date 1193300672 -7200 # Node ID 712ab7bd95121da9d4cbf0abd8465a24be82be8f # Parent 261d6791952c396259d05a6cfe11e00111a05c59 tuned diff -r 261d6791952c -r 712ab7bd9512 NEWS --- a/NEWS Wed Oct 24 21:42:17 2007 +0200 +++ b/NEWS Thu Oct 25 10:24:32 2007 +0200 @@ -118,6 +118,7 @@ syntax layer ("user space type system") takes care of converting between global polymorphic consts and internal locale representation. See src/HOL/ex/Classpackage.thy for examples (as well as main HOL). +"isatool doc classes" provides a tutorial. * Yet another code generator framework allows to generate executable code for ML and Haskell (including Isabelle classes). A short usage @@ -132,7 +133,10 @@ writing Haskell code to a bunch of files: code_gen in Haskell -Reasonable default setup of framework in HOL/Main. + evaluating propositions to True/False using code generation: + method ``eval'' + +Reasonable default setup of framework in HOL. Theorem attributs for selecting and transforming function equations theorems: @@ -168,12 +172,6 @@ referred to by usual term syntax (including optional type annotations). -* Code generator: basic definitions (from 'definition', 'constdefs', -or primitive 'instance' definitions) are added automatically to the -table of defining equations. Primitive defs are not used as defining -equations by default any longer. Defining equations are now definitly -restricted to meta "==" and object equality "=". - * Command 'no_translations' removes translation rules from theory syntax. @@ -563,35 +561,221 @@ wait for the automatic provers to return. WARNING: does not really work with multi-threading. -* Localized monotonicity predicate in theory "Orderings"; integrated -lemmas max_of_mono and min_of_mono with this predicate. -INCOMPATIBILITY. - -* Class "div" now inherits from class "times" rather than "type". -INCOMPATIBILITY. - * New "auto_quickcheck" feature tests outermost goal statements for potential counter-examples. Controlled by ML references auto_quickcheck (default true) and auto_quickcheck_time_limit (default 5000 milliseconds). Fails silently if statements is outside of executable fragment, or any other codgenerator problem occurs. +* New constant "undefined" with axiom "undefined x = undefined". + +* Added class "HOL.eq", allowing for code generation with polymorphic +equality. + +* Some renaming of class constants due to canonical name prefixing in +the new 'class' package: + + HOL.abs ~> HOL.abs_class.abs + HOL.divide ~> HOL.divide_class.divide + 0 ~> HOL.zero_class.zero + 1 ~> HOL.one_class.one + op + ~> HOL.plus_class.plus + op - ~> HOL.minus_class.minus + uminus ~> HOL.minus_class.uminus + op * ~> HOL.times_class.times + op < ~> HOL.ord_class.less + op <= > HOL.ord_class.less_eq + Nat.power ~> Power.power_class.power + Nat.size ~> Nat.size_class.size + Numeral.number_of ~> Numeral.number_class.number_of + FixedPoint.Inf ~> Lattices.complete_lattice_class.Inf + FixedPoint.Sup ~> Lattices.complete_lattice_class.Sup + Orderings.min ~> Orderings.ord_class.min + Orderings.max ~> Orderings.ord_class.max + Divides.op div ~> Divides.div_class.div + Divides.op mod ~> Divides.div_class.mod + Divides.op dvd ~> Divides.div_class.dvd + +INCOMPATIBILITY. Adaptions may be required in the following cases: + +a) User-defined constants using any of the names "plus", "minus", +"times", "less" or "less_eq". The standard syntax translations for +"+", "-" and "*" may go wrong. INCOMPATIBILITY: use more specific +names. + +b) Variables named "plus", "minus", "times", "less", "less_eq" +INCOMPATIBILITY: use more specific names. + +c) Permutative equations (e.g. "a + b = b + a") +Since the change of names also changes the order of terms, permutative +rewrite rules may get applied in a different order. Experience shows +that this is rarely the case (only two adaptions in the whole Isabelle +distribution). INCOMPATIBILITY: rewrite proofs + +d) ML code directly refering to constant names +This in general only affects hand-written proof tactics, simprocs and +so on. INCOMPATIBILITY: grep your sourcecode and replace names. +Consider using @{const_name} antiquotation. + +* New class "default" with associated constant "default". + +* Function "sgn" is now overloaded and available on int, real, complex +(and other numeric types), using class "sgn". Two possible defs of +sgn are given as equational assumptions in the classes sgn_if and +sgn_div_norm; ordered_idom now also inherits from sgn_if. +INCOMPATIBILITY. + +* Locale "partial_order" now unified with class "order" (cf. theory +Orderings), added parameter "less". INCOMPATIBILITY. + +* Renamings in classes "order" and "linorder": facts "refl", "trans" and +"cases" to "order_refl", "order_trans" and "linorder_cases", to avoid +clashes with HOL "refl" and "trans". INCOMPATIBILITY. + +* Classes "order" and "linorder": potential INCOMPATIBILITY due to +changed order of proof goals in instance proofs. + +* The transitivity reasoner for partial and linear orders is set up +for classes "order" and "linorder". Instances of the reasoner are available +in all contexts importing or interpreting the corresponding locales. +Method "order" invokes the reasoner separately; the reasoner +is also integrated with the Simplifier as a solver. Diagnostic +command 'print_orders' shows the available instances of the reasoner +in the current context. + +* Localized monotonicity predicate in theory "Orderings"; integrated +lemmas max_of_mono and min_of_mono with this predicate. +INCOMPATIBILITY. + +* Formulation of theorem "dense" changed slightly due to integration +with new class dense_linear_order. + +* Uniform lattice theory development in HOL. + + constants "meet" and "join" now named "inf" and "sup" + constant "Meet" now named "Inf" + + classes "meet_semilorder" and "join_semilorder" now named + "lower_semilattice" and "upper_semilattice" + class "lorder" now named "lattice" + class "comp_lat" now named "complete_lattice" + + Instantiation of lattice classes allows explicit definitions + for "inf" and "sup" operations (or "Inf" and "Sup" for complete lattices). + + INCOMPATIBILITY. Theorem renames: + + meet_left_le ~> inf_le1 + meet_right_le ~> inf_le2 + join_left_le ~> sup_ge1 + join_right_le ~> sup_ge2 + meet_join_le ~> inf_sup_ord + le_meetI ~> le_infI + join_leI ~> le_supI + le_meet ~> le_inf_iff + le_join ~> ge_sup_conv + meet_idempotent ~> inf_idem + join_idempotent ~> sup_idem + meet_comm ~> inf_commute + join_comm ~> sup_commute + meet_leI1 ~> le_infI1 + meet_leI2 ~> le_infI2 + le_joinI1 ~> le_supI1 + le_joinI2 ~> le_supI2 + meet_assoc ~> inf_assoc + join_assoc ~> sup_assoc + meet_left_comm ~> inf_left_commute + meet_left_idempotent ~> inf_left_idem + join_left_comm ~> sup_left_commute + join_left_idempotent ~> sup_left_idem + meet_aci ~> inf_aci + join_aci ~> sup_aci + le_def_meet ~> le_iff_inf + le_def_join ~> le_iff_sup + join_absorp2 ~> sup_absorb2 + join_absorp1 ~> sup_absorb1 + meet_absorp1 ~> inf_absorb1 + meet_absorp2 ~> inf_absorb2 + meet_join_absorp ~> inf_sup_absorb + join_meet_absorp ~> sup_inf_absorb + distrib_join_le ~> distrib_sup_le + distrib_meet_le ~> distrib_inf_le + + add_meet_distrib_left ~> add_inf_distrib_left + add_join_distrib_left ~> add_sup_distrib_left + is_join_neg_meet ~> is_join_neg_inf + is_meet_neg_join ~> is_meet_neg_sup + add_meet_distrib_right ~> add_inf_distrib_right + add_join_distrib_right ~> add_sup_distrib_right + add_meet_join_distribs ~> add_sup_inf_distribs + join_eq_neg_meet ~> sup_eq_neg_inf + meet_eq_neg_join ~> inf_eq_neg_sup + add_eq_meet_join ~> add_eq_inf_sup + meet_0_imp_0 ~> inf_0_imp_0 + join_0_imp_0 ~> sup_0_imp_0 + meet_0_eq_0 ~> inf_0_eq_0 + join_0_eq_0 ~> sup_0_eq_0 + neg_meet_eq_join ~> neg_inf_eq_sup + neg_join_eq_meet ~> neg_sup_eq_inf + join_eq_if ~> sup_eq_if + + mono_meet ~> mono_inf + mono_join ~> mono_sup + meet_bool_eq ~> inf_bool_eq + join_bool_eq ~> sup_bool_eq + meet_fun_eq ~> inf_fun_eq + join_fun_eq ~> sup_fun_eq + meet_set_eq ~> inf_set_eq + join_set_eq ~> sup_set_eq + meet1_iff ~> inf1_iff + meet2_iff ~> inf2_iff + meet1I ~> inf1I + meet2I ~> inf2I + meet1D1 ~> inf1D1 + meet2D1 ~> inf2D1 + meet1D2 ~> inf1D2 + meet2D2 ~> inf2D2 + meet1E ~> inf1E + meet2E ~> inf2E + join1_iff ~> sup1_iff + join2_iff ~> sup2_iff + join1I1 ~> sup1I1 + join2I1 ~> sup2I1 + join1I1 ~> sup1I1 + join2I2 ~> sup1I2 + join1CI ~> sup1CI + join2CI ~> sup2CI + join1E ~> sup1E + join2E ~> sup2E + + is_meet_Meet ~> is_meet_Inf + Meet_bool_def ~> Inf_bool_def + Meet_fun_def ~> Inf_fun_def + Meet_greatest ~> Inf_greatest + Meet_lower ~> Inf_lower + Meet_set_def ~> Inf_set_def + + Sup_def ~> Sup_Inf + Sup_bool_eq ~> Sup_bool_def + Sup_fun_eq ~> Sup_fun_def + Sup_set_eq ~> Sup_set_def + + listsp_meetI ~> listsp_infI + listsp_meet_eq ~> listsp_inf_eq + + meet_min ~> inf_min + join_max ~> sup_max + +* Added syntactic class "size"; overloaded constant "size" now has +type "'a::size ==> bool" + * Internal reorganisation of `size' of datatypes: size theorems "foo.size" are no longer subsumed by "foo.simps" (but are still simplification rules by default!); theorems "prod.size" now named -"*.size" - -* The transitivity reasoner for partial and linear orders is set up -for locales "order" and "linorder" generated by the new class package -(instead of axiomatic type classes used before). Instances of the -reasoner are available in all contexts importing or interpreting these -locales. Method "order" invokes the reasoner separately; the reasoner -is also integrated with the Simplifier as a solver. Diagnostic -command 'print_orders' shows the available instances of the reasoner -in the current context. - -* Formulation of theorem "dense" changed slightly due to integration -with new class dense_linear_order. +"*.size". + +* Class "div" now inherits from class "times" rather than "type". +INCOMPATIBILITY. * HOL/Finite_Set: "name-space" locales Lattice, Distrib_lattice, Linorder etc. have disappeared; operations defined in terms of @@ -765,25 +949,6 @@ antiquotations @{const_name List.append} or @{term " ... @ ... "} to circumvent possible incompatibilities when working on ML level. -* Some renaming of class constants due to canonical name prefixing in -the new 'class' package: - - HOL.abs ~> HOL.minus_class.abs - HOL.divide ~> HOL.divide_class.divide - Nat.power ~> Power.power_class.power - Nat.size ~> Nat.size_class.size - Numeral.number_of ~> Numeral.number_class.number_of - FixedPoint.Inf ~> Lattices.complete_lattice_class.Inf - FixedPoint.Sup ~> Lattices.complete_lattice_class.Sup - Orderings.min ~> Orderings.ord_class.min - Orderings.max ~> Orderings.ord_class.max - -INCOMPATIBILITY. - -* New class "default" with associated constant "default". - -* New constant "undefined" with axiom "undefined x = undefined". - * primrec: missing cases mapped to "undefined" instead of "arbitrary". * New function listsum :: 'a list => 'a for arbitrary monoids. @@ -804,12 +969,6 @@ * New functions "sorted" and "sort" in src/HOL/List.thy. -* Function "sgn" is now overloaded and available on int, real, complex -(and other numeric types), using class "sgn". Two possible defs of -sgn are given as equational assumptions in the classes sgn_if and -sgn_div_norm; ordered_idom now also inherits from sgn_if. -INCOMPATIBILITY. - * New lemma collection field_simps (an extension of ring_simps) for manipulating (in)equations involving division. Multiplies with all denominators that can be proved to be non-zero (in equations) or @@ -824,145 +983,12 @@ package; constants add, mul, pow now curried. Infix syntax for algebraic operations. -* More uniform lattice theory development in HOL. - - constants "meet" and "join" now named "inf" and "sup" - constant "Meet" now named "Inf" - - classes "meet_semilorder" and "join_semilorder" now named - "lower_semilattice" and "upper_semilattice" - class "lorder" now named "lattice" - class "comp_lat" now named "complete_lattice" - - Instantiation of lattice classes allows explicit definitions - for "inf" and "sup" operations (or "Inf" and "Sup" for complete lattices). - - INCOMPATIBILITY. Theorem renames: - - meet_left_le ~> inf_le1 - meet_right_le ~> inf_le2 - join_left_le ~> sup_ge1 - join_right_le ~> sup_ge2 - meet_join_le ~> inf_sup_ord - le_meetI ~> le_infI - join_leI ~> le_supI - le_meet ~> le_inf_iff - le_join ~> ge_sup_conv - meet_idempotent ~> inf_idem - join_idempotent ~> sup_idem - meet_comm ~> inf_commute - join_comm ~> sup_commute - meet_leI1 ~> le_infI1 - meet_leI2 ~> le_infI2 - le_joinI1 ~> le_supI1 - le_joinI2 ~> le_supI2 - meet_assoc ~> inf_assoc - join_assoc ~> sup_assoc - meet_left_comm ~> inf_left_commute - meet_left_idempotent ~> inf_left_idem - join_left_comm ~> sup_left_commute - join_left_idempotent ~> sup_left_idem - meet_aci ~> inf_aci - join_aci ~> sup_aci - le_def_meet ~> le_iff_inf - le_def_join ~> le_iff_sup - join_absorp2 ~> sup_absorb2 - join_absorp1 ~> sup_absorb1 - meet_absorp1 ~> inf_absorb1 - meet_absorp2 ~> inf_absorb2 - meet_join_absorp ~> inf_sup_absorb - join_meet_absorp ~> sup_inf_absorb - distrib_join_le ~> distrib_sup_le - distrib_meet_le ~> distrib_inf_le - - add_meet_distrib_left ~> add_inf_distrib_left - add_join_distrib_left ~> add_sup_distrib_left - is_join_neg_meet ~> is_join_neg_inf - is_meet_neg_join ~> is_meet_neg_sup - add_meet_distrib_right ~> add_inf_distrib_right - add_join_distrib_right ~> add_sup_distrib_right - add_meet_join_distribs ~> add_sup_inf_distribs - join_eq_neg_meet ~> sup_eq_neg_inf - meet_eq_neg_join ~> inf_eq_neg_sup - add_eq_meet_join ~> add_eq_inf_sup - meet_0_imp_0 ~> inf_0_imp_0 - join_0_imp_0 ~> sup_0_imp_0 - meet_0_eq_0 ~> inf_0_eq_0 - join_0_eq_0 ~> sup_0_eq_0 - neg_meet_eq_join ~> neg_inf_eq_sup - neg_join_eq_meet ~> neg_sup_eq_inf - join_eq_if ~> sup_eq_if - - mono_meet ~> mono_inf - mono_join ~> mono_sup - meet_bool_eq ~> inf_bool_eq - join_bool_eq ~> sup_bool_eq - meet_fun_eq ~> inf_fun_eq - join_fun_eq ~> sup_fun_eq - meet_set_eq ~> inf_set_eq - join_set_eq ~> sup_set_eq - meet1_iff ~> inf1_iff - meet2_iff ~> inf2_iff - meet1I ~> inf1I - meet2I ~> inf2I - meet1D1 ~> inf1D1 - meet2D1 ~> inf2D1 - meet1D2 ~> inf1D2 - meet2D2 ~> inf2D2 - meet1E ~> inf1E - meet2E ~> inf2E - join1_iff ~> sup1_iff - join2_iff ~> sup2_iff - join1I1 ~> sup1I1 - join2I1 ~> sup2I1 - join1I1 ~> sup1I1 - join2I2 ~> sup1I2 - join1CI ~> sup1CI - join2CI ~> sup2CI - join1E ~> sup1E - join2E ~> sup2E - - is_meet_Meet ~> is_meet_Inf - Meet_bool_def ~> Inf_bool_def - Meet_fun_def ~> Inf_fun_def - Meet_greatest ~> Inf_greatest - Meet_lower ~> Inf_lower - Meet_set_def ~> Inf_set_def - - Sup_def ~> Sup_Inf - Sup_bool_eq ~> Sup_bool_def - Sup_fun_eq ~> Sup_fun_def - Sup_set_eq ~> Sup_set_def - - listsp_meetI ~> listsp_infI - listsp_meet_eq ~> listsp_inf_eq - - meet_min ~> inf_min - join_max ~> sup_max - -* Renamed classes "order" and "linorder": facts "refl", "trans" and -"cases" to "order_refl", "order_trans" and "linorder_cases", to avoid -clashes with HOL "refl" and "trans". INCOMPATIBILITY. - -* Classes "order" and "linorder": potential INCOMPATIBILITY due to -changed order of proof goals instance proofs. - -* Locale "partial_order" now unified with class "order" (cf. theory -Orderings), added parameter "less". INCOMPATIBILITY. - * Dropped redundant lemma def_imp_eq in favor of meta_eq_to_obj_eq. INCOMPATIBILITY. * Dropped redundant lemma if_def2 in favor of if_bool_eq_conj. INCOMPATIBILITY. -* 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_class.div", "Divides.div_class.mod" and -"Divides.dvd". INCOMPATIBILITY. - * Method "lexicographic_order" automatically synthesizes termination relations as lexicographic combinations of size measures -- 'function' package. @@ -989,12 +1015,6 @@ * Renamed constant "List.op mem" to "List.member". INCOMPATIBILITY. -* Renamed constants "0" to "HOL.zero_class.zero" and "1" to -"HOL.one_class.one". INCOMPATIBILITY. - -* Added class "HOL.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: @@ -1017,36 +1037,6 @@ 25 like -->); output depends on the "iff" print_mode, the default is "A = B" (with priority 50). -* Renamed constants in HOL.thy and Orderings.thy: - op + ~> HOL.plus_class.plus - op - ~> HOL.minus_class.minus - uminus ~> HOL.minus_class.uminus - abs ~> HOL.abs_class.abs - op * ~> HOL.times_class.times - op < ~> HOL.ord_class.less - op <= ~> HOL.ord_class.less_eq - -Adaptions may be required in the following cases: - -a) User-defined constants using any of the names "plus", "minus", -"times", "less" or "less_eq". The standard syntax translations for -"+", "-" and "*" may go wrong. INCOMPATIBILITY: use more specific -names. - -b) Variables named "plus", "minus", "times", "less", "less_eq" -INCOMPATIBILITY: use more specific names. - -c) Permutative equations (e.g. "a + b = b + a") -Since the change of names also changes the order of terms, permutative -rewrite rules may get applied in a different order. Experience shows -that this is rarely the case (only two adaptions in the whole Isabelle -distribution). INCOMPATIBILITY: rewrite proofs - -d) ML code directly refering to constant names -This in general only affects hand-written proof tactics, simprocs and -so on. INCOMPATIBILITY: grep your sourcecode and replace names. -Consider using @{const_name} antiquotation. - * Relations less (<) and less_eq (<=) are also available on type bool. Modified syntax to disallow nesting without explicit parentheses, e.g. "(x < y) < z" or "x < (y < z)", but NOT "x < y < z". Potential