# HG changeset patch
# User kuncar
# Date 1381755701 -7200
# Node ID 03b10317ba78e702636987c8a6ca9e4bc6bcd214
# Parent  409d7f7247f4c12a0b20758f1b1cc56c1680ab61
update documentation of important public ML functions in Lifting

diff -r 409d7f7247f4 -r 03b10317ba78 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Oct 14 15:01:37 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Oct 14 15:01:41 2013 +0200
@@ -50,7 +50,15 @@
   SOME (Goal.prove ctxt [] [] prop (fn {context, ...} => refl_tac context 1))
     handle ERROR _ => NONE
 
-(* Generation of a transfer rule *)
+(* 
+  Generates a parametrized transfer rule.
+  transfer_rule - of the form T t f
+  parametric_transfer_rule - of the form par_R t' t
+  
+  Result: par_T t' f, after substituing op= for relations in par_T that relate
+    a type constructor to the same type constructor, it is a merge of (par_R' OO T) t' f
+    using Lifting_Term.merge_transfer_relations
+*)
 
 fun generate_parametric_transfer_rule ctxt transfer_rule parametric_transfer_rule =
   let
@@ -400,6 +408,7 @@
   rhs - a term representing the new constant on the raw level
   rsp_thm - a respectfulness theorem in the internal tagged form (like '(R ===> R ===> R) f f'),
     i.e. "(Lifting_Term.equiv_relation (fastype_of rhs, qty)) $ rhs $ rhs"
+  par_thms - a parametricity theorem for rhs
 *)
 
 fun add_lift_def var qty rhs rsp_thm par_thms lthy =
diff -r 409d7f7247f4 -r 03b10317ba78 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Oct 14 15:01:37 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Oct 14 15:01:41 2013 +0200
@@ -477,6 +477,7 @@
   quot_thm - a quotient theorem (Quotient R Abs Rep T)
   opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
     (in the form "reflp R")
+  opt_par_thm - a parametricity theorem for R
 *)
 
 fun setup_by_quotient gen_code quot_thm opt_reflp_thm opt_par_thm lthy =
@@ -852,6 +853,10 @@
                                             @ (map (Pretty.string_of o Pretty.item o single) errs)))
 end
 
+(*
+  Registers the data in qinfo in the Lifting infrastructure.
+*)
+
 fun lifting_restore qinfo ctxt =
   let
     val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo
diff -r 409d7f7247f4 -r 03b10317ba78 src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Mon Oct 14 15:01:37 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Mon Oct 14 15:01:41 2013 +0200
@@ -289,9 +289,17 @@
     quot_thm
   end
 
+(*
+  Computes the composed abstraction function for rty and qty.
+*)
+
 fun abs_fun ctxt (rty, qty) =
   quot_thm_abs (prove_quot_thm ctxt (rty, qty))
 
+(*
+  Computes the composed equivalence relation for rty and qty.
+*)
+
 fun equiv_relation ctxt (rty, qty) =
   quot_thm_rel (prove_quot_thm ctxt (rty, qty))
 
@@ -324,6 +332,16 @@
     end
   end
 
+(*
+  For the given type, it proves a composed Quotient map theorem, where for each type variable
+  extra Quotient assumption is generated. E.g., for 'a list it generates exactly
+  the Quotient map theorem for the list type. The function generalizes this for the whole
+  type universe. New fresh variables in the assumptions are fixed in the returned context.
+
+  Returns: the composed Quotient map theorem and list mapping each type variable in ty
+  to the corresponding assumption in the returned theorem.
+*)
+
 fun prove_param_quot_thm ctxt ty = 
   let 
     fun generate (ty as Type (s, tys)) (table_ctxt as (table, ctxt)) =
@@ -360,6 +378,13 @@
   end
   handle QUOT_THM_INTERNAL pretty_msg => raise PARAM_QUOT_THM (ty, pretty_msg)
 
+(*
+  It computes a parametrized relator for the given type ty. E.g., for 'a dlist:
+  list_all2 ?R OO cr_dlist with parameters [?R].
+  
+  Returns: the definitional term and list of parameters (relations).
+*)
+
 fun generate_parametrized_relator ctxt ty =
   let
     val orig_ctxt = ctxt
@@ -412,6 +437,15 @@
       map_interrupt' f l []
     end
 in
+
+  (*
+    ctm - of the form (par_R OO T) t f, where par_R is a parametricity transfer relation for t
+      and T is a transfer relation between t and f.
+    
+    The function merges par_R OO T using definitions of parametrized correspondence relations
+    (e.g., rel_T R OO cr_T == pcr_T R).
+  *)
+
   fun merge_transfer_relations ctxt ctm =
     let
       val ctm = Thm.dest_arg ctm
@@ -488,6 +522,14 @@
     handle QUOT_THM_INTERNAL pretty_msg => raise MERGE_TRANSFER_REL pretty_msg
 end
 
+(*
+  It replaces cr_T by pcr_T op= in the transfer relation. For composed
+  abstract types, it replaces T_rel R OO cr_T by pcr_T R. If the parametrized
+  correspondce relation does not exist, the original relation is kept.
+
+  thm - a transfer rule
+*)
+
 fun parametrize_transfer_rule ctxt thm =
   let
     fun parametrize_relation_conv ctm =