# HG changeset patch
# User huffman
# Date 1334909888 -7200
# Node ID 1568dadd598aede7991345781bfd7cf9e92612ac
# Parent  f5eaa7fa8d7285e6794515dc23a80b9c59aeb623
make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules

diff -r f5eaa7fa8d72 -r 1568dadd598a src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Thu Apr 19 23:18:47 2012 +0200
+++ b/src/HOL/Tools/transfer.ML	Fri Apr 20 10:18:08 2012 +0200
@@ -86,8 +86,7 @@
       Conv.implies_conv Conv.all_conv (correspond_conv ctxt)
       else_conv
       Trueprop_conv
-      (Conv.combination_conv
-         (Conv.combination_conv Rel_conv (fo_conv ctxt)) (fo_conv ctxt))
+      (Conv.combination_conv (Conv.fun_conv Rel_conv) (fo_conv ctxt))
       else_conv
       Conv.all_conv) ct
 
@@ -156,8 +155,11 @@
   in
     EVERY
       [CONVERSION (correspond_conv ctxt) i,
+       rtac @{thm correspondence_start} i,
        REPEAT_ALL_NEW
-         (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) i]
+         (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) (i+1),
+       rewrite_goal_tac @{thms App_def Abs_def} i,
+       rtac @{thm refl} i]
   end
 
 val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
diff -r f5eaa7fa8d72 -r 1568dadd598a src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Thu Apr 19 23:18:47 2012 +0200
+++ b/src/HOL/Transfer.thy	Fri Apr 20 10:18:08 2012 +0200
@@ -81,6 +81,9 @@
 lemma transfer_start': "\<lbrakk>Rel (op \<longrightarrow>) P Q; P\<rbrakk> \<Longrightarrow> Q"
   unfolding Rel_def by simp
 
+lemma correspondence_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
+  by simp
+
 lemma Rel_eq_refl: "Rel (op =) x x"
   unfolding Rel_def ..