generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
--- a/src/HOL/Quotient.thy Fri Mar 23 14:21:41 2012 +0100
+++ b/src/HOL/Quotient.thy Fri Mar 23 14:25:31 2012 +0100
@@ -9,6 +9,7 @@
keywords
"print_quotmaps" "print_quotients" "print_quotconsts" :: diag and
"quotient_type" :: thy_goal and "/" and
+ "setup_lifting" :: thy_decl and
"quotient_definition" :: thy_goal
uses
("Tools/Quotient/quotient_info.ML")
@@ -137,6 +138,18 @@
unfolding Quotient_def
by blast
+lemma Quotient_refl1:
+ assumes a: "Quotient R Abs Rep"
+ shows "R r s \<Longrightarrow> R r r"
+ using a unfolding Quotient_def
+ by fast
+
+lemma Quotient_refl2:
+ assumes a: "Quotient R Abs Rep"
+ shows "R r s \<Longrightarrow> R s s"
+ using a unfolding Quotient_def
+ by fast
+
lemma Quotient_rel_rep:
assumes a: "Quotient R Abs Rep"
shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
@@ -263,6 +276,15 @@
shows "R2 (f x) (g y)"
using a by (auto elim: fun_relE)
+lemma apply_rsp'':
+ assumes "Quotient R Abs Rep"
+ and "(R ===> S) f f"
+ shows "S (f (Rep x)) (f (Rep x))"
+proof -
+ from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp)
+ then show ?thesis using assms(2) by (auto intro: apply_rsp')
+qed
+
subsection {* lemmas for regularisation of ball and bex *}
lemma ball_reg_eqv:
@@ -679,6 +701,153 @@
end
+subsection {* Quotient composition *}
+
+lemma OOO_quotient:
+ fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
+ fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
+ fixes R2' :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ fixes R2 :: "'b \<Rightarrow> 'b \<Rightarrow> bool"
+ assumes R1: "Quotient R1 Abs1 Rep1"
+ assumes R2: "Quotient R2 Abs2 Rep2"
+ assumes Abs1: "\<And>x y. R2' x y \<Longrightarrow> R1 x x \<Longrightarrow> R1 y y \<Longrightarrow> R2 (Abs1 x) (Abs1 y)"
+ assumes Rep1: "\<And>x y. R2 x y \<Longrightarrow> R2' (Rep1 x) (Rep1 y)"
+ shows "Quotient (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
+apply (rule QuotientI)
+ apply (simp add: o_def Quotient_abs_rep [OF R2] Quotient_abs_rep [OF R1])
+ apply simp
+ apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI)
+ apply (rule Quotient_rep_reflp [OF R1])
+ apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated])
+ apply (rule Quotient_rep_reflp [OF R1])
+ apply (rule Rep1)
+ apply (rule Quotient_rep_reflp [OF R2])
+ apply safe
+ apply (rename_tac x y)
+ apply (drule Abs1)
+ apply (erule Quotient_refl2 [OF R1])
+ apply (erule Quotient_refl1 [OF R1])
+ apply (drule Quotient_refl1 [OF R2], drule Rep1)
+ apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
+ apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption)
+ apply (erule pred_compI)
+ apply (erule Quotient_symp [OF R1, THEN sympD])
+ apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
+ apply (rule conjI, erule Quotient_refl1 [OF R1])
+ apply (rule conjI, rule Quotient_rep_reflp [OF R1])
+ apply (subst Quotient_abs_rep [OF R1])
+ apply (erule Quotient_rel_abs [OF R1])
+ apply (rename_tac x y)
+ apply (drule Abs1)
+ apply (erule Quotient_refl2 [OF R1])
+ apply (erule Quotient_refl1 [OF R1])
+ apply (drule Quotient_refl2 [OF R2], drule Rep1)
+ apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
+ apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption)
+ apply (erule pred_compI)
+ apply (erule Quotient_symp [OF R1, THEN sympD])
+ apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
+ apply (rule conjI, erule Quotient_refl2 [OF R1])
+ apply (rule conjI, rule Quotient_rep_reflp [OF R1])
+ apply (subst Quotient_abs_rep [OF R1])
+ apply (erule Quotient_rel_abs [OF R1, THEN sym])
+ apply simp
+ apply (rule Quotient_rel_abs [OF R2])
+ apply (rule Quotient_rel_abs [OF R1, THEN ssubst], assumption)
+ apply (rule Quotient_rel_abs [OF R1, THEN subst], assumption)
+ apply (erule Abs1)
+ apply (erule Quotient_refl2 [OF R1])
+ apply (erule Quotient_refl1 [OF R1])
+ apply (rename_tac a b c d)
+ apply simp
+ apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI)
+ apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
+ apply (rule conjI, erule Quotient_refl1 [OF R1])
+ apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
+ apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated])
+ apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
+ apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
+ apply (erule Quotient_refl2 [OF R1])
+ apply (rule Rep1)
+ apply (drule Abs1)
+ apply (erule Quotient_refl2 [OF R1])
+ apply (erule Quotient_refl1 [OF R1])
+ apply (drule Abs1)
+ apply (erule Quotient_refl2 [OF R1])
+ apply (erule Quotient_refl1 [OF R1])
+ apply (drule Quotient_rel_abs [OF R1])
+ apply (drule Quotient_rel_abs [OF R1])
+ apply (drule Quotient_rel_abs [OF R1])
+ apply (drule Quotient_rel_abs [OF R1])
+ apply simp
+ apply (rule Quotient_rel[symmetric, OF R2, THEN iffD2])
+ apply simp
+done
+
+lemma OOO_eq_quotient:
+ fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
+ fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
+ assumes R1: "Quotient R1 Abs1 Rep1"
+ assumes R2: "Quotient op= Abs2 Rep2"
+ shows "Quotient (R1 OOO op=) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
+using assms
+by (rule OOO_quotient) auto
+
+subsection {* Invariant *}
+
+definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ where "invariant R = (\<lambda>x y. R x \<and> x = y)"
+
+lemma invariant_to_eq:
+ assumes "invariant P x y"
+ shows "x = y"
+using assms by (simp add: invariant_def)
+
+lemma fun_rel_eq_invariant:
+ shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
+by (auto simp add: invariant_def fun_rel_def)
+
+lemma invariant_same_args:
+ shows "invariant P x x \<equiv> P x"
+using assms by (auto simp add: invariant_def)
+
+lemma copy_type_to_Quotient:
+ assumes "type_definition Rep Abs UNIV"
+ shows "Quotient (op =) Abs Rep"
+proof -
+ interpret type_definition Rep Abs UNIV by fact
+ from Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI)
+qed
+
+lemma copy_type_to_equivp:
+ fixes Abs :: "'a \<Rightarrow> 'b"
+ and Rep :: "'b \<Rightarrow> 'a"
+ assumes "type_definition Rep Abs (UNIV::'a set)"
+ shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
+by (rule identity_equivp)
+
+lemma invariant_type_to_Quotient:
+ assumes "type_definition Rep Abs {x. P x}"
+ shows "Quotient (invariant P) Abs Rep"
+proof -
+ interpret type_definition Rep Abs "{x. P x}" by fact
+ from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI simp: invariant_def)
+qed
+
+lemma invariant_type_to_part_equivp:
+ assumes "type_definition Rep Abs {x. P x}"
+ shows "part_equivp (invariant P)"
+proof (intro part_equivpI)
+ interpret type_definition Rep Abs "{x. P x}" by fact
+ show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
+next
+ show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
+next
+ show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
+qed
+
subsection {* ML setup *}
text {* Auxiliary data for the quotient package *}
--- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Mar 23 14:21:41 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Mar 23 14:25:31 2012 +0100
@@ -27,6 +27,130 @@
(** Interface and Syntax Setup **)
+(* Generation of the code certificate from the rsp theorem *)
+
+infix 0 MRSL
+
+fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+
+fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
+ | get_body_types (U, V) = (U, V)
+
+fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
+ | get_binder_types _ = []
+
+fun unabs_def ctxt def =
+ let
+ val (_, rhs) = Thm.dest_equals (cprop_of def)
+ fun dest_abs (Abs (var_name, T, _)) = (var_name, T)
+ | dest_abs tm = raise TERM("get_abs_var",[tm])
+ val (var_name, T) = dest_abs (term_of rhs)
+ val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt
+ val thy = Proof_Context.theory_of ctxt'
+ val refl_thm = Thm.reflexive (cterm_of thy (Free (hd new_var_names, T)))
+ in
+ Thm.combination def refl_thm |>
+ singleton (Proof_Context.export ctxt' ctxt)
+ end
+
+fun unabs_all_def ctxt def =
+ let
+ val (_, rhs) = Thm.dest_equals (cprop_of def)
+ val xs = strip_abs_vars (term_of rhs)
+ in
+ fold (K (unabs_def ctxt)) xs def
+ end
+
+val map_fun_unfolded =
+ @{thm map_fun_def[abs_def]} |>
+ unabs_def @{context} |>
+ unabs_def @{context} |>
+ Local_Defs.unfold @{context} [@{thm comp_def}]
+
+fun unfold_fun_maps ctm =
+ let
+ fun unfold_conv ctm =
+ case (Thm.term_of ctm) of
+ Const (@{const_name "map_fun"}, _) $ _ $ _ =>
+ (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
+ | _ => Conv.all_conv ctm
+ val try_beta_conv = Conv.try_conv (Thm.beta_conversion false)
+ in
+ (Conv.arg_conv (Conv.fun_conv unfold_conv then_conv try_beta_conv)) ctm
+ end
+
+fun prove_rel ctxt rsp_thm (rty, qty) =
+ let
+ val ty_args = get_binder_types (rty, qty)
+ fun disch_arg args_ty thm =
+ let
+ val quot_thm = Quotient_Term.prove_quot_theorem ctxt args_ty
+ in
+ [quot_thm, thm] MRSL @{thm apply_rsp''}
+ end
+ in
+ fold disch_arg ty_args rsp_thm
+ end
+
+exception CODE_CERT_GEN of string
+
+fun simplify_code_eq ctxt def_thm =
+ Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm
+
+fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) =
+ let
+ val quot_thm = Quotient_Term.prove_quot_theorem ctxt (get_body_types (rty, qty))
+ val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
+ val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs}
+ val abs_rep_eq =
+ case (HOLogic.dest_Trueprop o prop_of) fun_rel of
+ Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm
+ | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
+ | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
+ val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
+ val unabs_def = unabs_all_def ctxt unfolded_def
+ val rep = (snd o Thm.dest_comb o snd o Thm.dest_comb o cprop_of) quot_thm
+ val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
+ val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
+ val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans}
+ in
+ simplify_code_eq ctxt code_cert
+ end
+
+fun define_code_cert def_thm rsp_thm (rty, qty) lthy =
+ let
+ val quot_thm = Quotient_Term.prove_quot_theorem lthy (get_body_types (rty, qty))
+ in
+ if Quotient_Type.can_generate_code_cert quot_thm then
+ let
+ val code_cert = generate_code_cert lthy def_thm rsp_thm (rty, qty)
+ val add_abs_eqn_attribute =
+ Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I)
+ val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
+ in
+ lthy
+ |> (snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [code_cert])
+ end
+ else
+ lthy
+ end
+
+fun define_code_eq def_thm lthy =
+ let
+ val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
+ val code_eq = unabs_all_def lthy unfolded_def
+ val simp_code_eq = simplify_code_eq lthy code_eq
+ in
+ lthy
+ |> (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [simp_code_eq])
+ end
+
+fun define_code def_thm rsp_thm (rty, qty) lthy =
+ if body_type rty = body_type qty then
+ define_code_eq def_thm lthy
+ else
+ define_code_cert def_thm rsp_thm (rty, qty) lthy
+
(* The ML-interface for a quotient definition takes
as argument:
@@ -52,17 +176,19 @@
fun add_quotient_def ((var, (name, atts)), (lhs, rhs)) rsp_thm lthy =
let
+ val rty = fastype_of rhs
+ val qty = fastype_of lhs
val absrep_trm =
- Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, fastype_of lhs) $ rhs
+ Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (rty, qty) $ rhs
val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm))
val (_, prop') = Local_Defs.cert_def lthy prop
val (_, newrhs) = Local_Defs.abs_def prop'
- val ((trm, (_ , thm)), lthy') =
+ val ((trm, (_ , def_thm)), lthy') =
Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy
(* data storage *)
- val qconst_data = {qconst = trm, rconst = rhs, def = thm}
+ val qconst_data = {qconst = trm, rconst = rhs, def = def_thm}
fun get_rsp_thm_name (lhs_name, _) = Binding.suffix_name "_rsp" lhs_name
val lthy'' = lthy'
@@ -75,6 +201,7 @@
|> (snd oo Local_Theory.note)
((get_rsp_thm_name var, [Attrib.internal (K Quotient_Info.rsp_rules_add)]),
[rsp_thm])
+ |> define_code def_thm rsp_thm (rty, qty)
in
(qconst_data, lthy'')
@@ -99,7 +226,8 @@
fun simp_arrows_conv ctm =
let
val unfold_conv = Conv.rewrs_conv
- [@{thm fun_rel_eq_rel[THEN eq_reflection]}, @{thm fun_rel_def[THEN eq_reflection]}]
+ [@{thm fun_rel_eq_invariant[THEN eq_reflection]}, @{thm fun_rel_eq_rel[THEN eq_reflection]},
+ @{thm fun_rel_def[THEN eq_reflection]}]
val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
in
@@ -109,11 +237,14 @@
| _ => Conv.all_conv ctm
end
+ val unfold_ret_val_invs = Conv.bottom_conv
+ (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy
val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
+ val beta_conv = Thm.beta_conversion true
val eq_thm =
- (simp_conv then_conv univq_prenex_conv then_conv Thm.beta_conversion true) ctm
+ (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
in
Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2)
end
--- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Mar 23 14:21:41 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Mar 23 14:25:31 2012 +0100
@@ -20,6 +20,9 @@
val equiv_relation: Proof.context -> typ * typ -> term
val equiv_relation_chk: Proof.context -> typ * typ -> term
+ val get_rel_from_quot_thm: thm -> term
+ val prove_quot_theorem: Proof.context -> typ * typ -> thm
+
val regularize_trm: Proof.context -> term * term -> term
val regularize_trm_chk: Proof.context -> term * term -> term
@@ -331,6 +334,78 @@
equiv_relation ctxt (rty, qty)
|> Syntax.check_term ctxt
+(* generation of the Quotient theorem *)
+
+fun get_quot_thm ctxt s =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ in
+ (case Quotient_Info.lookup_quotients_global thy s of
+ SOME qdata => #quot_thm qdata
+ | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
+ end
+
+fun get_rel_quot_thm thy s =
+ (case Quotient_Info.lookup_quotmaps thy s of
+ SOME map_data => #quot_thm map_data
+ | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"));
+
+fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
+
+infix 0 MRSL
+
+fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+
+exception NOT_IMPL of string
+
+fun get_rel_from_quot_thm quot_thm =
+ let
+ val (_ $ rel $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) quot_thm
+ in
+ rel
+ end
+
+fun mk_quot_thm_compose (rel_quot_thm, quot_thm) =
+ let
+ val quot_thm_rel = get_rel_from_quot_thm quot_thm
+ in
+ if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient}
+ else raise NOT_IMPL "nested quotients: not implemented yet"
+ end
+
+fun prove_quot_theorem ctxt (rty, qty) =
+ if rty = qty
+ then @{thm identity_quotient}
+ else
+ case (rty, qty) of
+ (Type (s, tys), Type (s', tys')) =>
+ if s = s'
+ then
+ let
+ val args = map (prove_quot_theorem ctxt) (tys ~~ tys')
+ in
+ args MRSL (get_rel_quot_thm ctxt s)
+ end
+ else
+ let
+ val (Type (_, rtys), qty_pat) = get_rty_qty ctxt 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')
+ val quot_thm = get_quot_thm ctxt s'
+ in
+ if forall is_id_quot args
+ then
+ quot_thm
+ else
+ let
+ val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s)
+ in
+ mk_quot_thm_compose (rel_quot_thm, quot_thm)
+ end
+ end
+ | _ => @{thm identity_quotient}
+
(*** Regularization ***)
--- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 23 14:21:41 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 23 14:25:31 2012 +0100
@@ -6,6 +6,8 @@
signature QUOTIENT_TYPE =
sig
+ val can_generate_code_cert: thm -> bool
+
val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) *
((binding * binding) option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
@@ -76,6 +78,44 @@
Goal.prove lthy [] [] goal
(K (typedef_quot_type_tac equiv_thm typedef_info))
end
+
+fun can_generate_code_cert quot_thm =
+ case Quotient_Term.get_rel_from_quot_thm quot_thm of
+ Const (@{const_name HOL.eq}, _) => true
+ | Const (@{const_name invariant}, _) $ _ => true
+ | _ => false
+
+fun define_abs_type quot_thm lthy =
+ if can_generate_code_cert quot_thm then
+ let
+ val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
+ val add_abstype_attribute =
+ Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
+ val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
+ in
+ lthy
+ |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
+ end
+ else
+ lthy
+
+fun init_quotient_infr quot_thm equiv_thm lthy =
+ let
+ val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm
+ val (qtyp, rtyp) = (dest_funT o fastype_of) rep
+ val qty_full_name = (fst o dest_Type) qtyp
+ val quotients = {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm,
+ quot_thm = quot_thm }
+ fun quot_info phi = Quotient_Info.transform_quotients phi quotients
+ val abs_rep = {abs = abs, rep = rep}
+ fun abs_rep_info phi = Quotient_Info.transform_abs_rep phi abs_rep
+ in
+ lthy
+ |> Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Quotient_Info.update_quotients qty_full_name (quot_info phi)
+ #> Quotient_Info.update_abs_rep qty_full_name (abs_rep_info phi))
+ |> define_abs_type quot_thm
+ end
(* main function for constructing a quotient type *)
fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), equiv_thm) lthy =
@@ -86,7 +126,7 @@
else equiv_thm RS @{thm equivp_implies_part_equivp}
(* generates the typedef *)
- val ((qty_full_name, typedef_info), lthy1) =
+ val ((_, typedef_info), lthy1) =
typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
(* abs and rep functions from the typedef *)
@@ -108,9 +148,9 @@
NONE => (Binding.prefix_name "rep_" qty_name, Binding.prefix_name "abs_" qty_name)
| SOME morphs => morphs)
- val ((abs_t, (_, abs_def)), lthy2) = lthy1
+ val ((_, (_, abs_def)), lthy2) = lthy1
|> Local_Theory.define ((abs_name, NoSyn), ((Thm.def_binding abs_name, []), abs_trm))
- val ((rep_t, (_, rep_def)), lthy3) = lthy2
+ val ((_, (_, rep_def)), lthy3) = lthy2
|> Local_Theory.define ((rep_name, NoSyn), ((Thm.def_binding rep_name, []), rep_trm))
(* quot_type theorem *)
@@ -129,13 +169,8 @@
val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm,
quot_thm = quotient_thm}
- fun qinfo phi = Quotient_Info.transform_quotients phi quotients
- fun abs_rep phi = Quotient_Info.transform_abs_rep phi {abs = abs_t, rep = rep_t}
-
val lthy4 = lthy3
- |> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
- #> Quotient_Info.update_abs_rep qty_full_name (abs_rep phi))
+ |> init_quotient_infr quotient_thm equiv_thm
|> (snd oo Local_Theory.note)
((equiv_thm_name,
if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
@@ -276,6 +311,32 @@
val _ =
Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
"quotient type definitions (require equivalence proofs)"
- (quotspec_parser >> quotient_type_cmd)
+ (quotspec_parser >> quotient_type_cmd)
+
+(* Setup lifting using type_def_thm *)
+
+exception SETUP_LIFT_TYPE of string
+
+fun setup_lift_type typedef_thm =
+ let
+ val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
+ val (quot_thm, equivp_thm) = (case typedef_set of
+ Const ("Orderings.top_class.top", _) =>
+ (typedef_thm RS @{thm copy_type_to_Quotient},
+ typedef_thm RS @{thm copy_type_to_equivp})
+ | Const (@{const_name "Collect"}, _) $ Abs (_, _, _ $ Bound 0) =>
+ (typedef_thm RS @{thm invariant_type_to_Quotient},
+ typedef_thm RS @{thm invariant_type_to_part_equivp})
+ | _ => raise SETUP_LIFT_TYPE "unsupported typedef theorem")
+ in
+ init_quotient_infr quot_thm equivp_thm
+ end
+
+fun setup_lift_type_aux xthm lthy = setup_lift_type (singleton (Attrib.eval_thms lthy) xthm) lthy
+
+val _ =
+ Outer_Syntax.local_theory @{command_spec "setup_lifting"}
+ "Setup lifting infrastracture"
+ (Parse_Spec.xthm >> (fn xthm => setup_lift_type_aux xthm))
end;