[isabelle] cases/induction on existential/free variables



datatype dt = A nat | B dt list;
lemma "EX (x :: dt). P x"

Assuming that producing an existential witness is out of the question
in the actual circumstance, how do I prove this? I.e., how do I apply
cases or induct on it? I'm thinking that the way would be to transform
it into something like

"EX x. (case x of A n => P' n | _ => False) | (case x of B n => P'' n
| _ => False)"

But I don't know how to accomplish this. (BTW, is there a more
succinct way to express that term?)

Upon further thought, it seems that actually the best way is to just
pick some good term to substitute for x, and then simplify. However,
I've encountered a problem with this as well. I have a lemma "!!z. EX
x. P x", and I need my substitution for "x" to depend on "z" to make
sense.

However, applying rule exI[of _ "Q z"] doesn't work--"z" can't be
captured this way; it's renamed to "za". Do I actually need to change
my lemma to read "!!z EX (x z). P (x z)"? That's kind of painful.

Chris Capel
-- 
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)





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