[isabelle-dev] [isabelle] Higher-order matching against schematic variables

[Lawrence Paulson]

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
>