[isabelle-dev] produce term patterns

[Walther Neuper]

Hi Jasmin,

thank's for your precise hint --- that underlines the issue, that one 
should query The Isabelle Programming Tutorial before asking in 
isabelle-dev@; sorry for having failed to do this this time.

Walther

On 09/02/2010 08:16 PM, Jasmin Christian Blanchette wrote:
> Hi Walther,
>    
>> Hope there is somebody who needs not dig in the code to answer this question ...
>>
>> How can we produce specific patterns (some variables of a term should become Free, some Var), for instance:
>>      
> On p. 24 of the Cookbook (http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/isabelle-cookbook/raw-file/tip/progtutorial.pdf) there's a "term_pat" antiquotation that seems to be doing what you want, if I'm not mistaken.
>    
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";
*}

...gives...

val it = () : unit
val ctxt = <context> : Proof.context
val it =
    Const ("Tools.matches", "bool => bool => bool") $
      (Const ("op =", "RealDef.real => RealDef.real => bool") $
        (Const ("Groups.plus_class.plus",
                "RealDef.real => RealDef.real => RealDef.real") $
          Var (("a", 0), "RealDef.real") 
$                                               (*!!!*)
          (Const ("Groups.times_class.times",
                  "RealDef.real => RealDef.real => RealDef.real") $
            Var (("b", 0), "RealDef.real") 
$                                              (*!!!*)
            (Const ("Power.power_class.power",
                    "RealDef.real => nat => RealDef.real") $
              Free ("bdv", "RealDef.real") 
$                                              (*!!!*)
              (Const ("Int.number_class.number_of", "Int.int => nat") $
                (Const ("Int.Bit0", "Int.int => Int.int") $
                  (Const ("Int.Bit1", "Int.int => Int.int") $
                    Const ("Int.Pls", "Int.int"))))))) $
        Const ("Groups.zero_class.zero", "RealDef.real")) $
      Free ("equ", "bool")
    : term