Defined the notion of relative boundary (hom_relboundary) and hence

proved the exact homology sequence for a triple of spaces. The proof
(following the very explicit one in Hu's "Homology Theory" pp. 32-37)
just works from the standard Eilenberg-Steenrod axioms.

Also added a few miscellaneous missing "real real" theorems (they
existed for R^1 but not R!) and even one list triviality. New definitions
and theorems:

        GROUP_HOMOMORPHISM_HOM_RELBOUNDARY
        HOMOLOGY_EXACTNESS_TRIPLE_1
        HOMOLOGY_EXACTNESS_TRIPLE_2
        HOMOLOGY_EXACTNESS_TRIPLE_3
        HOM_RELBOUNDARY
        HOM_RELBOUNDARY_EMPTY
        MEM_REPLICATE
        NATURALITY_HOM_INDUCED_RELBOUNDARY
        REAL_CONTINUOUS_ON_MAX
        REAL_CONTINUOUS_ON_MIN
        REAL_INDEFINITE_INTEGRAL_CONTINUOUS
        hom_relboundary

CHANGES

@@ -8,11 +8,18 @@
   * page: https://github.com/jrh13/hol-light/commits/master         *
   * *****************************************************************
 
+Sat 24th Mar 2018       lists.ml
+
+Added a trivial but sometimes convenient list theorem:
+
+  MEM_REPLICATE =
+   |- !n x y:A. MEM x (REPLICATE n y) <=> x = y /\ ~(n = 0)
+
 Sat 10th Mar 2018       int.ml
 
 Added a somewhat surprising missing lemma:
 
-  INT_MUL_EQ_1 = 
+  INT_MUL_EQ_1 =
     |- !x y:int. x * y = &1 <=> x = &1 /\ y = &1 \/ x = --(&1) /\ y = --(&1)
 
 Sat 10th Feb 2018       iterate.ml, Library/grouptheory.ml,

Multivariate/complex_database.ml

@@ -6386,6 +6386,7 @@ theorems :=
 "GROUP_HOMOMORPHISM_HOM_INDUCED",GROUP_HOMOMORPHISM_HOM_INDUCED;
 "GROUP_HOMOMORPHISM_HOM_INDUCED_EMPTY",GROUP_HOMOMORPHISM_HOM_INDUCED_EMPTY;
 "GROUP_HOMOMORPHISM_HOM_INDUCED_REDUCED",GROUP_HOMOMORPHISM_HOM_INDUCED_REDUCED;
+"GROUP_HOMOMORPHISM_HOM_RELBOUNDARY",GROUP_HOMOMORPHISM_HOM_RELBOUNDARY;
 "GROUP_HOMOMORPHISM_ID",GROUP_HOMOMORPHISM_ID;
 "GROUP_HOMOMORPHISM_INTO_SUBGROUP",GROUP_HOMOMORPHISM_INTO_SUBGROUP;
 "GROUP_HOMOMORPHISM_INTO_SUBGROUP_EQ",GROUP_HOMOMORPHISM_INTO_SUBGROUP_EQ;
@@ -7792,6 +7793,9 @@ theorems :=
 "HOMOLOGY_EXACTNESS_REDUCED_1",HOMOLOGY_EXACTNESS_REDUCED_1;
 "HOMOLOGY_EXACTNESS_REDUCED_2",HOMOLOGY_EXACTNESS_REDUCED_2;
 "HOMOLOGY_EXACTNESS_REDUCED_3",HOMOLOGY_EXACTNESS_REDUCED_3;
+"HOMOLOGY_EXACTNESS_TRIPLE_1",HOMOLOGY_EXACTNESS_TRIPLE_1;
+"HOMOLOGY_EXACTNESS_TRIPLE_2",HOMOLOGY_EXACTNESS_TRIPLE_2;
+"HOMOLOGY_EXACTNESS_TRIPLE_3",HOMOLOGY_EXACTNESS_TRIPLE_3;
 "HOMOLOGY_EXCISION_AXIOM",HOMOLOGY_EXCISION_AXIOM;
 "HOMOLOGY_HOMOTOPY_AXIOM",HOMOLOGY_HOMOTOPY_AXIOM;
 "HOMOLOGY_HOMOTOPY_EMPTY",HOMOLOGY_HOMOTOPY_EMPTY;
@@ -7985,6 +7989,8 @@ theorems :=
 "HOM_INDUCED_REDUCED",HOM_INDUCED_REDUCED;
 "HOM_INDUCED_RESTRICT",HOM_INDUCED_RESTRICT;
 "HOM_INDUCED_TRIVIAL",HOM_INDUCED_TRIVIAL;
+"HOM_RELBOUNDARY",HOM_RELBOUNDARY;
+"HOM_RELBOUNDARY_EMPTY",HOM_RELBOUNDARY_EMPTY;
 "HP",HP;
 "HREAL_ADD_AC",HREAL_ADD_AC;
 "HREAL_ADD_ASSOC",HREAL_ADD_ASSOC;
@@ -11027,6 +11033,7 @@ theorems :=
 "MEM_LINEAR_IMAGE",MEM_LINEAR_IMAGE;
 "MEM_LIST_OF_SET",MEM_LIST_OF_SET;
 "MEM_MAP",MEM_MAP;
+"MEM_REPLICATE",MEM_REPLICATE;
 "MEM_TRANSLATION",MEM_TRANSLATION;
 "METRIC",METRIC;
 "METRIC_BAIRE_CATEGORY",METRIC_BAIRE_CATEGORY;
@@ -11267,6 +11274,7 @@ theorems :=
 "NADD_SUC",NADD_SUC;
 "NADD_UBOUND",NADD_UBOUND;
 "NATURALITY_HOM_INDUCED",NATURALITY_HOM_INDUCED;
+"NATURALITY_HOM_INDUCED_RELBOUNDARY",NATURALITY_HOM_INDUCED_RELBOUNDARY;
 "NATURALITY_SIMPLICIAL_SUBDIVISION",NATURALITY_SIMPLICIAL_SUBDIVISION;
 "NATURALITY_SINGULAR_SUBDIVISION",NATURALITY_SINGULAR_SUBDIVISION;
 "NEARBY_INVERTIBLE_MATRIX",NEARBY_INVERTIBLE_MATRIX;
@@ -13379,6 +13387,8 @@ theorems :=
 "REAL_CONTINUOUS_ON_INVERSE_ALT",REAL_CONTINUOUS_ON_INVERSE_ALT;
 "REAL_CONTINUOUS_ON_LMUL",REAL_CONTINUOUS_ON_LMUL;
 "REAL_CONTINUOUS_ON_LOG",REAL_CONTINUOUS_ON_LOG;
+"REAL_CONTINUOUS_ON_MAX",REAL_CONTINUOUS_ON_MAX;
+"REAL_CONTINUOUS_ON_MIN",REAL_CONTINUOUS_ON_MIN;
 "REAL_CONTINUOUS_ON_MUL",REAL_CONTINUOUS_ON_MUL;
 "REAL_CONTINUOUS_ON_NEG",REAL_CONTINUOUS_ON_NEG;
 "REAL_CONTINUOUS_ON_POLYNOMIAL_FUNCTION",REAL_CONTINUOUS_ON_POLYNOMIAL_FUNCTION;
@@ -13661,6 +13671,7 @@ theorems :=
 "REAL_HREAL_LEMMA1",REAL_HREAL_LEMMA1;
 "REAL_HREAL_LEMMA2",REAL_HREAL_LEMMA2;
 "REAL_IMP_CNJ",REAL_IMP_CNJ;
+"REAL_INDEFINITE_INTEGRAL_CONTINUOUS",REAL_INDEFINITE_INTEGRAL_CONTINUOUS;
 "REAL_INDEFINITE_INTEGRAL_CONTINUOUS_LEFT",REAL_INDEFINITE_INTEGRAL_CONTINUOUS_LEFT;
 "REAL_INDEFINITE_INTEGRAL_CONTINUOUS_RIGHT",REAL_INDEFINITE_INTEGRAL_CONTINUOUS_RIGHT;
 "REAL_INFSUM",REAL_INFSUM;
@@ -17331,6 +17342,7 @@ theorems :=
 "higher_complex_derivative_alt",higher_complex_derivative_alt;
 "higher_real_derivative",higher_real_derivative;
 "holomorphic_on",holomorphic_on;
+"hom_relboundary",hom_relboundary;
 "homeomorphic",homeomorphic;
 "homeomorphic_map",homeomorphic_map;
 "homeomorphic_maps",homeomorphic_maps;

Multivariate/multivariate_database.ml

@@ -5375,6 +5375,7 @@ theorems :=
 "GROUP_HOMOMORPHISM_HOM_INDUCED",GROUP_HOMOMORPHISM_HOM_INDUCED;
 "GROUP_HOMOMORPHISM_HOM_INDUCED_EMPTY",GROUP_HOMOMORPHISM_HOM_INDUCED_EMPTY;
 "GROUP_HOMOMORPHISM_HOM_INDUCED_REDUCED",GROUP_HOMOMORPHISM_HOM_INDUCED_REDUCED;
+"GROUP_HOMOMORPHISM_HOM_RELBOUNDARY",GROUP_HOMOMORPHISM_HOM_RELBOUNDARY;
 "GROUP_HOMOMORPHISM_ID",GROUP_HOMOMORPHISM_ID;
 "GROUP_HOMOMORPHISM_INTO_SUBGROUP",GROUP_HOMOMORPHISM_INTO_SUBGROUP;
 "GROUP_HOMOMORPHISM_INTO_SUBGROUP_EQ",GROUP_HOMOMORPHISM_INTO_SUBGROUP_EQ;
@@ -6308,6 +6309,9 @@ theorems :=
 "HOMOLOGY_EXACTNESS_REDUCED_1",HOMOLOGY_EXACTNESS_REDUCED_1;
 "HOMOLOGY_EXACTNESS_REDUCED_2",HOMOLOGY_EXACTNESS_REDUCED_2;
 "HOMOLOGY_EXACTNESS_REDUCED_3",HOMOLOGY_EXACTNESS_REDUCED_3;
+"HOMOLOGY_EXACTNESS_TRIPLE_1",HOMOLOGY_EXACTNESS_TRIPLE_1;
+"HOMOLOGY_EXACTNESS_TRIPLE_2",HOMOLOGY_EXACTNESS_TRIPLE_2;
+"HOMOLOGY_EXACTNESS_TRIPLE_3",HOMOLOGY_EXACTNESS_TRIPLE_3;
 "HOMOLOGY_EXCISION_AXIOM",HOMOLOGY_EXCISION_AXIOM;
 "HOMOLOGY_HOMOTOPY_AXIOM",HOMOLOGY_HOMOTOPY_AXIOM;
 "HOMOLOGY_HOMOTOPY_EMPTY",HOMOLOGY_HOMOTOPY_EMPTY;
@@ -6479,6 +6483,8 @@ theorems :=
 "HOM_INDUCED_REDUCED",HOM_INDUCED_REDUCED;
 "HOM_INDUCED_RESTRICT",HOM_INDUCED_RESTRICT;
 "HOM_INDUCED_TRIVIAL",HOM_INDUCED_TRIVIAL;
+"HOM_RELBOUNDARY",HOM_RELBOUNDARY;
+"HOM_RELBOUNDARY_EMPTY",HOM_RELBOUNDARY_EMPTY;
 "HP",HP;
 "HREAL_ADD_AC",HREAL_ADD_AC;
 "HREAL_ADD_ASSOC",HREAL_ADD_ASSOC;
@@ -9242,6 +9248,7 @@ theorems :=
 "MEM_LINEAR_IMAGE",MEM_LINEAR_IMAGE;
 "MEM_LIST_OF_SET",MEM_LIST_OF_SET;
 "MEM_MAP",MEM_MAP;
+"MEM_REPLICATE",MEM_REPLICATE;
 "MEM_TRANSLATION",MEM_TRANSLATION;
 "METRIC",METRIC;
 "METRIC_BAIRE_CATEGORY",METRIC_BAIRE_CATEGORY;
@@ -9467,6 +9474,7 @@ theorems :=
 "NADD_SUC",NADD_SUC;
 "NADD_UBOUND",NADD_UBOUND;
 "NATURALITY_HOM_INDUCED",NATURALITY_HOM_INDUCED;
+"NATURALITY_HOM_INDUCED_RELBOUNDARY",NATURALITY_HOM_INDUCED_RELBOUNDARY;
 "NATURALITY_SIMPLICIAL_SUBDIVISION",NATURALITY_SIMPLICIAL_SUBDIVISION;
 "NATURALITY_SINGULAR_SUBDIVISION",NATURALITY_SINGULAR_SUBDIVISION;
 "NEARBY_INVERTIBLE_MATRIX",NEARBY_INVERTIBLE_MATRIX;
@@ -13947,6 +13955,7 @@ theorems :=
 "has_vector_derivative",has_vector_derivative;
 "hausdist",hausdist;
 "hausdorff_space",hausdorff_space;
+"hom_relboundary",hom_relboundary;
 "homeomorphic",homeomorphic;
 "homeomorphic_map",homeomorphic_map;
 "homeomorphic_maps",homeomorphic_maps;

Multivariate/realanalysis.ml

@@ -2393,6 +2393,23 @@ let REAL_CONTINUOUS_ON_ABS = prove
   REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
   SIMP_TAC[REAL_CONTINUOUS_ABS]);;
 
+let REAL_CONTINUOUS_ON_MAX = prove
+ (`!f g s. f real_continuous_on s /\ g real_continuous_on s
+           ==> (\x. max (f x) (g x)) real_continuous_on s`,
+  REPEAT STRIP_TAC THEN
+  REWRITE_TAC[REAL_ARITH `max a b = inv(&2) * (a + b + abs(b - a))`] THEN
+  MATCH_MP_TAC REAL_CONTINUOUS_ON_LMUL THEN
+  REPEAT(MATCH_MP_TAC REAL_CONTINUOUS_ON_ADD THEN ASM_REWRITE_TAC[]) THEN
+  MATCH_MP_TAC REAL_CONTINUOUS_ON_ABS THEN
+  MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN ASM_REWRITE_TAC[]);;
+
+let REAL_CONTINUOUS_ON_MIN = prove
+ (`!f g s. f real_continuous_on s /\ g real_continuous_on s
+           ==> (\x. min (f x) (g x)) real_continuous_on s`,
+  REPEAT STRIP_TAC THEN
+  REWRITE_TAC[REAL_ARITH `min a b = --(max (--a) (--b))`] THEN
+  ASM_SIMP_TAC[REAL_CONTINUOUS_ON_MAX; REAL_CONTINUOUS_ON_NEG]);;
+
 let REAL_CONTINUOUS_ON_EQ = prove
  (`!f g s. (!x. x IN s ==> f(x) = g(x)) /\ f real_continuous_on s
            ==> g real_continuous_on s`,
@@ -9781,6 +9798,39 @@ let HAS_REAL_INTEGRAL_UNIONS = prove
   DISCH_THEN SUBST1_TAC THEN
   REWRITE_TAC[o_DEF; GSYM IMAGE_o; IMAGE_LIFT_DROP]);;
 
