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