*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] obtaining existentials*From*: John Wickerson <jpw48 at cam.ac.uk>*Date*: Sun, 14 Nov 2010 09:30:32 +0000*In-reply-to*: <4CDECD3D.3060900@in.tum.de>*References*: <96ADB578-848C-44BD-82C5-D22AF043F1FF@cam.ac.uk> <4CDECD3D.3060900@in.tum.de>

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

**References**:**[isabelle] obtaining existentials***From:*John Wickerson

**Re: [isabelle] obtaining existentials***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] obtaining existentials
- Next by Date: [isabelle] Open project position at TUM: Computer-supported verification of automata constructions
- Previous by Thread: Re: [isabelle] obtaining existentials
- Next by Thread: [isabelle] Open project position at TUM: Computer-supported verification of automata constructions
- Cl-isabelle-users November 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list