Quelle  chain_chain.pvs

%-------------------------------------------------------------------------
%
%  Chain chains: chains of Ts ordered by inclusion.
%
%  For PVS version 3.2.  January 14, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: finite_sets[subchain], orders[chain_chain], orders[subchain],
%    orders[T], relations[subchain], sets[subchain], sets[T]
%  orders: bounded_orders[subchain], chain[subchain,chain_incl],
%    chain[T,<=], chain_chain[T,<=], relations_extra[subchain]
%
%-------------------------------------------------------------------------
chain_chain[T: TYPE, <=: (partial_order?[T])]: THEORY
 BEGIN

  % ==========================================================================
  % The lower level chains
  % ==========================================================================

  IMPORTING chain[T, <=]

  subchain: TYPE+ = chain[T, <=]

  subc1, subc2: VAR subchain


  % ==========================================================================
  % The higher level chains
  % ==========================================================================

  chain_incl(subc1, subc2): bool = subset?(subc1, subc2)

  chain_incl_partial_order: JUDGEMENT
    chain_incl HAS_TYPE (partial_order?[subchain])

  IMPORTING bounded_orders[subchain], chain[subchain, chain_incl]

  chain_chain: TYPE+ = chain[subchain, chain_incl]

  C: VAR chain_chain

  chain_union(C): subchain = Union(extend[set[T], subchain, bool, FALSE](C))

  chain_union_upper_bound: LEMMA
    FORALL (C: chain_chain):
      bounded_orders.upper_bound?(chain_union(C), C, chain_incl)

 END chain_chain