# HG changeset patch
# User kuncar
# Date 1335470296 -7200
# Node ID fe43977e434f8e3e01e452faa568744f5c600172
# Parent  0eadfb89badbe5cc109c321bc2fad200446c10d6
added a basic sanity check for quot_map

diff -r 0eadfb89badb -r fe43977e434f src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Thu Apr 26 20:22:39 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Thu Apr 26 21:58:16 2012 +0200
@@ -47,8 +47,46 @@
 
 (* FIXME export proper internal update operation!? *)
 
+fun quot_map_thm_sanity_check rel_quot_thm ctxt =
+  let
+    fun quot_term_absT ctxt quot_term = 
+      let 
+        val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term
+          handle TERM (_, [t]) => error (Pretty.string_of (Pretty.block
+            [Pretty.str "The Quotient map theorem is not in the right form.",
+             Pretty.brk 1,
+             Pretty.str "The following term is not the Quotient predicate:",
+             Pretty.brk 1,
+             Syntax.pretty_term ctxt t]))
+      in
+        fastype_of abs
+      end
+
+    val ((_, [rel_quot_thm_fixed]), ctxt') = Variable.importT [rel_quot_thm] ctxt
+    val rel_quot_thm_prop = prop_of rel_quot_thm_fixed
+    val rel_quot_thm_concl = Logic.strip_imp_concl rel_quot_thm_prop
+    val rel_quot_thm_prems = Logic.strip_imp_prems rel_quot_thm_prop;
+    val concl_absT = quot_term_absT ctxt' rel_quot_thm_concl
+    val concl_tfrees = Term.add_tfree_namesT (concl_absT) []
+    val prems_tfrees = fold (fn typ => fn list => Term.add_tfree_namesT (quot_term_absT ctxt' typ) list) 
+                          rel_quot_thm_prems []
+    val extra_prem_tfrees =
+      case subtract (op =) concl_tfrees prems_tfrees of
+        [] => []
+      | extras => [Pretty.block ([Pretty.str "Extra type variables in the premises:",
+                                 Pretty.brk 1] @ 
+                                 ((Pretty.commas o map (Pretty.str o quote)) extras) @
+                                 [Pretty.str "."])]
+    val errs = extra_prem_tfrees 
+  in
+    if null errs then () else error (cat_lines (["Sanity check of the quotient map theorem failed:",""] 
+                                                 @ (map Pretty.string_of errs)))
+  end
+
+
 fun add_quot_map rel_quot_thm ctxt = 
   let
+    val _ = Context.cases (K ()) (quot_map_thm_sanity_check rel_quot_thm) ctxt
     val rel_quot_thm_concl = (Logic.strip_imp_concl o prop_of) rel_quot_thm
     val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) rel_quot_thm_concl
     val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs