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.

Ondrej




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