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

[Walther Neuper]

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