src/HOL/Tools/Quotient/quotient_term.ML

   (* Allows Nitpick to represent quotient types as single elements from raw type *)
   val absrep_const_chk: Proof.context -> flag -> string -> term
 
   val equiv_relation: Proof.context -> typ * typ -> term
   val equiv_relation_chk: Proof.context -> typ * typ -> term
+
+  val get_rel_from_quot_thm: thm -> term
+  val prove_quot_theorem: Proof.context -> typ * typ -> thm
 
   val regularize_trm: Proof.context -> term * term -> term
   val regularize_trm_chk: Proof.context -> term * term -> term
 
   val inj_repabs_trm: Proof.context -> term * term -> term

 
 fun equiv_relation_chk ctxt (rty, qty) =
   equiv_relation ctxt (rty, qty)
   |> Syntax.check_term ctxt
 
+(* generation of the Quotient theorem  *)
+
+fun get_quot_thm ctxt s =
+  let
+    val thy = Proof_Context.theory_of ctxt
+  in
+    (case Quotient_Info.lookup_quotients_global thy s of
+      SOME qdata => #quot_thm qdata
+    | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
+  end
+
+fun get_rel_quot_thm thy s =
+  (case Quotient_Info.lookup_quotmaps thy s of
+    SOME map_data => #quot_thm map_data
+  | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"));
+
+fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
+
+infix 0 MRSL
+
+fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+
+exception NOT_IMPL of string
+
+fun get_rel_from_quot_thm quot_thm = 
+  let
+    val (_ $ rel $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) quot_thm
+  in
+    rel
+  end
+
+fun mk_quot_thm_compose (rel_quot_thm, quot_thm) = 
+  let
+    val quot_thm_rel = get_rel_from_quot_thm quot_thm
+  in
+    if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient}
+    else raise NOT_IMPL "nested quotients: not implemented yet"
+  end
+
+fun prove_quot_theorem ctxt (rty, qty) =
+  if rty = qty
+  then @{thm identity_quotient}
+  else
+    case (rty, qty) of
+      (Type (s, tys), Type (s', tys')) =>
+        if s = s'
+        then
+          let
+            val args = map (prove_quot_theorem ctxt) (tys ~~ tys')
+          in
+            args MRSL (get_rel_quot_thm ctxt s)
+          end
+        else
+          let
+            val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
+            val qtyenv = match ctxt equiv_match_err qty_pat qty
+            val rtys' = map (Envir.subst_type qtyenv) rtys
+            val args = map (prove_quot_theorem ctxt) (tys ~~ rtys')
+            val quot_thm = get_quot_thm ctxt s'
+          in
+            if forall is_id_quot args
+            then
+              quot_thm
+            else
+              let
+                val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s)
+              in
+                mk_quot_thm_compose (rel_quot_thm, quot_thm)
+             end
+          end
+    | _ => @{thm identity_quotient}
+
 
 
 (*** Regularization ***)
 
 (* Regularizing an rtrm means: