Quelle  relation_iterate.pvs

% iteration of binary relations R, i.e., R composed with itself n times
% R o ... o R
%
% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
% Date: Dec 2004

relation_iterate[T: TYPE]: THEORY

BEGIN

  IMPORTING relations_extra[T], relation_props2[T, T, T, T]

  R, R1, R2, S1, S2: VAR pred[[T, T]]
  m, n: VAR nat
  p: VAR posnat
  x, y, z: VAR T

  comp_equal_r: LEMMA
    R o =[T] = R

  comp_equal_l: LEMMA
    =[T] o R = R

  iterate(R, n): RECURSIVE pred[[T, T]] =
    IF n = 0 THEN =[T] ELSE iterate(R, n - 1) o R ENDIF
  MEASURE n

  iterate_add: LEMMA
    iterate(R, m + n) = iterate(R, m) o iterate(R, n)

  iterate_add_applied: LEMMA 
    iterate(R, m)(x,y) & iterate(R, n)(y,z) => iterate(R, m + n)(x,z)

  iterate_1: LEMMA
    iterate(R, 1) = R

  iterate_add_one: LEMMA 
    iterate(R, n + 1) = R o iterate(R, n)

  iterate_mult: LEMMA
    iterate(iterate(R, m), n) = iterate(R, m * n)

  converse_equal: LEMMA
    converse(=[T]) = =[T]

  converse_comp: LEMMA
    converse(R1 o R2) = converse(R2) o converse(R1)

  iterate_converse: LEMMA
    iterate(converse(R), n) = converse(iterate(R, n))

  comp_is_monotone: LEMMA
    subset?(R1, R2) & subset?(S1, S2) => subset?(R1 o S1, R2 o S2)

  iterate_is_monotone: LEMMA
    subset?(R1, R2) => subset?(iterate(R1, n), iterate(R2, n))

END relation_iterate