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