Generalized definition of bipartite graphs with explicit partitions

examples/generic_graphs/fsgraphScript.sml

@@ -729,7 +729,7 @@ Overload V[local] = “nodes (g :fsgraph)”
 Overload E[local] = “fsgedges (g :fsgraph)”
 
 Theorem fsgraph_valid :
-    !g n1 n2. {n1;n2} IN E ==> n1 IN V /\ n2 IN V /\ n1 <> n2
+    !(g :fsgraph) n1 n2. {n1;n2} IN E ==> n1 IN V /\ n2 IN V /\ n1 <> n2
 Proof
     rpt GEN_TAC
  >> DISCH_THEN (STRIP_ASSUME_TAC o MATCH_MP alledges_valid)
@@ -741,31 +741,57 @@ QED
    NOTE: ‘partitions’ requires that each partiton must be non-empty. This is not
    explicitly mentioned in the textbook but seems reasonable.
  *)
-Definition partite_def :
-    partite r (g :fsgraph) <=>
-      ?v. v partitions (nodes g) /\ CARD v = r /\
-          !n1 n2. {n1;n2} IN fsgedges g ==> part v n1 <> part v n2
+Definition gen_partite_def :
+    gen_partite r (g :fsgraph) v <=>
+      v partitions (nodes g) /\ CARD v = r /\
+      !n1 n2. {n1;n2} IN fsgedges g ==> part v n1 <> part v n2
 End
 
+Definition partite :
+    partite r (g :fsgraph) <=> ?v. gen_partite r g v
+End
+
+(* |- !r g.
+        partite r g <=>
+        ?v. v partitions V /\ CARD v = r /\
+            !n1 n2. {n1; n2} IN E ==> part v n1 <> part v n2
+ *)
+Theorem partite_def = REWRITE_RULE [gen_partite_def] partite
+
 (* "Instead of '2-partite' one usually says bipartite." *)
 Overload bipartite = “partite 2”
 
-Theorem bipartite_def :
-    !g. bipartite (g :fsgraph) <=>
-        ?A B. DISJOINT A B /\ A <> {} /\ B <> {} /\ A UNION B = nodes g /\
-              !n1 n2. {n1;n2} IN fsgedges g ==>
-                      (n1 IN A /\ n2 IN B) \/ (n1 IN B /\ n2 IN A)
+Definition gen_bipartite :
+    gen_bipartite (g :fsgraph) A B = gen_partite 2 g {A; B}
+End
+
+Theorem gen_bipartite_partitions[local] :
+    !g :fsgraph v. gen_partite 2 g v ==> ?A B. gen_bipartite g A B
+Proof
+    rw [gen_partite_def]
+ >> ‘FINITE V’ by rw []
+ >> ‘FINITE v’ by PROVE_TAC [partitions_FINITE]
+ >> gs [CARDEQ2]
+ >> qexistsl_tac [‘a’, ‘b’]
+ >> rw [gen_bipartite, gen_partite_def]
+QED
+
+Theorem gen_bipartite_def :
+    !g A B. gen_bipartite (g :fsgraph) A B <=>
+            DISJOINT A B /\ A <> {} /\ B <> {} /\ A UNION B = nodes g /\
+            !n1 n2. {n1;n2} IN fsgedges g ==>
+                    (n1 IN A /\ n2 IN B) \/ (n1 IN B /\ n2 IN A)
 Proof
-    rw [partite_def]
+    rw [gen_bipartite, gen_partite_def]
  >> EQ_TAC >> simp []
  >- (STRIP_TAC \\
     ‘FINITE V’ by rw [] \\
+     qabbrev_tac ‘v = {A; B}’ \\
     ‘FINITE v’ by PROVE_TAC [partitions_FINITE] \\
-     fs [CARDEQ2] >> rename1 ‘v = {A; B}’ >> gvs [] \\
-     qexistsl_tac [‘A’, ‘B’] \\
+     fs [CARDEQ2] >> gvs [Abbr ‘v’] \\
      CONJ_ASM1_TAC (* DISJOINT A B *)
      >- (MATCH_MP_TAC partitions_DISJOINT \\
-         qexistsl_tac [‘{A;B}’, ‘V’] >> rw []) \\
+         qexistsl_tac [‘{A; B}’, ‘V’] >> rw []) \\
      CONJ_TAC (* A <> {} *) >- fs [partitions_PAIR_DISJOINT] \\
      CONJ_TAC (* B <> {} *) >- fs [partitions_PAIR_DISJOINT] \\
      CONJ_ASM1_TAC (* A UNION B = V *)
