implement transfer tactic with more scalable forward proof methods

--- a/src/HOL/Tools/transfer.ML	Fri Apr 27 13:19:21 2012 +0200
+++ b/src/HOL/Tools/transfer.ML	Fri Apr 27 14:07:31 2012 +0200
@@ -6,7 +6,6 @@
 
 signature TRANSFER =
 sig
-  val fo_conv: Proof.context -> conv
   val prep_conv: conv
   val get_relator_eq: Proof.context -> thm list
   val transfer_add: attribute
@@ -14,7 +13,6 @@
   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
 end
 
 structure Transfer : TRANSFER =
@@ -37,22 +35,12 @@
 
 (** Conversions **)
 
-val App_rule = Thm.symmetric @{thm App_def}
-val Abs_rule = Thm.symmetric @{thm Abs_def}
 val Rel_rule = Thm.symmetric @{thm Rel_def}
 
 fun dest_funcT cT =
   (case Thm.dest_ctyp cT of [T, U] => (T, U)
     | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))
 
-fun App_conv ct =
-  let val (cT, cU) = dest_funcT (Thm.ctyp_of_term ct)
-  in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] App_rule end
-
-fun Abs_conv ct =
-  let val (cT, cU) = dest_funcT (Thm.ctyp_of_term ct)
-  in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Abs_rule end
-
 fun Rel_conv ct =
   let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)
       val (cU, _) = dest_funcT cT'
@@ -63,14 +51,6 @@
     Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
   | _ => raise CTERM ("Trueprop_conv", [ct]))
 
-(* Conversion to insert tags on every application and abstraction. *)
-fun fo_conv ctxt ct = (
-      Conv.combination_conv (fo_conv ctxt then_conv App_conv) (fo_conv ctxt)
-      else_conv
-      Conv.abs_conv (fo_conv o snd) ctxt then_conv Abs_conv
-      else_conv
-      Conv.all_conv) ct
-
 (* Conversion to preprocess a transfer rule *)
 fun prep_conv ct = (
       Conv.implies_conv Conv.all_conv prep_conv
@@ -79,24 +59,10 @@
       else_conv
       Conv.all_conv) ct
 
-(* Conversion to prep a proof goal containing a transfer rule *)
-fun transfer_goal_conv ctxt ct = (
-      Conv.forall_conv (transfer_goal_conv o snd) ctxt
-      else_conv
-      Conv.implies_conv Conv.all_conv (transfer_goal_conv ctxt)
-      else_conv
-      Trueprop_conv
-      (Conv.combination_conv (Conv.fun_conv Rel_conv) (fo_conv ctxt))
-      else_conv
-      Conv.all_conv) ct
-
-
 (** Transfer proof method **)
 
-fun dest_Rel (Const (@{const_name Rel}, _) $ r $ x $ y) = (r, x, y)
-  | dest_Rel t = raise TERM ("dest_Rel", [t])
-
 fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y
+  | RelT t = raise TERM ("RelT", [t])
 
 (* Tactic to correspond a value to itself *)
 fun eq_tac ctxt = SUBGOAL (fn (t, i) =>
@@ -111,7 +77,7 @@
   end handle Match => no_tac | TERM _ => no_tac)
 
 val post_simps =
-  @{thms App_def Abs_def transfer_forall_eq [symmetric]
+  @{thms transfer_forall_eq [symmetric]
     transfer_implies_eq [symmetric] transfer_bforall_unfold}
 
 fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) =>
@@ -122,47 +88,141 @@
     Induct.arbitrary_tac ctxt 0 vs' i
   end)
 
