merged topology$pairwise and pred_set$pairwise theorems

examples/generic_finite_graphs/fsgraphScript.sml

@@ -1,6 +1,6 @@
 open HolKernel Parse boolLib bossLib;
 
-open pairTheory pred_setTheory sortingTheory genericGraphTheory
+open pairTheory pred_setTheory sortingTheory genericGraphTheory topologyTheory;
 
 val _ = new_theory "fsgraph";
 
@@ -540,19 +540,9 @@ Proof
  >> POP_ASSUM MP_TAC >> SET_TAC []
 QED
 
-(* NOTE: Two disjoint paths may share nodes but not edges. *)
-Definition disjoint_path_def :
-  disjoint_path vs1 vs2 <=> DISJOINT (set (adjpairs vs1)) (set (adjpairs vs2))
-End
-
-Definition disjoint_paths_def :
-  disjoint_paths vss <=> !vs1 vs2. vs1 IN vss /\ vs2 IN vss /\ vs1 <> vs2 /\
-                                   disjoint_path vs1 vs2
-End
-
 Theorem Menger :
-  !g A B. CARD (BIGINTER {X | separate g X A B}) =
-          CARD (BIGUNION {vss | disjoint_paths vss /\
+  !g A B. CARD (BIGINTER {X | separation g X A B}) =
+          CARD (BIGUNION {vss | disjoint (IMAGE set vss) /\
                                 !vs. vs IN vss ==> AB_path g vs A B})
 Proof
     cheat

src/pred_set/src/more_theories/topologyScript.sml

@@ -25,7 +25,7 @@
 open HolKernel Parse bossLib boolLib;
 
 open boolSimps simpLib mesonLib metisLib pairTheory pairLib tautLib
-     pred_setTheory arithmeticTheory cardinalTheory;
+     combinTheory pred_setTheory arithmeticTheory cardinalTheory;
 
 val _ = new_theory "topology";
 
@@ -948,37 +948,178 @@ Proof
 QED
 
 (* ------------------------------------------------------------------------- *)
-(* Pairwise property over sets and lists (from real_topologyTheory)          *)
+(*   Easy lemmas of DISJOINT                                                 *)
 (* ------------------------------------------------------------------------- *)
 
-val _ = hide "pairwise"; (* pred_setTheory *)
+Theorem DISJOINT_RESTRICT_L :
+  !s t c. DISJOINT s t ==> DISJOINT (s INTER c) (t INTER c)
+Proof SET_TAC []
+QED
+
+Theorem DISJOINT_RESTRICT_R :
+  !s t c. DISJOINT s t ==> DISJOINT (c INTER s) (c INTER t)
+Proof SET_TAC []
+QED
+
+Theorem DISJOINT_CROSS_L :
+    !s t c. DISJOINT s t ==> DISJOINT (s CROSS c) (t CROSS c)
+Proof
+    RW_TAC std_ss [DISJOINT_ALT, CROSS_DEF, Once EXTENSION, IN_INTER,
+                   NOT_IN_EMPTY, GSPECIFICATION]
+QED
+
+Theorem DISJOINT_CROSS_R :
+    !s t c. DISJOINT s t ==> DISJOINT (c CROSS s) (c CROSS t)
+Proof
+    RW_TAC std_ss [DISJOINT_ALT, CROSS_DEF, Once EXTENSION, IN_INTER,
+                   NOT_IN_EMPTY, GSPECIFICATION]
+QED
+
+Theorem SUBSET_RESTRICT_L :
+  !r s t. s SUBSET t ==> (s INTER r) SUBSET (t INTER r)
+Proof SET_TAC []
+QED
+
+Theorem SUBSET_RESTRICT_R :
+  !r s t. s SUBSET t ==> (r INTER s) SUBSET (r INTER t)
+Proof SET_TAC []
+QED
+
+Theorem SUBSET_RESTRICT_DIFF :
+  !r s t. s SUBSET t ==> (r DIFF t) SUBSET (r DIFF s)
+Proof SET_TAC []
+QED
+
+Theorem SUBSET_INTER_SUBSET_L :
+  !r s t. s SUBSET t ==> (s INTER r) SUBSET t
+Proof SET_TAC []
+QED
+
+Theorem SUBSET_INTER_SUBSET_R :
+  !r s t. s SUBSET t ==> (r INTER s) SUBSET t
+Proof SET_TAC []
+QED
+
+Theorem SUBSET_MONO_DIFF :
+  !r s t. s SUBSET t ==> (s DIFF r) SUBSET (t DIFF r)
+Proof SET_TAC []
+QED
+
+Theorem SUBSET_DIFF_SUBSET :
+  !r s t. s SUBSET t ==> (s DIFF r) SUBSET t
+Proof SET_TAC []
+QED
+
+Theorem SUBSET_DIFF_DISJOINT :
+  !s1 s2 s3. (s1 SUBSET (s2 DIFF s3)) ==> DISJOINT s1 s3
+Proof
+    PROVE_TAC [SUBSET_DIFF]
+QED
+
+(* ------------------------------------------------------------------------- *)
+(* Disjoint system of sets                                                   *)
+(* ------------------------------------------------------------------------- *)
 
-val pairwise = new_definition ("pairwise",
-  ``pairwise r s <=> !x y. x IN s /\ y IN s /\ ~(x = y) ==> r x y``);
+Overload disjoint = “pairwise DISJOINT”
 
-val PAIRWISE_EMPTY = store_thm ("PAIRWISE_EMPTY",
- ``!r. pairwise r {} <=> T``,
-  REWRITE_TAC[pairwise, NOT_IN_EMPTY] THEN MESON_TAC[]);
+Theorem disjoint_def :
+    !A. disjoint A = !a b. a IN A /\ b IN A /\ (a <> b) ==> DISJOINT a b
+Proof
+    rw [pairwise]
+QED
+
+(* |- !A. disjoint A <=> !a b. a IN A /\ b IN A /\ a <> b ==> (a INTER b = {} ) *)
+Theorem disjoint = REWRITE_RULE [DISJOINT_DEF] disjoint_def
+
+Theorem disjointI :
+    !A. (!a b . a IN A ==> b IN A ==> (a <> b) ==> DISJOINT a b) ==> disjoint A
+Proof
+    METIS_TAC [disjoint_def]
+QED
+
+Theorem disjointD :
+    !A a b. disjoint A ==> a IN A ==> b IN A ==> (a <> b) ==> DISJOINT a b
+Proof
+    METIS_TAC [disjoint_def]
+QED
+
+Theorem disjoint_empty :
+    disjoint {}
+Proof
+    SET_TAC [disjoint_def]
+QED
+
+Theorem disjoint_union :
+    !A B. disjoint A /\ disjoint B /\ (BIGUNION A INTER BIGUNION B = {}) ==>
+          disjoint (A UNION B)
+Proof
+    SET_TAC [disjoint_def]
+QED
+
+Theorem disjoint_sing :
+    !a. disjoint {a}
+Proof
+    SET_TAC [disjoint_def]
+QED
+
+Theorem disjoint_same :
+    !s t. (s = t) ==> disjoint {s; t}
+Proof
+    RW_TAC std_ss [IN_INSERT, IN_SING, disjoint_def]
+QED
 
-val PAIRWISE_SING = store_thm ("PAIRWISE_SING",
- ``!r x. pairwise r {x} <=> T``,
-  REWRITE_TAC[pairwise, IN_SING] THEN MESON_TAC[]);
+Theorem disjoint_two :
+    !s t. s <> t /\ DISJOINT s t ==> disjoint {s; t}
+Proof
+    RW_TAC std_ss [IN_INSERT, IN_SING, disjoint_def]
+ >- ASM_REWRITE_TAC []
+ >> ASM_REWRITE_TAC [DISJOINT_SYM]
+QED
 
-val PAIRWISE_MONO = store_thm ("PAIRWISE_MONO",
- ``!r s t. pairwise r s /\ t SUBSET s ==> pairwise r t``,
-  REWRITE_TAC[pairwise] THEN SET_TAC[]);
+Theorem disjoint_image :
+    !f. (!i j. i <> j ==> DISJOINT (f i) (f j)) ==> disjoint (IMAGE f UNIV)
+Proof
+    rpt STRIP_TAC
+ >> MATCH_MP_TAC disjointI
+ >> RW_TAC std_ss [IN_IMAGE, IN_UNIV]
+ >> METIS_TAC []
+QED
 
-val PAIRWISE_INSERT = store_thm ("PAIRWISE_INSERT",
- ``!r x s.
-        pairwise r (x INSERT s) <=>
-        (!y. y IN s /\ ~(y = x) ==> r x y /\ r y x) /\
-        pairwise r s``,
-  REWRITE_TAC[pairwise, IN_INSERT] THEN MESON_TAC[]);
+Theorem disjoint_insert_imp :
+    !e c. disjoint (e INSERT c) ==> disjoint c
+Proof
+    RW_TAC std_ss [disjoint_def]
+ >> FIRST_ASSUM MATCH_MP_TAC
+ >> METIS_TAC [IN_INSERT]
+QED
 
-val PAIRWISE_IMAGE = store_thm ("PAIRWISE_IMAGE",
- ``!r f. pairwise r (IMAGE f s) <=>
-         pairwise (\x y. ~(f x = f y) ==> r (f x) (f y)) s``,
-  REWRITE_TAC[pairwise, IN_IMAGE] THEN MESON_TAC[]);
+Theorem disjoint_insert_notin :
+    !e c. disjoint (e INSERT c) /\ e NOTIN c ==> !s. s IN c ==> DISJOINT e s
+Proof
+    RW_TAC std_ss [disjoint_def]
+ >> FIRST_ASSUM MATCH_MP_TAC
+ >> METIS_TAC [IN_INSERT]
+QED
+
+Theorem disjoint_insert :
+    !e c. disjoint c /\ (!x. x IN c ==> DISJOINT x e) ==> disjoint (e INSERT c)
+Proof
+    rpt STRIP_TAC
+ >> Q_TAC KNOW_TAC ‘e INSERT c = {e} UNION c’ >- SET_TAC []
+ >> DISCH_THEN (fn th => ONCE_REWRITE_TAC [th])
+ >> MATCH_MP_TAC disjoint_union
+ >> ASM_REWRITE_TAC [disjoint_sing, BIGUNION_SING]
+ >> ASM_SET_TAC []
+QED
+
+Theorem disjoint_restrict :
+    !e c. disjoint c ==> disjoint (IMAGE ($INTER e) c)
+Proof
+    RW_TAC std_ss [disjoint_def, IN_IMAGE, o_DEF]
+ >> MATCH_MP_TAC DISJOINT_RESTRICT_R
+ >> FIRST_X_ASSUM MATCH_MP_TAC >> ASM_REWRITE_TAC []
+ >> CCONTR_TAC >> fs []
+QED
 
 (* ------------------------------------------------------------------------- *)
 (* Useful idioms for being a suitable union/intersection of somethings.      *)
@@ -1739,9 +1880,9 @@ QED
 
 Theorem COUNTABLE_DISJOINT_UNION_OF_IDEMPOT :
    !P:('a->bool)->bool.
-        ((COUNTABLE INTER pairwise DISJOINT) UNION_OF
-         (COUNTABLE INTER pairwise DISJOINT) UNION_OF P) =
-        (COUNTABLE INTER pairwise DISJOINT) UNION_OF P
+        ((COUNTABLE INTER disjoint) UNION_OF
+         (COUNTABLE INTER disjoint) UNION_OF P) =
+        (COUNTABLE INTER disjoint) UNION_OF P
 Proof
   GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN Q.X_GEN_TAC `s:'a->bool` THEN
   reverse EQ_TAC

src/pred_set/src/pred_setScript.sml

@@ -6255,25 +6255,71 @@ Proof
 QED
 
 (* ----------------------------------------------------------------------
-    Assert a predicate on all pairs of elements in a set.
-    Take the RC of the P argument to consider only pairs of distinct elements.
+    Assert a predicate on all (disjoint) pairs of elements in a set.
    ---------------------------------------------------------------------- *)
 
-val pairwise_def = new_definition(
-  "pairwise_def",
-  ``pairwise P s = !e1 e2. e1 IN s /\ e2 IN s ==> P e1 e2``);
+(* NOTE: The involved pairs are now required to be disjoint: ‘e1 <> e2’ *)
+Definition pairwise_def :
+    pairwise P s = !e1 e2. e1 IN s /\ e2 IN s /\ e1 <> e2 ==> P e1 e2
+End
+
+(* HOL-Light's equivalent definition (sets.ml) *)
+Theorem pairwise :
+    !r s. pairwise r s <=> !x y. x IN s /\ y IN s /\ ~(x = y) ==> r x y
+Proof
+    rw [pairwise_def]
+QED
+
+Theorem PAIRWISE_EMPTY :
+    !r. pairwise r {} <=> T
+Proof
+  REWRITE_TAC[pairwise, NOT_IN_EMPTY] THEN MESON_TAC[]
+QED
 
-val pairwise_UNION = Q.store_thm(
-"pairwise_UNION",
-`pairwise R (s1 UNION s2) <=>
- pairwise R s1 /\ pairwise R s2 /\ (!x y. x IN s1 /\ y IN s2 ==> R x y /\ R y x)`,
-SRW_TAC [boolSimps.DNF_ss][pairwise_def] THEN METIS_TAC []);
+Theorem PAIRWISE_SING :
+    !r x. pairwise r {x} <=> T
+Proof
+  REWRITE_TAC[pairwise, IN_SING] THEN MESON_TAC[]
+QED
 
-val pairwise_SUBSET = Q.store_thm(
-"pairwise_SUBSET",
-`!R s t. pairwise R t /\ s SUBSET t ==> pairwise R s`,
-SRW_TAC [][SUBSET_DEF,pairwise_def]);
+(* NOTE: added ‘x <> y’ to adapt the changed definition of ‘pairwise’ *)
+Theorem pairwise_UNION :
+    !R s1 s2. pairwise R (s1 UNION s2) <=>
+              pairwise R s1 /\ pairwise R s2 /\
+             (!x y. x IN s1 /\ y IN s2 /\ x <> y ==> R x y /\ R y x)
+Proof
+    SRW_TAC [boolSimps.DNF_ss][pairwise_def] THEN METIS_TAC []
+QED
 
+Theorem pairwise_SUBSET :
+    !R s t. pairwise R t /\ s SUBSET t ==> pairwise R s
+Proof
+  SRW_TAC [][SUBSET_DEF, pairwise_def]
+QED
+
+Theorem PAIRWISE_MONO :
+    !r s t. pairwise r s /\ t SUBSET s ==> pairwise r t
+Proof
+    rpt STRIP_TAC
+ >> MATCH_MP_TAC pairwise_SUBSET
+ >> Q.EXISTS_TAC ‘s’ >> ASM_REWRITE_TAC []
+QED
+
+Theorem PAIRWISE_INSERT :
+    !r x s.
+        pairwise r (x INSERT s) <=>
+        (!y. y IN s /\ ~(y = x) ==> r x y /\ r y x) /\
+        pairwise r s
+Proof
+  REWRITE_TAC[pairwise, IN_INSERT] THEN MESON_TAC[]
+QED
+
+Theorem PAIRWISE_IMAGE :
+    !r f s. pairwise r (IMAGE f s) <=>
+            pairwise (\x y. ~(f x = f y) ==> r (f x) (f y)) s
+Proof
+  REWRITE_TAC[pairwise, IN_IMAGE] THEN MESON_TAC[]
+QED
 
 (* ----------------------------------------------------------------------
     A proof of Koenig's Lemma

src/probability/martingaleScript.sml

@@ -12,7 +12,7 @@ open pairTheory relationTheory prim_recTheory arithmeticTheory pred_setTheory
      combinTheory fcpTheory hurdUtils;
 
 open realTheory realLib seqTheory transcTheory iterateTheory real_sigmaTheory
-     real_topologyTheory;
+     topologyTheory real_topologyTheory;
 
 open util_probTheory extrealTheory sigma_algebraTheory measureTheory
      real_borelTheory borelTheory lebesgueTheory;

src/probability/measureScript.sml

@@ -21,7 +21,7 @@
 open HolKernel Parse boolLib bossLib;
 
 open prim_recTheory arithmeticTheory optionTheory pairTheory combinTheory
-     pred_setTheory pred_setLib;
+     pred_setTheory pred_setLib topologyTheory;
 
 open realTheory realLib metricTheory seqTheory transcTheory real_sigmaTheory
      real_topologyTheory;

src/probability/real_probabilityScript.sml

@@ -19,7 +19,7 @@ open HolKernel Parse boolLib bossLib;
 open arithmeticTheory prim_recTheory seqTheory res_quanTheory res_quanTools
      listTheory rich_listTheory pairTheory combinTheory realTheory realLib
      optionTheory transcTheory real_sigmaTheory pred_setTheory pred_setLib
-     mesonLib hurdUtils iterateTheory;
+     mesonLib hurdUtils iterateTheory topologyTheory;
 
 open util_probTheory sigma_algebraTheory real_measureTheory real_lebesgueTheory;
 

src/probability/sigma_algebraScript.sml

@@ -2,8 +2,7 @@
 (* The (shared) theory of sigma-algebra and other systems of sets (ring,     *)
 (* semiring, and dynkin system) used in measureTheory/real_measureTheory     *)
 (*                                                                           *)
-(* Author: Chun Tian (2018-2020)                                             *)
-(* Fondazione Bruno Kessler and University of Trento, Italy                  *)
+(* Author: Chun Tian (2018 - 2023)                                           *)
 (* ------------------------------------------------------------------------- *)
 (* Based on the work of Tarek Mhamdi, Osman Hasan, Sofiene Tahar [3]         *)
 (* HVG Group, Concordia University, Montreal (2013, 2015)                    *)
@@ -19,6 +18,8 @@ open HolKernel Parse boolLib bossLib;
 open arithmeticTheory optionTheory pairTheory combinTheory pred_setTheory
      pred_setLib numLib realLib seqTheory hurdUtils util_probTheory;
 
+open topologyTheory;
+
 val _ = new_theory "sigma_algebra";
 
 val DISC_RW_KILL = DISCH_TAC >> ONCE_ASM_REWRITE_TAC [] >> POP_ASSUM K_TAC;