remove the generation of a code certificate from the Quotient package (mainly from quotient_def), because it's in lift_definition now
authorkuncar
Wed May 16 19:20:19 2012 +0200 (2012-05-16)
changeset 479382924f37cb6b3
parent 47937 70375fa2679d
child 47939 9ff976a6c2cb
remove the generation of a code certificate from the Quotient package (mainly from quotient_def), because it's in lift_definition now
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_type.ML
     1.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Wed May 16 19:17:20 2012 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Wed May 16 19:20:19 2012 +0200
     1.3 @@ -31,124 +31,6 @@
     1.4  
     1.5  infix 0 MRSL
     1.6  
     1.7 -fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
     1.8 -  | get_body_types (U, V)  = (U, V)
     1.9 -
    1.10 -fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
    1.11 -  | get_binder_types _ = []
    1.12 -
    1.13 -fun unabs_def ctxt def = 
    1.14 -  let
    1.15 -    val (_, rhs) = Thm.dest_equals (cprop_of def)
    1.16 -    fun dest_abs (Abs (var_name, T, _)) = (var_name, T)
    1.17 -      | dest_abs tm = raise TERM("get_abs_var",[tm])
    1.18 -    val (var_name, T) = dest_abs (term_of rhs)
    1.19 -    val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt
    1.20 -    val thy = Proof_Context.theory_of ctxt'
    1.21 -    val refl_thm = Thm.reflexive (cterm_of thy (Free (hd new_var_names, T)))
    1.22 -  in
    1.23 -    Thm.combination def refl_thm |>
    1.24 -    singleton (Proof_Context.export ctxt' ctxt)
    1.25 -  end
    1.26 -
    1.27 -fun unabs_all_def ctxt def = 
    1.28 -  let
    1.29 -    val (_, rhs) = Thm.dest_equals (cprop_of def)
    1.30 -    val xs = strip_abs_vars (term_of rhs)
    1.31 -  in  
    1.32 -    fold (K (unabs_def ctxt)) xs def
    1.33 -  end
    1.34 -
    1.35 -val map_fun_unfolded = 
    1.36 -  @{thm map_fun_def[abs_def]} |>
    1.37 -  unabs_def @{context} |>
    1.38 -  unabs_def @{context} |>
    1.39 -  Local_Defs.unfold @{context} [@{thm comp_def}]
    1.40 -
    1.41 -fun unfold_fun_maps ctm =
    1.42 -  let
    1.43 -    fun unfold_conv ctm =
    1.44 -      case (Thm.term_of ctm) of
    1.45 -        Const (@{const_name "map_fun"}, _) $ _ $ _ => 
    1.46 -          (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
    1.47 -        | _ => Conv.all_conv ctm
    1.48 -    val try_beta_conv = Conv.try_conv (Thm.beta_conversion false)
    1.49 -  in
    1.50 -    (Conv.arg_conv (Conv.fun_conv unfold_conv then_conv try_beta_conv)) ctm
    1.51 -  end
    1.52 -
    1.53 -fun prove_rel ctxt rsp_thm (rty, qty) =
    1.54 -  let
    1.55 -    val ty_args = get_binder_types (rty, qty)
    1.56 -    fun disch_arg args_ty thm = 
    1.57 -      let
    1.58 -        val quot_thm = Quotient_Term.prove_quot_thm ctxt args_ty
    1.59 -      in
    1.60 -        [quot_thm, thm] MRSL @{thm apply_rspQ3''}
    1.61 -      end
    1.62 -  in
    1.63 -    fold disch_arg ty_args rsp_thm
    1.64 -  end
    1.65 -
    1.66 -exception CODE_CERT_GEN of string
    1.67 -
    1.68 -fun simplify_code_eq ctxt def_thm = 
    1.69 -  Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm
    1.70 -
    1.71 -fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) =
    1.72 -  let
    1.73 -    val quot_thm = Quotient_Term.prove_quot_thm ctxt (get_body_types (rty, qty))
    1.74 -    val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
    1.75 -    val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient3_rep_abs}
    1.76 -    val abs_rep_eq = 
    1.77 -      case (HOLogic.dest_Trueprop o prop_of) fun_rel of
    1.78 -        Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm
    1.79 -        | Const (@{const_name Lifting.invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
    1.80 -        | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
    1.81 -    val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
    1.82 -    val unabs_def = unabs_all_def ctxt unfolded_def
    1.83 -    val rep = (snd o Thm.dest_comb o snd o Thm.dest_comb o cprop_of) quot_thm
    1.84 -    val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
    1.85 -    val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
    1.86 -    val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans}
    1.87 -  in
    1.88 -    simplify_code_eq ctxt code_cert
    1.89 -  end
    1.90 -
    1.91 -fun define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = 
    1.92 -  let
    1.93 -    val quot_thm = Quotient_Term.prove_quot_thm lthy (get_body_types (rty, qty))
    1.94 -  in
    1.95 -    if Quotient_Type.can_generate_code_cert quot_thm then
    1.96 -      let
    1.97 -        val code_cert = generate_code_cert lthy def_thm rsp_thm (rty, qty)
    1.98 -        val add_abs_eqn_attribute = 
    1.99 -          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I)
   1.100 -        val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
   1.101 -      in
   1.102 -        lthy
   1.103 -          |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [add_abs_eqn_attrib]), [code_cert])
   1.104 -      end
   1.105 -    else
   1.106 -      lthy
   1.107 -  end
   1.108 -
   1.109 -fun define_code_eq code_eqn_thm_name def_thm lthy =
   1.110 -  let
   1.111 -    val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
   1.112 -    val code_eq = unabs_all_def lthy unfolded_def
   1.113 -    val simp_code_eq = simplify_code_eq lthy code_eq
   1.114 -  in
   1.115 -    lthy
   1.116 -      |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [Code.add_default_eqn_attrib]), [simp_code_eq])
   1.117 -  end
   1.118 -
   1.119 -fun define_code code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy =
   1.120 -  if body_type rty = body_type qty then 
   1.121 -    define_code_eq code_eqn_thm_name def_thm lthy
   1.122 -  else 
   1.123 -    define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy
   1.124 -
   1.125  (* The ML-interface for a quotient definition takes
   1.126     as argument:
   1.127  
   1.128 @@ -193,7 +75,6 @@
   1.129  
   1.130      val lhs_name = Binding.name_of (#1 var)
   1.131      val rsp_thm_name = qualify lhs_name "rsp"
   1.132 -    val code_eqn_thm_name = qualify lhs_name "rep_eq"
   1.133      
   1.134      val lthy'' = lthy'
   1.135        |> Local_Theory.declaration {syntax = false, pervasive = true}
   1.136 @@ -205,8 +86,6 @@
   1.137        |> (snd oo Local_Theory.note) 
   1.138          ((rsp_thm_name, [Attrib.internal (K Quotient_Info.rsp_rules_add)]),
   1.139          [rsp_thm])
   1.140 -      |> define_code code_eqn_thm_name def_thm rsp_thm (rty, qty)
   1.141 -
   1.142    in
   1.143      (qconst_data, lthy'')
   1.144    end
     2.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Wed May 16 19:17:20 2012 +0200
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Wed May 16 19:20:19 2012 +0200
     2.3 @@ -6,8 +6,6 @@
     2.4  
     2.5  signature QUOTIENT_TYPE =
     2.6  sig
     2.7 -  val can_generate_code_cert: thm -> bool
     2.8 -  
     2.9    val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
    2.10      ((binding * binding) option * bool)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
    2.11  
    2.12 @@ -79,26 +77,6 @@
    2.13        (K (typedef_quot_type_tac equiv_thm typedef_info))
    2.14    end
    2.15     
    2.16 -fun can_generate_code_cert quot_thm  =
    2.17 -   case Quotient_Term.get_rel_from_quot_thm quot_thm of
    2.18 -      Const (@{const_name HOL.eq}, _) => true
    2.19 -      | Const (@{const_name Lifting.invariant}, _) $ _  => true
    2.20 -      | _ => false
    2.21 -
    2.22 -fun define_abs_type quot_thm lthy =
    2.23 -  if can_generate_code_cert quot_thm then
    2.24 -    let
    2.25 -      val abs_type_thm = quot_thm RS @{thm Quotient3_abs_rep}
    2.26 -      val add_abstype_attribute = 
    2.27 -          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
    2.28 -        val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
    2.29 -    in
    2.30 -      lthy
    2.31 -        |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
    2.32 -    end
    2.33 -  else
    2.34 -    lthy
    2.35 -
    2.36  open Lifting_Util
    2.37  
    2.38  infix 0 MRSL
    2.39 @@ -169,7 +147,6 @@
    2.40        |> Local_Theory.declaration {syntax = false, pervasive = true}
    2.41          (fn phi => Quotient_Info.update_quotients qty_full_name (quot_info phi)
    2.42            #> Quotient_Info.update_abs_rep qty_full_name (abs_rep_info phi))
    2.43 -      |> define_abs_type quot_thm
    2.44        |> setup_lifting_package gen_code quot_thm equiv_thm
    2.45    end
    2.46