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
1.1 --- a/src/HOL/Quotient.thy Fri Mar 23 14:21:41 2012 +0100
1.2 +++ b/src/HOL/Quotient.thy Fri Mar 23 14:25:31 2012 +0100
1.3 @@ -9,6 +9,7 @@
1.4 keywords
1.5 "print_quotmaps" "print_quotients" "print_quotconsts" :: diag and
1.6 "quotient_type" :: thy_goal and "/" and
1.7 + "setup_lifting" :: thy_decl and
1.8 "quotient_definition" :: thy_goal
1.9 uses
1.10 ("Tools/Quotient/quotient_info.ML")
1.11 @@ -137,6 +138,18 @@
1.12 unfolding Quotient_def
1.13 by blast
1.14
1.15 +lemma Quotient_refl1:
1.16 + assumes a: "Quotient R Abs Rep"
1.17 + shows "R r s \<Longrightarrow> R r r"
1.18 + using a unfolding Quotient_def
1.19 + by fast
1.20 +
1.21 +lemma Quotient_refl2:
1.22 + assumes a: "Quotient R Abs Rep"
1.23 + shows "R r s \<Longrightarrow> R s s"
1.24 + using a unfolding Quotient_def
1.25 + by fast
1.26 +
1.27 lemma Quotient_rel_rep:
1.28 assumes a: "Quotient R Abs Rep"
1.29 shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
1.30 @@ -263,6 +276,15 @@
1.31 shows "R2 (f x) (g y)"
1.32 using a by (auto elim: fun_relE)
1.33
1.34 +lemma apply_rsp'':
1.35 + assumes "Quotient R Abs Rep"
1.36 + and "(R ===> S) f f"
1.37 + shows "S (f (Rep x)) (f (Rep x))"
1.38 +proof -
1.39 + from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp)
1.40 + then show ?thesis using assms(2) by (auto intro: apply_rsp')
1.41 +qed
1.42 +
1.43 subsection {* lemmas for regularisation of ball and bex *}
1.44
1.45 lemma ball_reg_eqv:
1.46 @@ -679,6 +701,153 @@
1.47
1.48 end
1.49
1.50 +subsection {* Quotient composition *}
1.51 +
1.52 +lemma OOO_quotient:
1.53 + fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
1.54 + fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
1.55 + fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
1.56 + fixes R2' :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
1.57 + fixes R2 :: "'b \<Rightarrow> 'b \<Rightarrow> bool"
1.58 + assumes R1: "Quotient R1 Abs1 Rep1"
1.59 + assumes R2: "Quotient R2 Abs2 Rep2"
1.60 + assumes Abs1: "\<And>x y. R2' x y \<Longrightarrow> R1 x x \<Longrightarrow> R1 y y \<Longrightarrow> R2 (Abs1 x) (Abs1 y)"
1.61 + assumes Rep1: "\<And>x y. R2 x y \<Longrightarrow> R2' (Rep1 x) (Rep1 y)"
1.62 + shows "Quotient (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
1.63 +apply (rule QuotientI)
1.64 + apply (simp add: o_def Quotient_abs_rep [OF R2] Quotient_abs_rep [OF R1])
1.65 + apply simp
1.66 + apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI)
1.67 + apply (rule Quotient_rep_reflp [OF R1])
1.68 + apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated])
1.69 + apply (rule Quotient_rep_reflp [OF R1])
1.70 + apply (rule Rep1)
1.71 + apply (rule Quotient_rep_reflp [OF R2])
1.72 + apply safe
1.73 + apply (rename_tac x y)
1.74 + apply (drule Abs1)
1.75 + apply (erule Quotient_refl2 [OF R1])
1.76 + apply (erule Quotient_refl1 [OF R1])
1.77 + apply (drule Quotient_refl1 [OF R2], drule Rep1)
1.78 + apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
1.79 + apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption)
1.80 + apply (erule pred_compI)
1.81 + apply (erule Quotient_symp [OF R1, THEN sympD])
1.82 + apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
1.83 + apply (rule conjI, erule Quotient_refl1 [OF R1])
1.84 + apply (rule conjI, rule Quotient_rep_reflp [OF R1])
1.85 + apply (subst Quotient_abs_rep [OF R1])
1.86 + apply (erule Quotient_rel_abs [OF R1])
1.87 + apply (rename_tac x y)
1.88 + apply (drule Abs1)
1.89 + apply (erule Quotient_refl2 [OF R1])
1.90 + apply (erule Quotient_refl1 [OF R1])
1.91 + apply (drule Quotient_refl2 [OF R2], drule Rep1)
1.92 + apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
1.93 + apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption)
1.94 + apply (erule pred_compI)
1.95 + apply (erule Quotient_symp [OF R1, THEN sympD])
1.96 + apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
1.97 + apply (rule conjI, erule Quotient_refl2 [OF R1])
1.98 + apply (rule conjI, rule Quotient_rep_reflp [OF R1])
1.99 + apply (subst Quotient_abs_rep [OF R1])
1.100 + apply (erule Quotient_rel_abs [OF R1, THEN sym])
1.101 + apply simp
1.102 + apply (rule Quotient_rel_abs [OF R2])
1.103 + apply (rule Quotient_rel_abs [OF R1, THEN ssubst], assumption)
1.104 + apply (rule Quotient_rel_abs [OF R1, THEN subst], assumption)
1.105 + apply (erule Abs1)
1.106 + apply (erule Quotient_refl2 [OF R1])
1.107 + apply (erule Quotient_refl1 [OF R1])
1.108 + apply (rename_tac a b c d)
1.109 + apply simp
1.110 + apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI)
1.111 + apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
1.112 + apply (rule conjI, erule Quotient_refl1 [OF R1])
1.113 + apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
1.114 + apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated])
1.115 + apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
1.116 + apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
1.117 + apply (erule Quotient_refl2 [OF R1])
1.118 + apply (rule Rep1)
1.119 + apply (drule Abs1)
1.120 + apply (erule Quotient_refl2 [OF R1])
1.121 + apply (erule Quotient_refl1 [OF R1])
1.122 + apply (drule Abs1)
1.123 + apply (erule Quotient_refl2 [OF R1])
1.124 + apply (erule Quotient_refl1 [OF R1])
1.125 + apply (drule Quotient_rel_abs [OF R1])
1.126 + apply (drule Quotient_rel_abs [OF R1])
1.127 + apply (drule Quotient_rel_abs [OF R1])
1.128 + apply (drule Quotient_rel_abs [OF R1])
1.129 + apply simp
1.130 + apply (rule Quotient_rel[symmetric, OF R2, THEN iffD2])
1.131 + apply simp
1.132 +done
1.133 +
1.134 +lemma OOO_eq_quotient:
1.135 + fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
1.136 + fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
1.137 + fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
1.138 + assumes R1: "Quotient R1 Abs1 Rep1"
1.139 + assumes R2: "Quotient op= Abs2 Rep2"
1.140 + shows "Quotient (R1 OOO op=) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
1.141 +using assms
1.142 +by (rule OOO_quotient) auto
1.143 +
1.144 +subsection {* Invariant *}
1.145 +
1.146 +definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
1.147 + where "invariant R = (\<lambda>x y. R x \<and> x = y)"
1.148 +
1.149 +lemma invariant_to_eq:
1.150 + assumes "invariant P x y"
1.151 + shows "x = y"
1.152 +using assms by (simp add: invariant_def)
1.153 +
1.154 +lemma fun_rel_eq_invariant:
1.155 + shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
1.156 +by (auto simp add: invariant_def fun_rel_def)
1.157 +
1.158 +lemma invariant_same_args:
1.159 + shows "invariant P x x \<equiv> P x"
1.160 +using assms by (auto simp add: invariant_def)
1.161 +
1.162 +lemma copy_type_to_Quotient:
1.163 + assumes "type_definition Rep Abs UNIV"
1.164 + shows "Quotient (op =) Abs Rep"
1.165 +proof -
1.166 + interpret type_definition Rep Abs UNIV by fact
1.167 + from Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI)
1.168 +qed
1.169 +
1.170 +lemma copy_type_to_equivp:
1.171 + fixes Abs :: "'a \<Rightarrow> 'b"
1.172 + and Rep :: "'b \<Rightarrow> 'a"
1.173 + assumes "type_definition Rep Abs (UNIV::'a set)"
1.174 + shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
1.175 +by (rule identity_equivp)
1.176 +
1.177 +lemma invariant_type_to_Quotient:
1.178 + assumes "type_definition Rep Abs {x. P x}"
1.179 + shows "Quotient (invariant P) Abs Rep"
1.180 +proof -
1.181 + interpret type_definition Rep Abs "{x. P x}" by fact
1.182 + from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI simp: invariant_def)
1.183 +qed
1.184 +
1.185 +lemma invariant_type_to_part_equivp:
1.186 + assumes "type_definition Rep Abs {x. P x}"
1.187 + shows "part_equivp (invariant P)"
1.188 +proof (intro part_equivpI)
1.189 + interpret type_definition Rep Abs "{x. P x}" by fact
1.190 + show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
1.191 +next
1.192 + show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
1.193 +next
1.194 + show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
1.195 +qed
1.196 +
1.197 subsection {* ML setup *}
1.198
1.199 text {* Auxiliary data for the quotient package *}
2.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Mar 23 14:21:41 2012 +0100
2.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Mar 23 14:25:31 2012 +0100
2.3 @@ -27,6 +27,130 @@
2.4
2.5 (** Interface and Syntax Setup **)
2.6
2.7 +(* Generation of the code certificate from the rsp theorem *)
2.8 +
2.9 +infix 0 MRSL
2.10 +
2.11 +fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
2.12 +
2.13 +fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
2.14 + | get_body_types (U, V) = (U, V)
2.15 +
2.16 +fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
2.17 + | get_binder_types _ = []
2.18 +
2.19 +fun unabs_def ctxt def =
2.20 + let
2.21 + val (_, rhs) = Thm.dest_equals (cprop_of def)
2.22 + fun dest_abs (Abs (var_name, T, _)) = (var_name, T)
2.23 + | dest_abs tm = raise TERM("get_abs_var",[tm])
2.24 + val (var_name, T) = dest_abs (term_of rhs)
2.25 + val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt
2.26 + val thy = Proof_Context.theory_of ctxt'
2.27 + val refl_thm = Thm.reflexive (cterm_of thy (Free (hd new_var_names, T)))
2.28 + in
2.29 + Thm.combination def refl_thm |>
2.30 + singleton (Proof_Context.export ctxt' ctxt)
2.31 + end
2.32 +
2.33 +fun unabs_all_def ctxt def =
2.34 + let
2.35 + val (_, rhs) = Thm.dest_equals (cprop_of def)
2.36 + val xs = strip_abs_vars (term_of rhs)
2.37 + in
2.38 + fold (K (unabs_def ctxt)) xs def
2.39 + end
2.40 +
2.41 +val map_fun_unfolded =
2.42 + @{thm map_fun_def[abs_def]} |>
2.43 + unabs_def @{context} |>
2.44 + unabs_def @{context} |>
2.45 + Local_Defs.unfold @{context} [@{thm comp_def}]
2.46 +
2.47 +fun unfold_fun_maps ctm =
2.48 + let
2.49 + fun unfold_conv ctm =
2.50 + case (Thm.term_of ctm) of
2.51 + Const (@{const_name "map_fun"}, _) $ _ $ _ =>
2.52 + (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
2.53 + | _ => Conv.all_conv ctm
2.54 + val try_beta_conv = Conv.try_conv (Thm.beta_conversion false)
2.55 + in
2.56 + (Conv.arg_conv (Conv.fun_conv unfold_conv then_conv try_beta_conv)) ctm
2.57 + end
2.58 +
2.59 +fun prove_rel ctxt rsp_thm (rty, qty) =
2.60 + let
2.61 + val ty_args = get_binder_types (rty, qty)
2.62 + fun disch_arg args_ty thm =
2.63 + let
2.64 + val quot_thm = Quotient_Term.prove_quot_theorem ctxt args_ty
2.65 + in
2.66 + [quot_thm, thm] MRSL @{thm apply_rsp''}
2.67 + end
2.68 + in
2.69 + fold disch_arg ty_args rsp_thm
2.70 + end
2.71 +
2.72 +exception CODE_CERT_GEN of string
2.73 +
2.74 +fun simplify_code_eq ctxt def_thm =
2.75 + Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm
2.76 +
2.77 +fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) =
2.78 + let
2.79 + val quot_thm = Quotient_Term.prove_quot_theorem ctxt (get_body_types (rty, qty))
2.80 + val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
2.81 + val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs}
2.82 + val abs_rep_eq =
2.83 + case (HOLogic.dest_Trueprop o prop_of) fun_rel of
2.84 + Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm
2.85 + | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
2.86 + | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
2.87 + val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
2.88 + val unabs_def = unabs_all_def ctxt unfolded_def
2.89 + val rep = (snd o Thm.dest_comb o snd o Thm.dest_comb o cprop_of) quot_thm
2.90 + val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
2.91 + val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
2.92 + val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans}
2.93 + in
2.94 + simplify_code_eq ctxt code_cert
2.95 + end
2.96 +
2.97 +fun define_code_cert def_thm rsp_thm (rty, qty) lthy =
2.98 + let
2.99 + val quot_thm = Quotient_Term.prove_quot_theorem lthy (get_body_types (rty, qty))
2.100 + in
2.101 + if Quotient_Type.can_generate_code_cert quot_thm then
2.102 + let
2.103 + val code_cert = generate_code_cert lthy def_thm rsp_thm (rty, qty)
2.104 + val add_abs_eqn_attribute =
2.105 + Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I)
2.106 + val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
2.107 + in
2.108 + lthy
2.109 + |> (snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [code_cert])
2.110 + end
2.111 + else
2.112 + lthy
2.113 + end
2.114 +
2.115 +fun define_code_eq def_thm lthy =
2.116 + let
2.117 + val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
2.118 + val code_eq = unabs_all_def lthy unfolded_def
2.119 + val simp_code_eq = simplify_code_eq lthy code_eq
2.120 + in
2.121 + lthy
2.122 + |> (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [simp_code_eq])
2.123 + end
2.124 +
2.125 +fun define_code def_thm rsp_thm (rty, qty) lthy =
2.126 + if body_type rty = body_type qty then
2.127 + define_code_eq def_thm lthy
2.128 + else
2.129 + define_code_cert def_thm rsp_thm (rty, qty) lthy
2.130 +
2.131 (* The ML-interface for a quotient definition takes
2.132 as argument:
2.133
2.134 @@ -52,17 +176,19 @@
2.135
2.136 fun add_quotient_def ((var, (name, atts)), (lhs, rhs)) rsp_thm lthy =
2.137 let
2.138 + val rty = fastype_of rhs
2.139 + val qty = fastype_of lhs
2.140 val absrep_trm =
2.141 - Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, fastype_of lhs) $ rhs
2.142 + Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (rty, qty) $ rhs
2.143 val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm))
2.144 val (_, prop') = Local_Defs.cert_def lthy prop
2.145 val (_, newrhs) = Local_Defs.abs_def prop'
2.146
2.147 - val ((trm, (_ , thm)), lthy') =
2.148 + val ((trm, (_ , def_thm)), lthy') =
2.149 Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy
2.150
2.151 (* data storage *)
2.152 - val qconst_data = {qconst = trm, rconst = rhs, def = thm}
2.153 + val qconst_data = {qconst = trm, rconst = rhs, def = def_thm}
2.154 fun get_rsp_thm_name (lhs_name, _) = Binding.suffix_name "_rsp" lhs_name
2.155
2.156 val lthy'' = lthy'
2.157 @@ -75,6 +201,7 @@
2.158 |> (snd oo Local_Theory.note)
2.159 ((get_rsp_thm_name var, [Attrib.internal (K Quotient_Info.rsp_rules_add)]),
2.160 [rsp_thm])
2.161 + |> define_code def_thm rsp_thm (rty, qty)
2.162
2.163 in
2.164 (qconst_data, lthy'')
2.165 @@ -99,7 +226,8 @@
2.166 fun simp_arrows_conv ctm =
2.167 let
2.168 val unfold_conv = Conv.rewrs_conv
2.169 - [@{thm fun_rel_eq_rel[THEN eq_reflection]}, @{thm fun_rel_def[THEN eq_reflection]}]
2.170 + [@{thm fun_rel_eq_invariant[THEN eq_reflection]}, @{thm fun_rel_eq_rel[THEN eq_reflection]},
2.171 + @{thm fun_rel_def[THEN eq_reflection]}]
2.172 val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
2.173 fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
2.174 in
2.175 @@ -109,11 +237,14 @@
2.176 | _ => Conv.all_conv ctm
2.177 end
2.178
2.179 + val unfold_ret_val_invs = Conv.bottom_conv
2.180 + (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy
2.181 val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
2.182 val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
2.183 val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
2.184 + val beta_conv = Thm.beta_conversion true
2.185 val eq_thm =
2.186 - (simp_conv then_conv univq_prenex_conv then_conv Thm.beta_conversion true) ctm
2.187 + (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
2.188 in
2.189 Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2)
2.190 end
3.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Mar 23 14:21:41 2012 +0100
3.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Mar 23 14:25:31 2012 +0100
3.3 @@ -20,6 +20,9 @@
3.4 val equiv_relation: Proof.context -> typ * typ -> term
3.5 val equiv_relation_chk: Proof.context -> typ * typ -> term
3.6
3.7 + val get_rel_from_quot_thm: thm -> term
3.8 + val prove_quot_theorem: Proof.context -> typ * typ -> thm
3.9 +
3.10 val regularize_trm: Proof.context -> term * term -> term
3.11 val regularize_trm_chk: Proof.context -> term * term -> term
3.12
3.13 @@ -331,6 +334,78 @@
3.14 equiv_relation ctxt (rty, qty)
3.15 |> Syntax.check_term ctxt
3.16
3.17 +(* generation of the Quotient theorem *)
3.18 +
3.19 +fun get_quot_thm ctxt s =
3.20 + let
3.21 + val thy = Proof_Context.theory_of ctxt
3.22 + in
3.23 + (case Quotient_Info.lookup_quotients_global thy s of
3.24 + SOME qdata => #quot_thm qdata
3.25 + | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
3.26 + end
3.27 +
3.28 +fun get_rel_quot_thm thy s =
3.29 + (case Quotient_Info.lookup_quotmaps thy s of
3.30 + SOME map_data => #quot_thm map_data
3.31 + | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"));
3.32 +
3.33 +fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
3.34 +
3.35 +infix 0 MRSL
3.36 +
3.37 +fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
3.38 +
3.39 +exception NOT_IMPL of string
3.40 +
3.41 +fun get_rel_from_quot_thm quot_thm =
3.42 + let
3.43 + val (_ $ rel $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) quot_thm
3.44 + in
3.45 + rel
3.46 + end
3.47 +
3.48 +fun mk_quot_thm_compose (rel_quot_thm, quot_thm) =
3.49 + let
3.50 + val quot_thm_rel = get_rel_from_quot_thm quot_thm
3.51 + in
3.52 + if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient}
3.53 + else raise NOT_IMPL "nested quotients: not implemented yet"
3.54 + end
3.55 +
3.56 +fun prove_quot_theorem ctxt (rty, qty) =
3.57 + if rty = qty
3.58 + then @{thm identity_quotient}
3.59 + else
3.60 + case (rty, qty) of
3.61 + (Type (s, tys), Type (s', tys')) =>
3.62 + if s = s'
3.63 + then
3.64 + let
3.65 + val args = map (prove_quot_theorem ctxt) (tys ~~ tys')
3.66 + in
3.67 + args MRSL (get_rel_quot_thm ctxt s)
3.68 + end
3.69 + else
3.70 + let
3.71 + val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
3.72 + val qtyenv = match ctxt equiv_match_err qty_pat qty
3.73 + val rtys' = map (Envir.subst_type qtyenv) rtys
3.74 + val args = map (prove_quot_theorem ctxt) (tys ~~ rtys')
3.75 + val quot_thm = get_quot_thm ctxt s'
3.76 + in
3.77 + if forall is_id_quot args
3.78 + then
3.79 + quot_thm
3.80 + else
3.81 + let
3.82 + val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s)
3.83 + in
3.84 + mk_quot_thm_compose (rel_quot_thm, quot_thm)
3.85 + end
3.86 + end
3.87 + | _ => @{thm identity_quotient}
3.88 +
3.89
3.90
3.91 (*** Regularization ***)
4.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 23 14:21:41 2012 +0100
4.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 23 14:25:31 2012 +0100
4.3 @@ -6,6 +6,8 @@
4.4
4.5 signature QUOTIENT_TYPE =
4.6 sig
4.7 + val can_generate_code_cert: thm -> bool
4.8 +
4.9 val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) *
4.10 ((binding * binding) option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
4.11
4.12 @@ -76,6 +78,44 @@
4.13 Goal.prove lthy [] [] goal
4.14 (K (typedef_quot_type_tac equiv_thm typedef_info))
4.15 end
4.16 +
4.17 +fun can_generate_code_cert quot_thm =
4.18 + case Quotient_Term.get_rel_from_quot_thm quot_thm of
4.19 + Const (@{const_name HOL.eq}, _) => true
4.20 + | Const (@{const_name invariant}, _) $ _ => true
4.21 + | _ => false
4.22 +
4.23 +fun define_abs_type quot_thm lthy =
4.24 + if can_generate_code_cert quot_thm then
4.25 + let
4.26 + val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
4.27 + val add_abstype_attribute =
4.28 + Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
4.29 + val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
4.30 + in
4.31 + lthy
4.32 + |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
4.33 + end
4.34 + else
4.35 + lthy
4.36 +
4.37 +fun init_quotient_infr quot_thm equiv_thm lthy =
4.38 + let
4.39 + val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm
4.40 + val (qtyp, rtyp) = (dest_funT o fastype_of) rep
4.41 + val qty_full_name = (fst o dest_Type) qtyp
4.42 + val quotients = {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm,
4.43 + quot_thm = quot_thm }
4.44 + fun quot_info phi = Quotient_Info.transform_quotients phi quotients
4.45 + val abs_rep = {abs = abs, rep = rep}
4.46 + fun abs_rep_info phi = Quotient_Info.transform_abs_rep phi abs_rep
4.47 + in
4.48 + lthy
4.49 + |> Local_Theory.declaration {syntax = false, pervasive = true}
4.50 + (fn phi => Quotient_Info.update_quotients qty_full_name (quot_info phi)
4.51 + #> Quotient_Info.update_abs_rep qty_full_name (abs_rep_info phi))
4.52 + |> define_abs_type quot_thm
4.53 + end
4.54
4.55 (* main function for constructing a quotient type *)
4.56 fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), equiv_thm) lthy =
4.57 @@ -86,7 +126,7 @@
4.58 else equiv_thm RS @{thm equivp_implies_part_equivp}
4.59
4.60 (* generates the typedef *)
4.61 - val ((qty_full_name, typedef_info), lthy1) =
4.62 + val ((_, typedef_info), lthy1) =
4.63 typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
4.64
4.65 (* abs and rep functions from the typedef *)
4.66 @@ -108,9 +148,9 @@
4.67 NONE => (Binding.prefix_name "rep_" qty_name, Binding.prefix_name "abs_" qty_name)
4.68 | SOME morphs => morphs)
4.69
4.70 - val ((abs_t, (_, abs_def)), lthy2) = lthy1
4.71 + val ((_, (_, abs_def)), lthy2) = lthy1
4.72 |> Local_Theory.define ((abs_name, NoSyn), ((Thm.def_binding abs_name, []), abs_trm))
4.73 - val ((rep_t, (_, rep_def)), lthy3) = lthy2
4.74 + val ((_, (_, rep_def)), lthy3) = lthy2
4.75 |> Local_Theory.define ((rep_name, NoSyn), ((Thm.def_binding rep_name, []), rep_trm))
4.76
4.77 (* quot_type theorem *)
4.78 @@ -129,13 +169,8 @@
4.79 val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm,
4.80 quot_thm = quotient_thm}
4.81
4.82 - fun qinfo phi = Quotient_Info.transform_quotients phi quotients
4.83 - fun abs_rep phi = Quotient_Info.transform_abs_rep phi {abs = abs_t, rep = rep_t}
4.84 -
4.85 val lthy4 = lthy3
4.86 - |> Local_Theory.declaration {syntax = false, pervasive = true}
4.87 - (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
4.88 - #> Quotient_Info.update_abs_rep qty_full_name (abs_rep phi))
4.89 + |> init_quotient_infr quotient_thm equiv_thm
4.90 |> (snd oo Local_Theory.note)
4.91 ((equiv_thm_name,
4.92 if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
4.93 @@ -276,6 +311,32 @@
4.94 val _ =
4.95 Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
4.96 "quotient type definitions (require equivalence proofs)"
4.97 - (quotspec_parser >> quotient_type_cmd)
4.98 + (quotspec_parser >> quotient_type_cmd)
4.99 +
4.100 +(* Setup lifting using type_def_thm *)
4.101 +
4.102 +exception SETUP_LIFT_TYPE of string
4.103 +
4.104 +fun setup_lift_type typedef_thm =
4.105 + let
4.106 + val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
4.107 + val (quot_thm, equivp_thm) = (case typedef_set of
4.108 + Const ("Orderings.top_class.top", _) =>
4.109 + (typedef_thm RS @{thm copy_type_to_Quotient},
4.110 + typedef_thm RS @{thm copy_type_to_equivp})
4.111 + | Const (@{const_name "Collect"}, _) $ Abs (_, _, _ $ Bound 0) =>
4.112 + (typedef_thm RS @{thm invariant_type_to_Quotient},
4.113 + typedef_thm RS @{thm invariant_type_to_part_equivp})
4.114 + | _ => raise SETUP_LIFT_TYPE "unsupported typedef theorem")
4.115 + in
4.116 + init_quotient_infr quot_thm equivp_thm
4.117 + end
4.118 +
4.119 +fun setup_lift_type_aux xthm lthy = setup_lift_type (singleton (Attrib.eval_thms lthy) xthm) lthy
4.120 +
4.121 +val _ =
4.122 + Outer_Syntax.local_theory @{command_spec "setup_lifting"}
4.123 + "Setup lifting infrastracture"
4.124 + (Parse_Spec.xthm >> (fn xthm => setup_lift_type_aux xthm))
4.125
4.126 end;