add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer

--- a/src/HOL/Tools/transfer.ML	Wed Apr 04 12:25:58 2012 +0200
+++ b/src/HOL/Tools/transfer.ML	Wed Apr 04 16:03:01 2012 +0200
@@ -113,6 +113,10 @@
     rtac thm2 i
   end handle Match => no_tac | TERM _ => no_tac)
 
+val post_simps =
+  @{thms App_def Abs_def transfer_forall_eq [symmetric]
+    transfer_implies_eq [symmetric] transfer_bforall_unfold}
+
 fun transfer_tac ctxt = SUBGOAL (fn (t, i) =>
   let
     val bs = bnames t
@@ -128,8 +132,7 @@
          rtac @{thm equal_elim_rule1} i THEN
          rtac (Thm.reflexive (cert ctxt (fst (rename bs u)))) i) i,
        (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
-       rewrite_goal_tac @{thms App_def Abs_def} i,
-       rewrite_goal_tac @{thms transfer_forall_eq [symmetric] transfer_implies_eq [symmetric]} i,
+       rewrite_goal_tac post_simps i,
        rtac @{thm _} i]
   end)
 

--- a/src/HOL/Transfer.thy	Wed Apr 04 12:25:58 2012 +0200
+++ b/src/HOL/Transfer.thy	Wed Apr 04 16:03:01 2012 +0200
@@ -62,12 +62,19 @@
 definition transfer_implies where
   "transfer_implies \<equiv> op \<longrightarrow>"
 
+definition transfer_bforall :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+  where "transfer_bforall \<equiv> (\<lambda>P Q. \<forall>x. P x \<longrightarrow> Q x)"
+
 lemma transfer_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (transfer_forall (\<lambda>x. P x))"
   unfolding atomize_all transfer_forall_def ..
 
 lemma transfer_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (transfer_implies A B)"
   unfolding atomize_imp transfer_implies_def ..
 
+lemma transfer_bforall_unfold:
+  "Trueprop (transfer_bforall P (\<lambda>x. Q x)) \<equiv> (\<And>x. P x \<Longrightarrow> Q x)"
+  unfolding transfer_bforall_def atomize_imp atomize_all ..
+
 lemma transfer_start: "\<lbrakk>Rel (op =) P Q; P\<rbrakk> \<Longrightarrow> Q"
   unfolding Rel_def by simp