Quelle matroids.pvs Sprache: PVS

matroids[T: TYPE]: THEORY
%------------------------------------------------------------------------------
%
% Experimental Theory
%
% Author: Jon Sjogren, Rick Butler
%
%------------------------------------------------------------------------------

BEGIN

IMPORTING  finite_sets@finite_sets_eq[T,T]

  pre_matroid: TYPE = [# elem: finite_set[T],
                         indep: [finite_set[T] -> bool]  #]

  indep_in_elem(M: pre_matroid): bool = (FORALL (A:finite_set[T]):
                                         indep(M)(A) IMPLIES subset?(A,elem(M)))

  indep_subset(M: pre_matroid): bool = (FORALL (A,B:finite_set[T]):
                    indep(M)(A) and subset?(B,A) IMPLIES indep(M)(B))

  indep_card(M: pre_matroid): bool = (FORALL (A,B:finite_set[T]):
             indep(M)(A) AND indep(M)(B) AND card(A) < card(B)
                 IMPLIES (Exists (x: T): elem(M)(x) AND A(x) AND NOT B(x)
                                         AND indep(M)(add(x,B))))

  Matroid: TYPE = {M: pre_matroid | indep_in_elem(M) AND
                                    indep_subset(M) AND
                                    indep_card(M)}

  x,y: VAR T

  single(x): finite_set[T] = {t: T | t = x}

  double(x,y): finite_set[T] = {t: T | t = x OR t = y}

  simple?(M: Matroid): bool = (FORALL x: elem(M)(x) IMPLIES
                                         (indep(M)(single(x)) AND
                                          (FORALL y: x /=y IMPLIES
                                                  indep(M)(double(x,y)))))

  Simple_matroid: TYPE = {M: Matroid | simple?(M)}

  A,B: VAR finite_set[T]
  Subsets(A): TYPE = {B: finite_set[T] | subset?(B,A)}

  M1,M2: VAR Matroid

  extend(M1,M2,(f:[(elem(M1)) -> (elem(M2))])):
                          [Subsets(elem(M1)) -> finite_set[T]] =
           (LAMBDA (A: Subsets(elem(M1))): {t: T | (EXISTS (a: (A)): f(a) = t)})

  isomorph(M1,M2): TYPE = {f: [(elem(M1)) -> (elem(M2))] |
                         bijective?(f) AND
                         (FORALL (A: Subsets(elem(M1))): indep(M1)(A) IFF
                                              indep(M2)(extend(M1,M2,f)(A)))}

% A circuit is a non-independent set such that when you remove any element,
% it becomes independent.

  circuit?(M: Matroid, A: finite_set[T]): bool = subset?(A,elem(M))
                                                 AND NOT indep(M)(A) AND
                                                 (FORALL (x: (elem(M))): A(x)
                                                    IMPLIES indep(M)(remove(x,A)))

  M: VAR Matroid

  circuit_test: LEMMA circuit?(M,A) IMPLIES (subset?(A,elem(M)) AND
                      NOT indep(M)(A) AND (subset?(B,A) and B /= A
                  IMPLIES indep(M)(B)))

circuit_test2: LEMMA  (subset?(A,elem(M)) AND
                      NOT indep(M)(A) AND
                      FORALL B: (subset?(B,A) AND B /= A IMPLIES indep(M)(B)))
                         IMPLIES circuit?(M,A)

End matroids

quality71%

¤ Dauer der Verarbeitung: 0.12 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.