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.
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"
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
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.
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
"(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