[isabelle-dev] Forward reasoning with schematic variables?

[Makarius]

On Tue, 4 Dec 2007, Steven Obua wrote:

> until shortly before the Isabelle2007 release the following line worked:
> 
> lemmas find_simp = While_simp[where continue="(\<lambda> x. ?f x 
> \<noteq> x)", simplified find_def[symmetric]]

This was only accepted by accident, approx. since 2003/2004.


> Is there an alternative way of doing this?

Just use a regular fixed "f" and do "standard" on the result.

Generally, it is better to avoid such forward reasoning and specify the 
intended result outright, using 'lemma' etc.  (People in favour of 
unrestricted forward reasoning will experience some surprises when doing 
it in a locale context, for example.)


	Makarius