[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.
>
> 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
More information about the isabelle-dev
mailing list