Email Gateway (Aug 18 2022 at 11:19): Email Gateway (Aug 18 2022 at 11:19):From: John Ridgway <john@jacelridge.com>
Friends -
I have been using Isabelle 2005 for some time now, and I'm trying to
make the transition to Isabelle 2007. I'm running into a bit of a
problem. I have a number of inductively defined sets; and I've
modified their definitions to use inductive_set rather than
inductive. 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? (BTW, f is a constructor in a datatype
here.)
Please tell me I'm missing something simple... :-)
Peace
Email Gateway (Aug 18 2022 at 11:20):From: Stefan Berghofer <berghofe@in.tum.de>
John Ridgway wrote:
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
Last updated: May 03 2024 at 08:18 UTC