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

[Walther Neuper]

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