author huffman Wed, 04 Apr 2012 13:41:38 +0200 changeset 47350 ec46b60aa582 parent 47334 4708384e759d child 47351 0193e663a19e
prove_quot_theorem fixes types
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Wed Apr 04 10:38:04 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Wed Apr 04 13:41:38 2012 +0200
@@ -106,13 +106,13 @@
(domain_type abs_type, range_type abs_type)
end

-fun prove_quot_theorem ctxt (rty, qty) =
+fun prove_quot_theorem' ctxt (rty, qty) =
case (rty, qty) of
(Type (s, tys), Type (s', tys')) =>
if s = s'
then
let
-          val args = map (prove_quot_theorem ctxt) (tys ~~ tys')
+          val args = map (prove_quot_theorem' ctxt) (tys ~~ tys')
in
if forall is_id_quot args
then
@@ -126,7 +126,7 @@
val (Type (_, rtys), qty_pat) = quot_thm_rty_qty quot_thm
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 args = map (prove_quot_theorem' ctxt) (tys ~~ rtys')
in
if forall is_id_quot args
then
@@ -152,22 +152,18 @@
Thm.instantiate (ty_inst, []) quot_thm
end

-fun absrep_fun ctxt (rty, qty) =
+fun prove_quot_theorem ctxt (rty, qty) =
let
val thy = Proof_Context.theory_of ctxt
-    val quot_thm = prove_quot_theorem ctxt (rty, qty)
-    val forced_quot_thm = force_qty_type thy qty quot_thm
+    val quot_thm = prove_quot_theorem' ctxt (rty, qty)
in
-    quot_thm_abs forced_quot_thm
+    force_qty_type thy qty quot_thm
end

+fun absrep_fun ctxt (rty, qty) =
+  quot_thm_abs (prove_quot_theorem ctxt (rty, qty))
+
fun equiv_relation ctxt (rty, qty) =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val quot_thm = prove_quot_theorem ctxt (rty, qty)
-    val forced_quot_thm = force_qty_type thy qty quot_thm
-  in
-    quot_thm_rel forced_quot_thm
-  end
+  quot_thm_rel (prove_quot_theorem ctxt (rty, qty))

end;