[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Non empty finite set induction

On Thu, May 29, 2008 at 7:09 PM, Jerome <jerome@xxxxxxxxxxxxxx> wrote:
> I'm cc'ing the list to try and get our conversation back over
> there. I've attached a dump of the original 'curry' theory, as well as
> the 'dualton' theory you were working on, for background.

Okay.  The more eyes the better.

> The first two don't really help; I think the third one has potential
> though. One that I'm working on is:
>  sets_lemmas_ext[T: TYPE]: THEORY
>    a, b: VAR T
>    A: VAR non_empty_finite_set[T]
>    doubleton?(A): bool = singleton?(rest(A))
>    remove_is_element: LEMMA
>      FORALL (a, b: (A) | a /= b): doubleton?(A) IMPLIES
>        remove(a, A) = singleton(b) AND remove(b, A) = singleton(a)
>  END sets_lemmas_ext
> Does this make sense? I get some dead-ends when trying to prove it, so
> I may be missing something. Essentially, however, in the curry_x proof
> it would be ideal to bring something like this in and instantiate it
> with "k!1" and "choose(U!1)".

What do you think of the version I'm attaching here?  I like
"doubleton".  It makes more sense than "dualton". :-)
Jerry James

Attachment: doubleton.pvs
Description: Binary data

Attachment: doubleton.prf
Description: Binary data