src/HOL/Tools/Lifting/lifting_def.ML
changeset 47351 0193e663a19e
parent 47308 9caab698dbe4
child 47361 87c0eaf04bad
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 04 13:41:38 2012 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 04 13:42:01 2012 +0200
     1.3 @@ -165,7 +165,8 @@
     1.4  fun add_lift_def var qty rhs rsp_thm lthy =
     1.5    let
     1.6      val rty = fastype_of rhs
     1.7 -    val absrep_trm =  Lifting_Term.absrep_fun lthy (rty, qty)
     1.8 +    val quotient_thm = Lifting_Term.prove_quot_theorem lthy (rty, qty)
     1.9 +    val absrep_trm =  Lifting_Term.quot_thm_abs quotient_thm
    1.10      val rty_forced = (domain_type o fastype_of) absrep_trm
    1.11      val forced_rhs = force_rty_type lthy rty_forced rhs
    1.12      val lhs = Free (Binding.print (#1 var), qty)
    1.13 @@ -176,15 +177,19 @@
    1.14      val ((_, (_ , def_thm)), lthy') = 
    1.15        Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
    1.16  
    1.17 +    val transfer_thm = def_thm RS (rsp_thm RS (quotient_thm RS @{thm Quotient_to_transfer}))
    1.18 +
    1.19      fun qualify defname suffix = Binding.name suffix
    1.20        |> Binding.qualify true defname
    1.21  
    1.22      val lhs_name = Binding.name_of (#1 var)
    1.23      val rsp_thm_name = qualify lhs_name "rsp"
    1.24      val code_eqn_thm_name = qualify lhs_name "rep_eq"
    1.25 +    val transfer_thm_name = qualify lhs_name "transfer"
    1.26    in
    1.27      lthy'
    1.28        |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
    1.29 +      |> (snd oo Local_Theory.note) ((transfer_thm_name, []), [transfer_thm])
    1.30        |> define_code code_eqn_thm_name def_thm rsp_thm (rty_forced, qty)
    1.31    end
    1.32