1.1 --- a/src/HOL/Tools/transfer.ML	Tue Apr 17 20:48:07 2012 +0200
     1.2 +++ b/src/HOL/Tools/transfer.ML	Tue Apr 17 14:00:09 2012 +0200
     1.3 @@ -138,13 +138,16 @@
     1.4  fun transfer_tac ctxt = SUBGOAL (fn (t, i) =>
     1.5    let
     1.6      val bs = bnames t
     1.7 +    val rules0 = @{thms Rel_App Rel_Abs}
     1.8      val rules = Data.get ctxt
     1.9    in
    1.10      EVERY
    1.11        [rewrite_goal_tac @{thms transfer_forall_eq transfer_implies_eq} i,
    1.12         CONVERSION (Trueprop_conv (fo_conv ctxt)) i,
    1.13         rtac @{thm transfer_start [rotated]} i,
    1.14 -       REPEAT_ALL_NEW (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) (i + 1),
    1.15 +       REPEAT_ALL_NEW (resolve_tac rules0 ORELSE' atac
    1.16 +         ORELSE' SOLVED' (REPEAT_ALL_NEW (resolve_tac rules))
    1.17 +         ORELSE' eq_tac ctxt) (i + 1),
    1.18         (* Alpha-rename bound variables in goal *)
    1.19         SUBGOAL (fn (u, i) =>
    1.20           rtac @{thm equal_elim_rule1} i THEN
    1.21 @@ -156,7 +159,7 @@
    1.22  
    1.23  fun correspondence_tac ctxt i =
    1.24    let
    1.25 -    val rules = Data.get ctxt
    1.26 +    val rules = @{thms Rel_App Rel_Abs} @ Data.get ctxt
    1.27    in
    1.28      EVERY
    1.29        [CONVERSION (correspond_conv ctxt) i,

     2.1 --- a/src/HOL/Transfer.thy	Tue Apr 17 20:48:07 2012 +0200
     2.2 +++ b/src/HOL/Transfer.thy	Tue Apr 17 14:00:09 2012 +0200
     2.3 @@ -84,22 +84,22 @@
     2.4  lemma Rel_eq_refl: "Rel (op =) x x"
     2.5    unfolding Rel_def ..
     2.6  
     2.7 +lemma Rel_App:
     2.8 +  assumes "Rel (A ===> B) f g" and "Rel A x y"
     2.9 +  shows "Rel B (App f x) (App g y)"
    2.10 +  using assms unfolding Rel_def App_def fun_rel_def by fast
    2.11 +
    2.12 +lemma Rel_Abs:
    2.13 +  assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
    2.14 +  shows "Rel (A ===> B) (Abs (\<lambda>x. f x)) (Abs (\<lambda>y. g y))"
    2.15 +  using assms unfolding Rel_def Abs_def fun_rel_def by fast
    2.16 +
    2.17  use "Tools/transfer.ML"
    2.18  
    2.19  setup Transfer.setup
    2.20  
    2.21  declare fun_rel_eq [relator_eq]
    2.22  
    2.23 -lemma Rel_App [transfer_raw]:
    2.24 -  assumes "Rel (A ===> B) f g" and "Rel A x y"
    2.25 -  shows "Rel B (App f x) (App g y)"
    2.26 -  using assms unfolding Rel_def App_def fun_rel_def by fast
    2.27 -
    2.28 -lemma Rel_Abs [transfer_raw]:
    2.29 -  assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
    2.30 -  shows "Rel (A ===> B) (Abs (\<lambda>x. f x)) (Abs (\<lambda>y. g y))"
    2.31 -  using assms unfolding Rel_def Abs_def fun_rel_def by fast
    2.32 -
    2.33  hide_const (open) App Abs Rel
    2.34  
    2.35