[isabelle-dev] produce term patterns

[Walther Neuper]

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