digraphs[T: TYPE]: THEORY %------------------------------------------------------------------------------- % % Defines: % % digraph[T] -- digraph over domain T % vert(G) -- vertices of digraph G % edges(G) -- set of edges in a digraph G % % Authors: % % Ricky W. Butler NASA Langley % Jon Sjogren AFOSR % % Version 1.0 Last modified 12/20/96 % % Maintained by: % % Rick Butler NASA Langley Research Center % R.W.Butler@larc.nasa.gov % % NOTE: % %------------------------------------------------------------------------------- BEGIN IMPORTING finite_sets@finite_sets[T], pairs[T], finite_sets@finite_sets[pair[T]] x,y,v: VAR T edgetype: TYPE = pair[T] % ---------- ALLOW SELF LOOPS ---------- edg(x,(y:{y:T | y /= x})): edgetype = (x,y) predigraph: TYPE = [# vert : finite_set[T], edges: finite_set[edgetype] #] e: VAR edgetype directed_graph: TYPE = {g: predigraph | FORALL e: edges(g)(e) IMPLIES LET (x,y) = e IN vert(g)(x) AND vert(g)(y)} digraph : TYPE = directed_graph simple_digraph: TYPE = {g: digraph | FORALL e: edges(g)(e) IMPLIES LET (x,y) = e IN x /= y} sd_graph : TYPE = simple_digraph G: var digraph % edge?(G)(x,y): bool = x /= y AND edges(G)((x,y)) edge?(G)(x,y): bool = edges(G)((x,y)) edges_vert : LEMMA in?(x,e) AND edges(G)(e) IMPLIES (EXISTS y: vert(G)(y) AND in?(y,e)) other_vert : LEMMA in?(v,e) AND edges(G)(e) IMPLIES (EXISTS (u: T): vert(G)(u) AND e = (u, v) OR e = (v,u)) edges_to_pair : LEMMA edges(G)(e) IMPLIES (EXISTS x,y: edges(G)(x,y) AND vert(G)(x) AND vert(G)(y) AND x = proj_1(e) AND y = proj_2(e)) % -------------- size of digraphs -------------------- size(G): nat = card[T](vert(G)) empty?(G): bool = empty?(vert(G)) singleton?(G): bool = (size(G) = 1) isolated?(G): bool = empty?(edges(G)) empty?_rew : LEMMA empty?(G) = (card(vert(G)) = 0) edges_of_empty : LEMMA empty?(G) IMPLIES edges(G) = emptyset[edgetype] singleton_edges : LEMMA FORALL (SG: simple_digraph): singleton?(SG) IMPLIES empty?(edges(SG)) edge_in_card_gt_1 : LEMMA FORALL (SG: simple_digraph): edges(SG)(e) IMPLIES card(vert(SG)) > 1 not_singleton_2_vert: LEMMA NOT empty?(G) AND NOT singleton?(G) IMPLIES (EXISTS (x,y: T): x /= y AND vert(G)(x) AND vert(G)(y)) proj_rew: LEMMA (proj_1(e), proj_2(e)) = e infdigraph: TYPE = [# vert : set[T], edges: set[edgetype] #] is_digraph(g: infdigraph): bool = is_finite[T](vert(g)) AND is_finite[edgetype](edges(g)) AND (FORALL (e: edgetype): edges(g)(e) IMPLIES (FORALL x: in?(x,e) IMPLIES vert(g)(x))) singleton_digraph(v): digraph = (# vert := singleton[T](v), edges := emptyset[edgetype] #) is_sing: LEMMA singleton?(singleton_digraph(x)) Digraph: TYPE = {g: digraph | nonempty?(vert(g))} END digraphs