+let REAL_INDEFINITE_INTEGRAL_CONTINUOUS = prove
+ (`!f a b c d e.
+        f real_integrable_on real_interval[a,b] /\
+        c IN real_interval[a,b] /\
+        d IN real_interval[a,b] /\
+        &0 < e
+        ==> ?k. &0 < k /\
+                !c' d'. c' IN real_interval[a,b] /\
+                        d' IN real_interval[a,b] /\
+                        abs(c' - c) <= k /\ abs(d' - d) <= k
+                      ==> abs(real_integral (real_interval[c',d']) f -
+                              real_integral (real_interval[c,d]) f) < e`,
+  REPEAT STRIP_TAC THEN
+  MP_TAC(ISPECL
+   [`lift o f o drop`; `lift a`; `lift b`; `lift c`; `lift d`; `e:real`]
+        INDEFINITE_INTEGRAL_CONTINUOUS) THEN
+  ASM_REWRITE_TAC[GSYM REAL_INTEGRABLE_ON; GSYM IMAGE_LIFT_REAL_INTERVAL] THEN
+  ASM_SIMP_TAC[FUN_IN_IMAGE] THEN
+  MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:real` THEN
+  REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
+  REWRITE_TAC[IMP_IMP; RIGHT_IMP_FORALL_THM; GSYM LIFT_SUB; NORM_LIFT] THEN
+  STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
+  MAP_EVERY X_GEN_TAC [`c':real`; `d':real`] THEN STRIP_TAC THEN
+  FIRST_X_ASSUM(MP_TAC o SPECL [`c':real`; `d':real`]) THEN
+  ASM_REWRITE_TAC[NORM_1; DROP_SUB] THEN
+  MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
+  AP_TERM_TAC THEN BINOP_TAC THEN CONV_TAC SYM_CONV THEN
+  REWRITE_TAC[GSYM IMAGE_LIFT_REAL_INTERVAL] THEN
+  MATCH_MP_TAC REAL_INTEGRAL THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
+   (REWRITE_RULE[IMP_CONJ] REAL_INTEGRABLE_ON_SUBINTERVAL)) THEN
+  REWRITE_TAC[SUBSET; IN_REAL_INTERVAL] THEN
+  RULE_ASSUM_TAC(REWRITE_RULE[IN_REAL_INTERVAL]) THEN ASM_REAL_ARITH_TAC);;
+
 let REAL_MONOTONE_CONVERGENCE_INCREASING = prove
  (`!f:num->real->real g s.
         (!k. (f k) real_integrable_on s) /\

database.ml

@@ -1298,6 +1298,7 @@ theorems :=
 "MEM_FILTER",MEM_FILTER;
 "MEM_LIST_OF_SET",MEM_LIST_OF_SET;
 "MEM_MAP",MEM_MAP;
+"MEM_REPLICATE",MEM_REPLICATE;
 "MIN",MIN;
 "MINIMAL",MINIMAL;
 "MK_REC_INJ",MK_REC_INJ;

lists.ml

@@ -297,6 +297,11 @@ let LENGTH_REPLICATE = prove
  (`!n x. LENGTH(REPLICATE n x) = n`,
   INDUCT_TAC THEN ASM_REWRITE_TAC[LENGTH; REPLICATE]);;
 
+let MEM_REPLICATE = prove
+ (`!n x y:A. MEM x (REPLICATE n y) <=> x = y /\ ~(n = 0)`,
+  INDUCT_TAC THEN ASM_REWRITE_TAC[MEM; REPLICATE; NOT_SUC] THEN
+  MESON_TAC[]);;
+
 let EX_MAP = prove
  (`!P f l. EX P (MAP f l) <=> EX (P o f) l`,
   GEN_TAC THEN GEN_TAC THEN