src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
author immler
Tue Mar 18 10:12:57 2014 +0100 (2014-03-18)
changeset 56188 0268784f60da
parent 56154 f0a927235162
child 56226 29fd6bd9228e
permissions -rw-r--r--
use cbox to relax class constraints
wenzelm@53674
     1
(*  Author:     John Harrison
wenzelm@53674
     2
    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light)
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
hoelzl@33741
    19
header {* Results connected with topological dimension. *}
hoelzl@33741
    20
hoelzl@33741
    21
theory Brouwer_Fixpoint
wenzelm@53674
    22
imports Convex_Euclidean_Space
hoelzl@33741
    23
begin
hoelzl@33741
    24
hoelzl@50526
    25
(** move this **)
wenzelm@53185
    26
lemma divide_nonneg_nonneg:
wenzelm@53846
    27
  fixes a b :: real
wenzelm@53674
    28
  assumes "a \<ge> 0"
wenzelm@53674
    29
    and "b \<ge> 0"
wenzelm@53846
    30
  shows "0 \<le> a / b"
wenzelm@53674
    31
proof (cases "b = 0")
wenzelm@53674
    32
  case True
wenzelm@53674
    33
  then show ?thesis by auto
wenzelm@53674
    34
next
wenzelm@53674
    35
  case False
wenzelm@53674
    36
  show ?thesis
wenzelm@53674
    37
    apply (rule divide_nonneg_pos)
wenzelm@53674
    38
    using assms False
wenzelm@53674
    39
    apply auto
wenzelm@53674
    40
    done
wenzelm@53674
    41
qed
hoelzl@50526
    42
hoelzl@33741
    43
lemma brouwer_compactness_lemma:
hoelzl@50884
    44
  fixes f :: "'a::metric_space \<Rightarrow> 'b::euclidean_space"
wenzelm@53674
    45
  assumes "compact s"
wenzelm@53674
    46
    and "continuous_on s f"
wenzelm@53688
    47
    and "\<not> (\<exists>x\<in>s. f x = 0)"
wenzelm@53674
    48
  obtains d where "0 < d" and "\<forall>x\<in>s. d \<le> norm (f x)"
wenzelm@53185
    49
proof (cases "s = {}")
wenzelm@53674
    50
  case True
wenzelm@53688
    51
  show thesis
wenzelm@53688
    52
    by (rule that [of 1]) (auto simp: True)
wenzelm@53674
    53
next
wenzelm@49374
    54
  case False
wenzelm@49374
    55
  have "continuous_on s (norm \<circ> f)"
wenzelm@49555
    56
    by (rule continuous_on_intros continuous_on_norm assms(2))+
wenzelm@53674
    57
  with False obtain x where x: "x \<in> s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"
wenzelm@53674
    58
    using continuous_attains_inf[OF assms(1), of "norm \<circ> f"]
wenzelm@53674
    59
    unfolding o_def
wenzelm@53674
    60
    by auto
wenzelm@53674
    61
  have "(norm \<circ> f) x > 0"
wenzelm@53674
    62
    using assms(3) and x(1)
wenzelm@53674
    63
    by auto
wenzelm@53674
    64
  then show ?thesis
wenzelm@53674
    65
    by (rule that) (insert x(2), auto simp: o_def)
wenzelm@49555
    66
qed
hoelzl@33741
    67
wenzelm@49555
    68
lemma kuhn_labelling_lemma:
hoelzl@50526
    69
  fixes P Q :: "'a::euclidean_space \<Rightarrow> bool"
hoelzl@50526
    70
  assumes "(\<forall>x. P x \<longrightarrow> P (f x))"
hoelzl@50526
    71
    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
    72
  shows "\<exists>l. (\<forall>x.\<forall>i\<in>Basis. l x i \<le> (1::nat)) \<and>
hoelzl@50526
    73
             (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 0) \<longrightarrow> (l x i = 0)) \<and>
hoelzl@50526
    74
             (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 1) \<longrightarrow> (l x i = 1)) \<and>
hoelzl@50526
    75
             (\<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@50526
    76
             (\<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
    77
proof -
wenzelm@49374
    78
  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@49374
    79
    by auto
wenzelm@49555
    80
  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@49374
    81
    by auto
wenzelm@49374
    82
  show ?thesis
hoelzl@50526
    83
    unfolding and_forall_thm Ball_def
wenzelm@53185
    84
    apply (subst choice_iff[symmetric])+
wenzelm@49374
    85
    apply rule
wenzelm@49374
    86
    apply rule
wenzelm@49374
    87
  proof -
hoelzl@50526
    88
    case (goal1 x)
hoelzl@50526
    89
    let ?R = "\<lambda>y. (P x \<and> Q xa \<and> x \<bullet> xa = 0 \<longrightarrow> y = (0::nat)) \<and>
hoelzl@50526
    90
        (P x \<and> Q xa \<and> x \<bullet> xa = 1 \<longrightarrow> y = 1) \<and>
hoelzl@50526
    91
        (P x \<and> Q xa \<and> y = 0 \<longrightarrow> x \<bullet> xa \<le> f x \<bullet> xa) \<and>
hoelzl@50526
    92
        (P x \<and> Q xa \<and> y = 1 \<longrightarrow> f x \<bullet> xa \<le> x \<bullet> xa)"
wenzelm@49374
    93
    {
wenzelm@53688
    94
      assume "P x" "Q xa" "xa \<in> Basis"
hoelzl@50526
    95
      then have "0 \<le> f x \<bullet> xa \<and> f x \<bullet> xa \<le> 1"
wenzelm@49374
    96
        using assms(2)[rule_format,of "f x" xa]
wenzelm@49374
    97
        apply (drule_tac assms(1)[rule_format])
wenzelm@49374
    98
        apply auto
wenzelm@49374
    99
        done
wenzelm@49374
   100
    }
wenzelm@53688
   101
    then have "xa \<in> Basis \<Longrightarrow> ?R 0 \<or> ?R 1" by auto
wenzelm@49374
   102
    then show ?case by auto
wenzelm@49374
   103
  qed
wenzelm@49374
   104
qed
wenzelm@49374
   105
wenzelm@53185
   106
hoelzl@33741
   107
subsection {* The key "counting" observation, somewhat abstracted. *}
hoelzl@33741
   108
wenzelm@49374
   109
lemma setsum_Un_disjoint':
wenzelm@53688
   110
  assumes "finite A"
wenzelm@53688
   111
    and "finite B"
wenzelm@53688
   112
    and "A \<inter> B = {}"
wenzelm@53688
   113
    and "A \<union> B = C"
hoelzl@33741
   114
  shows "setsum g C = setsum g A + setsum g B"
hoelzl@33741
   115
  using setsum_Un_disjoint[OF assms(1-3)] and assms(4) by auto
hoelzl@33741
   116
wenzelm@53252
   117
lemma kuhn_counting_lemma:
wenzelm@53688
   118
  assumes "finite faces"
wenzelm@53688
   119
    and "finite simplices"
wenzelm@53688
   120
    and "\<forall>f\<in>faces. bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 1)"
wenzelm@53688
   121
    and "\<forall>f\<in>faces. \<not> bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 2)"
wenzelm@53688
   122
    and "\<forall>s\<in>simplices. compo s \<longrightarrow> (card {f \<in> faces. face f s \<and> compo' f} = 1)"
wenzelm@53688
   123
    and "\<forall>s\<in>simplices. \<not> compo s \<longrightarrow>
wenzelm@53252
   124
      (card {f \<in> faces. face f s \<and> compo' f} = 0) \<or> (card {f \<in> faces. face f s \<and> compo' f} = 2)"
wenzelm@53688
   125
    and "odd(card {f \<in> faces. compo' f \<and> bnd f})"
wenzelm@49374
   126
  shows "odd(card {s \<in> simplices. compo s})"
wenzelm@49374
   127
proof -
wenzelm@49374
   128
  have "\<And>x. {f\<in>faces. compo' f \<and> bnd f \<and> face f x} \<union> {f\<in>faces. compo' f \<and> \<not>bnd f \<and> face f x} =
wenzelm@49374
   129
      {f\<in>faces. compo' f \<and> face f x}"
wenzelm@49374
   130
    "\<And>x. {f \<in> faces. compo' f \<and> bnd f \<and> face f x} \<inter> {f \<in> faces. compo' f \<and> \<not> bnd f \<and> face f x} = {}"
wenzelm@49374
   131
    by auto
wenzelm@53688
   132
  then have lem1: "setsum (\<lambda>s. (card {f \<in> faces. face f s \<and> compo' f})) simplices =
wenzelm@49374
   133
      setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f s}) simplices +
wenzelm@49374
   134
      setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> \<not> (bnd f)}. face f s}) simplices"
wenzelm@53185
   135
    unfolding setsum_addf[symmetric]
wenzelm@49374
   136
    apply -
wenzelm@53688
   137
    apply (rule setsum_cong2)
wenzelm@49374
   138
    using assms(1)
wenzelm@49374
   139
    apply (auto simp add: card_Un_Int, auto simp add:conj_commute)
wenzelm@49374
   140
    done
wenzelm@53252
   141
  have lem2:
wenzelm@53252
   142
    "setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f j}) simplices =
wenzelm@53252
   143
      1 * card {f \<in> faces. compo' f \<and> bnd f}"
wenzelm@53252
   144
    "setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> \<not> bnd f}. face f j}) simplices =
wenzelm@53252
   145
      2 * card {f \<in> faces. compo' f \<and> \<not> bnd f}"
wenzelm@53688
   146
    apply (rule_tac[!] setsum_multicount)
wenzelm@49374
   147
    using assms
wenzelm@49374
   148
    apply auto
wenzelm@49374
   149
    done
wenzelm@53252
   150
  have lem3:
wenzelm@53252
   151
    "setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) simplices =
wenzelm@53252
   152
      setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices.   compo s}+
wenzelm@53252
   153
      setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. \<not> compo s}"
wenzelm@53252
   154
    apply (rule setsum_Un_disjoint')
wenzelm@53252
   155
    using assms(2)
wenzelm@53252
   156
    apply auto
wenzelm@53252
   157
    done
wenzelm@53252
   158
  have lem4: "setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. compo s} =
wenzelm@53252
   159
    setsum (\<lambda>s. 1) {s \<in> simplices. compo s}"
wenzelm@53252
   160
    apply (rule setsum_cong2)
wenzelm@53252
   161
    using assms(5)
wenzelm@53252
   162
    apply auto
wenzelm@53252
   163
    done
hoelzl@33741
   164
  have lem5: "setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. \<not> compo s} =
hoelzl@33741
   165
    setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f})
