Quelle Brouwer_Fixpoint.thy Sprache: Isabelle

(*  Author:     John Harrison
    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light) and LCP
*)

(* At the moment this is just Brouwer's fixpoint theorem. The proof is from  *)
(* Kuhn: "some combinatorial lemmas in topology", IBM J. v4. (1960) p. 518   *)
(* See "http://www.research.ibm.com/journal/rd/045/ibmrd0405K.pdf".          *)
(*                                                                           *)
(* The script below is quite messy, but at least we avoid formalizing any    *)
(* topological machinery; we don't even use barycentric subdivision; this is *)
(* the big advantage of Kuhn's proof over the usual Sperner's lemma one.     *)
(*                                                                           *)
(*              (c) Copyright, John Harrison 1998-2008                       *)

section \<open>Brouwer's Fixed Point Theorem\<close>

theory Brouwer_Fixpoint
  imports Homeomorphism Derivative
begin

subsection \<open>Retractions\<close>

lemma retract_of_contractible:
  assumes "contractible T" "S retract_of T"
  shows "contractible S"
  using assms
  apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with image_subset_iff_funcset)
  apply (rule_tac x="r a" in exI)
  apply (rule_tac x="r \ h" in exI)
  apply (intro conjI continuous_intros continuous_on_compose)
      apply (erule continuous_on_subset | force)+
  done

lemma retract_of_path_connected:
    "\path_connected T; S retract_of T\ \ path_connected S"
  by (metis path_connected_continuous_image retract_of_def retraction)

lemma retract_of_simply_connected:
  assumes T: "simply_connected T" and "S retract_of T"
  shows "simply_connected S"
proof -
  obtain r where r: "retraction T S r"
    using assms by (metis retract_of_def)
  have "S \ T"
    by (meson \<open>retraction T S r\<close> retraction)
  then have "(\a. a) \ S \ T"
    by blast
  then show ?thesis
    using simply_connected_retraction_gen [OF T]
    by (metis (no_types) r retraction retraction_refl)
qed

lemma retract_of_homotopically_trivial:
  assumes ts: "T retract_of S"
      and hom: "\f g. \continuous_on U f; f \ U \ S;
                       continuous_on U g; g \<in> U \<rightarrow> S\<rbrakk>
                       \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) U S f g"
      and "continuous_on U f" "f \ U \ T"
      and "continuous_on U g" "g \ U \ T"
    shows "homotopic_with_canon (\x. True) U T f g"
proof -
  obtain r where "r \ S \ S" "continuous_on S r" "\x\S. r (r x) = r x" "T = r ` S"
    using ts by (auto simp: retract_of_def retraction)
  then obtain k where "Retracts S r T k"
    unfolding Retracts_def using continuous_on_id by blast
  then show ?thesis
    by (rule Retracts.homotopically_trivial_retraction_gen) (use assms hom in force)+
qed

lemma retract_of_homotopically_trivial_null:
  assumes ts: "T retract_of S"
      and hom: "\f. \continuous_on U f; f \ U \ S\
                     \<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. c)"
      and "continuous_on U f" "f \ U \ T"
  obtains c where "homotopic_with_canon (\x. True) U T f (\x. c)"
proof -
  obtain r where "r \ S \ S" "continuous_on S r" "\x\S. r (r x) = r x" "T = r ` S"
    using ts by (auto simp: retract_of_def retraction)
  then obtain k where "Retracts S r T k"
    unfolding Retracts_def by fastforce
  then show ?thesis
  proof (rule Retracts.homotopically_trivial_retraction_null_gen)
    show "\f. \continuous_on U f; f \ U \ S\
         \<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>a. True) U S f (\<lambda>x. c)"
      using hom by blast
  qed (use assms that in auto)
qed

lemma retraction_openin_vimage_iff:
  "openin (top_of_set S) (S \ r -` U) \ openin (top_of_set T) U"
  if "retraction S T r" and "U \ T"
  by (simp add: retraction_openin_vimage_iff that)

lemma retract_of_locally_compact:
    fixes S :: "'a :: {heine_borel,real_normed_vector} set"
    shows  "\ locally compact S; T retract_of S\ \ locally compact T"
  by (metis locally_compact_closedin closedin_retract)

lemma homotopic_into_retract:
  assumes fg: "f \ S \ T" "g \ S \ T"
  assumes "T retract_of U"
  assumes "homotopic_with_canon (\x. True) S U f g"
  shows "homotopic_with_canon (\x. True) S T f g"
proof -
  obtain h r where r: "retraction U T r"
     "continuous_on ({0..1::real} \ S) h"
      and h: "h \ {0..1} \ S \ U \ (\x. h (0, x) = f x) \ (\x. h (1, x) = g x)"
    using assms by (auto simp: homotopic_with_def retract_of_def)
  then have "continuous_on ({0..1} \ S) (r \ h)"
    by (metis continuous_on_compose continuous_on_subset funcset_image
        retraction_def)
  then show ?thesis
    using r fg h
    apply (simp add: retraction homotopic_with Pi_iff)
    by (smt (verit, best) imageI)
qed

lemma retract_of_locally_connected:
  assumes "locally connected T" "S retract_of T"
  shows "locally connected S"
  using assms
  by (metis retraction_openin_vimage_iff idempotent_imp_retraction locally_connected_quotient_image retract_ofE)

lemma retract_of_locally_path_connected:
  assumes "locally path_connected T" "S retract_of T"
  shows "locally path_connected S"
  using assms
  by (metis retraction_openin_vimage_iff idempotent_imp_retraction locally_path_connected_quotient_image retract_ofE)

text \<open>A few simple lemmas about deformation retracts\<close>

lemma deformation_retract_imp_homotopy_eqv:
  fixes S :: "'a::euclidean_space set"
  assumes "homotopic_with_canon (\x. True) S S id r" and r: "retraction S T r"
  shows "S homotopy_eqv T"
proof -
  have "homotopic_with_canon (\x. True) S S (id \ r) id"
    by (simp add: assms(1) homotopic_with_symD)
  moreover have "homotopic_with_canon (\x. True) T T (r \ id) id"
    using r unfolding retraction_def
    by (metis eq_id_iff homotopic_with_id2 topspace_euclidean_subtopology)
  ultimately
  show ?thesis
    unfolding homotopy_equivalent_space_def
    by (meson continuous_map_from_subtopology_mono continuous_map_id
        continuous_map_subtopology_eu r retraction_def)
qed

lemma deformation_retract:
  fixes S :: "'a::euclidean_space set"
    shows "(\r. homotopic_with_canon (\x. True) S S id r \ retraction S T r) \
           T retract_of S \<and> (\<exists>f. homotopic_with_canon (\<lambda>x. True) S S id f \<and> f \<in> S \<rightarrow> T)"
    (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (auto simp: retract_of_def retraction_def)
next
  assume R: ?rhs
  have "\r f. \T \ S; continuous_on S r; homotopic_with_canon (\x. True) S S id f;
            f \<in> S \<rightarrow> T; r \<in> S \<rightarrow> T; \<forall>x\<in>T. r x = x\<rbrakk>
           \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) S S f r"
    apply (rule_tac f = "r \ f" and g="r \ id" in homotopic_with_eq)
       apply (rule_tac Y=S in homotopic_with_compose_continuous_left)
         apply (auto simp: homotopic_with_sym Pi_iff)
    done
  with R homotopic_with_trans show ?lhs
    unfolding retract_of_def retraction_def by blast
qed

lemma deformation_retract_of_contractible_sing:
  fixes S :: "'a::euclidean_space set"
  assumes "contractible S" "a \ S"
  obtains r where "homotopic_with_canon (\x. True) S S id r" "retraction S {a} r"
proof -
  have "{a} retract_of S"
    by (simp add: \<open>a \<in> S\<close>)
  moreover have "homotopic_with_canon (\x. True) S S id (\x. a)"
      using assms
      by (auto simp: contractible_def homotopic_into_contractible image_subset_iff)
  moreover have "(\x. a) \ S \ {a}"
    by (simp add: image_subsetI)
  ultimately show ?thesis
    by (metis that deformation_retract)
qed

lemma continuous_on_compact_surface_projection_aux:
  fixes S :: "'a::t2_space set"
  assumes "compact S" "S \ T" "image q T \ S"
      and contp: "continuous_on T p"
      and "\x. x \ S \ q x = x"
      and [simp]: "\x. x \ T \ q(p x) = q x"
      and "\x. x \ T \ p(q x) = p x"
    shows "continuous_on T q"
