Re: [isabelle] Matching done by the transfer method



On 03/22/2013 03:02 PM, Daniel Raggi wrote:


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

"(λ Q. (∀ x>0. Q x)) (λx. P x)" and "∀ x>0. P x" are not exactly the same. They are only beta-equivalent. And you should know that when a term is parsed in Isabelle, it's beta-normalized. Thus your goal is really this term "∀ x>0. P x".

Ondrej




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