detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr

--- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Apr 05 22:00:27 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Apr 05 23:22:54 2012 +0200
@@ -6,6 +6,8 @@
 
 signature LIFTING_DEF =
 sig
+  exception FORCE_RTY of typ * term
+
   val add_lift_def:
     (binding * mixfix) -> typ -> term -> thm -> local_theory -> local_theory
 
@@ -26,6 +28,8 @@
 
 fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
 
+exception FORCE_RTY of typ * term
+
 fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
   | get_body_types (U, V)  = (U, V)
 
@@ -38,6 +42,7 @@
     val rhs_schematic = singleton (Variable.polymorphic ctxt) rhs
     val rty_schematic = fastype_of rhs_schematic
     val match = Sign.typ_match thy (rty_schematic, rty) Vartab.empty
+      handle Type.TYPE_MATCH => raise FORCE_RTY (rty, rhs)
   in
     Envir.subst_term_types match rhs_schematic
   end
@@ -283,6 +288,46 @@
       | NONE =>  Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy
   end
 
+fun quot_thm_err ctxt (rty, qty) pretty_msg =
+  let
+    val error_msg = cat_lines
+       ["Lifting failed for the following types:",
+        Pretty.string_of (Pretty.block
+         [Pretty.str "Raw type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty]),
+        Pretty.string_of (Pretty.block
+         [Pretty.str "Abstract type:", Pretty.brk 2, Syntax.pretty_typ ctxt qty]),
+        "",
+        (Pretty.string_of (Pretty.block
+         [Pretty.str "Reason:", Pretty.brk 2, pretty_msg]))]
+  in
+    error error_msg
+  end
+
+fun force_rty_err ctxt rty rhs =
+  let
+    val error_msg = cat_lines
+       ["Lifting failed for the following term:",
+        Pretty.string_of (Pretty.block
+         [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt rhs]),
+        Pretty.string_of (Pretty.block
+         [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt (fastype_of rhs)]),
+        "",
+        (Pretty.string_of (Pretty.block
+         [Pretty.str "Reason:", 
+          Pretty.brk 2, 
+          Pretty.str "The type of the term cannot be instancied to",
+          Pretty.brk 1,
+          Pretty.quote (Syntax.pretty_typ ctxt rty),
+          Pretty.str "."]))]
+    in
+      error error_msg
+    end
+
+fun lift_def_cmd_with_err_handling (raw_var, rhs_raw) lthy =
+  (lift_def_cmd (raw_var, rhs_raw) lthy
+    handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg)
+    handle FORCE_RTY (rty, rhs) => force_rty_err lthy rty rhs
+
 (* parser and command *)
 val liftdef_parser =
   ((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2)
@@ -291,7 +336,7 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"}
     "definition for constants over the quotient type"
-      (liftdef_parser >> lift_def_cmd)
+      (liftdef_parser >> lift_def_cmd_with_err_handling)
 
 
 end; (* structure *)

--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 05 22:00:27 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 05 23:22:54 2012 +0200
@@ -50,8 +50,35 @@
   else
     lthy
 
+fun quot_thm_sanity_check ctxt quot_thm =
+  let
+    val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt 
+    val (rty, qty) = Lifting_Term.quot_thm_rty_qty quot_thm_fixed
+    val rty_tfreesT = Term.add_tfree_namesT rty []
+    val qty_tfreesT = Term.add_tfree_namesT qty []
+    val extra_rty_tfrees =
+      (case subtract (op =) qty_tfreesT rty_tfreesT of
+        [] => []
+      | extras => [Pretty.block ([Pretty.str "Extra variables in the raw type:",
+                                 Pretty.brk 1] @ 
+                                 ((Pretty.commas o map (Pretty.str o quote)) extras) @
+                                 [Pretty.str "."])])
+    val not_type_constr = 
+      (case qty of
+         Type _ => []
+         | _ => [Pretty.block [Pretty.str "The quotient type ",
+                                Pretty.quote (Syntax.pretty_typ ctxt' qty),
+                                Pretty.brk 1,
+                                Pretty.str "is not a type constructor."]])
+    val errs = extra_rty_tfrees @ not_type_constr
+  in
+    if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""] 
+                                                @ (map Pretty.string_of errs)))
+  end
+
 fun setup_lifting_infr quot_thm equiv_thm lthy =
   let
+    val _ = quot_thm_sanity_check lthy quot_thm
     val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
     val qty_full_name = (fst o dest_Type) qtyp
     val quotients = { quot_thm = quot_thm }

--- a/src/HOL/Tools/Lifting/lifting_term.ML	Thu Apr 05 22:00:27 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Thu Apr 05 23:22:54 2012 +0200
@@ -6,6 +6,8 @@
 
 signature LIFTING_TERM =
 sig
+  exception QUOT_THM of typ * typ * Pretty.T
+
   val prove_quot_theorem: Proof.context -> typ * typ -> thm
 
   val absrep_fun: Proof.context -> typ * typ -> term
@@ -24,7 +26,10 @@
 structure Lifting_Term: LIFTING_TERM =
 struct
 
-exception LIFT_MATCH of string
+(* generation of the Quotient theorem  *)
+
+exception QUOT_THM_INTERNAL of Pretty.T
+exception QUOT_THM of typ * typ * Pretty.T
 
 (* matches a type pattern with a type *)
 fun match ctxt err ty_pat ty =
@@ -40,21 +45,24 @@
     val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
     val ty_str = Syntax.string_of_typ ctxt ty
   in
-    raise LIFT_MATCH (space_implode " "
-      ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
+    raise QUOT_THM_INTERNAL (Pretty.block
+      [Pretty.str ("The quotient type " ^ quote ty_str),
+       Pretty.brk 1,
+       Pretty.str ("and the quotient type pattern " ^ quote ty_pat_str),
+       Pretty.brk 1,
+       Pretty.str "don't match."])
   end
 
-(* generation of the Quotient theorem  *)
-
-exception QUOT_THM of string
-
 fun get_quot_thm ctxt s =
   let
     val thy = Proof_Context.theory_of ctxt
   in
     (case Lifting_Info.lookup_quotients ctxt s of
       SOME qdata => Thm.transfer thy (#quot_thm qdata)
-    | NONE => raise QUOT_THM ("No quotient type " ^ quote s ^ " found."))
+    | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
+      [Pretty.str ("No quotient type " ^ quote s), 
+       Pretty.brk 1, 
+       Pretty.str "found."]))
   end
 
 fun get_rel_quot_thm ctxt s =
@@ -63,7 +71,10 @@
   in
     (case Lifting_Info.lookup_quotmaps ctxt s of
       SOME map_data => Thm.transfer thy (#quot_thm map_data)
-    | NONE => raise QUOT_THM ("get_relmap (no relation map function found for type " ^ s ^ ")"))
+    | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
+      [Pretty.str ("No relator for the type " ^ quote s), 
+       Pretty.brk 1,
+       Pretty.str "found."]))
   end
 
 fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
