summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 47655 | b9e132e54d25 |

parent 47622 | 6d53f2ef4a97 |

child 47659 | e3c4d1b0b351 |

1.1 --- a/NEWS Sat Apr 21 13:49:31 2012 +0200 1.2 +++ b/NEWS Sat Apr 21 13:54:29 2012 +0200 1.3 @@ -657,6 +657,86 @@ 1.4 1.5 * Theory Library/Multiset: Improved code generation of multisets. 1.6 1.7 +* New Transfer package: 1.8 + 1.9 + - transfer_rule attribute: Maintains a collection of transfer rules, 1.10 + which relate constants at two different types. Transfer rules may 1.11 + relate different type instances of the same polymorphic constant, 1.12 + or they may relate an operation on a raw type to a corresponding 1.13 + operation on an abstract type (quotient or subtype). For example: 1.14 + 1.15 + ((A ===> B) ===> list_all2 A ===> list_all2 B) map map 1.16 + (cr_int ===> cr_int ===> cr_int) (%(x,y) (u,v). (x+u, y+v)) plus_int 1.17 + 1.18 + - transfer method: Replaces a subgoal on abstract types with an 1.19 + equivalent subgoal on the corresponding raw types. Constants are 1.20 + replaced with corresponding ones according to the transfer rules. 1.21 + Goals are generalized over all free variables by default; this is 1.22 + necessary for variables whose types changes, but can be overridden 1.23 + for specific variables with e.g. 'transfer fixing: x y z'. 1.24 + 1.25 + - relator_eq attribute: Collects identity laws for relators of 1.26 + various type constructors, e.g. "list_all2 (op =) = (op =)". The 1.27 + transfer method uses these lemmas to infer transfer rules for 1.28 + non-polymorphic constants on the fly. 1.29 + 1.30 + - transfer_prover method: Assists with proving a transfer rule for a 1.31 + new constant, provided the constant is defined in terms of other 1.32 + constants that already have transfer rules. It should be applied 1.33 + after unfolding the constant definitions. 1.34 + 1.35 + - HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer 1.36 + from type nat to type int. 1.37 + 1.38 +* New Lifting package: 1.39 + 1.40 + - lift_definition command: Defines operations on an abstract type in 1.41 + terms of a corresponding operation on a representation type. Example 1.42 + syntax: 1.43 + 1.44 + lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist" 1.45 + is List.insert 1.46 + 1.47 + Users must discharge a respectfulness proof obligation when each 1.48 + constant is defined. (For a type copy, i.e. a typedef with UNIV, 1.49 + the proof is discharged automatically.) The obligation is 1.50 + presented in a user-friendly, readable form; a respectfulness 1.51 + theorem in the standard format and a transfer rule are generated 1.52 + by the package. 1.53 + 1.54 + - Integration with code_abstype: For typedefs (e.g. subtypes 1.55 + corresponding to a datatype invariant, such as dlist), 1.56 + lift_definition generates a code certificate theorem and sets up 1.57 + code generation for each constant. 1.58 + 1.59 + - setup_lifting command: Sets up the Lifting package to work with 1.60 + a user-defined type. The user must provide either a quotient 1.61 + theorem or a type_definition theorem. The package configures 1.62 + transfer rules for equality and quantifiers on the type, and sets 1.63 + up the lift_definition command to work with the type. 1.64 + 1.65 + - Usage examples: See Quotient_Examples/Lift_DList.thy, 1.66 + Quotient_Examples/Lift_RBT.thy, Word/Word.thy and 1.67 + Library/Float.thy. 1.68 + 1.69 +* Quotient package: 1.70 + 1.71 + - The 'quotient_type' command now supports a 'morphisms' option with 1.72 + rep and abs functions, similar to typedef. 1.73 + 1.74 + - 'quotient_type' sets up new types to work with the Lifting and 1.75 + Transfer packages, as with 'setup_lifting'. 1.76 + 1.77 + - The 'quotient_definition' command now requires the user to prove a 1.78 + respectfulness property at the point where the constant is 1.79 + defined, similar to lift_definition; INCOMPATIBILITY. Users are 1.80 + encouraged to use lift_definition + transfer instead of 1.81 + quotient_definition + descending, which will eventually be 1.82 + deprecated. 1.83 + 1.84 + - Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems 1.85 + accordingly, INCOMPATIBILITY. 1.86 + 1.87 * New diagnostic command 'find_unused_assms' to find potentially 1.88 superfluous assumptions in theorems using Quickcheck. 1.89