author | wenzelm |

Fri Apr 27 21:24:30 2012 +0200 (2012-04-27) | |

changeset 47809 | 4d8cbea248b0 |

parent 47808 | 04a6a6c03eea |

child 47810 | 9579464d00f9 |

child 47813 | 18de60b8c906 |

mention tools and packages earlier;

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