hoelzl@33741
   166
           {s \<in> simplices. (\<not> compo s) \<and> (card {f \<in> faces. face f s \<and> compo' f} = 0)} +
hoelzl@33741
   167
    setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f})
hoelzl@33741
   168
           {s \<in> simplices. (\<not> compo s) \<and> (card {f \<in> faces. face f s \<and> compo' f} = 2)}"
wenzelm@53252
   169
    apply (rule setsum_Un_disjoint')
wenzelm@53252
   170
    using assms(2,6)
wenzelm@53252
   171
    apply auto
wenzelm@53252
   172
    done
wenzelm@53252
   173
  have *: "int (\<Sum>s\<in>{s \<in> simplices. compo s}. card {f \<in> faces. face f s \<and> compo' f}) =
wenzelm@53185
   174
    int (card {f \<in> faces. compo' f \<and> bnd f} + 2 * card {f \<in> faces. compo' f \<and> \<not> bnd f}) -
hoelzl@33741
   175
    int (card {s \<in> simplices. \<not> compo s \<and> card {f \<in> faces. face f s \<and> compo' f} = 2} * 2)"
hoelzl@33741
   176
    using lem1[unfolded lem3 lem2 lem5] by auto
wenzelm@49374
   177
  have even_minus_odd:"\<And>x y. even x \<Longrightarrow> odd (y::int) \<Longrightarrow> odd (x - y)"
wenzelm@49374
   178
    using assms by auto
wenzelm@49374
   179
  have odd_minus_even:"\<And>x y. odd x \<Longrightarrow> even (y::int) \<Longrightarrow> odd (x - y)"
wenzelm@49374
   180
    using assms by auto
wenzelm@49374
   181
  show ?thesis
wenzelm@53185
   182
    unfolding even_nat_def card_eq_setsum and lem4[symmetric] and *[unfolded card_eq_setsum]
wenzelm@53185
   183
    unfolding card_eq_setsum[symmetric]
wenzelm@49374
   184
    apply (rule odd_minus_even)
wenzelm@49374
   185
    unfolding of_nat_add
wenzelm@49374
   186
    apply(rule odd_plus_even)
wenzelm@49374
   187
    apply(rule assms(7)[unfolded even_nat_def])
wenzelm@49374
   188
    unfolding int_mult
wenzelm@49374
   189
    apply auto
wenzelm@49374
   190
    done
wenzelm@49374
   191
qed
wenzelm@49374
   192
hoelzl@33741
   193
hoelzl@33741
   194
subsection {* The odd/even result for faces of complete vertices, generalized. *}
hoelzl@33741
   195
wenzelm@49374
   196
lemma card_1_exists: "card s = 1 \<longleftrightarrow> (\<exists>!x. x \<in> s)"
wenzelm@49374
   197
  unfolding One_nat_def
wenzelm@49374
   198
  apply rule
wenzelm@49374
   199
  apply (drule card_eq_SucD)
wenzelm@49374
   200
  defer
wenzelm@49555
   201
  apply (erule ex1E)
wenzelm@49374
   202
proof -
wenzelm@53186
   203
  fix x
wenzelm@53186
   204
  assume as: "x \<in> s" "\<forall>y. y \<in> s \<longrightarrow> y = x"
wenzelm@49374
   205
  have *: "s = insert x {}"
wenzelm@49555
   206
    apply (rule set_eqI, rule) unfolding singleton_iff
wenzelm@49374
   207
    apply (rule as(2)[rule_format]) using as(1)
wenzelm@49374
   208
    apply auto
wenzelm@49374
   209
    done
wenzelm@53248
   210
  show "card s = Suc 0"
wenzelm@53248
   211
    unfolding * using card_insert by auto
wenzelm@49374
   212
qed auto
hoelzl@33741
   213
wenzelm@53688
   214
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))"
wenzelm@49374
   215
proof
wenzelm@49374
   216
  assume "card s = 2"
wenzelm@53688
   217
  then obtain x y where s: "s = {x, y}" "x \<noteq> y"
wenzelm@53688
   218
    unfolding numeral_2_eq_2
wenzelm@53186
   219
    apply -
wenzelm@53186
   220
    apply (erule exE conjE | drule card_eq_SucD)+
wenzelm@53186
   221
    apply auto
wenzelm@53186
   222
    done
wenzelm@53186
   223
  show "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)"
wenzelm@53186
   224
    using s by auto
wenzelm@49555
   225
next
wenzelm@49374
   226
  assume "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)"
wenzelm@53688
   227
  then obtain x y where "x \<in> s" "y \<in> s" "x \<noteq> y" "\<forall>z\<in>s. z = x \<or> z = y"
wenzelm@53186
   228
    by auto
wenzelm@53688
   229
  then have "s = {x, y}"
wenzelm@53688
   230
    by auto
wenzelm@53688
   231
  with `x \<noteq> y` show "card s = 2"
wenzelm@53688
   232
    by auto
wenzelm@49555
   233
qed
wenzelm@49555
   234
wenzelm@49555
   235
lemma image_lemma_0:
wenzelm@49555
   236
  assumes "card {a\<in>s. f ` (s - {a}) = t - {b}} = n"
wenzelm@49555
   237
  shows "card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> (f ` s' = t - {b})} = n"
wenzelm@49555
   238
proof -
wenzelm@53185
   239
  have *: "{s'. \<exists>a\<in>s. (s' = s - {a}) \<and> (f ` s' = t - {b})} =
wenzelm@53185
   240
    (\<lambda>a. s - {a}) ` {a\<in>s. f ` (s - {a}) = t - {b}}"
wenzelm@49555
   241
    by auto
wenzelm@53185
   242
  show ?thesis
wenzelm@53185
   243
    unfolding *
wenzelm@53185
   244
    unfolding assms[symmetric]
wenzelm@53185
   245
    apply (rule card_image)
wenzelm@53185
   246
    unfolding inj_on_def
wenzelm@53185
   247
    apply (rule, rule, rule)
wenzelm@53185
   248
    unfolding mem_Collect_eq
wenzelm@53185
   249
    apply auto
wenzelm@53185
   250
    done
wenzelm@49555
   251
qed
wenzelm@49555
   252
wenzelm@49555
   253
lemma image_lemma_1:
wenzelm@53688
   254
  assumes "finite s"
wenzelm@53688
   255
    and "finite t"
wenzelm@53688
   256
    and "card s = card t"
wenzelm@53688
   257
    and "f ` s = t"
wenzelm@53688
   258
    and "b \<in> t"
wenzelm@49555
   259
  shows "card {s'. \<exists>a\<in>s. s' = s - {a} \<and>  f ` s' = t - {b}} = 1"
wenzelm@49555
   260
proof -
wenzelm@53688
   261
  obtain a where a: "b = f a" "a \<in> s"
wenzelm@53688
   262
    using assms(4-5) by auto
wenzelm@53185
   263
  have inj: "inj_on f s"
wenzelm@53185
   264
    apply (rule eq_card_imp_inj_on)
wenzelm@53688
   265
    using assms(1-4)
wenzelm@53688
   266
    apply auto
wenzelm@53185
   267
    done
wenzelm@53185
   268
  have *: "{a \<in> s. f ` (s - {a}) = t - {b}} = {a}"
wenzelm@53185
   269
    apply (rule set_eqI)
wenzelm@53185
   270
    unfolding singleton_iff
wenzelm@49555
   271
    apply (rule, rule inj[unfolded inj_on_def, rule_format])
wenzelm@53688
   272
    unfolding a
wenzelm@53688
   273
    using a(2) and assms and inj[unfolded inj_on_def]
wenzelm@53252
   274
    apply auto
wenzelm@49555
   275
    done
wenzelm@53185
   276
  show ?thesis
wenzelm@53185
   277
    apply (rule image_lemma_0)
wenzelm@53185
   278
    unfolding *
wenzelm@53185
   279
    apply auto
wenzelm@53185
   280
    done
wenzelm@49374
   281
qed
hoelzl@33741
   282
wenzelm@49555
   283
lemma image_lemma_2:
wenzelm@49555
   284
  assumes "finite s" "finite t" "card s = card t" "f ` s \<subseteq> t" "f ` s \<noteq> t" "b \<in> t"
wenzelm@53688
   285
  shows "card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 0 \<or>
wenzelm@53688
   286
         card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 2"
wenzelm@49555
   287
proof (cases "{a\<in>s. f ` (s - {a}) = t - {b}} = {}")
wenzelm@49555
   288
  case True
wenzelm@49555
   289
  then show ?thesis
wenzelm@49555
   290
    apply -
wenzelm@53185
   291
    apply (rule disjI1, rule image_lemma_0)
wenzelm@53252
   292
    using assms(1)
wenzelm@53252
   293
    apply auto
wenzelm@53185
   294
    done
wenzelm@49555
   295
next
wenzelm@49555
   296
  let ?M = "{a\<in>s. f ` (s - {a}) = t - {b}}"
wenzelm@49555
   297
  case False
wenzelm@53688
   298
  then obtain a where "a \<in> ?M"
wenzelm@53688
   299
    by auto
wenzelm@53688
   300
  then have a: "a \<in> s" "f ` (s - {a}) = t - {b}"
wenzelm@53688
   301
    by auto
wenzelm@53688
   302
  have "f a \<in> t - {b}"
wenzelm@53688
   303
    using a and assms by auto
wenzelm@53186
   304
  then have "\<exists>c \<in> s - {a}. f a = f c"
wenzelm@53688
   305
    unfolding image_iff[symmetric] and a
wenzelm@53688
   306
    by auto
wenzelm@53688
   307
  then obtain c where c: "c \<in> s" "a \<noteq> c" "f a = f c"
wenzelm@53688
   308
    by auto
wenzelm@49555
   309
  then have *: "f ` (s - {c}) = f ` (s - {a})"
wenzelm@49555
   310
    apply -
wenzelm@53688
   311
    apply (rule set_eqI)
wenzelm@53688
   312
    apply rule
wenzelm@49555
   313
  proof -
wenzelm@49555
   314
    fix x
wenzelm@49555
   315
    assume "x \<in> f ` (s - {a})"
wenzelm@53688
   316
    then obtain y where y: "f y = x" "y \<in> s - {a}"
wenzelm@53688
   317
      by auto
wenzelm@49555
   318
    then show "x \<in> f ` (s - {c})"
wenzelm@49555
   319
      unfolding image_iff
wenzelm@49555
   320
      apply (rule_tac x = "if y = c then a else y" in bexI)
wenzelm@53688
   321
      using c a
wenzelm@53688
   322
      apply auto
wenzelm@53688
   323
      done
wenzelm@49555
   324
  qed auto
wenzelm@53688
   325
  have "c \<in> ?M"
wenzelm@53186
   326
    unfolding mem_Collect_eq and *
wenzelm@53688
   327
    using a and c(1)
wenzelm@53688
   328
    by auto
wenzelm@49555
   329
  show ?thesis
wenzelm@53688
   330
    apply (rule disjI2)
wenzelm@53688
   331
    apply (rule image_lemma_0)
wenzelm@53688
   332
    unfolding card_2_exists
wenzelm@53688
   333
    apply (rule bexI[OF _ `a\<in>?M`])
wenzelm@53688
   334
    apply (rule bexI[OF _ `c\<in>?M`])
wenzelm@53688
   335
    apply rule
wenzelm@53688
   336
    apply (rule `a \<noteq> c`)
wenzelm@53688
   337
    apply rule
wenzelm@53688
   338
    apply (unfold mem_Collect_eq)
wenzelm@53688
   339
    apply (erule conjE)
wenzelm@53688
   340
  proof -
wenzelm@49555
   341
    fix z
wenzelm@49555
   342
    assume as: "z \<in> s" "f ` (s - {z}) = t - {b}"
wenzelm@49555
   343
    have inj: "inj_on f (s - {z})"
wenzelm@49555
   344
      apply (rule eq_card_imp_inj_on)
wenzelm@53688
   345
      unfolding as
wenzelm@53688
   346
      using as(1) and assms
wenzelm@53186
   347
      apply auto
wenzelm@49555
   348
      done
wenzelm@49555
   349
    show "z = a \<or> z = c"
wenzelm@49555
   350
    proof (rule ccontr)
wenzelm@49555
   351
      assume "\<not> ?thesis"
wenzelm@49555
   352
      then show False
wenzelm@49555
   353
        using inj[unfolded inj_on_def, THEN bspec[where x=a], THEN bspec[where x=c]]
wenzelm@53688
   354
        using `a \<in> s` `c \<in> s` `f a = f c` `a \<noteq> c`
wenzelm@53186
   355
        apply auto
wenzelm@49555
   356
        done
wenzelm@49555
   357
    qed
wenzelm@49555
   358
  qed
wenzelm@49555
   359
qed
wenzelm@49555
   360
hoelzl@33741
   361
hoelzl@33741
   362
subsection {* Combine this with the basic counting lemma. *}
hoelzl@33741
   363
hoelzl@33741
   364
lemma kuhn_complete_lemma:
hoelzl@33741
   365
  assumes "finite simplices"
wenzelm@53688
   366
    and "\<forall>f s. face f s \<longleftrightarrow> (\<exists>a\<in>s. f = s - {a})"
wenzelm@53688
   367
    and "\<forall>s\<in>simplices. card s = n + 2"
wenzelm@53688
   368
    and "\<forall>s\<in>simplices. (rl ` s) \<subseteq> {0..n+1}"
wenzelm@53688
   369
    and "\<forall>f\<in>{f. \<exists>s\<in>simplices. face f s}. bnd f  \<longrightarrow> card {s\<in>simplices. face f s} = 1"
wenzelm@53688
   370
    and "\<forall>f\<in>{f. \<exists>s\<in>simplices. face f s}. \<not> bnd f \<longrightarrow> card {s\<in>simplices. face f s} = 2"
wenzelm@53688
   371
    and "odd (card {f\<in>{f. \<exists>s\<in>simplices. face f s}. rl ` f = {0..n} \<and> bnd f})"
wenzelm@53185
   372
  shows "odd (card {s\<in>simplices. (rl ` s = {0..n+1})})"
wenzelm@49555
   373
  apply (rule kuhn_counting_lemma)
wenzelm@49555
   374
  defer
wenzelm@49555
   375
  apply (rule assms)+
wenzelm@49555
   376
  prefer 3
wenzelm@49555
   377
  apply (rule assms)
wenzelm@53688
   378
  apply (rule_tac[1-2] ballI impI)+
wenzelm@53688
   379
proof -
wenzelm@49555
   380
  have *: "{f. \<exists>s\<in>simplices. \<exists>a\<in>s. f = s - {a}} = (\<Union>s\<in>simplices. {f. \<exists>a\<in>s. (f = s - {a})})"
wenzelm@49555
   381
    by auto
wenzelm@49555
   382
  have **: "\<forall>s\<in>simplices. card s = n + 2 \<and> finite s"
wenzelm@49555
   383
    using assms(3) by (auto intro: card_ge_0_finite)
wenzelm@49555
   384
  show "finite {f. \<exists>s\<in>simplices. face f s}"
wenzelm@49555
   385
    unfolding assms(2)[rule_format] and *
wenzelm@53252
   386
    apply (rule finite_UN_I[OF assms(1)])
wenzelm@53252
   387
    using **
wenzelm@53252
   388
    apply auto
wenzelm@49555
   389
    done
wenzelm@49555
   390
  have *: "\<And>P f s. s\<in>simplices \<Longrightarrow> (f \<in> {f. \<exists>s\<in>simplices. \<exists>a\<in>s. f = s - {a}}) \<and>
wenzelm@53688
   391
    (\<exists>a\<in>s. (f = s - {a})) \<and> P f \<longleftrightarrow> (\<exists>a\<in>s. (f = s - {a}) \<and> P f)"
wenzelm@53688
   392
    by auto
wenzelm@53688
   393
  fix s
wenzelm@53688
   394
  assume s: "s \<in> simplices"
wenzelm@49555
   395
  let ?S = "{f \<in> {f. \<exists>s\<in>simplices. face f s}. face f s \<and> rl ` f = {0..n}}"
wenzelm@53688
   396
  have "{0..n + 1} - {n + 1} = {0..n}"
wenzelm@53688
   397
    by auto
wenzelm@49555
   398
  then have S: "?S = {s'. \<exists>a\<in>s. s' = s - {a} \<and> rl ` s' = {0..n + 1} - {n + 1}}"
wenzelm@49555
   399
    apply -
wenzelm@49555
   400
    apply (rule set_eqI)
wenzelm@53185
   401
    unfolding assms(2)[rule_format] mem_Collect_eq
wenzelm@53185
   402
    unfolding *[OF s, unfolded mem_Collect_eq, where P="\<lambda>x. rl ` x = {0..n}"]
wenzelm@49555
   403
    apply auto
wenzelm@49555
   404
    done
wenzelm@53688
   405
  show "rl ` s = {0..n+1} \<Longrightarrow> card ?S = 1" and "rl ` s \<noteq> {0..n+1} \<Longrightarrow> card ?S = 0 \<or> card ?S = 2"
wenzelm@49555
   406
    unfolding S
wenzelm@53688
   407
    apply (rule_tac[!] image_lemma_1 image_lemma_2)
wenzelm@53252
   408
    using ** assms(4) and s
wenzelm@53252
   409
    apply auto
wenzelm@49555
   410
    done
wenzelm@49555
   411
qed
wenzelm@49555
   412
hoelzl@33741
   413
hoelzl@33741
   414
subsection {*We use the following notion of ordering rather than pointwise indexing. *}
hoelzl@33741
   415
wenzelm@53688
   416
definition "kle n x y \<longleftrightarrow> (\<exists>k\<subseteq>{1..n::nat}. \<forall>j. y j = x j + (if j \<in> k then (1::nat) else 0))"
hoelzl@33741
   417
wenzelm@53185
   418
lemma kle_refl [intro]: "kle n x x"
wenzelm@53185
   419
  unfolding kle_def by auto
hoelzl@33741
   420
wenzelm@53688
   421
lemma kle_antisym: "kle n x y \<and> kle n y x \<longleftrightarrow> x = y"
wenzelm@53185
   422
  unfolding kle_def
wenzelm@53185
   423
  apply rule
wenzelm@53185
   424
  apply auto
wenzelm@53185
   425
  done
hoelzl@33741
   426
wenzelm@53185
   427
lemma pointwise_minimal_pointwise_maximal:
wenzelm@53185
   428
  fixes s :: "(nat \<Rightarrow> nat) set"
wenzelm@53688
   429
  assumes "finite s"
wenzelm@53688
   430
    and "s \<noteq> {}"
wenzelm@53688
   431
    and "\<forall>x\<in>s. \<forall>y\<in>s. (\<forall>j. x j \<le> y j) \<or> (\<forall>j. y j \<le> x j)"
wenzelm@53688
   432
  shows "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<le> x j"
wenzelm@53688
   433
    and "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. x j \<le> a j"
wenzelm@53688
   434
  using assms
wenzelm@53688
   435
  unfolding atomize_conj
wenzelm@53185
   436
proof (induct s rule: finite_induct)
wenzelm@53688
   437
  fix x
wenzelm@53688
   438
  fix F :: "(nat \<Rightarrow> nat) set"
wenzelm@53688
   439
  assume as: "finite F" "x \<notin> F"
hoelzl@33741
   440
    "\<lbrakk>F \<noteq> {}; \<forall>x\<in>F. \<forall>y\<in>F. (\<forall>j. x j \<le> y j) \<or> (\<forall>j. y j \<le> x j)\<rbrakk>
hoelzl@33741
   441
        \<Longrightarrow> (\<exists>a\<in>F. \<forall>x\<in>F. \<forall>j. a j \<le> x j) \<and> (\<exists>a\<in>F. \<forall>x\<in>F. \<forall>j. x j \<le> a j)" "insert x F \<noteq> {}"
hoelzl@33741
   442
    "\<forall>xa\<in>insert x F. \<forall>y\<in>insert x F. (\<forall>j. xa j \<le> y j) \<or> (\<forall>j. y j \<le> xa j)"
wenzelm@49555
   443
  show "(\<exists>a\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. a j \<le> x j) \<and> (\<exists>a\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. x j \<le> a j)"
wenzelm@49555
   444
  proof (cases "F = {}")
wenzelm@49555
   445
    case True
wenzelm@49555
   446
    then show ?thesis
wenzelm@49555
   447
      apply -
wenzelm@49555
   448
      apply (rule, rule_tac[!] x=x in bexI)
wenzelm@49555
   449
      apply auto
wenzelm@49555
   450
      done
wenzelm@49555
   451
  next
wenzelm@49555
   452
    case False
wenzelm@53186
   453
    obtain a b where a: "a\<in>insert x F" "\<forall>x\<in>F. \<forall>j. a j \<le> x j"
wenzelm@53186
   454
      and b: "b \<in> insert x F" "\<forall>x\<in>F. \<forall>j. x j \<le> b j"
wenzelm@53186
   455
      using as(3)[OF False] using as(5) by auto
wenzelm@53186
   456
    have "\<exists>a \<in> insert x F. \<forall>x \<in> insert x F. \<forall>j. a j \<le> x j"
wenzelm@49555
   457
      using as(5)[rule_format,OF a(1) insertI1]
wenzelm@49555
   458
      apply -
wenzelm@49555
   459
    proof (erule disjE)
wenzelm@49555
   460
      assume "\<forall>j. a j \<le> x j"
wenzelm@49555
   461
      then show ?thesis
wenzelm@53185
   462
        apply (rule_tac x=a in bexI)
wenzelm@53688
   463
        using a
wenzelm@53688
   464
        apply auto
wenzelm@53185
   465
        done
wenzelm@49555
   466
    next
wenzelm@49555
   467
      assume "\<forall>j. x j \<le> a j"
wenzelm@49555
   468
      then show ?thesis
wenzelm@49555
   469
        apply (rule_tac x=x in bexI)
wenzelm@53185
   470
        apply (rule, rule)
wenzelm@53185
   471
        apply (insert a)
wenzelm@49555
   472
        apply (erule_tac x=xa in ballE)
wenzelm@49555
   473
        apply (erule_tac x=j in allE)+
wenzelm@49555
   474
        apply auto
wenzelm@49555
   475
        done
wenzelm@49555
   476
    qed
wenzelm@49555
   477
    moreover
hoelzl@33741
   478
    have "\<exists>b\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. x j \<le> b j"
wenzelm@53186
   479
      using as(5)[rule_format,OF b(1) insertI1]
wenzelm@53186
   480
      apply -
wenzelm@49555
   481
    proof (erule disjE)
wenzelm@49555
   482
      assume "\<forall>j. x j \<le> b j"
wenzelm@49555
   483
      then show ?thesis
wenzelm@49555
   484
        apply(rule_tac x=b in bexI) using b
wenzelm@49555
   485
        apply auto
wenzelm@49555
   486
        done
wenzelm@49555
   487
    next
wenzelm@49555
   488
      assume "\<forall>j. b j \<le> x j"
wenzelm@49555
   489
      then show ?thesis
wenzelm@49555
   490
        apply (rule_tac x=x in bexI)
wenzelm@53185
   491
        apply (rule, rule)
wenzelm@53185
   492
        apply (insert b)
wenzelm@49555
   493
        apply (erule_tac x=xa in ballE)
wenzelm@49555
   494
        apply (erule_tac x=j in allE)+
wenzelm@49555
   495
        apply auto
wenzelm@49555
   496
        done
wenzelm@49555
   497
    qed
wenzelm@49555
   498
    ultimately show ?thesis by auto
wenzelm@49555
   499
  qed
wenzelm@49555
   500
qed auto
wenzelm@49555
   501
hoelzl@33741
   502
wenzelm@53688
   503
lemma kle_imp_pointwise: "kle n x y \<Longrightarrow> \<forall>j. x j \<le> y j"
wenzelm@53186
   504
  unfolding kle_def by auto
hoelzl@33741
   505
wenzelm@49555
   506
lemma pointwise_antisym:
wenzelm@49555
   507
  fixes x :: "nat \<Rightarrow> nat"
wenzelm@53252
   508
  shows "(\<forall>j. x j \<le> y j) \<and> (\<forall>j. y j \<le> x j) \<longleftrightarrow> x = y"
wenzelm@53688
   509
  apply rule
wenzelm@53688
   510
  apply (rule ext)
wenzelm@53688
   511
  apply (erule conjE)
wenzelm@53252
   512
  apply (erule_tac x = xa in allE)+
wenzelm@49555
   513
  apply auto
wenzelm@49555
   514
  done
hoelzl@33741
   515
wenzelm@49555
   516
lemma kle_trans:
wenzelm@53688
   517
  assumes "kle n x y"
wenzelm@53688
   518
    and "kle n y z"
wenzelm@53688
   519
    and "kle n x z \<or> kle n z x"
wenzelm@49555
   520
  shows "kle n x z"
wenzelm@49555
   521
  using assms
wenzelm@53688
   522
  apply -
wenzelm@53688
   523
  apply (erule disjE)
wenzelm@53688
   524
  apply assumption
wenzelm@49555
   525
proof -
wenzelm@49555
   526
  case goal1
wenzelm@49555
   527
  then have "x = z"
wenzelm@49555
   528
    apply -
wenzelm@49555
   529
    apply (rule ext)
wenzelm@49555
   530
    apply (drule kle_imp_pointwise)+
wenzelm@49555
   531
    apply (erule_tac x=xa in allE)+
wenzelm@49555
   532
    apply auto
wenzelm@49555
   533
    done
wenzelm@49555
   534
  then show ?case by auto
wenzelm@49555
   535
qed
hoelzl@33741
   536
wenzelm@49555
   537
lemma kle_strict:
wenzelm@53688
   538
  assumes "kle n x y"
wenzelm@53688
   539
    and "x \<noteq> y"
wenzelm@53688
   540
  shows "\<forall>j. x j \<le> y j"
wenzelm@53688
   541
    and "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x k < y k"
wenzelm@49555
   542
  apply (rule kle_imp_pointwise[OF assms(1)])
wenzelm@49555
   543
proof -
wenzelm@55493
   544
  obtain k where k: "k \<subseteq> {1..n} \<and> (\<forall>j. y j = x j + (if j \<in> k then 1 else 0))"
wenzelm@55493
   545
    using assms(1)[unfolded kle_def] ..
wenzelm@53688
   546
  show "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x k < y k"
wenzelm@55493
   547
  proof (cases "k = {}")
wenzelm@55493
   548
    case True
wenzelm@55493
   549
    then have "x = y"
wenzelm@55493
   550
      apply -
wenzelm@55493
   551
      apply (rule ext)
wenzelm@55493
   552
      using k
wenzelm@55493
   553
      apply auto
wenzelm@55493
   554
      done
wenzelm@55493
   555
    then show ?thesis
wenzelm@55493
   556
      using assms(2) by auto
wenzelm@55493
   557
  next
wenzelm@55493
   558
    case False
wenzelm@55493
   559
    then have "(SOME k'. k' \<in> k) \<in> k"
wenzelm@55493
   560
      apply -
wenzelm@55493
   561
      apply (rule someI_ex)
wenzelm@55493
   562
      apply auto
wenzelm@55493
   563
      done
wenzelm@55493
   564
    then show ?thesis
wenzelm@55493
   565
      apply (rule_tac x = "SOME k'. k' \<in> k" in exI)
wenzelm@55493
   566
      using k
wenzelm@55493
   567
      apply auto
wenzelm@55493
   568
      done
wenzelm@49555
   569
  qed
wenzelm@49555
   570
qed
hoelzl@33741
   571
wenzelm@53185
   572
lemma kle_minimal:
wenzelm@53688
   573
  assumes "finite s"
wenzelm@53688
   574
    and "s \<noteq> {}"
wenzelm@53688
   575
    and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
wenzelm@53185
   576
  shows "\<exists>a\<in>s. \<forall>x\<in>s. kle n a x"
wenzelm@53185
   577
proof -
wenzelm@53185
   578
  have "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<le> x j"
wenzelm@53185
   579
    apply (rule pointwise_minimal_pointwise_maximal(1)[OF assms(1-2)])
wenzelm@53688
   580
    apply rule
wenzelm@53688
   581
    apply rule
wenzelm@53688
   582
    apply (drule_tac assms(3)[rule_format])
wenzelm@53688
   583
    apply assumption
wenzelm@53252
   584
    using kle_imp_pointwise
wenzelm@53252
   585
    apply auto
wenzelm@53185
   586
    done
wenzelm@55493
   587
  then obtain a where a: "a \<in> s" "\<forall>x\<in>s. \<forall>j. a j \<le> x j" ..
wenzelm@53185
   588
  show ?thesis
wenzelm@53252
   589
    apply (rule_tac x = a in bexI)
wenzelm@53185
   590
  proof
wenzelm@53185
   591
    fix x
wenzelm@53185
   592
    assume "x \<in> s"
wenzelm@53185
   593
    show "kle n a x"
wenzelm@53185
   594
      using assms(3)[rule_format,OF a(1) `x\<in>s`]
wenzelm@53185
   595
      apply -
wenzelm@53185
   596
    proof (erule disjE)
wenzelm@53185
   597
      assume "kle n x a"
wenzelm@53252
   598
      then have "x = a"
wenzelm@53185
   599
        apply -
wenzelm@53185
   600
        unfolding pointwise_antisym[symmetric]
wenzelm@53185
   601
        apply (drule kle_imp_pointwise)
wenzelm@53252
   602
        using a(2)[rule_format,OF `x\<in>s`]
wenzelm@53252
   603
        apply auto
wenzelm@53185
   604
        done
wenzelm@53252
   605
      then show ?thesis using kle_refl by auto
wenzelm@53185
   606
    qed
wenzelm@53185
   607
  qed (insert a, auto)
wenzelm@53185
   608
qed
hoelzl@33741
   609
wenzelm@53185
   610
lemma kle_maximal:
wenzelm@53688
   611
  assumes "finite s"
wenzelm@53688
   612
    and "s \<noteq> {}"
wenzelm@53688
   613
    and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
wenzelm@53185
   614
  shows "\<exists>a\<in>s. \<forall>x\<in>s. kle n x a"
wenzelm@53185
   615
proof -
wenzelm@53185
   616
  have "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<ge> x j"
wenzelm@53185
   617
    apply (rule pointwise_minimal_pointwise_maximal(2)[OF assms(1-2)])
wenzelm@53688
   618
    apply rule
wenzelm@53688
   619
    apply rule
wenzelm@53185
   620
    apply (drule_tac assms(3)[rule_format],assumption)
wenzelm@53688
   621
    using kle_imp_pointwise
wenzelm@53688
   622
    apply auto
wenzelm@53185
   623
    done
wenzelm@55493
   624
  then obtain a where a: "a \<in> s" "\<forall>x\<in>s. \<forall>j. x j \<le> a j" ..
wenzelm@55522
   625
  show ?thesis
wenzelm@53186
   626
    apply (rule_tac x = a in bexI)
wenzelm@53185
   627
  proof
wenzelm@53185
   628
    fix x
wenzelm@53185
   629
    assume "x \<in> s"
wenzelm@53185
   630
    show "kle n x a"
wenzelm@53185
   631
      using assms(3)[rule_format,OF a(1) `x\<in>s`]
wenzelm@53185
   632
      apply -
wenzelm@53185
   633
    proof (erule disjE)
wenzelm@53185
   634
      assume "kle n a x"
wenzelm@53674
   635
      then have "x = a"
wenzelm@53185
   636
        apply -
wenzelm@53185
   637
        unfolding pointwise_antisym[symmetric]
wenzelm@53185
   638
        apply (drule kle_imp_pointwise)
wenzelm@53688
   639
        using a(2)[rule_format,OF `x\<in>s`]
wenzelm@53688
   640
        apply auto
wenzelm@53185
   641
        done
wenzelm@53688
   642
      then show ?thesis
wenzelm@53688
   643
        using kle_refl by auto
wenzelm@53185
   644
    qed
wenzelm@53185
   645
  qed (insert a, auto)
wenzelm@53185
   646
qed
hoelzl@33741
   647
wenzelm@53185
   648
lemma kle_strict_set:
wenzelm@53688
   649
  assumes "kle n x y"
wenzelm@53688
   650
    and "x \<noteq> y"
wenzelm@53185
   651
  shows "1 \<le> card {k\<in>{1..n}. x k < y k}"
wenzelm@53185
   652
proof -
wenzelm@55493
   653
  obtain i where "1 \<le> i" "i \<le> n" "x i < y i"
wenzelm@55493
   654
    using kle_strict(2)[OF assms] by blast
wenzelm@53674
   655
  then have "card {i} \<le> card {k\<in>{1..n}. x k < y k}"
wenzelm@53185
   656
    apply -
wenzelm@53185
   657
    apply (rule card_mono)
wenzelm@53185
   658
    apply auto
wenzelm@53185
   659
    done
wenzelm@53688
   660
  then show ?thesis
wenzelm@53688
   661
    by auto
wenzelm@53185
   662
qed
hoelzl@33741
   663
hoelzl@33741
   664
lemma kle_range_combine:
wenzelm@53688
   665
  assumes "kle n x y"
wenzelm@53688
   666
    and "kle n y z"
wenzelm@53688
   667
    and "kle n x z \<or> kle n z x"
wenzelm@53688
   668
    and "m1 \<le> card {k\<in>{1..n}. x k < y k}"
wenzelm@53688
   669
    and "m2 \<le> card {k\<in>{1..n}. y k < z k}"
hoelzl@33741
   670
  shows "kle n x z \<and> m1 + m2 \<le> card {k\<in>{1..n}. x k < z k}"
wenzelm@53688
   671
  apply rule
wenzelm@53688
   672
  apply (rule kle_trans[OF assms(1-3)])
wenzelm@53185
   673
proof -
wenzelm@53185
   674
  have "\<And>j. x j < y j \<Longrightarrow> x j < z j"
wenzelm@53185
   675
    apply (rule less_le_trans)
wenzelm@53252
   676
    using kle_imp_pointwise[OF assms(2)]
wenzelm@53252
   677
    apply auto
wenzelm@53185
   678
    done
wenzelm@53185
   679
  moreover
wenzelm@53185
   680
  have "\<And>j. y j < z j \<Longrightarrow> x j < z j"
wenzelm@53185
   681
    apply (rule le_less_trans)
wenzelm@53252
   682
    using kle_imp_pointwise[OF assms(1)]
wenzelm@53252
   683
    apply auto
wenzelm@53185
   684
    done
wenzelm@53185
   685
  ultimately
wenzelm@53185
   686
  have *: "{k\<in>{1..n}. x k < y k} \<union> {k\<in>{1..n}. y k < z k} = {k\<in>{1..n}. x k < z k}"
wenzelm@53185
   687
    by auto
wenzelm@53185
   688
  have **: "{k \<in> {1..n}. x k < y k} \<inter> {k \<in> {1..n}. y k < z k} = {}"
wenzelm@53185
   689
    unfolding disjoint_iff_not_equal
wenzelm@53688
   690
    apply rule
wenzelm@53688
   691
    apply rule
wenzelm@53688
   692
    apply (unfold mem_Collect_eq)
wenzelm@53688
   693
    apply (rule notI)
wenzelm@53185
   694
    apply (erule conjE)+
wenzelm@53185
   695
  proof -
wenzelm@53185
   696
    fix i j
wenzelm@53688
   697
    assume as: "i \<in> {1..n}" "x i < y i" "j \<in> {1..n}" "y j < z j" "i = j"
wenzelm@55493
   698
    obtain kx where kx: "kx \<subseteq> {1..n} \<and> (\<forall>j. y j = x j + (if j \<in> kx then 1 else 0))"
wenzelm@55493
   699
      using assms(1)[unfolded kle_def] ..
wenzelm@53688
   700
    have "x i < y i"
wenzelm@53688
   701
      using as by auto
wenzelm@53688
   702
    then have "i \<in> kx"
wenzelm@53688
   703
      using as(1) kx
wenzelm@53688
   704
      apply -
wenzelm@53688
   705
      apply (rule ccontr)
wenzelm@53185
   706
      apply auto
wenzelm@53185
   707
      done
wenzelm@53688
   708
    then have "x i + 1 = y i"
wenzelm@53688
   709
      using kx by auto
wenzelm@53185
   710
    moreover
wenzelm@55493
   711
    obtain ky where ky: "ky \<subseteq> {1..n} \<and> (\<forall>j. z j = y j + (if j \<in> ky then 1 else 0))"
wenzelm@55493
   712
      using assms(2)[unfolded kle_def] ..
wenzelm@53688
   713
    have "y i < z i"
wenzelm@53688
   714
      using as by auto
wenzelm@53688
   715
    then have "i \<in> ky"
wenzelm@53688
   716
      using as(1) ky
wenzelm@53688
   717
      apply -
wenzelm@53688
   718
      apply (rule ccontr)
wenzelm@53185
   719
      apply auto
wenzelm@53185
   720
      done
wenzelm@53688
   721
    then have "y i + 1 = z i"
wenzelm@53688
   722
      using ky by auto
wenzelm@53185
   723
    ultimately
wenzelm@53688
   724
    have "z i = x i + 2"
wenzelm@53688
   725
      by auto
wenzelm@53688
   726
    then show False
wenzelm@53688
   727
      using assms(3)
wenzelm@53688
   728
      unfolding kle_def
wenzelm@53185
   729
      by (auto simp add: split_if_eq1)
wenzelm@53185
   730
  qed
wenzelm@53688
   731
  have fin: "\<And>P. finite {x\<in>{1..n::nat}. P x}"
wenzelm@53688
   732
    by auto
wenzelm@53185
   733
  have "m1 + m2 \<le> card {k\<in>{1..n}. x k < y k} + card {k\<in>{1..n}. y k < z k}"
wenzelm@53185
   734
    using assms(4-5) by auto
wenzelm@53185
   735
  also have "\<dots> \<le> card {k\<in>{1..n}. x k < z k}"
wenzelm@53688
   736
    unfolding card_Un_Int[OF fin fin]
wenzelm@53688
   737
    unfolding * **
wenzelm@53688
   738
    by auto
wenzelm@53688
   739
  finally show "m1 + m2 \<le> card {k \<in> {1..n}. x k < z k}"
wenzelm@53688
   740
    by auto
wenzelm@53185
   741
qed
hoelzl@33741
   742
hoelzl@33741
   743
lemma kle_range_combine_l:
wenzelm@53185
   744
  assumes "kle n x y"
wenzelm@53185
   745
    and "kle n y z"
wenzelm@53185
   746
    and "kle n x z \<or> kle n z x"
wenzelm@53185
   747
    and "m \<le> card {k\<in>{1..n}. y(k) < z(k)}"
hoelzl@33741
   748
  shows "kle n x z \<and> m \<le> card {k\<in>{1..n}. x(k) < z(k)}"
hoelzl@33741
   749
  using kle_range_combine[OF assms(1-3) _ assms(4), of 0] by auto
hoelzl@33741
   750
hoelzl@33741
   751
lemma kle_range_combine_r:
wenzelm@53185
   752
  assumes "kle n x y"
wenzelm@53185
   753
    and "kle n y z"
wenzelm@53185
   754
    and "kle n x z \<or> kle n z x" "m \<le> card {k\<in>{1..n}. x k < y k}"
hoelzl@33741
   755
  shows "kle n x z \<and> m \<le> card {k\<in>{1..n}. x(k) < z(k)}"
hoelzl@33741
   756
  using kle_range_combine[OF assms(1-3) assms(4), of 0] by auto
hoelzl@33741
   757
hoelzl@33741
   758
lemma kle_range_induct:
wenzelm@53185
   759
  assumes "card s = Suc m"
wenzelm@53185
   760
    and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
wenzelm@53185
   761
  shows "\<exists>x\<in>s. \<exists>y\<in>s. kle n x y \<and> m \<le> card {k\<in>{1..n}. x k < y k}"
wenzelm@53185
   762
proof -
wenzelm@53688
   763
  have "finite s" and "s \<noteq> {}"
wenzelm@53688
   764
    using assms(1)
wenzelm@53185
   765
    by (auto intro: card_ge_0_finite)
wenzelm@53688
   766
  then show ?thesis
wenzelm@53688
   767
    using assms
wenzelm@53185
   768
  proof (induct m arbitrary: s)
wenzelm@53185
   769
    case 0
wenzelm@53688
   770
    then show ?case
wenzelm@53688
   771
      using kle_refl by auto
wenzelm@53185
   772
  next
wenzelm@53185
   773
    case (Suc m)
wenzelm@53185
   774
    then obtain a where a: "a \<in> s" "\<forall>x\<in>s. kle n a x"
wenzelm@53185
   775
      using kle_minimal[of s n] by auto
wenzelm@53185
   776
    show ?case
wenzelm@53185
   777
    proof (cases "s \<subseteq> {a}")
wenzelm@53185
   778
      case False
wenzelm@53688
   779
      then have "card (s - {a}) = Suc m" and "s - {a} \<noteq> {}"
wenzelm@53688
   780
        using card_Diff_singleton[OF _ a(1)] Suc(4) `finite s`
wenzelm@53688
   781
        by auto
wenzelm@53688
   782
      then obtain x b where xb:
wenzelm@53688
   783
        "x \<in> s - {a}"
wenzelm@53688
   784
        "b \<in> s - {a}"
wenzelm@53688
   785
        "kle n x b"
wenzelm@53688
   786
        "m \<le> card {k \<in> {1..n}. x k < b k}"
wenzelm@53688
   787
        using Suc(1)[of "s - {a}"]
wenzelm@53688
   788
        using Suc(5) `finite s`
wenzelm@53688
   789
        by auto
wenzelm@53688
   790
      have "1 \<le> card {k \<in> {1..n}. a k < x k}" and "m \<le> card {k \<in> {1..n}. x k < b k}"
wenzelm@53185
   791
        apply (rule kle_strict_set)
wenzelm@53185
   792
        apply (rule a(2)[rule_format])
wenzelm@53248
   793
        using a and xb
wenzelm@53248
   794
        apply auto
wenzelm@53185
   795
        done
wenzelm@53674
   796
      then show ?thesis
wenzelm@53688
   797
        apply (rule_tac x=a in bexI)
wenzelm@53688
   798
        apply (rule_tac x=b in bexI)
wenzelm@53185
   799
        using kle_range_combine[OF a(2)[rule_format] xb(3) Suc(5)[rule_format], of 1 "m"]
wenzelm@53248
   800
        using a(1) xb(1-2)
wenzelm@53248
   801
        apply auto
wenzelm@53185
   802
        done
wenzelm@53185
   803
    next
wenzelm@53185
   804
      case True
wenzelm@53688
   805
      then have "s = {a}"
wenzelm@53688
   806
        using Suc(3) by auto
wenzelm@53688
   807
      then have "card s = 1"
wenzelm@53688
   808
        by auto
wenzelm@53688
   809
      then have False
wenzelm@53688
   810
        using Suc(4) `finite s` by auto
wenzelm@53688
   811
      then show ?thesis
wenzelm@53688
   812
        by auto
wenzelm@53185
   813
    qed
wenzelm@53185
   814
  qed
wenzelm@53185
   815
qed
hoelzl@33741
   816
hoelzl@33741
   817
lemma kle_Suc: "kle n x y \<Longrightarrow> kle (n + 1) x y"
wenzelm@53185
   818
  unfolding kle_def
wenzelm@53185
   819
  apply (erule exE)
wenzelm@53185
   820
  apply (rule_tac x=k in exI)
wenzelm@53185
   821
  apply auto
wenzelm@53185
   822
  done
hoelzl@33741
   823
wenzelm@53185
   824
lemma kle_trans_1:
wenzelm@53185
   825
  assumes "kle n x y"
wenzelm@53688
   826
  shows "x j \<le> y j"
wenzelm@53688
   827
    and "y j \<le> x j + 1"
wenzelm@53185
   828
  using assms[unfolded kle_def] by auto
hoelzl@33741
   829
wenzelm@53185
   830
lemma kle_trans_2:
wenzelm@53688
   831
  assumes "kle n a b"
wenzelm@53688
   832
    and "kle n b c"
wenzelm@53688
   833
    and "\<forall>j. c j \<le> a j + 1"
wenzelm@53185
   834
  shows "kle n a c"
wenzelm@53185
   835
proof -
wenzelm@55493
   836
  obtain kk1 where kk1: "kk1 \<subseteq> {1..n} \<and> (\<forall>j. b j = a j + (if j \<in> kk1 then 1 else 0))"
wenzelm@55493
   837
    using assms(1)[unfolded kle_def] ..
wenzelm@55493
   838
  obtain kk2 where kk2: "kk2 \<subseteq> {1..n} \<and> (\<forall>j. c j = b j + (if j \<in> kk2 then 1 else 0))"
wenzelm@55493
   839
    using assms(2)[unfolded kle_def] ..
wenzelm@53185
   840
  show ?thesis
wenzelm@53185
   841
    unfolding kle_def
wenzelm@53185
   842
    apply (rule_tac x="kk1 \<union> kk2" in exI)
wenzelm@53252
   843
    apply rule
wenzelm@53252
   844
    defer
wenzelm@53185
   845
  proof
wenzelm@53185
   846
    fix i
wenzelm@53185
   847
    show "c i = a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)"
wenzelm@53185
   848
    proof (cases "i \<in> kk1 \<union> kk2")
wenzelm@53185
   849
      case True
wenzelm@53674
   850
      then have "c i \<ge> a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)"
wenzelm@53185
   851
        unfolding kk1[THEN conjunct2,rule_format,of i] kk2[THEN conjunct2,rule_format,of i]
wenzelm@53185
   852
        by auto
wenzelm@53185
   853
      moreover
wenzelm@53185
   854
      have "c i \<le> a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)"
wenzelm@53185
   855
        using True assms(3) by auto
wenzelm@53185
   856
      ultimately show ?thesis by auto
wenzelm@53185
   857
    next
wenzelm@53185
   858
      case False
wenzelm@53688
   859
      then show ?thesis
wenzelm@53688
   860
        using kk1 kk2 by auto
wenzelm@53185
   861
    qed
wenzelm@53185
   862
  qed (insert kk1 kk2, auto)
wenzelm@53185
   863
qed
hoelzl@33741
   864
wenzelm@53185
   865
lemma kle_between_r:
wenzelm@53688
   866
  assumes "kle n a b"
wenzelm@53688
   867
    and "kle n b c"
wenzelm@53688
   868
    and "kle n a x"
wenzelm@53688
   869
    and "kle n c x"
wenzelm@53185
   870
  shows "kle n b x"
wenzelm@53185
   871
  apply (rule kle_trans_2[OF assms(2,4)])
wenzelm@53185
   872
proof
wenzelm@53688
   873
  have *: "\<And>c b x::nat. x \<le> c + 1 \<Longrightarrow> c \<le> b \<Longrightarrow> x \<le> b + 1"
wenzelm@53688
   874
    by auto
wenzelm@53185
   875
  fix j
wenzelm@53185
   876
  show "x j \<le> b j + 1"
wenzelm@53185
   877
    apply (rule *)
wenzelm@53186
   878
    using kle_trans_1[OF assms(1),of j] kle_trans_1[OF assms(3), of j]
wenzelm@53186
   879
    apply auto
wenzelm@53185
   880
    done
wenzelm@53185
   881
qed
hoelzl@33741
   882
wenzelm@53185
   883
lemma kle_between_l:
wenzelm@53688
   884
  assumes "kle n a b"
wenzelm@53688
   885
    and "kle n b c"
wenzelm@53688
   886
    and "kle n x a"
wenzelm@53688
   887
    and "kle n x c"
wenzelm@53185
   888
  shows "kle n x b"
wenzelm@53185
   889
  apply (rule kle_trans_2[OF assms(3,1)])
wenzelm@53185
   890
proof
wenzelm@53185
   891
  have *: "\<And>c b x::nat. c \<le> x + 1 \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> x + 1"
wenzelm@53185
   892
    by auto
wenzelm@53185
   893
  fix j
wenzelm@53185
   894
  show "b j \<le> x j + 1"
wenzelm@53185
   895
    apply (rule *)
wenzelm@53186
   896
    using kle_trans_1[OF assms(2),of j] kle_trans_1[OF assms(4), of j]
wenzelm@53186
   897
    apply auto
wenzelm@53185
   898
    done
wenzelm@53185
   899
qed
hoelzl@33741
   900
hoelzl@33741
   901
lemma kle_adjacent:
wenzelm@53688
   902
  assumes "\<forall>j. b j = (if j = k then a(j) + 1 else a j)"
wenzelm@53688
   903
    and "kle n a x"
wenzelm@53688
   904
    and "kle n x b"
wenzelm@53252
   905
  shows "x = a \<or> x = b"
wenzelm@53185
   906
proof (cases "x k = a k")
wenzelm@53185
   907
  case True
wenzelm@53185
   908
  show ?thesis
wenzelm@53186
   909
    apply (rule disjI1)
wenzelm@53186
   910
    apply (rule ext)
wenzelm@53185
   911
  proof -
wenzelm@53185
   912
    fix j
wenzelm@53688
   913
    have "x j \<le> a j"
wenzelm@53688
   914
      using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]
wenzelm@53186
   915
      unfolding assms(1)[rule_format]
wenzelm@53186
   916
      apply -
wenzelm@53186
   917
      apply(cases "j = k")
wenzelm@53186
   918
      using True
wenzelm@53186
   919
      apply auto
wenzelm@53186
   920
      done
wenzelm@53252
   921
    then show "x j = a j"
wenzelm@53688
   922
      using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]]
wenzelm@53688
   923
      by auto
wenzelm@53185
   924
  qed
wenzelm@53185
   925
next
wenzelm@53185
   926
  case False
wenzelm@53688
   927
  show ?thesis
wenzelm@53688
   928
    apply (rule disjI2)
wenzelm@53688
   929
    apply (rule ext)
wenzelm@53185
   930
  proof -
wenzelm@53185
   931
    fix j
wenzelm@53248
   932
    have "x j \<ge> b j"
wenzelm@53248
   933
      using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]]