proof -
  have *: "image p T = image p S"
    using assms by auto (metis imageI subset_iff)
  have contp': "continuous_on S p"
    by (rule continuous_on_subset [OF contp \<open>S \<subseteq> T\<close>])
  have "continuous_on (p ` T) q"
    by (simp add: "*" assms(1) assms(2) assms(5) continuous_on_inv contp' rev_subsetD)
  then have "continuous_on T (q \ p)"
    by (rule continuous_on_compose [OF contp])
  then show ?thesis
    by (rule continuous_on_eq [of _ "q \ p"]) (simp add: o_def)
qed

lemma continuous_on_compact_surface_projection:
  fixes S :: "'a::real_normed_vector set"
  assumes "compact S"
      and S: "S \ V - {0}" and "cone V"
      and iff: "\x k. x \ V - {0} \ 0 < k \ (k *\<^sub>R x) \ S \ d x = k"
  shows "continuous_on (V - {0}) (\x. d x *\<^sub>R x)"
proof (rule continuous_on_compact_surface_projection_aux [OF \<open>compact S\<close> S])
  show "(\x. d x *\<^sub>R x) ` (V - {0}) \ S"
    using iff by auto
  show "continuous_on (V - {0}) (\x. inverse(norm x) *\<^sub>R x)"
    by (intro continuous_intros) force
  show "\x. x \ S \ d x *\<^sub>R x = x"
    by (metis S zero_less_one local.iff scaleR_one subset_eq)
  show "d (x /\<^sub>R norm x) *\<^sub>R (x /\<^sub>R norm x) = d x *\<^sub>R x" if "x \ V - {0}" for x
    using iff [of "inverse(norm x) *\<^sub>R x" "norm x * d x", symmetric] iff that \cone V\
    by (simp add: field_simps cone_def zero_less_mult_iff)
  show "d x *\<^sub>R x /\<^sub>R norm (d x *\<^sub>R x) = x /\<^sub>R norm x" if "x \ V - {0}" for x
  proof -
    have "0 < d x"
      using local.iff that by blast
    then show ?thesis
      by simp
  qed
qed

subsection \<open>Kuhn Simplices\<close>

lemma bij_betw_singleton_eq:
  assumes f: "bij_betw f A B" and g: "bij_betw g A B" and a: "a \ A"
  assumes eq: "(\x. x \ A \ x \ a \ f x = g x)"
  shows "f a = g a"
proof -
  have "f ` (A - {a}) = g ` (A - {a})"
    by (intro image_cong) (simp_all add: eq)
  then have "B - {f a} = B - {g a}"
    using f g a  by (auto simp: bij_betw_def inj_on_image_set_diff set_eq_iff)
  moreover have "f a \ B" "g a \ B"
    using f g a by (auto simp: bij_betw_def)
  ultimately show ?thesis
    by auto
qed

lemmas swap_apply1 = swap_apply(1)
lemmas swap_apply2 = swap_apply(2)

lemma pointwise_minimal_pointwise_maximal:
  fixes s :: "(nat \ nat) set"
  assumes "finite s"
    and "s \ {}"
    and "\x\s. \y\s. x \ y \ y \ x"
  shows "\a\s. \x\s. a \ x"
    and "\a\s. \x\s. x \ a"
  using assms
proof (induct s rule: finite_ne_induct)
  case (insert b s)
  assume *: "\x\insert b s. \y\insert b s. x \ y \ y \ x"
  then obtain u l where "l \ s" "\b\s. l \ b" "u \ s" "\b\s. b \ u"
    using insert by auto
  with * show "\a\insert b s. \x\insert b s. a \ x" "\a\insert b s. \x\insert b s. x \ a"
    by (metis insert_iff order.trans)+
qed auto

lemma kuhn_labelling_lemma:
  fixes P Q :: "'a::euclidean_space \ bool"
  assumes "\x. P x \ P (f x)"
    and "\x. P x \ (\i\Basis. Q i \ 0 \ x\i \ x\i \ 1)"
  shows "\l. (\x.\i\Basis. l x i \ (1::nat)) \
             (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 0) \<longrightarrow> (l x i = 0)) \<and>
             (\<forall>x.\<forall>i\<in>Basis. P x \<and> Q i \<and> (x\<bullet>i = 1) \<longrightarrow> (l x i = 1)) \<and>
             (\<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>
             (\<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)"
proof -
  { fix x i
    let ?R = "\y. (P x \ Q i \ x \ i = 0 \ y = (0::nat)) \
        (P x \<and> Q i \<and> x \<bullet> i = 1 \<longrightarrow> y = 1) \<and>
        (P x \<and> Q i \<and> y = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i) \<and>
        (P x \<and> Q i \<and> y = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i)"
    { assume "P x" "Q i" "i \ Basis" with assms have "0 \ f x \ i \ f x \ i \ 1" by auto }
    then have "i \ Basis \ ?R 0 \ ?R 1" by auto }
  then show ?thesis
    unfolding all_conj_distrib[symmetric] Ball_def (* FIXME: shouldn't this work by metis? *)
    by (subst choice_iff[symmetric])+ blast
qed

subsubsection \<open>The key "counting" observation, somewhat abstracted\<close>

lemma kuhn_counting_lemma:
  fixes bnd compo compo' face S F
  defines "nF s == card {f\F. face f s \ compo' f}"
  assumes [simp, intro]: "finite F" \<comment> \<open>faces\<close> and [simp, intro]: "finite S" \<comment> \<open>simplices\<close>
    and "\f. f \ F \ bnd f \ card {s\S. face f s} = 1"
    and "\f. f \ F \ \ bnd f \ card {s\S. face f s} = 2"
    and "\s. s \ S \ compo s \ nF s = 1"
    and "\s. s \ S \ \ compo s \ nF s = 0 \ nF s = 2"
    and "odd (card {f\F. compo' f \ bnd f})"
  shows "odd (card {s\S. compo s})"
proof -
  have "(\s | s \ S \ \ compo s. nF s) + (\s | s \ S \ compo s. nF s) = (\s\S. nF s)"
    by (subst sum.union_disjoint[symmetric]) (auto intro!: sum.cong)
  also have "\ = (\s\S. card {f \ {f\F. compo' f \ bnd f}. face f s}) +
                  (\<Sum>s\<in>S. card {f \<in> {f\<in>F. compo' f \<and> \<not> bnd f}. face f s})"
    unfolding sum.distrib[symmetric]
    by (subst card_Un_disjoint[symmetric])
       (auto simp: nF_def intro!: sum.cong arg_cong[where f=card])
  also have "\ = 1 * card {f\F. compo' f \ bnd f} + 2 * card {f\F. compo' f \ \ bnd f}"
    using assms(4,5) by (fastforce intro!: arg_cong2[where f="(+)"] sum_multicount)
  finally have "odd ((\s | s \ S \ \ compo s. nF s) + card {s\S. compo s})"
    using assms(6,8) by simp
  moreover have "(\s | s \ S \ \ compo s. nF s) =
    (\<Sum>s | s \<in> S \<and> \<not> compo s \<and> nF s = 0. nF s) + (\<Sum>s | s \<in> S \<and> \<not> compo s \<and> nF s = 2. nF s)"
    using assms(7) by (subst sum.union_disjoint[symmetric]) (fastforce intro!: sum.cong)+
  ultimately show ?thesis
    by auto
qed

subsubsection \<open>The odd/even result for faces of complete vertices, generalized\<close>

lemma kuhn_complete_lemma:
  assumes [simp]: "finite simplices"
    and face: "\f s. face f s \ (\a\s. f = s - {a})"
    and card_s[simp]:  "\s. s \ simplices \ card s = n + 2"
    and rl_bd: "\s. s \ simplices \ rl ` s \ {..Suc n}"
    and bnd: "\f s. s \ simplices \ face f s \ bnd f \ card {s\simplices. face f s} = 1"
    and nbnd: "\f s. s \ simplices \ face f s \ \ bnd f \ card {s\simplices. face f s} = 2"
    and odd_card: "odd (card {f. (\s\simplices. face f s) \ rl ` f = {..n} \ bnd f})"
  shows "odd (card {s\simplices. (rl ` s = {..Suc n})})"
proof (rule kuhn_counting_lemma)
  have finite_s[simp]: "\s. s \ simplices \ finite s"
    by (metis add_is_0 zero_neq_numeral card.infinite assms(3))

  let ?F = "{f. \s\simplices. face f s}"
  have F_eq: "?F = (\s\simplices. \a\s. {s - {a}})"
    by (auto simp: face)
  show "finite ?F"
    using \<open>finite simplices\<close> unfolding F_eq by auto

  show "card {s \ simplices. face f s} = 1" if "f \ ?F" "bnd f" for f
    using bnd that by auto

  show "card {s \ simplices. face f s} = 2" if "f \ ?F" "\ bnd f" for f
    using nbnd that by auto

  show "odd (card {f \ {f. \s\simplices. face f s}. rl ` f = {..n} \ bnd f})"
    using odd_card by simp

  fix s assume s[simp]: "s \ simplices"
  let ?S = "{f \ {f. \s\simplices. face f s}. face f s \ rl ` f = {..n}}"
  have "?S = (\a. s - {a}) ` {a\s. rl ` (s - {a}) = {..n}}"
    using s by (fastforce simp: face)
  then have card_S: "card ?S = card {a\s. rl ` (s - {a}) = {..n}}"
    by (auto intro!: card_image inj_onI)

  { assume rl: "rl ` s = {..Suc n}"
    then have inj_rl: "inj_on rl s"
      by (intro eq_card_imp_inj_on) auto
    moreover obtain a where "rl a = Suc n" "a \ s"
      by (metis atMost_iff image_iff le_Suc_eq rl)
    ultimately have n: "{..n} = rl ` (s - {a})"
      by (auto simp: inj_on_image_set_diff rl)
    have "{a\s. rl ` (s - {a}) = {..n}} = {a}"
      using inj_rl \<open>a \<in> s\<close> by (auto simp: n inj_on_image_eq_iff[OF inj_rl])
    then show "card ?S = 1"
      unfolding card_S by simp }

  { assume rl: "rl ` s \ {..Suc n}"
    show "card ?S = 0 \ card ?S = 2"
    proof cases
      assume *: "{..n} \ rl ` s"
      with rl rl_bd[OF s] have rl_s: "rl ` s = {..n}"
        by (auto simp: atMost_Suc subset_insert_iff split: if_split_asm)
      then have "\ inj_on rl s"
        by (intro pigeonhole) simp
      then obtain a b where ab: "a \ s" "b \ s" "rl a = rl b" "a \ b"
        by (auto simp: inj_on_def)
      then have eq: "rl ` (s - {a}) = rl ` s"
        by auto
      with ab have inj: "inj_on rl (s - {a})"
        by (intro eq_card_imp_inj_on) (auto simp: rl_s card_Diff_singleton_if)

      { fix x assume "x \ s" "x \ {a, b}"
        then have "rl ` s - {rl x} = rl ` ((s - {a}) - {x})"
          by (auto simp: eq inj_on_image_set_diff[OF inj])
        also have "\ = rl ` (s - {x})"
          using ab \<open>x \<notin> {a, b}\<close> by auto
        also assume "\ = rl ` s"
        finally have False
          using \<open>x\<in>s\<close> by auto }
      moreover
      { fix x assume "x \ {a, b}" with ab have "x \ s \ rl ` (s - {x}) = rl ` s"
          by (simp add: set_eq_iff image_iff Bex_def) metis }
      ultimately have "{a\s. rl ` (s - {a}) = {..n}} = {a, b}"
        unfolding rl_s[symmetric] by fastforce
      with \<open>a \<noteq> b\<close> show "card ?S = 0 \<or> card ?S = 2"
        unfolding card_S by simp
    next
      assume "\ {..n} \ rl ` s"
      then have "\x. rl ` (s - {x}) \ {..n}"
        by auto
      then show "card ?S = 0 \ card ?S = 2"
        unfolding card_S by simp
    qed }
qed fact

locale kuhn_simplex =
  fixes p n and base upd and S :: "(nat \ nat) set"
  assumes base: "base \ {..< n} \ {..< p}"
  assumes base_out: "\i. n \ i \ base i = p"
  assumes upd: "bij_betw upd {..< n} {..< n}"
  assumes s_pre: "S = (\i j. if j \ upd`{..< i} then Suc (base j) else base j) ` {.. n}"
begin

definition "enum i j = (if j \ upd`{..< i} then Suc (base j) else base j)"

lemma s_eq: "S = enum ` {.. n}"
  unfolding s_pre enum_def[abs_def] ..

lemma upd_space: "i < n \ upd i < n"
  using upd by (auto dest!: bij_betwE)

lemma s_space: "S \ {..< n} \ {.. p}"
proof -
  { fix i assume "i \ n" then have "enum i \ {..< n} \ {.. p}"
    proof (induct i)
      case 0 then show ?case
        using base by (auto simp: Pi_iff less_imp_le enum_def)
    next
      case (Suc i) with base show ?case
        by (auto simp: Pi_iff Suc_le_eq less_imp_le enum_def intro: upd_space)
    qed }
  then show ?thesis
    by (auto simp: s_eq)
qed

lemma inj_upd: "inj_on upd {..< n}"
  using upd by (simp add: bij_betw_def)

lemma inj_enum: "inj_on enum {.. n}"
proof -
  { fix x y :: nat assume "x \ y" "x \ n" "y \ n"
    with upd have "upd ` {..< x} \ upd ` {..< y}"
      by (subst inj_on_image_eq_iff[where C="{..< n}"]) (auto simp: bij_betw_def)
    then have "enum x \ enum y"
      by (auto simp: enum_def fun_eq_iff) }
  then show ?thesis
    by (auto simp: inj_on_def)
qed

lemma enum_0: "enum 0 = base"
  by (simp add: enum_def[abs_def])

lemma base_in_s: "base \ S"
  unfolding s_eq by (subst enum_0[symmetric]) auto

lemma enum_in: "i \ n \ enum i \ S"
  unfolding s_eq by auto

lemma one_step:
  assumes a: "a \ S" "j < n"
  assumes *: "\a'. a' \ S \ a' \ a \ a' j = p'"
  shows "a j \ p'"
proof
  assume "a j = p'"
  with * a have "\a'. a' \ S \ a' j = p'"
    by auto
  then have "\i. i \ n \ enum i j = p'"
    unfolding s_eq by auto
  from this[of 0] this[of n] have "j \ upd ` {..< n}"
    by (auto simp: enum_def fun_eq_iff split: if_split_asm)
  with upd \<open>j < n\<close> show False
    by (auto simp: bij_betw_def)
qed

lemma upd_inj: "i < n \ j < n \ upd i = upd j \ i = j"
  using upd by (auto simp: bij_betw_def inj_on_eq_iff)

lemma upd_surj: "upd ` {..< n} = {..< n}"
  using upd by (auto simp: bij_betw_def)

lemma in_upd_image: "A \ {..< n} \ i < n \ upd i \ upd ` A \ i \ A"
  using inj_on_image_mem_iff[of upd "{..< n}"] upd
  by (auto simp: bij_betw_def)

lemma enum_inj: "i \ n \ j \ n \ enum i = enum j \ i = j"
  using inj_enum by (auto simp: inj_on_eq_iff)

lemma in_enum_image: "A \ {.. n} \ i \ n \ enum i \ enum ` A \ i \ A"
  using inj_on_image_mem_iff[OF inj_enum] by auto

lemma enum_mono: "i \ n \ j \ n \ enum i \ enum j \ i \ j"
  by (auto simp: enum_def le_fun_def in_upd_image Ball_def[symmetric])

lemma enum_strict_mono: "i \ n \ j \ n \ enum i < enum j \ i < j"
  using enum_mono[of i j] enum_inj[of i j] by (auto simp: le_less)

lemma chain: "a \ S \ b \ S \ a \ b \ b \ a"
  by (auto simp: s_eq enum_mono)

lemma less: "a \ S \ b \ S \ a i < b i \ a < b"
  using chain[of a b] by (auto simp: less_fun_def le_fun_def not_le[symmetric])

lemma enum_0_bot: "a \ S \ a = enum 0 \ (\a'\S. a \ a')"
  unfolding s_eq by (auto simp: enum_mono Ball_def)

lemma enum_n_top: "a \ S \ a = enum n \ (\a'\S. a' \ a)"
  unfolding s_eq by (auto simp: enum_mono Ball_def)

lemma enum_Suc: "i < n \ enum (Suc i) = (enum i)(upd i := Suc (enum i (upd i)))"
  by (auto simp: fun_eq_iff enum_def upd_inj)

lemma enum_eq_p: "i \ n \ n \ j \ enum i j = p"
  by (induct i) (auto simp: enum_Suc enum_0 base_out upd_space not_less[symmetric])

lemma out_eq_p: "a \ S \ n \ j \ a j = p"
  unfolding s_eq by (auto simp: enum_eq_p)

lemma s_le_p: "a \ S \ a j \ p"
  using out_eq_p[of a j] s_space by (cases "j < n") auto

lemma le_Suc_base: "a \ S \ a j \ Suc (base j)"
  unfolding s_eq by (auto simp: enum_def)

lemma base_le: "a \ S \ base j \ a j"
  unfolding s_eq by (auto simp: enum_def)

lemma enum_le_p: "i \ n \ j < n \ enum i j \ p"
  using enum_in[of i] s_space by auto

lemma enum_less: "a \ S \ i < n \ enum i < a \ enum (Suc i) \ a"
  unfolding s_eq by (auto simp: enum_strict_mono enum_mono)

lemma ksimplex_0:
  "n = 0 \ S = {(\x. p)}"
  using s_eq enum_def base_out by auto

lemma replace_0:
  assumes "j < n" "a \ S" and p: "\x\S - {a}. x j = 0" and "x \ S"
  shows "x \ a"
proof cases
  assume "x \ a"
  have "a j \ 0"
    using assms by (intro one_step[where a=a]) auto
  with less[OF \<open>x\<in>S\<close> \<open>a\<in>S\<close>, of j] p[rule_format, of x] \<open>x \<in> S\<close> \<open>x \<noteq> a\<close>
  show ?thesis
    by auto
qed simp

lemma replace_1:
  assumes "j < n" "a \ S" and p: "\x\S - {a}. x j = p" and "x \ S"
  shows "a \ x"
proof cases
  assume "x \ a"
  have "a j \ p"
    using assms by (intro one_step[where a=a]) auto
  with enum_le_p[of _ j] \<open>j < n\<close> \<open>a\<in>S\<close>
  have "a j < p"
    by (auto simp: less_le s_eq)
  with less[OF \<open>a\<in>S\<close> \<open>x\<in>S\<close>, of j] p[rule_format, of x] \<open>x \<in> S\<close> \<open>x \<noteq> a\<close>
  show ?thesis
    by auto
qed simp

end

locale kuhn_simplex_pair = s: kuhn_simplex p n b_s u_s s + t: kuhn_simplex p n b_t u_t t
  for p n b_s u_s s b_t u_t t
begin

lemma enum_eq:
  assumes l: "i \ l" "l \ j" and "j + d \ n"
  assumes eq: "s.enum ` {i .. j} = t.enum ` {i + d .. j + d}"
  shows "s.enum l = t.enum (l + d)"
using l proof (induct l rule: dec_induct)
  case base
  then have s: "s.enum i \ t.enum ` {i + d .. j + d}" and t: "t.enum (i + d) \ s.enum ` {i .. j}"
    using eq by auto
  from t \<open>i \<le> j\<close> \<open>j + d \<le> n\<close> have "s.enum i \<le> t.enum (i + d)"
    by (auto simp: s.enum_mono)
  moreover from s \<open>i \<le> j\<close> \<open>j + d \<le> n\<close> have "t.enum (i + d) \<le> s.enum i"
    by (auto simp: t.enum_mono)
  ultimately show ?case
    by auto
next
  case (step l)
  moreover from step.prems \<open>j + d \<le> n\<close> have
      "s.enum l < s.enum (Suc l)"
      "t.enum (l + d) < t.enum (Suc l + d)"
    by (simp_all add: s.enum_strict_mono t.enum_strict_mono)
  moreover have
      "s.enum (Suc l) \ t.enum ` {i + d .. j + d}"
      "t.enum (Suc l + d) \ s.enum ` {i .. j}"
    using step \<open>j + d \<le> n\<close> eq by (auto simp: s.enum_inj t.enum_inj)
  ultimately have "s.enum (Suc l) = t.enum (Suc (l + d))"
    using \<open>j + d \<le> n\<close>
    by (intro antisym s.enum_less[THEN iffD1] t.enum_less[THEN iffD1])
       (auto intro!: s.enum_in t.enum_in)
  then show ?case by simp
qed

lemma ksimplex_eq_bot:
  assumes a: "a \ s" "\a'. a' \ s \ a \ a'"
  assumes b: "b \ t" "\b'. b' \ t \ b \ b'"
  assumes eq: "s - {a} = t - {b}"
  shows "s = t"
proof cases
  assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp
next
  assume "n \ 0"
  have "s.enum 0 = (s.enum (Suc 0)) (u_s 0 := s.enum (Suc 0) (u_s 0) - 1)"
       "t.enum 0 = (t.enum (Suc 0)) (u_t 0 := t.enum (Suc 0) (u_t 0) - 1)"
    using \<open>n \<noteq> 0\<close> by (simp_all add: s.enum_Suc t.enum_Suc)
  moreover have e0: "a = s.enum 0" "b = t.enum 0"
    using a b by (simp_all add: s.enum_0_bot t.enum_0_bot)
  moreover
  { fix j assume "0 < j" "j \ n"
    moreover have "s - {a} = s.enum ` {Suc 0 .. n}" "t - {b} = t.enum ` {Suc 0 .. n}"
      unfolding s.s_eq t.s_eq e0 by (auto simp: s.enum_inj t.enum_inj)
    ultimately have "s.enum j = t.enum j"
      using enum_eq[of "1" j n 0] eq by auto }
  note enum_eq = this
  then have "s.enum (Suc 0) = t.enum (Suc 0)"
    using \<open>n \<noteq> 0\<close> by auto
  moreover
  { fix j assume "Suc j < n"
    with enum_eq[of "Suc j"] enum_eq[of "Suc (Suc j)"]
    have "u_s (Suc j) = u_t (Suc j)"
      using s.enum_Suc[of "Suc j"] t.enum_Suc[of "Suc j"]
      by (auto simp: fun_eq_iff split: if_split_asm) }
  then have "\j. 0 < j \ j < n \ u_s j = u_t j"
    by (auto simp: gr0_conv_Suc)
  with \<open>n \<noteq> 0\<close> have "u_t 0 = u_s 0"
    by (intro bij_betw_singleton_eq[OF t.upd s.upd, of 0]) auto
  ultimately have "a = b"
    by simp
  with assms show "s = t"
    by auto
qed

lemma ksimplex_eq_top:
  assumes a: "a \ s" "\a'. a' \ s \ a' \ a"
  assumes b: "b \ t" "\b'. b' \ t \ b' \ b"
  assumes eq: "s - {a} = t - {b}"
  shows "s = t"
proof (cases n)
  assume "n = 0" with s.ksimplex_0 t.ksimplex_0 show ?thesis by simp
next
  case (Suc n')
  have "s.enum n = (s.enum n') (u_s n' := Suc (s.enum n' (u_s n')))"
       "t.enum n = (t.enum n') (u_t n' := Suc (t.enum n' (u_t n')))"
    using Suc by (simp_all add: s.enum_Suc t.enum_Suc)
  moreover have en: "a = s.enum n" "b = t.enum n"
    using a b by (simp_all add: s.enum_n_top t.enum_n_top)
  moreover
  { fix j assume "j < n"
    moreover have "s - {a} = s.enum ` {0 .. n'}" "t - {b} = t.enum ` {0 .. n'}"
      unfolding s.s_eq t.s_eq en by (auto simp: s.enum_inj t.enum_inj Suc)
    ultimately have "s.enum j = t.enum j"
      using enum_eq[of "0" j n' 0] eq Suc by auto }
  note enum_eq = this
  then have "s.enum n' = t.enum n'"
    using Suc by auto
  moreover
  { fix j assume "j < n'"
    with enum_eq[of j] enum_eq[of "Suc j"]
    have "u_s j = u_t j"
      using s.enum_Suc[of j] t.enum_Suc[of j]
      by (auto simp: Suc fun_eq_iff split: if_split_asm) }
  then have "\j. j < n' \ u_s j = u_t j"
    by (auto simp: gr0_conv_Suc)
  then have "u_t n' = u_s n'"
    by (intro bij_betw_singleton_eq[OF t.upd s.upd, of n']) (auto simp: Suc)
  ultimately have "a = b"
    by simp
  with assms show "s = t"
    by auto
qed

end

inductive ksimplex for p n :: nat where
  ksimplex: "kuhn_simplex p n base upd s \ ksimplex p n s"

lemma finite_ksimplexes: "finite {s. ksimplex p n s}"
proof (rule finite_subset)
  { fix a s assume "ksimplex p n s" "a \ s"
    then obtain b u where "kuhn_simplex p n b u s" by (auto elim: ksimplex.cases)
    then interpret kuhn_simplex p n b u s .
    from s_space \<open>a \<in> s\<close> out_eq_p[OF \<open>a \<in> s\<close>]
    have "a \ (\f x. if n \ x then p else f x) ` ({..< n} \\<^sub>E {.. p})"
      by (auto simp: image_iff subset_eq Pi_iff split: if_split_asm
               intro!: bexI[of _ "restrict a {..< n}"]) }
  then show "{s. ksimplex p n s} \ Pow ((\f x. if n \ x then p else f x) ` ({..< n} \\<^sub>E {.. p}))"
    by auto
qed (simp add: finite_PiE)

lemma ksimplex_card:
  assumes "ksimplex p n s" shows "card s = Suc n"
using assms proof cases
  case (ksimplex u b)
  then interpret kuhn_simplex p n u b s .
  show ?thesis
    by (simp add: card_image s_eq inj_enum)
qed

lemma simplex_top_face:
  assumes "0 < p" "\x\s'. x n = p"
  shows "ksimplex p n s' \ (\s a. ksimplex p (Suc n) s \ a \ s \ s' = s - {a})"
  using assms
proof safe
  fix s a assume "ksimplex p (Suc n) s" and a: "a \ s" and na: "\x\s - {a}. x n = p"
  then show "ksimplex p n (s - {a})"
  proof cases
    case (ksimplex base upd)
    then interpret kuhn_simplex p "Suc n" base upd "s" .

    have "a n < p"
      using one_step[of a n p] na \<open>a\<in>s\<close> s_space by (auto simp: less_le)
    then have "a = enum 0"
      using \<open>a \<in> s\<close> na by (subst enum_0_bot) (auto simp: le_less intro!: less[of a _ n])
    then have s_eq: "s - {a} = enum ` Suc ` {.. n}"
      using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident in_enum_image subset_eq)
    then have "enum 1 \ s - {a}"
      by auto
    then have "upd 0 = n"
      using \<open>a n < p\<close> \<open>a = enum 0\<close> na[rule_format, of "enum 1"]
      by (auto simp: fun_eq_iff enum_Suc split: if_split_asm)
    then have "bij_betw upd (Suc ` {..< n}) {..< n}"
      using upd
      by (subst notIn_Un_bij_betw3[where b=0])
         (auto simp: lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0)
    then have "bij_betw (upd\Suc) {..
      by (rule bij_betw_trans[rotated]) (auto simp: bij_betw_def)

    have "a n = p - 1"
      using enum_Suc[of 0] na[rule_format, OF \<open>enum 1 \<in> s - {a}\<close>] \<open>a = enum 0\<close> by (auto simp: \<open>upd 0 = n\<close>)

    show ?thesis
    proof (rule ksimplex.intros, standard)
      show "bij_betw (upd\Suc) {..< n} {..< n}" by fact
      show "base(n := p) \ {.. {..i. n\i \ (base(n := p)) i = p"
        using base base_out by (auto simp: Pi_iff)

      have "\i. Suc ` {..< i} = {..< Suc i} - {0}"
        by (auto simp: image_iff Ball_def) arith
      then have upd_Suc: "\i. i \ n \ (upd\Suc) ` {..< i} = upd ` {..< Suc i} - {n}"
        using \<open>upd 0 = n\<close> upd_inj by (auto simp add: image_iff less_Suc_eq_0_disj)
      have n_in_upd: "\i. n \ upd ` {..< Suc i}"
        using \<open>upd 0 = n\<close> by auto

      define f' where "f' i j =
        (if j \<in> (upd\<circ>Suc)`{..< i} then Suc ((base(n := p)) j) else (base(n := p)) j)" for i j
      { fix x i
        assume i [arith]: "i \ n"
        with upd_Suc have "(upd \ Suc) ` {..
        with \<open>a n < p\<close> \<open>a = enum 0\<close> \<open>upd 0 = n\<close> \<open>a n = p - 1\<close>
        have "enum (Suc i) x = f' i x"
          by (auto simp add: f'_def enum_def) }
      then show "s - {a} = f' ` {.. n}"
        unfolding s_eq image_comp by (intro image_cong) auto
    qed
  qed
next
  assume "ksimplex p n s'" and *: "\x\s'. x n = p"
  then show "\s a. ksimplex p (Suc n) s \ a \ s \ s' = s - {a}"
  proof cases
    case (ksimplex base upd)
    then interpret kuhn_simplex p n base upd s' .
    define b where "b = base (n := p - 1)"
    define u where "u i = (case i of 0 \ n | Suc i \ upd i)" for i

    have "ksimplex p (Suc n) (s' \ {b})"
    proof (rule ksimplex.intros, standard)
      show "b \ {.. {..
        using base \<open>0 < p\<close> unfolding lessThan_Suc b_def by (auto simp: PiE_iff)
      show "\i. Suc n \ i \ b i = p"
        using base_out by (auto simp: b_def)

      have "bij_betw u (Suc ` {..< n} \ {0}) ({.. {u 0})"
        using upd
        by (intro notIn_Un_bij_betw) (auto simp: u_def bij_betw_def image_comp comp_def inj_on_def)
      then show "bij_betw u {..
        by (simp add: u_def lessThan_Suc[symmetric] lessThan_Suc_eq_insert_0)

      define f' where "f' i j = (if j \<in> u`{..< i} then Suc (b j) else b j)" for i j

      have u_eq: "\i. i \ n \ u ` {..< Suc i} = upd ` {..< i} \ { n }"
        by (auto simp: u_def image_iff upd_inj Ball_def split: nat.split) arith

      { fix x have "x \ n \ n \ upd ` {..
          using upd_space by (simp add: image_iff neq_iff) }
      note n_not_upd = this

      have *: "f' ` {.. Suc n} = f' ` (Suc ` {.. n} \ {0})"
        unfolding atMost_Suc_eq_insert_0 by simp
      also have "\ = (f' \ Suc) ` {.. n} \ {b}"
        by (auto simp: f'_def)
      also have "(f' \ Suc) ` {.. n} = s'"
        using \<open>0 < p\<close> base_out[of n]
        unfolding s_eq enum_def[abs_def] f'_def[abs_def] upd_space
        by (intro image_cong) (simp_all add: u_eq b_def fun_eq_iff n_not_upd)
      finally show "s' \ {b} = f' ` {.. Suc n}" ..
    qed
    moreover have "b \ s'"
      using * \<open>0 < p\<close> by (auto simp: b_def)
    ultimately show ?thesis by auto
  qed
qed

lemma ksimplex_replace_0:
  assumes s: "ksimplex p n s" and a: "a \ s"
  assumes j: "j < n" and p: "\x\s - {a}. x j = 0"
  shows "card {s'. ksimplex p n s' \ (\b\s'. s' - {b} = s - {a})} = 1"
  using s
proof cases
  case (ksimplex b_s u_s)

  { fix t b assume "ksimplex p n t"
    then obtain b_t u_t where "kuhn_simplex p n b_t u_t t"
      by (auto elim: ksimplex.cases)
    interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t
      by intro_locales fact+

    assume b: "b \ t" "t - {b} = s - {a}"
    with a j p s.replace_0[of _ a] t.replace_0[of _ b] have "s = t"
      by (intro ksimplex_eq_top[of a b]) auto }
  then have "{s'. ksimplex p n s' \ (\b\s'. s' - {b} = s - {a})} = {s}"
    using s \<open>a \<in> s\<close> by auto
  then show ?thesis
    by simp
qed

lemma ksimplex_replace_1:
  assumes s: "ksimplex p n s" and a: "a \ s"
  assumes j: "j < n" and p: "\x\s - {a}. x j = p"
  shows "card {s'. ksimplex p n s' \ (\b\s'. s' - {b} = s - {a})} = 1"
  using s
proof cases
  case (ksimplex b_s u_s)

  { fix t b assume "ksimplex p n t"
    then obtain b_t u_t where "kuhn_simplex p n b_t u_t t"
      by (auto elim: ksimplex.cases)
    interpret kuhn_simplex_pair p n b_s u_s s b_t u_t t
      by intro_locales fact+

    assume b: "b \ t" "t - {b} = s - {a}"
    with a j p s.replace_1[of _ a] t.replace_1[of _ b] have "s = t"
      by (intro ksimplex_eq_bot[of a b]) auto }
  then have "{s'. ksimplex p n s' \ (\b\s'. s' - {b} = s - {a})} = {s}"
    using s \<open>a \<in> s\<close> by auto
  then show ?thesis
    by simp
qed

lemma ksimplex_replace_2:
  assumes s: "ksimplex p n s" and "a \ s" and "n \ 0"
    and lb: "\jx\s - {a}. x j \ 0"
    and ub: "\jx\s - {a}. x j \ p"
  shows "card {s'. ksimplex p n s' \ (\b\s'. s' - {b} = s - {a})} = 2"
  using s
proof cases
  case (ksimplex base upd)
  then interpret kuhn_simplex p n base upd s .

  from \<open>a \<in> s\<close> obtain i where "i \<le> n" "a = enum i"
    unfolding s_eq by auto

  from \<open>i \<le> n\<close> have "i = 0 \<or> i = n \<or> (0 < i \<and> i < n)"
    by linarith
  then have "\!s'. s' \ s \ ksimplex p n s' \ (\b\s'. s - {a} = s'- {b})"
  proof (elim disjE conjE)
    assume "i = 0"
    define rot where [abs_def]: "rot i = (if i + 1 = n then 0 else i + 1)" for i
    let ?upd = "upd \ rot"

    have rot: "bij_betw rot {..< n} {..< n}"
      by (auto simp: bij_betw_def inj_on_def image_iff Ball_def rot_def)
         arith+
    from rot upd have "bij_betw ?upd {..
      by (rule bij_betw_trans)

    define f' where [abs_def]: "f' i j =
      (if j \<in> ?upd`{..< i} then Suc (enum (Suc 0) j) else enum (Suc 0) j)" for i j

    interpret b: kuhn_simplex p n "enum (Suc 0)" "upd \ rot" "f' ` {.. n}"
    proof
      from \<open>a = enum i\<close> ub \<open>n \<noteq> 0\<close> \<open>i = 0\<close>
      obtain i' where "i' \<le> n" "enum i' \<noteq> enum 0" "enum i' (upd 0) \<noteq> p"
        unfolding s_eq by (auto intro: upd_space simp: enum_inj)
      then have "enum 1 \ enum i'" "enum i' (upd 0) < p"
        using enum_le_p[of i' "upd 0"] by (auto simp: enum_inj enum_mono upd_space)
      then have "enum 1 (upd 0) < p"
        by (auto simp: le_fun_def intro: le_less_trans)
      then show "enum (Suc 0) \ {.. {..
        using base \<open>n \<noteq> 0\<close> by (auto simp: enum_0 enum_Suc PiE_iff extensional_def upd_space)

      { fix i assume "n \ i" then show "enum (Suc 0) i = p"
        using \<open>n \<noteq> 0\<close> by (auto simp: enum_eq_p) }
      show "bij_betw ?upd {.. by fact
    qed (simp add: f'_def)
    have ks_f': "ksimplex p n (f' ` {.. n})"
      by rule unfold_locales

    have b_enum: "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
    with b.inj_enum have inj_f': "inj_on f' {.. n}" by simp

    have f'_eq_enum: "f' j = enum (Suc j)" if "j < n" for j
    proof -
      from that have "rot ` {..< j} = {0 <..< Suc j}"
        by (auto simp: rot_def image_Suc_lessThan cong: image_cong_simp)
      with that \<open>n \<noteq> 0\<close> show ?thesis
        by (simp only: f'_def enum_def fun_eq_iff image_comp [symmetric])
          (auto simp add: upd_inj)
    qed
    then have "enum ` Suc ` {..< n} = f' ` {..< n}"
      by (force simp: enum_inj)
    also have "Suc ` {..< n} = {.. n} - {0}"
      by (auto simp: image_iff Ball_def) arith
    also have "{..< n} = {.. n} - {n}"
      by auto
    finally have eq: "s - {a} = f' ` {.. n} - {f' n}"
      unfolding s_eq \<open>a = enum i\<close> \<open>i = 0\<close>
      by (simp add: inj_on_image_set_diff[OF inj_enum] inj_on_image_set_diff[OF inj_f'])

    have "enum 0 < f' 0"
      using \<open>n \<noteq> 0\<close> by (simp add: enum_strict_mono f'_eq_enum)
    also have "\ < f' n"
      using \<open>n \<noteq> 0\<close> b.enum_strict_mono[of 0 n] unfolding b_enum by simp
    finally have "a \ f' n"
      using \<open>a = enum i\<close> \<open>i = 0\<close> by auto

    { fix t c assume "ksimplex p n t" "c \ t" and eq_sma: "s - {a} = t - {c}"
      obtain b u where "kuhn_simplex p n b u t"
        using \<open>ksimplex p n t\<close> by (auto elim: ksimplex.cases)
      then interpret t: kuhn_simplex p n b u t .

      { fix x assume "x \ s" "x \ a"
         then have "x (upd 0) = enum (Suc 0) (upd 0)"
           by (auto simp: \<open>a = enum i\<close> \<open>i = 0\<close> s_eq enum_def enum_inj) }
      then have eq_upd0: "\x\t-{c}. x (upd 0) = enum (Suc 0) (upd 0)"
        unfolding eq_sma[symmetric] by auto
      then have "c (upd 0) \ enum (Suc 0) (upd 0)"
        using \<open>n \<noteq> 0\<close> by (intro t.one_step[OF \<open>c\<in>t\<close> ]) (auto simp: upd_space)
      then have "c (upd 0) < enum (Suc 0) (upd 0) \ c (upd 0) > enum (Suc 0) (upd 0)"
        by auto
      then have "t = s \ t = f' ` {..n}"
      proof (elim disjE conjE)
        assume *: "c (upd 0) < enum (Suc 0) (upd 0)"
        interpret st: kuhn_simplex_pair p n base upd s b u t ..
        { fix x assume "x \ t" with * \c\t\ eq_upd0[rule_format, of x] have "c \ x"
            by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
        note top = this
        have "s = t"
          using \<open>a = enum i\<close> \<open>i = 0\<close> \<open>c \<in> t\<close>
          by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq_sma])
             (auto simp: s_eq enum_mono t.s_eq t.enum_mono top)
        then show ?thesis by simp
      next
        assume *: "c (upd 0) > enum (Suc 0) (upd 0)"
        interpret st: kuhn_simplex_pair p n "enum (Suc 0)" "upd \ rot" "f' ` {.. n}" b u t ..
        have eq: "f' ` {..n} - {f' n} = t - {c}"
          using eq_sma eq by simp
        { fix x assume "x \ t" with * \c\t\ eq_upd0[rule_format, of x] have "x \ c"
            by (auto simp: le_less intro!: t.less[of _ _ "upd 0"]) }
        note top = this
        have "f' ` {..n} = t"
          using \<open>a = enum i\<close> \<open>i = 0\<close> \<open>c \<in> t\<close>
          by (intro st.ksimplex_eq_top[OF _ _ _ _ eq])
             (auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono b_enum[symmetric] top)
        then show ?thesis by simp
      qed }
    with ks_f' eq \a \ f' n\ \n \ 0\ show ?thesis
      apply (intro ex1I[of _ "f' ` {.. n}"])
       apply auto []
      apply metis
      done
  next
    assume "i = n"
    from \<open>n \<noteq> 0\<close> obtain n' where n': "n = Suc n'"
      by (cases n) auto

    define rot where "rot i = (case i of 0 \ n' | Suc i \ i)" for i
    let ?upd = "upd \ rot"

    have rot: "bij_betw rot {..< n} {..< n}"
      by (auto simp: bij_betw_def inj_on_def image_iff Bex_def rot_def n' split: nat.splits)
         arith
    from rot upd have "bij_betw ?upd {..
      by (rule bij_betw_trans)

    define b where "b = base (upd n' := base (upd n') - 1)"
    define f' where [abs_def]: "f' i j = (if j \<in> ?upd`{..< i} then Suc (b j) else b j)" for i j

    interpret b: kuhn_simplex p n b "upd \ rot" "f' ` {.. n}"
    proof
      { fix i assume "n \ i" then show "b i = p"
          using base_out[of i] upd_space[of n'] by (auto simp: b_def n') }
      show "b \ {.. {..
        using base \<open>n \<noteq> 0\<close> upd_space[of n']
        by (auto simp: b_def PiE_def Pi_iff Ball_def upd_space extensional_def n')

      show "bij_betw ?upd {.. by fact
    qed (simp add: f'_def)
    have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
    have ks_f': "ksimplex p n (b.enum ` {.. n})"
      unfolding f' by rule unfold_locales

    have "0 < n"
      using \<open>n \<noteq> 0\<close> by auto

    { from \<open>a = enum i\<close> \<open>n \<noteq> 0\<close> \<open>i = n\<close> lb upd_space[of n']
      obtain i' where "i' \<le> n" "enum i' \<noteq> enum n" "0 < enum i' (upd n')"
        unfolding s_eq by (auto simp: enum_inj n')
      moreover have "enum i' (upd n') = base (upd n')"
        unfolding enum_def using \<open>i' \<le> n\<close> \<open>enum i' \<noteq> enum n\<close> by (auto simp: n' upd_inj enum_inj)
      ultimately have "0 < base (upd n')"
        by auto }
    then have benum1: "b.enum (Suc 0) = base"
      unfolding b.enum_Suc[OF \<open>0<n\<close>] b.enum_0 by (auto simp: b_def rot_def)

    have [simp]: "\j. Suc j < n \ rot ` {..< Suc j} = {n'} \ {..< j}"
      by (auto simp: rot_def image_iff Ball_def split: nat.splits)
    have rot_simps: "\j. rot (Suc j) = j" "rot 0 = n'"
      by (simp_all add: rot_def)

    { fix j assume j: "Suc j \ n" then have "b.enum (Suc j) = enum j"
        by (induct j) (auto simp: benum1 enum_0 b.enum_Suc enum_Suc rot_simps) }
    note b_enum_eq_enum = this
    then have "enum ` {..< n} = b.enum ` Suc ` {..< n}"
      by (auto simp: image_comp intro!: image_cong)
    also have "Suc ` {..< n} = {.. n} - {0}"
      by (auto simp: image_iff Ball_def) arith
    also have "{..< n} = {.. n} - {n}"
      by auto
    finally have eq: "s - {a} = b.enum ` {.. n} - {b.enum 0}"
      unfolding s_eq \<open>a = enum i\<close> \<open>i = n\<close>
      using inj_on_image_set_diff[OF inj_enum Diff_subset, of "{n}"]
            inj_on_image_set_diff[OF b.inj_enum Diff_subset, of "{0}"]
      by (simp add: comp_def)

    have "b.enum 0 \ b.enum n"
      by (simp add: b.enum_mono)
    also have "b.enum n < enum n"
      using \<open>n \<noteq> 0\<close> by (simp add: enum_strict_mono b_enum_eq_enum n')
    finally have "a \ b.enum 0"
      using \<open>a = enum i\<close> \<open>i = n\<close> by auto

    { fix t c assume "ksimplex p n t" "c \ t" and eq_sma: "s - {a} = t - {c}"
      obtain b' u where "kuhn_simplex p n b' u t"
        using \<open>ksimplex p n t\<close> by (auto elim: ksimplex.cases)
      then interpret t: kuhn_simplex p n b' u t .

      { fix x assume "x \ s" "x \ a"
         then have "x (upd n') = enum n' (upd n')"
           by (auto simp: \<open>a = enum i\<close> n' \<open>i = n\<close> s_eq enum_def enum_inj in_upd_image) }
      then have eq_upd0: "\x\t-{c}. x (upd n') = enum n' (upd n')"
        unfolding eq_sma[symmetric] by auto
      then have "c (upd n') \ enum n' (upd n')"
        using \<open>n \<noteq> 0\<close> by (intro t.one_step[OF \<open>c\<in>t\<close> ]) (auto simp: n' upd_space[unfolded n'])
      then have "c (upd n') < enum n' (upd n') \ c (upd n') > enum n' (upd n')"
        by auto
      then have "t = s \ t = b.enum ` {..n}"
      proof (elim disjE conjE)
        assume *: "c (upd n') > enum n' (upd n')"
        interpret st: kuhn_simplex_pair p n base upd s b' u t ..
        { fix x assume "x \ t" with * \c\t\ eq_upd0[rule_format, of x] have "x \ c"
            by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) }
        note top = this
        have "s = t"
          using \<open>a = enum i\<close> \<open>i = n\<close> \<open>c \<in> t\<close>
          by (intro st.ksimplex_eq_top[OF _ _ _ _ eq_sma])
             (auto simp: s_eq enum_mono t.s_eq t.enum_mono top)
        then show ?thesis by simp
      next
        assume *: "c (upd n') < enum n' (upd n')"
        interpret st: kuhn_simplex_pair p n b "upd \ rot" "f' ` {.. n}" b' u t ..
        have eq: "f' ` {..n} - {b.enum 0} = t - {c}"
          using eq_sma eq f' by simp
        { fix x assume "x \ t" with * \c\t\ eq_upd0[rule_format, of x] have "c \ x"
            by (auto simp: le_less intro!: t.less[of _ _ "upd n'"]) }
        note bot = this
        have "f' ` {..n} = t"
          using \<open>a = enum i\<close> \<open>i = n\<close> \<open>c \<in> t\<close>
          by (intro st.ksimplex_eq_bot[OF _ _ _ _ eq])
             (auto simp: b.s_eq b.enum_mono t.s_eq t.enum_mono bot)
        with f' show ?thesis by simp
      qed }
    with ks_f' eq \a \ b.enum 0\ \n \ 0\ show ?thesis
      apply (intro ex1I[of _ "b.enum ` {.. n}"])
      apply fastforce
      apply metis
      done
  next
    assume i: "0 < i" "i < n"
    define i' where "i' = i - 1"
    with i have "Suc i' < n"
      by simp
    with i have Suc_i': "Suc i' = i"
      by (simp add: i'_def)

    let ?upd = "Fun.swap i' i upd"
    from i upd have "bij_betw ?upd {..< n} {..< n}"
      by (subst bij_betw_swap_iff) (auto simp: i'_def)

    define f' where [abs_def]: "f' i j = (if j \<in> ?upd`{..< i} then Suc (base j) else base j)"
      for i j
    interpret b: kuhn_simplex p n base ?upd "f' ` {.. n}"
    proof
      show "base \ {.. {..
      { fix i assume "n \ i" then show "base i = p" by (rule base_out) }
      show "bij_betw ?upd {.. by fact
    qed (simp add: f'_def)
    have f': "b.enum = f'" unfolding f'_def b.enum_def[abs_def] ..
    have ks_f': "ksimplex p n (b.enum ` {.. n})"
      unfolding f' by rule unfold_locales

    have "{i} \ {..n}"
      using i by auto
    { fix j assume "j \ n"
      with i Suc_i' have "enum j = b.enum j \ j \ i"
        unfolding fun_eq_iff enum_def b.enum_def image_comp [symmetric]
        apply (cases \<open>i = j\<close>)
         apply (metis imageI in_upd_image lessI lessThan_iff lessThan_subset_iff order_less_le transpose_apply_first)
        by (metis lessThan_iff linorder_not_less not_less_eq_eq order_less_le transpose_image_eq)
      }
    note enum_eq_benum = this
    then have "enum ` ({.. n} - {i}) = b.enum ` ({.. n} - {i})"
      by (intro image_cong) auto
    then have eq: "s - {a} = b.enum ` {.. n} - {b.enum i}"
      unfolding s_eq \<open>a = enum i\<close>
      using inj_on_image_set_diff[OF inj_enum Diff_subset \<open>{i} \<subseteq> {..n}\<close>]
            inj_on_image_set_diff[OF b.inj_enum Diff_subset \<open>{i} \<subseteq> {..n}\<close>]
      by (simp add: comp_def)

    have "a \ b.enum i"
      using \<open>a = enum i\<close> enum_eq_benum i by auto

    { fix t c assume "ksimplex p n t" "c \ t" and eq_sma: "s - {a} = t - {c}"
      obtain b' u where "kuhn_simplex p n b' u t"
        using \<open>ksimplex p n t\<close> by (auto elim: ksimplex.cases)
      then interpret t: kuhn_simplex p n b' u t .
      have "enum i' \ s - {a}" "enum (i + 1) \ s - {a}"
        using \<open>a = enum i\<close> i enum_in by (auto simp: enum_inj i'_def)
      then obtain l k where
        l: "t.enum l = enum i'" "l \ n" "t.enum l \ c" and
        k: "t.enum k = enum (i + 1)" "k \ n" "t.enum k \ c"
        unfolding eq_sma by (auto simp: t.s_eq)
      with i have "t.enum l < t.enum k"
        by (simp add: enum_strict_mono i'_def)
      with \<open>l \<le> n\<close> \<open>k \<le> n\<close> have "l < k"
        by (simp add: t.enum_strict_mono)
      { assume "Suc l = k"
        have "enum (Suc (Suc i')) = t.enum (Suc l)"
          using i by (simp add: k \<open>Suc l = k\<close> i'_def)
        then have False
          using \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close>
          by (auto simp: t.enum_Suc enum_Suc l upd_inj fun_eq_iff split: if_split_asm)
             (metis Suc_lessD n_not_Suc_n upd_inj) }
      with \<open>l < k\<close> have "Suc l < k"
        by arith
      have c_eq: "c = t.enum (Suc l)"
      proof (rule ccontr)
        assume "c \ t.enum (Suc l)"
        then have "t.enum (Suc l) \ s - {a}"
          using \<open>l < k\<close> \<open>k \<le> n\<close> by (simp add: t.s_eq eq_sma)
        then obtain j where "t.enum (Suc l) = enum j" "j \ n" "enum j \ enum i"
          unfolding s_eq \<open>a = enum i\<close> by auto
        with i have "t.enum (Suc l) \ t.enum l \ t.enum k \ t.enum (Suc l)"
          by (auto simp: i'_def enum_mono enum_inj l k)
        with \<open>Suc l < k\<close> \<open>k \<le> n\<close> show False
          by (simp add: t.enum_mono)
      qed

      { have "t.enum (Suc (Suc l)) \ s - {a}"
          unfolding eq_sma c_eq t.s_eq using \<open>Suc l < k\<close> \<open>k \<le> n\<close> by (auto simp: t.enum_inj)
        then obtain j where eq: "t.enum (Suc (Suc l)) = enum j" and "j \ n" "j \ i"
          by (auto simp: s_eq \<open>a = enum i\<close>)
        moreover have "enum i' < t.enum (Suc (Suc l))"
          unfolding l(1)[symmetric] using \<open>Suc l < k\<close> \<open>k \<le> n\<close> by (auto simp: t.enum_strict_mono)
        ultimately have "i' < j"
          using i by (simp add: enum_strict_mono i'_def)
        with \<open>j \<noteq> i\<close> \<open>j \<le> n\<close> have "t.enum k \<le> t.enum (Suc (Suc l))"
          unfolding i'_def by (simp add: enum_mono k eq)
        then have "k \ Suc (Suc l)"
          using \<open>k \<le> n\<close> \<open>Suc l < k\<close> by (simp add: t.enum_mono) }
      with \<open>Suc l < k\<close> have "Suc (Suc l) = k" by simp
      then have "enum (Suc (Suc i')) = t.enum (Suc (Suc l))"
        using i by (simp add: k i'_def)
      also have "\ = (enum i') (u l := Suc (enum i' (u l)), u (Suc l) := Suc (enum i' (u (Suc l))))"
        using \<open>Suc l < k\<close> \<open>k \<le> n\<close> by (simp add: t.enum_Suc l t.upd_inj)
      finally have "(u l = upd i' \ u (Suc l) = upd (Suc i')) \
        (u l = upd (Suc i') \ u (Suc l) = upd i')"
        using \<open>Suc i' < n\<close> by (auto simp: enum_Suc fun_eq_iff split: if_split_asm)

      then have "t = s \ t = b.enum ` {..n}"
      proof (elim disjE conjE)
        assume u: "u l = upd i'"
        have "c = t.enum (Suc l)" unfolding c_eq ..
        also have "t.enum (Suc l) = enum (Suc i')"
          using u \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close> by (simp add: enum_Suc t.enum_Suc l)
        also have "\ = a"
          using \<open>a = enum i\<close> i by (simp add: i'_def)
        finally show ?thesis
          using eq_sma \<open>a \<in> s\<close> \<open>c \<in> t\<close> by auto
      next
        assume u: "u l = upd (Suc i')"
        define B where "B = b.enum ` {..n}"
        have "b.enum i' = enum i'"
          using enum_eq_benum[of i'] i by (auto simp: i'_def gr0_conv_Suc)
        have "c = t.enum (Suc l)" unfolding c_eq ..
        also have "t.enum (Suc l) = b.enum (Suc i')"
          using u \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close>
          by (simp_all add: enum_Suc t.enum_Suc l b.enum_Suc \<open>b.enum i' = enum i'\<close>)
             (simp add: Suc_i')
        also have "\ = b.enum i"
          using i by (simp add: i'_def)
        finally have "c = b.enum i" .
        then have "t - {c} = B - {c}" "c \ B"
          unfolding eq_sma[symmetric] eq B_def using i by auto
        with \<open>c \<in> t\<close> have "t = B"
          by auto
        then show ?thesis
          by (simp add: B_def)
      qed }
    with ks_f' eq \a \ b.enum i\ \n \ 0\ \i \ n\ show ?thesis
      apply (intro ex1I[of _ "b.enum ` {.. n}"])
      apply auto []
      apply metis
      done
  qed
  then show ?thesis
    using s \<open>a \<in> s\<close> by (simp add: card_2_iff' Ex1_def) metis
qed

text \<open>Hence another step towards concreteness.\<close>

lemma kuhn_simplex_lemma:
  assumes "\s. ksimplex p (Suc n) s \ rl ` s \ {.. Suc n}"
    and "odd (card {f. \s a. ksimplex p (Suc n) s \ a \ s \ (f = s - {a}) \
      rl ` f = {..n} \<and> ((\<exists>j\<le>n. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<le>n. \<forall>x\<in>f. x j = p))})"
  shows "odd (card {s. ksimplex p (Suc n) s \ rl ` s = {..Suc n}})"
proof (rule kuhn_complete_lemma[OF finite_ksimplexes refl, unfolded mem_Collect_eq,
    where bnd="\f. (\j\{..n}. \x\f. x j = 0) \ (\j\{..n}. \x\f. x j = p)"],
    safe del: notI)

  have *: "\x y. x = y \ odd (card x) \ odd (card y)"
    by auto
  show "odd (card {f. (\s\{s. ksimplex p (Suc n) s}. \a\s. f = s - {a}) \
    rl ` f = {..n} \<and> ((\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{..n}. \<forall>x\<in>f. x j = p))})"
    apply (rule *[OF _ assms(2)])
    apply (auto simp: atLeast0AtMost)
    done

next

  fix s assume s: "ksimplex p (Suc n) s"
  then show "card s = n + 2"
    by (simp add: ksimplex_card)

  fix a assume a: "a \ s" then show "rl a \ Suc n"
    using assms(1) s by (auto simp: subset_eq)

  let ?S = "{t. ksimplex p (Suc n) t \ (\b\t. s - {a} = t - {b})}"
  { fix j assume j: "j \ n" "\x\s - {a}. x j = 0"
    with s a show "card ?S = 1"
      using ksimplex_replace_0[of p "n + 1" s a j]
      by (subst eq_commute) simp }

  { fix j assume j: "j \ n" "\x\s - {a}. x j = p"
    with s a show "card ?S = 1"
      using ksimplex_replace_1[of p "n + 1" s a j]
      by (subst eq_commute) simp }

  { assume "card ?S \ 2" "\ (\j\{..n}. \x\s - {a}. x j = p)"
    with s a show "\j\{..n}. \x\s - {a}. x j = 0"
      using ksimplex_replace_2[of p "n + 1" s a]
      by (subst (asm) eq_commute) auto }
qed

subsubsection \<open>Reduced labelling\<close>

definition reduced :: "nat \ (nat \ nat) \ nat" where "reduced n x = (LEAST k. k = n \ x k \ 0)"

lemma reduced_labelling:
  shows "reduced n x \ n"
    and "\i
    and "reduced n x = n \ x (reduced n x) \ 0"
proof -
  show "reduced n x \ n"
    unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) auto
  show "\i
    unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+
  show "reduced n x = n \ x (reduced n x) \ 0"
    unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) fastforce+
qed

lemma reduced_labelling_unique:
  "r \ n \ \i r = n \ x r \ 0 \ reduced n x = r"
  by (metis linorder_less_linear linorder_not_le reduced_labelling)

lemma reduced_labelling_zero: "j < n \ x j = 0 \ reduced n x \ j"
  using reduced_labelling[of n x] by auto

lemma reduce_labelling_zero[simp]: "reduced 0 x = 0"
  by (rule reduced_labelling_unique) auto

lemma reduced_labelling_nonzero: "j < n \ x j \ 0 \ reduced n x \ j"
  using reduced_labelling[of n x] by (elim allE[where x=j]) auto

lemma reduced_labelling_Suc: "reduced (Suc n) x \ Suc n \ reduced (Suc n) x = reduced n x"
  using reduced_labelling[of "Suc n" x]
  by (intro reduced_labelling_unique[symmetric]) auto

lemma complete_face_top:
  assumes "\x\f. \j\n. x j = 0 \ lab x j = 0"
    and "\x\f. \j\n. x j = p \ lab x j = 1"
    and eq: "(reduced (Suc n) \ lab) ` f = {..n}"
  shows "((\j\n. \x\f. x j = 0) \ (\j\n. \x\f. x j = p)) \ (\x\f. x n = p)"
proof (safe del: disjCI)
  fix x j assume j: "j \ n" "\x\f. x j = 0"
  { fix x assume "x \ f" with assms j have "reduced (Suc n) (lab x) \ j"
      by (intro reduced_labelling_zero) auto }
  moreover have "j \ (reduced (Suc n) \ lab) ` f"
    using j eq by auto
  ultimately show "x n = p"
    by force
next
  fix x j assume j: "j \ n" "\x\f. x j = p" and x: "x \ f"
  have "j = n"
  proof (rule ccontr)
    assume "\ ?thesis"
    { fix x assume "x \ f"
      with assms j have "reduced (Suc n) (lab x) \ j"
        by (intro reduced_labelling_nonzero) auto
      then have "reduced (Suc n) (lab x) \ n"
        using \<open>j \<noteq> n\<close> \<open>j \<le> n\<close> by simp }
    moreover
    have "n \ (reduced (Suc n) \ lab) ` f"
      using eq by auto
    ultimately show False
      by force
  qed
  moreover have "j \ (reduced (Suc n) \ lab) ` f"
    using j eq by auto
  ultimately show "x n = p"
    using j x by auto
qed auto

text \<open>Hence we get just about the nice induction.\<close>

lemma kuhn_induction:
  assumes "0 < p"
    and lab_0: "\x. \j\n. (\j. x j \ p) \ x j = 0 \ lab x j = 0"
    and lab_1: "\x. \j\n. (\j. x j \ p) \ x j = p \ lab x j = 1"
    and odd: "odd (card {s. ksimplex p n s \ (reduced n\lab) ` s = {..n}})"
  shows "odd (card {s. ksimplex p (Suc n) s \ (reduced (Suc n)\lab) ` s = {..Suc n}})"
proof -
  let ?rl = "reduced (Suc n) \ lab" and ?ext = "\f v. \j\n. \x\f. x j = v"
  let ?ext = "\s. (\j\n. \x\s. x j = 0) \ (\j\n. \x\s. x j = p)"
  have "\s. ksimplex p (Suc n) s \ ?rl ` s \ {..Suc n}"
    by (simp add: reduced_labelling subset_eq)
  moreover
  have "{s. ksimplex p n s \ (reduced n \ lab) ` s = {..n}} =
        {f. \<exists>s a. ksimplex p (Suc n) s \<and> a \<in> s \<and> f = s - {a} \<and> ?rl ` f = {..n} \<and> ?ext f}"
  proof (intro set_eqI, safe del: disjCI equalityI disjE)
    fix s assume s: "ksimplex p n s" and rl: "(reduced n \ lab) ` s = {..n}"
    from s obtain u b where "kuhn_simplex p n u b s" by (auto elim: ksimplex.cases)
    then interpret kuhn_simplex p n u b s .
    have all_eq_p: "\x\s. x n = p"
      by (auto simp: out_eq_p)
    moreover
    { fix x assume "x \ s"
      with lab_1[rule_format, of n x] all_eq_p s_le_p[of x]
      have "?rl x \ n"
        by (auto intro!: reduced_labelling_nonzero)
      then have "?rl x = reduced n (lab x)"
        by (auto intro!: reduced_labelling_Suc) }
    then have "?rl ` s = {..n}"
      using rl by (simp cong: image_cong)
    moreover
    obtain t a where "ksimplex p (Suc n) t" "a \ t" "s = t - {a}"
      using s unfolding simplex_top_face[OF \<open>0 < p\<close> all_eq_p] by auto
    ultimately
    show "\t a. ksimplex p (Suc n) t \ a \ t \ s = t - {a} \ ?rl ` s = {..n} \ ?ext s"
      by auto
  next
    fix x s a assume s: "ksimplex p (Suc n) s" and rl: "?rl ` (s - {a}) = {.. n}"
      and a: "a \ s" and "?ext (s - {a})"
    from s obtain u b where "kuhn_simplex p (Suc n) u b s" by (auto elim: ksimplex.cases)
    then interpret kuhn_simplex p "Suc n" u b s .
    have all_eq_p: "\x\s. x (Suc n) = p"
      by (auto simp: out_eq_p)

    { fix x assume "x \ s - {a}"
      then have "?rl x \ ?rl ` (s - {a})"
        by auto
      then have "?rl x \ n"
        unfolding rl by auto
      then have "?rl x = reduced n (lab x)"
        by (auto intro!: reduced_labelling_Suc) }
    then show rl': "(reduced n\lab) ` (s - {a}) = {..n}"
      unfolding rl[symmetric] by (intro image_cong) auto

    from \<open>?ext (s - {a})\<close>
    have all_eq_p: "\x\s - {a}. x n = p"
--> --------------------

--> maximum size reached

--> --------------------

quality99%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.38Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Versionsinformation zu Columbo

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders