[isabelle-dev] Inventing names (Re: Bug: Possible generalization error in 'Tactic.rule_by_tactic')
krauss at in.tum.de
Sat Apr 10 11:38:31 CEST 2010
Brian Huffman wrote:
> I'm sure that many of the internal proofs performed by fixrec and the
> domain package use free variable names like "P" or "x". Without
> locales or local theories, this was never a problem: The global
> context might mention Const "P", but never Free "P". However, local
> theory contexts *can* refer to free variables, and tools need to be
> aware of this.
Yes. Whenever you invent names, you must do this relative to a context.
Also, if you call other tools, you must make sure that the names you
invented are again known to the context. This corresponds to a "fix"
command in Isar.
> My question is this: With local theory contexts, what is the right way
> to obtain free variable names that are safe to use in local proofs?
I think the easiest way is to use Variable.variant_fixes.
More information about the isabelle-dev