Re: [isabelle] Matching done by the transfer method



>
>
>> 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.
>
>
Yes, Ball works, and some composite expressions work.
But suppose we have the transfer rules
"(BN ===> op ⟷) T P"
"((BN ===> op ⟷) ===> op ⟷) All (λ Q. (∀ x>0. Q x))"

and goal
"(λ Q. (∀ x>0. Q x)) (λx. P x)"

(note that this is exactly the same as "∀ x>0. P x"). The transfer rules
match the goal perfectly, but when "(λ Q. (∀ x>0. Q x)) (λx. P x)"  is
parsed by Isabelle it states the goal as "∀ x>0. P x" and apparently the
transfer method tries to find a match for that expression, and not the more
"internal" one.

Thanks for your help. I'll stop repeating myself now.

Daniel



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