@@ -106,8 +117,19 @@
     (domain_type abs_type, range_type abs_type)
   end
 
+fun check_raw_types (provided_rty_name, rty_of_qty_name) qty_name =
+  if provided_rty_name <> rty_of_qty_name then
+    raise QUOT_THM_INTERNAL (Pretty.block 
+        [Pretty.str ("The type " ^ quote provided_rty_name),
+         Pretty.brk 1,
+         Pretty.str ("is not a raw type for the quotient type " ^ quote qty_name ^ ";"),
+         Pretty.brk 1,
+         Pretty.str ("the correct raw type is " ^ quote rty_of_qty_name ^ ".")])
+  else
+    ()
+
 fun prove_quot_theorem' ctxt (rty, qty) =
-  case (rty, qty) of
+  (case (rty, qty) of
     (Type (s, tys), Type (s', tys')) =>
       if s = s'
       then
@@ -123,7 +145,8 @@
       else
         let
           val quot_thm = get_quot_thm ctxt s'
-          val (Type (_, rtys), qty_pat) = quot_thm_rty_qty quot_thm
+          val (Type (rs, rtys), qty_pat) = quot_thm_rty_qty quot_thm
+          val _ = check_raw_types (s, rs) 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')
@@ -138,7 +161,8 @@
               [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose}
            end
         end
-  | _ => @{thm identity_quotient}
+  | _ => @{thm identity_quotient})
+    handle QUOT_THM_INTERNAL pretty_msg => raise QUOT_THM (rty, qty, pretty_msg)
 
 fun force_qty_type thy qty quot_thm =
   let