lift_definition: return the result of lifting
authorkuncar
Tue Nov 18 16:19:57 2014 +0100 (2014-11-18)
changeset 602192bce9a690b1e
parent 60218 7e24e172052e
child 60220 530112e8c6ba
lift_definition: return the result of lifting
src/HOL/Tools/Lifting/lifting_def.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Nov 18 16:19:57 2014 +0100
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Nov 18 16:19:57 2014 +0100
     1.3 @@ -6,15 +6,26 @@
     1.4  
     1.5  signature LIFTING_DEF =
     1.6  sig
     1.7 +  type lift_def
     1.8 +  val rty_of_lift_def: lift_def -> typ
     1.9 +  val qty_of_lift_def: lift_def -> typ
    1.10 +  val rhs_of_lift_def: lift_def -> term
    1.11 +  val lift_const_of_lift_def: lift_def -> term
    1.12 +  val def_thm_of_lift_def: lift_def -> thm
    1.13 +  val rsp_thm_of_lift_def: lift_def -> thm
    1.14 +  val abs_eq_of_lift_def: lift_def -> thm
    1.15 +  val rep_eq_of_lift_def: lift_def -> thm option
    1.16 +  val transfer_rules_of_lift_def: lift_def -> thm list
    1.17 +
    1.18    val generate_parametric_transfer_rule:
    1.19      Proof.context -> thm -> thm -> thm
    1.20  
    1.21    val add_lift_def:
    1.22 -    binding * mixfix -> typ -> term -> thm -> thm list -> local_theory -> local_theory
    1.23 +    binding * mixfix -> typ -> term -> thm -> thm list -> local_theory -> lift_def * local_theory
    1.24      
    1.25    val lift_def: 
    1.26      binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list -> 
    1.27 -    local_theory -> local_theory
    1.28 +    local_theory -> lift_def * local_theory
    1.29  
    1.30    val lift_def_cmd:
    1.31      (binding * string option * mixfix) * string * (Facts.ref * Token.src list) list ->
    1.32 @@ -30,6 +41,35 @@
    1.33  
    1.34  infix 0 MRSL
    1.35  
    1.36 +datatype lift_def = LIFT_DEF of {
    1.37 +  rty: typ,
    1.38 +  qty: typ,
    1.39 +  rhs: term,
    1.40 +  lift_const: term,
    1.41 +  def_thm: thm,
    1.42 +  rsp_thm: thm,
    1.43 +  abs_eq: thm,
    1.44 +  rep_eq: thm option,
    1.45 +  transfer_rules: thm list
    1.46 +};
    1.47 +
    1.48 +fun rep_lift_def (LIFT_DEF lift_def) = lift_def;
    1.49 +val rty_of_lift_def = #rty o rep_lift_def;
    1.50 +val qty_of_lift_def = #qty o rep_lift_def;
    1.51 +val rhs_of_lift_def = #rhs o rep_lift_def;
    1.52 +val lift_const_of_lift_def = #lift_const o rep_lift_def;
    1.53 +val def_thm_of_lift_def = #def_thm o rep_lift_def;
    1.54 +val rsp_thm_of_lift_def = #rsp_thm o rep_lift_def;
    1.55 +val abs_eq_of_lift_def = #abs_eq o rep_lift_def;
    1.56 +val rep_eq_of_lift_def = #rep_eq o rep_lift_def;
    1.57 +val transfer_rules_of_lift_def = #transfer_rules o rep_lift_def;
    1.58 +
    1.59 +fun mk_lift_def rty qty rhs lift_const def_thm rsp_thm abs_eq rep_eq transfer_rules =
    1.60 +  LIFT_DEF {rty = rty, qty = qty,
    1.61 +            rhs = rhs, lift_const = lift_const,
    1.62 +            def_thm = def_thm, rsp_thm = rsp_thm, abs_eq = abs_eq, rep_eq = rep_eq,
    1.63 +            transfer_rules = transfer_rules };
    1.64 +
    1.65  (* Reflexivity prover *)
    1.66  
    1.67  fun mono_eq_prover ctxt prop =
    1.68 @@ -462,7 +502,7 @@
    1.69      val (_, prop') = Local_Defs.cert_def lthy prop
    1.70      val (_, newrhs) = Local_Defs.abs_def prop'
    1.71  
    1.72 -    val ((_, (_ , def_thm)), lthy') = 
    1.73 +    val ((lift_const, (_ , def_thm)), lthy') = 
    1.74        Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
    1.75  
    1.76      val transfer_rules = generate_transfer_rules lthy' quot_thm rsp_thm def_thm par_thms
    1.77 @@ -478,6 +518,8 @@
    1.78      val rep_eq_thm_name = qualify lhs_name "rep_eq"
    1.79      val transfer_rule_name = qualify lhs_name "transfer"
    1.80      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
    1.81 +    val lift_def = mk_lift_def rty_forced qty newrhs lift_const def_thm rsp_thm abs_eq_thm 
    1.82 +      opt_rep_eq_thm transfer_rules 
    1.83    in
    1.84      lthy'
    1.85        |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
    1.86 @@ -487,6 +529,7 @@
    1.87              SOME rep_eq_thm => (snd oo Local_Theory.note) ((rep_eq_thm_name, []), [rep_eq_thm])
    1.88              | NONE => I)
    1.89        |> register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty)
    1.90 +      |> pair lift_def
    1.91    end
    1.92  
    1.93  local
    1.94 @@ -674,7 +717,7 @@
    1.95      val par_thms = Attrib.eval_thms lthy par_xthms
    1.96      val (goal, after_qed) = prepare_lift_def var qty rhs par_thms lthy
    1.97    in
    1.98 -    Proof.theorem NONE after_qed [map (rpair []) (the_list goal)] lthy
    1.99 +    Proof.theorem NONE (snd oo after_qed) [map (rpair []) (the_list goal)] lthy
   1.100    end
   1.101  
   1.102  fun quot_thm_err ctxt (rty, qty) pretty_msg =