wenzelm@53248
   934
      unfolding assms(1)[rule_format]
wenzelm@53248
   935
      apply -
wenzelm@53688
   936
      apply (cases "j = k")
wenzelm@53688
   937
      using False
wenzelm@53688
   938
      apply auto
wenzelm@53688
   939
      done
wenzelm@53252
   940
    then show "x j = b j"
wenzelm@53248
   941
      using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]]
wenzelm@53185
   942
    by auto
wenzelm@53185
   943
  qed
wenzelm@53185
   944
qed
wenzelm@53185
   945
hoelzl@33741
   946
wenzelm@53688
   947
subsection {* Kuhn's notion of a simplex (a reformulation to avoid so much indexing) *}
hoelzl@33741
   948
hoelzl@33741
   949
definition "ksimplex p n (s::(nat \<Rightarrow> nat) set) \<longleftrightarrow>
wenzelm@53674
   950
  card s = n + 1 \<and>
wenzelm@53674
   951
  (\<forall>x\<in>s. \<forall>j. x j \<le> p) \<and>
wenzelm@53674
   952
  (\<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p) \<and>
wenzelm@53674
   953
  (\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x)"
hoelzl@33741
   954
wenzelm@53185
   955
lemma ksimplexI:
wenzelm@53185
   956
  "card s = n + 1 \<Longrightarrow>
wenzelm@53185
   957
  \<forall>x\<in>s. \<forall>j. x j \<le> p \<Longrightarrow>
wenzelm@53185
   958
  \<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p \<Longrightarrow>
wenzelm@53185
   959
  \<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x \<Longrightarrow>
wenzelm@53185
   960
  ksimplex p n s"
hoelzl@33741
   961
  unfolding ksimplex_def by auto
hoelzl@33741
   962
wenzelm@53185
   963
lemma ksimplex_eq:
wenzelm@53185
   964
  "ksimplex p n (s::(nat \<Rightarrow> nat) set) \<longleftrightarrow>
wenzelm@53688
   965
    card s = n + 1 \<and>
wenzelm@53688
   966
    finite s \<and>
wenzelm@53185
   967
    (\<forall>x\<in>s. \<forall>j. x(j) \<le> p) \<and>
wenzelm@53688
   968
    (\<forall>x\<in>s. \<forall>j. j\<notin>{1..n} \<longrightarrow> x j = p) \<and>
wenzelm@53688
   969
    (\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x)"
hoelzl@33741
   970
  unfolding ksimplex_def by (auto intro: card_ge_0_finite)
hoelzl@33741
   971
wenzelm@53185
   972
lemma ksimplex_extrema:
wenzelm@53185
   973
  assumes "ksimplex p n s"
wenzelm@53688
   974
  obtains a b where "a \<in> s"
wenzelm@53688
   975
    and "b \<in> s"
wenzelm@53688
   976
    and "\<forall>x\<in>s. kle n a x \<and> kle n x b"
wenzelm@53688
   977
    and "\<forall>i. b i = (if i \<in> {1..n} then a i + 1 else a i)"
wenzelm@53185
   978
proof (cases "n = 0")
wenzelm@53185
   979
  case True
wenzelm@53185
   980
  obtain x where *: "s = {x}"
wenzelm@53185
   981
    using assms[unfolded ksimplex_eq True,THEN conjunct1]
wenzelm@53688
   982
    unfolding add_0_left card_1_exists
wenzelm@53688
   983
    by auto
wenzelm@53185
   984
  show ?thesis
wenzelm@53688
   985
    apply (rule that[of x x])
wenzelm@53688
   986
    unfolding * True
wenzelm@53185
   987
    apply auto
wenzelm@53185
   988
    done
wenzelm@53185
   989
next
hoelzl@33741
   990
  note assm = assms[unfolded ksimplex_eq]
wenzelm@53185
   991
  case False
wenzelm@53688
   992
  have "s \<noteq> {}"
wenzelm@53688
   993
    using assm by auto
wenzelm@53185
   994
  obtain a where a: "a \<in> s" "\<forall>x\<in>s. kle n a x"
wenzelm@53688
   995
    using `s \<noteq> {}` assm
wenzelm@53688
   996
    using kle_minimal[of s n]
wenzelm@53688
   997
    by auto
wenzelm@53185
   998
  obtain b where b: "b \<in> s" "\<forall>x\<in>s. kle n x b"
wenzelm@53688
   999
    using `s \<noteq> {}` assm
wenzelm@53688
  1000
    using kle_maximal[of s n]
wenzelm@53688
  1001
    by auto
wenzelm@53248
  1002
  obtain c d where c_d: "c \<in> s" "d \<in> s" "kle n c d" "n \<le> card {k \<in> {1..n}. c k < d k}"
wenzelm@53688
  1003
    using kle_range_induct[of s n n]
wenzelm@53688
  1004
    using assm
wenzelm@53688
  1005
    by auto
wenzelm@53185
  1006
  have "kle n c b \<and> n \<le> card {k \<in> {1..n}. c k < b k}"
wenzelm@53185
  1007
    apply (rule kle_range_combine_r[where y=d])
wenzelm@53252
  1008
    using c_d a b
wenzelm@53252
  1009
    apply auto
wenzelm@53185
  1010
    done
wenzelm@53674
  1011
  then have "kle n a b \<and> n \<le> card {k\<in>{1..n}. a(k) < b(k)}"
wenzelm@53185
  1012
    apply -
wenzelm@53185
  1013
    apply (rule kle_range_combine_l[where y=c])
wenzelm@53252
  1014
    using a `c \<in> s` `b \<in> s`
wenzelm@53252
  1015
    apply auto
wenzelm@53185
  1016
    done
wenzelm@53185
  1017
  moreover
wenzelm@53185
  1018
  have "card {1..n} \<ge> card {k\<in>{1..n}. a(k) < b(k)}"
wenzelm@53185
  1019
    by (rule card_mono) auto
wenzelm@53185
  1020
  ultimately
wenzelm@53185
  1021
  have *: "{k\<in>{1 .. n}. a k < b k} = {1..n}"
wenzelm@53185
  1022
    apply -
wenzelm@53185
  1023
    apply (rule card_subset_eq)
wenzelm@53185
  1024
    apply auto
wenzelm@53185
  1025
    done
wenzelm@53185
  1026
  show ?thesis
wenzelm@53185
  1027
    apply (rule that[OF a(1) b(1)])
wenzelm@53185
  1028
    defer
wenzelm@53688
  1029
    apply (subst *[symmetric])
wenzelm@53688
  1030
    unfolding mem_Collect_eq
wenzelm@53185
  1031
  proof
wenzelm@55493
  1032
    obtain k where k: "k \<subseteq> {1..n} \<and> (\<forall>j. b j = a j + (if j \<in> k then 1 else 0))"
wenzelm@55493
  1033
      using a(2)[rule_format, OF b(1), unfolded kle_def] ..
wenzelm@53185
  1034
    fix i
wenzelm@53185
  1035
    show "b i = (if i \<in> {1..n} \<and> a i < b i then a i + 1 else a i)"
wenzelm@53185
  1036
    proof (cases "i \<in> {1..n}")
wenzelm@53185
  1037
      case True
wenzelm@53688
  1038
      then show ?thesis
wenzelm@53688
  1039
        unfolding k[THEN conjunct2,rule_format] by auto
wenzelm@53185
  1040
    next
wenzelm@53185
  1041
      case False
wenzelm@53688
  1042
      have "a i = p"
wenzelm@53688
  1043
        using assm and False `a\<in>s` by auto
wenzelm@53688
  1044
      moreover have "b i = p"
wenzelm@53688
  1045
        using assm and False `b\<in>s` by auto
wenzelm@53688
  1046
      ultimately show ?thesis
wenzelm@53688
  1047
        by auto
wenzelm@53185
  1048
    qed
wenzelm@53688
  1049
  qed (insert a(2) b(2) assm, auto)
wenzelm@53185
  1050
qed
hoelzl@33741
  1051
hoelzl@33741
  1052
lemma ksimplex_extrema_strong:
wenzelm@53688
  1053
  assumes "ksimplex p n s"
wenzelm@53688
  1054
    and "n \<noteq> 0"
wenzelm@53688
  1055
  obtains a b where "a \<in> s"
wenzelm@53688
  1056
    and "b \<in> s"
wenzelm@53688
  1057
    and "a \<noteq> b"
wenzelm@53688
  1058
    and "\<forall>x\<in>s. kle n a x \<and> kle n x b"
wenzelm@53688
  1059
    and "\<forall>i. b i = (if i \<in> {1..n} then a(i) + 1 else a i)"
wenzelm@53185
  1060
proof -
wenzelm@53185
  1061
  obtain a b where ab: "a \<in> s" "b \<in> s"
wenzelm@53185
  1062
    "\<forall>x\<in>s. kle n a x \<and> kle n x b" "\<forall>i. b(i) = (if i \<in> {1..n} then a(i) + 1 else a(i))"
wenzelm@53185
  1063
    apply (rule ksimplex_extrema[OF assms(1)])
wenzelm@53185
  1064
    apply auto
wenzelm@53185
  1065
    done
wenzelm@53185
  1066
  have "a \<noteq> b"
wenzelm@53185
  1067
    apply (rule notI)
wenzelm@53185
  1068
    apply (drule cong[of _ _ 1 1])
wenzelm@53688
  1069
    using ab(4) assms(2)
wenzelm@53688
  1070
    apply auto
wenzelm@53185
  1071
    done
wenzelm@53674
  1072
  then show ?thesis
wenzelm@53185
  1073
    apply (rule_tac that[of a b])
wenzelm@53688
  1074
    using ab
wenzelm@53688
  1075
    apply auto
wenzelm@53185
  1076
    done
wenzelm@53185
  1077
qed
hoelzl@33741
  1078
hoelzl@33741
  1079
lemma ksimplexD:
hoelzl@33741
  1080
  assumes "ksimplex p n s"
wenzelm@53688
  1081
  shows "card s = n + 1"
wenzelm@53688
  1082
    and "finite s"
wenzelm@53688
  1083
    and "card s = n + 1"
wenzelm@53688
  1084
    and "\<forall>x\<in>s. \<forall>j. x j \<le> p"
wenzelm@53688
  1085
    and "\<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
wenzelm@53688
  1086
    and "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
wenzelm@53185
  1087
  using assms unfolding ksimplex_eq by auto
hoelzl@33741
  1088
hoelzl@33741
  1089
lemma ksimplex_successor:
wenzelm@53688
  1090
  assumes "ksimplex p n s"
wenzelm@53688
  1091
    and "a \<in> s"
wenzelm@53688
  1092
  shows "(\<forall>x\<in>s. kle n x a) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a j + 1 else a j))"
wenzelm@53185
  1093
proof (cases "\<forall>x\<in>s. kle n x a")
wenzelm@53185
  1094
  case True
wenzelm@53674
  1095
  then show ?thesis by auto
wenzelm@53185
  1096
next
wenzelm@53185
  1097
  note assm = ksimplexD[OF assms(1)]
wenzelm@53185
  1098
  case False
wenzelm@53688
  1099
  then obtain b where b: "b \<in> s" "\<not> kle n b a" "\<forall>x\<in>{x \<in> s. \<not> kle n x a}. kle n b x"
wenzelm@53688
  1100
    using kle_minimal[of "{x\<in>s. \<not> kle n x a}" n] and assm
wenzelm@53688
  1101
    by auto
wenzelm@53252
  1102
  then have **: "1 \<le> card {k\<in>{1..n}. a k < b k}"
wenzelm@53185
  1103
    apply -
wenzelm@53185
  1104
    apply (rule kle_strict_set)
wenzelm@53252
  1105
    using assm(6) and `a\<in>s`
wenzelm@53688
  1106
    apply (auto simp add: kle_refl)
wenzelm@53185
  1107
    done
hoelzl@33741
  1108
wenzelm@53185
  1109
  let ?kle1 = "{x \<in> s. \<not> kle n x a}"
wenzelm@53185
  1110
  have "card ?kle1 > 0"
wenzelm@53185
  1111
    apply (rule ccontr)
wenzelm@53252
  1112
    using assm(2) and False
wenzelm@53252
  1113
    apply auto
wenzelm@53185
  1114
    done
wenzelm@53674
  1115
  then have sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)"
