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

Re: the "the" operator



Hi,

Bruno is right, of course, but there is a minor point I think is
worth noting.  I created the following theory

singleton_the: THEORY
 BEGIN
  k: VAR nat
  found?: pred[nat]
  f: FORMULA
    singleton?({k | found?(k)}) AND found?(k) => k = the({k | found?(k)})
 END singleton_the

If you simply run
 (skosimp)
 (expand "singleton?")
 (skosimp)
 (inst-cp -1 "k!1")
 (inst -1 "the({k | found?(k)})")

then this last instantiation will lead to two goals, one of which
is that "{k | found?(k)}" is a singleton.  This was a hypothesis
earlier, but was expanded out and is no longer readily available.
The right way to deal with this is to use (assert) before expanding
singleton? - that way the hypotheses are recorded, and the second
subgoal is no longer generated.

Sam

> Mauro Gargano wrote:
> > Hi again,
> > 
> > It should be easy to prove but I don't know how:
> > 
> > 
> > [-1]  singleton?(LAMBDA (i: subrange(j!1, l`len - 1)): found?(Nth(l, i)))
> > [-2]  0 <= j!1
> > [-3]  j!1 <= len(l) - 2
> > [-4]  j!1 >= 0
> > [-5]  j!1 < l`len
> > [-6]  found?(Nth(l, j!1))
> >  |-------
> > [1]   j!1 = the(LAMBDA (k: subrange(j!1, l`len - 1)): found?(Nth(l, k)))
> > 
> > 
> > 
> > I have a predicate true for j!1, I have the hypotesis of uniquenes,
> > so the set is "singleton?" and the "the" operator should give back the 
> > value j!1....am I wrong?
> > 
> > 
> > 
> > please, give me a feedback.
> > 
> > Mauro.
> > 
> 
> Hi,
> 
> Expanding the definition of "singleton?" followed by
> (skolem!) and two instantiations should work.
> 
> Bruno
> -- 
> Bruno Dutertre                             | bruno@sdl.sri.com
> SDL, SRI International                     | fax: 650 859-2844
> 333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717
>