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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
