src/HOL/Analysis/Brouwer_Fixpoint.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 19 16:44:45 2018 +0000 (18 months ago)
changeset 67673 c8caefb20564
parent 67443 3abf6a722518
child 67682 00c436488398
permissions -rw-r--r--
lots of new material, ultimately related to measure theory
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
(* ========================================================================= *)
hoelzl@33741
     6
(* Results connected with topological dimension.                             *)
hoelzl@33741
     7
(*                                                                           *)
hoelzl@33741
     8
(* At the moment this is just Brouwer's fixpoint theorem. The proof is from  *)
hoelzl@33741
     9
(* Kuhn: "some combinatorial lemmas in topology", IBM J. v4. (1960) p. 518   *)
hoelzl@33741
    10
(* See "http://www.research.ibm.com/journal/rd/045/ibmrd0405K.pdf".          *)
hoelzl@33741
    11
(*                                                                           *)
hoelzl@33741
    12
(* The script below is quite messy, but at least we avoid formalizing any    *)
hoelzl@33741
    13
(* topological machinery; we don't even use barycentric subdivision; this is *)
hoelzl@33741
    14
(* the big advantage of Kuhn's proof over the usual Sperner's lemma one.     *)
hoelzl@33741
    15
(*                                                                           *)
hoelzl@33741
    16
(*              (c) Copyright, John Harrison 1998-2008                       *)
hoelzl@33741
    17
(* ========================================================================= *)
hoelzl@33741
    18
wenzelm@60420
    19
section \<open>Results connected with topological dimension.\<close>
hoelzl@33741
    20
hoelzl@33741
    21
theory Brouwer_Fixpoint
lp15@63129
    22
imports Path_Connected Homeomorphism
hoelzl@33741
    23
begin
hoelzl@33741
    24
hoelzl@56273
    25
lemma bij_betw_singleton_eq:
hoelzl@56273
    26
  assumes f: "bij_betw f A B" and g: "bij_betw g A B" and a: "a \<in> A"
hoelzl@56273
    27
  assumes eq: "(\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x = g x)"
hoelzl@56273
    28
  shows "f a = g a"
hoelzl@56273
    29
proof -
hoelzl@56273
    30
  have "f ` (A - {a}) = g ` (A - {a})"
hoelzl@56273
    31
    by (intro image_cong) (simp_all add: eq)
hoelzl@56273
    32
  then have "B - {f a} = B - {g a}"
paulson@60303
    33
    using f g a  by (auto simp: bij_betw_def inj_on_image_set_diff set_eq_iff Diff_subset)
hoelzl@56273
    34
  moreover have "f a \<in> B" "g a \<in> B"
hoelzl@56273
    35
    using f g a by (auto simp: bij_betw_def)
hoelzl@56273
    36
  ultimately show ?thesis
hoelzl@56273
    37
    by auto
hoelzl@56273
    38
qed
hoelzl@56273
    39
hoelzl@56273
    40
lemma swap_image:
hoelzl@56273
    41
  "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
    42
                                  else (if j \<in> A then f ` ((A - {j}) \<union> {i}) else f ` A))"
hoelzl@56273
    43
  apply (auto simp: Fun.swap_def image_iff)
hoelzl@56273
    44
  apply metis
hoelzl@56273
    45
  apply (metis member_remove remove_def)
hoelzl@56273
    46
  apply (metis member_remove remove_def)
hoelzl@56273
    47
  done
hoelzl@56273
    48
haftmann@63365
    49
lemmas swap_apply1 = swap_apply(1)
haftmann@63365
    50
lemmas swap_apply2 = swap_apply(2)
haftmann@63365
    51
lemmas lessThan_empty_iff = Iio_eq_empty_iff_nat
haftmann@63365
    52
lemmas Zero_notin_Suc = zero_notin_Suc_image
haftmann@63365
    53
lemmas atMost_Suc_eq_insert_0 = Iic_Suc_eq_insert_0
hoelzl@56273
    54
hoelzl@56273
    55
lemma pointwise_minimal_pointwise_maximal:
hoelzl@56273
    56
  fixes s :: "(nat \<Rightarrow> nat) set"
hoelzl@56273
    57
  assumes "finite s"
hoelzl@56273
    58
    and "s \<noteq> {}"
hoelzl@56273
    59
    and "\<forall>x\<in>s. \<forall>y\<in>s. x \<le> y \<or> y \<le> x"
hoelzl@56273
    60
  shows "\<exists>a\<in>s. \<forall>x\<in>s. a \<le> x"
hoelzl@56273
    61
    and "\<exists>a\<in>s. \<forall>x\<in>s. x \<le> a"
hoelzl@56273
    62
  using assms
hoelzl@56273
    63
proof (induct s rule: finite_ne_induct)
hoelzl@56273
    64
  case (insert b s)
hoelzl@56273
    65
  assume *: "\<forall>x\<in>insert b s. \<forall>y\<in>insert b s. x \<le> y \<or> y \<le> x"
wenzelm@63540
    66
  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
    67
    using insert by auto
wenzelm@63540
    68
  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
    69
    using *[rule_format, of b u] *[rule_format, of b l] by (metis insert_iff order.trans)+
hoelzl@56273
    70
qed auto
hoelzl@50526
    71
hoelzl@33741
    72
lemma brouwer_compactness_lemma:
huffman@56226
    73
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
wenzelm@53674
    74
  assumes "compact s"
wenzelm@53674
    75
    and "continuous_on s f"
wenzelm@53688
    76
    and "\<not> (\<exists>x\<in>s. f x = 0)"
wenzelm@53674
    77
  obtains d where "0 < d" and "\<forall>x\<in>s. d \<le> norm (f x)"
wenzelm@53185
    78
proof (cases "s = {}")
wenzelm@53674
    79
  case True
wenzelm@53688
    80
  show thesis
wenzelm@53688
    81
    by (rule that [of 1]) (auto simp: True)
wenzelm@53674
    82
next
wenzelm@49374
    83
  case False
wenzelm@49374
    84
  have "continuous_on s (norm \<circ> f)"
hoelzl@56371
    85
    by (rule continuous_intros continuous_on_norm assms(2))+
wenzelm@53674
    86
  with False obtain x where x: "x \<in> s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"
wenzelm@53674
    87
    using continuous_attains_inf[OF assms(1), of "norm \<circ> f"]
wenzelm@53674
    88
    unfolding o_def
wenzelm@53674
    89
    by auto
wenzelm@53674
    90
  have "(norm \<circ> f) x > 0"
wenzelm@53674
    91
    using assms(3) and x(1)
wenzelm@53674
    92
    by auto
wenzelm@53674
    93
  then show ?thesis
wenzelm@53674
    94
    by (rule that) (insert x(2), auto simp: o_def)
wenzelm@49555
    95
qed
hoelzl@33741
    96
wenzelm@49555
    97
lemma kuhn_labelling_lemma:
hoelzl@50526
    98
  fixes P Q :: "'a::euclidean_space \<Rightarrow> bool"
hoelzl@56273
    99
  assumes "\<forall>x. P x \<longrightarrow> P (f x)"
hoelzl@50526
   100
    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
   101
  shows "\<exists>l. (\<forall>x.\<forall>i\<in>Basis. l x i \<le> (1::nat)) \<and>
hoelzl@50526
   102
             (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 0) \<longrightarrow> (l x i = 0)) \<and>
hoelzl@50526
   103
             (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 1) \<longrightarrow> (l x i = 1)) \<and>
