graph_connected[T: TYPE]: THEORY BEGIN IMPORTING graph_ops[T], graph_deg[T], walks[T], graph_conn_defs[T], graph_conn_piece, graph_piece_path, % FOR PROOF ONLY graph_path_conn, graph_complected % FOR PROOF ONLY G,G1,G2,H1,H2: VAR graph[T] conn_eq_path : THEOREM connected?(G) = path_connected?(G) path_eq_piece : THEOREM path_connected?(G) = piece_connected?(G) piece_eq_conn : THEOREM piece_connected?(G) = connected?(G) conn_eq_complected : THEOREM connected?(G) = complected?(G) %WHERE (defined in graph_conn_defs[T]) % % connected?(G): RECURSIVE bool = singleton?(G) OR % (EXISTS (v: (vert(G))): deg(v,G) > 0 % AND connected?(del_vert(G,v))) % MEASURE size(G) % % path_connected?(G): bool = (FORALL (x,y: (vert(G))): x /= y IMPLIES % (EXISTS (w: Walk(G)): seq(w)(0) = x AND % seq(w)(l(w)-1) = y)) % % piece_connected?(G): bool = NOT empty?(G) AND % (FORALL H1,H2: G = union(H1,H2) AND % NOT empty?(H1) AND NOT empty?(H2) % IMPLIES NOT empty?(intersection(vert(H1), % vert(H2)))) % % complected?(G): bool = IF isolated?(G) THEN singleton?(G) % ELSIF (EXISTS (v: (vert(G))): deg(v,G) = 1) THEN % (EXISTS (x: (vert(G))): deg(x,G) = 1 AND % connected?(del_vert(G,x))) % ELSE % (EXISTS (e: (edges(G))): % connected?(del_edge(G,e))) % ENDIF % % are defined in graph_conn_defs.pvs END graph_connected