max_di_subgraphs[T: TYPE]: THEORY BEGIN IMPORTING di_subgraphs[T], max_upto G: VAR digraph[T] Gpred(G): TYPE = {P: pred[digraph[T]] | (EXISTS (S: digraph[T]): di_subgraph?(S,G) AND P(S))} n: VAR nat is_one_of_size(G: digraph[T], P: Gpred(G),n: nat): bool = (EXISTS (S: di_subgraph(G)): P(S) AND size(S) = n) prep0: LEMMA FORALL (G: digraph[T], P: Gpred(G)): nonempty?[upto[size(G)]]({n: upto[size(G)] | is_one_of_size(G,P,n)}) max_size(G: digraph[T], P: Gpred(G)): upto[size(G)] = max({n: upto[size(G)] | is_one_of_size(G,P,n)}) prep : LEMMA FORALL (G: digraph[T], P: Gpred(G)): nonempty?[di_subgraph(G)]({S: di_subgraph(G) | size[T](S) = max_size(G,P) AND P(S)}) maximal?(G: digraph[T], S: di_subgraph(G),P: Gpred(G)): bool = P(S) AND (FORALL (SS: di_subgraph(G)): P(SS) IMPLIES size(SS) <= size(S)) % Existence TCC satisfied by % choose({S: di_subgraph(G) | size(S) = max_size AND P(S)}) max_di_subgraph(G: digraph[T], P: Gpred(G)): {S: di_subgraph(G) | maximal?(G,S,P)} max_di_subgraph_def : LEMMA FORALL (P: Gpred(G)): maximal?(G,max_di_subgraph(G,P),P) max_di_subgraph_in : LEMMA FORALL (P: Gpred(G)): P(max_di_subgraph(G,P)) max_di_subgraph_is_max : LEMMA FORALL (P: Gpred(G)): (FORALL (SS: di_subgraph(G)): P(SS) IMPLIES size(SS) <= size(max_di_subgraph(G,P))) END max_di_subgraphs