wenzelm@53185
  1116
    using assm(2) by auto
wenzelm@53185
  1117
  obtain c d where c_d: "c \<in> s" "\<not> kle n c a" "d \<in> s" "\<not> kle n d a"
wenzelm@53185
  1118
    "kle n c d" "card ?kle1 - 1 \<le> card {k \<in> {1..n}. c k < d k}"
hoelzl@33741
  1119
    using kle_range_induct[OF sizekle1, of n] using assm by auto
hoelzl@33741
  1120
hoelzl@33741
  1121
  let ?kle2 = "{x \<in> s. kle n x a}"
wenzelm@53185
  1122
  have "card ?kle2 > 0"
wenzelm@53185
  1123
    apply (rule ccontr)
wenzelm@53252
  1124
    using assm(6)[rule_format,of a a] and `a\<in>s` and assm(2)
wenzelm@53252
  1125
    apply auto
wenzelm@53185
  1126
    done
wenzelm@53674
  1127
  then have sizekle2: "card ?kle2 = Suc (card ?kle2 - 1)"
wenzelm@53185
  1128
    using assm(2) by auto
wenzelm@53185
  1129
  obtain e f where e_f: "e \<in> s" "kle n e a" "f \<in> s" "kle n f a"
wenzelm@53185
  1130
    "kle n e f" "card ?kle2 - 1 \<le> card {k \<in> {1..n}. e k < f k}"
wenzelm@53688
  1131
    using kle_range_induct[OF sizekle2, of n]
wenzelm@53688
  1132
    using assm
wenzelm@53688
  1133
    by auto
hoelzl@33741
  1134
wenzelm@53185
  1135
  have "card {k\<in>{1..n}. a k < b k} = 1"
wenzelm@53185
  1136
  proof (rule ccontr)
wenzelm@53688
  1137
    assume "\<not> ?thesis"
wenzelm@53674
  1138
    then have as: "card {k\<in>{1..n}. a k < b k} \<ge> 2"
wenzelm@53185
  1139
      using ** by auto
wenzelm@53185
  1140
    have *: "finite ?kle2" "finite ?kle1" "?kle2 \<union> ?kle1 = s" "?kle2 \<inter> ?kle1 = {}"
wenzelm@53185
  1141
      using assm(2) by auto
wenzelm@53185
  1142
    have "(card ?kle2 - 1) + 2 + (card ?kle1 - 1) = card ?kle2 + card ?kle1"
wenzelm@53185
  1143
      using sizekle1 sizekle2 by auto
wenzelm@53185
  1144
    also have "\<dots> = n + 1"
wenzelm@53688
  1145
      unfolding card_Un_Int[OF *(1-2)] *(3-)
wenzelm@53688
  1146
      using assm(3)
wenzelm@53688
  1147
      by auto
wenzelm@53185
  1148
    finally have n: "(card ?kle2 - 1) + (2 + (card ?kle1 - 1)) = n + 1"
wenzelm@53185
  1149
      by auto
hoelzl@33741
  1150
    have "kle n e a \<and> card {x \<in> s. kle n x a} - 1 \<le> card {k \<in> {1..n}. e k < a k}"
wenzelm@53185
  1151
      apply (rule kle_range_combine_r[where y=f])
wenzelm@53688
  1152
      using e_f using `a \<in> s` assm(6)
wenzelm@53252
  1153
      apply auto
wenzelm@53185
  1154
      done
hoelzl@33741
  1155
    moreover have "kle n b d \<and> card {x \<in> s. \<not> kle n x a} - 1 \<le> card {k \<in> {1..n}. b k < d k}"
wenzelm@53185
  1156
      apply (rule kle_range_combine_l[where y=c])
wenzelm@53252
  1157
      using c_d using assm(6) and b
wenzelm@53252
  1158
      apply auto
wenzelm@53185
  1159
      done
wenzelm@53674
  1160
    then have "kle n a d \<and> 2 + (card {x \<in> s. \<not> kle n x a} - 1) \<le> card {k \<in> {1..n}. a k < d k}"
wenzelm@53185
  1161
      apply -
wenzelm@53688
  1162
      apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a \<in> s` `d \<in> s`
wenzelm@53185
  1163
      apply blast+
wenzelm@53185
  1164
      done
wenzelm@53185
  1165
    ultimately
wenzelm@53185
  1166
    have "kle n e d \<and> (card ?kle2 - 1) + (2 + (card ?kle1 - 1)) \<le> card {k\<in>{1..n}. e k < d k}"
wenzelm@53185
  1167
      apply -
wenzelm@53688
  1168
      apply (rule kle_range_combine[where y=a]) using assm(6)[rule_format, OF `e \<in> s` `d \<in> s`]
wenzelm@53185
  1169
      apply blast+
wenzelm@53185
  1170
      done
wenzelm@53185
  1171
    moreover have "card {k \<in> {1..n}. e k < d k} \<le> card {1..n}"
wenzelm@53185
  1172
      by (rule card_mono) auto
wenzelm@53688
  1173
    ultimately show False
wenzelm@53688
  1174
      unfolding n by auto
wenzelm@53185
  1175
  qed
wenzelm@55493
  1176
  then obtain k where k:
wenzelm@55493
  1177
      "k \<in> {1..n} \<and> a k < b k"
wenzelm@55493
  1178
      "\<And>y y'. (y \<in> {1..n} \<and> a y < b y) \<and> y' \<in> {1..n} \<and> a y' < b y' \<Longrightarrow> y = y'"
wenzelm@55493
  1179
    unfolding card_1_exists by blast
hoelzl@33741
  1180
wenzelm@53185
  1181
  show ?thesis
wenzelm@53185
  1182
    apply (rule disjI2)
wenzelm@53688
  1183
    apply (rule_tac x=b in bexI)
wenzelm@53688
  1184
    apply (rule_tac x=k in bexI)
wenzelm@53185
  1185
  proof
wenzelm@53185
  1186
    fix j :: nat
wenzelm@53185
  1187
    have "kle n a b"
wenzelm@53688
  1188
      using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`]
wenzelm@53688
  1189
      by auto
wenzelm@55493
  1190
    then obtain kk where kk: "kk \<subseteq> {1..n}" "\<And>j. b j = a j + (if j \<in> kk then 1 else 0)"
wenzelm@55493
  1191
      unfolding kle_def by blast
wenzelm@53185
  1192
    have kkk: "k \<in> kk"
wenzelm@53185
  1193
      apply (rule ccontr)
wenzelm@53185
  1194
      using k(1)
wenzelm@55493
  1195
      unfolding kk(2)
wenzelm@53252
  1196
      apply auto
wenzelm@53185
  1197
      done
wenzelm@53185
  1198
    show "b j = (if j = k then a j + 1 else a j)"
wenzelm@53185
  1199
    proof (cases "j \<in> kk")
wenzelm@53185
  1200
      case True
wenzelm@53252
  1201
      then have "j = k"
wenzelm@53252
  1202
        apply -
wenzelm@55493
  1203
        apply (rule k(2))
wenzelm@55493
  1204
        using kk kkk
wenzelm@53252
  1205
        apply auto
wenzelm@53252
  1206
        done
wenzelm@53688
  1207
      then show ?thesis
wenzelm@55493
  1208
        unfolding kk(2) using kkk by auto
wenzelm@53185
  1209
    next
wenzelm@53185
  1210
      case False
wenzelm@53252
  1211
      then have "j \<noteq> k"
wenzelm@55493
  1212
        using k(2)[of j k] and kkk
wenzelm@53688
  1213
        by auto
wenzelm@53688
  1214
      then show ?thesis
wenzelm@55493
  1215
        unfolding kk(2)
wenzelm@53688
  1216
        using kkk and False
wenzelm@53185
  1217
        by auto
wenzelm@53185
  1218
    qed
wenzelm@53688
  1219
  qed (insert k(1) `b \<in> s`, auto)
wenzelm@53185
  1220
qed
hoelzl@33741
  1221
hoelzl@33741
  1222
lemma ksimplex_predecessor:
wenzelm@53688
  1223
  assumes "ksimplex p n s"
wenzelm@53688
  1224
    and "a \<in> s"
wenzelm@53688
  1225
  shows "(\<forall>x\<in>s. kle n a x) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a j = (if j = k then y j + 1 else y j))"
wenzelm@53185
  1226
proof (cases "\<forall>x\<in>s. kle n a x")
wenzelm@53185
  1227
  case True
wenzelm@53674
  1228
  then show ?thesis by auto
wenzelm@53185
  1229
next
wenzelm@53185
  1230
  note assm = ksimplexD[OF assms(1)]
wenzelm@53185
  1231
  case False
wenzelm@53688
  1232
  then obtain b where b: "b \<in> s" "\<not> kle n a b" "\<forall>x\<in>{x \<in> s. \<not> kle n a x}. kle n x b"
wenzelm@53688
  1233
    using kle_maximal[of "{x\<in>s. \<not> kle n a x}" n] and assm
wenzelm@53688
  1234
    by auto
wenzelm@53674
  1235
  then have **: "1 \<le> card {k\<in>{1..n}. a k > b k}"
wenzelm@53185
  1236
    apply -
wenzelm@53185
  1237
    apply (rule kle_strict_set)
wenzelm@53688
  1238
    using assm(6) and `a \<in> s`
wenzelm@53252
  1239
    apply (auto simp add: kle_refl)
wenzelm@53185
  1240
    done
hoelzl@33741
  1241
wenzelm@53185
  1242
  let ?kle1 = "{x \<in> s. \<not> kle n a x}"
wenzelm@53185
  1243
  have "card ?kle1 > 0"
wenzelm@53185
  1244
    apply (rule ccontr)
wenzelm@53252
  1245
    using assm(2) and False
wenzelm@53252
  1246
    apply auto
wenzelm@53185
  1247
    done
wenzelm@53674
  1248
  then have sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)"
wenzelm@53185
  1249
    using assm(2) by auto
wenzelm@53185
  1250
  obtain c d where c_d: "c \<in> s" "\<not> kle n a c" "d \<in> s" "\<not> kle n a d"
wenzelm@53185
  1251
    "kle n d c" "card ?kle1 - 1 \<le> card {k \<in> {1..n}. c k > d k}"
wenzelm@53688
  1252
    using kle_range_induct[OF sizekle1, of n]
wenzelm@53688
  1253
    using assm
wenzelm@53688
  1254
    by auto
hoelzl@33741
  1255
hoelzl@33741
  1256
  let ?kle2 = "{x \<in> s. kle n a x}"
wenzelm@53185
  1257
  have "card ?kle2 > 0"
wenzelm@53185
  1258
    apply (rule ccontr)
wenzelm@53688
  1259
    using assm(6)[rule_format,of a a] and `a \<in> s` and assm(2)
wenzelm@53252
  1260
    apply auto
wenzelm@53185
  1261
    done
wenzelm@53688
  1262
  then have sizekle2: "card ?kle2 = Suc (card ?kle2 - 1)"
wenzelm@53688
  1263
    using assm(2)
wenzelm@53688
  1264
    by auto
