--- 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,
--- 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