Re: [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)"

Why not just "case x of A n => P' n | B n => P'' n"?

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

If you want to rewrite "EX (x :: dt). P x" into some other form, you can
do it explicitly by stating the subgoal "(EX (x :: dt). P x) = ...",
which you prove in the usual way (you may need extensionality here, rule
"ext").

Tobias





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