Re: [isabelle] ind_cases in Isabelle 2005 vs 2007



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.