# [isabelle] Higher-order matching against schematic variables

```Hi all,

```
I have a question with higher-order matching against schematic variables. I can't figure out why the pattern trm1 can't be matched against lem if lem was "A x y --> x y = 0". However, if the RHS contains constants instead, e.g., "A x y --> g a = 0", a matcher is found. Since x and y have the same types of g and a respectively, how come there isn't a matcher in the former case? A difference is that x and y are schematic variables, but why can't schematic variables be matched against?
```
Here's the code:

locale A =
fixes f :: "nat => nat"
and a :: nat
assumes ax: "f a = 0"

consts
g :: "nat => nat"
a :: nat

lemma lem: "A x y --> x y = 0"
sorry

ML {*

val trm1 = term_of @{cpat "?P --> (?f::((?'a=>?'b)=>?'c)) ?stuff = ?v"};
val trm2 = Thm.prop_of @{thm lem};

val mtch_seq = let
val init = Envir.empty 0
val ctxt = @{context}
```
val (Const ("Trueprop",_) \$ trm2) = Thm.prop_of (ProofContext.get_thm ctxt "lem")
```in
Unify.matchers @{theory} [(trm1,trm2)]
end;

val seq as SOME (mtch,_) = nthseq 0 mtch_seq;
pretty_env @{context} (Envir.term_env mtch);
*}

Thanks
Michael

--
Postal Address: School of Informatics, University of Edinburgh,
Room 2.05, Informatics Forum, 10 Crichton Street,
Edinburgh EH8 9AB, UK.
Telephone Number: +44-131-651-3077,
Fax Number: +44-131-650-6899,
Email: M.Chan at ed.ac.uk
Web Page: http://homepages.inf.ed.ac.uk/mchan/

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

```

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