# HG changeset patch # User kuncar # Date 1332509131 -3600 # Node ID 3ea48c19673e4f35b0d70b7d1260a6a553dc597f # Parent b43ddeea727f27a8ff2dc561fc71c4c1c906274f 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 diff -r b43ddeea727f -r 3ea48c19673e src/HOL/Quotient.thy --- 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 \ R r r" + using a unfolding Quotient_def + by fast + +lemma Quotient_refl2: + assumes a: "Quotient R Abs Rep" + shows "R r s \ 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) \ 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 \ 'a \ bool" + fixes Abs1 :: "'a \ 'b" and Rep1 :: "'b \ 'a" + fixes Abs2 :: "'b \ 'c" and Rep2 :: "'c \ 'b" + fixes R2' :: "'a \ 'a \ bool" + fixes R2 :: "'b \ 'b \ bool" + assumes R1: "Quotient R1 Abs1 Rep1" + assumes R2: "Quotient R2 Abs2 Rep2" + assumes Abs1: "\x y. R2' x y \ R1 x x \ R1 y y \ R2 (Abs1 x) (Abs1 y)" + assumes Rep1: "\x y. R2 x y \ R2' (Rep1 x) (Rep1 y)" + shows "Quotient (R1 OO R2' OO R1) (Abs2 \ Abs1) (Rep1 \ 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 \ 'a \ bool" + fixes Abs1 :: "'a \ 'b" and Rep1 :: "'b \ 'a" + fixes Abs2 :: "'b \ 'c" and Rep2 :: "'c \ 'b" + assumes R1: "Quotient R1 Abs1 Rep1" + assumes R2: "Quotient op= Abs2 Rep2" + shows "Quotient (R1 OOO op=) (Abs2 \ Abs1) (Rep1 \ Rep2)" +using assms +by (rule OOO_quotient) auto + +subsection {* Invariant *} + +definition invariant :: "('a \ bool) \ 'a \ 'a \ bool" + where "invariant R = (\x y. R x \ 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) = (\f g. \x. R x \ S (f x) (g x))" +by (auto simp add: invariant_def fun_rel_def) + +lemma invariant_same_args: + shows "invariant P x x \ 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 \ 'b" + and Rep :: "'b \ 'a" + assumes "type_definition Rep Abs (UNIV::'a set)" + shows "equivp (op=::'a\'a\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 "\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 *} diff -r b43ddeea727f -r 3ea48c19673e src/HOL/Tools/Quotient/quotient_def.ML --- 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 diff -r b43ddeea727f -r 3ea48c19673e src/HOL/Tools/Quotient/quotient_term.ML --- 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 ***) diff -r b43ddeea727f -r 3ea48c19673e src/HOL/Tools/Quotient/quotient_type.ML --- 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;