Thanks to the help of several developers our database (of types of
equations etc) can be parsed again !
Now we are going to use this database, and again we have problems with
different behavior of Isabelle2009-2:
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 !
Walther
PS:
(1) The environment '[(l, a+b*x), (r, 0)]' looks like ready to use:
val inst =
(Empty,
Branch3
(Empty,
(("l", 0),
("RealDef.real",
Const ("Groups.plus_class.plus",
"RealDef.real => RealDef.real => RealDef.real") $
Free ("a", "RealDef.real") $
(Const ("Groups.times_class.times",
"RealDef.real => RealDef.real => RealDef.real") $
Free ("b", "RealDef.real") $ Free ("x", "RealDef.real")))),
Empty,
(("r", 0),
("RealDef.real", Const ("Groups.zero_class.zero", "RealDef.real"))),
Empty))
: Type.tyenv * Envir.tenv
(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
What is going on here ?
On 09/03/2010 02:19 PM, Walther Neuper wrote:
Makarius,
thanks for the warning ...
On 09/03/2010 01:31 PM, Makarius wrote:
On Fri, 3 Sep 2010, Walther Neuper wrote:
[...]
That is exactly what we need, ...
ML {* print_depth 99;
val ctxt = ProofContext.init_global @{theory};
ProofContext.read_term_pattern ctxt "matches (?a + ?b * bdv^2 =
(0::real)) equ";
*}
BTW, the "global" in ProofContext.init_global indicates that this is a
somewhat unusual operation to be used only as last resort, when no
proper local context is available. Here you have one, which is the
context of the 'ML' command.
... but we are still struggling to bring the old code alive in the
Isabelle2009 world. If the code runs again, then we shall take advantage
of all the wonderful services of present Isabelle and then with pleasure
follow your recommendations ...
>
So you really should use proper @{context} here, not the raw
background @{theory}. Of course, these antiquotations only work for
individual tests -- the context is that of the compile-time of the ML
command. In production code you need to abstract over the "ctxt",
passing through the value that you get from the surrounding system
infrastructure (i.e. concrete syntax wrappers of proof methods etc.).
Makarius
Walther
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