-(* Apply rule Rel_Abs with appropriate bound variable name *)
-val abs_tac = SUBGOAL (fn (t, i) =>
+(* 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 =
+      let
+        val (t', ctxt) = skeleton t ctxt
+      in
+        (Abs (x, dummyT, t'), ctxt)
+      end
+  | skeleton (t $ u) ctxt =
+      let
+        val (t', ctxt) = skeleton t ctxt
+        val (u', ctxt) = skeleton u ctxt
+      in
+        (t' $ u', ctxt)
+      end
+  | skeleton _ ctxt =
+      let
+        val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt
+      in
+        (Free (c, dummyT), ctxt)
+      end
+
+fun mk_relT (T, U) = T --> U --> HOLogic.boolT
+
+fun mk_Rel t =
+  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 =
   let
-    val pat = (#2 o dest_Rel o HOLogic.dest_Trueprop o Thm.concl_of) @{thm Rel_Abs}
-    val obj = (#3 o dest_Rel o HOLogic.dest_Trueprop o Logic.strip_assums_concl) t
-    val rule = Thm.rename_boundvars pat obj @{thm Rel_Abs}
+    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])) =
+        let
+          val r1 = rel T1 U1
+          val r2 = rel T2 U2
+          val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
+        in
+          Const (@{const_name fun_rel}, rT) $ r1 $ r2
+        end
+      | rel T U = raise TYPE ("rel", [T, U], [])
+    fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
+      | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =
+        let
+          val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
+          val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
+          val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
+          val thm0 = Thm.assume cprop
+          val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
+          val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
+          val r2 = Thm.dest_fun2 (Thm.dest_arg (cprop_of thm1))
+          val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r1))
+          val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r2))
+          val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
+          val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
+          val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
+          val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
+        in
+          (thm2 COMP rule, hyps)
+        end
+      | zip ctxt thms (f $ t) (g $ u) =
+        let
+          val (thm1, hyps1) = zip ctxt thms f g
+          val (thm2, hyps2) = zip ctxt thms t u
+        in
+          (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
+        end
+      | zip _ _ (t as Free (_, T)) u =
+        let
+          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)
+    val (thm, hyps) = zip ctxt [] t u
   in
-    rtac rule i
-  end handle TERM _ => no_tac)
+    Drule.implies_intr_list hyps (thm RS rename)
+  end
 
-fun transfer_tac equiv ctxt = SUBGOAL (fn (t, i) =>
+fun transfer_rule_of_term ctxt t =
   let
+    val s = skeleton t ctxt |> fst |> Syntax.check_term ctxt |>
+      map_types (map_type_tfree (fn (a, _) => TFree (a, HOLogic.typeS)))
+    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
+  in
+    Thm.generalize (tfrees, rnames @ frees) (Thm.maxidx_of thm + 1) thm
+  end
+
+fun transfer_tac equiv ctxt i =
+  let
+    val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
+    val start_rule = 
+      if equiv then @{thm transfer_start} else @{thm transfer_start'}
     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 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),
+      [rewrite_goal_tac pre_simps i THEN
+       SUBGOAL (fn (t, i) =>
+         rtac start_rule i THEN
+         (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t))
+           THEN_ALL_NEW
+             (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules))
+               ORELSE' eq_tac ctxt)) (i + 1)) i,
        (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
        rewrite_goal_tac post_simps i,
        rtac @{thm _} i]
-  end)
+  end
 
-fun transfer_prover_tac ctxt i =
+fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
   let
-    val rules = @{thms Rel_App Rel_Abs} @ Data.get ctxt
+    val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
+    val rule1 = transfer_rule_of_term ctxt rhs
+    val rules = Data.get ctxt
   in
     EVERY
-      [CONVERSION (transfer_goal_conv ctxt) i,
+      [CONVERSION prep_conv i,
        rtac @{thm transfer_prover_start} i,
-       REPEAT_ALL_NEW
-         (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) (i+1),
-       rewrite_goal_tac @{thms App_def Abs_def} i,
+       (rtac rule1 THEN_ALL_NEW
+         REPEAT_ALL_NEW
+           (resolve_tac rules ORELSE' eq_tac ctxt)) (i+1),
        rtac @{thm refl} i]
-  end
+  end)
+
+(** Methods and attributes **)
 
 val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
   error ("Bad free variable: " ^ Syntax.string_of_term ctxt t))

--- a/src/HOL/Transfer.thy	Fri Apr 27 13:19:21 2012 +0200
+++ b/src/HOL/Transfer.thy	Fri Apr 27 14:07:31 2012 +0200
@@ -42,14 +42,8 @@
 
 subsection {* Transfer method *}
 
-text {* Explicit tags for application, abstraction, and relation
-membership allow for backward proof methods. *}
-
-definition App :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-  where "App f \<equiv> f"
-
-definition Abs :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-  where "Abs f \<equiv> f"
+text {* Explicit tag for relation membership allows for
+  backward proof methods. *}
 
 definition Rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   where "Rel r \<equiv> r"
@@ -87,15 +81,15 @@
 lemma Rel_eq_refl: "Rel (op =) x x"
   unfolding Rel_def ..
 
-lemma Rel_App:
+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
+  shows "Rel B (f x) (g y)"
+  using assms unfolding Rel_def fun_rel_def by fast
 
-lemma Rel_Abs:
+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
+  shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
+  using assms unfolding Rel_def fun_rel_def by fast
 
 use "Tools/transfer.ML"
 
@@ -103,7 +97,7 @@
 
 declare fun_rel_eq [relator_eq]
 
-hide_const (open) App Abs Rel
+hide_const (open) Rel
 
 
 subsection {* Predicates on relations, i.e. ``class constraints'' *}