author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44890  22f665a2e91c 
child 49374  b08c6312782b 
permissions  rwrr 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

2 
(* ========================================================================= *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

3 
(* Results connected with topological dimension. *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

4 
(* *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

5 
(* At the moment this is just Brouwer's fixpoint theorem. The proof is from *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

6 
(* Kuhn: "some combinatorial lemmas in topology", IBM J. v4. (1960) p. 518 *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

7 
(* See "http://www.research.ibm.com/journal/rd/045/ibmrd0405K.pdf". *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

8 
(* *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

9 
(* The script below is quite messy, but at least we avoid formalizing any *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

10 
(* topological machinery; we don't even use barycentric subdivision; this is *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

11 
(* the big advantage of Kuhn's proof over the usual Sperner's lemma one. *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

12 
(* *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

13 
(* (c) Copyright, John Harrison 19982008 *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

14 
(* ========================================================================= *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

15 

33759
b369324fc244
Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS
hoelzl
parents:
33758
diff
changeset

16 
(* Author: John Harrison 
b369324fc244
Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS
hoelzl
parents:
33758
diff
changeset

17 
Translation from HOL light: Robert Himmelmann, TU Muenchen *) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

18 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

19 
header {* Results connected with topological dimension. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

20 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

21 
theory Brouwer_Fixpoint 
36432
1ad1cfeaec2d
move proof of Fashoda meet theorem into separate file
huffman
parents:
36431
diff
changeset

22 
imports Convex_Euclidean_Space 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

23 
begin 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

24 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

25 
lemma brouwer_compactness_lemma: 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36587
diff
changeset

26 
assumes "compact s" "continuous_on s f" "\<not> (\<exists>x\<in>s. (f x = (0::_::euclidean_space)))" 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

27 
obtains d where "0 < d" "\<forall>x\<in>s. d \<le> norm(f x)" proof(cases "s={}") case False 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

28 
have "continuous_on s (norm \<circ> f)" by(rule continuous_on_intros continuous_on_norm assms(2))+ 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

29 
then obtain x where x:"x\<in>s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

30 
using continuous_attains_inf[OF assms(1), of "norm \<circ> f"] and False unfolding o_def by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

31 
have "(norm \<circ> f) x > 0" using assms(3) and x(1) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

32 
thus ?thesis apply(rule that) using x(2) unfolding o_def by auto qed(rule that[of 1], auto) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

33 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36587
diff
changeset

34 
lemma kuhn_labelling_lemma: fixes type::"'a::euclidean_space" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36587
diff
changeset

35 
assumes "(\<forall>x::'a. P x \<longrightarrow> P (f x))" "\<forall>x. P x \<longrightarrow> (\<forall>i<DIM('a). Q i \<longrightarrow> 0 \<le> x$$i \<and> x$$i \<le> 1)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36587
diff
changeset

36 
shows "\<exists>l. (\<forall>x.\<forall> i<DIM('a). l x i \<le> (1::nat)) \<and> 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36587
diff
changeset

37 
(\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (x$$i = 0) \<longrightarrow> (l x i = 0)) \<and> 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36587
diff
changeset

38 
(\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (x$$i = 1) \<longrightarrow> (l x i = 1)) \<and> 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36587
diff
changeset

39 
(\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x$$i \<le> f(x)$$i) \<and> 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36587
diff
changeset

40 
(\<forall>x.\<forall> i<DIM('a). P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f(x)$$i \<le> x$$i)" proof 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

41 
have and_forall_thm:"\<And>P Q. (\<forall>x. P x) \<and> (\<forall>x. Q x) \<longleftrightarrow> (\<forall>x. P x \<and> Q x)" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

42 
have *:"\<forall>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow> (x \<noteq> 1 \<and> x \<le> y \<or> x \<noteq> 0 \<and> y \<le> x)" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

43 
show ?thesis unfolding and_forall_thm apply(subst choice_iff[THEN sym])+ proof(rule,rule) case goal1 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36587
diff
changeset

44 
let ?R = "\<lambda>y. (P x \<and> Q xa \<and> x $$ xa = 0 \<longrightarrow> y = (0::nat)) \<and> 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36587
diff
changeset

45 
(P x \<and> Q xa \<and> x $$ xa = 1 \<longrightarrow> y = 1) \<and> (P x \<and> Q xa \<and> y = 0 \<longrightarrow> x $$ xa \<le> f x $$ xa) \<and> (P x \<and> Q xa \<and> y = 1 \<longrightarrow> f x $$ xa \<le> x $$ xa)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36587
diff
changeset

46 
{ assume "P x" "Q xa" "xa<DIM('a)" hence "0 \<le> f x $$ xa \<and> f x $$ xa \<le> 1" using assms(2)[rule_format,of "f x" xa] 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

47 
apply(drule_tac assms(1)[rule_format]) by auto } 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36587
diff
changeset

48 
hence "xa<DIM('a) \<Longrightarrow> ?R 0 \<or> ?R 1" by auto thus ?case by auto qed qed 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

49 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

50 
subsection {* The key "counting" observation, somewhat abstracted. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

51 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

52 
lemma setsum_Un_disjoint':assumes "finite A" "finite B" "A \<inter> B = {}" "A \<union> B = C" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

53 
shows "setsum g C = setsum g A + setsum g B" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

54 
using setsum_Un_disjoint[OF assms(13)] and assms(4) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

55 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

56 
lemma kuhn_counting_lemma: assumes "finite faces" "finite simplices" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

57 
"\<forall>f\<in>faces. bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 1)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

58 
"\<forall>f\<in>faces. \<not> bnd f \<longrightarrow> (card {s \<in> simplices. face f s} = 2)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

59 
"\<forall>s\<in>simplices. compo s \<longrightarrow> (card {f \<in> faces. face f s \<and> compo' f} = 1)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

60 
"\<forall>s\<in>simplices. \<not> compo s \<longrightarrow> (card {f \<in> faces. face f s \<and> compo' f} = 0) \<or> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

61 
(card {f \<in> faces. face f s \<and> compo' f} = 2)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

62 
"odd(card {f \<in> faces. compo' f \<and> bnd f})" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

63 
shows "odd(card {s \<in> simplices. compo s})" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

64 
have "\<And>x. {f\<in>faces. compo' f \<and> bnd f \<and> face f x} \<union> {f\<in>faces. compo' f \<and> \<not>bnd f \<and> face f x} = {f\<in>faces. compo' f \<and> face f x}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

65 
"\<And>x. {f \<in> faces. compo' f \<and> bnd f \<and> face f x} \<inter> {f \<in> faces. compo' f \<and> \<not> bnd f \<and> face f x} = {}" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

66 
hence lem1:"setsum (\<lambda>s. (card {f \<in> faces. face f s \<and> compo' f})) simplices = 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

67 
setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f s}) simplices + 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

68 
setsum (\<lambda>s. card {f \<in> {f \<in> faces. compo' f \<and> \<not> (bnd f)}. face f s}) simplices" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

69 
unfolding setsum_addf[THEN sym] apply apply(rule setsum_cong2) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

70 
using assms(1) by(auto simp add: card_Un_Int, auto simp add:conj_commute) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

71 
have lem2:"setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> bnd f}. face f j}) simplices = 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

72 
1 * card {f \<in> faces. compo' f \<and> bnd f}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

73 
"setsum (\<lambda>j. card {f \<in> {f \<in> faces. compo' f \<and> \<not> bnd f}. face f j}) simplices = 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

74 
2 * card {f \<in> faces. compo' f \<and> \<not> bnd f}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

75 
apply(rule_tac[!] setsum_multicount) using assms by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

76 
have lem3:"setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) simplices = 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

77 
setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. compo s}+ 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

78 
setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. \<not> compo s}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

79 
apply(rule setsum_Un_disjoint') using assms(2) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

80 
have lem4:"setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. compo s} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

81 
= setsum (\<lambda>s. 1) {s \<in> simplices. compo s}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

82 
apply(rule setsum_cong2) using assms(5) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

83 
have lem5: "setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) {s \<in> simplices. \<not> compo s} = 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

84 
setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

85 
{s \<in> simplices. (\<not> compo s) \<and> (card {f \<in> faces. face f s \<and> compo' f} = 0)} + 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

86 
setsum (\<lambda>s. card {f \<in> faces. face f s \<and> compo' f}) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

87 
{s \<in> simplices. (\<not> compo s) \<and> (card {f \<in> faces. face f s \<and> compo' f} = 2)}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

88 
apply(rule setsum_Un_disjoint') using assms(2,6) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

89 
have *:"int (\<Sum>s\<in>{s \<in> simplices. compo s}. card {f \<in> faces. face f s \<and> compo' f}) = 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

90 
int (card {f \<in> faces. compo' f \<and> bnd f} + 2 * card {f \<in> faces. compo' f \<and> \<not> bnd f})  
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

91 
int (card {s \<in> simplices. \<not> compo s \<and> card {f \<in> faces. face f s \<and> compo' f} = 2} * 2)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

92 
using lem1[unfolded lem3 lem2 lem5] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

93 
have even_minus_odd:"\<And>x y. even x \<Longrightarrow> odd (y::int) \<Longrightarrow> odd (x  y)" using assms by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

94 
have odd_minus_even:"\<And>x y. odd x \<Longrightarrow> even (y::int) \<Longrightarrow> odd (x  y)" using assms by auto 
35729  95 
show ?thesis unfolding even_nat_def unfolding card_eq_setsum and lem4[THEN sym] and *[unfolded card_eq_setsum] 
44821  96 
unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding of_nat_add apply(rule odd_plus_even) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

97 
apply(rule assms(7)[unfolded even_nat_def]) unfolding int_mult by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

98 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

99 
subsection {* The odd/even result for faces of complete vertices, generalized. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

100 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

101 
lemma card_1_exists: "card s = 1 \<longleftrightarrow> (\<exists>!x. x \<in> s)" unfolding One_nat_def 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

102 
apply rule apply(drule card_eq_SucD) defer apply(erule ex1E) proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

103 
fix x assume as:"x \<in> s" "\<forall>y. y \<in> s \<longrightarrow> y = x" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

104 
have *:"s = insert x {}" apply apply(rule set_eqI,rule) unfolding singleton_iff 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

105 
apply(rule as(2)[rule_format]) using as(1) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

106 
show "card s = Suc 0" unfolding * using card_insert by auto qed auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

107 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

108 
lemma card_2_exists: "card s = 2 \<longleftrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. (z = x) \<or> (z = y)))" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

109 
assume "card s = 2" then obtain x y where obt:"s = {x, y}" "x\<noteq>y" unfolding numeral_2_eq_2 apply  apply(erule exE conjEdrule card_eq_SucD)+ by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

110 
show "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)" using obt by auto next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

111 
assume "\<exists>x\<in>s. \<exists>y\<in>s. x \<noteq> y \<and> (\<forall>z\<in>s. z = x \<or> z = y)" then guess x .. from this(2) guess y .. 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

112 
with `x\<in>s` have *:"s = {x, y}" "x\<noteq>y" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

113 
from this(2) show "card s = 2" unfolding * by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

114 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

115 
lemma image_lemma_0: assumes "card {a\<in>s. f ` (s  {a}) = t  {b}} = n" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

116 
shows "card {s'. \<exists>a\<in>s. (s' = s  {a}) \<and> (f ` s' = t  {b})} = n" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

117 
have *:"{s'. \<exists>a\<in>s. (s' = s  {a}) \<and> (f ` s' = t  {b})} = (\<lambda>a. s  {a}) ` {a\<in>s. f ` (s  {a}) = t  {b}}" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

118 
show ?thesis unfolding * unfolding assms[THEN sym] apply(rule card_image) unfolding inj_on_def 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

119 
apply(rule,rule,rule) unfolding mem_Collect_eq by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

120 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

121 
lemma image_lemma_1: assumes "finite s" "finite t" "card s = card t" "f ` s = t" "b \<in> t" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

122 
shows "card {s'. \<exists>a\<in>s. s' = s  {a} \<and> f ` s' = t  {b}} = 1" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

123 
obtain a where a:"b = f a" "a\<in>s" using assms(45) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

124 
have inj:"inj_on f s" apply(rule eq_card_imp_inj_on) using assms(14) by auto 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

125 
have *:"{a \<in> s. f ` (s  {a}) = t  {b}} = {a}" apply(rule set_eqI) unfolding singleton_iff 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

126 
apply(rule,rule inj[unfolded inj_on_def,rule_format]) unfolding a using a(2) and assms and inj[unfolded inj_on_def] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

127 
show ?thesis apply(rule image_lemma_0) unfolding * by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

128 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

129 
lemma image_lemma_2: assumes "finite s" "finite t" "card s = card t" "f ` s \<subseteq> t" "f ` s \<noteq> t" "b \<in> t" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

130 
shows "(card {s'. \<exists>a\<in>s. (s' = s  {a}) \<and> f ` s' = t  {b}} = 0) \<or> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

131 
(card {s'. \<exists>a\<in>s. (s' = s  {a}) \<and> f ` s' = t  {b}} = 2)" proof(cases "{a\<in>s. f ` (s  {a}) = t  {b}} = {}") 
36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
36340
diff
changeset

132 
case True thus ?thesis applyapply(rule disjI1, rule image_lemma_0) using assms(1) by auto 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

133 
next let ?M = "{a\<in>s. f ` (s  {a}) = t  {b}}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

134 
case False then obtain a where "a\<in>?M" by auto hence a:"a\<in>s" "f ` (s  {a}) = t  {b}" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

135 
have "f a \<in> t  {b}" using a and assms by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

136 
hence "\<exists>c \<in> s  {a}. f a = f c" unfolding image_iff[symmetric] and a by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

137 
then obtain c where c:"c \<in> s" "a \<noteq> c" "f a = f c" by auto 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

138 
hence *:"f ` (s  {c}) = f ` (s  {a})" applyapply(rule set_eqI,rule) proof 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

139 
fix x assume "x \<in> f ` (s  {a})" then obtain y where y:"f y = x" "y\<in>s {a}" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

140 
thus "x \<in> f ` (s  {c})" unfolding image_iff apply(rule_tac x="if y = c then a else y" in bexI) using c a by auto qed auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

141 
have "c\<in>?M" unfolding mem_Collect_eq and * using a and c(1) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

142 
show ?thesis apply(rule disjI2, rule image_lemma_0) unfolding card_2_exists 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

143 
apply(rule bexI[OF _ `a\<in>?M`], rule bexI[OF _ `c\<in>?M`],rule,rule `a\<noteq>c`) proof(rule,unfold mem_Collect_eq,erule conjE) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

144 
fix z assume as:"z \<in> s" "f ` (s  {z}) = t  {b}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

145 
have inj:"inj_on f (s  {z})" apply(rule eq_card_imp_inj_on) unfolding as using as(1) and assms by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

146 
show "z = a \<or> z = c" proof(rule ccontr) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

147 
assume "\<not> (z = a \<or> z = c)" thus False using inj[unfolded inj_on_def,THEN bspec[where x=a],THEN bspec[where x=c]] 
41958  148 
using `a\<in>s` `c\<in>s` `f a = f c` `a\<noteq>c` by auto qed qed qed 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

149 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

150 
subsection {* Combine this with the basic counting lemma. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

151 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

152 
lemma kuhn_complete_lemma: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

153 
assumes "finite simplices" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

154 
"\<forall>f s. face f s \<longleftrightarrow> (\<exists>a\<in>s. f = s  {a})" "\<forall>s\<in>simplices. card s = n + 2" "\<forall>s\<in>simplices. (rl ` s) \<subseteq> {0..n+1}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

155 
"\<forall>f\<in> {f. \<exists>s\<in>simplices. face f s}. bnd f \<longrightarrow> (card {s\<in>simplices. face f s} = 1)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

156 
"\<forall>f\<in> {f. \<exists>s\<in>simplices. face f s}. \<not>bnd f \<longrightarrow> (card {s\<in>simplices. face f s} = 2)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

157 
"odd(card {f\<in>{f. \<exists>s\<in>simplices. face f s}. rl ` f = {0..n} \<and> bnd f})" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

158 
shows "odd (card {s\<in>simplices. (rl ` s = {0..n+1})})" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

159 
apply(rule kuhn_counting_lemma) defer apply(rule assms)+ prefer 3 apply(rule assms) proof(rule_tac[12] ballI impI)+ 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

160 
have *:"{f. \<exists>s\<in>simplices. \<exists>a\<in>s. f = s  {a}} = (\<Union>s\<in>simplices. {f. \<exists>a\<in>s. (f = s  {a})})" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

161 
have **: "\<forall>s\<in>simplices. card s = n + 2 \<and> finite s" using assms(3) by (auto intro: card_ge_0_finite) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

162 
show "finite {f. \<exists>s\<in>simplices. face f s}" unfolding assms(2)[rule_format] and * 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

163 
apply(rule finite_UN_I[OF assms(1)]) using ** by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

164 
have *:"\<And> P f s. s\<in>simplices \<Longrightarrow> (f \<in> {f. \<exists>s\<in>simplices. \<exists>a\<in>s. f = s  {a}}) \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

165 
(\<exists>a\<in>s. (f = s  {a})) \<and> P f \<longleftrightarrow> (\<exists>a\<in>s. (f = s  {a}) \<and> P f)" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

166 
fix s assume s:"s\<in>simplices" let ?S = "{f \<in> {f. \<exists>s\<in>simplices. face f s}. face f s \<and> rl ` f = {0..n}}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

167 
have "{0..n + 1}  {n + 1} = {0..n}" by auto 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

168 
hence S:"?S = {s'. \<exists>a\<in>s. s' = s  {a} \<and> rl ` s' = {0..n + 1}  {n + 1}}" apply apply(rule set_eqI) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

169 
unfolding assms(2)[rule_format] mem_Collect_eq and *[OF s, unfolded mem_Collect_eq, where P="\<lambda>x. rl ` x = {0..n}"] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

170 
show "rl ` s = {0..n+1} \<Longrightarrow> card ?S = 1" "rl ` s \<noteq> {0..n+1} \<Longrightarrow> card ?S = 0 \<or> card ?S = 2" unfolding S 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

171 
apply(rule_tac[!] image_lemma_1 image_lemma_2) using ** assms(4) and s by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

172 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

173 
subsection {*We use the following notion of ordering rather than pointwise indexing. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

174 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

175 
definition "kle n x y \<longleftrightarrow> (\<exists>k\<subseteq>{1..n::nat}. (\<forall>j. y(j) = x(j) + (if j \<in> k then (1::nat) else 0)))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

176 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

177 
lemma kle_refl[intro]: "kle n x x" unfolding kle_def by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

178 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

179 
lemma kle_antisym: "kle n x y \<and> kle n y x \<longleftrightarrow> (x = y)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

180 
unfolding kle_def apply rule apply(rule ext) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

181 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

182 
lemma pointwise_minimal_pointwise_maximal: fixes s::"(nat\<Rightarrow>nat) set" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

183 
assumes "finite s" "s \<noteq> {}" "\<forall>x\<in>s. \<forall>y\<in>s. (\<forall>j. x j \<le> y j) \<or> (\<forall>j. y j \<le> x j)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

184 
shows "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<le> x j" "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. x j \<le> a j" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

185 
using assms unfolding atomize_conj apply proof(induct s rule:finite_induct) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

186 
fix x and F::"(nat\<Rightarrow>nat) set" assume as:"finite F" "x \<notin> F" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

187 
"\<lbrakk>F \<noteq> {}; \<forall>x\<in>F. \<forall>y\<in>F. (\<forall>j. x j \<le> y j) \<or> (\<forall>j. y j \<le> x j)\<rbrakk> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

188 
\<Longrightarrow> (\<exists>a\<in>F. \<forall>x\<in>F. \<forall>j. a j \<le> x j) \<and> (\<exists>a\<in>F. \<forall>x\<in>F. \<forall>j. x j \<le> a j)" "insert x F \<noteq> {}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

189 
"\<forall>xa\<in>insert x F. \<forall>y\<in>insert x F. (\<forall>j. xa j \<le> y j) \<or> (\<forall>j. y j \<le> xa j)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

190 
show "(\<exists>a\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. a j \<le> x j) \<and> (\<exists>a\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. x j \<le> a j)" proof(cases "F={}") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

191 
case True thus ?thesis applyapply(rule,rule_tac[!] x=x in bexI) by auto next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

192 
case False obtain a b where a:"a\<in>insert x F" "\<forall>x\<in>F. \<forall>j. a j \<le> x j" and 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

193 
b:"b\<in>insert x F" "\<forall>x\<in>F. \<forall>j. x j \<le> b j" using as(3)[OF False] using as(5) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

194 
have "\<exists>a\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. a j \<le> x j" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

195 
using as(5)[rule_format,OF a(1) insertI1] apply proof(erule disjE) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

196 
assume "\<forall>j. a j \<le> x j" thus ?thesis apply(rule_tac x=a in bexI) using a by auto next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

197 
assume "\<forall>j. x j \<le> a j" thus ?thesis apply(rule_tac x=x in bexI) apply(rule,rule) using a apply  
41958  198 
apply(erule_tac x=xa in ballE) apply(erule_tac x=j in allE)+ by auto qed moreover 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

199 
have "\<exists>b\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. x j \<le> b j" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

200 
using as(5)[rule_format,OF b(1) insertI1] apply proof(erule disjE) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

201 
assume "\<forall>j. x j \<le> b j" thus ?thesis apply(rule_tac x=b in bexI) using b by auto next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

202 
assume "\<forall>j. b j \<le> x j" thus ?thesis apply(rule_tac x=x in bexI) apply(rule,rule) using b apply  
41958  203 
apply(erule_tac x=xa in ballE) apply(erule_tac x=j in allE)+ by auto qed 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

204 
ultimately show ?thesis by auto qed qed(auto) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

205 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

206 
lemma kle_imp_pointwise: "kle n x y \<Longrightarrow> (\<forall>j. x j \<le> y j)" unfolding kle_def by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

207 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

208 
lemma pointwise_antisym: fixes x::"nat \<Rightarrow> nat" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

209 
shows "(\<forall>j. x j \<le> y j) \<and> (\<forall>j. y j \<le> x j) \<longleftrightarrow> (x = y)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

210 
apply(rule, rule ext,erule conjE) apply(erule_tac x=xa in allE)+ by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

211 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

212 
lemma kle_trans: assumes "kle n x y" "kle n y z" "kle n x z \<or> kle n z x" shows "kle n x z" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

213 
using assms apply apply(erule disjE) apply assumption proof case goal1 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

214 
hence "x=z" apply apply(rule ext) apply(drule kle_imp_pointwise)+ 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

215 
apply(erule_tac x=xa in allE)+ by auto thus ?case by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

216 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

217 
lemma kle_strict: assumes "kle n x y" "x \<noteq> y" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

218 
shows "\<forall>j. x j \<le> y j" "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x(k) < y(k)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

219 
apply(rule kle_imp_pointwise[OF assms(1)]) proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

220 
guess k using assms(1)[unfolded kle_def] .. note k = this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

221 
show "\<exists>k. 1 \<le> k \<and> k \<le> n \<and> x(k) < y(k)" proof(cases "k={}") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

222 
case True hence "x=y" applyapply(rule ext) using k by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

223 
thus ?thesis using assms(2) by auto next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

224 
case False hence "(SOME k'. k' \<in> k) \<in> k" applyapply(rule someI_ex) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

225 
thus ?thesis apply(rule_tac x="SOME k'. k' \<in> k" in exI) using k by auto qed qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

226 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

227 
lemma kle_minimal: assumes "finite s" "s \<noteq> {}" "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

228 
shows "\<exists>a\<in>s. \<forall>x\<in>s. kle n a x" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

229 
have "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<le> x j" apply(rule pointwise_minimal_pointwise_maximal(1)[OF assms(12)]) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

230 
apply(rule,rule) apply(drule_tac assms(3)[rule_format],assumption) using kle_imp_pointwise by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

231 
then guess a .. note a=this show ?thesis apply(rule_tac x=a in bexI) proof fix x assume "x\<in>s" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

232 
show "kle n a x" using assms(3)[rule_format,OF a(1) `x\<in>s`] apply proof(erule disjE) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

233 
assume "kle n x a" hence "x = a" apply unfolding pointwise_antisym[THEN sym] 
41958  234 
apply(drule kle_imp_pointwise) using a(2)[rule_format,OF `x\<in>s`] by auto 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

235 
thus ?thesis using kle_refl by auto qed qed(insert a, auto) qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

236 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

237 
lemma kle_maximal: assumes "finite s" "s \<noteq> {}" "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

238 
shows "\<exists>a\<in>s. \<forall>x\<in>s. kle n x a" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

239 
have "\<exists>a\<in>s. \<forall>x\<in>s. \<forall>j. a j \<ge> x j" apply(rule pointwise_minimal_pointwise_maximal(2)[OF assms(12)]) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

240 
apply(rule,rule) apply(drule_tac assms(3)[rule_format],assumption) using kle_imp_pointwise by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

241 
then guess a .. note a=this show ?thesis apply(rule_tac x=a in bexI) proof fix x assume "x\<in>s" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

242 
show "kle n x a" using assms(3)[rule_format,OF a(1) `x\<in>s`] apply proof(erule disjE) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

243 
assume "kle n a x" hence "x = a" apply unfolding pointwise_antisym[THEN sym] 
41958  244 
apply(drule kle_imp_pointwise) using a(2)[rule_format,OF `x\<in>s`] by auto 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

245 
thus ?thesis using kle_refl by auto qed qed(insert a, auto) qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

246 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

247 
lemma kle_strict_set: assumes "kle n x y" "x \<noteq> y" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

248 
shows "1 \<le> card {k\<in>{1..n}. x k < y k}" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

249 
guess i using kle_strict(2)[OF assms] .. 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

250 
hence "card {i} \<le> card {k\<in>{1..n}. x k < y k}" apply apply(rule card_mono) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

251 
thus ?thesis by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

252 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

253 
lemma kle_range_combine: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

254 
assumes "kle n x y" "kle n y z" "kle n x z \<or> kle n z x" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

255 
"m1 \<le> card {k\<in>{1..n}. x k < y k}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

256 
"m2 \<le> card {k\<in>{1..n}. y k < z k}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

257 
shows "kle n x z \<and> m1 + m2 \<le> card {k\<in>{1..n}. x k < z k}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

258 
apply(rule,rule kle_trans[OF assms(13)]) proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

259 
have "\<And>j. x j < y j \<Longrightarrow> x j < z j" apply(rule less_le_trans) using kle_imp_pointwise[OF assms(2)] by auto moreover 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

260 
have "\<And>j. y j < z j \<Longrightarrow> x j < z j" apply(rule le_less_trans) using kle_imp_pointwise[OF assms(1)] by auto ultimately 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

261 
have *:"{k\<in>{1..n}. x k < y k} \<union> {k\<in>{1..n}. y k < z k} = {k\<in>{1..n}. x k < z k}" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

262 
have **:"{k \<in> {1..n}. x k < y k} \<inter> {k \<in> {1..n}. y k < z k} = {}" unfolding disjoint_iff_not_equal 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

263 
apply(rule,rule,unfold mem_Collect_eq,rule ccontr) apply(erule conjE)+ proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

264 
fix i j assume as:"i \<in> {1..n}" "x i < y i" "j \<in> {1..n}" "y j < z j" "\<not> i \<noteq> j" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

265 
guess kx using assms(1)[unfolded kle_def] .. note kx=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

266 
have "x i < y i" using as by auto hence "i \<in> kx" using as(1) kx apply(rule_tac ccontr) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

267 
hence "x i + 1 = y i" using kx by auto moreover 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

268 
guess ky using assms(2)[unfolded kle_def] .. note ky=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

269 
have "y i < z i" using as by auto hence "i \<in> ky" using as(1) ky apply(rule_tac ccontr) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

270 
hence "y i + 1 = z i" using ky by auto ultimately 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

271 
have "z i = x i + 2" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

272 
thus False using assms(3) unfolding kle_def by(auto simp add: split_if_eq1) qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

273 
have fin:"\<And>P. finite {x\<in>{1..n::nat}. P x}" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

274 
have "m1 + m2 \<le> card {k\<in>{1..n}. x k < y k} + card {k\<in>{1..n}. y k < z k}" using assms(45) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

275 
also have "\<dots> \<le> card {k\<in>{1..n}. x k < z k}" unfolding card_Un_Int[OF fin fin] unfolding * ** by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

276 
finally show " m1 + m2 \<le> card {k \<in> {1..n}. x k < z k}" by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

277 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

278 
lemma kle_range_combine_l: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

279 
assumes "kle n x y" "kle n y z" "kle n x z \<or> kle n z x" "m \<le> card {k\<in>{1..n}. y(k) < z(k)}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

280 
shows "kle n x z \<and> m \<le> card {k\<in>{1..n}. x(k) < z(k)}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

281 
using kle_range_combine[OF assms(13) _ assms(4), of 0] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

282 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

283 
lemma kle_range_combine_r: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

284 
assumes "kle n x y" "kle n y z" "kle n x z \<or> kle n z x" "m \<le> card {k\<in>{1..n}. x k < y k}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

285 
shows "kle n x z \<and> m \<le> card {k\<in>{1..n}. x(k) < z(k)}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

286 
using kle_range_combine[OF assms(13) assms(4), of 0] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

287 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

288 
lemma kle_range_induct: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

289 
assumes "card s = Suc m" "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

290 
shows "\<exists>x\<in>s. \<exists>y\<in>s. kle n x y \<and> m \<le> card {k\<in>{1..n}. x k < y k}" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

291 
have "finite s" "s\<noteq>{}" using assms(1) by (auto intro: card_ge_0_finite) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

292 
thus ?thesis using assms apply proof(induct m arbitrary: s) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

293 
case 0 thus ?case using kle_refl by auto next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

294 
case (Suc m) then obtain a where a:"a\<in>s" "\<forall>x\<in>s. kle n a x" using kle_minimal[of s n] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

295 
show ?case proof(cases "s \<subseteq> {a}") case False 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

296 
hence "card (s  {a}) = Suc m" "s  {a} \<noteq> {}" using card_Diff_singleton[OF _ a(1)] Suc(4) `finite s` by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

297 
then obtain x b where xb:"x\<in>s  {a}" "b\<in>s  {a}" "kle n x b" "m \<le> card {k \<in> {1..n}. x k < b k}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

298 
using Suc(1)[of "s  {a}"] using Suc(5) `finite s` by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

299 
have "1 \<le> card {k \<in> {1..n}. a k < x k}" "m \<le> card {k \<in> {1..n}. x k < b k}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

300 
apply(rule kle_strict_set) apply(rule a(2)[rule_format]) using a and xb by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

301 
thus ?thesis apply(rule_tac x=a in bexI, rule_tac x=b in bexI) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

302 
using kle_range_combine[OF a(2)[rule_format] xb(3) Suc(5)[rule_format], of 1 "m"] using a(1) xb(12) by auto next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

303 
case True hence "s = {a}" using Suc(3) by auto hence "card s = 1" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

304 
hence False using Suc(4) `finite s` by auto thus ?thesis by auto qed qed qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

305 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

306 
lemma kle_Suc: "kle n x y \<Longrightarrow> kle (n + 1) x y" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

307 
unfolding kle_def apply(erule exE) apply(rule_tac x=k in exI) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

308 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

309 
lemma kle_trans_1: assumes "kle n x y" shows "x j \<le> y j" "y j \<le> x j + 1" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

310 
using assms[unfolded kle_def] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

311 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

312 
lemma kle_trans_2: assumes "kle n a b" "kle n b c" "\<forall>j. c j \<le> a j + 1" shows "kle n a c" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

313 
guess kk1 using assms(1)[unfolded kle_def] .. note kk1=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

314 
guess kk2 using assms(2)[unfolded kle_def] .. note kk2=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

315 
show ?thesis unfolding kle_def apply(rule_tac x="kk1 \<union> kk2" in exI) apply(rule) defer proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

316 
fix i show "c i = a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)" proof(cases "i\<in>kk1 \<union> kk2") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

317 
case True hence "c i \<ge> a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)" 
41958  318 
unfolding kk1[THEN conjunct2,rule_format,of i] kk2[THEN conjunct2,rule_format,of i] by auto 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

319 
moreover have "c i \<le> a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)" using True assms(3) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

320 
ultimately show ?thesis by auto next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

321 
case False thus ?thesis using kk1 kk2 by auto qed qed(insert kk1 kk2, auto) qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

322 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

323 
lemma kle_between_r: assumes "kle n a b" "kle n b c" "kle n a x" "kle n c x" shows "kle n b x" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

324 
apply(rule kle_trans_2[OF assms(2,4)]) proof have *:"\<And>c b x::nat. x \<le> c + 1 \<Longrightarrow> c \<le> b \<Longrightarrow> x \<le> b + 1" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

325 
fix j show "x j \<le> b j + 1" apply(rule *)using kle_trans_1[OF assms(1),of j] kle_trans_1[OF assms(3), of j] by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

326 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

327 
lemma kle_between_l: assumes "kle n a b" "kle n b c" "kle n x a" "kle n x c" shows "kle n x b" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

328 
apply(rule kle_trans_2[OF assms(3,1)]) proof have *:"\<And>c b x::nat. c \<le> x + 1 \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> x + 1" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

329 
fix j show "b j \<le> x j + 1" apply(rule *) using kle_trans_1[OF assms(2),of j] kle_trans_1[OF assms(4), of j] by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

330 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

331 
lemma kle_adjacent: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

332 
assumes "\<forall>j. b j = (if j = k then a(j) + 1 else a j)" "kle n a x" "kle n x b" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

333 
shows "(x = a) \<or> (x = b)" proof(cases "x k = a k") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

334 
case True show ?thesis apply(rule disjI1,rule ext) proof fix j 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

335 
have "x j \<le> a j" using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

336 
unfolding assms(1)[rule_format] applyapply(cases "j=k") using True by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

337 
thus "x j = a j" using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]] by auto qed next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

338 
case False show ?thesis apply(rule disjI2,rule ext) proof fix j 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

339 
have "x j \<ge> b j" using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

340 
unfolding assms(1)[rule_format] applyapply(cases "j=k") using False by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

341 
thus "x j = b j" using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]] by auto qed qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

342 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

343 
subsection {* kuhn's notion of a simplex (a reformulation to avoid so much indexing). *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

344 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

345 
definition "ksimplex p n (s::(nat \<Rightarrow> nat) set) \<longleftrightarrow> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

346 
(card s = n + 1 \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

347 
(\<forall>x\<in>s. \<forall>j. x(j) \<le> p) \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

348 
(\<forall>x\<in>s. \<forall>j. j\<notin>{1..n} \<longrightarrow> (x j = p)) \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

349 
(\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

350 

36318  351 
lemma ksimplexI:"card s = n + 1 \<Longrightarrow> \<forall>x\<in>s. \<forall>j. x j \<le> p \<Longrightarrow> \<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p \<Longrightarrow> \<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x \<Longrightarrow> ksimplex p n s" 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

352 
unfolding ksimplex_def by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

353 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

354 
lemma ksimplex_eq: "ksimplex p n (s::(nat \<Rightarrow> nat) set) \<longleftrightarrow> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

355 
(card s = n + 1 \<and> finite s \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

356 
(\<forall>x\<in>s. \<forall>j. x(j) \<le> p) \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

357 
(\<forall>x\<in>s. \<forall>j. j\<notin>{1..n} \<longrightarrow> (x j = p)) \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

358 
(\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

359 
unfolding ksimplex_def by (auto intro: card_ge_0_finite) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

360 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

361 
lemma ksimplex_extrema: assumes "ksimplex p n s" obtains a b where "a \<in> s" "b \<in> s" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

362 
"\<forall>x\<in>s. kle n a x \<and> kle n x b" "\<forall>i. b(i) = (if i \<in> {1..n} then a(i) + 1 else a(i))" proof(cases "n=0") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

363 
case True obtain x where *:"s = {x}" using assms[unfolded ksimplex_eq True,THEN conjunct1] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

364 
unfolding add_0_left card_1_exists by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

365 
show ?thesis apply(rule that[of x x]) unfolding * True by auto next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

366 
note assm = assms[unfolded ksimplex_eq] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

367 
case False have "s\<noteq>{}" using assm by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

368 
obtain a where a:"a\<in>s" "\<forall>x\<in>s. kle n a x" using `s\<noteq>{}` assm using kle_minimal[of s n] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

369 
obtain b where b:"b\<in>s" "\<forall>x\<in>s. kle n x b" using `s\<noteq>{}` assm using kle_maximal[of s n] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

370 
obtain c d where c_d:"c\<in>s" "d\<in>s" "kle n c d" "n \<le> card {k \<in> {1..n}. c k < d k}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

371 
using kle_range_induct[of s n n] using assm by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

372 
have "kle n c b \<and> n \<le> card {k \<in> {1..n}. c k < b k}" apply(rule kle_range_combine_r[where y=d]) using c_d a b by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

373 
hence "kle n a b \<and> n \<le> card {k\<in>{1..n}. a(k) < b(k)}" applyapply(rule kle_range_combine_l[where y=c]) using a `c\<in>s` `b\<in>s` by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

374 
moreover have "card {1..n} \<ge> card {k\<in>{1..n}. a(k) < b(k)}" apply(rule card_mono) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

375 
ultimately have *:"{k\<in>{1 .. n}. a k < b k} = {1..n}" apply apply(rule card_subset_eq) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

376 
show ?thesis apply(rule that[OF a(1) b(1)]) defer apply(subst *[THEN sym]) unfolding mem_Collect_eq proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

377 
guess k using a(2)[rule_format,OF b(1),unfolded kle_def] .. note k=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

378 
fix i show "b i = (if i \<in> {1..n} \<and> a i < b i then a i + 1 else a i)" proof(cases "i \<in> {1..n}") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

379 
case True thus ?thesis unfolding k[THEN conjunct2,rule_format] by auto next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

380 
case False have "a i = p" using assm and False `a\<in>s` by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

381 
moreover have "b i = p" using assm and False `b\<in>s` by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

382 
ultimately show ?thesis by auto qed qed(insert a(2) b(2) assm,auto) qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

383 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

384 
lemma ksimplex_extrema_strong: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

385 
assumes "ksimplex p n s" "n \<noteq> 0" obtains a b where "a \<in> s" "b \<in> s" "a \<noteq> b" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

386 
"\<forall>x\<in>s. kle n a x \<and> kle n x b" "\<forall>i. b(i) = (if i \<in> {1..n} then a(i) + 1 else a(i))" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

387 
obtain a b where ab:"a \<in> s" "b \<in> s" "\<forall>x\<in>s. kle n a x \<and> kle n x b" "\<forall>i. b(i) = (if i \<in> {1..n} then a(i) + 1 else a(i))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

388 
apply(rule ksimplex_extrema[OF assms(1)]) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

389 
have "a \<noteq> b" apply(rule ccontr) unfolding not_not apply(drule cong[of _ _ 1 1]) using ab(4) assms(2) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

390 
thus ?thesis apply(rule_tac that[of a b]) using ab by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

391 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

392 
lemma ksimplexD: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

393 
assumes "ksimplex p n s" 
36318  394 
shows "card s = n + 1" "finite s" "card s = n + 1" "\<forall>x\<in>s. \<forall>j. x j \<le> p" "\<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p" 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

395 
"\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x" using assms unfolding ksimplex_eq by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

396 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

397 
lemma ksimplex_successor: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

398 
assumes "ksimplex p n s" "a \<in> s" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

399 
shows "(\<forall>x\<in>s. kle n x a) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y(j) = (if j = k then a(j) + 1 else a(j)))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

400 
proof(cases "\<forall>x\<in>s. kle n x a") case True thus ?thesis by auto next note assm = ksimplexD[OF assms(1)] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

401 
case False then obtain b where b:"b\<in>s" "\<not> kle n b a" "\<forall>x\<in>{x \<in> s. \<not> kle n x a}. kle n b x" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

402 
using kle_minimal[of "{x\<in>s. \<not> kle n x a}" n] and assm by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

403 
hence **:"1 \<le> card {k\<in>{1..n}. a k < b k}" apply apply(rule kle_strict_set) using assm(6) and `a\<in>s` by(auto simp add:kle_refl) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

404 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

405 
let ?kle1 = "{x \<in> s. \<not> kle n x a}" have "card ?kle1 > 0" apply(rule ccontr) using assm(2) and False by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

406 
hence sizekle1: "card ?kle1 = Suc (card ?kle1  1)" using assm(2) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

407 
obtain c d where c_d: "c \<in> s" "\<not> kle n c a" "d \<in> s" "\<not> kle n d a" "kle n c d" "card ?kle1  1 \<le> card {k \<in> {1..n}. c k < d k}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

408 
using kle_range_induct[OF sizekle1, of n] using assm by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

409 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

410 
let ?kle2 = "{x \<in> s. kle n x a}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

411 
have "card ?kle2 > 0" apply(rule ccontr) using assm(6)[rule_format,of a a] and `a\<in>s` and assm(2) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

412 
hence sizekle2:"card ?kle2 = Suc (card ?kle2  1)" using assm(2) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

413 
obtain e f where e_f: "e \<in> s" "kle n e a" "f \<in> s" "kle n f a" "kle n e f" "card ?kle2  1 \<le> card {k \<in> {1..n}. e k < f k}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

414 
using kle_range_induct[OF sizekle2, of n] using assm by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

415 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

416 
have "card {k\<in>{1..n}. a k < b k} = 1" proof(rule ccontr) case goal1 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

417 
hence as:"card {k\<in>{1..n}. a k < b k} \<ge> 2" using ** by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

418 
have *:"finite ?kle2" "finite ?kle1" "?kle2 \<union> ?kle1 = s" "?kle2 \<inter> ?kle1 = {}" using assm(2) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

419 
have "(card ?kle2  1) + 2 + (card ?kle1  1) = card ?kle2 + card ?kle1" using sizekle1 sizekle2 by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

420 
also have "\<dots> = n + 1" unfolding card_Un_Int[OF *(12)] *(3) using assm(3) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

421 
finally have n:"(card ?kle2  1) + (2 + (card ?kle1  1)) = n + 1" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

422 
have "kle n e a \<and> card {x \<in> s. kle n x a}  1 \<le> card {k \<in> {1..n}. e k < a k}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

423 
apply(rule kle_range_combine_r[where y=f]) using e_f using `a\<in>s` assm(6) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

424 
moreover have "kle n b d \<and> card {x \<in> s. \<not> kle n x a}  1 \<le> card {k \<in> {1..n}. b k < d k}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

425 
apply(rule kle_range_combine_l[where y=c]) using c_d using assm(6) and b by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

426 
hence "kle n a d \<and> 2 + (card {x \<in> s. \<not> kle n x a}  1) \<le> card {k \<in> {1..n}. a k < d k}" apply 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

427 
apply(rule kle_range_combine[where y=b]) using as and b assm(6) `a\<in>s` `d\<in>s` apply by blast+ 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

428 
ultimately have "kle n e d \<and> (card ?kle2  1) + (2 + (card ?kle1  1)) \<le> card {k\<in>{1..n}. e k < d k}" apply 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

429 
apply(rule kle_range_combine[where y=a]) using assm(6)[rule_format,OF `e\<in>s` `d\<in>s`] apply  by blast+ 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

430 
moreover have "card {k \<in> {1..n}. e k < d k} \<le> card {1..n}" apply(rule card_mono) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

431 
ultimately show False unfolding n by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

432 
then guess k unfolding card_1_exists .. note k=this[unfolded mem_Collect_eq] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

433 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

434 
show ?thesis apply(rule disjI2) apply(rule_tac x=b in bexI,rule_tac x=k in bexI) proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

435 
fix j::nat have "kle n a b" using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

436 
then guess kk unfolding kle_def .. note kk_raw=this note kk=this[THEN conjunct2,rule_format] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

437 
have kkk:"k\<in>kk" apply(rule ccontr) using k(1) unfolding kk by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

438 
show "b j = (if j = k then a j + 1 else a j)" proof(cases "j\<in>kk") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

439 
case True hence "j=k" applyapply(rule k(2)[rule_format]) using kk_raw kkk by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

440 
thus ?thesis unfolding kk using kkk by auto next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

441 
case False hence "j\<noteq>k" using k(2)[rule_format, of j k] using kk_raw kkk by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

442 
thus ?thesis unfolding kk using kkk using False by auto qed qed(insert k(1) `b\<in>s`, auto) qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

443 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

444 
lemma ksimplex_predecessor: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

445 
assumes "ksimplex p n s" "a \<in> s" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

446 
shows "(\<forall>x\<in>s. kle n a x) \<or> (\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a(j) = (if j = k then y(j) + 1 else y(j)))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

447 
proof(cases "\<forall>x\<in>s. kle n a x") case True thus ?thesis by auto next note assm = ksimplexD[OF assms(1)] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

448 
case False then obtain b where b:"b\<in>s" "\<not> kle n a b" "\<forall>x\<in>{x \<in> s. \<not> kle n a x}. kle n x b" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

449 
using kle_maximal[of "{x\<in>s. \<not> kle n a x}" n] and assm by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

450 
hence **:"1 \<le> card {k\<in>{1..n}. a k > b k}" apply apply(rule kle_strict_set) using assm(6) and `a\<in>s` by(auto simp add:kle_refl) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

451 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

452 
let ?kle1 = "{x \<in> s. \<not> kle n a x}" have "card ?kle1 > 0" apply(rule ccontr) using assm(2) and False by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

453 
hence sizekle1:"card ?kle1 = Suc (card ?kle1  1)" using assm(2) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

454 
obtain c d where c_d: "c \<in> s" "\<not> kle n a c" "d \<in> s" "\<not> kle n a d" "kle n d c" "card ?kle1  1 \<le> card {k \<in> {1..n}. c k > d k}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

455 
using kle_range_induct[OF sizekle1, of n] using assm by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

456 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

457 
let ?kle2 = "{x \<in> s. kle n a x}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

458 
have "card ?kle2 > 0" apply(rule ccontr) using assm(6)[rule_format,of a a] and `a\<in>s` and assm(2) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

459 
hence sizekle2:"card ?kle2 = Suc (card ?kle2  1)" using assm(2) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

460 
obtain e f where e_f: "e \<in> s" "kle n a e" "f \<in> s" "kle n a f" "kle n f e" "card ?kle2  1 \<le> card {k \<in> {1..n}. e k > f k}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

461 
using kle_range_induct[OF sizekle2, of n] using assm by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

462 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

463 
have "card {k\<in>{1..n}. a k > b k} = 1" proof(rule ccontr) case goal1 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

464 
hence as:"card {k\<in>{1..n}. a k > b k} \<ge> 2" using ** by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

465 
have *:"finite ?kle2" "finite ?kle1" "?kle2 \<union> ?kle1 = s" "?kle2 \<inter> ?kle1 = {}" using assm(2) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

466 
have "(card ?kle2  1) + 2 + (card ?kle1  1) = card ?kle2 + card ?kle1" using sizekle1 sizekle2 by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

467 
also have "\<dots> = n + 1" unfolding card_Un_Int[OF *(12)] *(3) using assm(3) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

468 
finally have n:"(card ?kle1  1) + 2 + (card ?kle2  1) = n + 1" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

469 
have "kle n a e \<and> card {x \<in> s. kle n a x}  1 \<le> card {k \<in> {1..n}. e k > a k}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

470 
apply(rule kle_range_combine_l[where y=f]) using e_f using `a\<in>s` assm(6) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

471 
moreover have "kle n d b \<and> card {x \<in> s. \<not> kle n a x}  1 \<le> card {k \<in> {1..n}. b k > d k}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

472 
apply(rule kle_range_combine_r[where y=c]) using c_d using assm(6) and b by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

473 
hence "kle n d a \<and> (card {x \<in> s. \<not> kle n a x}  1) + 2 \<le> card {k \<in> {1..n}. a k > d k}" apply 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

474 
apply(rule kle_range_combine[where y=b]) using as and b assm(6) `a\<in>s` `d\<in>s` by blast+ 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

475 
ultimately have "kle n d e \<and> (card ?kle1  1 + 2) + (card ?kle2  1) \<le> card {k\<in>{1..n}. e k > d k}" apply 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

476 
apply(rule kle_range_combine[where y=a]) using assm(6)[rule_format,OF `e\<in>s` `d\<in>s`] apply  by blast+ 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

477 
moreover have "card {k \<in> {1..n}. e k > d k} \<le> card {1..n}" apply(rule card_mono) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

478 
ultimately show False unfolding n by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

479 
then guess k unfolding card_1_exists .. note k=this[unfolded mem_Collect_eq] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

480 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

481 
show ?thesis apply(rule disjI2) apply(rule_tac x=b in bexI,rule_tac x=k in bexI) proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

482 
fix j::nat have "kle n b a" using b and assm(6)[rule_format, OF `a\<in>s` `b\<in>s`] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

483 
then guess kk unfolding kle_def .. note kk_raw=this note kk=this[THEN conjunct2,rule_format] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

484 
have kkk:"k\<in>kk" apply(rule ccontr) using k(1) unfolding kk by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

485 
show "a j = (if j = k then b j + 1 else b j)" proof(cases "j\<in>kk") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

486 
case True hence "j=k" applyapply(rule k(2)[rule_format]) using kk_raw kkk by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

487 
thus ?thesis unfolding kk using kkk by auto next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

488 
case False hence "j\<noteq>k" using k(2)[rule_format, of j k] using kk_raw kkk by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

489 
thus ?thesis unfolding kk using kkk using False by auto qed qed(insert k(1) `b\<in>s`, auto) qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

490 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

491 
subsection {* The lemmas about simplices that we need. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

492 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

493 
lemma card_funspace': assumes "finite s" "finite t" "card s = m" "card t = n" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

494 
shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV  s. f x = d)} = n ^ m" (is "card (?M s) = _") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

495 
using assms apply  proof(induct m arbitrary: s) 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

496 
have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" apply(rule set_eqI,rule)unfolding mem_Collect_eq apply(rule,rule ext) by auto 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

497 
case 0 thus ?case by(auto simp add: *) next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

498 
case (Suc m) guess a using card_eq_SucD[OF Suc(4)] .. then guess s0 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

499 
apply(erule_tac exE) apply(erule conjE)+ . note as0 = this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

500 
have **:"card s0 = m" using as0 using Suc(2) Suc(4) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

501 
let ?l = "(\<lambda>(b,g) x. if x = a then b else g x)" have *:"?M (insert a s0) = ?l ` {(b,g). b\<in>t \<and> g\<in>?M s0}" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

502 
apply(rule set_eqI,rule) unfolding mem_Collect_eq image_iff apply(erule conjE) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

503 
apply(rule_tac x="(x a, \<lambda>y. if y\<in>s0 then x y else d)" in bexI) apply(rule ext) prefer 3 apply rule defer 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

504 
apply(erule bexE,rule) unfolding mem_Collect_eq apply(erule splitE)+ apply(erule conjE)+ proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

505 
fix x xa xb xc y assume as:"x = (\<lambda>(b, g) x. if x = a then b else g x) xa" "xb \<in> UNIV  insert a s0" "xa = (xc, y)" "xc \<in> t" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

506 
"\<forall>x\<in>s0. y x \<in> t" "\<forall>x\<in>UNIV  s0. y x = d" thus "x xb = d" unfolding as by auto qed auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

507 
have inj:"inj_on ?l {(b,g). b\<in>t \<and> g\<in>?M s0}" unfolding inj_on_def apply(rule,rule,rule) unfolding mem_Collect_eq apply(erule splitE conjE)+ proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

508 
case goal1 note as = this(1,4)[unfolded goal1 split_conv] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

509 
have "xa = xb" using as(1)[THEN cong[of _ _ a]] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

510 
moreover have "ya = yb" proof(rule ext) fix x show "ya x = yb x" proof(cases "x = a") 
41958  511 
case False thus ?thesis using as(1)[THEN cong[of _ _ x x]] by auto next 
512 
case True thus ?thesis using as(5,7) using as0(2) by auto qed qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

513 
ultimately show ?case unfolding goal1 by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

514 
have "finite s0" using `finite s` unfolding as0 by simp 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

515 
show ?case unfolding as0 * card_image[OF inj] using assms 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

516 
unfolding SetCompr_Sigma_eq apply 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

517 
unfolding card_cartesian_product 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

518 
using Suc(1)[OF `finite s0` `finite t` ** `card t = n`] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

519 
qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

520 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

521 
lemma card_funspace: assumes "finite s" "finite t" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

522 
shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV  s. f x = d)} = (card t) ^ (card s)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

523 
using assms by (auto intro: card_funspace') 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

524 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

525 
lemma finite_funspace: assumes "finite s" "finite t" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

526 
shows "finite {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV  s. f x = d)}" (is "finite ?S") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

527 
proof (cases "card t > 0") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

528 
case True 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

529 
have "card ?S = (card t) ^ (card s)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

530 
using assms by (auto intro!: card_funspace) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

531 
thus ?thesis using True by (auto intro: card_ge_0_finite) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

532 
next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

533 
case False hence "t = {}" using `finite t` by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

534 
show ?thesis 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

535 
proof (cases "s = {}") 
44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44282
diff
changeset

536 
have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" by auto 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

537 
case True thus ?thesis using `t = {}` by (auto simp: *) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

538 
next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

539 
case False thus ?thesis using `t = {}` by simp 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

540 
qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

541 
qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

542 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

543 
lemma finite_simplices: "finite {s. ksimplex p n s}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

544 
apply(rule finite_subset[of _ "{s. s\<subseteq>{f. (\<forall>i\<in>{1..n}. f i \<in> {0..p}) \<and> (\<forall>i\<in>UNIV{1..n}. f i = p)}}"]) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

545 
unfolding ksimplex_def defer apply(rule finite_Collect_subsets) apply(rule finite_funspace) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

546 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

547 
lemma simplex_top_face: assumes "0<p" "\<forall>x\<in>f. x (n + 1) = p" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

548 
shows "(\<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s  {a})) \<longleftrightarrow> ksimplex p n f" (is "?ls = ?rs") proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

549 
assume ?ls then guess s .. then guess a applyapply(erule exE,(erule conjE)+) . note sa=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

550 
show ?rs unfolding ksimplex_def sa(3) apply(rule) defer apply rule defer apply(rule,rule,rule,rule) defer apply(rule,rule) proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

551 
fix x y assume as:"x \<in>s  {a}" "y \<in>s  {a}" have xyp:"x (n + 1) = y (n + 1)" 
41958  552 
using as(1)[unfolded sa(3)[THEN sym], THEN assms(2)[rule_format]] 
553 
using as(2)[unfolded sa(3)[THEN sym], THEN assms(2)[rule_format]] by auto 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

554 
show "kle n x y \<or> kle n y x" proof(cases "kle (n + 1) x y") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

555 
case True then guess k unfolding kle_def .. note k=this hence *:"n+1 \<notin> k" using xyp by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

556 
have "\<not> (\<exists>x\<in>k. x\<notin>{1..n})" apply(rule ccontr) unfolding not_not apply(erule bexE) proof 
41958  557 
fix x assume as:"x \<in> k" "x \<notin> {1..n}" have "x \<noteq> n+1" using as and * by auto 
558 
thus False using as and k[THEN conjunct1,unfolded subset_eq] by auto qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

559 
thus ?thesis applyapply(rule disjI1) unfolding kle_def using k apply(rule_tac x=k in exI) by auto next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

560 
case False hence "kle (n + 1) y x" using ksimplexD(6)[OF sa(1),rule_format, of x y] using as by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

561 
then guess k unfolding kle_def .. note k=this hence *:"n+1 \<notin> k" using xyp by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

562 
hence "\<not> (\<exists>x\<in>k. x\<notin>{1..n})" applyapply(rule ccontr) unfolding not_not apply(erule bexE) proof 
41958  563 
fix x assume as:"x \<in> k" "x \<notin> {1..n}" have "x \<noteq> n+1" using as and * by auto 
564 
thus False using as and k[THEN conjunct1,unfolded subset_eq] by auto qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

565 
thus ?thesis applyapply(rule disjI2) unfolding kle_def using k apply(rule_tac x=k in exI) by auto qed next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

566 
fix x j assume as:"x\<in>s  {a}" "j\<notin>{1..n}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

567 
thus "x j = p" using as(1)[unfolded sa(3)[THEN sym], THEN assms(2)[rule_format]] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

568 
apply(cases "j = n+1") using sa(1)[unfolded ksimplex_def] by auto qed(insert sa ksimplexD[OF sa(1)], auto) next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

569 
assume ?rs note rs=ksimplexD[OF this] guess a b apply(rule ksimplex_extrema[OF `?rs`]) . note ab = this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

570 
def c \<equiv> "\<lambda>i. if i = (n + 1) then p  1 else a i" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

571 
have "c\<notin>f" apply(rule ccontr) unfolding not_not apply(drule assms(2)[rule_format]) unfolding c_def using assms(1) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

572 
thus ?ls apply(rule_tac x="insert c f" in exI,rule_tac x=c in exI) unfolding ksimplex_def conj_assoc 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

573 
apply(rule conjI) defer apply(rule conjI) defer apply(rule conjI) defer apply(rule conjI) defer 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

574 
proof(rule_tac[35] ballI allI)+ 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

575 
fix x j assume x:"x \<in> insert c f" thus "x j \<le> p" proof (cases "x=c") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

576 
case True show ?thesis unfolding True c_def apply(cases "j=n+1") using ab(1) and rs(4) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

577 
qed(insert x rs(4), auto simp add:c_def) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

578 
show "j \<notin> {1..n + 1} \<longrightarrow> x j = p" apply(cases "x=c") using x ab(1) rs(5) unfolding c_def by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

579 
{ fix z assume z:"z \<in> insert c f" hence "kle (n + 1) c z" apply(cases "z = c") (*defer apply(rule kle_Suc)*) proof 
41958  580 
case False hence "z\<in>f" using z by auto 
581 
then guess k apply(drule_tac ab(3)[THEN bspec[where x=z], THEN conjunct1]) unfolding kle_def apply(erule exE) . 

582 
thus "kle (n + 1) c z" unfolding kle_def apply(rule_tac x="insert (n + 1) k" in exI) unfolding c_def 

583 
using ab using rs(5)[rule_format,OF ab(1),of "n + 1"] assms(1) by auto qed auto } note * = this 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

584 
fix y assume y:"y \<in> insert c f" show "kle (n + 1) x y \<or> kle (n + 1) y x" proof(cases "x = c \<or> y = c") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

585 
case False hence **:"x\<in>f" "y\<in>f" using x y by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

586 
show ?thesis using rs(6)[rule_format,OF **] by(auto dest: kle_Suc) qed(insert * x y, auto) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

587 
qed(insert rs, auto) qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

588 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

589 
lemma ksimplex_fix_plane: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

590 
assumes "a \<in> s" "j\<in>{1..n::nat}" "\<forall>x\<in>s  {a}. x j = q" "a0 \<in> s" "a1 \<in> s" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

591 
"\<forall>i. a1 i = ((if i\<in>{1..n} then a0 i + 1 else a0 i)::nat)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

592 
shows "(a = a0) \<or> (a = a1)" proof have *:"\<And>P A x y. \<forall>x\<in>A. P x \<Longrightarrow> x\<in>A \<Longrightarrow> y\<in>A \<Longrightarrow> P x \<and> P y" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

593 
show ?thesis apply(rule ccontr) using *[OF assms(3), of a0 a1] unfolding assms(6)[THEN spec[where x=j]] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

594 
using assms(12,45) by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

595 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

596 
lemma ksimplex_fix_plane_0: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

597 
assumes "a \<in> s" "j\<in>{1..n::nat}" "\<forall>x\<in>s  {a}. x j = 0" "a0 \<in> s" "a1 \<in> s" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

598 
"\<forall>i. a1 i = ((if i\<in>{1..n} then a0 i + 1 else a0 i)::nat)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

599 
shows "a = a1" apply(rule ccontr) using ksimplex_fix_plane[OF assms] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

600 
using assms(3)[THEN bspec[where x=a1]] using assms(2,5) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

601 
unfolding assms(6)[THEN spec[where x=j]] by simp 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

602 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

603 
lemma ksimplex_fix_plane_p: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

604 
assumes "ksimplex p n s" "a \<in> s" "j\<in>{1..n}" "\<forall>x\<in>s  {a}. x j = p" "a0 \<in> s" "a1 \<in> s" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

605 
"\<forall>i. a1 i = (if i\<in>{1..n} then a0 i + 1 else a0 i)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

606 
shows "a = a0" proof(rule ccontr) note s = ksimplexD[OF assms(1),rule_format] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

607 
assume as:"a \<noteq> a0" hence *:"a0 \<in> s  {a}" using assms(5) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

608 
hence "a1 = a" using ksimplex_fix_plane[OF assms(2)] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

609 
thus False using as using assms(3,5) and assms(7)[rule_format,of j] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

610 
unfolding assms(4)[rule_format,OF *] using s(4)[OF assms(6), of j] by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

611 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

612 
lemma ksimplex_replace_0: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

613 
assumes "ksimplex p n s" "a \<in> s" "n \<noteq> 0" "j\<in>{1..n}" "\<forall>x\<in>s  {a}. x j = 0" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

614 
shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s'  {b} = s  {a})} = 1" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

615 
have *:"\<And>s' a a'. s'  {a'} = s  {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> (s' = s)" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

616 
have **:"\<And>s' a'. ksimplex p n s' \<Longrightarrow> a' \<in> s' \<Longrightarrow> s'  {a'} = s  {a} \<Longrightarrow> s' = s" proof case goal1 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

617 
guess a0 a1 apply(rule ksimplex_extrema_strong[OF assms(1,3)]) . note exta = this[rule_format] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

618 
have a:"a = a1" apply(rule ksimplex_fix_plane_0[OF assms(2,45)]) using exta(12,5) by auto moreover 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

619 
guess b0 b1 apply(rule ksimplex_extrema_strong[OF goal1(1) assms(3)]) . note extb = this[rule_format] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

620 
have a':"a' = b1" apply(rule ksimplex_fix_plane_0[OF goal1(2) assms(4), of b0]) unfolding goal1(3) using assms extb goal1 by auto moreover 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

621 
have "b0 = a0" unfolding kle_antisym[THEN sym, of b0 a0 n] using exta extb using goal1(3) unfolding a a' by blast 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

622 
hence "b1 = a1" applyapply(rule ext) unfolding exta(5) extb(5) by auto ultimately 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

623 
show "s' = s" applyapply(rule *[of _ a1 b1]) using exta(12) extb(12) goal1 by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

624 
show ?thesis unfolding card_1_exists applyapply(rule ex1I[of _ s]) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

625 
unfolding mem_Collect_eq defer apply(erule conjE bexE)+ apply(rule_tac a'=b in **) using assms(1,2) by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

626 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

627 
lemma ksimplex_replace_1: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

628 
assumes "ksimplex p n s" "a \<in> s" "n \<noteq> 0" "j\<in>{1..n}" "\<forall>x\<in>s  {a}. x j = p" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

629 
shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s'  {b} = s  {a})} = 1" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

630 
have lem:"\<And>a a' s'. s'  {a'} = s  {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

631 
have lem:"\<And>s' a'. ksimplex p n s' \<Longrightarrow> a'\<in>s' \<Longrightarrow> s'  {a'} = s  {a} \<Longrightarrow> s' = s" proof case goal1 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

632 
guess a0 a1 apply(rule ksimplex_extrema_strong[OF assms(1,3)]) . note exta = this[rule_format] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

633 
have a:"a = a0" apply(rule ksimplex_fix_plane_p[OF assms(12,45) exta(1,2)]) unfolding exta by auto moreover 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

634 
guess b0 b1 apply(rule ksimplex_extrema_strong[OF goal1(1) assms(3)]) . note extb = this[rule_format] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

635 
have a':"a' = b0" apply(rule ksimplex_fix_plane_p[OF goal1(12) assms(4), of _ b1]) unfolding goal1 extb using extb(1,2) assms(5) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

636 
moreover have *:"b1 = a1" unfolding kle_antisym[THEN sym, of b1 a1 n] using exta extb using goal1(3) unfolding a a' by blast moreover 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

637 
have "a0 = b0" apply(rule ext) proof case goal1 show "a0 x = b0 x" 
41958  638 
using *[THEN cong, of x x] unfolding exta extb applyapply(cases "x\<in>{1..n}") by auto qed 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

639 
ultimately show "s' = s" applyapply(rule lem[OF goal1(3) _ goal1(2) assms(2)]) by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

640 
show ?thesis unfolding card_1_exists apply(rule ex1I[of _ s]) unfolding mem_Collect_eq apply(rule,rule assms(1)) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

641 
apply(rule_tac x=a in bexI) prefer 3 apply(erule conjE bexE)+ apply(rule_tac a'=b in lem) using assms(12) by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

642 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

643 
lemma ksimplex_replace_2: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

644 
assumes "ksimplex p n s" "a \<in> s" "n \<noteq> 0" "~(\<exists>j\<in>{1..n}. \<forall>x\<in>s  {a}. x j = 0)" "~(\<exists>j\<in>{1..n}. \<forall>x\<in>s  {a}. x j = p)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

645 
shows "card {s'. ksimplex p n s' \<and> (\<exists>b\<in>s'. s'  {b} = s  {a})} = 2" (is "card ?A = 2") proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

646 
have lem1:"\<And>a a' s s'. s'  {a'} = s  {a} \<Longrightarrow> a' = a \<Longrightarrow> a' \<in> s' \<Longrightarrow> a \<in> s \<Longrightarrow> s' = s" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

647 
have lem2:"\<And>a b. a\<in>s \<Longrightarrow> b\<noteq>a \<Longrightarrow> s \<noteq> insert b (s  {a})" proof case goal1 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

648 
hence "a\<in>insert b (s  {a})" by auto hence "a\<in> s  {a}" unfolding insert_iff using goal1 by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

649 
thus False by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

650 
guess a0 a1 apply(rule ksimplex_extrema_strong[OF assms(1,3)]) . note a0a1=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

651 
{ assume "a=a0" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

652 
have *:"\<And>P Q. (P \<or> Q) \<Longrightarrow> \<not> P \<Longrightarrow> Q" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

653 
have "\<exists>x\<in>s. \<not> kle n x a0" apply(rule_tac x=a1 in bexI) proof assume as:"kle n a1 a0" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

654 
show False using kle_imp_pointwise[OF as,THEN spec[where x=1]] unfolding a0a1(5)[THEN spec[where x=1]] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

655 
using assms(3) by auto qed(insert a0a1,auto) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

656 
hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a0 j + 1 else a0 j)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

657 
apply(rule_tac *[OF ksimplex_successor[OF assms(12),unfolded `a=a0`]]) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

658 
then guess a2 .. from this(2) guess k .. note k=this note a2=`a2\<in>s` 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

659 
def a3 \<equiv> "\<lambda>j. if j = k then a1 j + 1 else a1 j" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

660 
have "a3 \<notin> s" proof assume "a3\<in>s" hence "kle n a3 a1" using a0a1(4) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

661 
thus False apply(drule_tac kle_imp_pointwise) unfolding a3_def 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

662 
apply(erule_tac x=k in allE) by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

663 
hence "a3 \<noteq> a0" "a3 \<noteq> a1" using a0a1 by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

664 
have "a2 \<noteq> a0" using k(2)[THEN spec[where x=k]] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

665 
have lem3:"\<And>x. x\<in>(s  {a0}) \<Longrightarrow> kle n a2 x" proof(rule ccontr) case goal1 hence as:"x\<in>s" "x\<noteq>a0" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

666 
have "kle n a2 x \<or> kle n x a2" using ksimplexD(6)[OF assms(1)] and as `a2\<in>s` by auto moreover 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

667 
have "kle n a0 x" using a0a1(4) as by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

668 
ultimately have "x = a0 \<or> x = a2" applyapply(rule kle_adjacent[OF k(2)]) using goal1(2) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

669 
hence "x = a2" using as by auto thus False using goal1(2) using kle_refl by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

670 
let ?s = "insert a3 (s  {a0})" have "ksimplex p n ?s" apply(rule ksimplexI) proof(rule_tac[2] ballI,rule_tac[4] ballI) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

671 
show "card ?s = n + 1" using ksimplexD(23)[OF assms(1)] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

672 
using `a3\<noteq>a0` `a3\<notin>s` `a0\<in>s` by(auto simp add:card_insert_if) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

673 
fix x assume x:"x \<in> insert a3 (s  {a0})" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

674 
show "\<forall>j. x j \<le> p" proof(rule,cases "x = a3") 
41958  675 
fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next 
676 
fix j case True show "x j\<le>p" unfolding True proof(cases "j=k") 

677 
case False thus "a3 j \<le>p" unfolding True a3_def using `a1\<in>s` ksimplexD(4)[OF assms(1)] by auto next 

678 
guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] .. note a4=this 

679 
have "a2 k \<le> a4 k" using lem3[OF a4(1)[unfolded `a=a0`],THEN kle_imp_pointwise] by auto 

680 
also have "\<dots> < p" using ksimplexD(4)[OF assms(1),rule_format,of a4 k] using a4 by auto 

681 
finally have *:"a0 k + 1 < p" unfolding k(2)[rule_format] by auto 

682 
case True thus "a3 j \<le>p" unfolding a3_def unfolding a0a1(5)[rule_format] 

683 
using k(1) k(2)assms(5) using * by simp qed qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

684 
show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p" proof(rule,rule,cases "x=a3") fix j::nat assume j:"j\<notin>{1..n}" 
41958  685 
{ case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto } 
686 
case True show "x j = p" unfolding True a3_def using j k(1) 

687 
using ksimplexD(5)[OF assms(1),rule_format,OF `a1\<in>s` j] by auto qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

688 
fix y assume y:"y\<in>insert a3 (s  {a0})" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

689 
have lem4:"\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a0 \<Longrightarrow> kle n x a3" proof case goal1 
41958  690 
guess kk using a0a1(4)[rule_format,OF `x\<in>s`,THEN conjunct2,unfolded kle_def] 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

691 
applyapply(erule exE,erule conjE) . note kk=this 
41958  692 
have "k\<notin>kk" proof assume "k\<in>kk" 
693 
hence "a1 k = x k + 1" using kk by auto 

694 
hence "a0 k = x k" unfolding a0a1(5)[rule_format] using k(1) by auto 

695 
hence "a2 k = x k + 1" unfolding k(2)[rule_format] by auto moreover 

696 
have "a2 k \<le> x k" using lem3[of x,THEN kle_imp_pointwise] goal1 by auto 

697 
ultimately show False by auto qed 

698 
thus ?case unfolding kle_def apply(rule_tac x="insert k kk" in exI) using kk(1) 

699 
unfolding a3_def kle_def kk(2)[rule_format] using k(1) by auto qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

700 
show "kle n x y \<or> kle n y x" proof(cases "y=a3") 
41958  701 
case True show ?thesis unfolding True apply(cases "x=a3") defer apply(rule disjI1,rule lem4) 
702 
using x by auto next 

703 
case False show ?thesis proof(cases "x=a3") case True show ?thesis unfolding True 

704 
apply(rule disjI2,rule lem4) using y False by auto next 

705 
case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) 

706 
using x y `y\<noteq>a3` by auto qed qed qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

707 
hence "insert a3 (s  {a0}) \<in> ?A" unfolding mem_Collect_eq applyapply(rule,assumption) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

708 
apply(rule_tac x="a3" in bexI) unfolding `a=a0` using `a3\<notin>s` by auto moreover 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

709 
have "s \<in> ?A" using assms(1,2) by auto ultimately have "?A \<supseteq> {s, insert a3 (s  {a0})}" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

710 
moreover have "?A \<subseteq> {s, insert a3 (s  {a0})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

711 
fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>s'. s'  {b} = s  {a}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

712 
from this(2) guess a' .. note a'=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

713 
guess a_min a_max apply(rule ksimplex_extrema_strong[OF as assms(3)]) . note min_max=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

714 
have *:"\<forall>x\<in>s'  {a'}. x k = a2 k" unfolding a' proof fix x assume x:"x\<in>s{a}" 
41958  715 
hence "kle n a2 x" applyapply(rule lem3) using `a=a0` by auto 
716 
hence "a2 k \<le> x k" apply(drule_tac kle_imp_pointwise) by auto moreover 

717 
have "x k \<le> a2 k" unfolding k(2)[rule_format] using a0a1(4)[rule_format,of x,THEN conjunct1] 

718 
unfolding kle_def using x by auto ultimately show "x k = a2 k" by auto qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

719 
have **:"a'=a_min \<or> a'=a_max" apply(rule ksimplex_fix_plane[OF a'(1) k(1) *]) using min_max by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

720 
show "s' \<in> {s, insert a3 (s  {a0})}" proof(cases "a'=a_min") 
41958  721 
case True have "a_max = a1" unfolding kle_antisym[THEN sym,of a_max a1 n] apply(rule) 
722 
apply(rule a0a1(4)[rule_format,THEN conjunct2]) defer proof(rule min_max(4)[rule_format,THEN conjunct2]) 

723 
show "a1\<in>s'" using a' unfolding `a=a0` using a0a1 by auto 

724 
show "a_max \<in> s" proof(rule ccontr) assume "a_max\<notin>s" 

725 
hence "a_max = a'" using a' min_max by auto 

726 
thus False unfolding True using min_max by auto qed qed 

727 
hence "\<forall>i. a_max i = a1 i" by auto 

728 
hence "a' = a" unfolding True `a=a0` applyapply(subst fun_eq_iff,rule) 

729 
apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format] 

730 
proof case goal1 thus ?case apply(cases "x\<in>{1..n}") by auto qed 

731 
hence "s' = s" applyapply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` by auto 

732 
thus ?thesis by auto next 

733 
case False hence as:"a' = a_max" using ** by auto 

734 
have "a_min = a2" unfolding kle_antisym[THEN sym, of _ _ n] apply rule 

735 
apply(rule min_max(4)[rule_format,THEN conjunct1]) defer proof(rule lem3) 

736 
show "a_min \<in> s  {a0}" unfolding a'(2)[THEN sym,unfolded `a=a0`] 

737 
unfolding as using min_max(13) by auto 

738 
have "a2 \<noteq> a" unfolding `a=a0` using k(2)[rule_format,of k] by auto 

739 
hence "a2 \<in> s  {a}" using a2 by auto thus "a2 \<in> s'" unfolding a'(2)[THEN sym] by auto qed 

740 
hence "\<forall>i. a_min i = a2 i" by auto 

741 
hence "a' = a3" unfolding as `a=a0` applyapply(subst fun_eq_iff,rule) 

742 
apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format] 

743 
unfolding a3_def k(2)[rule_format] unfolding a0a1(5)[rule_format] proof case goal1 

744 
show ?case unfolding goal1 apply(cases "x\<in>{1..n}") defer apply(cases "x=k") 

745 
using `k\<in>{1..n}` by auto qed 

746 
hence "s' = insert a3 (s  {a0})" applyapply(rule lem1) defer apply assumption 

747 
apply(rule a'(1)) unfolding a' `a=a0` using `a3\<notin>s` by auto 

748 
thus ?thesis by auto qed qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

749 
ultimately have *:"?A = {s, insert a3 (s  {a0})}" by blast 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

750 
have "s \<noteq> insert a3 (s  {a0})" using `a3\<notin>s` by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

751 
hence ?thesis unfolding * by auto } moreover 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

752 
{ assume "a=a1" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

753 
have *:"\<And>P Q. (P \<or> Q) \<Longrightarrow> \<not> P \<Longrightarrow> Q" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

754 
have "\<exists>x\<in>s. \<not> kle n a1 x" apply(rule_tac x=a0 in bexI) proof assume as:"kle n a1 a0" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

755 
show False using kle_imp_pointwise[OF as,THEN spec[where x=1]] unfolding a0a1(5)[THEN spec[where x=1]] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

756 
using assms(3) by auto qed(insert a0a1,auto) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

757 
hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a1 j = (if j = k then y j + 1 else y j)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

758 
apply(rule_tac *[OF ksimplex_predecessor[OF assms(12),unfolded `a=a1`]]) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

759 
then guess a2 .. from this(2) guess k .. note k=this note a2=`a2\<in>s` 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

760 
def a3 \<equiv> "\<lambda>j. if j = k then a0 j  1 else a0 j" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

761 
have "a2 \<noteq> a1" using k(2)[THEN spec[where x=k]] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

762 
have lem3:"\<And>x. x\<in>(s  {a1}) \<Longrightarrow> kle n x a2" proof(rule ccontr) case goal1 hence as:"x\<in>s" "x\<noteq>a1" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

763 
have "kle n a2 x \<or> kle n x a2" using ksimplexD(6)[OF assms(1)] and as `a2\<in>s` by auto moreover 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

764 
have "kle n x a1" using a0a1(4) as by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

765 
ultimately have "x = a2 \<or> x = a1" applyapply(rule kle_adjacent[OF k(2)]) using goal1(2) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

766 
hence "x = a2" using as by auto thus False using goal1(2) using kle_refl by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

767 
have "a0 k \<noteq> 0" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

768 
guess a4 using assms(4)[unfolded bex_simps ball_simps,rule_format,OF `k\<in>{1..n}`] .. note a4=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

769 
have "a4 k \<le> a2 k" using lem3[OF a4(1)[unfolded `a=a1`],THEN kle_imp_pointwise] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

770 
moreover have "a4 k > 0" using a4 by auto ultimately have "a2 k > 0" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

771 
hence "a1 k > 1" unfolding k(2)[rule_format] by simp 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

772 
thus ?thesis unfolding a0a1(5)[rule_format] using k(1) by simp qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

773 
hence lem4:"\<forall>j. a0 j = (if j=k then a3 j + 1 else a3 j)" unfolding a3_def by simp 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

774 
have "\<not> kle n a0 a3" apply(rule ccontr) unfolding not_not apply(drule kle_imp_pointwise) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

775 
unfolding lem4[rule_format] apply(erule_tac x=k in allE) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

776 
hence "a3 \<notin> s" using a0a1(4) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

777 
hence "a3 \<noteq> a1" "a3 \<noteq> a0" using a0a1 by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

778 
let ?s = "insert a3 (s  {a1})" have "ksimplex p n ?s" apply(rule ksimplexI) proof(rule_tac[2] ballI,rule_tac[4] ballI) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

779 
show "card ?s = n+1" using ksimplexD(23)[OF assms(1)] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

780 
using `a3\<noteq>a0` `a3\<notin>s` `a1\<in>s` by(auto simp add:card_insert_if) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

781 
fix x assume x:"x \<in> insert a3 (s  {a1})" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

782 
show "\<forall>j. x j \<le> p" proof(rule,cases "x = a3") 
41958  783 
fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next 
784 
fix j case True show "x j\<le>p" unfolding True proof(cases "j=k") 

785 
case False thus "a3 j \<le>p" unfolding True a3_def using `a0\<in>s` ksimplexD(4)[OF assms(1)] by auto next 

786 
guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] .. note a4=this 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

787 
case True have "a3 k \<le> a0 k" unfolding lem4[rule_format] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

788 
also have "\<dots> \<le> p" using ksimplexD(4)[OF assms(1),rule_format,of a0 k] a0a1 by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

789 
finally show "a3 j \<le> p" unfolding True by auto qed qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

790 
show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p" proof(rule,rule,cases "x=a3") fix j::nat assume j:"j\<notin>{1..n}" 
41958  791 
{ case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto } 
792 
case True show "x j = p" unfolding True a3_def using j k(1) 

793 
using ksimplexD(5)[OF assms(1),rule_format,OF `a0\<in>s` j] by auto qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

794 
fix y assume y:"y\<in>insert a3 (s  {a1})" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

795 
have lem4:"\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a1 \<Longrightarrow> kle n a3 x" proof case goal1 hence *:"x\<in>s  {a1}" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

796 
have "kle n a3 a2" proof have "kle n a0 a1" using a0a1 by auto then guess kk unfolding kle_def .. 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

797 
thus ?thesis unfolding kle_def apply(rule_tac x=kk in exI) unfolding lem4[rule_format] k(2)[rule_format] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

798 
apply(rule)defer proof(rule) case goal1 thus ?case applyapply(erule conjE) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

799 
apply(erule_tac[!] x=j in allE) apply(cases "j\<in>kk") apply(case_tac[!] "j=k") by auto qed auto qed moreover 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

800 
have "kle n a3 a0" unfolding kle_def lem4[rule_format] apply(rule_tac x="{k}" in exI) using k(1) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

801 
ultimately show ?case applyapply(rule kle_between_l[of _ a0 _ a2]) using lem3[OF *] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

802 
using a0a1(4)[rule_format,OF goal1(1)] by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

803 
show "kle n x y \<or> kle n y x" proof(cases "y=a3") 
41958  804 
case True show ?thesis unfolding True apply(cases "x=a3") defer apply(rule disjI2,rule lem4) 
805 
using x by auto next 

806 
case False show ?thesis proof(cases "x=a3") case True show ?thesis unfolding True 

807 
apply(rule disjI1,rule lem4) using y False by auto next 

808 
case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) 

809 
using x y `y\<noteq>a3` by auto qed qed qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

810 
hence "insert a3 (s  {a1}) \<in> ?A" unfolding mem_Collect_eq applyapply(rule,assumption) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

811 
apply(rule_tac x="a3" in bexI) unfolding `a=a1` using `a3\<notin>s` by auto moreover 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

812 
have "s \<in> ?A" using assms(1,2) by auto ultimately have "?A \<supseteq> {s, insert a3 (s  {a1})}" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

813 
moreover have "?A \<subseteq> {s, insert a3 (s  {a1})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

814 
fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>s'. s'  {b} = s  {a}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

815 
from this(2) guess a' .. note a'=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

816 
guess a_min a_max apply(rule ksimplex_extrema_strong[OF as assms(3)]) . note min_max=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

817 
have *:"\<forall>x\<in>s'  {a'}. x k = a2 k" unfolding a' proof fix x assume x:"x\<in>s{a}" 
41958  818 
hence "kle n x a2" applyapply(rule lem3) using `a=a1` by auto 
819 
hence "x k \<le> a2 k" apply(drule_tac kle_imp_pointwise) by auto moreover 

820 
{ have "a2 k \<le> a0 k" using k(2)[rule_format,of k] unfolding a0a1(5)[rule_format] using k(1) by simp 

821 
also have "\<dots> \<le> x k" using a0a1(4)[rule_format,of x,THEN conjunct1,THEN kle_imp_pointwise] x by auto 

822 
finally have "a2 k \<le> x k" . } ultimately show "x k = a2 k" by auto qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

823 
have **:"a'=a_min \<or> a'=a_max" apply(rule ksimplex_fix_plane[OF a'(1) k(1) *]) using min_max by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

824 
have "a2 \<noteq> a1" proof assume as:"a2 = a1" 
41958  825 
show False using k(2) unfolding as apply(erule_tac x=k in allE) by auto qed 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

826 
hence a2':"a2 \<in> s'  {a'}" unfolding a' using a2 unfolding `a=a1` by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

827 
show "s' \<in> {s, insert a3 (s  {a1})}" proof(cases "a'=a_min") 
41958  828 
case True have "a_max \<in> s  {a1}" using min_max unfolding a'(2)[unfolded `a=a1`,THEN sym] True by auto 
829 
hence "a_max = a2" unfolding kle_antisym[THEN sym,of a_max a2 n] applyapply(rule) 

830 
apply(rule lem3,assumption) apply(rule min_max(4)[rule_format,THEN conjunct2]) using a2' by auto 

831 
hence a_max:"\<forall>i. a_max i = a2 i" by auto 

832 
have *:"\<forall>j. a2 j = (if j\<in>{1..n} then a3 j + 1 else a3 j)" 

833 
using k(2) unfolding lem4[rule_format] a0a1(5)[rule_format] applyapply(rule,erule_tac x=j in allE) 

834 
proof case goal1 thus ?case apply(cases "j\<in>{1..n}",case_tac[!] "j=k") by auto qed 

835 
have "\<forall>i. a_min i = a3 i" using a_max applyapply(rule,erule_tac x=i in allE) 

836 
unfolding min_max(5)[rule_format] *[rule_format] proof case goal1 

837 
thus ?case apply(cases "i\<in>{1..n}") by auto qed hence "a_min = a3" unfolding fun_eq_iff . 

838 
hence "s' = insert a3 (s  {a1})" using a' unfolding `a=a1` True by auto thus ?thesis by auto next 

839 
case False hence as:"a'=a_max" using ** by auto 

840 
have "a_min = a0" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule) 

841 
apply(rule min_max(4)[rule_format,THEN conjunct1]) defer apply(rule a0a1(4)[rule_format,THEN conjunct1]) proof 

842 
have "a_min \<in> s  {a1}" using min_max(1,3) unfolding a'(2)[THEN sym,unfolded `a=a1`] as by auto 

843 
thus "a_min \<in> s" by auto have "a0 \<in> s  {a1}" using a0a1(13) by auto thus "a0 \<in> s'" 

844 
unfolding a'(2)[THEN sym,unfolded `a=a1`] by auto qed 

845 
hence "\<forall>i. a_max i = a1 i" unfolding a0a1(5)[rule_format] min_max(5)[rule_format] by auto 

846 
hence "s' = s" applyapply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` unfolding as `a=a1` unfolding fun_eq_iff by auto 

847 
thus ?thesis by auto qed qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

848 
ultimately have *:"?A = {s, insert a3 (s  {a1})}" by blast 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

849 
have "s \<noteq> insert a3 (s  {a1})" using `a3\<notin>s` by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

850 
hence ?thesis unfolding * by auto } moreover 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

851 
{ assume as:"a\<noteq>a0" "a\<noteq>a1" have "\<not> (\<forall>x\<in>s. kle n a x)" proof case goal1 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

852 
have "a=a0" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule) 
41958  853 
using goal1 a0a1 assms(2) by auto thus False using as by auto qed 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

854 
hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a j = (if j = k then y j + 1 else y j)" using ksimplex_predecessor[OF assms(12)] by blast 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

855 
then guess u .. from this(2) guess k .. note k = this[rule_format] note u = `u\<in>s` 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

856 
have "\<not> (\<forall>x\<in>s. kle n x a)" proof case goal1 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

857 
have "a=a1" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule) 
41958  858 
using goal1 a0a1 assms(2) by auto thus False using as by auto qed 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

859 
hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a j + 1 else a j)" using ksimplex_successor[OF assms(12)] by blast 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

860 
then guess v .. from this(2) guess l .. note l = this[rule_format] note v = `v\<in>s` 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

861 
def a' \<equiv> "\<lambda>j. if j = l then u j + 1 else u j" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

862 
have kl:"k \<noteq> l" proof assume "k=l" have *:"\<And>P. (if P then (1::nat) else 0) \<noteq> 2" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

863 
thus False using ksimplexD(6)[OF assms(1),rule_format,OF u v] unfolding kle_def 
41958  864 
unfolding l(2) k(2) `k=l` applyapply(erule disjE)apply(erule_tac[!] exE conjE)+ 
865 
apply(erule_tac[!] x=l in allE)+ by(auto simp add: *) qed 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

866 
hence aa':"a'\<noteq>a" applyapply rule unfolding fun_eq_iff unfolding a'_def k(2) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

867 
apply(erule_tac x=l in allE) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

868 
have "a' \<notin> s" apply(rule) apply(drule ksimplexD(6)[OF assms(1),rule_format,OF `a\<in>s`]) proof(cases "kle n a a'") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

869 
case goal2 hence "kle n a' a" by auto thus False apply(drule_tac kle_imp_pointwise) 
41958  870 
apply(erule_tac x=l in allE) unfolding a'_def k(2) using kl by auto next 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

871 
case True thus False apply(drule_tac kle_imp_pointwise) 
41958  872 
apply(erule_tac x=k in allE) unfolding a'_def k(2) using kl by auto qed 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

873 
have kle_uv:"kle n u a" "kle n u a'" "kle n a v" "kle n a' v" unfolding kle_def apply 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

874 
apply(rule_tac[1] x="{k}" in exI,rule_tac[2] x="{l}" in exI) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

875 
apply(rule_tac[3] x="{l}" in exI,rule_tac[4] x="{k}" in exI) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

876 
unfolding l(2) k(2) a'_def using l(1) k(1) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

877 
have uxv:"\<And>x. kle n u x \<Longrightarrow> kle n x v \<Longrightarrow> (x = u) \<or> (x = a) \<or> (x = a') \<or> (x = v)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

878 
proof case goal1 thus ?case proof(cases "x k = u k", case_tac[!] "x l = u l") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

879 
assume as:"x l = u l" "x k = u k" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

880 
have "x = u" unfolding fun_eq_iff 
41958  881 
using goal1(2)[THEN kle_imp_pointwise,unfolded l(2)] unfolding k(2) apply 
882 
using goal1(1)[THEN kle_imp_pointwise] applyapply rule apply(erule_tac x=xa in allE)+ proof case goal1 

883 
thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

884 
assume as:"x l \<noteq> u l" "x k = u k" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

885 
have "x = a'" unfolding fun_eq_iff unfolding a'_def 
41958  886 
using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply 
887 
using goal1(1)[THEN kle_imp_pointwise] applyapply rule apply(erule_tac x=xa in allE)+ proof case goal1 

888 
thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

889 
assume as:"x l = u l" "x k \<noteq> u k" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

890 
have "x = a" unfolding fun_eq_iff 
41958  891 
using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply 
892 
using goal1(1)[THEN kle_imp_pointwise] applyapply rule apply(erule_tac x=xa in allE)+ proof case goal1 

893 
thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

894 
assume as:"x l \<noteq> u l" "x k \<noteq> u k" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

895 
have "x = v" unfolding fun_eq_iff 
41958  896 
using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply 
897 
using goal1(1)[THEN kle_imp_pointwise] applyapply rule apply(erule_tac x=xa in allE)+ proof case goal1 

898 
thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as `k\<noteq>l` by auto qed thus ?case by auto qed qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

899 
have uv:"kle n u v" apply(rule kle_trans[OF kle_uv(1,3)]) using ksimplexD(6)[OF assms(1)] using u v by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

900 
have lem3:"\<And>x. x\<in>s \<Longrightarrow> kle n v x \<Longrightarrow> kle n a' x" apply(rule kle_between_r[of _ u _ v]) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

901 
prefer 3 apply(rule kle_trans[OF uv]) defer apply(rule ksimplexD(6)[OF assms(1),rule_format]) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

902 
using kle_uv `u\<in>s` by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

903 
have lem4:"\<And>x. x\<in>s \<Longrightarrow> kle n x u \<Longrightarrow> kle n x a'" apply(rule kle_between_l[of _ u _ v]) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

904 
prefer 4 apply(rule kle_trans[OF _ uv]) defer apply(rule ksimplexD(6)[OF assms(1),rule_format]) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

905 
using kle_uv `v\<in>s` by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

906 
have lem5:"\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a \<Longrightarrow> kle n x a' \<or> kle n a' x" proof case goal1 thus ?case 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

907 
proof(cases "kle n v x \<or> kle n x u") case True thus ?thesis using goal1 by(auto intro:lem3 lem4) next 
41958  908 
case False hence *:"kle n u x" "kle n x v" using ksimplexD(6)[OF assms(1)] using goal1 `u\<in>s` `v\<in>s` by auto 
909 
show ?thesis using uxv[OF *] using kle_uv using goal1 by auto qed qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

910 
have "ksimplex p n (insert a' (s  {a}))" apply(rule ksimplexI) proof(rule_tac[2] ballI,rule_tac[4] ballI) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

911 
show "card (insert a' (s  {a})) = n + 1" using ksimplexD(23)[OF assms(1)] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

912 
using `a'\<noteq>a` `a'\<notin>s` `a\<in>s` by(auto simp add:card_insert_if) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

913 
fix x assume x:"x \<in> insert a' (s  {a})" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

914 
show "\<forall>j. x j \<le> p" proof(rule,cases "x = a'") 
41958  915 
fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next 
916 
fix j case True show "x j\<le>p" unfolding True proof(cases "j=l") 

917 
case False thus "a' j \<le>p" unfolding True a'_def using `u\<in>s` ksimplexD(4)[OF assms(1)] by auto next 

918 
case True have *:"a l = u l" "v l = a l + 1" using k(2)[of l] l(2)[of l] `k\<noteq>l` by auto 

919 
have "u l + 1 \<le> p" unfolding *[THEN sym] using ksimplexD(4)[OF assms(1)] using `v\<in>s` by auto 

920 
thus "a' j \<le>p" unfolding a'_def True by auto qed qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

921 
show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p" proof(rule,rule,cases "x=a'") fix j::nat assume j:"j\<notin>{1..n}" 
41958  922 
{ case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto } 
923 
case True show "x j = p" unfolding True a'_def using j l(1) 

924 
using ksimplexD(5)[OF assms(1),rule_format,OF `u\<in>s` j] by auto qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

925 
fix y assume y:"y\<in>insert a' (s  {a})" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

926 
show "kle n x y \<or> kle n y x" proof(cases "y=a'") 
41958  927 
case True show ?thesis unfolding True apply(cases "x=a'") defer apply(rule lem5) using x by auto next 
928 
case False show ?thesis proof(cases "x=a'") case True show ?thesis unfolding True 

929 
using lem5[of y] using y by auto next 

930 
case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) 

931 
using x y `y\<noteq>a'` by auto qed qed qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

932 
hence "insert a' (s  {a}) \<in> ?A" unfolding mem_Collect_eq applyapply(rule,assumption) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

933 
apply(rule_tac x="a'" in bexI) using aa' `a'\<notin>s` by auto moreover 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

934 
have "s \<in> ?A" using assms(1,2) by auto ultimately have "?A \<supseteq> {s, insert a' (s  {a})}" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

935 
moreover have "?A \<subseteq> {s, insert a' (s  {a})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

936 
fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>s'. s'  {b} = s  {a}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

937 
from this(2) guess a'' .. note a''=this 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

938 
have "u\<noteq>v" unfolding fun_eq_iff unfolding l(2) k(2) by auto 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

939 
hence uv':"\<not> kle n v u" using uv using kle_antisym by auto 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

940 
have "u\<noteq>a" "v\<noteq>a" unfolding fun_eq_iff k(2) l(2) by auto 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

941 
hence uvs':"u\<in>s'" "v\<in>s'" using `u\<in>s` `v\<in>s` using a'' by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

942 
have lem6:"a \<in> s' \<or> a' \<in> s'" proof(cases "\<forall>x\<in>s'. kle n x u \<or> kle n v x") 
41958  943 
case False then guess w unfolding ball_simps .. note w=this 
944 
hence "kle n u w" "kle n w v" using ksimplexD(6)[OF as] uvs' by auto 

945 
hence "w = a' \<or> w = a" using uxv[of w] uvs' w by auto thus ?thesis using w by auto next 

946 
case True have "\<not> (\<forall>x\<in>s'. kle n x u)" unfolding ball_simps apply(rule_tac x=v in bexI) 

947 
using uv `u\<noteq>v` unfolding kle_antisym[of n u v,THEN sym] using `v\<in>s'` by auto 

948 
hence "\<exists>y\<in>s'. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then u j + 1 else u j)" using ksimplex_successor[OF as `u\<in>s'`] by blast 

949 
then guess w .. note w=this from this(2) guess kk .. note kk=this[rule_format] 

950 
have "\<not> kle n w u" applyapply(rule,drule kle_imp_pointwise) 

951 
apply(erule_tac x=kk in allE) unfolding kk by auto 

952 
hence *:"kle n v w" using True[rule_format,OF w(1)] by auto 

953 
hence False proof(cases "kk\<noteq>l") case True thus False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)] 

954 
apply(erule_tac x=l in allE) using `k\<noteq>l` by auto next 

955 
case False hence "kk\<noteq>k" using `k\<noteq>l` by auto thus False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)] 

956 
apply(erule_tac x=k in allE) using `k\<noteq>l` by auto qed 

957 
thus ?thesis by auto qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

958 
thus "s' \<in> {s, insert a' (s  {a})}" proof(cases "a\<in>s'") 
41958  959 
case True hence "s' = s" applyapply(rule lem1[OF a''(2)]) using a'' `a\<in>s` by auto 
960 
thus ?thesis by auto next case False hence "a'\<in>s'" using lem6 by auto 

961 
hence "s' = insert a' (s  {a})" applyapply(rule lem1[of _ a'' _ a']) 

962 
unfolding a''(2)[THEN sym] using a'' using `a'\<notin>s` by auto 

963 
thus ?thesis by auto qed qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

964 
ultimately have *:"?A = {s, insert a' (s  {a})}" by blast 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

965 
have "s \<noteq> insert a' (s  {a})" using `a'\<notin>s` by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

966 
hence ?thesis unfolding * by auto } 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

967 
ultimately show ?thesis by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

968 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

969 
subsection {* Hence another step towards concreteness. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

970 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

971 
lemma kuhn_simplex_lemma: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

972 
assumes "\<forall>s. ksimplex p (n + 1) s \<longrightarrow> (rl ` s \<subseteq>{0..n+1})" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

973 
"odd (card{f. \<exists>s a. ksimplex p (n + 1) s \<and> a \<in> s \<and> (f = s  {a}) \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

974 
(rl ` f = {0 .. n}) \<and> ((\<exists>j\<in>{1..n+1}.\<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}.\<forall>x\<in>f. x j = p))})" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

975 
shows "odd(card {s\<in>{s. ksimplex p (n + 1) s}. rl ` s = {0..n+1} })" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

976 
have *:"\<And>x y. x = y \<Longrightarrow> odd (card x) \<Longrightarrow> odd (card y)" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

977 
have *:"odd(card {f\<in>{f. \<exists>s\<in>{s. ksimplex p (n + 1) s}. (\<exists>a\<in>s. f = s  {a})}. 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

978 
(rl ` f = {0..n}) \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

979 
((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

980 
(\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p))})" apply(rule *[OF _ assms(2)]) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

981 
show ?thesis apply(rule kuhn_complete_lemma[OF finite_simplices]) prefer 6 apply(rule *) apply(rule,rule,rule) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

982 
apply(subst ksimplex_def) defer apply(rule,rule assms(1)[rule_format]) unfolding mem_Collect_eq apply assumption 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

983 
apply default+ unfolding mem_Collect_eq apply(erule disjE bexE)+ defer apply(erule disjE bexE)+ defer 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

984 
apply default+ unfolding mem_Collect_eq apply(erule disjE bexE)+ unfolding mem_Collect_eq proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

985 
fix f s a assume as:"ksimplex p (n + 1) s" "a\<in>s" "f = s  {a}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

986 
let ?S = "{s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s  {a})}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

987 
have S:"?S = {s'. ksimplex p (n + 1) s' \<and> (\<exists>b\<in>s'. s'  {b} = s  {a})}" unfolding as by blast 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

988 
{ fix j assume j:"j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = 0" thus "card {s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s  {a})} = 1" unfolding S 
41958  989 
applyapply(rule ksimplex_replace_0) apply(rule as)+ unfolding as by auto } 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

990 
{ fix j assume j:"j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = p" thus "card {s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s  {a})} = 1" unfolding S 
41958  991 
applyapply(rule ksimplex_replace_1) apply(rule as)+ unfolding as by auto } 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

992 
show "\<not> ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p)) \<Longrightarrow> card ?S = 2" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

993 
unfolding S apply(rule ksimplex_replace_2) apply(rule as)+ unfolding as by auto qed auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

994 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

995 
subsection {* Reduced labelling. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

996 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

997 
definition "reduced label (n::nat) (x::nat\<Rightarrow>nat) = 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

998 
(SOME k. k \<le> n \<and> (\<forall>i. 1\<le>i \<and> i<k+1 \<longrightarrow> label x i = 0) \<and> (k = n \<or> label x (k + 1) \<noteq> (0::nat)))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

999 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1000 
lemma reduced_labelling: shows "reduced label n x \<le> n" (is ?t1) and 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1001 
"\<forall>i. 1\<le>i \<and> i < reduced label n x + 1 \<longrightarrow> (label x i = 0)" (is ?t2) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1002 
"(reduced label n x = n) \<or> (label x (reduced label n x + 1) \<noteq> 0)" (is ?t3) proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1003 
have num_WOP:"\<And>P k. P (k::nat) \<Longrightarrow> \<exists>n. P n \<and> (\<forall>m<n. \<not> P m)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1004 
apply(drule ex_has_least_nat[where m="\<lambda>x. x"]) apply(erule exE,rule_tac x=x in exI) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1005 
have *:"n \<le> n \<and> (label x (n + 1) \<noteq> 0 \<or> n = n)" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1006 
then guess N apply(drule_tac num_WOP[of "\<lambda>j. j\<le>n \<and> (label x (j+1) \<noteq> 0 \<or> n = j)"]) apply(erule exE) . note N=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1007 
have N':"N \<le> n" "\<forall>i. 1 \<le> i \<and> i < N + 1 \<longrightarrow> label x i = 0" "N = n \<or> label x (N + 1) \<noteq> 0" defer proof(rule,rule) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1008 
fix i assume i:"1\<le>i \<and> i<N+1" thus "label x i = 0" using N[THEN conjunct2,THEN spec[where x="i  1"]] using N by auto qed(insert N, auto) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1009 
show ?t1 ?t2 ?t3 unfolding reduced_def apply(rule_tac[!] someI2_ex) using N' by(auto intro!: exI[where x=N]) qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1010 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1011 
lemma reduced_labelling_unique: fixes x::"nat \<Rightarrow> nat" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1012 
assumes "r \<le> n" "\<forall>i. 1 \<le> i \<and> i < r + 1 \<longrightarrow> (label x i = 0)" "(r = n) \<or> (label x (r + 1) \<noteq> 0)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1013 
shows "reduced label n x = r" apply(rule le_antisym) apply(rule_tac[!] ccontr) unfolding not_le 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1014 
using reduced_labelling[of label n x] using assms by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1015 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1016 
lemma reduced_labelling_0: assumes "j\<in>{1..n}" "label x j = 0" shows "reduced label n x \<noteq> j  1" 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44821
diff
changeset

1017 
using reduced_labelling[of label n x] using assms by fastforce 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1018 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1019 
lemma reduced_labelling_1: assumes "j\<in>{1..n}" "label x j \<noteq> 0" shows "reduced label n x < j" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1020 
using assms and reduced_labelling[of label n x] apply(erule_tac x=j in allE) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1021 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1022 
lemma reduced_labelling_Suc: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1023 
assumes "reduced lab (n + 1) x \<noteq> n + 1" shows "reduced lab (n + 1) x = reduced lab n x" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1024 
apply(subst eq_commute) apply(rule reduced_labelling_unique) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1025 
using reduced_labelling[of lab "n+1" x] and assms by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1026 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1027 
lemma complete_face_top: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1028 
assumes "\<forall>x\<in>f. \<forall>j\<in>{1..n+1}. x j = 0 \<longrightarrow> lab x j = 0" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1029 
"\<forall>x\<in>f. \<forall>j\<in>{1..n+1}. x j = p \<longrightarrow> lab x j = 1" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1030 
shows "((reduced lab (n + 1)) ` f = {0..n}) \<and> ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p)) \<longleftrightarrow> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1031 
((reduced lab (n + 1)) ` f = {0..n}) \<and> (\<forall>x\<in>f. x (n + 1) = p)" (is "?l = ?r") proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1032 
assume ?l (is "?as \<and> (?a \<or> ?b)") thus ?r applyapply(rule,erule conjE,assumption) proof(cases ?a) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1033 
case True then guess j .. note j=this {fix x assume x:"x\<in>f" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1034 
have "reduced lab (n+1) x \<noteq> j  1" using j applyapply(rule reduced_labelling_0) defer apply(rule assms(1)[rule_format]) using x by auto } 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1035 
moreover have "j  1 \<in> {0..n}" using j by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1036 
then guess y unfolding `?l`[THEN conjunct1,THEN sym] and image_iff .. note y = this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1037 
ultimately have False by auto thus "\<forall>x\<in>f. x (n + 1) = p" by auto next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1038 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1039 
case False hence ?b using `?l` by blast then guess j .. note j=this {fix x assume x:"x\<in>f" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1040 
have "reduced lab (n+1) x < j" using j applyapply(rule reduced_labelling_1) using assms(2)[rule_format,of x j] and x by auto } note * = this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1041 
have "j = n + 1" proof(rule ccontr) case goal1 hence "j < n + 1" using j by auto moreover 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1042 
have "n \<in> {0..n}" by auto then guess y unfolding `?l`[THEN conjunct1,THEN sym] image_iff .. 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1043 
ultimately show False using *[of y] by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1044 
thus "\<forall>x\<in>f. x (n + 1) = p" using j by auto qed qed(auto) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1045 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1046 
subsection {* Hence we get just about the nice induction. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1047 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1048 
lemma kuhn_induction: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1049 
assumes "0 < p" "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = 0) \<longrightarrow> (lab x j = 0)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1050 
"\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1051 
"odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1052 
shows "odd (card {s. ksimplex p (n+1) s \<and>((reduced lab (n+1)) ` s = {0..n+1})})" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1053 
have *:"\<And>s t. odd (card s) \<Longrightarrow> s = t \<Longrightarrow> odd (card t)" "\<And>s f. (\<And>x. f x \<le> n +1 ) \<Longrightarrow> f ` s \<subseteq> {0..n+1}" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1054 
show ?thesis apply(rule kuhn_simplex_lemma[unfolded mem_Collect_eq]) apply(rule,rule,rule *,rule reduced_labelling) 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

1055 
apply(rule *(1)[OF assms(4)]) apply(rule set_eqI) unfolding mem_Collect_eq apply(rule,erule conjE) defer apply(rule) proof(*(rule,rule)*) 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1056 
fix f assume as:"ksimplex p n f" "reduced lab n ` f = {0..n}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1057 
have *:"\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = 0 \<longrightarrow> lab x j = 0" "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = p \<longrightarrow> lab x j = 1" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1058 
using assms(23) using as(1)[unfolded ksimplex_def] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1059 
have allp:"\<forall>x\<in>f. x (n + 1) = p" using assms(2) using as(1)[unfolded ksimplex_def] by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1060 
{ fix x assume "x\<in>f" hence "reduced lab (n + 1) x < n + 1" applyapply(rule reduced_labelling_1) 
41958  1061 
defer using assms(3) using as(1)[unfolded ksimplex_def] by auto 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1062 
hence "reduced lab (n + 1) x = reduced lab n x" applyapply(rule reduced_labelling_Suc) using reduced_labelling(1) by auto } 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

1063 
hence "reduced lab (n + 1) ` f = {0..n}" unfolding as(2)[THEN sym] apply apply(rule set_eqI) unfolding image_iff by auto 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1064 
moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,THEN sym]] .. then guess a .. 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1065 
ultimately show "\<exists>s a. ksimplex p (n + 1) s \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1066 
a \<in> s \<and> f = s  {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and> ((\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p))" (is ?ex) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1067 
apply(rule_tac x=s in exI,rule_tac x=a in exI) unfolding complete_face_top[OF *] using allp as(1) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1068 
next fix f assume as:"\<exists>s a. ksimplex p (n + 1) s \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1069 
a \<in> s \<and> f = s  {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and> ((\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p))" (is ?ex) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1070 
then guess s .. then guess a applyapply(erule exE,(erule conjE)+) . note sa=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1071 
{ fix x assume "x\<in>f" hence "reduced lab (n + 1) x \<in> reduced lab (n + 1) ` f" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1072 
hence "reduced lab (n + 1) x < n + 1" using sa(4) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1073 
hence "reduced lab (n + 1) x = reduced lab n x" applyapply(rule reduced_labelling_Suc) 
41958  1074 
using reduced_labelling(1) by auto } 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

1075 
thus part1:"reduced lab n ` f = {0..n}" unfolding sa(4)[THEN sym] applyapply(rule set_eqI) unfolding image_iff by auto 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1076 
have *:"\<forall>x\<in>f. x (n + 1) = p" proof(cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0") 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1077 
case True then guess j .. hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j  1" applyapply(rule reduced_labelling_0) apply assumption 
41958  1078 
apply(rule assms(2)[rule_format]) using sa(1)[unfolded ksimplex_def] unfolding sa by auto moreover 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1079 
have "j  1 \<in> {0..n}" using `j\<in>{1..n+1}` by auto 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44821
diff
changeset

1080 
ultimately have False unfolding sa(4)[THEN sym] unfolding image_iff by fastforce thus ?thesis by auto next 
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44821
diff
changeset

1081 
case False hence "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p" using sa(5) by fastforce then guess j .. note j=this 
33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1082 
thus ?thesis proof(cases "j = n+1") 
41958  1083 
case False hence *:"j\<in>{1..n}" using j by auto 
1084 
hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab n x < j" apply(rule reduced_labelling_1) proof fix x assume "x\<in>f" 

1085 
hence "lab x j = 1" applyapply(rule assms(3)[rule_format,OF j(1)]) 

1086 
using sa(1)[unfolded ksimplex_def] using j unfolding sa by auto thus "lab x j \<noteq> 0" by auto qed 

1087 
moreover have "j\<in>{0..n}" using * by auto 

1088 
ultimately have False unfolding part1[THEN sym] using * unfolding image_iff by auto thus ?thesis by auto qed auto qed 

33741
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1089 
thus "ksimplex p n f" using as unfolding simplex_top_face[OF assms(1) *,THEN sym] by auto qed qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1090 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1091 
lemma kuhn_induction_Suc: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1092 
assumes "0 < p" "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> (x j = 0) \<longrightarrow> (lab x j = 0)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1093 
"\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1094 
"odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1095 
shows "odd (card {s. ksimplex p (Suc n) s \<and>((reduced lab (Suc n)) ` s = {0..Suc n})})" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1096 
using assms unfolding Suc_eq_plus1 by(rule kuhn_induction) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1097 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1098 
subsection {* And so we get the final combinatorial result. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1099 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1100 
lemma ksimplex_0: "ksimplex p 0 s \<longleftrightarrow> s = {(\<lambda>x. p)}" (is "?l = ?r") proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1101 
assume l:?l guess a using ksimplexD(3)[OF l, unfolded add_0] unfolding card_1_exists .. note a=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1102 
have "a = (\<lambda>x. p)" using ksimplexD(5)[OF l, rule_format, OF a(1)] by(rule,auto) thus ?r using a by auto next 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1103 
assume r:?r show ?l unfolding r ksimplex_eq by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1104 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1105 
lemma reduce_labelling_0[simp]: "reduced lab 0 x = 0" apply(rule reduced_labelling_unique) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1106 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1107 
lemma kuhn_combinatorial: 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1108 
assumes "0 < p" "\<forall>x j. (\<forall>j. x(j) \<le> p) \<and> 1 \<le> j \<and> j \<le> n \<and> (x j = 0) \<longrightarrow> (lab x j = 0)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1109 
"\<forall>x j. (\<forall>j. x(j) \<le> p) \<and> 1 \<le> j \<and> j \<le> n \<and> (x j = p) \<longrightarrow> (lab x j = 1)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1110 
shows " odd (card {s. ksimplex p n s \<and> ((reduced lab n) ` s = {0..n})})" using assms proof(induct n) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1111 
let ?M = "\<lambda>n. {s. ksimplex p n s \<and> ((reduced lab n) ` s = {0..n})}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1112 
{ case 0 have *:"?M 0 = {{(\<lambda>x. p)}}" unfolding ksimplex_0 by auto show ?case unfolding * by auto } 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1113 
case (Suc n) have "odd (card (?M n))" apply(rule Suc(1)[OF Suc(2)]) using Suc(3) by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1114 
thus ?case applyapply(rule kuhn_induction_Suc) using Suc(2) by auto qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1115 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1116 
lemma kuhn_lemma: assumes "0 < (p::nat)" "0 < (n::nat)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1117 
"\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (label x i = (0::nat)) \<or> (label x i = 1))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1118 
"\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (x i = 0) \<longrightarrow> (label x i = 0))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1119 
"\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (x i = p) \<longrightarrow> (label x i = 1))" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1120 
obtains q where "\<forall>i\<in>{1..n}. q i < p" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1121 
"\<forall>i\<in>{1..n}. \<exists>r s. (\<forall>j\<in>{1..n}. q(j) \<le> r(j) \<and> r(j) \<le> q(j) + 1) \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1122 
(\<forall>j\<in>{1..n}. q(j) \<le> s(j) \<and> s(j) \<le> q(j) + 1) \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1123 
~(label r i = label s i)" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1124 
let ?A = "{s. ksimplex p n s \<and> reduced label n ` s = {0..n}}" have "n\<noteq>0" using assms by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1125 
have conjD:"\<And>P Q. P \<and> Q \<Longrightarrow> P" "\<And>P Q. P \<and> Q \<Longrightarrow> Q" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1126 
have "odd (card ?A)" apply(rule kuhn_combinatorial[of p n label]) using assms by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1127 
hence "card ?A \<noteq> 0" applyapply(rule ccontr) by auto hence "?A \<noteq> {}" unfolding card_eq_0_iff by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1128 
then obtain s where "s\<in>?A" by auto note s=conjD[OF this[unfolded mem_Collect_eq]] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1129 
guess a b apply(rule ksimplex_extrema_strong[OF s(1) `n\<noteq>0`]) . note ab=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1130 
show ?thesis apply(rule that[of a]) proof(rule_tac[!] ballI) fix i assume "i\<in>{1..n}" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1131 
hence "a i + 1 \<le> p" applyapply(rule order_trans[of _ "b i"]) apply(subst ab(5)[THEN spec[where x=i]]) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1132 
using s(1)[unfolded ksimplex_def] defer apply apply(erule conjE)+ apply(drule_tac bspec[OF _ ab(2)])+ by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1133 
thus "a i < p" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1134 
case goal2 hence "i \<in> reduced label n ` s" using s by auto then guess u unfolding image_iff .. note u=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1135 
from goal2 have "i  1 \<in> reduced label n ` s" using s by auto then guess v unfolding image_iff .. note v=this 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1136 
show ?case apply(rule_tac x=u in exI, rule_tac x=v in exI) apply(rule conjI) defer apply(rule conjI) defer 2 proof(rule_tac[12] ballI) 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1137 
show "label u i \<noteq> label v i" using reduced_labelling[of label n u] reduced_labelling[of label n v] 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1138 
unfolding u(2)[THEN sym] v(2)[THEN sym] using goal2 by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1139 
fix j assume j:"j\<in>{1..n}" show "a j \<le> u j \<and> u j \<le> a j + 1" "a j \<le> v j \<and> v j \<le> a j + 1" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1140 
using conjD[OF ab(4)[rule_format, OF u(1)]] and conjD[OF ab(4)[rule_format, OF v(1)]] apply 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1141 
apply(drule_tac[!] kle_imp_pointwise)+ apply(erule_tac[!] x=j in allE)+ unfolding ab(5)[rule_format] using j 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1142 
by auto qed qed qed 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1143 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1144 
subsection {* The main result for the unit cube. *} 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1145 

4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1146 
lemma kuhn_labelling_lemma': 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1147 
assumes "(\<forall>x::nat\<Rightarrow>real. P x \<longrightarrow> P (f x))" "\<forall>x. P x \<longrightarrow> (\<forall>i::nat. Q i \<longrightarrow> 0 \<le> x i \<and> x i \<le> 1)" 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1148 
shows "\<exists>l. (\<forall>x i. l x i \<le> (1::nat)) \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1149 
(\<forall>x i. P x \<and> Q i \<and> (x i = 0) \<longrightarrow> (l x i = 0)) \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1150 
(\<forall>x i. P x \<and> Q i \<and> (x i = 1) \<longrightarrow> (l x i = 1)) \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1151 
(\<forall>x i. P x \<and> Q i \<and> (l x i = 0) \<longrightarrow> x i \<le> f(x) i) \<and> 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1152 
(\<forall>x i. P x \<and> Q i \<and> (l x i = 1) \<longrightarrow> f(x) i \<le> x i)" proof 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1153 
have and_forall_thm:"\<And>P Q. (\<forall>x. P x) \<and> (\<forall>x. Q x) \<longleftrightarrow> (\<forall>x. P x \<and> Q x)" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1154 
have *:"\<forall>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow> (x \<noteq> 1 \<and> x \<le> y \<or> x \<noteq> 0 \<and> y \<le> x)" by auto 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1155 
show ?thesis unfolding and_forall_thm apply(subst choice_iff[THEN sym])+ proof(rule,rule) case goal1 
4c414d0835ab
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
hoelzl
parents:
diff
changeset

1156 
let ?R = "\<lambda>y. (P x \<and> Q xa \<and> x xa = 0 \<longrightarrow> y = (0::nat)) \<and> 