I will tackle your questions one at a time.
The difficulty with your original question concerns, what do we mean by
higher-order matching? For Isabelle, these are nothing but unifiers which leave
the object unchanged.
The problem is that you are trying to match ?x ?y against ?f ?stuff and this
creates a so-called flex-flex disagreement pair. There is no practical way to
enumerate these. for higher-order matching, Isabelle eliminates these using a
trivial substitution that modifies the object; this unifier is not a matcher
and is therefore discarded. I don't see this as a bug. If you need to have Vars
in the object but don't want them to be treated as variables, I suggest that
you use Frees instead and generalise them later.
Turning to your second question, the first-order matchers do appear to have
incorrect types. I don't know why this is. I also don't understand why this
code returns both first-order matchers and higher-order ones. These are simply
different things in some cases, and other cases the first-order ones are
redundant duplicates.
I am copying this to the developers' list in the hope that somebody else can
comment.
Larry
On 18 Nov 2010, at 18:05, Michael Chan wrote:
> On 18/11/10 16:07, Lawrence Paulson wrote:
>> I can't see the answer to this, but something complicated is going on when
>> you match (?f::((?'a=>?'b)=>?'c)) ?stuff against x y where x :: nat => nat.
>
> Thanks, Larry. Indeed, even without the predicate, it gives the same problem
> when using that pattern, i.e.
>
> lemma lem: "g a = 0"
> sorry
>
> vs
>
> lemma lem: "(x::nat=>nat) y = 0"
> sorry
>
> Now, if we instead use a simpler pattern:
>
> val trm1 = term_of @{cpat "(?f::?'a=>?'b) ?stuff = ?v"};
>
> matching it against "g a = 0" gives 4 matchers:
>
> 1. [?f::nat => nat := %a::nat. a, ?v::nat := 0::nat, ?stuff::nat := g a]
>
> 2. [?f::nat => nat := g, ?v::nat := 0::nat, ?stuff::nat := a]
>
> 3. [?f::?'a => nat := %b::?'a. g a, ?v::nat := 0::nat,
> ?stuff::?'a := ?stuff::?'a]
>
> 4. [?f::?'a => ?'b := g, ?v::?'b := 0::nat, ?stuff::?'a := a]
>
> But matching it against "(x::nat=>nat) y = 0", gives only 1 matcher:
>
> 1. [?f::?'a => ?'b := ?x::nat => nat, ?v::?'b := 0::nat,
> ?stuff::?'a := ?y::nat]
>
> which is of the same shape of the first lemma's 4th matcher.
>
> Perhaps the higher-order matcher somehow fails, since 1. and 3. should be
> returned by it. 2. is essentially 4., but with the schematic type variables
> instantiated. Now, is 4. a valid matcher even when ?'a and ?'b can be clearly
> instantiated (to become 2.)? If it is valid, isn't it redundant to have a
> separate matcher with the type variables uninstantiated?
>
> Thanks
> Michael
>
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