hoelzl@56273
   104
             (\<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
   105
             (\<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
   106
proof -
hoelzl@56273
   107
  { fix x i
hoelzl@56273
   108
    let ?R = "\<lambda>y. (P x \<and> Q i \<and> x \<bullet> i = 0 \<longrightarrow> y = (0::nat)) \<and>
hoelzl@56273
   109
        (P x \<and> Q i \<and> x \<bullet> i = 1 \<longrightarrow> y = 1) \<and>
hoelzl@56273
   110
        (P x \<and> Q i \<and> y = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i) \<and>
hoelzl@56273
   111
        (P x \<and> Q i \<and> y = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i)"
hoelzl@56273
   112
    { 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
   113
    then have "i \<in> Basis \<Longrightarrow> ?R 0 \<or> ?R 1" by auto }
hoelzl@56273
   114
  then show ?thesis
hoelzl@56273
   115
    unfolding all_conj_distrib[symmetric] Ball_def (* FIXME: shouldn't this work by metis? *)
hoelzl@56273
   116
    by (subst choice_iff[symmetric])+ blast
wenzelm@49374
   117
qed
wenzelm@49374
   118
wenzelm@53185
   119
wenzelm@60420
   120
subsection \<open>The key "counting" observation, somewhat abstracted.\<close>
hoelzl@33741
   121
wenzelm@53252
   122
lemma kuhn_counting_lemma:
hoelzl@56273
   123
  fixes bnd compo compo' face S F
hoelzl@56273
   124
  defines "nF s == card {f\<in>F. face f s \<and> compo' f}"
wenzelm@67443
   125
  assumes [simp, intro]: "finite F" \<comment> \<open>faces\<close> and [simp, intro]: "finite S" \<comment> \<open>simplices\<close>
hoelzl@56273
   126
    and "\<And>f. f \<in> F \<Longrightarrow> bnd f \<Longrightarrow> card {s\<in>S. face f s} = 1"
hoelzl@56273
   127
    and "\<And>f. f \<in> F \<Longrightarrow> \<not> bnd f \<Longrightarrow> card {s\<in>S. face f s} = 2"
hoelzl@56273
   128
    and "\<And>s. s \<in> S \<Longrightarrow> compo s \<Longrightarrow> nF s = 1"
hoelzl@56273
   129
    and "\<And>s. s \<in> S \<Longrightarrow> \<not> compo s \<Longrightarrow> nF s = 0 \<or> nF s = 2"
hoelzl@56273
   130
    and "odd (card {f\<in>F. compo' f \<and> bnd f})"
hoelzl@56273
   131
  shows "odd (card {s\<in>S. compo s})"
wenzelm@53185
   132
proof -
hoelzl@56273
   133
  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
   134
    by (subst sum.union_disjoint[symmetric]) (auto intro!: sum.cong)
hoelzl@56273
   135
  also have "\<dots> = (\<Sum>s\<in>S. card {f \<in> {f\<in>F. compo' f \<and> bnd f}. face f s}) +
hoelzl@56273
   136
                  (\<Sum>s\<in>S. card {f \<in> {f\<in>F. compo' f \<and> \<not> bnd f}. face f s})"
nipkow@64267
   137
    unfolding sum.distrib[symmetric]
hoelzl@56273
   138
    by (subst card_Un_disjoint[symmetric])
nipkow@64267
   139
       (auto simp: nF_def intro!: sum.cong arg_cong[where f=card])
hoelzl@56273
   140
  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
   141
    using assms(4,5) by (fastforce intro!: arg_cong2[where f="(+)"] sum_multicount)
hoelzl@56273
   142
  finally have "odd ((\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) + card {s\<in>S. compo s})"
hoelzl@56273
   143
    using assms(6,8) by simp
hoelzl@56273
   144
  moreover have "(\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) =
hoelzl@56273
   145
    (\<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
   146
    using assms(7) by (subst sum.union_disjoint[symmetric]) (fastforce intro!: sum.cong)+
wenzelm@53688
   147
  ultimately show ?thesis
wenzelm@53688
   148
    by auto
wenzelm@53186
   149
qed
wenzelm@53186
   150
wenzelm@60420
   151
subsection \<open>The odd/even result for faces of complete vertices, generalized.\<close>
hoelzl@56273
   152
hoelzl@56273
   153
lemma kuhn_complete_lemma:
hoelzl@56273
   154
  assumes [simp]: "finite simplices"
hoelzl@56273
   155
    and face: "\<And>f s. face f s \<longleftrightarrow> (\<exists>a\<in>s. f = s - {a})"
hoelzl@56273
   156
    and card_s[simp]:  "\<And>s. s \<in> simplices \<Longrightarrow> card s = n + 2"
hoelzl@56273
   157
    and rl_bd: "\<And>s. s \<in> simplices \<Longrightarrow> rl ` s \<subseteq> {..Suc n}"
hoelzl@56273
   158
    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
   159
    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
   160
    and odd_card: "odd (card {f. (\<exists>s\<in>simplices. face f s) \<and> rl ` f = {..n} \<and> bnd f})"
hoelzl@56273
   161
  shows "odd (card {s\<in>simplices. (rl ` s = {..Suc n})})"
hoelzl@56273
   162
proof (rule kuhn_counting_lemma)
hoelzl@56273
   163
  have finite_s[simp]: "\<And>s. s \<in> simplices \<Longrightarrow> finite s"
lp15@61609
   164
    by (metis add_is_0 zero_neq_numeral card_infinite assms(3))
hoelzl@56273
   165
hoelzl@56273
   166
  let ?F = "{f. \<exists>s\<in>simplices. face f s}"
hoelzl@56273
   167
  have F_eq: "?F = (\<Union>s\<in>simplices. \<Union>a\<in>s. {s - {a}})"
hoelzl@56273
   168
    by (auto simp: face)
hoelzl@56273
   169
  show "finite ?F"
wenzelm@60420
   170
    using \<open>finite simplices\<close> unfolding F_eq by auto
hoelzl@56273
   171
wenzelm@60421
   172
  show "card {s \<in> simplices. face f s} = 1" if "f \<in> ?F" "bnd f" for f
wenzelm@60449
   173
    using bnd that by auto
hoelzl@56273
   174
wenzelm@60421
   175
  show "card {s \<in> simplices. face f s} = 2" if "f \<in> ?F" "\<not> bnd f" for f
wenzelm@60449
   176
    using nbnd that by auto
hoelzl@56273
   177
hoelzl@56273
   178
  show "odd (card {f \<in> {f. \<exists>s\<in>simplices. face f s}. rl ` f = {..n} \<and> bnd f})"
hoelzl@56273
   179
    using odd_card by simp
hoelzl@56273
   180
hoelzl@56273
   181
  fix s assume s[simp]: "s \<in> simplices"
hoelzl@56273
   182
  let ?S = "{f \<in> {f. \<exists>s\<in>simplices. face f s}. face f s \<and> rl ` f = {..n}}"
hoelzl@56273
   183
  have "?S = (\<lambda>a. s - {a}) ` {a\<in>s. rl ` (s - {a}) = {..n}}"
hoelzl@56273
   184
    using s by (fastforce simp: face)
hoelzl@56273
   185
  then have card_S: "card ?S = card {a\<in>s. rl ` (s - {a}) = {..n}}"
hoelzl@56273
   186
    by (auto intro!: card_image inj_onI)
hoelzl@56273
   187
hoelzl@56273
   188
  { assume rl: "rl ` s = {..Suc n}"
hoelzl@56273
   189
    then have inj_rl: "inj_on rl s"
hoelzl@56273
   190
      by (intro eq_card_imp_inj_on) auto
hoelzl@56273
   191
    moreover obtain a where "rl a = Suc n" "a \<in> s"
hoelzl@56273
   192
      by (metis atMost_iff image_iff le_Suc_eq rl)
hoelzl@56273
   193
    ultimately have n: "{..n} = rl ` (s - {a})"
paulson@60303
   194
      by (auto simp add: inj_on_image_set_diff Diff_subset rl)
hoelzl@56273
   195
    have "{a\<in>s. rl ` (s - {a}) = {..n}} = {a}"
wenzelm@60420
   196
      using inj_rl \<open>a \<in> s\<close> by (auto simp add: n inj_on_image_eq_iff[OF inj_rl] Diff_subset)
hoelzl@56273
   197
    then show "card ?S = 1"
hoelzl@56273
   198
      unfolding card_S by simp }
hoelzl@56273
   199
hoelzl@56273
   200
  { assume rl: "rl ` s \<noteq> {..Suc n}"
hoelzl@56273
   201
    show "card ?S = 0 \<or> card ?S = 2"
hoelzl@56273
   202
    proof cases
hoelzl@56273
   203
      assume *: "{..n} \<subseteq> rl ` s"
hoelzl@56273
   204
      with rl rl_bd[OF s] have rl_s: "rl ` s = {..n}"
nipkow@62390
   205
        by (auto simp add: atMost_Suc subset_insert_iff split: if_split_asm)
hoelzl@56273
   206
      then have "\<not> inj_on rl s"
hoelzl@56273
   207
        by (intro pigeonhole) simp
hoelzl@56273
   208
      then obtain a b where ab: "a \<in> s" "b \<in> s" "rl a = rl b" "a \<noteq> b"
hoelzl@56273
   209
        by (auto simp: inj_on_def)
hoelzl@56273
   210
      then have eq: "rl ` (s - {a}) = rl ` s"
hoelzl@56273
   211
        by auto
hoelzl@56273
   212
      with ab have inj: "inj_on rl (s - {a})"
hoelzl@56273
   213
        by (intro eq_card_imp_inj_on) (auto simp add: rl_s card_Diff_singleton_if)
hoelzl@56273
   214
hoelzl@56273
   215
      { fix x assume "x \<in> s" "x \<notin> {a, b}"
hoelzl@56273
   216
        then have "rl ` s - {rl x} = rl ` ((s - {a}) - {x})"
paulson@60303
   217
          by (auto simp: eq Diff_subset inj_on_image_set_diff[OF inj])
hoelzl@56273
   218
        also have "\<dots> = rl ` (s - {x})"
wenzelm@60420
   219
          using ab \<open>x \<notin> {a, b}\<close> by auto
hoelzl@56273
   220
        also assume "\<dots> = rl ` s"
hoelzl@56273
   221
        finally have False
wenzelm@60420
   222
          using \<open>x\<in>s\<close> by auto }
hoelzl@56273
   223
      moreover
hoelzl@56273
   224
      { fix x assume "x \<in> {a, b}" with ab have "x \<in> s \<and> rl ` (s - {x}) = rl ` s"
hoelzl@56273
   225
          by (simp add: set_eq_iff image_iff Bex_def) metis }
hoelzl@56273
   226
      ultimately have "{a\<in>s. rl ` (s - {a}) = {..n}} = {a, b}"
hoelzl@56273
   227
        unfolding rl_s[symmetric] by fastforce
wenzelm@60420
   228
      with \<open>a \<noteq> b\<close> show "card ?S = 0 \<or> card ?S = 2"
hoelzl@56273
   229
        unfolding card_S by simp
hoelzl@56273
   230
    next
hoelzl@56273
   231
      assume "\<not> {..n} \<subseteq> rl ` s"
hoelzl@56273
   232
      then have "\<And>x. rl ` (s - {x}) \<noteq> {..n}"
hoelzl@56273
   233
        by auto
hoelzl@56273
   234
      then show "card ?S = 0 \<or> card ?S = 2"
hoelzl@56273
   235
        unfolding card_S by simp
hoelzl@56273
   236
    qed }
hoelzl@56273
   237
qed fact
hoelzl@56273
   238
hoelzl@56273
   239
locale kuhn_simplex =
hoelzl@56273
   240
  fixes p n and base upd and s :: "(nat \<Rightarrow> nat) set"
hoelzl@56273
   241
  assumes base: "base \<in> {..< n} \<rightarrow> {..< p}"
hoelzl@56273
   242
  assumes base_out: "\<And>i. n \<le> i \<Longrightarrow> base i = p"
hoelzl@56273
   243
  assumes upd: "bij_betw upd {..< n} {..< n}"
hoelzl@56273
   244
  assumes s_pre: "s = (\<lambda>i j. if j \<in> upd`{..< i} then Suc (base j) else base j) ` {.. n}"
hoelzl@56273
   245
begin
hoelzl@56273
   246
hoelzl@56273
   247
definition "enum i j = (if j \<in> upd`{..< i} then Suc (base j) else base j)"
hoelzl@56273
   248
hoelzl@56273
   249
lemma s_eq: "s = enum ` {.. n}"
hoelzl@56273
   250
  unfolding s_pre enum_def[abs_def] ..
hoelzl@56273
   251
hoelzl@56273
   252
lemma upd_space: "i < n \<Longrightarrow> upd i < n"
hoelzl@56273
   253
  using upd by (auto dest!: bij_betwE)
hoelzl@56273
   254
hoelzl@56273
   255
lemma s_space: "s \<subseteq> {..< n} \<rightarrow> {.. p}"
hoelzl@56273
   256
proof -
hoelzl@56273
   257
  { fix i assume "i \<le> n" then have "enum i \<in> {..< n} \<rightarrow> {.. p}"
hoelzl@56273
   258
    proof (induct i)
hoelzl@56273
   259
      case 0 then show ?case
hoelzl@56273
   260
        using base by (auto simp: Pi_iff less_imp_le enum_def)
hoelzl@56273
   261
    next
hoelzl@56273
   262
      case (Suc i) with base show ?case
hoelzl@56273
   263
        by (auto simp: Pi_iff Suc_le_eq less_imp_le enum_def intro: upd_space)
hoelzl@56273
   264
    qed }
hoelzl@56273
   265
  then show ?thesis
hoelzl@56273
   266
    by (auto simp: s_eq)
hoelzl@56273
   267
qed
hoelzl@56273
   268
hoelzl@56273
   269
lemma inj_upd: "inj_on upd {..< n}"
hoelzl@56273
   270
  using upd by (simp add: bij_betw_def)
hoelzl@56273
   271
hoelzl@56273
   272
lemma inj_enum: "inj_on enum {.. n}"
hoelzl@56273
   273
proof -
hoelzl@56273
   274
  { fix x y :: nat assume "x \<noteq> y" "x \<le> n" "y \<le> n"
hoelzl@56273
   275
    with upd have "upd ` {..< x} \<noteq> upd ` {..< y}"
lp15@61609
   276
      by (subst inj_on_image_eq_iff[where C="{..< n}"]) (auto simp: bij_betw_def)
hoelzl@56273
   277
    then have "enum x \<noteq> enum y"
hoelzl@56273
   278
      by (auto simp add: enum_def fun_eq_iff) }
hoelzl@56273
   279
  then show ?thesis
hoelzl@56273
   280
    by (auto simp: inj_on_def)
hoelzl@56273
   281
qed
hoelzl@56273
   282
hoelzl@56273
   283
lemma enum_0: "enum 0 = base"
hoelzl@56273
   284
  by (simp add: enum_def[abs_def])
hoelzl@56273
   285
hoelzl@56273
   286
lemma base_in_s: "base \<in> s"
hoelzl@56273
   287
  unfolding s_eq by (subst enum_0[symmetric]) auto
hoelzl@56273
   288
hoelzl@56273
   289
lemma enum_in: "i \<le> n \<Longrightarrow> enum i \<in> s"
hoelzl@56273
   290
  unfolding s_eq by auto
hoelzl@56273
   291
hoelzl@56273
   292
lemma one_step:
hoelzl@56273
   293
  assumes a: "a \<in> s" "j < n"
hoelzl@56273
   294
  assumes *: "\<And>a'. a' \<in> s \<Longrightarrow> a' \<noteq> a \<Longrightarrow> a' j = p'"
hoelzl@56273
   295
  shows "a j \<noteq> p'"
hoelzl@56273
   296
proof
hoelzl@56273
   297
  assume "a j = p'"
hoelzl@56273
   298
  with * a have "\<And>a'. a' \<in> s \<Longrightarrow> a' j = p'"
hoelzl@56273
   299
    by auto
hoelzl@56273
   300
  then have "\<And>i. i \<le> n \<Longrightarrow> enum i j = p'"
hoelzl@56273
   301
    unfolding s_eq by auto
hoelzl@56273
   302
  from this[of 0] this[of n] have "j \<notin> upd ` {..< n}"
nipkow@62390
   303
    by (auto simp: enum_def fun_eq_iff split: if_split_asm)
wenzelm@60420
   304
  with upd \<open>j < n\<close> show False
hoelzl@56273
   305
    by (auto simp: bij_betw_def)
hoelzl@56273
   306
qed
hoelzl@56273
   307
hoelzl@56273
   308
lemma upd_inj: "i < n \<Longrightarrow> j < n \<Longrightarrow> upd i = upd j \<longleftrightarrow> i = j"
lp15@61520
   309
  using upd by (auto simp: bij_betw_def inj_on_eq_iff)
hoelzl@56273
   310
hoelzl@56273
   311
lemma upd_surj: "upd ` {..< n} = {..< n}"
hoelzl@56273
   312
  using upd by (auto simp: bij_betw_def)
hoelzl@56273
   313
hoelzl@56273
   314
lemma in_upd_image: "A \<subseteq> {..< n} \<Longrightarrow> i < n \<Longrightarrow> upd i \<in> upd ` A \<longleftrightarrow> i \<in> A"
lp15@61520
   315
  using inj_on_image_mem_iff[of upd "{..< n}"] upd
hoelzl@56273
   316
  by (auto simp: bij_betw_def)
hoelzl@56273
   317
hoelzl@56273
   318
lemma enum_inj: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i = enum j \<longleftrightarrow> i = j"
lp15@61520
   319
  using inj_enum by (auto simp: inj_on_eq_iff)
hoelzl@56273
   320
hoelzl@56273
   321
lemma in_enum_image: "A \<subseteq> {.. n} \<Longrightarrow> i \<le> n \<Longrightarrow> enum i \<in> enum ` A \<longleftrightarrow> i \<in> A"
lp15@61520
   322
  using inj_on_image_mem_iff[OF inj_enum] by auto
hoelzl@56273
   323
hoelzl@56273
   324
lemma enum_mono: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i \<le> enum j \<longleftrightarrow> i \<le> j"
hoelzl@56273
   325
  by (auto simp: enum_def le_fun_def in_upd_image Ball_def[symmetric])
hoelzl@56273
   326
hoelzl@56273
   327
lemma enum_strict_mono: "i \<le> n \<Longrightarrow> j \<le> n \<Longrightarrow> enum i < enum j \<longleftrightarrow> i < j"
hoelzl@56273
   328
  using enum_mono[of i j] enum_inj[of i j] by (auto simp add: le_less)
hoelzl@56273
   329
hoelzl@56273
   330
lemma chain: "a \<in> s \<Longrightarrow> b \<in> s \<Longrightarrow> a \<le> b \<or> b \<le> a"
hoelzl@56273
   331
  by (auto simp: s_eq enum_mono)
hoelzl@56273
   332
hoelzl@56273
   333
lemma less: "a \<in> s \<Longrightarrow> b \<in> s \<Longrightarrow> a i < b i \<Longrightarrow> a < b"
hoelzl@56273
   334
  using chain[of a b] by (auto simp: less_fun_def le_fun_def not_le[symmetric])
hoelzl@56273
   335
hoelzl@56273
   336
lemma enum_0_bot: "a \<in> s \<Longrightarrow> a = enum 0 \<longleftrightarrow> (\<forall>a'\<in>s. a \<le> a')"
hoelzl@56273
   337
  unfolding s_eq by (auto simp: enum_mono Ball_def)
hoelzl@56273
   338
hoelzl@56273
   339
lemma enum_n_top: "a \<in> s \<Longrightarrow> a = enum n \<longleftrightarrow> (\<forall>a'\<in>s. a' \<le> a)"
hoelzl@56273
   340
  unfolding s_eq by (auto simp: enum_mono Ball_def)
hoelzl@56273
   341
hoelzl@56273
   342
lemma enum_Suc: "i < n \<Longrightarrow> enum (Suc i) = (enum i)(upd i := Suc (enum i (upd i)))"
hoelzl@56273
   343
  by (auto simp: fun_eq_iff enum_def upd_inj)
hoelzl@56273
   344
hoelzl@56273
   345
lemma enum_eq_p: "i \<le> n \<Longrightarrow> n \<le> j \<Longrightarrow> enum i j = p"
hoelzl@56273
   346
  by (induct i) (auto simp: enum_Suc enum_0 base_out upd_space not_less[symmetric])
hoelzl@56273
   347
hoelzl@56273
   348
lemma out_eq_p: "a \<in> s \<Longrightarrow> n \<le> j \<Longrightarrow> a j = p"
hoelzl@56273
   349
  unfolding s_eq by (auto simp add: enum_eq_p)
hoelzl@56273
   350
hoelzl@56273
   351
lemma s_le_p: "a \<in> s \<Longrightarrow> a j \<le> p"
hoelzl@56273
   352
  using out_eq_p[of a j] s_space by (cases "j < n") auto
hoelzl@56273
   353
hoelzl@56273
   354
lemma le_Suc_base: "a \<in> s \<Longrightarrow> a j \<le> Suc (base j)"
hoelzl@56273
   355
  unfolding s_eq by (auto simp: enum_def)
hoelzl@56273
   356
hoelzl@56273
   357
lemma base_le: "a \<in> s \<Longrightarrow> base j \<le> a j"
hoelzl@56273
   358
  unfolding s_eq by (auto simp: enum_def)
hoelzl@56273
   359
hoelzl@56273
   360
lemma enum_le_p: "i \<le> n \<Longrightarrow> j < n \<Longrightarrow> enum i j \<le> p"
hoelzl@56273
   361
  using enum_in[of i] s_space by auto
hoelzl@56273
   362
hoelzl@56273
   363
lemma enum_less: "a \<in> s \<Longrightarrow> i < n \<Longrightarrow> enum i < a \<longleftrightarrow> enum (Suc i) \<le> a"
hoelzl@56273
   364
  unfolding s_eq by (auto simp: enum_strict_mono enum_mono)
hoelzl@56273
   365
hoelzl@56273
   366
lemma ksimplex_0:
hoelzl@56273
   367
  "n = 0 \<Longrightarrow> s = {(\<lambda>x. p)}"
hoelzl@56273
   368
  using s_eq enum_def base_out by auto
hoelzl@56273
   369
hoelzl@56273
   370
lemma replace_0:
hoelzl@56273
   371
  assumes "j < n" "a \<in> s" and p: "\<forall>x\<in>s - {a}. x j = 0" and "x \<in> s"
hoelzl@56273
   372
  shows "x \<le> a"
hoelzl@56273
   373
proof cases
hoelzl@56273
   374
  assume "x \<noteq> a"
hoelzl@56273
   375
  have "a j \<noteq> 0"
hoelzl@56273
   376
    using assms by (intro one_step[where a=a]) auto
wenzelm@60420
   377
  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
   378
  show ?thesis
hoelzl@56273
   379
    by auto
hoelzl@56273
   380
qed simp
hoelzl@56273
   381
hoelzl@56273
   382
lemma replace_1:
hoelzl@56273
   383
  assumes "j < n" "a \<in> s" and p: "\<forall>x\<in>s - {a}. x j = p" and "x \<in> s"
hoelzl@56273
   384
  shows "a \<le> x"
hoelzl@56273
   385
proof cases
hoelzl@56273
   386
  assume "x \<noteq> a"
hoelzl@56273
   387
  have "a j \<noteq> p"
hoelzl@56273
   388
    using assms by (intro one_step[where a=a]) auto
wenzelm@60420
   389
  with enum_le_p[of _ j] \<open>j < n\<close> \<open>a\<in>s\<close>
hoelzl@56273
   390
  have "a j < p"
hoelzl@56273
   391
    by (auto simp: less_le s_eq)
wenzelm@60420
   392
  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
   393
  show ?thesis
hoelzl@56273
   394
    by auto
hoelzl@56273
   395
qed simp
hoelzl@56273
   396
hoelzl@56273
   397
end
hoelzl@56273
   398
hoelzl@56273
   399
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
   400
  for p n b_s u_s s b_t u_t t
hoelzl@56273
   401
begin
hoelzl@56273
   402
hoelzl@56273
   403
lemma enum_eq:
hoelzl@56273
   404
  assumes l: "i \<le> l" "l \<le> j" and "j + d \<le> n"
hoelzl@56273
   405
  assumes eq: "s.enum ` {i .. j} = t.enum ` {i + d .. j + d}"
hoelzl@56273
   406
  shows "s.enum l = t.enum (l + d)"
hoelzl@56273
   407
using l proof (induct l rule: dec_induct)
hoelzl@56273
   408
  case base
hoelzl@56273
   409
  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
   410
    using eq by auto
wenzelm@60420
   411
  from t \<open>i \<le> j\<close> \<open>j + d \<le> n\<close> have "s.enum i \<le> t.enum (i + d)"
hoelzl@56273
   412
    by (auto simp: s.enum_mono)
wenzelm@60420
   413
  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
   414
    by (auto simp: t.enum_mono)
hoelzl@56273
   415
  ultimately show ?case
hoelzl@56273
   416
    by auto
hoelzl@56273
   417
next
hoelzl@56273
   418
  case (step l)
wenzelm@60420
   419
  moreover from step.prems \<open>j + d \<le> n\<close> have
hoelzl@56273
   420
      "s.enum l < s.enum (Suc l)"
hoelzl@56273
   421
      "t.enum (l + d) < t.enum (Suc l + d)"
hoelzl@56273
   422
    by (simp_all add: s.enum_strict_mono t.enum_strict_mono)
hoelzl@56273
   423
  moreover have
hoelzl@56273
   424
      "s.enum (Suc l) \<in> t.enum ` {i + d .. j + d}"
hoelzl@56273
   425
      "t.enum (Suc l + d) \<in> s.enum ` {i .. j}"
wenzelm@60420
   426
    using step \<open>j + d \<le> n\<close> eq by (auto simp: s.enum_inj t.enum_inj)
hoelzl@56273
   427
  ultimately have "s.enum (Suc l) = t.enum (Suc (l + d))"
wenzelm@60420
   428
    using \<open>j + d \<le> n\<close>
lp15@61609
   429
    by (intro antisym s.enum_less[THEN iffD1] t.enum_less[THEN iffD1])
hoelzl@56273
   430
       (auto intro!: s.enum_in t.enum_in)
hoelzl@56273
   431
  then show ?case by simp
hoelzl@56273
   432
qed
hoelzl@56273
   433
hoelzl@56273
   434
lemma ksimplex_eq_bot:
hoelzl@56273
   435
  assumes a: "a \<in> s" "\<And>a'. a' \<in> s \<Longrightarrow> a \<le> a'"
hoelzl@56273
   436
  assumes b: "b \<in> t" "\<And>b'. b' \<in> t \<Longrightarrow> b \<le> b'"
hoelzl@56273
   437
  assumes eq: "s - {a} = t - {b}"
hoelzl@56273
   438
  shows "s = t"
hoelzl@56273
   439
proof cases
hoelzl@56273
   440
  assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp
hoelzl@56273
   441
next
hoelzl@56273
   442
  assume "n \<noteq> 0"
hoelzl@56273
   443
  have "s.enum 0 = (s.enum (Suc 0)) (u_s 0 := s.enum (Suc 0) (u_s 0) - 1)"
hoelzl@56273
   444
       "t.enum 0 = (t.enum (Suc 0)) (u_t 0 := t.enum (Suc 0) (u_t 0) - 1)"
wenzelm@60420
   445
    using \<open>n \<noteq> 0\<close> by (simp_all add: s.enum_Suc t.enum_Suc)
hoelzl@56273
   446
  moreover have e0: "a = s.enum 0" "b = t.enum 0"
hoelzl@56273
   447
    using a b by (simp_all add: s.enum_0_bot t.enum_0_bot)
hoelzl@56273
   448
  moreover
lp15@61609
   449
  { fix j assume "0 < j" "j \<le> n"
hoelzl@56273
   450
    moreover have "s - {a} = s.enum ` {Suc 0 .. n}" "t - {b} = t.enum ` {Suc 0 .. n}"
hoelzl@56273
   451
      unfolding s.s_eq t.s_eq e0 by (auto simp: s.enum_inj t.enum_inj)
hoelzl@56273
   452
    ultimately have "s.enum j = t.enum j"
hoelzl@56273
   453
      using enum_eq[of "1" j n 0] eq by auto }
hoelzl@56273
   454
  note enum_eq = this
hoelzl@56273
   455
  then have "s.enum (Suc 0) = t.enum (Suc 0)"
wenzelm@60420
   456
    using \<open>n \<noteq> 0\<close> by auto
hoelzl@56273
   457
  moreover
hoelzl@56273
   458
  { fix j assume "Suc j < n"
hoelzl@56273
   459
    with enum_eq[of "Suc j"] enum_eq[of "Suc (Suc j)"]
hoelzl@56273
   460
    have "u_s (Suc j) = u_t (Suc j)"
hoelzl@56273
   461
      using s.enum_Suc[of "Suc j"] t.enum_Suc[of "Suc j"]
nipkow@62390
   462
      by (auto simp: fun_eq_iff split: if_split_asm) }
hoelzl@56273
   463
  then have "\<And>j. 0 < j \<Longrightarrow> j < n \<Longrightarrow> u_s j = u_t j"
hoelzl@56273
   464
    by (auto simp: gr0_conv_Suc)
wenzelm@60420
   465
  with \<open>n \<noteq> 0\<close> have "u_t 0 = u_s 0"
hoelzl@56273
   466
    by (intro bij_betw_singleton_eq[OF t.upd s.upd, of 0]) auto
hoelzl@56273
   467
  ultimately have "a = b"
hoelzl@56273
   468
    by simp
hoelzl@56273
   469
  with assms show "s = t"
hoelzl@56273
   470
    by auto
hoelzl@56273
   471
qed
hoelzl@56273
   472
hoelzl@56273
   473
lemma ksimplex_eq_top:
hoelzl@56273
   474
  assumes a: "a \<in> s" "\<And>a'. a' \<in> s \<Longrightarrow> a' \<le> a"
hoelzl@56273
   475
  assumes b: "b \<in> t" "\<And>b'. b' \<in> t \<Longrightarrow> b' \<le> b"
hoelzl@56273
   476
  assumes eq: "s - {a} = t - {b}"
hoelzl@56273
   477
  shows "s = t"
hoelzl@56273
   478
proof (cases n)
hoelzl@56273
   479
  assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp
hoelzl@56273
   480
next
hoelzl@56273
   481
  case (Suc n')
hoelzl@56273
   482
  have "s.enum n = (s.enum n') (u_s n' := Suc (s.enum n' (u_s n')))"
hoelzl@56273
   483
       "t.enum n = (t.enum n') (u_t n' := Suc (t.enum n' (u_t n')))"
hoelzl@56273
   484
    using Suc by (simp_all add: s.enum_Suc t.enum_Suc)
hoelzl@56273
   485
  moreover have en: "a = s.enum n" "b = t.enum n"
hoelzl@56273
   486
    using a b by (simp_all add: s.enum_n_top t.enum_n_top)
hoelzl@56273
   487
  moreover
lp15@61609
   488
  { fix j assume "j < n"
hoelzl@56273
   489
    moreover have "s - {a} = s.enum ` {0 .. n'}" "t - {b} = t.enum ` {0 .. n'}"
hoelzl@56273
   490
      unfolding s.s_eq t.s_eq en by (auto simp: s.enum_inj t.enum_inj Suc)
hoelzl@56273
   491
    ultimately have "s.enum j = t.enum j"
hoelzl@56273
   492
      using enum_eq[of "0" j n' 0] eq Suc by auto }
hoelzl@56273
   493
  note enum_eq = this
hoelzl@56273
   494
  then have "s.enum n' = t.enum n'"
hoelzl@56273
   495
    using Suc by auto
hoelzl@56273
   496
  moreover
hoelzl@56273
   497
  { fix j assume "j < n'"
hoelzl@56273
   498
    with enum_eq[of j] enum_eq[of "Suc j"]
hoelzl@56273
   499
    have "u_s j = u_t j"
hoelzl@56273
   500
      using s.enum_Suc[of j] t.enum_Suc[of j]
nipkow@62390
   501
      by (auto simp: Suc fun_eq_iff split: if_split_asm) }
hoelzl@56273
   502
  then have "\<And>j. j < n' \<Longrightarrow> u_s j = u_t j"
hoelzl@56273
   503
    by (auto simp: gr0_conv_Suc)
hoelzl@56273
   504
  then have "u_t n' = u_s n'"
hoelzl@56273
   505
    by (intro bij_betw_singleton_eq[OF t.upd s.upd, of n']) (auto simp: Suc)
hoelzl@56273
   506
  ultimately have "a = b"
hoelzl@56273
   507
    by simp
hoelzl@56273
   508
  with assms show "s = t"
hoelzl@56273
   509
    by auto
hoelzl@56273
   510
qed
hoelzl@56273
   511
hoelzl@56273
   512
end
hoelzl@56273
   513
hoelzl@56273
   514
inductive ksimplex for p n :: nat where
hoelzl@56273
   515
  ksimplex: "kuhn_simplex p n base upd s \<Longrightarrow> ksimplex p n s"
hoelzl@56273
   516
hoelzl@56273
   517
lemma finite_ksimplexes: "finite {s. ksimplex p n s}"
hoelzl@56273
   518
proof (rule finite_subset)
hoelzl@56273
   519
  { fix a s assume "ksimplex p n s" "a \<in> s"
hoelzl@56273
   520
    then obtain b u where "kuhn_simplex p n b u s" by (auto elim: ksimplex.cases)
hoelzl@56273
   521
    then interpret kuhn_simplex p n b u s .
wenzelm@60420
   522
    from s_space \<open>a \<in> s\<close> out_eq_p[OF \<open>a \<in> s\<close>]
hoelzl@56273
   523
    have "a \<in> (\<lambda>f x. if n \<le> x then p else f x) ` ({..< n} \<rightarrow>\<^sub>E {.. p})"
nipkow@62390
   524
      by (auto simp: image_iff subset_eq Pi_iff split: if_split_asm
hoelzl@56273
   525
               intro!: bexI[of _ "restrict a {..< n}"]) }
hoelzl@56273
   526
  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
   527
    by auto
hoelzl@56273
   528
qed (simp add: finite_PiE)
hoelzl@56273
   529
hoelzl@56273
   530
lemma ksimplex_card:
hoelzl@56273
   531
  assumes "ksimplex p n s" shows "card s = Suc n"
hoelzl@56273
   532
using assms proof cases
hoelzl@56273
   533
  case (ksimplex u b)
hoelzl@56273
   534
  then interpret kuhn_simplex p n u b s .
hoelzl@56273
   535
  show ?thesis
hoelzl@56273
   536
    by (simp add: card_image s_eq inj_enum)
hoelzl@56273
   537
qed
hoelzl@56273
   538
hoelzl@56273
   539
lemma simplex_top_face:
hoelzl@56273
   540
  assumes "0 < p" "\<forall>x\<in>s'. x n = p"
hoelzl@56273
   541
  shows "ksimplex p n s' \<longleftrightarrow> (\<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> s' = s - {a})"
hoelzl@56273
   542
  using assms
hoelzl@56273
   543
proof safe
hoelzl@56273
   544
  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
   545
  then show "ksimplex p n (s - {a})"
hoelzl@56273
   546
  proof cases
hoelzl@56273
   547
    case (ksimplex base upd)
hoelzl@56273
   548
    then interpret kuhn_simplex p "Suc n" base upd "s" .
hoelzl@56273
   549
hoelzl@56273
   550
    have "a n < p"
wenzelm@60420
   551
      using one_step[of a n p] na \<open>a\<in>s\<close> s_space by (auto simp: less_le)
hoelzl@56273
   552
    then have "a = enum 0"
wenzelm@60420
   553
      using \<open>a \<in> s\<close> na by (subst enum_0_bot) (auto simp: le_less intro!: less[of a _ n])
hoelzl@56273
   554
    then have s_eq: "s - {a} = enum ` Suc ` {.. n}"
hoelzl@56273
   555
      using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident Zero_notin_Suc in_enum_image subset_eq)
hoelzl@56273
   556
    then have "enum 1 \<in> s - {a}"
hoelzl@56273
   557
      by auto
hoelzl@56273
   558
    then have "upd 0 = n"
wenzelm@60420
   559
      using \<open>a n < p\<close> \<open>a = enum 0\<close> na[rule_format, of "enum 1"]
nipkow@62390
   560
      by (auto simp: fun_eq_iff enum_Suc split: if_split_asm)
hoelzl@56273
   561
    then have "bij_betw upd (Suc ` {..< n}) {..< n}"
hoelzl@56273
   562
      using upd
hoelzl@56273
   563
      by (subst notIn_Un_bij_betw3[where b=0])
hoelzl@56273
   564
         (auto simp: lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0)
hoelzl@56273
   565
    then have "bij_betw (upd\<circ>Suc) {..<n} {..<n}"
hoelzl@56273
   566
      by (rule bij_betw_trans[rotated]) (auto simp: bij_betw_def)
hoelzl@56273
   567
hoelzl@56273
   568
    have "a n = p - 1"
wenzelm@60420
   569
      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
   570
hoelzl@56273
   571
    show ?thesis
wenzelm@61169
   572
    proof (rule ksimplex.intros, standard)
hoelzl@56273
   573
      show "bij_betw (upd\<circ>Suc) {..< n} {..< n}" by fact
hoelzl@56273
   574
      show "base(n := p) \<in> {..<n} \<rightarrow> {..<p}" "\<And>i. n\<le>i \<Longrightarrow> (base(n := p)) i = p"
hoelzl@56273
   575
        using base base_out by (auto simp: Pi_iff)
hoelzl@56273
   576
hoelzl@56273
   577
      have "\<And>i. Suc ` {..< i} = {..< Suc i} - {0}"
hoelzl@56273
   578
        by (auto simp: image_iff Ball_def) arith
hoelzl@56273
   579
      then have upd_Suc: "\<And>i. i \<le> n \<Longrightarrow> (upd\<circ>Suc) ` {..< i} = upd ` {..< Suc i} - {n}"
wenzelm@60420
   580
        using \<open>upd 0 = n\<close> upd_inj
paulson@60303
   581
        by (auto simp add: image_comp[symmetric] inj_on_image_set_diff[OF inj_upd])
hoelzl@56273
   582
      have n_in_upd: "\<And>i. n \<in> upd ` {..< Suc i}"
wenzelm@60420
   583
        using \<open>upd 0 = n\<close> by auto
hoelzl@56273
   584
wenzelm@63040
   585
      define f' where "f' i j =
wenzelm@63040
   586
        (if j \<in> (upd\<circ>Suc)`{..< i} then Suc ((base(n := p)) j) else (base(n := p)) j)" for i j
hoelzl@56273
   587
      { fix x i assume i[arith]: "i \<le> n" then have "enum (Suc i) x = f' i x"
wenzelm@60420
   588
          unfolding f'_def enum_def using \<open>a n < p\<close> \<open>a = enum 0\<close> \<open>upd 0 = n\<close> \<open>a n = p - 1\<close>
hoelzl@56273
   589
          by (simp add: upd_Suc enum_0 n_in_upd) }
hoelzl@56273
   590
      then show "s - {a} = f' ` {.. n}"
hoelzl@56273
   591
        unfolding s_eq image_comp by (intro image_cong) auto
hoelzl@56273
   592
    qed
hoelzl@56273
   593
  qed
hoelzl@56273
   594
next
hoelzl@56273
   595
  assume "ksimplex p n s'" and *: "\<forall>x\<in>s'. x n = p"
hoelzl@56273
   596
  then show "\<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> s' = s - {a}"
hoelzl@56273
   597
  proof cases
hoelzl@56273
   598
    case (ksimplex base upd)
hoelzl@56273
   599
    then interpret kuhn_simplex p n base upd s' .
wenzelm@63040
   600
    define b where "b = base (n := p - 1)"
wenzelm@63040
   601
    define u where "u i = (case i of 0 \<Rightarrow> n | Suc i \<Rightarrow> upd i)" for i
hoelzl@56273
   602
hoelzl@56273
   603
    have "ksimplex p (Suc n) (s' \<union> {b})"
wenzelm@61169
   604
    proof (rule ksimplex.intros, standard)
hoelzl@56273
   605
      show "b \<in> {..<Suc n} \<rightarrow> {..<p}"
wenzelm@60420
   606
        using base \<open>0 < p\<close> unfolding lessThan_Suc b_def by (auto simp: PiE_iff)
hoelzl@56273
   607
      show "\<And>i. Suc n \<le> i \<Longrightarrow> b i = p"
hoelzl@56273
   608
        using base_out by (auto simp: b_def)
hoelzl@56273
   609
hoelzl@56273
   610
      have "bij_betw u (Suc ` {..< n} \<union> {0}) ({..<n} \<union> {u 0})"
hoelzl@56273
   611
        using upd
hoelzl@56273
   612
        by (intro notIn_Un_bij_betw) (auto simp: u_def bij_betw_def image_comp comp_def inj_on_def)
hoelzl@56273
   613
      then show "bij_betw u {..<Suc n} {..<Suc n}"
hoelzl@56273
   614
        by (simp add: u_def lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0)
hoelzl@56273
   615
wenzelm@63040
   616
      define f' where "f' i j = (if j \<in> u`{..< i} then Suc (b j) else b j)" for i j
hoelzl@56273
   617
hoelzl@56273
   618
      have u_eq: "\<And>i. i \<le> n \<Longrightarrow> u ` {..< Suc i} = upd ` {..< i} \<union> { n }"
hoelzl@56273
   619
        by (auto simp: u_def image_iff upd_inj Ball_def split: nat.split) arith
hoelzl@56273
   620
hoelzl@56273
   621
      { fix x have "x \<le> n \<Longrightarrow> n \<notin> upd ` {..<x}"
hoelzl@56273
   622
          using upd_space by (simp add: image_iff neq_iff) }
hoelzl@56273
   623
      note n_not_upd = this
hoelzl@56273
   624
hoelzl@56273
   625
      have *: "f' ` {.. Suc n} = f' ` (Suc ` {.. n} \<union> {0})"
hoelzl@56273
   626
        unfolding atMost_Suc_eq_insert_0 by simp
hoelzl@56273
   627
      also have "\<dots> = (f' \<circ> Suc) ` {.. n} \<union> {b}"
hoelzl@56273
   628
        by (auto simp: f'_def)
hoelzl@56273
   629
      also have "(f' \<circ> Suc) ` {.. n} = s'"
wenzelm@60420
   630
        using \<open>0 < p\<close> base_out[of n]
hoelzl@56273
   631
        unfolding s_eq enum_def[abs_def] f'_def[abs_def] upd_space
hoelzl@56273
   632
        by (intro image_cong) (simp_all add: u_eq b_def fun_eq_iff n_not_upd)
hoelzl@56273
   633
      finally show "s' \<union> {b} = f' ` {.. Suc n}" ..
hoelzl@56273
   634
    qed
hoelzl@56273
   635
    moreover have "b \<notin> s'"
wenzelm@60420
   636
      using * \<open>0 < p\<close> by (auto simp: b_def)
hoelzl@56273
   637
    ultimately show ?thesis by auto
hoelzl@56273
   638
  qed
hoelzl@56273
   639
qed
hoelzl@56273
   640
hoelzl@56273
   641
lemma ksimplex_replace_0:
hoelzl@56273
   642
  assumes s: "ksimplex p n s" and a: "a \<in> s"
hoelzl@56273
   643
  assumes j: "j < n" and p: "\<forall>x\<in>s - {a}. x j = 0"
hoelzl@56273
   644
  shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
hoelzl@56273
   645
  using s
hoelzl@56273
   646
proof cases
hoelzl@56273
   647
  case (ksimplex b_s u_s)
hoelzl@56273
   648
lp15@61609
   649
  { fix t b assume "ksimplex p n t"
hoelzl@56273
   650
    then obtain b_t u_t where "kuhn_simplex p n b_t u_t t"
hoelzl@56273
   651
      by (auto elim: ksimplex.cases)
hoelzl@56273
   652
    interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t
hoelzl@56273
   653
      by intro_locales fact+
hoelzl@56273
   654
hoelzl@56273
   655
    assume b: "b \<in> t" "t - {b} = s - {a}"
hoelzl@56273
   656
    with a j p s.replace_0[of _ a] t.replace_0[of _ b] have "s = t"
hoelzl@56273
   657
      by (intro ksimplex_eq_top[of a b]) auto }
hoelzl@56273
   658
  then have "{s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = {s}"
wenzelm@60420
   659
    using s \<open>a \<in> s\<close> by auto
hoelzl@56273
   660
  then show ?thesis
hoelzl@56273
   661
    by simp
hoelzl@56273
   662
qed
hoelzl@56273
   663
hoelzl@56273
   664
lemma ksimplex_replace_1:
hoelzl@56273
   665
  assumes s: "ksimplex p n s" and a: "a \<in> s"
hoelzl@56273
   666
  assumes j: "j < n" and p: "\<forall>x\<in>s - {a}. x j = p"
hoelzl@56273
   667
  shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
hoelzl@56273
   668
  using s
hoelzl@56273
   669
proof cases
hoelzl@56273
   670
  case (ksimplex b_s u_s)
hoelzl@56273
   671
lp15@61609
   672
  { fix t b assume "ksimplex p n t"
hoelzl@56273
   673
    then obtain b_t u_t where "kuhn_simplex p n b_t u_t t"
hoelzl@56273
   674
      by (auto elim: ksimplex.cases)
hoelzl@56273
   675
    interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t
hoelzl@56273
   676
      by intro_locales fact+
hoelzl@56273
   677
hoelzl@56273
   678
    assume b: "b \<in> t" "t - {b} = s - {a}"
hoelzl@56273
   679
    with a j p s.replace_1[of _ a] t.replace_1[of _ b] have "s = t"
hoelzl@56273
   680
      by (intro ksimplex_eq_bot[of a b]) auto }
hoelzl@56273
   681
  then have "{s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = {s}"
wenzelm@60420
   682
    using s \<open>a \<in> s\<close> by auto
hoelzl@56273
   683
  then show ?thesis
hoelzl@56273
   684
    by simp
hoelzl@56273
   685
qed
hoelzl@56273
   686
hoelzl@56273
   687
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))"
hoelzl@56273
   688
  by (auto simp add: card_Suc_eq eval_nat_numeral)
hoelzl@56273
   689
hoelzl@56273
   690
lemma ksimplex_replace_2:
hoelzl@56273
   691
  assumes s: "ksimplex p n s" and "a \<in> s" and "n \<noteq> 0"
hoelzl@56273
   692
    and lb: "\<forall>j<n. \<exists>x\<in>s - {a}. x j \<noteq> 0"
hoelzl@56273
   693
    and ub: "\<forall>j<n. \<exists>x\<in>s - {a}. x j \<noteq> p"
hoelzl@56273
   694
  shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 2"
hoelzl@56273
   695
  using s
hoelzl@56273
   696
proof cases
hoelzl@56273
   697
  case (ksimplex base upd)
hoelzl@56273
   698
  then interpret kuhn_simplex p n base upd s .
hoelzl@56273
   699
wenzelm@60420
   700
  from \<open>a \<in> s\<close> obtain i where "i \<le> n" "a = enum i"
hoelzl@56273
   701
    unfolding s_eq by auto
hoelzl@56273
   702
wenzelm@60420
   703
  from \<open>i \<le> n\<close> have "i = 0 \<or> i = n \<or> (0 < i \<and> i < n)"
hoelzl@56273
   704
    by linarith
hoelzl@56273
   705
  then have "\<exists>!s'. s' \<noteq> s \<and> ksimplex p n s' \<and> (\<exists>b\<in>s'. s - {a} = s'- {b})"
hoelzl@56273
   706
  proof (elim disjE conjE)
hoelzl@56273
   707
    assume "i = 0"
wenzelm@63040
   708
    define rot where [abs_def]: "rot i = (if i + 1 = n then 0 else i + 1)" for i
hoelzl@56273
   709
    let ?upd = "upd \<circ> rot"
hoelzl@56273
   710
hoelzl@56273
   711
    have rot: "bij_betw rot {..< n} {..< n}"
hoelzl@56273
   712
      by (auto simp: bij_betw_def inj_on_def image_iff Ball_def rot_def)
hoelzl@56273
   713
         arith+
hoelzl@56273
   714
    from rot upd have "bij_betw ?upd {..<n} {..<n}"
hoelzl@56273
   715
      by (rule bij_betw_trans)
hoelzl@56273
   716
wenzelm@63040
   717
    define f' where [abs_def]: "f' i j =
wenzelm@63040
   718
      (if j \<in> ?upd`{..< i} then Suc (enum (Suc 0) j) else enum (Suc 0) j)" for i j
hoelzl@56273
   719
hoelzl@56273
   720
    interpret b: kuhn_simplex p n "enum (Suc 0)" "upd \<circ> rot" "f' ` {.. n}"
hoelzl@56273
   721
    proof
wenzelm@60420
   722
      from \<open>a = enum i\<close> ub \<open>n \<noteq> 0\<close> \<open>i = 0\<close>
hoelzl@56273
   723
      obtain i' where "i' \<le> n" "enum i' \<noteq> enum 0" "enum i' (upd 0) \<noteq> p"
hoelzl@56273
   724
        unfolding s_eq by (auto intro: upd_space simp: enum_inj)
hoelzl@56273
   725
      then have "enum 1 \<le> enum i'" "enum i' (upd 0) < p"
hoelzl@56273
   726
        using enum_le_p[of i' "upd 0"] by (auto simp add: enum_inj enum_mono upd_space)
hoelzl@56273
   727
      then have "enum 1 (upd 0) < p"
hoelzl@56273
   728
        by (auto simp add: le_fun_def intro: le_less_trans)
hoelzl@56273
   729
      then show "enum (Suc 0) \<in> {..<n} \<rightarrow> {..<p}"
wenzelm@60420
   730
        using base \<open>n \<noteq> 0\<close> by (auto simp add: enum_0 enum_Suc PiE_iff extensional_def upd_space)
hoelzl@56273
   731
hoelzl@56273
   732
      { fix i assume "n \<le> i" then show "enum (Suc 0) i = p"
wenzelm@60420
   733
        using \<open>n \<noteq> 0\<close> by (auto simp: enum_eq_p) }
hoelzl@56273
   734
      show "bij_betw ?upd {..<n} {..<n}" by fact
hoelzl@56273
   735
    qed (simp add: f'_def)
hoelzl@56273
   736
    have ks_f': "ksimplex p n (f' ` {.. n})"
hoelzl@56273
   737
      by rule unfold_locales
hoelzl@56273
   738
hoelzl@56273
   739
    have b_enum: "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
hoelzl@56273
   740
    with b.inj_enum have inj_f': "inj_on f' {.. n}" by simp
hoelzl@56273
   741
hoelzl@56273
   742
    have [simp]: "\<And>j. j < n \<Longrightarrow> rot ` {..< j} = {0 <..< Suc j}"
hoelzl@56273
   743
      by (auto simp: rot_def image_iff Ball_def)
hoelzl@56273
   744
         arith
hoelzl@56273
   745
hoelzl@56273
   746
    { fix j assume j: "j < n"
wenzelm@60420
   747
      from j \<open>n \<noteq> 0\<close> have "f' j = enum (Suc j)"
hoelzl@56273
   748
        by (auto simp add: f'_def enum_def upd_inj in_upd_image image_comp[symmetric] fun_eq_iff) }
hoelzl@56273
   749
    note f'_eq_enum = this
hoelzl@56273
   750
    then have "enum ` Suc ` {..< n} = f' ` {..< n}"
hoelzl@56273
   751
      by (force simp: enum_inj)
hoelzl@56273
   752
    also have "Suc ` {..< n} = {.. n} - {0}"
hoelzl@56273
   753
      by (auto simp: image_iff Ball_def) arith
hoelzl@56273
   754
    also have "{..< n} = {.. n} - {n}"
hoelzl@56273
   755
      by auto
hoelzl@56273
   756
    finally have eq: "s - {a} = f' ` {.. n} - {f' n}"
wenzelm@60420
   757
      unfolding s_eq \<open>a = enum i\<close> \<open>i = 0\<close>
paulson@60303
   758
      by (simp add: Diff_subset inj_on_image_set_diff[OF inj_enum] inj_on_image_set_diff[OF inj_f'])
hoelzl@56273
   759
hoelzl@56273
   760
    have "enum 0 < f' 0"
wenzelm@60420
   761
      using \<open>n \<noteq> 0\<close> by (simp add: enum_strict_mono f'_eq_enum)
hoelzl@56273
   762
    also have "\<dots> < f' n"
wenzelm@60420
   763
      using \<open>n \<noteq> 0\<close> b.enum_strict_mono[of 0 n] unfolding b_enum by simp
hoelzl@56273
   764
    finally have "a \<noteq> f' n"
wenzelm@60420
   765
      using \<open>a = enum i\<close> \<open>i = 0\<close> by auto
hoelzl@56273
   766
hoelzl@56273
   767
    { fix t c assume "ksimplex p n t" "c \<in> t" and eq_sma: "s - {a} = t - {c}"
hoelzl@56273
   768
      obtain b u where "kuhn_simplex p n b u t"
wenzelm@60420
   769
        using \<open>ksimplex p n t\<close> by (auto elim: ksimplex.cases)
hoelzl@56273
   770
      then interpret t: kuhn_simplex p n b u t .
hoelzl@56273
   771
hoelzl@56273
   772
      { fix x assume "x \<in> s" "x \<noteq> a"
hoelzl@56273
   773
         then have "x (upd 0) = enum (Suc 0) (upd 0)"
wenzelm@60420
   774
           by (auto simp: \<open>a = enum i\<close> \<open>i = 0\<close> s_eq enum_def enum_inj) }
hoelzl@56273
   775
      then have eq_upd0: "\<forall>x\<in>t-{c}. x (upd 0) = enum (Suc 0) (upd 0)"
hoelzl@56273
   776
        unfolding eq_sma[symmetric] by auto
hoelzl@56273
   777
      then have "c (upd 0) \<noteq> enum (Suc 0) (upd 0)"
wenzelm@60420
   778
        using \<open>n \<noteq> 0\<close> by (intro t.one_step[OF \<open>c\<in>t\<close> ]) (auto simp: upd_space)
hoelzl@56273
   779
      then have "c (upd 0) < enum (Suc 0) (upd 0) \<or> c (upd 0) > enum (Suc 0) (upd 0)"
hoelzl@56273
   780
        by auto
hoelzl@56273
   781
      then have "t = s \<or> t = f' ` {..n}"
hoelzl@56273
   782
      proof (elim disjE conjE)
hoelzl@56273
   783
        assume *: "c (upd 0) < enum (Suc 0) (upd 0)"
hoelzl@56273
   784
        interpret st: kuhn_simplex_pair p n base upd s b u t ..
wenzelm@60420
   785
        { fix x assume "x \<in> t" with * \<open>c\<in>t\<close> eq_upd0[rule_format, of x] have "c \<le> x"
hoelzl@56273
   786
            by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
hoelzl@56273
   787
        note top = this
hoelzl@56273
   788
        have "s = t"
wenzelm@60420
   789
          using \<open>a = enum i\<close> \<open>i = 0\<close> \<open>c \<in> t\<close>
hoelzl@56273
   790
          by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq_sma])
hoelzl@56273
   791
             (auto simp: s_eq enum_mono t.s_eq t.enum_mono top)
hoelzl@56273
   792
        then show ?thesis by simp
hoelzl@56273
   793
      next
hoelzl@56273
   794
        assume *: "c (upd 0) > enum (Suc 0) (upd 0)"
hoelzl@56273
   795
        interpret st: kuhn_simplex_pair p n "enum (Suc 0)" "upd \<circ> rot" "f' ` {.. n}" b u t ..
hoelzl@56273
   796
        have eq: "f' ` {..n} - {f' n} = t - {c}"
hoelzl@56273
   797
          using eq_sma eq by simp
wenzelm@60420
   798
        { fix x assume "x \<in> t" with * \<open>c\<in>t\<close> eq_upd0[rule_format, of x] have "x \<le> c"
hoelzl@56273
   799
            by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
hoelzl@56273
   800
        note top = this
hoelzl@56273
   801
        have "f' ` {..n} = t"
wenzelm@60420
   802
          using \<open>a = enum i\<close> \<open>i = 0\<close> \<open>c \<in> t\<close>
hoelzl@56273
   803
          by (intro st.ksimplex_eq_top[OF _ _ _ _ eq])
hoelzl@56273
   804
             (auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono b_enum[symmetric] top)
hoelzl@56273
   805
        then show ?thesis by simp
hoelzl@56273
   806
      qed }
wenzelm@60420
   807
    with ks_f' eq \<open>a \<noteq> f' n\<close> \<open>n \<noteq> 0\<close> show ?thesis
hoelzl@56273
   808
      apply (intro ex1I[of _ "f' ` {.. n}"])
hoelzl@56273
   809
      apply auto []
hoelzl@56273
   810
      apply metis
hoelzl@56273
   811
      done
hoelzl@56273
   812
  next
hoelzl@56273
   813
    assume "i = n"
wenzelm@60420
   814
    from \<open>n \<noteq> 0\<close> obtain n' where n': "n = Suc n'"
hoelzl@56273
   815
      by (cases n) auto
hoelzl@56273
   816
wenzelm@63040
   817
    define rot where "rot i = (case i of 0 \<Rightarrow> n' | Suc i \<Rightarrow> i)" for i
hoelzl@56273
   818
    let ?upd = "upd \<circ> rot"
hoelzl@56273
   819
hoelzl@56273
   820
    have rot: "bij_betw rot {..< n} {..< n}"
hoelzl@56273
   821
      by (auto simp: bij_betw_def inj_on_def image_iff Bex_def rot_def n' split: nat.splits)
hoelzl@56273
   822
         arith
hoelzl@56273
   823
    from rot upd have "bij_betw ?upd {..<n} {..<n}"
hoelzl@56273
   824
      by (rule bij_betw_trans)
hoelzl@56273
   825
wenzelm@63040
   826
    define b where "b = base (upd n' := base (upd n') - 1)"
wenzelm@63040
   827
    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
   828
hoelzl@56273
   829
    interpret b: kuhn_simplex p n b "upd \<circ> rot" "f' ` {.. n}"
hoelzl@56273
   830
    proof
hoelzl@56273
   831
      { fix i assume "n \<le> i" then show "b i = p"
hoelzl@56273
   832
          using base_out[of i] upd_space[of n'] by (auto simp: b_def n') }
hoelzl@56273
   833
      show "b \<in> {..<n} \<rightarrow> {..<p}"
wenzelm@60420
   834
        using base \<open>n \<noteq> 0\<close> upd_space[of n']
hoelzl@56273
   835
        by (auto simp: b_def PiE_def Pi_iff Ball_def upd_space extensional_def n')
hoelzl@56273
   836
hoelzl@56273
   837
      show "bij_betw ?upd {..<n} {..<n}" by fact
hoelzl@56273
   838
    qed (simp add: f'_def)
hoelzl@56273
   839
    have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
hoelzl@56273
   840
    have ks_f': "ksimplex p n (b.enum ` {.. n})"
hoelzl@56273
   841
      unfolding f' by rule unfold_locales
hoelzl@56273
   842
lp15@61609
   843
    have "0 < n"
wenzelm@60420
   844
      using \<open>n \<noteq> 0\<close> by auto
hoelzl@56273
   845
wenzelm@60420
   846
    { from \<open>a = enum i\<close> \<open>n \<noteq> 0\<close> \<open>i = n\<close> lb upd_space[of n']
hoelzl@56273
   847
      obtain i' where "i' \<le> n" "enum i' \<noteq> enum n" "0 < enum i' (upd n')"
hoelzl@56273
   848
        unfolding s_eq by (auto simp: enum_inj n')
hoelzl@56273
   849
      moreover have "enum i' (upd n') = base (upd n')"
wenzelm@60420
   850
        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
   851
      ultimately have "0 < base (upd n')"
hoelzl@56273
   852
        by auto }
hoelzl@56273
   853
    then have benum1: "b.enum (Suc 0) = base"
wenzelm@60420
   854
      unfolding b.enum_Suc[OF \<open>0<n\<close>] b.enum_0 by (auto simp: b_def rot_def)
hoelzl@56273
   855
hoelzl@56273
   856
    have [simp]: "\<And>j. Suc j < n \<Longrightarrow> rot ` {..< Suc j} = {n'} \<union> {..< j}"
hoelzl@56273
   857
      by (auto simp: rot_def image_iff Ball_def split: nat.splits)
hoelzl@56273
   858
    have rot_simps: "\<And>j. rot (Suc j) = j" "rot 0 = n'"
hoelzl@56273
   859
      by (simp_all add: rot_def)
hoelzl@56273
   860
hoelzl@56273
   861
    { fix j assume j: "Suc j \<le> n" then have "b.enum (Suc j) = enum j"
hoelzl@56273
   862
        by (induct j) (auto simp add: benum1 enum_0 b.enum_Suc enum_Suc rot_simps) }
hoelzl@56273
   863
    note b_enum_eq_enum = this
hoelzl@56273
   864
    then have "enum ` {..< n} = b.enum ` Suc ` {..< n}"
hoelzl@56273
   865
      by (auto simp add: image_comp intro!: image_cong)
hoelzl@56273
   866
    also have "Suc ` {..< n} = {.. n} - {0}"
hoelzl@56273
   867
      by (auto simp: image_iff Ball_def) arith
hoelzl@56273
   868
    also have "{..< n} = {.. n} - {n}"
hoelzl@56273
   869
      by auto
hoelzl@56273
   870
    finally have eq: "s - {a} = b.enum ` {.. n} - {b.enum 0}"
wenzelm@60420
   871
      unfolding s_eq \<open>a = enum i\<close> \<open>i = n\<close>
paulson@60303
   872
      using inj_on_image_set_diff[OF inj_enum Diff_subset, of "{n}"]
paulson@60303
   873
            inj_on_image_set_diff[OF b.inj_enum Diff_subset, of "{0}"]
paulson@60303
   874
      by (simp add: comp_def )
hoelzl@56273
   875
hoelzl@56273
   876
    have "b.enum 0 \<le> b.enum n"
hoelzl@56273
   877
      by (simp add: b.enum_mono)
hoelzl@56273
   878
    also have "b.enum n < enum n"
wenzelm@60420
   879
      using \<open>n \<noteq> 0\<close> by (simp add: enum_strict_mono b_enum_eq_enum n')
hoelzl@56273
   880
    finally have "a \<noteq> b.enum 0"
wenzelm@60420
   881
      using \<open>a = enum i\<close> \<open>i = n\<close> by auto
hoelzl@56273
   882
hoelzl@56273
   883
    { fix t c assume "ksimplex p n t" "c \<in> t" and eq_sma: "s - {a} = t - {c}"
hoelzl@56273
   884
      obtain b' u where "kuhn_simplex p n b' u t"
wenzelm@60420
   885
        using \<open>ksimplex p n t\<close> by (auto elim: ksimplex.cases)
hoelzl@56273
   886
      then interpret t: kuhn_simplex p n b' u t .
hoelzl@56273
   887
hoelzl@56273
   888
      { fix x assume "x \<in> s" "x \<noteq> a"
hoelzl@56273
   889
         then have "x (upd n') = enum n' (upd n')"
wenzelm@60420
   890
           by (auto simp: \<open>a = enum i\<close> n' \<open>i = n\<close> s_eq enum_def enum_inj in_upd_image) }
hoelzl@56273
   891
      then have eq_upd0: "\<forall>x\<in>t-{c}. x (upd n') = enum n' (upd n')"
hoelzl@56273
   892
        unfolding eq_sma[symmetric] by auto
hoelzl@56273
   893
      then have "c (upd n') \<noteq> enum n' (upd n')"
wenzelm@60420
   894
        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
   895
      then have "c (upd n') < enum n' (upd n') \<or> c (upd n') > enum n' (upd n')"
hoelzl@56273
   896
        by auto
hoelzl@56273
   897
      then have "t = s \<or> t = b.enum ` {..n}"
hoelzl@56273
   898
      proof (elim disjE conjE)
hoelzl@56273
   899
        assume *: "c (upd n') > enum n' (upd n')"
hoelzl@56273
   900
        interpret st: kuhn_simplex_pair p n base upd s b' u t ..
wenzelm@60420
   901
        { fix x assume "x \<in> t" with * \<open>c\<in>t\<close> eq_upd0[rule_format, of x] have "x \<le> c"
hoelzl@56273
   902
            by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) }
hoelzl@56273
   903
        note top = this
hoelzl@56273
   904
        have "s = t"
wenzelm@60420
   905
          using \<open>a = enum i\<close> \<open>i = n\<close> \<open>c \<in> t\<close>
hoelzl@56273
   906
          by (intro st.ksimplex_eq_top[OF _ _ _ _ eq_sma])
hoelzl@56273
   907
             (auto simp: s_eq enum_mono t.s_eq t.enum_mono top)
hoelzl@56273
   908
        then show ?thesis by simp
hoelzl@56273
   909
      next
hoelzl@56273
   910
        assume *: "c (upd n') < enum n' (upd n')"
hoelzl@56273
   911
        interpret st: kuhn_simplex_pair p n b "upd \<circ> rot" "f' ` {.. n}" b' u t ..
hoelzl@56273
   912
        have eq: "f' ` {..n} - {b.enum 0} = t - {c}"
hoelzl@56273
   913
          using eq_sma eq f' by simp
wenzelm@60420
   914
        { fix x assume "x \<in> t" with * \<open>c\<in>t\<close> eq_upd0[rule_format, of x] have "c \<le> x"
hoelzl@56273
   915
            by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) }
hoelzl@56273
   916
        note bot = this
hoelzl@56273
   917
        have "f' ` {..n} = t"
wenzelm@60420
   918
          using \<open>a = enum i\<close> \<open>i = n\<close> \<open>c \<in> t\<close>
hoelzl@56273
   919
          by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq])
hoelzl@56273
   920
             (auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono bot)
hoelzl@56273
   921
        with f' show ?thesis by simp
hoelzl@56273
   922
      qed }
wenzelm@60420
   923
    with ks_f' eq \<open>a \<noteq> b.enum 0\<close> \<open>n \<noteq> 0\<close> show ?thesis
hoelzl@56273
   924
      apply (intro ex1I[of _ "b.enum ` {.. n}"])
hoelzl@56273
   925
      apply auto []
hoelzl@56273
   926
      apply metis
hoelzl@56273
   927
      done
hoelzl@56273
   928
  next
hoelzl@56273
   929
    assume i: "0 < i" "i < n"
wenzelm@63040
   930
    define i' where "i' = i - 1"
hoelzl@56273
   931
    with i have "Suc i' < n"
hoelzl@56273
   932
      by simp
hoelzl@56273
   933
    with i have Suc_i': "Suc i' = i"
hoelzl@56273
   934
      by (simp add: i'_def)
hoelzl@56273
   935
hoelzl@56273
   936
    let ?upd = "Fun.swap i' i upd"
hoelzl@56273
   937
    from i upd have "bij_betw ?upd {..< n} {..< n}"
hoelzl@56273
   938
      by (subst bij_betw_swap_iff) (auto simp: i'_def)
hoelzl@56273
   939
wenzelm@63040
   940
    define f' where [abs_def]: "f' i j = (if j \<in> ?upd`{..< i} then Suc (base j) else base j)"
wenzelm@63040
   941
      for i j
hoelzl@56273
   942
    interpret b: kuhn_simplex p n base ?upd "f' ` {.. n}"
hoelzl@56273
   943
    proof
hoelzl@56273
   944
      show "base \<in> {..<n} \<rightarrow> {..<p}" by fact
hoelzl@56273
   945
      { fix i assume "n \<le> i" then show "base i = p" by fact }
hoelzl@56273
   946
      show "bij_betw ?upd {..<n} {..<n}" by fact
hoelzl@56273
   947
    qed (simp add: f'_def)
hoelzl@56273
   948
    have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
hoelzl@56273
   949
    have ks_f': "ksimplex p n (b.enum ` {.. n})"
hoelzl@56273
   950
      unfolding f' by rule unfold_locales
hoelzl@56273
   951
hoelzl@56273
   952
    have "{i} \<subseteq> {..n}"
hoelzl@56273
   953
      using i by auto
hoelzl@56273
   954
    { fix j assume "j \<le> n"
hoelzl@56273
   955
      moreover have "j < i \<or> i = j \<or> i < j" by arith
hoelzl@56273
   956
      moreover note i
hoelzl@56273
   957
      ultimately have "enum j = b.enum j \<longleftrightarrow> j \<noteq> i"
hoelzl@56273
   958
        unfolding enum_def[abs_def] b.enum_def[abs_def]
hoelzl@56273
   959
        by (auto simp add: fun_eq_iff swap_image i'_def
hoelzl@56273
   960
                           in_upd_image inj_on_image_set_diff[OF inj_upd]) }
hoelzl@56273
   961
    note enum_eq_benum = this
hoelzl@56273
   962
    then have "enum ` ({.. n} - {i}) = b.enum ` ({.. n} - {i})"
hoelzl@56273
   963
      by (intro image_cong) auto
hoelzl@56273
   964
    then have eq: "s - {a} = b.enum ` {.. n} - {b.enum i}"
wenzelm@60420
   965
      unfolding s_eq \<open>a = enum i\<close>
wenzelm@60420
   966
      using inj_on_image_set_diff[OF inj_enum Diff_subset \<open>{i} \<subseteq> {..n}\<close>]
wenzelm@60420
   967
            inj_on_image_set_diff[OF b.inj_enum Diff_subset \<open>{i} \<subseteq> {..n}\<close>]
hoelzl@56273
   968
      by (simp add: comp_def)
hoelzl@56273
   969
hoelzl@56273
   970
    have "a \<noteq> b.enum i"
wenzelm@60420
   971
      using \<open>a = enum i\<close> enum_eq_benum i by auto
hoelzl@56273
   972
hoelzl@56273
   973
    { fix t c assume "ksimplex p n t" "c \<in> t" and eq_sma: "s - {a} = t - {c}"
hoelzl@56273
   974
      obtain b' u where "kuhn_simplex p n b' u t"
wenzelm@60420
   975
        using \<open>ksimplex p n t\<close> by (auto elim: ksimplex.cases)
hoelzl@56273
   976
      then interpret t: kuhn_simplex p n b' u t .
hoelzl@56273
   977
      have "enum i' \<in> s - {a}" "enum (i + 1) \<in> s - {a}"
wenzelm@60420
   978
        using \<open>a = enum i\<close> i enum_in by (auto simp: enum_inj i'_def)
hoelzl@56273
   979
      then obtain l k where
hoelzl@56273
   980
        l: "t.enum l = enum i'" "l \<le> n" "t.enum l \<noteq> c" and
hoelzl@56273
   981
        k: "t.enum k = enum (i + 1)" "k \<le> n" "t.enum k \<noteq> c"
hoelzl@56273
   982
        unfolding eq_sma by (auto simp: t.s_eq)
hoelzl@56273
   983
      with i have "t.enum l < t.enum k"
hoelzl@56273
   984
        by (simp add: enum_strict_mono i'_def)
wenzelm@60420
   985
      with \<open>l \<le> n\<close> \<open>k \<le> n\<close> have "l < k"
hoelzl@56273
   986
        by (simp add: t.enum_strict_mono)
hoelzl@56273
   987
      { assume "Suc l = k"
hoelzl@56273
   988
        have "enum (Suc (Suc i')) = t.enum (Suc l)"
wenzelm@60420
   989
          using i by (simp add: k \<open>Suc l = k\<close> i'_def)
hoelzl@56273
   990
        then have False
wenzelm@60420
   991
          using \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close>
nipkow@62390
   992
          by (auto simp: t.enum_Suc enum_Suc l upd_inj fun_eq_iff split: if_split_asm)
hoelzl@56273
   993
             (metis Suc_lessD n_not_Suc_n upd_inj) }
wenzelm@60420
   994
      with \<open>l < k\<close> have "Suc l < k"
hoelzl@56273
   995
        by arith
hoelzl@56273
   996
      have c_eq: "c = t.enum (Suc l)"
hoelzl@56273
   997
      proof (rule ccontr)
hoelzl@56273
   998
        assume "c \<noteq> t.enum (Suc l)"
hoelzl@56273
   999
        then have "t.enum (Suc l) \<in> s - {a}"
wenzelm@60420
  1000
          using \<open>l < k\<close> \<open>k \<le> n\<close> by (simp add: t.s_eq eq_sma)
hoelzl@56273
  1001
        then obtain j where "t.enum (Suc l) = enum j" "j \<le> n" "enum j \<noteq> enum i"
wenzelm@60420
  1002
          unfolding s_eq \<open>a = enum i\<close> by auto
hoelzl@56273
  1003
        with i have "t.enum (Suc l) \<le> t.enum l \<or> t.enum k \<le> t.enum (Suc l)"
hoelzl@56273
  1004
          by (auto simp add: i'_def enum_mono enum_inj l k)
wenzelm@60420
  1005
        with \<open>Suc l < k\<close> \<open>k \<le> n\<close> show False
hoelzl@56273
  1006
          by (simp add: t.enum_mono)
hoelzl@56273
  1007
      qed
hoelzl@56273
  1008
hoelzl@56273
  1009
      { have "t.enum (Suc (Suc l)) \<in> s - {a}"
wenzelm@60420
  1010
          unfolding eq_sma c_eq t.s_eq using \<open>Suc l < k\<close> \<open>k \<le> n\<close> by (auto simp: t.enum_inj)
hoelzl@56273
  1011
        then obtain j where eq: "t.enum (Suc (Suc l)) = enum j" and "j \<le> n" "j \<noteq> i"
wenzelm@60420
  1012
          by (auto simp: s_eq \<open>a = enum i\<close>)
hoelzl@56273
  1013
        moreover have "enum i' < t.enum (Suc (Suc l))"
wenzelm@60420
  1014
          unfolding l(1)[symmetric] using \<open>Suc l < k\<close> \<open>k \<le> n\<close> by (auto simp: t.enum_strict_mono)
hoelzl@56273
  1015
        ultimately have "i' < j"
hoelzl@56273
  1016
          using i by (simp add: enum_strict_mono i'_def)
wenzelm@60420
  1017
        with \<open>j \<noteq> i\<close> \<open>j \<le> n\<close> have "t.enum k \<le> t.enum (Suc (Suc l))"
hoelzl@56273
  1018
          unfolding i'_def by (simp add: enum_mono k eq)
hoelzl@56273
  1019
        then have "k \<le> Suc (Suc l)"
wenzelm@60420
  1020
          using \<open>k \<le> n\<close> \<open>Suc l < k\<close> by (simp add: t.enum_mono) }
wenzelm@60420
  1021
      with \<open>Suc l < k\<close> have "Suc (Suc l) = k" by simp
hoelzl@56273
  1022
      then have "enum (Suc (Suc i')) = t.enum (Suc (Suc l))"
hoelzl@56273
  1023
        using i by (simp add: k i'_def)
hoelzl@56273
  1024
      also have "\<dots> = (enum i') (u l := Suc (enum i' (u l)), u (Suc l) := Suc (enum i' (u (Suc l))))"
wenzelm@60420
  1025
        using \<open>Suc l < k\<close> \<open>k \<le> n\<close> by (simp add: t.enum_Suc l t.upd_inj)
lp15@61609
  1026
      finally have "(u l = upd i' \<and> u (Suc l) = upd (Suc i')) \<or>
hoelzl@56273
  1027
        (u l = upd (Suc i') \<and> u (Suc l) = upd i')"
nipkow@62390
  1028
        using \<open>Suc i' < n\<close> by (auto simp: enum_Suc fun_eq_iff split: if_split_asm)
hoelzl@56273
  1029
hoelzl@56273
  1030
      then have "t = s \<or> t = b.enum ` {..n}"
hoelzl@56273
  1031
      proof (elim disjE conjE)
hoelzl@56273
  1032
        assume u: "u l = upd i'"
hoelzl@56273
  1033
        have "c = t.enum (Suc l)" unfolding c_eq ..
hoelzl@56273
  1034
        also have "t.enum (Suc l) = enum (Suc i')"
wenzelm@60420
  1035
          using u \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close> by (simp add: enum_Suc t.enum_Suc l)
hoelzl@56273
  1036
        also have "\<dots> = a"
wenzelm@60420
  1037
          using \<open>a = enum i\<close> i by (simp add: i'_def)
hoelzl@56273
  1038
        finally show ?thesis
wenzelm@60420
  1039
          using eq_sma \<open>a \<in> s\<close> \<open>c \<in> t\<close> by auto
hoelzl@56273
  1040
      next
hoelzl@56273
  1041
        assume u: "u l = upd (Suc i')"
wenzelm@63040
  1042
        define B where "B = b.enum ` {..n}"
hoelzl@56273
  1043
        have "b.enum i' = enum i'"
hoelzl@56273
  1044
          using enum_eq_benum[of i'] i by (auto simp add: i'_def gr0_conv_Suc)
hoelzl@56273
  1045
        have "c = t.enum (Suc l)" unfolding c_eq ..
hoelzl@56273
  1046
        also have "t.enum (Suc l) = b.enum (Suc i')"
wenzelm@60420
  1047
          using u \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close>
wenzelm@60420
  1048
          by (simp_all add: enum_Suc t.enum_Suc l b.enum_Suc \<open>b.enum i' = enum i'\<close> swap_apply1)
hoelzl@56273
  1049
             (simp add: Suc_i')
hoelzl@56273
  1050
        also have "\<dots> = b.enum i"
hoelzl@56273
  1051
          using i by (simp add: i'_def)
hoelzl@56273
  1052
        finally have "c = b.enum i" .
hoelzl@56273
  1053
        then have "t - {c} = B - {c}" "c \<in> B"
hoelzl@56273
  1054
          unfolding eq_sma[symmetric] eq B_def using i by auto
wenzelm@60420
  1055
        with \<open>c \<in> t\<close> have "t = B"
hoelzl@56273
  1056
          by auto
hoelzl@56273
  1057
        then show ?thesis
hoelzl@56273
  1058
          by (simp add: B_def)
hoelzl@56273
  1059
      qed }
wenzelm@60420
  1060
    with ks_f' eq \<open>a \<noteq> b.enum i\<close> \<open>n \<noteq> 0\<close> \<open>i \<le> n\<close> show ?thesis
hoelzl@56273
  1061
      apply (intro ex1I[of _ "b.enum ` {.. n}"])
hoelzl@56273
  1062
      apply auto []
hoelzl@56273
  1063
      apply metis
hoelzl@56273
  1064
      done
hoelzl@56273
  1065
  qed
hoelzl@56273
  1066
  then show ?thesis
wenzelm@60420
  1067
    using s \<open>a \<in> s\<close> by (simp add: card_2_exists Ex1_def) metis
hoelzl@56273
  1068
qed
hoelzl@33741
  1069
wenzelm@60420
  1070
text \<open>Hence another step towards concreteness.\<close>
hoelzl@33741
  1071
hoelzl@33741
  1072
lemma kuhn_simplex_lemma:
hoelzl@56273
  1073
  assumes "\<forall>s. ksimplex p (Suc n) s \<longrightarrow> rl ` s \<subseteq> {.. Suc n}"
hoelzl@56273
  1074
    and "odd (card {f. \<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> (f = s - {a}) \<and>
hoelzl@56273
  1075
      rl ` f = {..n} \<and> ((\<exists>j\<le>n. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<le>n. \<forall>x\<in>f. x j = p))})"
hoelzl@56273
  1076
  shows "odd (card {s. ksimplex p (Suc n) s \<and> rl ` s = {..Suc n}})"
hoelzl@56273
  1077
proof (rule kuhn_complete_lemma[OF finite_ksimplexes refl, unfolded mem_Collect_eq,
hoelzl@56273
  1078
    where bnd="\<lambda>f. (\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = p)"],
hoelzl@56273
  1079
    safe del: notI)
hoelzl@56273
  1080
wenzelm@53186
  1081
  have *: "\<And>x y. x = y \<Longrightarrow> odd (card x) \<Longrightarrow> odd (card y)"
wenzelm@53186
  1082
    by auto
hoelzl@56273
  1083
  show "odd (card {f. (\<exists>s\<in>{s. ksimplex p (Suc n) s}. \<exists>a\<in>s. f = s - {a}) \<and>
hoelzl@56273
  1084
    rl ` f = {..n} \<and> ((\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = p))})"
wenzelm@53186
  1085
    apply (rule *[OF _ assms(2)])
hoelzl@56273
  1086
    apply (auto simp: atLeast0AtMost)
wenzelm@53186
  1087
    done
hoelzl@56273
  1088
hoelzl@56273
  1089
next
hoelzl@56273
  1090
hoelzl@56273
  1091
  fix s assume s: "ksimplex p (Suc n) s"
hoelzl@56273
  1092
  then show "card s = n + 2"
hoelzl@56273
  1093
    by (simp add: ksimplex_card)
hoelzl@56273
  1094
hoelzl@56273
  1095
  fix a assume a: "a \<in> s" then show "rl a \<le> Suc n"
hoelzl@56273
  1096
    using assms(1) s by (auto simp: subset_eq)
hoelzl@56273
  1097
hoelzl@56273
  1098
  let ?S = "{t. ksimplex p (Suc n) t \<and> (\<exists>b\<in>t. s - {a} = t - {b})}"
hoelzl@56273
  1099
  { fix j assume j: "j \<le> n" "\<forall>x\<in>s - {a}. x j = 0"
hoelzl@56273
  1100
    with s a show "card ?S = 1"
hoelzl@56273
  1101
      using ksimplex_replace_0[of p "n + 1" s a j]
hoelzl@56273
  1102
      by (subst eq_commute) simp }
hoelzl@56273
  1103
hoelzl@56273
  1104
  { fix j assume j: "j \<le> n" "\<forall>x\<in>s - {a}. x j = p"
hoelzl@56273
  1105
    with s a show "card ?S = 1"
hoelzl@56273
  1106
      using ksimplex_replace_1[of p "n + 1" s a j]
hoelzl@56273
  1107
      by (subst eq_commute) simp }
hoelzl@56273
  1108
hoelzl@56273
  1109
  { assume "card ?S \<noteq> 2" "\<not> (\<exists>j\<in>{..n}. \<forall>x\<in>s - {a}. x j = p)"
hoelzl@56273
  1110
    with s a show "\<exists>j\<in>{..n}. \<forall>x\<in>s - {a}. x j = 0"
hoelzl@56273
  1111
      using ksimplex_replace_2[of p "n + 1" s a]
hoelzl@56273
  1112
      by (subst (asm) eq_commute) auto }
wenzelm@53186
  1113
qed
wenzelm@53186
  1114
wenzelm@60420
  1115
subsection \<open>Reduced labelling\<close>
hoelzl@33741
  1116
hoelzl@56273
  1117
definition reduced :: "nat \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> nat" where "reduced n x = (LEAST k. k = n \<or> x k \<noteq> 0)"
hoelzl@33741
  1118
wenzelm@53186
  1119
lemma reduced_labelling:
hoelzl@56273
  1120
  shows "reduced n x \<le> n"
hoelzl@56273
  1121
    and "\<forall>i<reduced n x. x i = 0"
hoelzl@56273
  1122
    and "reduced n x = n \<or> x (reduced n x) \<noteq> 0"
wenzelm@53186
  1123
proof -
hoelzl@56273
  1124
  show "reduced n x \<le> n"
hoelzl@56273
  1125
    unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) auto
hoelzl@56273
  1126
  show "\<forall>i<reduced n x. x i = 0"
hoelzl@56273
  1127
    unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+
hoelzl@56273
  1128
  show "reduced n x = n \<or> x (reduced n x) \<noteq> 0"
hoelzl@56273
  1129
    unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+
wenzelm@53186
  1130
qed
hoelzl@33741
  1131
wenzelm@53186
  1132
lemma reduced_labelling_unique:
hoelzl@56273
  1133
  "r \<le> n \<Longrightarrow> \<forall>i<r. x i = 0 \<Longrightarrow> r = n \<or> x r \<noteq> 0 \<Longrightarrow> reduced n x = r"
hoelzl@56273
  1134
 unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) (metis le_less not_le)+
hoelzl@56273
  1135
hoelzl@56273
  1136
lemma reduced_labelling_zero: "j < n \<Longrightarrow> x j = 0 \<Longrightarrow> reduced n x \<noteq> j"
hoelzl@56273
  1137
  using reduced_labelling[of n x] by auto
hoelzl@33741
  1138
hoelzl@56273
  1139
lemma reduce_labelling_zero[simp]: "reduced 0 x = 0"
hoelzl@56273
  1140
  by (rule reduced_labelling_unique) auto
hoelzl@33741
  1141
hoelzl@56273
  1142
lemma reduced_labelling_nonzero: "j < n \<Longrightarrow> x j \<noteq> 0 \<Longrightarrow> reduced n x \<le> j"
hoelzl@56273
  1143
  using reduced_labelling[of n x] by (elim allE[where x=j]) auto
hoelzl@33741
  1144
hoelzl@56273
  1145
lemma reduced_labelling_Suc: "reduced (Suc n) x \<noteq> Suc n \<Longrightarrow> reduced (Suc n) x = reduced n x"
hoelzl@56273
  1146
  using reduced_labelling[of "Suc n" x]
hoelzl@56273
  1147
  by (intro reduced_labelling_unique[symmetric]) auto
hoelzl@33741
  1148
hoelzl@33741
  1149
lemma complete_face_top:
hoelzl@56273
  1150
  assumes "\<forall>x\<in>f. \<forall>j\<le>n. x j = 0 \<longrightarrow> lab x j = 0"
hoelzl@56273
  1151
    and "\<forall>x\<in>f. \<forall>j\<le>n. x j = p \<longrightarrow> lab x j = 1"
hoelzl@56273
  1152
    and eq: "(reduced (Suc n) \<circ> lab) ` f = {..n}"
hoelzl@56273
  1153
  shows "((\<exists>j\<le>n. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<le>n. \<forall>x\<in>f. x j = p)) \<longleftrightarrow> (\<forall>x\<in>f. x n = p)"
hoelzl@56273
  1154
proof (safe del: disjCI)
hoelzl@56273
  1155
  fix x j assume j: "j \<le> n" "\<forall>x\<in>f. x j = 0"
hoelzl@56273
  1156
  { fix x assume "x \<in> f" with assms j have "reduced (Suc n) (lab x) \<noteq> j"
hoelzl@56273
  1157
      by (intro reduced_labelling_zero) auto }
hoelzl@56273
  1158
  moreover have "j \<in> (reduced (Suc n) \<circ> lab) ` f"
hoelzl@56273
  1159
    using j eq by auto
hoelzl@56273
  1160
  ultimately show "x n = p"
hoelzl@56273
  1161
    by force
hoelzl@56273
  1162
next
hoelzl@56273
  1163
  fix x j assume j: "j \<le> n" "\<forall>x\<in>f. x j = p" and x: "x \<in> f"
hoelzl@56273
  1164
  have "j = n"
hoelzl@56273
  1165
  proof (rule ccontr)
hoelzl@56273
  1166
    assume "\<not> ?thesis"
hoelzl@56273
  1167
    { fix x assume "x \<in> f"
hoelzl@56273
  1168
      with assms j have "reduced (Suc n) (lab x) \<le> j"
hoelzl@56273
  1169
        by (intro reduced_labelling_nonzero) auto
hoelzl@56273
  1170
      then have "reduced (Suc n) (lab x) \<noteq> n"
wenzelm@60420
  1171
        using \<open>j \<noteq> n\<close> \<open>j \<le> n\<close> by simp }
hoelzl@56273
  1172
    moreover
lp15@61609
  1173
    have "n \<in> (reduced (Suc n) \<circ> lab) ` f"
hoelzl@56273
  1174
      using eq by auto
hoelzl@56273
  1175
    ultimately show False
hoelzl@56273
  1176
      by force
wenzelm@53186
  1177
  qed
hoelzl@56273
  1178
  moreover have "j \<in> (reduced (Suc n) \<circ> lab) ` f"
hoelzl@56273
  1179
    using j eq by auto
hoelzl@56273
  1180
  ultimately show "x n = p"
hoelzl@56273
  1181
    using j x by auto
wenzelm@53688
  1182
qed auto
hoelzl@33741
  1183
wenzelm@60420
  1184
text \<open>Hence we get just about the nice induction.\<close>
hoelzl@33741
  1185
hoelzl@33741
  1186
lemma kuhn_induction:
wenzelm@53688
  1187
  assumes "0 < p"
hoelzl@56273
  1188
    and lab_0: "\<forall>x. \<forall>j\<le>n. (\<forall>j. x j \<le> p) \<and> x j = 0 \<longrightarrow> lab x j = 0"
hoelzl@56273
  1189
    and lab_1: "\<forall>x. \<forall>j\<le>n. (\<forall>j. x j \<le> p) \<and> x j = p \<longrightarrow> lab x j = 1"
hoelzl@56273
  1190
    and odd: "odd (card {s. ksimplex p n s \<and> (reduced n\<circ>lab) ` s = {..n}})"
hoelzl@56273
  1191
  shows "odd (card {s. ksimplex p (Suc n) s \<and> (reduced (Suc n)\<circ>lab) ` s = {..Suc n}})"
wenzelm@53248
  1192
proof -
hoelzl@56273
  1193
  let ?rl = "reduced (Suc n) \<circ> lab" and ?ext = "\<lambda>f v. \<exists>j\<le>n. \<forall>x\<in>f. x j = v"
hoelzl@56273
  1194
  let ?ext = "\<lambda>s. (\<exists>j\<le>n. \<forall>x\<in>s. x j = 0) \<or> (\<exists>j\<le>n. \<forall>x\<in>s. x j = p)"
hoelzl@56273
  1195
  have "\<forall>s. ksimplex p (Suc n) s \<longrightarrow> ?rl ` s \<subseteq> {..Suc n}"
hoelzl@56273
  1196
    by (simp add: reduced_labelling subset_eq)
hoelzl@56273
  1197
  moreover
hoelzl@56273
  1198
  have "{s. ksimplex p n s \<and> (reduced n \<circ> lab) ` s = {..n}} =
hoelzl@56273
  1199
        {f. \<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> f = s - {a} \<and> ?rl ` f = {..n} \<and> ?ext f}"
hoelzl@56273
  1200
  proof (intro set_eqI, safe del: disjCI equalityI disjE)
hoelzl@56273
  1201
    fix s assume s: "ksimplex p n s" and rl: "(reduced n \<circ> lab) ` s = {..n}"
hoelzl@56273
  1202
    from s obtain u b where "kuhn_simplex p n u b s" by (auto elim: ksimplex.cases)
hoelzl@56273
  1203
    then interpret kuhn_simplex p n u b s .
hoelzl@56273
  1204
    have all_eq_p: "\<forall>x\<in>s. x n = p"
hoelzl@56273
  1205
      by (auto simp: out_eq_p)
hoelzl@56273
  1206
    moreover
hoelzl@56273
  1207
    { fix x assume "x \<in> s"
hoelzl@56273
  1208
      with lab_1[rule_format, of n x] all_eq_p s_le_p[of x]
hoelzl@56273
  1209
      have "?rl x \<le> n"
hoelzl@56273
  1210
        by (auto intro!: reduced_labelling_nonzero)
hoelzl@56273
  1211
      then have "?rl x = reduced n (lab x)"
hoelzl@56273
  1212
        by (auto intro!: reduced_labelling_Suc) }
hoelzl@56273
  1213
    then have "?rl ` s = {..n}"
hoelzl@56273
  1214
      using rl by (simp cong: image_cong)
hoelzl@56273
  1215
    moreover
hoelzl@56273
  1216
    obtain t a where "ksimplex p (Suc n) t" "a \<in> t" "s = t - {a}"
wenzelm@60420
  1217
      using s unfolding simplex_top_face[OF \<open>0 < p\<close> all_eq_p] by auto
hoelzl@56273
  1218
    ultimately
hoelzl@56273
  1219
    show "\<exists>t a. ksimplex p (Suc n) t \<and> a \<in> t \<and> s = t - {a} \<and> ?rl ` s = {..n} \<and> ?ext s"
wenzelm@53688
  1220
      by auto
wenzelm@53248
  1221
  next
hoelzl@56273
  1222
    fix x s a assume s: "ksimplex p (Suc n) s" and rl: "?rl ` (s - {a}) = {.. n}"
hoelzl@56273
  1223
      and a: "a \<in> s" and "?ext (s - {a})"
hoelzl@56273
  1224
    from s obtain u b where "kuhn_simplex p (Suc n) u b s" by (auto elim: ksimplex.cases)
hoelzl@56273
  1225
    then interpret kuhn_simplex p "Suc n" u b s .
hoelzl@56273
  1226
    have all_eq_p: "\<forall>x\<in>s. x (Suc n) = p"
hoelzl@56273
  1227
      by (auto simp: out_eq_p)
hoelzl@56273
  1228
hoelzl@56273
  1229
    { fix x assume "x \<in> s - {a}"
hoelzl@56273
  1230
      then have "?rl x \<in> ?rl ` (s - {a})"
wenzelm@53248
  1231
        by auto
hoelzl@56273
  1232
      then have "?rl x \<le> n"
hoelzl@56273
  1233
        unfolding rl by auto
hoelzl@56273
  1234
      then have "?rl x = reduced n (lab x)"
hoelzl@56273
  1235
        by (auto intro!: reduced_labelling_Suc) }
hoelzl@56273
  1236
    then show rl': "(reduced n\<circ>lab) ` (s - {a}) = {..n}"
hoelzl@56273
  1237
      unfolding rl[symmetric] by (intro image_cong) auto
hoelzl@56273
  1238
wenzelm@60420
  1239
    from \<open>?ext (s - {a})\<close>
hoelzl@56273
  1240
    have all_eq_p: "\<forall>x\<in>s - {a}. x n = p"
hoelzl@56273
  1241
    proof (elim disjE exE conjE)
hoelzl@56273
  1242
      fix j assume "j \<le> n" "\<forall>x\<in>s - {a}. x j = 0"
hoelzl@56273
  1243
      with lab_0[rule_format, of j] all_eq_p s_le_p
hoelzl@56273
  1244
      have "\<And>x. x \<in> s - {a} \<Longrightarrow> reduced (Suc n) (lab x) \<noteq> j"
hoelzl@56273
  1245
        by (intro reduced_labelling_zero) auto
hoelzl@56273
  1246
      moreover have "j \<in> ?rl ` (s - {a})"
wenzelm@60420
  1247
        using \<open>j \<le> n\<close> unfolding rl by auto
hoelzl@56273
  1248
      ultimately show ?thesis
hoelzl@56273
  1249
        by force
wenzelm@53248
  1250
    next
hoelzl@56273
  1251
      fix j assume "j \<le> n" and eq_p: "\<forall>x\<in>s - {a}. x j = p"
hoelzl@56273
  1252
      show ?thesis
hoelzl@56273
  1253
      proof cases
hoelzl@56273
  1254
        assume "j = n" with eq_p show ?thesis by simp
hoelzl@56273
  1255
      next
hoelzl@56273
  1256
        assume "j \<noteq> n"
hoelzl@56273
  1257
        { fix x assume x: "x \<in> s - {a}"
hoelzl@56273
  1258
          have "reduced n (lab x) \<le> j"
hoelzl@56273
  1259
          proof (rule reduced_labelling_nonzero)
hoelzl@56273
  1260
            show "lab x j \<noteq> 0"
wenzelm@60420
  1261
              using lab_1[rule_format, of j x] x s_le_p[of x] eq_p \<open>j \<le> n\<close> by auto
hoelzl@56273
  1262
            show "j < n"
wenzelm@60420
  1263
              using \<open>j \<le> n\<close> \<open>j \<noteq> n\<close> by simp
hoelzl@56273
  1264
          qed
hoelzl@56273
  1265
          then have "reduced n (lab x) \<noteq> n"
wenzelm@60420
  1266
            using \<open>j \<le> n\<close> \<open>j \<noteq> n\<close> by simp }
hoelzl@56273
  1267
        moreover have "n \<in> (reduced n\<circ>lab) ` (s - {a})"
hoelzl@56273
  1268
          unfolding rl' by auto
hoelzl@56273
  1269
        ultimately show ?thesis
hoelzl@56273
  1270
          by force
hoelzl@56273
  1271
      qed
wenzelm@53248
  1272
    qed
hoelzl@56273
  1273
    show "ksimplex p n (s - {a})"
wenzelm@60420
  1274
      unfolding simplex_top_face[OF \<open>0 < p\<close> all_eq_p] using s a by auto
wenzelm@53248
  1275
  qed
hoelzl@56273
  1276
  ultimately show ?thesis
hoelzl@56273
  1277
    using assms by (intro kuhn_simplex_lemma) auto
wenzelm@53248
  1278
qed
hoelzl@33741
  1279
wenzelm@60420
  1280
text \<open>And so we get the final combinatorial result.\<close>
hoelzl@33741
  1281
wenzelm@53688
  1282
lemma ksimplex_0: "ksimplex p 0 s \<longleftrightarrow> s = {(\<lambda>x. p)}"
wenzelm@53248
  1283
proof
hoelzl@56273
  1284
  assume "ksimplex p 0 s" then show "s = {(\<lambda>x. p)}"
hoelzl@56273
  1285
    by (blast dest: kuhn_simplex.ksimplex_0 elim: ksimplex.cases)
wenzelm@53248
  1286
next
hoelzl@56273
  1287
  assume s: "s = {(\<lambda>x. p)}"
hoelzl@56273
  1288
  show "ksimplex p 0 s"
hoelzl@56273
  1289
  proof (intro ksimplex, unfold_locales)
hoelzl@56273
  1290
    show "(\<lambda>_. p) \<in> {..<0::nat} \<rightarrow> {..<p}" by auto
hoelzl@56273
  1291
    show "bij_betw id {..<0} {..<0}"
hoelzl@56273
  1292
      by simp
hoelzl@56273
  1293
  qed (auto simp: s)
wenzelm@53248
  1294
qed
hoelzl@33741
  1295
hoelzl@33741
  1296
lemma kuhn_combinatorial:
wenzelm@53688
  1297
  assumes "0 < p"
hoelzl@56273
  1298
    and "\<forall>x j. (\<forall>j. x j \<le> p) \<and> j < n \<and> x j = 0 \<longrightarrow> lab x j = 0"
hoelzl@56273
  1299
    and "\<forall>x j. (\<forall>j. x j \<le> p) \<and> j < n  \<and> x j = p \<longrightarrow> lab x j = 1"
hoelzl@56273
  1300
  shows "odd (card {s. ksimplex p n s \<and> (reduced n\<circ>lab) ` s = {..n}})"
hoelzl@56273
  1301
    (is "odd (card (?M n))")
wenzelm@53248
  1302
  using assms
wenzelm@53248
  1303
proof (induct n)
hoelzl@56273
  1304
  case 0 then show ?case
hoelzl@56273
  1305
    by (simp add: ksimplex_0 cong: conj_cong)
hoelzl@56273
  1306
next
hoelzl@56273
  1307
  case (Suc n)
hoelzl@56273
  1308
  then have "odd (card (?M n))"
hoelzl@56273
  1309
    by force
hoelzl@56273
  1310
  with Suc show ?case
hoelzl@56273
  1311
    using kuhn_induction[of p n] by (auto simp: comp_def)
wenzelm@53248
  1312
qed
hoelzl@33741
  1313
wenzelm@53248
  1314
lemma kuhn_lemma:
wenzelm@53688
  1315
  fixes n p :: nat
wenzelm@53688
  1316
  assumes "0 < p"
hoelzl@56273
  1317
    and "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. label x i = (0::nat) \<or> label x i = 1)"
hoelzl@56273
  1318
    and "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow> label x i = 0)"
hoelzl@56273
  1319
    and "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = p \<longrightarrow> label x i = 1)"
hoelzl@56273
  1320
  obtains q where "\<forall>i<n. q i < p"
hoelzl@56273
  1321
    and "\<forall>i<n. \<exists>r s. (\<forall>j<n. q j \<le> r j \<and> r j \<le> q j + 1) \<and> (\<forall>j<n. q j \<le> s j \<and> s j \<le> q j + 1) \<and> label r i \<noteq> label s i"
wenzelm@53248
  1322
proof -
wenzelm@60580
  1323
  let ?rl = "reduced n \<circ> label"
hoelzl@56273
  1324
  let ?A = "{s. ksimplex p n s \<and> ?rl ` s = {..n}}"
wenzelm@53248
  1325
  have "odd (card ?A)"
hoelzl@56273
  1326
    using assms by (intro kuhn_combinatorial[of p n label]) auto
wenzelm@53688
  1327
  then have "?A \<noteq> {}"
wenzelm@60580
  1328
    by fastforce
hoelzl@56273
  1329
  then obtain s b u where "kuhn_simplex p n b u s" and rl: "?rl ` s = {..n}"
hoelzl@56273
  1330
    by (auto elim: ksimplex.cases)
hoelzl@56273
  1331
  interpret kuhn_simplex p n b u s by fact
hoelzl@56273
  1332
wenzelm@53248
  1333
  show ?thesis
hoelzl@56273
  1334
  proof (intro that[of b] allI impI)
wenzelm@60580
  1335
    fix i
wenzelm@60580
  1336
    assume "i < n"
wenzelm@60580
  1337
    then show "b i < p"
hoelzl@56273
  1338
      using base by auto
wenzelm@53248
  1339
  next
wenzelm@60580
  1340
    fix i
wenzelm@60580
  1341
    assume "i < n"
hoelzl@56273
  1342
    then have "i \<in> {.. n}" "Suc i \<in> {.. n}"
hoelzl@56273
  1343
      by auto
hoelzl@56273
  1344
    then obtain u v where u: "u \<in> s" "Suc i = ?rl u" and v: "v \<in> s" "i = ?rl v"
hoelzl@56273
  1345
      unfolding rl[symmetric] by blast
hoelzl@56273
  1346
hoelzl@56273
  1347
    have "label u i \<noteq> label v i"
hoelzl@56273
  1348
      using reduced_labelling [of n "label u"] reduced_labelling [of n "label v"]
wenzelm@60420
  1349
        u(2)[symmetric] v(2)[symmetric] \<open>i < n\<close>
hoelzl@56273
  1350
      by auto
hoelzl@56273
  1351
    moreover
wenzelm@60580
  1352
    have "b j \<le> u j" "u j \<le> b j + 1" "b j \<le> v j" "v j \<le> b j + 1" if "j < n" for j
wenzelm@60580
  1353
      using that base_le[OF \<open>u\<in>s\<close>] le_Suc_base[OF \<open>u\<in>s\<close>] base_le[OF \<open>v\<in>s\<close>] le_Suc_base[OF \<open>v\<in>s\<close>]
wenzelm@60580
  1354
      by auto
wenzelm@60580
  1355
    ultimately show "\<exists>r s. (\<forall>j<n. b j \<le> r j \<and> r j \<le> b j + 1) \<and>
wenzelm@60580
  1356
        (\<forall>j<n. b j \<le> s j \<and> s j \<le> b j + 1) \<and> label r i \<noteq> label s i"
hoelzl@56273
  1357
      by blast
wenzelm@53248
  1358
  qed
wenzelm@53248
  1359
qed
hoelzl@33741
  1360
wenzelm@60420
  1361
subsection \<open>The main result for the unit cube\<close>
hoelzl@33741
  1362
hoelzl@33741
  1363
lemma kuhn_labelling_lemma':
wenzelm@53688
  1364
  assumes "(\<forall>x::nat\<Rightarrow>real. P x \<longrightarrow> P (f x))"
wenzelm@53688
  1365
    and "\<forall>x. P x \<longrightarrow> (\<forall>i::nat. Q i \<longrightarrow> 0 \<le> x i \<and> x i \<le> 1)"
hoelzl@33741
  1366
  shows "\<exists>l. (\<forall>x i. l x i \<le> (1::nat)) \<and>
wenzelm@53688
  1367
             (\<forall>x i. P x \<and> Q i \<and> x i = 0 \<longrightarrow> l x i = 0) \<and>
wenzelm@53688
  1368
             (\<forall>x i. P x \<and> Q i \<and> x i = 1 \<longrightarrow> l x i = 1) \<and>
wenzelm@53688
  1369
             (\<forall>x i. P x \<and> Q i \<and> l x i = 0 \<longrightarrow> x i \<le> f x i) \<and>
wenzelm@53688
  1370
             (\<forall>x i. P x \<and> Q i \<and> l x i = 1 \<longrightarrow> f x i \<le> x i)"
wenzelm@53185
  1371
proof -
wenzelm@53688
  1372
  have and_forall_thm: "\<And>P Q. (\<forall>x. P x) \<and> (\<forall>x. Q x) \<longleftrightarrow> (\<forall>x. P x \<and> Q x)"
wenzelm@53688
  1373
    by auto
wenzelm@53688
  1374
  have *: "\<forall>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow> x \<noteq> 1 \<and> x \<le> y \<or> x \<noteq> 0 \<and> y \<le> x"
wenzelm@53185
  1375
    by auto
wenzelm@53185
  1376
  show ?thesis
wenzelm@53185
  1377
    unfolding and_forall_thm
wenzelm@53185
  1378
    apply (subst choice_iff[symmetric])+
wenzelm@53688
  1379
    apply rule
wenzelm@53688
  1380
    apply rule
wenzelm@53688
  1381
  proof -
wenzelm@60580
  1382
    fix x x'
wenzelm@53688
  1383
    let ?R = "\<lambda>y::nat.
wenzelm@60580
  1384
      (P x \<and> Q x' \<and> x x' = 0 \<longrightarrow> y = 0) \<and>
wenzelm@60580
  1385
      (P x \<and> Q x' \<and> x x' = 1 \<longrightarrow> y = 1) \<and>
wenzelm@60580
  1386
      (P x \<and> Q x' \<and> y = 0 \<longrightarrow> x x' \<le> (f x) x') \<and>
wenzelm@60580
  1387
      (P x \<and> Q x' \<and> y = 1 \<longrightarrow> (f x) x' \<le> x x')"
wenzelm@60580
  1388
    have "0 \<le> f x x' \<and> f x x' \<le> 1" if "P x" "Q x'"
wenzelm@60580
  1389
      using assms(2)[rule_format,of "f x" x'] that
wenzelm@60580
  1390
      apply (drule_tac assms(1)[rule_format])
wenzelm@60580
  1391
      apply auto
wenzelm@60580
  1392
      done
wenzelm@53688
  1393
    then have "?R 0 \<or> ?R 1"
wenzelm@53688
  1394
      by auto
wenzelm@60580
  1395
    then show "\<exists>y\<le>1. ?R y"
wenzelm@53688
  1396
      by auto
wenzelm@53185
  1397
  qed
wenzelm@53185
  1398
qed
hoelzl@33741
  1399
huffman@56117
  1400
definition unit_cube :: "'a::euclidean_space set"
huffman@56117
  1401
  where "unit_cube = {x. \<forall>i\<in>Basis. 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1}"
huffman@56117
  1402
huffman@56117
  1403
lemma mem_unit_cube: "x \<in> unit_cube \<longleftrightarrow> (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
huffman@56117
  1404
  unfolding unit_cube_def by simp
huffman@56117
  1405
huffman@56117
  1406
lemma bounded_unit_cube: "bounded unit_cube"
huffman@56117
  1407
  unfolding bounded_def
huffman@56117
  1408
proof (intro exI ballI)
huffman@56117
  1409
  fix y :: 'a assume y: "y \<in> unit_cube"
huffman@56117
  1410
  have "dist 0 y = norm y" by (rule dist_0_norm)
huffman@56117
  1411
  also have "\<dots> = norm (\<Sum>i\<in>Basis. (y \<bullet> i) *\<^sub>R i)" unfolding euclidean_representation ..
nipkow@64267
  1412
  also have "\<dots> \<le> (\<Sum>i\<in>Basis. norm ((y \<bullet> i) *\<^sub>R i))" by (rule norm_sum)
huffman@56117
  1413
  also have "\<dots> \<le> (\<Sum>i::'a\<in>Basis. 1)"
nipkow@64267
  1414
    by (rule sum_mono, simp add: y [unfolded mem_unit_cube])
huffman@56117
  1415
  finally show "dist 0 y \<le> (\<Sum>i::'a\<in>Basis. 1)" .
huffman@56117
  1416
qed
huffman@56117
  1417
huffman@56117
  1418
lemma closed_unit_cube: "closed unit_cube"
huffman@56117
  1419
  unfolding unit_cube_def Collect_ball_eq Collect_conj_eq
hoelzl@63332
  1420
  by (rule closed_INT, auto intro!: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
huffman@56117
  1421
huffman@56117
  1422
lemma compact_unit_cube: "compact unit_cube" (is "compact ?C")
huffman@56117
  1423
  unfolding compact_eq_seq_compact_metric
huffman@56117
  1424
  using bounded_unit_cube closed_unit_cube
huffman@56117
  1425
  by (rule bounded_closed_imp_seq_compact)
huffman@56117
  1426
hoelzl@50526
  1427
lemma brouwer_cube:
huffman@56117
  1428
  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
huffman@56117
  1429
  assumes "continuous_on unit_cube f"
huffman@56117
  1430
    and "f ` unit_cube \<subseteq> unit_cube"
huffman@56117
  1431
  shows "\<exists>x\<in>unit_cube. f x = x"
wenzelm@53185
  1432
proof (rule ccontr)
wenzelm@63040
  1433
  define n where "n = DIM('a)"
wenzelm@53185
  1434
  have n: "1 \<le> n" "0 < n" "n \<noteq> 0"
wenzelm@53185
  1435
    unfolding n_def by (auto simp add: Suc_le_eq DIM_positive)
wenzelm@53674
  1436
  assume "\<not> ?thesis"
huffman@56117
  1437
  then have *: "\<not> (\<exists>x\<in>unit_cube. f x - x = 0)"
wenzelm@53674
  1438
    by auto
wenzelm@55522
  1439
  obtain d where
huffman@56117
  1440
      d: "d > 0" "\<And>x. x \<in> unit_cube \<Longrightarrow> d \<le> norm (f x - x)"
huffman@56117
  1441
    apply (rule brouwer_compactness_lemma[OF compact_unit_cube _ *])
hoelzl@56371
  1442
    apply (rule continuous_intros assms)+
wenzelm@55522
  1443
    apply blast
wenzelm@53185
  1444
    done
huffman@56117
  1445
  have *: "\<forall>x. x \<in> unit_cube \<longrightarrow> f x \<in> unit_cube"
huffman@56117
  1446
    "\<forall>x. x \<in> (unit_cube::'a set) \<longrightarrow> (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
wenzelm@53185
  1447
    using assms(2)[unfolded image_subset_iff Ball_def]
huffman@56117
  1448
    unfolding mem_unit_cube
wenzelm@55522
  1449
    by auto
wenzelm@55522
  1450
  obtain label :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where
wenzelm@55522
  1451
    "\<forall>x. \<forall>i\<in>Basis. label x i \<le> 1"
huffman@56117
  1452
    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> x \<bullet> i = 0 \<longrightarrow> label x i = 0"
huffman@56117
  1453
    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> x \<bullet> i = 1 \<longrightarrow> label x i = 1"
huffman@56117
  1454
    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> label x i = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i"
huffman@56117
  1455
    "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> label x i = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
wenzelm@55522
  1456
    using kuhn_labelling_lemma[OF *] by blast
wenzelm@53185
  1457
  note label = this [rule_format]
huffman@56117
  1458
  have lem1: "\<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>i\<in>Basis. label x i \<noteq> label y i \<longrightarrow>
wenzelm@61945
  1459
    \<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
wenzelm@53185
  1460
  proof safe
wenzelm@53185
  1461
    fix x y :: 'a
huffman@56117
  1462
    assume x: "x \<in> unit_cube"
huffman@56117
  1463
    assume y: "y \<in> unit_cube"
wenzelm@53185
  1464
    fix i
wenzelm@53185
  1465
    assume i: "label x i \<noteq> label y i" "i \<in> Basis"
wenzelm@53185
  1466
    have *: "\<And>x y fx fy :: real. x \<le> fx \<and> fy \<le> y \<or> fx \<le> x \<and> y \<le> fy \<Longrightarrow>
wenzelm@61945
  1467
      \<bar>fx - x\<bar> \<le> \<bar>fy - fx\<bar> + \<bar>y - x\<bar>" by auto
wenzelm@61945
  1468
    have "\<bar>(f x - x) \<bullet> i\<bar> \<le> \<bar>(f y - f x)\<bullet>i\<bar> + \<bar>(y - x)\<bullet>i\<bar>"
hoelzl@50526
  1469
      unfolding inner_simps
wenzelm@53185
  1470
      apply (rule *)
wenzelm@53185
  1471
      apply (cases "label x i = 0")
wenzelm@53688
  1472
      apply (rule disjI1)
wenzelm@53688
  1473
      apply rule
wenzelm@53185
  1474
      prefer 3
wenzelm@53688
  1475
      apply (rule disjI2)
wenzelm@53688
  1476
      apply rule
wenzelm@53688
  1477
    proof -
wenzelm@53185
  1478
      assume lx: "label x i = 0"
wenzelm@53674
  1479
      then have ly: "label y i = 1"
wenzelm@53688
  1480
        using i label(1)[of i y]
wenzelm@53688
  1481
        by auto
wenzelm@53185
  1482
      show "x \<bullet> i \<le> f x \<bullet> i"
wenzelm@53185
  1483
        apply (rule label(4)[rule_format])
wenzelm@53674
  1484
        using x y lx i(2)
wenzelm@53252
  1485
        apply auto
wenzelm@53185
  1486
        done
wenzelm@53185
  1487
      show "f y \<bullet> i \<le> y \<bullet> i"
wenzelm@53185
  1488
        apply (rule label(5)[rule_format])
wenzelm@53674
  1489
        using x y ly i(2)
wenzelm@53252
  1490
        apply auto
wenzelm@53185
  1491
        done
wenzelm@53185
  1492
    next
wenzelm@53185
  1493
      assume "label x i \<noteq> 0"
wenzelm@53688
  1494
      then have l: "label x i = 1" "label y i = 0"
wenzelm@53688
  1495
        using i label(1)[of i x] label(1)[of i y]
wenzelm@53688
  1496
        by auto
wenzelm@53185
  1497
      show "f x \<bullet> i \<le> x \<bullet> i"
wenzelm@53185
  1498
        apply (rule label(5)[rule_format])
wenzelm@53674
  1499
        using x y l i(2)
wenzelm@53252
  1500
        apply auto
wenzelm@53185
  1501
        done
wenzelm@53185
  1502
      show "y \<bullet> i \<le> f y \<bullet> i"
wenzelm@53185
  1503
        apply (rule label(4)[rule_format])
wenzelm@53674
  1504
        using x y l i(2)
wenzelm@53252
  1505
        apply auto
wenzelm@53185
  1506
        done
wenzelm@53185
  1507
    qed
wenzelm@53185
  1508
    also have "\<dots> \<le> norm (f y - f x) + norm (y - x)"
wenzelm@53185
  1509
      apply (rule add_mono)
wenzelm@53185
  1510
      apply (rule Basis_le_norm[OF i(2)])+
wenzelm@53185
  1511
      done
wenzelm@53185
  1512
    finally show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
wenzelm@53185
  1513
      unfolding inner_simps .
hoelzl@50526
  1514
  qed
huffman@56117
  1515
  have "\<exists>e>0. \<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>z\<in>unit_cube. \<forall>i\<in>Basis.
wenzelm@53688
  1516
    norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<longrightarrow>
wenzelm@61945
  1517
      \<bar>(f(z) - z)\<bullet>i\<bar> < d / (real n)"
wenzelm@53185
  1518
  proof -
wenzelm@53688
  1519
    have d': "d / real n / 8 > 0"
nipkow@56541
  1520
      using d(1) by (simp add: n_def DIM_positive)
huffman@56117
  1521
    have *: "uniformly_continuous_on unit_cube f"
huffman@56117
  1522
      by (rule compact_uniformly_continuous[OF assms(1) compact_unit_cube])
wenzelm@55522
  1523
    obtain e where e:
wenzelm@55522
  1524
        "e > 0"
huffman@56117
  1525
        "\<And>x x'. x \<in> unit_cube \<Longrightarrow>
huffman@56117
  1526
          x' \<in> unit_cube \<Longrightarrow>
wenzelm@55522
  1527
          norm (x' - x) < e \<Longrightarrow>
wenzelm@55522
  1528
          norm (f x' - f x) < d / real n / 8"
wenzelm@55522
  1529
      using *[unfolded uniformly_continuous_on_def,rule_format,OF d']
wenzelm@55522
  1530
      unfolding dist_norm
wenzelm@55522
  1531
      by blast
wenzelm@53185
  1532
    show ?thesis
wenzelm@53185
  1533
      apply (rule_tac x="min (e/2) (d/real n/8)" in exI)
wenzelm@53248
  1534
      apply safe
wenzelm@53248
  1535
    proof -
wenzelm@53185
  1536
      show "0 < min (e / 2) (d / real n / 8)"
wenzelm@53185
  1537
        using d' e by auto
wenzelm@53185
  1538
      fix x y z i
wenzelm@53688
  1539
      assume as:
huffman@56117
  1540
        "x \<in> unit_cube" "y \<in> unit_cube" "z \<in> unit_cube"
hoelzl@37489
  1541
        "norm (x - z) < min (e / 2) (d / real n / 8)"
wenzelm@53688
  1542
        "norm (y - z) < min (e / 2) (d / real n / 8)"
wenzelm@53688
  1543
        "label x i \<noteq> label y i"
wenzelm@53688
  1544
      assume i: "i \<in> Basis"
wenzelm@61945
  1545
      have *: "\<And>z fz x fx n1 n2 n3 n4 d4 d :: real. \<bar>fx - x\<bar> \<le> n1 + n2 \<Longrightarrow>
wenzelm@61945
  1546
        \<bar>fx - fz\<bar> \<le> n3 \<Longrightarrow> \<bar>x - z\<bar> \<le> n4 \<Longrightarrow>
wenzelm@53185
  1547
        n1 < d4 \<Longrightarrow> n2 < 2 * d4 \<Longrightarrow> n3 < d4 \<Longrightarrow> n4 < d4 \<Longrightarrow>
wenzelm@61945
  1548
        (8 * d4 = d) \<Longrightarrow> \<bar>fz - z\<bar> < d"
wenzelm@53688
  1549
        by auto
wenzelm@53688
  1550
      show "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
wenzelm@53688
  1551
        unfolding inner_simps
wenzelm@53185
  1552
      proof (rule *)
wenzelm@53185
  1553
        show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y -f x) + norm (y - x)"
wenzelm@53185
  1554
          apply (rule lem1[rule_format])
wenzelm@53688
  1555
          using as i
wenzelm@53688
  1556
          apply auto
wenzelm@53185
  1557
          done
hoelzl@50526
  1558
        show "\<bar>f x \<bullet> i - f z \<bullet> i\<bar> \<le> norm (f x - f z)" "\<bar>x \<bullet> i - z \<bullet> i\<bar> \<le> norm (x - z)"
wenzelm@55522
  1559
          unfolding inner_diff_left[symmetric]
wenzelm@53688
  1560
          by (rule Basis_le_norm[OF i])+
wenzelm@53688
  1561
        have tria: "norm (y - x) \<le> norm (y - z) + norm (x - z)"
wenzelm@53185
  1562
          using dist_triangle[of y x z, unfolded dist_norm]
wenzelm@53688
  1563
          unfolding norm_minus_commute
wenzelm@53688
  1564
          by auto
wenzelm@53185
  1565
        also have "\<dots> < e / 2 + e / 2"
wenzelm@53185
  1566
          apply (rule add_strict_mono)
wenzelm@53252
  1567
          using as(4,5)
wenzelm@53252
  1568
          apply auto
wenzelm@53185
  1569
          done
wenzelm@53185
  1570
        finally show "norm (f y - f x) < d / real n / 8"
wenzelm@53185
  1571
          apply -
wenzelm@53185
  1572
          apply (rule e(2))
wenzelm@53252
  1573
          using as
wenzelm@53252
  1574
          apply auto
wenzelm@53185
  1575
          done
wenzelm@53185
  1576
        have "norm (y - z) + norm (x - z) < d / real n / 8 + d / real n / 8"
wenzelm@53185
  1577
          apply (rule add_strict_mono)
wenzelm@53252
  1578
          using as
wenzelm@53252
  1579
          apply auto
wenzelm@53185
  1580
          done
wenzelm@53688
  1581
        then show "norm (y - x) < 2 * (d / real n / 8)"
wenzelm@53688
  1582
          using tria
wenzelm@53688
  1583
          by auto
wenzelm@53185
  1584
        show "norm (f x - f z) < d / real n / 8"
wenzelm@53185
  1585
          apply (rule e(2))
wenzelm@53252
  1586
          using as e(1)
wenzelm@53252
  1587
          apply auto
wenzelm@53185
  1588
          done
wenzelm@53185
  1589
      qed (insert as, auto)
wenzelm@53185
  1590
    qed
wenzelm@53185
  1591
  qed
wenzelm@55522
  1592
  then
wenzelm@55522
  1593
  obtain e where e:
wenzelm@55522
  1594
    "e > 0"
huffman@56117
  1595
    "\<And>x y z i. x \<in> unit_cube \<Longrightarrow>
huffman@56117
  1596
      y \<in> unit_cube \<Longrightarrow>
huffman@56117
  1597
      z \<in> unit_cube \<Longrightarrow>
wenzelm@55522
  1598
      i \<in> Basis \<Longrightarrow>
wenzelm@55522
  1599
      norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<Longrightarrow>
wenzelm@55522
  1600
      \<bar>(f z - z) \<bullet> i\<bar> < d / real n"
wenzelm@55522
  1601
    by blast
wenzelm@55522
  1602
  obtain p :: nat where p: "1 + real n / e \<le> real p"
wenzelm@55522
  1603
    using real_arch_simple ..
wenzelm@53185
  1604
  have "1 + real n / e > 0"
nipkow@56541
  1605
    using e(1) n by (simp add: add_pos_pos)
wenzelm@53688
  1606
  then have "p > 0"
wenzelm@53688
  1607
    using p by auto
hoelzl@50526
  1608
hoelzl@56273
  1609
  obtain b :: "nat \<Rightarrow> 'a" where b: "bij_betw b {..< n} Basis"
hoelzl@50526
  1610
    by atomize_elim (auto simp: n_def intro!: finite_same_card_bij)
wenzelm@63040
  1611
  define b' where "b' = inv_into {..< n} b"
hoelzl@56273
  1612
  then have b': "bij_betw b' Basis {..< n}"
hoelzl@50526
  1613
    using bij_betw_inv_into[OF b] by auto
hoelzl@56273
  1614
  then have b'_Basis: "\<And>i. i \<in> Basis \<Longrightarrow> b' i \<in> {..< n}"
hoelzl@50526
  1615
    unfolding bij_betw_def by (auto simp: set_eq_iff)
hoelzl@50526
  1616
  have bb'[simp]:"\<And>i. i \<in> Basis \<Longrightarrow> b (b' i) = i"
wenzelm@53688
  1617
    unfolding b'_def
wenzelm@53688
  1618
    using b
wenzelm@53688
  1619
    by (auto simp: f_inv_into_f bij_betw_def)
hoelzl@56273
  1620
  have b'b[simp]:"\<And>i. i < n \<Longrightarrow> b' (b i) = i"
wenzelm@53688
  1621
    unfolding b'_def
wenzelm@53688
  1622
    using b
wenzelm@53688
  1623
    by (auto simp: inv_into_f_eq bij_betw_def)
wenzelm@53688
  1624
  have *: "\<And>x :: nat. x = 0 \<or> x = 1 \<longleftrightarrow> x \<le> 1"
wenzelm@53688
  1625
    by auto
hoelzl@56273
  1626
  have b'': "\<And>j. j < n \<Longrightarrow> b j \<in> Basis"
wenzelm@53185
  1627
    using b unfolding bij_betw_def by auto
hoelzl@56273
  1628
  have q1: "0 < p" "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow>
hoelzl@56273
  1629
    (\<forall>i<n. (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0 \<or>
hoelzl@56273
  1630
           (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
wenzelm@53688
  1631
    unfolding *
wenzelm@60420
  1632
    using \<open>p > 0\<close> \<open>n > 0\<close>
wenzelm@53688
  1633
    using label(1)[OF b'']
wenzelm@53688
  1634
    by auto
hoelzl@56273
  1635
  { fix x :: "nat \<Rightarrow> nat" and i assume "\<forall>i<n. x i \<le> p" "i < n" "x i = p \<or> x i = 0"
hoelzl@56273
  1636
    then have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> (unit_cube::'a set)"
hoelzl@56273
  1637
      using b'_Basis
hoelzl@56273
  1638
      by (auto simp add: mem_unit_cube inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) }
hoelzl@56273
  1639
  note cube = this
hoelzl@56273
  1640
  have q2: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow>
hoelzl@50526
  1641
      (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0)"
wenzelm@60420
  1642
    unfolding o_def using cube \<open>p > 0\<close> by (intro allI impI label(2)) (auto simp add: b'')
lp15@61609
  1643
  have q3: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = p \<longrightarrow>
hoelzl@50526
  1644
      (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 1)"
wenzelm@60420
  1645
    using cube \<open>p > 0\<close> unfolding o_def by (intro allI impI label(3)) (auto simp add: b'')
wenzelm@55522
  1646
  obtain q where q:
hoelzl@56273
  1647
      "\<forall>i<n. q i < p"
hoelzl@56273
  1648
      "\<forall>i<n.
hoelzl@56273
  1649
         \<exists>r s. (\<forall>j<n. q j \<le> r j \<and> r j \<le> q j + 1) \<and>
hoelzl@56273
  1650
               (\<forall>j<n. q j \<le> s j \<and> s j \<le> q j + 1) \<and>
wenzelm@55522
  1651
               (label (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i) \<circ> b) i \<noteq>
wenzelm@55522
  1652
               (label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) i"
hoelzl@56273
  1653
    by (rule kuhn_lemma[OF q1 q2 q3])
wenzelm@63040
  1654
  define z :: 'a where "z = (\<Sum>i\<in>Basis. (real (q (b' i)) / real p) *\<^sub>R i)"
wenzelm@61945
  1655
  have "\<exists>i\<in>Basis. d / real n \<le> \<bar>(f z - z)\<bullet>i\<bar>"
wenzelm@53185
  1656
  proof (rule ccontr)
hoelzl@50526
  1657
    have "\<forall>i\<in>Basis. q (b' i) \<in> {0..p}"
wenzelm@53688
  1658
      using q(1) b'
wenzelm@53688
  1659
      by (auto intro: less_imp_le simp: bij_betw_def)
huffman@56117
  1660
    then have "z \<in> unit_cube"
huffman@56117
  1661
      unfolding z_def mem_unit_cube
wenzelm@53688
  1662
      using b'_Basis
hoelzl@56273
  1663
      by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
wenzelm@53688
  1664
    then have d_fz_z: "d \<le> norm (f z - z)"
wenzelm@53688
  1665
      by (rule d)
wenzelm@53688
  1666
    assume "\<not> ?thesis"
wenzelm@53674
  1667
    then have as: "\<forall>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar> < d / real n"
wenzelm@60420
  1668
      using \<open>n > 0\<close>
hoelzl@56273
  1669
      by (auto simp add: not_le inner_diff)
hoelzl@50526
  1670
    have "norm (f z - z) \<le> (\<Sum>i\<in>Basis. \<bar>f z \<bullet> i - z \<bullet> i\<bar>)"
wenzelm@53688
  1671
      unfolding inner_diff_left[symmetric]
wenzelm@53688
  1672
      by (rule norm_le_l1)
wenzelm@53185
  1673
    also have "\<dots> < (\<Sum>(i::'a) \<in> Basis. d / real n)"
nipkow@64267
  1674
      apply (rule sum_strict_mono)
wenzelm@53688
  1675
      using as
wenzelm@53688
  1676
      apply auto
wenzelm@53185
  1677
      done
wenzelm@53185
  1678
    also have "\<dots> = d"
wenzelm@53688
  1679
      using DIM_positive[where 'a='a]
lp15@61609
  1680
      by (auto simp: n_def)
wenzelm@53688
  1681
    finally show False
wenzelm@53688
  1682
      using d_fz_z by auto
wenzelm@53185
  1683
  qed
wenzelm@55522
  1684
  then obtain i where i: "i \<in> Basis" "d / real n \<le> \<bar>(f z - z) \<bullet> i\<bar>" ..
hoelzl@56273
  1685
  have *: "b' i < n"
wenzelm@55522
  1686
    using i and b'[unfolded bij_betw_def]
wenzelm@53688
  1687
    by auto
wenzelm@55522
  1688
  obtain r s where rs:
hoelzl@56273
  1689
    "\<And>j. j < n \<Longrightarrow> q j \<le> r j \<and> r j \<le> q j + 1"
hoelzl@56273
  1690
    "\<And>j. j < n \<Longrightarrow> q j \<le> s j \<and> s j \<le> q j + 1"
wenzelm@55522
  1691
    "(label (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i) \<circ> b) (b' i) \<noteq>
wenzelm@55522
  1692
      (label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) (b' i)"
wenzelm@55522
  1693
    using q(2)[rule_format,OF *] by blast
hoelzl@56273
  1694
  have b'_im: "\<And>i. i \<in> Basis \<Longrightarrow>  b' i < n"
wenzelm@53185
  1695
    using b' unfolding bij_betw_def by auto
wenzelm@63040
  1696
  define r' ::'a where "r' = (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i)"
wenzelm@53185
  1697
  have "\<And>i. i \<in> Basis \<Longrightarrow> r (b' i) \<le> p"
wenzelm@53185
  1698
    apply (rule order_trans)
wenzelm@53185
  1699
    apply (rule rs(1)[OF b'_im,THEN conjunct2])
wenzelm@53252
  1700
    using q(1)[rule_format,OF b'_im]
wenzelm@53252
  1701
    apply (auto simp add: Suc_le_eq)
wenzelm@53185
  1702
    done
huffman@56117
  1703
  then have "r' \<in> unit_cube"
huffman@56117
  1704
    unfolding r'_def mem_unit_cube
wenzelm@53688
  1705
    using b'_Basis
hoelzl@56273
  1706
    by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
wenzelm@63040
  1707
  define s' :: 'a where "s' = (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i)"
wenzelm@53688
  1708
  have "\<And>i. i \<in> Basis \<Longrightarrow> s (b' i) \<le> p"
wenzelm@53185
  1709
    apply (rule order_trans)
wenzelm@53185
  1710
    apply (rule rs(2)[OF b'_im, THEN conjunct2])
wenzelm@53252
  1711
    using q(1)[rule_format,OF b'_im]
wenzelm@53252
  1712
    apply (auto simp add: Suc_le_eq)
wenzelm@53185
  1713
    done
huffman@56117
  1714
  then have "s' \<in> unit_cube"
huffman@56117
  1715
    unfolding s'_def mem_unit_cube
wenzelm@53688
  1716
    using b'_Basis
hoelzl@56273
  1717
    by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1)
huffman@56117
  1718
  have "z \<in> unit_cube"
huffman@56117
  1719
    unfolding z_def mem_unit_cube
wenzelm@60420
  1720
    using b'_Basis q(1)[rule_format,OF b'_im] \<open>p > 0\<close>
hoelzl@56273
  1721
    by (auto simp add: bij_betw_def zero_le_divide_iff divide_le_eq_1 less_imp_le)
wenzelm@53688
  1722
  have *: "\<And>x. 1 + real x = real (Suc x)"
wenzelm@53688
  1723
    by auto
wenzelm@53688
  1724
  {
wenzelm@53688
  1725
    have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
nipkow@64267
  1726
      apply (rule sum_mono)
wenzelm@53252
  1727
      using rs(1)[OF b'_im]
lp15@61609
  1728
      apply (auto simp add:* field_simps simp del: of_nat_Suc)
wenzelm@53185
  1729
      done
wenzelm@53688
  1730
    also have "\<dots> < e * real p"
wenzelm@60420
  1731
      using p \<open>e > 0\<close> \<open>p > 0\<close>
lp15@61609
  1732
      by (auto simp add: field_simps n_def)
wenzelm@53185
  1733
    finally have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) < e * real p" .
wenzelm@53185
  1734
  }
wenzelm@53185
  1735
  moreover
wenzelm@53688
  1736
  {
wenzelm@53688
  1737
    have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
nipkow@64267
  1738
      apply (rule sum_mono)
wenzelm@53252
  1739
      using rs(2)[OF b'_im]
lp15@61609
  1740
      apply (auto simp add:* field_simps simp del: of_nat_Suc)
wenzelm@53185
  1741
      done
wenzelm@53688
  1742
    also have "\<dots> < e * real p"
wenzelm@60420
  1743
      using p \<open>e > 0\<close> \<open>p > 0\<close>
lp15@61609
  1744
      by (auto simp add: field_simps n_def)
wenzelm@53185
  1745
    finally have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) < e * real p" .
wenzelm@53185
  1746
  }
wenzelm@53185
  1747
  ultimately
wenzelm@53688
  1748
  have "norm (r' - z) < e" and "norm (s' - z) < e"
wenzelm@53185
  1749
    unfolding r'_def s'_def z_def
wenzelm@60420
  1750
    using \<open>p > 0\<close>
wenzelm@53185
  1751
    apply (rule_tac[!] le_less_trans[OF norm_le_l1])
nipkow@64267
  1752
    apply (auto simp add: field_simps sum_divide_distrib[symmetric] inner_diff_left)
wenzelm@53185
  1753
    done
wenzelm@53674
  1754
  then have "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
wenzelm@53688
  1755
    using rs(3) i
wenzelm@53688
  1756
    unfolding r'_def[symmetric] s'_def[symmetric] o_def bb'
wenzelm@60420
  1757
    by (intro e(2)[OF \<open>r'\<in>unit_cube\<close> \<open>s'\<in>unit_cube\<close> \<open>z\<in>unit_cube\<close>]) auto
wenzelm@53688
  1758
  then show False
wenzelm@53688
  1759
    using i by auto
hoelzl@50526
  1760
qed
hoelzl@33741
  1761
wenzelm@53185
  1762
wenzelm@60420
  1763
subsection \<open>Retractions\<close>
hoelzl@33741
  1764
wenzelm@53688
  1765
definition "retraction s t r \<longleftrightarrow> t \<subseteq> s \<and> continuous_on s r \<and> r ` s \<subseteq> t \<and> (\<forall>x\<in>t. r x = x)"
hoelzl@33741
  1766
lp15@62843
  1767
definition retract_of (infixl "retract'_of" 50)
wenzelm@53185
  1768
  where "(t retract_of s) \<longleftrightarrow> (\<exists>r. retraction s t r)"
hoelzl@33741
  1769
wenzelm@53674
  1770
lemma retraction_idempotent: "retraction s t r \<Longrightarrow> x \<in> s \<Longrightarrow>  r (r x) = r x"
hoelzl@33741
  1771
  unfolding retraction_def by auto
hoelzl@33741
  1772
wenzelm@60420
  1773
subsection \<open>Preservation of fixpoints under (more general notion of) retraction\<close>
hoelzl@33741
  1774
wenzelm@53185
  1775
lemma invertible_fixpoint_property:
wenzelm@53674
  1776
  fixes s :: "'a::euclidean_space set"
wenzelm@53674
  1777
    and t :: "'b::euclidean_space set"
wenzelm@53674
  1778
  assumes "continuous_on t i"
wenzelm@53674
  1779
    and "i ` t \<subseteq> s"
wenzelm@53688
  1780
    and "continuous_on s r"
wenzelm@53688
  1781
    and "r ` s \<subseteq> t"
wenzelm@53674
  1782
    and "\<forall>y\<in>t. r (i y) = y"
wenzelm@53674
  1783
    and "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)"
wenzelm@53674
  1784
    and "continuous_on t g"
wenzelm@53674
  1785
    and "g ` t \<subseteq> t"
wenzelm@53674
  1786
  obtains y where "y \<in> t" and "g y = y"
wenzelm@53185
  1787
proof -
wenzelm@53185
  1788
  have "\<exists>x\<in>s. (i \<circ> g \<circ> r) x = x"
wenzelm@53688
  1789
    apply (rule assms(6)[rule_format])
wenzelm@53688
  1790
    apply rule
wenzelm@53185
  1791
    apply (rule continuous_on_compose assms)+
wenzelm@53688
  1792
    apply ((rule continuous_on_subset)?, rule assms)+
wenzelm@53688
  1793
    using assms(2,4,8)
wenzelm@53185
  1794
    apply auto
wenzelm@53185
  1795
    apply blast
wenzelm@53185
  1796
    done
wenzelm@55522
  1797
  then obtain x where x: "x \<in> s" "(i \<circ> g \<circ> r) x = x" ..
wenzelm@53674
  1798
  then have *: "g (r x) \<in> t"
wenzelm@53674
  1799
    using assms(4,8) by auto
wenzelm@53674
  1800
  have "r ((i \<circ> g \<circ> r) x) = r x"
wenzelm@53674
  1801
    using x by auto
wenzelm@53674
  1802
  then show ?thesis
wenzelm@53185
  1803
    apply (rule_tac that[of "r x"])
wenzelm@53674
  1804
    using x
wenzelm@53674
  1805
    unfolding o_def
wenzelm@53674
  1806
    unfolding assms(5)[rule_format,OF *]
wenzelm@53674
  1807
    using assms(4)
wenzelm@53185
  1808
    apply auto
wenzelm@53185
  1809
    done
wenzelm@53185
  1810
qed
hoelzl@33741
  1811
hoelzl@33741
  1812
lemma homeomorphic_fixpoint_property:
wenzelm@53674
  1813
  fixes s :: "'a::euclidean_space set"
wenzelm@53674
  1814
    and t :: "'b::euclidean_space set"
wenzelm@53185
  1815
  assumes "s homeomorphic t"
hoelzl@33741
  1816
  shows "(\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)) \<longleftrightarrow>
wenzelm@53248
  1817
    (\<forall>g. continuous_on t g \<and> g ` t \<subseteq> t \<longrightarrow> (\<exists>y\<in>t. g y = y))"
wenzelm@53185
  1818
proof -
wenzelm@55522
  1819
  obtain r i where
wenzelm@55522
  1820
      "\<forall>x\<in>s. i (r x) = x"
wenzelm@55522
  1821
      "r ` s = t"
wenzelm@55522
  1822
      "continuous_on s r"
wenzelm@55522
  1823
      "\<forall>y\<in>t. r (i y) = y"
wenzelm@55522
  1824
      "i ` t = s"
wenzelm@55522
  1825
      "continuous_on t i"
wenzelm@55522
  1826
    using assms
wenzelm@55522
  1827
    unfolding homeomorphic_def homeomorphism_def
wenzelm@55522
  1828
    by blast
wenzelm@53674
  1829
  then show ?thesis
wenzelm@53185
  1830
    apply -
wenzelm@53185
  1831
    apply rule
wenzelm@53185
  1832
    apply (rule_tac[!] allI impI)+
wenzelm@53185
  1833
    apply (rule_tac g=g in invertible_fixpoint_property[of t i s r])
wenzelm@53185
  1834
    prefer 10
wenzelm@53185
  1835
    apply (rule_tac g=f in invertible_fixpoint_property[of s r t i])
wenzelm@53185
  1836
    apply auto
wenzelm@53185
  1837
    done
wenzelm@53185
  1838
qed
hoelzl@33741
  1839
wenzelm@53185
  1840
lemma retract_fixpoint_property:
wenzelm@53688
  1841
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
wenzelm@53674
  1842
    and s :: "'a set"
wenzelm@53185
  1843
  assumes "t retract_of s"
wenzelm@53674
  1844
    and "\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)"
wenzelm@53674
  1845
    and "continuous_on t g"
wenzelm@53674
  1846
    and "g ` t \<subseteq> t"
wenzelm@53674
  1847
  obtains y where "y \<in> t" and "g y = y"
wenzelm@53185
  1848
proof -
wenzelm@55522
  1849
  obtain h where "retraction s t h"
wenzelm@55522
  1850
    using assms(1) unfolding retract_of_def ..
wenzelm@53674
  1851
  then show ?thesis
wenzelm@53185
  1852
    unfolding retraction_def
wenzelm@53185
  1853
    apply -
wenzelm@53185
  1854
    apply (rule invertible_fixpoint_property[OF continuous_on_id _ _ _ _ assms(2), of t h g])
wenzelm@53185
  1855
    prefer 7
wenzelm@53248
  1856
    apply (rule_tac y = y in that)
wenzelm@53248
  1857
    using assms
wenzelm@53248
  1858
    apply auto
wenzelm@53185
  1859
    done
wenzelm@53185
  1860
qed
wenzelm@53185
  1861
hoelzl@33741
  1862
wenzelm@60420
  1863
subsection \<open>The Brouwer theorem for any set with nonempty interior\<close>
hoelzl@33741
  1864
huffman@56117
  1865
lemma convex_unit_cube: "convex unit_cube"
huffman@56117
  1866
  apply (rule is_interval_convex)
huffman@56117
  1867
  apply (clarsimp simp add: is_interval_def mem_unit_cube)
huffman@56117
  1868
  apply (drule (1) bspec)+
huffman@56117
  1869
  apply auto
huffman@56117
  1870
  done
huffman@56117
  1871
hoelzl@50526
  1872
lemma brouwer_weak:
huffman@56117
  1873
  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
wenzelm@53674
  1874
  assumes "compact s"
wenzelm@53674
  1875
    and "convex s"
wenzelm@53674
  1876
    and "interior s \<noteq> {}"
wenzelm@53674
  1877
    and "continuous_on s f"
wenzelm@53674
  1878
    and "f ` s \<subseteq> s"
wenzelm@53674
  1879
  obtains x where "x \<in> s" and "f x = x"
wenzelm@53185
  1880
proof -
huffman@56117
  1881
  let ?U = "unit_cube :: 'a set"
huffman@56117
  1882
  have "\<Sum>Basis /\<^sub>R 2 \<in> interior ?U"
huffman@56117
  1883
  proof (rule interiorI)
huffman@56117
  1884
    let ?I = "(\<Inter>i\<in>Basis. {x::'a. 0 < x \<bullet> i} \<inter> {x. x \<bullet> i < 1})"
huffman@56117
  1885
    show "open ?I"
hoelzl@63332
  1886
      by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less simp: continuous_on_inner continuous_on_const continuous_on_id)
huffman@56117
  1887
    show "\<Sum>Basis /\<^sub>R 2 \<in> ?I"
huffman@56117
  1888
      by simp
huffman@56117
  1889
    show "?I \<subseteq> unit_cube"
huffman@56117
  1890
      unfolding unit_cube_def by force
huffman@56117
  1891
  qed
huffman@56117
  1892
  then have *: "interior ?U \<noteq> {}" by fast
huffman@56117
  1893
  have *: "?U homeomorphic s"
huffman@56117
  1894
    using homeomorphic_convex_compact[OF convex_unit_cube compact_unit_cube * assms(2,1,3)] .
huffman@56117
  1895
  have "\<forall>f. continuous_on ?U f \<and> f ` ?U \<subseteq> ?U \<longrightarrow>
huffman@56117
  1896
    (\<exists>x\<in>?U. f x = x)"
hoelzl@37489
  1897
    using brouwer_cube by auto
wenzelm@53674
  1898
  then show ?thesis
wenzelm@53185
  1899
    unfolding homeomorphic_fixpoint_property[OF *]
wenzelm@53252
  1900
    using assms
lp15@59765
  1901
    by (auto simp: intro: that)
wenzelm@53185
  1902
qed
wenzelm@53185
  1903
hoelzl@33741
  1904
wenzelm@60420
  1905
text \<open>And in particular for a closed ball.\<close>
hoelzl@33741
  1906
wenzelm@53185
  1907
lemma brouwer_ball:
huffman@56117
  1908
  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
wenzelm@53674
  1909
  assumes "e > 0"
wenzelm@53674
  1910
    and "continuous_on (cball a e) f"
wenzelm@53688
  1911
    and "f ` cball a e \<subseteq> cball a e"
wenzelm@53674
  1912
  obtains x where "x \<in> cball a e" and "f x = x"
wenzelm@53185
  1913
  using brouwer_weak[OF compact_cball convex_cball, of a e f]
wenzelm@53185
  1914
  unfolding interior_cball ball_eq_empty
hoelzl@33741
  1915
  using assms by auto
hoelzl@33741
  1916
wenzelm@60420
  1917
text \<open>Still more general form; could derive this directly without using the
wenzelm@61808
  1918
  rather involved \<open>HOMEOMORPHIC_CONVEX_COMPACT\<close> theorem, just using
wenzelm@60420
  1919
  a scaling and translation to put the set inside the unit cube.\<close>
hoelzl@33741
  1920
wenzelm@53248
  1921
lemma brouwer:
huffman@56117
  1922
  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
wenzelm@53674
  1923
  assumes "compact s"
wenzelm@53674
  1924
    and "convex s"
wenzelm@53674
  1925
    and "s \<noteq> {}"
wenzelm@53674
  1926
    and "continuous_on s f"
wenzelm@53674
  1927
    and "f ` s \<subseteq> s"
wenzelm@53674
  1928
  obtains x where "x \<in> s" and "f x = x"
wenzelm@53185
  1929
proof -
wenzelm@53185
  1930
  have "\<exists>e>0. s \<subseteq> cball 0 e"
wenzelm@53688
  1931
    using compact_imp_bounded[OF assms(1)]
wenzelm@53688
  1932
    unfolding bounded_pos
wenzelm@53674
  1933
    apply (erule_tac exE)
wenzelm@53674
  1934
    apply (rule_tac x=b in exI)
wenzelm@53185
  1935
    apply (auto simp add: dist_norm)
wenzelm@53185
  1936
    done
wenzelm@55522
  1937
  then obtain e where e: "e > 0" "s \<subseteq> cball 0 e"
wenzelm@55522
  1938
    by blast
hoelzl@33741
  1939
  have "\<exists>x\<in> cball 0 e. (f \<circ> closest_point s) x = x"
wenzelm@53185
  1940
    apply (rule_tac brouwer_ball[OF e(1), of 0 "f \<circ> closest_point s"])
wenzelm@53185
  1941
    apply (rule continuous_on_compose )
wenzelm@53185
  1942
    apply (rule continuous_on_closest_point[OF assms(2) compact_imp_closed[OF assms(1)] assms(3)])
wenzelm@53185
  1943
    apply (rule continuous_on_subset[OF assms(4)])
wenzelm@53185
  1944
    apply (insert closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)])
wenzelm@53185
  1945
    using assms(5)[unfolded subset_eq]
wenzelm@53185
  1946
    using e(2)[unfolded subset_eq mem_cball]
wenzelm@53185
  1947
    apply (auto simp add: dist_norm)
wenzelm@53185
  1948
    done
wenzelm@55522
  1949
  then obtain x where x: "x \<in> cball 0 e" "(f \<circ> closest_point s) x = x" ..
wenzelm@53185
  1950
  have *: "closest_point s x = x"
wenzelm@53185
  1951
    apply (rule closest_point_self)
wenzelm@53185
  1952
    apply (rule assms(5)[unfolded subset_eq,THEN bspec[where x="x"], unfolded image_iff])
wenzelm@53185
  1953
    apply (rule_tac x="closest_point s x" in bexI)
wenzelm@53185
  1954
    using x
wenzelm@53185
  1955
    unfolding o_def
wenzelm@53185
  1956
    using closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3), of x]
wenzelm@53185
  1957
    apply auto
wenzelm@53185
  1958
    done
wenzelm@53185
  1959
  show thesis
wenzelm@53185
  1960
    apply (rule_tac x="closest_point s x" in that)
wenzelm@53185
  1961
    unfolding x(2)[unfolded o_def]
wenzelm@53185
  1962
    apply (rule closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)])
wenzelm@53674
  1963
    using *
wenzelm@53674
  1964
    apply auto
wenzelm@53674
  1965
    done
wenzelm@53185
  1966
qed
hoelzl@33741
  1967
wenzelm@60420
  1968
text \<open>So we get the no-retraction theorem.\<close>
hoelzl@33741
  1969
lp15@64006
  1970
theorem no_retraction_cball:
huffman@56117
  1971
  fixes a :: "'a::euclidean_space"
wenzelm@53674
  1972
  assumes "e > 0"
wenzelm@53674
  1973
  shows "\<not> (frontier (cball a e) retract_of (cball a e))"
wenzelm@53185
  1974
proof
wenzelm@60580
  1975
  assume *: "frontier (cball a e) retract_of (cball a e)"
wenzelm@60580
  1976
  have **: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
wenzelm@53185
  1977
    using scaleR_left_distrib[of 1 1 a] by auto
wenzelm@55522
  1978
  obtain x where x:
wenzelm@55522
  1979
      "x \<in> {x. norm (a - x) = e}"
wenzelm@55522
  1980
      "2 *\<^sub>R a - x = x"
wenzelm@60580
  1981
    apply (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"])
lp15@59765
  1982
    apply (blast intro: brouwer_ball[OF assms])
lp15@59765
  1983
    apply (intro continuous_intros)
lp15@62381
  1984
    unfolding frontier_cball subset_eq Ball_def image_iff dist_norm sphere_def
wenzelm@60580
  1985
    apply (auto simp add: ** norm_minus_commute)
wenzelm@53185
  1986
    done
wenzelm@53674
  1987
  then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
wenzelm@53248
  1988
    by (auto simp add: algebra_simps)
wenzelm@53674
  1989
  then have "a = x"
wenzelm@53688
  1990
    unfolding scaleR_left_distrib[symmetric]
wenzelm@53688
  1991
    by auto
wenzelm@53674
  1992
  then show False
wenzelm@53674
  1993
    using x assms by auto
wenzelm@53185
  1994
qed
wenzelm@53185
  1995
lp15@64006
  1996
corollary contractible_sphere:
lp15@64006
  1997
  fixes a :: "'a::euclidean_space"
lp15@64006
  1998
  shows "contractible(sphere a r) \<longleftrightarrow> r \<le> 0"
lp15@64006
  1999
proof (cases "0 < r")
lp15@64006
  2000
  case True
lp15@64006
  2001
  then show ?thesis
lp15@64006
  2002
    unfolding contractible_def nullhomotopic_from_sphere_extension
lp15@64006
  2003
    using no_retraction_cball [OF True, of a]
lp15@64006
  2004
    by (auto simp: retract_of_def retraction_def)
lp15@64006
  2005
next
lp15@64006
  2006
  case False
lp15@64006
  2007
  then show ?thesis
lp15@64006
  2008
    unfolding contractible_def nullhomotopic_from_sphere_extension
lp15@64006
  2009
    apply (simp add: not_less)
lp15@64006
  2010
    apply (rule_tac x=id in exI)
lp15@64006
  2011
    apply (auto simp: continuous_on_def)
lp15@64006
  2012
    apply (meson dist_not_less_zero le_less less_le_trans)
lp15@64006
  2013
    done
lp15@64006
  2014
qed
lp15@64006
  2015
lp15@64789
  2016
lemma connected_sphere_eq:
lp15@64789
  2017
  fixes a :: "'a :: euclidean_space"
lp15@64789
  2018
  shows "connected(sphere a r) \<longleftrightarrow> 2 \<le> DIM('a) \<or> r \<le> 0"
lp15@64789
  2019
    (is "?lhs = ?rhs")
lp15@64789
  2020
proof (cases r "0::real" rule: linorder_cases)
lp15@64789
  2021
  case less
lp15@64789
  2022
  then show ?thesis by auto
lp15@64789
  2023
next
lp15@64789
  2024
  case equal
lp15@64789
  2025
  then show ?thesis by auto
lp15@64789
  2026
next
lp15@64789
  2027
  case greater
lp15@64789
  2028
  show ?thesis
lp15@64789
  2029
  proof
lp15@64789
  2030
    assume L: ?lhs
lp15@64789
  2031
    have "False" if 1: "DIM('a) = 1"
lp15@64789
  2032
    proof -
lp15@64789
  2033
      obtain x y where xy: "sphere a r = {x,y}" "x \<noteq> y"
lp15@64789
  2034
        using sphere_1D_doubleton [OF 1 greater]
lp15@64789
  2035
        by (metis dist_self greater insertI1 less_add_same_cancel1 mem_sphere mult_2 not_le zero_le_dist)
lp15@64789
  2036
      then have "finite (sphere a r)"
lp15@64789
  2037
        by auto
lp15@64789
  2038
      with L \<open>r > 0\<close> show "False"
lp15@64789
  2039
        apply (auto simp: connected_finite_iff_sing)
lp15@64789
  2040
        using xy by auto
lp15@64789
  2041
    qed
lp15@64789
  2042
    with greater show ?rhs
lp15@64789
  2043
      by (metis DIM_ge_Suc0 One_nat_def Suc_1 le_antisym not_less_eq_eq)
lp15@64789
  2044
  next
lp15@64789
  2045
    assume ?rhs
lp15@64789
  2046
    then show ?lhs
lp15@64789
  2047
      using connected_sphere greater by auto
lp15@64789
  2048
  qed
lp15@64789
  2049
qed
lp15@64789
  2050
lp15@64789
  2051
lemma path_connected_sphere_eq:
lp15@64789
  2052
  fixes a :: "'a :: euclidean_space"
lp15@64789
  2053
  shows "path_connected(sphere a r) \<longleftrightarrow> 2 \<le> DIM('a) \<or> r \<le> 0"
lp15@64789
  2054
         (is "?lhs = ?rhs")
lp15@64789
  2055
proof
lp15@64789
  2056
  assume ?lhs
lp15@64789
  2057
  then show ?rhs
lp15@64789
  2058
    using connected_sphere_eq path_connected_imp_connected by blast
lp15@64789
  2059
next
lp15@64789
  2060
  assume R: ?rhs
lp15@64789
  2061
  then show ?lhs
lp15@64789
  2062
    by (auto simp: contractible_imp_path_connected contractible_sphere path_connected_sphere)
lp15@64789
  2063
qed
lp15@64789
  2064
lp15@64122
  2065
proposition frontier_subset_retraction:
lp15@64122
  2066
  fixes S :: "'a::euclidean_space set"
lp15@64122
  2067
  assumes "bounded S" and fros: "frontier S \<subseteq> T"
lp15@64122
  2068
      and contf: "continuous_on (closure S) f"
lp15@64122
  2069
      and fim: "f ` S \<subseteq> T"
lp15@64122
  2070
      and fid: "\<And>x. x \<in> T \<Longrightarrow> f x = x"
lp15@64122
  2071
    shows "S \<subseteq> T"
lp15@64122
  2072
proof (rule ccontr)
lp15@64122
  2073
  assume "\<not> S \<subseteq> T"
lp15@64122
  2074
  then obtain a where "a \<in> S" "a \<notin> T" by blast
lp15@64122
  2075
  define g where "g \<equiv> \<lambda>z. if z \<in> closure S then f z else z"
lp15@64122
  2076
  have "continuous_on (closure S \<union> closure(-S)) g"
lp15@64122
  2077
    unfolding g_def
lp15@64122
  2078
    apply (rule continuous_on_cases)
lp15@64122
  2079
    using fros fid frontier_closures
lp15@64122
  2080
        apply (auto simp: contf continuous_on_id)
lp15@64122
  2081
    done
lp15@64122
  2082
  moreover have "closure S \<union> closure(- S) = UNIV"
lp15@64122
  2083
    using closure_Un by fastforce
lp15@64122
  2084
  ultimately have contg: "continuous_on UNIV g" by metis
lp15@64122
  2085
  obtain B where "0 < B" and B: "closure S \<subseteq> ball a B"
lp15@64122
  2086
    using \<open>bounded S\<close> bounded_subset_ballD by blast
lp15@64122
  2087
  have notga: "g x \<noteq> a" for x
lp15@64122
  2088
    unfolding g_def using fros fim \<open>a \<notin> T\<close>
lp15@64122
  2089
    apply (auto simp: frontier_def)
lp15@64122
  2090
    using fid interior_subset apply fastforce
lp15@64122
  2091
    by (simp add: \<open>a \<in> S\<close> closure_def)
lp15@64122
  2092
  define h where "h \<equiv> (\<lambda>y. a + (B / norm(y - a)) *\<^sub>R (y - a)) \<circ> g"
lp15@64122
  2093
  have "\<not> (frontier (cball a B) retract_of (cball a B))"
lp15@64122
  2094
    by (metis no_retraction_cball \<open>0 < B\<close>)
lp15@64122
  2095
  then have "\<And>k. \<not> retraction (cball a B) (frontier (cball a B)) k"
lp15@64122
  2096
    by (simp add: retract_of_def)
lp15@64122
  2097
  moreover have "retraction (cball a B) (frontier (cball a B)) h"
lp15@64122
  2098
    unfolding retraction_def
lp15@64122
  2099
  proof (intro conjI ballI)
lp15@64122
  2100
    show "frontier (cball a B) \<subseteq> cball a B"
lp15@64122
  2101
      by (force simp:)
lp15@64122
  2102
    show "continuous_on (cball a B) h"
lp15@64122
  2103
      unfolding h_def
lp15@64122
  2104
      apply (intro continuous_intros)
lp15@64122
  2105
      using contg continuous_on_subset notga apply auto
lp15@64122
  2106
      done
lp15@64122
  2107
    show "h ` cball a B \<subseteq> frontier (cball a B)"
lp15@64122
  2108
      using \<open>0 < B\<close> by (auto simp: h_def notga dist_norm)
lp15@64122
  2109
    show "\<And>x. x \<in> frontier (cball a B) \<Longrightarrow> h x = x"
lp15@64122
  2110
      apply (auto simp: h_def algebra_simps)
lp15@64122
  2111
      apply (simp add: vector_add_divide_simps  notga)
lp15@64122
  2112
      by (metis (no_types, hide_lams) B add.commute dist_commute  dist_norm g_def mem_ball not_less_iff_gr_or_eq  subset_eq)
lp15@64122
  2113
  qed
lp15@64122
  2114
  ultimately show False by simp
lp15@64122
  2115
qed
lp15@64122
  2116
lp15@64789
  2117
subsection\<open>More Properties of Retractions\<close>
lp15@62948
  2118
lp15@62948
  2119
lemma retraction:
lp15@62948
  2120
   "retraction s t r \<longleftrightarrow>
lp15@62948
  2121
    t \<subseteq> s \<and> continuous_on s r \<and> r ` s = t \<and> (\<forall>x \<in> t. r x = x)"
lp15@62948
  2122
by (force simp: retraction_def)
lp15@62948
  2123
lp15@62948
  2124
lemma retract_of_imp_extensible:
lp15@62948
  2125
  assumes "s retract_of t" and "continuous_on s f" and "f ` s \<subseteq> u"
lp15@62948
  2126
  obtains g where "continuous_on t g" "g ` t \<subseteq> u" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
lp15@62948
  2127
using assms
lp15@62948
  2128
apply (clarsimp simp add: retract_of_def retraction)
lp15@62948
  2129
apply (rule_tac g = "f o r" in that)
lp15@62948
  2130
apply (auto simp: continuous_on_compose2)
lp15@62948
  2131
done
lp15@62948
  2132
lp15@62948
  2133
lemma idempotent_imp_retraction:
lp15@62948
  2134
  assumes "continuous_on s f" and "f ` s \<subseteq> s" and "\<And>x. x \<in> s \<Longrightarrow> f(f x) = f x"
lp15@62948
  2135
    shows "retraction s (f ` s) f"
lp15@62948
  2136
by (simp add: assms retraction)
lp15@62948
  2137
lp15@62948
  2138
lemma retraction_subset:
lp15@62948
  2139
  assumes "retraction s t r" and "t \<subseteq> s'" and "s' \<subseteq> s"
lp15@62948
  2140
    shows "retraction s' t r"
lp15@62948
  2141
apply (simp add: retraction_def)
lp15@62948
  2142
by (metis assms continuous_on_subset image_mono retraction)
lp15@62948
  2143
lp15@62948
  2144
lemma retract_of_subset:
lp15@62948
  2145
  assumes "t retract_of s" and "t \<subseteq> s'" and "s' \<subseteq> s"
lp15@62948
  2146
    shows "t retract_of s'"
lp15@62948
  2147
by (meson assms retract_of_def retraction_subset)
lp15@62948
  2148
lp15@62948
  2149
lemma retraction_refl [simp]: "retraction s s (\<lambda>x. x)"
lp15@62948
  2150
by (simp add: continuous_on_id retraction)
lp15@62948
  2151
lp15@62948
  2152
lemma retract_of_refl [iff]: "s retract_of s"
lp15@62948
  2153
  using continuous_on_id retract_of_def retraction_def by fastforce
lp15@62948
  2154
lp15@62948
  2155
lemma retract_of_imp_subset:
lp15@62948
  2156
   "s retract_of t \<Longrightarrow> s \<subseteq> t"
lp15@62948
  2157
by (simp add: retract_of_def retraction_def)
lp15@62948
  2158
lp15@62948
  2159
lemma retract_of_empty [simp]:
lp15@62948
  2160
     "({} retract_of s) \<longleftrightarrow> s = {}"  "(s retract_of {}) \<longleftrightarrow> s = {}"
lp15@62948
  2161
by (auto simp: retract_of_def retraction_def)
lp15@62948
  2162
lp15@62948
  2163
lemma retract_of_singleton [iff]: "({x} retract_of s) \<longleftrightarrow> x \<in> s"
lp15@62948
  2164
  using continuous_on_const
lp15@62948
  2165
  by (auto simp: retract_of_def retraction_def)
lp15@62948
  2166
lp15@62948
  2167
lemma retraction_comp:
lp15@62948
  2168
   "\<lbrakk>retraction s t f; retraction t u g\<rbrakk>
lp15@62948
  2169
        \<Longrightarrow> retraction s u (g o f)"
lp15@62948
  2170
apply (auto simp: retraction_def intro: continuous_on_compose2)
lp15@62948
  2171
by blast
lp15@62948
  2172
lp15@63492
  2173
lemma retract_of_trans [trans]:
lp15@62948
  2174
  assumes "s retract_of t" and "t retract_of u"
lp15@62948
  2175
    shows "s retract_of u"
lp15@62948
  2176
using assms by (auto simp: retract_of_def intro: retraction_comp)
lp15@62948
  2177
lp15@62948
  2178
lemma closedin_retract:
lp15@62948
  2179
  fixes s :: "'a :: real_normed_vector set"
lp15@62948
  2180
  assumes "s retract_of t"
lp15@62948
  2181
    shows "closedin (subtopology euclidean t) s"
lp15@62948
  2182
proof -
lp15@62948
  2183
  obtain r where "s \<subseteq> t" "continuous_on t r" "r ` t \<subseteq> s" "\<And>x. x \<in> s \<Longrightarrow> r x = x"
lp15@62948
  2184
    using assms by (auto simp: retract_of_def retraction_def)
lp15@62948
  2185
  then have s: "s = {x \<in> t. (norm(r x - x)) = 0}" by auto
lp15@62948
  2186
  show ?thesis
lp15@62948
  2187
    apply (subst s)
lp15@62948
  2188
    apply (rule continuous_closedin_preimage_constant)
lp15@62948
  2189
    by (simp add: \<open>continuous_on t r\<close> continuous_on_diff continuous_on_id continuous_on_norm)
lp15@62948
  2190
qed
lp15@62948
  2191
lp15@63301
  2192
lemma closedin_self [simp]:
lp15@63301
  2193
    fixes S :: "'a :: real_normed_vector set"
lp15@63301
  2194
    shows "closedin (subtopology euclidean S) S"
lp15@63301
  2195
  by (simp add: closedin_retract)
lp15@63301
  2196
lp15@62948
  2197
lemma retract_of_contractible:
lp15@62948
  2198
  assumes "contractible t" "s retract_of t"
lp15@62948
  2199
    shows "contractible s"
lp15@62948
  2200
using assms
lp15@62948
  2201
apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with)
lp15@62948
  2202
apply (rule_tac x="r a" in exI)
lp15@62948
  2203
apply (rule_tac x="r o h" in exI)
lp15@62948
  2204
apply (intro conjI continuous_intros continuous_on_compose)
lp15@62948
  2205
apply (erule continuous_on_subset | force)+
lp15@62948
  2206
done
lp15@62948
  2207
lp15@62948
  2208
lemma retract_of_compact:
lp15@62948
  2209
     "\<lbrakk>compact t; s retract_of t\<rbrakk> \<Longrightarrow> compact s"
lp15@62948
  2210
  by (metis compact_continuous_image retract_of_def retraction)
lp15@62948
  2211
lp15@62948
  2212
lemma retract_of_closed:
lp15@62948
  2213
    fixes s :: "'a :: real_normed_vector set"
lp15@62948
  2214
    shows "\<lbrakk>closed t; s retract_of t\<rbrakk> \<Longrightarrow> closed s"
lp15@62948
  2215
  by (metis closedin_retract closedin_closed_eq)
lp15@62948
  2216
lp15@62948
  2217
lemma retract_of_connected:
lp15@62948
  2218
    "\<lbrakk>connected t; s retract_of t\<rbrakk> \<Longrightarrow> connected s"
lp15@62948
  2219
  by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
lp15@62948
  2220
lp15@62948
  2221
lemma retract_of_path_connected:
lp15@62948
  2222
    "\<lbrakk>path_connected t; s retract_of t\<rbrakk> \<Longrightarrow> path_connected s"
lp15@62948
  2223
  by (metis path_connected_continuous_image retract_of_def retraction)
lp15@62948
  2224
lp15@62948
  2225
lemma retract_of_simply_connected:
lp15@62948
  2226
    "\<lbrakk>simply_connected t; s retract_of t\<rbrakk> \<Longrightarrow> simply_connected s"
lp15@62948
  2227
apply (simp add: retract_of_def retraction_def, clarify)
lp15@62948
  2228
apply (rule simply_connected_retraction_gen)
lp15@62948
  2229
apply (force simp: continuous_on_id elim!: continuous_on_subset)+
lp15@62948
  2230
done
lp15@62948
  2231
lp15@62948
  2232
lemma retract_of_homotopically_trivial:
lp15@62948
  2233
  assumes ts: "t retract_of s"
lp15@62948
  2234
      and hom: "\<And>f g. \<lbrakk>continuous_on u f; f ` u \<subseteq> s;
lp15@62948
  2235
                       continuous_on u g; g ` u \<subseteq> s\<rbrakk>
lp15@62948
  2236
                       \<Longrightarrow> homotopic_with (\<lambda>x. True) u s f g"
lp15@62948
  2237
      and "continuous_on u f" "f ` u \<subseteq> t"
lp15@62948
  2238
      and "continuous_on u g" "g ` u \<subseteq> t"
lp15@62948
  2239
    shows "homotopic_with (\<lambda>x. True) u t f g"
lp15@62948
  2240
proof -
lp15@62948
  2241
  obtain r where "r ` s \<subseteq> s" "continuous_on s r" "\<forall>x\<in>s. r (r x) = r x" "t = r ` s"
lp15@62948
  2242
    using ts by (auto simp: retract_of_def retraction)
lp15@62948
  2243
  then obtain k where "Retracts s r t k"
lp15@62948
  2244
    unfolding Retracts_def
lp15@62948
  2245
    by (metis continuous_on_subset dual_order.trans image_iff image_mono)
lp15@62948
  2246
  then show ?thesis
lp15@62948
  2247
    apply (rule Retracts.homotopically_trivial_retraction_gen)
lp15@62948
  2248
    using assms
lp15@62948
  2249
    apply (force simp: hom)+
lp15@62948
  2250
    done
lp15@62948
  2251
qed
lp15@62948
  2252
lp15@62948
  2253
lemma retract_of_homotopically_trivial_null:
lp15@62948
  2254
  assumes ts: "t retract_of s"
lp15@62948
  2255
      and hom: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s\<rbrakk>
lp15@62948
  2256
                     \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) u s f (\<lambda>x. c)"
lp15@62948
  2257
      and "continuous_on u f" "f ` u \<subseteq> t"
lp15@62948
  2258
  obtains c where "homotopic_with (\<lambda>x. True) u t f (\<lambda>x. c)"
lp15@62948
  2259
proof -
lp15@62948
  2260
  obtain r where "r ` s \<subseteq> s" "continuous_on s r" "\<forall>x\<in>s. r (r x) = r x" "t = r ` s"
lp15@62948
  2261
    using ts by (auto simp: retract_of_def retraction)
lp15@62948
  2262
  then obtain k where "Retracts s r t k"
lp15@62948
  2263
    unfolding Retracts_def
lp15@62948
  2264
    by (metis continuous_on_subset dual_order.trans image_iff image_mono)
lp15@62948
  2265
  then show ?thesis
lp15@62948
  2266
    apply (rule Retracts.homotopically_trivial_retraction_null_gen)
lp15@62948
  2267
    apply (rule TrueI refl assms that | assumption)+
lp15@62948
  2268
    done
lp15@62948
  2269
qed
lp15@62948
  2270
lp15@62948
  2271
lemma retraction_imp_quotient_map:
lp15@62948
  2272
   "retraction s t r
lp15@62948
  2273
    \<Longrightarrow> u \<subseteq> t
lp15@66884
  2274
            \<Longrightarrow> (openin (subtopology euclidean s) (s \<inter> r -` u) \<longleftrightarrow>