big_ops_nat[T:Type,o:(associative?[T]),id: {tid: T | FORALL (t:T): tid o t = t AND t o tid = t}]: THEORY

BEGIN

  IMPORTING for_iterate[T]

  F,G : VAR [nat->T]
  i   : VAR nat
  j   : VAR int
  z   : VAR nat
  p   : VAR int
  rel : VAR (preorder?[T])
  c   : VAR T

  big_ops_nat(i,j,F): T =
    for(i,j,id,LAMBDA(k:subrange(i,j),t:T):t o F(k))

  big_ops_nat_eq: LEMMA (FORALL (k:nat): i<=k AND k<=j IMPLIES F(k)=G(k))
    IMPLIES big_ops_nat(i,j,F) = big_ops_nat(i,j,G)

  big_ops_nat_expand_right: LEMMA
    big_ops_nat(i,j,F) = (IF i <= j THEN big_ops_nat(i,j-1,F) o F(j) ELSE id ENDIF)

  big_ops_nat_expand_left: LEMMA
    big_ops_nat(i,j,F) = (IF i <= j THEN F(i) o big_ops_nat(i+1,j,F) ELSE id ENDIF)

  big_ops_nat_split: LEMMA
    i-1<=z AND z<=j IMPLIES
    big_ops_nat(i,j,F) = big_ops_nat(i,z,F) o big_ops_nat(z+1,j,F)

  big_ops_nat_shift: LEMMA
    i+p>=0 IMPLIES 
    big_ops_nat(i+p,j+p,F) = big_ops_nat(i,j,LAMBDA (k:nat): IF k+p>=0 THEN F(k+p) ELSE id ENDIF)

  big_ops_nat_reverse: LEMMA
    commutative?[T](o) IMPLIES
    big_ops_nat(i,j,F) = big_ops_nat(i,j,LAMBDA (k:nat): IF i+j-k>=0 THEN F(i+j-k) ELSE id ENDIF)

  big_ops_nat_id : LEMMA
    (FORALL (k:nat): i<=k AND k<=j IMPLIES F(k) = id) IMPLIES big_ops_nat(i,j,F)=id

  big_ops_nat_comp: LEMMA
    commutative?[T](o) IMPLIES
    big_ops_nat(i,j,F) o big_ops_nat(i,j,G) = big_ops_nat(i,j,LAMBDA (k:nat): F(k) o G(k))

  ; * : VAR [[T,T]->T]

  big_ops_nat_distrib: LEMMA
    i<=j AND
    (FORALL (t1,t2,t3:T): t1 * (t2 o t3) = (t1 * t2) o (t1 * t3)) IMPLIES
    c * big_ops_nat(i,j,F) = big_ops_nat(i,j,LAMBDA (k:nat): c * F(k))

END big_ops_nat