[isabelle-dev] use term patterns, was: 'produce term patterns'

Christian Urban urbanc at in.tum.de
Thu Sep 30 19:48:29 CEST 2010

Hi Walther,

Here my guess what is going on:

> Given
>   val t = @{term "a + b * x = (0 ::real)"};
>  val pat = parse_patt thy "?l = (?r ::real)";
>   val precond = @{term "l is_polynomial"};
> we match
>   val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
> in order to get an environment for instantiating the precondition
>   val preinst = Envir.subst_term inst precond;
> to "(a + b * x) is_polynomial"; but we have still 'preinst = precond'.
> Studying pattern.ML and envir.ML did not help.
> Any help is appreciated !

Is it possible you forgot the "?" in the term
precond to indicate that ?l is a (schematic)
variable. Substitutions only work over schematic

> (2) val precond = parse_patt thy "?l is_polynomial";  produces
> *** exception TYPE raised (line 109 of "envir.ML"):
> *** Variable "?l" has two distinct types
> *** real
> *** ?'a1 => ?'b1

With antiquotations you have to be careful with
typing. In your matcher you calculate a substitution
for ?l and an empty type substitution, since no
type variable needs to be matched.

Now @{term "l is_polynomial"} might not completely
determine what the type of l is. In this case it
will be assigned a fixed (free) type-variable.
This will then cause problems when you apply the
substitution, since real does not match with the
fixed type-variable.

Even if you use the antiquotation @{term_pat "?l is_polynomial"}
(see below) and the assigned type is a schematic type-variable,
your way of calculating the substitution does not provide
a substitution for types. One solution is to make explicit
the type of ?l to avoid any problems with type variables.
See below.

Hope this is helpful,


theory Test
imports Main Complex

ML {*
   val parser = Args.context -- Scan.lift Args.name_source
   fun term_pat (ctxt, str) = str |> ProofContext.read_term_pattern ctxt
   |> ML_Syntax.print_term |> ML_Syntax.atomic
   ML_Antiquote.inline "term_pat" (parser >> term_pat)

ML {*
   val t = @{term "a + b * x = (0 ::real)"};
   val pat = @{term_pat "?l = (?r ::real)"};
   val precond = @{term_pat "is_polynomial (?l::real)"};
   val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);

ML {*
   Envir.subst_term inst precond
   |> Syntax.string_of_term @{context}
   |> writeln


More information about the isabelle-dev mailing list