section ‹Results connected with topological dimension.›
theory Brouwer_Fixpoint
imports Path_Connected
begin
lemma bij_betw_singleton_eq:
assumes f: "bij_betw f A B" and g: "bij_betw g A B" and a: "a ∈ A"
assumes eq: "(⋀x. x ∈ A ⟹ x ≠ a ⟹ f x = g x)"
shows "f a = g a"
proof -
have "f ` (A - {a}) = g ` (A - {a})"
by (intro image_cong) (simp_all add: eq)
then have "B - {f a} = B - {g a}"
using f g a by (auto simp: bij_betw_def inj_on_image_set_diff set_eq_iff Diff_subset)
moreover have "f a ∈ B" "g a ∈ B"
using f g a by (auto simp: bij_betw_def)
ultimately show ?thesis
by auto
qed
lemma swap_image:
"Fun.swap i j f ` A = (if i ∈ A then (if j ∈ A then f ` A else f ` ((A - {i}) ∪ {j}))
else (if j ∈ A then f ` ((A - {j}) ∪ {i}) else f ` A))"
apply (auto simp: Fun.swap_def image_iff)
apply metis
apply (metis member_remove remove_def)
apply (metis member_remove remove_def)
done
lemma swap_apply1: "Fun.swap x y f x = f y"
by (simp add: Fun.swap_def)
lemma swap_apply2: "Fun.swap x y f y = f x"
by (simp add: Fun.swap_def)
lemma lessThan_empty_iff: "{..< n::nat} = {} ⟷ n = 0"
by auto
lemma Zero_notin_Suc: "0 ∉ Suc ` A"
by auto
lemma atMost_Suc_eq_insert_0: "{.. Suc n} = insert 0 (Suc ` {.. n})"
apply auto
apply (case_tac x)
apply auto
done
lemma setsum_union_disjoint':
assumes "finite A"
and "finite B"
and "A ∩ B = {}"
and "A ∪ B = C"
shows "setsum g C = setsum g A + setsum g B"
using setsum.union_disjoint[OF assms(1-3)] and assms(4) by auto
lemma pointwise_minimal_pointwise_maximal:
fixes s :: "(nat ⇒ nat) set"
assumes "finite s"
and "s ≠ {}"
and "∀x∈s. ∀y∈s. x ≤ y ∨ y ≤ x"
shows "∃a∈s. ∀x∈s. a ≤ x"
and "∃a∈s. ∀x∈s. x ≤ a"
using assms
proof (induct s rule: finite_ne_induct)
case (insert b s)
assume *: "∀x∈insert b s. ∀y∈insert b s. x ≤ y ∨ y ≤ x"
moreover then obtain u l where "l ∈ s" "∀b∈s. l ≤ b" "u ∈ s" "∀b∈s. b ≤ u"
using insert by auto
ultimately show "∃a∈insert b s. ∀x∈insert b s. a ≤ x" "∃a∈insert b s. ∀x∈insert b s. x ≤ a"
using *[rule_format, of b u] *[rule_format, of b l] by (metis insert_iff order.trans)+
qed auto
lemma brouwer_compactness_lemma:
fixes f :: "'a::metric_space ⇒ 'b::real_normed_vector"
assumes "compact s"
and "continuous_on s f"
and "¬ (∃x∈s. f x = 0)"
obtains d where "0 < d" and "∀x∈s. d ≤ norm (f x)"
proof (cases "s = {}")
case True
show thesis
by (rule that [of 1]) (auto simp: True)
next
case False
have "continuous_on s (norm ∘ f)"
by (rule continuous_intros continuous_on_norm assms(2))+
with False obtain x where x: "x ∈ s" "∀y∈s. (norm ∘ f) x ≤ (norm ∘ f) y"
using continuous_attains_inf[OF assms(1), of "norm ∘ f"]
unfolding o_def
by auto
have "(norm ∘ f) x > 0"
using assms(3) and x(1)
by auto
then show ?thesis
by (rule that) (insert x(2), auto simp: o_def)
qed
lemma kuhn_labelling_lemma:
fixes P Q :: "'a::euclidean_space ⇒ bool"
assumes "∀x. P x ⟶ P (f x)"
and "∀x. P x ⟶ (∀i∈Basis. Q i ⟶ 0 ≤ x∙i ∧ x∙i ≤ 1)"
shows "∃l. (∀x.∀i∈Basis. l x i ≤ (1::nat)) ∧
(∀x.∀i∈Basis. P x ∧ Q i ∧ (x∙i = 0) ⟶ (l x i = 0)) ∧
(∀x.∀i∈Basis. P x ∧ Q i ∧ (x∙i = 1) ⟶ (l x i = 1)) ∧
(∀x.∀i∈Basis. P x ∧ Q i ∧ (l x i = 0) ⟶ x∙i ≤ f x∙i) ∧
(∀x.∀i∈Basis. P x ∧ Q i ∧ (l x i = 1) ⟶ f x∙i ≤ x∙i)"
proof -
{ fix x i
let ?R = "λy. (P x ∧ Q i ∧ x ∙ i = 0 ⟶ y = (0::nat)) ∧
(P x ∧ Q i ∧ x ∙ i = 1 ⟶ y = 1) ∧
(P x ∧ Q i ∧ y = 0 ⟶ x ∙ i ≤ f x ∙ i) ∧
(P x ∧ Q i ∧ y = 1 ⟶ f x ∙ i ≤ x ∙ i)"
{ assume "P x" "Q i" "i ∈ Basis" with assms have "0 ≤ f x ∙ i ∧ f x ∙ i ≤ 1" by auto }
then have "i ∈ Basis ⟹ ?R 0 ∨ ?R 1" by auto }
then show ?thesis
unfolding all_conj_distrib[symmetric] Ball_def
by (subst choice_iff[symmetric])+ blast
qed
subsection ‹The key "counting" observation, somewhat abstracted.›
lemma kuhn_counting_lemma:
fixes bnd compo compo' face S F
defines "nF s == card {f∈F. face f s ∧ compo' f}"
assumes [simp, intro]: "finite F" ― "faces" and [simp, intro]: "finite S" ― "simplices"
and "⋀f. f ∈ F ⟹ bnd f ⟹ card {s∈S. face f s} = 1"
and "⋀f. f ∈ F ⟹ ¬ bnd f ⟹ card {s∈S. face f s} = 2"
and "⋀s. s ∈ S ⟹ compo s ⟹ nF s = 1"
and "⋀s. s ∈ S ⟹ ¬ compo s ⟹ nF s = 0 ∨ nF s = 2"
and "odd (card {f∈F. compo' f ∧ bnd f})"
shows "odd (card {s∈S. compo s})"
proof -
have "(∑s | s ∈ S ∧ ¬ compo s. nF s) + (∑s | s ∈ S ∧ compo s. nF s) = (∑s∈S. nF s)"
by (subst setsum.union_disjoint[symmetric]) (auto intro!: setsum.cong)
also have "… = (∑s∈S. card {f ∈ {f∈F. compo' f ∧ bnd f}. face f s}) +
(∑s∈S. card {f ∈ {f∈F. compo' f ∧ ¬ bnd f}. face f s})"
unfolding setsum.distrib[symmetric]
by (subst card_Un_disjoint[symmetric])
(auto simp: nF_def intro!: setsum.cong arg_cong[where f=card])
also have "… = 1 * card {f∈F. compo' f ∧ bnd f} + 2 * card {f∈F. compo' f ∧ ¬ bnd f}"
using assms(4,5) by (fastforce intro!: arg_cong2[where f="op +"] setsum_multicount)
finally have "odd ((∑s | s ∈ S ∧ ¬ compo s. nF s) + card {s∈S. compo s})"
using assms(6,8) by simp
moreover have "(∑s | s ∈ S ∧ ¬ compo s. nF s) =
(∑s | s ∈ S ∧ ¬ compo s ∧ nF s = 0. nF s) + (∑s | s ∈ S ∧ ¬ compo s ∧ nF s = 2. nF s)"
using assms(7) by (subst setsum.union_disjoint[symmetric]) (fastforce intro!: setsum.cong)+
ultimately show ?thesis
by auto
qed
subsection ‹The odd/even result for faces of complete vertices, generalized.›
lemma kuhn_complete_lemma:
assumes [simp]: "finite simplices"
and face: "⋀f s. face f s ⟷ (∃a∈s. f = s - {a})"
and card_s[simp]: "⋀s. s ∈ simplices ⟹ card s = n + 2"
and rl_bd: "⋀s. s ∈ simplices ⟹ rl ` s ⊆ {..Suc n}"
and bnd: "⋀f s. s ∈ simplices ⟹ face f s ⟹ bnd f ⟹ card {s∈simplices. face f s} = 1"
and nbnd: "⋀f s. s ∈ simplices ⟹ face f s ⟹ ¬ bnd f ⟹ card {s∈simplices. face f s} = 2"
and odd_card: "odd (card {f. (∃s∈simplices. face f s) ∧ rl ` f = {..n} ∧ bnd f})"
shows "odd (card {s∈simplices. (rl ` s = {..Suc n})})"
proof (rule kuhn_counting_lemma)
have finite_s[simp]: "⋀s. s ∈ simplices ⟹ finite s"
by (metis add_is_0 zero_neq_numeral card_infinite assms(3))
let ?F = "{f. ∃s∈simplices. face f s}"
have F_eq: "?F = (⋃s∈simplices. ⋃a∈s. {s - {a}})"
by (auto simp: face)
show "finite ?F"
using ‹finite simplices› unfolding F_eq by auto
show "card {s ∈ simplices. face f s} = 1" if "f ∈ ?F" "bnd f" for f
using bnd that by auto
show "card {s ∈ simplices. face f s} = 2" if "f ∈ ?F" "¬ bnd f" for f
using nbnd that by auto
show "odd (card {f ∈ {f. ∃s∈simplices. face f s}. rl ` f = {..n} ∧ bnd f})"
using odd_card by simp
fix s assume s[simp]: "s ∈ simplices"
let ?S = "{f ∈ {f. ∃s∈simplices. face f s}. face f s ∧ rl ` f = {..n}}"
have "?S = (λa. s - {a}) ` {a∈s. rl ` (s - {a}) = {..n}}"
using s by (fastforce simp: face)
then have card_S: "card ?S = card {a∈s. rl ` (s - {a}) = {..n}}"
by (auto intro!: card_image inj_onI)
{ assume rl: "rl ` s = {..Suc n}"
then have inj_rl: "inj_on rl s"
by (intro eq_card_imp_inj_on) auto
moreover obtain a where "rl a = Suc n" "a ∈ s"
by (metis atMost_iff image_iff le_Suc_eq rl)
ultimately have n: "{..n} = rl ` (s - {a})"
by (auto simp add: inj_on_image_set_diff Diff_subset rl)
have "{a∈s. rl ` (s - {a}) = {..n}} = {a}"
using inj_rl ‹a ∈ s› by (auto simp add: n inj_on_image_eq_iff[OF inj_rl] Diff_subset)
then show "card ?S = 1"
unfolding card_S by simp }
{ assume rl: "rl ` s ≠ {..Suc n}"
show "card ?S = 0 ∨ card ?S = 2"
proof cases
assume *: "{..n} ⊆ rl ` s"
with rl rl_bd[OF s] have rl_s: "rl ` s = {..n}"
by (auto simp add: atMost_Suc subset_insert_iff split: if_split_asm)
then have "¬ inj_on rl s"
by (intro pigeonhole) simp
then obtain a b where ab: "a ∈ s" "b ∈ s" "rl a = rl b" "a ≠ b"
by (auto simp: inj_on_def)
then have eq: "rl ` (s - {a}) = rl ` s"
by auto
with ab have inj: "inj_on rl (s - {a})"
by (intro eq_card_imp_inj_on) (auto simp add: rl_s card_Diff_singleton_if)
{ fix x assume "x ∈ s" "x ∉ {a, b}"
then have "rl ` s - {rl x} = rl ` ((s - {a}) - {x})"
by (auto simp: eq Diff_subset inj_on_image_set_diff[OF inj])
also have "… = rl ` (s - {x})"
using ab ‹x ∉ {a, b}› by auto
also assume "… = rl ` s"
finally have False
using ‹x∈s› by auto }
moreover
{ fix x assume "x ∈ {a, b}" with ab have "x ∈ s ∧ rl ` (s - {x}) = rl ` s"
by (simp add: set_eq_iff image_iff Bex_def) metis }
ultimately have "{a∈s. rl ` (s - {a}) = {..n}} = {a, b}"
unfolding rl_s[symmetric] by fastforce
with ‹a ≠ b› show "card ?S = 0 ∨ card ?S = 2"
unfolding card_S by simp
next
assume "¬ {..n} ⊆ rl ` s"
then have "⋀x. rl ` (s - {x}) ≠ {..n}"
by auto
then show "card ?S = 0 ∨ card ?S = 2"
unfolding card_S by simp
qed }
qed fact
locale kuhn_simplex =
fixes p n and base upd and s :: "(nat ⇒ nat) set"
assumes base: "base ∈ {..< n} → {..< p}"
assumes base_out: "⋀i. n ≤ i ⟹ base i = p"
assumes upd: "bij_betw upd {..< n} {..< n}"
assumes s_pre: "s = (λi j. if j ∈ upd`{..< i} then Suc (base j) else base j) ` {.. n}"
begin
definition "enum i j = (if j ∈ upd`{..< i} then Suc (base j) else base j)"
lemma s_eq: "s = enum ` {.. n}"
unfolding s_pre enum_def[abs_def] ..
lemma upd_space: "i < n ⟹ upd i < n"
using upd by (auto dest!: bij_betwE)
lemma s_space: "s ⊆ {..< n} → {.. p}"
proof -
{ fix i assume "i ≤ n" then have "enum i ∈ {..< n} → {.. p}"
proof (induct i)
case 0 then show ?case
using base by (auto simp: Pi_iff less_imp_le enum_def)
next
case (Suc i) with base show ?case
by (auto simp: Pi_iff Suc_le_eq less_imp_le enum_def intro: upd_space)
qed }
then show ?thesis
by (auto simp: s_eq)
qed
lemma inj_upd: "inj_on upd {..< n}"
using upd by (simp add: bij_betw_def)
lemma inj_enum: "inj_on enum {.. n}"
proof -
{ fix x y :: nat assume "x ≠ y" "x ≤ n" "y ≤ n"
with upd have "upd ` {..< x} ≠ upd ` {..< y}"
by (subst inj_on_image_eq_iff[where C="{..< n}"]) (auto simp: bij_betw_def)
then have "enum x ≠ enum y"
by (auto simp add: enum_def fun_eq_iff) }
then show ?thesis
by (auto simp: inj_on_def)
qed
lemma enum_0: "enum 0 = base"
by (simp add: enum_def[abs_def])
lemma base_in_s: "base ∈ s"
unfolding s_eq by (subst enum_0[symmetric]) auto
lemma enum_in: "i ≤ n ⟹ enum i ∈ s"
unfolding s_eq by auto
lemma one_step:
assumes a: "a ∈ s" "j < n"
assumes *: "⋀a'. a' ∈ s ⟹ a' ≠ a ⟹ a' j = p'"
shows "a j ≠ p'"
proof
assume "a j = p'"
with * a have "⋀a'. a' ∈ s ⟹ a' j = p'"
by auto
then have "⋀i. i ≤ n ⟹ enum i j = p'"
unfolding s_eq by auto
from this[of 0] this[of n] have "j ∉ upd ` {..< n}"
by (auto simp: enum_def fun_eq_iff split: if_split_asm)
with upd ‹j < n› show False
by (auto simp: bij_betw_def)
qed
lemma upd_inj: "i < n ⟹ j < n ⟹ upd i = upd j ⟷ i = j"
using upd by (auto simp: bij_betw_def inj_on_eq_iff)
lemma upd_surj: "upd ` {..< n} = {..< n}"
using upd by (auto simp: bij_betw_def)
lemma in_upd_image: "A ⊆ {..< n} ⟹ i < n ⟹ upd i ∈ upd ` A ⟷ i ∈ A"
using inj_on_image_mem_iff[of upd "{..< n}"] upd
by (auto simp: bij_betw_def)
lemma enum_inj: "i ≤ n ⟹ j ≤ n ⟹ enum i = enum j ⟷ i = j"
using inj_enum by (auto simp: inj_on_eq_iff)
lemma in_enum_image: "A ⊆ {.. n} ⟹ i ≤ n ⟹ enum i ∈ enum ` A ⟷ i ∈ A"
using inj_on_image_mem_iff[OF inj_enum] by auto
lemma enum_mono: "i ≤ n ⟹ j ≤ n ⟹ enum i ≤ enum j ⟷ i ≤ j"
by (auto simp: enum_def le_fun_def in_upd_image Ball_def[symmetric])
lemma enum_strict_mono: "i ≤ n ⟹ j ≤ n ⟹ enum i < enum j ⟷ i < j"
using enum_mono[of i j] enum_inj[of i j] by (auto simp add: le_less)
lemma chain: "a ∈ s ⟹ b ∈ s ⟹ a ≤ b ∨ b ≤ a"
by (auto simp: s_eq enum_mono)
lemma less: "a ∈ s ⟹ b ∈ s ⟹ a i < b i ⟹ a < b"
using chain[of a b] by (auto simp: less_fun_def le_fun_def not_le[symmetric])
lemma enum_0_bot: "a ∈ s ⟹ a = enum 0 ⟷ (∀a'∈s. a ≤ a')"
unfolding s_eq by (auto simp: enum_mono Ball_def)
lemma enum_n_top: "a ∈ s ⟹ a = enum n ⟷ (∀a'∈s. a' ≤ a)"
unfolding s_eq by (auto simp: enum_mono Ball_def)
lemma enum_Suc: "i < n ⟹ enum (Suc i) = (enum i)(upd i := Suc (enum i (upd i)))"
by (auto simp: fun_eq_iff enum_def upd_inj)
lemma enum_eq_p: "i ≤ n ⟹ n ≤ j ⟹ enum i j = p"
by (induct i) (auto simp: enum_Suc enum_0 base_out upd_space not_less[symmetric])
lemma out_eq_p: "a ∈ s ⟹ n ≤ j ⟹ a j = p"
unfolding s_eq by (auto simp add: enum_eq_p)
lemma s_le_p: "a ∈ s ⟹ a j ≤ p"
using out_eq_p[of a j] s_space by (cases "j < n") auto
lemma le_Suc_base: "a ∈ s ⟹ a j ≤ Suc (base j)"
unfolding s_eq by (auto simp: enum_def)
lemma base_le: "a ∈ s ⟹ base j ≤ a j"
unfolding s_eq by (auto simp: enum_def)
lemma enum_le_p: "i ≤ n ⟹ j < n ⟹ enum i j ≤ p"
using enum_in[of i] s_space by auto
lemma enum_less: "a ∈ s ⟹ i < n ⟹ enum i < a ⟷ enum (Suc i) ≤ a"
unfolding s_eq by (auto simp: enum_strict_mono enum_mono)
lemma ksimplex_0:
"n = 0 ⟹ s = {(λx. p)}"
using s_eq enum_def base_out by auto
lemma replace_0:
assumes "j < n" "a ∈ s" and p: "∀x∈s - {a}. x j = 0" and "x ∈ s"
shows "x ≤ a"
proof cases
assume "x ≠ a"
have "a j ≠ 0"
using assms by (intro one_step[where a=a]) auto
with less[OF ‹x∈s› ‹a∈s›, of j] p[rule_format, of x] ‹x ∈ s› ‹x ≠ a›
show ?thesis
by auto
qed simp
lemma replace_1:
assumes "j < n" "a ∈ s" and p: "∀x∈s - {a}. x j = p" and "x ∈ s"
shows "a ≤ x"
proof cases
assume "x ≠ a"
have "a j ≠ p"
using assms by (intro one_step[where a=a]) auto
with enum_le_p[of _ j] ‹j < n› ‹a∈s›
have "a j < p"
by (auto simp: less_le s_eq)
with less[OF ‹a∈s› ‹x∈s›, of j] p[rule_format, of x] ‹x ∈ s› ‹x ≠ a›
show ?thesis
by auto
qed simp
end
locale kuhn_simplex_pair = s: kuhn_simplex p n b_s u_s s + t: kuhn_simplex p n b_t u_t t
for p n b_s u_s s b_t u_t t
begin
lemma enum_eq:
assumes l: "i ≤ l" "l ≤ j" and "j + d ≤ n"
assumes eq: "s.enum ` {i .. j} = t.enum ` {i + d .. j + d}"
shows "s.enum l = t.enum (l + d)"
using l proof (induct l rule: dec_induct)
case base
then have s: "s.enum i ∈ t.enum ` {i + d .. j + d}" and t: "t.enum (i + d) ∈ s.enum ` {i .. j}"
using eq by auto
from t ‹i ≤ j› ‹j + d ≤ n› have "s.enum i ≤ t.enum (i + d)"
by (auto simp: s.enum_mono)
moreover from s ‹i ≤ j› ‹j + d ≤ n› have "t.enum (i + d) ≤ s.enum i"
by (auto simp: t.enum_mono)
ultimately show ?case
by auto
next
case (step l)
moreover from step.prems ‹j + d ≤ n› have
"s.enum l < s.enum (Suc l)"
"t.enum (l + d) < t.enum (Suc l + d)"
by (simp_all add: s.enum_strict_mono t.enum_strict_mono)
moreover have
"s.enum (Suc l) ∈ t.enum ` {i + d .. j + d}"
"t.enum (Suc l + d) ∈ s.enum ` {i .. j}"
using step ‹j + d ≤ n› eq by (auto simp: s.enum_inj t.enum_inj)
ultimately have "s.enum (Suc l) = t.enum (Suc (l + d))"
using ‹j + d ≤ n›
by (intro antisym s.enum_less[THEN iffD1] t.enum_less[THEN iffD1])
(auto intro!: s.enum_in t.enum_in)
then show ?case by simp
qed
lemma ksimplex_eq_bot:
assumes a: "a ∈ s" "⋀a'. a' ∈ s ⟹ a ≤ a'"
assumes b: "b ∈ t" "⋀b'. b' ∈ t ⟹ b ≤ b'"
assumes eq: "s - {a} = t - {b}"
shows "s = t"
proof cases
assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp
next
assume "n ≠ 0"
have "s.enum 0 = (s.enum (Suc 0)) (u_s 0 := s.enum (Suc 0) (u_s 0) - 1)"
"t.enum 0 = (t.enum (Suc 0)) (u_t 0 := t.enum (Suc 0) (u_t 0) - 1)"
using ‹n ≠ 0› by (simp_all add: s.enum_Suc t.enum_Suc)
moreover have e0: "a = s.enum 0" "b = t.enum 0"
using a b by (simp_all add: s.enum_0_bot t.enum_0_bot)
moreover
{ fix j assume "0 < j" "j ≤ n"
moreover have "s - {a} = s.enum ` {Suc 0 .. n}" "t - {b} = t.enum ` {Suc 0 .. n}"
unfolding s.s_eq t.s_eq e0 by (auto simp: s.enum_inj t.enum_inj)
ultimately have "s.enum j = t.enum j"
using enum_eq[of "1" j n 0] eq by auto }
note enum_eq = this
then have "s.enum (Suc 0) = t.enum (Suc 0)"
using ‹n ≠ 0› by auto
moreover
{ fix j assume "Suc j < n"
with enum_eq[of "Suc j"] enum_eq[of "Suc (Suc j)"]
have "u_s (Suc j) = u_t (Suc j)"
using s.enum_Suc[of "Suc j"] t.enum_Suc[of "Suc j"]
by (auto simp: fun_eq_iff split: if_split_asm) }
then have "⋀j. 0 < j ⟹ j < n ⟹ u_s j = u_t j"
by (auto simp: gr0_conv_Suc)
with ‹n ≠ 0› have "u_t 0 = u_s 0"
by (intro bij_betw_singleton_eq[OF t.upd s.upd, of 0]) auto
ultimately have "a = b"
by simp
with assms show "s = t"
by auto
qed
lemma ksimplex_eq_top:
assumes a: "a ∈ s" "⋀a'. a' ∈ s ⟹ a' ≤ a"
assumes b: "b ∈ t" "⋀b'. b' ∈ t ⟹ b' ≤ b"
assumes eq: "s - {a} = t - {b}"
shows "s = t"
proof (cases n)
assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp
next
case (Suc n')
have "s.enum n = (s.enum n') (u_s n' := Suc (s.enum n' (u_s n')))"
"t.enum n = (t.enum n') (u_t n' := Suc (t.enum n' (u_t n')))"
using Suc by (simp_all add: s.enum_Suc t.enum_Suc)
moreover have en: "a = s.enum n" "b = t.enum n"
using a b by (simp_all add: s.enum_n_top t.enum_n_top)
moreover
{ fix j assume "j < n"
moreover have "s - {a} = s.enum ` {0 .. n'}" "t - {b} = t.enum ` {0 .. n'}"
unfolding s.s_eq t.s_eq en by (auto simp: s.enum_inj t.enum_inj Suc)
ultimately have "s.enum j = t.enum j"
using enum_eq[of "0" j n' 0] eq Suc by auto }
note enum_eq = this
then have "s.enum n' = t.enum n'"
using Suc by auto
moreover
{ fix j assume "j < n'"
with enum_eq[of j] enum_eq[of "Suc j"]
have "u_s j = u_t j"
using s.enum_Suc[of j] t.enum_Suc[of j]
by (auto simp: Suc fun_eq_iff split: if_split_asm) }
then have "⋀j. j < n' ⟹ u_s j = u_t j"
by (auto simp: gr0_conv_Suc)
then have "u_t n' = u_s n'"
by (intro bij_betw_singleton_eq[OF t.upd s.upd, of n']) (auto simp: Suc)
ultimately have "a = b"
by simp
with assms show "s = t"
by auto
qed
end
inductive ksimplex for p n :: nat where
ksimplex: "kuhn_simplex p n base upd s ⟹ ksimplex p n s"
lemma finite_ksimplexes: "finite {s. ksimplex p n s}"
proof (rule finite_subset)
{ fix a s assume "ksimplex p n s" "a ∈ s"
then obtain b u where "kuhn_simplex p n b u s" by (auto elim: ksimplex.cases)
then interpret kuhn_simplex p n b u s .
from s_space ‹a ∈ s› out_eq_p[OF ‹a ∈ s›]
have "a ∈ (λf x. if n ≤ x then p else f x) ` ({..< n} →⇩E {.. p})"
by (auto simp: image_iff subset_eq Pi_iff split: if_split_asm
intro!: bexI[of _ "restrict a {..< n}"]) }
then show "{s. ksimplex p n s} ⊆ Pow ((λf x. if n ≤ x then p else f x) ` ({..< n} →⇩E {.. p}))"
by auto
qed (simp add: finite_PiE)
lemma ksimplex_card:
assumes "ksimplex p n s" shows "card s = Suc n"
using assms proof cases
case (ksimplex u b)
then interpret kuhn_simplex p n u b s .
show ?thesis
by (simp add: card_image s_eq inj_enum)
qed
lemma simplex_top_face:
assumes "0 < p" "∀x∈s'. x n = p"
shows "ksimplex p n s' ⟷ (∃s a. ksimplex p (Suc n) s ∧ a ∈ s ∧ s' = s - {a})"
using assms
proof safe
fix s a assume "ksimplex p (Suc n) s" and a: "a ∈ s" and na: "∀x∈s - {a}. x n = p"
then show "ksimplex p n (s - {a})"
proof cases
case (ksimplex base upd)
then interpret kuhn_simplex p "Suc n" base upd "s" .
have "a n < p"
using one_step[of a n p] na ‹a∈s› s_space by (auto simp: less_le)
then have "a = enum 0"
using ‹a ∈ s› na by (subst enum_0_bot) (auto simp: le_less intro!: less[of a _ n])
then have s_eq: "s - {a} = enum ` Suc ` {.. n}"
using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident Zero_notin_Suc in_enum_image subset_eq)
then have "enum 1 ∈ s - {a}"
by auto
then have "upd 0 = n"
using ‹a n < p› ‹a = enum 0› na[rule_format, of "enum 1"]
by (auto simp: fun_eq_iff enum_Suc split: if_split_asm)
then have "bij_betw upd (Suc ` {..< n}) {..< n}"
using upd
by (subst notIn_Un_bij_betw3[where b=0])
(auto simp: lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0)
then have "bij_betw (upd∘Suc) {..<n} {..<n}"
by (rule bij_betw_trans[rotated]) (auto simp: bij_betw_def)
have "a n = p - 1"
using enum_Suc[of 0] na[rule_format, OF ‹enum 1 ∈ s - {a}›] ‹a = enum 0› by (auto simp: ‹upd 0 = n›)
show ?thesis
proof (rule ksimplex.intros, standard)
show "bij_betw (upd∘Suc) {..< n} {..< n}" by fact
show "base(n := p) ∈ {..<n} → {..<p}" "⋀i. n≤i ⟹ (base(n := p)) i = p"
using base base_out by (auto simp: Pi_iff)
have "⋀i. Suc ` {..< i} = {..< Suc i} - {0}"
by (auto simp: image_iff Ball_def) arith
then have upd_Suc: "⋀i. i ≤ n ⟹ (upd∘Suc) ` {..< i} = upd ` {..< Suc i} - {n}"
using ‹upd 0 = n› upd_inj
by (auto simp add: image_comp[symmetric] inj_on_image_set_diff[OF inj_upd])
have n_in_upd: "⋀i. n ∈ upd ` {..< Suc i}"
using ‹upd 0 = n› by auto
def f' ≡ "λi j. if j ∈ (upd∘Suc)`{..< i} then Suc ((base(n := p)) j) else (base(n := p)) j"
{ fix x i assume i[arith]: "i ≤ n" then have "enum (Suc i) x = f' i x"
unfolding f'_def enum_def using ‹a n < p› ‹a = enum 0› ‹upd 0 = n› ‹a n = p - 1›
by (simp add: upd_Suc enum_0 n_in_upd) }
then show "s - {a} = f' ` {.. n}"
unfolding s_eq image_comp by (intro image_cong) auto
qed
qed
next
assume "ksimplex p n s'" and *: "∀x∈s'. x n = p"
then show "∃s a. ksimplex p (Suc n) s ∧ a ∈ s ∧ s' = s - {a}"
proof cases
case (ksimplex base upd)
then interpret kuhn_simplex p n base upd s' .
def b ≡ "base (n := p - 1)"
def u ≡ "λi. case i of 0 ⇒ n | Suc i ⇒ upd i"
have "ksimplex p (Suc n) (s' ∪ {b})"
proof (rule ksimplex.intros, standard)
show "b ∈ {..<Suc n} → {..<p}"
using base ‹0 < p› unfolding lessThan_Suc b_def by (auto simp: PiE_iff)
show "⋀i. Suc n ≤ i ⟹ b i = p"
using base_out by (auto simp: b_def)
have "bij_betw u (Suc ` {..< n} ∪ {0}) ({..<n} ∪ {u 0})"
using upd
by (intro notIn_Un_bij_betw) (auto simp: u_def bij_betw_def image_comp comp_def inj_on_def)
then show "bij_betw u {..<Suc n} {..<Suc n}"
by (simp add: u_def lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0)
def f' ≡ "λi j. if j ∈ u`{..< i} then Suc (b j) else b j"
have u_eq: "⋀i. i ≤ n ⟹ u ` {..< Suc i} = upd ` {..< i} ∪ { n }"
by (auto simp: u_def image_iff upd_inj Ball_def split: nat.split) arith
{ fix x have "x ≤ n ⟹ n ∉ upd ` {..<x}"
using upd_space by (simp add: image_iff neq_iff) }
note n_not_upd = this
have *: "f' ` {.. Suc n} = f' ` (Suc ` {.. n} ∪ {0})"
unfolding atMost_Suc_eq_insert_0 by simp
also have "… = (f' ∘ Suc) ` {.. n} ∪ {b}"
by (auto simp: f'_def)
also have "(f' ∘ Suc) ` {.. n} = s'"
using ‹0 < p› base_out[of n]
unfolding s_eq enum_def[abs_def] f'_def[abs_def] upd_space
by (intro image_cong) (simp_all add: u_eq b_def fun_eq_iff n_not_upd)
finally show "s' ∪ {b} = f' ` {.. Suc n}" ..
qed
moreover have "b ∉ s'"
using * ‹0 < p› by (auto simp: b_def)
ultimately show ?thesis by auto
qed
qed
lemma ksimplex_replace_0:
assumes s: "ksimplex p n s" and a: "a ∈ s"
assumes j: "j < n" and p: "∀x∈s - {a}. x j = 0"
shows "card {s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = 1"
using s
proof cases
case (ksimplex b_s u_s)
{ fix t b assume "ksimplex p n t"
then obtain b_t u_t where "kuhn_simplex p n b_t u_t t"
by (auto elim: ksimplex.cases)
interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t
by intro_locales fact+
assume b: "b ∈ t" "t - {b} = s - {a}"
with a j p s.replace_0[of _ a] t.replace_0[of _ b] have "s = t"
by (intro ksimplex_eq_top[of a b]) auto }
then have "{s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = {s}"
using s ‹a ∈ s› by auto
then show ?thesis
by simp
qed
lemma ksimplex_replace_1:
assumes s: "ksimplex p n s" and a: "a ∈ s"
assumes j: "j < n" and p: "∀x∈s - {a}. x j = p"
shows "card {s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = 1"
using s
proof cases
case (ksimplex b_s u_s)
{ fix t b assume "ksimplex p n t"
then obtain b_t u_t where "kuhn_simplex p n b_t u_t t"
by (auto elim: ksimplex.cases)
interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t
by intro_locales fact+
assume b: "b ∈ t" "t - {b} = s - {a}"
with a j p s.replace_1[of _ a] t.replace_1[of _ b] have "s = t"
by (intro ksimplex_eq_bot[of a b]) auto }
then have "{s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = {s}"
using s ‹a ∈ s› by auto
then show ?thesis
by simp
qed
lemma card_2_exists: "card s = 2 ⟷ (∃x∈s. ∃y∈s. x ≠ y ∧ (∀z∈s. z = x ∨ z = y))"
by (auto simp add: card_Suc_eq eval_nat_numeral)
lemma ksimplex_replace_2:
assumes s: "ksimplex p n s" and "a ∈ s" and "n ≠ 0"
and lb: "∀j<n. ∃x∈s - {a}. x j ≠ 0"
and ub: "∀j<n. ∃x∈s - {a}. x j ≠ p"
shows "card {s'. ksimplex p n s' ∧ (∃b∈s'. s' - {b} = s - {a})} = 2"
using s
proof cases
case (ksimplex base upd)
then interpret kuhn_simplex p n base upd s .
from ‹a ∈ s› obtain i where "i ≤ n" "a = enum i"
unfolding s_eq by auto
from ‹i ≤ n› have "i = 0 ∨ i = n ∨ (0 < i ∧ i < n)"
by linarith
then have "∃!s'. s' ≠ s ∧ ksimplex p n s' ∧ (∃b∈s'. s - {a} = s'- {b})"
proof (elim disjE conjE)
assume "i = 0"
def rot ≡ "λi. if i + 1 = n then 0 else i + 1"
let ?upd = "upd ∘ rot"
have rot: "bij_betw rot {..< n} {..< n}"
by (auto simp: bij_betw_def inj_on_def image_iff Ball_def rot_def)
arith+
from rot upd have "bij_betw ?upd {..<n} {..<n}"
by (rule bij_betw_trans)
def f' ≡ "λi j. if j ∈ ?upd`{..< i} then Suc (enum (Suc 0) j) else enum (Suc 0) j"
interpret b: kuhn_simplex p n "enum (Suc 0)" "upd ∘ rot" "f' ` {.. n}"
proof
from ‹a = enum i› ub ‹n ≠ 0› ‹i = 0›
obtain i' where "i' ≤ n" "enum i' ≠ enum 0" "enum i' (upd 0) ≠ p"
unfolding s_eq by (auto intro: upd_space simp: enum_inj)
then have "enum 1 ≤ enum i'" "enum i' (upd 0) < p"
using enum_le_p[of i' "upd 0"] by (auto simp add: enum_inj enum_mono upd_space)
then have "enum 1 (upd 0) < p"
by (auto simp add: le_fun_def intro: le_less_trans)
then show "enum (Suc 0) ∈ {..<n} → {..<p}"
using base ‹n ≠ 0› by (auto simp add: enum_0 enum_Suc PiE_iff extensional_def upd_space)
{ fix i assume "n ≤ i" then show "enum (Suc 0) i = p"
using ‹n ≠ 0› by (auto simp: enum_eq_p) }
show "bij_betw ?upd {..<n} {..<n}" by fact
qed (simp add: f'_def)
have ks_f': "ksimplex p n (f' ` {.. n})"
by rule unfold_locales
have b_enum: "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
with b.inj_enum have inj_f': "inj_on f' {.. n}" by simp
have [simp]: "⋀j. j < n ⟹ rot ` {..< j} = {0 <..< Suc j}"
by (auto simp: rot_def image_iff Ball_def)
arith
{ fix j assume j: "j < n"
from j ‹n ≠ 0› have "f' j = enum (Suc j)"
by (auto simp add: f'_def enum_def upd_inj in_upd_image image_comp[symmetric] fun_eq_iff) }
note f'_eq_enum = this
then have "enum ` Suc ` {..< n} = f' ` {..< n}"
by (force simp: enum_inj)
also have "Suc ` {..< n} = {.. n} - {0}"
by (auto simp: image_iff Ball_def) arith
also have "{..< n} = {.. n} - {n}"
by auto
finally have eq: "s - {a} = f' ` {.. n} - {f' n}"
unfolding s_eq ‹a = enum i› ‹i = 0›
by (simp add: Diff_subset inj_on_image_set_diff[OF inj_enum] inj_on_image_set_diff[OF inj_f'])
have "enum 0 < f' 0"
using ‹n ≠ 0› by (simp add: enum_strict_mono f'_eq_enum)
also have "… < f' n"
using ‹n ≠ 0› b.enum_strict_mono[of 0 n] unfolding b_enum by simp
finally have "a ≠ f' n"
using ‹a = enum i› ‹i = 0› by auto
{ fix t c assume "ksimplex p n t" "c ∈ t" and eq_sma: "s - {a} = t - {c}"
obtain b u where "kuhn_simplex p n b u t"
using ‹ksimplex p n t› by (auto elim: ksimplex.cases)
then interpret t: kuhn_simplex p n b u t .
{ fix x assume "x ∈ s" "x ≠ a"
then have "x (upd 0) = enum (Suc 0) (upd 0)"
by (auto simp: ‹a = enum i› ‹i = 0› s_eq enum_def enum_inj) }
then have eq_upd0: "∀x∈t-{c}. x (upd 0) = enum (Suc 0) (upd 0)"
unfolding eq_sma[symmetric] by auto
then have "c (upd 0) ≠ enum (Suc 0) (upd 0)"
using ‹n ≠ 0› by (intro t.one_step[OF ‹c∈t› ]) (auto simp: upd_space)
then have "c (upd 0) < enum (Suc 0) (upd 0) ∨ c (upd 0) > enum (Suc 0) (upd 0)"
by auto
then have "t = s ∨ t = f' ` {..n}"
proof (elim disjE conjE)
assume *: "c (upd 0) < enum (Suc 0) (upd 0)"
interpret st: kuhn_simplex_pair p n base upd s b u t ..
{ fix x assume "x ∈ t" with * ‹c∈t› eq_upd0[rule_format, of x] have "c ≤ x"
by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
note top = this
have "s = t"
using ‹a = enum i› ‹i = 0› ‹c ∈ t›
by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq_sma])
(auto simp: s_eq enum_mono t.s_eq t.enum_mono top)
then show ?thesis by simp
next
assume *: "c (upd 0) > enum (Suc 0) (upd 0)"
interpret st: kuhn_simplex_pair p n "enum (Suc 0)" "upd ∘ rot" "f' ` {.. n}" b u t ..
have eq: "f' ` {..n} - {f' n} = t - {c}"
using eq_sma eq by simp
{ fix x assume "x ∈ t" with * ‹c∈t› eq_upd0[rule_format, of x] have "x ≤ c"
by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
note top = this
have "f' ` {..n} = t"
using ‹a = enum i› ‹i = 0› ‹c ∈ t›
by (intro st.ksimplex_eq_top[OF _ _ _ _ eq])
(auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono b_enum[symmetric] top)
then show ?thesis by simp
qed }
with ks_f' eq ‹a ≠ f' n› ‹n ≠ 0› show ?thesis
apply (intro ex1I[of _ "f' ` {.. n}"])
apply auto []
apply metis
done
next
assume "i = n"
from ‹n ≠ 0› obtain n' where n': "n = Suc n'"
by (cases n) auto
def rot ≡ "λi. case i of 0 ⇒ n' | Suc i ⇒ i"
let ?upd = "upd ∘ rot"
have rot: "bij_betw rot {..< n} {..< n}"
by (auto simp: bij_betw_def inj_on_def image_iff Bex_def rot_def n' split: nat.splits)
arith
from rot upd have "bij_betw ?upd {..<n} {..<n}"
by (rule bij_betw_trans)
def b ≡ "base (upd n' := base (upd n') - 1)"
def f' ≡ "λi j. if j ∈ ?upd`{..< i} then Suc (b j) else b j"
interpret b: kuhn_simplex p n b "upd ∘ rot" "f' ` {.. n}"
proof
{ fix i assume "n ≤ i" then show "b i = p"
using base_out[of i] upd_space[of n'] by (auto simp: b_def n') }
show "b ∈ {..<n} → {..<p}"
using base ‹n ≠ 0› upd_space[of n']
by (auto simp: b_def PiE_def Pi_iff Ball_def upd_space extensional_def n')
show "bij_betw ?upd {..<n} {..<n}" by fact
qed (simp add: f'_def)
have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
have ks_f': "ksimplex p n (b.enum ` {.. n})"
unfolding f' by rule unfold_locales
have "0 < n"
using ‹n ≠ 0› by auto
{ from ‹a = enum i› ‹n ≠ 0› ‹i = n› lb upd_space[of n']
obtain i' where "i' ≤ n" "enum i' ≠ enum n" "0 < enum i' (upd n')"
unfolding s_eq by (auto simp: enum_inj n')
moreover have "enum i' (upd n') = base (upd n')"
unfolding enum_def using ‹i' ≤ n› ‹enum i' ≠ enum n› by (auto simp: n' upd_inj enum_inj)
ultimately have "0 < base (upd n')"
by auto }
then have benum1: "b.enum (Suc 0) = base"
unfolding b.enum_Suc[OF ‹0<n›] b.enum_0 by (auto simp: b_def rot_def)
have [simp]: "⋀j. Suc j < n ⟹ rot ` {..< Suc j} = {n'} ∪ {..< j}"
by (auto simp: rot_def image_iff Ball_def split: nat.splits)
have rot_simps: "⋀j. rot (Suc j) = j" "rot 0 = n'"
by (simp_all add: rot_def)
{ fix j assume j: "Suc j ≤ n" then have "b.enum (Suc j) = enum j"
by (induct j) (auto simp add: benum1 enum_0 b.enum_Suc enum_Suc rot_simps) }
note b_enum_eq_enum = this
then have "enum ` {..< n} = b.enum ` Suc ` {..< n}"
by (auto simp add: image_comp intro!: image_cong)
also have "Suc ` {..< n} = {.. n} - {0}"
by (auto simp: image_iff Ball_def) arith
also have "{..< n} = {.. n} - {n}"
by auto
finally have eq: "s - {a} = b.enum ` {.. n} - {b.enum 0}"
unfolding s_eq ‹a = enum i› ‹i = n›
using inj_on_image_set_diff[OF inj_enum Diff_subset, of "{n}"]
inj_on_image_set_diff[OF b.inj_enum Diff_subset, of "{0}"]
by (simp add: comp_def )
have "b.enum 0 ≤ b.enum n"
by (simp add: b.enum_mono)
also have "b.enum n < enum n"
using ‹n ≠ 0› by (simp add: enum_strict_mono b_enum_eq_enum n')
finally have "a ≠ b.enum 0"
using ‹a = enum i› ‹i = n› by auto
{ fix t c assume "ksimplex p n t" "c ∈ t" and eq_sma: "s - {a} = t - {c}"
obtain b' u where "kuhn_simplex p n b' u t"
using ‹ksimplex p n t› by (auto elim: ksimplex.cases)
then interpret t: kuhn_simplex p n b' u t .
{ fix x assume "x ∈ s" "x ≠ a"
then have "x (upd n') = enum n' (upd n')"
by (auto simp: ‹a = enum i› n' ‹i = n› s_eq enum_def enum_inj in_upd_image) }
then have eq_upd0: "∀x∈t-{c}. x (upd n') = enum n' (upd n')"
unfolding eq_sma[symmetric] by auto
then have "c (upd n') ≠ enum n' (upd n')"
using ‹n ≠ 0› by (intro t.one_step[OF ‹c∈t› ]) (auto simp: n' upd_space[unfolded n'])
then have "c (upd n') < enum n' (upd n') ∨ c (upd n') > enum n' (upd n')"
by auto
then have "t = s ∨ t = b.enum ` {..n}"
proof (elim disjE conjE)
assume *: "c (upd n') > enum n' (upd n')"
interpret st: kuhn_simplex_pair p n base upd s b' u t ..
{ fix x assume "x ∈ t" with * ‹c∈t› eq_upd0[rule_format, of x] have "x ≤ c"
by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) }
note top = this
have "s = t"
using ‹a = enum i› ‹i = n› ‹c ∈ t›
by (intro st.ksimplex_eq_top[OF _ _ _ _ eq_sma])
(auto simp: s_eq enum_mono t.s_eq t.enum_mono top)
then show ?thesis by simp
next
assume *: "c (upd n') < enum n' (upd n')"
interpret st: kuhn_simplex_pair p n b "upd ∘ rot" "f' ` {.. n}" b' u t ..
have eq: "f' ` {..n} - {b.enum 0} = t - {c}"
using eq_sma eq f' by simp
{ fix x assume "x ∈ t" with * ‹c∈t› eq_upd0[rule_format, of x] have "c ≤ x"
by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) }
note bot = this
have "f' ` {..n} = t"
using ‹a = enum i› ‹i = n› ‹c ∈ t›
by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq])
(auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono bot)
with f' show ?thesis by simp
qed }
with ks_f' eq ‹a ≠ b.enum 0› ‹n ≠ 0› show ?thesis
apply (intro ex1I[of _ "b.enum ` {.. n}"])
apply auto []
apply metis
done
next
assume i: "0 < i" "i < n"
def i' ≡ "i - 1"
with i have "Suc i' < n"
by simp
with i have Suc_i': "Suc i' = i"
by (simp add: i'_def)
let ?upd = "Fun.swap i' i upd"
from i upd have "bij_betw ?upd {..< n} {..< n}"
by (subst bij_betw_swap_iff) (auto simp: i'_def)
def f' ≡ "λi j. if j ∈ ?upd`{..< i} then Suc (base j) else base j"
interpret b: kuhn_simplex p n base ?upd "f' ` {.. n}"
proof
show "base ∈ {..<n} → {..<p}" by fact
{ fix i assume "n ≤ i" then show "base i = p" by fact }
show "bij_betw ?upd {..<n} {..<n}" by fact
qed (simp add: f'_def)
have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
have ks_f': "ksimplex p n (b.enum ` {.. n})"
unfolding f' by rule unfold_locales
have "{i} ⊆ {..n}"
using i by auto
{ fix j assume "j ≤ n"
moreover have "j < i ∨ i = j ∨ i < j" by arith
moreover note i
ultimately have "enum j = b.enum j ⟷ j ≠ i"
unfolding enum_def[abs_def] b.enum_def[abs_def]
by (auto simp add: fun_eq_iff swap_image i'_def
in_upd_image inj_on_image_set_diff[OF inj_upd]) }
note enum_eq_benum = this
then have "enum ` ({.. n} - {i}) = b.enum ` ({.. n} - {i})"
by (intro image_cong) auto
then have eq: "s - {a} = b.enum ` {.. n} - {b.enum i}"
unfolding s_eq ‹a = enum i›
using inj_on_image_set_diff[OF inj_enum Diff_subset ‹{i} ⊆ {..n}›]
inj_on_image_set_diff[OF b.inj_enum Diff_subset ‹{i} ⊆ {..n}›]
by (simp add: comp_def)
have "a ≠ b.enum i"
using ‹a = enum i› enum_eq_benum i by auto
{ fix t c assume "ksimplex p n t" "c ∈ t" and eq_sma: "s - {a} = t - {c}"
obtain b' u where "kuhn_simplex p n b' u t"
using ‹ksimplex p n t› by (auto elim: ksimplex.cases)
then interpret t: kuhn_simplex p n b' u t .
have "enum i' ∈ s - {a}" "enum (i + 1) ∈ s - {a}"
using ‹a = enum i› i enum_in by (auto simp: enum_inj i'_def)
then obtain l k where
l: "t.enum l = enum i'" "l ≤ n" "t.enum l ≠ c" and
k: "t.enum k = enum (i + 1)" "k ≤ n" "t.enum k ≠ c"
unfolding eq_sma by (auto simp: t.s_eq)
with i have "t.enum l < t.enum k"
by (simp add: enum_strict_mono i'_def)
with ‹l ≤ n› ‹k ≤ n› have "l < k"
by (simp add: t.enum_strict_mono)
{ assume "Suc l = k"
have "enum (Suc (Suc i')) = t.enum (Suc l)"
using i by (simp add: k ‹Suc l = k› i'_def)
then have False
using ‹l < k› ‹k ≤ n› ‹Suc i' < n›
by (auto simp: t.enum_Suc enum_Suc l upd_inj fun_eq_iff split: if_split_asm)
(metis Suc_lessD n_not_Suc_n upd_inj) }
with ‹l < k› have "Suc l < k"
by arith
have c_eq: "c = t.enum (Suc l)"
proof (rule ccontr)
assume "c ≠ t.enum (Suc l)"
then have "t.enum (Suc l) ∈ s - {a}"
using ‹l < k› ‹k ≤ n› by (simp add: t.s_eq eq_sma)
then obtain j where "t.enum (Suc l) = enum j" "j ≤ n" "enum j ≠ enum i"
unfolding s_eq ‹a = enum i› by auto
with i have "t.enum (Suc l) ≤ t.enum l ∨ t.enum k ≤ t.enum (Suc l)"
by (auto simp add: i'_def enum_mono enum_inj l k)
with ‹Suc l < k› ‹k ≤ n› show False
by (simp add: t.enum_mono)
qed
{ have "t.enum (Suc (Suc l)) ∈ s - {a}"
unfolding eq_sma c_eq t.s_eq using ‹Suc l < k› ‹k ≤ n› by (auto simp: t.enum_inj)
then obtain j where eq: "t.enum (Suc (Suc l)) = enum j" and "j ≤ n" "j ≠ i"
by (auto simp: s_eq ‹a = enum i›)
moreover have "enum i' < t.enum (Suc (Suc l))"
unfolding l(1)[symmetric] using ‹Suc l < k› ‹k ≤ n› by (auto simp: t.enum_strict_mono)
ultimately have "i' < j"
using i by (simp add: enum_strict_mono i'_def)
with ‹j ≠ i› ‹j ≤ n› have "t.enum k ≤ t.enum (Suc (Suc l))"
unfolding i'_def by (simp add: enum_mono k eq)
then have "k ≤ Suc (Suc l)"
using ‹k ≤ n› ‹Suc l < k› by (simp add: t.enum_mono) }
with ‹Suc l < k› have "Suc (Suc l) = k" by simp
then have "enum (Suc (Suc i')) = t.enum (Suc (Suc l))"
using i by (simp add: k i'_def)
also have "… = (enum i') (u l := Suc (enum i' (u l)), u (Suc l) := Suc (enum i' (u (Suc l))))"
using ‹Suc l < k› ‹k ≤ n› by (simp add: t.enum_Suc l t.upd_inj)
finally have "(u l = upd i' ∧ u (Suc l) = upd (Suc i')) ∨
(u l = upd (Suc i') ∧ u (Suc l) = upd i')"
using ‹Suc i' < n› by (auto simp: enum_Suc fun_eq_iff split: if_split_asm)
then have "t = s ∨ t = b.enum ` {..n}"
proof (elim disjE conjE)
assume u: "u l = upd i'"
have "c = t.enum (Suc l)" unfolding c_eq ..
also have "t.enum (Suc l) = enum (Suc i')"
using u ‹l < k› ‹k ≤ n› ‹Suc i' < n› by (simp add: enum_Suc t.enum_Suc l)
also have "… = a"
using ‹a = enum i› i by (simp add: i'_def)
finally show ?thesis
using eq_sma ‹a ∈ s› ‹c ∈ t› by auto
next
assume u: "u l = upd (Suc i')"
def B ≡ "b.enum ` {..n}"
have "b.enum i' = enum i'"
using enum_eq_benum[of i'] i by (auto simp add: i'_def gr0_conv_Suc)
have "c = t.enum (Suc l)" unfolding c_eq ..
also have "t.enum (Suc l) = b.enum (Suc i')"
using u ‹l < k› ‹k ≤ n› ‹Suc i' < n›
by (simp_all add: enum_Suc t.enum_Suc l b.enum_Suc ‹b.enum i' = enum i'› swap_apply1)
(simp add: Suc_i')
also have "… = b.enum i"
using i by (simp add: i'_def)
finally have "c = b.enum i" .
then have "t - {c} = B - {c}" "c ∈ B"
unfolding eq_sma[symmetric] eq B_def using i by auto
with ‹c ∈ t› have "t = B"
by auto
then show ?thesis
by (simp add: B_def)
qed }
with ks_f' eq ‹a ≠ b.enum i› ‹n ≠ 0› ‹i ≤ n› show ?thesis
apply (intro ex1I[of _ "b.enum ` {.. n}"])
apply auto []
apply metis
done
qed
then show ?thesis
using s ‹a ∈ s› by (simp add: card_2_exists Ex1_def) metis
qed
text ‹Hence another step towards concreteness.›
lemma kuhn_simplex_lemma:
assumes "∀s. ksimplex p (Suc n) s ⟶ rl ` s ⊆ {.. Suc n}"
and "odd (card {f. ∃s a. ksimplex p (Suc n) s ∧ a ∈ s ∧ (f = s - {a}) ∧
rl ` f = {..n} ∧ ((∃j≤n. ∀x∈f. x j = 0) ∨ (∃j≤n. ∀x∈f. x j = p))})"
shows "odd (card {s. ksimplex p (Suc n) s ∧ rl ` s = {..Suc n}})"
proof (rule kuhn_complete_lemma[OF finite_ksimplexes refl, unfolded mem_Collect_eq,
where bnd="λf. (∃j∈{..n}. ∀x∈f. x j = 0) ∨ (∃j∈{..n}. ∀x∈f. x j = p)"],
safe del: notI)
have *: "⋀x y. x = y ⟹ odd (card x) ⟹ odd (card y)"
by auto
show "odd (card {f. (∃s∈{s. ksimplex p (Suc n) s}. ∃a∈s. f = s - {a}) ∧
rl ` f = {..n} ∧ ((∃j∈{..n}. ∀x∈f. x j = 0) ∨ (∃j∈{..n}. ∀x∈f. x j = p))})"
apply (rule *[OF _ assms(2)])
apply (auto simp: atLeast0AtMost)
done
next
fix s assume s: "ksimplex p (Suc n) s"
then show "card s = n + 2"
by (simp add: ksimplex_card)
fix a assume a: "a ∈ s" then show "rl a ≤ Suc n"
using assms(1) s by (auto simp: subset_eq)
let ?S = "{t. ksimplex p (Suc n) t ∧ (∃b∈t. s - {a} = t - {b})}"
{ fix j assume j: "j ≤ n" "∀x∈s - {a}. x j = 0"
with s a show "card ?S = 1"
using ksimplex_replace_0[of p "n + 1" s a j]
by (subst eq_commute) simp }
{ fix j assume j: "j ≤ n" "∀x∈s - {a}. x j = p"
with s a show "card ?S = 1"
using ksimplex_replace_1[of p "n + 1" s a j]
by (subst eq_commute) simp }
{ assume "card ?S ≠ 2" "¬ (∃j∈{..n}. ∀x∈s - {a}. x j = p)"
with s a show "∃j∈{..n}. ∀x∈s - {a}. x j = 0"
using ksimplex_replace_2[of p "n + 1" s a]
by (subst (asm) eq_commute) auto }
qed
subsection ‹Reduced labelling›
definition reduced :: "nat ⇒ (nat ⇒ nat) ⇒ nat" where "reduced n x = (LEAST k. k = n ∨ x k ≠ 0)"
lemma reduced_labelling:
shows "reduced n x ≤ n"
and "∀i<reduced n x. x i = 0"
and "reduced n x = n ∨ x (reduced n x) ≠ 0"
proof -
show "reduced n x ≤ n"
unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) auto
show "∀i<reduced n x. x i = 0"
unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+
show "reduced n x = n ∨ x (reduced n x) ≠ 0"
unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+
qed
lemma reduced_labelling_unique:
"r ≤ n ⟹ ∀i<r. x i = 0 ⟹ r = n ∨ x r ≠ 0 ⟹ reduced n x = r"
unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) (metis le_less not_le)+
lemma reduced_labelling_zero: "j < n ⟹ x j = 0 ⟹ reduced n x ≠ j"
using reduced_labelling[of n x] by auto
lemma reduce_labelling_zero[simp]: "reduced 0 x = 0"
by (rule reduced_labelling_unique) auto
lemma reduced_labelling_nonzero: "j < n ⟹ x j ≠ 0 ⟹ reduced n x ≤ j"
using reduced_labelling[of n x] by (elim allE[where x=j]) auto
lemma reduced_labelling_Suc: "reduced (Suc n) x ≠ Suc n ⟹ reduced (Suc n) x = reduced n x"
using reduced_labelling[of "Suc n" x]
by (intro reduced_labelling_unique[symmetric]) auto
lemma complete_face_top:
assumes "∀x∈f. ∀j≤n. x j = 0 ⟶ lab x j = 0"
and "∀x∈f. ∀j≤n. x j = p ⟶ lab x j = 1"
and eq: "(reduced (Suc n) ∘ lab) ` f = {..n}"
shows "((∃j≤n. ∀x∈f. x j = 0) ∨ (∃j≤n. ∀x∈f. x j = p)) ⟷ (∀x∈f. x n = p)"
proof (safe del: disjCI)
fix x j assume j: "j ≤ n" "∀x∈f. x j = 0"
{ fix x assume "x ∈ f" with assms j have "reduced (Suc n) (lab x) ≠ j"
by (intro reduced_labelling_zero) auto }
moreover have "j ∈ (reduced (Suc n) ∘ lab) ` f"
using j eq by auto
ultimately show "x n = p"
by force
next
fix x j assume j: "j ≤ n" "∀x∈f. x j = p" and x: "x ∈ f"
have "j = n"
proof (rule ccontr)
assume "¬ ?thesis"
{ fix x assume "x ∈ f"
with assms j have "reduced (Suc n) (lab x) ≤ j"
by (intro reduced_labelling_nonzero) auto
then have "reduced (Suc n) (lab x) ≠ n"
using ‹j ≠ n› ‹j ≤ n› by simp }
moreover
have "n ∈ (reduced (Suc n) ∘ lab) ` f"
using eq by auto
ultimately show False
by force
qed
moreover have "j ∈ (reduced (Suc n) ∘ lab) ` f"
using j eq by auto
ultimately show "x n = p"
using j x by auto
qed auto
text ‹Hence we get just about the nice induction.›
lemma kuhn_induction:
assumes "0 < p"
and lab_0: "∀x. ∀j≤n. (∀j. x j ≤ p) ∧ x j = 0 ⟶ lab x j = 0"
and lab_1: "∀x. ∀j≤n. (∀j. x j ≤ p) ∧ x j = p ⟶ lab x j = 1"
and odd: "odd (card {s. ksimplex p n s ∧ (reduced n∘lab) ` s = {..n}})"
shows "odd (card {s. ksimplex p (Suc n) s ∧ (reduced (Suc n)∘lab) ` s = {..Suc n}})"
proof -
let ?rl = "reduced (Suc n) ∘ lab" and ?ext = "λf v. ∃j≤n. ∀x∈f. x j = v"
let ?ext = "λs. (∃j≤n. ∀x∈s. x j = 0) ∨ (∃j≤n. ∀x∈s. x j = p)"
have "∀s. ksimplex p (Suc n) s ⟶ ?rl ` s ⊆ {..Suc n}"
by (simp add: reduced_labelling subset_eq)
moreover
have "{s. ksimplex p n s ∧ (reduced n ∘ lab) ` s = {..n}} =
{f. ∃s a. ksimplex p (Suc n) s ∧ a ∈ s ∧ f = s - {a} ∧ ?rl ` f = {..n} ∧ ?ext f}"
proof (intro set_eqI, safe del: disjCI equalityI disjE)
fix s assume s: "ksimplex p n s" and rl: "(reduced n ∘ lab) ` s = {..n}"
from s obtain u b where "kuhn_simplex p n u b s" by (auto elim: ksimplex.cases)
then interpret kuhn_simplex p n u b s .
have all_eq_p: "∀x∈s. x n = p"
by (auto simp: out_eq_p)
moreover
{ fix x assume "x ∈ s"
with lab_1[rule_format, of n x] all_eq_p s_le_p[of x]
have "?rl x ≤ n"
by (auto intro!: reduced_labelling_nonzero)
then have "?rl x = reduced n (lab x)"
by (auto intro!: reduced_labelling_Suc) }
then have "?rl ` s = {..n}"
using rl by (simp cong: image_cong)
moreover
obtain t a where "ksimplex p (Suc n) t" "a ∈ t" "s = t - {a}"
using s unfolding simplex_top_face[OF ‹0 < p› all_eq_p] by auto
ultimately
show "∃t a. ksimplex p (Suc n) t ∧ a ∈ t ∧ s = t - {a} ∧ ?rl ` s = {..n} ∧ ?ext s"
by auto
next
fix x s a assume s: "ksimplex p (Suc n) s" and rl: "?rl ` (s - {a}) = {.. n}"
and a: "a ∈ s" and "?ext (s - {a})"
from s obtain u b where "kuhn_simplex p (Suc n) u b s" by (auto elim: ksimplex.cases)
then interpret kuhn_simplex p "Suc n" u b s .
have all_eq_p: "∀x∈s. x (Suc n) = p"
by (auto simp: out_eq_p)
{ fix x assume "x ∈ s - {a}"
then have "?rl x ∈ ?rl ` (s - {a})"
by auto
then have "?rl x ≤ n"
unfolding rl by auto
then have "?rl x = reduced n (lab x)"
by (auto intro!: reduced_labelling_Suc) }
then show rl': "(reduced n∘lab) ` (s - {a}) = {..n}"
unfolding rl[symmetric] by (intro image_cong) auto
from ‹?ext (s - {a})›
have all_eq_p: "∀x∈s - {a}. x n = p"
proof (elim disjE exE conjE)
fix j assume "j ≤ n" "∀x∈s - {a}. x j = 0"
with lab_0[rule_format, of j] all_eq_p s_le_p
have "⋀x. x ∈ s - {a} ⟹ reduced (Suc n) (lab x) ≠ j"
by (intro reduced_labelling_zero) auto
moreover have "j ∈ ?rl ` (s - {a})"
using ‹j ≤ n› unfolding rl by auto
ultimately show ?thesis
by force
next
fix j assume "j ≤ n" and eq_p: "∀x∈s - {a}. x j = p"
show ?thesis
proof cases
assume "j = n" with eq_p show ?thesis by simp
next
assume "j ≠ n"
{ fix x assume x: "x ∈ s - {a}"
have "reduced n (lab x) ≤ j"
proof (rule reduced_labelling_nonzero)
show "lab x j ≠ 0"
using lab_1[rule_format, of j x] x s_le_p[of x] eq_p ‹j ≤ n› by auto
show "j < n"
using ‹j ≤ n› ‹j ≠ n› by simp
qed
then have "reduced n (lab x) ≠ n"
using ‹j ≤ n› ‹j ≠ n› by simp }
moreover have "n ∈ (reduced n∘lab) ` (s - {a})"
unfolding rl' by auto
ultimately show ?thesis
by force
qed
qed
show "ksimplex p n (s - {a})"
unfolding simplex_top_face[OF ‹0 < p› all_eq_p] using s a by auto
qed
ultimately show ?thesis
using assms by (intro kuhn_simplex_lemma) auto
qed
text ‹And so we get the final combinatorial result.›
lemma ksimplex_0: "ksimplex p 0 s ⟷ s = {(λx. p)}"
proof
assume "ksimplex p 0 s" then show "s = {(λx. p)}"
by (blast dest: kuhn_simplex.ksimplex_0 elim: ksimplex.cases)
next
assume s: "s = {(λx. p)}"
show "ksimplex p 0 s"
proof (intro ksimplex, unfold_locales)
show "(λ_. p) ∈ {..<0::nat} → {..<p}" by auto
show "bij_betw id {..<0} {..<0}"
by simp
qed (auto simp: s)
qed
lemma kuhn_combinatorial:
assumes "0 < p"
and "∀x j. (∀j. x j ≤ p) ∧ j < n ∧ x j = 0 ⟶ lab x j = 0"
and "∀x j. (∀j. x j ≤ p) ∧ j < n ∧ x j = p ⟶ lab x j = 1"
shows "odd (card {s. ksimplex p n s ∧ (reduced n∘lab) ` s = {..n}})"
(is "odd (card (?M n))")
using assms
proof (induct n)
case 0 then show ?case
by (simp add: ksimplex_0 cong: conj_cong)
next
case (Suc n)
then have "odd (card (?M n))"
by force
with Suc show ?case
using kuhn_induction[of p n] by (auto simp: comp_def)
qed
lemma kuhn_lemma:
fixes n p :: nat
assumes "0 < p"
and "∀x. (∀i<n. x i ≤ p) ⟶ (∀i<n. label x i = (0::nat) ∨ label x i = 1)"
and "∀x. (∀i<n. x i ≤ p) ⟶ (∀i<n. x i = 0 ⟶ label x i = 0)"
and "∀x. (∀i<n. x i ≤ p) ⟶ (∀i<n. x i = p ⟶ label x i = 1)"
obtains q where "∀i<n. q i < p"
and "∀i<n. ∃r s. (∀j<n. q j ≤ r j ∧ r j ≤ q j + 1) ∧ (∀j<n. q j ≤ s j ∧ s j ≤ q j + 1) ∧ label r i ≠ label s i"
proof -
let ?rl = "reduced n ∘ label"
let ?A = "{s. ksimplex p n s ∧ ?rl ` s = {..n}}"
have "odd (card ?A)"
using assms by (intro kuhn_combinatorial[of p n label]) auto
then have "?A ≠ {}"
by fastforce
then obtain s b u where "kuhn_simplex p n b u s" and rl: "?rl ` s = {..n}"
by (auto elim: ksimplex.cases)
interpret kuhn_simplex p n b u s by fact
show ?thesis
proof (intro that[of b] allI impI)
fix i
assume "i < n"
then show "b i < p"
using base by auto
next
fix i
assume "i < n"
then have "i ∈ {.. n}" "Suc i ∈ {.. n}"
by auto
then obtain u v where u: "u ∈ s" "Suc i = ?rl u" and v: "v ∈ s" "i = ?rl v"
unfolding rl[symmetric] by blast
have "label u i ≠ label v i"
using reduced_labelling [of n "label u"] reduced_labelling [of n "label v"]
u(2)[symmetric] v(2)[symmetric] ‹i < n›
by auto
moreover
have "b j ≤ u j" "u j ≤ b j + 1" "b j ≤ v j" "v j ≤ b j + 1" if "j < n" for j
using that base_le[OF ‹u∈s›] le_Suc_base[OF ‹u∈s›] base_le[OF ‹v∈s›] le_Suc_base[OF ‹v∈s›]
by auto
ultimately show "∃r s. (∀j<n. b j ≤ r j ∧ r j ≤ b j + 1) ∧
(∀j<n. b j ≤ s j ∧ s j ≤ b j + 1) ∧ label r i ≠ label s i"
by blast
qed
qed
subsection ‹The main result for the unit cube›
lemma kuhn_labelling_lemma':
assumes "(∀x::nat⇒real. P x ⟶ P (f x))"
and "∀x. P x ⟶ (∀i::nat. Q i ⟶ 0 ≤ x i ∧ x i ≤ 1)"
shows "∃l. (∀x i. l x i ≤ (1::nat)) ∧
(∀x i. P x ∧ Q i ∧ x i = 0 ⟶ l x i = 0) ∧
(∀x i. P x ∧ Q i ∧ x i = 1 ⟶ l x i = 1) ∧
(∀x i. P x ∧ Q i ∧ l x i = 0 ⟶ x i ≤ f x i) ∧
(∀x i. P x ∧ Q i ∧ l x i = 1 ⟶ f x i ≤ x i)"
proof -
have and_forall_thm: "⋀P Q. (∀x. P x) ∧ (∀x. Q x) ⟷ (∀x. P x ∧ Q x)"
by auto
have *: "∀x y::real. 0 ≤ x ∧ x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1 ⟶ x ≠ 1 ∧ x ≤ y ∨ x ≠ 0 ∧ y ≤ x"
by auto
show ?thesis
unfolding and_forall_thm
apply (subst choice_iff[symmetric])+
apply rule
apply rule
proof -
fix x x'
let ?R = "λy::nat.
(P x ∧ Q x' ∧ x x' = 0 ⟶ y = 0) ∧
(P x ∧ Q x' ∧ x x' = 1 ⟶ y = 1) ∧
(P x ∧ Q x' ∧ y = 0 ⟶ x x' ≤ (f x) x') ∧
(P x ∧ Q x' ∧ y = 1 ⟶ (f x) x' ≤ x x')"
have "0 ≤ f x x' ∧ f x x' ≤ 1" if "P x" "Q x'"
using assms(2)[rule_format,of "f x" x'] that
apply (drule_tac assms(1)[rule_format])
apply auto
done
then have "?R 0 ∨ ?R 1"
by auto
then show "∃y≤1. ?R y"
by auto
qed
qed
definition unit_cube :: "'a::euclidean_space set"
where "unit_cube = {x. ∀i∈Basis. 0 ≤ x ∙ i ∧ x ∙ i ≤ 1}"
lemma mem_unit_cube: "x ∈ unit_cube ⟷ (∀i∈Basis. 0 ≤ x ∙ i ∧ x ∙ i ≤ 1)"
unfolding unit_cube_def by simp
lemma bounded_unit_cube: "bounded unit_cube"
unfolding bounded_def
proof (intro exI ballI)
fix y :: 'a assume y: "y ∈ unit_cube"
have "dist 0 y = norm y" by (rule dist_0_norm)
also have "… = norm (∑i∈Basis. (y ∙ i) *⇩R i)" unfolding euclidean_representation ..
also have "… ≤ (∑i∈Basis. norm ((y ∙ i) *⇩R i))" by (rule norm_setsum)
also have "… ≤ (∑i::'a∈Basis. 1)"
by (rule setsum_mono, simp add: y [unfolded mem_unit_cube])
finally show "dist 0 y ≤ (∑i::'a∈Basis. 1)" .
qed
lemma closed_unit_cube: "closed unit_cube"
unfolding unit_cube_def Collect_ball_eq Collect_conj_eq
by (rule closed_INT, auto intro!: closed_Collect_le)
lemma compact_unit_cube: "compact unit_cube" (is "compact ?C")
unfolding compact_eq_seq_compact_metric
using bounded_unit_cube closed_unit_cube
by (rule bounded_closed_imp_seq_compact)
lemma brouwer_cube:
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes "continuous_on unit_cube f"
and "f ` unit_cube ⊆ unit_cube"
shows "∃x∈unit_cube. f x = x"
proof (rule ccontr)
def n ≡ "DIM('a)"
have n: "1 ≤ n" "0 < n" "n ≠ 0"
unfolding n_def by (auto simp add: Suc_le_eq DIM_positive)
assume "¬ ?thesis"
then have *: "¬ (∃x∈unit_cube. f x - x = 0)"
by auto
obtain d where
d: "d > 0" "⋀x. x ∈ unit_cube ⟹ d ≤ norm (f x - x)"
apply (rule brouwer_compactness_lemma[OF compact_unit_cube _ *])
apply (rule continuous_intros assms)+
apply blast
done
have *: "∀x. x ∈ unit_cube ⟶ f x ∈ unit_cube"
"∀x. x ∈ (unit_cube::'a set) ⟶ (∀i∈Basis. True ⟶ 0 ≤ x ∙ i ∧ x ∙ i ≤ 1)"
using assms(2)[unfolded image_subset_iff Ball_def]
unfolding mem_unit_cube
by auto
obtain label :: "'a ⇒ 'a ⇒ nat" where
"∀x. ∀i∈Basis. label x i ≤ 1"
"∀x. ∀i∈Basis. x ∈ unit_cube ∧ True ∧ x ∙ i = 0 ⟶ label x i = 0"
"∀x. ∀i∈Basis. x ∈ unit_cube ∧ True ∧ x ∙ i = 1 ⟶ label x i = 1"
"∀x. ∀i∈Basis. x ∈ unit_cube ∧ True ∧ label x i = 0 ⟶ x ∙ i ≤ f x ∙ i"
"∀x. ∀i∈Basis. x ∈ unit_cube ∧ True ∧ label x i = 1 ⟶ f x ∙ i ≤ x ∙ i"
using kuhn_labelling_lemma[OF *] by blast
note label = this [rule_format]
have lem1: "∀x∈unit_cube. ∀y∈unit_cube. ∀i∈Basis. label x i ≠ label y i ⟶
¦f x ∙ i - x ∙ i¦ ≤ norm (f y - f x) + norm (y - x)"
proof safe
fix x y :: 'a
assume x: "x ∈ unit_cube"
assume y: "y ∈ unit_cube"
fix i
assume i: "label x i ≠ label y i" "i ∈ Basis"
have *: "⋀x y fx fy :: real. x ≤ fx ∧ fy ≤ y ∨ fx ≤ x ∧ y ≤ fy ⟹
¦fx - x¦ ≤ ¦fy - fx¦ + ¦y - x¦" by auto
have "¦(f x - x) ∙ i¦ ≤ ¦(f y - f x)∙i¦ + ¦(y - x)∙i¦"
unfolding inner_simps
apply (rule *)
apply (cases "label x i = 0")
apply (rule disjI1)
apply rule
prefer 3
apply (rule disjI2)
apply rule
proof -
assume lx: "label x i = 0"
then have ly: "label y i = 1"
using i label(1)[of i y]
by auto
show "x ∙ i ≤ f x ∙ i"
apply (rule label(4)[rule_format])
using x y lx i(2)
apply auto
done
show "f y ∙ i ≤ y ∙ i"
apply (rule label(5)[rule_format])
using x y ly i(2)
apply auto
done
next
assume "label x i ≠ 0"
then have l: "label x i = 1" "label y i = 0"
using i label(1)[of i x] label(1)[of i y]
by auto
show "f x ∙ i ≤ x ∙ i"
apply (rule label(5)[rule_format])
using x y l i(2)
apply auto
done
show "y ∙ i ≤ f y ∙ i"
apply (rule label(4)[rule_format])
using x y l i(2)
apply auto
done
qed
also have "… ≤ norm (f y - f x) + norm (y - x)"
apply (rule add_mono)
apply (rule Basis_le_norm[OF i(2)])+
done
finally show "¦f x ∙ i - x ∙ i¦ ≤ norm (f y - f x) + norm (y - x)"
unfolding inner_simps .
qed
have "∃e>0. ∀x∈unit_cube. ∀y∈unit_cube. ∀z∈unit_cube. ∀i∈Basis.
norm (x - z) < e ∧ norm (y - z) < e ∧ label x i ≠ label y i ⟶
¦(f(z) - z)∙i¦ < d / (real n)"
proof -
have d': "d / real n / 8 > 0"
using d(1) by (simp add: n_def DIM_positive)
have *: "uniformly_continuous_on unit_cube f"
by (rule compact_uniformly_continuous[OF assms(1) compact_unit_cube])
obtain e where e:
"e > 0"
"⋀x x'. x ∈ unit_cube ⟹
x' ∈ unit_cube ⟹
norm (x' - x) < e ⟹
norm (f x' - f x) < d / real n / 8"
using *[unfolded uniformly_continuous_on_def,rule_format,OF d']
unfolding dist_norm
by blast
show ?thesis
apply (rule_tac x="min (e/2) (d/real n/8)" in exI)
apply safe
proof -
show "0 < min (e / 2) (d / real n / 8)"
using d' e by auto
fix x y z i
assume as:
"x ∈ unit_cube" "y ∈ unit_cube" "z ∈ unit_cube"
"norm (x - z) < min (e / 2) (d / real n / 8)"
"norm (y - z) < min (e / 2) (d / real n / 8)"
"label x i ≠ label y i"
assume i: "i ∈ Basis"
have *: "⋀z fz x fx n1 n2 n3 n4 d4 d :: real. ¦fx - x¦ ≤ n1 + n2 ⟹
¦fx - fz¦ ≤ n3 ⟹ ¦x - z¦ ≤ n4 ⟹
n1 < d4 ⟹ n2 < 2 * d4 ⟹ n3 < d4 ⟹ n4 < d4 ⟹
(8 * d4 = d) ⟹ ¦fz - z¦ < d"
by auto
show "¦(f z - z) ∙ i¦ < d / real n"
unfolding inner_simps
proof (rule *)
show "¦f x ∙ i - x ∙ i¦ ≤ norm (f y -f x) + norm (y - x)"
apply (rule lem1[rule_format])
using as i
apply auto
done
show "¦f x ∙ i - f z ∙ i¦ ≤ norm (f x - f z)" "¦x ∙ i - z ∙ i¦ ≤ norm (x - z)"
unfolding inner_diff_left[symmetric]
by (rule Basis_le_norm[OF i])+
have tria: "norm (y - x) ≤ norm (y - z) + norm (x - z)"
using dist_triangle[of y x z, unfolded dist_norm]
unfolding norm_minus_commute
by auto
also have "… < e / 2 + e / 2"
apply (rule add_strict_mono)
using as(4,5)
apply auto
done
finally show "norm (f y - f x) < d / real n / 8"
apply -
apply (rule e(2))
using as
apply auto
done
have "norm (y - z) + norm (x - z) < d / real n / 8 + d / real n / 8"
apply (rule add_strict_mono)
using as
apply auto
done
then show "norm (y - x) < 2 * (d / real n / 8)"
using tria
by auto
show "norm (f x - f z) < d / real n / 8"
apply (rule e(2))
using as e(1)
apply auto
done
qed (insert as, auto)
qed
qed
then
obtain e where e:
"e > 0"
"⋀x y z i. x ∈ unit_cube ⟹
y ∈ unit_cube ⟹
z ∈ unit_cube ⟹
i ∈ Basis ⟹
norm (x - z) < e ∧ norm (y - z) < e ∧ label x i ≠ label y i ⟹
¦(f z - z) ∙ i¦ < d / real n"
by blast
obtain p :: nat where p: "1 + real n / e ≤ real p"
using real_arch_simple ..
have "1 + real n / e > 0"
using e(1) n by (simp add: add_pos_pos)
then have "p > 0"
using p by auto
obtain b :: "nat ⇒ 'a" where b: "bij_betw b {..< n} Basis"
by atomize_elim (auto simp: n_def intro!: finite_same_card_bij)
def b' ≡ "inv_into {..< n} b"
then have b': "bij_betw b' Basis {..< n}"
using bij_betw_inv_into[OF b] by auto
then have b'_Basis: "⋀i. i ∈ Basis ⟹ b' i ∈ {..< n}"
unfolding bij_betw_def by (auto simp: set_eq_iff)
have bb'[simp]:"⋀i. i ∈ Basis ⟹ b (b' i) = i"
unfolding b'_def
using b
by (auto simp: f_inv_into_f bij_betw_def)
have b'b[simp]:"⋀i. i < n ⟹ b' (b i) = i"
unfolding b'_def
using b
by (auto simp: inv_into_f_eq bij_betw_def)
have *: "⋀x :: nat. x = 0 ∨ x = 1 ⟷ x ≤ 1"
by auto
have b'': "⋀j. j < n ⟹ b j ∈ Basis"
using b unfolding bij_betw_def by auto
have q1: "0 < p" "∀x. (∀i<n. x i ≤ p) ⟶
(∀i<n. (label (∑i∈Basis. (real (x (b' i)) / real p) *⇩R i) ∘ b) i = 0 ∨
(label (∑i∈Basis. (real (x (b' i)) / real p) *⇩R i) ∘ b) i = 1)"
unfolding *
using ‹p > 0› ‹n > 0›
using label(1)[OF b'']
by auto
{ fix x :: "nat ⇒ nat" and i assume "∀i<n. x i ≤ p" "i < n" "x i = p ∨ x i = 0"
then have "(∑i∈Basis. (real (x (b' i)) / real p) *⇩R i) ∈ (unit_cube::'a set)"
using b'_Basis
by (auto simp add: mem_unit_cube inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) }
note cube = this
have q2: "∀x. (∀i<n. x i ≤ p) ⟶ (∀i<n. x i = 0 ⟶
(label (∑i∈Basis. (real (x (b' i)) / real p) *⇩R i) ∘ b) i = 0)"
unfolding o_def using cube ‹p > 0› by (intro allI impI label(2)) (auto simp add: b'')
have q3: "∀x. (∀i<n. x i ≤ p) ⟶ (∀i<n. x i = p ⟶
(label (∑i∈Basis. (real (x (b' i)) / real p) *⇩R i) ∘ b) i = 1)"
using cube ‹p > 0› unfolding o_def by (intro allI impI label(3)) (auto simp add: b'')
obtain q where q:
"∀i<n. q i < p"
"∀i<n.
∃r s. (∀j<n. q j ≤ r j ∧ r j ≤ q j + 1) ∧
(∀j<n. q j ≤ s j ∧ s j ≤ q j + 1) ∧
(label (∑i∈Basis. (real (r (b' i)) / real p) *⇩R i) ∘ b) i ≠
(label (∑i∈Basis. (real (s (b' i)) / real p) *⇩R i) ∘ b) i"
by (rule kuhn_lemma[OF q1 q2 q3])
def z ≡ "(∑i∈Basis. (real (q (b' i)) / real p) *⇩R i)::'a"
have "∃i∈Basis. d / real n ≤ ¦(f z - z)∙i¦"
proof (rule ccontr)
have "∀i∈Basis. q (b' i) ∈ {0..p}"
using q(1) b'
by (auto intro: less_imp_le simp: bij_betw_def)
then have "z ∈ unit_cube"
unfolding z_def mem_unit_cube
using b'_Basis
by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
then have d_fz_z: "d ≤ norm (f z - z)"
by (rule d)
assume "¬ ?thesis"
then have as: "∀i∈Basis. ¦f z ∙ i - z ∙ i¦ < d / real n"
using ‹n > 0›
by (auto simp add: not_le inner_diff)
have "norm (f z - z) ≤ (∑i∈Basis. ¦f z ∙ i - z ∙ i¦)"
unfolding inner_diff_left[symmetric]
by (rule norm_le_l1)
also have "… < (∑(i::'a) ∈ Basis. d / real n)"
apply (rule setsum_strict_mono)
using as
apply auto
done
also have "… = d"
using DIM_positive[where 'a='a]
by (auto simp: n_def)
finally show False
using d_fz_z by auto
qed
then obtain i where i: "i ∈ Basis" "d / real n ≤ ¦(f z - z) ∙ i¦" ..
have *: "b' i < n"
using i and b'[unfolded bij_betw_def]
by auto
obtain r s where rs:
"⋀j. j < n ⟹ q j ≤ r j ∧ r j ≤ q j + 1"
"⋀j. j < n ⟹ q j ≤ s j ∧ s j ≤ q j + 1"
"(label (∑i∈Basis. (real (r (b' i)) / real p) *⇩R i) ∘ b) (b' i) ≠
(label (∑i∈Basis. (real (s (b' i)) / real p) *⇩R i) ∘ b) (b' i)"
using q(2)[rule_format,OF *] by blast
have b'_im: "⋀i. i ∈ Basis ⟹ b' i < n"
using b' unfolding bij_betw_def by auto
def r' ≡ "(∑i∈Basis. (real (r (b' i)) / real p) *⇩R i)::'a"
have "⋀i. i ∈ Basis ⟹ r (b' i) ≤ p"
apply (rule order_trans)
apply (rule rs(1)[OF b'_im,THEN conjunct2])
using q(1)[rule_format,OF b'_im]
apply (auto simp add: Suc_le_eq)
done
then have "r' ∈ unit_cube"
unfolding r'_def mem_unit_cube
using b'_Basis
by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
def s' ≡ "(∑i∈Basis. (real (s (b' i)) / real p) *⇩R i)::'a"
have "⋀i. i ∈ Basis ⟹ s (b' i) ≤ p"
apply (rule order_trans)
apply (rule rs(2)[OF b'_im, THEN conjunct2])
using q(1)[rule_format,OF b'_im]
apply (auto simp add: Suc_le_eq)
done
then have "s' ∈ unit_cube"
unfolding s'_def mem_unit_cube
using b'_Basis
by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
have "z ∈ unit_cube"
unfolding z_def mem_unit_cube
using b'_Basis q(1)[rule_format,OF b'_im] ‹p > 0›
by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)
have *: "⋀x. 1 + real x = real (Suc x)"
by auto
{
have "(∑i∈Basis. ¦real (r (b' i)) - real (q (b' i))¦) ≤ (∑(i::'a)∈Basis. 1)"
apply (rule setsum_mono)
using rs(1)[OF b'_im]
apply (auto simp add:* field_simps simp del: of_nat_Suc)
done
also have "… < e * real p"
using p ‹e > 0› ‹p > 0›
by (auto simp add: field_simps n_def)
finally have "(∑i∈Basis. ¦real (r (b' i)) - real (q (b' i))¦) < e * real p" .
}
moreover
{
have "(∑i∈Basis. ¦real (s (b' i)) - real (q (b' i))¦) ≤ (∑(i::'a)∈Basis. 1)"
apply (rule setsum_mono)
using rs(2)[OF b'_im]
apply (auto simp add:* field_simps simp del: of_nat_Suc)
done
also have "… < e * real p"
using p ‹e > 0› ‹p > 0›
by (auto simp add: field_simps n_def)
finally have "(∑i∈Basis. ¦real (s (b' i)) - real (q (b' i))¦) < e * real p" .
}
ultimately
have "norm (r' - z) < e" and "norm (s' - z) < e"
unfolding r'_def s'_def z_def
using ‹p > 0›
apply (rule_tac[!] le_less_trans[OF norm_le_l1])
apply (auto simp add: field_simps setsum_divide_distrib[symmetric] inner_diff_left)
done
then have "¦(f z - z) ∙ i¦ < d / real n"
using rs(3) i
unfolding r'_def[symmetric] s'_def[symmetric] o_def bb'
by (intro e(2)[OF ‹r'∈unit_cube› ‹s'∈unit_cube› ‹z∈unit_cube›]) auto
then show False
using i by auto
qed
subsection ‹Retractions›
definition "retraction s t r ⟷ t ⊆ s ∧ continuous_on s r ∧ r ` s ⊆ t ∧ (∀x∈t. r x = x)"
definition retract_of (infixl "retract'_of" 50)
where "(t retract_of s) ⟷ (∃r. retraction s t r)"
lemma retraction_idempotent: "retraction s t r ⟹ x ∈ s ⟹ r (r x) = r x"
unfolding retraction_def by auto
subsection ‹Preservation of fixpoints under (more general notion of) retraction›
lemma invertible_fixpoint_property:
fixes s :: "'a::euclidean_space set"
and t :: "'b::euclidean_space set"
assumes "continuous_on t i"
and "i ` t ⊆ s"
and "continuous_on s r"
and "r ` s ⊆ t"
and "∀y∈t. r (i y) = y"
and "∀f. continuous_on s f ∧ f ` s ⊆ s ⟶ (∃x∈s. f x = x)"
and "continuous_on t g"
and "g ` t ⊆ t"
obtains y where "y ∈ t" and "g y = y"
proof -
have "∃x∈s. (i ∘ g ∘ r) x = x"
apply (rule assms(6)[rule_format])
apply rule
apply (rule continuous_on_compose assms)+
apply ((rule continuous_on_subset)?, rule assms)+
using assms(2,4,8)
apply auto
apply blast
done
then obtain x where x: "x ∈ s" "(i ∘ g ∘ r) x = x" ..
then have *: "g (r x) ∈ t"
using assms(4,8) by auto
have "r ((i ∘ g ∘ r) x) = r x"
using x by auto
then show ?thesis
apply (rule_tac that[of "r x"])
using x
unfolding o_def
unfolding assms(5)[rule_format,OF *]
using assms(4)
apply auto
done
qed
lemma homeomorphic_fixpoint_property:
fixes s :: "'a::euclidean_space set"
and t :: "'b::euclidean_space set"
assumes "s homeomorphic t"
shows "(∀f. continuous_on s f ∧ f ` s ⊆ s ⟶ (∃x∈s. f x = x)) ⟷
(∀g. continuous_on t g ∧ g ` t ⊆ t ⟶ (∃y∈t. g y = y))"
proof -
obtain r i where
"∀x∈s. i (r x) = x"
"r ` s = t"
"continuous_on s r"
"∀y∈t. r (i y) = y"
"i ` t = s"
"continuous_on t i"
using assms
unfolding homeomorphic_def homeomorphism_def
by blast
then show ?thesis
apply -
apply rule
apply (rule_tac[!] allI impI)+
apply (rule_tac g=g in invertible_fixpoint_property[of t i s r])
prefer 10
apply (rule_tac g=f in invertible_fixpoint_property[of s r t i])
apply auto
done
qed
lemma retract_fixpoint_property:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
and s :: "'a set"
assumes "t retract_of s"
and "∀f. continuous_on s f ∧ f ` s ⊆ s ⟶ (∃x∈s. f x = x)"
and "continuous_on t g"
and "g ` t ⊆ t"
obtains y where "y ∈ t" and "g y = y"
proof -
obtain h where "retraction s t h"
using assms(1) unfolding retract_of_def ..
then show ?thesis
unfolding retraction_def
apply -
apply (rule invertible_fixpoint_property[OF continuous_on_id _ _ _ _ assms(2), of t h g])
prefer 7
apply (rule_tac y = y in that)
using assms
apply auto
done
qed
subsection ‹The Brouwer theorem for any set with nonempty interior›
lemma convex_unit_cube: "convex unit_cube"
apply (rule is_interval_convex)
apply (clarsimp simp add: is_interval_def mem_unit_cube)
apply (drule (1) bspec)+
apply auto
done
lemma brouwer_weak:
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes "compact s"
and "convex s"
and "interior s ≠ {}"
and "continuous_on s f"
and "f ` s ⊆ s"
obtains x where "x ∈ s" and "f x = x"
proof -
let ?U = "unit_cube :: 'a set"
have "∑Basis /⇩R 2 ∈ interior ?U"
proof (rule interiorI)
let ?I = "(⋂i∈Basis. {x::'a. 0 < x ∙ i} ∩ {x. x ∙ i < 1})"
show "open ?I"
by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less)
show "∑Basis /⇩R 2 ∈ ?I"
by simp
show "?I ⊆ unit_cube"
unfolding unit_cube_def by force
qed
then have *: "interior ?U ≠ {}" by fast
have *: "?U homeomorphic s"
using homeomorphic_convex_compact[OF convex_unit_cube compact_unit_cube * assms(2,1,3)] .
have "∀f. continuous_on ?U f ∧ f ` ?U ⊆ ?U ⟶
(∃x∈?U. f x = x)"
using brouwer_cube by auto
then show ?thesis
unfolding homeomorphic_fixpoint_property[OF *]
using assms
by (auto simp: intro: that)
qed
text ‹And in particular for a closed ball.›
lemma brouwer_ball:
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes "e > 0"
and "continuous_on (cball a e) f"
and "f ` cball a e ⊆ cball a e"
obtains x where "x ∈ cball a e" and "f x = x"
using brouwer_weak[OF compact_cball convex_cball, of a e f]
unfolding interior_cball ball_eq_empty
using assms by auto
text ‹Still more general form; could derive this directly without using the
rather involved ‹HOMEOMORPHIC_CONVEX_COMPACT› theorem, just using
a scaling and translation to put the set inside the unit cube.›
lemma brouwer:
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes "compact s"
and "convex s"
and "s ≠ {}"
and "continuous_on s f"
and "f ` s ⊆ s"
obtains x where "x ∈ s" and "f x = x"
proof -
have "∃e>0. s ⊆ cball 0 e"
using compact_imp_bounded[OF assms(1)]
unfolding bounded_pos
apply (erule_tac exE)
apply (rule_tac x=b in exI)
apply (auto simp add: dist_norm)
done
then obtain e where e: "e > 0" "s ⊆ cball 0 e"
by blast
have "∃x∈ cball 0 e. (f ∘ closest_point s) x = x"
apply (rule_tac brouwer_ball[OF e(1), of 0 "f ∘ closest_point s"])
apply (rule continuous_on_compose )
apply (rule continuous_on_closest_point[OF assms(2) compact_imp_closed[OF assms(1)] assms(3)])
apply (rule continuous_on_subset[OF assms(4)])
apply (insert closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)])
using assms(5)[unfolded subset_eq]
using e(2)[unfolded subset_eq mem_cball]
apply (auto simp add: dist_norm)
done
then obtain x where x: "x ∈ cball 0 e" "(f ∘ closest_point s) x = x" ..
have *: "closest_point s x = x"
apply (rule closest_point_self)
apply (rule assms(5)[unfolded subset_eq,THEN bspec[where x="x"], unfolded image_iff])
apply (rule_tac x="closest_point s x" in bexI)
using x
unfolding o_def
using closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3), of x]
apply auto
done
show thesis
apply (rule_tac x="closest_point s x" in that)
unfolding x(2)[unfolded o_def]
apply (rule closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)])
using *
apply auto
done
qed
text ‹So we get the no-retraction theorem.›
lemma no_retraction_cball:
fixes a :: "'a::euclidean_space"
assumes "e > 0"
shows "¬ (frontier (cball a e) retract_of (cball a e))"
proof
assume *: "frontier (cball a e) retract_of (cball a e)"
have **: "⋀xa. a - (2 *⇩R a - xa) = - (a - xa)"
using scaleR_left_distrib[of 1 1 a] by auto
obtain x where x:
"x ∈ {x. norm (a - x) = e}"
"2 *⇩R a - x = x"
apply (rule retract_fixpoint_property[OF *, of "λx. scaleR 2 a - x"])
apply (blast intro: brouwer_ball[OF assms])
apply (intro continuous_intros)
unfolding frontier_cball subset_eq Ball_def image_iff dist_norm sphere_def
apply (auto simp add: ** norm_minus_commute)
done
then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
by (auto simp add: algebra_simps)
then have "a = x"
unfolding scaleR_left_distrib[symmetric]
by auto
then show False
using x assms by auto
qed
subsection‹Retractions›
lemma retraction:
"retraction s t r ⟷
t ⊆ s ∧ continuous_on s r ∧ r ` s = t ∧ (∀x ∈ t. r x = x)"
by (force simp: retraction_def)
lemma retract_of_imp_extensible:
assumes "s retract_of t" and "continuous_on s f" and "f ` s ⊆ u"
obtains g where "continuous_on t g" "g ` t ⊆ u" "⋀x. x ∈ s ⟹ g x = f x"
using assms
apply (clarsimp simp add: retract_of_def retraction)
apply (rule_tac g = "f o r" in that)
apply (auto simp: continuous_on_compose2)
done
lemma idempotent_imp_retraction:
assumes "continuous_on s f" and "f ` s ⊆ s" and "⋀x. x ∈ s ⟹ f(f x) = f x"
shows "retraction s (f ` s) f"
by (simp add: assms retraction)
lemma retraction_subset:
assumes "retraction s t r" and "t ⊆ s'" and "s' ⊆ s"
shows "retraction s' t r"
apply (simp add: retraction_def)
by (metis assms continuous_on_subset image_mono retraction)
lemma retract_of_subset:
assumes "t retract_of s" and "t ⊆ s'" and "s' ⊆ s"
shows "t retract_of s'"
by (meson assms retract_of_def retraction_subset)
lemma retraction_refl [simp]: "retraction s s (λx. x)"
by (simp add: continuous_on_id retraction)
lemma retract_of_refl [iff]: "s retract_of s"
using continuous_on_id retract_of_def retraction_def by fastforce
lemma retract_of_imp_subset:
"s retract_of t ⟹ s ⊆ t"
by (simp add: retract_of_def retraction_def)
lemma retract_of_empty [simp]:
"({} retract_of s) ⟷ s = {}" "(s retract_of {}) ⟷ s = {}"
by (auto simp: retract_of_def retraction_def)
lemma retract_of_singleton [iff]: "({x} retract_of s) ⟷ x ∈ s"
using continuous_on_const
by (auto simp: retract_of_def retraction_def)
lemma retraction_comp:
"⟦retraction s t f; retraction t u g⟧
⟹ retraction s u (g o f)"
apply (auto simp: retraction_def intro: continuous_on_compose2)
by blast
lemma retract_of_trans:
assumes "s retract_of t" and "t retract_of u"
shows "s retract_of u"
using assms by (auto simp: retract_of_def intro: retraction_comp)
lemma closedin_retract:
fixes s :: "'a :: real_normed_vector set"
assumes "s retract_of t"
shows "closedin (subtopology euclidean t) s"
proof -
obtain r where "s ⊆ t" "continuous_on t r" "r ` t ⊆ s" "⋀x. x ∈ s ⟹ r x = x"
using assms by (auto simp: retract_of_def retraction_def)
then have s: "s = {x ∈ t. (norm(r x - x)) = 0}" by auto
show ?thesis
apply (subst s)
apply (rule continuous_closedin_preimage_constant)
by (simp add: ‹continuous_on t r› continuous_on_diff continuous_on_id continuous_on_norm)
qed
lemma retract_of_contractible:
assumes "contractible t" "s retract_of t"
shows "contractible s"
using assms
apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with)
apply (rule_tac x="r a" in exI)
apply (rule_tac x="r o h" in exI)
apply (intro conjI continuous_intros continuous_on_compose)
apply (erule continuous_on_subset | force)+
done
lemma retract_of_compact:
"⟦compact t; s retract_of t⟧ ⟹ compact s"
by (metis compact_continuous_image retract_of_def retraction)
lemma retract_of_closed:
fixes s :: "'a :: real_normed_vector set"
shows "⟦closed t; s retract_of t⟧ ⟹ closed s"
by (metis closedin_retract closedin_closed_eq)
lemma retract_of_connected:
"⟦connected t; s retract_of t⟧ ⟹ connected s"
by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
lemma retract_of_path_connected:
"⟦path_connected t; s retract_of t⟧ ⟹ path_connected s"
by (metis path_connected_continuous_image retract_of_def retraction)
lemma retract_of_simply_connected:
"⟦simply_connected t; s retract_of t⟧ ⟹ simply_connected s"
apply (simp add: retract_of_def retraction_def, clarify)
apply (rule simply_connected_retraction_gen)
apply (force simp: continuous_on_id elim!: continuous_on_subset)+
done
lemma retract_of_homotopically_trivial:
assumes ts: "t retract_of s"
and hom: "⋀f g. ⟦continuous_on u f; f ` u ⊆ s;
continuous_on u g; g ` u ⊆ s⟧
⟹ homotopic_with (λx. True) u s f g"
and "continuous_on u f" "f ` u ⊆ t"
and "continuous_on u g" "g ` u ⊆ t"
shows "homotopic_with (λx. True) u t f g"
proof -
obtain r where "r ` s ⊆ s" "continuous_on s r" "∀x∈s. r (r x) = r x" "t = r ` s"
using ts by (auto simp: retract_of_def retraction)
then obtain k where "Retracts s r t k"
unfolding Retracts_def
by (metis continuous_on_subset dual_order.trans image_iff image_mono)
then show ?thesis
apply (rule Retracts.homotopically_trivial_retraction_gen)
using assms
apply (force simp: hom)+
done
qed
lemma retract_of_homotopically_trivial_null:
assumes ts: "t retract_of s"
and hom: "⋀f. ⟦continuous_on u f; f ` u ⊆ s⟧
⟹ ∃c. homotopic_with (λx. True) u s f (λx. c)"
and "continuous_on u f" "f ` u ⊆ t"
obtains c where "homotopic_with (λx. True) u t f (λx. c)"
proof -
obtain r where "r ` s ⊆ s" "continuous_on s r" "∀x∈s. r (r x) = r x" "t = r ` s"
using ts by (auto simp: retract_of_def retraction)
then obtain k where "Retracts s r t k"
unfolding Retracts_def
by (metis continuous_on_subset dual_order.trans image_iff image_mono)
then show ?thesis
apply (rule Retracts.homotopically_trivial_retraction_null_gen)
apply (rule TrueI refl assms that | assumption)+
done
qed
lemma retraction_imp_quotient_map:
"retraction s t r
⟹ u ⊆ t
⟹ (openin (subtopology euclidean s) {x. x ∈ s ∧ r x ∈ u} ⟷
openin (subtopology euclidean t) u)"
apply (clarsimp simp add: retraction)
apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
apply (auto simp: elim: continuous_on_subset)
done
lemma retract_of_locally_compact:
fixes s :: "'a :: {heine_borel,real_normed_vector} set"
shows "⟦ locally compact s; t retract_of s⟧ ⟹ locally compact t"
by (metis locally_compact_closedin closedin_retract)
lemma retract_of_times:
"⟦s retract_of s'; t retract_of t'⟧ ⟹ (s × t) retract_of (s' × t')"
apply (simp add: retract_of_def retraction_def Sigma_mono, clarify)
apply (rename_tac f g)
apply (rule_tac x="λz. ((f o fst) z, (g o snd) z)" in exI)
apply (rule conjI continuous_intros | erule continuous_on_subset | force)+
done
lemma homotopic_into_retract:
"⟦f ` s ⊆ t; g ` s ⊆ t; t retract_of u;
homotopic_with (λx. True) s u f g⟧
⟹ homotopic_with (λx. True) s t f g"
apply (subst (asm) homotopic_with_def)
apply (simp add: homotopic_with retract_of_def retraction_def, clarify)
apply (rule_tac x="r o h" in exI)
apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
done
end