Re: [isabelle] Surprises with transfer method

On 01/31/2013 10:58 AM, Florian Haftmann wrote:
When experimenting with lifting and transfer, I ran into situations
where transfer yields funny goal states.  I have distilled two prominent
candidates into the attached theories.  The first one seems to me a
result of erroneous backtracking in a tactic behind the transfer method.
  For the second one, I am standing in the dark.

Maybe experts on transfer can comment on this.


Hi Florian,

Example 1:
yes, transfer backtracks: first uses later introduced matching transfer rules and then it tries earlier introduced rules. So if you do this:

  fixes m n q :: natural
  shows "(m + n) * q = m * q + n * q"
apply transfer

you get:

1. ?a21 (λm. transfer_forall (λn. transfer_forall (λq. (m + n) * q = m * q + n * q))) 2. Transfer.Rel (fun_rel (fun_rel cr_natural op ⟶) op =) ?a21 transfer_forall

The first goal is solved by simplifier by substituting (λa. True) for ?a21 and then you get the second goal to prove. That's the reason it doesn't fail because the simplifier did some progress.

Example 2:
No surprise. Transfer knows that the abstraction function natural_of_nat transfers to identity on the raw level (i.e., there is a transfer rule for this; the rule is proved in setup_lifting) but it doesn't know anything about of_nat. Thut it transfers natural_of_nat to id and it doesn't do anything with of_nat. Because the types doesn't match it cannot transfer equality to equality on the raw level and thus it asks for a rule saying what equality should be transferred to.

If you prove a transfer rule for of_nat

lemma [transfer_rule]:
"(op= ===> cr_natural) (of_nat::nat=>nat) (of_nat::nat=>natural)"
unfolding of_nat_def[abs_def] by transfer_prover

then you can finish your proof:

lemma natural_of_nat_of_nat [simp]:
  "natural_of_nat = of_nat"
  by transfer auto

I hope my answer helps.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.