[isabelle-dev] Forward reasoning with schematic variables?
makarius at sketis.net
Wed Dec 5 11:47:34 CET 2007
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.)
More information about the isabelle-dev