Re: [isabelle] Matching done by the transfer method



No, actually my example is wrong... it does reduce "P (4+3)" to "Q N". Then
it is more puzzling than I thought, because it is specific to the forall.


On 22 March 2013 13:07, Daniel Raggi <danielraggi at gmail.com> wrote:

> ok, so I made a simpler example to clarify stuff. Suppose you have this
> transfer rules:
> "BN N (4+3)"
> "(BN ===> op <->) Q P"
> (where N and Q are some constants we previously defined)
>
> and this goal:
> "P (4+3)"
>
> One would think that the transfer method would reduce the goal to "Q N",
> but it doesn't, because I think it would rather find transfer rules for 4,
> 3 and +, not the whole term.
>
> Daniel
>
>
>
> On 22 March 2013 12:38, Daniel Raggi <danielraggi at gmail.com> wrote:
>
>> 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.