% lower semilattices; binary glb function
% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
% Date: Oct 2004 / Jan 2005

lower_semilattices[
  T: TYPE,
  (IMPORTING bounded_orders[T])
  <=: (lower_semilattice?[T])
]: THEORY

BEGIN

  IMPORTING bounded_sets[T, <=]

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

  finite_set_is_greatest_bounded_below: JUDGEMENT
    non_empty_finite_set[T] SUBTYPE_OF (greatest_bounded_below?(<=))

  greatest_lower_bound_singleton: LEMMA
    greatest_lower_bound?[T](t, singleton(t), <=)

  glb_singleton: LEMMA
    glb(<=)(singleton(t)) = t

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

  le_glb: LEMMA s <= glb(t, u) IFF s <= t AND s <= u
  glb_le_1: LEMMA t <= s => glb(t, u) <= s
  glb_le_2: LEMMA u <= s => glb(t, u) <= s

  union_preserves_bounded_below: JUDGEMENT
    union(S1, S2: (bounded_below?[T](<=))) HAS_TYPE (bounded_below?[T](<=))

  add_preserves_bounded_below: JUDGEMENT
    add(s: T, S: (bounded_below?[T](<=))) HAS_TYPE (bounded_below?[T](<=))

  greatest_lower_bound_union: LEMMA
    greatest_lower_bound?[T](t1, S1, <=) &
    greatest_lower_bound?[T](t2, S2, <=) =>
      greatest_lower_bound?[T](glb(t1, t2), union(S1, S2), <=)

  greatest_lower_bound_add: LEMMA
    greatest_lower_bound?[T](t, S, <=) =>
      greatest_lower_bound?[T](glb(t, s), add(s, S), <=)

  union_preserves_greatest_bounded_below: JUDGEMENT
    union(S1, S2) HAS_TYPE (greatest_bounded_below?[T](<=))

  add_preserves_greatest_bounded_below: JUDGEMENT
    add(s, S) HAS_TYPE (greatest_bounded_below?[T](<=))

  glb_union: LEMMA
    glb[T](<=)(union(S1, S2)) = glb(glb[T](<=)(S1), glb[T](<=)(S2))

  glb_add: LEMMA
    glb[T](<=)(add(s, S)) = glb(glb[T](<=)(S), s)

END lower_semilattices