# Re: [isabelle] ind_cases in Isabelle 2005 vs 2007

*To*: John Ridgway <john at jacelridge.com>
*Subject*: Re: [isabelle] ind_cases in Isabelle 2005 vs 2007
*From*: Stefan Berghofer <berghofe at in.tum.de>
*Date*: Fri, 01 Feb 2008 11:40:35 +0100
*Cc*: isabelle-users at cl.cam.ac.uk
*In-reply-to*: <6FF41B11-B181-4571-97A3-622CB664D125@jacelridge.com>
*Organization*: Technische Universität München
*References*: <6FF41B11-B181-4571-97A3-622CB664D125@jacelridge.com>
*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.13) Gecko/20060417

John Ridgway wrote:

Unfortunately I also have a number of
apply(ind_cases "(f x, y) \<in> z")
and these don't seem to be working. I can get around it by:
inductive_cases f_z_cases : "(f x, y) \<in> z"
and using
erule(f_z_cases)

`but that's going to mean a bunch of changes to my proofs. Is there a
``reason this isn't working?
`

ind_cases does not work when the formula specified as an argument refers
to variables bound by meta quantifiers in the current goal (these variables
are displayed with green colour in ProofGeneral). Like most proper Isar
proof methods (e.g. "cases") and attributes (e.g. "of"), "ind_cases" cannot
deal with such variables. To make it work, you have to explicitly tell ind_cases
(using the "for" keyword) to generalize the variables that you want to match with
the bound variables in the goal. In the example
lemma "(x, x) : r^* ==> True"
apply (ind_cases "(x, x) : r^*")
everything works as expected, since x is a free variable (as indicated by the
blue colour in ProofGeneral). In contrast,
lemma "!!x. (x, x) : r^* ==> True"
apply (ind_cases "(x, x) : r^*")
fails, because x is a bound variable (as indicated by the green colour in
ProofGeneral). If you instruct ind_cases to generalize x, it works as well:
lemma "!!x. (x, x) : r^* ==> True"
apply (ind_cases "(x, x) : r^*" for x)
Greetings,
Stefan
--
Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de
Institut fuer Informatik Phone: +49 89 289 17328
Technische Universitaet Muenchen Fax: +49 89 289 17307
Boltzmannstr. 3 Room: 01.11.059
85748 Garching, GERMANY http://www.in.tum.de/~berghofe

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*