enable variant of transfer method that proves an implication instead of an equivalence

--- a/src/HOL/Tools/transfer.ML	Thu Apr 19 19:36:24 2012 +0200
+++ b/src/HOL/Tools/transfer.ML	Sat Apr 21 20:52:33 2012 +0200
@@ -11,7 +11,7 @@
   val get_relator_eq: Proof.context -> thm list
   val transfer_add: attribute
   val transfer_del: attribute
-  val transfer_tac: Proof.context -> int -> tactic
+  val transfer_tac: bool -> Proof.context -> int -> tactic
   val transfer_prover_tac: Proof.context -> int -> tactic
   val setup: theory -> theory
   val abs_tac: int -> tactic
@@ -132,18 +132,20 @@
     rtac rule i
   end handle TERM _ => no_tac)
 
-fun transfer_tac ctxt = SUBGOAL (fn (t, i) =>
+fun transfer_tac equiv ctxt = SUBGOAL (fn (t, i) =>
   let
     val rules = Data.get ctxt
     val app_tac = rtac @{thm Rel_App}
+    val start_rule =
+      if equiv then @{thm transfer_start} else @{thm transfer_start'}
   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 (app_tac ORELSE' abs_tac ORELSE' atac
+       rtac start_rule i,
+       SOLVED' (REPEAT_ALL_NEW (app_tac ORELSE' abs_tac ORELSE' atac
          ORELSE' SOLVED' (REPEAT_ALL_NEW (resolve_tac rules))
-         ORELSE' eq_tac ctxt) (i + 1),
+         ORELSE' eq_tac ctxt)) (i + 1),
        (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
        rewrite_goal_tac post_simps i,
        rtac @{thm _} i]
@@ -168,9 +170,9 @@
 val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon)
   |-- Scan.repeat free) []
 
-val transfer_method : (Proof.context -> Method.method) context_parser =
+fun transfer_method equiv : (Proof.context -> Method.method) context_parser =
   fixing >> (fn vs => fn ctxt =>
-    SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac ctxt))
+    SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt))
 
 val transfer_prover_method : (Proof.context -> Method.method) context_parser =
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
@@ -195,7 +197,9 @@
   #> Relator_Eq.setup
   #> Attrib.setup @{binding transfer_rule} transfer_attribute
      "transfer rule for transfer method"
-  #> Method.setup @{binding transfer} transfer_method
+  #> Method.setup @{binding transfer} (transfer_method true)
+     "generic theorem transfer method"
+  #> Method.setup @{binding transfer'} (transfer_method false)
      "generic theorem transfer method"
   #> Method.setup @{binding transfer_prover} transfer_prover_method
      "for proving transfer rules"

--- a/src/HOL/Transfer.thy	Thu Apr 19 19:36:24 2012 +0200
+++ b/src/HOL/Transfer.thy	Sat Apr 21 20:52:33 2012 +0200
@@ -75,10 +75,10 @@
   "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"
+lemma transfer_start: "\<lbrakk>P; Rel (op =) P Q\<rbrakk> \<Longrightarrow> Q"
   unfolding Rel_def by simp
 
-lemma transfer_start': "\<lbrakk>Rel (op \<longrightarrow>) P Q; P\<rbrakk> \<Longrightarrow> Q"
+lemma transfer_start': "\<lbrakk>P; Rel (op \<longrightarrow>) P Q\<rbrakk> \<Longrightarrow> Q"
   unfolding Rel_def by simp
 
 lemma transfer_prover_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
@@ -278,4 +278,14 @@
   "bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
   unfolding transfer_forall_def by (rule All_transfer)
 
+text {* Transfer rules using implication instead of equality on booleans. *}
+
+lemma eq_imp_transfer [transfer_rule]:
+  "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
+  unfolding right_unique_alt_def .
+
+lemma forall_imp_transfer [transfer_rule]:
+  "right_total A \<Longrightarrow> ((A ===> op \<longrightarrow>) ===> op \<longrightarrow>) transfer_forall transfer_forall"
+  unfolding right_total_alt_def transfer_forall_def .
+
 end