On Fri, Apr 9, 2010 at 2:32 PM, Alexander Krauss <[email protected]> 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 _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
