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

Walther Neuper wneuper at ist.tugraz.at
Fri Oct 1 09:20:41 CEST 2010

```Hi Christian,

thanks for the code !

The code was helpful to set my wits to combinators. And it gave another
good exercise to distinguish what should be related to contexts and what
to theories (formulas of concrete calculations to the former, and
predefined patterns like those describing classes of equations to the
latter)

On 09/30/2010 07:48 PM, Christian Urban wrote:
> Hi Walther,
>
> Here my guess what is going on:
> [...]
> 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.
>
> 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

```