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