--- a/src/HOL/Analysis/Further_Topology.thy Sun Apr 19 13:01:40 2020 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy Sun Apr 19 22:16:57 2020 +0100
@@ -4,6 +4,7 @@
theory Further_Topology
imports Weierstrass_Theorems Polytope Complex_Transcendental Equivalence_Lebesgue_Henstock_Integration Retracts
+Sketch_and_Explore
begin
subsection\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>
@@ -28,10 +29,10 @@
by (rule diff_f' derivative_intros differentiable_on_compose [where f=f] | force)+
have geq: "g ` (S - {0}) = T - {0}"
proof
- have "g ` (S - {0}) \<subseteq> T"
- apply (auto simp: g_def subspace_mul [OF \<open>subspace T\<close>])
- apply (metis (mono_tags, lifting) DiffI subS01 subspace_mul [OF \<open>subspace T\<close>] fim image_subset_iff inf_le2 singletonD)
- done
+ have "\<And>u. \<lbrakk>u \<in> S; norm u *\<^sub>R f (u /\<^sub>R norm u) \<notin> T\<rbrakk> \<Longrightarrow> u = 0"
+ by (metis (mono_tags, lifting) DiffI subS01 subspace_mul [OF \<open>subspace T\<close>] fim image_subset_iff inf_le2 singletonD)
+ then have "g ` (S - {0}) \<subseteq> T"
+ using g_def by blast
moreover have "g ` (S - {0}) \<subseteq> UNIV - {0}"
proof (clarsimp simp: g_def)
fix y
@@ -51,12 +52,14 @@
proof -
have "x /\<^sub>R norm x \<in> T"
using \<open>subspace T\<close> subspace_mul that by blast
- then show ?thesis
- using * [THEN subsetD, of "x /\<^sub>R norm x"] that apply clarsimp
- apply (rule_tac x="norm x *\<^sub>R xa" in image_eqI, simp)
- apply (metis norm_eq_zero right_inverse scaleR_one scaleR_scaleR)
- using \<open>subspace S\<close> subspace_mul apply force
- done
+ then obtain u where u: "f u \<in> T" "x /\<^sub>R norm x = f u" "norm u = 1" "u \<in> S"
+ using * [THEN subsetD, of "x /\<^sub>R norm x"] \<open>x \<noteq> 0\<close> by auto
+ with that have [simp]: "norm x *\<^sub>R f u = x"
+ by (metis divideR_right norm_eq_zero)
+ moreover have "norm x *\<^sub>R u \<in> S - {0}"
+ using \<open>subspace S\<close> subspace_scale that(2) u by auto
+ with u show ?thesis
+ by (simp add: image_eqI [where x="norm x *\<^sub>R u"])
qed
then have "T - {0} \<subseteq> (\<lambda>x. norm x *\<^sub>R f (x /\<^sub>R norm x)) ` (S - {0})"
by force
@@ -107,12 +110,10 @@
qed (auto simp: p1span p2 span_base span_add)
ultimately have "linear p1" "linear p2"
by unfold_locales auto
- have "(\<lambda>z. g (p1 z)) differentiable_on {x + y |x y. x \<in> S - {0} \<and> y \<in> T'}"
- apply (rule differentiable_on_compose [where f=g])
- apply (rule linear_imp_differentiable_on [OF \<open>linear p1\<close>])
- apply (rule differentiable_on_subset [OF gdiff])
- using p12_eq \<open>S \<subseteq> T\<close> apply auto
- done
+ have "g differentiable_on p1 ` {x + y |x y. x \<in> S - {0} \<and> y \<in> T'}"
+ using p12_eq \<open>S \<subseteq> T\<close> by (force intro: differentiable_on_subset [OF gdiff])
+ then have "(\<lambda>z. g (p1 z)) differentiable_on {x + y |x y. x \<in> S - {0} \<and> y \<in> T'}"
+ by (rule differentiable_on_compose [OF linear_imp_differentiable_on [OF \<open>linear p1\<close>]])
then have diff: "(\<lambda>x. g (p1 x) + p2 x) differentiable_on {x + y |x y. x \<in> S - {0} \<and> y \<in> T'}"
by (intro derivative_intros linear_imp_differentiable_on [OF \<open>linear p2\<close>])
have "dim {x + y |x y. x \<in> S - {0} \<and> y \<in> T'} \<le> dim {x + y |x y. x \<in> S \<and> y \<in> T'}"
@@ -141,10 +142,7 @@
proof clarsimp
fix z assume "z \<notin> T'"
show "\<exists>x y. z = x + y \<and> x \<in> g ` (S - {0}) \<and> y \<in> T'"
- apply (rule_tac x="p1 z" in exI)
- apply (rule_tac x="p2 z" in exI)
- apply (simp add: p1 eq p2 geq)
- by (metis \<open>z \<notin> T'\<close> add.left_neutral eq p2)
+ by (metis Diff_iff \<open>z \<notin> T'\<close> add.left_neutral eq geq p1 p2 singletonD)
qed
ultimately have "negligible (-T')"
using negligible_subset by blast
@@ -173,8 +171,7 @@
then obtain g where pfg: "polynomial_function g" and gim: "g ` (sphere 0 1 \<inter> S) \<subseteq> T"
and g12: "\<And>x. x \<in> sphere 0 1 \<inter> S \<Longrightarrow> norm(f x - g x) < 1/2"
apply (rule Stone_Weierstrass_polynomial_function_subspace [OF _ contf _ \<open>subspace T\<close>, of "1/2"])
- using fim apply auto
- done
+ using fim by auto
have gnz: "g x \<noteq> 0" if "x \<in> sphere 0 1 \<inter> S" for x
proof -
have "norm (f x) = 1"
@@ -190,10 +187,8 @@
using gnz [of x]
by (auto simp: subspace_mul [OF \<open>subspace T\<close>] subsetD [OF gim])
have diffh: "h differentiable_on sphere 0 1 \<inter> S"
- unfolding h_def
- apply (intro derivative_intros diffg differentiable_on_compose [OF diffg])
- using gnz apply auto
- done
+ unfolding h_def using gnz
+ by (fastforce intro: derivative_intros diffg differentiable_on_compose [OF diffg])
have homfg: "homotopic_with_canon (\<lambda>z. True) (sphere 0 1 \<inter> S) (T - {0}) f g"
proof (rule homotopic_with_linear [OF contf])
show "continuous_on (sphere 0 1 \<inter> S) g"
@@ -204,18 +199,19 @@
have "f x \<in> sphere 0 1"
using fim that by (simp add: image_subset_iff)
moreover have "norm(f x - g x) < 1/2"
- apply (rule g12)
- using that by force
+ using g12 that by auto
ultimately show ?thesis
by (auto simp: norm_minus_commute dest: segment_bound)
qed
- show "\<And>x. x \<in> sphere 0 1 \<inter> S \<Longrightarrow> closed_segment (f x) (g x) \<subseteq> T - {0}"
- apply (simp add: subset_Diff_insert non0fg)
- apply (simp add: segment_convex_hull)
- apply (rule hull_minimal)
- using fim image_eqI gim apply force
- apply (rule subspace_imp_convex [OF \<open>subspace T\<close>])
- done
+ show "closed_segment (f x) (g x) \<subseteq> T - {0}" if "x \<in> sphere 0 1 \<inter> S" for x
+ proof -
+ have "convex T"
+ by (simp add: \<open>subspace T\<close> subspace_imp_convex)
+ then have "convex hull {f x, g x} \<subseteq> T"
+ by (metis IntD2 closed_segment_subset fim gim image_subset_iff segment_convex_hull that)
+ then show ?thesis
+ using that non0fg segment_convex_hull by fastforce
+ qed
qed
obtain d where d: "d \<in> (sphere 0 1 \<inter> T) - h ` (sphere 0 1 \<inter> S)"
using h spheremap_lemma1 [OF ST \<open>S \<subseteq> T\<close> diffh] by force
@@ -225,13 +221,17 @@
have conth: "continuous_on (sphere 0 1 \<inter> S) h"
using differentiable_imp_continuous_on diffh by blast
have hom_hd: "homotopic_with_canon (\<lambda>z. True) (sphere 0 1 \<inter> S) (T - {0}) h (\<lambda>x. -d)"
- apply (rule homotopic_with_linear [OF conth continuous_on_const])
- apply (simp add: subset_Diff_insert non0hd)
- apply (simp add: segment_convex_hull)
- apply (rule hull_minimal)
- using h d apply (force simp: subspace_neg [OF \<open>subspace T\<close>])
- apply (rule subspace_imp_convex [OF \<open>subspace T\<close>])
- done
+ proof (rule homotopic_with_linear [OF conth continuous_on_const])
+ fix x
+ assume x: "x \<in> sphere 0 1 \<inter> S"
+ have "convex hull {h x, - d} \<subseteq> T"
+ proof (rule hull_minimal)
+ show "{h x, - d} \<subseteq> T"
+ using h d x by (force simp: subspace_neg [OF \<open>subspace T\<close>])
+ qed (simp add: subspace_imp_convex [OF \<open>subspace T\<close>])
+ with x segment_convex_hull show "closed_segment (h x) (- d) \<subseteq> T - {0}"
+ by (auto simp add: subset_Diff_insert non0hd)
+ qed
have conT0: "continuous_on (T - {0}) (\<lambda>y. inverse(norm y) *\<^sub>R y)"
by (intro continuous_intros) auto
have sub0T: "(\<lambda>y. y /\<^sub>R norm y) ` (T - {0}) \<subseteq> sphere 0 1 \<inter> T"
@@ -242,13 +242,11 @@
apply (rule homotopic_with_compose_continuous_left [OF hom_hd conT0 sub0T])
using d apply (auto simp: h_def)
done
- show ?thesis
- apply (rule_tac x=c in exI)
- apply (rule homotopic_with_trans [OF _ homhc])
- apply (rule homotopic_with_eq)
- apply (rule homotopic_with_compose_continuous_left [OF homfg conT0 sub0T])
- apply (auto simp: h_def)
- done
+ have "homotopic_with_canon (\<lambda>x. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) f h"
+ apply (rule homotopic_with_eq [OF homotopic_with_compose_continuous_left [OF homfg conT0 sub0T]])
+ by (auto simp: h_def)
+ then show ?thesis
+ by (metis homotopic_with_trans [OF _ homhc])
qed
@@ -283,15 +281,21 @@
then have affS_eq: "aff_dim S = aff_dim (ball 0 1 \<inter> T)"
using \<open>aff_dim T = aff_dim S\<close> by simp
have "rel_frontier S homeomorphic rel_frontier(ball 0 1 \<inter> T)"
- apply (rule homeomorphic_rel_frontiers_convex_bounded_sets [OF \<open>convex S\<close> \<open>bounded S\<close>])
- apply (simp add: \<open>subspace T\<close> convex_Int subspace_imp_convex)
- apply (simp add: bounded_Int)
- apply (rule affS_eq)
- done
+ proof (rule homeomorphic_rel_frontiers_convex_bounded_sets [OF \<open>convex S\<close> \<open>bounded S\<close>])
+ show "convex (ball 0 1 \<inter> T)"
+ by (simp add: \<open>subspace T\<close> convex_Int subspace_imp_convex)
+ show "bounded (ball 0 1 \<inter> T)"
+ by (simp add: bounded_Int)
+ show "aff_dim S = aff_dim (ball 0 1 \<inter> T)"
+ by (rule affS_eq)
+ qed
also have "... = frontier (ball 0 1) \<inter> T"
- apply (rule convex_affine_rel_frontier_Int [OF convex_ball])
- apply (simp add: \<open>subspace T\<close> subspace_imp_affine)
- using \<open>subspace T\<close> subspace_0 by force
+ proof (rule convex_affine_rel_frontier_Int [OF convex_ball])
+ show "affine T"
+ by (simp add: \<open>subspace T\<close> subspace_imp_affine)
+ show "interior (ball 0 1) \<inter> T \<noteq> {}"
+ using \<open>subspace T\<close> subspace_0 by force
+ qed
also have "... = sphere 0 1 \<inter> T"
by auto
finally show ?thesis .
@@ -367,11 +371,10 @@
next
case False
with \<open>\<not> s \<le> 0\<close> have "r > 0" "s > 0" by auto
- show ?thesis
+ show thesis
apply (rule inessential_spheremap_lowdim_gen [of "cball a r" "cball b s" f])
- using \<open>0 < r\<close> \<open>0 < s\<close> assms(1)
- apply (simp_all add: f aff_dim_cball)
- using that by blast
+ using \<open>0 < r\<close> \<open>0 < s\<close> assms(1) that
+ by (simp_all add: f aff_dim_cball inessential_spheremap_lowdim_gen [of "cball a r" "cball b s" f])
qed
qed
@@ -404,7 +407,6 @@
show ?case
apply (rule_tac x="\<lambda>x. if x \<in> S then f x else g x" in exI, simp)
apply (intro conjI continuous_on_cases)
- apply (simp_all add: insert closed_Union contf contg)
using fim gim feq geq
apply (force simp: insert closed_Union contf contg inf_commute intro: fg)+
done
@@ -426,18 +428,18 @@
assumes "finite \<F>" "\<G> \<subseteq> \<F>" "convex T" "bounded T"
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
and aff: "\<And>X. X \<in> \<F> - \<G> \<Longrightarrow> aff_dim X < aff_dim T"
- and face: "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>\<rbrakk> \<Longrightarrow> (S \<inter> T) face_of S \<and> (S \<inter> T) face_of T"
+ and face: "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>\<rbrakk> \<Longrightarrow> (S \<inter> T) face_of S"
and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T"
obtains g where "continuous_on (\<Union>\<F>) g" "g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
proof (cases "\<F> - \<G> = {}")
case True
- then have "\<Union>\<F> \<subseteq> \<Union>\<G>"
- by (simp add: Union_mono)
- then show ?thesis
- apply (rule_tac g=f in that)
- using contf continuous_on_subset apply blast
- using fim apply blast
- by simp
+ show ?thesis
+ proof
+ show "continuous_on (\<Union> \<F>) f"
+ using True \<open>\<G> \<subseteq> \<F>\<close> contf by auto
+ show "f ` \<Union> \<F> \<subseteq> rel_frontier T"
+ using True fim by auto
+ qed auto
next
case False
then have "0 \<le> aff_dim T"
@@ -446,19 +448,17 @@
by (metis nonneg_eq_int)
have Union_empty_eq: "\<Union>{D. D = {} \<and> P D} = {}" for P :: "'a set \<Rightarrow> bool"
by auto
+ have face': "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>\<rbrakk> \<Longrightarrow> (S \<inter> T) face_of S \<and> (S \<inter> T) face_of T"
+ by (metis face inf_commute)
have extendf: "\<exists>g. continuous_on (\<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < i})) g \<and>
g ` (\<Union> (\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < i})) \<subseteq> rel_frontier T \<and>
(\<forall>x \<in> \<Union>\<G>. g x = f x)"
if "i \<le> aff_dim T" for i::nat
using that
proof (induction i)
- case 0 then show ?case
- apply (simp add: Union_empty_eq)
- apply (rule_tac x=f in exI)
- apply (intro conjI)
- using contf continuous_on_subset apply blast
- using fim apply blast
- by simp
+ case 0
+ show ?case
+ using 0 contf fim by (auto simp add: Union_empty_eq)
next
case (Suc p)
with \<open>bounded T\<close> have "rel_frontier T \<noteq> {}"
@@ -477,12 +477,12 @@
if D: "D \<in> \<G> \<union> ?Faces" for D
proof (cases "D \<subseteq> \<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p})")
case True
- then show ?thesis
- apply (rule_tac x=h in exI)
- apply (intro conjI)
- apply (blast intro: continuous_on_subset [OF conth])
- using him apply blast
- by simp
+ have "continuous_on D h"
+ using True conth continuous_on_subset by blast
+ moreover have "h ` D \<subseteq> rel_frontier T"
+ using True him by blast
+ ultimately show ?thesis
+ by blast
next
case False
note notDsub = False
@@ -507,9 +507,7 @@
then have [simp]: "\<not> affine D"
using affine_bounded_eq_trivial False \<open>D \<noteq> {}\<close> \<open>bounded D\<close> by blast
have "{F. F facet_of D} \<subseteq> {E. E face_of C \<and> aff_dim E < int p}"
- apply clarify
- apply (metis \<open>D face_of C\<close> affD eq_iff face_of_trans facet_of_def zle_diff1_eq)
- done
+ by clarify (metis \<open>D face_of C\<close> affD eq_iff face_of_trans facet_of_def zle_diff1_eq)
moreover have "polyhedron D"
using \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> face_of_polytope_polytope poly polytope_imp_polyhedron by auto
ultimately have relf_sub: "rel_frontier D \<subseteq> \<Union> {E. E face_of C \<and> aff_dim E < p}"
@@ -540,30 +538,39 @@
if "E \<in> \<G> \<union> {D. Bex \<F> ((face_of) D) \<and> aff_dim D < int p}" for E
proof (rule face_of_subset_rel_frontier)
show "D \<inter> E face_of D"
- using that \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> face
- apply auto
- apply (meson face_of_Int_subface \<open>\<G> \<subseteq> \<F>\<close> face_of_refl_eq poly polytope_imp_convex subsetD)
- using face_of_Int_subface apply blast
- done
+ using that
+ proof safe
+ assume "E \<in> \<G>"
+ then show "D \<inter> E face_of D"
+ by (meson \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> assms(2) face' face_of_Int_subface face_of_refl_eq poly polytope_imp_convex subsetD)
+ next
+ fix x
+ assume "aff_dim E < int p" "x \<in> \<F>" "E face_of x"
+ then show "D \<inter> E face_of D"
+ by (meson \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> face' face_of_Int_subface that)
+ qed
show "D \<inter> E \<noteq> D"
using that notDsub by auto
qed
- then show ?thesis
- apply (rule_tac x=g in exI)
- apply (intro conjI ballI)
- using continuous_on_subset contg apply blast
- using gim apply blast
- using gh by fastforce
+ moreover have "continuous_on D g"
+ using contg continuous_on_subset by blast
+ ultimately show ?thesis
+ by (rule_tac x=g in exI) (use gh gim in fastforce)
qed
qed
have intle: "i < 1 + int j \<longleftrightarrow> i \<le> int j" for i j
by auto
have "finite \<G>"
using \<open>finite \<F>\<close> \<open>\<G> \<subseteq> \<F>\<close> rev_finite_subset by blast
- then have fin: "finite (\<G> \<union> ?Faces)"
- apply simp
- apply (rule_tac B = "\<Union>{{D. D face_of C}| C. C \<in> \<F>}" in finite_subset)
- by (auto simp: \<open>finite \<F>\<close> finite_polytope_faces poly)
+ moreover have "finite (?Faces)"
+ proof -
+ have \<section>: "finite (\<Union> {{D. D face_of C} |C. C \<in> \<F>})"
+ by (auto simp: \<open>finite \<F>\<close> finite_polytope_faces poly)
+ show ?thesis
+ by (auto intro: finite_subset [OF _ \<section>])
+ qed
+ ultimately have fin: "finite (\<G> \<union> ?Faces)"
+ by simp
have clo: "closed S" if "S \<in> \<G> \<union> ?Faces" for S
using that \<open>\<G> \<subseteq> \<F>\<close> face_of_polytope_polytope poly polytope_imp_closed by blast
have K: "X \<inter> Y \<subseteq> \<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < int p})"
@@ -571,9 +578,7 @@
proof -
have ff: "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
if XY: "X face_of D" "Y face_of E" and DE: "D \<in> \<F>" "E \<in> \<F>" for D E
- apply (rule face_of_Int_subface [OF _ _ XY])
- apply (auto simp: face DE)
- done
+ by (rule face_of_Int_subface [OF _ _ XY]) (auto simp: face' DE)
show ?thesis
using that
apply auto
@@ -586,22 +591,19 @@
"g ` \<Union>(\<G> \<union> ?Faces) \<subseteq> rel_frontier T"
"(\<forall>x \<in> \<Union>(\<G> \<union> ?Faces) \<inter>
\<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < p}). g x = h x)"
- apply (rule exE [OF extending_maps_Union [OF fin extendh clo K]], blast+)
- done
+ by (rule exE [OF extending_maps_Union [OF fin extendh clo K]], blast+)
then show ?case
- apply (simp add: intle local.heq [symmetric], blast)
- done
+ by (simp add: intle local.heq [symmetric], blast)
qed
have eq: "\<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < i}) = \<Union>\<F>"
proof
show "\<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < int i}) \<subseteq> \<Union>\<F>"
- apply (rule Union_subsetI)
- using \<open>\<G> \<subseteq> \<F>\<close> face_of_imp_subset apply force
- done
+ using \<open>\<G> \<subseteq> \<F>\<close> face_of_imp_subset by fastforce
show "\<Union>\<F> \<subseteq> \<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < i})"
- apply (rule Union_mono)
- using face apply (fastforce simp: aff i)
- done
+ proof (rule Union_mono)
+ show "\<F> \<subseteq> \<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < int i}"
+ using face by (fastforce simp: aff i)
+ qed
qed
have "int i \<le> aff_dim T" by (simp add: i)
then show ?thesis
@@ -647,13 +649,15 @@
by (simp add: C card_insert_if insert.hyps le_SucI)
have "closed (\<Union>\<F>)"
using clo insert.hyps by blast
+ have "continuous_on (X - insert a C) f"
+ using contf by (force simp: elim: continuous_on_subset)
+ moreover have "continuous_on (\<Union> \<F> - insert a C) g"
+ using contg by (force simp: elim: continuous_on_subset)
+ ultimately
have "continuous_on (X - insert a C \<union> (\<Union>\<F> - insert a C)) (\<lambda>x. if x \<in> X then f x else g x)"
- apply (rule continuous_on_cases_local)
- apply (simp_all add: closedin_closed)
+ apply (intro continuous_on_cases_local; simp add: closedin_closed)
using \<open>closed X\<close> apply blast
using \<open>closed (\<Union>\<F>)\<close> apply blast
- using contf apply (force simp: elim: continuous_on_subset)
- using contg apply (force simp: elim: continuous_on_subset)
using fh gh insert.hyps pwX by fastforce
then show "continuous_on (\<Union>(insert X \<F>) - insert a C) (\<lambda>a. if a \<in> X then f a else g a)"
by (blast intro: continuous_on_subset)
@@ -687,9 +691,7 @@
obtain C g where "finite C \<and> disjnt C U \<and> card C \<le> card ?\<F> \<and>
continuous_on (\<Union>?\<F> - C) g \<and> g ` (\<Union>?\<F> - C) \<subseteq> T
\<and> (\<forall>x \<in> (\<Union>?\<F> - C) \<inter> K. g x = h x)"
- apply (rule exE [OF extend_map_lemma_cofinite0 [OF fin pw, of U T h]])
- apply (fastforce intro!: clo \<F>)+
- done
+ using extend_map_lemma_cofinite0 [OF fin pw, of U T h] by (fastforce intro!: clo \<F>)
ultimately show ?thesis
by (rule_tac C=C and g=g in that) auto
qed
@@ -699,7 +701,7 @@
assumes "finite \<F>" "\<G> \<subseteq> \<F>" and T: "convex T" "bounded T"
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T"
- and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X \<and> (X \<inter> Y) face_of Y"
+ and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
and aff: "\<And>X. X \<in> \<F> - \<G> \<Longrightarrow> aff_dim X \<le> aff_dim T"
obtains C g where
"finite C" "disjnt C (\<Union>\<G>)" "card C \<le> card \<F>" "continuous_on (\<Union>\<F> - C) g"
@@ -708,28 +710,23 @@
define \<H> where "\<H> \<equiv> \<G> \<union> {D. \<exists>C \<in> \<F> - \<G>. D face_of C \<and> aff_dim D < aff_dim T}"
have "finite \<G>"
using assms finite_subset by blast
- moreover have "finite (\<Union>{{D. D face_of C} |C. C \<in> \<F>})"
- apply (rule finite_Union)
- apply (simp add: \<open>finite \<F>\<close>)
- using finite_polytope_faces poly by auto
- ultimately have "finite \<H>"
- apply (simp add: \<H>_def)
- apply (rule finite_subset [of _ "\<Union> {{D. D face_of C} | C. C \<in> \<F>}"], auto)
- done
- have *: "\<And>X Y. \<lbrakk>X \<in> \<H>; Y \<in> \<H>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+ have *: "finite (\<Union>{{D. D face_of C} |C. C \<in> \<F>})"
+ using finite_polytope_faces poly \<open>finite \<F>\<close> by force
+ then have "finite \<H>"
+ by (auto simp: \<H>_def \<open>finite \<G>\<close> intro: finite_subset [OF _ *])
+ have face': "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>\<rbrakk> \<Longrightarrow> (S \<inter> T) face_of S \<and> (S \<inter> T) face_of T"
+ by (metis face inf_commute)
+ have *: "\<And>X Y. \<lbrakk>X \<in> \<H>; Y \<in> \<H>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
unfolding \<H>_def
- apply (elim UnE bexE CollectE DiffE)
- using subsetD [OF \<open>\<G> \<subseteq> \<F>\<close>] apply (simp_all add: face)
- apply (meson subsetD [OF \<open>\<G> \<subseteq> \<F>\<close>] face face_of_Int_subface face_of_imp_subset face_of_refl poly polytope_imp_convex)+
+ using subsetD [OF \<open>\<G> \<subseteq> \<F>\<close>] apply (auto simp add: face)
+ apply (meson face' face_of_Int_subface face_of_refl_eq poly polytope_imp_convex)+
done
obtain h where conth: "continuous_on (\<Union>\<H>) h" and him: "h ` (\<Union>\<H>) \<subseteq> rel_frontier T"
- and hf: "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> h x = f x"
- using \<open>finite \<H>\<close>
- unfolding \<H>_def
- apply (rule extend_map_lemma [OF _ Un_upper1 T _ _ _ contf fim])
- using \<open>\<G> \<subseteq> \<F>\<close> face_of_polytope_polytope poly apply fastforce
- using * apply (auto simp: \<H>_def)
- done
+ and hf: "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> h x = f x"
+ proof (rule extend_map_lemma [OF \<open>finite \<H>\<close> [unfolded \<H>_def] Un_upper1 T])
+ show "\<And>X. \<lbrakk>X \<in> \<G> \<union> {D. \<exists>C\<in>\<F> - \<G>. D face_of C \<and> aff_dim D < aff_dim T}\<rbrakk> \<Longrightarrow> polytope X"
+ using \<open>\<G> \<subseteq> \<F>\<close> face_of_polytope_polytope poly by fastforce
+ qed (use * \<H>_def contf fim in auto)
have "bounded (\<Union>\<G>)"
using \<open>finite \<G>\<close> \<open>\<G> \<subseteq> \<F>\<close> poly polytope_imp_bounded by blast
then have "\<Union>\<G> \<noteq> UNIV"
@@ -783,7 +780,7 @@
fix E
assume "b \<in> E" "E \<in> \<G>"
then have "E \<inter> D face_of E \<and> E \<inter> D face_of D"
- using \<open>\<G> \<subseteq> \<F>\<close> face that by auto
+ using \<open>\<G> \<subseteq> \<F>\<close> face' that by auto
with face_of_subset_rel_frontier \<open>E \<in> \<G>\<close> \<open>b \<in> E\<close> brelD rel_interior_subset [of D]
D_not_subset rel_frontier_def \<H>_def
show False
@@ -824,11 +821,10 @@
next
case 2 show ?thesis
proof (rule face_of_subset_rel_frontier [THEN subsetD])
- show "D \<inter> A face_of D"
- apply (rule face_of_Int_subface [of D B _ A, THEN conjunct1])
- apply (simp_all add: 2 \<open>D \<in> \<F>\<close> face)
- apply (simp add: \<open>polyhedron D\<close> polyhedron_imp_convex face_of_refl)
- done
+ have "D face_of D"
+ by (simp add: \<open>polyhedron D\<close> polyhedron_imp_convex face_of_refl)
+ then show "D \<inter> A face_of D"
+ by (meson "2"(2) "2"(3) \<open>D \<in> \<F>\<close> face' face_of_Int_Int face_of_face)
show "D \<inter> A \<noteq> D"
using "2" D_not_subset \<H>_def by blast
qed (auto simp: 2)
@@ -873,7 +869,7 @@
assumes "finite \<F>" and S: "S \<subseteq> \<Union>\<F>" "closed S" and T: "convex T" "bounded T"
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X < aff_dim T"
- and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X \<and> (X \<inter> Y) face_of Y"
+ and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
and contf: "continuous_on S f" and fim: "f ` S \<subseteq> rel_frontier T"
obtains g where "continuous_on (\<Union>\<F>) g"
"g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
@@ -888,7 +884,7 @@
and diaG: "\<And>X. X \<in> \<G> \<Longrightarrow> diameter X < d"
and polyG: "\<And>X. X \<in> \<G> \<Longrightarrow> polytope X"
and affG: "\<And>X. X \<in> \<G> \<Longrightarrow> aff_dim X \<le> aff_dim T - 1"
- and faceG: "\<And>X Y. \<lbrakk>X \<in> \<G>; Y \<in> \<G>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+ and faceG: "\<And>X Y. \<lbrakk>X \<in> \<G>; Y \<in> \<G>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
proof (rule cell_complex_subdivision_exists [OF \<open>d>0\<close> \<open>finite \<F>\<close> poly _ face])
show "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> aff_dim T - 1"
by (simp add: aff)
@@ -928,7 +924,7 @@
assumes "finite \<F>" and S: "S \<subseteq> \<Union>\<F>" "closed S" and T: "convex T" "bounded T"
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> aff_dim T"
- and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X \<and> (X \<inter> Y) face_of Y"
+ and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
and contf: "continuous_on S f" and fim: "f ` S \<subseteq> rel_frontier T"
obtains C g where "finite C" "disjnt C S" "continuous_on (\<Union>\<F> - C) g"
"g ` (\<Union>\<F> - C) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
@@ -943,7 +939,7 @@
and diaG: "\<And>X. X \<in> \<G> \<Longrightarrow> diameter X < d"
and polyG: "\<And>X. X \<in> \<G> \<Longrightarrow> polytope X"
and affG: "\<And>X. X \<in> \<G> \<Longrightarrow> aff_dim X \<le> aff_dim T"
- and faceG: "\<And>X Y. \<lbrakk>X \<in> \<G>; Y \<in> \<G>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+ and faceG: "\<And>X Y. \<lbrakk>X \<in> \<G>; Y \<in> \<G>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
by (rule cell_complex_subdivision_exists [OF \<open>d>0\<close> \<open>finite \<F>\<close> poly aff face]) auto
obtain C h where "finite C" and dis: "disjnt C (\<Union>(\<G> \<inter> Pow V))"
and card: "card C \<le> card \<G>" and conth: "continuous_on (\<Union>\<G> - C) h"
@@ -978,8 +974,7 @@
show "h x = f x" if "x \<in> S" for x
proof -
have "h x = g x"
- apply (rule hg)
- using Ssub that by blast
+ using Ssub hg that by blast
also have "... = f x"
by (simp add: gf that)
finally show "h x = f x" .
@@ -1054,7 +1049,7 @@
using \<open>compact S\<close> compact_eq_bounded_closed by auto
show poly: "\<And>X. X \<in> {bbox \<inter> T} \<Longrightarrow> polytope X"
by (simp add: polytope_Int_polyhedron bbox_def polytope_interval affine_imp_polyhedron \<open>affine T\<close>)
- show "\<And>X Y. \<lbrakk>X \<in> {bbox \<inter> T}; Y \<in> {bbox \<inter> T}\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+ show "\<And>X Y. \<lbrakk>X \<in> {bbox \<inter> T}; Y \<in> {bbox \<inter> T}\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
by (simp add:poly face_of_refl polytope_imp_convex)
show "\<And>X. X \<in> {bbox \<inter> T} \<Longrightarrow> aff_dim X \<le> aff_dim U"
by (simp add: \<open>aff_dim (bbox \<inter> T) \<le> aff_dim U\<close>)
@@ -3886,7 +3881,7 @@
by (auto simp: homotopic_with_imp_continuous dest: homotopic_with_imp_subset1 homotopic_with_imp_subset2)
next
assume ?rhs then show ?lhs
- by (force simp: elim: homotopic_with_eq dest: homotopic_with_sphere_times [where h=g])
+ by (elim conjE homotopic_with_eq [OF homotopic_with_sphere_times]; force)
qed
then show ?thesis
by (simp add: *)
--- a/src/HOL/Analysis/Polytope.thy Sun Apr 19 13:01:40 2020 +0100
+++ b/src/HOL/Analysis/Polytope.thy Sun Apr 19 22:16:57 2020 +0100
@@ -2913,7 +2913,7 @@
assumes "finite \<F>"
and "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
and "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> d"
- and "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X \<and> (X \<inter> Y) face_of Y"
+ and "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
and "finite I"
shows "\<exists>\<G>. \<Union>\<G> = \<Union>\<F> \<and>
finite \<G> \<and>
@@ -2921,7 +2921,7 @@
(\<forall>C \<in> \<F>. \<forall>x \<in> C. \<exists>D. D \<in> \<G> \<and> x \<in> D \<and> D \<subseteq> C) \<and>
(\<forall>X \<in> \<G>. polytope X) \<and>
(\<forall>X \<in> \<G>. aff_dim X \<le> d) \<and>
- (\<forall>X \<in> \<G>. \<forall>Y \<in> \<G>. X \<inter> Y face_of X \<and> X \<inter> Y face_of Y) \<and>
+ (\<forall>X \<in> \<G>. \<forall>Y \<in> \<G>. X \<inter> Y face_of X) \<and>
(\<forall>X \<in> \<G>. \<forall>x \<in> X. \<forall>y \<in> X. \<forall>a b.
(a,b) \<in> I \<longrightarrow> a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or>
a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b)"
@@ -2937,7 +2937,7 @@
and sub2: "\<And>C x. C \<in> \<F> \<and> x \<in> C \<Longrightarrow> \<exists>D. D \<in> \<G> \<and> x \<in> D \<and> D \<subseteq> C"
and poly: "\<And>X. X \<in> \<G> \<Longrightarrow> polytope X"
and aff: "\<And>X. X \<in> \<G> \<Longrightarrow> aff_dim X \<le> d"
- and face: "\<And>X Y. \<lbrakk>X \<in> \<G>; Y \<in> \<G>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+ and face: "\<And>X Y. \<lbrakk>X \<in> \<G>; Y \<in> \<G>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
and I: "\<And>X x y a b. \<lbrakk>X \<in> \<G>; x \<in> X; y \<in> X; (a,b) \<in> I\<rbrakk> \<Longrightarrow>
a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or> a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
by (auto simp: that)
@@ -2960,7 +2960,7 @@
(a,b) \<in> insert ab I \<longrightarrow> a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or>
a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
using \<open>ab = (a, b)\<close> I by fastforce
- show "\<forall>X \<in> ?\<G>. \<forall>Y \<in> ?\<G>. X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+ show "\<forall>X \<in> ?\<G>. \<forall>Y \<in> ?\<G>. X \<inter> Y face_of X"
by (auto simp: eqInt halfspace_Int_eq face_of_Int_Int face face_of_halfspace_le face_of_halfspace_ge)
show "\<forall>C \<in> ?\<G>. \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
using sub1 by force
@@ -2984,10 +2984,10 @@
assumes "0 < e" "finite \<F>"
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> d"
- and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+ and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
obtains "\<F>'" where "finite \<F>'" "\<Union>\<F>' = \<Union>\<F>" "\<And>X. X \<in> \<F>' \<Longrightarrow> diameter X < e"
"\<And>X. X \<in> \<F>' \<Longrightarrow> polytope X" "\<And>X. X \<in> \<F>' \<Longrightarrow> aff_dim X \<le> d"
- "\<And>X Y. \<lbrakk>X \<in> \<F>'; Y \<in> \<F>'\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+ "\<And>X Y. \<lbrakk>X \<in> \<F>'; Y \<in> \<F>'\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
"\<And>C. C \<in> \<F>' \<Longrightarrow> \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
"\<And>C x. C \<in> \<F> \<and> x \<in> C \<Longrightarrow> \<exists>D. D \<in> \<F>' \<and> x \<in> D \<and> D \<subseteq> C"
proof -
@@ -3009,7 +3009,7 @@
obtain \<F>' where eq: "\<Union>\<F>' = \<Union>\<F>" and "finite \<F>'"
and poly: "\<And>X. X \<in> \<F>' \<Longrightarrow> polytope X"
and aff: "\<And>X. X \<in> \<F>' \<Longrightarrow> aff_dim X \<le> d"
- and face: "\<And>X Y. \<lbrakk>X \<in> \<F>'; Y \<in> \<F>'\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+ and face: "\<And>X Y. \<lbrakk>X \<in> \<F>'; Y \<in> \<F>'\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
and I: "\<And>X x y a b. \<lbrakk>X \<in> \<F>'; x \<in> X; y \<in> X; (a,b) \<in> I\<rbrakk> \<Longrightarrow>
a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or> a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
and sub1: "\<And>C. C \<in> \<F>' \<Longrightarrow> \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
@@ -3214,15 +3214,13 @@
finite \<C> \<and>
(\<forall>S \<in> \<C>. \<exists>n. n simplex S) \<and>
(\<forall>F S. S \<in> \<C> \<and> F face_of S \<longrightarrow> F \<in> \<C>) \<and>
- (\<forall>S S'. S \<in> \<C> \<and> S' \<in> \<C>
- \<longrightarrow> (S \<inter> S') face_of S \<and> (S \<inter> S') face_of S')"
+ (\<forall>S S'. S \<in> \<C> \<and> S' \<in> \<C> \<longrightarrow> (S \<inter> S') face_of S)"
definition\<^marker>\<open>tag important\<close> triangulation where
"triangulation \<T> \<equiv>
finite \<T> \<and>
(\<forall>T \<in> \<T>. \<exists>n. n simplex T) \<and>
- (\<forall>T T'. T \<in> \<T> \<and> T' \<in> \<T>
- \<longrightarrow> (T \<inter> T') face_of T \<and> (T \<inter> T') face_of T')"
+ (\<forall>T T'. T \<in> \<T> \<and> T' \<in> \<T> \<longrightarrow> (T \<inter> T') face_of T)"
subsection\<open>Refining a cell complex to a simplicial complex\<close>
@@ -3312,7 +3310,7 @@
and "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
and "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
and "\<And>C F. \<lbrakk>C \<in> \<M>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<M>"
- and "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+ and "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1"
shows "\<exists>\<T>. simplicial_complex \<T> \<and>
(\<forall>K \<in> \<T>. aff_dim K \<le> of_nat n) \<and>
\<Union>\<T> = \<Union>\<M> \<and>
@@ -3322,9 +3320,9 @@
proof (induction n arbitrary: \<M> rule: less_induct)
case (less n)
then have poly\<M>: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
- and aff\<M>: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
- and face\<M>: "\<And>C F. \<lbrakk>C \<in> \<M>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<M>"
- and intface\<M>: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+ and aff\<M>: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
+ and face\<M>: "\<And>C F. \<lbrakk>C \<in> \<M>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<M>"
+ and intface\<M>: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1"
by metis+
show ?case
proof (cases "n \<le> 1")
@@ -3339,22 +3337,22 @@
case False
define \<S> where "\<S> \<equiv> {C \<in> \<M>. aff_dim C < n}"
have "finite \<S>" "\<And>C. C \<in> \<S> \<Longrightarrow> polytope C" "\<And>C. C \<in> \<S> \<Longrightarrow> aff_dim C \<le> int (n - 1)"
- "\<And>C F. \<lbrakk>C \<in> \<S>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<S>"
- "\<And>C1 C2. \<lbrakk>C1 \<in> \<S>; C2 \<in> \<S>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+ "\<And>C F. \<lbrakk>C \<in> \<S>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<S>"
+ "\<And>C1 C2. \<lbrakk>C1 \<in> \<S>; C2 \<in> \<S>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1"
using less.prems
- apply (auto simp: \<S>_def)
+ apply (auto simp: \<S>_def)
by (metis aff_dim_subset face_of_imp_subset less_le not_le)
with less.IH [of "n-1" \<S>] False
obtain \<U> where "simplicial_complex \<U>"
- and aff_dim\<U>: "\<And>K. K \<in> \<U> \<Longrightarrow> aff_dim K \<le> int (n - 1)"
- and "\<Union>\<U> = \<Union>\<S>"
- and fin\<U>: "\<And>C. C \<in> \<S> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<U> \<and> C = \<Union>F"
- and C\<U>: "\<And>K. K \<in> \<U> \<Longrightarrow> \<exists>C. C \<in> \<S> \<and> K \<subseteq> C"
+ and aff_dim\<U>: "\<And>K. K \<in> \<U> \<Longrightarrow> aff_dim K \<le> int (n - 1)"
+ and "\<Union>\<U> = \<Union>\<S>"
+ and fin\<U>: "\<And>C. C \<in> \<S> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<U> \<and> C = \<Union>F"
+ and C\<U>: "\<And>K. K \<in> \<U> \<Longrightarrow> \<exists>C. C \<in> \<S> \<and> K \<subseteq> C"
by auto
then have "finite \<U>"
- and simpl\<U>: "\<And>S. S \<in> \<U> \<Longrightarrow> \<exists>n. n simplex S"
- and face\<U>: "\<And>F S. \<lbrakk>S \<in> \<U>; F face_of S\<rbrakk> \<Longrightarrow> F \<in> \<U>"
- and faceI\<U>: "\<And>S S'. \<lbrakk>S \<in> \<U>; S' \<in> \<U>\<rbrakk> \<Longrightarrow> (S \<inter> S') face_of S \<and> (S \<inter> S') face_of S'"
+ and simpl\<U>: "\<And>S. S \<in> \<U> \<Longrightarrow> \<exists>n. n simplex S"
+ and face\<U>: "\<And>F S. \<lbrakk>S \<in> \<U>; F face_of S\<rbrakk> \<Longrightarrow> F \<in> \<U>"
+ and faceI\<U>: "\<And>S S'. \<lbrakk>S \<in> \<U>; S' \<in> \<U>\<rbrakk> \<Longrightarrow> (S \<inter> S') face_of S"
by (auto simp: simplicial_complex_def)
define \<N> where "\<N> \<equiv> {C \<in> \<M>. aff_dim C = n}"
have "finite \<N>"
@@ -3364,7 +3362,7 @@
and closed\<N>: "\<And>C. C \<in> \<N> \<Longrightarrow> closed C"
by (auto simp: \<N>_def poly\<M> polytope_imp_convex polytope_imp_closed)
have in_rel_interior: "(SOME z. z \<in> rel_interior C) \<in> rel_interior C" if "C \<in> \<N>" for C
- using that poly\<M> polytope_imp_convex rel_interior_aff_dim some_in_eq by (fastforce simp: \<N>_def)
+ using that poly\<M> polytope_imp_convex rel_interior_aff_dim some_in_eq by (fastforce simp: \<N>_def)
have *: "\<exists>T. \<not> affine_dependent T \<and> card T \<le> n \<and> aff_dim K < n \<and> K = convex hull T"
if "K \<in> \<U>" for K
proof -
@@ -3392,7 +3390,7 @@
by (simp add: \<open>closed C\<close> rel_frontier_def subset_iff)
finally have "K \<subseteq> C" .
have "L \<inter> C face_of C"
- using \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>L \<in> \<S>\<close> intface\<M> by auto
+ using \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>L \<in> \<S>\<close> intface\<M> by (simp add: inf_commute)
moreover have "L \<inter> C \<noteq> C"
using \<open>C \<in> \<N>\<close> \<open>L \<in> \<S>\<close>
apply (clarsimp simp: \<N>_def \<S>_def)
@@ -3480,192 +3478,185 @@
ultimately show ?thesis
using that by auto
qed
- have "(S \<inter> S' face_of S) \<and> (S \<inter> S' face_of S')"
- if "S \<in> \<U> \<union> ?\<T>" "S' \<in> \<U> \<union> ?\<T>" for S S'
+ have \<section>: "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+ if XY: "X \<in> \<U>" "Y \<in> ?\<T>" for X Y
proof -
- have symmy: "\<lbrakk>\<And>X Y. R X Y \<Longrightarrow> R Y X;
- \<And>X Y. \<lbrakk>X \<in> \<U>; Y \<in> \<U>\<rbrakk> \<Longrightarrow> R X Y;
- \<And>X Y. \<lbrakk>X \<in> \<U>; Y \<in> ?\<T>\<rbrakk> \<Longrightarrow> R X Y;
- \<And>X Y. \<lbrakk>X \<in> ?\<T>; Y \<in> ?\<T>\<rbrakk> \<Longrightarrow> R X Y\<rbrakk> \<Longrightarrow> R S S'" for R
- using that by (metis (no_types, lifting) Un_iff)
- show ?thesis
- proof (rule symmy)
- show "Y \<inter> X face_of Y \<and> Y \<inter> X face_of X"
- if "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y" for X Y :: "'a set"
- by (simp add: inf_commute that)
- next
- show "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
- if "X \<in> \<U>" and "Y \<in> \<U>" for X Y
- by (simp add: faceI\<U> that)
- next
- show "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
- if XY: "X \<in> \<U>" "Y \<in> ?\<T>" for X Y
- proof -
- obtain C K
- where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
- and Y: "Y = convex hull insert (SOME z. z \<in> rel_interior C) K"
- using XY by blast
- have "convex C"
- by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
- have "K \<subseteq> C"
- by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_iff)
- let ?z = "(SOME z. z \<in> rel_interior C)"
- have z: "?z \<in> rel_interior C"
- using \<open>C \<in> \<N>\<close> in_rel_interior by blast
- obtain D where "D \<in> \<S>" "X \<subseteq> D"
- using C\<U> \<open>X \<in> \<U>\<close> by blast
- have "D \<inter> rel_interior C = (C \<inter> D) \<inter> rel_interior C"
- using rel_interior_subset by blast
- also have "(C \<inter> D) \<inter> rel_interior C = {}"
- proof (rule face_of_disjoint_rel_interior)
- show "C \<inter> D face_of C"
- using \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<S>\<close> intface\<M> by blast
- show "C \<inter> D \<noteq> C"
- by (metis (mono_tags, lifting) Int_lower2 \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<S>\<close> aff_dim_subset mem_Collect_eq not_le)
- qed
- finally have DC: "D \<inter> rel_interior C = {}" .
- have eq: "X \<inter> convex hull (insert ?z K) = X \<inter> convex hull K"
- apply (rule Int_convex_hull_insert_rel_exterior [OF \<open>convex C\<close> \<open>K \<subseteq> C\<close> z])
- using DC by (meson \<open>X \<subseteq> D\<close> disjnt_def disjnt_subset1)
- obtain I where I: "\<not> affine_dependent I"
- and Keq: "K = convex hull I" and [simp]: "convex hull K = K"
- using "*" \<open>K \<in> \<U>\<close> by force
- then have "?z \<notin> affine hull I"
- using ahK_C_disjoint \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>K \<subseteq> rel_frontier C\<close> affine_hull_convex_hull z by blast
- have "X \<inter> K face_of K"
- by (simp add: \<open>K \<in> \<U>\<close> faceI\<U> \<open>X \<in> \<U>\<close>)
- also have "... face_of convex hull insert ?z K"
- by (metis I Keq \<open>?z \<notin> affine hull I\<close> aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert)
- finally have "X \<inter> K face_of convex hull insert ?z K" .
- then show ?thesis
- using "*" \<open>K \<in> \<U>\<close> faceI\<U> that(1) by (fastforce simp add: Y eq)
- qed
- next
- show "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
- if XY: "X \<in> ?\<T>" "Y \<in> ?\<T>" for X Y
- proof -
- obtain C K D L
- where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
+ obtain C K
+ where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
+ and Y: "Y = convex hull insert (SOME z. z \<in> rel_interior C) K"
+ using XY by blast
+ have "convex C"
+ by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
+ have "K \<subseteq> C"
+ by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_iff)
+ let ?z = "(SOME z. z \<in> rel_interior C)"
+ have z: "?z \<in> rel_interior C"
+ using \<open>C \<in> \<N>\<close> in_rel_interior by blast
+ obtain D where "D \<in> \<S>" "X \<subseteq> D"
+ using C\<U> \<open>X \<in> \<U>\<close> by blast
+ have "D \<inter> rel_interior C = (C \<inter> D) \<inter> rel_interior C"
+ using rel_interior_subset by blast
+ also have "(C \<inter> D) \<inter> rel_interior C = {}"
+ proof (rule face_of_disjoint_rel_interior)
+ show "C \<inter> D face_of C"
+ using \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<S>\<close> intface\<M> by blast
+ show "C \<inter> D \<noteq> C"
+ by (metis (mono_tags, lifting) Int_lower2 \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<S>\<close> aff_dim_subset mem_Collect_eq not_le)
+ qed
+ finally have DC: "D \<inter> rel_interior C = {}" .
+ have eq: "X \<inter> convex hull (insert ?z K) = X \<inter> convex hull K"
+ apply (rule Int_convex_hull_insert_rel_exterior [OF \<open>convex C\<close> \<open>K \<subseteq> C\<close> z])
+ using DC by (meson \<open>X \<subseteq> D\<close> disjnt_def disjnt_subset1)
+ obtain I where I: "\<not> affine_dependent I"
+ and Keq: "K = convex hull I" and [simp]: "convex hull K = K"
+ using "*" \<open>K \<in> \<U>\<close> by force
+ then have "?z \<notin> affine hull I"
+ using ahK_C_disjoint \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>K \<subseteq> rel_frontier C\<close> affine_hull_convex_hull z by blast
+ have "X \<inter> K face_of K"
+ by (simp add: XY(1) \<open>K \<in> \<U>\<close> faceI\<U> inf_commute)
+ also have "... face_of convex hull insert ?z K"
+ by (metis I Keq \<open>?z \<notin> affine hull I\<close> aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert)
+ finally have "X \<inter> K face_of convex hull insert ?z K" .
+ then show ?thesis
+ by (simp add: XY(1) Y \<open>K \<in> \<U>\<close> eq faceI\<U>)
+ qed
+
+ show "S \<inter> S' face_of S"
+ if "S \<in> \<U> \<union> ?\<T> \<and> S' \<in> \<U> \<union> ?\<T>" for S S'
+ using that
+ proof (elim conjE UnE)
+ fix X Y
+ assume "X \<in> \<U>" and "Y \<in> \<U>"
+ then show "X \<inter> Y face_of X"
+ by (simp add: faceI\<U>)
+ next
+ fix X Y
+ assume XY: "X \<in> \<U>" "Y \<in> ?\<T>"
+ then show "X \<inter> Y face_of X" "Y \<inter> X face_of Y"
+ using \<section> [OF XY] by (auto simp: Int_commute)
+ next
+ fix X Y
+ assume XY: "X \<in> ?\<T>" "Y \<in> ?\<T>"
+ show "X \<inter> Y face_of X"
+ proof -
+ obtain C K D L
+ where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
and X: "X = convex hull insert (SOME z. z \<in> rel_interior C) K"
and "D \<in> \<N>" "L \<in> \<U>" "L \<subseteq> rel_frontier D"
and Y: "Y = convex hull insert (SOME z. z \<in> rel_interior D) L"
- using XY by blast
- let ?z = "(SOME z. z \<in> rel_interior C)"
- have z: "?z \<in> rel_interior C"
- using \<open>C \<in> \<N>\<close> in_rel_interior by blast
+ using XY by blast
+ let ?z = "(SOME z. z \<in> rel_interior C)"
+ have z: "?z \<in> rel_interior C"
+ using \<open>C \<in> \<N>\<close> in_rel_interior by blast
+ have "convex C"
+ by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
+ have "convex K"
+ using "*" \<open>K \<in> \<U>\<close> by blast
+ have "convex L"
+ by (meson \<open>L \<in> \<U>\<close> convex_simplex simpl\<U>)
+ show ?thesis
+ proof (cases "D=C")
+ case True
+ then have "L \<subseteq> rel_frontier C"
+ using \<open>L \<subseteq> rel_frontier D\<close> by auto
+ show ?thesis
+ apply (simp add: X Y True)
+ apply (simp add: convex_hull_insert_Int_eq [OF z] \<open>K \<subseteq> rel_frontier C\<close> \<open>L \<subseteq> rel_frontier C\<close> \<open>convex C\<close> \<open>convex K\<close> \<open>convex L\<close>)
+ using face_of_polytope_insert2
+ by (metis "*" IntI \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close>\<open>K \<subseteq> rel_frontier C\<close> \<open>L \<subseteq> rel_frontier C\<close> aff_independent_finite ahK_C_disjoint empty_iff faceI\<U> polytope_convex_hull z)
+ next
+ case False
+ have "convex D"
+ by (simp add: \<open>D \<in> \<N>\<close> convex\<N>)
+ have "K \<subseteq> C"
+ by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
+ have "L \<subseteq> D"
+ by (metis DiffE \<open>D \<in> \<N>\<close> \<open>L \<subseteq> rel_frontier D\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
+ let ?w = "(SOME w. w \<in> rel_interior D)"
+ have w: "?w \<in> rel_interior D"
+ using \<open>D \<in> \<N>\<close> in_rel_interior by blast
+ have "C \<inter> rel_interior D = (D \<inter> C) \<inter> rel_interior D"
+ using rel_interior_subset by blast
+ also have "(D \<inter> C) \<inter> rel_interior D = {}"
+ proof (rule face_of_disjoint_rel_interior)
+ show "D \<inter> C face_of D"
+ using \<N>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<N>\<close> intface\<M> by blast
+ have "D \<in> \<M> \<and> aff_dim D = int n"
+ using \<N>_def \<open>D \<in> \<N>\<close> by blast
+ moreover have "C \<in> \<M> \<and> aff_dim C = int n"
+ using \<N>_def \<open>C \<in> \<N>\<close> by blast
+ ultimately show "D \<inter> C \<noteq> D"
+ by (metis Int_commute False face_of_aff_dim_lt inf.idem inf_le1 intface\<M> not_le poly\<M> polytope_imp_convex)
+ qed
+ finally have CD: "C \<inter> (rel_interior D) = {}" .
+ have zKC: "(convex hull insert ?z K) \<subseteq> C"
+ by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed convex\<N> hull_minimal insert_subset rel_frontier_def rel_interior_subset subset_iff z)
+ have eq: "convex hull (insert ?z K) \<inter> convex hull (insert ?w L) =
+ convex hull (insert ?z K) \<inter> convex hull L"
+ apply (rule Int_convex_hull_insert_rel_exterior [OF \<open>convex D\<close> \<open>L \<subseteq> D\<close> w])
+ using zKC CD apply (force simp: disjnt_def)
+ done
+ have ch_id: "convex hull K = K" "convex hull L = L"
+ using "*" \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> hull_same by auto
have "convex C"
by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
- have "convex K"
- using "*" \<open>K \<in> \<U>\<close> by blast
- have "convex L"
- by (meson \<open>L \<in> \<U>\<close> convex_simplex simpl\<U>)
- show ?thesis
- proof (cases "D=C")
- case True
- then have "L \<subseteq> rel_frontier C"
- using \<open>L \<subseteq> rel_frontier D\<close> by auto
- show ?thesis
- apply (simp add: X Y True)
- apply (simp add: convex_hull_insert_Int_eq [OF z] \<open>K \<subseteq> rel_frontier C\<close> \<open>L \<subseteq> rel_frontier C\<close> \<open>convex C\<close> \<open>convex K\<close> \<open>convex L\<close>)
- using face_of_polytope_insert2
- by (metis "*" IntI \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close>\<open>K \<subseteq> rel_frontier C\<close> \<open>L \<subseteq> rel_frontier C\<close> aff_independent_finite ahK_C_disjoint empty_iff faceI\<U> polytope_convex_hull z)
- next
- case False
- have "convex D"
- by (simp add: \<open>D \<in> \<N>\<close> convex\<N>)
- have "K \<subseteq> C"
- by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
- have "L \<subseteq> D"
- by (metis DiffE \<open>D \<in> \<N>\<close> \<open>L \<subseteq> rel_frontier D\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
- let ?w = "(SOME w. w \<in> rel_interior D)"
- have w: "?w \<in> rel_interior D"
- using \<open>D \<in> \<N>\<close> in_rel_interior by blast
- have "C \<inter> rel_interior D = (D \<inter> C) \<inter> rel_interior D"
- using rel_interior_subset by blast
- also have "(D \<inter> C) \<inter> rel_interior D = {}"
+ have "convex hull (insert ?z K) \<inter> L = L \<inter> convex hull (insert ?z K)"
+ by blast
+ also have "... = convex hull K \<inter> L"
+ proof (subst Int_convex_hull_insert_rel_exterior [OF \<open>convex C\<close> \<open>K \<subseteq> C\<close> z])
+ have "(C \<inter> D) \<inter> rel_interior C = {}"
proof (rule face_of_disjoint_rel_interior)
- show "D \<inter> C face_of D"
+ show "C \<inter> D face_of C"
using \<N>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<N>\<close> intface\<M> by blast
- have "D \<in> \<M> \<and> aff_dim D = int n"
- using \<N>_def \<open>D \<in> \<N>\<close> by blast
- moreover have "C \<in> \<M> \<and> aff_dim C = int n"
- using \<N>_def \<open>C \<in> \<N>\<close> by blast
- ultimately show "D \<inter> C \<noteq> D"
- by (metis False face_of_aff_dim_lt inf.idem inf_le1 intface\<M> not_le poly\<M> polytope_imp_convex)
+ have "D \<in> \<M>" "aff_dim D = int n"
+ using \<N>_def \<open>D \<in> \<N>\<close> by fastforce+
+ moreover have "C \<in> \<M>" "aff_dim C = int n"
+ using \<N>_def \<open>C \<in> \<N>\<close> by fastforce+
+ ultimately have "aff_dim D + - 1 * aff_dim C \<le> 0"
+ by fastforce
+ then have "\<not> C face_of D"
+ using False \<open>convex D\<close> face_of_aff_dim_lt by fastforce
+ show "C \<inter> D \<noteq> C"
+ by (metis inf_commute \<open>C \<in> \<M>\<close> \<open>D \<in> \<M>\<close> \<open>\<not> C face_of D\<close> intface\<M>)
qed
- finally have CD: "C \<inter> (rel_interior D) = {}" .
- have zKC: "(convex hull insert ?z K) \<subseteq> C"
- by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed convex\<N> hull_minimal insert_subset rel_frontier_def rel_interior_subset subset_iff z)
- have eq: "convex hull (insert ?z K) \<inter> convex hull (insert ?w L) =
- convex hull (insert ?z K) \<inter> convex hull L"
- apply (rule Int_convex_hull_insert_rel_exterior [OF \<open>convex D\<close> \<open>L \<subseteq> D\<close> w])
- using zKC CD apply (force simp: disjnt_def)
- done
- have ch_id: "convex hull K = K" "convex hull L = L"
- using "*" \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> hull_same by auto
- have "convex C"
- by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
- have "convex hull (insert ?z K) \<inter> L = L \<inter> convex hull (insert ?z K)"
- by blast
- also have "... = convex hull K \<inter> L"
- proof (subst Int_convex_hull_insert_rel_exterior [OF \<open>convex C\<close> \<open>K \<subseteq> C\<close> z])
- have "(C \<inter> D) \<inter> rel_interior C = {}"
- proof (rule face_of_disjoint_rel_interior)
- show "C \<inter> D face_of C"
- using \<N>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<N>\<close> intface\<M> by blast
- have "D \<in> \<M>" "aff_dim D = int n"
- using \<N>_def \<open>D \<in> \<N>\<close> by fastforce+
- moreover have "C \<in> \<M>" "aff_dim C = int n"
- using \<N>_def \<open>C \<in> \<N>\<close> by fastforce+
- ultimately have "aff_dim D + - 1 * aff_dim C \<le> 0"
- by fastforce
- then have "\<not> C face_of D"
- using False \<open>convex D\<close> face_of_aff_dim_lt by fastforce
- show "C \<inter> D \<noteq> C"
- using \<open>C \<in> \<M>\<close> \<open>D \<in> \<M>\<close> \<open>\<not> C face_of D\<close> intface\<M> by fastforce
- qed
- then have "D \<inter> rel_interior C = {}"
- by (metis inf.absorb_iff2 inf_assoc inf_sup_aci(1) rel_interior_subset)
- then show "disjnt L (rel_interior C)"
- by (meson \<open>L \<subseteq> D\<close> disjnt_def disjnt_subset1)
- next
- show "L \<inter> convex hull K = convex hull K \<inter> L"
- by force
- qed
- finally have chKL: "convex hull (insert ?z K) \<inter> L = convex hull K \<inter> L" .
- have "convex hull insert ?z K \<inter> convex hull L face_of K"
- by (simp add: \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> ch_id chKL faceI\<U>)
- also have "... face_of convex hull insert ?z K"
- proof -
- obtain I where I: "\<not> affine_dependent I" "K = convex hull I"
- using * [OF \<open>K \<in> \<U>\<close>] by auto
- then have "\<And>a. a \<notin> rel_interior C \<or> a \<notin> affine hull I"
- using ahK_C_disjoint \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>K \<subseteq> rel_frontier C\<close> affine_hull_convex_hull by blast
- then show ?thesis
- by (metis I affine_independent_insert face_of_convex_hull_affine_independent hull_insert subset_insertI z)
- qed
- finally have 1: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?z K" .
- have "convex hull insert ?z K \<inter> convex hull L face_of L"
- by (simp add: \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> ch_id chKL faceI\<U>)
- also have "... face_of convex hull insert ?w L"
- proof -
- obtain I where I: "\<not> affine_dependent I" "L = convex hull I"
- using * [OF \<open>L \<in> \<U>\<close>] by auto
- then have "\<And>a. a \<notin> rel_interior D \<or> a \<notin> affine hull I"
- using \<open>D \<in> \<N>\<close> \<open>L \<in> \<U>\<close> \<open>L \<subseteq> rel_frontier D\<close> affine_hull_convex_hull ahK_C_disjoint by blast
- then show ?thesis
- by (metis I aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert w)
- qed
- finally have 2: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?w L" .
- show ?thesis
- by (simp add: X Y eq 1 2)
+ then have "D \<inter> rel_interior C = {}"
+ by (metis inf.absorb_iff2 inf_assoc inf_sup_aci(1) rel_interior_subset)
+ then show "disjnt L (rel_interior C)"
+ by (meson \<open>L \<subseteq> D\<close> disjnt_def disjnt_subset1)
+ next
+ show "L \<inter> convex hull K = convex hull K \<inter> L"
+ by force
qed
+ finally have chKL: "convex hull (insert ?z K) \<inter> L = convex hull K \<inter> L" .
+ have "convex hull insert ?z K \<inter> convex hull L face_of K"
+ by (simp add: \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> ch_id chKL faceI\<U>)
+ also have "... face_of convex hull insert ?z K"
+ proof -
+ obtain I where I: "\<not> affine_dependent I" "K = convex hull I"
+ using * [OF \<open>K \<in> \<U>\<close>] by auto
+ then have "\<And>a. a \<notin> rel_interior C \<or> a \<notin> affine hull I"
+ using ahK_C_disjoint \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>K \<subseteq> rel_frontier C\<close> affine_hull_convex_hull by blast
+ then show ?thesis
+ by (metis I affine_independent_insert face_of_convex_hull_affine_independent hull_insert subset_insertI z)
+ qed
+ finally have 1: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?z K" .
+ have "convex hull insert ?z K \<inter> convex hull L face_of L"
+ by (metis \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> chKL ch_id faceI\<U> inf_commute)
+ also have "... face_of convex hull insert ?w L"
+ proof -
+ obtain I where I: "\<not> affine_dependent I" "L = convex hull I"
+ using * [OF \<open>L \<in> \<U>\<close>] by auto
+ then have "\<And>a. a \<notin> rel_interior D \<or> a \<notin> affine hull I"
+ using \<open>D \<in> \<N>\<close> \<open>L \<in> \<U>\<close> \<open>L \<subseteq> rel_frontier D\<close> affine_hull_convex_hull ahK_C_disjoint by blast
+ then show ?thesis
+ by (metis I aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert w)
+ qed
+ finally have 2: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?w L" .
+ show ?thesis
+ by (simp add: X Y eq 1 2)
qed
qed
- qed
- then
- show "S \<inter> S' face_of S" "S \<inter> S' face_of S'" if "S \<in> \<U> \<union> ?\<T> \<and> S' \<in> \<U> \<union> ?\<T>" for S S'
- using that by auto
+ qed
qed
show "\<exists>F \<subseteq> \<U> \<union> ?\<T>. C = \<Union>F" if "C \<in> \<M>" for C
proof (cases "C \<in> \<S>")
@@ -3772,7 +3763,7 @@
lemma simplicial_subdivision_of_cell_complex_lowdim:
assumes "finite \<M>"
and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
- and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+ and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1"
and aff: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> d"
obtains \<T> where "simplicial_complex \<T>" "\<And>K. K \<in> \<T> \<Longrightarrow> aff_dim K \<le> d"
"\<Union>\<T> = \<Union>\<M>"
@@ -3800,10 +3791,13 @@
if "G \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" and "F face_of G" for F G
using that face_of_trans by blast
next
- show "F1 \<inter> F2 face_of F1 \<and> F1 \<inter> F2 face_of F2"
- if "F1 \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" and "F2 \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" for F1 F2
- using that
- by safe (meson face face_of_Int_subface)+
+ fix F1 F2
+ assume "F1 \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" and "F2 \<in> (\<Union>C\<in>\<M>. {F. F face_of C})"
+ then obtain C1 C2 where "C1 \<in> \<M>" "C2 \<in> \<M>" and F: "F1 face_of C1" "F2 face_of C2"
+ by auto
+ show "F1 \<inter> F2 face_of F1"
+ using face_of_Int_subface [OF _ _ F]
+ by (metis \<open>C1 \<in> \<M>\<close> \<open>C2 \<in> \<M>\<close> face inf_commute)
qed
moreover
have "\<Union>(\<Union>C\<in>\<M>. {F. F face_of C}) = \<Union>\<M>"
@@ -3838,7 +3832,7 @@
proposition simplicial_subdivision_of_cell_complex:
assumes "finite \<M>"
and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
- and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+ and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1"
obtains \<T> where "simplicial_complex \<T>"
"\<Union>\<T> = \<Union>\<M>"
"\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
@@ -3848,7 +3842,7 @@
corollary fine_simplicial_subdivision_of_cell_complex:
assumes "0 < e" "finite \<M>"
and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
- and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+ and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1"
obtains \<T> where "simplicial_complex \<T>"
"\<And>K. K \<in> \<T> \<Longrightarrow> diameter K < e"
"\<Union>\<T> = \<Union>\<M>"
@@ -3857,7 +3851,7 @@
proof -
obtain \<N> where \<N>: "finite \<N>" "\<Union>\<N> = \<Union>\<M>"
and diapoly: "\<And>X. X \<in> \<N> \<Longrightarrow> diameter X < e" "\<And>X. X \<in> \<N> \<Longrightarrow> polytope X"
- and "\<And>X Y. \<lbrakk>X \<in> \<N>; Y \<in> \<N>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+ and "\<And>X Y. \<lbrakk>X \<in> \<N>; Y \<in> \<N>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
and \<N>covers: "\<And>C x. C \<in> \<M> \<and> x \<in> C \<Longrightarrow> \<exists>D. D \<in> \<N> \<and> x \<in> D \<and> D \<subseteq> C"
and \<N>covered: "\<And>C. C \<in> \<N> \<Longrightarrow> \<exists>D. D \<in> \<M> \<and> C \<subseteq> D"
by (blast intro: cell_complex_subdivision_exists [OF \<open>0 < e\<close> \<open>finite \<M>\<close> poly aff_dim_le_DIM face])
@@ -3952,7 +3946,7 @@
assumes "0 < e" "finite \<M>"
and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
and aff: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C = d"
- and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+ and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1"
obtains \<T> where "triangulation \<T>" "\<And>k. k \<in> \<T> \<Longrightarrow> diameter k < e"
"\<And>k. k \<in> \<T> \<Longrightarrow> aff_dim k = d" "\<Union>\<T> = \<Union>\<M>"
"\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>f. finite f \<and> f \<subseteq> \<T> \<and> C = \<Union>f"