# HG changeset patch
# User kuncar
# Date 1416323991 -3600
# Node ID ef4f0b5b925e1d4e52c11a47fb9603300c0d6020
# Parent  5fb4990dfc736da4b7c73ffb3f9b2be42dfecedc
added pred_def, rel_eq_onp tuned

diff -r 5fb4990dfc73 -r ef4f0b5b925e src/HOL/Tools/Lifting/lifting_bnf.ML
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Sun May 03 00:01:10 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Tue Nov 18 16:19:51 2014 +0100
@@ -87,9 +87,8 @@
 
 fun relator_eq_onp bnf ctxt =
   let
-    val relator_eq_onp_thm = lookup_defined_pred_data ctxt (type_name_of_bnf bnf)
-      |> Transfer.rel_eq_onp |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv 
-          (Raw_Simplifier.rewrite ctxt false @{thms eq_onp_top_eq_eq[THEN eq_reflection]})))
+    val relator_eq_onp_thm = lookup_defined_pred_data ctxt (type_name_of_bnf bnf) 
+      |> Transfer.rel_eq_onp
   in
     [((Binding.empty, []), [([relator_eq_onp_thm], @{attributes [relator_eq_onp]})])]    
   end
diff -r 5fb4990dfc73 -r ef4f0b5b925e src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Sun May 03 00:01:10 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Tue Nov 18 16:19:51 2014 +0100
@@ -9,9 +9,12 @@
 sig
   type pred_data
   val rel_eq_onp: pred_data -> thm
+  val rel_eq_onp_with_tops: pred_data -> thm
+  val pred_def: pred_data -> thm
 
   val bottom_rewr_conv: thm list -> conv
   val top_rewr_conv: thm list -> conv
+  val top_sweep_rewr_conv: thm list -> conv
 
   val prep_conv: conv
   val get_transfer_raw: Proof.context -> thm list
@@ -46,15 +49,23 @@
 structure Transfer : TRANSFER =
 struct
 
+fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
+fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
+fun top_sweep_rewr_conv rewrs = Conv.top_sweep_conv (K (Conv.rewrs_conv rewrs)) @{context}
+
 (** Theory Data **)
 
 val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o apply2 snd) (single o fst);
 val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq
   o HOLogic.dest_Trueprop o Thm.concl_of);
 
-type pred_data = {rel_eq_onp: thm}
+type pred_data = {pred_def:thm, rel_eq_onp: thm}
 
 val rel_eq_onp: pred_data -> thm = #rel_eq_onp
+val rel_eq_onp_with_tops: pred_data -> thm = (Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
+  (top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))))
+  o #rel_eq_onp
+val pred_def: pred_data -> thm = #pred_def
 
 structure Data = Generic_Data
 (
@@ -182,9 +193,6 @@
 
 (** Conversions **)
 
-fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
-fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
-
 fun transfer_rel_conv conv =
   Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv)))
 
@@ -788,7 +796,9 @@
 val untransferred_attribute_parser =
   Attrib.thms >> untransferred_attribute
 
-fun morph_pred_data phi {rel_eq_onp} = {rel_eq_onp = Morphism.thm phi rel_eq_onp}
+fun morph_pred_data phi {pred_def, rel_eq_onp} = 
+  {pred_def =  Morphism.thm phi pred_def,
+  rel_eq_onp = Morphism.thm phi rel_eq_onp}
 
 fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name
   |> Option.map (morph_pred_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
diff -r 5fb4990dfc73 -r ef4f0b5b925e src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Sun May 03 00:01:10 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Nov 18 16:19:51 2014 +0100
@@ -283,10 +283,7 @@
     fun qualify defname suffix = Binding.qualified true suffix defname
     val Domainp_rel_thm_name = qualify (base_name_of_bnf bnf) "Domainp_rel"
     val rel_eq_onp_thm_name = qualify (base_name_of_bnf bnf) "rel_eq_onp"
-    val rel_eq_onp_internal = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
-      (Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
-        rel_eq_onp
-    val pred_data = {rel_eq_onp = rel_eq_onp_internal}
+    val pred_data = {pred_def = pred_def, rel_eq_onp = rel_eq_onp}
     val type_name = type_name_of_bnf bnf
     val relator_domain_attr = @{attributes [relator_domain]}
     val notes = [((Domainp_rel_thm_name, []), [([Domainp_rel], relator_domain_attr)]),
@@ -340,7 +337,7 @@
         map type_name_of_bnf (#fp_nesting_bnfs fp_sugar)
       @ map type_name_of_bnf (#live_nesting_bnfs fp_sugar)
       @ map type_name_of_bnf (#bnfs (#fp_res fp_sugar)))
-    val eq_onps = map (Transfer.rel_eq_onp o lookup_defined_pred_data lthy) involved_types
+    val eq_onps = map (Transfer.rel_eq_onp_with_tops o lookup_defined_pred_data lthy) involved_types
     val old_lthy = lthy
     val (As, lthy) = mk_TFrees' (map Type.sort_of_atyp (lives_of_fp fp_sugar)) lthy
     val predTs = map mk_pred1T As