implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
authorhuffman
Sat, 08 Jun 2013 19:40:19 -0700
changeset 52354 acb4f932dd24
parent 52353 dba3d398c322
child 52355 ebd1f6918663
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
src/HOL/Quotient_Examples/Lift_FSet.thy
src/HOL/Tools/transfer.ML
src/HOL/Transfer.thy
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Fri Jun 07 22:17:22 2013 -0400
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Sat Jun 08 19:40:19 2013 -0700
@@ -136,34 +136,22 @@
   but sometimes more convenient. *}
 
 lemma "fmap f (fmap g xs) = fmap (f \<circ> g) xs"
-  apply transfer'
-  apply (rule map_map)
-  done
+  using map_map [Transfer.transferred] .
 
 lemma "ffilter p (fmap f xs) = fmap f (ffilter (p \<circ> f) xs)"
-  apply transfer'
-  apply (rule filter_map)
-  done
+  using filter_map [Transfer.transferred] .
 
 lemma "ffilter p (ffilter q xs) = ffilter (\<lambda>x. q x \<and> p x) xs"
-  apply transfer'
-  apply (rule filter_filter)
-  done
+  using filter_filter [Transfer.transferred] .
 
 lemma "fset (fcons x xs) = insert x (fset xs)"
-  apply transfer
-  apply (rule set.simps)
-  done
+  using set.simps(2) [Transfer.transferred] .
 
 lemma "fset (fappend xs ys) = fset xs \<union> fset ys"
-  apply transfer
-  apply (rule set_append)
-  done
+  using set_append [Transfer.transferred] .
 
 lemma "fset (fconcat xss) = (\<Union>xs\<in>fset xss. fset xs)"
-  apply transfer
-  apply (rule set_concat)
-  done
+  using set_concat [Transfer.transferred] .
 
 lemma "\<forall>x\<in>fset xs. f x = g x \<Longrightarrow> fmap f xs = fmap g xs"
   apply transfer
@@ -176,7 +164,7 @@
   done
 
 lemma "fconcat (fmap (\<lambda>x. fcons x fnil) xs) = xs"
-  apply transfer'
+  apply transfer
   apply simp
   done
 
@@ -184,8 +172,6 @@
   by (induct xsss, simp_all)
 
 lemma "fconcat (fmap fconcat xss) = fconcat (fconcat xss)"
-  apply transfer'
-  apply (rule concat_map_concat)
-  done
+  using concat_map_concat [Transfer.transferred] .
 
 end
--- a/src/HOL/Tools/transfer.ML	Fri Jun 07 22:17:22 2013 -0400
+++ b/src/HOL/Tools/transfer.ML	Sat Jun 08 19:40:19 2013 -0700
@@ -15,11 +15,14 @@
   val get_relator_domain: Proof.context -> thm list
   val transfer_add: attribute
   val transfer_del: attribute
+  val transferred_attribute: thm list -> attribute
   val transfer_domain_add: attribute
   val transfer_domain_del: attribute
-  val transfer_rule_of_term: Proof.context -> term -> thm
+  val transfer_rule_of_term: Proof.context -> bool -> term -> thm
+  val transfer_rule_of_lhs: Proof.context -> term -> thm
   val transfer_tac: bool -> Proof.context -> int -> tactic
   val transfer_prover_tac: Proof.context -> int -> tactic
+  val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic
   val setup: theory -> theory
 end
 
@@ -33,13 +36,15 @@
   type T =
     { transfer_raw : thm Item_Net.T,
       known_frees : (string * typ) list,
+      compound_lhs : unit Net.net,
       compound_rhs : unit Net.net,
       relator_eq : thm Item_Net.T,
       relator_eq_raw : thm Item_Net.T,
       relator_domain : thm Item_Net.T }
   val empty =
