some re-ordering;
authorwenzelm
Wed May 02 20:31:15 2012 +0200 (2012-05-02)
changeset 478551246d847b8c1
parent 47854 94c5aaf32269
child 47856 57d1df2f2a0f
some re-ordering;
NEWS
     1.1 --- a/NEWS	Wed May 02 20:15:31 2012 +0200
     1.2 +++ b/NEWS	Wed May 02 20:31:15 2012 +0200
     1.3 @@ -47,10 +47,8 @@
     1.4  * Bundled declarations associate attributed fact expressions with a
     1.5  given name in the context.  These may be later included in other
     1.6  contexts.  This allows to manage context extensions casually, without
     1.7 -the logical dependencies of locales and locale interpretation.
     1.8 -
     1.9 -See commands 'bundle', 'include', 'including' etc. in the isar-ref
    1.10 -manual.
    1.11 +the logical dependencies of locales and locale interpretation.  See
    1.12 +commands 'bundle', 'include', 'including' etc. in the isar-ref manual.
    1.13  
    1.14  * Commands 'lemmas' and 'theorems' allow local variables using 'for'
    1.15  declaration, and results are standardized before being stored.  Thus
    1.16 @@ -91,6 +89,11 @@
    1.17  into the user context.  Minor INCOMPATIBILITY, may use the regular
    1.18  "def" result with attribute "abs_def" to imitate the old version.
    1.19  
    1.20 +* Attribute "abs_def" turns an equation of the form "f x y == t" into
    1.21 +"f == %x y. t", which ensures that "simp" or "unfold" steps always
    1.22 +expand it.  This also works for object-logic equality.  (Formerly
    1.23 +undocumented feature.)
    1.24 +
    1.25  * Renamed some inner syntax categories:
    1.26  
    1.27      num ~> num_token
    1.28 @@ -105,11 +108,6 @@
    1.29  "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
    1.30  manual.  Minor INCOMPATIBILITY.
    1.31  
    1.32 -* Attribute "abs_def" turns an equation of the form "f x y == t" into
    1.33 -"f == %x y. t", which ensures that "simp" or "unfold" steps always
    1.34 -expand it.  This also works for object-logic equality.  (Formerly
    1.35 -undocumented feature.)
    1.36 -
    1.37  * Obsolete command 'types' has been discontinued.  Use 'type_synonym'
    1.38  instead.  INCOMPATIBILITY.
    1.39  
    1.40 @@ -136,29 +134,38 @@
    1.41    lemma "P (x::'a)" and "Q (y::'a::bar)"
    1.42      -- "now uniform 'a::bar instead of default sort for first occurrence (!)"
    1.43  
    1.44 +* Discontinued configuration option "syntax_positions": atomic terms
    1.45 +in parse trees are always annotated by position constraints.
    1.46 +
    1.47  
    1.48  *** HOL ***
    1.49  
    1.50  * Type 'a set is now a proper type constructor (just as before
    1.51  Isabelle2008).  Definitions mem_def and Collect_def have disappeared.
    1.52  Non-trivial INCOMPATIBILITY.  For developments keeping predicates and
    1.53 -sets separate, it is often sufficient to rephrase sets S accidentally
    1.54 -used as predicates by "%x. x : S" and predicates P accidentally used
    1.55 -as sets by "{x. P x}".  Corresponding proofs in a first step should be
    1.56 -pruned from any tinkering with former theorems mem_def and Collect_def
    1.57 -as far as possible.
    1.58 -
    1.59 -For developments which deliberately mixed predicates and sets, a
    1.60 +sets separate, it is often sufficient to rephrase some set S that has
    1.61 +been accidentally used as predicates by "%x. x : S", and some
    1.62 +predicate P that has been accidentally used as set by "{x. P x}".
    1.63 +Corresponding proofs in a first step should be pruned from any
    1.64 +tinkering with former theorems mem_def and Collect_def as far as
    1.65 +possible.
    1.66 +
    1.67 +For developments which deliberately mix predicates and sets, a
    1.68  planning step is necessary to determine what should become a predicate
    1.69  and what a set.  It can be helpful to carry out that step in
    1.70  Isabelle2011-1 before jumping right into the current release.
    1.71  
    1.72 +* Code generation by default implements sets as container type rather
    1.73 +than predicates.  INCOMPATIBILITY.
    1.74 +
    1.75 +* New type synonym 'a rel = ('a * 'a) set
    1.76 +
    1.77  * The representation of numerals has changed.  Datatype "num"
    1.78  represents strictly positive binary numerals, along with functions
    1.79  "numeral :: num => 'a" and "neg_numeral :: num => 'a" to represent
    1.80 -positive and negated numeric literals, respectively. (See definitions
    1.81 -in ~~/src/HOL/Num.thy.) Potential INCOMPATIBILITY, some user theories
    1.82 -may require adaptations as follows:
    1.83 +positive and negated numeric literals, respectively.  See also
    1.84 +definitions in ~~/src/HOL/Num.thy.  Potential INCOMPATIBILITY, some
    1.85 +user theories may require adaptations as follows:
    1.86  
    1.87    - Theorems with number_ring or number_semiring constraints: These
    1.88      classes are gone; use comm_ring_1 or comm_semiring_1 instead.
    1.89 @@ -177,18 +184,8 @@
    1.90    - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:
    1.91      Redefine using other integer operations.
    1.92  
    1.93 -* Code generation by default implements sets as container type rather
    1.94 -than predicates.  INCOMPATIBILITY.
    1.95 -
    1.96  * Records: code generation can be switched off manually with 
    1.97 -declare [[record_coden = false]]. Default remains true.
    1.98 -
    1.99 -* HOL-Import: Re-implementation from scratch is faster, simpler, and
   1.100 -more scalable.  Requires a proof bundle, which is available as an
   1.101 -external component.  Discontinued old (and mostly dead) Importer for
   1.102 -HOL4 and HOL Light.  INCOMPATIBILITY.
   1.103 -
   1.104 -* New type synonym 'a rel = ('a * 'a) set
   1.105 +declare [[record_coden = false]].  Default remains true.
   1.106  
   1.107  * New "case_product" attribute to generate a case rule doing multiple
   1.108  case distinctions at the same time.  E.g.
   1.109 @@ -198,11 +195,11 @@
   1.110  produces a rule which can be used to perform case distinction on both
   1.111  a list and a nat.
   1.112  
   1.113 -* Transfer: New package intended to generalize the existing descending
   1.114 -method and related theorem attributes from the Quotient package. (Not
   1.115 -all functionality is implemented yet, but future development will
   1.116 -focus on Transfer as an eventual replacement for the corresponding
   1.117 -parts of the Quotient package.)
   1.118 +* Transfer: New package intended to generalize the existing
   1.119 +"descending" method and related theorem attributes from the Quotient
   1.120 +package.  (Not all functionality is implemented yet, but future
   1.121 +development will focus on Transfer as an eventual replacement for the
   1.122 +corresponding parts of the Quotient package.)
   1.123  
   1.124    - transfer_rule attribute: Maintains a collection of transfer rules,
   1.125      which relate constants at two different types. Transfer rules may
   1.126 @@ -218,7 +215,7 @@
   1.127      replaced with corresponding ones according to the transfer rules.
   1.128      Goals are generalized over all free variables by default; this is
   1.129      necessary for variables whose types change, but can be overridden
   1.130 -    for specific variables with e.g. 'transfer fixing: x y z'.  The
   1.131 +    for specific variables with e.g. "transfer fixing: x y z".  The
   1.132      variant transfer' method allows replacing a subgoal with one that
   1.133      is logically stronger (rather than equivalent).
   1.134  
   1.135 @@ -317,9 +314,8 @@
   1.136    - Added "quickcheck_locale" configuration to specify how to process
   1.137      conjectures in a locale context.
   1.138  
   1.139 -* Nitpick:
   1.140 -  - Fixed infinite loop caused by the 'peephole_optim' option and
   1.141 -    affecting 'rat' and 'real'.
   1.142 +* Nitpick: Fixed infinite loop caused by the 'peephole_optim' option
   1.143 +and affecting 'rat' and 'real'.
   1.144  
   1.145  * Sledgehammer:
   1.146    - Integrated more tightly with SPASS, as described in the ITP 2012
   1.147 @@ -333,23 +329,31 @@
   1.148    - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
   1.149    - Renamed "sound" option to "strict".
   1.150  
   1.151 -* Metis:
   1.152 -  - Added possibility to specify lambda translations scheme as a
   1.153 -    parenthesized argument (e.g., "by (metis (lifting) ...)").
   1.154 -
   1.155 -* SMT:
   1.156 -  - Renamed "smt_fixed" option to "smt_read_only_certificates".
   1.157 -
   1.158 -* Command 'try0':
   1.159 -  - Renamed from 'try_methods'. INCOMPATIBILITY.
   1.160 +* Metis: Added possibility to specify lambda translations scheme as a
   1.161 +parenthesized argument (e.g., "by (metis (lifting) ...)").
   1.162 +
   1.163 +* SMT: Renamed "smt_fixed" option to "smt_read_only_certificates".
   1.164 +
   1.165 +* Command 'try0': Renamed from 'try_methods'. INCOMPATIBILITY.
   1.166  
   1.167  * New "eventually_elim" method as a generalized variant of the
   1.168 -eventually_elim* rules. Supports structured proofs.
   1.169 +eventually_elim* rules.  Supports structured proofs.
   1.170 +
   1.171 +* 'datatype' specifications allow explicit sort constraints.
   1.172  
   1.173  * Typedef with implicit set definition is considered legacy.  Use
   1.174  "typedef (open)" form instead, which will eventually become the
   1.175  default.
   1.176  
   1.177 +* Concrete syntax for case expressions includes constraints for source
   1.178 +positions, and thus produces Prover IDE markup for its bindings.
   1.179 +INCOMPATIBILITY for old-style syntax translations that augment the
   1.180 +pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
   1.181 +one_case.
   1.182 +
   1.183 +* Clarified attribute "mono_set": pure declaration without modifying
   1.184 +the result of the fact expression.
   1.185 +
   1.186  * More default pred/set conversions on a couple of relation operations
   1.187  and predicates.  Added powers of predicate relations.  Consolidation
   1.188  of some relation theorems:
   1.189 @@ -512,16 +516,7 @@
   1.190  * Congruence rules Option.map_cong and Option.bind_cong for recursion
   1.191  through option types.
   1.192  
   1.193 -* Concrete syntax for case expressions includes constraints for source
   1.194 -positions, and thus produces Prover IDE markup for its bindings.
   1.195 -INCOMPATIBILITY for old-style syntax translations that augment the
   1.196 -pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
   1.197 -one_case.
   1.198 -
   1.199 -* Discontinued configuration option "syntax_positions": atomic terms
   1.200 -in parse trees are always annotated by position constraints.
   1.201 -
   1.202 -* HOL/Library/Set_Algebras.thy: Addition and multiplication on sets
   1.203 +* Theory HOL/Library/Set_Algebras: Addition and multiplication on sets
   1.204  are expressed via type classes again. The special syntax
   1.205  \<oplus>/\<otimes> has been replaced by plain +/*. Removed constant
   1.206  setsum_set, which is now subsumed by Big_Operators.setsum.
   1.207 @@ -530,8 +525,6 @@
   1.208  * New theory HOL/Library/DAList provides an abstract type for
   1.209  association lists with distinct keys.
   1.210  
   1.211 -* 'datatype' specifications allow explicit sort constraints.
   1.212 -
   1.213  * Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,
   1.214  use theory HOL/Library/Nat_Bijection instead.
   1.215  
   1.216 @@ -711,55 +704,6 @@
   1.217    real_of_float_neg_exp, real_of_float_nge0_exp, round_down floor_fl,
   1.218    round_up, zero_le_float, zero_less_float
   1.219  
   1.220 -* Session HOL-Word: Discontinued many redundant theorems specific to
   1.221 -type 'a word. INCOMPATIBILITY, use the corresponding generic theorems
   1.222 -instead.
   1.223 -
   1.224 -  word_sub_alt ~> word_sub_wi
   1.225 -  word_add_alt ~> word_add_def
   1.226 -  word_mult_alt ~> word_mult_def
   1.227 -  word_minus_alt ~> word_minus_def
   1.228 -  word_0_alt ~> word_0_wi
   1.229 -  word_1_alt ~> word_1_wi
   1.230 -  word_add_0 ~> add_0_left
   1.231 -  word_add_0_right ~> add_0_right
   1.232 -  word_mult_1 ~> mult_1_left
   1.233 -  word_mult_1_right ~> mult_1_right
   1.234 -  word_add_commute ~> add_commute
   1.235 -  word_add_assoc ~> add_assoc
   1.236 -  word_add_left_commute ~> add_left_commute
   1.237 -  word_mult_commute ~> mult_commute
   1.238 -  word_mult_assoc ~> mult_assoc
   1.239 -  word_mult_left_commute ~> mult_left_commute
   1.240 -  word_left_distrib ~> left_distrib
   1.241 -  word_right_distrib ~> right_distrib
   1.242 -  word_left_minus ~> left_minus
   1.243 -  word_diff_0_right ~> diff_0_right
   1.244 -  word_diff_self ~> diff_self
   1.245 -  word_sub_def ~> diff_minus
   1.246 -  word_diff_minus ~> diff_minus
   1.247 -  word_add_ac ~> add_ac
   1.248 -  word_mult_ac ~> mult_ac
   1.249 -  word_plus_ac0 ~> add_0_left add_0_right add_ac
   1.250 -  word_times_ac1 ~> mult_1_left mult_1_right mult_ac
   1.251 -  word_order_trans ~> order_trans
   1.252 -  word_order_refl ~> order_refl
   1.253 -  word_order_antisym ~> order_antisym
   1.254 -  word_order_linear ~> linorder_linear
   1.255 -  lenw1_zero_neq_one ~> zero_neq_one
   1.256 -  word_number_of_eq ~> number_of_eq
   1.257 -  word_of_int_add_hom ~> wi_hom_add
   1.258 -  word_of_int_sub_hom ~> wi_hom_sub
   1.259 -  word_of_int_mult_hom ~> wi_hom_mult
   1.260 -  word_of_int_minus_hom ~> wi_hom_neg
   1.261 -  word_of_int_succ_hom ~> wi_hom_succ
   1.262 -  word_of_int_pred_hom ~> wi_hom_pred
   1.263 -  word_of_int_0_hom ~> word_0_wi
   1.264 -  word_of_int_1_hom ~> word_1_wi
   1.265 -
   1.266 -* Clarified attribute "mono_set": pure declaration without modifying
   1.267 -the result of the fact expression.
   1.268 -
   1.269  * "Transitive_Closure.ntrancl": bounded transitive closure on
   1.270  relations.
   1.271  
   1.272 @@ -807,6 +751,57 @@
   1.273  
   1.274    DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing
   1.275  
   1.276 +* Session HOL-Import: Re-implementation from scratch is faster,
   1.277 +simpler, and more scalable.  Requires a proof bundle, which is
   1.278 +available as an external component.  Discontinued old (and mostly
   1.279 +dead) Importer for HOL4 and HOL Light.  INCOMPATIBILITY.
   1.280 +
   1.281 +* Session HOL-Word: Discontinued many redundant theorems specific to
   1.282 +type 'a word. INCOMPATIBILITY, use the corresponding generic theorems
   1.283 +instead.
   1.284 +
   1.285 +  word_sub_alt ~> word_sub_wi
   1.286 +  word_add_alt ~> word_add_def
   1.287 +  word_mult_alt ~> word_mult_def
   1.288 +  word_minus_alt ~> word_minus_def
   1.289 +  word_0_alt ~> word_0_wi
   1.290 +  word_1_alt ~> word_1_wi
   1.291 +  word_add_0 ~> add_0_left
   1.292 +  word_add_0_right ~> add_0_right
   1.293 +  word_mult_1 ~> mult_1_left
   1.294 +  word_mult_1_right ~> mult_1_right
   1.295 +  word_add_commute ~> add_commute
   1.296 +  word_add_assoc ~> add_assoc
   1.297 +  word_add_left_commute ~> add_left_commute
   1.298 +  word_mult_commute ~> mult_commute
   1.299 +  word_mult_assoc ~> mult_assoc
   1.300 +  word_mult_left_commute ~> mult_left_commute
   1.301 +  word_left_distrib ~> left_distrib
   1.302 +  word_right_distrib ~> right_distrib
   1.303 +  word_left_minus ~> left_minus
   1.304 +  word_diff_0_right ~> diff_0_right
   1.305 +  word_diff_self ~> diff_self
   1.306 +  word_sub_def ~> diff_minus
   1.307 +  word_diff_minus ~> diff_minus
   1.308 +  word_add_ac ~> add_ac
   1.309 +  word_mult_ac ~> mult_ac
   1.310 +  word_plus_ac0 ~> add_0_left add_0_right add_ac
   1.311 +  word_times_ac1 ~> mult_1_left mult_1_right mult_ac
   1.312 +  word_order_trans ~> order_trans
   1.313 +  word_order_refl ~> order_refl
   1.314 +  word_order_antisym ~> order_antisym
   1.315 +  word_order_linear ~> linorder_linear
   1.316 +  lenw1_zero_neq_one ~> zero_neq_one
   1.317 +  word_number_of_eq ~> number_of_eq
   1.318 +  word_of_int_add_hom ~> wi_hom_add
   1.319 +  word_of_int_sub_hom ~> wi_hom_sub
   1.320 +  word_of_int_mult_hom ~> wi_hom_mult
   1.321 +  word_of_int_minus_hom ~> wi_hom_neg
   1.322 +  word_of_int_succ_hom ~> wi_hom_succ
   1.323 +  word_of_int_pred_hom ~> wi_hom_pred
   1.324 +  word_of_int_0_hom ~> word_0_wi
   1.325 +  word_of_int_1_hom ~> word_1_wi
   1.326 +
   1.327  * Theory Library/Multiset: Improved code generation of multisets.
   1.328  
   1.329  * Session HOL-Word: New proof method "word_bitwise" for splitting
   1.330 @@ -991,8 +986,8 @@
   1.331    sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq
   1.332    space_product_algebra -> space_PiM
   1.333  
   1.334 -* HOL/TPTP: support to parse and import TPTP problems (all languages)
   1.335 -into Isabelle/HOL.
   1.336 +* Session HOL-TPTP: support to parse and import TPTP problems (all
   1.337 +languages) into Isabelle/HOL.
   1.338  
   1.339  
   1.340  *** FOL ***