diff --git a/CHANGES b/CHANGES index 8d46713d..da1df2a7 100644 --- a/CHANGES +++ b/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, diff --git a/Multivariate/complex_database.ml b/Multivariate/complex_database.ml index e157dc2e..9ff40a99 100644 --- a/Multivariate/complex_database.ml +++ b/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; diff --git a/Multivariate/homology.ml b/Multivariate/homology.ml index 77e9f790..45481229 100644 --- a/Multivariate/homology.ml +++ b/Multivariate/homology.ml @@ -6152,6 +6152,442 @@ let HOMOLOGY_ADDITIVITY_EXPLICIT = prove CONTINUOUS_MAP_FROM_SUBTOPOLOGY; CONTINUOUS_MAP_ID] THEN REWRITE_TAC[o_DEF]]);; +(* ------------------------------------------------------------------------- *) +(* Generalize exact homology sequence to triples (derived from E-S axioms) *) +(* ------------------------------------------------------------------------- *) + +let hom_relboundary = new_definition + `hom_relboundary p (top:A topology,s,t) = + hom_induced (p - &1) (subtopology top s,{}) (subtopology top s,t) (\x. x) o + hom_boundary p (top,s)`;; + +let GROUP_HOMOMORPHISM_HOM_RELBOUNDARY = prove + (`!p top s t:A->bool. + group_homomorphism + (relative_homology_group (p,top,s), + relative_homology_group (p - &1,subtopology top s,t)) + (hom_relboundary p (top,s,t))`, + REPEAT GEN_TAC THEN REWRITE_TAC[hom_relboundary] THEN + MATCH_MP_TAC GROUP_HOMOMORPHISM_COMPOSE THEN + EXISTS_TAC `homology_group(p - &1,subtopology top (s:A->bool))` THEN + REWRITE_TAC[GROUP_HOMOMORPHISM_HOM_BOUNDARY; GROUP_HOMOMORPHISM_HOM_INDUCED; + homology_group]);; + +let HOM_RELBOUNDARY = prove + (`!p top s t c. + hom_relboundary p (top,s,t) c IN + group_carrier (relative_homology_group (p - &1,subtopology top s,t))`, + REWRITE_TAC[hom_relboundary; o_THM; HOM_INDUCED]);; + +let HOM_RELBOUNDARY_EMPTY = prove + (`!p top s:A->bool. + hom_relboundary p (top,s,{}) = hom_boundary p (top,s)`, + SIMP_TAC[hom_relboundary; o_DEF; HOM_INDUCED_ID; HOM_BOUNDARY; + GSYM homology_group; ETA_AX]);; + +let NATURALITY_HOM_INDUCED_RELBOUNDARY = prove + (`!p top s t top' u v (f:A->B). + continuous_map(top,top') f /\ IMAGE f s SUBSET u /\ IMAGE f t SUBSET v + ==> hom_relboundary p (top',u,v) o + hom_induced p (top,s) (top',u) f = + hom_induced (p - &1) (subtopology top s,t) (subtopology top' u,v) f o + hom_relboundary p (top,s,t)`, + REPEAT STRIP_TAC THEN + ASM_SIMP_TAC[hom_relboundary; GSYM o_ASSOC; NATURALITY_HOM_INDUCED] THEN + REWRITE_TAC[o_ASSOC] THEN AP_THM_TAC THEN AP_TERM_TAC THEN + W(MP_TAC o PART_MATCH (rand o rand) HOM_INDUCED_COMPOSE o lhand o snd) THEN + W(MP_TAC o PART_MATCH (rand o rand) + HOM_INDUCED_COMPOSE o rand o rand o snd) THEN + ASM_SIMP_TAC[IMAGE_CLAUSES; IMAGE_ID; EMPTY_SUBSET; INTER_SUBSET; + CONTINUOUS_MAP_ID; CONTINUOUS_MAP_IN_SUBTOPOLOGY; + CONTINUOUS_MAP_FROM_SUBTOPOLOGY; TOPSPACE_SUBTOPOLOGY; SET_RULE + `IMAGE f s SUBSET t ==> IMAGE f (u INTER s) SUBSET t`] THEN + REPEAT(DISCH_THEN(SUBST1_TAC o SYM)) THEN REWRITE_TAC[o_DEF]);; + +let HOMOLOGY_EXACTNESS_TRIPLE_1 = prove + (`!p top s t:A->bool. + t SUBSET s + ==> group_exactness(relative_homology_group(p,top,t), + relative_homology_group(p,top,s), + relative_homology_group(p - &1,subtopology top s,t)) + (hom_induced p (top,t) (top,s) (\x. x), + hom_relboundary p (top,s,t))`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[group_exactness; GROUP_HOMOMORPHISM_HOM_RELBOUNDARY; + GROUP_HOMOMORPHISM_HOM_INDUCED] THEN + REWRITE_TAC[group_image; group_kernel] THEN + MATCH_MP_TAC SUBSET_ANTISYM THEN GEN_REWRITE_TAC BINOP_CONV [SUBSET] THEN + REWRITE_TAC[FORALL_IN_IMAGE] THEN REWRITE_TAC[IN_IMAGE; IN_ELIM_THM] THEN + CONJ_TAC THENL + [X_GEN_TAC `b:((num->real)->A)frag->bool` THEN DISCH_TAC THEN + REWRITE_TAC[HOM_INDUCED; hom_relboundary] THEN + GEN_REWRITE_TAC LAND_CONV [GSYM o_THM] THEN REWRITE_TAC[GSYM o_ASSOC] THEN + ASM_SIMP_TAC[NATURALITY_HOM_INDUCED; IMAGE_ID; CONTINUOUS_MAP_ID] THEN + REWRITE_TAC[o_THM] THEN + MP_TAC(ISPECL [`p - &1:int`; `subtopology top (s:A->bool)`; `t:A->bool`] + HOMOLOGY_EXACTNESS_AXIOM_3) THEN + ASM_SIMP_TAC[SUBTOPOLOGY_SUBTOPOLOGY; SET_RULE + `t SUBSET s ==> s INTER t = t`] THEN + REWRITE_TAC[group_exactness; group_kernel; group_image] THEN + DISCH_THEN(MATCH_MP_TAC o MATCH_MP (SET_RULE + `P /\ Q /\ IMAGE f s = {y | y IN t /\ g y = z} + ==> !x. x IN s ==> g(f x) = z`)) THEN + REWRITE_TAC[HOM_BOUNDARY]; + ALL_TAC] THEN + X_GEN_TAC `x:((num->real)->A)frag->bool` THEN + REWRITE_TAC[hom_relboundary; o_THM] THEN STRIP_TAC THEN + MP_TAC(ISPECL + [`p - &1:int`; `subtopology top (s:A->bool)`; `t:A->bool`] + HOMOLOGY_EXACTNESS_AXIOM_3) THEN + REWRITE_TAC[group_exactness; group_kernel; group_image] THEN + DISCH_THEN(MP_TAC o SPEC `hom_boundary p (top,s:A->bool) x` o + MATCH_MP (SET_RULE + `P /\ Q /\ IMAGE f s = {y | y IN t /\ g y = z} + ==> !x. x IN t /\ g x = z ==> ?y. y IN s /\ f y = x`)) THEN + ASM_REWRITE_TAC[HOM_BOUNDARY] THEN + ASM_SIMP_TAC[SUBTOPOLOGY_SUBTOPOLOGY; SET_RULE + `t SUBSET s ==> s INTER t = t`] THEN + DISCH_THEN(X_CHOOSE_THEN + `y:((num->real)->A)frag->bool` STRIP_ASSUME_TAC) THEN + MP_TAC(ISPECL + [`p:int`; `top:A topology`; `t:A->bool`] + HOMOLOGY_EXACTNESS_AXIOM_2) THEN + REWRITE_TAC[group_exactness; group_kernel; group_image] THEN + DISCH_THEN(MP_TAC o MATCH_MP (SET_RULE + `P /\ Q /\ IMAGE f s = {y | y IN t /\ g y = z} + ==> !x. x IN t /\ g x = z ==> ?y. y IN s /\ f y = x`)) THEN + DISCH_THEN(MP_TAC o SPEC `y:((num->real)->A)frag->bool`) THEN + ASM_REWRITE_TAC[] THEN ANTS_TAC THENL + [MP_TAC(ISPECL + [`p:int`; `top:A topology`; `s:A->bool`] + HOMOLOGY_EXACTNESS_AXIOM_2) THEN + REWRITE_TAC[group_exactness; group_kernel; group_image] THEN + DISCH_THEN(MP_TAC o MATCH_MP (SET_RULE + `P /\ Q /\ IMAGE f s = {y | y IN t /\ g y = z} + ==> !x. x IN s ==> g(f x) = z`)) THEN + DISCH_THEN(MP_TAC o SPEC `x:((num->real)->A)frag->bool`) THEN + ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EQ_TRANS) THEN + FIRST_X_ASSUM(fun th -> + GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [SYM th]) THEN + GEN_REWRITE_TAC RAND_CONV [GSYM o_THM] THEN AP_THM_TAC THEN + W(MP_TAC o PART_MATCH (rand o rand) HOM_INDUCED_COMPOSE o rand o snd) THEN + SIMP_TAC[CONTINUOUS_MAP_ID; CONTINUOUS_MAP_IN_SUBTOPOLOGY; + CONTINUOUS_MAP_FROM_SUBTOPOLOGY; IMAGE_ID; EMPTY_SUBSET] THEN + REWRITE_TAC[TOPSPACE_SUBTOPOLOGY] THEN + ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN(SUBST1_TAC o SYM)] THEN + REWRITE_TAC[o_DEF]; + DISCH_THEN(X_CHOOSE_THEN `z:((num->real)->A)frag->bool` + STRIP_ASSUME_TAC)] THEN + MP_TAC(ISPECL [`p:int`; `top:A topology`; `s:A->bool`] + HOMOLOGY_EXACTNESS_AXIOM_1) THEN + REWRITE_TAC[group_exactness; group_kernel; group_image] THEN + DISCH_THEN(MP_TAC o MATCH_MP (SET_RULE + `P /\ Q /\ IMAGE f s = {y | y IN t /\ g y = z} + ==> !x. x IN t /\ g x = z ==> ?y. y IN s /\ f y = x`)) THEN + DISCH_THEN(MP_TAC o SPEC + `group_div (relative_homology_group (p,top,s)) x + (hom_induced p (top,t) (top,s) (\x:A. x) z)`) THEN + ASM_SIMP_TAC[GROUP_DIV; HOM_INDUCED; HOM_BOUNDARY; + MATCH_MP GROUP_HOMOMORPHISM_DIV + (SPEC_ALL GROUP_HOMOMORPHISM_HOM_BOUNDARY); + GROUP_RULE `group_div G x y = group_id G <=> y = x`] THEN + ANTS_TAC THENL + [GEN_REWRITE_TAC LAND_CONV [GSYM o_THM] THEN + ASM_SIMP_TAC[NATURALITY_HOM_INDUCED; IMAGE_ID; CONTINUOUS_MAP_ID] THEN + ASM_REWRITE_TAC[o_THM]; + DISCH_THEN(X_CHOOSE_THEN `w:((num->real)->A)frag->bool` + STRIP_ASSUME_TAC)] THEN + EXISTS_TAC `group_mul (relative_homology_group (p,top,t)) z + (hom_induced p (top,{}) (top,t) (\x:A. x) w)` THEN + ASM_SIMP_TAC[GROUP_MUL; HOM_INDUCED; + MATCH_MP GROUP_HOMOMORPHISM_MUL + (SPEC_ALL GROUP_HOMOMORPHISM_HOM_INDUCED)] THEN + W(MP_TAC o PART_MATCH (lhand o rand) + (REWRITE_RULE[abelian_group] ABELIAN_RELATIVE_HOMOLOGY_GROUP) o + rand o snd) THEN + REWRITE_TAC[HOM_INDUCED] THEN DISCH_THEN SUBST1_TAC THEN + ASM_SIMP_TAC[GROUP_MUL; HOM_INDUCED; + GROUP_RULE `x = group_mul G z y <=> group_div G x y = z`] THEN + FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN + GEN_REWRITE_TAC RAND_CONV [GSYM o_THM] THEN AP_THM_TAC THEN + W(MP_TAC o PART_MATCH (rand o rand) HOM_INDUCED_COMPOSE o rand o snd) THEN + SIMP_TAC[CONTINUOUS_MAP_ID; CONTINUOUS_MAP_IN_SUBTOPOLOGY; + CONTINUOUS_MAP_FROM_SUBTOPOLOGY; IMAGE_ID; EMPTY_SUBSET] THEN + REWRITE_TAC[TOPSPACE_SUBTOPOLOGY] THEN + ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN(SUBST1_TAC o SYM)] THEN + REWRITE_TAC[o_DEF]);; + +let HOMOLOGY_EXACTNESS_TRIPLE_2 = prove + (`!p top s t:A->bool. + t SUBSET s + ==> group_exactness(relative_homology_group(p,top,s), + relative_homology_group(p - &1,subtopology top s,t), + relative_homology_group(p - &1,top,t)) + (hom_relboundary p (top,s,t), + hom_induced (p - &1) (subtopology top s,t) (top,t) (\x. x))`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[group_exactness; GROUP_HOMOMORPHISM_HOM_RELBOUNDARY; + GROUP_HOMOMORPHISM_HOM_INDUCED] THEN + REWRITE_TAC[group_image; group_kernel] THEN + MATCH_MP_TAC SUBSET_ANTISYM THEN GEN_REWRITE_TAC BINOP_CONV [SUBSET] THEN + REWRITE_TAC[FORALL_IN_IMAGE] THEN REWRITE_TAC[IN_IMAGE; IN_ELIM_THM] THEN + CONJ_TAC THENL + [REWRITE_TAC[HOM_RELBOUNDARY] THEN + X_GEN_TAC `c:((num->real)->A)frag->bool` THEN DISCH_TAC THEN + REWRITE_TAC[hom_relboundary] THEN + GEN_REWRITE_TAC LAND_CONV [GSYM o_THM] THEN + TRANS_TAC EQ_TRANS + `(hom_induced (p - &1) (top,{}) (top,t) (\x:A. x) o + hom_induced (p - &1) (subtopology top s,{}) (top,{}) (\x. x) o + hom_boundary p (top,s)) c` THEN + CONJ_TAC THENL + [AP_THM_TAC THEN REWRITE_TAC[o_ASSOC] THEN + AP_THM_TAC THEN AP_TERM_TAC THEN + W(MP_TAC o PART_MATCH (rand o rand) HOM_INDUCED_COMPOSE o + rand o snd) THEN + SIMP_TAC[IMAGE_ID; EMPTY_SUBSET; CONTINUOUS_MAP_FROM_SUBTOPOLOGY; + CONTINUOUS_MAP_ID] THEN + DISCH_THEN(SUBST1_TAC o SYM) THEN + W(MP_TAC o PART_MATCH (rand o rand) HOM_INDUCED_COMPOSE o + lhand o snd) THEN + REWRITE_TAC[CONTINUOUS_MAP_ID; IMAGE_ID; EMPTY_SUBSET] THEN + SIMP_TAC[SUBSET_REFL; CONTINUOUS_MAP_ID; + CONTINUOUS_MAP_FROM_SUBTOPOLOGY]; + ONCE_REWRITE_TAC[o_THM] THEN MATCH_MP_TAC(MESON[group_homomorphism] + `!G. group_homomorphism(G,H) f /\ x = group_id G + ==> f x = group_id H`) THEN + EXISTS_TAC `homology_group(p - &1,top:A topology)` THEN + REWRITE_TAC[homology_group; GROUP_HOMOMORPHISM_HOM_INDUCED] THEN + MP_TAC(ISPECL[`p:int`; `top:A topology`; `s:A->bool`] + HOMOLOGY_EXACTNESS_AXIOM_2) THEN + REWRITE_TAC[group_exactness; group_kernel; group_image; o_THM] THEN + REWRITE_TAC[GSYM homology_group] THEN MATCH_MP_TAC(SET_RULE + `x IN s ==> P /\ Q /\ IMAGE f s = {y | y IN t /\ g y = z} + ==> g(f x) = z`) THEN + ASM SET_TAC[]]; + ALL_TAC] THEN + X_GEN_TAC `x:((num->real)->A)frag->bool` THEN STRIP_TAC THEN + MP_TAC(ISPECL[`p - &1:int`; `subtopology top s:A topology`; `t:A->bool`] + HOMOLOGY_EXACTNESS_AXIOM_1) THEN + REWRITE_TAC[group_exactness; group_kernel; group_image] THEN + DISCH_THEN(MP_TAC o MATCH_MP (SET_RULE + `P /\ Q /\ IMAGE f s = {y | y IN t /\ g y = z} + ==> !x. x IN t /\ g x = z ==> ?y. y IN s /\ f y = x`)) THEN + DISCH_THEN(MP_TAC o SPEC `x:((num->real)->A)frag->bool`) THEN + ASM_REWRITE_TAC[] THEN ANTS_TAC THENL + [MP_TAC(ISPECL + [`p - &1:int`; `subtopology top s:A topology`; `t:A->bool`; + `top:A topology`; `t:A->bool`; `\x:A. x`] + NATURALITY_HOM_INDUCED) THEN + REWRITE_TAC[IMAGE_ID; SUBSET_REFL] THEN + SIMP_TAC[CONTINUOUS_MAP_ID; CONTINUOUS_MAP_FROM_SUBTOPOLOGY] THEN + ASM_SIMP_TAC[SUBTOPOLOGY_SUBTOPOLOGY; SET_RULE + `t SUBSET s ==> s INTER t = t`] THEN + DISCH_THEN(MP_TAC o C AP_THM `x:((num->real)->A)frag->bool`) THEN + ASM_REWRITE_TAC[o_THM; + REWRITE_RULE[group_homomorphism] GROUP_HOMOMORPHISM_HOM_BOUNDARY] THEN + DISCH_THEN SUBST1_TAC THEN CONV_TAC SYM_CONV THEN + MATCH_MP_TAC HOM_INDUCED_ID THEN + W(MP_TAC o PART_MATCH lhand HOM_BOUNDARY o lhand o snd) THEN + ASM_SIMP_TAC[homology_group; SUBTOPOLOGY_SUBTOPOLOGY; SET_RULE + `t SUBSET s ==> s INTER t = t`]; + DISCH_THEN(X_CHOOSE_THEN `y:((num->real)->A)frag->bool` + STRIP_ASSUME_TAC)] THEN + MP_TAC(ISPECL [`p - &1:int`; `top:A topology`; `t:A->bool`] + HOMOLOGY_EXACTNESS_AXIOM_3) THEN + REWRITE_TAC[group_exactness; group_kernel; group_image] THEN + DISCH_THEN(MP_TAC o MATCH_MP (SET_RULE + `P /\ Q /\ IMAGE f s = {y | y IN t /\ g y = z} + ==> !x. x IN t /\ g x = z ==> ?y. y IN s /\ f y = x`)) THEN + DISCH_THEN(MP_TAC o SPEC + `hom_induced (p - &1) (subtopology top s,{}) (top,{}) (\x:A. x) y`) THEN + REWRITE_TAC[HOM_INDUCED; homology_group] THEN + GEN_REWRITE_TAC (funpow 3 LAND_CONV) [GSYM o_THM] THEN + W(MP_TAC o PART_MATCH (rand o rand) HOM_INDUCED_COMPOSE o + rator o lhand o lhand o lhand o snd) THEN + REWRITE_TAC[IMAGE_ID; EMPTY_SUBSET] THEN + SIMP_TAC[CONTINUOUS_MAP_ID; CONTINUOUS_MAP_FROM_SUBTOPOLOGY] THEN + DISCH_THEN(SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[o_DEF] THEN + MP_TAC(ISPECL + [`p - &1:int`; `subtopology top s:A topology`; `{}:A->bool`; + `subtopology top s:A topology`; `t:A->bool`; + `top:A topology`; `t:A->bool`; `\x:A. x`; `\x:A. x`] + HOM_INDUCED_COMPOSE) THEN + REWRITE_TAC[IMAGE_ID; EMPTY_SUBSET; SUBSET_REFL] THEN + SIMP_TAC[CONTINUOUS_MAP_ID; CONTINUOUS_MAP_FROM_SUBTOPOLOGY] THEN + REWRITE_TAC[o_DEF] THEN DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[] THEN + DISCH_THEN(X_CHOOSE_THEN `z:((num->real)->A)frag->bool` + STRIP_ASSUME_TAC) THEN + MP_TAC(ISPECL [`p:int`; `top:A topology`; `s:A->bool`] + HOMOLOGY_EXACTNESS_AXIOM_2) THEN + REWRITE_TAC[group_exactness; group_kernel; group_image] THEN + DISCH_THEN(MP_TAC o MATCH_MP (SET_RULE + `P /\ Q /\ IMAGE f s = {y | y IN t /\ g y = z} + ==> !x. x IN t /\ g x = z ==> ?y. y IN s /\ f y = x`)) THEN + DISCH_THEN(MP_TAC o SPEC + `group_div (homology_group(p - &1,subtopology top s)) y + (hom_induced (p - &1) (subtopology top t,{}) + (subtopology top s,{}) (\x:A. x) z)`) THEN + RULE_ASSUM_TAC(REWRITE_RULE[homology_group]) THEN + ASM_SIMP_TAC[GROUP_DIV; HOM_INDUCED; homology_group; + MATCH_MP GROUP_HOMOMORPHISM_DIV (SPEC_ALL GROUP_HOMOMORPHISM_HOM_INDUCED); + GROUP_RULE `group_div G x y = group_id G <=> y = x`] THEN + GEN_REWRITE_TAC (funpow 3 LAND_CONV) [GSYM o_THM] THEN + W(MP_TAC o PART_MATCH (rand o rand) HOM_INDUCED_COMPOSE o + rator o lhand o lhand o lhand o snd) THEN + SIMP_TAC[IMAGE_ID; EMPTY_SUBSET; CONTINUOUS_MAP_ID; + CONTINUOUS_MAP_FROM_SUBTOPOLOGY; CONTINUOUS_MAP_IN_SUBTOPOLOGY] THEN + REWRITE_TAC[TOPSPACE_SUBTOPOLOGY] THEN + ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN(SUBST1_TAC o SYM)] THEN + ASM_REWRITE_TAC[o_DEF] THEN + MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `w:((num->real)->A)frag->bool` THEN + STRIP_TAC THEN ASM_REWRITE_TAC[hom_relboundary; o_THM] THEN + ASM_SIMP_TAC[HOM_INDUCED; MATCH_MP GROUP_HOMOMORPHISM_DIV + (SPEC_ALL GROUP_HOMOMORPHISM_HOM_INDUCED)] THEN + ASM_SIMP_TAC[HOM_INDUCED; GROUP_RULE + `x = group_div G x y <=> y = group_id G`] THEN + MP_TAC(ISPECL[`p - &1:int`; `subtopology top s:A topology`; `t:A->bool`] + HOMOLOGY_EXACTNESS_AXIOM_3) THEN + ASM_SIMP_TAC[SUBTOPOLOGY_SUBTOPOLOGY; SET_RULE + `t SUBSET s ==> s INTER t = t`] THEN + REWRITE_TAC[group_exactness; group_kernel; group_image; o_THM] THEN + REWRITE_TAC[GSYM homology_group] THEN MATCH_MP_TAC(SET_RULE + `x IN s ==> P /\ Q /\ IMAGE f s = {y | y IN t /\ g y = z} + ==> g(f x) = z`) THEN + ASM_REWRITE_TAC[homology_group]);; + +let HOMOLOGY_EXACTNESS_TRIPLE_3 = prove + (`!p top s t:A->bool. + t SUBSET s + ==> group_exactness(relative_homology_group(p,subtopology top s,t), + relative_homology_group(p,top,t), + relative_homology_group(p,top,s)) + (hom_induced p (subtopology top s,t) (top,t) (\x. x), + hom_induced p (top,t) (top,s) (\x. x))`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[group_exactness; GROUP_HOMOMORPHISM_HOM_RELBOUNDARY; + GROUP_HOMOMORPHISM_HOM_INDUCED] THEN + REWRITE_TAC[group_image; group_kernel] THEN + MATCH_MP_TAC SUBSET_ANTISYM THEN GEN_REWRITE_TAC BINOP_CONV [SUBSET] THEN + REWRITE_TAC[FORALL_IN_IMAGE] THEN REWRITE_TAC[IN_IMAGE; IN_ELIM_THM] THEN + REWRITE_TAC[HOM_INDUCED; HOM_RELBOUNDARY] THEN + MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN CONJ_TAC THENL + [X_GEN_TAC `c:((num->real)->A)frag->bool` THEN DISCH_TAC THEN + TRANS_TAC EQ_TRANS + `hom_induced p (subtopology top s,s) (top,s) (\x:A. x) + (hom_induced p (subtopology top s,t) (subtopology top s,s) (\x. x) + c)` THEN + CONJ_TAC THENL + [GEN_REWRITE_TAC BINOP_CONV [GSYM o_THM] THEN AP_THM_TAC THEN + ASM_SIMP_TAC[GSYM HOM_INDUCED_COMPOSE; CONTINUOUS_MAP_FROM_SUBTOPOLOGY; + IMAGE_ID; SUBSET_REFL; CONTINUOUS_MAP_ID]; + MATCH_MP_TAC(MESON[group_homomorphism] + `!G. group_homomorphism(G,H) f /\ x = group_id G + ==> f x = group_id H`) THEN + EXISTS_TAC + `relative_homology_group (p,subtopology top (s:A->bool),s)` THEN + REWRITE_TAC[GROUP_HOMOMORPHISM_HOM_INDUCED] THEN + MP_TAC(ISPECL [`p:int`; `subtopology top (s:A->bool)`] + TRIVIAL_RELATIVE_HOMOLOGY_GROUP_TOPSPACE) THEN + REWRITE_TAC[trivial_group] THEN MATCH_MP_TAC(SET_RULE + `x IN c /\ a = b ==> c = {b} ==> x = a`) THEN + REWRITE_TAC[TOPSPACE_SUBTOPOLOGY] THEN + ONCE_REWRITE_TAC[SET_RULE `u INTER s = (u INTER s) INTER s`] THEN + ONCE_REWRITE_TAC[GSYM TOPSPACE_SUBTOPOLOGY] THEN + REWRITE_TAC[GSYM RELATIVE_HOMOLOGY_GROUP_RESTRICT; HOM_INDUCED]]; + DISCH_TAC] THEN + X_GEN_TAC `x:((num->real)->A)frag->bool` THEN STRIP_TAC THEN + ABBREV_TAC `b = hom_boundary p (top:A topology,t) x` THEN + SUBGOAL_THEN + `b IN group_carrier(homology_group(p - &1,subtopology top (t:A->bool)))` + ASSUME_TAC THENL + [EXPAND_TAC "b" THEN REWRITE_TAC[HOM_BOUNDARY]; ALL_TAC] THEN + MP_TAC(ISPECL + [`p:int`; `top:A topology`; `t:A->bool`; `top:A topology`; + `s:A->bool`; `\x:A. x`] NATURALITY_HOM_INDUCED) THEN + ASM_SIMP_TAC[CONTINUOUS_MAP_ID; IMAGE_ID] THEN + DISCH_THEN(MP_TAC o C AP_THM `x:((num->real)->A)frag->bool`) THEN + ASM_REWRITE_TAC[o_THM; REWRITE_RULE[group_homomorphism] + GROUP_HOMOMORPHISM_HOM_BOUNDARY] THEN + DISCH_THEN(ASSUME_TAC o SYM) THEN + MP_TAC(ISPECL [`p:int`; `subtopology top s:A topology`; `t:A->bool`] + HOMOLOGY_EXACTNESS_AXIOM_2) THEN + REWRITE_TAC[group_exactness; group_image; group_kernel] THEN + DISCH_THEN(MP_TAC o GEN_REWRITE_RULE I [EXTENSION] o last o CONJUNCTS) THEN + DISCH_THEN(MP_TAC o SPEC `b:((num->real)->A)frag->bool`) THEN + REWRITE_TAC[IN_IMAGE; IN_ELIM_THM; SUBTOPOLOGY_SUBTOPOLOGY] THEN + ASM_SIMP_TAC[SET_RULE `t SUBSET s ==> s INTER t = t`] THEN + DISCH_THEN(X_CHOOSE_THEN `u:((num->real)->A)frag->bool` + (STRIP_ASSUME_TAC o GSYM)) THEN + ABBREV_TAC + `y = group_div (relative_homology_group(p,top,t)) + x (hom_induced p (subtopology top s,t) (top,t) (\x:A. x) u)` THEN + SUBGOAL_THEN + `y IN group_carrier(relative_homology_group(p,top:A topology,t))` + ASSUME_TAC THENL + [EXPAND_TAC "y" THEN MATCH_MP_TAC GROUP_DIV THEN + ASM_REWRITE_TAC[HOM_INDUCED]; + ALL_TAC] THEN + MP_TAC(ISPECL [`p:int`; `top:A topology`; `t:A->bool`] + HOMOLOGY_EXACTNESS_AXIOM_1) THEN + REWRITE_TAC[group_exactness; group_image; group_kernel] THEN + DISCH_THEN(MP_TAC o GEN_REWRITE_RULE I [EXTENSION] o last o CONJUNCTS) THEN + DISCH_THEN(MP_TAC o SPEC `y:((num->real)->A)frag->bool`) THEN + DISCH_THEN(MP_TAC o snd o EQ_IMP_RULE) THEN + ASM_REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM; IN_IMAGE] THEN + ANTS_TAC THENL + [EXPAND_TAC "y" THEN + ASM_SIMP_TAC[HOM_INDUCED; MATCH_MP GROUP_HOMOMORPHISM_DIV + (SPEC_ALL GROUP_HOMOMORPHISM_HOM_BOUNDARY)] THEN + ASM_SIMP_TAC[GROUP_DIV_EQ_ID; HOM_INDUCED; HOM_BOUNDARY] THEN + CONV_TAC SYM_CONV THEN GEN_REWRITE_TAC LAND_CONV [GSYM o_THM] THEN + SIMP_TAC[NATURALITY_HOM_INDUCED; IMAGE_ID; CONTINUOUS_MAP_ID; + CONTINUOUS_MAP_FROM_SUBTOPOLOGY; SUBSET_REFL] THEN + ASM_REWRITE_TAC[o_THM; SUBTOPOLOGY_SUBTOPOLOGY] THEN + ASM_SIMP_TAC[SET_RULE `t SUBSET s ==> s INTER t = t`] THEN + ASM_SIMP_TAC[HOM_INDUCED_ID; GSYM homology_group]; + DISCH_THEN(X_CHOOSE_THEN `z:((num->real)->A)frag->bool` + (STRIP_ASSUME_TAC o GSYM))] THEN + MP_TAC(ISPECL [`p:int`; `top:A topology`; `s:A->bool`] + HOMOLOGY_EXACTNESS_AXIOM_3) THEN + REWRITE_TAC[group_exactness; group_image; group_kernel] THEN + DISCH_THEN(MP_TAC o GEN_REWRITE_RULE I [EXTENSION] o last o CONJUNCTS) THEN + DISCH_THEN(MP_TAC o SPEC `z:((num->real)->A)frag->bool`) THEN + DISCH_THEN(MP_TAC o snd o EQ_IMP_RULE) THEN + ASM_REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM; IN_IMAGE] THEN + ANTS_TAC THENL + [TRANS_TAC EQ_TRANS + `(hom_induced p (top,t) (top,s) (\x:A. x) o + hom_induced p (top,{}) (top,t) (\x. x)) z` THEN + CONJ_TAC THENL + [ASM_SIMP_TAC[GSYM HOM_INDUCED_COMPOSE; CONTINUOUS_MAP_ID; + IMAGE_ID; EMPTY_SUBSET] THEN + REWRITE_TAC[o_DEF]; + ASM_REWRITE_TAC[o_THM]] THEN + SUBST1_TAC(SYM(ASSUME + `group_div (relative_homology_group (p,top,t)) x + (hom_induced p (subtopology top s,t) (top,t) (\x:A. x) u) = + y`)) THEN + ASM_SIMP_TAC[HOM_INDUCED; MATCH_MP GROUP_HOMOMORPHISM_DIV + (SPEC_ALL GROUP_HOMOMORPHISM_HOM_INDUCED)] THEN + REWRITE_TAC[GROUP_RULE + `group_div G (group_id G) (group_id G) = group_id G`]; + DISCH_THEN(X_CHOOSE_THEN `w:((num->real)->A)frag->bool` + (STRIP_ASSUME_TAC o GSYM)) THEN + EXISTS_TAC + `group_mul (relative_homology_group (p,subtopology top s,t)) + (hom_induced p (subtopology top s,{}) (subtopology top s,t) + (\x:A. x) w) u` THEN + ASM_SIMP_TAC[GROUP_MUL; HOM_INDUCED; + MATCH_MP GROUP_HOMOMORPHISM_MUL + (SPEC_ALL GROUP_HOMOMORPHISM_HOM_INDUCED)] THEN + ASM_SIMP_TAC[GROUP_RULE `x = group_mul G z u <=> z = group_div G x u`; + HOM_INDUCED] THEN + EXPAND_TAC "y" THEN EXPAND_TAC "z" THEN + GEN_REWRITE_TAC BINOP_CONV [GSYM o_THM] THEN + SIMP_TAC[GSYM HOM_INDUCED_COMPOSE; IMAGE_ID; SUBSET_REFL; EMPTY_SUBSET; + CONTINUOUS_MAP_ID; CONTINUOUS_MAP_FROM_SUBTOPOLOGY]]);; + (* ------------------------------------------------------------------------- *) (* Reduced homology. *) (* ------------------------------------------------------------------------- *) diff --git a/Multivariate/multivariate_database.ml b/Multivariate/multivariate_database.ml index 09daeae4..191d0560 100644 --- a/Multivariate/multivariate_database.ml +++ b/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; diff --git a/Multivariate/realanalysis.ml b/Multivariate/realanalysis.ml index bf8e8955..3d88e7f8 100644 --- a/Multivariate/realanalysis.ml +++ b/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) /\ diff --git a/Proofrecording/hol_light/Help b/Proofrecording/hol_light/Help deleted file mode 120000 index bd807221..00000000 --- a/Proofrecording/hol_light/Help +++ /dev/null @@ -1 +0,0 @@ -../../Help/ \ No newline at end of file diff --git a/database.ml b/database.ml index 425bc810..a45d97e5 100644 --- a/database.ml +++ b/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; diff --git a/lists.ml b/lists.ml index 9d39ba7d..c57a79a1 100644 --- a/lists.ml +++ b/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