-    { transfer_raw = Thm.full_rules,
+    { transfer_raw = Thm.intro_rules,
       known_frees = [],
+      compound_lhs = Net.empty,
       compound_rhs = Net.empty,
       relator_eq = Thm.full_rules,
       relator_eq_raw = Thm.full_rules,
@@ -47,13 +52,16 @@
   val extend = I
   fun merge
     ( { transfer_raw = t1, known_frees = k1,
+        compound_lhs = l1,
         compound_rhs = c1, relator_eq = r1,
         relator_eq_raw = rw1, relator_domain = rd1 },
       { transfer_raw = t2, known_frees = k2,
+        compound_lhs = l2,
         compound_rhs = c2, relator_eq = r2,
         relator_eq_raw = rw2, relator_domain = rd2 } ) =
     { transfer_raw = Item_Net.merge (t1, t2),
       known_frees = Library.merge (op =) (k1, k2),
+      compound_lhs = Net.merge (K true) (l1, l2),
       compound_rhs = Net.merge (K true) (c1, c2),
       relator_eq = Item_Net.merge (r1, r2),
       relator_eq_raw = Item_Net.merge (rw1, rw2),
@@ -66,6 +74,9 @@
 fun get_known_frees ctxt = ctxt
   |> (#known_frees o Data.get o Context.Proof)
 
+fun get_compound_lhs ctxt = ctxt
+  |> (#compound_lhs o Data.get o Context.Proof)
+
 fun get_compound_rhs ctxt = ctxt
   |> (#compound_rhs o Data.get o Context.Proof)
 
@@ -83,27 +94,36 @@
 fun get_relator_domain ctxt = ctxt
   |> (Item_Net.content o #relator_domain o Data.get o Context.Proof)
 
-fun map_data f1 f2 f3 f4 f5 f6
-  { transfer_raw, known_frees, compound_rhs, relator_eq, relator_eq_raw, relator_domain } =
+fun map_data f1 f2 f3 f4 f5 f6 f7
+  { transfer_raw, known_frees, compound_lhs, compound_rhs,
+    relator_eq, relator_eq_raw, relator_domain } =
   { transfer_raw = f1 transfer_raw,
     known_frees = f2 known_frees,
-    compound_rhs = f3 compound_rhs,
-    relator_eq = f4 relator_eq,
-    relator_eq_raw = f5 relator_eq_raw,
-    relator_domain = f6 relator_domain }
+    compound_lhs = f3 compound_lhs,
+    compound_rhs = f4 compound_rhs,
+    relator_eq = f5 relator_eq,
+    relator_eq_raw = f6 relator_eq_raw,
+    relator_domain = f7 relator_domain }
 
-fun map_transfer_raw f = map_data f I I I I I
-fun map_known_frees f = map_data I f I I I I
-fun map_compound_rhs f = map_data I I f I I I
-fun map_relator_eq f = map_data I I I f I I
-fun map_relator_eq_raw f = map_data I I I I f I
-fun map_relator_domain f = map_data I I I I I f
+fun map_transfer_raw   f = map_data f I I I I I I
+fun map_known_frees    f = map_data I f I I I I I
+fun map_compound_lhs   f = map_data I I f I I I I
+fun map_compound_rhs   f = map_data I I I f I I I
+fun map_relator_eq     f = map_data I I I I f I I
+fun map_relator_eq_raw f = map_data I I I I I f I
+fun map_relator_domain f = map_data I I I I I I f
 
 fun add_transfer_thm thm = Data.map
   (map_transfer_raw (Item_Net.update thm) o
+   map_compound_lhs
+     (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
+        Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>
+          Net.insert_term_safe (K true) (lhs, ())
+      | _ => I) o
    map_compound_rhs
      (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
-        (Const (@{const_name Rel}, _)) $ _ $ _ $ (rhs as (_ $ _)) => Net.insert_term (K true) (rhs, ())
+        Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>
+          Net.insert_term_safe (K true) (rhs, ())
       | _ => I) o
    map_known_frees (Term.add_frees (Thm.concl_of thm)))
 
@@ -148,8 +168,11 @@
     val thy = Thm.theory_of_thm thm
     val prop = Thm.prop_of thm
     val (t, mk_prop') = dest prop
-    val add_eqs = Term.fold_aterms
-      (fn t as Const (@{const_name HOL.eq}, _) => insert (op =) t | _ => I)
+    (* Only consider "op =" at non-base types *)
+    fun is_eq (Const (@{const_name HOL.eq}, Type ("fun", [T, _]))) =
+        (case T of Type (_, []) => false | _ => true)
+      | is_eq _ = false
+    val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)
     val eq_consts = rev (add_eqs t [])
     val eqTs = map (snd o dest_Const) eq_consts
     val used = Term.add_free_names prop []
@@ -308,13 +331,11 @@
   let val T = fastype_of t
   in Const (@{const_name Transfer.Rel}, T --> T) $ t end
 
-fun transfer_rule_of_terms ctxt tab t u =
+fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u =
   let
     val thy = Proof_Context.theory_of ctxt
-    (* precondition: T must consist of only TFrees and function space *)
-    fun rel (T as TFree (a, _)) U =
-          Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
-      | rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
+    (* precondition: prj(T,U) must consist of only TFrees and type "fun" *)
+    fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
         let
           val r1 = rel T1 U1
           val r2 = rel T2 U2
@@ -322,7 +343,12 @@
         in
           Const (@{const_name fun_rel}, rT) $ r1 $ r2
         end
-      | rel T U = raise TYPE ("rel", [T, U], [])
+      | rel T U =
+        let
+          val (a, _) = dest_TFree (prj (T, U))
+        in
+          Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
+        end
     fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
       | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =
         let
@@ -349,15 +375,15 @@
         in
           (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
         end
-      | zip _ _ (t as Free (_, T)) u =
+      | zip _ _ t u =
         let
+          val T = fastype_of t
           val U = fastype_of u
           val prop = mk_Rel (rel T U) $ t $ u
           val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
         in
           (Thm.assume cprop, [cprop])
         end
-      | zip _ _ t u = raise TERM ("zip_relterm", [t, u])
     val r = mk_Rel (rel (fastype_of t) (fastype_of u))
     val goal = HOLogic.mk_Trueprop (r $ t $ u)
     val rename = Thm.trivial (cterm_of thy goal)
@@ -366,42 +392,136 @@
     Drule.implies_intr_list hyps (thm RS rename)
   end
 
-fun transfer_rule_of_term ctxt t =
+(* create a lambda term of the same shape as the given term *)
+fun skeleton (is_atom : term -> bool) ctxt t =
   let
-    val compound_rhs = get_compound_rhs ctxt
-    val is_rhs = not o null o Net.unify_term compound_rhs
     fun dummy ctxt =
       let
         val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt
       in
         (Free (c, dummyT), ctxt)
       end
-    (* create a lambda term of the same shape as the given term *)
-    fun skeleton (Bound i) ctxt = (Bound i, ctxt)
-      | skeleton (Abs (x, _, t)) ctxt =
+    fun go (Bound i) ctxt = (Bound i, ctxt)
+      | go (Abs (x, _, t)) ctxt =
         let
-          val (t', ctxt) = skeleton t ctxt
+          val (t', ctxt) = go t ctxt
         in
           (Abs (x, dummyT, t'), ctxt)
         end
-      | skeleton (tu as (t $ u)) ctxt =
-        if is_rhs tu andalso not (Term.is_open tu) then dummy ctxt else
+      | go (tu as (t $ u)) ctxt =
+        if is_atom tu andalso not (Term.is_open tu) then dummy ctxt else
         let
-          val (t', ctxt) = skeleton t ctxt
-          val (u', ctxt) = skeleton u ctxt
+          val (t', ctxt) = go t ctxt
+          val (u', ctxt) = go u ctxt
         in
           (t' $ u', ctxt)
         end
-      | skeleton _ ctxt = dummy ctxt
-    val s = skeleton t ctxt |> fst |> Syntax.check_term ctxt |>
+      | go _ ctxt = dummy ctxt
+  in
+    go t ctxt |> fst |> Syntax.check_term ctxt |>
       map_types (map_type_tfree (fn (a, _) => TFree (a, HOLogic.typeS)))
+  end
+
+(** Monotonicity analysis **)
+
+(* TODO: Put extensible table in theory data *)
+val monotab =
+  Symtab.make
+    [(@{const_name transfer_implies}, [~1, 1]),
+     (@{const_name transfer_forall}, [1])(*,
+     (@{const_name implies}, [~1, 1]),
+     (@{const_name All}, [1])*)]
+
+(*
+Function bool_insts determines the set of boolean-relation variables
+that can be instantiated to implies, rev_implies, or iff.
+
+Invariants: bool_insts p (t, u) requires that
+  u :: _ => _ => ... => bool, and
+  t is a skeleton of u
+*)
+fun bool_insts p (t, u) =
+  let
+    fun strip2 (t1 $ t2, u1 $ u2, tus) =
+        strip2 (t1, u1, (t2, u2) :: tus)
+      | strip2 x = x
+    fun or3 ((a, b, c), (x, y, z)) = (a orelse x, b orelse y, c orelse z)
+    fun go Ts p (Abs (_, T, t), Abs (_, _, u)) tab = go (T :: Ts) p (t, u) tab
+      | go Ts p (t, u) tab =
+        let
+          val (a, _) = dest_TFree (Term.body_type (Term.fastype_of1 (Ts, t)))
+          val (_, tf, tus) = strip2 (t, u, [])
+          val ps_opt = case tf of Const (c, _) => Symtab.lookup monotab c | _ => NONE
+          val tab1 =
+            case ps_opt of
+              SOME ps =>
+              let
+                val ps' = map (fn x => p * x) (take (length tus) ps)
+              in
+                fold I (map2 (go Ts) ps' tus) tab
+              end
+            | NONE => tab
+          val tab2 = Symtab.make [(a, (p >= 0, p <= 0, is_none ps_opt))]
+        in
+          Symtab.join (K or3) (tab1, tab2)
+        end
+    val tab = go [] p (t, u) Symtab.empty
+    fun f (a, (true, false, false)) = SOME (a, @{const implies})
+      | f (a, (false, true, false)) = SOME (a, @{const rev_implies})
+      | f (a, (true, true, _))      = SOME (a, HOLogic.eq_const HOLogic.boolT)
+      | f _                         = NONE
+  in
+    map_filter f (Symtab.dest tab)
+  end
+
+fun transfer_rule_of_term ctxt equiv t : thm =
+  let
+    val compound_rhs = get_compound_rhs ctxt
+    val is_rhs = not o null o Net.unify_term compound_rhs
+    val s = skeleton is_rhs ctxt t
     val frees = map fst (Term.add_frees s [])
     val tfrees = map fst (Term.add_tfrees s [])
     fun prep a = "R" ^ Library.unprefix "'" a
     val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
-    val thm = transfer_rule_of_terms ctxt' (tfrees ~~ rnames) s t
+    val tab = tfrees ~~ rnames
+    fun prep a = the (AList.lookup (op =) tab a)
+    val thm = transfer_rule_of_terms fst ctxt' tab s t
+    val binsts = bool_insts (if equiv then 0 else 1) (s, t)
+    val cbool = @{ctyp bool}
+    val relT = @{typ "bool => bool => bool"}
+    val idx = Thm.maxidx_of thm + 1
+    val thy = Proof_Context.theory_of ctxt
+    fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool)
+    fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
   in
-    Thm.generalize (tfrees, rnames @ frees) (Thm.maxidx_of thm + 1) thm
+    thm
+      |> Thm.generalize (tfrees, rnames @ frees) idx
+      |> Thm.instantiate (map tinst binsts, map inst binsts)
+  end
+
+fun transfer_rule_of_lhs ctxt t : thm =
+  let
+    val compound_lhs = get_compound_lhs ctxt
+    val is_lhs = not o null o Net.unify_term compound_lhs
+    val s = skeleton is_lhs ctxt t
+    val frees = map fst (Term.add_frees s [])
+    val tfrees = map fst (Term.add_tfrees s [])
+    fun prep a = "R" ^ Library.unprefix "'" a
+    val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
+    val tab = tfrees ~~ rnames
+    fun prep a = the (AList.lookup (op =) tab a)
+    val thm = transfer_rule_of_terms snd ctxt' tab t s
+    val binsts = bool_insts 1 (s, t)
+    val cbool = @{ctyp bool}
+    val relT = @{typ "bool => bool => bool"}
+    val idx = Thm.maxidx_of thm + 1
+    val thy = Proof_Context.theory_of ctxt
+    fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool)
+    fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
+  in
+    thm
+      |> Thm.generalize (tfrees, rnames @ frees) idx
+      |> Thm.instantiate (map tinst binsts, map inst binsts)
   end
 
 fun eq_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) THEN_ALL_NEW rtac @{thm is_equality_eq}
@@ -409,7 +529,7 @@
 fun transfer_tac equiv ctxt i =
   let
     val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
-    val start_rule = 
+    val start_rule =
       if equiv then @{thm transfer_start} else @{thm transfer_start'}
     val rules = get_transfer_raw ctxt
     val eq_rules = get_relator_eq_raw ctxt
@@ -418,7 +538,7 @@
     val err_msg = "Transfer failed to convert goal to an object-logic formula"
     fun main_tac (t, i) =
       rtac start_rule i THEN
-      (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t))
+      (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))
         THEN_ALL_NEW
           (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))
             ORELSE' end_tac)) (i + 1)
@@ -429,13 +549,13 @@
        SUBGOAL main_tac i,
        (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
        rewrite_goal_tac post_simps i,
-       rtac @{thm _} i]
+       Goal.norm_hhf_tac i]
   end
 
 fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
   let
     val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
-    val rule1 = transfer_rule_of_term ctxt rhs
+    val rule1 = transfer_rule_of_term ctxt false rhs
     val rules = get_transfer_raw ctxt
     val eq_rules = get_relator_eq_raw ctxt
   in
@@ -447,6 +567,45 @@
        rtac @{thm refl} i]
   end)
 
+(** Transfer attribute **)
+
+fun transferred ctxt extra_rules thm =
+  let
+    val start_rule = @{thm transfer_start}
+    val start_rule' = @{thm transfer_start'}
+    val rules = extra_rules @ get_transfer_raw ctxt
+    val eq_rules = get_relator_eq_raw ctxt
+    val err_msg = "Transfer failed to convert goal to an object-logic formula"
+    val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
+    val thm1 = Drule.forall_intr_vars thm
+    val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
+                |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
+    val thm2 = thm1
+      |> Thm.certify_instantiate (instT, [])
+      |> Raw_Simplifier.rewrite_rule pre_simps
+    val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
+    val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
+    val rule = transfer_rule_of_lhs ctxt' t
+    val tac =
+      resolve_tac [thm2 RS start_rule', thm2 RS start_rule] 1 THEN
+      (rtac rule
+        THEN_ALL_NEW
+          (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
+            THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
+        handle TERM (_, ts) => raise TERM (err_msg, ts)
+    val thm3 = Goal.prove_internal [] @{cpat "Trueprop ?P"} (K tac)
+    val tnames = map (fst o dest_TFree o snd) instT
+  in
+    thm3
+      |> Raw_Simplifier.rewrite_rule post_simps
+      |> Raw_Simplifier.norm_hhf
+      |> Drule.generalize (tnames, [])
+      |> Drule.zero_var_indexes
+  end
+(*
+    handle THM _ => thm
+*)
+
 (** Methods and attributes **)
 
 val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
@@ -484,6 +643,14 @@
 val transfer_domain_attribute =
   Attrib.add_del transfer_domain_add transfer_domain_del
 
+(* Attributes for transferred rules *)
+
+fun transferred_attribute thms = Thm.rule_attribute
+  (fn context => transferred (Context.proof_of context) thms)
+
+val transferred_attribute_parser =
+  Attrib.thms >> transferred_attribute
+
 (* Theory setup *)
 
 val relator_eq_setup =
@@ -528,6 +695,8 @@
      (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
   #> Attrib.setup @{binding transfer_domain_rule} transfer_domain_attribute
      "transfer domain rule for transfer method"
+  #> Attrib.setup @{binding transferred} transferred_attribute_parser
+     "raw theorem transferred to abstract theorem using transfer rules"
   #> Global_Theory.add_thms_dynamic
      (@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get)
   #> Method.setup @{binding transfer} (transfer_method true)
--- a/src/HOL/Transfer.thy	Fri Jun 07 22:17:22 2013 -0400
+++ b/src/HOL/Transfer.thy	Sat Jun 08 19:40:19 2013 -0700
@@ -61,6 +61,11 @@
 lemma is_equality_eq: "is_equality (op =)"
   unfolding is_equality_def by simp
 
+text {* Reverse implication for monotonicity rules *}
+
+definition rev_implies where
+  "rev_implies x y \<longleftrightarrow> (y \<longrightarrow> x)"
+
 text {* Handling of meta-logic connectives *}
 
 definition transfer_forall where
@@ -252,14 +257,31 @@
 
 text {* Transfer rules using implication instead of equality on booleans. *}
 
+lemma transfer_forall_transfer [transfer_rule]:
+  "bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
+  "right_total A \<Longrightarrow> ((A ===> op =) ===> implies) transfer_forall transfer_forall"
+  "right_total A \<Longrightarrow> ((A ===> implies) ===> implies) transfer_forall transfer_forall"
+  "bi_total A \<Longrightarrow> ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall"
+  "bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall"
+  unfolding transfer_forall_def rev_implies_def fun_rel_def right_total_def bi_total_def
+  by metis+
+
+lemma transfer_implies_transfer [transfer_rule]:
+  "(op =        ===> op =        ===> op =       ) transfer_implies transfer_implies"
+  "(rev_implies ===> implies     ===> implies    ) transfer_implies transfer_implies"
+  "(rev_implies ===> op =        ===> implies    ) transfer_implies transfer_implies"
+  "(op =        ===> implies     ===> implies    ) transfer_implies transfer_implies"
+  "(op =        ===> op =        ===> implies    ) transfer_implies transfer_implies"
+  "(implies     ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
+  "(implies     ===> op =        ===> rev_implies) transfer_implies transfer_implies"
+  "(op =        ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
+  "(op =        ===> op =        ===> rev_implies) transfer_implies transfer_implies"
+  unfolding transfer_implies_def rev_implies_def fun_rel_def by auto
+
 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 .
-
 lemma eq_transfer [transfer_rule]:
   assumes "bi_unique A"
   shows "(A ===> A ===> op =) (op =) (op =)"