mention tools and packages earlier;
authorwenzelm
Fri Apr 27 21:24:30 2012 +0200 (2012-04-27)
changeset 478094d8cbea248b0
parent 47808 04a6a6c03eea
child 47810 9579464d00f9
child 47813 18de60b8c906
mention tools and packages earlier;
NEWS
     1.1 --- a/NEWS	Fri Apr 27 21:17:35 2012 +0200
     1.2 +++ b/NEWS	Fri Apr 27 21:24:30 2012 +0200
     1.3 @@ -186,6 +186,157 @@
     1.4  
     1.5  * New type synonym 'a rel = ('a * 'a) set
     1.6  
     1.7 +* New "case_product" attribute to generate a case rule doing multiple
     1.8 +case distinctions at the same time.  E.g.
     1.9 +
    1.10 +  list.exhaust [case_product nat.exhaust]
    1.11 +
    1.12 +produces a rule which can be used to perform case distinction on both
    1.13 +a list and a nat.
    1.14 +
    1.15 +* New Transfer package:
    1.16 +
    1.17 +  - transfer_rule attribute: Maintains a collection of transfer rules,
    1.18 +    which relate constants at two different types. Transfer rules may
    1.19 +    relate different type instances of the same polymorphic constant,
    1.20 +    or they may relate an operation on a raw type to a corresponding
    1.21 +    operation on an abstract type (quotient or subtype). For example:
    1.22 +
    1.23 +    ((A ===> B) ===> list_all2 A ===> list_all2 B) map map
    1.24 +    (cr_int ===> cr_int ===> cr_int) (%(x,y) (u,v). (x+u, y+v)) plus_int
    1.25 +
    1.26 +  - transfer method: Replaces a subgoal on abstract types with an
    1.27 +    equivalent subgoal on the corresponding raw types. Constants are
    1.28 +    replaced with corresponding ones according to the transfer rules.
    1.29 +    Goals are generalized over all free variables by default; this is
    1.30 +    necessary for variables whose types changes, but can be overridden
    1.31 +    for specific variables with e.g. 'transfer fixing: x y z'.  The
    1.32 +    variant transfer' method allows replacing a subgoal with one that
    1.33 +    is logically stronger (rather than equivalent).
    1.34 +
    1.35 +  - relator_eq attribute: Collects identity laws for relators of
    1.36 +    various type constructors, e.g. "list_all2 (op =) = (op =)".  The
    1.37 +    transfer method uses these lemmas to infer transfer rules for
    1.38 +    non-polymorphic constants on the fly.
    1.39 +
    1.40 +  - transfer_prover method: Assists with proving a transfer rule for a
    1.41 +    new constant, provided the constant is defined in terms of other
    1.42 +    constants that already have transfer rules. It should be applied
    1.43 +    after unfolding the constant definitions.
    1.44 +
    1.45 +  - HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer
    1.46 +    from type nat to type int.
    1.47 +
    1.48 +* New Lifting package:
    1.49 +
    1.50 +  - lift_definition command: Defines operations on an abstract type in
    1.51 +    terms of a corresponding operation on a representation
    1.52 +    type.  Example syntax:
    1.53 +
    1.54 +    lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist"
    1.55 +      is List.insert
    1.56 +
    1.57 +    Users must discharge a respectfulness proof obligation when each
    1.58 +    constant is defined. (For a type copy, i.e. a typedef with UNIV,
    1.59 +    the proof is discharged automatically.) The obligation is
    1.60 +    presented in a user-friendly, readable form; a respectfulness
    1.61 +    theorem in the standard format and a transfer rule are generated
    1.62 +    by the package.
    1.63 +
    1.64 +  - Integration with code_abstype: For typedefs (e.g. subtypes
    1.65 +    corresponding to a datatype invariant, such as dlist),
    1.66 +    lift_definition generates a code certificate theorem and sets up
    1.67 +    code generation for each constant.
    1.68 +
    1.69 +  - setup_lifting command: Sets up the Lifting package to work with a
    1.70 +    user-defined type. The user must provide either a quotient theorem
    1.71 +    or a type_definition theorem.  The package configures transfer
    1.72 +    rules for equality and quantifiers on the type, and sets up the
    1.73 +    lift_definition command to work with the type.
    1.74 +
    1.75 +  - Usage examples: See Quotient_Examples/Lift_DList.thy,
    1.76 +    Quotient_Examples/Lift_RBT.thy, Word/Word.thy and
    1.77 +    Library/Float.thy.
    1.78 +
    1.79 +* Quotient package:
    1.80 +
    1.81 +  - The 'quotient_type' command now supports a 'morphisms' option with
    1.82 +    rep and abs functions, similar to typedef.
    1.83 +
    1.84 +  - 'quotient_type' sets up new types to work with the Lifting and
    1.85 +    Transfer packages, as with 'setup_lifting'.
    1.86 +
    1.87 +  - The 'quotient_definition' command now requires the user to prove a
    1.88 +    respectfulness property at the point where the constant is
    1.89 +    defined, similar to lift_definition; INCOMPATIBILITY.
    1.90 +
    1.91 +  - Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems
    1.92 +    accordingly, INCOMPATIBILITY.
    1.93 +
    1.94 +* New diagnostic command 'find_unused_assms' to find potentially
    1.95 +superfluous assumptions in theorems using Quickcheck.
    1.96 +
    1.97 +* Quickcheck:
    1.98 +
    1.99 +  - Quickcheck returns variable assignments as counterexamples, which
   1.100 +    allows to reveal the underspecification of functions under test.
   1.101 +    For example, refuting "hd xs = x", it presents the variable
   1.102 +    assignment xs = [] and x = a1 as a counterexample, assuming that
   1.103 +    any property is false whenever "hd []" occurs in it.
   1.104 +
   1.105 +    These counterexample are marked as potentially spurious, as
   1.106 +    Quickcheck also returns "xs = []" as a counterexample to the
   1.107 +    obvious theorem "hd xs = hd xs".
   1.108 +
   1.109 +    After finding a potentially spurious counterexample, Quickcheck
   1.110 +    continues searching for genuine ones.
   1.111 +
   1.112 +    By default, Quickcheck shows potentially spurious and genuine
   1.113 +    counterexamples. The option "genuine_only" sets quickcheck to only
   1.114 +    show genuine counterexamples.
   1.115 +
   1.116 +  - The command 'quickcheck_generator' creates random and exhaustive
   1.117 +    value generators for a given type and operations.
   1.118 +
   1.119 +    It generates values by using the operations as if they were
   1.120 +    constructors of that type.
   1.121 +
   1.122 +  - Support for multisets.
   1.123 +
   1.124 +  - Added "use_subtype" options.
   1.125 +
   1.126 +  - Added "quickcheck_locale" configuration to specify how to process
   1.127 +    conjectures in a locale context.
   1.128 +
   1.129 +* Nitpick:
   1.130 +  - Fixed infinite loop caused by the 'peephole_optim' option and
   1.131 +    affecting 'rat' and 'real'.
   1.132 +
   1.133 +* Sledgehammer:
   1.134 +  - Integrated more tightly with SPASS, as described in the ITP 2012
   1.135 +    paper "More SPASS with Isabelle".
   1.136 +  - Made it try "smt" as a fallback if "metis" fails or times out.
   1.137 +  - Added support for the following provers: Alt-Ergo (via Why3 and
   1.138 +    TFF1), iProver, iProver-Eq.
   1.139 +  - Replaced remote E-SInE with remote Satallax in the default setup.
   1.140 +  - Sped up the minimizer.
   1.141 +  - Added "lam_trans", "uncurry_aliases", and "minimize" options.
   1.142 +  - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
   1.143 +  - Renamed "sound" option to "strict".
   1.144 +
   1.145 +* Metis:
   1.146 +  - Added possibility to specify lambda translations scheme as a
   1.147 +    parenthesized argument (e.g., "by (metis (lifting) ...)").
   1.148 +
   1.149 +* SMT:
   1.150 +  - Renamed "smt_fixed" option to "smt_read_only_certificates".
   1.151 +
   1.152 +* Command 'try0':
   1.153 +  - Renamed from 'try_methods'. INCOMPATIBILITY.
   1.154 +
   1.155 +* New "eventually_elim" method as a generalized variant of the
   1.156 +eventually_elim* rules. Supports structured proofs.
   1.157 +
   1.158  * Typedef with implicit set definition is considered legacy.  Use
   1.159  "typedef (open)" form instead, which will eventually become the
   1.160  default.
   1.161 @@ -597,15 +748,6 @@
   1.162    word_of_int_0_hom ~> word_0_wi
   1.163    word_of_int_1_hom ~> word_1_wi
   1.164  
   1.165 -* New proof method "word_bitwise" for splitting machine word
   1.166 -equalities and inequalities into logical circuits, defined in
   1.167 -HOL/Word/WordBitwise.thy.  Supports addition, subtraction,
   1.168 -multiplication, shifting by constants, bitwise operators and numeric
   1.169 -constants.  Requires fixed-length word types, not 'a word.  Solves
   1.170 -many standard word identies outright and converts more into first
   1.171 -order problems amenable to blast or similar.  See also examples in
   1.172 -HOL/Word/Examples/WordExamples.thy.
   1.173 -
   1.174  * Clarified attribute "mono_set": pure declaration without modifying
   1.175  the result of the fact expression.
   1.176  
   1.177 @@ -658,6 +800,15 @@
   1.178  
   1.179  * Theory Library/Multiset: Improved code generation of multisets.
   1.180  
   1.181 +* Session HOL-Word: New proof method "word_bitwise" for splitting
   1.182 +machine word equalities and inequalities into logical circuits,
   1.183 +defined in HOL/Word/WordBitwise.thy.  Supports addition, subtraction,
   1.184 +multiplication, shifting by constants, bitwise operators and numeric
   1.185 +constants.  Requires fixed-length word types, not 'a word.  Solves
   1.186 +many standard word identies outright and converts more into first
   1.187 +order problems amenable to blast or similar.  See also examples in
   1.188 +HOL/Word/Examples/WordExamples.thy.
   1.189 +
   1.190  * Session HOL-Probability: Introduced the type "'a measure" to
   1.191  represent measures, this replaces the records 'a algebra and 'a
   1.192  measure_space.  The locales based on subset_class now have two
   1.193 @@ -831,157 +982,6 @@
   1.194    sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq
   1.195    space_product_algebra -> space_PiM
   1.196  
   1.197 -* New "case_product" attribute to generate a case rule doing multiple
   1.198 -case distinctions at the same time.  E.g.
   1.199 -
   1.200 -  list.exhaust [case_product nat.exhaust]
   1.201 -
   1.202 -produces a rule which can be used to perform case distinction on both
   1.203 -a list and a nat.
   1.204 -
   1.205 -* New Transfer package:
   1.206 -
   1.207 -  - transfer_rule attribute: Maintains a collection of transfer rules,
   1.208 -    which relate constants at two different types. Transfer rules may
   1.209 -    relate different type instances of the same polymorphic constant,
   1.210 -    or they may relate an operation on a raw type to a corresponding
   1.211 -    operation on an abstract type (quotient or subtype). For example:
   1.212 -
   1.213 -    ((A ===> B) ===> list_all2 A ===> list_all2 B) map map
   1.214 -    (cr_int ===> cr_int ===> cr_int) (%(x,y) (u,v). (x+u, y+v)) plus_int
   1.215 -
   1.216 -  - transfer method: Replaces a subgoal on abstract types with an
   1.217 -    equivalent subgoal on the corresponding raw types. Constants are
   1.218 -    replaced with corresponding ones according to the transfer rules.
   1.219 -    Goals are generalized over all free variables by default; this is
   1.220 -    necessary for variables whose types changes, but can be overridden
   1.221 -    for specific variables with e.g. 'transfer fixing: x y z'.  The
   1.222 -    variant transfer' method allows replacing a subgoal with one that
   1.223 -    is logically stronger (rather than equivalent).
   1.224 -
   1.225 -  - relator_eq attribute: Collects identity laws for relators of
   1.226 -    various type constructors, e.g. "list_all2 (op =) = (op =)".  The
   1.227 -    transfer method uses these lemmas to infer transfer rules for
   1.228 -    non-polymorphic constants on the fly.
   1.229 -
   1.230 -  - transfer_prover method: Assists with proving a transfer rule for a
   1.231 -    new constant, provided the constant is defined in terms of other
   1.232 -    constants that already have transfer rules. It should be applied
   1.233 -    after unfolding the constant definitions.
   1.234 -
   1.235 -  - HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer
   1.236 -    from type nat to type int.
   1.237 -
   1.238 -* New Lifting package:
   1.239 -
   1.240 -  - lift_definition command: Defines operations on an abstract type in
   1.241 -    terms of a corresponding operation on a representation
   1.242 -    type.  Example syntax:
   1.243 -
   1.244 -    lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist"
   1.245 -      is List.insert
   1.246 -
   1.247 -    Users must discharge a respectfulness proof obligation when each
   1.248 -    constant is defined. (For a type copy, i.e. a typedef with UNIV,
   1.249 -    the proof is discharged automatically.) The obligation is
   1.250 -    presented in a user-friendly, readable form; a respectfulness
   1.251 -    theorem in the standard format and a transfer rule are generated
   1.252 -    by the package.
   1.253 -
   1.254 -  - Integration with code_abstype: For typedefs (e.g. subtypes
   1.255 -    corresponding to a datatype invariant, such as dlist),
   1.256 -    lift_definition generates a code certificate theorem and sets up
   1.257 -    code generation for each constant.
   1.258 -
   1.259 -  - setup_lifting command: Sets up the Lifting package to work with a
   1.260 -    user-defined type. The user must provide either a quotient theorem
   1.261 -    or a type_definition theorem.  The package configures transfer
   1.262 -    rules for equality and quantifiers on the type, and sets up the
   1.263 -    lift_definition command to work with the type.
   1.264 -
   1.265 -  - Usage examples: See Quotient_Examples/Lift_DList.thy,
   1.266 -    Quotient_Examples/Lift_RBT.thy, Word/Word.thy and
   1.267 -    Library/Float.thy.
   1.268 -
   1.269 -* Quotient package:
   1.270 -
   1.271 -  - The 'quotient_type' command now supports a 'morphisms' option with
   1.272 -    rep and abs functions, similar to typedef.
   1.273 -
   1.274 -  - 'quotient_type' sets up new types to work with the Lifting and
   1.275 -    Transfer packages, as with 'setup_lifting'.
   1.276 -
   1.277 -  - The 'quotient_definition' command now requires the user to prove a
   1.278 -    respectfulness property at the point where the constant is
   1.279 -    defined, similar to lift_definition; INCOMPATIBILITY.
   1.280 -
   1.281 -  - Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems
   1.282 -    accordingly, INCOMPATIBILITY.
   1.283 -
   1.284 -* New diagnostic command 'find_unused_assms' to find potentially
   1.285 -superfluous assumptions in theorems using Quickcheck.
   1.286 -
   1.287 -* Quickcheck:
   1.288 -
   1.289 -  - Quickcheck returns variable assignments as counterexamples, which
   1.290 -    allows to reveal the underspecification of functions under test.
   1.291 -    For example, refuting "hd xs = x", it presents the variable
   1.292 -    assignment xs = [] and x = a1 as a counterexample, assuming that
   1.293 -    any property is false whenever "hd []" occurs in it.
   1.294 -
   1.295 -    These counterexample are marked as potentially spurious, as
   1.296 -    Quickcheck also returns "xs = []" as a counterexample to the
   1.297 -    obvious theorem "hd xs = hd xs".
   1.298 -
   1.299 -    After finding a potentially spurious counterexample, Quickcheck
   1.300 -    continues searching for genuine ones.
   1.301 -
   1.302 -    By default, Quickcheck shows potentially spurious and genuine
   1.303 -    counterexamples. The option "genuine_only" sets quickcheck to only
   1.304 -    show genuine counterexamples.
   1.305 -
   1.306 -  - The command 'quickcheck_generator' creates random and exhaustive
   1.307 -    value generators for a given type and operations.
   1.308 -
   1.309 -    It generates values by using the operations as if they were
   1.310 -    constructors of that type.
   1.311 -
   1.312 -  - Support for multisets.
   1.313 -
   1.314 -  - Added "use_subtype" options.
   1.315 -
   1.316 -  - Added "quickcheck_locale" configuration to specify how to process
   1.317 -    conjectures in a locale context.
   1.318 -
   1.319 -* Nitpick:
   1.320 -  - Fixed infinite loop caused by the 'peephole_optim' option and
   1.321 -    affecting 'rat' and 'real'.
   1.322 -
   1.323 -* Sledgehammer:
   1.324 -  - Integrated more tightly with SPASS, as described in the ITP 2012
   1.325 -    paper "More SPASS with Isabelle".
   1.326 -  - Made it try "smt" as a fallback if "metis" fails or times out.
   1.327 -  - Added support for the following provers: Alt-Ergo (via Why3 and
   1.328 -    TFF1), iProver, iProver-Eq.
   1.329 -  - Replaced remote E-SInE with remote Satallax in the default setup.
   1.330 -  - Sped up the minimizer.
   1.331 -  - Added "lam_trans", "uncurry_aliases", and "minimize" options.
   1.332 -  - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
   1.333 -  - Renamed "sound" option to "strict".
   1.334 -
   1.335 -* Metis:
   1.336 -  - Added possibility to specify lambda translations scheme as a
   1.337 -    parenthesized argument (e.g., "by (metis (lifting) ...)").
   1.338 -
   1.339 -* SMT:
   1.340 -  - Renamed "smt_fixed" option to "smt_read_only_certificates".
   1.341 -
   1.342 -* Command 'try0':
   1.343 -  - Renamed from 'try_methods'. INCOMPATIBILITY.
   1.344 -
   1.345 -* New "eventually_elim" method as a generalized variant of the
   1.346 -eventually_elim* rules. Supports structured proofs.
   1.347 -
   1.348  * HOL/TPTP: support to parse and import TPTP problems (all languages)
   1.349  into Isabelle/HOL.
   1.350