return also which code equation was used; tuned
authorkuncar
Fri Dec 05 14:14:36 2014 +0100 (2014-12-05)
changeset 60227eacf75e4da95
parent 60226 ec23f2a97ba4
child 60228 32dd7adba5a4
return also which code equation was used; tuned
src/HOL/Tools/Lifting/lifting_def.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Dec 05 14:14:36 2014 +0100
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Dec 05 14:14:36 2014 +0100
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  signature LIFTING_DEF =
     1.6  sig
     1.7 +  datatype code_eq = NONE_EQ | ABS_EQ | REP_EQ
     1.8    type lift_def
     1.9    val rty_of_lift_def: lift_def -> typ
    1.10    val qty_of_lift_def: lift_def -> typ
    1.11 @@ -15,6 +16,7 @@
    1.12    val rsp_thm_of_lift_def: lift_def -> thm
    1.13    val abs_eq_of_lift_def: lift_def -> thm
    1.14    val rep_eq_of_lift_def: lift_def -> thm option
    1.15 +  val code_eq_of_lift_def: lift_def -> code_eq
    1.16    val transfer_rules_of_lift_def: lift_def -> thm list
    1.17    val morph_lift_def: morphism -> lift_def -> lift_def
    1.18    val inst_of_lift_def: Proof.context -> typ -> lift_def -> lift_def
    1.19 @@ -29,7 +31,19 @@
    1.20    val add_lift_def: 
    1.21      config -> binding * mixfix -> typ -> term -> thm -> thm list -> local_theory -> 
    1.22        lift_def * local_theory
    1.23 -    
    1.24 +  
    1.25 +  val prepare_lift_def:
    1.26 +    (binding * mixfix -> typ -> term -> thm -> thm list -> Proof.context -> 
    1.27 +      lift_def * local_theory) -> 
    1.28 +    binding * mixfix -> typ -> term -> thm list -> local_theory -> 
    1.29 +    term option * (thm list list -> Proof.context -> lift_def * local_theory)
    1.30 +
    1.31 +  val gen_lift_def:
    1.32 +    (binding * mixfix -> typ -> term -> thm -> thm list -> local_theory -> 
    1.33 +      lift_def * local_theory) -> 
    1.34 +    binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list -> 
    1.35 +    local_theory -> lift_def * local_theory
    1.36 +
    1.37    val lift_def: 
    1.38      config -> binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list -> 
    1.39      local_theory -> lift_def * local_theory
    1.40 @@ -48,6 +62,8 @@
    1.41  
    1.42  infix 0 MRSL
    1.43  
    1.44 +datatype code_eq = NONE_EQ | ABS_EQ | REP_EQ
    1.45 +
    1.46  datatype lift_def = LIFT_DEF of {
    1.47    rty: typ,
    1.48    qty: typ,
    1.49 @@ -57,6 +73,7 @@
    1.50    rsp_thm: thm,
    1.51    abs_eq: thm,
    1.52    rep_eq: thm option,
    1.53 +  code_eq: code_eq,
    1.54    transfer_rules: thm list
    1.55  };
    1.56  
    1.57 @@ -69,21 +86,22 @@
    1.58  val rsp_thm_of_lift_def = #rsp_thm o rep_lift_def;
    1.59  val abs_eq_of_lift_def = #abs_eq o rep_lift_def;
    1.60  val rep_eq_of_lift_def = #rep_eq o rep_lift_def;
    1.61 +val code_eq_of_lift_def = #code_eq o rep_lift_def;
    1.62  val transfer_rules_of_lift_def = #transfer_rules o rep_lift_def;
    1.63  
    1.64 -fun mk_lift_def rty qty rhs lift_const def_thm rsp_thm abs_eq rep_eq transfer_rules =
    1.65 +fun mk_lift_def rty qty rhs lift_const def_thm rsp_thm abs_eq rep_eq code_eq transfer_rules =
    1.66    LIFT_DEF {rty = rty, qty = qty,
    1.67              rhs = rhs, lift_const = lift_const,
    1.68 -            def_thm = def_thm, rsp_thm = rsp_thm, abs_eq = abs_eq, rep_eq = rep_eq,
    1.69 -            transfer_rules = transfer_rules };
    1.70 +            def_thm = def_thm, rsp_thm = rsp_thm, abs_eq = abs_eq, rep_eq = rep_eq, 
    1.71 +            code_eq = code_eq, transfer_rules = transfer_rules };
    1.72  
    1.73 -fun map_lift_def f1 f2 f3 f4 f5 f6 f7 f8 f9
    1.74 +fun map_lift_def f1 f2 f3 f4 f5 f6 f7 f8 f9 f10
    1.75    (LIFT_DEF {rty = rty, qty = qty, rhs = rhs, lift_const = lift_const,
    1.76 -  def_thm = def_thm, rsp_thm = rsp_thm, abs_eq = abs_eq, rep_eq = rep_eq, 
    1.77 +  def_thm = def_thm, rsp_thm = rsp_thm, abs_eq = abs_eq, rep_eq = rep_eq, code_eq = code_eq,
    1.78    transfer_rules = transfer_rules }) =
    1.79    LIFT_DEF {rty = f1 rty, qty = f2 qty, rhs = f3 rhs, lift_const = f4 lift_const,
    1.80              def_thm = f5 def_thm, rsp_thm = f6 rsp_thm, abs_eq = f7 abs_eq, rep_eq = f8 rep_eq,
    1.81 -            transfer_rules = f9 transfer_rules }
    1.82 +            code_eq = f9 code_eq, transfer_rules = f10 transfer_rules }
    1.83  
    1.84  fun morph_lift_def phi =
    1.85    let
    1.86 @@ -91,7 +109,7 @@
    1.87      val mterm = Morphism.term phi
    1.88      val mthm = Morphism.thm phi
    1.89    in
    1.90 -    map_lift_def mtyp mtyp mterm mterm mthm mthm mthm (Option.map mthm) (map mthm)
    1.91 +    map_lift_def mtyp mtyp mterm mterm mthm mthm mthm (Option.map mthm) I (map mthm)
    1.92    end
    1.93  
    1.94  fun mk_inst_of_lift_def qty lift_def = Vartab.empty |> Type.raw_match (qty_of_lift_def lift_def, qty)
    1.95 @@ -438,55 +456,23 @@
    1.96  
    1.97    in
    1.98      if is_valid_eq abs_eq_thm then
    1.99 -      Code.add_default_eqn abs_eq_thm thy
   1.100 +      (ABS_EQ, Code.add_default_eqn abs_eq_thm thy)
   1.101      else
   1.102        let
   1.103          val (rty_body, qty_body) = get_body_types (rty, qty)
   1.104        in
   1.105          if rty_body = qty_body then
   1.106 -         Code.add_default_eqn (the opt_rep_eq_thm) thy
   1.107 +          (REP_EQ, Code.add_default_eqn (the opt_rep_eq_thm) thy)
   1.108          else
   1.109            if is_some opt_rep_eq_thm andalso is_valid_abs_eq (the opt_rep_eq_thm)
   1.110            then
   1.111 -            Code.add_abs_default_eqn (the opt_rep_eq_thm) thy
   1.112 +            (REP_EQ, Code.add_abs_default_eqn (the opt_rep_eq_thm) thy)
   1.113            else
   1.114 -            thy
   1.115 +            (NONE_EQ, thy)
   1.116        end
   1.117    end
   1.118  
   1.119  local
   1.120 -  fun encode_code_eq ctxt abs_eq opt_rep_eq (rty, qty) = 
   1.121 -    let
   1.122 -      fun mk_type typ = typ |> Logic.mk_type |> Thm.cterm_of ctxt |> Drule.mk_term
   1.123 -    in
   1.124 -      Conjunction.intr_balanced [abs_eq, (the_default TrueI opt_rep_eq), mk_type rty, mk_type qty]
   1.125 -    end
   1.126 -  
   1.127 -  exception DECODE
   1.128 -    
   1.129 -  fun decode_code_eq thm =
   1.130 -    if Thm.nprems_of thm > 0 then raise DECODE 
   1.131 -    else
   1.132 -      let
   1.133 -        val [abs_eq, rep_eq, rty, qty] = Conjunction.elim_balanced 4 thm
   1.134 -        val opt_rep_eq = if Thm.eq_thm_prop (rep_eq, TrueI) then NONE else SOME rep_eq
   1.135 -        fun dest_type typ = typ |> Drule.dest_term |> Thm.term_of |> Logic.dest_type
   1.136 -      in
   1.137 -        (abs_eq, opt_rep_eq, (dest_type rty, dest_type qty)) 
   1.138 -      end
   1.139 -  
   1.140 -  fun register_encoded_code_eq thm thy =
   1.141 -    let
   1.142 -      val (abs_eq_thm, opt_rep_eq_thm, (rty, qty)) = decode_code_eq thm
   1.143 -    in
   1.144 -      register_code_eq_thy abs_eq_thm opt_rep_eq_thm (rty, qty) thy
   1.145 -    end
   1.146 -    handle DECODE => thy
   1.147 -  
   1.148 -  val register_code_eq_attribute = Thm.declaration_attribute
   1.149 -    (fn thm => Context.mapping (register_encoded_code_eq thm) I)
   1.150 -  val register_code_eq_attrib = Attrib.internal (K register_code_eq_attribute)
   1.151 -
   1.152    fun no_no_code ctxt (rty, qty) =
   1.153      if same_type_constrs (rty, qty) then
   1.154        forall (no_no_code ctxt) (Targs rty ~~ Targs qty)
   1.155 @@ -506,12 +492,15 @@
   1.156  
   1.157  fun register_code_eq abs_eq_thm opt_rep_eq_thm (rty, qty) lthy =
   1.158    let
   1.159 -    val encoded_code_eq = encode_code_eq lthy abs_eq_thm opt_rep_eq_thm (rty, qty)
   1.160 +    val mthm = Morphism.thm (Local_Theory.target_morphism lthy)
   1.161 +    val abs_eq_thm =  mthm abs_eq_thm
   1.162 +    val opt_rep_eq_thm = Option.map mthm opt_rep_eq_thm
   1.163    in
   1.164      if no_no_code lthy (rty, qty) then 
   1.165 -      (snd oo Local_Theory.note) ((Binding.empty, [register_code_eq_attrib]), [encoded_code_eq]) lthy
   1.166 +      Local_Theory.background_theory_result 
   1.167 +        (register_code_eq_thy abs_eq_thm opt_rep_eq_thm (rty, qty)) lthy
   1.168      else
   1.169 -      lthy
   1.170 +      (NONE_EQ, lthy)
   1.171    end
   1.172  end
   1.173              
   1.174 @@ -568,12 +557,12 @@
   1.175          else map_filter (fn (_, attrs, thms) => if null attrs then NONE 
   1.176            else SOME ((Binding.empty, []), [(thms, attrs)])) notes
   1.177        end
   1.178 +    val (code_eq, lthy) = register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty) lthy
   1.179      val lift_def = mk_lift_def rty_forced qty newrhs lift_const def_thm rsp_thm abs_eq_thm 
   1.180 -          opt_rep_eq_thm transfer_rules
   1.181 +          opt_rep_eq_thm code_eq transfer_rules
   1.182    in
   1.183      lthy
   1.184        |> Local_Theory.notes (notes (#notes config)) |> snd
   1.185 -      |> register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty)
   1.186        |> ` (fn lthy => morph_lift_def (Local_Theory.target_morphism lthy) lift_def)
   1.187        ||> Local_Theory.restore
   1.188    end
   1.189 @@ -697,7 +686,7 @@
   1.190      Symtab.fold (fn (_, data) => fn l => collect data l) table []
   1.191    end
   1.192  
   1.193 -fun prepare_lift_def config var qty rhs par_thms lthy =
   1.194 +fun prepare_lift_def add_lift_def var qty rhs par_thms lthy =
   1.195    let
   1.196      val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty)
   1.197      val rty_forced = (domain_type o fastype_of) rsp_rel;
   1.198 @@ -714,7 +703,7 @@
   1.199      val opt_proven_rsp_thm = try_prove_reflexivity lthy prsp_tm
   1.200      
   1.201      fun after_qed internal_rsp_thm lthy = 
   1.202 -      add_lift_def config var qty rhs (internal_rsp_thm RS to_rsp) par_thms lthy
   1.203 +      add_lift_def var qty rhs (internal_rsp_thm RS to_rsp) par_thms lthy
   1.204    in
   1.205      case opt_proven_rsp_thm of
   1.206        SOME thm => (NONE, K (after_qed thm))
   1.207 @@ -737,9 +726,9 @@
   1.208          end 
   1.209    end
   1.210  
   1.211 -fun lift_def config var qty rhs tac par_thms lthy =
   1.212 +fun gen_lift_def add_lift_def var qty rhs tac par_thms lthy =
   1.213    let
   1.214 -    val (goal, after_qed) = prepare_lift_def config var qty rhs par_thms lthy
   1.215 +    val (goal, after_qed) = prepare_lift_def add_lift_def var qty rhs par_thms lthy
   1.216    in
   1.217      case goal of
   1.218        SOME goal => 
   1.219 @@ -752,6 +741,9 @@
   1.220        | NONE => after_qed [[Drule.dummy_thm]] lthy
   1.221    end
   1.222  
   1.223 +fun lift_def config var qty rhs tac par_thms lthy = gen_lift_def (add_lift_def config)
   1.224 +  var qty rhs tac par_thms lthy
   1.225 +
   1.226  (*
   1.227  
   1.228    lifting_definition command. It opens a proof of a corresponding respectfulness 
   1.229 @@ -765,7 +757,7 @@
   1.230      val var = (binding, mx)
   1.231      val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw
   1.232      val par_thms = Attrib.eval_thms lthy par_xthms
   1.233 -    val (goal, after_qed) = prepare_lift_def default_config var qty rhs par_thms lthy
   1.234 +    val (goal, after_qed) = prepare_lift_def (add_lift_def default_config) var qty rhs par_thms lthy
   1.235    in
   1.236      Proof.theorem NONE (snd oo after_qed) [map (rpair []) (the_list goal)] lthy
   1.237    end