Re: [isabelle] cases/induction on existential/free variables



Quoting Chris Capel <pdf23ds at gmail.com>:

However, applying rule exI[of _ "Q z"] doesn't work--"z" can't be
captured this way; it's renamed to "za".

Using the "of" attribute only works in this way if "z" is a free variable. In your case, it appears that "z" is bound by a meta-universal quantifier within your proof subgoal; there is no way to refer to such variables using the "of" or "where" attributes.

You have two alternatives:

1. Use Isar-style declarative proofs. When proving this subgoal, you can "fix z", after which "z" can be referred to as a free variable.

2. Stay with apply-style proofs, but use "rule_tac". The "_tac" variations of tactics *can* refer to meta-universal-bound variables within your subgoal. For example, try

apply (rule_tac x="Q z" in exI)

Hope this helps,
- Brian







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