% A simulation of Bruno Dutertre's fixedpoints/mucalculus_prop.
%
% Author: Alfons Geser, National Institute of Aerospace
% Date: Feb 2005

new_mucalculus_prop[T: TYPE]: THEORY

BEGIN

  IMPORTING
    fixed_points[set[T]],
    sets_complete_lattices[T]

  leq_equals_subset: LEMMA <= = subset?[T]

  monotonic_is_monotone: JUDGEMENT
    (monotonic?[T]) SUBTYPE_OF (monotone?(subset?))

  leq_is_complete_lattice: JUDGEMENT
    <= HAS_TYPE (complete_lattice?[set[T]])

  IMPORTING complementary_lattices[set[T], <=]

  C: VAR (complement?(<=))
  F: VAR (monotonic?[T])
  p, q: VAR pred[T]
  x: VAR set[T]
  A: VAR set[pred[T]]

  fixpoint_equals_fixed_point: LEMMA
    fixpoint?(F) = fixed_point?[set[T]](F)

  fixpoint2_equals_fixed_point: LEMMA
    fixpoint?(F, x) = fixed_point?[set[T]](F)(x)

  antisymmetry: LEMMA p <= q AND q <= p IMPLIES p = q

  reflexivity: LEMMA p <= p


  %--- glb(A) is the greatest lower bound of A

  glb_equals_glb: LEMMA glb[T] = glb[set[T]](subset?)

  glb_lower_bound: LEMMA FORALL (q: (A)): glb(A) <= q

  glb_greatest_lower_bound: LEMMA
       p <= glb(A) IFF FORALL (q: (A)): p <= q


  %--- lub(A) is the least upper bound of A 

  lub_equals_lub: LEMMA lub[T] = lub[set[T]](subset?)

  lub_upper_bound: LEMMA FORALL (q: (A)): q <= lub(A)

  lub_least_upper_bound: LEMMA
       lub(A) <= p IFF FORALL (q: (A)): q <= p
  

  %--- properties of mu operator

  mu_equals_least_prefixed_point: LEMMA
    mu(F) = glb[set[T]](<=)(prefixed_point?(<=)(F))

  smallest_closed: PROPOSITION F(p) <= p IMPLIES mu(F) <= p

  fixpoint_mu2: PROPOSITION fixpoint?(F)(mu(F))

  fixpoint_mu1: PROPOSITION F(mu(F)) = mu(F)

  closure_mu: PROPOSITION F(mu(F)) <= mu(F)

  least_fixpoint2: PROPOSITION fixpoint?(F)(p) IMPLIES mu(F) <= p

  least_fixpoint1: PROPOSITION F(p) = p IMPLIES mu(F) <= p

  lfp_equals_lfp: LEMMA lfp?(F) = lfp?[set[T]](<=)(F)

  mu_lfp: JUDGEMENT mu(F) HAS_TYPE (lfp?(F))



  %--- fixed points and dual

  monotonic_dual_monotonic: JUDGEMENT dual(C)(F) HAS_TYPE (monotonic?[T])

  least_fixpoint_dual: PROPOSITION mu(dual(C)(F)) = C(nu(F))

  greatest_fixpoint_dual: PROPOSITION nu(dual(C)(F)) = C(mu(F))

  complement_is_complement: JUDGEMENT
    complement[T] HAS_TYPE (complement?(<=))


  %--- properties of nu operator

  closure_nu: PROPOSITION nu(F) <= F(nu(F))

  largest_closed: PROPOSITION p <= F(p) IMPLIES p <= nu(F)

  fixpoint_nu1: PROPOSITION F(nu(F)) = nu(F)

  fixpoint_nu2: PROPOSITION fixpoint?(F)(nu(F))

  greatest_fixpoint1: PROPOSITION F(p) = p IMPLIES p <= nu(F)

  greatest_fixpoint2: PROPOSITION fixpoint?(F)(p) IMPLIES p <= nu(F)

  nu_gfp: JUDGEMENT nu(F) HAS_TYPE (gfp?(F))

END new_mucalculus_prop