Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: hausdorff_convergence.pvs Sprache: PVS

Original von: 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)
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:
    "\simply_connected T; S retract_of T\ \ simply_connected S"
apply (simp add: retract_of_def retraction_def, clarify)
apply (rule simply_connected_retraction_gen)
apply (force elim!: continuous_on_subset)+
done

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 ` U \<subseteq> 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
    by (metis continuous_on_subset dual_order.trans image_iff image_mono)
  then show ?thesis
    apply (rule Retracts.homotopically_trivial_retraction_gen)
    using assms
    apply (force simp: hom)+
    done
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 (metis continuous_on_subset dual_order.trans image_iff image_mono)
  then show ?thesis
    apply (rule Retracts.homotopically_trivial_retraction_null_gen)
    apply (rule TrueI refl assms that | assumption)+
    done
qed

lemma retraction_openin_vimage_iff:
  "openin (top_of_set S) (S \ r -` U) \ openin (top_of_set T) U"
  if retraction: "retraction S T r" and "U \ T"
  using retraction apply (rule retractionE)
  apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
  using \<open>U \<subseteq> T\<close> apply (auto elim: continuous_on_subset)
  done

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:
   "\f ` S \ T; g ` S \ T; T retract_of U; homotopic_with_canon (\x. True) S U f g\
        \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g"
apply (subst (asm) homotopic_with_def)
apply (simp add: homotopic_with retract_of_def retraction_def, clarify)
apply (rule_tac x="r \ h" in exI)
apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
done

lemma retract_of_locally_connected:
  assumes "locally connected T" "S retract_of T"
  shows "locally connected S"
  using assms
  by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: 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 (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: 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 (metis (no_types, lifting) continuous_map_subtopology_eu continuous_on_id' id_def image_id 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 ` S \<subseteq> T)"
    (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (auto simp: retract_of_def retraction_def)
next
  assume ?rhs
  then show ?lhs
    apply (clarsimp simp add: retract_of_def retraction_def)
    apply (rule_tac x=r in exI, simp)
     apply (rule homotopic_with_trans, assumption)
     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)
    done
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
    using that deformation_retract  by metis
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

lemma swap_image:
  "Fun.swap i j f ` A = (if i \ A then (if j \ A then f ` A else f ` ((A - {i}) \ {j}))
                                  else (if j \<in> A then f ` ((A - {j}) \<union> {i}) else f ` A))"
  by (auto simp: swap_def cong: image_cong_simp)

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"
    using *[rule_format, of b u] *[rule_format, of b l] 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 auto []
      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"
      moreover have "j < i \ i = j \ i < j" by arith
      moreover note i
      ultimately have "enum j = b.enum j \ j \ i"
        unfolding enum_def[abs_def] b.enum_def[abs_def]
        by (auto simp: fun_eq_iff swap_image i'_def
                           in_upd_image inj_on_image_set_diff[OF inj_upd]) }
    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"
unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) (metis le_less not_le)+

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"
    proof (elim disjE exE conjE)
      fix j assume "j \ n" "\x\s - {a}. x j = 0"
      with lab_0[rule_format, of j] all_eq_p s_le_p
      have "\x. x \ s - {a} \ reduced (Suc n) (lab x) \ j"
        by (intro reduced_labelling_zero) auto
      moreover have "j \ ?rl ` (s - {a})"
        using \<open>j \<le> n\<close> unfolding rl by auto
      ultimately show ?thesis
        by force
    next
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.60 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.