wenzelm@53185
  1265
  obtain e f where e_f: "e \<in> s" "kle n a e" "f \<in> s" "kle n a f"
wenzelm@53185
  1266
    "kle n f e" "card ?kle2 - 1 \<le> card {k \<in> {1..n}. e k > f k}"
wenzelm@53688
  1267
    using kle_range_induct[OF sizekle2, of n]
wenzelm@53688
  1268
    using assm
wenzelm@53688
  1269
    by auto
hoelzl@33741
  1270
wenzelm@53185
  1271
  have "card {k\<in>{1..n}. a k > b k} = 1"
wenzelm@53185
  1272
  proof (rule ccontr)
wenzelm@53688
  1273
    assume "\<not> ?thesis"
wenzelm@53674
  1274
    then have as: "card {k\<in>{1..n}. a k > b k} \<ge> 2"
wenzelm@53185
  1275
      using ** by auto
wenzelm@53185
  1276
    have *: "finite ?kle2" "finite ?kle1" "?kle2 \<union> ?kle1 = s" "?kle2 \<inter> ?kle1 = {}"
wenzelm@53185
  1277
      using assm(2) by auto
wenzelm@53185
  1278
    have "(card ?kle2 - 1) + 2 + (card ?kle1 - 1) = card ?kle2 + card ?kle1"
wenzelm@53185
  1279
      using sizekle1 sizekle2 by auto
wenzelm@53185
  1280
    also have "\<dots> = n + 1"
wenzelm@53688
  1281
      unfolding card_Un_Int[OF *(1-2)] *(3-)
wenzelm@53688
  1282
      using assm(3) by auto
wenzelm@53185
  1283
    finally have n: "(card ?kle1 - 1) + 2 + (card ?kle2 - 1) = n + 1"
wenzelm@53185
  1284
      by auto
hoelzl@33741
  1285
    have "kle n a e \<and> card {x \<in> s. kle n a x} - 1 \<le> card {k \<in> {1..n}. e k > a k}"
wenzelm@53185
  1286
      apply (rule kle_range_combine_l[where y=f])
wenzelm@53252
  1287
      using e_f and `a\<in>s` assm(6)
wenzelm@53252
  1288
      apply auto
wenzelm@53185
  1289
      done
hoelzl@33741
  1290
    moreover have "kle n d b \<and> card {x \<in> s. \<not> kle n a x} - 1 \<le> card {k \<in> {1..n}. b k > d k}"
wenzelm@53185
  1291
      apply (rule kle_range_combine_r[where y=c])
wenzelm@53252
  1292
      using c_d and assm(6) and b
wenzelm@53252
  1293
      apply auto
wenzelm@53185
  1294
      done
wenzelm@53674
  1295
    then have "kle n d a \<and> (card {x \<in> s. \<not> kle n a x} - 1) + 2 \<le> card {k \<in> {1..n}. a k > d k}"
wenzelm@53185
  1296
      apply -
wenzelm@53688
  1297
      apply (rule kle_range_combine[where y=b]) using as and b assm(6) `a \<in> s` `d \<in> s`
wenzelm@53185
  1298
      apply blast+
wenzelm@53185
  1299
      done
wenzelm@53185
  1300
    ultimately have "kle n d e \<and> (card ?kle1 - 1 + 2) + (card ?kle2 - 1) \<le> card {k\<in>{1..n}. e k > d k}"
wenzelm@53185
  1301
      apply -
wenzelm@53185
  1302
      apply (rule kle_range_combine[where y=a])
wenzelm@53252
  1303
      using assm(6)[rule_format,OF `e\<in>s` `d\<in>s`]
wenzelm@53252
  1304
      apply blast+
wenzelm@53185
  1305
      done
wenzelm@53185
  1306
    moreover have "card {k \<in> {1..n}. e k > d k} \<le> card {1..n}"
wenzelm@53185
  1307
      by (rule card_mono) auto
wenzelm@53688
  1308
    ultimately show False
wenzelm@53688
  1309
      unfolding n by auto
wenzelm@53185
  1310
  qed
wenzelm@55493
  1311
  then obtain k where k:
wenzelm@55493
  1312
    "k \<in> {1..n} \<and> b k < a k"
wenzelm@55493
  1313
    "\<And>y y'. (y \<in> {1..n} \<and> b y < a y) \<and> y' \<in> {1..n} \<and> b y' < a y' \<Longrightarrow> y = y'"
wenzelm@55493
  1314
    unfolding card_1_exists by blast
hoelzl@33741
  1315
wenzelm@53185
  1316
  show ?thesis
wenzelm@53185
  1317
    apply (rule disjI2)
wenzelm@53688
  1318
    apply (rule_tac x=b in bexI)
wenzelm@53688
  1319
    apply (rule_tac x=k in bexI)
wenzelm@53185
  1320
  proof
wenzelm@53185
  1321
    fix j :: nat
wenzelm@53185
  1322
    have "kle n b a"
wenzelm@53185
  1323
      using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`] by auto
wenzelm@55493
  1324
    then obtain kk where kk: "kk \<subseteq> {1..n}" "\<And>j. a j = b j + (if j \<in> kk then 1 else 0)"
wenzelm@55493
  1325
      unfolding kle_def by blast
wenzelm@53185
  1326
    have kkk: "k \<in> kk"
wenzelm@53185
  1327
      apply (rule ccontr)
wenzelm@53185
  1328
      using k(1)
wenzelm@55493
  1329
      unfolding kk(2)
wenzelm@53185
  1330
      apply auto
wenzelm@53185
  1331
      done
wenzelm@53185
  1332
    show "a j = (if j = k then b j + 1 else b j)"
wenzelm@53185
  1333
    proof (cases "j \<in> kk")
wenzelm@53185
  1334
      case True
wenzelm@53674
  1335
      then have "j = k"
wenzelm@53185
  1336
        apply -
wenzelm@55493
  1337
        apply (rule k(2))
wenzelm@55493
  1338
        using kk kkk
wenzelm@53252
  1339
        apply auto
wenzelm@53185
  1340
        done
wenzelm@53688
  1341
      then show ?thesis
wenzelm@55493
  1342
        unfolding kk(2) using kkk by auto
wenzelm@53185
  1343
    next
wenzelm@53185
  1344
      case False
wenzelm@53688
  1345
      then have "j \<noteq> k"
wenzelm@55493
  1346
        using k(2)[of j k]
wenzelm@55493
  1347
        using kkk
wenzelm@53688
  1348
        by auto
wenzelm@53688
  1349
      then show ?thesis
wenzelm@55493
  1350
        unfolding kk(2)
wenzelm@53688
  1351
        using kkk and False
wenzelm@53688
  1352
        by auto
wenzelm@53185
  1353
    qed
wenzelm@53186
  1354
  qed (insert k(1) `b\<in>s`, auto)
wenzelm@53185
  1355
qed
wenzelm@53185
  1356
hoelzl@33741
  1357
hoelzl@33741
  1358
subsection {* The lemmas about simplices that we need. *}
hoelzl@33741
  1359
wenzelm@53185
  1360
(* FIXME: These are clones of lemmas in Library/FuncSet *)
wenzelm@53185
  1361
lemma card_funspace':
wenzelm@53688
  1362
  assumes "finite s"
wenzelm@53688
  1363
    and "finite t"
wenzelm@53688
  1364
    and "card s = m"
wenzelm@53688
  1365
    and "card t = n"
wenzelm@53688
  1366
  shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = n ^ m"
wenzelm@53688
  1367
    (is "card (?M s) = _")
wenzelm@53185
  1368
  using assms
wenzelm@53185
  1369
proof (induct m arbitrary: s)
wenzelm@53252
  1370
  case 0
wenzelm@53252
  1371
  have [simp]: "{f. \<forall>x. f x = d} = {\<lambda>x. d}"
wenzelm@53688
  1372
    apply (rule set_eqI)
wenzelm@53688
  1373
    apply rule
wenzelm@53185
  1374
    unfolding mem_Collect_eq
wenzelm@53688
  1375
    apply rule
wenzelm@53688
  1376
    apply (rule ext)
wenzelm@53185
  1377
    apply auto
wenzelm@53185
  1378
    done
wenzelm@53688
  1379
  from 0 show ?case
wenzelm@53688
  1380
    by auto
wenzelm@53185
  1381
next
wenzelm@53185
  1382
  case (Suc m)
wenzelm@55493
  1383
  obtain a s0 where as0:
wenzelm@55493
  1384
    "s = insert a s0"
wenzelm@55493
  1385
    "a \<notin> s0"
wenzelm@55493
  1386
    "card s0 = m"
wenzelm@55493
  1387
    "m = 0 \<longrightarrow> s0 = {}"
wenzelm@55493
  1388
    using card_eq_SucD[OF Suc(4)] by auto
wenzelm@53185
  1389
  have **: "card s0 = m"
wenzelm@53688
  1390
    using as0 using Suc(2) Suc(4)
wenzelm@53688
  1391
    by auto
wenzelm@53185
  1392
  let ?l = "(\<lambda>(b, g) x. if x = a then b else g x)"
wenzelm@53185
  1393
  have *: "?M (insert a s0) = ?l ` {(b,g). b\<in>t \<and> g\<in>?M s0}"
wenzelm@53185
  1394
    apply (rule set_eqI, rule)
wenzelm@53185
  1395
    unfolding mem_Collect_eq image_iff
wenzelm@53185
  1396
    apply (erule conjE)
wenzelm@53185
  1397
    apply (rule_tac x="(x a, \<lambda>y. if y\<in>s0 then x y else d)" in bexI)
wenzelm@53185
  1398
    apply (rule ext)
wenzelm@53185
  1399
    prefer 3
wenzelm@53185
  1400
    apply rule
wenzelm@53185
  1401
    defer
wenzelm@53688
  1402
    apply (erule bexE)
wenzelm@53688
  1403
    apply rule
wenzelm@53185
  1404
    unfolding mem_Collect_eq
wenzelm@53185
  1405
    apply (erule splitE)+
wenzelm@53185
  1406
    apply (erule conjE)+
wenzelm@53185
  1407
  proof -
wenzelm@53185
  1408
    fix x xa xb xc y
wenzelm@53688
  1409
    assume as:
wenzelm@53688
  1410
      "x = (\<lambda>(b, g) x. if x = a then b else g x) xa"
wenzelm@53846
  1411
      "xb \<in> UNIV - insert a s0"
wenzelm@53846
  1412
      "xa = (xc, y)"
wenzelm@53688
  1413
      "xc \<in> t"
wenzelm@53688
  1414
      "\<forall>x\<in>s0. y x \<in> t"
wenzelm@53688
  1415
      "\<forall>x\<in>UNIV - s0. y x = d"
wenzelm@53688
  1416
    then show "x xb = d"
wenzelm@53688
  1417
      unfolding as by auto
wenzelm@53185
  1418
  qed auto
wenzelm@53185
  1419
  have inj: "inj_on ?l {(b,g). b\<in>t \<and> g\<in>?M s0}"
wenzelm@53185
  1420
    unfolding inj_on_def
wenzelm@53688
  1421
    apply rule
wenzelm@53688
  1422
    apply rule
wenzelm@53688
  1423
    apply rule
wenzelm@53688
  1424
    unfolding mem_Collect_eq
wenzelm@53688
  1425
    apply (erule splitE conjE)+
wenzelm@53185
  1426
  proof -
hoelzl@33741
  1427
    case goal1 note as = this(1,4-)[unfolded goal1 split_conv]
wenzelm@53688
  1428
    have "xa = xb"
wenzelm@53688
  1429
      using as(1)[THEN cong[of _ _ a]] by auto
wenzelm@53185
  1430
    moreover have "ya = yb"
wenzelm@53185
  1431
    proof (rule ext)
wenzelm@53185
  1432
      fix x
wenzelm@53185
  1433
      show "ya x = yb x"
wenzelm@53185
  1434
      proof (cases "x = a")
wenzelm@53185
  1435
        case False
wenzelm@53688
  1436
        then show ?thesis
wenzelm@53688
  1437
          using as(1)[THEN cong[of _ _ x x]] by auto
wenzelm@53185
  1438
      next
wenzelm@53185
  1439
        case True
wenzelm@53688
  1440
        then show ?thesis
wenzelm@53688
  1441
          using as(5,7) using as0(2) by auto
wenzelm@53185
  1442
      qed
wenzelm@53185
  1443
    qed
wenzelm@53688
  1444
    ultimately show ?case
wenzelm@53688
  1445
      unfolding goal1 by auto
wenzelm@53185
  1446
  qed
wenzelm@53688
  1447
  have "finite s0"
wenzelm@53688
  1448
    using `finite s` unfolding as0 by simp
wenzelm@53185
  1449
  show ?case
wenzelm@53185
  1450
    unfolding as0 * card_image[OF inj]
wenzelm@53185
  1451
    using assms
wenzelm@53185
  1452
    unfolding SetCompr_Sigma_eq
hoelzl@33741
  1453
    unfolding card_cartesian_product
wenzelm@53185
  1454
    using Suc(1)[OF `finite s0` `finite t` ** `card t = n`]
wenzelm@53185
  1455
    by auto
hoelzl@33741
  1456
qed
hoelzl@33741
  1457
wenzelm@53185
  1458
lemma card_funspace:
wenzelm@53688
  1459
  assumes "finite s"
wenzelm@53688
  1460
    and "finite t"
wenzelm@53688
  1461
  shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = card t ^ card s"
