Re: [isabelle] Matching done by the transfer method



On 03/22/2013 01:38 PM, Daniel Raggi 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.

My point was about the order of the transfer rule, not about the relation.
But I was too hasty. I thought you tried to use BN :: int => nat => bool, but your relation is really BN :: nat => int => bool.


    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"

As far as I know, that works. If you have a transfer rule "R f (g h)" and your goal contains "g h", that term is transferred to f.

If your rule is, let's say, "R f (%P. g P)" and your goal contains g R, this is not magically transferred to "f R". Because in order to transfer g, a rule "R ? g" is expected.

But concerning your example with quantifiers, I think you can use Ball constant instead

"((R ===> op =) ===> op =) All (Ball {0..})",

similarly to  HOL/ex/Transfer_Int_Nat.thy.

Hope this helps.

Ondrej




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