Quelle ordered_finite_sequences.pvs Sprache: PVS

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

quality92%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.