Re: IF-EXISTS

[Sam Owre <owre@csl.sri.com>]

Hi Mauro,

What you probably want here is the "epsilon" function (or one of the
variants "choose" or "the").  In this case, I would probably write
something like

  LET found(k: nat): bool = L`list(k)`f=f1 ) AND k < 10
  IN IF (EXISTS (k: nat) : found(k))
     THEN epsilon ! (k: nat): found(k)
     ELSE 0
     ENDIF

This just returns some k, not necessarily the smallest such, though you
said it was assumed to be unique.  The other possibility is to write a
recursive function, something like

  FIND_REC(L : list_t, f1: nat, k: nat) :nat =
    IF k = L`max
    ELSIF L`list(k)`f=f1 AND k < 10 THEN k
    ELSE FIND_REC(L, f1, k+1)
    ENDIF
   MEASURE L`max - k

  FIND(L : list_t, f1: nat): nat = FIND_REC(L, f1, 0)

Hope this helps,
Sam  

> Hallo to everybody,
> 
> I have the need to create a function to that return the index of a element 
> (for which a predicate holds) of a list (assumed that this element is 
> unique).
> I tried something like this:
> 
> 
> 
> help 
>        : THEORY
> 
>  BEGIN
> 
>    A : TYPE+ = [# f: nat, g: nat, h:nat #]
> 
>    list_t: TYPE = [# max:nat, list: [below(max) -> A] #]
> 
> % I just want to define a find function ....
> 
>    FIND(L : list_t, f1: nat) :nat = (
> 
>            IF (( EXISTS (k: nat) : L`list(k)`f=f1 ) AND k < 10) THEN k
> 
>            ELSE 0
> 
>            ENDIF
> 
>    )
> 
>  
> 
>  END help
> 
> 
> but whithout success.
> Has someone an idea of how to do this? and, in the case I reject the 
> uniqueness-hypotesis, what happens? Obviously I should get in return a 
> sublist, but how....
> 
> 
> 
> Thanks,
> Mauro Gargano.