%% 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

mutheorems[T : TYPE]: THEORY

BEGIN


IMPORTING mucalculus[T]

f,g,h: VAR pred[T]

refl: LEMMA
f <= f

antisym: LEMMA
f <= g AND g <= f IMPLIES f =g

trans: LEMMA
f <= g AND g <= h IMPLIES f <= h

AND_comm: LEMMA
(f AND g) = (g AND f)

AND_assoc: LEMMA
(f AND (g AND h)) = ((f AND g) AND h)

OR_comm: LEMMA
(f OR g) = (g OR f)

OR_assoc: LEMMA
(f OR (g OR h)) = ((f OR g) OR h)

AND_OR_dist: LEMMA
(f AND (g OR h)) = ((f AND g) OR (f AND h))

lem1: LEMMA
(f <= (g AND h)) = ((f <= g) AND (f <= h))

lem2: LEMMA
(f AND g) <= f

lem3: LEMMA
f <= (f OR g)

lem4: LEMMA
(f OR g) <= g IMPLIES f <= g

lem5: LEMMA
((f <= h) AND (g <= h)) = ((f OR g) <= h)

F: VAR pred[pred[T]]
glb_min: THEOREM
member(f,F) IMPLIES glb(F) <= f 

glb_max: THEOREM
(FORALL g: member(g,F) IMPLIES f <= g) IMPLIES
f <= glb(F)

lub_max: THEOREM
member(f,F) IMPLIES f <= lub(F) 

lub_min: THEOREM
(FORALL g: member(g,F) IMPLIES g <= f) IMPLIES
lub(F) <= f

ff: VAR [pred[T]->pred[T]]
lfp_lem1: LEMMA
(ff(f) = f) IMPLIES (lfp(ff) <= f)

lfp_lem2: LEMMA
monotonic?(ff) IMPLIES FORALL f: ff(f) <= f IMPLIES
		             ff(glb(LAMBDA f: ff(f) <= f)) <= f

lfp_thm: THEOREM
monotonic?(ff) IMPLIES ff(lfp(ff)) <= lfp(ff)

lfp_thm1: THEOREM
monotonic?(ff) IMPLIES lfp(ff) <= ff(lfp(ff))

lfp_thm2: THEOREM
monotonic?(ff) IMPLIES (ff(lfp(ff)) = lfp(ff))

lfp_lem3: LEMMA
monotonic?(ff) IMPLIES FORALL f: ff(f) <= f IMPLIES
		             lfp(ff) <= f

lfp_is_lfp: THEOREM
monotonic?(ff) IMPLIES lfp?(ff,lfp(ff))

gfp_lem1: LEMMA
 ff(f) = f IMPLIES f <= gfp(ff)

gfp_lem2: LEMMA
  monotonic?(ff) IMPLIES
  (FORALL f: f <= ff(f)  IMPLIES f <= ff(lub(LAMBDA f: f <= ff(f) )))

gfp_thm1: THEOREM
 monotonic?(ff) IMPLIES gfp(ff) <= ff(gfp(ff))


gfp_thm: THEOREM
 monotonic?(ff) IMPLIES ff(gfp(ff)) <= gfp(ff)

gfp_thm2: THEOREM
 monotonic?(ff) IMPLIES (ff(gfp(ff)) = gfp(ff))

gfp_lem3: LEMMA
monotonic?(ff) IMPLIES FORALL f: f <= ff(f) IMPLIES
		             f <= gfp(ff)

gfp_is_gfp: THEOREM
monotonic?(ff) IMPLIES gfp?(ff,gfp(ff))

END mutheorems