Re: [isabelle] Matching done by the transfer method
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)"
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):
1. ?a10 (λx. ?ab10 0 x ⟶ P1 x) (* here P1 is the match for P *)
2. Transfer.Rel ((BN ===> op =) ===> op =) ?a10 All
3. Transfer.Rel (op = ===> BN ===> op =) ?ab10 op <
which suggests that the method is not looking for any `complex' matches,
but just searching for simpler matches.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and