[isabelle-dev] produce term patterns

[Florian Haftmann]

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).

Hope this helps,
	Florian


-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100903/a0e194d3/attachment.sig>