hoelzl@33741
  1462
  using assms by (auto intro: card_funspace')
hoelzl@33741
  1463
wenzelm@53185
  1464
lemma finite_funspace:
wenzelm@53688
  1465
  assumes "finite s"
wenzelm@53688
  1466
    and "finite t"
wenzelm@53688
  1467
  shows "finite {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)}"
wenzelm@53688
  1468
    (is "finite ?S")
hoelzl@33741
  1469
proof (cases "card t > 0")
hoelzl@33741
  1470
  case True
wenzelm@53688
  1471
  have "card ?S = card t ^ card s"
hoelzl@33741
  1472
    using assms by (auto intro!: card_funspace)
wenzelm@53688
  1473
  then show ?thesis
wenzelm@53688
  1474
    using True by (rule_tac card_ge_0_finite) simp
hoelzl@33741
  1475
next
wenzelm@53688
  1476
  case False
wenzelm@53688
  1477
  then have "t = {}"
wenzelm@53688
  1478
    using `finite t` by auto
hoelzl@33741
  1479
  show ?thesis
hoelzl@33741
  1480
  proof (cases "s = {}")
wenzelm@53185
  1481
    case True
wenzelm@53688
  1482
    have *: "{f. \<forall>x. f x = d} = {\<lambda>x. d}"
wenzelm@53688
  1483
      by auto
wenzelm@53688
  1484
    from True show ?thesis
wenzelm@53688
  1485
      using `t = {}` by (auto simp: *)
hoelzl@33741
  1486
  next
wenzelm@53185
  1487
    case False
wenzelm@53688
  1488
    then show ?thesis
wenzelm@53688
  1489
      using `t = {}` by simp
hoelzl@33741
  1490
  qed
hoelzl@33741
  1491
qed
hoelzl@33741
  1492
hoelzl@33741
  1493
lemma finite_simplices: "finite {s. ksimplex p n s}"
wenzelm@53185
  1494
  apply (rule finite_subset[of _ "{s. s\<subseteq>{f. (\<forall>i\<in>{1..n}. f i \<in> {0..p}) \<and> (\<forall>i\<in>UNIV-{1..n}. f i = p)}}"])
wenzelm@53185
  1495
  unfolding ksimplex_def
wenzelm@53185
  1496
  defer
wenzelm@53185
  1497
  apply (rule finite_Collect_subsets)
wenzelm@53185
  1498
  apply (rule finite_funspace)
wenzelm@53185
  1499
  apply auto
wenzelm@53185
  1500
  done
hoelzl@33741
  1501
wenzelm@53185
  1502
lemma simplex_top_face:
wenzelm@53688
  1503
  assumes "0 < p"
wenzelm@53688
  1504
    and "\<forall>x\<in>f. x (n + 1) = p"
wenzelm@53688
  1505
  shows "(\<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s - {a})) \<longleftrightarrow> ksimplex p n f"
wenzelm@53688
  1506
    (is "?ls = ?rs")
wenzelm@53185
  1507
proof
wenzelm@53185
  1508
  assume ?ls
wenzelm@55493
  1509
  then obtain s a where sa:
wenzelm@55493
  1510
    "ksimplex p (n + 1) s"
wenzelm@55493
  1511
    "a \<in> s"
wenzelm@55493
  1512
    "f = s - {a}"
wenzelm@55493
  1513
    by auto
wenzelm@53185
  1514
  show ?rs
wenzelm@53185
  1515
    unfolding ksimplex_def sa(3)
wenzelm@53185
  1516
    apply rule
wenzelm@53185
  1517
    defer
wenzelm@53185
  1518
    apply rule
wenzelm@53185
  1519
    defer
wenzelm@53185
  1520
    apply (rule, rule, rule, rule)
wenzelm@53185
  1521
    defer
wenzelm@53185
  1522
    apply (rule, rule)
wenzelm@53185
  1523
  proof -
wenzelm@53185
  1524
    fix x y
wenzelm@53185
  1525
    assume as: "x \<in>s - {a}" "y \<in>s - {a}"
wenzelm@53185
  1526
    have xyp: "x (n + 1) = y (n + 1)"
wenzelm@53185
  1527
      using as(1)[unfolded sa(3)[symmetric], THEN assms(2)[rule_format]]
wenzelm@53185
  1528
      using as(2)[unfolded sa(3)[symmetric], THEN assms(2)[rule_format]]
wenzelm@53185
  1529
      by auto
wenzelm@53185
  1530
    show "kle n x y \<or> kle n y x"
wenzelm@53185
  1531
    proof (cases "kle (n + 1) x y")
wenzelm@53185
  1532
      case True
wenzelm@55493
  1533
      then obtain k where k: "k \<subseteq> {1..n + 1}" "\<And>j. y j = x j + (if j \<in> k then 1 else 0)"
wenzelm@55493
  1534
        unfolding kle_def by blast
wenzelm@53674
  1535
      then have *: "n + 1 \<notin> k" using xyp by auto
wenzelm@53688
  1536
      have "\<not> (\<exists>x\<in>k. x \<notin> {1..n})"
wenzelm@53252
  1537
        apply (rule notI)
wenzelm@53252
  1538
        apply (erule bexE)
wenzelm@53185
  1539
      proof -
wenzelm@53185
  1540
        fix x
wenzelm@53185
  1541
        assume as: "x \<in> k" "x \<notin> {1..n}"
wenzelm@53688
  1542
        have "x \<noteq> n + 1"
wenzelm@53688
  1543
          using as and * by auto
wenzelm@53688
  1544
        then show False
wenzelm@55493
  1545
          using as and k(1) by auto
wenzelm@53185
  1546
      qed
wenzelm@53674
  1547
      then show ?thesis
wenzelm@53185
  1548
        apply -
wenzelm@53185
  1549
        apply (rule disjI1)
wenzelm@53185
  1550
        unfolding kle_def
wenzelm@55493
  1551
        using k(2)
wenzelm@53185
  1552
        apply (rule_tac x=k in exI)
wenzelm@53185
  1553
        apply auto
wenzelm@53185
  1554
        done
wenzelm@53185
  1555
    next
wenzelm@53185
  1556
      case False
wenzelm@53674
  1557
      then have "kle (n + 1) y x"
wenzelm@53688
  1558
        using ksimplexD(6)[OF sa(1),rule_format, of x y] and as
wenzelm@53688
  1559
        by auto
wenzelm@55493
  1560
      then obtain k where k: "k \<subseteq> {1..n + 1}" "\<And>j. x j = y j + (if j \<in> k then 1 else 0)"
wenzelm@55493
  1561
        unfolding kle_def by auto
wenzelm@53688
  1562
      then have *: "n + 1 \<notin> k"
wenzelm@53688
  1563
        using xyp by auto
wenzelm@53688
  1564
      then have "\<not> (\<exists>x\<in>k. x \<notin> {1..n})"
wenzelm@53185
  1565
        apply -
wenzelm@53252
  1566
        apply (rule notI)
wenzelm@53185
  1567
        apply (erule bexE)
wenzelm@53185
  1568
      proof -
wenzelm@53185
  1569
        fix x
wenzelm@53185
  1570
        assume as: "x \<in> k" "x \<notin> {1..n}"
wenzelm@53688
  1571
        have "x \<noteq> n + 1"
wenzelm@53688
  1572
          using as and * by auto
wenzelm@53688
  1573
        then show False
wenzelm@55493
  1574
          using as and k(1)
wenzelm@53688
  1575
          by auto
wenzelm@53185
  1576
      qed
wenzelm@53252
  1577
      then show ?thesis
wenzelm@53185
  1578
        apply -
wenzelm@53185
  1579
        apply (rule disjI2)
wenzelm@53185
  1580
        unfolding kle_def
wenzelm@55493
  1581
        using k(2)
wenzelm@53252
  1582
        apply (rule_tac x = k in exI)
wenzelm@53252
  1583
        apply auto
wenzelm@53252
  1584
        done
wenzelm@53185
  1585
    qed
wenzelm@53185
  1586
  next
wenzelm@53185
  1587
    fix x j
wenzelm@53688
  1588
    assume as: "x \<in> s - {a}" "j \<notin> {1..n}"
wenzelm@53674
  1589
    then show "x j = p"
wenzelm@53185
  1590
      using as(1)[unfolded sa(3)[symmetric], THEN assms(2)[rule_format]]
wenzelm@53688
  1591
      apply (cases "j = n + 1")
wenzelm@53185
  1592
      using sa(1)[unfolded ksimplex_def]
wenzelm@53185
  1593
      apply auto
wenzelm@53185
  1594
      done
wenzelm@53185
  1595
  qed (insert sa ksimplexD[OF sa(1)], auto)
wenzelm@53185
  1596
next
wenzelm@53185
  1597
  assume ?rs note rs=ksimplexD[OF this]
wenzelm@55493
  1598
  obtain a b where ab:
wenzelm@55493
  1599
    "a \<in> f"
wenzelm@55493
  1600
    "b \<in> f"
wenzelm@55493
  1601
    "\<forall>x\<in>f. kle n a x \<and> kle n x b"
wenzelm@55493
  1602
    "\<forall>i. b i = (if i \<in> {1..n} then a i + 1 else a i)"
wenzelm@55493
  1603
    by (rule ksimplex_extrema[OF `?rs`])
hoelzl@33741
  1604
  def c \<equiv> "\<lambda>i. if i = (n + 1) then p - 1 else a i"
wenzelm@53185
  1605
  have "c \<notin> f"
wenzelm@53252
  1606
    apply (rule notI)
wenzelm@53185
  1607
    apply (drule assms(2)[rule_format])
wenzelm@53185
  1608
    unfolding c_def
wenzelm@53252
  1609
    using assms(1)
wenzelm@53252
  1610
    apply auto
wenzelm@53185
  1611
    done
wenzelm@53674
  1612
  then show ?ls
wenzelm@53688
  1613
    apply (rule_tac x = "insert c f" in exI)
wenzelm@53688
  1614
    apply (rule_tac x = c in exI)
wenzelm@53185
  1615
    unfolding ksimplex_def conj_assoc
wenzelm@53185
  1616
    apply (rule conjI)
wenzelm@53185
  1617
    defer
wenzelm@53185
  1618
    apply (rule conjI)
wenzelm@53185
  1619
    defer
wenzelm@53185
  1620
    apply (rule conjI)
wenzelm@53185
  1621
    defer
wenzelm@53185
  1622
    apply (rule conjI)
wenzelm@53185
  1623
    defer
wenzelm@53185
  1624
  proof (rule_tac[3-5] ballI allI)+
wenzelm@53185
  1625
    fix x j
wenzelm@53185
  1626
    assume x: "x \<in> insert c f"
wenzelm@53674
  1627
    then show "x j \<le> p"
wenzelm@53688
  1628
    proof (cases "x = c")
wenzelm@53185
  1629
      case True
wenzelm@53185
  1630
      show ?thesis
wenzelm@53185
  1631
        unfolding True c_def
wenzelm@53688
  1632
        apply (cases "j = n + 1")
wenzelm@53252
  1633
        using ab(1) and rs(4)
wenzelm@53252
  1634
        apply auto
wenzelm@53185
  1635
        done
wenzelm@53688
  1636
    next
wenzelm@53688
  1637
      case False
wenzelm@53688
  1638
      with insert x rs(4) show ?thesis
wenzelm@53688
  1639
        by (auto simp add: c_def)
wenzelm@53688
  1640
    qed
wenzelm@53185
  1641
    show "j \<notin> {1..n + 1} \<longrightarrow> x j = p"
wenzelm@53185
  1642
      apply (cases "x = c")
wenzelm@53252
  1643
      using x ab(1) rs(5)
wenzelm@53252
  1644
      unfolding c_def
wenzelm@53252
  1645
      apply auto
wenzelm@53252
  1646
      done
wenzelm@53185
  1647
    {
wenzelm@53185
  1648
      fix z
wenzelm@53185
  1649
      assume z: "z \<in> insert c f"
wenzelm@53674
  1650
      then have "kle (n + 1) c z"
wenzelm@53688
  1651
      proof (cases "z = c")
wenzelm@53185
  1652
        case False
wenzelm@53688
  1653
        then have "z \<in> f"
wenzelm@53688
  1654
          using z by auto
wenzelm@55493
  1655
        with ab(3) have "kle n a z" by blast
wenzelm@55493
  1656
        then obtain k where "k \<subseteq> {1..n}" "\<And>j. z j = a j + (if j \<in> k then 1 else 0)"
wenzelm@55493
  1657
          unfolding kle_def by blast
wenzelm@53674
  1658
        then show "kle (n + 1) c z"
wenzelm@53185
  1659
          unfolding kle_def
wenzelm@53185
  1660
          apply (rule_tac x="insert (n + 1) k" in exI)
wenzelm@53185
  1661
          unfolding c_def
wenzelm@53185
  1662
          using ab
wenzelm@53185
  1663
          using rs(5)[rule_format,OF ab(1),of "n + 1"] assms(1)
wenzelm@53185
  1664
          apply auto
wenzelm@53185
  1665
          done
wenzelm@53688
  1666
      next
wenzelm@53688
  1667
        case True
wenzelm@53688
  1668
        then show ?thesis by auto
wenzelm@53688
  1669
      qed
wenzelm@53185
  1670
    } note * = this
wenzelm@53185
  1671
    fix y
wenzelm@53185
  1672
    assume y: "y \<in> insert c f"
wenzelm@53185
  1673
    show "kle (n + 1) x y \<or> kle (n + 1) y x"
wenzelm@53185
  1674
    proof (cases "x = c \<or> y = c")
wenzelm@53688
  1675
      case False
wenzelm@53688
  1676
      then have **: "x \<in> f" "y \<in> f"
wenzelm@53688
  1677
        using x y by auto
wenzelm@53688
  1678
      show ?thesis
wenzelm@53688
  1679
        using rs(6)[rule_format,OF **]
wenzelm@53252
  1680
        by (auto dest: kle_Suc)
wenzelm@53185
  1681
    qed (insert * x y, auto)
wenzelm@53185
  1682
  qed (insert rs, auto)
wenzelm@53185
  1683
qed
hoelzl@33741
  1684
hoelzl@33741
  1685
lemma ksimplex_fix_plane:
wenzelm@53688
  1686
  fixes a a0 a1 :: "nat \<Rightarrow> nat"
wenzelm@53688
  1687
  assumes "a \<in> s"
wenzelm@53688
  1688
    and "j \<in> {1..n}"
wenzelm@53688
  1689
    and "\<forall>x\<in>s - {a}. x j = q"
wenzelm@53688
  1690
    and "a0 \<in> s"
wenzelm@53688
  1691
    and "a1 \<in> s"
wenzelm@53688
  1692
    and "\<forall>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
wenzelm@53688
  1693
  shows "a = a0 \<or> a = a1"
wenzelm@53185
  1694
proof -
wenzelm@53185
  1695
  have *: "\<And>P A x y. \<forall>x\<in>A. P x \<Longrightarrow> x\<in>A \<Longrightarrow> y\<in>A \<Longrightarrow> P x \<and> P y"
wenzelm@53185
  1696
    by auto
wenzelm@53185
  1697
  show ?thesis
wenzelm@53185
  1698
    apply (rule ccontr)
wenzelm@53185
  1699
    using *[OF assms(3), of a0 a1]
wenzelm@53185
  1700
    unfolding assms(6)[THEN spec[where x=j]]
wenzelm@53252
  1701
    using assms(1-2,4-5)
wenzelm@53252
  1702
    apply auto
wenzelm@53252
  1703
    done
wenzelm@53185
  1704
qed
hoelzl@33741
  1705
hoelzl@33741
  1706
lemma ksimplex_fix_plane_0:
wenzelm@53688
  1707
  fixes a a0 a1 :: "nat \<Rightarrow> nat"
wenzelm@53688
  1708
  assumes "a \<in> s"
wenzelm@53688
  1709
    and "j \<in> {1..n}"
wenzelm@53688
  1710
    and "\<forall>x\<in>s - {a}. x j = 0"
wenzelm@53688
  1711
    and "a0 \<in> s"
wenzelm@53688
  1712
    and "a1 \<in> s"
wenzelm@53688
  1713
    and "\<forall>i. a1 i = (if i\<in>{1..n} then a0 i + 1 else a0 i)"
wenzelm@53185
  1714
  shows "a = a1"
wenzelm@53185
  1715
    apply (rule ccontr)
wenzelm@53185
  1716
    using ksimplex_fix_plane[OF assms]
wenzelm@53185
  1717
    using assms(3)[THEN bspec[where x=a1]]
wenzelm@53185
  1718
    using assms(2,5)
wenzelm@53185
  1719
    unfolding assms(6)[THEN spec[where x=j]]
wenzelm@53185
  1720
    apply simp
wenzelm@53185
  1721
    done
hoelzl@33741
  1722
hoelzl@33741
  1723
lemma ksimplex_fix_plane_p:
wenzelm@53688
  1724
  assumes "ksimplex p n s"
wenzelm@53688
  1725
    and "a \<in> s"
wenzelm@53688
  1726
    and "j \<in> {1..n}"
wenzelm@53688
  1727
    and "\<forall>x\<in>s - {a}. x j = p"
wenzelm@53688
  1728
    and "a0 \<in> s"
wenzelm@53688
  1729
    and "a1 \<in> s"
wenzelm@53688
  1730
    and "\<forall>i. a1 i = (if i\<in>{1..n} then a0 i + 1 else a0 i)"
wenzelm@53185
  1731
  shows "a = a0"
wenzelm@53185
  1732
proof (rule ccontr)
wenzelm@53185
  1733
  note s = ksimplexD[OF assms(1),rule_format]
wenzelm@53688
  1734
  assume as: "\<not> ?thesis"
wenzelm@53252
  1735
  then have *: "a0 \<in> s - {a}"
wenzelm@53185
  1736
    using assms(5) by auto
wenzelm@53252
  1737
  then have "a1 = a"
wenzelm@53185
  1738
    using ksimplex_fix_plane[OF assms(2-)] by auto
wenzelm@53252
  1739
  then show False
wenzelm@53185
  1740
    using as and assms(3,5) and assms(7)[rule_format,of j]
wenzelm@53185
  1741
    unfolding assms(4)[rule_format,OF *]
wenzelm@53185
  1742
    using s(4)[OF assms(6), of j]
wenzelm@53185
  1743
    by auto
wenzelm@53185
  1744
qed
hoelzl@33741
  1745
hoelzl@33741
  1746
lemma ksimplex_replace_0:
wenzelm@53688
  1747
  assumes "ksimplex p n s" "a \<in> s"
wenzelm@53688
  1748
    and "n \<noteq> 0"
wenzelm@53688
  1749
    and "j \<in> {1..n}"
wenzelm@53688
  1750
    and "\<forall>x\<in>s - {a}. x j = 0"
wenzelm@53185
  1751
  shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
wenzelm@53185
  1752
proof -
wenzelm@53688
  1753
  have *: "\<And>s' a a'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s"
wenzelm@53185
  1754
    by auto
wenzelm@53185
  1755
  have **: "\<And>s' a'. ksimplex p n s' \<Longrightarrow> a' \<in> s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s"
wenzelm@53185
  1756
  proof -
wenzelm@53185
  1757
    case goal1
wenzelm@55522
  1758
    obtain a0 a1 where exta:
wenzelm@55522
  1759
        "a0 \<in> s"
wenzelm@55522
  1760
        "a1 \<in> s"
wenzelm@55522
  1761
        "a0 \<noteq> a1"
wenzelm@55522
  1762
        "\<And>x. x \<in> s \<Longrightarrow> kle n a0 x \<and> kle n x a1"
wenzelm@55522
  1763
        "\<And>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
wenzelm@55522
  1764
      by (rule ksimplex_extrema_strong[OF assms(1,3)]) blast
wenzelm@53688
  1765
    have a: "a = a1"
wenzelm@53185
  1766
      apply (rule ksimplex_fix_plane_0[OF assms(2,4-5)])
wenzelm@53252
  1767
      using exta(1-2,5)
wenzelm@53252
  1768
      apply auto
wenzelm@53185
  1769
      done
wenzelm@53185
  1770
    moreover
wenzelm@55522
  1771
    obtain b0 b1 where extb:
wenzelm@55522
  1772
        "b0 \<in> s'"
wenzelm@55522
  1773
        "b1 \<in> s'"
wenzelm@55522
  1774
        "b0 \<noteq> b1"
wenzelm@55522
  1775
        "\<And>x. x \<in> s' \<Longrightarrow> kle n b0 x \<and> kle n x b1"
wenzelm@55522
  1776
        "\<And>i. b1 i = (if i \<in> {1..n} then b0 i + 1 else b0 i)"
wenzelm@55522
  1777
      by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)]) blast
wenzelm@53185
  1778
    have a': "a' = b1"
wenzelm@53185
  1779
      apply (rule ksimplex_fix_plane_0[OF goal1(2) assms(4), of b0])
wenzelm@53185
  1780
      unfolding goal1(3)
wenzelm@53252
  1781
      using assms extb goal1
wenzelm@53252
  1782
      apply auto
wenzelm@53252
  1783
      done
wenzelm@53185
  1784
    moreover
wenzelm@53185
  1785
    have "b0 = a0"
wenzelm@53185
  1786
      unfolding kle_antisym[symmetric, of b0 a0 n]
wenzelm@53185
  1787
      using exta extb and goal1(3)
wenzelm@53185
  1788
      unfolding a a' by blast
wenzelm@53674
  1789
    then have "b1 = a1"
wenzelm@53185
  1790
      apply -
wenzelm@53185
  1791
      apply (rule ext)
wenzelm@53185
  1792
      unfolding exta(5) extb(5)
wenzelm@53185
  1793
      apply auto
wenzelm@53185
  1794
      done
wenzelm@53185
  1795
    ultimately
wenzelm@53185
  1796
    show "s' = s"
wenzelm@53185
  1797
      apply -
wenzelm@53185
  1798
      apply (rule *[of _ a1 b1])
wenzelm@53252
  1799
      using exta(1-2) extb(1-2) goal1
wenzelm@53252
  1800
      apply auto
wenzelm@53185
  1801
      done
wenzelm@53185
  1802
  qed
wenzelm@53185
  1803
  show ?thesis
wenzelm@53185
  1804
    unfolding card_1_exists
wenzelm@53185
  1805
    apply -
wenzelm@53185
  1806
    apply(rule ex1I[of _ s])
wenzelm@53185
  1807
    unfolding mem_Collect_eq
wenzelm@53185
  1808
    defer
wenzelm@53185
  1809
    apply (erule conjE bexE)+
wenzelm@53185
  1810
    apply (rule_tac a'=b in **)
wenzelm@53252
  1811
    using assms(1,2)
wenzelm@53252
  1812
    apply auto
wenzelm@53185
  1813
    done
wenzelm@53185
  1814
qed
hoelzl@33741
  1815
hoelzl@33741
  1816
lemma ksimplex_replace_1:
wenzelm@53688
  1817
  assumes "ksimplex p n s"
wenzelm@53688
  1818
    and "a \<in> s"
wenzelm@53688
  1819
    and "n \<noteq> 0"
wenzelm@53688
  1820
    and "j \<in> {1..n}"
wenzelm@53688
  1821
    and "\<forall>x\<in>s - {a}. x j = p"
wenzelm@53186
  1822
  shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 1"
wenzelm@53186
  1823
proof -
wenzelm@53186
  1824
  have lem: "\<And>a a' s'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s"
wenzelm@53186
  1825
    by auto
wenzelm@53186
  1826
  have lem: "\<And>s' a'. ksimplex p n s' \<Longrightarrow> a'\<in>s' \<Longrightarrow> s' - {a'} = s - {a} \<Longrightarrow> s' = s"
wenzelm@53186
  1827
  proof -
wenzelm@53186
  1828
    case goal1
wenzelm@55522
  1829
    obtain a0 a1 where exta:
wenzelm@55522
  1830
        "a0 \<in> s"
wenzelm@55522
  1831
        "a1 \<in> s"
wenzelm@55522
  1832
        "a0 \<noteq> a1"
wenzelm@55522
  1833
        "\<And>x. x \<in> s \<Longrightarrow> kle n a0 x \<and> kle n x a1"
wenzelm@55522
  1834
        "\<And>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
wenzelm@55522
  1835
      by (rule ksimplex_extrema_strong[OF assms(1,3)]) blast
wenzelm@53186
  1836
    have a: "a = a0"
wenzelm@53186
  1837
      apply (rule ksimplex_fix_plane_p[OF assms(1-2,4-5) exta(1,2)])
wenzelm@53186
  1838
      unfolding exta
wenzelm@53186
  1839
      apply auto
wenzelm@53186
  1840
      done
wenzelm@53186
  1841
    moreover
wenzelm@55522
  1842
    obtain b0 b1 where extb:
wenzelm@55522
  1843
        "b0 \<in> s'"
wenzelm@55522
  1844
        "b1 \<in> s'"
wenzelm@55522
  1845
        "b0 \<noteq> b1"
wenzelm@55522
  1846
        "\<And>x. x \<in> s' \<Longrightarrow> kle n b0 x \<and> kle n x b1"
wenzelm@55522
  1847
        "\<And>i. b1 i = (if i \<in> {1..n} then b0 i + 1 else b0 i)"
wenzelm@55522
  1848
      by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)]) blast
wenzelm@53186
  1849
    have a': "a' = b0"
wenzelm@53186
  1850
      apply (rule ksimplex_fix_plane_p[OF goal1(1-2) assms(4), of _ b1])
wenzelm@53186
  1851
      unfolding goal1 extb
wenzelm@53186
  1852
      using extb(1,2) assms(5)
wenzelm@53186
  1853
      apply auto
wenzelm@53186
  1854
      done
wenzelm@53186
  1855
    moreover
wenzelm@53186
  1856
    have *: "b1 = a1"
wenzelm@53186
  1857
      unfolding kle_antisym[symmetric, of b1 a1 n]
wenzelm@53186
  1858
      using exta extb
wenzelm@53186
  1859
      using goal1(3)
wenzelm@53186
  1860
      unfolding a a'
wenzelm@53186
  1861
      by blast
wenzelm@53186
  1862
    moreover
wenzelm@53186
  1863
    have "a0 = b0"
wenzelm@53688
  1864
    proof (rule ext)
wenzelm@53688
  1865
      fix x
wenzelm@53186
  1866
      show "a0 x = b0 x"
wenzelm@53186
  1867
        using *[THEN cong, of x x]
wenzelm@53186
  1868
        unfolding exta extb
wenzelm@53688
  1869
        by (cases "x \<in> {1..n}") auto
wenzelm@53186
  1870
    qed
wenzelm@53186
  1871
    ultimately
wenzelm@53186
  1872
    show "s' = s"
wenzelm@53186
  1873
      apply -
wenzelm@53186
  1874
      apply (rule lem[OF goal1(3) _ goal1(2) assms(2)])
wenzelm@53186
  1875
      apply auto
wenzelm@53186
  1876
      done
wenzelm@53186
  1877
  qed
wenzelm@53186
  1878
  show ?thesis
wenzelm@53186
  1879
    unfolding card_1_exists
wenzelm@53186
  1880
    apply (rule ex1I[of _ s])
wenzelm@53186
  1881
    unfolding mem_Collect_eq
wenzelm@53688
  1882
    apply rule
wenzelm@53688
  1883
    apply (rule assms(1))
wenzelm@53186
  1884
    apply (rule_tac x = a in bexI)
wenzelm@53186
  1885
    prefer 3
wenzelm@53186
  1886
    apply (erule conjE bexE)+
wenzelm@53186
  1887
    apply (rule_tac a'=b in lem)
wenzelm@53186
  1888
    using assms(1-2)
wenzelm@53186
  1889
    apply auto
wenzelm@53186
  1890
    done
wenzelm@53186
  1891
qed
hoelzl@33741
  1892
hoelzl@33741
  1893
lemma ksimplex_replace_2:
wenzelm@53688
  1894
  assumes "ksimplex p n s"
wenzelm@53688
  1895
    and "a \<in> s"
wenzelm@53688
  1896
    and "n \<noteq> 0"
wenzelm@53688
  1897
    and "\<not> (\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = 0)"
wenzelm@53688
  1898
    and "\<not> (\<exists>j\<in>{1..n}. \<forall>x\<in>s - {a}. x j = p)"
wenzelm@53186
  1899
  shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})} = 2"
wenzelm@53688
  1900
    (is "card ?A = 2")
wenzelm@53186
  1901
proof -
wenzelm@53186
  1902
  have lem1: "\<And>a a' s s'. s' - {a'} = s - {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s"
