Transferring higher order goals

Question

I’m trying to establish an induction rule for a custom datatype using the transfer package, but apply transfer does not work for me. Here is a simple example:

theory TransferHO imports Main begin

typedef pos = "{x :: nat. x > 0}" by blast
setup_lifting  type_definition_pos

lift_definition one :: pos is 1 by auto
lift_definition S :: "pos ⇒ pos" is Suc by auto

lemma
  assumes "P one"
  assumes "⋀ x. P x ⟹ P (S x)"
  shows "P n"
  using assms
  apply transfer

At this point, the goal is still

⋀P x. P one ⟹ (⋀x. P x ⟹ P (S x)) ⟹ P x

and not

⋀P x. P 1 ⟹ (⋀x. x > 0 ⟹ P x ⟹ P (Suc x)) ⟹ x > 0 ⟹ P x

which I would expect. What do I need to do to transfer the lemma before proving it?

Also, generally, how can one have better control over apply transfer, or at least better debugging ways?

Answer 1

The result of a transfer is not unique in general, the transfer method merely computes one of the possible solutions, but you can backtrack with back to cycle through the others. In your particular example, you find your desired outcome after backtracking 53 times (at least with Isabelle2013-1-RC3). The order of the solutions is determined by the order of the [transfer_rule] declarations, and therefore the number of backtracking is likely to change from one release to the next.

Unfortunately, transfer provides hardly any control to where it takes the goal if there are many solutions.