# HG changeset patch # User kuncar # Date 1337188819 -7200 # Node ID 2924f37cb6b38ae6cf70ab9105dae993dc10ae65 # Parent 70375fa2679d9e0caa3435ad2b002725c30c955f remove the generation of a code certificate from the Quotient package (mainly from quotient_def), because it's in lift_definition now diff -r 70375fa2679d -r 2924f37cb6b3 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Wed May 16 19:17:20 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Wed May 16 19:20:19 2012 +0200 @@ -31,124 +31,6 @@ infix 0 MRSL -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_thm ctxt args_ty - in - [quot_thm, thm] MRSL @{thm apply_rspQ3''} - 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_thm 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 Quotient3_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 Lifting.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 code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = - let - val quot_thm = Quotient_Term.prove_quot_thm 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) ((code_eqn_thm_name, [add_abs_eqn_attrib]), [code_cert]) - end - else - lthy - end - -fun define_code_eq code_eqn_thm_name 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) ((code_eqn_thm_name, [Code.add_default_eqn_attrib]), [simp_code_eq]) - end - -fun define_code code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = - if body_type rty = body_type qty then - define_code_eq code_eqn_thm_name def_thm lthy - else - define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy - (* The ML-interface for a quotient definition takes as argument: @@ -193,7 +75,6 @@ val lhs_name = Binding.name_of (#1 var) val rsp_thm_name = qualify lhs_name "rsp" - val code_eqn_thm_name = qualify lhs_name "rep_eq" val lthy'' = lthy' |> Local_Theory.declaration {syntax = false, pervasive = true} @@ -205,8 +86,6 @@ |> (snd oo Local_Theory.note) ((rsp_thm_name, [Attrib.internal (K Quotient_Info.rsp_rules_add)]), [rsp_thm]) - |> define_code code_eqn_thm_name def_thm rsp_thm (rty, qty) - in (qconst_data, lthy'') end diff -r 70375fa2679d -r 2924f37cb6b3 src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Wed May 16 19:17:20 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Wed May 16 19:20:19 2012 +0200 @@ -6,8 +6,6 @@ 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 * bool)) * thm -> local_theory -> Quotient_Info.quotients * local_theory @@ -79,26 +77,6 @@ (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 Lifting.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 Quotient3_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 - open Lifting_Util infix 0 MRSL @@ -169,7 +147,6 @@ |> 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 |> setup_lifting_package gen_code quot_thm equiv_thm end