% upper semilattices; binary lub function
% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
% Date: Oct 2004

upper_semilattices[
  T: TYPE,
  (IMPORTING bounded_orders[T])
  <=: (upper_semilattice?[T])
]: THEORY

BEGIN

  IMPORTING bounded_sets[T, <=]

  s, t, u, t1, t2: VAR T
  S, S1, S2: VAR (least_bounded_above?[T](<=))

  finite_set_is_least_bounded_above: JUDGEMENT
    non_empty_finite_set[T] SUBTYPE_OF (least_bounded_above?(<=))

  least_upper_bound_singleton: LEMMA
    least_upper_bound?[T](t, singleton(t), <=)

  lub_singleton: LEMMA
    lub(<=)(singleton(t)) = t

  lub(t, u): T = lub[T](<=)(union(singleton(t), singleton(u)))

  lub_le: LEMMA lub(t, u) <= s IFF t <= s AND u <= s
  le_lub_1: LEMMA s <= t => s <= lub(t, u)
  le_lub_2: LEMMA s <= u => s <= lub(t, u)

  union_preserves_bounded_above: JUDGEMENT
    union(S1, S2: (bounded_above?[T](<=))) HAS_TYPE (bounded_above?[T](<=))

  add_preserves_bounded_above: JUDGEMENT
    add(s: T, S: (bounded_above?[T](<=))) HAS_TYPE (bounded_above?[T](<=))

  least_upper_bound_union: LEMMA
    least_upper_bound?[T](t1, S1, <=) &
    least_upper_bound?[T](t2, S2, <=) =>
      least_upper_bound?[T](lub(t1, t2), union(S1, S2), <=)

  least_upper_bound_add: LEMMA
    least_upper_bound?[T](t, S, <=) =>
      least_upper_bound?[T](lub(t, s), add(s, S), <=)

  union_preserves_least_bounded_above: JUDGEMENT
    union(S1, S2) HAS_TYPE (least_bounded_above?[T](<=))

  add_preserves_least_bounded_above: JUDGEMENT
    add(s, S) HAS_TYPE (least_bounded_above?[T](<=))

  lub_union: LEMMA
    lub[T](<=)(union(S1, S2)) = lub(lub[T](<=)(S1), lub[T](<=)(S2))

  lub_add: LEMMA
    lub[T](<=)(add(s, S)) = lub(lub[T](<=)(S), s)

END upper_semilattices