author huffman Tue, 17 Apr 2012 14:00:09 +0200 changeset 47523 1bf0e92c1ca0 parent 47522 f74da4658bd1 child 47524 f80c6d492763
make transfer method more deterministic by using SOLVED' on some subgoals
 src/HOL/Tools/transfer.ML file | annotate | diff | comparison | revisions src/HOL/Transfer.thy file | annotate | diff | comparison | revisions
```--- 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

```