# HG changeset patch # User wenzelm # Date 1335554670 -7200 # Node ID 4d8cbea248b025a449f6346e1965fa23ac2374c4 # Parent 04a6a6c03eeae8211f18783778cc0755005f1b9c mention tools and packages earlier; diff -r 04a6a6c03eea -r 4d8cbea248b0 NEWS --- a/NEWS Fri Apr 27 21:17:35 2012 +0200 +++ b/NEWS Fri Apr 27 21:24:30 2012 +0200 @@ -186,6 +186,157 @@ * New type synonym 'a rel = ('a * 'a) set +* New "case_product" attribute to generate a case rule doing multiple +case distinctions at the same time. E.g. + + list.exhaust [case_product nat.exhaust] + +produces a rule which can be used to perform case distinction on both +a list and a nat. + +* New Transfer package: + + - transfer_rule attribute: Maintains a collection of transfer rules, + which relate constants at two different types. Transfer rules may + relate different type instances of the same polymorphic constant, + or they may relate an operation on a raw type to a corresponding + operation on an abstract type (quotient or subtype). For example: + + ((A ===> B) ===> list_all2 A ===> list_all2 B) map map + (cr_int ===> cr_int ===> cr_int) (%(x,y) (u,v). (x+u, y+v)) plus_int + + - transfer method: Replaces a subgoal on abstract types with an + equivalent subgoal on the corresponding raw types. Constants are + 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 changes, but can be overridden + 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). + + - relator_eq attribute: Collects identity laws for relators of + various type constructors, e.g. "list_all2 (op =) = (op =)". The + transfer method uses these lemmas to infer transfer rules for + non-polymorphic constants on the fly. + + - transfer_prover method: Assists with proving a transfer rule for a + new constant, provided the constant is defined in terms of other + constants that already have transfer rules. It should be applied + after unfolding the constant definitions. + + - HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer + from type nat to type int. + +* New Lifting package: + + - lift_definition command: Defines operations on an abstract type in + terms of a corresponding operation on a representation + type. Example syntax: + + lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist" + is List.insert + + Users must discharge a respectfulness proof obligation when each + constant is defined. (For a type copy, i.e. a typedef with UNIV, + the proof is discharged automatically.) The obligation is + presented in a user-friendly, readable form; a respectfulness + theorem in the standard format and a transfer rule are generated + by the package. + + - Integration with code_abstype: For typedefs (e.g. subtypes + corresponding to a datatype invariant, such as dlist), + lift_definition generates a code certificate theorem and sets up + code generation for each constant. + + - setup_lifting command: Sets up the Lifting package to work with a + user-defined type. The user must provide either a quotient theorem + or a type_definition theorem. The package configures transfer + rules for equality and quantifiers on the type, and sets up the + lift_definition command to work with the type. + + - Usage examples: See Quotient_Examples/Lift_DList.thy, + Quotient_Examples/Lift_RBT.thy, Word/Word.thy and + Library/Float.thy. + +* Quotient package: + + - The 'quotient_type' command now supports a 'morphisms' option with + rep and abs functions, similar to typedef. + + - 'quotient_type' sets up new types to work with the Lifting and + Transfer packages, as with 'setup_lifting'. + + - The 'quotient_definition' command now requires the user to prove a + respectfulness property at the point where the constant is + defined, similar to lift_definition; INCOMPATIBILITY. + + - Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems + accordingly, INCOMPATIBILITY. + +* New diagnostic command 'find_unused_assms' to find potentially +superfluous assumptions in theorems using Quickcheck. + +* Quickcheck: + + - Quickcheck returns variable assignments as counterexamples, which + allows to reveal the underspecification of functions under test. + For example, refuting "hd xs = x", it presents the variable + assignment xs = [] and x = a1 as a counterexample, assuming that + any property is false whenever "hd []" occurs in it. + + These counterexample are marked as potentially spurious, as + Quickcheck also returns "xs = []" as a counterexample to the + obvious theorem "hd xs = hd xs". + + After finding a potentially spurious counterexample, Quickcheck + continues searching for genuine ones. + + By default, Quickcheck shows potentially spurious and genuine + counterexamples. The option "genuine_only" sets quickcheck to only + show genuine counterexamples. + + - The command 'quickcheck_generator' creates random and exhaustive + value generators for a given type and operations. + + It generates values by using the operations as if they were + constructors of that type. + + - Support for multisets. + + - Added "use_subtype" options. + + - 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'. + +* Sledgehammer: + - Integrated more tightly with SPASS, as described in the ITP 2012 + paper "More SPASS with Isabelle". + - Made it try "smt" as a fallback if "metis" fails or times out. + - Added support for the following provers: Alt-Ergo (via Why3 and + TFF1), iProver, iProver-Eq. + - Replaced remote E-SInE with remote Satallax in the default setup. + - Sped up the minimizer. + - Added "lam_trans", "uncurry_aliases", and "minimize" options. + - 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. + +* New "eventually_elim" method as a generalized variant of the +eventually_elim* rules. Supports structured proofs. + * Typedef with implicit set definition is considered legacy. Use "typedef (open)" form instead, which will eventually become the default. @@ -597,15 +748,6 @@ word_of_int_0_hom ~> word_0_wi word_of_int_1_hom ~> word_1_wi -* New proof method "word_bitwise" for splitting machine word -equalities and inequalities into logical circuits, defined in -HOL/Word/WordBitwise.thy. Supports addition, subtraction, -multiplication, shifting by constants, bitwise operators and numeric -constants. Requires fixed-length word types, not 'a word. Solves -many standard word identies outright and converts more into first -order problems amenable to blast or similar. See also examples in -HOL/Word/Examples/WordExamples.thy. - * Clarified attribute "mono_set": pure declaration without modifying the result of the fact expression. @@ -658,6 +800,15 @@ * Theory Library/Multiset: Improved code generation of multisets. +* Session HOL-Word: New proof method "word_bitwise" for splitting +machine word equalities and inequalities into logical circuits, +defined in HOL/Word/WordBitwise.thy. Supports addition, subtraction, +multiplication, shifting by constants, bitwise operators and numeric +constants. Requires fixed-length word types, not 'a word. Solves +many standard word identies outright and converts more into first +order problems amenable to blast or similar. See also examples in +HOL/Word/Examples/WordExamples.thy. + * Session HOL-Probability: Introduced the type "'a measure" to represent measures, this replaces the records 'a algebra and 'a measure_space. The locales based on subset_class now have two @@ -831,157 +982,6 @@ sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq space_product_algebra -> space_PiM -* New "case_product" attribute to generate a case rule doing multiple -case distinctions at the same time. E.g. - - list.exhaust [case_product nat.exhaust] - -produces a rule which can be used to perform case distinction on both -a list and a nat. - -* New Transfer package: - - - transfer_rule attribute: Maintains a collection of transfer rules, - which relate constants at two different types. Transfer rules may - relate different type instances of the same polymorphic constant, - or they may relate an operation on a raw type to a corresponding - operation on an abstract type (quotient or subtype). For example: - - ((A ===> B) ===> list_all2 A ===> list_all2 B) map map - (cr_int ===> cr_int ===> cr_int) (%(x,y) (u,v). (x+u, y+v)) plus_int - - - transfer method: Replaces a subgoal on abstract types with an - equivalent subgoal on the corresponding raw types. Constants are - 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 changes, but can be overridden - 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). - - - relator_eq attribute: Collects identity laws for relators of - various type constructors, e.g. "list_all2 (op =) = (op =)". The - transfer method uses these lemmas to infer transfer rules for - non-polymorphic constants on the fly. - - - transfer_prover method: Assists with proving a transfer rule for a - new constant, provided the constant is defined in terms of other - constants that already have transfer rules. It should be applied - after unfolding the constant definitions. - - - HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer - from type nat to type int. - -* New Lifting package: - - - lift_definition command: Defines operations on an abstract type in - terms of a corresponding operation on a representation - type. Example syntax: - - lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist" - is List.insert - - Users must discharge a respectfulness proof obligation when each - constant is defined. (For a type copy, i.e. a typedef with UNIV, - the proof is discharged automatically.) The obligation is - presented in a user-friendly, readable form; a respectfulness - theorem in the standard format and a transfer rule are generated - by the package. - - - Integration with code_abstype: For typedefs (e.g. subtypes - corresponding to a datatype invariant, such as dlist), - lift_definition generates a code certificate theorem and sets up - code generation for each constant. - - - setup_lifting command: Sets up the Lifting package to work with a - user-defined type. The user must provide either a quotient theorem - or a type_definition theorem. The package configures transfer - rules for equality and quantifiers on the type, and sets up the - lift_definition command to work with the type. - - - Usage examples: See Quotient_Examples/Lift_DList.thy, - Quotient_Examples/Lift_RBT.thy, Word/Word.thy and - Library/Float.thy. - -* Quotient package: - - - The 'quotient_type' command now supports a 'morphisms' option with - rep and abs functions, similar to typedef. - - - 'quotient_type' sets up new types to work with the Lifting and - Transfer packages, as with 'setup_lifting'. - - - The 'quotient_definition' command now requires the user to prove a - respectfulness property at the point where the constant is - defined, similar to lift_definition; INCOMPATIBILITY. - - - Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems - accordingly, INCOMPATIBILITY. - -* New diagnostic command 'find_unused_assms' to find potentially -superfluous assumptions in theorems using Quickcheck. - -* Quickcheck: - - - Quickcheck returns variable assignments as counterexamples, which - allows to reveal the underspecification of functions under test. - For example, refuting "hd xs = x", it presents the variable - assignment xs = [] and x = a1 as a counterexample, assuming that - any property is false whenever "hd []" occurs in it. - - These counterexample are marked as potentially spurious, as - Quickcheck also returns "xs = []" as a counterexample to the - obvious theorem "hd xs = hd xs". - - After finding a potentially spurious counterexample, Quickcheck - continues searching for genuine ones. - - By default, Quickcheck shows potentially spurious and genuine - counterexamples. The option "genuine_only" sets quickcheck to only - show genuine counterexamples. - - - The command 'quickcheck_generator' creates random and exhaustive - value generators for a given type and operations. - - It generates values by using the operations as if they were - constructors of that type. - - - Support for multisets. - - - Added "use_subtype" options. - - - 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'. - -* Sledgehammer: - - Integrated more tightly with SPASS, as described in the ITP 2012 - paper "More SPASS with Isabelle". - - Made it try "smt" as a fallback if "metis" fails or times out. - - Added support for the following provers: Alt-Ergo (via Why3 and - TFF1), iProver, iProver-Eq. - - Replaced remote E-SInE with remote Satallax in the default setup. - - Sped up the minimizer. - - Added "lam_trans", "uncurry_aliases", and "minimize" options. - - 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. - -* New "eventually_elim" method as a generalized variant of the -eventually_elim* rules. Supports structured proofs. - * HOL/TPTP: support to parse and import TPTP problems (all languages) into Isabelle/HOL.