wenzelm@53186
  1903
    by auto
wenzelm@53688
  1904
  have lem2: "\<And>a b. a \<in> s \<Longrightarrow> b \<noteq> a \<Longrightarrow> s \<noteq> insert b (s - {a})"
wenzelm@53186
  1905
  proof
wenzelm@53186
  1906
    case goal1
wenzelm@53688
  1907
    then have "a \<in> insert b (s - {a})"
wenzelm@53688
  1908
      by auto
wenzelm@53688
  1909
    then have "a \<in> s - {a}"
wenzelm@53688
  1910
      unfolding insert_iff
wenzelm@53688
  1911
      using goal1
wenzelm@53688
  1912
      by auto
wenzelm@53688
  1913
    then show False
wenzelm@53688
  1914
      by auto
wenzelm@53186
  1915
  qed
wenzelm@55522
  1916
  obtain a0 a1 where a0a1:
wenzelm@55522
  1917
      "a0 \<in> s"
wenzelm@55522
  1918
      "a1 \<in> s"
wenzelm@55522
  1919
      "a0 \<noteq> a1"
wenzelm@55522
  1920
      "\<forall>x\<in>s. kle n a0 x \<and> kle n x a1"
wenzelm@55522
  1921
      "\<forall>i. a1 i = (if i \<in> {1..n} then a0 i + 1 else a0 i)"
wenzelm@55522
  1922
    by (rule ksimplex_extrema_strong[OF assms(1,3)])
wenzelm@53186
  1923
  {
wenzelm@53186
  1924
    assume "a = a0"
wenzelm@53688
  1925
    have *: "\<And>P Q. P \<or> Q \<Longrightarrow> \<not> P \<Longrightarrow> Q"
wenzelm@53688
  1926
      by auto
wenzelm@53186
  1927
    have "\<exists>x\<in>s. \<not> kle n x a0"
wenzelm@53186
  1928
      apply (rule_tac x=a1 in bexI)
wenzelm@53186
  1929
    proof
wenzelm@53186
  1930
      assume as: "kle n a1 a0"
wenzelm@53186
  1931
      show False
wenzelm@53186
  1932
        using kle_imp_pointwise[OF as,THEN spec[where x=1]]
wenzelm@53186
  1933
        unfolding a0a1(5)[THEN spec[where x=1]]
wenzelm@53688
  1934
        using assms(3)
wenzelm@53688
  1935
        by auto
wenzelm@53186
  1936
    qed (insert a0a1, auto)
wenzelm@53674
  1937
    then have "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a0 j + 1 else a0 j)"
wenzelm@53186
  1938
      apply (rule_tac *[OF ksimplex_successor[OF assms(1-2),unfolded `a=a0`]])
wenzelm@53186
  1939
      apply auto
wenzelm@53186
  1940
      done
wenzelm@55522
  1941
    then
wenzelm@55522
  1942
    obtain a2 k where a2: "a2 \<in> s"
wenzelm@55522
  1943
      and k: "k \<in> {1..n}" "\<forall>j. a2 j = (if j = k then a0 j + 1 else a0 j)"
wenzelm@55522
  1944
      by blast
hoelzl@33741
  1945
    def a3 \<equiv> "\<lambda>j. if j = k then a1 j + 1 else a1 j"
wenzelm@53186
  1946
    have "a3 \<notin> s"
wenzelm@53186
  1947
    proof
wenzelm@53186
  1948
      assume "a3\<in>s"
wenzelm@53674
  1949
      then have "kle n a3 a1"
wenzelm@53688
  1950
        using a0a1(4) by auto
wenzelm@53674
  1951
      then show False
wenzelm@53688
  1952
        apply (drule_tac kle_imp_pointwise)
wenzelm@53688
  1953
        unfolding a3_def
wenzelm@53186
  1954
        apply (erule_tac x = k in allE)
wenzelm@53186
  1955
        apply auto
wenzelm@53186
  1956
        done
wenzelm@53186
  1957
    qed
wenzelm@53688
  1958
    then have "a3 \<noteq> a0" and "a3 \<noteq> a1"
wenzelm@53688
  1959
      using a0a1 by auto
wenzelm@53688
  1960
    have "a2 \<noteq> a0"
wenzelm@53688
  1961
      using k(2)[THEN spec[where x=k]] by auto
wenzelm@53688
  1962
    have lem3: "\<And>x. x \<in> (s - {a0}) \<Longrightarrow> kle n a2 x"
wenzelm@53186
  1963
    proof (rule ccontr)
wenzelm@53186
  1964
      case goal1
wenzelm@53688
  1965
      then have as: "x \<in> s" "x \<noteq> a0"
wenzelm@53688
  1966
        by auto
wenzelm@53186
  1967
      have "kle n a2 x \<or> kle n x a2"
wenzelm@53688
  1968
        using ksimplexD(6)[OF assms(1)] and as `a2 \<in> s`
wenzelm@53688
  1969
        by auto
wenzelm@53186
  1970
      moreover
wenzelm@53688
  1971
      have "kle n a0 x"
wenzelm@53688
  1972
        using a0a1(4) as by auto
wenzelm@53186
  1973
      ultimately have "x = a0 \<or> x = a2"
wenzelm@53186
  1974
        apply -
wenzelm@53186
  1975
        apply (rule kle_adjacent[OF k(2)])
wenzelm@53186
  1976
        using goal1(2)
wenzelm@53186
  1977
        apply auto
wenzelm@53186
  1978
        done
wenzelm@53688
  1979
      then have "x = a2"
wenzelm@53688
  1980
        using as by auto
wenzelm@53688
  1981
      then show False
wenzelm@53688
  1982
        using goal1(2)
wenzelm@53688
  1983
        using kle_refl
wenzelm@53688
  1984
        by auto
wenzelm@53186
  1985
    qed
wenzelm@53186
  1986
    let ?s = "insert a3 (s - {a0})"
wenzelm@53186
  1987
    have "ksimplex p n ?s"
wenzelm@53186
  1988
      apply (rule ksimplexI)
wenzelm@53688
  1989
      apply (rule_tac[2-] ballI)
wenzelm@53688
  1990
      apply (rule_tac[4] ballI)
wenzelm@53688
  1991
    proof -
wenzelm@53186
  1992
      show "card ?s = n + 1"
wenzelm@53186
  1993
        using ksimplexD(2-3)[OF assms(1)]
wenzelm@53688
  1994
        using `a3 \<noteq> a0` `a3 \<notin> s` `a0 \<in> s`
wenzelm@53688
  1995
        by (auto simp add: card_insert_if)
wenzelm@53186
  1996
      fix x
wenzelm@53186
  1997
      assume x: "x \<in> insert a3 (s - {a0})"
wenzelm@53186
  1998
      show "\<forall>j. x j \<le> p"
wenzelm@53688
  1999
      proof
wenzelm@53186
  2000
        fix j
wenzelm@53688
  2001
        show "x j \<le> p"
wenzelm@53688
  2002
        proof (cases "x = a3")
wenzelm@53186
  2003
          case False
wenzelm@53688
  2004
          then show ?thesis
wenzelm@53688
  2005
            using x ksimplexD(4)[OF assms(1)] by auto
wenzelm@53186
  2006
        next
wenzelm@53186
  2007
          case True
wenzelm@53688
  2008
          show ?thesis unfolding True
wenzelm@53688
  2009
          proof (cases "j = k")
wenzelm@53688
  2010
            case False
wenzelm@53688
  2011
            then show "a3 j \<le> p"
wenzelm@53688
  2012
              unfolding True a3_def
wenzelm@53688
  2013
              using `a1 \<in> s` ksimplexD(4)[OF assms(1)]
wenzelm@53688
  2014
              by auto
wenzelm@53688
  2015
          next
wenzelm@55522
  2016
            obtain a4 where a4: "a4 \<in> s - {a}" "a4 k \<noteq> p"
wenzelm@55522
  2017
              using assms(5) k(1) by blast
wenzelm@53688
  2018
            have "a2 k \<le> a4 k"
wenzelm@53688
  2019
              using lem3[OF a4(1)[unfolded `a = a0`],THEN kle_imp_pointwise]
wenzelm@53688
  2020
              by auto
wenzelm@53688
  2021
            also have "\<dots> < p"
wenzelm@53688
  2022
              using ksimplexD(4)[OF assms(1),rule_format,of a4 k]
wenzelm@53688
  2023
              using a4 by auto
wenzelm@53688
  2024
            finally have *: "a0 k + 1 < p"
wenzelm@53688
  2025
              unfolding k(2)[rule_format]
wenzelm@53688
  2026
              by auto
wenzelm@53688
  2027
            case True
wenzelm@53688
  2028
            then show "a3 j \<le>p"
wenzelm@53688
  2029
              unfolding a3_def
wenzelm@53688
  2030
              unfolding a0a1(5)[rule_format]
wenzelm@53688
  2031
              using k(1) k(2)assms(5)
wenzelm@53688
  2032
              using *
wenzelm@53688
  2033
              by simp
wenzelm@53688
  2034
          qed
wenzelm@53186
  2035
        qed
wenzelm@53186
  2036
      qed
wenzelm@53186
  2037
      show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
wenzelm@53688
  2038
      proof (rule, rule)
wenzelm@53186
  2039
        fix j :: nat
wenzelm@53186
  2040
        assume j: "j \<notin> {1..n}"
wenzelm@53688
  2041
        show "x j = p"
wenzelm@53688
  2042
        proof (cases "x = a3")
wenzelm@53186
  2043
          case False
wenzelm@53688
  2044
          then show ?thesis
wenzelm@53688
  2045
            using j x ksimplexD(5)[OF assms(1)]
wenzelm@53688
  2046
            by auto
wenzelm@53688
  2047
        next
wenzelm@53688
  2048
          case True
wenzelm@53688
  2049
          show ?thesis
wenzelm@53688
  2050
            unfolding True a3_def
wenzelm@53688
  2051
            using j k(1)
wenzelm@53688
  2052
            using ksimplexD(5)[OF assms(1),rule_format,OF `a1\<in>s` j]
wenzelm@53688
  2053
            by auto
wenzelm@53688
  2054
        qed
wenzelm@53186
  2055
      qed
wenzelm@53186
  2056
      fix y
wenzelm@53186
  2057
      assume y: "y \<in> insert a3 (s - {a0})"
wenzelm@53688
  2058
      have lem4: "\<And>x. x\<in>s \<Longrightarrow> x \<noteq> a0 \<Longrightarrow> kle n x a3"
wenzelm@53186
  2059
      proof -
wenzelm@53186
  2060
        case goal1
wenzelm@55522
  2061
        obtain kk where kk:
wenzelm@55522
  2062
            "kk \<subseteq> {1..n}"
wenzelm@55522
  2063
            "\<forall>j. a1 j = x j + (if j \<in> kk then 1 else 0)"
wenzelm@55522
  2064
          using a0a1(4)[rule_format, OF `x\<in>s`,THEN conjunct2,unfolded kle_def]
wenzelm@55522
  2065
          by blast
wenzelm@53186
  2066
        have "k \<notin> kk"
wenzelm@53186
  2067
        proof
wenzelm@53186
  2068
          assume "k \<in> kk"
wenzelm@53688
  2069
          then have "a1 k = x k + 1"
wenzelm@53688
  2070
            using kk by auto
wenzelm@53688
  2071
          then have "a0 k = x k"
wenzelm@53688
  2072
            unfolding a0a1(5)[rule_format] using k(1) by auto
wenzelm@53688
  2073
          then have "a2 k = x k + 1"
wenzelm@53688
  2074
            unfolding k(2)[rule_format] by auto
wenzelm@53186
  2075
          moreover
wenzelm@53688
  2076
          have "a2 k \<le> x k"
wenzelm@53688
  2077
            using lem3[of x,THEN kle_imp_pointwise] goal1 by auto
wenzelm@53688
  2078
          ultimately show False
wenzelm@53688
  2079
            by auto
wenzelm@53186
  2080
        qed
wenzelm@53674
  2081
        then show ?case
wenzelm@53186
  2082
          unfolding kle_def
wenzelm@53186
  2083
          apply (rule_tac x="insert k kk" in exI)
wenzelm@53186
  2084
          using kk(1)
wenzelm@53186
  2085
          unfolding a3_def kle_def kk(2)[rule_format]
wenzelm@53186
  2086
          using k(1)
wenzelm@53186
  2087
          apply auto
wenzelm@53186
  2088
          done
wenzelm@53186
  2089
      qed
wenzelm@53186
  2090
      show "kle n x y \<or> kle n y x"
wenzelm@53186
  2091
      proof (cases "y = a3")
wenzelm@53186
  2092
        case True
wenzelm@53186
  2093
        show ?thesis
wenzelm@53186
  2094
          unfolding True
wenzelm@53186
  2095
          apply (cases "x = a3")
wenzelm@53186
  2096
          defer
wenzelm@53186
  2097
          apply (rule disjI1, rule lem4)
wenzelm@53186
  2098
          using x
wenzelm@53186
  2099
          apply auto
wenzelm@53186
  2100
          done
wenzelm@53186
  2101
      next
wenzelm@53186
  2102
        case False
wenzelm@53186
  2103
        show ?thesis
wenzelm@53186
  2104
        proof (cases "x = a3")
wenzelm@53186
  2105
          case True
wenzelm@53186
  2106
          show ?thesis
wenzelm@53186
  2107
            unfolding True
wenzelm@53688
  2108
            apply (rule disjI2)
wenzelm@53688
  2109
            apply (rule lem4)
wenzelm@53186
  2110
            using y False
wenzelm@53186
  2111
            apply auto
wenzelm@53186
  2112
            done
wenzelm@53186
  2113
        next
wenzelm@53186
  2114
          case False
wenzelm@53674
  2115
          then show ?thesis
wenzelm@53186
  2116
            apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])
wenzelm@53186
  2117
            using x y `y \<noteq> a3`
wenzelm@53186
  2118
            apply auto
wenzelm@53186
  2119
            done
wenzelm@53186
  2120
        qed
wenzelm@53186
  2121
      qed
wenzelm@53186
  2122
    qed
wenzelm@53674
  2123
    then have "insert a3 (s - {a0}) \<in> ?A"
wenzelm@53186
  2124
      unfolding mem_Collect_eq
wenzelm@53186
  2125
      apply -
wenzelm@53688
  2126
      apply rule
wenzelm@53688
  2127
      apply assumption
wenzelm@53186
  2128
      apply (rule_tac x = "a3" in bexI)
wenzelm@53186
  2129
      unfolding `a = a0`
wenzelm@53186
  2130
      using `a3 \<notin> s`
wenzelm@53186
  2131
      apply auto
wenzelm@53186
  2132
      done
wenzelm@53186
  2133
    moreover
wenzelm@53688
  2134
    have "s \<in> ?A"
wenzelm@53688
  2135
      using assms(1,2) by auto
wenzelm@53688
  2136
    ultimately have "?A \<supseteq> {s, insert a3 (s - {a0})}"
wenzelm@53688
  2137
      by auto
wenzelm@53186
  2138
    moreover
wenzelm@53186
  2139
    have "?A \<subseteq> {s, insert a3 (s - {a0})}"
wenzelm@53186
  2140
      apply rule
wenzelm@53186
  2141
      unfolding mem_Collect_eq
wenzelm@53186
  2142
    proof (erule conjE)
wenzelm@53186
  2143
      fix s'
wenzelm@55522
  2144
      assume as: "ksimplex p n s'"
wenzelm@55522
  2145
      assume "\<exists>b\<in>s'. s' - {b} = s - {a}"
wenzelm@55522
  2146
      then obtain a' where a': "a' \<in> s'" "s' - {a'} = s - {a}" ..
wenzelm@55522
  2147
      obtain a_min a_max where min_max:
wenzelm@55522
  2148
          "a_min \<in> s'"
wenzelm@55522
  2149
          "a_max \<in> s'"
wenzelm@55522
  2150
          "a_min \<noteq> a_max"
wenzelm@55522
  2151
          "\<forall>x\<in>s'. kle n a_min x \<and> kle n x a_max"
wenzelm@55522
  2152
          "\<forall>i. a_max i = (if i \<in> {1..n} then a_min i + 1 else a_min i)"
wenzelm@55522
  2153
        by (rule ksimplex_extrema_strong[OF as assms(3)])
wenzelm@53186
  2154
      have *: "\<forall>x\<in>s' - {a'}. x k = a2 k"
wenzelm@53186
  2155
        unfolding a'
wenzelm@53186
  2156
      proof
wenzelm@53186
  2157
        fix x
wenzelm@53186
  2158
        assume x: "x \<in> s - {a}"
wenzelm@53674
  2159
        then have "kle n a2 x"
wenzelm@53186
  2160
          apply -
wenzelm@53186
  2161
          apply (rule lem3)
wenzelm@53186
  2162
          using `a = a0`
wenzelm@53186
  2163
          apply auto
wenzelm@53186
  2164
          done
wenzelm@53674
  2165
        then have "a2 k \<le> x k"
wenzelm@53186
  2166
          apply (drule_tac kle_imp_pointwise)
wenzelm@53186
  2167
          apply auto
wenzelm@53186
  2168
          done
wenzelm@53186
  2169
        moreover
wenzelm@53186
  2170
        have "x k \<le> a2 k"
wenzelm@53186
  2171
          unfolding k(2)[rule_format]
wenzelm@53186
  2172
          using a0a1(4)[rule_format,of x, THEN conjunct1]
wenzelm@53688
  2173
          unfolding kle_def using x
wenzelm@53688
  2174
          by auto
wenzelm@53688
  2175
        ultimately show "x k = a2 k"
wenzelm@53688
  2176
        by auto
wenzelm@53186
  2177
      qed
wenzelm@53186
  2178
      have **: "a' = a_min \<or> a' = a_max"
