Re: [isabelle] obtaining existentials



On Sat, Nov 13, 2010 at 7:45 AM, John Wickerson <jpw48 at cam.ac.uk> wrote:
> It looks like a very straightforward deduction to me. Ignoring the messy long expression, we start with a something of the form "∃b. BLAH", and from this I want to say "obtain b where BLAH". But it doesn't work; auto can't handle it.
>
> My question is: which tactic should I use to prove this?

You can use

from `EX b. BLAH`
obtain b where "BLAH" by (rule exE)

or more simply,

from `EX b. BLAH`
obtain b where "BLAH" ..

Of course, this can still fail if the types of the expressions don't
match. If "BLAH" has some polymorphic stuff in it, you might need to
add some type constraints (either on parts of "BLAH" or on the
variable "b").

Hope this helps,

- Brian





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