@@ -799,14 +825,9 @@ Proof
          DISCH_THEN (fs o wrap o SYM)) \\
      ASM_SET_TAC [])
  >> STRIP_TAC
- >> Q.EXISTS_TAC ‘{A; B}’
  >> CONJ_ASM1_TAC (* {A; B} partitions V *)
  >- (rw [partitions_PAIR_DISJOINT] >- art [] \\
      rw [Once DISJOINT_SYM])
- >> CONJ_TAC
- >- (rw [CARDEQ2] \\
-     qexistsl_tac [‘A’, ‘B’] >> art [] \\
-     CCONTR_TAC >> fs [DISJOINT_EMPTY_REFL_RWT])
  >> rpt STRIP_TAC
  >> ‘n1 IN V /\ n2 IN V /\ n1 <> n2’ by PROVE_TAC [fsgraph_valid]
  >> Q.PAT_X_ASSUM ‘!n1 n2. P’ (MP_TAC o Q.SPECL [‘n1’, ‘n2’]) >> rw []
@@ -832,6 +853,42 @@ Proof
       DISCH_THEN (fs o wrap o SYM) ]
 QED
 
+Theorem gen_bipartite_alt :
+    !g A B. gen_bipartite (g :fsgraph) A B <=>
+            DISJOINT A B /\ A <> {} /\ B <> {} /\ A UNION B = nodes g /\
+            !e. e IN fsgedges g ==> ?n1 n2. e = {n1; n2} /\ n1 IN A /\ n2 IN B
+Proof
+    rw [gen_bipartite_def]
+ >> EQ_TAC >> rw []
+ >| [ (* goal 1 (of 2) *)
+      MP_TAC (Q.SPEC ‘g’ alledges_valid) >> rw [] \\
+      Q.PAT_X_ASSUM ‘!n1 n2. P’ (MP_TAC o Q.SPECL [‘a’, ‘b’]) >> rw []
+      >- (qexistsl_tac [‘a’, ‘b’] >> art []) \\
+      qexistsl_tac [‘b’, ‘a’] >> art [] \\
+      rw [INSERT2_lemma],
+      (* goal 2 (of 2) *)
+      Q.PAT_X_ASSUM ‘!e. P’ (MP_TAC o Q.SPEC ‘{n1; n2}’) >> rw [] \\
+      gvs [INSERT2_lemma] ]
+QED
+
+Theorem bipartite_def :
+    !g. bipartite (g :fsgraph) <=>
+        ?A B. DISJOINT A B /\ A <> {} /\ B <> {} /\ A UNION B = nodes g /\
+              !n1 n2. {n1;n2} IN fsgedges g ==>
+                      (n1 IN A /\ n2 IN B) \/ (n1 IN B /\ n2 IN A)
+Proof
+    Q.X_GEN_TAC ‘g’
+ >> EQ_TAC
+ >- (rw [partite] \\
+    ‘?A B. gen_bipartite g A B’ by METIS_TAC [gen_bipartite_partitions] \\
+     fs [gen_bipartite_def] \\
+     qexistsl_tac [‘A’, ‘B’] >> rw [])
+ >> rw [partite]
+ >> Q.EXISTS_TAC ‘{A; B}’
+ >> REWRITE_TAC [GSYM gen_bipartite]
+ >> rw [gen_bipartite_def]
+QED
+
 Theorem bipartite_alt :
     !g. bipartite (g :fsgraph) <=>
         ?A B. DISJOINT A B /\ A <> {} /\ B <> {} /\ A UNION B = nodes g /\