|
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
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
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.
|
