Re: [isabelle] obtaining existentials



Since the quantified expression was proved so easily, you can often
obtain the witnesses right away with the same method. In your case this
means you can probably drop the "hence ... by auto" altogether. If this
is too much in one go, prove the EX-statement first, as you did. But
don't repeat the text but

hence "EX b. ..." (is "EX b. ?P b") by auto
then obtain b where "?P b" ..

Note also that .. no longer works for multiple witnesses.

Tobias

John Wickerson schrieb:
> 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.