Hi Florian,
thank you for the detailed explanations about Vars and Frees+Context.
This is very helpful in updating our equation solver from 2000. At that
time we did not know about Contexts, thus we built some simple kind of
context ourselves.
So we really appreciate the services provided by Isabelle nowadays !
Walther
On 09/03/2010 08:41 AM, Florian Haftmann wrote:
Hi Walther,
How can we produce specific patterns (some variables of a term should
become Free, some Var),
in principle, the two syntactic categories of term variables have the
following purpose:
Free -- locally fixed variable, e.g. fixed variable in a proof context
or locally defined symbol in a local theory
Var -- schematic term, also used for textual pattern bindings in Isar
proofs (e.g.
let ?f = ...
have "..:" (is "?lhs = ?rhs")
This implies that Frees (at least at the level of the system the user /
tool developer is involved in) never exist on their own right, but are
relative to a context.
Whenever non-trivial hard-coded term fragments are needed in ML source
(non-trivial means that these are not accomplished conveniently using
term constructor primitives or abstract syntax combinators from logic.ML
or hologic.ML and such), nowadays term antiquotations are used, e.g.
@{term "\<lambda>x. x"}
or
@{prop "id = \<lambda>x. x"}
These antiquotations do not permit Vars -- a design decision for which I
remember there was a striking cause which I don't remember, though
(maybe somebody else can comment on this).
A possible workaround in your situation could be to use cpat, e.g.
@{cpat "..."} |> Thm.term_of
These hints however cover only the technical part. When I look at your
example
(term_of o the o (parse thy)) "matches (?a + ?b * bdv^2 = (0::real)) equ"
I wonder what the Frees bdv and que are actually supposed to mean. In a
conventional Isar setting they must belong to a context, of which there
is no trace here. From a purely technical point of view, you are free
to interpret Frees in what manner you want in a particular tool, but
this won't interact ever with the Isar machinery of nested proof
contexts etc. (maybe this issue is far beyond the intention of your e-mail).
That's the point: we want our equation solver interact with the Isar
machinery; thus we are going to use Isars context (after having
reanimated the solver in the Isabelle2009 world).
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
