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