%% This file and the associated prf-file are taken
%% from the PVS 2.2 library
%% I have adopted the proofs to run under PVS 2.3

more_mucalculus_theorems[T:TYPE]: THEORY
 %Contains definitions of union and intersection continuity along
 %with proof that the iterated fixpoint of a union-continuous
 %predicate transformer least 

BEGIN

IMPORTING mucalculus[T], mutheorems[T]

q : VAR sequence[PRED[T]]
r, s: VAR T
Q, P, f, g, p,p1,p2: VAR pred[T]
N: VAR [T, T->bool]
predtt: TYPE = [pred[T]->pred[T]]
pp, qq: VAR predtt
setofpred: VAR pred[pred[T]]

%ascending/descending sequences of predicates
ascends?(q): bool = ascends?(q, <=)
descends?(q): bool = descends?(q, <=)

%pp(Uq) = U(pp(q)), q ascending
U_continuous?(pp): bool =
 (FORALL (q: (ascends?)) :
    pp(lub({p | EXISTS (i : nat): p = q(i)})) =
    lub({p | EXISTS (i : nat) : p = pp(q(i))}))

%pp(/\q) = /\pp(q), q descending
I_continuous?(pp) : bool =
 (FORALL (q: (descends?)) :
    pp(glb({p | EXISTS (i : nat): p = q(i)})) =
    glb({p | EXISTS (i : nat) : p = pp(q(i))}))

U_continuity_implies_monotonicity: LEMMA
  U_continuous?(pp) IMPLIES monotonic?(pp)

I_continuity_implies_monotonicity: LEMMA
  I_continuous?(pp) IMPLIES monotonic?(pp)

%pp(pp^{i}(p)) = pp^{i+1}(p)
iterate_step: LEMMA
  (FORALL (i:nat): pp(iterate(pp, i)(p)) = iterate(pp, i+1)(p))

%Mu is iterated fixpoint
Mu(pp)(s): bool =   lub({p | (EXISTS (j:nat):  p = iterate(pp, j)(emptyset[T]))})(s)

%For U_continuous pp, iterated fixpoint is the least fixpoint
Mu_mu: LEMMA (FORALL (pp: (U_continuous?)): Mu(pp) = mu(pp))

%remaining lemmas are useful but not hard.
mu_monot: LEMMA
  monotonic?(pp) AND monotonic?(qq) AND 
(FORALL p: pp(p) <= qq(p)) IMPLIES mu(pp) <= mu(qq)

nu_mu: LEMMA monotonic?(pp) IMPLIES
  nu(pp) = NOT mu(LAMBDA p: NOT pp(NOT p))

Pp, Qq : VAR (monotonic?)

mu_induction: LEMMA
   monotonic?(pp) AND 
  (FORALL s: pp(Q)(s) IMPLIES Q(s)) IMPLIES
  (FORALL s: mu(pp)(s) IMPLIES Q(s))


END more_mucalculus_theorems