wenzelm@53186
  2179
        apply (rule ksimplex_fix_plane[OF a'(1) k(1) *])
wenzelm@53186
  2180
        using min_max
wenzelm@53186
  2181
        apply auto
wenzelm@53186
  2182
        done
wenzelm@53186
  2183
      show "s' \<in> {s, insert a3 (s - {a0})}"
wenzelm@53186
  2184
      proof (cases "a' = a_min")
wenzelm@53186
  2185
        case True
wenzelm@53186
  2186
        have "a_max = a1"
wenzelm@53186
  2187
          unfolding kle_antisym[symmetric,of a_max a1 n]
wenzelm@53186
  2188
          apply rule
wenzelm@53186
  2189
          apply (rule a0a1(4)[rule_format,THEN conjunct2])
wenzelm@53186
  2190
          defer
wenzelm@53186
  2191
        proof (rule min_max(4)[rule_format,THEN conjunct2])
wenzelm@53688
  2192
          show "a1 \<in> s'"
wenzelm@53688
  2193
            using a'
wenzelm@53688
  2194
            unfolding `a = a0`
wenzelm@53688
  2195
            using a0a1
wenzelm@53688
  2196
            by auto
wenzelm@53186
  2197
          show "a_max \<in> s"
wenzelm@53186
  2198
          proof (rule ccontr)
wenzelm@53688
  2199
            assume "\<not> ?thesis"
wenzelm@53688
  2200
            then have "a_max = a'"
wenzelm@53688
  2201
              using a' min_max by auto
wenzelm@53688
  2202
            then show False
wenzelm@53688
  2203
              unfolding True using min_max by auto
wenzelm@53186
  2204
          qed
wenzelm@53186
  2205
        qed
wenzelm@53688
  2206
        then have "\<forall>i. a_max i = a1 i"
wenzelm@53688
  2207
          by auto
wenzelm@53688
  2208
        then have "a' = a"
wenzelm@53688
  2209
          unfolding True `a = a0`
wenzelm@53186
  2210
          apply -
wenzelm@53688
  2211
          apply (subst fun_eq_iff)
wenzelm@53688
  2212
          apply rule
wenzelm@53186
  2213
          apply (erule_tac x=x in allE)
wenzelm@53186
  2214
          unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
wenzelm@53186
  2215
        proof -
wenzelm@53186
  2216
          case goal1
wenzelm@53688
  2217
          then show ?case
wenzelm@53688
  2218
            by (cases "x \<in> {1..n}") auto
wenzelm@53186
  2219
        qed
wenzelm@53674
  2220
        then have "s' = s"
wenzelm@53186
  2221
          apply -
wenzelm@53186
  2222
          apply (rule lem1[OF a'(2)])
wenzelm@53688
  2223
          using `a \<in> s` `a' \<in> s'`
wenzelm@53186
  2224
          apply auto
wenzelm@53186
  2225
          done
wenzelm@53688
  2226
        then show ?thesis
wenzelm@53688
  2227
          by auto
wenzelm@53186
  2228
      next
wenzelm@53186
  2229
        case False
wenzelm@53688
  2230
        then have as: "a' = a_max"
wenzelm@53688
  2231
          using ** by auto
wenzelm@53688
  2232
        have "a_min = a2"
wenzelm@53688
  2233
          unfolding kle_antisym[symmetric, of _ _ n]
wenzelm@53186
  2234
          apply rule
wenzelm@53186
  2235
          apply (rule min_max(4)[rule_format,THEN conjunct1])
wenzelm@53186
  2236
          defer
wenzelm@53186
  2237
        proof (rule lem3)
wenzelm@53186
  2238
          show "a_min \<in> s - {a0}"
wenzelm@53186
  2239
            unfolding a'(2)[symmetric,unfolded `a = a0`]
wenzelm@53688
  2240
            unfolding as
wenzelm@53688
  2241
            using min_max(1-3)
wenzelm@53688
  2242
            by auto
wenzelm@53186
  2243
          have "a2 \<noteq> a"
wenzelm@53688
  2244
            unfolding `a = a0`
wenzelm@53688
  2245
            using k(2)[rule_format,of k]
wenzelm@53688
  2246
            by auto
wenzelm@53674
  2247
          then have "a2 \<in> s - {a}"
wenzelm@53186
  2248
            using a2 by auto
wenzelm@53688
  2249
          then show "a2 \<in> s'"
wenzelm@53688
  2250
            unfolding a'(2)[symmetric] by auto
wenzelm@53186
  2251
        qed
wenzelm@53688
  2252
        then have "\<forall>i. a_min i = a2 i"
wenzelm@53688
  2253
          by auto
wenzelm@53674
  2254
        then have "a' = a3"
wenzelm@53186
  2255
          unfolding as `a = a0`
wenzelm@53688
  2256
          apply (subst fun_eq_iff)
wenzelm@53688
  2257
          apply rule
wenzelm@53186
  2258
          apply (erule_tac x=x in allE)
wenzelm@53186
  2259
          unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
wenzelm@53186
  2260
          unfolding a3_def k(2)[rule_format]
wenzelm@53186
  2261
          unfolding a0a1(5)[rule_format]
wenzelm@53186
  2262
        proof -
wenzelm@53186
  2263
          case goal1
wenzelm@53186
  2264
          show ?case
wenzelm@53186
  2265
            unfolding goal1
wenzelm@53688
  2266
            apply (cases "x \<in> {1..n}")
wenzelm@53186
  2267
            defer
wenzelm@53186
  2268
            apply (cases "x = k")
wenzelm@53688
  2269
            using `k \<in> {1..n}`
wenzelm@53186
  2270
            apply auto
wenzelm@53186
  2271
            done
wenzelm@53186
  2272
        qed
wenzelm@53674
  2273
        then have "s' = insert a3 (s - {a0})"
wenzelm@53186
  2274
          apply -
wenzelm@53186
  2275
          apply (rule lem1)
wenzelm@53186
  2276
          defer
wenzelm@53186
  2277
          apply assumption
wenzelm@53186
  2278
          apply (rule a'(1))
wenzelm@53186
  2279
          unfolding a' `a = a0`
wenzelm@53186
  2280
          using `a3 \<notin> s`
wenzelm@53186
  2281
          apply auto
wenzelm@53186
  2282
          done
wenzelm@53674
  2283
        then show ?thesis by auto
wenzelm@53186
  2284
      qed
wenzelm@53186
  2285
    qed
wenzelm@53688
  2286
    ultimately have *: "?A = {s, insert a3 (s - {a0})}"
wenzelm@53688
  2287
      by blast
wenzelm@53688
  2288
    have "s \<noteq> insert a3 (s - {a0})"
wenzelm@53846
  2289
      using `a3 \<notin> s` by auto
wenzelm@53688
  2290
    then have ?thesis
wenzelm@53688
  2291
      unfolding * by auto
wenzelm@53186
  2292
  }
wenzelm@53186
  2293
  moreover
wenzelm@53186
  2294
  {
wenzelm@53186
  2295
    assume "a = a1"
wenzelm@53688
  2296
    have *: "\<And>P Q. P \<or> Q \<Longrightarrow> \<not> P \<Longrightarrow> Q"
wenzelm@53688
  2297
      by auto
wenzelm@53186
  2298
    have "\<exists>x\<in>s. \<not> kle n a1 x"
wenzelm@53186
  2299
      apply (rule_tac x=a0 in bexI)
wenzelm@53186
  2300
    proof
wenzelm@53186
  2301
      assume as: "kle n a1 a0"
wenzelm@53186
  2302
      show False
wenzelm@53186
  2303
        using kle_imp_pointwise[OF as,THEN spec[where x=1]]
wenzelm@53186
  2304
        unfolding a0a1(5)[THEN spec[where x=1]]
wenzelm@53186
  2305
        using assms(3)
wenzelm@53186
  2306
        by auto
wenzelm@53186
  2307
    qed (insert a0a1, auto)
wenzelm@53674
  2308
    then have "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a1 j = (if j = k then y j + 1 else y j)"
wenzelm@53186
  2309
      apply (rule_tac *[OF ksimplex_predecessor[OF assms(1-2),unfolded `a=a1`]])
wenzelm@53186
  2310
      apply auto
wenzelm@53186
  2311
      done
wenzelm@55522
  2312
    then
wenzelm@55522
  2313
    obtain a2 k where a2: "a2 \<in> s"
wenzelm@55522
  2314
      and k: "k \<in> {1..n}" "\<forall>j. a1 j = (if j = k then a2 j + 1 else a2 j)"
wenzelm@55522
  2315
      by blast
hoelzl@33741
  2316
    def a3 \<equiv> "\<lambda>j. if j = k then a0 j - 1 else a0 j"
wenzelm@53688
  2317
    have "a2 \<noteq> a1"
wenzelm@53688
  2318
      using k(2)[THEN spec[where x=k]] by auto
wenzelm@53688
  2319
    have lem3: "\<And>x. x \<in> s - {a1} \<Longrightarrow> kle n x a2"
wenzelm@53186
  2320
    proof (rule ccontr)
wenzelm@53186
  2321
      case goal1
wenzelm@53688
  2322
      then have as: "x \<in> s" "x \<noteq> a1" by auto
wenzelm@53186
  2323
      have "kle n a2 x \<or> kle n x a2"
wenzelm@53688
  2324
        using ksimplexD(6)[OF assms(1)] and as `a2\<in>s`
wenzelm@53688
  2325
        by auto
wenzelm@53186
  2326
      moreover
wenzelm@53688
  2327
      have "kle n x a1"
wenzelm@53688
  2328
        using a0a1(4) as by auto
wenzelm@53186
  2329
      ultimately have "x = a2 \<or> x = a1"
wenzelm@53186
  2330
        apply -
wenzelm@53186
  2331
        apply (rule kle_adjacent[OF k(2)])
wenzelm@53186
  2332
        using goal1(2)
wenzelm@53186
  2333
        apply auto
wenzelm@53186
  2334
        done
wenzelm@53688
  2335
      then have "x = a2"
wenzelm@53688
  2336
        using as by auto
wenzelm@53688
  2337
      then show False
wenzelm@53688
  2338
        using goal1(2) using kle_refl by auto
wenzelm@53186
  2339
    qed
wenzelm@53186
  2340
    have "a0 k \<noteq> 0"
wenzelm@53186
  2341
    proof -
wenzelm@55522
  2342
      obtain a4 where a4: "a4 \<in> s - {a}" "a4 k \<noteq> 0"
wenzelm@55522
  2343
        using assms(4) `k\<in>{1..n}` by blast
wenzelm@53688
  2344
      have "a4 k \<le> a2 k"
wenzelm@53688
  2345
        using lem3[OF a4(1)[unfolded `a=a1`],THEN kle_imp_pointwise]
wenzelm@53688
  2346
        by auto
wenzelm@53688
  2347
      moreover have "a4 k > 0"
wenzelm@53688
  2348
        using a4 by auto
wenzelm@53688
  2349
      ultimately have "a2 k > 0"
wenzelm@53186
  2350
        by auto
wenzelm@53688
  2351
      then have "a1 k > 1"
wenzelm@53688
  2352
        unfolding k(2)[rule_format] by simp
wenzelm@53688
  2353
      then show ?thesis
wenzelm@53688
  2354
        unfolding a0a1(5)[rule_format] using k(1) by simp
wenzelm@53186
  2355
    qed
wenzelm@53688
  2356
    then have lem4: "\<forall>j. a0 j = (if j = k then a3 j + 1 else a3 j)"
wenzelm@53186
  2357
      unfolding a3_def by simp
wenzelm@53186
  2358
    have "\<not> kle n a0 a3"
wenzelm@53688
  2359
      apply (rule notI)
wenzelm@53186
  2360
      apply (drule kle_imp_pointwise)
wenzelm@53186
  2361
      unfolding lem4[rule_format]
wenzelm@53186
  2362
      apply (erule_tac x=k in allE)
wenzelm@53186
  2363
      apply auto
wenzelm@53186
  2364
      done
wenzelm@53688
  2365
    then have "a3 \<notin> s"
wenzelm@53688
  2366
      using a0a1(4) by auto
wenzelm@53688
  2367
    then have "a3 \<noteq> a1" "a3 \<noteq> a0"
wenzelm@53688
  2368
      using a0a1 by auto
wenzelm@53186
  2369
    let ?s = "insert a3 (s - {a1})"
wenzelm@53186
  2370
    have "ksimplex p n ?s"
wenzelm@53186
  2371
      apply (rule ksimplexI)
wenzelm@53186
  2372
    proof (rule_tac[2-] ballI,rule_tac[4] ballI)
wenzelm@53186
  2373
      show "card ?s = n+1"
wenzelm@53186
  2374
        using ksimplexD(2-3)[OF assms(1)]
wenzelm@53688
  2375
        using `a3 \<noteq> a0` `a3 \<notin> s` `a1 \<in> s`
wenzelm@53688
  2376
        by (auto simp add:card_insert_if)
wenzelm@53186
  2377
      fix x
wenzelm@53186
  2378
      assume x: "x \<in> insert a3 (s - {a1})"
wenzelm@53688
  2379
      show "\<forall>j. x j \<le> p"
wenzelm@53688
  2380
      proof
wenzelm@53186
  2381
        fix j
wenzelm@53688
  2382
        show "x j \<le> p"
wenzelm@53688
  2383
        proof (cases "x = a3")
wenzelm@53186
  2384
          case False
wenzelm@53688
  2385
          then show ?thesis
wenzelm@53688
  2386
            using x ksimplexD(4)[OF assms(1)] by auto
wenzelm@53186
  2387
        next
wenzelm@53688
  2388
          case True
wenzelm@53688
  2389
          show ?thesis
wenzelm@53688
  2390
            unfolding True
wenzelm@53688
  2391
          proof (cases "j = k")
wenzelm@53688
  2392
            case False
wenzelm@53688
  2393
            then show "a3 j \<le> p"
wenzelm@53688
  2394
              unfolding True a3_def
wenzelm@53688
  2395
              using `a0 \<in> s` ksimplexD(4)[OF assms(1)]
wenzelm@53688
  2396
              by auto
wenzelm@53688
  2397
          next
wenzelm@55522
  2398
            case True
wenzelm@55522
  2399
            obtain a4 where a4: "a4 \<in> s - {a}" "a4 k \<noteq> p"
wenzelm@55522
  2400
              using assms(5) k(1) by blast
wenzelm@55522
  2401
            have "a3 k \<le> a0 k"
wenzelm@53688
  2402
              unfolding lem4[rule_format] by auto
wenzelm@53688
  2403
            also have "\<dots> \<le> p"
wenzelm@53688
  2404
              using ksimplexD(4)[OF assms(1),rule_format, of a0 k] a0a1
wenzelm@53688
  2405
              by auto
wenzelm@53688
  2406
            finally show "a3 j \<le> p"
wenzelm@53688
  2407
              unfolding True by auto
wenzelm@53688
  2408
          qed
wenzelm@53186
  2409
        qed
wenzelm@53186
  2410
      qed
wenzelm@53186
  2411
      show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
wenzelm@53688
  2412
      proof (rule, rule)
wenzelm@53186
  2413
        fix j :: nat
wenzelm@53186
  2414
        assume j: "j \<notin> {1..n}"
wenzelm@53688
  2415
        show "x j = p"
wenzelm@53688
  2416
        proof (cases "x = a3")
wenzelm@53186
  2417
          case False
wenzelm@53688
  2418
          then show ?thesis
wenzelm@53688
  2419
            using j x ksimplexD(5)[OF assms(1)] by auto
wenzelm@53186
  2420
        next
wenzelm@53186
  2421
          case True
wenzelm@53688
  2422
          show ?thesis
wenzelm@53688
  2423
            unfolding True a3_def
wenzelm@53688
  2424
            using j k(1)
wenzelm@53688
  2425
            using ksimplexD(5)[OF assms(1),rule_format,OF `a0\<in>s` j]
wenzelm@53688
  2426
            by auto
wenzelm@53688
  2427
        qed
wenzelm@53186
  2428
      qed
wenzelm@53186
  2429
      fix y
wenzelm@53688
  2430
      assume y: "y \<in> insert a3 (s - {a1})"
wenzelm@53688
  2431
      have lem4: "\<And>x. x \<in> s \<Longrightarrow> x \<noteq> a1 \<Longrightarrow> kle n a3 x"
wenzelm@53186
  2432
      proof -
wenzelm@53186
  2433
        case goal1
wenzelm@53688
  2434
        then have *: "x\<in>s - {a1}"
wenzelm@53688
  2435
          by auto
wenzelm@53186
  2436
        have "kle n a3 a2"
wenzelm@53186
  2437
        proof -
wenzelm@53186
  2438
          have "kle n a0 a1"
wenzelm@55522
  2439
            using a0a1 by auto
wenzelm@55522
  2440
          then obtain kk where "kk \<subseteq> {1..n}" "(\<forall>j. a1 j = a0 j + (if j \<in> kk then 1 else 0))"
wenzelm@55522
  2441
            unfolding kle_def by blast
wenzelm@53674
  2442
          then show ?thesis
wenzelm@53186
  2443
            unfolding kle_def
wenzelm@53186
  2444
            apply (rule_tac x=kk in exI)
wenzelm@53186
  2445
            unfolding lem4[rule_format] k(2)[rule_format]
wenzelm@53186
  2446
            apply rule
wenzelm@53186
  2447
            defer
wenzelm@53186
  2448
          proof rule
wenzelm@53186
  2449
            case goal1
wenzelm@53674
  2450
            then show ?case
wenzelm@53186
  2451
              apply -
wenzelm@53186
  2452
              apply (erule_tac[!] x=j in allE)
wenzelm@53186
  2453
              apply (cases "j \<in> kk")
wenzelm@53186
  2454
              apply (case_tac[!] "j=k")
wenzelm@53186
  2455
              apply auto
wenzelm@53186
  2456
              done
wenzelm@53186
  2457
          qed auto
wenzelm@53186
  2458
        qed
wenzelm@53186
  2459
        moreover
wenzelm@53186
  2460
        have "kle n a3 a0"
wenzelm@53186
  2461
          unfolding kle_def lem4[rule_format]
wenzelm@53186
  2462
          apply (rule_tac x="{k}" in exI)
wenzelm@53186
  2463
          using k(1)
wenzelm@53186
  2464
          apply auto
wenzelm@53186
  2465
          done
wenzelm@53186
  2466
        ultimately
wenzelm@53186
  2467
        show ?case
wenzelm@53186
  2468
          apply -
wenzelm@53186
  2469
          apply (rule kle_between_l[of _ a0 _ a2])
wenzelm@53186
  2470
          using lem3[OF *]
wenzelm@53186
  2471
          using a0a1(4)[rule_format,OF goal1(1)]
wenzelm@53186
  2472
          apply auto
wenzelm@53186
  2473
          done
wenzelm@53186
  2474
      qed
wenzelm@53186
  2475
      show "kle n x y \<or> kle n y x"
wenzelm@53186
  2476
      proof (cases "y = a3")
wenzelm@53186
  2477
        case True
wenzelm@53186
  2478
        show ?thesis
wenzelm@53186
  2479
          unfolding True
wenzelm@53186
  2480
          apply (cases "x = a3")
wenzelm@53186
  2481
          defer
wenzelm@53688
  2482
          apply (rule disjI2)
wenzelm@53688
  2483
          apply (rule lem4)
wenzelm@53186
  2484
          using x
wenzelm@53186
  2485
          apply auto
wenzelm@53186
  2486
          done
wenzelm@53186
  2487
      next
wenzelm@53186
  2488
        case False
wenzelm@53186
  2489
        show ?thesis
wenzelm@53186
  2490
        proof (cases "x = a3")
wenzelm@53186
  2491
          case True
wenzelm@53186
  2492
          show ?thesis
wenzelm@53186
  2493
            unfolding True
wenzelm@53688
  2494
            apply (rule disjI1)
wenzelm@53688
  2495
            apply (rule lem4)
wenzelm@53186
  2496
            using y False
wenzelm@53186
  2497
            apply auto
wenzelm@53186
  2498
            done
wenzelm@53186
  2499
        next
wenzelm@53186
  2500
          case False
wenzelm@53674
  2501
          then show ?thesis
wenzelm@53186
  2502
            apply (rule_tac ksimplexD(6)[OF assms(1),rule_format])
wenzelm@53688
  2503
            using x y `y \<noteq> a3`
wenzelm@53186
  2504
            apply auto
wenzelm@53186
  2505
            done
wenzelm@53186
  2506
        qed
wenzelm@53186
  2507
      qed
wenzelm@53186
  2508
    qed
wenzelm@53674
  2509
    then have "insert a3 (s - {a1}) \<in> ?A"
wenzelm@53186
  2510
      unfolding mem_Collect_eq
wenzelm@53186
  2511
        apply -
wenzelm@53186
  2512
        apply (rule, assumption)
wenzelm@53186
  2513
        apply (rule_tac x = "a3" in bexI)
wenzelm@53186
  2514
        unfolding `a = a1`
wenzelm@53186
  2515
        using `a3 \<notin> s`
wenzelm@53186
  2516
        apply auto
wenzelm@53186
  2517
        done
wenzelm@53186
  2518
    moreover
wenzelm@53688
  2519
    have "s \<in> ?A"
wenzelm@53688
  2520
      using assms(1,2) by auto
wenzelm@53688
  2521
    ultimately have "?A \<supseteq> {s, insert a3 (s - {a1})}"
wenzelm@53688
  2522
      by auto
wenzelm@53186
  2523
    moreover have "?A \<subseteq> {s, insert a3 (s - {a1})}"
wenzelm@53186
  2524
      apply rule
wenzelm@53186
  2525
      unfolding mem_Collect_eq
wenzelm@53186
  2526
    proof (erule conjE)
wenzelm@53186
  2527
      fix s'
wenzelm@55522
  2528
      assume as: "ksimplex p n s'"
wenzelm@55522
  2529
      assume "\<exists>b\<in>s'. s' - {b} = s - {a}"
wenzelm@55522
  2530
      then obtain a' where a': "a' \<in> s'" "s' - {a'} = s - {a}" ..
wenzelm@55522
  2531
      obtain a_min a_max where min_max:
wenzelm@55522
  2532
          "a_min \<in> s'"
wenzelm@55522
  2533
          "a_max \<in> s'"
wenzelm@55522
  2534
          "a_min \<noteq> a_max"
wenzelm@55522
  2535
          "\<forall>x\<in>s'. kle n a_min x \<and> kle n x a_max"
wenzelm@55522
  2536
          "\<forall>i. a_max i = (if i \<in> {1..n} then a_min i + 1 else a_min i)"
wenzelm@55522
  2537
        by (rule ksimplex_extrema_strong[OF as assms(3)])
wenzelm@53186
  2538
      have *: "\<forall>x\<in>s' - {a'}. x k = a2 k" unfolding a'
wenzelm@53186
  2539
      proof
wenzelm@53186
  2540
        fix x
wenzelm@53186
  2541
        assume x: "x \<in> s - {a}"
wenzelm@53674
  2542
        then have "kle n x a2"
wenzelm@53186
  2543
          apply -
wenzelm@53186
  2544
          apply (rule lem3)
wenzelm@53186
  2545
          using `a = a1`
wenzelm@53186
  2546
          apply auto
wenzelm@53186
  2547
          done
wenzelm@53674
  2548
        then have "x k \<le> a2 k"
wenzelm@53186
  2549
          apply (drule_tac kle_imp_pointwise)
wenzelm@53186
  2550
          apply auto
wenzelm@53186
  2551
          done
wenzelm@53186
  2552
        moreover
wenzelm@53186
  2553
        {
wenzelm@53186
  2554
          have "a2 k \<le> a0 k"
wenzelm@53186
  2555
            using k(2)[rule_format,of k]
wenzelm@53186
  2556
            unfolding a0a1(5)[rule_format]
wenzelm@53186
  2557
            using k(1)
wenzelm@53186
  2558
            by simp
wenzelm@53186
  2559
          also have "\<dots> \<le> x k"
wenzelm@53186
  2560
            using a0a1(4)[rule_format,of x,THEN conjunct1,THEN kle_imp_pointwise] x