# HG changeset patch
# User huffman
# Date 1334664009 -7200
# Node ID 1bf0e92c1ca07f864ebe7aca9d85a1e3d86a6d6f
# Parent  f74da4658bd1ea629f020d8451386baeafa3e4e7
make transfer method more deterministic by using SOLVED' on some subgoals

diff -r f74da4658bd1 -r 1bf0e92c1ca0 src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Tue Apr 17 20:48:07 2012 +0200
+++ b/src/HOL/Tools/transfer.ML	Tue Apr 17 14:00:09 2012 +0200
@@ -138,13 +138,16 @@
 fun transfer_tac ctxt = SUBGOAL (fn (t, i) =>
   let
     val bs = bnames t
+    val rules0 = @{thms Rel_App Rel_Abs}
     val rules = Data.get ctxt
   in
     EVERY
       [rewrite_goal_tac @{thms transfer_forall_eq transfer_implies_eq} i,
        CONVERSION (Trueprop_conv (fo_conv ctxt)) i,
        rtac @{thm transfer_start [rotated]} i,
-       REPEAT_ALL_NEW (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) (i + 1),
+       REPEAT_ALL_NEW (resolve_tac rules0 ORELSE' atac
+         ORELSE' SOLVED' (REPEAT_ALL_NEW (resolve_tac rules))
+         ORELSE' eq_tac ctxt) (i + 1),
        (* Alpha-rename bound variables in goal *)
        SUBGOAL (fn (u, i) =>
          rtac @{thm equal_elim_rule1} i THEN
@@ -156,7 +159,7 @@
 
 fun correspondence_tac ctxt i =
   let
-    val rules = Data.get ctxt
+    val rules = @{thms Rel_App Rel_Abs} @ Data.get ctxt
   in
     EVERY
       [CONVERSION (correspond_conv ctxt) i,
diff -r f74da4658bd1 -r 1bf0e92c1ca0 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Tue Apr 17 20:48:07 2012 +0200
+++ b/src/HOL/Transfer.thy	Tue Apr 17 14:00:09 2012 +0200
@@ -84,22 +84,22 @@
 lemma Rel_eq_refl: "Rel (op =) x x"
   unfolding Rel_def ..
 
+lemma Rel_App:
+  assumes "Rel (A ===> B) f g" and "Rel A x y"
+  shows "Rel B (App f x) (App g y)"
+  using assms unfolding Rel_def App_def fun_rel_def by fast
+
+lemma Rel_Abs:
+  assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
+  shows "Rel (A ===> B) (Abs (\<lambda>x. f x)) (Abs (\<lambda>y. g y))"
+  using assms unfolding Rel_def Abs_def fun_rel_def by fast
+
 use "Tools/transfer.ML"
 
 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)"
-  using assms unfolding Rel_def App_def fun_rel_def by fast
-
-lemma Rel_Abs [transfer_raw]:
-  assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
-  shows "Rel (A ===> B) (Abs (\<lambda>x. f x)) (Abs (\<lambda>y. g y))"
-  using assms unfolding Rel_def Abs_def fun_rel_def by fast
-
 hide_const (open) App Abs Rel