SSL chain.pvs

%-------------------------------------------------------------------------
%
%  Chains (totally ordered subsets of a poset).
%
%  For PVS version 3.2.  January 14, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: orders[chain], orders[T], sets[T]
%  orders: chain[T, <=]
%
%-------------------------------------------------------------------------
chain[T: TYPE, <=: (partial_order?[T])]: THEORY
 BEGIN

  IMPORTING orders[T], sets[T]

  S: VAR set

  % The chain type
  chain?(S): bool = total_order?(restrict[[T, T], [(S), (S)], bool](<=))

  chain: TYPE+ = (chain?) CONTAINING emptyset

  ch, ch1, ch2: VAR chain

  % Maximal chains
  maximal_chain?(ch): bool = NOT (EXISTS ch1: strict_subset?(ch, ch1))

  % Chain properties
  subset_chain: THEOREM FORALL ch, S: subset?(S, ch) => chain?(S)

  intersection_chain: JUDGEMENT intersection(ch1, ch2) HAS_TYPE chain

  % Chain order
  IMPORTING orders[chain]

  chain_order(ch1, ch2): bool = subset?(ch1, ch2)

  chain_order_partial: JUDGEMENT
    chain_order HAS_TYPE (partial_order?[chain])

 END chain