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

[Christian Urban]

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
variables.

> (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,
Christian

------------------------------

theory Test
imports Main Complex
begin

ML {*
let
   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
in
   ML_Antiquote.inline "term_pat" (parser >> term_pat)
end
*}

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
*}


end