diff -r 94c5aaf32269 -r 1246d847b8c1 NEWS --- a/NEWS Wed May 02 20:15:31 2012 +0200 +++ b/NEWS Wed May 02 20:31:15 2012 +0200 @@ -47,10 +47,8 @@ * Bundled declarations associate attributed fact expressions with a given name in the context. These may be later included in other contexts. This allows to manage context extensions casually, without -the logical dependencies of locales and locale interpretation. - -See commands 'bundle', 'include', 'including' etc. in the isar-ref -manual. +the logical dependencies of locales and locale interpretation. See +commands 'bundle', 'include', 'including' etc. in the isar-ref manual. * Commands 'lemmas' and 'theorems' allow local variables using 'for' declaration, and results are standardized before being stored. Thus @@ -91,6 +89,11 @@ into the user context. Minor INCOMPATIBILITY, may use the regular "def" result with attribute "abs_def" to imitate the old version. +* Attribute "abs_def" turns an equation of the form "f x y == t" into +"f == %x y. t", which ensures that "simp" or "unfold" steps always +expand it. This also works for object-logic equality. (Formerly +undocumented feature.) + * Renamed some inner syntax categories: num ~> num_token @@ -105,11 +108,6 @@ "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref manual. Minor INCOMPATIBILITY. -* Attribute "abs_def" turns an equation of the form "f x y == t" into -"f == %x y. t", which ensures that "simp" or "unfold" steps always -expand it. This also works for object-logic equality. (Formerly -undocumented feature.) - * Obsolete command 'types' has been discontinued. Use 'type_synonym' instead. INCOMPATIBILITY. @@ -136,29 +134,38 @@ lemma "P (x::'a)" and "Q (y::'a::bar)" -- "now uniform 'a::bar instead of default sort for first occurrence (!)" +* Discontinued configuration option "syntax_positions": atomic terms +in parse trees are always annotated by position constraints. + *** HOL *** * Type 'a set is now a proper type constructor (just as before Isabelle2008). Definitions mem_def and Collect_def have disappeared. Non-trivial INCOMPATIBILITY. For developments keeping predicates and -sets separate, it is often sufficient to rephrase sets S accidentally -used as predicates by "%x. x : S" and predicates P accidentally used -as sets by "{x. P x}". Corresponding proofs in a first step should be -pruned from any tinkering with former theorems mem_def and Collect_def -as far as possible. - -For developments which deliberately mixed predicates and sets, a +sets separate, it is often sufficient to rephrase some set S that has +been accidentally used as predicates by "%x. x : S", and some +predicate P that has been accidentally used as set by "{x. P x}". +Corresponding proofs in a first step should be pruned from any +tinkering with former theorems mem_def and Collect_def as far as +possible. + +For developments which deliberately mix predicates and sets, a planning step is necessary to determine what should become a predicate and what a set. It can be helpful to carry out that step in Isabelle2011-1 before jumping right into the current release. +* Code generation by default implements sets as container type rather +than predicates. INCOMPATIBILITY. + +* New type synonym 'a rel = ('a * 'a) set + * The representation of numerals has changed. Datatype "num" represents strictly positive binary numerals, along with functions "numeral :: num => 'a" and "neg_numeral :: num => 'a" to represent -positive and negated numeric literals, respectively. (See definitions -in ~~/src/HOL/Num.thy.) Potential INCOMPATIBILITY, some user theories -may require adaptations as follows: +positive and negated numeric literals, respectively. See also +definitions in ~~/src/HOL/Num.thy. Potential INCOMPATIBILITY, some +user theories may require adaptations as follows: - Theorems with number_ring or number_semiring constraints: These classes are gone; use comm_ring_1 or comm_semiring_1 instead. @@ -177,18 +184,8 @@ - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1: Redefine using other integer operations. -* Code generation by default implements sets as container type rather -than predicates. INCOMPATIBILITY. - * Records: code generation can be switched off manually with -declare [[record_coden = false]]. Default remains true. - -* HOL-Import: Re-implementation from scratch is faster, simpler, and -more scalable. Requires a proof bundle, which is available as an -external component. Discontinued old (and mostly dead) Importer for -HOL4 and HOL Light. INCOMPATIBILITY. - -* New type synonym 'a rel = ('a * 'a) set +declare [[record_coden = false]]. Default remains true. * New "case_product" attribute to generate a case rule doing multiple case distinctions at the same time. E.g. @@ -198,11 +195,11 @@ produces a rule which can be used to perform case distinction on both a list and a nat. -* Transfer: New package intended to generalize the existing descending -method and related theorem attributes from the Quotient package. (Not -all functionality is implemented yet, but future development will -focus on Transfer as an eventual replacement for the corresponding -parts of the Quotient package.) +* Transfer: New package intended to generalize the existing +"descending" method and related theorem attributes from the Quotient +package. (Not all functionality is implemented yet, but future +development will focus on Transfer as an eventual replacement for the +corresponding parts of the Quotient package.) - transfer_rule attribute: Maintains a collection of transfer rules, which relate constants at two different types. Transfer rules may @@ -218,7 +215,7 @@ replaced with corresponding ones according to the transfer rules. Goals are generalized over all free variables by default; this is necessary for variables whose types change, but can be overridden - for specific variables with e.g. 'transfer fixing: x y z'. The + for specific variables with e.g. "transfer fixing: x y z". The variant transfer' method allows replacing a subgoal with one that is logically stronger (rather than equivalent). @@ -317,9 +314,8 @@ - Added "quickcheck_locale" configuration to specify how to process conjectures in a locale context. -* Nitpick: - - Fixed infinite loop caused by the 'peephole_optim' option and - affecting 'rat' and 'real'. +* Nitpick: Fixed infinite loop caused by the 'peephole_optim' option +and affecting 'rat' and 'real'. * Sledgehammer: - Integrated more tightly with SPASS, as described in the ITP 2012 @@ -333,23 +329,31 @@ - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice"). - Renamed "sound" option to "strict". -* Metis: - - Added possibility to specify lambda translations scheme as a - parenthesized argument (e.g., "by (metis (lifting) ...)"). - -* SMT: - - Renamed "smt_fixed" option to "smt_read_only_certificates". - -* Command 'try0': - - Renamed from 'try_methods'. INCOMPATIBILITY. +* Metis: Added possibility to specify lambda translations scheme as a +parenthesized argument (e.g., "by (metis (lifting) ...)"). + +* SMT: Renamed "smt_fixed" option to "smt_read_only_certificates". + +* Command 'try0': Renamed from 'try_methods'. INCOMPATIBILITY. * New "eventually_elim" method as a generalized variant of the -eventually_elim* rules. Supports structured proofs. +eventually_elim* rules. Supports structured proofs. + +* 'datatype' specifications allow explicit sort constraints. * Typedef with implicit set definition is considered legacy. Use "typedef (open)" form instead, which will eventually become the default. +* Concrete syntax for case expressions includes constraints for source +positions, and thus produces Prover IDE markup for its bindings. +INCOMPATIBILITY for old-style syntax translations that augment the +pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of +one_case. + +* Clarified attribute "mono_set": pure declaration without modifying +the result of the fact expression. + * More default pred/set conversions on a couple of relation operations and predicates. Added powers of predicate relations. Consolidation of some relation theorems: @@ -512,16 +516,7 @@ * Congruence rules Option.map_cong and Option.bind_cong for recursion through option types. -* Concrete syntax for case expressions includes constraints for source -positions, and thus produces Prover IDE markup for its bindings. -INCOMPATIBILITY for old-style syntax translations that augment the -pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of -one_case. - -* Discontinued configuration option "syntax_positions": atomic terms -in parse trees are always annotated by position constraints. - -* HOL/Library/Set_Algebras.thy: Addition and multiplication on sets +* Theory HOL/Library/Set_Algebras: Addition and multiplication on sets are expressed via type classes again. The special syntax \/\ has been replaced by plain +/*. Removed constant setsum_set, which is now subsumed by Big_Operators.setsum. @@ -530,8 +525,6 @@ * New theory HOL/Library/DAList provides an abstract type for association lists with distinct keys. -* 'datatype' specifications allow explicit sort constraints. - * Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY, use theory HOL/Library/Nat_Bijection instead. @@ -711,55 +704,6 @@ real_of_float_neg_exp, real_of_float_nge0_exp, round_down floor_fl, round_up, zero_le_float, zero_less_float -* Session HOL-Word: Discontinued many redundant theorems specific to -type 'a word. INCOMPATIBILITY, use the corresponding generic theorems -instead. - - word_sub_alt ~> word_sub_wi - word_add_alt ~> word_add_def - word_mult_alt ~> word_mult_def - word_minus_alt ~> word_minus_def - word_0_alt ~> word_0_wi - word_1_alt ~> word_1_wi - word_add_0 ~> add_0_left - word_add_0_right ~> add_0_right - word_mult_1 ~> mult_1_left - word_mult_1_right ~> mult_1_right - word_add_commute ~> add_commute - word_add_assoc ~> add_assoc - word_add_left_commute ~> add_left_commute - word_mult_commute ~> mult_commute - word_mult_assoc ~> mult_assoc - word_mult_left_commute ~> mult_left_commute - word_left_distrib ~> left_distrib - word_right_distrib ~> right_distrib - word_left_minus ~> left_minus - word_diff_0_right ~> diff_0_right - word_diff_self ~> diff_self - word_sub_def ~> diff_minus - word_diff_minus ~> diff_minus - word_add_ac ~> add_ac - word_mult_ac ~> mult_ac - word_plus_ac0 ~> add_0_left add_0_right add_ac - word_times_ac1 ~> mult_1_left mult_1_right mult_ac - word_order_trans ~> order_trans - word_order_refl ~> order_refl - word_order_antisym ~> order_antisym - word_order_linear ~> linorder_linear - lenw1_zero_neq_one ~> zero_neq_one - word_number_of_eq ~> number_of_eq - word_of_int_add_hom ~> wi_hom_add - word_of_int_sub_hom ~> wi_hom_sub - word_of_int_mult_hom ~> wi_hom_mult - word_of_int_minus_hom ~> wi_hom_neg - word_of_int_succ_hom ~> wi_hom_succ - word_of_int_pred_hom ~> wi_hom_pred - word_of_int_0_hom ~> word_0_wi - word_of_int_1_hom ~> word_1_wi - -* Clarified attribute "mono_set": pure declaration without modifying -the result of the fact expression. - * "Transitive_Closure.ntrancl": bounded transitive closure on relations. @@ -807,6 +751,57 @@ DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing +* Session HOL-Import: Re-implementation from scratch is faster, +simpler, and more scalable. Requires a proof bundle, which is +available as an external component. Discontinued old (and mostly +dead) Importer for HOL4 and HOL Light. INCOMPATIBILITY. + +* Session HOL-Word: Discontinued many redundant theorems specific to +type 'a word. INCOMPATIBILITY, use the corresponding generic theorems +instead. + + word_sub_alt ~> word_sub_wi + word_add_alt ~> word_add_def + word_mult_alt ~> word_mult_def + word_minus_alt ~> word_minus_def + word_0_alt ~> word_0_wi + word_1_alt ~> word_1_wi + word_add_0 ~> add_0_left + word_add_0_right ~> add_0_right + word_mult_1 ~> mult_1_left + word_mult_1_right ~> mult_1_right + word_add_commute ~> add_commute + word_add_assoc ~> add_assoc + word_add_left_commute ~> add_left_commute + word_mult_commute ~> mult_commute + word_mult_assoc ~> mult_assoc + word_mult_left_commute ~> mult_left_commute + word_left_distrib ~> left_distrib + word_right_distrib ~> right_distrib + word_left_minus ~> left_minus + word_diff_0_right ~> diff_0_right + word_diff_self ~> diff_self + word_sub_def ~> diff_minus + word_diff_minus ~> diff_minus + word_add_ac ~> add_ac + word_mult_ac ~> mult_ac + word_plus_ac0 ~> add_0_left add_0_right add_ac + word_times_ac1 ~> mult_1_left mult_1_right mult_ac + word_order_trans ~> order_trans + word_order_refl ~> order_refl + word_order_antisym ~> order_antisym + word_order_linear ~> linorder_linear + lenw1_zero_neq_one ~> zero_neq_one + word_number_of_eq ~> number_of_eq + word_of_int_add_hom ~> wi_hom_add + word_of_int_sub_hom ~> wi_hom_sub + word_of_int_mult_hom ~> wi_hom_mult + word_of_int_minus_hom ~> wi_hom_neg + word_of_int_succ_hom ~> wi_hom_succ + word_of_int_pred_hom ~> wi_hom_pred + word_of_int_0_hom ~> word_0_wi + word_of_int_1_hom ~> word_1_wi + * Theory Library/Multiset: Improved code generation of multisets. * Session HOL-Word: New proof method "word_bitwise" for splitting @@ -991,8 +986,8 @@ sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq space_product_algebra -> space_PiM -* HOL/TPTP: support to parse and import TPTP problems (all languages) -into Isabelle/HOL. +* Session HOL-TPTP: support to parse and import TPTP problems (all +languages) into Isabelle/HOL. *** FOL ***