[isabelle-dev] Bug: Possible generalization error in 'Tactic.rule_by_tactic'

[Brian Huffman]

On Fri, Apr 9, 2010 at 2:32 PM, Alexander Krauss <krauss at in.tum.de> wrote:
> Stefan Berghofer wrote:
>>
>>  inductive foo :: "'a => 'a => bool"
>>  where
>>    "foo x x"
>>
>>  locale test =
>>    fixes t P
>>    assumes ensure_clash [simp]: "t = P"
>>  begin
>>
>>  inductive_cases bar: "foo t z"
>
> Nice. :-)

As the author of some other packages that generate theorems, I am
concerned about this problem.

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.

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?
Since many of Isabelle's packages have only recently been converted to
use local theories, I'm not sure which other packages have code that
is safe to imitate.

- Brian