# HG changeset patch
# User kuncar
# Date 1368440004 -7200
# Node ID 04d9381bebffce715d8adeb02efb970b7194c179
# Parent  2e3f9e72b8c4021ab777fd1c4726e57a0369ddcc
try to detect assumptions of transfer rules that are in a shape of a transfer rule

diff -r 2e3f9e72b8c4 -r 04d9381bebff src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Tools/transfer.ML	Mon May 13 12:13:24 2013 +0200
@@ -111,10 +111,25 @@
   in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
 
 (* Conversion to preprocess a transfer rule *)
+fun strip_args n = funpow n (fst o dest_comb)
+
+fun safe_Rel_conv ct =
+  let
+    val head = ct |> term_of |> HOLogic.dest_Trueprop |> strip_args 2
+    fun is_known (Const (s, _)) = (s = @{const_name DOM})
+      | is_known _ = false
+  in
+    if not (is_known head)
+      then HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv)) ct
+    else Conv.all_conv ct
+  end
+  handle TERM _ => Conv.all_conv ct
+;
+
 fun prep_conv ct = (
-      Conv.implies_conv Conv.all_conv prep_conv
+      Conv.implies_conv safe_Rel_conv prep_conv
       else_conv
-      HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))
+      safe_Rel_conv
       else_conv
       Conv.all_conv) ct
 
diff -r 2e3f9e72b8c4 -r 04d9381bebff src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Transfer.thy	Mon May 13 12:13:24 2013 +0200
@@ -103,6 +103,10 @@
   shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
   using assms unfolding Rel_def fun_rel_def by fast
 
+text {* Handling of domains *}
+
+definition DOM :: "('a => 'b => bool) => ('a => bool) => bool" where "DOM T R \<equiv> Domainp T = R"
+
 ML_file "Tools/transfer.ML"
 setup Transfer.setup