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