Quelle  select_minmax.pvs

%
%
% Purpose : properties of the min/max of the results 
%           from a set of parallel nodes
%
%

select_minmax[N: posnat, T: TYPE+, <=: (total_order?[T])]: THEORY

  BEGIN

  IMPORTING
    finite_sets@finite_sets_minmax[T, <=],
    node[N, T],
    relations_extra[T]

  node_set: VAR non_empty_finite_set[below(N)]
  v: VAR vec
  n: VAR below(N)
  t: VAR T

  v_min(v, node_set): T = min(image(v, node_set))

  v_max(v, node_set): T = max(image(v, node_set))

  v_min_witness: LEMMA
    EXISTS n: node_set(n) AND v_min(v, node_set) = v(n)

  v_max_witness: LEMMA
    EXISTS n: node_set(n) AND v_max(v, node_set) = v(n)

  v_min_is_min: LEMMA
    node_set(n) IMPLIES v_min(v, node_set) <= v(n)

  v_max_is_max: LEMMA
    node_set(n) IMPLIES v(n) <= v_max(v, node_set)

  min_le_max: LEMMA
    v_min(v, node_set) <= v_max(v, node_set)

  min_le_max_alt: LEMMA
    v_max(v, node_set) = v_min(v, node_set) IFF
      (v_max(v, node_set) <= v_min(v, node_set))

  v_minmax_choose: LEMMA
    uniform?(v, t)(node_set) IFF 
      (v_max(v, node_set) = v_min(v, node_set) AND v_min(v, node_set) = t)

  v_minmax_choose_alt: LEMMA
    uniform?(v, t)(node_set) IFF 
      (v_max(v, node_set) <= t AND t <= v_min(v, node_set))

  END select_minmax