Re: [isabelle] Matching done by the transfer method



On 03/22/2013 12:20 PM, Daniel Raggi wrote:

> Suppose I have a transfer rule of the form:
> "((R ===> op =) ===> op =) All (λ Q. ∀ x>0. Q x)"


Ok, sorry I wrote this. I meant BN instead of R.



> Well, this suggests that you need a rule of this form:
> "((BN ===> op =) ===> op =) <something> All"
>
> but your rule is
> "((R ===> op =) ===> op =) All <something>"
>
>
The problem is that if you define a rule like
"((BN ===> op =) ===> op =) All <something>"
with <something> being composite (say it is "s t"), the rule will be
completely useless because the transfer method, when applied to a goal,
will search for matches only for the symbols in the goal, i.e., it will
search for a match
"(<transfer stuff here>) <something> s"
and another match
"(<transfer stuff here>) <something> t"

Even when the goal contains expression "s t" explicitly, a rule of the form
"(<transfer stuff here>) <something> (s t)"
will not be used.

In the case I'm working one wouldn't be able to find a rule of the form
"((BN ===> op =) ===> op =) <something> All"
because BN is not right-total. That's why I am bounding it.

I have looked at Transfer_Int_Nat.thy. The difference from my example and
that example is that, there, things are being transferred from Int to Nat,
so every All in a goal is translated to a bounded forall. That same example
wouldn't work the other way around if we had a bounded forall in a goal (of
Int) and tried to reduce it to an All (of Nat).

I hope I'm not being too unclear...

Daniel



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