Re: [isabelle] obtaining existentials



Hi Brian and Tobias, thanks very much for your helpful replies.

cheers,
John

On 13 Nov 2010, at 17:39, Tobias Nipkow wrote:

> 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.