src/HOL/Analysis/Brouwer_Fixpoint.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 69945 35ba13ac6e5c
child 69986 f2d327275065
permissions -rw-r--r--
more strict AFP properties;
wenzelm@53674
     1
(*  Author:     John Harrison
lp15@63305
     2
    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light) and LCP
wenzelm@53674
     3
*)
hoelzl@33741
     4
hoelzl@33741
     5
(* At the moment this is just Brouwer's fixpoint theorem. The proof is from  *)
hoelzl@33741
     6
(* Kuhn: "some combinatorial lemmas in topology", IBM J. v4. (1960) p. 518   *)
hoelzl@33741
     7
(* See "http://www.research.ibm.com/journal/rd/045/ibmrd0405K.pdf".          *)
hoelzl@33741
     8
(*                                                                           *)
hoelzl@33741
     9
(* The script below is quite messy, but at least we avoid formalizing any    *)
hoelzl@33741
    10
(* topological machinery; we don't even use barycentric subdivision; this is *)
hoelzl@33741
    11
(* the big advantage of Kuhn's proof over the usual Sperner's lemma one.     *)
hoelzl@33741
    12
(*                                                                           *)
hoelzl@33741
    13
(*              (c) Copyright, John Harrison 1998-2008                       *)
hoelzl@33741
    14
nipkow@68617
    15
section \<open>Brouwer's Fixed Point Theorem\<close>
hoelzl@33741
    16
hoelzl@33741
    17
theory Brouwer_Fixpoint
immler@69620
    18
  imports
immler@69620
    19
    Path_Connected
immler@69620
    20
    Homeomorphism
immler@69620
    21
    Continuous_Extension
hoelzl@33741
    22
begin
hoelzl@33741
    23
nipkow@68617
    24
subsection \<open>Retractions\<close>
nipkow@68617
    25
nipkow@68617
    26
lemma retract_of_contractible:
nipkow@68617
    27
  assumes "contractible T" "S retract_of T"
nipkow@68617
    28
    shows "contractible S"
nipkow@68617
    29
using assms
nipkow@68617
    30
apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with)
nipkow@68617
    31
apply (rule_tac x="r a" in exI)
nipkow@68617
    32
apply (rule_tac x="r \<circ> h" in exI)
nipkow@68617
    33
apply (intro conjI continuous_intros continuous_on_compose)
nipkow@68617
    34
apply (erule continuous_on_subset | force)+
nipkow@68617
    35
done
nipkow@68617
    36
nipkow@68617
    37
lemma retract_of_path_connected:
nipkow@68617
    38
    "\<lbrakk>path_connected T; S retract_of T\<rbrakk> \<Longrightarrow> path_connected S"
nipkow@68617
    39
  by (metis path_connected_continuous_image retract_of_def retraction)
nipkow@68617
    40
nipkow@68617
    41
lemma retract_of_simply_connected:
nipkow@68617
    42
    "\<lbrakk>simply_connected T; S retract_of T\<rbrakk> \<Longrightarrow> simply_connected S"
nipkow@68617
    43
apply (simp add: retract_of_def retraction_def, clarify)
nipkow@68617
    44
apply (rule simply_connected_retraction_gen)
nipkow@69738
    45
apply (force elim!: continuous_on_subset)+
nipkow@68617
    46
done
nipkow@68617
    47
nipkow@68617
    48
lemma retract_of_homotopically_trivial:
nipkow@68617
    49
  assumes ts: "T retract_of S"
nipkow@68617
    50
      and hom: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S;
nipkow@68617
    51
                       continuous_on U g; g ` U \<subseteq> S\<rbrakk>
nipkow@68617
    52
                       \<Longrightarrow> homotopic_with (\<lambda>x. True) U S f g"
nipkow@68617
    53
      and "continuous_on U f" "f ` U \<subseteq> T"
nipkow@68617
    54
      and "continuous_on U g" "g ` U \<subseteq> T"
nipkow@68617
    55
    shows "homotopic_with (\<lambda>x. True) U T f g"
nipkow@68617
    56
proof -
nipkow@68617
    57
  obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
nipkow@68617
    58
    using ts by (auto simp: retract_of_def retraction)
nipkow@68617
    59
  then obtain k where "Retracts S r T k"
nipkow@68617
    60
    unfolding Retracts_def
nipkow@68617
    61
    by (metis continuous_on_subset dual_order.trans image_iff image_mono)
nipkow@68617
    62
  then show ?thesis
nipkow@68617
    63
    apply (rule Retracts.homotopically_trivial_retraction_gen)
nipkow@68617
    64
    using assms
nipkow@68617
    65
    apply (force simp: hom)+
nipkow@68617
    66
    done
nipkow@68617
    67
qed
nipkow@68617
    68
nipkow@68617
    69
lemma retract_of_homotopically_trivial_null:
nipkow@68617
    70
  assumes ts: "T retract_of S"
nipkow@68617
    71
      and hom: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S\<rbrakk>
nipkow@68617
    72
                     \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c)"
nipkow@68617
    73
      and "continuous_on U f" "f ` U \<subseteq> T"
nipkow@68617
    74
  obtains c where "homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)"
nipkow@68617
    75
proof -
nipkow@68617
    76
  obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
nipkow@68617
    77
    using ts by (auto simp: retract_of_def retraction)
nipkow@68617
    78
  then obtain k where "Retracts S r T k"
nipkow@68617
    79
    unfolding Retracts_def
nipkow@68617
    80
    by (metis continuous_on_subset dual_order.trans image_iff image_mono)
nipkow@68617
    81
  then show ?thesis
nipkow@68617
    82
    apply (rule Retracts.homotopically_trivial_retraction_null_gen)
nipkow@68617
    83
    apply (rule TrueI refl assms that | assumption)+
nipkow@68617
    84
    done
nipkow@68617
    85
qed
nipkow@68617
    86
lp15@69945
    87
lemma retraction_openin_vimage_iff:
lp15@69922
    88
  "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U"
haftmann@69661
    89
  if retraction: "retraction S T r" and "U \<subseteq> T"
haftmann@69661
    90
  using retraction apply (rule retractionE)
haftmann@69661
    91
  apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
haftmann@69661
    92
  using \<open>U \<subseteq> T\<close> apply (auto elim: continuous_on_subset)
haftmann@69661
    93
  done
nipkow@68617
    94
nipkow@68617
    95
lemma retract_of_locally_compact:
nipkow@68617
    96
    fixes S :: "'a :: {heine_borel,real_normed_vector} set"
nipkow@68617
    97
    shows  "\<lbrakk> locally compact S; T retract_of S\<rbrakk> \<Longrightarrow> locally compact T"
nipkow@68617
    98
  by (metis locally_compact_closedin closedin_retract)
nipkow@68617
    99
nipkow@68617
   100
lemma homotopic_into_retract:
nipkow@68617
   101
   "\<lbrakk>f ` S \<subseteq> T; g ` S \<subseteq> T; T retract_of U; homotopic_with (\<lambda>x. True) S U f g\<rbrakk>
nipkow@68617
   102
        \<Longrightarrow> homotopic_with (\<lambda>x. True) S T f g"
nipkow@68617
   103
apply (subst (asm) homotopic_with_def)
nipkow@68617
   104
apply (simp add: homotopic_with retract_of_def retraction_def, clarify)
nipkow@68617
   105
apply (rule_tac x="r \<circ> h" in exI)
nipkow@68617
   106
apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
nipkow@68617
   107
done
nipkow@68617
   108
nipkow@68617
   109
lemma retract_of_locally_connected:
nipkow@68617
   110
  assumes "locally connected T" "S retract_of T"
haftmann@69661
   111
  shows "locally connected S"
nipkow@68617
   112
  using assms
lp15@69945
   113
  by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_connected_quotient_image retract_ofE)
nipkow@68617
   114
nipkow@68617
   115
lemma retract_of_locally_path_connected:
nipkow@68617
   116
  assumes "locally path_connected T" "S retract_of T"
haftmann@69661
   117
  shows "locally path_connected S"
nipkow@68617
   118
  using assms
lp15@69945
   119
  by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_path_connected_quotient_image retract_ofE)
nipkow@68617
   120
nipkow@68617
   121
text \<open>A few simple lemmas about deformation retracts\<close>
nipkow@68617
   122
nipkow@68617
   123
lemma deformation_retract_imp_homotopy_eqv:
nipkow@68617
   124
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   125
  assumes "homotopic_with (\<lambda>x. True) S S id r" and r: "retraction S T r"
nipkow@68617
   126
  shows "S homotopy_eqv T"
nipkow@68617
   127
proof -
nipkow@68617
   128
  have "homotopic_with (\<lambda>x. True) S S (id \<circ> r) id"
nipkow@68617
   129
    by (simp add: assms(1) homotopic_with_symD)
nipkow@68617
   130
  moreover have "homotopic_with (\<lambda>x. True) T T (r \<circ> id) id"
nipkow@68617
   131
    using r unfolding retraction_def
