# HG changeset patch
# User huffman
# Date 1334653388 -7200
# Node ID cb44d09d9d22748f2f87c51506855e0361dfb78b
# Parent  4c949049cd78b08609d812a223eb8e6216a83f90
add theory data for relator identity rules;
preprocess transfer rules generated by lift_definition using relator rules

diff -r 4c949049cd78 -r cb44d09d9d22 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Apr 17 09:12:15 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Apr 17 11:03:08 2012 +0200
@@ -183,6 +183,7 @@
       Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
 
     val transfer_thm = [quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}
+        |> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy')
 
     fun qualify defname suffix = Binding.name suffix
       |> Binding.qualify true defname
diff -r 4c949049cd78 -r cb44d09d9d22 src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Tue Apr 17 09:12:15 2012 +0200
+++ b/src/HOL/Tools/transfer.ML	Tue Apr 17 11:03:08 2012 +0200
@@ -8,6 +8,7 @@
 sig
   val fo_conv: Proof.context -> conv
   val prep_conv: conv
+  val get_relator_eq: Proof.context -> thm list
   val transfer_add: attribute
   val transfer_del: attribute
   val transfer_tac: Proof.context -> int -> tactic
@@ -24,6 +25,15 @@
   val description = "raw correspondence rule for transfer method"
 )
 
+structure Relator_Eq = Named_Thms
+(
+  val name = @{binding relator_eq}
+  val description = "relator equality rule (used by transfer method)"
+)
+
+fun get_relator_eq ctxt =
+  map (Thm.symmetric o mk_meta_eq) (Relator_Eq.get ctxt)
+
 (** Conversions **)
 
 val App_rule = Thm.symmetric @{thm App_def}
@@ -106,7 +116,7 @@
   let
     val T = RelT (HOLogic.dest_Trueprop (Logic.strip_assums_concl t))
     val cT = ctyp_of (Proof_Context.theory_of ctxt) T
-    val rews = [@{thm fun_rel_eq [symmetric, THEN eq_reflection]}]
+    val rews = get_relator_eq ctxt
     val thm1 = Drule.instantiate' [SOME cT] [] @{thm Rel_eq_refl}
     val thm2 = Raw_Simplifier.rewrite_rule rews thm1
   in
@@ -177,6 +187,7 @@
 
 val setup =
   Data.setup
+  #> Relator_Eq.setup
   #> Attrib.setup @{binding transfer_rule} transfer_attribute
      "correspondence rule for transfer method"
   #> Method.setup @{binding transfer} transfer_method
diff -r 4c949049cd78 -r cb44d09d9d22 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Tue Apr 17 09:12:15 2012 +0200
+++ b/src/HOL/Transfer.thy	Tue Apr 17 11:03:08 2012 +0200
@@ -88,6 +88,8 @@
 
 setup Transfer.setup
 
+declare fun_rel_eq [relator_eq]
+
 lemma Rel_App [transfer_raw]:
   assumes "Rel (A ===> B) f g" and "Rel A x y"
   shows "Rel B (App f x) (App g y)"