|
%=============================================================================
%
% Mantel's Theorem
% ——————————————————
%
% Author: Aaron Dutle University of South Carolina
%
% Mantel's Theorem states that any graph on N vertices that does not contain
% a triangle can have at most N²/4 edges.
%
% Comment: This is the author's first attempt at proving a theorem using PVS.
% Because of this, some of the proofs are likely longer than needed,
% and some of the organization of the file may be nonstandard.
%
%=============================================================================
mantel[T: TYPE ]: THEORY
BEGIN
IMPORTING graphs[T], graph_ops[T], graph_inductions[T],
graph_deg[T], finite_sets[doubleton[T]], sets[doubleton[T]],
sets_lemmas[doubleton[T]]
x,y,z,w: VAR T
G, GG, GS: VAR graph[T]
e: VAR doubleton[T]
%
% Definitions for use in the proofs.
tri?(G)(x,y,z): bool = vert(G)(x) AND vert(G)(y) AND vert(G)(z)
AND x/=y AND y/=z AND x/=z AND edge?(G)(x,y) AND edge?(G)(y,z) AND edge?(G)(x,z)
tri?(G): bool = EXISTS x,y,z : tri?(G)(x,y,z)
tri?(G)(x,y): bool = EXISTS z : tri?(G)(x,y,z)
del2_vert(G, x,y): graph[T] = del_vert( del_vert(G,x), y)
common_neighbor?(G)(x,y): bool = EXISTS z: x/=z AND y/=z
AND edge?(G)(x,z) AND edge?(G)(y,z)
%
% Three lemmas about the existence of triangles
%
one_to_some: LEMMA (tri?(G)(x,y,z) IMPLIES tri?(G)(x,y) )
some_to_lots: LEMMA (tri?(G)(x,y) IMPLIES tri?(G) )
one_to_lots: LEMMA (tri?(G)(x,y,z) IMPLIES tri?(G))
% The collection of Lemmas used in the proof
exst_tri: LEMMA (edge?(G)(x,y) AND common_neighbor?(G)(x,y)
IMPLIES tri?(G)(x,y))
one_vert_edges: LEMMA singleton?(G) IMPLIES edges(G) = emptyset[doubleton[T]]
edge_adjacent: LEMMA ( edge?(G)(x,y) IMPLIES member(y, adjacent(G,x)))
disj_neighbor_sets: LEMMA ( disjoint?(adjacent(G,x), adjacent(G,y))
IMPLIES NOT common_neighbor?(G)(x,y))
adj_is_subset: LEMMA subset?(union(adjacent(G,x), adjacent(G,y)),vert(G))
adj_is_subset2: LEMMA subset?(adjacent(G,x), vert(G))
no_cn: LEMMA NOT common_neighbor?(G)(x,y)
IMPLIES disjoint?(adjacent(G,x), adjacent(G,y))
disj_adj_card: LEMMA disjoint?(adjacent(G,x), adjacent(G,y))
IMPLIES card(adjacent(G,x))+card(adjacent(G,y))<=size(G)
pre_edges_del21: LEMMA edges(G) = union(edges(del2_vert(G,x,y)),
union(incident_edges(x,G), incident_edges(y,G)))
pre_edges_del22: LEMMA disjoint?(edges(del2_vert(G,x,y)),
union(incident_edges(x,G), incident_edges(y,G)))
edges_del2: LEMMA num_edges(del2_vert(G,x,y))+
card(union(incident_edges(x,G), incident_edges(y,G)))
=num_edges(G)
verts_del2: LEMMA vert(G)(x) AND vert(G)(y) AND x/=y
IMPLIES size(del2_vert(G,x,y)) = size(G)-2
tri_del2: LEMMA tri?(del2_vert(G,x,y)) IMPLIES tri?(G)
int_lem: LEMMA edge?(G)(x,y)
IMPLIES singleton?({e: doubleton[T] |
(edges(G)(e) AND e(x)) AND edges(G)(e) AND e(y)})
card_union: LEMMA edge?(G)(x,y) IMPLIES
card(union(incident_edges(x,G),incident_edges(y,G))) =
card(incident_edges(x,G))+card(incident_edges(y,G))-1
% Used in a previous proof attempt. Not required now.
adj_helper: LEMMA empty?(G) IMPLIES card(adjacent(G,x))=0
% Five lemmas, some with difficult proofs, used to prove the Obvious Fact.
adj_helper2: LEMMA edges(G)=emptyset[doubleton[T]]
IMPLIES card(adjacent(G,x))=0
inc_ind1: LEMMA edges(G)(e) AND NOT e(x) IMPLIES
incident_edges(x, del_edge(G,e)) =
incident_edges(x, G)
adj_ind1: LEMMA edges(G)(e) AND NOT e(x) IMPLIES
adjacent(del_edge(G,e),x)=
adjacent(G,x)
inc_ind2: LEMMA edges(G)(e) AND e(x) IMPLIES
card(incident_edges(x, del_edge(G,e))) =
card(incident_edges(x, G))-1
adj_ind2: LEMMA edges(G)(e) AND e(x) IMPLIES
card(adjacent(del_edge(G,e),x))=
card(adjacent(G,x))-1
% The Obvious Fact.
inc_equals_adj: LEMMA card(incident_edges(x,G)) = card(adjacent(G,x))
%
% Mantel's Theorem. Any graph on N vertices with no triangle has at
% most N^2/4 edges.
%
Mantel: THEOREM ( FORALL G: NOT tri?(G)
IMPLIES num_edges(G)<= size(G)*size(G)/4)
END mantel
¤ Dauer der Verarbeitung: 0.17 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.
|
