lift_definition command generates transfer rule
authorhuffman
Wed Apr 04 13:42:01 2012 +0200 (2012-04-04)
changeset 473510193e663a19e
parent 47350 ec46b60aa582
child 47352 e0bff2ae939f
lift_definition command generates transfer rule
src/HOL/Lifting.thy
src/HOL/Tools/Lifting/lifting_def.ML
     1.1 --- a/src/HOL/Lifting.thy	Wed Apr 04 13:41:38 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Wed Apr 04 13:42:01 2012 +0200
     1.3 @@ -273,6 +273,11 @@
     1.4    show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
     1.5  qed
     1.6  
     1.7 +lemma Quotient_to_transfer:
     1.8 +  assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
     1.9 +  shows "T c c'"
    1.10 +  using assms by (auto dest: Quotient_cr_rel)
    1.11 +
    1.12  subsection {* ML setup *}
    1.13  
    1.14  text {* Auxiliary data for the lifting package *}
     2.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 04 13:41:38 2012 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 04 13:42:01 2012 +0200
     2.3 @@ -165,7 +165,8 @@
     2.4  fun add_lift_def var qty rhs rsp_thm lthy =
     2.5    let
     2.6      val rty = fastype_of rhs
     2.7 -    val absrep_trm =  Lifting_Term.absrep_fun lthy (rty, qty)
     2.8 +    val quotient_thm = Lifting_Term.prove_quot_theorem lthy (rty, qty)
     2.9 +    val absrep_trm =  Lifting_Term.quot_thm_abs quotient_thm
    2.10      val rty_forced = (domain_type o fastype_of) absrep_trm
    2.11      val forced_rhs = force_rty_type lthy rty_forced rhs
    2.12      val lhs = Free (Binding.print (#1 var), qty)
    2.13 @@ -176,15 +177,19 @@
    2.14      val ((_, (_ , def_thm)), lthy') = 
    2.15        Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
    2.16  
    2.17 +    val transfer_thm = def_thm RS (rsp_thm RS (quotient_thm RS @{thm Quotient_to_transfer}))
    2.18 +
    2.19      fun qualify defname suffix = Binding.name suffix
    2.20        |> Binding.qualify true defname
    2.21  
    2.22      val lhs_name = Binding.name_of (#1 var)
    2.23      val rsp_thm_name = qualify lhs_name "rsp"
    2.24      val code_eqn_thm_name = qualify lhs_name "rep_eq"
    2.25 +    val transfer_thm_name = qualify lhs_name "transfer"
    2.26    in
    2.27      lthy'
    2.28        |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
    2.29 +      |> (snd oo Local_Theory.note) ((transfer_thm_name, []), [transfer_thm])
    2.30        |> define_code code_eqn_thm_name def_thm rsp_thm (rty_forced, qty)
    2.31    end
    2.32