1.1 --- a/src/HOL/Tools/transfer.ML	Thu Apr 19 10:49:47 2012 +0200
     1.2 +++ b/src/HOL/Tools/transfer.ML	Thu Apr 19 11:52:07 2012 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4    val transfer_tac: Proof.context -> int -> tactic
     1.5    val correspondence_tac: Proof.context -> int -> tactic
     1.6    val setup: theory -> theory
     1.7 +  val abs_tac: int -> tactic
     1.8  end
     1.9  
    1.10  structure Transfer : TRANSFER =
    1.11 @@ -93,21 +94,8 @@
    1.12  
    1.13  (** Transfer proof method **)
    1.14  
    1.15 -fun bnames (t $ u) = bnames t @ bnames u
    1.16 -  | bnames (Abs (x,_,t)) = x :: bnames t
    1.17 -  | bnames _ = []
    1.18 -
    1.19 -fun rename [] t = (t, [])
    1.20 -  | rename (x::xs) ((c as Const (@{const_name Abs}, _)) $ Abs (_, T, t)) =
    1.21 -    let val (t', xs') = rename xs t
    1.22 -    in (c $ Abs (x, T, t'), xs') end
    1.23 -  | rename xs0 (t $ u) =
    1.24 -    let val (t', xs1) = rename xs0 t
    1.25 -        val (u', xs2) = rename xs1 u
    1.26 -    in (t' $ u', xs2) end
    1.27 -  | rename xs t = (t, xs)
    1.28 -
    1.29 -fun cert ctxt t = cterm_of (Proof_Context.theory_of ctxt) t
    1.30 +fun dest_Rel (Const (@{const_name Rel}, _) $ r $ x $ y) = (r, x, y)
    1.31 +  | dest_Rel t = raise TERM ("dest_Rel", [t])
    1.32  
    1.33  fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y
    1.34  
    1.35 @@ -135,23 +123,28 @@
    1.36      Induct.arbitrary_tac ctxt 0 vs' i
    1.37    end)
    1.38  
    1.39 +(* Apply rule Rel_Abs with appropriate bound variable name *)
    1.40 +val abs_tac = SUBGOAL (fn (t, i) =>
    1.41 +  let
    1.42 +    val pat = (#2 o dest_Rel o HOLogic.dest_Trueprop o Thm.concl_of) @{thm Rel_Abs}
    1.43 +    val obj = (#3 o dest_Rel o HOLogic.dest_Trueprop o Logic.strip_assums_concl) t
    1.44 +    val rule = Thm.rename_boundvars pat obj @{thm Rel_Abs}
    1.45 +  in
    1.46 +    rtac rule i
    1.47 +  end handle TERM _ => no_tac)
    1.48 +
    1.49  fun transfer_tac ctxt = SUBGOAL (fn (t, i) =>
    1.50    let
    1.51 -    val bs = bnames t
    1.52 -    val rules0 = @{thms Rel_App Rel_Abs}
    1.53      val rules = Data.get ctxt
    1.54 +    val app_tac = rtac @{thm Rel_App}
    1.55    in
    1.56      EVERY
    1.57        [rewrite_goal_tac @{thms transfer_forall_eq transfer_implies_eq} i,
    1.58         CONVERSION (Trueprop_conv (fo_conv ctxt)) i,
    1.59         rtac @{thm transfer_start [rotated]} i,
    1.60 -       REPEAT_ALL_NEW (resolve_tac rules0 ORELSE' atac
    1.61 +       REPEAT_ALL_NEW (app_tac ORELSE' abs_tac ORELSE' atac
    1.62           ORELSE' SOLVED' (REPEAT_ALL_NEW (resolve_tac rules))
    1.63           ORELSE' eq_tac ctxt) (i + 1),
    1.64 -       (* Alpha-rename bound variables in goal *)
    1.65 -       SUBGOAL (fn (u, i) =>
    1.66 -         rtac @{thm equal_elim_rule1} i THEN
    1.67 -         rtac (Thm.reflexive (cert ctxt (fst (rename bs u)))) i) i,
    1.68         (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
    1.69         rewrite_goal_tac post_simps i,
    1.70         rtac @{thm _} i]