src/HOL/Tools/Lifting/lifting_term.ML

   exception QUOT_THM of typ * typ * Pretty.T
   exception CHECK_RTY of typ * typ
 
   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
 
   val quot_thm_rel: thm -> term
   val quot_thm_abs: thm -> term

 
 open Lifting_Util
 
 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
   in
     Sign.typ_match thy (ty_pat, ty) Vartab.empty

        Pretty.brk 1,
        Pretty.str "found."]))
   end
 
 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
 

       handle Type.TYPE_MATCH => raise CHECK_RTY (rty_schematic, rty_forced)
   in
     ()
   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
     val schematic_quot_thm = prove_schematic_quot_thm ctxt (rty, qty)
     val quot_thm = force_qty_type thy qty schematic_quot_thm
     val _ = check_rty_type ctxt rty quot_thm
   in
     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) =
   quot_thm_rel (prove_quot_thm ctxt (rty, qty))