Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] obtaining existentials

Email Gateway (Aug 18 2022 at 16:27):

From: John Wickerson <jpw48@cam.ac.uk>
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

Email Gateway (Aug 18 2022 at 16:27):

From: Brian Huffman <brianh@cs.pdx.edu>
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

Email Gateway (Aug 18 2022 at 16:27):

From: Tobias Nipkow <nipkow@in.tum.de>
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:

Email Gateway (Aug 18 2022 at 16:27):

From: John Wickerson <jpw48@cam.ac.uk>
Hi Brian and Tobias, thanks very much for your helpful replies.

cheers,
John

Last updated: Apr 20 2024 at 01:05 UTC