[isabelle] obtaining existentials



Hi,

I have a very quick isabelle question about existentials...

Here is a snippet of my proof:

<BEGIN>

hence "∃b. ∃l' T.
⌊h'⌋ = (⌊l'⌋ ⋅ (toheap T) ⋅ ⌊r⌋) 
∧ safe n C' l' T (Γ(a := ⌊A⌋)) ([Q]a) 
∧ ((S(a:=⌊l⌋)) = T ∨ (∃B Sb Tb. (Γ(a := ⌊A⌋)) b = ⌊B⌋ 
∧ (S(a:=⌊l⌋)) b = ⌊Sb⌋ ∧ T b = ⌊Tb⌋ ∧ (empty, Sb, Tb) ∈ B 
∧ (S(a:=⌊l⌋))(b:=None) = T(b:=None)))" by auto

then obtain b where "∃l' T.
⌊h'⌋ = (⌊l'⌋ ⋅ (toheap T) ⋅ ⌊r⌋) 
∧ safe n C' l' T (Γ(a := ⌊A⌋)) ([Q]a) 
∧ ((S(a:=⌊l⌋)) = T ∨ (∃B Sb Tb. (Γ(a := ⌊A⌋)) b = ⌊B⌋ 
∧ (S(a:=⌊l⌋)) b = ⌊Sb⌋ ∧ T b = ⌊Tb⌋ ∧ (empty, Sb, Tb) ∈ B 
∧ (S(a:=⌊l⌋))(b:=None) = T(b:=None)))" by auto

<END>

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?

Thanks very much,
John






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