Email Gateway (Aug 19 2022 at 10:36): Email Gateway (Aug 19 2022 at 10:36):From: Daniel Raggi <danielraggi@gmail.com>
Suppose I have a transfer rule of the form:
"((R ===> op =) ===> op =) All (λ Q. ∀ x>0. Q x)"
and a goal of the form:
"∀ x>0. P x"
I would expect the transfer method to find the transfer rule as a match for
the goal provided that we have a match for P). However, what I get is:
goal (3 subgoals):
which suggests that the method is not looking for any `complex' matches,
but just searching for simpler matches. Is this a limitation of the
transfer method, or am I missing something? Should I have to create a
definition for "λ Q. ∀ x>0. Q x" (or whichever constraint I suggest as a
transfer target).
Daniel
Email Gateway (Aug 19 2022 at 10:36):From: Ondřej Kunčar <kuncar@in.tum.de>
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>"
I don't know what your example is about but it looks like you might want
to take a look to HOL/ex/Transfer_Int_Nat.thy.
Ondrej
Email Gateway (Aug 19 2022 at 10:36):From: Daniel Raggi <danielraggi@gmail.com>
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
Email Gateway (Aug 19 2022 at 10:36):From: Daniel Raggi <danielraggi@gmail.com>
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
Email Gateway (Aug 19 2022 at 10:36):From: Daniel Raggi <danielraggi@gmail.com>
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.
Email Gateway (Aug 19 2022 at 10:36):From: Ondřej Kunčar <kuncar@in.tum.de>
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
Email Gateway (Aug 19 2022 at 10:37):From: Daniel Raggi <danielraggi@gmail.com>
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
Email Gateway (Aug 19 2022 at 10:37):From: Ondřej Kunčar <kuncar@in.tum.de>
"(λ 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
Email Gateway (Aug 19 2022 at 10:37):From: Daniel Raggi <danielraggi@gmail.com>
I see. Thanks. Then I'll find my way around this using tricks like Ball,
or defining my own bounded quantifiers when I need them.
Last updated: Nov 21 2024 at 12:39 UTC