# HG changeset patch
# User huffman
# Date 1333539721 -7200
# Node ID 0193e663a19e3891895132257cf70eb22267b1f6
# Parent  ec46b60aa582c373374c1d76652a83cea37f3f23
lift_definition command generates transfer rule

diff -r ec46b60aa582 -r 0193e663a19e src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Wed Apr 04 13:41:38 2012 +0200
+++ b/src/HOL/Lifting.thy	Wed Apr 04 13:42:01 2012 +0200
@@ -273,6 +273,11 @@
   show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
 qed
 
+lemma Quotient_to_transfer:
+  assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
+  shows "T c c'"
+  using assms by (auto dest: Quotient_cr_rel)
+
 subsection {* ML setup *}
 
 text {* Auxiliary data for the lifting package *}
diff -r ec46b60aa582 -r 0193e663a19e src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 04 13:41:38 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Apr 04 13:42:01 2012 +0200
@@ -165,7 +165,8 @@
 fun add_lift_def var qty rhs rsp_thm lthy =
   let
     val rty = fastype_of rhs
-    val absrep_trm =  Lifting_Term.absrep_fun lthy (rty, qty)
+    val quotient_thm = Lifting_Term.prove_quot_theorem lthy (rty, qty)
+    val absrep_trm =  Lifting_Term.quot_thm_abs quotient_thm
     val rty_forced = (domain_type o fastype_of) absrep_trm
     val forced_rhs = force_rty_type lthy rty_forced rhs
     val lhs = Free (Binding.print (#1 var), qty)
@@ -176,15 +177,19 @@
     val ((_, (_ , def_thm)), lthy') = 
       Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
 
+    val transfer_thm = def_thm RS (rsp_thm RS (quotient_thm RS @{thm Quotient_to_transfer}))
+
     fun qualify defname suffix = Binding.name suffix
       |> Binding.qualify true defname
 
     val lhs_name = Binding.name_of (#1 var)
     val rsp_thm_name = qualify lhs_name "rsp"
     val code_eqn_thm_name = qualify lhs_name "rep_eq"
+    val transfer_thm_name = qualify lhs_name "transfer"
   in
     lthy'
       |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
+      |> (snd oo Local_Theory.note) ((transfer_thm_name, []), [transfer_thm])
       |> define_code code_eqn_thm_name def_thm rsp_thm (rty_forced, qty)
   end