Quelle  max_bounded_posnat.pvs

max_bounded_posnat: THEORY
BEGIN

  a,x,y,n,UB: VAR posnat

  S: VAR {A: (nonempty?[posnat]) | EXISTS UB: FORALL (y: (A)): y <= UB}

  bnd(S): { a |  FORALL (x: (S)): x <= a}

  max_rec(S,(i:{j: posnat | j >= choose(S)})): RECURSIVE posnat =
                              IF S(i) THEN i
                              ELSE max_rec(S,i-1)
                              ENDIF
                              MEASURE i - choose(S)


  m: VAR nat  
  max_rec_in: LEMMA n >= choose(S) AND m = n - choose(S) IMPLIES S(max_rec(S, n))

  max_rec_bnd: LEMMA n >= x AND n >= choose(S) AND S(x) AND m >= n - x 
                 IMPLIES x <= max_rec(S, n)

  max(S): {a: posnat | S(a) AND (FORALL x: S(x) IMPLIES x <= a)}

  maximum?(a, S) : bool = S(a) AND (FORALL x: S(x) IMPLIES x <= a)

  max_def        : LEMMA max(S) = a IFF maximum?(a, S)

  max_lem        : LEMMA maximum?(max(S),S)

  max_in         : LEMMA S(max(S))

END max_bounded_posnat