From 662e116d179857bb053f797be332fc9297a9e250 Mon Sep 17 00:00:00 2001
From: Chun Tian <binghe.lisp@gmail.com>
Date: Fri, 18 Aug 2023 00:05:48 +0200
Subject: [PATCH] Move disjoint_def to pred_setTheory with new proofs

---
 .../src/more_theories/topologyScript.sml      | 161 +-----------------
 src/pred_set/src/pred_setScript.sml           | 104 +++++++++++
 src/probability/util_probScript.sml           |  65 +++++++
 3 files changed, 170 insertions(+), 160 deletions(-)

diff --git a/src/pred_set/src/more_theories/topologyScript.sml b/src/pred_set/src/more_theories/topologyScript.sml
index 384672f648..258a6d927b 100644
--- a/src/pred_set/src/more_theories/topologyScript.sml
+++ b/src/pred_set/src/more_theories/topologyScript.sml
@@ -1023,166 +1023,7 @@ Theorem PAIRWISE_UNION :
            pairwise R s /\ pairwise R t /\
            (!x y. x IN s DIFF t /\ y IN t DIFF s ==> R x y /\ R y x)
 Proof
-  REWRITE_TAC[pairwise] >> SET_TAC[]
-QED
-
-(* ------------------------------------------------------------------------- *)
-(*  Disjoint system of sets (‘disjoint’, originally from Isabelle/HOL)       *)
-(* ------------------------------------------------------------------------- *)
-
-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
-
-Overload disjoint = “pairwiseD DISJOINT”
-
-Theorem disjoint_def :
-    !A. disjoint A = !a b. a IN A /\ b IN A /\ (a <> b) ==> DISJOINT a b
-Proof
-    RW_TAC std_ss [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
-    rw [PAIRWISE_EMPTY]
-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
-    rw [PAIRWISE_SING]
-QED
-
-Theorem disjoint_same :
-    !s t. (s = t) ==> disjoint {s; t}
-Proof
-    RW_TAC std_ss [IN_INSERT, IN_SING, disjoint_def]
-QED
-
-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 [DISJOINT_SYM]
-QED
-
-Theorem disjoint_image :
-    !f. (!i j. i <> j ==> DISJOINT (f i) (f j)) ==> disjoint (IMAGE f UNIV)
-Proof
-    rw [PAIRWISE_IMAGE, pairwise]
-QED
-
-Theorem disjoint_insert_imp :
-    !e c. disjoint (e INSERT c) ==> disjoint c
-Proof
-    rw [PAIRWISE_INSERT]
-QED
-
-Theorem disjoint_insert_notin :
-    !e c. disjoint (e INSERT c) /\ e NOTIN c ==> !s. s IN c ==> DISJOINT e s
-Proof
-    rw [PAIRWISE_INSERT]
- >> METIS_TAC []
-QED
-
-Theorem disjoint_insert :
-    !e c. disjoint c /\ (!x. x IN c ==> DISJOINT x e) ==> disjoint (e INSERT c)
-Proof
-    rw [PAIRWISE_INSERT]
- >> rw [Once DISJOINT_SYM]
-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 []
+  REWRITE_TAC[pairwise] THEN SET_TAC[]
 QED
 
 (* ------------------------------------------------------------------------- *)
diff --git a/src/pred_set/src/pred_setScript.sml b/src/pred_set/src/pred_setScript.sml
index fa3eb1d688..a7af48c86e 100644
--- a/src/pred_set/src/pred_setScript.sml
+++ b/src/pred_set/src/pred_setScript.sml
@@ -6263,6 +6263,110 @@ Proof
   REWRITE_TAC[pairwise_def, NOT_IN_EMPTY] THEN MESON_TAC[]
 QED
 
+(* ------------------------------------------------------------------------- *)
+(*  Disjoint system of sets (‘disjoint’, originally from Isabelle/HOL)       *)
+(* ------------------------------------------------------------------------- *)
+
+Definition disjoint :
+    disjoint = pairwise (RC DISJOINT)
+End
+
+Theorem disjoint_def :
+    !A. disjoint A = !a b. a IN A /\ b IN A /\ (a <> b) ==> DISJOINT a b
+Proof
+    RW_TAC std_ss [disjoint, pairwise_def, RC_DEF]
+ >> METIS_TAC []
+QED
+
+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
+    rw [disjoint, pairwise_EMPTY]
+QED
+
+Theorem disjoint_sing :
+    !a. disjoint {a}
+Proof
+    rw [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
+
+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 [DISJOINT_SYM]
+QED
+
+Theorem disjoint_union :
+    !A B. disjoint A /\ disjoint B /\ (BIGUNION A INTER BIGUNION B = {}) ==>
+          disjoint (A UNION B)
+Proof
+    rw [disjoint_def, DISJOINT_DEF] >> rw []
+ >> (Q.PAT_X_ASSUM ‘_ = {}’ MP_TAC >>
+     rw [Once EXTENSION, IN_BIGUNION] \\
+     rw [Once EXTENSION] >> METIS_TAC [])
+QED
+
+Theorem disjoint_image :
+    !f. (!i j. i <> j ==> DISJOINT (f i) (f j)) ==> disjoint (IMAGE f UNIV)
+Proof
+    rw [disjoint_def, DISJOINT_DEF]
+ >> FIRST_X_ASSUM MATCH_MP_TAC
+ >> CCONTR_TAC >> fs []
+QED
+
+Theorem disjoint_insert_imp :
+    !e c. disjoint (e INSERT c) ==> disjoint c
+Proof
+    rw [disjoint_def, DISJOINT_DEF]
+QED
+
+Theorem disjoint_insert_notin :
+    !e c. disjoint (e INSERT c) /\ e NOTIN c ==> !s. s IN c ==> DISJOINT e s
+Proof
+    rw [disjoint_def, DISJOINT_DEF]
+ >> FIRST_X_ASSUM MATCH_MP_TAC >> rw []
+ >> CCONTR_TAC >> fs []
+QED
+
+Theorem disjoint_insert :
+    !e c. disjoint c /\ (!x. x IN c ==> DISJOINT x e) ==> disjoint (e INSERT c)
+Proof
+    rw [disjoint_def, DISJOINT_DEF] >> rw []
+ >> ONCE_REWRITE_TAC [INTER_COMM]
+ >> FIRST_X_ASSUM MATCH_MP_TAC >> rw []
+QED
+
+Theorem disjoint_restrict :
+    !e c. disjoint c ==> disjoint (IMAGE ($INTER e) c)
+Proof
+    rw [disjoint_def, o_DEF, DISJOINT_DEF]
+ >> ‘x <> x'’ by (CCONTR_TAC >> fs [])
+ >> ‘e INTER x INTER (e INTER x') = e INTER (x INTER x')’
+     by METIS_TAC [INTER_ASSOC, INTER_COMM, INTER_IDEMPOT]
+ >> POP_ASSUM (fn th => ONCE_REWRITE_TAC [th])
+ >> SUFF_TAC “x INTER x' = {}” >- rw []
+ >> FIRST_X_ASSUM MATCH_MP_TAC >> rw []
+QED
+
 (* ----------------------------------------------------------------------
     A proof of Koenig's Lemma
    ---------------------------------------------------------------------- *)
diff --git a/src/probability/util_probScript.sml b/src/probability/util_probScript.sml
index ded3625585..daf52af879 100644
--- a/src/probability/util_probScript.sml
+++ b/src/probability/util_probScript.sml
@@ -146,6 +146,71 @@ val GBIGUNION_IMAGE = store_thm
    ``!s p n. {s | ?n. p s n} = BIGUNION (IMAGE (\n. {s | p s n}) UNIV)``,
    RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_BIGUNION_IMAGE, IN_UNIV]);
 
+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
+
 (* ------------------------------------------------------------------------- *)
 (* Binary Unions                                                             *)
 (* ------------------------------------------------------------------------- *)