--- 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