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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and