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

*To*: pvs-help@csl.sri.com*Subject*: Re: proofs involving epsilon*From*: John Rushby <RUSHBY@csl.sri.com>*Date*: Tue 23 May 00 15:56:33-PDT*Cc*: pvs-help@csl.sri.com, RUSHBY@csl.sri.com*Delivery-Date*: Tue May 23 15:57:37 2000*In-Reply-To*: <Pine.LNX.4.10.10005211849420.19659-200000@dizzy.ittc.ukans.edu>*Mail-System-Version*: <SUN-MM(229)+TOPSLIB(128)@csl.sri.com>

Murali Rangarajan posed the question" how to prove "choice" in the following: choice: THEORY BEGIN t: TYPE sets: TYPE = setof[t] sets_of_sets: TYPE = setof[sets] u, z: VAR t w, y: VAR sets x: VAR sets_of_sets % forall nonempty sets x whose members are nonempty sets, there exists % a set y such that every member of y is a member of some member of x, % and every member of x has a member in y choice: THEOREM (FORALL x: (nonempty?(x) AND (FORALL y: member(y, x) => nonempty?(y))) => ((EXISTS y: (FORALL z: member(z, y) IMPLIES (EXISTS w: member(w, x) AND member(z, w))) and (FORALL w: member(w, x) IMPLIES (EXISTS z: member(z, w) AND member(z, y)))))) END choice -------------------------------------------------------------------------- The following proof does it. Generally, it's preferable to use "choose" rather than epsilon, because then the essential property is encoded in the type. There's some discussion of this in the paper http://www.csl.sri.com/reports/html/tse98.html It's important to exclude "choose" from any grinds ('cos you do not want the definition opened up). The initial instantiation needs some thought; the rest of the proof is then pretty routine: grind and its friends will get the wrong instantiations, so you have to step somewhat slowly and make the instantiations by hand until you get to the point on each branch where you can let rip with reduce (the guts of grind). ("" (SKOSIMP*) (INST + "{a:t| exists (b: sets): member(b,x!1) and a=choose(b)}") (("1" (GRIND :IF-MATCH NIL :EXCLUDE ("choose")) (("1" (INST + "choose(w!1)") (("1" (ASSERT) (INST + "w!1") (ASSERT)) ("2" (REDUCE)))) ("2" (INST + "b!1") (ASSERT)))) ("2" (REDUCE)))) John -------

**References**:**proofs involving epsilon***From:*Murali Rangarajan <rmurali@ittc.ukans.edu>

- Prev by Date:
**proofs involving epsilon** - Next by Date:
**Re: Need help finding documentation on how to construct new strategies and add them into my context** - Prev by thread:
**proofs involving epsilon** - Next by thread:
**Identical antecedent and consequent** - Index(es):