Quelle  ordered_finite_sequences.pvs  Sprache: unbekannt

ordered_finite_sequences[T: TYPE+, <=:(total_order?[T])]: THEORY

  BEGIN

  IMPORTING structures@sort_seq_lems[T, <=], relations_extra[T], finite_seqs[T]

  s, s1, s2: VAR ne_seqs

  consensus_function: TYPE = [s: ne_seqs -> {t: T | min(s) <= t AND t <= max(s)}]

  cf: VAR consensus_function

  k: VAR posnat
  i,j,l: VAR nat

  extract_one: LEMMA 
    i<=j AND i<s`length AND j<s`length AND l<=j-i 
      IMPLIES (s^(i,j))`seq(l) = s`seq(i+l)
  extract_upper: LEMMA 
    i<=j AND i<s`length AND j<s`length 
      IMPLIES (s^(i,j))`seq(length(s^(i,j))-1) = s`seq(j)

  min_extract: LEMMA 
    i<=j AND i<s`length IMPLIES min(sort(s)^(i,j)) = sort(s)`seq(i)
  max_extract: LEMMA 
    i<=j AND i<s`length AND j<s`length 
      IMPLIES max(sort(s)^(i,j)) = sort(s)`seq(j)

  minmax(s): ne_seqs = (: min(s), max(s) :) % uses conversion list2finseq

  min_le_max: LEMMA min(s) <= max(s)

  min_minmax: LEMMA min(minmax(s)) = min(s)
  max_minmax: LEMMA max(minmax(s)) = max(s)

   min_in_consensus: JUDGEMENT min HAS_TYPE in_consensus_function
   max_in_consensus: JUDGEMENT max HAS_TYPE in_consensus_function
   in_consensus:     JUDGEMENT in_consensus_function SUBTYPE_OF consensus_function

  min_consensus:    JUDGEMENT min HAS_TYPE consensus_function
  max_consensus:    JUDGEMENT max HAS_TYPE consensus_function
  choose_consensus: JUDGEMENT choose(i) HAS_TYPE consensus_function
  

  IMPORTING pigeonhole,  
            finite_sets@finite_sets_below, 
            finite_sets@finite_sets_card_eq

  % Set of indexes from the unsorted seq whose value is equal or 
  % lower than the value of given index in the sorted sequence
  lower(s, k, (i: below(k))): finite_set[below(k)] = 
    {j: below(k) | s`length = k AND s`seq(j) <= sort(s)`seq(i)}
  upper(s, k, (i: below(k))): finite_set[below(k)] = 
    {j: below(k) | s`length = k AND sort(s)`seq(i) <= s`seq(j)}

  % Map a set of indexes from the sorted sequence into a set of indexes 
  % in the unsorted seq
  map_set(s, k, (a: finite_set[below(k)])): finite_set[below(k)] =
    {i: below(k) | s`length = k AND a(sort_map(s)(i))}

  map_subset_lower: LEMMA
      i<k AND s`length = k 
    IMPLIES 
      subset?(map_set(s, k, {m:below(k) | m <= i}), lower(s, k, i))

  map_subset_upper: LEMMA
      i<k AND s`length = k 
    IMPLIES 
      subset?(map_set(s, k, {m:below(k) | i <= m}), upper(s, k, i))

  % a bijective mapping function for a subset of below(k)
  mapper(s, k, (a: finite_set[below(k)]))(i:(map_set(s,k,a))): (a) = sort_map(s)(i)

  map_card_eq: LEMMA
    FORALL (a:finite_set[below(k)]):
      s`length = k 
    IMPLIES 
      card(map_set(s, k, a)) = card(a)
  
  card_below_set: LEMMA i < k IMPLIES i+1 <= card({m:below(k) | m <= i})
  card_above_set: LEMMA i < k IMPLIES k-i <= card({m:below(k) | i <= m})

  card_lower: LEMMA i < k AND s`length = k IMPLIES i + 1 <= card[below(k)](lower(s, k, i)) 
  card_upper: LEMMA i < k AND s`length = k IMPLIES k - i <= card[below(k)](upper(s, k, i))

  sort_overlap: LEMMA
      s1`length = k AND
      s2`length = k
    IMPLIES
      FORALL (i: below(k)): 
        EXISTS (j: below(k)):
          s2`seq(j) <= sort(s2)`seq(i) AND
            sort(s1)`seq(i) <= s1`seq(j)

  leq_validity: COROLLARY
      s`length = k 
    IMPLIES
      FORALL (i: below(k)): 
        EXISTS (j: below(k)):
          s`seq(j) <= sort(s)`seq(i) 

  END ordered_finite_sequences