--- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 04 16:29:17 2012 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 04 17:51:12 2012 +0200
@@ -22,26 +22,11 @@
exception SETUP_LIFTING_INFR of string
-fun define_cr_rel equiv_thm abs_fun lthy =
+fun define_cr_rel rep_fun lthy =
let
- fun force_type_of_rel rel forced_ty =
- let
- val thy = Proof_Context.theory_of lthy
- val rel_ty = (domain_type o fastype_of) rel
- val ty_inst = Sign.typ_match thy (rel_ty, forced_ty) Vartab.empty
- in
- Envir.subst_term_types ty_inst rel
- end
-
- val (rty, qty) = (dest_funT o fastype_of) abs_fun
- val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0)
- val Abs_body = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
- Const (@{const_name equivp}, _) $ _ => abs_fun_graph
- | Const (@{const_name part_equivp}, _) $ rel =>
- HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
- | _ => raise SETUP_LIFTING_INFR "unsupported equivalence theorem"
- )
- val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
+ val (qty, rty) = (dest_funT o fastype_of) rep_fun
+ val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0)
+ val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph));
val qty_name = (fst o dest_Type) qty
val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name)
val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
@@ -82,9 +67,9 @@
let
fun derive_quot_and_equiv_thm to_quot_thm to_equiv_thm typedef_thm lthy =
let
- val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
+ val (_ $ rep_fun $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
val equiv_thm = typedef_thm RS to_equiv_thm
- val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
+ val (T_def, lthy') = define_cr_rel rep_fun lthy
val quot_thm = [typedef_thm, T_def] MRSL to_quot_thm
in
(quot_thm, equiv_thm, lthy')
@@ -93,12 +78,13 @@
val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
val (quot_thm, equiv_thm, lthy') = (case typedef_set of
Const ("Orderings.top_class.top", _) =>
- derive_quot_and_equiv_thm @{thm copy_type_to_Quotient} @{thm copy_type_to_equivp}
+ derive_quot_and_equiv_thm @{thm UNIV_typedef_to_Quotient} @{thm UNIV_typedef_to_equivp}
typedef_thm lthy
| Const (@{const_name "Collect"}, _) $ Abs (_, _, _) =>
- derive_quot_and_equiv_thm @{thm invariant_type_to_Quotient} @{thm invariant_type_to_part_equivp}
+ derive_quot_and_equiv_thm @{thm open_typedef_to_Quotient} @{thm open_typedef_to_part_equivp}
typedef_thm lthy
- | _ => raise SETUP_LIFTING_INFR "unsupported typedef theorem")
+ | _ => derive_quot_and_equiv_thm @{thm typedef_to_Quotient} @{thm typedef_to_part_equivp}
+ typedef_thm lthy)
in
setup_lifting_infr quot_thm equiv_thm lthy'
end
@@ -109,5 +95,4 @@
Outer_Syntax.local_theory @{command_spec "setup_lifting"}
"Setup lifting infrastructure"
(Parse_Spec.xthm >> (fn xthm => setup_by_typedef_thm_aux xthm))
-
end;