documentation of the Lifting package on the ML level & tuned

--- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed May 02 17:23:41 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed May 02 18:26:10 2012 +0200
@@ -98,6 +98,12 @@
 fun simplify_code_eq ctxt def_thm = 
   Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm
 
+(*
+  quot_thm - quotient theorem (Quotient R Abs Rep T).
+  returns: whether the Lifting package is capable to generate code for the abstract type
+    represented by quot_thm
+*)
+
 fun can_generate_code_cert quot_thm  =
   case Lifting_Term.quot_thm_rel quot_thm of
     Const (@{const_name HOL.eq}, _) => true
@@ -173,6 +179,16 @@
   else 
     define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy
 
+(*
+  Defines an operation on an abstract type in terms of a corresponding operation 
+    on a representation type.
+
+  var - a binding and a mixfix of the new constant being defined
+  qty - an abstract type of the new constant
+  rhs - a term representing the new constant on the raw level
+  rsp_thm - a respectfulness theorem in the internal form (like (R ===> R ===> R) f f),
+    i.e. "(Lifting_Term.equiv_relation (fastype_of rhs, qty)) $ rhs $ rhs"
+*)
 
 fun add_lift_def var qty rhs rsp_thm lthy =
   let
@@ -265,6 +281,13 @@
     rename term new_names
   end
 
+(*
+
+  lifting_definition command. It opens a proof of a corresponding respectfulness 
+  theorem in a user-friendly, readable form. Then add_lift_def is called internally.
+
+*)
+
 fun lift_def_cmd (raw_var, rhs_raw) lthy =
   let
     val ((binding, SOME qty, mx), lthy') = yield_singleton Proof_Context.read_vars raw_var lthy 

--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed May 02 17:23:41 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed May 02 18:26:10 2012 +0200
@@ -8,8 +8,6 @@
 sig
   exception SETUP_LIFTING_INFR of string
 
-  val setup_lifting_infr: bool -> thm -> local_theory -> local_theory
-
   val setup_by_quotient: bool -> thm -> thm option -> local_theory -> local_theory
 
   val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
@@ -92,6 +90,16 @@
       |> define_abs_type gen_abs_code quot_thm
   end
 
+(*
+  Sets up the Lifting package by a quotient theorem.
+
+  gen_abs_code - flag if an abstract type given by quot_thm should be registred 
+    as an abstract type in the code generator
+  quot_thm - a quotient theorem (Quotient R Abs Rep T)
+  maybe_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
+    (in the form "reflp R")
+*)
+
 fun setup_by_quotient gen_abs_code quot_thm maybe_reflp_thm lthy =
   let
     val transfer_attr = Attrib.internal (K Transfer.transfer_add)
@@ -127,6 +135,14 @@
       |> setup_lifting_infr gen_abs_code quot_thm
   end
 
+(*
+  Sets up the Lifting package by a typedef theorem.
+
+  gen_abs_code - flag if an abstract type given by typedef_thm should be registred 
+    as an abstract type in the code generator
+  typedef_thm - a typedef theorem (type_definition Rep Abs S)
+*)
+
 fun setup_by_typedef_thm gen_abs_code typedef_thm lthy =
   let
     val transfer_attr = Attrib.internal (K Transfer.transfer_add)

--- a/src/HOL/Tools/Lifting/lifting_term.ML	Wed May 02 17:23:41 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Wed May 02 18:26:10 2012 +0200
@@ -11,10 +11,7 @@
 
   val prove_quot_thm: Proof.context -> typ * typ -> thm
 
-  val absrep_fun: Proof.context -> typ * typ -> term
-
-  (* Allows Nitpick to represent quotient types as single elements from raw type *)
-  (* val absrep_const_chk: Proof.context -> flag -> string -> term *)
+  val abs_fun: Proof.context -> typ * typ -> term
 
   val equiv_relation: Proof.context -> typ * typ -> term
 
@@ -31,13 +28,10 @@
 
 infix 0 MRSL
 
-(* generation of the Quotient theorem  *)
-
 exception QUOT_THM_INTERNAL of Pretty.T
 exception QUOT_THM of typ * typ * Pretty.T
 exception CHECK_RTY of typ * typ
 
-(* matches a type pattern with a type *)
 fun match ctxt err ty_pat ty =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -85,6 +79,11 @@
 
 fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
 
+(*
+  quot_thm_rel, quot_thm_abs, quot_thm_rep and quot_thm_rty_qty - simple functions
+    for destructing quotient theorems (Quotient R Abs Rep T).
+*)
+
 fun quot_thm_rel quot_thm =
   case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
     (rel, _, _, _) => rel
@@ -242,6 +241,13 @@
     ()
   end
 
+(*
+  The function tries to prove that rty and qty form a quotient.
+
+  Returns: Quotient theorem; an abstract type of the theorem is exactly
+    qty, a representation type of the theorem is an instance of rty in general.
+*)
+
 fun prove_quot_thm ctxt (rty, qty) =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -252,7 +258,7 @@
     quot_thm
   end
 
-fun absrep_fun ctxt (rty, qty) =
+fun abs_fun ctxt (rty, qty) =
   quot_thm_abs (prove_quot_thm ctxt (rty, qty))
 
 fun equiv_relation ctxt (rty, qty) =