From 64b350e7bed1981a138c02c8d49b2b01c6055f0a Mon Sep 17 00:00:00 2001
From: Chun Tian <binghe.lisp@gmail.com>
Date: Fri, 8 Sep 2023 12:42:32 +1000
Subject: [PATCH] Fixed duplicated theorems after the forbidden "rebinds"
 changes

---
 src/probability/measureScript.sml       | 11 ++++++-----
 src/probability/real_borelScript.sml    |  9 ++++++---
 src/real/analysis/integrationScript.sml |  6 ------
 3 files changed, 12 insertions(+), 14 deletions(-)

diff --git a/src/probability/measureScript.sml b/src/probability/measureScript.sml
index 4c211dc657..04ee3ab5ae 100644
--- a/src/probability/measureScript.sml
+++ b/src/probability/measureScript.sml
@@ -5446,7 +5446,7 @@ val _ = reveal "C";
 
 (*** measure_space Theorems ***)
 
-Theorem measure_space_eq' : (* was: measure_space_measure_eq *)
+Theorem measure_space_measure_eq :
     !sp sts u v. measure_space (sp,sts,u) /\ (!s. s IN sts ==> u s = v s) ==>
                  measure_space (sp,sts,v)
 Proof
@@ -5460,10 +5460,10 @@ Theorem measure_space_cong:
                  (measure_space (sp,sts,u) <=> measure_space (sp,sts,v))
 Proof
     rw[] >> eq_tac >> rw[]
- >> dxrule_at_then (Pos $ el 1) irule measure_space_eq' >> simp[]
+ >> dxrule_at_then (Pos $ el 1) irule measure_space_measure_eq >> simp[]
 QED
 
-Theorem measure_space_add:
+Theorem measure_space_add':
     !a mu nu p. measure_space (space a,subsets a,mu) /\
                 measure_space (space a,subsets a,nu) /\
                (!s. s IN subsets a ==> p s = mu s + nu s) ==>
@@ -5489,11 +5489,12 @@ Proof
         measure_space (space a,subsets a,m)’ suffices_by (rw[] >>
         last_x_assum $ drule_then assume_tac >> pop_assum $ drule_all_then assume_tac >> simp[]) >>
     Induct_on ‘s’ >> rw[]
-    >- (fs[EXTREAL_SUM_IMAGE_EMPTY] >> irule measure_space_eq' \\
+    >- (fs[EXTREAL_SUM_IMAGE_EMPTY] >> irule measure_space_measure_eq \\
         qexists_tac ‘K 0’ >> simp[] >> dxrule_then assume_tac measure_space_trivial >>
         fs[sigma_finite_measure_space_def,K_DEF]) >>
     last_x_assum $ qspecl_then [‘a’,‘f’,‘\t. EXTREAL_SUM_IMAGE (C f t) s’] assume_tac >> rfs[] >>
-    irule measure_space_add >> qexistsl_tac [‘f e’,‘(\t. EXTREAL_SUM_IMAGE (C f t) s)’] >>
+    irule measure_space_add' >>
+    qexistsl_tac [‘f e’,‘(\t. EXTREAL_SUM_IMAGE (C f t) s)’] >>
     simp[] >> qx_gen_tac ‘t’ >> rw[] >>
     qspecl_then [‘C f t’,‘s’,‘e’]
         (fn th => assume_tac th >> rfs[DELETE_NON_ELEMENT_RWT] >> pop_assum irule) $
diff --git a/src/probability/real_borelScript.sml b/src/probability/real_borelScript.sml
index a2e979f206..d245b1def9 100644
--- a/src/probability/real_borelScript.sml
+++ b/src/probability/real_borelScript.sml
@@ -1489,8 +1489,11 @@ Proof
  >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
 QED
 
-(* cf. borelTheory.in_borel_measurable_imp' for measure_space version *)
-Theorem in_borel_measurable_open :
+(* cf. borelTheory.in_borel_measurable_imp' for measure_space version
+
+   NOTE: theorem renamed due to name conflicts with HVG's work.
+ *)
+Theorem in_borel_measurable_open_imp : (* was: in_borel_measurable_open *)
     !a f. sigma_algebra a /\
          (!s. open s ==> (PREIMAGE f s) INTER space a IN subsets a) ==>
           f IN measurable a borel
@@ -1506,7 +1509,7 @@ Theorem in_borel_measurable_continuous_on : (* was: borel_measurable_continuous_
     !f. f continuous_on UNIV ==> f IN measurable borel borel
 Proof
     rpt STRIP_TAC
- >> MATCH_MP_TAC in_borel_measurable_open
+ >> MATCH_MP_TAC in_borel_measurable_open_imp
  >> rw [sigma_algebra_borel]
  >> Know `open {x | x IN UNIV /\ f x IN s}`
  >- (MATCH_MP_TAC CONTINUOUS_OPEN_PREIMAGE (* key lemma *) \\
diff --git a/src/real/analysis/integrationScript.sml b/src/real/analysis/integrationScript.sml
index bc618a84db..d51a87d384 100644
--- a/src/real/analysis/integrationScript.sml
+++ b/src/real/analysis/integrationScript.sml
@@ -18860,12 +18860,6 @@ val HAS_BOUNDED_VARIATION_ON_REFLECT_INTERVAL = store_thm ("HAS_BOUNDED_VARIATIO
   REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_BOUNDED_VARIATION_ON_REFLECT THEN
   ASM_REWRITE_TAC[REFLECT_INTERVAL]);
 
-val VECTOR_VARIATION_REFLECT_INTERVAL = store_thm ("VECTOR_VARIATION_REFLECT_INTERVAL",
- ``!f:real->real a b.
-        vector_variation (interval[a,b]) (\x. f(-x)) =
-        vector_variation (interval[-b,-a]) f``,
-  REWRITE_TAC[VECTOR_VARIATION_REFLECT, REFLECT_INTERVAL]);
-
 val HAS_BOUNDED_VARIATION_COMPOSE_DECREASING = store_thm ("HAS_BOUNDED_VARIATION_COMPOSE_DECREASING",
  ``!f g:real->real a b.
         (!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ x <= y