1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Oct 14 15:01:37 2013 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Oct 14 15:01:41 2013 +0200
     1.3 @@ -50,7 +50,15 @@
     1.4    SOME (Goal.prove ctxt [] [] prop (fn {context, ...} => refl_tac context 1))
     1.5      handle ERROR _ => NONE
     1.6  
     1.7 -(* Generation of a transfer rule *)
     1.8 +(* 
     1.9 +  Generates a parametrized transfer rule.
    1.10 +  transfer_rule - of the form T t f
    1.11 +  parametric_transfer_rule - of the form par_R t' t
    1.12 +  
    1.13 +  Result: par_T t' f, after substituing op= for relations in par_T that relate
    1.14 +    a type constructor to the same type constructor, it is a merge of (par_R' OO T) t' f
    1.15 +    using Lifting_Term.merge_transfer_relations
    1.16 +*)
    1.17  
    1.18  fun generate_parametric_transfer_rule ctxt transfer_rule parametric_transfer_rule =
    1.19    let
    1.20 @@ -400,6 +408,7 @@
    1.21    rhs - a term representing the new constant on the raw level
    1.22    rsp_thm - a respectfulness theorem in the internal tagged form (like '(R ===> R ===> R) f f'),
    1.23      i.e. "(Lifting_Term.equiv_relation (fastype_of rhs, qty)) $ rhs $ rhs"
    1.24 +  par_thms - a parametricity theorem for rhs
    1.25  *)
    1.26  
    1.27  fun add_lift_def var qty rhs rsp_thm par_thms lthy =

     2.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Oct 14 15:01:37 2013 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Oct 14 15:01:41 2013 +0200
     2.3 @@ -477,6 +477,7 @@
     2.4    quot_thm - a quotient theorem (Quotient R Abs Rep T)
     2.5    opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
     2.6      (in the form "reflp R")
     2.7 +  opt_par_thm - a parametricity theorem for R
     2.8  *)
     2.9  
    2.10  fun setup_by_quotient gen_code quot_thm opt_reflp_thm opt_par_thm lthy =
    2.11 @@ -852,6 +853,10 @@
    2.12                                              @ (map (Pretty.string_of o Pretty.item o single) errs)))
    2.13  end
    2.14  
    2.15 +(*
    2.16 +  Registers the data in qinfo in the Lifting infrastructure.
    2.17 +*)
    2.18 +
    2.19  fun lifting_restore qinfo ctxt =
    2.20    let
    2.21      val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo

     3.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Mon Oct 14 15:01:37 2013 +0200
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Mon Oct 14 15:01:41 2013 +0200
     3.3 @@ -289,9 +289,17 @@
     3.4      quot_thm
     3.5    end
     3.6  
     3.7 +(*
     3.8 +  Computes the composed abstraction function for rty and qty.
     3.9 +*)
    3.10 +
    3.11  fun abs_fun ctxt (rty, qty) =
    3.12    quot_thm_abs (prove_quot_thm ctxt (rty, qty))
    3.13  
    3.14 +(*
    3.15 +  Computes the composed equivalence relation for rty and qty.
    3.16 +*)
    3.17 +
    3.18  fun equiv_relation ctxt (rty, qty) =
    3.19    quot_thm_rel (prove_quot_thm ctxt (rty, qty))
    3.20  
    3.21 @@ -324,6 +332,16 @@
    3.22      end
    3.23    end
    3.24  
    3.25 +(*
    3.26 +  For the given type, it proves a composed Quotient map theorem, where for each type variable
    3.27 +  extra Quotient assumption is generated. E.g., for 'a list it generates exactly
    3.28 +  the Quotient map theorem for the list type. The function generalizes this for the whole
    3.29 +  type universe. New fresh variables in the assumptions are fixed in the returned context.
    3.30 +
    3.31 +  Returns: the composed Quotient map theorem and list mapping each type variable in ty
    3.32 +  to the corresponding assumption in the returned theorem.
    3.33 +*)
    3.34 +
    3.35  fun prove_param_quot_thm ctxt ty = 
    3.36    let 
    3.37      fun generate (ty as Type (s, tys)) (table_ctxt as (table, ctxt)) =
    3.38 @@ -360,6 +378,13 @@
    3.39    end
    3.40    handle QUOT_THM_INTERNAL pretty_msg => raise PARAM_QUOT_THM (ty, pretty_msg)
    3.41  
    3.42 +(*
    3.43 +  It computes a parametrized relator for the given type ty. E.g., for 'a dlist:
    3.44 +  list_all2 ?R OO cr_dlist with parameters [?R].
    3.45 +  
    3.46 +  Returns: the definitional term and list of parameters (relations).
    3.47 +*)
    3.48 +
    3.49  fun generate_parametrized_relator ctxt ty =
    3.50    let
    3.51      val orig_ctxt = ctxt
    3.52 @@ -412,6 +437,15 @@
    3.53        map_interrupt' f l []
    3.54      end
    3.55  in
    3.56 +
    3.57 +  (*
    3.58 +    ctm - of the form (par_R OO T) t f, where par_R is a parametricity transfer relation for t
    3.59 +      and T is a transfer relation between t and f.
    3.60 +    
    3.61 +    The function merges par_R OO T using definitions of parametrized correspondence relations
    3.62 +    (e.g., rel_T R OO cr_T == pcr_T R).
    3.63 +  *)
    3.64 +
    3.65    fun merge_transfer_relations ctxt ctm =
    3.66      let
    3.67        val ctm = Thm.dest_arg ctm
    3.68 @@ -488,6 +522,14 @@
    3.69      handle QUOT_THM_INTERNAL pretty_msg => raise MERGE_TRANSFER_REL pretty_msg
    3.70  end
    3.71  
    3.72 +(*
    3.73 +  It replaces cr_T by pcr_T op= in the transfer relation. For composed
    3.74 +  abstract types, it replaces T_rel R OO cr_T by pcr_T R. If the parametrized
    3.75 +  correspondce relation does not exist, the original relation is kept.
    3.76 +
    3.77 +  thm - a transfer rule
    3.78 +*)
    3.79 +
    3.80  fun parametrize_transfer_rule ctxt thm =
    3.81    let
    3.82      fun parametrize_relation_conv ctm =