nipkow@68617
   132
    by (metis (no_types, lifting) comp_id continuous_on_id' homotopic_with_equal homotopic_with_symD id_def image_id order_refl)
nipkow@68617
   133
  ultimately
nipkow@68617
   134
  show ?thesis
nipkow@68617
   135
    unfolding homotopy_eqv_def
nipkow@68617
   136
    by (metis continuous_on_id' id_def image_id r retraction_def)
nipkow@68617
   137
qed
nipkow@68617
   138
nipkow@68617
   139
lemma deformation_retract:
nipkow@68617
   140
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   141
    shows "(\<exists>r. homotopic_with (\<lambda>x. True) S S id r \<and> retraction S T r) \<longleftrightarrow>
nipkow@68617
   142
           T retract_of S \<and> (\<exists>f. homotopic_with (\<lambda>x. True) S S id f \<and> f ` S \<subseteq> T)"
nipkow@68617
   143
    (is "?lhs = ?rhs")
nipkow@68617
   144
proof
nipkow@68617
   145
  assume ?lhs
nipkow@68617
   146
  then show ?rhs
nipkow@68617
   147
    by (auto simp: retract_of_def retraction_def)
nipkow@68617
   148
next
nipkow@68617
   149
  assume ?rhs
nipkow@68617
   150
  then show ?lhs
nipkow@68617
   151
    apply (clarsimp simp add: retract_of_def retraction_def)
nipkow@68617
   152
    apply (rule_tac x=r in exI, simp)
nipkow@68617
   153
     apply (rule homotopic_with_trans, assumption)
nipkow@68617
   154
     apply (rule_tac f = "r \<circ> f" and g="r \<circ> id" in homotopic_with_eq)
nipkow@68617
   155
        apply (rule_tac Y=S in homotopic_compose_continuous_left)
nipkow@68617
   156
         apply (auto simp: homotopic_with_sym)
nipkow@68617
   157
    done
nipkow@68617
   158
qed
nipkow@68617
   159
nipkow@68617
   160
lemma deformation_retract_of_contractible_sing:
nipkow@68617
   161
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   162
  assumes "contractible S" "a \<in> S"
nipkow@68617
   163
  obtains r where "homotopic_with (\<lambda>x. True) S S id r" "retraction S {a} r"
nipkow@68617
   164
proof -
nipkow@68617
   165
  have "{a} retract_of S"
nipkow@68617
   166
    by (simp add: \<open>a \<in> S\<close>)
nipkow@68617
   167
  moreover have "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
nipkow@68617
   168
      using assms
nipkow@69738
   169
      by (auto simp: contractible_def homotopic_into_contractible image_subset_iff)
nipkow@68617
   170
  moreover have "(\<lambda>x. a) ` S \<subseteq> {a}"
nipkow@68617
   171
    by (simp add: image_subsetI)
nipkow@68617
   172
  ultimately show ?thesis
nipkow@68617
   173
    using that deformation_retract  by metis
nipkow@68617
   174
qed
nipkow@68617
   175
nipkow@68617
   176
nipkow@68617
   177
lemma continuous_on_compact_surface_projection_aux:
nipkow@68617
   178
  fixes S :: "'a::t2_space set"
nipkow@68617
   179
  assumes "compact S" "S \<subseteq> T" "image q T \<subseteq> S"
nipkow@68617
   180
      and contp: "continuous_on T p"
nipkow@68617
   181
      and "\<And>x. x \<in> S \<Longrightarrow> q x = x"
nipkow@68617
   182
      and [simp]: "\<And>x. x \<in> T \<Longrightarrow> q(p x) = q x"
nipkow@68617
   183
      and "\<And>x. x \<in> T \<Longrightarrow> p(q x) = p x"
nipkow@68617
   184
    shows "continuous_on T q"
nipkow@68617
   185
proof -
nipkow@68617
   186
  have *: "image p T = image p S"
nipkow@68617
   187
    using assms by auto (metis imageI subset_iff)
nipkow@68617
   188
  have contp': "continuous_on S p"
nipkow@68617
   189
    by (rule continuous_on_subset [OF contp \<open>S \<subseteq> T\<close>])
nipkow@68617
   190
  have "continuous_on (p ` T) q"
nipkow@68617
   191
    by (simp add: "*" assms(1) assms(2) assms(5) continuous_on_inv contp' rev_subsetD)
nipkow@68617
   192
  then have "continuous_on T (q \<circ> p)"
nipkow@68617
   193
    by (rule continuous_on_compose [OF contp])
nipkow@68617
   194
  then show ?thesis
nipkow@68617
   195
    by (rule continuous_on_eq [of _ "q \<circ> p"]) (simp add: o_def)
nipkow@68617
   196
qed
nipkow@68617
   197
nipkow@68617
   198
lemma continuous_on_compact_surface_projection:
nipkow@68617
   199
  fixes S :: "'a::real_normed_vector set"
nipkow@68617
   200
  assumes "compact S"
nipkow@68617
   201
      and S: "S \<subseteq> V - {0}" and "cone V"
nipkow@68617
   202
      and iff: "\<And>x k. x \<in> V - {0} \<Longrightarrow> 0 < k \<and> (k *\<^sub>R x) \<in> S \<longleftrightarrow> d x = k"
nipkow@68617
   203
  shows "continuous_on (V - {0}) (\<lambda>x. d x *\<^sub>R x)"
nipkow@68617
   204
proof (rule continuous_on_compact_surface_projection_aux [OF \<open>compact S\<close> S])
nipkow@68617
   205
  show "(\<lambda>x. d x *\<^sub>R x) ` (V - {0}) \<subseteq> S"
nipkow@68617
   206
    using iff by auto
nipkow@68617
   207
  show "continuous_on (V - {0}) (\<lambda>x. inverse(norm x) *\<^sub>R x)"
nipkow@68617
   208
    by (intro continuous_intros) force
nipkow@68617
   209
  show "\<And>x. x \<in> S \<Longrightarrow> d x *\<^sub>R x = x"
nipkow@68617
   210
    by (metis S zero_less_one local.iff scaleR_one subset_eq)
nipkow@68617
   211
  show "d (x /\<^sub>R norm x) *\<^sub>R (x /\<^sub>R norm x) = d x *\<^sub>R x" if "x \<in> V - {0}" for x
nipkow@68617
   212
    using iff [of "inverse(norm x) *\<^sub>R x" "norm x * d x", symmetric] iff that \<open>cone V\<close>
nipkow@68617
   213
    by (simp add: field_simps cone_def zero_less_mult_iff)
nipkow@68617
   214
  show "d x *\<^sub>R x /\<^sub>R norm (d x *\<^sub>R x) = x /\<^sub>R norm x" if "x \<in> V - {0}" for x
nipkow@68617
   215
  proof -
nipkow@68617
   216
    have "0 < d x"
nipkow@68617
   217
      using local.iff that by blast
nipkow@68617
   218
    then show ?thesis
nipkow@68617
   219
      by simp
nipkow@68617
   220
  qed
nipkow@68617
   221
qed
nipkow@68617
   222
nipkow@69529
   223
subsection \<open>Absolute Retracts, Absolute Neighbourhood Retracts and Euclidean Neighbourhood Retracts\<close>
nipkow@68617
   224
nipkow@68617
   225
text \<open>Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also Euclidean neighbourhood
nipkow@68617
   226
retracts (ENR). We define AR and ANR by specializing the standard definitions for a set to embedding
nipkow@68617
   227
in spaces of higher dimension.
nipkow@68617
   228
wenzelm@69566
   229
John Harrison writes: "This turns out to be sufficient (since any set in \<open>\<real>\<^sup>n\<close> can be
wenzelm@69566
   230
embedded as a closed subset of a convex subset of \<open>\<real>\<^sup>n\<^sup>+\<^sup>1\<close>) to derive the usual
nipkow@68617
   231
definitions, but we need to split them into two implications because of the lack of type
nipkow@68617
   232
quantifiers. Then ENR turns out to be equivalent to ANR plus local compactness."\<close>
nipkow@68617
   233
nipkow@69529
   234
definition%important AR :: "'a::topological_space set \<Rightarrow> bool" where
nipkow@69529
   235
"AR S \<equiv> \<forall>U. \<forall>S'::('a * real) set.
lp15@69922
   236
  S homeomorphic S' \<and> closedin (top_of_set U) S' \<longrightarrow> S' retract_of U"
nipkow@69529
   237
nipkow@69529
   238
definition%important ANR :: "'a::topological_space set \<Rightarrow> bool" where
nipkow@69529
   239
"ANR S \<equiv> \<forall>U. \<forall>S'::('a * real) set.
lp15@69922
   240
  S homeomorphic S' \<and> closedin (top_of_set U) S'
lp15@69922
   241
  \<longrightarrow> (\<exists>T. openin (top_of_set U) T \<and> S' retract_of T)"
nipkow@69529
   242
nipkow@69529
   243
definition%important ENR :: "'a::topological_space set \<Rightarrow> bool" where
nipkow@69529
   244
"ENR S \<equiv> \<exists>U. open U \<and> S retract_of U"
nipkow@68617
   245
nipkow@68617
   246
text \<open>First, show that we do indeed get the "usual" properties of ARs and ANRs.\<close>
nipkow@68617
   247
nipkow@68617
   248
lemma AR_imp_absolute_extensor:
nipkow@68617
   249
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
nipkow@68617
   250
  assumes "AR S" and contf: "continuous_on T f" and "f ` T \<subseteq> S"
lp15@69922
   251
      and cloUT: "closedin (top_of_set U) T"
nipkow@68617
   252
  obtains g where "continuous_on U g" "g ` U \<subseteq> S" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
nipkow@68617
   253
proof -
nipkow@68617
   254
  have "aff_dim S < int (DIM('b \<times> real))"
nipkow@68617
   255
    using aff_dim_le_DIM [of S] by simp
nipkow@68617
   256
  then obtain C and S' :: "('b * real) set"
nipkow@68617
   257
          where C: "convex C" "C \<noteq> {}"
lp15@69922
   258
            and cloCS: "closedin (top_of_set C) S'"
nipkow@68617
   259
            and hom: "S homeomorphic S'"
nipkow@68617
   260
    by (metis that homeomorphic_closedin_convex)
nipkow@68617
   261
  then have "S' retract_of C"
nipkow@68617
   262
    using \<open>AR S\<close> by (simp add: AR_def)
nipkow@68617
   263
  then obtain r where "S' \<subseteq> C" and contr: "continuous_on C r"
nipkow@68617
   264
                  and "r ` C \<subseteq> S'" and rid: "\<And>x. x\<in>S' \<Longrightarrow> r x = x"
nipkow@68617
   265
    by (auto simp: retraction_def retract_of_def)
nipkow@68617
   266
  obtain g h where "homeomorphism S S' g h"
nipkow@68617
   267
    using hom by (force simp: homeomorphic_def)
nipkow@68617
   268
  then have "continuous_on (f ` T) g"
nipkow@68617
   269
    by (meson \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def)
nipkow@68617
   270
  then have contgf: "continuous_on T (g \<circ> f)"
nipkow@68617
   271
    by (metis continuous_on_compose contf)
nipkow@68617
   272
  have gfTC: "(g \<circ> f) ` T \<subseteq> C"
nipkow@68617
   273
  proof -
nipkow@68617
   274
    have "g ` S = S'"
nipkow@68617
   275
      by (metis (no_types) \<open>homeomorphism S S' g h\<close> homeomorphism_def)
nipkow@68617
   276
    with \<open>S' \<subseteq> C\<close> \<open>f ` T \<subseteq> S\<close> show ?thesis by force
nipkow@68617
   277
  qed
nipkow@68617
   278
  obtain f' where f': "continuous_on U f'"  "f' ` U \<subseteq> C"
nipkow@68617
   279
                      "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
nipkow@68617
   280
    by (metis Dugundji [OF C cloUT contgf gfTC])
nipkow@68617
   281
  show ?thesis
nipkow@68617
   282
  proof (rule_tac g = "h \<circ> r \<circ> f'" in that)
nipkow@68617
   283
    show "continuous_on U (h \<circ> r \<circ> f')"
nipkow@68617
   284
      apply (intro continuous_on_compose f')
nipkow@68617
   285
       using continuous_on_subset contr f' apply blast
nipkow@68617
   286
      by (meson \<open>homeomorphism S S' g h\<close> \<open>r ` C \<subseteq> S'\<close> continuous_on_subset \<open>f' ` U \<subseteq> C\<close> homeomorphism_def image_mono)
nipkow@68617
   287
    show "(h \<circ> r \<circ> f') ` U \<subseteq> S"
nipkow@68617
   288
      using \<open>homeomorphism S S' g h\<close> \<open>r ` C \<subseteq> S'\<close> \<open>f' ` U \<subseteq> C\<close>
nipkow@68617
   289
      by (fastforce simp: homeomorphism_def)
nipkow@68617
   290
    show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
nipkow@68617
   291
      using \<open>homeomorphism S S' g h\<close> \<open>f ` T \<subseteq> S\<close> f'
nipkow@68617
   292
      by (auto simp: rid homeomorphism_def)
nipkow@68617
   293
  qed
nipkow@68617
   294
qed
nipkow@68617
   295
nipkow@68617
   296
lemma AR_imp_absolute_retract:
nipkow@68617
   297
  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
nipkow@68617
   298
  assumes "AR S" "S homeomorphic S'"
lp15@69922
   299
      and clo: "closedin (top_of_set U) S'"
nipkow@68617
   300
    shows "S' retract_of U"
nipkow@68617
   301
proof -
nipkow@68617
   302
  obtain g h where hom: "homeomorphism S S' g h"
nipkow@68617
   303
    using assms by (force simp: homeomorphic_def)
nipkow@68617
   304
  have h: "continuous_on S' h" " h ` S' \<subseteq> S"
nipkow@68617
   305
    using hom homeomorphism_def apply blast
nipkow@68617
   306
    apply (metis hom equalityE homeomorphism_def)
nipkow@68617
   307
    done
nipkow@68617
   308
  obtain h' where h': "continuous_on U h'" "h' ` U \<subseteq> S"
nipkow@68617
   309
              and h'h: "\<And>x. x \<in> S' \<Longrightarrow> h' x = h x"
nipkow@68617
   310
    by (blast intro: AR_imp_absolute_extensor [OF \<open>AR S\<close> h clo])
nipkow@68617
   311
  have [simp]: "S' \<subseteq> U" using clo closedin_limpt by blast
nipkow@68617
   312
  show ?thesis
nipkow@68617
   313
  proof (simp add: retraction_def retract_of_def, intro exI conjI)
nipkow@68617
   314
    show "continuous_on U (g \<circ> h')"
nipkow@68617
   315
      apply (intro continuous_on_compose h')
nipkow@68617
   316
      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
nipkow@68617
   317
      done
nipkow@68617
   318
    show "(g \<circ> h') ` U \<subseteq> S'"
nipkow@68617
   319
      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
nipkow@68617
   320
    show "\<forall>x\<in>S'. (g \<circ> h') x = x"
nipkow@68617
   321
      by clarsimp (metis h'h hom homeomorphism_def)
nipkow@68617
   322
  qed
nipkow@68617
   323
qed
nipkow@68617
   324
nipkow@68617
   325
lemma AR_imp_absolute_retract_UNIV:
nipkow@68617
   326
  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
nipkow@68617
   327
  assumes "AR S" and hom: "S homeomorphic S'"
nipkow@68617
   328
      and clo: "closed S'"
nipkow@68617
   329
    shows "S' retract_of UNIV"
nipkow@68617
   330
apply (rule AR_imp_absolute_retract [OF \<open>AR S\<close> hom])
nipkow@68617
   331
using clo closed_closedin by auto
nipkow@68617
   332
nipkow@68617
   333
lemma absolute_extensor_imp_AR:
nipkow@68617
   334
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   335
  assumes "\<And>f :: 'a * real \<Rightarrow> 'a.
nipkow@68617
   336
           \<And>U T. \<lbrakk>continuous_on T f;  f ` T \<subseteq> S;
lp15@69922
   337
                  closedin (top_of_set U) T\<rbrakk>
nipkow@68617
   338
                 \<Longrightarrow> \<exists>g. continuous_on U g \<and> g ` U \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)"
nipkow@68617
   339
  shows "AR S"
nipkow@68617
   340
proof (clarsimp simp: AR_def)
nipkow@68617
   341
  fix U and T :: "('a * real) set"
lp15@69922
   342
  assume "S homeomorphic T" and clo: "closedin (top_of_set U) T"
nipkow@68617
   343
  then obtain g h where hom: "homeomorphism S T g h"
nipkow@68617
   344
    by (force simp: homeomorphic_def)
nipkow@68617
   345
  have h: "continuous_on T h" " h ` T \<subseteq> S"
nipkow@68617
   346
    using hom homeomorphism_def apply blast
nipkow@68617
   347
    apply (metis hom equalityE homeomorphism_def)
nipkow@68617
   348
    done
nipkow@68617
   349
  obtain h' where h': "continuous_on U h'" "h' ` U \<subseteq> S"
nipkow@68617
   350
              and h'h: "\<forall>x\<in>T. h' x = h x"
nipkow@68617
   351
    using assms [OF h clo] by blast
nipkow@68617
   352
  have [simp]: "T \<subseteq> U"
nipkow@68617
   353
    using clo closedin_imp_subset by auto
nipkow@68617
   354
  show "T retract_of U"
nipkow@68617
   355
  proof (simp add: retraction_def retract_of_def, intro exI conjI)
nipkow@68617
   356
    show "continuous_on U (g \<circ> h')"
nipkow@68617
   357
      apply (intro continuous_on_compose h')
nipkow@68617
   358
      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
nipkow@68617
   359
      done
nipkow@68617
   360
    show "(g \<circ> h') ` U \<subseteq> T"
nipkow@68617
   361
      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
nipkow@68617
   362
    show "\<forall>x\<in>T. (g \<circ> h') x = x"
nipkow@68617
   363
      by clarsimp (metis h'h hom homeomorphism_def)
nipkow@68617
   364
  qed
nipkow@68617
   365
qed
nipkow@68617
   366
nipkow@68617
   367
lemma AR_eq_absolute_extensor:
nipkow@68617
   368
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   369
  shows "AR S \<longleftrightarrow>
nipkow@68617
   370
       (\<forall>f :: 'a * real \<Rightarrow> 'a.
nipkow@68617
   371
        \<forall>U T. continuous_on T f \<longrightarrow> f ` T \<subseteq> S \<longrightarrow>
lp15@69922
   372
               closedin (top_of_set U) T \<longrightarrow>
nipkow@68617
   373
                (\<exists>g. continuous_on U g \<and> g ` U \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)))"
nipkow@68617
   374
apply (rule iffI)
nipkow@68617
   375
 apply (metis AR_imp_absolute_extensor)
nipkow@68617
   376
apply (simp add: absolute_extensor_imp_AR)
nipkow@68617
   377
done
nipkow@68617
   378
nipkow@68617
   379
lemma AR_imp_retract:
nipkow@68617
   380
  fixes S :: "'a::euclidean_space set"
lp15@69922
   381
  assumes "AR S \<and> closedin (top_of_set U) S"
nipkow@68617
   382
    shows "S retract_of U"
nipkow@68617
   383
using AR_imp_absolute_retract assms homeomorphic_refl by blast
nipkow@68617
   384
nipkow@68617
   385
lemma AR_homeomorphic_AR:
nipkow@68617
   386
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
nipkow@68617
   387
  assumes "AR T" "S homeomorphic T"
nipkow@68617
   388
    shows "AR S"
nipkow@68617
   389
unfolding AR_def
nipkow@68617
   390
by (metis assms AR_imp_absolute_retract homeomorphic_trans [of _ S] homeomorphic_sym)
nipkow@68617
   391
nipkow@68617
   392
lemma homeomorphic_AR_iff_AR:
nipkow@68617
   393
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
nipkow@68617
   394
  shows "S homeomorphic T \<Longrightarrow> AR S \<longleftrightarrow> AR T"
nipkow@68617
   395
by (metis AR_homeomorphic_AR homeomorphic_sym)
nipkow@68617
   396
nipkow@68617
   397
nipkow@68617
   398
lemma ANR_imp_absolute_neighbourhood_extensor:
nipkow@68617
   399
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
nipkow@68617
   400
  assumes "ANR S" and contf: "continuous_on T f" and "f ` T \<subseteq> S"
lp15@69922
   401
      and cloUT: "closedin (top_of_set U) T"
lp15@69922
   402
  obtains V g where "T \<subseteq> V" "openin (top_of_set U) V"
nipkow@68617
   403
                    "continuous_on V g"
nipkow@68617
   404
                    "g ` V \<subseteq> S" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
nipkow@68617
   405
proof -
nipkow@68617
   406
  have "aff_dim S < int (DIM('b \<times> real))"
nipkow@68617
   407
    using aff_dim_le_DIM [of S] by simp
nipkow@68617
   408
  then obtain C and S' :: "('b * real) set"
nipkow@68617
   409
          where C: "convex C" "C \<noteq> {}"
lp15@69922
   410
            and cloCS: "closedin (top_of_set C) S'"
nipkow@68617
   411
            and hom: "S homeomorphic S'"
nipkow@68617
   412
    by (metis that homeomorphic_closedin_convex)
lp15@69922
   413
  then obtain D where opD: "openin (top_of_set C) D" and "S' retract_of D"
nipkow@68617
   414
    using \<open>ANR S\<close> by (auto simp: ANR_def)
nipkow@68617
   415
  then obtain r where "S' \<subseteq> D" and contr: "continuous_on D r"
nipkow@68617
   416
                  and "r ` D \<subseteq> S'" and rid: "\<And>x. x \<in> S' \<Longrightarrow> r x = x"
nipkow@68617
   417
    by (auto simp: retraction_def retract_of_def)
nipkow@68617
   418
  obtain g h where homgh: "homeomorphism S S' g h"
nipkow@68617
   419
    using hom by (force simp: homeomorphic_def)
nipkow@68617
   420
  have "continuous_on (f ` T) g"
nipkow@68617
   421
    by (meson \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def homgh)
nipkow@68617
   422
  then have contgf: "continuous_on T (g \<circ> f)"
nipkow@68617
   423
    by (intro continuous_on_compose contf)
nipkow@68617
   424
  have gfTC: "(g \<circ> f) ` T \<subseteq> C"
nipkow@68617
   425
  proof -
nipkow@68617
   426
    have "g ` S = S'"
nipkow@68617
   427
      by (metis (no_types) homeomorphism_def homgh)
nipkow@68617
   428
    then show ?thesis
nipkow@68617
   429
      by (metis (no_types) assms(3) cloCS closedin_def image_comp image_mono order.trans topspace_euclidean_subtopology)
nipkow@68617
   430
  qed
nipkow@68617
   431
  obtain f' where contf': "continuous_on U f'"
nipkow@68617
   432
              and "f' ` U \<subseteq> C"
nipkow@68617
   433
              and eq: "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
nipkow@68617
   434
    by (metis Dugundji [OF C cloUT contgf gfTC])
nipkow@68617
   435
  show ?thesis
nipkow@68617
   436
  proof (rule_tac V = "U \<inter> f' -` D" and g = "h \<circ> r \<circ> f'" in that)
nipkow@68617
   437
    show "T \<subseteq> U \<inter> f' -` D"
nipkow@68617
   438
      using cloUT closedin_imp_subset \<open>S' \<subseteq> D\<close> \<open>f ` T \<subseteq> S\<close> eq homeomorphism_image1 homgh
nipkow@68617
   439
      by fastforce
lp15@69922
   440
    show ope: "openin (top_of_set U) (U \<inter> f' -` D)"
nipkow@68617
   441
      using  \<open>f' ` U \<subseteq> C\<close> by (auto simp: opD contf' continuous_openin_preimage)
nipkow@68617
   442
    have conth: "continuous_on (r ` f' ` (U \<inter> f' -` D)) h"
nipkow@68617
   443
      apply (rule continuous_on_subset [of S'])
nipkow@68617
   444
      using homeomorphism_def homgh apply blast
nipkow@68617
   445
      using \<open>r ` D \<subseteq> S'\<close> by blast
nipkow@68617
   446
    show "continuous_on (U \<inter> f' -` D) (h \<circ> r \<circ> f')"
nipkow@68617
   447
      apply (intro continuous_on_compose conth
nipkow@68617
   448
                   continuous_on_subset [OF contr] continuous_on_subset [OF contf'], auto)
nipkow@68617
   449
      done
nipkow@68617
   450
    show "(h \<circ> r \<circ> f') ` (U \<inter> f' -` D) \<subseteq> S"
nipkow@68617
   451
      using \<open>homeomorphism S S' g h\<close>  \<open>f' ` U \<subseteq> C\<close>  \<open>r ` D \<subseteq> S'\<close>
nipkow@68617
   452
      by (auto simp: homeomorphism_def)
nipkow@68617
   453
    show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
nipkow@68617
   454
      using \<open>homeomorphism S S' g h\<close> \<open>f ` T \<subseteq> S\<close> eq
nipkow@68617
   455
      by (auto simp: rid homeomorphism_def)
nipkow@68617
   456
  qed
nipkow@68617
   457
qed
nipkow@68617
   458
nipkow@68617
   459
nipkow@68617
   460
corollary ANR_imp_absolute_neighbourhood_retract:
nipkow@68617
   461
  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
nipkow@68617
   462
  assumes "ANR S" "S homeomorphic S'"
lp15@69922
   463
      and clo: "closedin (top_of_set U) S'"
lp15@69922
   464
  obtains V where "openin (top_of_set U) V" "S' retract_of V"
nipkow@68617
   465
proof -
nipkow@68617
   466
  obtain g h where hom: "homeomorphism S S' g h"
nipkow@68617
   467
    using assms by (force simp: homeomorphic_def)
nipkow@68617
   468
  have h: "continuous_on S' h" " h ` S' \<subseteq> S"
nipkow@68617
   469
    using hom homeomorphism_def apply blast
nipkow@68617
   470
    apply (metis hom equalityE homeomorphism_def)
nipkow@68617
   471
    done
nipkow@68617
   472
    from ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> h clo]
lp15@69922
   473
  obtain V h' where "S' \<subseteq> V" and opUV: "openin (top_of_set U) V"
nipkow@68617
   474
                and h': "continuous_on V h'" "h' ` V \<subseteq> S"
nipkow@68617
   475
                and h'h:"\<And>x. x \<in> S' \<Longrightarrow> h' x = h x"
nipkow@68617
   476
    by (blast intro: ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> h clo])
nipkow@68617
   477
  have "S' retract_of V"
nipkow@68617
   478
  proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>S' \<subseteq> V\<close>)
nipkow@68617
   479
    show "continuous_on V (g \<circ> h')"
nipkow@68617
   480
      apply (intro continuous_on_compose h')
nipkow@68617
   481
      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
nipkow@68617
   482
      done
nipkow@68617
   483
    show "(g \<circ> h') ` V \<subseteq> S'"
nipkow@68617
   484
      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
nipkow@68617
   485
    show "\<forall>x\<in>S'. (g \<circ> h') x = x"
nipkow@68617
   486
      by clarsimp (metis h'h hom homeomorphism_def)
nipkow@68617
   487
  qed
nipkow@68617
   488
  then show ?thesis
nipkow@68617
   489
    by (rule that [OF opUV])
nipkow@68617
   490
qed
nipkow@68617
   491
nipkow@68617
   492
corollary ANR_imp_absolute_neighbourhood_retract_UNIV:
nipkow@68617
   493
  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
nipkow@68617
   494
  assumes "ANR S" and hom: "S homeomorphic S'" and clo: "closed S'"
nipkow@68617
   495
  obtains V where "open V" "S' retract_of V"
nipkow@68617
   496
  using ANR_imp_absolute_neighbourhood_retract [OF \<open>ANR S\<close> hom]
nipkow@68617
   497
by (metis clo closed_closedin open_openin subtopology_UNIV)
nipkow@68617
   498
nipkow@68617
   499
corollary neighbourhood_extension_into_ANR:
nipkow@68617
   500
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
nipkow@68617
   501
  assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> T" and "ANR T" "closed S"
nipkow@68617
   502
  obtains V g where "S \<subseteq> V" "open V" "continuous_on V g"
nipkow@68617
   503
                    "g ` V \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
nipkow@68617
   504
  using ANR_imp_absolute_neighbourhood_extensor [OF  \<open>ANR T\<close> contf fim]
nipkow@68617
   505
  by (metis \<open>closed S\<close> closed_closedin open_openin subtopology_UNIV)
nipkow@68617
   506
nipkow@68617
   507
lemma absolute_neighbourhood_extensor_imp_ANR:
nipkow@68617
   508
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   509
  assumes "\<And>f :: 'a * real \<Rightarrow> 'a.
nipkow@68617
   510
           \<And>U T. \<lbrakk>continuous_on T f;  f ` T \<subseteq> S;
lp15@69922
   511
                  closedin (top_of_set U) T\<rbrakk>
lp15@69922
   512
                 \<Longrightarrow> \<exists>V g. T \<subseteq> V \<and> openin (top_of_set U) V \<and>
nipkow@68617
   513
                       continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)"
nipkow@68617
   514
  shows "ANR S"
nipkow@68617
   515
proof (clarsimp simp: ANR_def)
nipkow@68617
   516
  fix U and T :: "('a * real) set"
lp15@69922
   517
  assume "S homeomorphic T" and clo: "closedin (top_of_set U) T"
nipkow@68617
   518
  then obtain g h where hom: "homeomorphism S T g h"
nipkow@68617
   519
    by (force simp: homeomorphic_def)
nipkow@68617
   520
  have h: "continuous_on T h" " h ` T \<subseteq> S"
nipkow@68617
   521
    using hom homeomorphism_def apply blast
nipkow@68617
   522
    apply (metis hom equalityE homeomorphism_def)
nipkow@68617
   523
    done
lp15@69922
   524
  obtain V h' where "T \<subseteq> V" and opV: "openin (top_of_set U) V"
nipkow@68617
   525
                and h': "continuous_on V h'" "h' ` V \<subseteq> S"
nipkow@68617
   526
              and h'h: "\<forall>x\<in>T. h' x = h x"
nipkow@68617
   527
    using assms [OF h clo] by blast
nipkow@68617
   528
  have [simp]: "T \<subseteq> U"
nipkow@68617
   529
    using clo closedin_imp_subset by auto
nipkow@68617
   530
  have "T retract_of V"
nipkow@68617
   531
  proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>T \<subseteq> V\<close>)
nipkow@68617
   532
    show "continuous_on V (g \<circ> h')"
nipkow@68617
   533
      apply (intro continuous_on_compose h')
nipkow@68617
   534
      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
nipkow@68617
   535
      done
nipkow@68617
   536
    show "(g \<circ> h') ` V \<subseteq> T"
nipkow@68617
   537
      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
nipkow@68617
   538
    show "\<forall>x\<in>T. (g \<circ> h') x = x"
nipkow@68617
   539
      by clarsimp (metis h'h hom homeomorphism_def)
nipkow@68617
   540
  qed
lp15@69922
   541
  then show "\<exists>V. openin (top_of_set U) V \<and> T retract_of V"
nipkow@68617
   542
    using opV by blast
nipkow@68617
   543
qed
nipkow@68617
   544
nipkow@68617
   545
lemma ANR_eq_absolute_neighbourhood_extensor:
nipkow@68617
   546
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   547
  shows "ANR S \<longleftrightarrow>
nipkow@68617
   548
         (\<forall>f :: 'a * real \<Rightarrow> 'a.
nipkow@68617
   549
          \<forall>U T. continuous_on T f \<longrightarrow> f ` T \<subseteq> S \<longrightarrow>
lp15@69922
   550
                closedin (top_of_set U) T \<longrightarrow>
lp15@69922
   551
               (\<exists>V g. T \<subseteq> V \<and> openin (top_of_set U) V \<and>
nipkow@68617
   552
                       continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)))"
nipkow@68617
   553
apply (rule iffI)
nipkow@68617
   554
 apply (metis ANR_imp_absolute_neighbourhood_extensor)
nipkow@68617
   555
apply (simp add: absolute_neighbourhood_extensor_imp_ANR)
nipkow@68617
   556
done
nipkow@68617
   557
nipkow@68617
   558
lemma ANR_imp_neighbourhood_retract:
nipkow@68617
   559
  fixes S :: "'a::euclidean_space set"
lp15@69922
   560
  assumes "ANR S" "closedin (top_of_set U) S"
lp15@69922
   561
  obtains V where "openin (top_of_set U) V" "S retract_of V"
nipkow@68617
   562
using ANR_imp_absolute_neighbourhood_retract assms homeomorphic_refl by blast
nipkow@68617
   563
nipkow@68617
   564
lemma ANR_imp_absolute_closed_neighbourhood_retract:
nipkow@68617
   565
  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
lp15@69922
   566
  assumes "ANR S" "S homeomorphic S'" and US': "closedin (top_of_set U) S'"
nipkow@68617
   567
  obtains V W
lp15@69922
   568
    where "openin (top_of_set U) V"
lp15@69922
   569
          "closedin (top_of_set U) W"
nipkow@68617
   570
          "S' \<subseteq> V" "V \<subseteq> W" "S' retract_of W"
nipkow@68617
   571
proof -
lp15@69922
   572
  obtain Z where "openin (top_of_set U) Z" and S'Z: "S' retract_of Z"
nipkow@68617
   573
    by (blast intro: assms ANR_imp_absolute_neighbourhood_retract)
lp15@69922
   574
  then have UUZ: "closedin (top_of_set U) (U - Z)"
nipkow@68617
   575
    by auto
nipkow@68617
   576
  have "S' \<inter> (U - Z) = {}"
nipkow@68617
   577
    using \<open>S' retract_of Z\<close> closedin_retract closedin_subtopology by fastforce
nipkow@68617
   578
  then obtain V W
lp15@69922
   579
      where "openin (top_of_set U) V"
lp15@69922
   580
        and "openin (top_of_set U) W"
nipkow@68617
   581
        and "S' \<subseteq> V" "U - Z \<subseteq> W" "V \<inter> W = {}"
nipkow@68617
   582
      using separation_normal_local [OF US' UUZ]  by auto
nipkow@68617
   583
  moreover have "S' retract_of U - W"
nipkow@68617
   584
    apply (rule retract_of_subset [OF S'Z])
nipkow@68617
   585
    using US' \<open>S' \<subseteq> V\<close> \<open>V \<inter> W = {}\<close> closedin_subset apply fastforce
nipkow@68617
   586
    using Diff_subset_conv \<open>U - Z \<subseteq> W\<close> by blast
nipkow@68617
   587
  ultimately show ?thesis
nipkow@68617
   588
    apply (rule_tac V=V and W = "U-W" in that)
nipkow@68617
   589
    using openin_imp_subset apply force+
nipkow@68617
   590
    done
nipkow@68617
   591
qed
nipkow@68617
   592
nipkow@68617
   593
lemma ANR_imp_closed_neighbourhood_retract:
nipkow@68617
   594
  fixes S :: "'a::euclidean_space set"
lp15@69922
   595
  assumes "ANR S" "closedin (top_of_set U) S"
lp15@69922
   596
  obtains V W where "openin (top_of_set U) V"
lp15@69922
   597
                    "closedin (top_of_set U) W"
nipkow@68617
   598
                    "S \<subseteq> V" "V \<subseteq> W" "S retract_of W"
nipkow@68617
   599
by (meson ANR_imp_absolute_closed_neighbourhood_retract assms homeomorphic_refl)
nipkow@68617
   600
nipkow@68617
   601
lemma ANR_homeomorphic_ANR:
nipkow@68617
   602
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
nipkow@68617
   603
  assumes "ANR T" "S homeomorphic T"
nipkow@68617
   604
    shows "ANR S"
nipkow@68617
   605
unfolding ANR_def
nipkow@68617
   606
by (metis assms ANR_imp_absolute_neighbourhood_retract homeomorphic_trans [of _ S] homeomorphic_sym)
nipkow@68617
   607
nipkow@68617
   608
lemma homeomorphic_ANR_iff_ANR:
nipkow@68617
   609
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
nipkow@68617
   610
  shows "S homeomorphic T \<Longrightarrow> ANR S \<longleftrightarrow> ANR T"
nipkow@68617
   611
by (metis ANR_homeomorphic_ANR homeomorphic_sym)
nipkow@68617
   612
nipkow@68617
   613
subsubsection \<open>Analogous properties of ENRs\<close>
nipkow@68617
   614
nipkow@68617
   615
lemma ENR_imp_absolute_neighbourhood_retract:
nipkow@68617
   616
  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
nipkow@68617
   617
  assumes "ENR S" and hom: "S homeomorphic S'"
nipkow@68617
   618
      and "S' \<subseteq> U"
lp15@69922
   619
  obtains V where "openin (top_of_set U) V" "S' retract_of V"
nipkow@68617
   620
proof -
nipkow@68617
   621
  obtain X where "open X" "S retract_of X"
nipkow@68617
   622
    using \<open>ENR S\<close> by (auto simp: ENR_def)
nipkow@68617
   623
  then obtain r where "retraction X S r"
nipkow@68617
   624
    by (auto simp: retract_of_def)
nipkow@68617
   625
  have "locally compact S'"
nipkow@68617
   626
    using retract_of_locally_compact open_imp_locally_compact
nipkow@68617
   627
          homeomorphic_local_compactness \<open>S retract_of X\<close> \<open>open X\<close> hom by blast
lp15@69922
   628
  then obtain W where UW: "openin (top_of_set U) W"
lp15@69922
   629
                  and WS': "closedin (top_of_set W) S'"
nipkow@68617
   630
    apply (rule locally_compact_closedin_open)
nipkow@68617
   631
    apply (rename_tac W)
nipkow@68617
   632
    apply (rule_tac W = "U \<inter> W" in that, blast)
nipkow@68617
   633
    by (simp add: \<open>S' \<subseteq> U\<close> closedin_limpt)
nipkow@68617
   634
  obtain f g where hom: "homeomorphism S S' f g"
nipkow@68617
   635
    using assms by (force simp: homeomorphic_def)
nipkow@68617
   636
  have contg: "continuous_on S' g"
nipkow@68617
   637
    using hom homeomorphism_def by blast
nipkow@68617
   638
  moreover have "g ` S' \<subseteq> S" by (metis hom equalityE homeomorphism_def)
nipkow@68617
   639
  ultimately obtain h where conth: "continuous_on W h" and hg: "\<And>x. x \<in> S' \<Longrightarrow> h x = g x"
nipkow@68617
   640
    using Tietze_unbounded [of S' g W] WS' by blast
nipkow@68617
   641
  have "W \<subseteq> U" using UW openin_open by auto
nipkow@68617
   642
  have "S' \<subseteq> W" using WS' closedin_closed by auto
nipkow@68617
   643
  have him: "\<And>x. x \<in> S' \<Longrightarrow> h x \<in> X"
nipkow@68617
   644
    by (metis (no_types) \<open>S retract_of X\<close> hg hom homeomorphism_def image_insert insert_absorb insert_iff retract_of_imp_subset subset_eq)
nipkow@68617
   645
  have "S' retract_of (W \<inter> h -` X)"
nipkow@68617
   646
  proof (simp add: retraction_def retract_of_def, intro exI conjI)
nipkow@68617
   647
    show "S' \<subseteq> W" "S' \<subseteq> h -` X"
nipkow@68617
   648
      using him WS' closedin_imp_subset by blast+
nipkow@68617
   649
    show "continuous_on (W \<inter> h -` X) (f \<circ> r \<circ> h)"
nipkow@68617
   650
    proof (intro continuous_on_compose)
nipkow@68617
   651
      show "continuous_on (W \<inter> h -` X) h"
nipkow@68617
   652
        by (meson conth continuous_on_subset inf_le1)
nipkow@68617
   653
      show "continuous_on (h ` (W \<inter> h -` X)) r"
nipkow@68617
   654
      proof -
nipkow@68617
   655
        have "h ` (W \<inter> h -` X) \<subseteq> X"
nipkow@68617
   656
          by blast
nipkow@68617
   657
        then show "continuous_on (h ` (W \<inter> h -` X)) r"
nipkow@68617
   658
          by (meson \<open>retraction X S r\<close> continuous_on_subset retraction)
nipkow@68617
   659
      qed
nipkow@68617
   660
      show "continuous_on (r ` h ` (W \<inter> h -` X)) f"
nipkow@68617
   661
        apply (rule continuous_on_subset [of S])
nipkow@68617
   662
         using hom homeomorphism_def apply blast
nipkow@68617
   663
        apply clarify
nipkow@68617
   664
        apply (meson \<open>retraction X S r\<close> subsetD imageI retraction_def)
nipkow@68617
   665
        done
nipkow@68617
   666
    qed
nipkow@68617
   667
    show "(f \<circ> r \<circ> h) ` (W \<inter> h -` X) \<subseteq> S'"
nipkow@68617
   668
      using \<open>retraction X S r\<close> hom
nipkow@68617
   669
      by (auto simp: retraction_def homeomorphism_def)
nipkow@68617
   670
    show "\<forall>x\<in>S'. (f \<circ> r \<circ> h) x = x"
nipkow@68617
   671
      using \<open>retraction X S r\<close> hom by (auto simp: retraction_def homeomorphism_def hg)
nipkow@68617
   672
  qed
nipkow@68617
   673
  then show ?thesis
nipkow@68617
   674
    apply (rule_tac V = "W \<inter> h -` X" in that)
nipkow@68617
   675
     apply (rule openin_trans [OF _ UW])
nipkow@68617
   676
     using \<open>continuous_on W h\<close> \<open>open X\<close> continuous_openin_preimage_eq apply blast+
nipkow@68617
   677
     done
nipkow@68617
   678
qed
nipkow@68617
   679
nipkow@68617
   680
corollary ENR_imp_absolute_neighbourhood_retract_UNIV:
nipkow@68617
   681
  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
nipkow@68617
   682
  assumes "ENR S" "S homeomorphic S'"
nipkow@68617
   683
  obtains T' where "open T'" "S' retract_of T'"
nipkow@68617
   684
by (metis ENR_imp_absolute_neighbourhood_retract UNIV_I assms(1) assms(2) open_openin subsetI subtopology_UNIV)
nipkow@68617
   685
nipkow@68617
   686
lemma ENR_homeomorphic_ENR:
nipkow@68617
   687
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
nipkow@68617
   688
  assumes "ENR T" "S homeomorphic T"
nipkow@68617
   689
    shows "ENR S"
nipkow@68617
   690
unfolding ENR_def
nipkow@68617
   691
by (meson ENR_imp_absolute_neighbourhood_retract_UNIV assms homeomorphic_sym)
nipkow@68617
   692
nipkow@68617
   693
lemma homeomorphic_ENR_iff_ENR:
nipkow@68617
   694
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
nipkow@68617
   695
  assumes "S homeomorphic T"
nipkow@68617
   696
    shows "ENR S \<longleftrightarrow> ENR T"
nipkow@68617
   697
by (meson ENR_homeomorphic_ENR assms homeomorphic_sym)
nipkow@68617
   698
nipkow@68617
   699
lemma ENR_translation:
nipkow@68617
   700
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   701
  shows "ENR(image (\<lambda>x. a + x) S) \<longleftrightarrow> ENR S"
nipkow@68617
   702
by (meson homeomorphic_sym homeomorphic_translation homeomorphic_ENR_iff_ENR)
nipkow@68617
   703
nipkow@68617
   704
lemma ENR_linear_image_eq:
nipkow@68617
   705
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
nipkow@68617
   706
  assumes "linear f" "inj f"
nipkow@68617
   707
  shows "ENR (image f S) \<longleftrightarrow> ENR S"
nipkow@68617
   708
apply (rule homeomorphic_ENR_iff_ENR)
nipkow@68617
   709
using assms homeomorphic_sym linear_homeomorphic_image by auto
nipkow@68617
   710
nipkow@68617
   711
text \<open>Some relations among the concepts. We also relate AR to being a retract of UNIV, which is
nipkow@68617
   712
often a more convenient proxy in the closed case.\<close>
nipkow@68617
   713
nipkow@68617
   714
lemma AR_imp_ANR: "AR S \<Longrightarrow> ANR S"
nipkow@68617
   715
  using ANR_def AR_def by fastforce
nipkow@68617
   716
nipkow@68617
   717
lemma ENR_imp_ANR:
nipkow@68617
   718
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   719
  shows "ENR S \<Longrightarrow> ANR S"
nipkow@68617
   720
apply (simp add: ANR_def)
nipkow@68617
   721
by (metis ENR_imp_absolute_neighbourhood_retract closedin_imp_subset)
nipkow@68617
   722
nipkow@68617
   723
lemma ENR_ANR:
nipkow@68617
   724
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   725
  shows "ENR S \<longleftrightarrow> ANR S \<and> locally compact S"
nipkow@68617
   726
proof
nipkow@68617
   727
  assume "ENR S"
nipkow@68617
   728
  then have "locally compact S"
nipkow@68617
   729
    using ENR_def open_imp_locally_compact retract_of_locally_compact by auto
nipkow@68617
   730
  then show "ANR S \<and> locally compact S"
nipkow@68617
   731
    using ENR_imp_ANR \<open>ENR S\<close> by blast
nipkow@68617
   732
next
nipkow@68617
   733
  assume "ANR S \<and> locally compact S"
nipkow@68617
   734
  then have "ANR S" "locally compact S" by auto
nipkow@68617
   735
  then obtain T :: "('a * real) set" where "closed T" "S homeomorphic T"
nipkow@68617
   736
    using locally_compact_homeomorphic_closed
nipkow@68617
   737
    by (metis DIM_prod DIM_real Suc_eq_plus1 lessI)
nipkow@68617
   738
  then show "ENR S"
nipkow@68617
   739
    using \<open>ANR S\<close>
nipkow@68617
   740
    apply (simp add: ANR_def)
nipkow@68617
   741
    apply (drule_tac x=UNIV in spec)
nipkow@68617
   742
    apply (drule_tac x=T in spec, clarsimp)
nipkow@68617
   743
    apply (meson ENR_def ENR_homeomorphic_ENR open_openin)
nipkow@68617
   744
    done
nipkow@68617
   745
qed
nipkow@68617
   746
nipkow@68617
   747
nipkow@68617
   748
lemma AR_ANR:
nipkow@68617
   749
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   750
  shows "AR S \<longleftrightarrow> ANR S \<and> contractible S \<and> S \<noteq> {}"
nipkow@68617
   751
        (is "?lhs = ?rhs")
nipkow@68617
   752
proof
nipkow@68617
   753
  assume ?lhs
nipkow@68617
   754
  obtain C and S' :: "('a * real) set"
lp15@69922
   755
    where "convex C" "C \<noteq> {}" "closedin (top_of_set C) S'" "S homeomorphic S'"
nipkow@68617
   756
      apply (rule homeomorphic_closedin_convex [of S, where 'n = "'a * real"])
nipkow@68617
   757
      using aff_dim_le_DIM [of S] by auto
nipkow@68617
   758
  with \<open>AR S\<close> have "contractible S"
nipkow@68617
   759
    apply (simp add: AR_def)
nipkow@68617
   760
    apply (drule_tac x=C in spec)
nipkow@68617
   761
    apply (drule_tac x="S'" in spec, simp)
nipkow@68617
   762
    using convex_imp_contractible homeomorphic_contractible_eq retract_of_contractible by fastforce
nipkow@68617
   763
  with \<open>AR S\<close> show ?rhs
nipkow@68617
   764
    apply (auto simp: AR_imp_ANR)
nipkow@68617
   765
    apply (force simp: AR_def)
nipkow@68617
   766
    done
nipkow@68617
   767
next
nipkow@68617
   768
  assume ?rhs
nipkow@68617
   769
  then obtain a and h:: "real \<times> 'a \<Rightarrow> 'a"
nipkow@68617
   770
      where conth: "continuous_on ({0..1} \<times> S) h"
nipkow@68617
   771
        and hS: "h ` ({0..1} \<times> S) \<subseteq> S"
nipkow@68617
   772
        and [simp]: "\<And>x. h(0, x) = x"
nipkow@68617
   773
        and [simp]: "\<And>x. h(1, x) = a"
nipkow@68617
   774
        and "ANR S" "S \<noteq> {}"
nipkow@68617
   775
    by (auto simp: contractible_def homotopic_with_def)
nipkow@68617
   776
  then have "a \<in> S"
nipkow@68617
   777
    by (metis all_not_in_conv atLeastAtMost_iff image_subset_iff mem_Sigma_iff order_refl zero_le_one)
nipkow@68617
   778
  have "\<exists>g. continuous_on W g \<and> g ` W \<subseteq> S \<and> (\<forall>x\<in>T. g x = f x)"
nipkow@68617
   779
         if      f: "continuous_on T f" "f ` T \<subseteq> S"
lp15@69922
   780
            and WT: "closedin (top_of_set W) T"
nipkow@68617
   781
         for W T and f :: "'a \<times> real \<Rightarrow> 'a"
nipkow@68617
   782
  proof -
nipkow@68617
   783
    obtain U g
lp15@69922
   784
      where "T \<subseteq> U" and WU: "openin (top_of_set W) U"
nipkow@68617
   785
        and contg: "continuous_on U g"
nipkow@68617
   786
        and "g ` U \<subseteq> S" and gf: "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
nipkow@68617
   787
      using iffD1 [OF ANR_eq_absolute_neighbourhood_extensor \<open>ANR S\<close>, rule_format, OF f WT]
nipkow@68617
   788
      by auto
lp15@69922
   789
    have WWU: "closedin (top_of_set W) (W - U)"
nipkow@68617
   790
      using WU closedin_diff by fastforce
nipkow@68617
   791
    moreover have "(W - U) \<inter> T = {}"
nipkow@68617
   792
      using \<open>T \<subseteq> U\<close> by auto
nipkow@68617
   793
    ultimately obtain V V'
lp15@69922
   794
      where WV': "openin (top_of_set W) V'"
lp15@69922
   795
        and WV: "openin (top_of_set W) V"
nipkow@68617
   796
        and "W - U \<subseteq> V'" "T \<subseteq> V" "V' \<inter> V = {}"
nipkow@68617
   797
      using separation_normal_local [of W "W-U" T] WT by blast
nipkow@68617
   798
    then have WVT: "T \<inter> (W - V) = {}"
nipkow@68617
   799
      by auto
lp15@69922
   800
    have WWV: "closedin (top_of_set W) (W - V)"
nipkow@68617
   801
      using WV closedin_diff by fastforce
nipkow@68617
   802
    obtain j :: " 'a \<times> real \<Rightarrow> real"
nipkow@68617
   803
      where contj: "continuous_on W j"
nipkow@68617
   804
        and j:  "\<And>x. x \<in> W \<Longrightarrow> j x \<in> {0..1}"
nipkow@68617
   805
        and j0: "\<And>x. x \<in> W - V \<Longrightarrow> j x = 1"
nipkow@68617
   806
        and j1: "\<And>x. x \<in> T \<Longrightarrow> j x = 0"
nipkow@68617
   807
      by (rule Urysohn_local [OF WT WWV WVT, of 0 "1::real"]) (auto simp: in_segment)
nipkow@68617
   808
    have Weq: "W = (W - V) \<union> (W - V')"
nipkow@68617
   809
      using \<open>V' \<inter> V = {}\<close> by force
nipkow@68617
   810
    show ?thesis
nipkow@68617
   811
    proof (intro conjI exI)
nipkow@68617
   812
      have *: "continuous_on (W - V') (\<lambda>x. h (j x, g x))"
nipkow@68617
   813
        apply (rule continuous_on_compose2 [OF conth continuous_on_Pair])
nipkow@68617
   814
          apply (rule continuous_on_subset [OF contj Diff_subset])
nipkow@68617
   815
         apply (rule continuous_on_subset [OF contg])
nipkow@68617
   816
         apply (metis Diff_subset_conv Un_commute \<open>W - U \<subseteq> V'\<close>)
nipkow@68617
   817
        using j \<open>g ` U \<subseteq> S\<close> \<open>W - U \<subseteq> V'\<close> apply fastforce
nipkow@68617
   818
        done
nipkow@68617
   819
      show "continuous_on W (\<lambda>x. if x \<in> W - V then a else h (j x, g x))"
nipkow@68617
   820
        apply (subst Weq)
nipkow@68617
   821
        apply (rule continuous_on_cases_local)
nipkow@68617
   822
            apply (simp_all add: Weq [symmetric] WWV continuous_on_const *)
nipkow@68617
   823
          using WV' closedin_diff apply fastforce
nipkow@68617
   824
         apply (auto simp: j0 j1)
nipkow@68617
   825
        done
nipkow@68617
   826
    next
nipkow@68617
   827
      have "h (j (x, y), g (x, y)) \<in> S" if "(x, y) \<in> W" "(x, y) \<in> V" for x y
nipkow@68617
   828
      proof -
nipkow@68617
   829
        have "j(x, y) \<in> {0..1}"
nipkow@68617
   830
          using j that by blast
nipkow@68617
   831
        moreover have "g(x, y) \<in> S"
nipkow@68617
   832
          using \<open>V' \<inter> V = {}\<close> \<open>W - U \<subseteq> V'\<close> \<open>g ` U \<subseteq> S\<close> that by fastforce
nipkow@68617
   833
        ultimately show ?thesis
nipkow@68617
   834
          using hS by blast
nipkow@68617
   835
      qed
nipkow@68617
   836
      with \<open>a \<in> S\<close> \<open>g ` U \<subseteq> S\<close>
nipkow@68617
   837
      show "(\<lambda>x. if x \<in> W - V then a else h (j x, g x)) ` W \<subseteq> S"
nipkow@68617
   838
        by auto
nipkow@68617
   839
    next
nipkow@68617
   840
      show "\<forall>x\<in>T. (if x \<in> W - V then a else h (j x, g x)) = f x"
nipkow@68617
   841
        using \<open>T \<subseteq> V\<close> by (auto simp: j0 j1 gf)
nipkow@68617
   842
    qed
nipkow@68617
   843
  qed
nipkow@68617
   844
  then show ?lhs
nipkow@68617
   845
    by (simp add: AR_eq_absolute_extensor)
nipkow@68617
   846
qed
nipkow@68617
   847
nipkow@68617
   848
nipkow@68617
   849
lemma ANR_retract_of_ANR:
nipkow@68617
   850
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   851
  assumes "ANR T" "S retract_of T"
nipkow@68617
   852
  shows "ANR S"
nipkow@68617
   853
using assms
nipkow@68617
   854
apply (simp add: ANR_eq_absolute_neighbourhood_extensor retract_of_def retraction_def)
nipkow@68617
   855
apply (clarsimp elim!: all_forward)
nipkow@68617
   856
apply (erule impCE, metis subset_trans)
nipkow@68617
   857
apply (clarsimp elim!: ex_forward)
nipkow@68617
   858
apply (rule_tac x="r \<circ> g" in exI)
nipkow@68617
   859
by (metis comp_apply continuous_on_compose continuous_on_subset subsetD imageI image_comp image_mono subset_trans)
nipkow@68617
   860
nipkow@68617
   861
lemma AR_retract_of_AR:
nipkow@68617
   862
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   863
  shows "\<lbrakk>AR T; S retract_of T\<rbrakk> \<Longrightarrow> AR S"
nipkow@68617
   864
using ANR_retract_of_ANR AR_ANR retract_of_contractible by fastforce
nipkow@68617
   865
nipkow@68617
   866
lemma ENR_retract_of_ENR:
nipkow@68617
   867
   "\<lbrakk>ENR T; S retract_of T\<rbrakk> \<Longrightarrow> ENR S"
nipkow@68617
   868
by (meson ENR_def retract_of_trans)
nipkow@68617
   869
nipkow@68617
   870
lemma retract_of_UNIV:
nipkow@68617
   871
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   872
  shows "S retract_of UNIV \<longleftrightarrow> AR S \<and> closed S"
nipkow@68617
   873
by (metis AR_ANR AR_imp_retract ENR_def ENR_imp_ANR closed_UNIV closed_closedin contractible_UNIV empty_not_UNIV open_UNIV retract_of_closed retract_of_contractible retract_of_empty(1) subtopology_UNIV)
nipkow@68617
   874
nipkow@68617
   875
lemma compact_AR:
nipkow@68617
   876
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   877
  shows "compact S \<and> AR S \<longleftrightarrow> compact S \<and> S retract_of UNIV"
nipkow@68617
   878
using compact_imp_closed retract_of_UNIV by blast
nipkow@68617
   879
nipkow@68617
   880
text \<open>More properties of ARs, ANRs and ENRs\<close>
nipkow@68617
   881
nipkow@69508
   882
lemma not_AR_empty [simp]: "\<not> AR({})"
nipkow@68617
   883
  by (auto simp: AR_def)
nipkow@68617
   884
nipkow@68617
   885
lemma ENR_empty [simp]: "ENR {}"
nipkow@68617
   886
  by (simp add: ENR_def)
nipkow@68617
   887
nipkow@68617
   888
lemma ANR_empty [simp]: "ANR ({} :: 'a::euclidean_space set)"
nipkow@68617
   889
  by (simp add: ENR_imp_ANR)
nipkow@68617
   890
nipkow@68617
   891
lemma convex_imp_AR:
nipkow@68617
   892
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   893
  shows "\<lbrakk>convex S; S \<noteq> {}\<rbrakk> \<Longrightarrow> AR S"
nipkow@68617
   894
apply (rule absolute_extensor_imp_AR)
nipkow@68617
   895
apply (rule Dugundji, assumption+)
nipkow@68617
   896
by blast
nipkow@68617
   897
nipkow@68617
   898
lemma convex_imp_ANR:
nipkow@68617
   899
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   900
  shows "convex S \<Longrightarrow> ANR S"
nipkow@68617
   901
using ANR_empty AR_imp_ANR convex_imp_AR by blast
nipkow@68617
   902
nipkow@68617
   903
lemma ENR_convex_closed:
nipkow@68617
   904
  fixes S :: "'a::euclidean_space set"
nipkow@68617
   905
  shows "\<lbrakk>closed S; convex S\<rbrakk> \<Longrightarrow> ENR S"
nipkow@68617
   906
using ENR_def ENR_empty convex_imp_AR retract_of_UNIV by blast
nipkow@68617
   907
nipkow@68617
   908
lemma AR_UNIV [simp]: "AR (UNIV :: 'a::euclidean_space set)"
nipkow@68617
   909
  using retract_of_UNIV by auto
nipkow@68617
   910
nipkow@68617
   911
lemma ANR_UNIV [simp]: "ANR (UNIV :: 'a::euclidean_space set)"
nipkow@68617
   912
  by (simp add: AR_imp_ANR)
nipkow@68617
   913
nipkow@68617
   914
lemma ENR_UNIV [simp]:"ENR UNIV"
nipkow@68617
   915
  using ENR_def by blast
nipkow@68617
   916
nipkow@68617
   917
lemma AR_singleton:
nipkow@68617
   918
    fixes a :: "'a::euclidean_space"
nipkow@68617
   919
    shows "AR {a}"
nipkow@68617
   920
  using retract_of_UNIV by blast
nipkow@68617
   921
nipkow@68617
   922
lemma ANR_singleton:
nipkow@68617
   923
    fixes a :: "'a::euclidean_space"
nipkow@68617
   924
    shows "ANR {a}"
nipkow@68617
   925
  by (simp add: AR_imp_ANR AR_singleton)
nipkow@68617
   926
nipkow@68617
   927
lemma ENR_singleton: "ENR {a}"
nipkow@68617
   928
  using ENR_def by blast
nipkow@68617
   929
nipkow@68617
   930
text \<open>ARs closed under union\<close>
nipkow@68617
   931
nipkow@68617
   932
lemma AR_closed_Un_local_aux:
nipkow@68617
   933
  fixes U :: "'a::euclidean_space set"
lp15@69922
   934
  assumes "closedin (top_of_set U) S"
lp15@69922
   935
          "closedin (top_of_set U) T"
nipkow@68617
   936
          "AR S" "AR T" "AR(S \<inter> T)"
nipkow@68617
   937
  shows "(S \<union> T) retract_of U"
nipkow@68617
   938
proof -
nipkow@68617
   939
  have "S \<inter> T \<noteq> {}"
nipkow@68617
   940
    using assms AR_def by fastforce
nipkow@68617
   941
  have "S \<subseteq> U" "T \<subseteq> U"
nipkow@68617
   942
    using assms by (auto simp: closedin_imp_subset)
nipkow@68617
   943
  define S' where "S' \<equiv> {x \<in> U. setdist {x} S \<le> setdist {x} T}"
nipkow@68617
   944
  define T' where "T' \<equiv> {x \<in> U. setdist {x} T \<le> setdist {x} S}"
nipkow@68617
   945
  define W  where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
lp15@69922
   946
  have US': "closedin (top_of_set U) S'"
nipkow@68617
   947
    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
nipkow@68617
   948
    by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
lp15@69922
   949
  have UT': "closedin (top_of_set U) T'"
nipkow@68617
   950
    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
nipkow@68617
   951
    by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
nipkow@68617
   952
  have "S \<subseteq> S'"
nipkow@68617
   953
    using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
nipkow@68617
   954
  have "T \<subseteq> T'"
nipkow@68617
   955
    using T'_def \<open>T \<subseteq> U\<close> setdist_sing_in_set by fastforce
nipkow@68617
   956
  have "S \<inter> T \<subseteq> W" "W \<subseteq> U"
nipkow@68617
   957
    using \<open>S \<subseteq> U\<close> by (auto simp: W_def setdist_sing_in_set)
nipkow@68617
   958
  have "(S \<inter> T) retract_of W"
nipkow@68617
   959
    apply (rule AR_imp_absolute_retract [OF \<open>AR(S \<inter> T)\<close>])
nipkow@68617
   960
     apply (simp add: homeomorphic_refl)
nipkow@68617
   961
    apply (rule closedin_subset_trans [of U])
nipkow@68617
   962
    apply (simp_all add: assms closedin_Int \<open>S \<inter> T \<subseteq> W\<close> \<open>W \<subseteq> U\<close>)
nipkow@68617
   963
    done
nipkow@68617
   964
  then obtain r0
nipkow@68617
   965
    where "S \<inter> T \<subseteq> W" and contr0: "continuous_on W r0"
nipkow@68617
   966
      and "r0 ` W \<subseteq> S \<inter> T"
nipkow@68617
   967
      and r0 [simp]: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> r0 x = x"
nipkow@68617
   968
      by (auto simp: retract_of_def retraction_def)
nipkow@68617
   969
  have ST: "x \<in> W \<Longrightarrow> x \<in> S \<longleftrightarrow> x \<in> T" for x
nipkow@68617
   970
    using setdist_eq_0_closedin \<open>S \<inter> T \<noteq> {}\<close> assms
nipkow@68617
   971
    by (force simp: W_def setdist_sing_in_set)
nipkow@68617
   972
  have "S' \<inter> T' = W"
nipkow@68617
   973
    by (auto simp: S'_def T'_def W_def)
lp15@69922
   974
  then have cloUW: "closedin (top_of_set U) W"
nipkow@68617
   975
    using closedin_Int US' UT' by blast
nipkow@68617
   976
  define r where "r \<equiv> \<lambda>x. if x \<in> W then r0 x else x"
nipkow@68617
   977
  have "r ` (W \<union> S) \<subseteq> S" "r ` (W \<union> T) \<subseteq> T"
nipkow@68617
   978
    using \<open>r0 ` W \<subseteq> S \<inter> T\<close> r_def by auto
nipkow@68617
   979
  have contr: "continuous_on (W \<union> (S \<union> T)) r"
nipkow@68617
   980
  unfolding r_def
nipkow@68617
   981
  proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id])
lp15@69922
   982
    show "closedin (top_of_set (W \<union> (S \<union> T))) W"
lp15@69922
   983
      using \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> \<open>W \<subseteq> U\<close> \<open>closedin (top_of_set U) W\<close> closedin_subset_trans by fastforce
lp15@69922
   984
    show "closedin (top_of_set (W \<union> (S \<union> T))) (S \<union> T)"
nipkow@68617
   985
      by (meson \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> \<open>W \<subseteq> U\<close> assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2)
nipkow@68617
   986
    show "\<And>x. x \<in> W \<and> x \<notin> W \<or> x \<in> S \<union> T \<and> x \<in> W \<Longrightarrow> r0 x = x"
nipkow@68617
   987
      by (auto simp: ST)
nipkow@68617
   988
  qed
lp15@69922
   989
  have cloUWS: "closedin (top_of_set U) (W \<union> S)"
nipkow@68617
   990
    by (simp add: cloUW assms closedin_Un)
nipkow@68617
   991
  obtain g where contg: "continuous_on U g"
nipkow@68617
   992
             and "g ` U \<subseteq> S" and geqr: "\<And>x. x \<in> W \<union> S \<Longrightarrow> g x = r x"
nipkow@68617
   993
    apply (rule AR_imp_absolute_extensor [OF \<open>AR S\<close> _ _ cloUWS])
nipkow@68617
   994
      apply (rule continuous_on_subset [OF contr])
nipkow@68617
   995
      using \<open>r ` (W \<union> S) \<subseteq> S\<close> apply auto
nipkow@68617
   996
    done
lp15@69922
   997
  have cloUWT: "closedin (top_of_set U) (W \<union> T)"
nipkow@68617
   998
    by (simp add: cloUW assms closedin_Un)
nipkow@68617
   999
  obtain h where conth: "continuous_on U h"
nipkow@68617
  1000
             and "h ` U \<subseteq> T" and heqr: "\<And>x. x \<in> W \<union> T \<Longrightarrow> h x = r x"
nipkow@68617
  1001
    apply (rule AR_imp_absolute_extensor [OF \<open>AR T\<close> _ _ cloUWT])
nipkow@68617
  1002
      apply (rule continuous_on_subset [OF contr])
nipkow@68617
  1003
      using \<open>r ` (W \<union> T) \<subseteq> T\<close> apply auto
nipkow@68617
  1004
    done
nipkow@68617
  1005
  have "U = S' \<union> T'"
nipkow@68617
  1006
    by (force simp: S'_def T'_def)
nipkow@68617
  1007
  then have cont: "continuous_on U (\<lambda>x. if x \<in> S' then g x else h x)"
nipkow@68617
  1008
    apply (rule ssubst)
nipkow@68617
  1009
    apply (rule continuous_on_cases_local)
nipkow@68617
  1010
    using US' UT' \<open>S' \<inter> T' = W\<close> \<open>U = S' \<union> T'\<close>
nipkow@68617
  1011
          contg conth continuous_on_subset geqr heqr apply auto
nipkow@68617
  1012
    done
nipkow@68617
  1013
  have UST: "(\<lambda>x. if x \<in> S' then g x else h x) ` U \<subseteq> S \<union> T"
nipkow@68617
  1014
    using \<open>g ` U \<subseteq> S\<close> \<open>h ` U \<subseteq> T\<close> by auto
nipkow@68617
  1015
  show ?thesis
nipkow@68617
  1016
    apply (simp add: retract_of_def retraction_def \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close>)
nipkow@68617
  1017
    apply (rule_tac x="\<lambda>x. if x \<in> S' then g x else h x" in exI)
nipkow@68617
  1018
    apply (intro conjI cont UST)
nipkow@68617
  1019
    by (metis IntI ST Un_iff \<open>S \<subseteq> S'\<close> \<open>S' \<inter> T' = W\<close> \<open>T \<subseteq> T'\<close> subsetD geqr heqr r0 r_def)
nipkow@68617
  1020
qed
nipkow@68617
  1021
nipkow@68617
  1022
nipkow@68617
  1023
lemma AR_closed_Un_local:
nipkow@68617
  1024
  fixes S :: "'a::euclidean_space set"
lp15@69922
  1025
  assumes STS: "closedin (top_of_set (S \<union> T)) S"
lp15@69922
  1026
      and STT: "closedin (top_of_set (S \<union> T)) T"
nipkow@68617
  1027
      and "AR S" "AR T" "AR(S \<inter> T)"
nipkow@68617
  1028
    shows "AR(S \<union> T)"
nipkow@68617
  1029
proof -
nipkow@68617
  1030
  have "C retract_of U"
lp15@69922
  1031
       if hom: "S \<union> T homeomorphic C" and UC: "closedin (top_of_set U) C"
nipkow@68617
  1032
       for U and C :: "('a * real) set"
nipkow@68617
  1033
  proof -
nipkow@68617
  1034
    obtain f g where hom: "homeomorphism (S \<union> T) C f g"
nipkow@68617
  1035
      using hom by (force simp: homeomorphic_def)
lp15@69922
  1036
    have US: "closedin (top_of_set U) (C \<inter> g -` S)"
nipkow@68617
  1037
      apply (rule closedin_trans [OF _ UC])
nipkow@68617
  1038
      apply (rule continuous_closedin_preimage_gen [OF _ _ STS])
nipkow@68617
  1039
      using hom homeomorphism_def apply blast
nipkow@68617
  1040
      apply (metis hom homeomorphism_def set_eq_subset)
nipkow@68617
  1041
      done
lp15@69922
  1042
    have UT: "closedin (top_of_set U) (C \<inter> g -` T)"
nipkow@68617
  1043
      apply (rule closedin_trans [OF _ UC])
nipkow@68617
  1044
      apply (rule continuous_closedin_preimage_gen [OF _ _ STT])
nipkow@68617
  1045
      using hom homeomorphism_def apply blast
nipkow@68617
  1046
      apply (metis hom homeomorphism_def set_eq_subset)
nipkow@68617
  1047
      done
nipkow@68617
  1048
    have ARS: "AR (C \<inter> g -` S)"
nipkow@68617
  1049
      apply (rule AR_homeomorphic_AR [OF \<open>AR S\<close>])
nipkow@68617
  1050
      apply (simp add: homeomorphic_def)
nipkow@68617
  1051
      apply (rule_tac x=g in exI)
nipkow@68617
  1052
      apply (rule_tac x=f in exI)
nipkow@68617
  1053
      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
nipkow@68617
  1054
      apply (rule_tac x="f x" in image_eqI, auto)
nipkow@68617
  1055
      done
nipkow@68617
  1056
    have ART: "AR (C \<inter> g -` T)"
nipkow@68617
  1057
      apply (rule AR_homeomorphic_AR [OF \<open>AR T\<close>])
nipkow@68617
  1058
      apply (simp add: homeomorphic_def)
nipkow@68617
  1059
      apply (rule_tac x=g in exI)
nipkow@68617
  1060
      apply (rule_tac x=f in exI)
nipkow@68617
  1061
      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
nipkow@68617
  1062
      apply (rule_tac x="f x" in image_eqI, auto)
nipkow@68617
  1063
      done
nipkow@68617
  1064
    have ARI: "AR ((C \<inter> g -` S) \<inter> (C \<inter> g -` T))"
nipkow@68617
  1065
      apply (rule AR_homeomorphic_AR [OF \<open>AR (S \<inter> T)\<close>])
nipkow@68617
  1066
      apply (simp add: homeomorphic_def)
nipkow@68617
  1067
      apply (rule_tac x=g in exI)
nipkow@68617
  1068
      apply (rule_tac x=f in exI)
nipkow@68617
  1069
      using hom
nipkow@68617
  1070
      apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
nipkow@68617
  1071
      apply (rule_tac x="f x" in image_eqI, auto)
nipkow@68617
  1072
      done
nipkow@68617
  1073
    have "C = (C \<inter> g -` S) \<union> (C \<inter> g -` T)"
nipkow@68617
  1074
      using hom  by (auto simp: homeomorphism_def)
nipkow@68617
  1075
    then show ?thesis
nipkow@68617
  1076
      by (metis AR_closed_Un_local_aux [OF US UT ARS ART ARI])
nipkow@68617
  1077
  qed
nipkow@68617
  1078
  then show ?thesis
nipkow@68617
  1079
    by (force simp: AR_def)
nipkow@68617
  1080
qed
nipkow@68617
  1081
nipkow@68617
  1082
corollary AR_closed_Un:
nipkow@68617
  1083
  fixes S :: "'a::euclidean_space set"
nipkow@68617
  1084
  shows "\<lbrakk>closed S; closed T; AR S; AR T; AR (S \<inter> T)\<rbrakk> \<Longrightarrow> AR (S \<union> T)"
nipkow@68617
  1085
by (metis AR_closed_Un_local_aux closed_closedin retract_of_UNIV subtopology_UNIV)
nipkow@68617
  1086
nipkow@68617
  1087
text \<open>ANRs closed under union\<close>
nipkow@68617
  1088
nipkow@68617
  1089
lemma ANR_closed_Un_local_aux:
nipkow@68617
  1090
  fixes U :: "'a::euclidean_space set"
lp15@69922
  1091
  assumes US: "closedin (top_of_set U) S"
lp15@69922
  1092
      and UT: "closedin (top_of_set U) T"
nipkow@68617
  1093
      and "ANR S" "ANR T" "ANR(S \<inter> T)"
lp15@69922
  1094
  obtains V where "openin (top_of_set U) V" "(S \<union> T) retract_of V"
nipkow@68617
  1095
proof (cases "S = {} \<or> T = {}")
nipkow@68617
  1096
  case True with assms that show ?thesis
nipkow@68617
  1097
    by (metis ANR_imp_neighbourhood_retract Un_commute inf_bot_right sup_inf_absorb)
nipkow@68617
  1098
next
nipkow@68617
  1099
  case False
nipkow@68617
  1100
  then have [simp]: "S \<noteq> {}" "T \<noteq> {}" by auto
nipkow@68617
  1101
  have "S \<subseteq> U" "T \<subseteq> U"
nipkow@68617
  1102
    using assms by (auto simp: closedin_imp_subset)
nipkow@68617
  1103
  define S' where "S' \<equiv> {x \<in> U. setdist {x} S \<le> setdist {x} T}"
nipkow@68617
  1104
  define T' where "T' \<equiv> {x \<in> U. setdist {x} T \<le> setdist {x} S}"
nipkow@68617
  1105
  define W  where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
lp15@69922
  1106
  have cloUS': "closedin (top_of_set U) S'"
nipkow@68617
  1107
    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
nipkow@68617
  1108
    by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
lp15@69922
  1109
  have cloUT': "closedin (top_of_set U) T'"
nipkow@68617
  1110
    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
nipkow@68617
  1111
    by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
nipkow@68617
  1112
  have "S \<subseteq> S'"
nipkow@68617
  1113
    using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
nipkow@68617
  1114
  have "T \<subseteq> T'"
nipkow@68617
  1115
    using T'_def \<open>T \<subseteq> U\<close> setdist_sing_in_set by fastforce
nipkow@68617
  1116
  have "S' \<union> T' = U"
nipkow@68617
  1117
    by (auto simp: S'_def T'_def)
nipkow@68617
  1118
  have "W \<subseteq> S'"
nipkow@68617
  1119
    by (simp add: Collect_mono S'_def W_def)
nipkow@68617
  1120
  have "W \<subseteq> T'"
nipkow@68617
  1121
    by (simp add: Collect_mono T'_def W_def)
nipkow@68617
  1122
  have ST_W: "S \<inter> T \<subseteq> W" and "W \<subseteq> U"
nipkow@68617
  1123
    using \<open>S \<subseteq> U\<close> by (force simp: W_def setdist_sing_in_set)+
nipkow@68617
  1124
  have "S' \<inter> T' = W"
nipkow@68617
  1125
    by (auto simp: S'_def T'_def W_def)
lp15@69922
  1126
  then have cloUW: "closedin (top_of_set U) W"
nipkow@68617
  1127
    using closedin_Int cloUS' cloUT' by blast
lp15@69922
  1128
  obtain W' W0 where "openin (top_of_set W) W'"
lp15@69922
  1129
                 and cloWW0: "closedin (top_of_set W) W0"
nipkow@68617
  1130
                 and "S \<inter> T \<subseteq> W'" "W' \<subseteq> W0"
nipkow@68617
  1131
                 and ret: "(S \<inter> T) retract_of W0"
nipkow@68617
  1132
    apply (rule ANR_imp_closed_neighbourhood_retract [OF \<open>ANR(S \<inter> T)\<close>])
nipkow@68617
  1133
    apply (rule closedin_subset_trans [of U, OF _ ST_W \<open>W \<subseteq> U\<close>])
nipkow@68617
  1134
    apply (blast intro: assms)+
nipkow@68617
  1135
    done
lp15@69922
  1136
  then obtain U0 where opeUU0: "openin (top_of_set U) U0"
nipkow@68617
  1137
                   and U0: "S \<inter> T \<subseteq> U0" "U0 \<inter> W \<subseteq> W0"
nipkow@68617
  1138
    unfolding openin_open  using \<open>W \<subseteq> U\<close> by blast
nipkow@68617
  1139
  have "W0 \<subseteq> U"
nipkow@68617
  1140
    using \<open>W \<subseteq> U\<close> cloWW0 closedin_subset by fastforce
nipkow@68617
  1141
  obtain r0
nipkow@68617
  1142
    where "S \<inter> T \<subseteq> W0" and contr0: "continuous_on W0 r0" and "r0 ` W0 \<subseteq> S \<inter> T"
nipkow@68617
  1143
      and r0 [simp]: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> r0 x = x"
nipkow@68617
  1144
    using ret  by (force simp: retract_of_def retraction_def)
nipkow@68617
  1145
  have ST: "x \<in> W \<Longrightarrow> x \<in> S \<longleftrightarrow> x \<in> T" for x
nipkow@68617
  1146
    using assms by (auto simp: W_def setdist_sing_in_set dest!: setdist_eq_0_closedin)
nipkow@68617
  1147
  define r where "r \<equiv> \<lambda>x. if x \<in> W0 then r0 x else x"
nipkow@68617
  1148
  have "r ` (W0 \<union> S) \<subseteq> S" "r ` (W0 \<union> T) \<subseteq> T"
nipkow@68617
  1149
    using \<open>r0 ` W0 \<subseteq> S \<inter> T\<close> r_def by auto
nipkow@68617
  1150
  have contr: "continuous_on (W0 \<union> (S \<union> T)) r"
nipkow@68617
  1151
  unfolding r_def
nipkow@68617
  1152
  proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id])
lp15@69922
  1153
    show "closedin (top_of_set (W0 \<union> (S \<union> T))) W0"
nipkow@68617
  1154
      apply (rule closedin_subset_trans [of U])
nipkow@68617
  1155
      using cloWW0 cloUW closedin_trans \<open>W0 \<subseteq> U\<close> \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> apply blast+
nipkow@68617
  1156
      done
lp15@69922
  1157
    show "closedin (top_of_set (W0 \<union> (S \<union> T))) (S \<union> T)"
nipkow@68617
  1158
      by (meson \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> \<open>W0 \<subseteq> U\<close> assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2)
nipkow@68617
  1159
    show "\<And>x. x \<in> W0 \<and> x \<notin> W0 \<or> x \<in> S \<union> T \<and> x \<in> W0 \<Longrightarrow> r0 x = x"
nipkow@68617
  1160
      using ST cloWW0 closedin_subset by fastforce
nipkow@68617
  1161
  qed
lp15@69922
  1162
  have cloS'WS: "closedin (top_of_set S') (W0 \<union> S)"
nipkow@68617
  1163
    by (meson closedin_subset_trans US cloUS' \<open>S \<subseteq> S'\<close> \<open>W \<subseteq> S'\<close> cloUW cloWW0 
nipkow@68617
  1164
              closedin_Un closedin_imp_subset closedin_trans)
nipkow@68617
  1165
  obtain W1 g where "W0 \<union> S \<subseteq> W1" and contg: "continuous_on W1 g"
lp15@69922
  1166
                and opeSW1: "openin (top_of_set S') W1"
nipkow@68617
  1167
                and "g ` W1 \<subseteq> S" and geqr: "\<And>x. x \<in> W0 \<union> S \<Longrightarrow> g x = r x"
nipkow@68617
  1168
    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> _ \<open>r ` (W0 \<union> S) \<subseteq> S\<close> cloS'WS])
nipkow@68617
  1169
     apply (rule continuous_on_subset [OF contr], blast+)
nipkow@68617
  1170
    done
lp15@69922
  1171
  have cloT'WT: "closedin (top_of_set T') (W0 \<union> T)"
nipkow@68617
  1172
    by (meson closedin_subset_trans UT cloUT' \<open>T \<subseteq> T'\<close> \<open>W \<subseteq> T'\<close> cloUW cloWW0 
nipkow@68617
  1173
              closedin_Un closedin_imp_subset closedin_trans)
nipkow@68617
  1174
  obtain W2 h where "W0 \<union> T \<subseteq> W2" and conth: "continuous_on W2 h"
lp15@69922
  1175
                and opeSW2: "openin (top_of_set T') W2"
nipkow@68617
  1176
                and "h ` W2 \<subseteq> T" and heqr: "\<And>x. x \<in> W0 \<union> T \<Longrightarrow> h x = r x"
nipkow@68617
  1177
    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> _ \<open>r ` (W0 \<union> T) \<subseteq> T\<close> cloT'WT])
nipkow@68617
  1178
     apply (rule continuous_on_subset [OF contr], blast+)
nipkow@68617
  1179
    done
nipkow@68617
  1180
  have "S' \<inter> T' = W"
nipkow@68617
  1181
    by (force simp: S'_def T'_def W_def)
nipkow@68617
  1182
  obtain O1 O2 where "open O1" "W1 = S' \<inter> O1" "open O2" "W2 = T' \<inter> O2"
nipkow@68617
  1183
    using opeSW1 opeSW2 by (force simp: openin_open)
nipkow@68617
  1184
  show ?thesis
nipkow@68617
  1185
  proof
nipkow@68617
  1186
    have eq: "W1 - (W - U0) \<union> (W2 - (W - U0)) =
nipkow@68617
  1187
         ((U - T') \<inter> O1 \<union> (U - S') \<inter> O2 \<union> U \<inter> O1 \<inter> O2) - (W - U0)"
nipkow@68617
  1188
     using \<open>U0 \<inter> W \<subseteq> W0\<close> \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W0 \<union> T \<subseteq> W2\<close>
nipkow@68617
  1189
      by (auto simp: \<open>S' \<union> T' = U\<close> [symmetric] \<open>S' \<inter> T' = W\<close> [symmetric] \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close>)
lp15@69922
  1190
    show "openin (top_of_set U) (W1 - (W - U0) \<union> (W2 - (W - U0)))"
nipkow@68617
  1191
      apply (subst eq)
nipkow@68617
  1192
      apply (intro openin_Un openin_Int_open openin_diff closedin_diff cloUW opeUU0 cloUS' cloUT' \<open>open O1\<close> \<open>open O2\<close>, simp_all)
nipkow@68617
  1193
      done
lp15@69922
  1194
    have cloW1: "closedin (top_of_set (W1 - (W - U0) \<union> (W2 - (W - U0)))) (W1 - (W - U0))"
nipkow@68617
  1195
      using cloUS' apply (simp add: closedin_closed)
nipkow@68617
  1196
      apply (erule ex_forward)
nipkow@68617
  1197
      using U0 \<open>W0 \<union> S \<subseteq> W1\<close>
nipkow@68617
  1198
      apply (auto simp: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
nipkow@68617
  1199
      done
lp15@69922
  1200
    have cloW2: "closedin (top_of_set (W1 - (W - U0) \<union> (W2 - (W - U0)))) (W2 - (W - U0))"
nipkow@68617
  1201
      using cloUT' apply (simp add: closedin_closed)
nipkow@68617
  1202
      apply (erule ex_forward)
nipkow@68617
  1203
      using U0 \<open>W0 \<union> T \<subseteq> W2\<close>
nipkow@68617
  1204
      apply (auto simp: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
nipkow@68617
  1205
      done
nipkow@68617
  1206
    have *: "\<forall>x\<in>S \<union> T. (if x \<in> S' then g x else h x) = x"
nipkow@68617
  1207
      using ST \<open>S' \<inter> T' = W\<close> cloT'WT closedin_subset geqr heqr 
nipkow@68617
  1208
      apply (auto simp: r_def, fastforce)
nipkow@68617
  1209
      using \<open>S \<subseteq> S'\<close> \<open>T \<subseteq> T'\<close> \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W1 = S' \<inter> O1\<close>  by auto
nipkow@68617
  1210
    have "\<exists>r. continuous_on (W1 - (W - U0) \<union> (W2 - (W - U0))) r \<and>
nipkow@68617
  1211
              r ` (W1 - (W - U0) \<union> (W2 - (W - U0))) \<subseteq> S \<union> T \<and> 
nipkow@68617
  1212
              (\<forall>x\<in>S \<union> T. r x = x)"
nipkow@68617
  1213
      apply (rule_tac x = "\<lambda>x. if  x \<in> S' then g x else h x" in exI)
nipkow@68617
  1214
      apply (intro conjI *)
nipkow@68617
  1215
      apply (rule continuous_on_cases_local 
nipkow@68617
  1216
                  [OF cloW1 cloW2 continuous_on_subset [OF contg] continuous_on_subset [OF conth]])
nipkow@68617
  1217
      using \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<inter> T' = W\<close>
nipkow@68617
  1218
            \<open>g ` W1 \<subseteq> S\<close> \<open>h ` W2 \<subseteq> T\<close> apply auto
nipkow@68617
  1219
      using \<open>U0 \<inter> W \<subseteq> W0\<close> \<open>W0 \<union> S \<subseteq> W1\<close> apply (fastforce simp add: geqr heqr)+
nipkow@68617
  1220
      done
nipkow@68617
  1221
    then show "S \<union> T retract_of W1 - (W - U0) \<union> (W2 - (W - U0))"
nipkow@68617
  1222
      using  \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W0 \<union> T \<subseteq> W2\<close> ST opeUU0 U0
nipkow@68617
  1223
      by (auto simp: retract_of_def retraction_def)
nipkow@68617
  1224
  qed
nipkow@68617
  1225
qed
nipkow@68617
  1226
nipkow@68617
  1227
nipkow@68617
  1228
lemma ANR_closed_Un_local:
nipkow@68617
  1229
  fixes S :: "'a::euclidean_space set"
lp15@69922
  1230
  assumes STS: "closedin (top_of_set (S \<union> T)) S"
lp15@69922
  1231
      and STT: "closedin (top_of_set (S \<union> T)) T"
nipkow@68617
  1232
      and "ANR S" "ANR T" "ANR(S \<inter> T)" 
nipkow@68617
  1233
    shows "ANR(S \<union> T)"
nipkow@68617
  1234
proof -
lp15@69922
  1235
  have "\<exists>T. openin (top_of_set U) T \<and> C retract_of T"
lp15@69922
  1236
       if hom: "S \<union> T homeomorphic C" and UC: "closedin (top_of_set U) C"
nipkow@68617
  1237
       for U and C :: "('a * real) set"
nipkow@68617
  1238
  proof -
nipkow@68617
  1239
    obtain f g where hom: "homeomorphism (S \<union> T) C f g"
nipkow@68617
  1240
      using hom by (force simp: homeomorphic_def)
lp15@69922
  1241
    have US: "closedin (top_of_set U) (C \<inter> g -` S)"
nipkow@68617
  1242
      apply (rule closedin_trans [OF _ UC])
nipkow@68617
  1243
      apply (rule continuous_closedin_preimage_gen [OF _ _ STS])
nipkow@68617
  1244
      using hom [unfolded homeomorphism_def] apply blast
nipkow@68617
  1245
      apply (metis hom homeomorphism_def set_eq_subset)
nipkow@68617
  1246
      done
lp15@69922
  1247
    have UT: "closedin (top_of_set U) (C \<inter> g -` T)"
nipkow@68617
  1248
      apply (rule closedin_trans [OF _ UC])
nipkow@68617
  1249
      apply (rule continuous_closedin_preimage_gen [OF _ _ STT])
nipkow@68617
  1250
      using hom [unfolded homeomorphism_def] apply blast
nipkow@68617
  1251
      apply (metis hom homeomorphism_def set_eq_subset)
nipkow@68617
  1252
      done
nipkow@68617
  1253
    have ANRS: "ANR (C \<inter> g -` S)"
nipkow@68617
  1254
      apply (rule ANR_homeomorphic_ANR [OF \<open>ANR S\<close>])
nipkow@68617
  1255
      apply (simp add: homeomorphic_def)
nipkow@68617
  1256
      apply (rule_tac x=g in exI)
nipkow@68617
  1257
      apply (rule_tac x=f in exI)
nipkow@68617
  1258
      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
nipkow@68617
  1259
      apply (rule_tac x="f x" in image_eqI, auto)
nipkow@68617
  1260
      done
nipkow@68617
  1261
    have ANRT: "ANR (C \<inter> g -` T)"
nipkow@68617
  1262
      apply (rule ANR_homeomorphic_ANR [OF \<open>ANR T\<close>])
nipkow@68617
  1263
      apply (simp add: homeomorphic_def)
nipkow@68617
  1264
      apply (rule_tac x=g in exI)
nipkow@68617
  1265
      apply (rule_tac x=f in exI)
nipkow@68617
  1266
      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
nipkow@68617
  1267
      apply (rule_tac x="f x" in image_eqI, auto)
nipkow@68617
  1268
      done
nipkow@68617
  1269
    have ANRI: "ANR ((C \<inter> g -` S) \<inter> (C \<inter> g -` T))"
nipkow@68617
  1270
      apply (rule ANR_homeomorphic_ANR [OF \<open>ANR (S \<inter> T)\<close>])
nipkow@68617
  1271
      apply (simp add: homeomorphic_def)
nipkow@68617
  1272
      apply (rule_tac x=g in exI)
nipkow@68617
  1273
      apply (rule_tac x=f in exI)
nipkow@68617
  1274
      using hom
nipkow@68617
  1275
      apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
nipkow@68617
  1276
      apply (rule_tac x="f x" in image_eqI, auto)
nipkow@68617
  1277
      done
nipkow@68617
  1278
    have "C = (C \<inter> g -` S) \<union> (C \<inter> g -` T)"
nipkow@68617
  1279
      using hom by (auto simp: homeomorphism_def)
nipkow@68617
  1280
    then show ?thesis
nipkow@68617
  1281
      by (metis ANR_closed_Un_local_aux [OF US UT ANRS ANRT ANRI])
nipkow@68617
  1282
  qed
nipkow@68617
  1283
  then show ?thesis
nipkow@68617
  1284
    by (auto simp: ANR_def)
nipkow@68617
  1285
qed    
nipkow@68617
  1286
nipkow@68617
  1287
corollary ANR_closed_Un:
nipkow@68617
  1288
  fixes S :: "'a::euclidean_space set"
nipkow@68617
  1289
  shows "\<lbrakk>closed S; closed T; ANR S; ANR T; ANR (S \<inter> T)\<rbrakk> \<Longrightarrow> ANR (S \<union> T)"
nipkow@68617
  1290
by (simp add: ANR_closed_Un_local closedin_def diff_eq open_Compl openin_open_Int)
nipkow@68617
  1291
nipkow@68617
  1292
lemma ANR_openin:
nipkow@68617
  1293
  fixes S :: "'a::euclidean_space set"
lp15@69922
  1294
  assumes "ANR T" and opeTS: "openin (top_of_set T) S"
nipkow@68617
  1295
  shows "ANR S"
nipkow@68617
  1296
proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor)
nipkow@68617
  1297
  fix f :: "'a \<times> real \<Rightarrow> 'a" and U C
nipkow@68617
  1298
  assume contf: "continuous_on C f" and fim: "f ` C \<subseteq> S"
lp15@69922
  1299
     and cloUC: "closedin (top_of_set U) C"
nipkow@68617
  1300
  have "f ` C \<subseteq> T"
nipkow@68617
  1301
    using fim opeTS openin_imp_subset by blast
nipkow@68617
  1302
  obtain W g where "C \<subseteq> W"
lp15@69922
  1303
               and UW: "openin (top_of_set U) W"
nipkow@68617
  1304
               and contg: "continuous_on W g"
nipkow@68617
  1305
               and gim: "g ` W \<subseteq> T"
nipkow@68617
  1306
               and geq: "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
nipkow@68617
  1307
    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf \<open>f ` C \<subseteq> T\<close> cloUC])
nipkow@68617
  1308
    using fim by auto
lp15@69922
  1309
  show "\<exists>V g. C \<subseteq> V \<and> openin (top_of_set U) V \<and> continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x\<in>C. g x = f x)"
nipkow@68617
  1310
  proof (intro exI conjI)
nipkow@68617
  1311
    show "C \<subseteq> W \<inter> g -` S"
nipkow@68617
  1312
      using \<open>C \<subseteq> W\<close> fim geq by blast
lp15@69922
  1313
    show "openin (top_of_set U) (W \<inter> g -` S)"
nipkow@68617
  1314
      by (metis (mono_tags, lifting) UW contg continuous_openin_preimage gim opeTS openin_trans)
nipkow@68617
  1315
    show "continuous_on (W \<inter> g -` S) g"
nipkow@68617
  1316
      by (blast intro: continuous_on_subset [OF contg])
nipkow@68617
  1317
    show "g ` (W \<inter> g -` S) \<subseteq> S"
nipkow@68617
  1318
      using gim by blast
nipkow@68617
  1319
    show "\<forall>x\<in>C. g x = f x"
nipkow@68617
  1320
      using geq by blast
nipkow@68617
  1321
  qed
nipkow@68617
  1322
qed
nipkow@68617
  1323
nipkow@68617
  1324
lemma ENR_openin:
nipkow@68617
  1325
    fixes S :: "'a::euclidean_space set"
lp15@69922
  1326
    assumes "ENR T" and opeTS: "openin (top_of_set T) S"
nipkow@68617
  1327
    shows "ENR S"
nipkow@68617
  1328
  using assms apply (simp add: ENR_ANR)
nipkow@68617
  1329
  using ANR_openin locally_open_subset by blast
nipkow@68617
  1330
nipkow@68617
  1331
lemma ANR_neighborhood_retract:
nipkow@68617
  1332
    fixes S :: "'a::euclidean_space set"
lp15@69922
  1333
    assumes "ANR U" "S retract_of T" "openin (top_of_set U) T"
nipkow@68617
  1334
    shows "ANR S"
nipkow@68617
  1335
  using ANR_openin ANR_retract_of_ANR assms by blast
nipkow@68617
  1336
nipkow@68617
  1337
lemma ENR_neighborhood_retract:
nipkow@68617
  1338
    fixes S :: "'a::euclidean_space set"
lp15@69922
  1339
    assumes "ENR U" "S retract_of T" "openin (top_of_set U) T"
nipkow@68617
  1340
    shows "ENR S"
nipkow@68617
  1341
  using ENR_openin ENR_retract_of_ENR assms by blast
nipkow@68617
  1342
nipkow@68617
  1343
lemma ANR_rel_interior:
nipkow@68617
  1344
  fixes S :: "'a::euclidean_space set"
nipkow@68617
  1345
  shows "ANR S \<Longrightarrow> ANR(rel_interior S)"
nipkow@68617
  1346
   by (blast intro: ANR_openin openin_set_rel_interior)
nipkow@68617
  1347
nipkow@68617
  1348
lemma ANR_delete:
nipkow@68617
  1349
  fixes S :: "'a::euclidean_space set"
nipkow@68617
  1350
  shows "ANR S \<Longrightarrow> ANR(S - {a})"
nipkow@68617
  1351
   by (blast intro: ANR_openin openin_delete openin_subtopology_self)
nipkow@68617
  1352
nipkow@68617
  1353
lemma ENR_rel_interior:
nipkow@68617
  1354
  fixes S :: "'a::euclidean_space set"
nipkow@68617
  1355
  shows "ENR S \<Longrightarrow> ENR(rel_interior S)"
nipkow@68617
  1356
   by (blast intro: ENR_openin openin_set_rel_interior)
nipkow@68617
  1357
nipkow@68617
  1358
lemma ENR_delete:
nipkow@68617
  1359
  fixes S :: "'a::euclidean_space set"
nipkow@68617
  1360
  shows "ENR S \<Longrightarrow> ENR(S - {a})"
nipkow@68617
  1361
   by (blast intro: ENR_openin openin_delete openin_subtopology_self)
nipkow@68617
  1362
nipkow@68617
  1363
lemma open_imp_ENR: "open S \<Longrightarrow> ENR S"
nipkow@68617
  1364
    using ENR_def by blast
nipkow@68617
  1365
nipkow@68617
  1366
lemma open_imp_ANR:
nipkow@68617
  1367
    fixes S :: "'a::euclidean_space set"
nipkow@68617
  1368
    shows "open S \<Longrightarrow> ANR S"
nipkow@68617
  1369
  by (simp add: ENR_imp_ANR open_imp_ENR)
nipkow@68617
  1370
nipkow@68617
  1371
lemma ANR_ball [iff]:
nipkow@68617
  1372
    fixes a :: "'a::euclidean_space"
nipkow@68617
  1373
    shows "ANR(ball a r)"
nipkow@68617
  1374
  by (simp add: convex_imp_ANR)
nipkow@68617
  1375
nipkow@68617
  1376
lemma ENR_ball [iff]: "ENR(ball a r)"
nipkow@68617
  1377
  by (simp add: open_imp_ENR)
nipkow@68617
  1378
nipkow@68617
  1379
lemma AR_ball [simp]:
nipkow@68617
  1380
    fixes a :: "'a::euclidean_space"
nipkow@68617
  1381
    shows "AR(ball a r) \<longleftrightarrow> 0 < r"
nipkow@68617
  1382
  by (auto simp: AR_ANR convex_imp_contractible)
nipkow@68617
  1383
nipkow@68617
  1384
lemma ANR_cball [iff]:
nipkow@68617
  1385
    fixes a :: "'a::euclidean_space"
nipkow@68617
  1386
    shows "ANR(cball a r)"
nipkow@68617
  1387
  by (simp add: convex_imp_ANR)
nipkow@68617
  1388
nipkow@68617
  1389
lemma ENR_cball:
nipkow@68617
  1390
    fixes a :: "'a::euclidean_space"
nipkow@68617
  1391
    shows "ENR(cball a r)"
nipkow@68617
  1392
  using ENR_convex_closed by blast
nipkow@68617
  1393
nipkow@68617
  1394
lemma AR_cball [simp]:
nipkow@68617
  1395
    fixes a :: "'a::euclidean_space"
nipkow@68617
  1396
    shows "AR(cball a r) \<longleftrightarrow> 0 \<le> r"
nipkow@68617
  1397
  by (auto simp: AR_ANR convex_imp_contractible)
nipkow@68617
  1398
nipkow@68617
  1399
lemma ANR_box [iff]:
nipkow@68617
  1400
    fixes a :: "'a::euclidean_space"
nipkow@68617
  1401
    shows "ANR(cbox a b)" "ANR(box a b)"
nipkow@68617
  1402
  by (auto simp: convex_imp_ANR open_imp_ANR)
nipkow@68617
  1403
nipkow@68617
  1404
lemma ENR_box [iff]:
nipkow@68617
  1405
    fixes a :: "'a::euclidean_space"
nipkow@68617
  1406
    shows "ENR(cbox a b)" "ENR(box a b)"
nipkow@68617
  1407
apply (simp add: ENR_convex_closed closed_cbox)
nipkow@68617
  1408
by (simp add: open_box open_imp_ENR)
nipkow@68617
  1409
nipkow@68617
  1410
lemma AR_box [simp]:
nipkow@68617
  1411
    "AR(cbox a b) \<longleftrightarrow> cbox a b \<noteq> {}" "AR(box a b) \<longleftrightarrow> box a b \<noteq> {}"
nipkow@68617
  1412
  by (auto simp: AR_ANR convex_imp_contractible)
nipkow@68617
  1413
nipkow@68617
  1414
lemma ANR_interior:
nipkow@68617
  1415
     fixes S :: "'a::euclidean_space set"
nipkow@68617
  1416
     shows "ANR(interior S)"
nipkow@68617
  1417
  by (simp add: open_imp_ANR)
nipkow@68617
  1418
nipkow@68617
  1419
lemma ENR_interior:
nipkow@68617
  1420
     fixes S :: "'a::euclidean_space set"
nipkow@68617
  1421
     shows "ENR(interior S)"
nipkow@68617
  1422
  by (simp add: open_imp_ENR)
nipkow@68617
  1423
nipkow@68617
  1424
lemma AR_imp_contractible:
nipkow@68617
  1425
    fixes S :: "'a::euclidean_space set"
nipkow@68617
  1426
    shows "AR S \<Longrightarrow> contractible S"
nipkow@68617
  1427
  by (simp add: AR_ANR)
nipkow@68617
  1428
nipkow@68617
  1429
lemma ENR_imp_locally_compact:
nipkow@68617
  1430
    fixes S :: "'a::euclidean_space set"
nipkow@68617
  1431
    shows "ENR S \<Longrightarrow> locally compact S"
nipkow@68617
  1432
  by (simp add: ENR_ANR)
nipkow@68617
  1433
nipkow@68617
  1434
lemma ANR_imp_locally_path_connected:
nipkow@68617
  1435
  fixes S :: "'a::euclidean_space set"
nipkow@68617
  1436
  assumes "ANR S"
nipkow@68617
  1437
    shows "locally path_connected S"
nipkow@68617
  1438
proof -
nipkow@68617
  1439
  obtain U and T :: "('a \<times> real) set"
nipkow@68617
  1440
     where "convex U" "U \<noteq> {}"
lp15@69922
  1441
       and UT: "closedin (top_of_set U) T"
nipkow@68617
  1442
       and "S homeomorphic T"
nipkow@68617
  1443
    apply (rule homeomorphic_closedin_convex [of S])
nipkow@68617
  1444
    using aff_dim_le_DIM [of S] apply auto
nipkow@68617
  1445
    done
nipkow@68617
  1446
  then have "locally path_connected T"
nipkow@68617
  1447
    by (meson ANR_imp_absolute_neighbourhood_retract
nipkow@68617
  1448
        assms convex_imp_locally_path_connected locally_open_subset retract_of_locally_path_connected)
nipkow@68617
  1449
  then have S: "locally path_connected S"
lp15@69922
  1450
      if "openin (top_of_set U) V" "T retract_of V" "U \<noteq> {}" for V
nipkow@68617
  1451
    using \<open>S homeomorphic T\<close> homeomorphic_locally homeomorphic_path_connectedness by blast
nipkow@68617
  1452
  show ?thesis
nipkow@68617
  1453
    using assms
nipkow@68617
  1454
    apply (clarsimp simp: ANR_def)
nipkow@68617
  1455
    apply (drule_tac x=U in spec)
nipkow@68617
  1456
    apply (drule_tac x=T in spec)
nipkow@68617
  1457
    using \<open>S homeomorphic T\<close> \<open>U \<noteq> {}\<close> UT  apply (blast intro: S)
nipkow@68617
  1458
    done
nipkow@68617
  1459
qed
nipkow@68617
  1460
nipkow@68617
  1461
lemma ANR_imp_locally_connected:
nipkow@68617
  1462
  fixes S :: "'a::euclidean_space set"
nipkow@68617
  1463
  assumes "ANR S"
nipkow@68617
  1464
    shows "locally connected S"
nipkow@68617
  1465
using locally_path_connected_imp_locally_connected ANR_imp_locally_path_connected assms by auto
nipkow@68617
  1466
nipkow@68617
  1467
lemma AR_imp_locally_path_connected:
nipkow@68617
  1468
  fixes S :: "'a::euclidean_space set"
nipkow@68617
  1469
  assumes "AR S"
nipkow@68617
  1470
    shows "locally path_connected S"
nipkow@68617
  1471
by (simp add: ANR_imp_locally_path_connected AR_imp_ANR assms)
nipkow@68617
  1472
nipkow@68617
  1473
lemma AR_imp_locally_connected:
nipkow@68617
  1474
  fixes S :: "'a::euclidean_space set"
nipkow@68617
  1475
  assumes "AR S"
nipkow@68617
  1476
    shows "locally connected S"
nipkow@68617
  1477
using ANR_imp_locally_connected AR_ANR assms by blast
nipkow@68617
  1478
nipkow@68617
  1479
lemma ENR_imp_locally_path_connected:
nipkow@68617
  1480
  fixes S :: "'a::euclidean_space set"
nipkow@68617
  1481
  assumes "ENR S"
nipkow@68617
  1482
    shows "locally path_connected S"
nipkow@68617
  1483
by (simp add: ANR_imp_locally_path_connected ENR_imp_ANR assms)
nipkow@68617
  1484
nipkow@68617
  1485
lemma ENR_imp_locally_connected:
nipkow@68617
  1486
  fixes S :: "'a::euclidean_space set"
nipkow@68617
  1487
  assumes "ENR S"
nipkow@68617
  1488
    shows "locally connected S"
nipkow@68617
  1489
using ANR_imp_locally_connected ENR_ANR assms by blast
nipkow@68617
  1490
nipkow@68617
  1491
lemma ANR_Times:
nipkow@68617
  1492
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
nipkow@68617
  1493
  assumes "ANR S" "ANR T" shows "ANR(S \<times> T)"
nipkow@68617
  1494
proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor)
nipkow@68617
  1495
  fix f :: " ('a \<times> 'b) \<times> real \<Rightarrow> 'a \<times> 'b" and U C
nipkow@68617
  1496
  assume "continuous_on C f" and fim: "f ` C \<subseteq> S \<times> T"
lp15@69922
  1497
     and cloUC: "closedin (top_of_set U) C"
nipkow@68617
  1498
  have contf1: "continuous_on C (fst \<circ> f)"
nipkow@68617
  1499
    by (simp add: \<open>continuous_on C f\<close> continuous_on_fst)
nipkow@68617
  1500
  obtain W1 g where "C \<subseteq> W1"
lp15@69922
  1501
               and UW1: "openin (top_of_set U) W1"
nipkow@68617
  1502
               and contg: "continuous_on W1 g"
nipkow@68617
  1503
               and gim: "g ` W1 \<subseteq> S"
nipkow@68617
  1504
               and geq: "\<And>x. x \<in> C \<Longrightarrow> g x = (fst \<circ> f) x"
nipkow@68617
  1505
    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> contf1 _ cloUC])
nipkow@68617
  1506
    using fim apply auto
nipkow@68617
  1507
    done
nipkow@68617
  1508
  have contf2: "continuous_on C (snd \<circ> f)"
nipkow@68617
  1509
    by (simp add: \<open>continuous_on C f\<close> continuous_on_snd)
nipkow@68617
  1510
  obtain W2 h where "C \<subseteq> W2"
lp15@69922
  1511
               and UW2: "openin (top_of_set U) W2"
nipkow@68617
  1512
               and conth: "continuous_on W2 h"
nipkow@68617
  1513
               and him: "h ` W2 \<subseteq> T"
nipkow@68617
  1514
               and heq: "\<And>x. x \<in> C \<Longrightarrow> h x = (snd \<circ> f) x"
nipkow@68617
  1515
    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf2 _ cloUC])
nipkow@68617
  1516
    using fim apply auto
nipkow@68617
  1517
    done
nipkow@68617
  1518
  show "\<exists>V g. C \<subseteq> V \<and>
lp15@69922
  1519
               openin (top_of_set U) V \<and>
nipkow@68617
  1520
               continuous_on V g \<and> g ` V \<subseteq> S \<times> T \<and> (\<forall>x\<in>C. g x = f x)"
nipkow@68617
  1521
  proof (intro exI conjI)
nipkow@68617
  1522
    show "C \<subseteq> W1 \<inter> W2"
nipkow@68617
  1523
      by (simp add: \<open>C \<subseteq> W1\<close> \<open>C \<subseteq> W2\<close>)
lp15@69922
  1524
    show "openin (top_of_set U) (W1 \<inter> W2)"
nipkow@68617
  1525
      by (simp add: UW1 UW2 openin_Int)
nipkow@68617
  1526
    show  "continuous_on (W1 \<inter> W2) (\<lambda>x. (g x, h x))"
nipkow@68617
  1527
      by (metis (no_types) contg conth continuous_on_Pair continuous_on_subset inf_commute inf_le1)
nipkow@68617
  1528
    show  "(\<lambda>x. (g x, h x)) ` (W1 \<inter> W2) \<subseteq> S \<times> T"
nipkow@68617
  1529
      using gim him by blast
nipkow@68617
  1530
    show  "(\<forall>x\<in>C. (g x, h x) = f x)"
nipkow@68617
  1531
      using geq heq by auto
nipkow@68617
  1532
  qed
nipkow@68617
  1533
qed
nipkow@68617
  1534
nipkow@68617
  1535
lemma AR_Times:
nipkow@68617
  1536
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
nipkow@68617
  1537
  assumes "AR S" "AR T" shows "AR(S \<times> T)"
nipkow@68617
  1538
using assms by (simp add: AR_ANR ANR_Times contractible_Times)
nipkow@68617
  1539
nipkow@68617
  1540
subsection \<open>Kuhn Simplices\<close>
nipkow@68617
  1541
hoelzl@56273
  1542
lemma bij_betw_singleton_eq:
hoelzl@56273
  1543
  assumes f: "bij_betw f A B" and g: "bij_betw g A B" and a: "a \<in> A"
hoelzl@56273
  1544
  assumes eq: "(\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x = g x)"
hoelzl@56273
  1545
  shows "f a = g a"
hoelzl@56273
  1546
proof -
hoelzl@56273
  1547
  have "f ` (A - {a}) = g ` (A - {a})"
hoelzl@56273
  1548
    by (intro image_cong) (simp_all add: eq)
hoelzl@56273
  1549
  then have "B - {f a} = B - {g a}"
nipkow@69286
  1550
    using f g a  by (auto simp: bij_betw_def inj_on_image_set_diff set_eq_iff)
hoelzl@56273
  1551
  moreover have "f a \<in> B" "g a \<in> B"
hoelzl@56273
  1552
    using f g a by (auto simp: bij_betw_def)
hoelzl@56273
  1553
  ultimately show ?thesis
hoelzl@56273
  1554
    by auto
hoelzl@56273
  1555
qed
hoelzl@56273
  1556
hoelzl@56273
  1557
lemma swap_image:
hoelzl@56273
  1558
  "Fun.swap i j f ` A = (if i \<in> A then (if j \<in> A then f ` A else f ` ((A - {i}) \<union> {j}))
hoelzl@56273
  1559
                                  else (if j \<in> A then f ` ((A - {j}) \<union> {i}) else f ` A))"
haftmann@69661
  1560
  by (auto simp: swap_def cong: image_cong_simp)
hoelzl@56273
  1561
haftmann@63365
  1562
lemmas swap_apply1 = swap_apply(1)
haftmann@63365
  1563
lemmas swap_apply2 = swap_apply(2)
hoelzl@56273
  1564
hoelzl@56273
  1565
lemma pointwise_minimal_pointwise_maximal:
hoelzl@56273
  1566
  fixes s :: "(nat \<Rightarrow> nat) set"
hoelzl@56273
  1567
  assumes "finite s"
hoelzl@56273
  1568
    and "s \<noteq> {}"
hoelzl@56273
  1569
    and "\<forall>x\<in>s. \<forall>y\<in>s. x \<le> y \<or> y \<le> x"
hoelzl@56273
  1570
  shows "\<exists>a\<in>s. \<forall>x\<in>s. a \<le> x"
hoelzl@56273
  1571
    and "\<exists>a\<in>s. \<forall>x\<in>s. x \<le> a"
hoelzl@56273
  1572
  using assms
hoelzl@56273
  1573
proof (induct s rule: finite_ne_induct)
hoelzl@56273
  1574
  case (insert b s)
hoelzl@56273
  1575
  assume *: "\<forall>x\<in>insert b s. \<forall>y\<in>insert b s. x \<le> y \<or> y \<le> x"
wenzelm@63540
  1576
  then obtain u l where "l \<in> s" "\<forall>b\<in>s. l \<le> b" "u \<in> s" "\<forall>b\<in>s. b \<le> u"
hoelzl@56273
  1577
    using insert by auto
wenzelm@63540
  1578
  with * show "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. a \<le> x" "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. x \<le> a"
hoelzl@56273
  1579
    using *[rule_format, of b u] *[rule_format, of b l] by (metis insert_iff order.trans)+
hoelzl@56273
  1580
qed auto
hoelzl@50526
  1581
wenzelm@49555
  1582
lemma kuhn_labelling_lemma:
hoelzl@50526
  1583
  fixes P Q :: "'a::euclidean_space \<Rightarrow> bool"
hoelzl@56273
  1584
  assumes "\<forall>x. P x \<longrightarrow> P (f x)"
hoelzl@50526
  1585
    and "\<forall>x. P x \<longrightarrow> (\<forall>i\<in>Basis. Q i \<longrightarrow> 0 \<le> x\<bullet>i \<and> x\<bullet>i \<le> 1)"
hoelzl@50526
  1586
  shows "\<exists>l. (\<forall>x.\<forall>i\<in>Basis. l x i \<le> (1::nat)) \<and>
hoelzl@50526
  1587
             (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 0) \<longrightarrow> (l x i = 0)) \<and>
hoelzl@50526
  1588
             (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 1) \<longrightarrow> (l x i = 1)) \<and>
hoelzl@56273
  1589
             (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x\<bullet>i \<le> f x\<bullet>i) \<and>
hoelzl@56273
  1590
             (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f x\<bullet>i \<le> x\<bullet>i)"
wenzelm@49374
  1591
proof -
hoelzl@56273
  1592
  { fix x i
hoelzl@56273
  1593
    let ?R = "\<lambda>y. (P x \<and> Q i \<and> x \<bullet> i = 0 \<longrightarrow> y = (0::nat)) \<and>
hoelzl@56273
  1594
        (P x \<and> Q i \<and> x \<bullet> i = 1 \<longrightarrow> y = 1) \<and>
hoelzl@56273
  1595
        (P x \<and> Q i \<and> y = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i) \<and>
hoelzl@56273
  1596
        (P x \<and> Q i \<and> y = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i)"
hoelzl@56273
  1597
    { assume "P x" "Q i" "i \<in> Basis" with assms have "0 \<le> f x \<bullet> i \<and> f x \<bullet> i \<le> 1" by auto }
hoelzl@56273
  1598
    then have "i \<in> Basis \<Longrightarrow> ?R 0 \<or> ?R 1" by auto }
hoelzl@56273
  1599
  then show ?thesis
hoelzl@56273
  1600
    unfolding all_conj_distrib[symmetric] Ball_def (* FIXME: shouldn't this work by metis? *)
hoelzl@56273
  1601
    by (subst choice_iff[symmetric])+ blast
wenzelm@49374
  1602
qed
wenzelm@49374
  1603
wenzelm@53185
  1604
nipkow@68617
  1605
subsubsection \<open>The key "counting" observation, somewhat abstracted\<close>
hoelzl@33741
  1606
wenzelm@53252
  1607
lemma kuhn_counting_lemma:
hoelzl@56273
  1608
  fixes bnd compo compo' face S F
hoelzl@56273
  1609
  defines "nF s == card {f\<in>F. face f s \<and> compo' f}"
wenzelm@67443
  1610
  assumes [simp, intro]: "finite F" \<comment> \<open>faces\<close> and [simp, intro]: "finite S" \<comment> \<open>simplices\<close>
hoelzl@56273
  1611
    and "\<And>f. f \<in> F \<Longrightarrow> bnd f \<Longrightarrow> card {s\<in>S. face f s} = 1"
hoelzl@56273
  1612
    and "\<And>f. f \<in> F \<Longrightarrow> \<not> bnd f \<Longrightarrow> card {s\<in>S. face f s} = 2"
hoelzl@56273
  1613
    and "\<And>s. s \<in> S \<Longrightarrow> compo s \<Longrightarrow> nF s = 1"
hoelzl@56273
  1614
    and "\<And>s. s \<in> S \<Longrightarrow> \<not> compo s \<Longrightarrow> nF s = 0 \<or> nF s = 2"
hoelzl@56273
  1615
    and "odd (card {f\<in>F. compo' f \<and> bnd f})"
hoelzl@56273
  1616
  shows "odd (card {s\<in>S. compo s})"
wenzelm@53185
  1617
proof -
hoelzl@56273
  1618
  have "(\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) + (\<Sum>s | s \<in> S \<and> compo s. nF s) = (\<Sum>s\<in>S. nF s)"
nipkow@64267
  1619
    by (subst sum.union_disjoint[symmetric]) (auto intro!: sum.cong)
hoelzl@56273
  1620
  also have "\<dots> = (\<Sum>s\<in>S. card {f \<in> {f\<in>F. compo' f \<and> bnd f}. face f s}) +
hoelzl@56273
  1621
                  (\<Sum>s\<in>S. card {f \<in> {f\<in>F. compo' f \<and> \<not> bnd f}. face f s})"
nipkow@64267
  1622
    unfolding sum.distrib[symmetric]
hoelzl@56273
  1623
    by (subst card_Un_disjoint[symmetric])
nipkow@64267
  1624
       (auto simp: nF_def intro!: sum.cong arg_cong[where f=card])
hoelzl@56273
  1625
  also have "\<dots> = 1 * card {f\<in>F. compo' f \<and> bnd f} + 2 * card {f\<in>F. compo' f \<and> \<not> bnd f}"
nipkow@67399
  1626
    using assms(4,5) by (fastforce intro!: arg_cong2[where f="(+)"] sum_multicount)
hoelzl@56273
  1627
  finally have "odd ((\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) + card {s\<in>S. compo s})"
hoelzl@56273
  1628
    using assms(6,8) by simp
hoelzl@56273
  1629
  moreover have "(\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) =
hoelzl@56273
  1630
    (\<Sum>s | s \<in> S \<and> \<not> compo s \<and> nF s = 0. nF s) + (\<Sum>s | s \<in> S \<and> \<not> compo s \<and> nF s = 2. nF s)"
nipkow@64267
  1631
    using assms(7) by (subst sum.union_disjoint[symmetric]) (fastforce intro!: sum.cong)+
wenzelm@53688
  1632
  ultimately show ?thesis
wenzelm@53688
  1633
    by auto
wenzelm@53186
  1634
qed
wenzelm@53186
  1635
nipkow@68617
  1636
subsubsection \<open>The odd/even result for faces of complete vertices, generalized\<close>
hoelzl@56273
  1637
hoelzl@56273
  1638
lemma kuhn_complete_lemma:
hoelzl@56273
  1639
  assumes [simp]: "finite simplices"
hoelzl@56273
  1640
    and face: "\<And>f s. face f s \<longleftrightarrow> (\<exists>a\<in>s. f = s - {a})"
hoelzl@56273
  1641
    and card_s[simp]:  "\<And>s. s \<in> simplices \<Longrightarrow> card s = n + 2"
hoelzl@56273
  1642
    and rl_bd: "\<And>s. s \<in> simplices \<Longrightarrow> rl ` s \<subseteq> {..Suc n}"
hoelzl@56273
  1643
    and bnd: "\<And>f s. s \<in> simplices \<Longrightarrow> face f s \<Longrightarrow> bnd f \<Longrightarrow> card {s\<in>simplices. face f s} = 1"
hoelzl@56273
  1644
    and nbnd: "\<And>f s. s \<in> simplices \<Longrightarrow> face f s \<Longrightarrow> \<not> bnd f \<Longrightarrow> card {s\<in>simplices. face f s} = 2"
hoelzl@56273
  1645
    and odd_card: "odd (card {f. (\<exists>s\<in>simplices. face f s) \<and> rl ` f = {..n} \<and> bnd f})"
hoelzl@56273
  1646
  shows "odd (card {s\<in>simplices. (rl ` s = {..Suc n})})"
hoelzl@56273
  1647
proof (rule kuhn_counting_lemma)
hoelzl@56273
  1648
  have finite_s[simp]: "\<And>s. s \<in> simplices \<Longrightarrow> finite s"
lp15@61609
  1649
    by (metis add_is_0 zero_neq_numeral card_infinite assms(3))
hoelzl@56273
  1650
hoelzl@56273
  1651
  let ?F = "{f. \<exists>s\<in>simplices. face f s}"
hoelzl@56273
  1652
  have F_eq: "?F = (\<Union>s\<in>simplices. \<Union>a\<in>s. {s - {a}})"
hoelzl@56273
  1653
    by (auto simp: face)
hoelzl@56273
  1654
  show "finite ?F"
wenzelm@60420
  1655
    using \<open>finite simplices\<close> unfolding F_eq by auto
hoelzl@56273
  1656
wenzelm@60421
  1657
  show "card {s \<in> simplices. face f s} = 1" if "f \<in> ?F" "bnd f" for f
wenzelm@60449
  1658
    using bnd that by auto
hoelzl@56273
  1659
wenzelm@60421
  1660
  show "card {s \<in> simplices. face f s} = 2" if "f \<in> ?F" "\<not> bnd f" for f
wenzelm@60449
  1661
    using nbnd that by auto
hoelzl@56273
  1662
hoelzl@56273
  1663
  show "odd (card {f \<in> {f. \<exists>s\<in>simplices. face f s}. rl ` f = {..n} \<and> bnd f})"
hoelzl@56273
  1664
    using odd_card by simp
hoelzl@56273
  1665
hoelzl@56273
  1666
  fix s assume s[simp]: "s \<in> simplices"
hoelzl@56273
  1667
  let ?S = "{f \<in> {f. \<exists>s\<in>simplices. face f s}. face f s \<and> rl ` f = {..n}}"
hoelzl@56273
  1668
  have "?S = (\<lambda>a. s - {a}) ` {a\<in>s. rl ` (s - {a}) = {..n}}"
hoelzl@56273
  1669
    using s by (fastforce simp: face)
hoelzl@56273
  1670
  then have card_S: "card ?S = card {a\<in>s. rl ` (s - {a}) = {..n}}"
hoelzl@56273
  1671
    by (auto intro!: card_image inj_onI)
hoelzl@56273
  1672
hoelzl@56273
  1673
  { assume rl: "rl ` s = {..Suc n}"
hoelzl@56273
  1674
    then have inj_rl: "inj_on rl s"
hoelzl@56273
  1675
      by (intro eq_card_imp_inj_on) auto
hoelzl@56273
  1676
    moreover obtain a where "rl a = Suc n" "a \<in> s"
hoelzl@56273
  1677
      by (metis atMost_iff image_iff le_Suc_eq rl)
hoelzl@56273
  1678
    ultimately have n: "{..n} = rl ` (s - {a})"
nipkow@69286
  1679
      by (auto simp: inj_on_image_set_diff rl)
hoelzl@56273
  1680
    have "{a\<in>s. rl ` (s - {a}) = {..n}} = {a}"
nipkow@69286
  1681
      using inj_rl \<open>a \<in> s\<close> by (auto simp: n inj_on_image_eq_iff[OF inj_rl])
hoelzl@56273
  1682
    then show "card ?S = 1"
hoelzl@56273
  1683
      unfolding card_S by simp }
hoelzl@56273
  1684
hoelzl@56273
  1685
  { assume rl: "rl ` s \<noteq> {..Suc n}"
hoelzl@56273
  1686
    show "card ?S = 0 \<or> card ?S = 2"
hoelzl@56273
  1687
    proof cases
hoelzl@56273
  1688
      assume *: "{..n} \<subseteq> rl ` s"
hoelzl@56273
  1689
      with rl rl_bd[OF s] have rl_s: "rl ` s = {..n}"
lp15@68022
  1690
        by (auto simp: atMost_Suc subset_insert_iff split: if_split_asm)
hoelzl@56273
  1691
      then have "\<not> inj_on rl s"
hoelzl@56273
  1692
        by (intro pigeonhole) simp
hoelzl@56273
  1693
      then obtain a b where ab: "a \<in> s" "b \<in> s" "rl a = rl b" "a \<noteq> b"
hoelzl@56273
  1694
        by (auto simp: inj_on_def)
hoelzl@56273
  1695
      then have eq: "rl ` (s - {a}) = rl ` s"
hoelzl@56273
  1696
        by auto
hoelzl@56273
  1697
      with ab have inj: "inj_on rl (s - {a})"
lp15@68022
  1698
        by (intro eq_card_imp_inj_on) (auto simp: rl_s card_Diff_singleton_if)
hoelzl@56273
  1699
hoelzl@56273
  1700
      { fix x assume "x \<in> s" "x \<notin> {a, b}"
hoelzl@56273
  1701
        then have "rl ` s - {rl x} = rl ` ((s - {a}) - {x})"
nipkow@69286
  1702
          by (auto simp: eq inj_on_image_set_diff[OF inj])
hoelzl@56273
  1703
        also have "\<dots> = rl ` (s - {x})"
wenzelm@60420
  1704
          using ab \<open>x \<notin> {a, b}\<close> by auto
hoelzl@56273
  1705
        also assume "\<dots> = rl ` s"
hoelzl@56273
  1706
        finally have False
wenzelm@60420
  1707
          using \<open>x\<in>s\<close> by auto }
hoelzl@56273
  1708
      moreover
hoelzl@56273
  1709
      { fix x assume "x \<in> {a, b}" with ab have "x \<in> s \<and> rl ` (s - {x}) = rl ` s"
hoelzl@56273
  1710
          by (simp add: set_eq_iff image_iff Bex_def) metis }
hoelzl@56273
  1711
      ultimately have "{a\<in>s. rl ` (s - {a}) = {..n}} = {a, b}"
hoelzl@56273
  1712
        unfolding rl_s[symmetric] by fastforce
wenzelm@60420
  1713
      with \<open>a \<noteq> b\<close> show "card ?S = 0 \<or> card ?S = 2"
hoelzl@56273
  1714
        unfolding card_S by simp
hoelzl@56273
  1715
    next
hoelzl@56273
  1716
      assume "\<not> {..n} \<subseteq> rl ` s"
hoelzl@56273
  1717
      then have "\<And>x. rl ` (s - {x}) \<noteq> {..n}"
hoelzl@56273
  1718
        by auto
hoelzl@56273
  1719
      then show "card ?S = 0 \<or> card ?S = 2"
hoelzl@56273
  1720
        unfolding card_S by simp
hoelzl@56273
  1721
    qed }
hoelzl@56273
  1722
qed fact
hoelzl@56273
  1723
hoelzl@56273
  1724
locale kuhn_simplex =
hoelzl@56273
  1725
  fixes p n and base upd and s :: "(nat \<Rightarrow> nat) set"
hoelzl@56273
  1726
  assumes base: "base \<in> {..< n} \<rightarrow> {..< p}"
hoelzl@56273
  1727
  assumes base_out: "\<And>i. n \<le> i \<Longrightarrow> base i = p"
hoelzl@56273
  1728
  assumes upd: "bij_betw upd {..< n} {..< n}"
hoelzl@56273
  1729
  assumes s_pre: "s = (\<lambda>i j. if j \<in> upd`{..< i} then Suc (base j) else base j) ` {.. n}"
hoelzl@56273
  1730
begin
hoelzl@56273
  1731
hoelzl@56273
  1732
definition "enum i j = (if j \<in> upd`{..< i} then Suc (base j) else base j)"
hoelzl@56273
  1733
hoelzl@56273
  1734
lemma s_eq: "s = enum ` {.. n}"
hoelzl@56273
  1735
  unfolding s_pre enum_def[abs_def] ..
hoelzl@56273
  1736
hoelzl@56273
  1737
lemma upd_space: "i < n \<Longrightarrow> upd i < n"
hoelzl@56273
  1738
  using upd by (auto dest!: bij_betwE)
hoelzl@56273
  1739
hoelzl@56273
  1740
lemma s_space: "s \<subseteq> {..< n} \<rightarrow> {.. p}"
hoelzl@56273
  1741
proof -
hoelzl@56273
  1742
  { fix i assume "i \<le> n" then have "enum i \<in> {..< n} \<rightarrow> {.. p}"
hoelzl@56273
  1743
    proof (induct i)
hoelzl@56273
  1744
      case 0 then show ?case
hoelzl@56273
  1745
        using base by (auto simp: Pi_iff less_imp_le enum_def)
hoelzl@56273
  1746
    next
hoelzl@56273
  1747
      case (Suc i) with base show ?case
hoelzl@56273
  1748
        by (auto simp: Pi_iff Suc_le_eq less_imp_le enum_def intro: upd_space)
hoelzl@56273
  1749
    qed }
hoelzl@56273
  1750
  then show ?thesis
hoelzl@56273
  1751
    by (auto simp: s_eq)
hoelzl@56273
  1752
qed
hoelzl@56273
  1753
hoelzl@56273
  1754
lemma inj_upd: "inj_on upd {..< n}"
hoelzl@56273
  1755
  using upd by (simp add: bij_betw_def)
hoelzl@56273
  1756
hoelzl@56273
  1757
lemma inj_enum: "inj_on enum {.. n}"
hoelzl@56273
  1758
proof -
hoelzl@56273
  1759
  { fix x y :: nat assume "x \<noteq> y" "x \<le> n" "y \<le> n"
hoelzl@56273
  1760
    with upd have "upd ` {..< x} \<noteq> upd ` {..< y}"
lp15@61609
  1761
      by (subst inj_on_image_eq_iff[where C="{..< n}"]) (auto simp: bij_betw_def)
hoelzl@56273
  1762
    then have "enum x \<noteq> enum y"
lp15@68022
  1763
      by (auto simp: enum_def fun_eq_iff) }
hoelzl@56273
  1764
  then show ?thesis
hoelzl@56273
  1765
    by (auto simp: inj_on_def)
hoelzl@56273
  1766
qed
hoelzl@56273
  1767
hoelzl@56273
  1768
lemma enum_0: "enum 0 = base"
hoelzl@56273
  1769
  by (simp add: enum_def[abs_def])
hoelzl@56273
  1770
hoelzl@56273
  1771
lemma base_in_s: "base \<in> s"
hoelzl@56273
  1772
  unfolding s_eq by (subst enum_0[symmetric]) auto
hoelzl@56273
  1773
hoelzl@56273
  1774
lemma enum_in: "i \<le> n \<Longrightarrow> enum i \<in> s"
hoelzl@56273
  1775
  unfolding s_eq by auto
hoelzl@56273
  1776
hoelzl@56273
  1777
lemma one_step:
hoelzl@56273
  1778
  assumes a: "a \<in> s" "j < n"
hoelzl@56273
  1779
  assumes *: "\<And>a'. a' \<in> s \<Longrightarrow> a' \<noteq> a \<Longrightarrow> a' j = p'"
hoelzl@56273
  1780
  shows "a j \<noteq> p'"
hoelzl@56273
  1781
proof
hoelzl@56273
  1782
  assume "a j = p'"
hoelzl@56273
  1783
  with * a have "\<And>a'. a' \<in> s \<Longrightarrow> a' j = p'"
hoelzl@56273
  1784
    by auto
hoelzl@56273
  1785
  then have "\<And>i. i \<le> n \<Longrightarrow> enum i j = p'"
hoelzl@56273
  1786
    unfolding s_eq by auto
hoelzl@56273
  1787
  from this[of 0] this[of n] have "j \<notin> upd ` {..< n}"
nipkow@62390
  1788
    by (auto simp: enum_def fun_eq_iff split: if_split_asm)
wenzelm@60420
  1789
  with upd \<open>j < n\<close> show False
hoelzl@56273
  1790
    by (auto simp: bij_betw_def)
hoelzl@56273
  1791
qed
hoelzl@56273
  1792
hoelzl@56273
  1793
lemma upd_inj: "i < n \<Longrightarrow> j < n \<Longrightarrow> upd i = upd j \<longleftrightarrow> i = j"
lp15@61520
  1794
  using upd by (auto simp: bij_betw_def inj_on_eq_iff)
hoelzl@56273
  1795
hoelzl@56273
  1796
lemma upd_surj: "upd ` {..< n} = {..< n}"
hoelzl@56273
  1797
  using upd by (auto simp: bij_betw_def)
hoelzl@56273
  1798
hoelzl@56273
  1799
lemma in_upd_image: "A \<subseteq> {..< n} \<Longrightarrow> i < n \<Longrightarrow> upd i \<in> upd ` A \<longleftrightarrow> i \<in> A"
lp15@61520
  1800
  using inj_on_image_mem_iff[of upd "{..< n}"] upd
hoelzl@56273
  1801
  by (auto simp: bij_betw_def)
hoelzl@56273
  1802
hoelzl@56273
  1803
lemma enum_inj: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i = enum j \<longleftrightarrow> i = j"
lp15@61520
  1804
  using inj_enum by (auto simp: inj_on_eq_iff)
hoelzl@56273
  1805
hoelzl@56273
  1806
lemma in_enum_image: "A \<subseteq> {.. n} \<Longrightarrow> i \<le> n \<Longrightarrow> enum i \<in> enum ` A \<longleftrightarrow> i \<in> A"
lp15@61520
  1807
  using inj_on_image_mem_iff[OF inj_enum] by auto
hoelzl@56273
  1808
hoelzl@56273
  1809
lemma enum_mono: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i \<le> enum j \<longleftrightarrow> i \<le> j"
hoelzl@56273
  1810
  by (auto simp: enum_def le_fun_def in_upd_image Ball_def[symmetric])
hoelzl@56273
  1811
hoelzl@56273
  1812
lemma enum_strict_mono: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i < enum j \<longleftrightarrow> i < j"
lp15@68022
  1813
  using enum_mono[of i j] enum_inj[of i j] by (auto simp: le_less)
hoelzl@56273
  1814
hoelzl@56273
  1815
lemma chain: "a \<in> s \<Longrightarrow> b \<in> s \<Longrightarrow> a \<le> b \<or> b \<le> a"
hoelzl@56273
  1816
  by (auto simp: s_eq enum_mono)
hoelzl@56273
  1817
hoelzl@56273
  1818
lemma less: "a \<in> s \<Longrightarrow> b \<in> s \<Longrightarrow> a i < b i \<Longrightarrow> a < b"
hoelzl@56273
  1819
  using chain[of a b] by (auto simp: less_fun_def le_fun_def not_le[symmetric])
hoelzl@56273
  1820
hoelzl@56273
  1821
lemma enum_0_bot: "a \<in> s \<Longrightarrow> a = enum 0 \<longleftrightarrow> (\<forall>a'\<in>s. a \<le> a')"
hoelzl@56273
  1822
  unfolding s_eq by (auto simp: enum_mono Ball_def)
hoelzl@56273
  1823
hoelzl@56273
  1824
lemma enum_n_top: "a \<in> s \<Longrightarrow> a = enum n \<longleftrightarrow> (\<forall>a'\<in>s. a' \<le> a)"
hoelzl@56273
  1825
  unfolding s_eq by (auto simp: enum_mono Ball_def)
hoelzl@56273
  1826
hoelzl@56273
  1827
lemma enum_Suc: "i < n \<Longrightarrow> enum (Suc i) = (enum i)(upd i := Suc (enum i (upd i)))"
hoelzl@56273
  1828
  by (auto simp: fun_eq_iff enum_def upd_inj)
hoelzl@56273
  1829
hoelzl@56273
  1830
lemma enum_eq_p: "i \<le> n \<Longrightarrow> n \<le> j \<Longrightarrow> enum i j = p"
hoelzl@56273
  1831
  by (induct i) (auto simp: enum_Suc enum_0 base_out upd_space not_less[symmetric])
hoelzl@56273
  1832
hoelzl@56273
  1833
lemma out_eq_p: "a \<in> s \<Longrightarrow> n \<le> j \<Longrightarrow> a j = p"
lp15@68022
  1834
  unfolding s_eq by (auto simp: enum_eq_p)
hoelzl@56273
  1835
hoelzl@56273
  1836
lemma s_le_p: "a \<in> s \<Longrightarrow> a j \<le> p"
hoelzl@56273
  1837
  using out_eq_p[of a j] s_space by (cases "j < n") auto
hoelzl@56273
  1838
hoelzl@56273
  1839
lemma le_Suc_base: "a \<in> s \<Longrightarrow> a j \<le> Suc (base j)"
hoelzl@56273
  1840
  unfolding s_eq by (auto simp: enum_def)
hoelzl@56273
  1841
hoelzl@56273
  1842
lemma base_le: "a \<in> s \<Longrightarrow> base j \<le> a j"
hoelzl@56273
  1843
  unfolding s_eq by (auto simp: enum_def)
hoelzl@56273
  1844
hoelzl@56273
  1845
lemma enum_le_p: "i \<le> n \<Longrightarrow> j < n \<Longrightarrow> enum i j \<le> p"
hoelzl@56273
  1846
  using enum_in[of i] s_space by auto
hoelzl@56273
  1847
hoelzl@56273
  1848
lemma enum_less: "a \<in> s \<Longrightarrow> i < n \<Longrightarrow> enum i < a \<longleftrightarrow> enum (Suc i) \<le> a"
hoelzl@56273
  1849
  unfolding s_eq by (auto simp: enum_strict_mono enum_mono)
hoelzl@56273
  1850
hoelzl@56273
  1851
lemma ksimplex_0:
hoelzl@56273
  1852
  "n = 0 \<Longrightarrow> s = {(\<lambda>x. p)}"
hoelzl@56273
  1853
  using s_eq enum_def base_out by auto
hoelzl@56273
  1854
hoelzl@56273
  1855
lemma replace_0:
hoelzl@56273
  1856
  assumes "j < n" "a \<in> s" and p: "\<forall>x\<in>s - {a}. x j = 0" and "x \<in> s"
hoelzl@56273
  1857
  shows "x \<le> a"
hoelzl@56273
  1858
proof cases
hoelzl@56273
  1859
  assume "x \<noteq> a"
hoelzl@56273
  1860
  have "a j \<noteq> 0"
hoelzl@56273
  1861
    using assms by (intro one_step[where a=a]) auto
wenzelm@60420
  1862
  with less[OF \<open>x\<in>s\<close> \<open>a\<in>s\<close>, of j] p[rule_format, of x] \<open>x \<in> s\<close> \<open>x \<noteq> a\<close>
hoelzl@56273
  1863
  show ?thesis
hoelzl@56273
  1864
    by auto
hoelzl@56273
  1865
qed simp
hoelzl@56273
  1866
hoelzl@56273
  1867
lemma replace_1:
hoelzl@56273
  1868
  assumes "j < n" "a \<in> s" and p: "\<forall>x\<in>s - {a}. x j = p" and "x \<in> s"
hoelzl@56273
  1869
  shows "a \<le> x"
hoelzl@56273
  1870
proof cases
hoelzl@56273
  1871
  assume "x \<noteq> a"
hoelzl@56273
  1872
  have "a j \<noteq> p"
hoelzl@56273
  1873
    using assms by (intro one_step[where a=a]) auto
wenzelm@60420
  1874
  with enum_le_p[of _ j] \<open>j < n\<close> \<open>a\<in>s\<close>
hoelzl@56273
  1875
  have "a j < p"
hoelzl@56273
  1876
    by (auto simp: less_le s_eq)
wenzelm@60420
  1877
  with less[OF \<open>a\<in>s\<close> \<open>x\<in>s\<close>, of j] p[rule_format, of x] \<open>x \<in> s\<close> \<open>x \<noteq> a\<close>
hoelzl@56273
  1878
  show ?thesis
hoelzl@56273
  1879
    by auto
hoelzl@56273
  1880
qed simp
hoelzl@56273
  1881
hoelzl@56273
  1882
end
hoelzl@56273
  1883
hoelzl@56273
  1884
locale kuhn_simplex_pair = s: kuhn_simplex p n b_s u_s s + t: kuhn_simplex p n b_t u_t t
hoelzl@56273
  1885
  for p n b_s u_s s b_t u_t t
hoelzl@56273
  1886
begin
hoelzl@56273
  1887
hoelzl@56273
  1888
lemma enum_eq:
hoelzl@56273
  1889
  assumes l: "i \<le> l" "l \<le> j" and "j + d \<le> n"
hoelzl@56273
  1890
  assumes eq: "s.enum ` {i .. j} = t.enum ` {i + d .. j + d}"
hoelzl@56273
  1891
  shows "s.enum l = t.enum (l + d)"
hoelzl@56273
  1892
using l proof (induct l rule: dec_induct)
hoelzl@56273
  1893
  case base
hoelzl@56273
  1894
  then have s: "s.enum i \<in> t.enum ` {i + d .. j + d}" and t: "t.enum (i + d) \<in> s.enum ` {i .. j}"
hoelzl@56273
  1895
    using eq by auto
wenzelm@60420
  1896
  from t \<open>i \<le> j\<close> \<open>j + d \<le> n\<close> have "s.enum i \<le> t.enum (i + d)"
hoelzl@56273
  1897
    by (auto simp: s.enum_mono)
wenzelm@60420
  1898
  moreover from s \<open>i \<le> j\<close> \<open>j + d \<le> n\<close> have "t.enum (i + d) \<le> s.enum i"
hoelzl@56273
  1899
    by (auto simp: t.enum_mono)
hoelzl@56273
  1900
  ultimately show ?case
hoelzl@56273
  1901
    by auto
hoelzl@56273
  1902
next
hoelzl@56273
  1903
  case (step l)
wenzelm@60420
  1904
  moreover from step.prems \<open>j + d \<le> n\<close> have
hoelzl@56273
  1905
      "s.enum l < s.enum (Suc l)"
hoelzl@56273
  1906
      "t.enum (l + d) < t.enum (Suc l + d)"
hoelzl@56273
  1907
    by (simp_all add: s.enum_strict_mono t.enum_strict_mono)
hoelzl@56273
  1908
  moreover have
hoelzl@56273
  1909
      "s.enum (Suc l) \<in> t.enum ` {i + d .. j + d}"
hoelzl@56273
  1910
      "t.enum (Suc l + d) \<in> s.enum ` {i .. j}"
wenzelm@60420
  1911
    using step \<open>j + d \<le> n\<close> eq by (auto simp: s.enum_inj t.enum_inj)
hoelzl@56273
  1912
  ultimately have "s.enum (Suc l) = t.enum (Suc (l + d))"
wenzelm@60420
  1913
    using \<open>j + d \<le> n\<close>
lp15@61609
  1914
    by (intro antisym s.enum_less[THEN iffD1] t.enum_less[THEN iffD1])
hoelzl@56273
  1915
       (auto intro!: s.enum_in t.enum_in)
hoelzl@56273
  1916
  then show ?case by simp
hoelzl@56273
  1917
qed
hoelzl@56273
  1918
hoelzl@56273
  1919
lemma ksimplex_eq_bot:
hoelzl@56273
  1920
  assumes a: "a \<in> s" "\<And>a'. a' \<in> s \<Longrightarrow> a \<le> a'"
hoelzl@56273
  1921
  assumes b: "b \<in> t" "\<And>b'. b' \<in> t \<Longrightarrow> b \<le> b'"
hoelzl@56273
  1922
  assumes eq: "s - {a} = t - {b}"
hoelzl@56273
  1923
  shows "s = t"
hoelzl@56273
  1924
proof cases
hoelzl@56273
  1925
  assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp
hoelzl@56273
  1926
next
hoelzl@56273
  1927
  assume "n \<noteq> 0"
hoelzl@56273
  1928
  have "s.enum 0 = (s.enum (Suc 0)) (u_s 0 := s.enum (Suc 0) (u_s 0) - 1)"
hoelzl@56273
  1929
       "t.enum 0 = (t.enum (Suc 0)) (u_t 0 := t.enum (Suc 0) (u_t 0) - 1)"
wenzelm@60420
  1930
    using \<open>n \<noteq> 0\<close> by (simp_all add: s.enum_Suc t.enum_Suc)
hoelzl@56273
  1931
  moreover have e0: "a = s.enum 0" "b = t.enum 0"
hoelzl@56273
  1932
    using a b by (simp_all add: s.enum_0_bot t.enum_0_bot)
hoelzl@56273
  1933
  moreover
lp15@61609
  1934
  { fix j assume "0 < j" "j \<le> n"
hoelzl@56273
  1935
    moreover have "s - {a} = s.enum ` {Suc 0 .. n}" "t - {b} = t.enum ` {Suc 0 .. n}"
hoelzl@56273
  1936
      unfolding s.s_eq t.s_eq e0 by (auto simp: s.enum_inj t.enum_inj)
hoelzl@56273
  1937
    ultimately have "s.enum j = t.enum j"
hoelzl@56273
  1938
      using enum_eq[of "1" j n 0] eq by auto }
hoelzl@56273
  1939
  note enum_eq = this
hoelzl@56273
  1940
  then have "s.enum (Suc 0) = t.enum (Suc 0)"
wenzelm@60420
  1941
    using \<open>n \<noteq> 0\<close> by auto
hoelzl@56273
  1942
  moreover
hoelzl@56273
  1943
  { fix j assume "Suc j < n"
hoelzl@56273
  1944
    with enum_eq[of "Suc j"] enum_eq[of "Suc (Suc j)"]
hoelzl@56273
  1945
    have "u_s (Suc j) = u_t (Suc j)"
hoelzl@56273
  1946
      using s.enum_Suc[of "Suc j"] t.enum_Suc[of "Suc j"]
nipkow@62390
  1947
      by (auto simp: fun_eq_iff split: if_split_asm) }
hoelzl@56273
  1948
  then have "\<And>j. 0 < j \<Longrightarrow> j < n \<Longrightarrow> u_s j = u_t j"
hoelzl@56273
  1949
    by (auto simp: gr0_conv_Suc)
wenzelm@60420
  1950
  with \<open>n \<noteq> 0\<close> have "u_t 0 = u_s 0"
hoelzl@56273
  1951
    by (intro bij_betw_singleton_eq[OF t.upd s.upd, of 0]) auto
hoelzl@56273
  1952
  ultimately have "a = b"
hoelzl@56273
  1953
    by simp
hoelzl@56273
  1954
  with assms show "s = t"
hoelzl@56273
  1955
    by auto
hoelzl@56273
  1956
qed
hoelzl@56273
  1957
hoelzl@56273
  1958
lemma ksimplex_eq_top:
hoelzl@56273
  1959
  assumes a: "a \<in> s" "\<And>a'. a' \<in> s \<Longrightarrow> a' \<le> a"
hoelzl@56273
  1960
  assumes b: "b \<in> t" "\<And>b'. b' \<in> t \<Longrightarrow> b' \<le> b"
hoelzl@56273
  1961
  assumes eq: "s - {a} = t - {b}"
hoelzl@56273
  1962
  shows "s = t"
hoelzl@56273
  1963
proof (cases n)
hoelzl@56273
  1964
  assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp
hoelzl@56273
  1965
next
hoelzl@56273
  1966
  case (Suc n')
hoelzl@56273
  1967
  have "s.enum n = (s.enum n') (u_s n' := Suc (s.enum n' (u_s n')))"
hoelzl@56273
  1968
       "t.enum n = (t.enum n') (u_t n' := Suc (t.enum n' (u_t n')))"
hoelzl@56273
  1969
    using Suc by (simp_all add: s.enum_Suc t.enum_Suc)
hoelzl@56273
  1970
  moreover have en: "a = s.enum n" "b = t.enum n"
hoelzl@56273
  1971
    using a b by (simp_all add: s.enum_n_top t.enum_n_top)
hoelzl@56273
  1972
  moreover
lp15@61609
  1973
  { fix j assume "j < n"
hoelzl@56273
  1974
    moreover have "s - {a} = s.enum ` {0 .. n'}" "t - {b} = t.enum ` {0 .. n'}"
hoelzl@56273
  1975
      unfolding s.s_eq t.s_eq en by (auto simp: s.enum_inj t.enum_inj Suc)
hoelzl@56273
  1976
    ultimately have "s.enum j = t.enum j"
hoelzl@56273
  1977
      using enum_eq[of "0" j n' 0] eq Suc by auto }
hoelzl@56273
  1978
  note enum_eq = this
hoelzl@56273
  1979
  then have "s.enum n' = t.enum n'"
hoelzl@56273
  1980
    using Suc by auto
hoelzl@56273
  1981
  moreover
hoelzl@56273
  1982
  { fix j assume "j < n'"
hoelzl@56273
  1983
    with enum_eq[of j] enum_eq[of "Suc j"]
hoelzl@56273
  1984
    have "u_s j = u_t j"
hoelzl@56273
  1985
      using s.enum_Suc[of j] t.enum_Suc[of j]
nipkow@62390
  1986
      by (auto simp: Suc fun_eq_iff split: if_split_asm) }
hoelzl@56273
  1987
  then have "\<And>j. j < n' \<Longrightarrow> u_s j = u_t j"
hoelzl@56273
  1988
    by (auto simp: gr0_conv_Suc)
hoelzl@56273
  1989
  then have "u_t n' = u_s n'"
hoelzl@56273
  1990
    by (intro bij_betw_singleton_eq[OF t.upd s.upd, of n']) (auto simp: Suc)
hoelzl@56273
  1991
  ultimately have "a = b"
hoelzl@56273
  1992
    by simp
hoelzl@56273
  1993
  with assms show "s = t"
hoelzl@56273
  1994
    by auto
hoelzl@56273
  1995
qed
hoelzl@56273
  1996
hoelzl@56273
  1997
end
hoelzl@56273
  1998
hoelzl@56273
  1999
inductive ksimplex for p n :: nat where
hoelzl@56273
  2000
  ksimplex: "kuhn_simplex p n base upd s \<Longrightarrow> ksimplex p n s"
hoelzl@56273
  2001
hoelzl@56273
  2002
lemma finite_ksimplexes: "finite {s. ksimplex p n s}"
hoelzl@56273
  2003
proof (rule finite_subset)
hoelzl@56273
  2004
  { fix a s assume "ksimplex p n s" "a \<in> s"
hoelzl@56273
  2005
    then obtain b u where "kuhn_simplex p n b u s" by (auto elim: ksimplex.cases)
hoelzl@56273
  2006
    then interpret kuhn_simplex p n b u s .
wenzelm@60420
  2007
    from s_space \<open>a \<in> s\<close> out_eq_p[OF \<open>a \<in> s\<close>]
hoelzl@56273
  2008
    have "a \<in> (\<lambda>f x. if n \<le> x then p else f x) ` ({..< n} \<rightarrow>\<^sub>E {.. p})"
nipkow@62390
  2009
      by (auto simp: image_iff subset_eq Pi_iff split: if_split_asm
hoelzl@56273
  2010
               intro!: bexI[of _ "restrict a {..< n}"]) }
hoelzl@56273
  2011
  then show "{s. ksimplex p n s} \<subseteq> Pow ((\<lambda>f x. if n \<le> x then p else f x) ` ({..< n} \<rightarrow>\<^sub>E {.. p}))"
hoelzl@56273
  2012
    by auto
hoelzl@56273
  2013
qed (simp add: finite_PiE)
hoelzl@56273
  2014
hoelzl@56273
  2015
lemma ksimplex_card:
hoelzl@56273
  2016
  assumes "ksimplex p n s" shows "card s = Suc n"
hoelzl@56273
  2017
using assms proof cases
hoelzl@56273
  2018
  case (ksimplex u b)
hoelzl@56273
  2019
  then interpret kuhn_simplex p n u b s .
hoelzl@56273
  2020
  show ?thesis
hoelzl@56273
  2021
    by (simp add: card_image s_eq inj_enum)
hoelzl@56273
  2022
qed
hoelzl@56273
  2023
hoelzl@56273
  2024
lemma simplex_top_face:
hoelzl@56273
  2025
  assumes "0 < p" "\<forall>x\<in>s'. x n = p"
hoelzl@56273
  2026
  shows "ksimplex p n s' \<longleftrightarrow> (\<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> s' = s - {a})"
hoelzl@56273
  2027
  using assms
hoelzl@56273
  2028
proof safe
hoelzl@56273
  2029
  fix s a assume "ksimplex p (Suc n) s" and a: "a \<in> s" and na: "\<forall>x\<in>s - {a}. x n = p"
hoelzl@56273
  2030
  then show "ksimplex p n (s - {a})"
hoelzl@56273
  2031
  proof cases
hoelzl@56273
  2032
    case (ksimplex base upd)
hoelzl@56273
  2033
    then interpret kuhn_simplex p "Suc n" base upd "s" .
hoelzl@56273
  2034
hoelzl@56273
  2035
    have "a n < p"
wenzelm@60420
  2036
      using one_step[of a n p] na \<open>a\<in>s\<close> s_space by (auto simp: less_le)
hoelzl@56273
  2037
    then have "a = enum 0"
wenzelm@60420
  2038
      using \<open>a \<in> s\<close> na by (subst enum_0_bot) (auto simp: le_less intro!: less[of a _ n])
hoelzl@56273
  2039
    then have s_eq: "s - {a} = enum ` Suc ` {.. n}"
lp15@69700
  2040
      using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident zero_notin_Suc_image in_enum_image subset_eq)
hoelzl@56273
  2041
    then have "enum 1 \<in> s - {a}"
hoelzl@56273
  2042
      by auto
hoelzl@56273
  2043
    then have "upd 0 = n"
wenzelm@60420
  2044
      using \<open>a n < p\<close> \<open>a = enum 0\<close> na[rule_format, of "enum 1"]
nipkow@62390
  2045
      by (auto simp: fun_eq_iff enum_Suc split: if_split_asm)
hoelzl@56273
  2046
    then have "bij_betw upd (Suc ` {..< n}) {..< n}"
hoelzl@56273
  2047
      using upd
hoelzl@56273
  2048
      by (subst notIn_Un_bij_betw3[where b=0])
hoelzl@56273
  2049
         (auto simp: lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0)
hoelzl@56273
  2050
    then have "bij_betw (upd\<circ>Suc) {..<n} {..<n}"
hoelzl@56273
  2051
      by (rule bij_betw_trans[rotated]) (auto simp: bij_betw_def)
hoelzl@56273
  2052
hoelzl@56273
  2053
    have "a n = p - 1"
wenzelm@60420
  2054
      using enum_Suc[of 0] na[rule_format, OF \<open>enum 1 \<in> s - {a}\<close>] \<open>a = enum 0\<close> by (auto simp: \<open>upd 0 = n\<close>)
hoelzl@56273
  2055
hoelzl@56273
  2056
    show ?thesis
wenzelm@61169
  2057
    proof (rule ksimplex.intros, standard)
hoelzl@56273
  2058
      show "bij_betw (upd\<circ>Suc) {..< n} {..< n}" by fact
hoelzl@56273
  2059
      show "base(n := p) \<in> {..<n} \<rightarrow> {..<p}" "\<And>i. n\<le>i \<Longrightarrow> (base(n := p)) i = p"
hoelzl@56273
  2060
        using base base_out by (auto simp: Pi_iff)
hoelzl@56273
  2061
hoelzl@56273
  2062
      have "\<And>i. Suc ` {..< i} = {..< Suc i} - {0}"
hoelzl@56273
  2063
        by (auto simp: image_iff Ball_def) arith
hoelzl@56273
  2064
      then have upd_Suc: "\<And>i. i \<le> n \<Longrightarrow> (upd\<circ>Suc) ` {..< i} = upd ` {..< Suc i} - {n}"
haftmann@69661
  2065
        using \<open>upd 0 = n\<close> upd_inj by (auto simp add: image_iff less_Suc_eq_0_disj)
hoelzl@56273
  2066
      have n_in_upd: "\<And>i. n \<in> upd ` {..< Suc i}"
wenzelm@60420
  2067
        using \<open>upd 0 = n\<close> by auto
hoelzl@56273
  2068
wenzelm@63040
  2069
      define f' where "f' i j =
wenzelm@63040
  2070
        (if j \<in> (upd\<circ>Suc)`{..< i} then Suc ((base(n := p)) j) else (base(n := p)) j)" for i j
haftmann@69661
  2071
      { fix x i
haftmann@69661
  2072
        assume i [arith]: "i \<le> n"
haftmann@69661
  2073
        with upd_Suc have "(upd \<circ> Suc) ` {..<i} = upd ` {..<Suc i} - {n}" .
haftmann@69661
  2074
        with \<open>a n < p\<close> \<open>a = enum 0\<close> \<open>upd 0 = n\<close> \<open>a n = p - 1\<close>
haftmann@69661
  2075
        have "enum (Suc i) x = f' i x"
haftmann@69661
  2076
          by (auto simp add: f'_def enum_def)  }
hoelzl@56273
  2077
      then show "s - {a} = f' ` {.. n}"
hoelzl@56273
  2078
        unfolding s_eq image_comp by (intro image_cong) auto
hoelzl@56273
  2079
    qed
hoelzl@56273
  2080
  qed
hoelzl@56273
  2081
next
hoelzl@56273
  2082
  assume "ksimplex p n s'" and *: "\<forall>x\<in>s'. x n = p"
hoelzl@56273
  2083
  then show "\<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> s' = s - {a}"
hoelzl@56273
  2084
  proof cases
hoelzl@56273
  2085
    case (ksimplex base upd)
hoelzl@56273
  2086
    then interpret kuhn_simplex p n base upd s' .
wenzelm@63040
  2087
    define b where "b = base (n := p - 1)"
wenzelm@63040
  2088
    define u where "u i = (case i of 0 \<Rightarrow> n | Suc i \<Rightarrow> upd i)" for i
hoelzl@56273
  2089
hoelzl@56273
  2090
    have "ksimplex p (Suc n) (s' \<union> {b})"
wenzelm@61169
  2091
    proof (rule ksimplex.intros, standard)
hoelzl@56273
  2092
      show "b \<in> {..<Suc n} \<rightarrow> {..<p}"
wenzelm@60420
  2093
        using base \<open>0 < p\<close> unfolding lessThan_Suc b_def by (auto simp: PiE_iff)
hoelzl@56273
  2094
      show "\<And>i. Suc n \<le> i \<Longrightarrow> b i = p"
hoelzl@56273
  2095
        using base_out by (auto simp: b_def)
hoelzl@56273
  2096
hoelzl@56273
  2097
      have "bij_betw u (Suc ` {..< n} \<union> {0}) ({..<n} \<union> {u 0})"
hoelzl@56273
  2098
        using upd
hoelzl@56273
  2099
        by (intro notIn_Un_bij_betw) (auto simp: u_def bij_betw_def image_comp comp_def inj_on_def)
hoelzl@56273
  2100
      then show "bij_betw u {..<Suc n} {..<Suc n}"
hoelzl@56273
  2101
        by (simp add: u_def lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0)
hoelzl@56273
  2102
wenzelm@63040
  2103
      define f' where "f' i j = (if j \<in> u`{..< i} then Suc (b j) else b j)" for i j
hoelzl@56273
  2104
hoelzl@56273
  2105
      have u_eq: "\<And>i. i \<le> n \<Longrightarrow> u ` {..< Suc i} = upd ` {..< i} \<union> { n }"
hoelzl@56273
  2106
        by (auto simp: u_def image_iff upd_inj Ball_def split: nat.split) arith
hoelzl@56273
  2107
hoelzl@56273
  2108
      { fix x have "x \<le> n \<Longrightarrow> n \<notin> upd ` {..<x}"
hoelzl@56273
  2109
          using upd_space by (simp add: image_iff neq_iff) }
hoelzl@56273
  2110
      note n_not_upd = this
hoelzl@56273
  2111
hoelzl@56273
  2112
      have *: "f' ` {.. Suc n} = f' ` (Suc ` {.. n} \<union> {0})"
hoelzl@56273
  2113
        unfolding atMost_Suc_eq_insert_0 by simp
hoelzl@56273
  2114
      also have "\<dots> = (f' \<circ> Suc) ` {.. n} \<union> {b}"
hoelzl@56273
  2115
        by (auto simp: f'_def)
hoelzl@56273
  2116
      also have "(f' \<circ> Suc) ` {.. n} = s'"
wenzelm@60420
  2117
        using \<open>0 < p\<close> base_out[of n]
hoelzl@56273
  2118
        unfolding s_eq enum_def[abs_def] f'_def[abs_def] upd_space
hoelzl@56273
  2119
        by (intro image_cong) (simp_all add: u_eq b_def fun_eq_iff n_not_upd)
hoelzl@56273
  2120
      finally show "s' \<union> {b} = f' ` {.. Suc n}" ..
hoelzl@56273
  2121
    qed
hoelzl@56273
  2122
    moreover have "b \<notin> s'"
wenzelm@60420
  2123
      using * \<open>0 < p\<close> by (auto simp: b_def)
hoelzl@56273
  2124
    ultimately show ?thesis by auto
hoelzl@56273
  2125
  qed
hoelzl@56273
  2126
qed
hoelzl@56273
  2127
hoelzl@56273
  2128
lemma ksimplex_replace_0:
hoelzl@56273
  2129
  assumes s: "ksimplex p n s" and a: "a \<in> s"
hoelzl@56273
  2130
  assumes j: "j < n" and p: "\<forall>x\<in>s - {a}. x j = 0"
hoelzl@56273
  2131
  shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
hoelzl@56273
  2132
  using s
hoelzl@56273
  2133
proof cases
hoelzl@56273
  2134
  case (ksimplex b_s u_s)
hoelzl@56273
  2135
lp15@61609
  2136
  { fix t b assume "ksimplex p n t"
hoelzl@56273
  2137
    then obtain b_t u_t where "kuhn_simplex p n b_t u_t t"
hoelzl@56273
  2138
      by (auto elim: ksimplex.cases)
hoelzl@56273
  2139
    interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t
hoelzl@56273
  2140
      by intro_locales fact+
hoelzl@56273
  2141
hoelzl@56273
  2142
    assume b: "b \<in> t" "t - {b} = s - {a}"
hoelzl@56273
  2143
    with a j p s.replace_0[of _ a] t.replace_0[of _ b] have "s = t"
hoelzl@56273
  2144
      by (intro ksimplex_eq_top[of a b]) auto }
hoelzl@56273
  2145
  then have "{s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = {s}"
wenzelm@60420
  2146
    using s \<open>a \<in> s\<close> by auto
hoelzl@56273
  2147
  then show ?thesis
hoelzl@56273
  2148
    by simp
hoelzl@56273
  2149
qed
hoelzl@56273
  2150
hoelzl@56273
  2151
lemma ksimplex_replace_1:
hoelzl@56273
  2152
  assumes s: "ksimplex p n s" and a: "a \<in> s"
hoelzl@56273
  2153
  assumes j: "j < n" and p: "\<forall>x\<in>s - {a}. x j = p"
hoelzl@56273
  2154
  shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
hoelzl@56273
  2155
  using s
hoelzl@56273
  2156
proof cases
hoelzl@56273
  2157
  case (ksimplex b_s u_s)
hoelzl@56273
  2158
lp15@61609
  2159
  { fix t b assume "ksimplex p n t"
hoelzl@56273
  2160
    then obtain b_t u_t where "kuhn_simplex p n b_t u_t t"
hoelzl@56273
  2161
      by (auto elim: ksimplex.cases)
hoelzl@56273
  2162
    interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t
hoelzl@56273
  2163
      by intro_locales fact+
hoelzl@56273
  2164
hoelzl@56273
  2165
    assume b: "b \<in> t" "t - {b} = s - {a}"
hoelzl@56273
  2166
    with a j p s.replace_1[of _ a] t.replace_1[of _ b] have "s = t"
hoelzl@56273
  2167
      by (intro ksimplex_eq_bot[of a b]) auto }
hoelzl@56273
  2168
  then have "{s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = {s}"
wenzelm@60420
  2169
    using s \<open>a \<in> s\<close> by auto
hoelzl@56273
  2170
  then show ?thesis
hoelzl@56273
  2171
    by simp
hoelzl@56273
  2172
qed
hoelzl@56273
  2173
hoelzl@56273
  2174
lemma card_2_exists: "card s = 2 \<longleftrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y))"
lp15@68022
  2175
  by (auto simp: card_Suc_eq eval_nat_numeral)
hoelzl@56273
  2176
hoelzl@56273
  2177
lemma ksimplex_replace_2:
hoelzl@56273
  2178
  assumes s: "ksimplex p n s" and "a \<in> s" and "n \<noteq> 0"
hoelzl@56273
  2179
    and lb: "\<forall>j<n. \<exists>x\<in>s - {a}. x j \<noteq> 0"
hoelzl@56273
  2180
    and ub: "\<forall>j<n. \<exists>x\<in>s - {a}. x j \<noteq> p"
hoelzl@56273
  2181
  shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 2"
hoelzl@56273
  2182
  using s
hoelzl@56273
  2183
proof cases
hoelzl@56273
  2184
  case (ksimplex base upd)
hoelzl@56273
  2185
  then interpret kuhn_simplex p n base upd s .
hoelzl@56273
  2186
wenzelm@60420
  2187
  from \<open>a \<in> s\<close> obtain i where "i \<le> n" "a = enum i"
hoelzl@56273
  2188
    unfolding s_eq by auto
hoelzl@56273
  2189
wenzelm@60420
  2190
  from \<open>i \<le> n\<close> have "i = 0 \<or> i = n \<or> (0 < i \<and> i < n)"
hoelzl@56273
  2191
    by linarith
hoelzl@56273
  2192
  then have "\<exists>!s'. s' \<noteq> s \<and> ksimplex p n s' \<and> (\<exists>b\<in>s'. s - {a} = s'- {b})"
hoelzl@56273
  2193
  proof (elim disjE conjE)
hoelzl@56273
  2194
    assume "i = 0"
wenzelm@63040
  2195
    define rot where [abs_def]: "rot i = (if i + 1 = n then 0 else i + 1)" for i
hoelzl@56273
  2196
    let ?upd = "upd \<circ> rot"
hoelzl@56273
  2197
hoelzl@56273
  2198
    have rot: "bij_betw rot {..< n} {..< n}"
hoelzl@56273
  2199
      by (auto simp: bij_betw_def inj_on_def image_iff Ball_def rot_def)
hoelzl@56273
  2200
         arith+
hoelzl@56273
  2201
    from rot upd have "bij_betw ?upd {..<n} {..<n}"
hoelzl@56273
  2202
      by (rule bij_betw_trans)
hoelzl@56273
  2203
wenzelm@63040
  2204
    define f' where [abs_def]: "f' i j =
wenzelm@63040
  2205
      (if j \<in> ?upd`{..< i} then Suc (enum (Suc 0) j) else enum (Suc 0) j)" for i j
hoelzl@56273
  2206
hoelzl@56273
  2207
    interpret b: kuhn_simplex p n "enum (Suc 0)" "upd \<circ> rot" "f' ` {.. n}"
hoelzl@56273
  2208
    proof
wenzelm@60420
  2209
      from \<open>a = enum i\<close> ub \<open>n \<noteq> 0\<close> \<open>i = 0\<close>
hoelzl@56273
  2210
      obtain i' where "i' \<le> n" "enum i' \<noteq> enum 0" "enum i' (upd 0) \<noteq> p"
hoelzl@56273
  2211
        unfolding s_eq by (auto intro: upd_space simp: enum_inj)
hoelzl@56273
  2212
      then have "enum 1 \<le> enum i'" "enum i' (upd 0) < p"
lp15@68022
  2213
        using enum_le_p[of i' "upd 0"] by (auto simp: enum_inj enum_mono upd_space)
hoelzl@56273
  2214
      then have "enum 1 (upd 0) < p"
lp15@68022
  2215
        by (auto simp: le_fun_def intro: le_less_trans)
hoelzl@56273
  2216
      then show "enum (Suc 0) \<in> {..<n} \<rightarrow> {..<p}"
lp15@68022
  2217
        using base \<open>n \<noteq> 0\<close> by (auto simp: enum_0 enum_Suc PiE_iff extensional_def upd_space)
hoelzl@56273
  2218
hoelzl@56273
  2219
      { fix i assume "n \<le> i" then show "enum (Suc 0) i = p"
wenzelm@60420
  2220
        using \<open>n \<noteq> 0\<close> by (auto simp: enum_eq_p) }
hoelzl@56273
  2221
      show "bij_betw ?upd {..<n} {..<n}" by fact
hoelzl@56273
  2222
    qed (simp add: f'_def)
hoelzl@56273
  2223
    have ks_f': "ksimplex p n (f' ` {.. n})"
hoelzl@56273
  2224
      by rule unfold_locales
hoelzl@56273
  2225
hoelzl@56273
  2226
    have b_enum: "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
hoelzl@56273
  2227
    with b.inj_enum have inj_f': "inj_on f' {.. n}" by simp
hoelzl@56273
  2228
haftmann@69661
  2229
    have f'_eq_enum: "f' j = enum (Suc j)" if "j < n" for j
haftmann@69661
  2230
    proof -
haftmann@69661
  2231
      from that have "rot ` {..< j} = {0 <..< Suc j}"
haftmann@69661
  2232
        by (auto simp: rot_def image_Suc_lessThan cong: image_cong_simp)
haftmann@69661
  2233
      with that \<open>n \<noteq> 0\<close> show ?thesis
haftmann@69661
  2234
        by (simp only: f'_def enum_def fun_eq_iff image_comp [symmetric])
haftmann@69661
  2235
          (auto simp add: upd_inj)
haftmann@69661
  2236
    qed
hoelzl@56273
  2237
    then have "enum ` Suc ` {..< n} = f' ` {..< n}"
hoelzl@56273
  2238
      by (force simp: enum_inj)
hoelzl@56273
  2239
    also have "Suc ` {..< n} = {.. n} - {0}"
hoelzl@56273
  2240
      by (auto simp: image_iff Ball_def) arith
hoelzl@56273
  2241
    also have "{..< n} = {.. n} - {n}"
hoelzl@56273
  2242
      by auto
hoelzl@56273
  2243
    finally have eq: "s - {a} = f' ` {.. n} - {f' n}"
wenzelm@60420
  2244
      unfolding s_eq \<open>a = enum i\<close> \<open>i = 0\<close>
nipkow@69286
  2245
      by (simp add: inj_on_image_set_diff[OF inj_enum] inj_on_image_set_diff[OF inj_f'])
hoelzl@56273
  2246
hoelzl@56273
  2247
    have "enum 0 < f' 0"
wenzelm@60420
  2248
      using \<open>n \<noteq> 0\<close> by (simp add: enum_strict_mono f'_eq_enum)
hoelzl@56273
  2249
    also have "\<dots> < f' n"
wenzelm@60420
  2250
      using \<open>n \<noteq> 0\<close> b.enum_strict_mono[of 0 n] unfolding b_enum by simp
hoelzl@56273
  2251
    finally have "a \<noteq> f' n"
wenzelm@60420
  2252
      using \<open>a = enum i\<close> \<open>i = 0\<close> by auto
hoelzl@56273
  2253
hoelzl@56273
  2254
    { fix t c assume "ksimplex p n t" "c \<in> t" and eq_sma: "s - {a} = t - {c}"
hoelzl@56273
  2255
      obtain b u where "kuhn_simplex p n b u t"
wenzelm@60420
  2256
        using \<open>ksimplex p n t\<close> by (auto elim: ksimplex.cases)
hoelzl@56273
  2257
      then interpret t: kuhn_simplex p n b u t .
hoelzl@56273
  2258
hoelzl@56273
  2259
      { fix x assume "x \<in> s" "x \<noteq> a"
hoelzl@56273
  2260
         then have "x (upd 0) = enum (Suc 0) (upd 0)"
wenzelm@60420
  2261
           by (auto simp: \<open>a = enum i\<close> \<open>i = 0\<close> s_eq enum_def enum_inj) }
hoelzl@56273
  2262
      then have eq_upd0: "\<forall>x\<in>t-{c}. x (upd 0) = enum (Suc 0) (upd 0)"
hoelzl@56273
  2263
        unfolding eq_sma[symmetric] by auto
hoelzl@56273
  2264
      then have "c (upd 0) \<noteq> enum (Suc 0) (upd 0)"
wenzelm@60420
  2265
        using \<open>n \<noteq> 0\<close> by (intro t.one_step[OF \<open>c\<in>t\<close> ]) (auto simp: upd_space)
hoelzl@56273
  2266
      then have "c (upd 0) < enum (Suc 0) (upd 0) \<or> c (upd 0) > enum (Suc 0) (upd 0)"
hoelzl@56273
  2267
        by auto
hoelzl@56273
  2268
      then have "t = s \<or> t = f' ` {..n}"
hoelzl@56273
  2269
      proof (elim disjE conjE)
hoelzl@56273
  2270
        assume *: "c (upd 0) < enum (Suc 0) (upd 0)"
hoelzl@56273
  2271
        interpret st: kuhn_simplex_pair p n base upd s b u t ..
wenzelm@60420
  2272
        { fix x assume "x \<in> t" with * \<open>c\<in>t\<close> eq_upd0[rule_format, of x] have "c \<le> x"
hoelzl@56273
  2273
            by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
hoelzl@56273
  2274
        note top = this
hoelzl@56273
  2275
        have "s = t"
wenzelm@60420
  2276
          using \<open>a = enum i\<close> \<open>i = 0\<close> \<open>c \<in> t\<close>
hoelzl@56273
  2277
          by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq_sma])
hoelzl@56273
  2278
             (auto simp: s_eq enum_mono t.s_eq t.enum_mono top)
hoelzl@56273
  2279
        then show ?thesis by simp
hoelzl@56273
  2280
      next
hoelzl@56273
  2281
        assume *: "c (upd 0) > enum (Suc 0) (upd 0)"
hoelzl@56273
  2282
        interpret st: kuhn_simplex_pair p n "enum (Suc 0)" "upd \<circ> rot" "f' ` {.. n}" b u t ..
hoelzl@56273
  2283
        have eq: "f' ` {..n} - {f' n} = t - {c}"
hoelzl@56273
  2284
          using eq_sma eq by simp
wenzelm@60420
  2285
        { fix x assume "x \<in> t" with * \<open>c\<in>t\<close> eq_upd0[rule_format, of x] have "x \<le> c"
hoelzl@56273
  2286
            by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
hoelzl@56273
  2287
        note top = this
hoelzl@56273
  2288
        have "f' ` {..n} = t"
wenzelm@60420
  2289
          using \<open>a = enum i\<close> \<open>i = 0\<close> \<open>c \<in> t\<close>
hoelzl@56273
  2290
          by (intro st.ksimplex_eq_top[OF _ _ _ _ eq])
hoelzl@56273
  2291
             (auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono b_enum[symmetric] top)
hoelzl@56273
  2292
        then show ?thesis by simp
hoelzl@56273
  2293
      qed }
wenzelm@60420
  2294
    with ks_f' eq \<open>a \<noteq> f' n\<close> \<open>n \<noteq> 0\<close> show ?thesis
hoelzl@56273
  2295
      apply (intro ex1I[of _ "f' ` {.. n}"])
hoelzl@56273
  2296
      apply auto []
hoelzl@56273
  2297
      apply metis
hoelzl@56273
  2298
      done
hoelzl@56273
  2299
  next
hoelzl@56273
  2300
    assume "i = n"
wenzelm@60420
  2301
    from \<open>n \<noteq> 0\<close> obtain n' where n': "n = Suc n'"
hoelzl@56273
  2302
      by (cases n) auto
hoelzl@56273
  2303
wenzelm@63040
  2304
    define rot where "rot i = (case i of 0 \<Rightarrow> n' | Suc i \<Rightarrow> i)" for i
hoelzl@56273
  2305
    let ?upd = "upd \<circ> rot"
hoelzl@56273
  2306
hoelzl@56273
  2307
    have rot: "bij_betw rot {..< n} {..< n}"
hoelzl@56273
  2308
      by (auto simp: bij_betw_def inj_on_def image_iff Bex_def rot_def n' split: nat.splits)
hoelzl@56273
  2309
         arith
hoelzl@56273
  2310
    from rot upd have "bij_betw ?upd {..<n} {..<n}"
hoelzl@56273
  2311
      by (rule bij_betw_trans)
hoelzl@56273
  2312
wenzelm@63040
  2313
    define b where "b = base (upd n' := base (upd n') - 1)"
wenzelm@63040
  2314
    define f' where [abs_def]: "f' i j = (if j \<in> ?upd`{..< i} then Suc (b j) else b j)" for i j
hoelzl@56273
  2315
hoelzl@56273
  2316
    interpret b: kuhn_simplex p n b "upd \<circ> rot" "f' ` {.. n}"
hoelzl@56273
  2317
    proof
hoelzl@56273
  2318
      { fix i assume "n \<le> i" then show "b i = p"
hoelzl@56273
  2319
          using base_out[of i] upd_space[of n'] by (auto simp: b_def n') }
hoelzl@56273
  2320
      show "b \<in> {..<n} \<rightarrow> {..<p}"
wenzelm@60420
  2321
        using base \<open>n \<noteq> 0\<close> upd_space[of n']
hoelzl@56273
  2322
        by (auto simp: b_def PiE_def Pi_iff Ball_def upd_space extensional_def n')
hoelzl@56273
  2323
hoelzl@56273
  2324
      show "bij_betw ?upd {..<n} {..<n}" by fact
hoelzl@56273
  2325
    qed (simp add: f'_def)
hoelzl@56273
  2326
    have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
hoelzl@56273
  2327
    have ks_f': "ksimplex p n (b.enum ` {.. n})"
hoelzl@56273
  2328
      unfolding f' by rule unfold_locales
hoelzl@56273
  2329
lp15@61609
  2330
    have "0 < n"
wenzelm@60420
  2331
      using \<open>n \<noteq> 0\<close> by auto
hoelzl@56273
  2332
wenzelm@60420
  2333
    { from \<open>a = enum i\<close> \<open>n \<noteq> 0\<close> \<open>i = n\<close> lb upd_space[of n']
hoelzl@56273
  2334
      obtain i' where "i' \<le> n" "enum i' \<noteq> enum n" "0 < enum i' (upd n')"
hoelzl@56273
  2335
        unfolding s_eq by (auto simp: enum_inj n')
hoelzl@56273
  2336
      moreover have "enum i' (upd n') = base (upd n')"
wenzelm@60420
  2337
        unfolding enum_def using \<open>i' \<le> n\<close> \<open>enum i' \<noteq> enum n\<close> by (auto simp: n' upd_inj enum_inj)
hoelzl@56273
  2338
      ultimately have "0 < base (upd n')"
hoelzl@56273
  2339
        by auto }
hoelzl@56273
  2340
    then have benum1: "b.enum (Suc 0) = base"
wenzelm@60420
  2341
      unfolding b.enum_Suc[OF \<open>0<n\<close>] b.enum_0 by (auto simp: b_def rot_def)
hoelzl@56273
  2342
hoelzl@56273
  2343
    have [simp]: "\<And>j. Suc j < n \<Longrightarrow> rot ` {..< Suc j} = {n'} \<union> {..< j}"
hoelzl@56273
  2344
      by (auto simp: rot_def image_iff Ball_def split: nat.splits)
hoelzl@56273
  2345
    have rot_simps: "\<And>j. rot (Suc j) = j" "rot 0 = n'"
hoelzl@56273
  2346
      by (simp_all add: rot_def)
hoelzl@56273
  2347
hoelzl@56273
  2348
    { fix j assume j: "Suc j \<le> n" then have "b.enum (Suc j) = enum j"
lp15@68022
  2349
        by (induct j) (auto simp: benum1 enum_0 b.enum_Suc enum_Suc rot_simps) }
hoelzl@56273
  2350
    note b_enum_eq_enum = this
hoelzl@56273
  2351
    then have "enum ` {..< n} = b.enum ` Suc ` {..< n}"
lp15@68022
  2352
      by (auto simp: image_comp intro!: image_cong)
hoelzl@56273
  2353
    also have "Suc ` {..< n} = {.. n} - {0}"
hoelzl@56273
  2354
      by (auto simp: image_iff Ball_def) arith
hoelzl@56273
  2355
    also have "{..< n} = {.. n} - {n}"
hoelzl@56273
  2356
      by auto
hoelzl@56273
  2357
    finally have eq: "s - {a} = b.enum ` {.. n} - {b.enum 0}"
wenzelm@60420
  2358
      unfolding s_eq \<open>a = enum i\<close> \<open>i = n\<close>
paulson@60303
  2359
      using inj_on_image_set_diff[OF inj_enum Diff_subset, of "{n}"]
paulson@60303
  2360
            inj_on_image_set_diff[OF b.inj_enum Diff_subset, of "{0}"]
lp15@68022
  2361
      by (simp add: comp_def)
hoelzl@56273
  2362
hoelzl@56273
  2363
    have "b.enum 0 \<le> b.enum n"
hoelzl@56273
  2364
      by (simp add: b.enum_mono)
hoelzl@56273
  2365
    also have "b.enum n < enum n"
wenzelm@60420
  2366
      using \<open>n \<noteq> 0\<close> by (simp add: enum_strict_mono b_enum_eq_enum n')
hoelzl@56273
  2367
    finally have "a \<noteq> b.enum 0"
wenzelm@60420
  2368
      using \<open>a = enum i\<close> \<open>i = n\<close> by auto
hoelzl@56273
  2369
hoelzl@56273
  2370
    { fix t c assume "ksimplex p n t" "c \<in> t" and eq_sma: "s - {a} = t - {c}"
hoelzl@56273
  2371
      obtain b' u where "kuhn_simplex p n b' u t"
wenzelm@60420
  2372
        using \<open>ksimplex p n t\<close> by (auto elim: ksimplex.cases)
hoelzl@56273
  2373
      then interpret t: kuhn_simplex p n b' u t .
hoelzl@56273
  2374
hoelzl@56273
  2375
      { fix x assume "x \<in> s" "x \<noteq> a"
hoelzl@56273
  2376
         then have "x (upd n') = enum n' (upd n')"
wenzelm@60420
  2377
           by (auto simp: \<open>a = enum i\<close> n' \<open>i = n\<close> s_eq enum_def enum_inj in_upd_image) }
hoelzl@56273
  2378
      then have eq_upd0: "\<forall>x\<in>t-{c}. x (upd n') = enum n' (upd n')"
hoelzl@56273
  2379
        unfolding eq_sma[symmetric] by auto
hoelzl@56273
  2380
      then have "c (upd n') \<noteq> enum n' (upd n')"
wenzelm@60420
  2381
        using \<open>n \<noteq> 0\<close> by (intro t.one_step[OF \<open>c\<in>t\<close> ]) (auto simp: n' upd_space[unfolded n'])
hoelzl@56273
  2382
      then have "c (upd n') < enum n' (upd n') \<or> c (upd n') > enum n' (upd n')"
hoelzl@56273
  2383
        by auto
hoelzl@56273
  2384
      then have "t = s \<or> t = b.enum ` {..n}"
hoelzl@56273
  2385
      proof (elim disjE conjE)
hoelzl@56273
  2386
        assume *: "c (upd n') > enum n' (upd n')"
hoelzl@56273
  2387
        interpret st: kuhn_simplex_pair p n base upd s b' u t ..
wenzelm@60420
  2388
        { fix x assume "x \<in> t" with * \<open>c\<in>t\<close> eq_upd0[rule_format, of x] have "x \<le> c"
hoelzl@56273
  2389
            by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) }
hoelzl@56273
  2390
        note top = this
hoelzl@56273
  2391
        have "s = t"
wenzelm@60420
  2392
          using \<open>a = enum i\<close> \<open>i = n\<close> \<open>c \<in> t\<close>
hoelzl@56273
  2393
          by (intro st.ksimplex_eq_top[OF _ _ _ _ eq_sma])