author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47317  432b29a96f61 
child 48069  e9b2782c4f99 
permissions  rwrr 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1 
header {* KurzweilHenstock Gauge Integration in many dimensions. *} 
35172  2 
(* Author: John Harrison 
3 
Translation from HOL light: Robert Himmelmann, TU Muenchen *) 

4 

35292
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
35291
diff
changeset

5 
theory Integration 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
40513
diff
changeset

6 
imports 
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
40513
diff
changeset

7 
Derivative 
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
40513
diff
changeset

8 
"~~/src/HOL/Library/Indicator_Function" 
35172  9 
begin 
10 

47152
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46905
diff
changeset

11 
declare [[smt_certificates = "Integration.certs"]] 
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46905
diff
changeset

12 
declare [[smt_read_only_certificates = true]] 
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46905
diff
changeset

13 
declare [[smt_oracle = false]] 
35172  14 

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

15 
(*declare not_less[simp] not_le[simp]*) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

16 

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

17 
lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

18 
scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44176
diff
changeset

19 
scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

20 

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

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

22 
"0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

23 
by(subst(asm) real_arch_inv) 
36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

24 
subsection {* Sundries *} 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

25 

35172  26 
lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto 
27 
lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto 

28 
lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto 

29 
lemma conjunctD5: assumes "a \<and> b \<and> c \<and> d \<and> e" shows a b c d e using assms by auto 

30 

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

31 
declare norm_triangle_ineq4[intro] 
35172  32 

36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

33 
lemma simple_image: "{f x x . x \<in> s} = f ` s" by blast 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

34 

027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

35 
lemma linear_simps: assumes "bounded_linear f" 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

36 
shows "f (a + b) = f a + f b" "f (a  b) = f a  f b" "f 0 = 0" "f ( a) =  f a" "f (s *\<^sub>R v) = s *\<^sub>R (f v)" 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

37 
apply(rule_tac[!] additive.add additive.minus additive.diff additive.zero bounded_linear.scaleR) 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

38 
using assms unfolding bounded_linear_def additive_def by auto 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

39 

027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

40 
lemma bounded_linearI:assumes "\<And>x y. f (x + y) = f x + f y" 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

41 
"\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x" "\<And>x. norm (f x) \<le> norm x * K" 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

42 
shows "bounded_linear f" 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

43 
unfolding bounded_linear_def additive_def bounded_linear_axioms_def using assms by auto 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

44 

027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

45 
lemma real_le_inf_subset: 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

46 
assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. b <=* s" shows "Inf s <= Inf (t::real set)" 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

47 
apply(rule isGlb_le_isLb) apply(rule Inf[OF assms(1)]) 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

48 
using assms applyapply(erule exE) apply(rule_tac x=b in exI) 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

49 
unfolding isLb_def setge_def by auto 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

50 

027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

51 
lemma real_ge_sup_subset: 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

52 
assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. s *<= b" shows "Sup s >= Sup (t::real set)" 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

53 
apply(rule isLub_le_isUb) apply(rule Sup[OF assms(1)]) 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

54 
using assms applyapply(erule exE) apply(rule_tac x=b in exI) 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

55 
unfolding isUb_def setle_def by auto 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

56 

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

57 
lemma bounded_linear_component[intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x $$ k)" 
36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

58 
apply(rule bounded_linearI[where K=1]) 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

59 
using component_le_norm[of _ k] unfolding real_norm_def by auto 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

60 

027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

61 
lemma transitive_stepwise_lt_eq: 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

62 
assumes "(\<And>x y z::nat. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z)" 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

63 
shows "((\<forall>m. \<forall>n>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n)))" (is "?l = ?r") 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

64 
proof(safe) assume ?r fix n m::nat assume "m < n" thus "R m n" apply 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

65 
proof(induct n arbitrary: m) case (Suc n) show ?case 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

66 
proof(cases "m < n") case True 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

67 
show ?thesis apply(rule assms[OF Suc(1)[OF True]]) using `?r` by auto 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

68 
next case False hence "m = n" using Suc(2) by auto 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

69 
thus ?thesis using `?r` by auto 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

70 
qed qed auto qed auto 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

71 

027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

72 
lemma transitive_stepwise_gt: 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

73 
assumes "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n) " 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

74 
shows "\<forall>n>m. R m n" 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

75 
proof have "\<forall>m. \<forall>n>m. R m n" apply(subst transitive_stepwise_lt_eq) 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

76 
apply(rule assms) apply(assumption,assumption) using assms(2) by auto 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

77 
thus ?thesis by auto qed 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

78 

027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

79 
lemma transitive_stepwise_le_eq: 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

80 
assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

81 
shows "(\<forall>m. \<forall>n\<ge>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n))" (is "?l = ?r") 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

82 
proof safe assume ?r fix m n::nat assume "m\<le>n" thus "R m n" apply 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

83 
proof(induct n arbitrary: m) case (Suc n) show ?case 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

84 
proof(cases "m \<le> n") case True show ?thesis apply(rule assms(2)) 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

85 
apply(rule Suc(1)[OF True]) using `?r` by auto 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

86 
next case False hence "m = Suc n" using Suc(2) by auto 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

87 
thus ?thesis using assms(1) by auto 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

88 
qed qed(insert assms(1), auto) qed auto 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

89 

027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

90 
lemma transitive_stepwise_le: 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

91 
assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n) " 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

92 
shows "\<forall>n\<ge>m. R m n" 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

93 
proof have "\<forall>m. \<forall>n\<ge>m. R m n" apply(subst transitive_stepwise_le_eq) 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

94 
apply(rule assms) apply(rule assms,assumption,assumption) using assms(3) by auto 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

95 
thus ?thesis by auto qed 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

96 

35172  97 
subsection {* Some useful lemmas about intervals. *} 
98 

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

99 
abbreviation One where "One \<equiv> ((\<chi>\<chi> i. 1)::_::ordered_euclidean_space)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

100 

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

101 
lemma empty_as_interval: "{} = {One..0}" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
38656
diff
changeset

102 
apply(rule set_eqI,rule) defer unfolding mem_interval 
35172  103 
using UNIV_witness[where 'a='n] apply(erule_tac exE,rule_tac x=x in allE) by auto 
104 

105 
lemma interior_subset_union_intervals: 

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

106 
assumes "i = {a..b::'a::ordered_euclidean_space}" "j = {c..d}" "interior j \<noteq> {}" "i \<subseteq> j \<union> s" "interior(i) \<inter> interior(j) = {}" 
35172  107 
shows "interior i \<subseteq> interior s" proof 
108 
have "{a<..<b} \<inter> {c..d} = {}" using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5) 

109 
unfolding assms(1,2) interior_closed_interval by auto 

110 
moreover have "{a<..<b} \<subseteq> {c..d} \<union> s" apply(rule order_trans,rule interval_open_subset_closed) 

111 
using assms(4) unfolding assms(1,2) by auto 

112 
ultimately show ?thesis applyapply(rule interior_maximal) defer apply(rule open_interior) 

113 
unfolding assms(1,2) interior_closed_interval by auto qed 

114 

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

115 
lemma inter_interior_unions_intervals: fixes f::"('a::ordered_euclidean_space) set set" 
35172  116 
assumes "finite f" "open s" "\<forall>t\<in>f. \<exists>a b. t = {a..b}" "\<forall>t\<in>f. s \<inter> (interior t) = {}" 
117 
shows "s \<inter> interior(\<Union>f) = {}" proof(rule ccontr,unfold ex_in_conv[THEN sym]) case goal1 

118 
have lem1:"\<And>x e s U. ball x e \<subseteq> s \<inter> interior U \<longleftrightarrow> ball x e \<subseteq> s \<inter> U" apply rule defer apply(rule_tac Int_greatest) 

119 
unfolding open_subset_interior[OF open_ball] using interior_subset by auto 

120 
have lem2:"\<And>x s P. \<exists>x\<in>s. P x \<Longrightarrow> \<exists>x\<in>insert x s. P x" by auto 

121 
have "\<And>f. finite f \<Longrightarrow> (\<forall>t\<in>f. \<exists>a b. t = {a..b}) \<Longrightarrow> (\<exists>x. x \<in> s \<inter> interior (\<Union>f)) \<Longrightarrow> (\<exists>t\<in>f. \<exists>x. \<exists>e>0. ball x e \<subseteq> s \<inter> t)" proof case goal1 

122 
thus ?case proof(induct rule:finite_induct) 

123 
case empty from this(2) guess x .. hence False unfolding Union_empty interior_empty by auto thus ?case by auto next 

124 
case (insert i f) guess x using insert(5) .. note x = this 

125 
then guess e unfolding open_contains_ball_eq[OF open_Int[OF assms(2) open_interior],rule_format] .. note e=this 

126 
guess a using insert(4)[rule_format,OF insertI1] .. then guess b .. note ab = this 

127 
show ?case proof(cases "x\<in>i") case False hence "x \<in> UNIV  {a..b}" unfolding ab by auto 

128 
then guess d unfolding open_contains_ball_eq[OF open_Diff[OF open_UNIV closed_interval],rule_format] .. 

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

129 
hence "0 < d" "ball x (min d e) \<subseteq> UNIV  i" unfolding ab ball_min_Int by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

130 
hence "ball x (min d e) \<subseteq> s \<inter> interior (\<Union>f)" using e unfolding lem1 unfolding ball_min_Int by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

131 
hence "x \<in> s \<inter> interior (\<Union>f)" using `d>0` e by auto 
35172  132 
hence "\<exists>t\<in>f. \<exists>x e. 0 < e \<and> ball x e \<subseteq> s \<inter> t" applyapply(rule insert(3)) using insert(4) by auto thus ?thesis by auto next 
133 
case True show ?thesis proof(cases "x\<in>{a<..<b}") 

134 
case True then guess d unfolding open_contains_ball_eq[OF open_interval,rule_format] .. 

135 
thus ?thesis apply(rule_tac x=i in bexI,rule_tac x=x in exI,rule_tac x="min d e" in exI) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44522
diff
changeset

136 
unfolding ab using interval_open_subset_closed[of a b] and e by fastforce+ next 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

137 
case False then obtain k where "x$$k \<le> a$$k \<or> x$$k \<ge> b$$k" and k:"k<DIM('a)" unfolding mem_interval by(auto simp add:not_less) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

138 
hence "x$$k = a$$k \<or> x$$k = b$$k" using True unfolding ab and mem_interval apply(erule_tac x=k in allE) by auto 
35172  139 
hence "\<exists>x. ball x (e/2) \<subseteq> s \<inter> (\<Union>f)" proof(erule_tac disjE) 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

140 
let ?z = "x  (e/2) *\<^sub>R basis k" assume as:"x$$k = a$$k" have "ball ?z (e / 2) \<inter> i = {}" apply(rule ccontr) unfolding ex_in_conv[THEN sym] proof(erule exE) 
41958  141 
fix y assume "y \<in> ball ?z (e / 2) \<inter> i" hence "dist ?z y < e/2" and yi:"y\<in>i" by auto 
142 
hence "\<bar>(?z  y) $$ k\<bar> < e/2" using component_le_norm[of "?z  y" k] unfolding dist_norm by auto 

44167  143 
hence "y$$k < a$$k" using e[THEN conjunct1] k by(auto simp add:field_simps as) 
41958  144 
hence "y \<notin> i" unfolding ab mem_interval not_all apply(rule_tac x=k in exI) using k by auto thus False using yi by auto qed 
35172  145 
moreover have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)" apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) proof 
41958  146 
fix y assume as:"y\<in> ball ?z (e/2)" have "norm (x  y) \<le> \<bar>e\<bar> / 2 + norm (x  y  (e / 2) *\<^sub>R basis k)" 
147 
applyapply(rule order_trans,rule norm_triangle_sub[of "x  y" "(e/2) *\<^sub>R basis k"]) 

148 
unfolding norm_scaleR norm_basis by auto 

149 
also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball dist_norm using e by(auto simp add:field_simps) 

150 
finally show "y\<in>ball x e" unfolding mem_ball dist_norm using e by(auto simp add:field_simps) qed 

35172  151 
ultimately show ?thesis apply(rule_tac x="?z" in exI) unfolding Union_insert by auto 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

152 
next let ?z = "x + (e/2) *\<^sub>R basis k" assume as:"x$$k = b$$k" have "ball ?z (e / 2) \<inter> i = {}" apply(rule ccontr) unfolding ex_in_conv[THEN sym] proof(erule exE) 
41958  153 
fix y assume "y \<in> ball ?z (e / 2) \<inter> i" hence "dist ?z y < e/2" and yi:"y\<in>i" by auto 
154 
hence "\<bar>(?z  y) $$ k\<bar> < e/2" using component_le_norm[of "?z  y" k] unfolding dist_norm by auto 

155 
hence "y$$k > b$$k" using e[THEN conjunct1] k by(auto simp add:field_simps as) 

156 
hence "y \<notin> i" unfolding ab mem_interval not_all using k by(rule_tac x=k in exI,auto) thus False using yi by auto qed 

35172  157 
moreover have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)" apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) proof 
41958  158 
fix y assume as:"y\<in> ball ?z (e/2)" have "norm (x  y) \<le> \<bar>e\<bar> / 2 + norm (x  y + (e / 2) *\<^sub>R basis k)" 
159 
applyapply(rule order_trans,rule norm_triangle_sub[of "x  y" " (e/2) *\<^sub>R basis k"]) 

160 
unfolding norm_scaleR by auto 

161 
also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball dist_norm using e by(auto simp add:field_simps) 

162 
finally show "y\<in>ball x e" unfolding mem_ball dist_norm using e by(auto simp add:field_simps) qed 

35172  163 
ultimately show ?thesis apply(rule_tac x="?z" in exI) unfolding Union_insert by auto qed 
164 
then guess x .. hence "x \<in> s \<inter> interior (\<Union>f)" unfolding lem1[where U="\<Union>f",THEN sym] using centre_in_ball e[THEN conjunct1] by auto 

165 
thus ?thesis applyapply(rule lem2,rule insert(3)) using insert(4) by auto qed qed qed qed note * = this 

166 
guess t using *[OF assms(1,3) goal1] .. from this(2) guess x .. then guess e .. 

167 
hence "x \<in> s" "x\<in>interior t" defer using open_subset_interior[OF open_ball, of x e t] by auto 

168 
thus False using `t\<in>f` assms(4) by auto qed 

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

169 

35172  170 
subsection {* Bounds on intervals where they exist. *} 
171 

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

172 
definition "interval_upperbound (s::('a::ordered_euclidean_space) set) = ((\<chi>\<chi> i. Sup {a. \<exists>x\<in>s. x$$i = a})::'a)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

173 

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

174 
definition "interval_lowerbound (s::('a::ordered_euclidean_space) set) = ((\<chi>\<chi> i. Inf {a. \<exists>x\<in>s. x$$i = a})::'a)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

175 

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

176 
lemma interval_upperbound[simp]: assumes "\<forall>i<DIM('a::ordered_euclidean_space). a$$i \<le> (b::'a)$$i" shows "interval_upperbound {a..b} = b" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

177 
using assms unfolding interval_upperbound_def apply(subst euclidean_eq[where 'a='a]) apply safe 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

178 
unfolding euclidean_lambda_beta' apply(erule_tac x=i in allE) 
35172  179 
apply(rule Sup_unique) unfolding setle_def apply rule unfolding mem_Collect_eq apply(erule bexE) unfolding mem_interval defer 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

180 
apply(rule,rule) apply(rule_tac x="b$$i" in bexI) defer unfolding mem_Collect_eq apply(rule_tac x=b in bexI) 
35172  181 
unfolding mem_interval using assms by auto 
182 

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

183 
lemma interval_lowerbound[simp]: assumes "\<forall>i<DIM('a::ordered_euclidean_space). a$$i \<le> (b::'a)$$i" shows "interval_lowerbound {a..b} = a" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

184 
using assms unfolding interval_lowerbound_def apply(subst euclidean_eq[where 'a='a]) apply safe 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

185 
unfolding euclidean_lambda_beta' apply(erule_tac x=i in allE) 
35172  186 
apply(rule Inf_unique) unfolding setge_def apply rule unfolding mem_Collect_eq apply(erule bexE) unfolding mem_interval defer 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

187 
apply(rule,rule) apply(rule_tac x="a$$i" in bexI) defer unfolding mem_Collect_eq apply(rule_tac x=a in bexI) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

188 
unfolding mem_interval using assms by auto 
35172  189 

190 
lemmas interval_bounds = interval_upperbound interval_lowerbound 

191 

192 
lemma interval_bounds'[simp]: assumes "{a..b}\<noteq>{}" shows "interval_upperbound {a..b} = b" "interval_lowerbound {a..b} = a" 

193 
using assms unfolding interval_ne_empty by auto 

194 

195 
subsection {* Content (length, area, volume...) of an interval. *} 

196 

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

197 
definition "content (s::('a::ordered_euclidean_space) set) = 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

198 
(if s = {} then 0 else (\<Prod>i<DIM('a). (interval_upperbound s)$$i  (interval_lowerbound s)$$i))" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

199 

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

200 
lemma interval_not_empty:"\<forall>i<DIM('a). a$$i \<le> b$$i \<Longrightarrow> {a..b::'a::ordered_euclidean_space} \<noteq> {}" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

201 
unfolding interval_eq_empty unfolding not_ex not_less by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

202 

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

203 
lemma content_closed_interval: fixes a::"'a::ordered_euclidean_space" assumes "\<forall>i<DIM('a). a$$i \<le> b$$i" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

204 
shows "content {a..b} = (\<Prod>i<DIM('a). b$$i  a$$i)" 
35172  205 
using interval_not_empty[OF assms] unfolding content_def interval_upperbound[OF assms] interval_lowerbound[OF assms] by auto 
206 

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

207 
lemma content_closed_interval': fixes a::"'a::ordered_euclidean_space" assumes "{a..b}\<noteq>{}" shows "content {a..b} = (\<Prod>i<DIM('a). b$$i  a$$i)" 
35172  208 
apply(rule content_closed_interval) using assms unfolding interval_ne_empty . 
209 

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

210 
lemma content_real:assumes "a\<le>b" shows "content {a..b} = ba" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

211 
proof have *:"{..<Suc 0} = {0}" by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

212 
show ?thesis unfolding content_def using assms by(auto simp: *) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

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

214 

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

215 
lemma content_unit[intro]: "content{0..One::'a::ordered_euclidean_space} = 1" proof 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

216 
have *:"\<forall>i<DIM('a). (0::'a)$$i \<le> (One::'a)$$i" by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

217 
have "0 \<in> {0..One::'a}" unfolding mem_interval by auto 
35172  218 
thus ?thesis unfolding content_def interval_bounds[OF *] using setprod_1 by auto qed 
219 

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

220 
lemma content_pos_le[intro]: fixes a::"'a::ordered_euclidean_space" shows "0 \<le> content {a..b}" proof(cases "{a..b}={}") 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

221 
case False hence *:"\<forall>i<DIM('a). a $$ i \<le> b $$ i" unfolding interval_ne_empty by assumption 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

222 
have "(\<Prod>i<DIM('a). interval_upperbound {a..b} $$ i  interval_lowerbound {a..b} $$ i) \<ge> 0" 
35172  223 
apply(rule setprod_nonneg) unfolding interval_bounds[OF *] using * apply(erule_tac x=x in allE) by auto 
224 
thus ?thesis unfolding content_def by(auto simp del:interval_bounds') qed(unfold content_def, auto) 

225 

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

226 
lemma content_pos_lt: fixes a::"'a::ordered_euclidean_space" assumes "\<forall>i<DIM('a). a$$i < b$$i" shows "0 < content {a..b}" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

227 
proof have help_lemma1: "\<forall>i<DIM('a). a$$i < b$$i \<Longrightarrow> \<forall>i<DIM('a). a$$i \<le> ((b$$i)::real)" apply(rule,erule_tac x=i in allE) by auto 
35172  228 
show ?thesis unfolding content_closed_interval[OF help_lemma1[OF assms]] apply(rule setprod_pos) 
229 
using assms apply(erule_tac x=x in allE) by auto qed 

230 

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

231 
lemma content_eq_0: "content{a..b::'a::ordered_euclidean_space} = 0 \<longleftrightarrow> (\<exists>i<DIM('a). b$$i \<le> a$$i)" proof(cases "{a..b} = {}") 
35172  232 
case True thus ?thesis unfolding content_def if_P[OF True] unfolding interval_eq_empty apply 
233 
apply(rule,erule exE) apply(rule_tac x=i in exI) by auto next 

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

234 
case False note this[unfolded interval_eq_empty not_ex not_less] 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44522
diff
changeset

235 
hence as:"\<forall>i<DIM('a). b $$ i \<ge> a $$ i" by fastforce 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

236 
show ?thesis unfolding content_def if_not_P[OF False] setprod_zero_iff[OF finite_lessThan] 
35172  237 
apply(rule) apply(erule_tac[!] exE bexE) unfolding interval_bounds[OF as] apply(rule_tac x=x in exI) defer 
238 
apply(rule_tac x=i in bexI) using as apply(erule_tac x=i in allE) by auto qed 

239 

240 
lemma cond_cases:"(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)" by auto 

241 

242 
lemma content_closed_interval_cases: 

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

243 
"content {a..b::'a::ordered_euclidean_space} = (if \<forall>i<DIM('a). a$$i \<le> b$$i then setprod (\<lambda>i. b$$i  a$$i) {..<DIM('a)} else 0)" apply(rule cond_cases) 
35172  244 
apply(rule content_closed_interval) unfolding content_eq_0 not_all not_le defer apply(erule exE,rule_tac x=x in exI) by auto 
245 

246 
lemma content_eq_0_interior: "content {a..b} = 0 \<longleftrightarrow> interior({a..b}) = {}" 

247 
unfolding content_eq_0 interior_closed_interval interval_eq_empty by auto 

248 

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

249 
(*lemma content_eq_0_1: "content {a..b::real^1} = 0 \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

250 
unfolding content_eq_0 by auto*) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

251 

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

252 
lemma content_pos_lt_eq: "0 < content {a..b::'a::ordered_euclidean_space} \<longleftrightarrow> (\<forall>i<DIM('a). a$$i < b$$i)" 
35172  253 
apply(rule) defer apply(rule content_pos_lt,assumption) proof assume "0 < content {a..b}" 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44522
diff
changeset

254 
hence "content {a..b} \<noteq> 0" by auto thus "\<forall>i<DIM('a). a$$i < b$$i" unfolding content_eq_0 not_ex not_le by fastforce qed 
35172  255 

256 
lemma content_empty[simp]: "content {} = 0" unfolding content_def by auto 

257 

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

258 
lemma content_subset: assumes "{a..b} \<subseteq> {c..d}" shows "content {a..b::'a::ordered_euclidean_space} \<le> content {c..d}" proof(cases "{a..b}={}") 
35172  259 
case True thus ?thesis using content_pos_le[of c d] by auto next 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

260 
case False hence ab_ne:"\<forall>i<DIM('a). a $$ i \<le> b $$ i" unfolding interval_ne_empty by auto 
35172  261 
hence ab_ab:"a\<in>{a..b}" "b\<in>{a..b}" unfolding mem_interval by auto 
262 
have "{c..d} \<noteq> {}" using assms False by auto 

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

263 
hence cd_ne:"\<forall>i<DIM('a). c $$ i \<le> d $$ i" using assms unfolding interval_ne_empty by auto 
35172  264 
show ?thesis unfolding content_def unfolding interval_bounds[OF ab_ne] interval_bounds[OF cd_ne] 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

265 
unfolding if_not_P[OF False] if_not_P[OF `{c..d} \<noteq> {}`] apply(rule setprod_mono,rule) proof 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

266 
fix i assume i:"i\<in>{..<DIM('a)}" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

267 
show "0 \<le> b $$ i  a $$ i" using ab_ne[THEN spec[where x=i]] i by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

268 
show "b $$ i  a $$ i \<le> d $$ i  c $$ i" 
35172  269 
using assms[unfolded subset_eq mem_interval,rule_format,OF ab_ab(2),of i] 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

270 
using assms[unfolded subset_eq mem_interval,rule_format,OF ab_ab(1),of i] using i by auto qed qed 
35172  271 

272 
lemma content_lt_nz: "0 < content {a..b} \<longleftrightarrow> content {a..b} \<noteq> 0" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44522
diff
changeset

273 
unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce 
35172  274 

275 
subsection {* The notion of a gauge  simply an open set containing the point. *} 

276 

277 
definition gauge where "gauge d \<longleftrightarrow> (\<forall>x. x\<in>(d x) \<and> open(d x))" 

278 

279 
lemma gaugeI:assumes "\<And>x. x\<in>g x" "\<And>x. open (g x)" shows "gauge g" 

280 
using assms unfolding gauge_def by auto 

281 

282 
lemma gaugeD[dest]: assumes "gauge d" shows "x\<in>d x" "open (d x)" using assms unfolding gauge_def by auto 

283 

284 
lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))" 

285 
unfolding gauge_def by auto 

286 

35751  287 
lemma gauge_ball[intro]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)" unfolding gauge_def by auto 
35172  288 

289 
lemma gauge_trivial[intro]: "gauge (\<lambda>x. ball x 1)" apply(rule gauge_ball) by auto 

290 

35751  291 
lemma gauge_inter[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. (d1 x) \<inter> (d2 x))" 
35172  292 
unfolding gauge_def by auto 
293 

294 
lemma gauge_inters: assumes "finite s" "\<forall>d\<in>s. gauge (f d)" shows "gauge(\<lambda>x. \<Inter> {f d x  d. d \<in> s})" proof 

295 
have *:"\<And>x. {f d x d. d \<in> s} = (\<lambda>d. f d x) ` s" by auto show ?thesis 

296 
unfolding gauge_def unfolding * 

297 
using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto qed 

298 

299 
lemma gauge_existence_lemma: "(\<forall>x. \<exists>d::real. p x \<longrightarrow> 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. p x \<longrightarrow> q d x)" by(meson zero_less_one) 

300 

301 
subsection {* Divisions. *} 

302 

303 
definition division_of (infixl "division'_of" 40) where 

304 
"s division_of i \<equiv> 

305 
finite s \<and> 

306 
(\<forall>k\<in>s. k \<subseteq> i \<and> k \<noteq> {} \<and> (\<exists>a b. k = {a..b})) \<and> 

307 
(\<forall>k1\<in>s. \<forall>k2\<in>s. k1 \<noteq> k2 \<longrightarrow> interior(k1) \<inter> interior(k2) = {}) \<and> 

308 
(\<Union>s = i)" 

309 

310 
lemma division_ofD[dest]: assumes "s division_of i" 

311 
shows"finite s" "\<And>k. k\<in>s \<Longrightarrow> k \<subseteq> i" "\<And>k. k\<in>s \<Longrightarrow> k \<noteq> {}" "\<And>k. k\<in>s \<Longrightarrow> (\<exists>a b. k = {a..b})" 

312 
"\<And>k1 k2. \<lbrakk>k1\<in>s; k2\<in>s; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}" "\<Union>s = i" using assms unfolding division_of_def by auto 

313 

314 
lemma division_ofI: 

315 
assumes "finite s" "\<And>k. k\<in>s \<Longrightarrow> k \<subseteq> i" "\<And>k. k\<in>s \<Longrightarrow> k \<noteq> {}" "\<And>k. k\<in>s \<Longrightarrow> (\<exists>a b. k = {a..b})" 

316 
"\<And>k1 k2. \<lbrakk>k1\<in>s; k2\<in>s; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}" "\<Union>s = i" 

317 
shows "s division_of i" using assms unfolding division_of_def by auto 

318 

319 
lemma division_of_finite: "s division_of i \<Longrightarrow> finite s" 

320 
unfolding division_of_def by auto 

321 

322 
lemma division_of_self[intro]: "{a..b} \<noteq> {} \<Longrightarrow> {{a..b}} division_of {a..b}" 

323 
unfolding division_of_def by auto 

324 

325 
lemma division_of_trivial[simp]: "s division_of {} \<longleftrightarrow> s = {}" unfolding division_of_def by auto 

326 

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

327 
lemma division_of_sing[simp]: "s division_of {a..a::'a::ordered_euclidean_space} \<longleftrightarrow> s = {{a..a}}" (is "?l = ?r") proof 
35172  328 
assume ?r moreover { assume "s = {{a}}" moreover fix k assume "k\<in>s" 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

329 
ultimately have"\<exists>x y. k = {x..y}" apply(rule_tac x=a in exI)+ unfolding interval_sing by auto } 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

330 
ultimately show ?l unfolding division_of_def interval_sing by auto next 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

331 
assume ?l note as=conjunctD4[OF this[unfolded division_of_def interval_sing]] 
35172  332 
{ fix x assume x:"x\<in>s" have "x={a}" using as(2)[rule_format,OF x] by auto } 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

333 
moreover have "s \<noteq> {}" using as(4) by auto ultimately show ?r unfolding interval_sing by auto qed 
35172  334 

335 
lemma elementary_empty: obtains p where "p division_of {}" 

336 
unfolding division_of_trivial by auto 

337 

338 
lemma elementary_interval: obtains p where "p division_of {a..b}" 

339 
by(metis division_of_trivial division_of_self) 

340 

341 
lemma division_contains: "s division_of i \<Longrightarrow> \<forall>x\<in>i. \<exists>k\<in>s. x \<in> k" 

342 
unfolding division_of_def by auto 

343 

344 
lemma forall_in_division: 

345 
"d division_of i \<Longrightarrow> ((\<forall>x\<in>d. P x) \<longleftrightarrow> (\<forall>a b. {a..b} \<in> d \<longrightarrow> P {a..b}))" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44522
diff
changeset

346 
unfolding division_of_def by fastforce 
35172  347 

348 
lemma division_of_subset: assumes "p division_of (\<Union>p)" "q \<subseteq> p" shows "q division_of (\<Union>q)" 

349 
apply(rule division_ofI) proof note as=division_ofD[OF assms(1)] 

350 
show "finite q" apply(rule finite_subset) using as(1) assms(2) by auto 

351 
{ fix k assume "k \<in> q" hence kp:"k\<in>p" using assms(2) by auto show "k\<subseteq>\<Union>q" using `k \<in> q` by auto 

352 
show "\<exists>a b. k = {a..b}" using as(4)[OF kp] by auto show "k \<noteq> {}" using as(3)[OF kp] by auto } 

353 
fix k1 k2 assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2" hence *:"k1\<in>p" "k2\<in>p" "k1\<noteq>k2" using assms(2) by auto 

354 
show "interior k1 \<inter> interior k2 = {}" using as(5)[OF *] by auto qed auto 

355 

356 
lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)" unfolding division_of_def by auto 

357 

358 
lemma division_of_content_0: assumes "content {a..b} = 0" "d division_of {a..b}" shows "\<forall>k\<in>d. content k = 0" 

359 
unfolding forall_in_division[OF assms(2)] apply(rule,rule,rule) apply(drule division_ofD(2)[OF assms(2)]) 

360 
apply(drule content_subset) unfolding assms(1) proof case goal1 thus ?case using content_pos_le[of a b] by auto qed 

361 

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

362 
lemma division_inter: assumes "p1 division_of s1" "p2 division_of (s2::('a::ordered_euclidean_space) set)" 
35172  363 
shows "{k1 \<inter> k2  k1 k2 .k1 \<in> p1 \<and> k2 \<in> p2 \<and> k1 \<inter> k2 \<noteq> {}} division_of (s1 \<inter> s2)" (is "?A' division_of _") proof 
364 
let ?A = "{s. s \<in> (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}" have *:"?A' = ?A" by auto 

365 
show ?thesis unfolding * proof(rule division_ofI) have "?A \<subseteq> (\<lambda>(x, y). x \<inter> y) ` (p1 \<times> p2)" by auto 

366 
moreover have "finite (p1 \<times> p2)" using assms unfolding division_of_def by auto ultimately show "finite ?A" by auto 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
38656
diff
changeset

367 
have *:"\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s" by auto show "\<Union>?A = s1 \<inter> s2" apply(rule set_eqI) unfolding * and Union_image_eq UN_iff 
35172  368 
using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] by auto 
369 
{ fix k assume "k\<in>?A" then obtain k1 k2 where k:"k = k1 \<inter> k2" "k1\<in>p1" "k2\<in>p2" "k\<noteq>{}" by auto thus "k \<noteq> {}" by auto 

370 
show "k \<subseteq> s1 \<inter> s2" using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)] unfolding k by auto 

371 
guess a1 using division_ofD(4)[OF assms(1) k(2)] .. then guess b1 .. note ab1=this 

372 
guess a2 using division_ofD(4)[OF assms(2) k(3)] .. then guess b2 .. note ab2=this 

373 
show "\<exists>a b. k = {a..b}" unfolding k ab1 ab2 unfolding inter_interval by auto } fix k1 k2 

374 
assume "k1\<in>?A" then obtain x1 y1 where k1:"k1 = x1 \<inter> y1" "x1\<in>p1" "y1\<in>p2" "k1\<noteq>{}" by auto 

375 
assume "k2\<in>?A" then obtain x2 y2 where k2:"k2 = x2 \<inter> y2" "x2\<in>p1" "y2\<in>p2" "k2\<noteq>{}" by auto 

376 
assume "k1 \<noteq> k2" hence th:"x1\<noteq>x2 \<or> y1\<noteq>y2" unfolding k1 k2 by auto 

377 
have *:"(interior x1 \<inter> interior x2 = {} \<or> interior y1 \<inter> interior y2 = {}) \<Longrightarrow> 

378 
interior(x1 \<inter> y1) \<subseteq> interior(x1) \<Longrightarrow> interior(x1 \<inter> y1) \<subseteq> interior(y1) \<Longrightarrow> 

379 
interior(x2 \<inter> y2) \<subseteq> interior(x2) \<Longrightarrow> interior(x2 \<inter> y2) \<subseteq> interior(y2) 

380 
\<Longrightarrow> interior(x1 \<inter> y1) \<inter> interior(x2 \<inter> y2) = {}" by auto 

44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44514
diff
changeset

381 
show "interior k1 \<inter> interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[14] interior_mono) 
35172  382 
using division_ofD(5)[OF assms(1) k1(2) k2(2)] 
383 
using division_ofD(5)[OF assms(2) k1(3) k2(3)] using th by auto qed qed 

384 

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

385 
lemma division_inter_1: assumes "d division_of i" "{a..b::'a::ordered_euclidean_space} \<subseteq> i" 
35172  386 
shows "{ {a..b} \<inter> k k. k \<in> d \<and> {a..b} \<inter> k \<noteq> {} } division_of {a..b}" proof(cases "{a..b} = {}") 
387 
case True show ?thesis unfolding True and division_of_trivial by auto next 

388 
have *:"{a..b} \<inter> i = {a..b}" using assms(2) by auto 

389 
case False show ?thesis using division_inter[OF division_of_self[OF False] assms(1)] unfolding * by auto qed 

390 

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

391 
lemma elementary_inter: assumes "p1 division_of s" "p2 division_of (t::('a::ordered_euclidean_space) set)" 
35172  392 
shows "\<exists>p. p division_of (s \<inter> t)" 
393 
by(rule,rule division_inter[OF assms]) 

394 

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

395 
lemma elementary_inters: assumes "finite f" "f\<noteq>{}" "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::ordered_euclidean_space) set)" 
35172  396 
shows "\<exists>p. p division_of (\<Inter> f)" using assms applyproof(induct f rule:finite_induct) 
397 
case (insert x f) show ?case proof(cases "f={}") 

398 
case True thus ?thesis unfolding True using insert by auto next 

399 
case False guess p using insert(3)[OF False insert(5)[unfolded ball_simps,THEN conjunct2]] .. 

400 
moreover guess px using insert(5)[rule_format,OF insertI1] .. ultimately 

401 
show ?thesis unfolding Inter_insert apply(rule_tac elementary_inter) by assumption+ qed qed auto 

402 

403 
lemma division_disjoint_union: 

404 
assumes "p1 division_of s1" "p2 division_of s2" "interior s1 \<inter> interior s2 = {}" 

405 
shows "(p1 \<union> p2) division_of (s1 \<union> s2)" proof(rule division_ofI) 

406 
note d1 = division_ofD[OF assms(1)] and d2 = division_ofD[OF assms(2)] 

407 
show "finite (p1 \<union> p2)" using d1(1) d2(1) by auto 

408 
show "\<Union>(p1 \<union> p2) = s1 \<union> s2" using d1(6) d2(6) by auto 

409 
{ fix k1 k2 assume as:"k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2" moreover let ?g="interior k1 \<inter> interior k2 = {}" 

44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44514
diff
changeset

410 
{ assume as:"k1\<in>p1" "k2\<in>p2" have ?g using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]] 
35172  411 
using assms(3) by blast } moreover 
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44514
diff
changeset

412 
{ assume as:"k1\<in>p2" "k2\<in>p1" have ?g using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]] 
35172  413 
using assms(3) by blast} ultimately 
414 
show ?g using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto } 

415 
fix k assume k:"k \<in> p1 \<union> p2" show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto 

416 
show "k \<noteq> {}" using k d1(3) d2(3) by auto show "\<exists>a b. k = {a..b}" using k d1(4) d2(4) by auto qed 

417 

418 
lemma partial_division_extend_1: 

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

419 
assumes "{c..d} \<subseteq> {a..b::'a::ordered_euclidean_space}" "{c..d} \<noteq> {}" 
35172  420 
obtains p where "p division_of {a..b}" "{c..d} \<in> p" 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

421 
proof def n \<equiv> "DIM('a)" have n:"1 \<le> n" "0 < n" "n \<noteq> 0" unfolding n_def using DIM_positive[where 'a='a] by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

422 
guess \<pi> using ex_bij_betw_nat_finite_1[OF finite_lessThan[of "DIM('a)"]] .. note \<pi>=this 
35172  423 
def \<pi>' \<equiv> "inv_into {1..n} \<pi>" 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

424 
have \<pi>':"bij_betw \<pi>' {..<DIM('a)} {1..n}" using bij_betw_inv_into[OF \<pi>] unfolding \<pi>'_def n_def by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

425 
hence \<pi>'i:"\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i \<in> {1..n}" unfolding bij_betw_def by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

426 
have \<pi>i:"\<And>i. i\<in>{1..n} \<Longrightarrow> \<pi> i <DIM('a)" using \<pi> unfolding bij_betw_def n_def by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

427 
have \<pi>\<pi>'[simp]:"\<And>i. i<DIM('a) \<Longrightarrow> \<pi> (\<pi>' i) = i" unfolding \<pi>'_def 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

428 
apply(rule f_inv_into_f) unfolding n_def using \<pi> unfolding bij_betw_def by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

429 
have \<pi>'\<pi>[simp]:"\<And>i. i\<in>{1..n} \<Longrightarrow> \<pi>' (\<pi> i) = i" unfolding \<pi>'_def apply(rule inv_into_f_eq) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

430 
using \<pi> unfolding n_def bij_betw_def by auto 
35172  431 
have "{c..d} \<noteq> {}" using assms by auto 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

432 
let ?p1 = "\<lambda>l. {(\<chi>\<chi> i. if \<pi>' i < l then c$$i else a$$i)::'a .. (\<chi>\<chi> i. if \<pi>' i < l then d$$i else if \<pi>' i = l then c$$\<pi> l else b$$i)}" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

433 
let ?p2 = "\<lambda>l. {(\<chi>\<chi> i. if \<pi>' i < l then c$$i else if \<pi>' i = l then d$$\<pi> l else a$$i)::'a .. (\<chi>\<chi> i. if \<pi>' i < l then d$$i else b$$i)}" 
35172  434 
let ?p = "{?p1 l l. l \<in> {1..n+1}} \<union> {?p2 l l. l \<in> {1..n+1}}" 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

435 
have abcd:"\<And>i. i<DIM('a) \<Longrightarrow> a $$ i \<le> c $$ i \<and> c$$i \<le> d$$i \<and> d $$ i \<le> b $$ i" using assms 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

436 
unfolding subset_interval interval_eq_empty by auto 
35172  437 
show ?thesis apply(rule that[of ?p]) apply(rule division_ofI) 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

438 
proof have "\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i < Suc n" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

439 
proof(rule ccontr,unfold not_less) fix i assume i:"i<DIM('a)" and "Suc n \<le> \<pi>' i" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

440 
hence "\<pi>' i \<notin> {1..n}" by auto thus False using \<pi>' i unfolding bij_betw_def by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

441 
qed hence "c = (\<chi>\<chi> i. if \<pi>' i < Suc n then c $$ i else a $$ i)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

442 
"d = (\<chi>\<chi> i. if \<pi>' i < Suc n then d $$ i else if \<pi>' i = n + 1 then c $$ \<pi> (n + 1) else b $$ i)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

443 
unfolding euclidean_eq[where 'a='a] using \<pi>' unfolding bij_betw_def by auto 
35172  444 
thus cdp:"{c..d} \<in> ?p" applyapply(rule UnI1) unfolding mem_Collect_eq apply(rule_tac x="n + 1" in exI) by auto 
445 
have "\<And>l. l\<in>{1..n+1} \<Longrightarrow> ?p1 l \<subseteq> {a..b}" "\<And>l. l\<in>{1..n+1} \<Longrightarrow> ?p2 l \<subseteq> {a..b}" 

446 
unfolding subset_eq apply(rule_tac[!] ballI,rule_tac[!] ccontr) 

447 
proof fix l assume l:"l\<in>{1..n+1}" fix x assume "x\<notin>{a..b}" 

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

448 
then guess i unfolding mem_interval not_all not_imp .. note i=conjunctD2[OF this] 
35172  449 
show "x \<in> ?p1 l \<Longrightarrow> False" "x \<in> ?p2 l \<Longrightarrow> False" unfolding mem_interval apply(erule_tac[!] x=i in allE) 
450 
apply(case_tac[!] "\<pi>' i < l", case_tac[!] "\<pi>' i = l") using abcd[of i] i by auto 

451 
qed moreover have "\<And>x. x \<in> {a..b} \<Longrightarrow> x \<in> \<Union>?p" 

452 
proof fix x assume x:"x\<in>{a..b}" 

453 
{ presume "x\<notin>{c..d} \<Longrightarrow> x \<in> \<Union>?p" thus "x \<in> \<Union>?p" using cdp by blast } 

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

454 
let ?M = "{i. i\<in>{1..n+1} \<and> \<not> (c $$ \<pi> i \<le> x $$ \<pi> i \<and> x $$ \<pi> i \<le> d $$ \<pi> i)}" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

455 
assume "x\<notin>{c..d}" then guess i0 unfolding mem_interval not_all not_imp .. 
35172  456 
hence "\<pi>' i0 \<in> ?M" using \<pi>' unfolding bij_betw_def by(auto intro!:le_SucI) 
457 
hence M:"finite ?M" "?M \<noteq> {}" by auto 

458 
def l \<equiv> "Min ?M" note l = Min_less_iff[OF M,unfolded l_def[symmetric]] Min_in[OF M,unfolded mem_Collect_eq l_def[symmetric]] 

459 
Min_gr_iff[OF M,unfolded l_def[symmetric]] 

460 
have "x\<in>?p1 l \<or> x\<in>?p2 l" using l(2)[THEN conjunct2] unfolding de_Morgan_conj not_le 

461 
apply apply(erule disjE) apply(rule disjI1) defer apply(rule disjI2) 

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

462 
proof assume as:"x $$ \<pi> l < c $$ \<pi> l" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

463 
show "x \<in> ?p1 l" unfolding mem_interval apply safe unfolding euclidean_lambda_beta' 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

464 
proof case goal1 have "\<pi>' i \<in> {1..n}" using \<pi>' unfolding bij_betw_def not_le using goal1 by auto 
35172  465 
thus ?case using as x[unfolded mem_interval,rule_format,of i] 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

466 
apply auto using l(3)[of "\<pi>' i"] using goal1 by(auto elim!:ballE[where x="\<pi>' i"]) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

467 
next case goal2 have "\<pi>' i \<in> {1..n}" using \<pi>' unfolding bij_betw_def not_le using goal2 by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

468 
thus ?case using as x[unfolded mem_interval,rule_format,of i] 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

469 
apply auto using l(3)[of "\<pi>' i"] using goal2 by(auto elim!:ballE[where x="\<pi>' i"]) 
35172  470 
qed 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

471 
next assume as:"x $$ \<pi> l > d $$ \<pi> l" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

472 
show "x \<in> ?p2 l" unfolding mem_interval apply safe unfolding euclidean_lambda_beta' 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

473 
proof fix i assume i:"i<DIM('a)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

474 
have "\<pi>' i \<in> {1..n}" using \<pi>' unfolding bij_betw_def not_le using i by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

475 
thus "(if \<pi>' i < l then c $$ i else if \<pi>' i = l then d $$ \<pi> l else a $$ i) \<le> x $$ i" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

476 
"x $$ i \<le> (if \<pi>' i < l then d $$ i else b $$ i)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

477 
using as x[unfolded mem_interval,rule_format,of i] 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

478 
apply auto using l(3)[of "\<pi>' i"] i by(auto elim!:ballE[where x="\<pi>' i"]) 
35172  479 
qed qed 
480 
thus "x \<in> \<Union>?p" using l(2) by blast 

481 
qed ultimately show "\<Union>?p = {a..b}" applyapply(rule) defer apply(rule) by(assumption,blast) 

482 

483 
show "finite ?p" by auto 

484 
fix k assume k:"k\<in>?p" then obtain l where l:"k = ?p1 l \<or> k = ?p2 l" "l \<in> {1..n + 1}" by auto 

485 
show "k\<subseteq>{a..b}" apply(rule,unfold mem_interval,rule,rule) 

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

486 
proof fix i x assume i:"i<DIM('a)" assume "x \<in> k" moreover have "\<pi>' i < l \<or> \<pi>' i = l \<or> \<pi>' i > l" by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

487 
ultimately show "a$$i \<le> x$$i" "x$$i \<le> b$$i" using abcd[of i] using l using i 
44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44282
diff
changeset

488 
by(auto elim!:allE[where x=i] simp add:eucl_le[where 'a='a]) (* FIXME: SLOW *) 
35172  489 
qed have "\<And>l. ?p1 l \<noteq> {}" "\<And>l. ?p2 l \<noteq> {}" unfolding interval_eq_empty not_ex apply(rule_tac[!] allI) 
490 
proof case goal1 thus ?case using abcd[of x] by auto 

491 
next case goal2 thus ?case using abcd[of x] by auto 

492 
qed thus "k \<noteq> {}" using k by auto 

493 
show "\<exists>a b. k = {a..b}" using k by auto 

494 
fix k' assume k':"k' \<in> ?p" "k \<noteq> k'" then obtain l' where l':"k' = ?p1 l' \<or> k' = ?p2 l'" "l' \<in> {1..n + 1}" by auto 

495 
{ fix k k' l l' 

496 
assume k:"k\<in>?p" and l:"k = ?p1 l \<or> k = ?p2 l" "l \<in> {1..n + 1}" 

497 
assume k':"k' \<in> ?p" "k \<noteq> k'" and l':"k' = ?p1 l' \<or> k' = ?p2 l'" "l' \<in> {1..n + 1}" 

498 
assume "l \<le> l'" fix x 

499 
have "x \<notin> interior k \<inter> interior k'" 

500 
proof(rule,cases "l' = n+1") assume x:"x \<in> interior k \<inter> interior k'" 

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

501 
case True hence "\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i < l'" using \<pi>'i using l' by(auto simp add:less_Suc_eq_le) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

502 
hence *:"\<And> P Q. (\<chi>\<chi> i. if \<pi>' i < l' then P i else Q i) = ((\<chi>\<chi> i. P i)::'a)" applyapply(subst euclidean_eq) by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

503 
hence k':"k' = {c..d}" using l'(1) unfolding * by auto 
35172  504 
have ln:"l < n + 1" 
505 
proof(rule ccontr) case goal1 hence l2:"l = n+1" using l by auto 

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

506 
hence "\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i < l" using \<pi>'i by(auto simp add:less_Suc_eq_le) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

507 
hence *:"\<And> P Q. (\<chi>\<chi> i. if \<pi>' i < l then P i else Q i) = ((\<chi>\<chi> i. P i)::'a)" applyapply(subst euclidean_eq) by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

508 
hence "k = {c..d}" using l(1) \<pi>'i unfolding * by(auto) 
35172  509 
thus False using `k\<noteq>k'` k' by auto 
510 
qed have **:"\<pi>' (\<pi> l) = l" using \<pi>'\<pi>[of l] using l ln by auto 

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

511 
have "x $$ \<pi> l < c $$ \<pi> l \<or> d $$ \<pi> l < x $$ \<pi> l" using l(1) apply 
35172  512 
proof(erule disjE) 
513 
assume as:"k = ?p1 l" note * = conjunct1[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format] 

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

514 
show ?thesis using *[of "\<pi> l"] using ln l(2) using \<pi>i[of l] by(auto simp add:** not_less) 
35172  515 
next assume as:"k = ?p2 l" note * = conjunct1[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format] 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

516 
show ?thesis using *[of "\<pi> l"] using ln l(2) using \<pi>i[of l] unfolding ** by auto 
35172  517 
qed thus False using x unfolding k' unfolding Int_iff interior_closed_interval mem_interval 
518 
by(auto elim!:allE[where x="\<pi> l"]) 

519 
next case False hence "l < n + 1" using l'(2) using `l\<le>l'` by auto 

520 
hence ln:"l \<in> {1..n}" "l' \<in> {1..n}" using l l' False by auto 

521 
note \<pi>l = \<pi>'\<pi>[OF ln(1)] \<pi>'\<pi>[OF ln(2)] 

522 
assume x:"x \<in> interior k \<inter> interior k'" 

523 
show False using l(1) l'(1) apply 

524 
proof(erule_tac[!] disjE)+ 

525 
assume as:"k = ?p1 l" "k' = ?p1 l'" 

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

526 
note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format] 
35172  527 
have "l \<noteq> l'" using k'(2)[unfolded as] by auto 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

528 
thus False using *[of "\<pi> l'"] *[of "\<pi> l"] ln using \<pi>i[OF ln(1)] \<pi>i[OF ln(2)] apply(cases "l<l'") 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

529 
by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def) 
35172  530 
next assume as:"k = ?p2 l" "k' = ?p2 l'" 
531 
note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format] 

532 
have "l \<noteq> l'" apply(rule) using k'(2)[unfolded as] by auto 

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

533 
thus False using *[of "\<pi> l"] *[of "\<pi> l'"] `l \<le> l'` ln by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def) 
35172  534 
next assume as:"k = ?p1 l" "k' = ?p2 l'" 
535 
note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format] 

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

536 
show False using abcd[of "\<pi> l'"] using *[of "\<pi> l"] *[of "\<pi> l'"] `l \<le> l'` ln apply(cases "l=l'") 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

537 
by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def) 
35172  538 
next assume as:"k = ?p2 l" "k' = ?p1 l'" 
539 
note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format] 

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

540 
show False using *[of "\<pi> l"] *[of "\<pi> l'"] ln `l \<le> l'` apply(cases "l=l'") using abcd[of "\<pi> l'"] 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

541 
by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def) 
35172  542 
qed qed } 
543 
from this[OF k l k' l'] this[OF k'(1) l' k _ l] have "\<And>x. x \<notin> interior k \<inter> interior k'" 

544 
apply  apply(cases "l' \<le> l") using k'(2) by auto 

545 
thus "interior k \<inter> interior k' = {}" by auto 

546 
qed qed 

547 

548 
lemma partial_division_extend_interval: assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> {a..b}" 

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

549 
obtains q where "p \<subseteq> q" "q division_of {a..b::'a::ordered_euclidean_space}" proof(cases "p = {}") 
35172  550 
case True guess q apply(rule elementary_interval[of a b]) . 
551 
thus ?thesis apply apply(rule that[of q]) unfolding True by auto next 

552 
case False note p = division_ofD[OF assms(1)] 

553 
have *:"\<forall>k\<in>p. \<exists>q. q division_of {a..b} \<and> k\<in>q" proof case goal1 

554 
guess c using p(4)[OF goal1] .. then guess d .. note cd_ = this 

555 
have *:"{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}" using p(2,3)[OF goal1, unfolded cd_] using assms(2) by auto 

556 
guess q apply(rule partial_division_extend_1[OF *]) . thus ?case unfolding cd_ by auto qed 

557 
guess q using bchoice[OF *] .. note q = conjunctD2[OF this[rule_format]] 

558 
have "\<And>x. x\<in>p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x  {x})" apply(rule,rule_tac p="q x" in division_of_subset) proof 

559 
fix x assume x:"x\<in>p" show "q x division_of \<Union>q x" applyapply(rule division_ofI) 

560 
using division_ofD[OF q(1)[OF x]] by auto show "q x  {x} \<subseteq> q x" by auto qed 

561 
hence "\<exists>d. d division_of \<Inter> ((\<lambda>i. \<Union>(q i  {i})) ` p)" apply apply(rule elementary_inters) 

562 
apply(rule finite_imageI[OF p(1)]) unfolding image_is_empty apply(rule False) by auto 

563 
then guess d .. note d = this 

564 
show ?thesis apply(rule that[of "d \<union> p"]) proof 

565 
have *:"\<And>s f t. s \<noteq> {} \<Longrightarrow> (\<forall>i\<in>s. f i \<union> i = t) \<Longrightarrow> t = \<Inter> (f ` s) \<union> (\<Union>s)" by auto 

566 
have *:"{a..b} = \<Inter> (\<lambda>i. \<Union>(q i  {i})) ` p \<union> \<Union>p" apply(rule *[OF False]) proof fix i assume i:"i\<in>p" 

567 
show "\<Union>(q i  {i}) \<union> i = {a..b}" using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto qed 

568 
show "d \<union> p division_of {a..b}" unfolding * apply(rule division_disjoint_union[OF d assms(1)]) 

569 
apply(rule inter_interior_unions_intervals) apply(rule p open_interior ballI)+ proof(assumption,rule) 

570 
fix k assume k:"k\<in>p" have *:"\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}" by auto 

571 
show "interior (\<Inter>(\<lambda>i. \<Union>(q i  {i})) ` p) \<inter> interior k = {}" apply(rule *[of _ "interior (\<Union>(q k  {k}))"]) 

41958  572 
defer apply(subst Int_commute) apply(rule inter_interior_unions_intervals) proof note qk=division_ofD[OF q(1)[OF k]] 
573 
show "finite (q k  {k})" "open (interior k)" "\<forall>t\<in>q k  {k}. \<exists>a b. t = {a..b}" using qk by auto 

574 
show "\<forall>t\<in>q k  {k}. interior k \<inter> interior t = {}" using qk(5) using q(2)[OF k] by auto 

575 
have *:"\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto show "interior (\<Inter>(\<lambda>i. \<Union>(q i  {i})) ` p) \<subseteq> interior (\<Union>(q k  {k}))" 

44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44514
diff
changeset

576 
apply(rule interior_mono *)+ using k by auto qed qed qed auto qed 
35172  577 

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

578 
lemma elementary_bounded[dest]: "p division_of s \<Longrightarrow> bounded (s::('a::ordered_euclidean_space) set)" 
35172  579 
unfolding division_of_def by(metis bounded_Union bounded_interval) 
580 

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

581 
lemma elementary_subset_interval: "p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> {a..b::'a::ordered_euclidean_space}" 
35172  582 
by(meson elementary_bounded bounded_subset_closed_interval) 
583 

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

584 
lemma division_union_intervals_exists: assumes "{a..b::'a::ordered_euclidean_space} \<noteq> {}" 
35172  585 
obtains p where "(insert {a..b} p) division_of ({a..b} \<union> {c..d})" proof(cases "{c..d} = {}") 
586 
case True show ?thesis apply(rule that[of "{}"]) unfolding True using assms by auto next 

587 
case False note false=this show ?thesis proof(cases "{a..b} \<inter> {c..d} = {}") 

588 
have *:"\<And>a b. {a,b} = {a} \<union> {b}" by auto 

589 
case True show ?thesis apply(rule that[of "{{c..d}}"]) unfolding * apply(rule division_disjoint_union) 

590 
using false True assms using interior_subset by auto next 

591 
case False obtain u v where uv:"{a..b} \<inter> {c..d} = {u..v}" unfolding inter_interval by auto 

592 
have *:"{u..v} \<subseteq> {c..d}" using uv by auto 

593 
guess p apply(rule partial_division_extend_1[OF * False[unfolded uv]]) . note p=this division_ofD[OF this(1)] 

594 
have *:"{a..b} \<union> {c..d} = {a..b} \<union> \<Union>(p  {{u..v}})" "\<And>x s. insert x s = {x} \<union> s" using p(8) unfolding uv[THEN sym] by auto 

595 
show thesis apply(rule that[of "p  {{u..v}}"]) unfolding *(1) apply(subst *(2)) apply(rule division_disjoint_union) 

596 
apply(rule,rule assms) apply(rule division_of_subset[of p]) apply(rule division_of_union_self[OF p(1)]) defer 

597 
unfolding interior_inter[THEN sym] proof 

598 
have *:"\<And>cd p uv ab. p \<subseteq> cd \<Longrightarrow> ab \<inter> cd = uv \<Longrightarrow> ab \<inter> p = uv \<inter> p" by auto 

599 
have "interior ({a..b} \<inter> \<Union>(p  {{u..v}})) = interior({u..v} \<inter> \<Union>(p  {{u..v}}))" 

600 
apply(rule arg_cong[of _ _ interior]) apply(rule *[OF _ uv]) using p(8) by auto 

601 
also have "\<dots> = {}" unfolding interior_inter apply(rule inter_interior_unions_intervals) using p(6) p(7)[OF p(2)] p(3) by auto 

602 
finally show "interior ({a..b} \<inter> \<Union>(p  {{u..v}})) = {}" by assumption qed auto qed qed 

603 

604 
lemma division_of_unions: assumes "finite f" "\<And>p. p\<in>f \<Longrightarrow> p division_of (\<Union>p)" 

605 
"\<And>k1 k2. \<lbrakk>k1 \<in> \<Union>f; k2 \<in> \<Union>f; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior k1 \<inter> interior k2 = {}" 

606 
shows "\<Union>f division_of \<Union>\<Union>f" apply(rule division_ofI) prefer 5 apply(rule assms(3)assumption)+ 

607 
apply(rule finite_Union assms(1))+ prefer 3 apply(erule UnionE) apply(rule_tac s=X in division_ofD(3)[OF assms(2)]) 

608 
using division_ofD[OF assms(2)] by auto 

609 

610 
lemma elementary_union_interval: assumes "p division_of \<Union>p" 

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

611 
obtains q where "q division_of ({a..b::'a::ordered_euclidean_space} \<union> \<Union>p)" proof 
35172  612 
note assm=division_ofD[OF assms] 
613 
have lem1:"\<And>f s. \<Union>\<Union> (f ` s) = \<Union>(\<lambda>x.\<Union>(f x)) ` s" by auto 

614 
have lem2:"\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t t. t \<in> f} = s \<union> \<Union>f" by auto 

615 
{ presume "p={} \<Longrightarrow> thesis" "{a..b} = {} \<Longrightarrow> thesis" "{a..b} \<noteq> {} \<Longrightarrow> interior {a..b} = {} \<Longrightarrow> thesis" 

616 
"p\<noteq>{} \<Longrightarrow> interior {a..b}\<noteq>{} \<Longrightarrow> {a..b} \<noteq> {} \<Longrightarrow> thesis" 

617 
thus thesis by auto 

618 
next assume as:"p={}" guess p apply(rule elementary_interval[of a b]) . 

619 
thus thesis apply(rule_tac that[of p]) unfolding as by auto 

620 
next assume as:"{a..b}={}" show thesis apply(rule that) unfolding as using assms by auto 

621 
next assume as:"interior {a..b} = {}" "{a..b} \<noteq> {}" 

622 
show thesis apply(rule that[of "insert {a..b} p"],rule division_ofI) 

623 
unfolding finite_insert apply(rule assm(1)) unfolding Union_insert 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44522
diff
changeset

624 
using assm(24) as apply by(fastforce dest: assm(5))+ 
35172  625 
next assume as:"p \<noteq> {}" "interior {a..b} \<noteq> {}" "{a..b}\<noteq>{}" 
626 
have "\<forall>k\<in>p. \<exists>q. (insert {a..b} q) division_of ({a..b} \<union> k)" proof case goal1 

627 
from assm(4)[OF this] guess c .. then guess d .. 

628 
thus ?case applyapply(rule division_union_intervals_exists[OF as(3),of c d]) by auto 

629 
qed from bchoice[OF this] guess q .. note q=division_ofD[OF this[rule_format]] 

630 
let ?D = "\<Union>{insert {a..b} (q k)  k. k \<in> p}" 

631 
show thesis apply(rule that[of "?D"]) proof(rule division_ofI) 

632 
have *:"{insert {a..b} (q k) k. k \<in> p} = (\<lambda>k. insert {a..b} (q k)) ` p" by auto 

633 
show "finite ?D" apply(rule finite_Union) unfolding * apply(rule finite_imageI) using assm(1) q(1) by auto 

634 
show "\<Union>?D = {a..b} \<union> \<Union>p" unfolding * lem1 unfolding lem2[OF as(1), of "{a..b}",THEN sym] 

635 
using q(6) by auto 

636 
fix k assume k:"k\<in>?D" thus " k \<subseteq> {a..b} \<union> \<Union>p" using q(2) by auto 

637 
show "k \<noteq> {}" using q(3) k by auto show "\<exists>a b. k = {a..b}" using q(4) k by auto 

638 
fix k' assume k':"k'\<in>?D" "k\<noteq>k'" 

639 
obtain x where x: "k \<in>insert {a..b} (q x)" "x\<in>p" using k by auto 

640 
obtain x' where x':"k'\<in>insert {a..b} (q x')" "x'\<in>p" using k' by auto 

641 
show "interior k \<inter> interior k' = {}" proof(cases "x=x'") 

642 
case True show ?thesis apply(rule q(5)) using x x' k' unfolding True by auto 

643 
next case False 

644 
{ presume "k = {a..b} \<Longrightarrow> ?thesis" "k' = {a..b} \<Longrightarrow> ?thesis" 

645 
"k \<noteq> {a..b} \<Longrightarrow> k' \<noteq> {a..b} \<Longrightarrow> ?thesis" 

646 
thus ?thesis by auto } 

647 
{ assume as':"k = {a..b}" show ?thesis apply(rule q(5)) using x' k'(2) unfolding as' by auto } 

648 
{ assume as':"k' = {a..b}" show ?thesis apply(rule q(5)) using x k'(2) unfolding as' by auto } 

649 
assume as':"k \<noteq> {a..b}" "k' \<noteq> {a..b}" 

650 
guess c using q(4)[OF x(2,1)] .. then guess d .. note c_d=this 

651 
have "interior k \<inter> interior {a..b} = {}" apply(rule q(5)) using x k'(2) using as' by auto 

652 
hence "interior k \<subseteq> interior x" apply 

653 
apply(rule interior_subset_union_intervals[OF c_d _ as(2) q(2)[OF x(2,1)]]) by auto moreover 

654 
guess c using q(4)[OF x'(2,1)] .. then guess d .. note c_d=this 

655 
have "interior k' \<inter> interior {a..b} = {}" apply(rule q(5)) using x' k'(2) using as' by auto 

656 
hence "interior k' \<subseteq> interior x'" apply 

657 
apply(rule interior_subset_union_intervals[OF c_d _ as(2) q(2)[OF x'(2,1)]]) by auto 

658 
ultimately show ?thesis using assm(5)[OF x(2) x'(2) False] by auto 

659 
qed qed } qed 

660 

661 
lemma elementary_unions_intervals: 

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

662 
assumes "finite f" "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = {a..b::'a::ordered_euclidean_space}" 
35172  663 
obtains p where "p division_of (\<Union>f)" proof 
664 
have "\<exists>p. p division_of (\<Union>f)" proof(induct_tac f rule:finite_subset_induct) 

665 
show "\<exists>p. p division_of \<Union>{}" using elementary_empty by auto 

666 
fix x F assume as:"finite F" "x \<notin> F" "\<exists>p. p division_of \<Union>F" "x\<in>f" 

667 
from this(3) guess p .. note p=this 

668 
from assms(2)[OF as(4)] guess a .. then guess b .. note ab=this 

669 
have *:"\<Union>F = \<Union>p" using division_ofD[OF p] by auto 

670 
show "\<exists>p. p division_of \<Union>insert x F" using elementary_union_interval[OF p[unfolded *], of a b] 

671 
unfolding Union_insert ab * by auto 

672 
qed(insert assms,auto) thus ?thesis applyapply(erule exE,rule that) by auto qed 

673 

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

674 
lemma elementary_union: assumes "ps division_of s" "pt division_of (t::('a::ordered_euclidean_space) set)" 
35172  675 
obtains p where "p division_of (s \<union> t)" 
676 
proof have "s \<union> t = \<Union>ps \<union> \<Union>pt" using assms unfolding division_of_def by auto 

677 
hence *:"\<Union>(ps \<union> pt) = s \<union> t" by auto 

678 
show ?thesis applyapply(rule elementary_unions_intervals[of "ps\<union>pt"]) 

679 
unfolding * prefer 3 apply(rule_tac p=p in that) 

680 
using assms[unfolded division_of_def] by auto qed 

681 

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

682 
lemma partial_division_extend: fixes t::"('a::ordered_euclidean_space) set" 
35172  683 
assumes "p division_of s" "q division_of t" "s \<subseteq> t" 
684 
obtains r where "p \<subseteq> r" "r division_of t" proof 

685 
note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)] 

686 
obtain a b where ab:"t\<subseteq>{a..b}" using elementary_subset_interval[OF assms(2)] by auto 

687 
guess r1 apply(rule partial_division_extend_interval) apply(rule assms(1)[unfolded divp(6)[THEN sym]]) 

688 
apply(rule subset_trans) by(rule ab assms[unfolded divp(6)[THEN sym]])+ note r1 = this division_ofD[OF this(2)] 

689 
guess p' apply(rule elementary_unions_intervals[of "r1  p"]) using r1(3,6) by auto 

690 
then obtain r2 where r2:"r2 division_of (\<Union>(r1  p)) \<inter> (\<Union>q)" 

691 
apply apply(drule elementary_inter[OF _ assms(2)[unfolded divq(6)[THEN sym]]]) by auto 

692 
{ fix x assume x:"x\<in>t" "x\<notin>s" 

693 
hence "x\<in>\<Union>r1" unfolding r1 using ab by auto 

694 
then guess r unfolding Union_iff .. note r=this moreover 

695 
have "r \<notin> p" proof assume "r\<in>p" hence "x\<in>s" using divp(2) r by auto 

696 
thus False using x by auto qed 

697 
ultimately have "x\<in>\<Union>(r1  p)" by auto } 

698 
hence *:"t = \<Union>p \<union> (\<Union>(r1  p) \<inter> \<Union>q)" unfolding divp divq using assms(3) by auto 

699 
show ?thesis apply(rule that[of "p \<union> r2"]) unfolding * defer apply(rule division_disjoint_union) 

700 
unfolding divp(6) apply(rule assms r2)+ 

701 
proof have "interior s \<inter> interior (\<Union>(r1p)) = {}" 

702 
proof(rule inter_interior_unions_intervals) 

703 
show "finite (r1  p)" "open (interior s)" "\<forall>t\<in>r1p. \<exists>a b. t = {a..b}" using r1 by auto 

704 
have *:"\<And>s. (\<And>x. x \<in> s \<Longrightarrow> False) \<Longrightarrow> s = {}" by auto 

705 
show "\<forall>t\<in>r1p. interior s \<inter> interior t = {}" proof(rule) 

706 
fix m x assume as:"m\<in>r1p" 

707 
have "interior m \<inter> interior (\<Union>p) = {}" proof(rule inter_interior_unions_intervals) 

708 
show "finite p" "open (interior m)" "\<forall>t\<in>p. \<exists>a b. t = {a..b}" using divp by auto 

709 
show "\<forall>t\<in>p. interior m \<inter> interior t = {}" apply(rule, rule r1(7)) using as using r1 by auto 

710 
qed thus "interior s \<inter> interior m = {}" unfolding divp by auto 

711 
qed qed 

712 
thus "interior s \<inter> interior (\<Union>(r1p) \<inter> (\<Union>q)) = {}" using interior_subset by auto 

713 
qed auto qed 

714 

715 
subsection {* Tagged (partial) divisions. *} 

716 

717 
definition tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40) where 

718 
"(s tagged_partial_division_of i) \<equiv> 

719 
finite s \<and> 

720 
(\<forall>x k. (x,k) \<in> s \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = {a..b})) \<and> 

721 
(\<forall>x1 k1 x2 k2. (x1,k1) \<in> s \<and> (x2,k2) \<in> s \<and> ((x1,k1) \<noteq> (x2,k2)) 

722 
\<longrightarrow> (interior(k1) \<inter> interior(k2) = {}))" 

723 

724 
lemma tagged_partial_division_ofD[dest]: assumes "s tagged_partial_division_of i" 

725 
shows "finite s" "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k" "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i" 

726 
"\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = {a..b}" 

727 
"\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2,k2) \<in> s \<Longrightarrow> (x1,k1) \<noteq> (x2,k2) \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}" 

728 
using assms unfolding tagged_partial_division_of_def apply by blast+ 

729 

730 
definition tagged_division_of (infixr "tagged'_division'_of" 40) where 

731 
"(s tagged_division_of i) \<equiv> 

732 
(s tagged_partial_division_of i) \<and> (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)" 

733 

44167  734 
lemma tagged_division_of_finite: "s tagged_division_of i \<Longrightarrow> finite s" 
35172  735 
unfolding tagged_division_of_def tagged_partial_division_of_def by auto 
736 

737 
lemma tagged_division_of: 

738 
"(s tagged_division_of i) \<longleftrightarrow> 

739 
finite s \<and> 

740 
(\<forall>x k. (x,k) \<in> s 

741 
\<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = {a..b})) \<and> 

742 
(\<forall>x1 k1 x2 k2. (x1,k1) \<in> s \<and> (x2,k2) \<in> s \<and> ~((x1,k1) = (x2,k2)) 

743 
\<longrightarrow> (interior(k1) \<inter> interior(k2) = {})) \<and> 

744 
(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)" 

745 
unfolding tagged_division_of_def tagged_partial_division_of_def by auto 

746 

747 
lemma tagged_division_ofI: assumes 

748 
"finite s" "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k" "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i" "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = {a..b}" 

749 
"\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2,k2) \<in> s \<Longrightarrow> ~((x1,k1) = (x2,k2)) \<Longrightarrow> (interior(k1) \<inter> interior(k2) = {})" 

750 
"(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)" 

751 
shows "s tagged_division_of i" 

752 
unfolding tagged_division_of apply(rule) defer apply rule 

753 
apply(rule allI impI conjI assms)+ apply assumption 

754 
apply(rule, rule assms, assumption) apply(rule assms, assumption) 

755 
using assms(1,5) apply by blast+ 

756 

757 
lemma tagged_division_ofD[dest]: assumes "s tagged_division_of i" 

758 
shows "finite s" "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k" "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i" "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = {a..b}" 

759 
"\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2,k2) \<in> s \<Longrightarrow> ~((x1,k1) = (x2,k2)) \<Longrightarrow> (interior(k1) \<inter> interior(k2) = {})" 

760 
"(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)" using assms unfolding tagged_division_of apply by blast+ 

761 

762 
lemma division_of_tagged_division: assumes"s tagged_division_of i" shows "(snd ` s) division_of i" 

763 
proof(rule division_ofI) note assm=tagged_division_ofD[OF assms] 

764 
show "\<Union>snd ` s = i" "finite (snd ` s)" using assm by auto 

765 
fix k assume k:"k \<in> snd ` s" then obtain xk where xk:"(xk, k) \<in> s" by auto 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44522
diff
changeset

766 
thus "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = {a..b}" using assm apply by fastforce+ 
35172  767 
fix k' assume k':"k' \<in> snd ` s" "k \<noteq> k'" from this(1) obtain xk' where xk':"(xk', k') \<in> s" by auto 
768 
thus "interior k \<inter> interior k' = {}" applyapply(rule assm(5)) apply(rule xk xk')+ using k' by auto 

769 
qed 

770 

771 
lemma partial_division_of_tagged_division: assumes "s tagged_partial_division_of i" 

772 
shows "(snd ` s) division_of \<Union>(snd ` s)" 

773 
proof(rule division_ofI) note assm=tagged_partial_division_ofD[OF assms] 

774 
show "finite (snd ` s)" "\<Union>snd ` s = \<Union>snd ` s" using assm by auto 

775 
fix k assume k:"k \<in> snd ` s" then obtain xk where xk:"(xk, k) \<in> s" by auto 

776 
thus "k\<noteq>{}" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>snd ` s" using assm by auto 

777 
fix k' assume k':"k' \<in> snd ` s" "k \<noteq> k'" from this(1) obtain xk' where xk':"(xk', k') \<in> s" by auto 

778 
thus "interior k \<inter> interior k' = {}" applyapply(rule assm(5)) apply(rule xk xk')+ using k' by auto 

779 
qed 

780 

781 
lemma tagged_partial_division_subset: assumes "s tagged_partial_division_of i" "t \<subseteq> s" 

782 
shows "t tagged_partial_division_of i" 

783 
using assms unfolding tagged_partial_division_of_def using finite_subset[OF assms(2)] by blast 

784 

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

785 
lemma setsum_over_tagged_division_lemma: fixes d::"('m::ordered_euclidean_space) set \<Rightarrow> 'a::real_normed_vector" 
35172  786 
assumes "p tagged_division_of i" "\<And>u v. {u..v} \<noteq> {} \<Longrightarrow> content {u..v} = 0 \<Longrightarrow> d {u..v} = 0" 
787 
shows "setsum (\<lambda>(x,k). d k) p = setsum d (snd ` p)" 

788 
proof note assm=tagged_division_ofD[OF assms(1)] 

789 
have *:"(\<lambda>(x,k). d k) = d \<circ> snd" unfolding o_def apply(rule ext) by auto 

790 
show ?thesis unfolding * apply(subst eq_commute) proof(rule setsum_reindex_nonzero) 

791 
show "finite p" using assm by auto 

792 
fix x y assume as:"x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y" 

793 
obtain a b where ab:"snd x = {a..b}" using assm(4)[of "fst x" "snd x"] as(1) by auto 

794 
have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y" unfolding as(4)[THEN sym] using as(13) by auto 

795 
hence "interior (snd x) \<inter> interior (snd y) = {}" applyapply(rule assm(5)[of "fst x" _ "fst y"]) using as by auto 

796 
hence "content {a..b} = 0" unfolding as(4)[THEN sym] ab content_eq_0_interior by auto 

797 
hence "d {a..b} = 0" applyapply(rule assms(2)) using assm(2)[of "fst x" "snd x"] as(1) unfolding ab[THEN sym] by auto 

798 
thus "d (snd x) = 0" unfolding ab by auto qed qed 

799 

800 
lemma tag_in_interval: "p tagged_division_of i \<Longrightarrow> (x,k) \<in> p \<Longrightarrow> x \<in> i" by auto 

801 

802 
lemma tagged_division_of_empty: "{} tagged_division_of {}" 

803 
unfolding tagged_division_of by auto 

804 

805 
lemma tagged_partial_division_of_trivial[simp]: 

806 
"p tagged_partial_division_of {} \<longleftrightarrow> p = {}" 

807 
unfolding tagged_partial_division_of_def by auto 

808 

809 
lemma tagged_division_of_trivial[simp]: 

810 
"p tagged_division_of {} \<longleftrightarrow> p = {}" 

811 
unfolding tagged_division_of by auto 

812 

813 
lemma tagged_division_of_self: 

814 
"x \<in> {a..b} \<Longrightarrow> {(x,{a..b})} tagged_division_of {a..b}" 

815 
apply(rule tagged_division_ofI) by auto 

816 

817 
lemma tagged_division_union: 

818 
assumes "p1 tagged_division_of s1" "p2 tagged_division_of s2" "interior s1 \<inter> interior s2 = {}" 

819 
shows "(p1 \<union> p2) tagged_division_of (s1 \<union> s2)" 

820 
proof(rule tagged_division_ofI) note p1=tagged_division_ofD[OF assms(1)] and p2=tagged_division_ofD[OF assms(2)] 

821 
show "finite (p1 \<union> p2)" using p1(1) p2(1) by auto 

822 
show "\<Union>{k. \<exists>x. (x, k) \<in> p1 \<union> p2} = s1 \<union> s2" using p1(6) p2(6) by blast 

823 
fix x k assume xk:"(x,k)\<in>p1\<union>p2" show "x\<in>k" "\<exists>a b. k = {a..b}" using xk p1(2,4) p2(2,4) by auto 

824 
show "k\<subseteq>s1\<union>s2" using xk p1(3) p2(3) by blast 

825 
fix x' k' assume xk':"(x',k')\<in>p1\<union>p2" "(x,k) \<noteq> (x',k')" 

44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44514
diff
changeset

826 
have *:"\<And>a b. a\<subseteq> s1 \<Longrightarrow> b\<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}" using assms(3) interior_mono by blast 
35172  827 
show "interior k \<inter> interior k' = {}" apply(cases "(x,k)\<in>p1", case_tac[!] "(x',k')\<in>p1") 
828 
apply(rule p1(5)) prefer 4 apply(rule *) prefer 6 apply(subst Int_commute,rule *) prefer 8 apply(rule p2(5)) 

829 
using p1(3) p2(3) using xk xk' by auto qed 

830 

831 
lemma tagged_division_unions: 

832 
assumes "finite iset" "\<forall>i\<in>iset. (pfn(i) tagged_division_of i)" 

833 
"\<forall>i1 \<in> iset. \<forall>i2 \<in> iset. ~(i1 = i2) \<longrightarrow> (interior(i1) \<inter> interior(i2) = {})" 

834 
shows "\<Union>(pfn ` iset) tagged_division_of (\<Union>iset)" 

835 
proof(rule tagged_division_ofI) 

836 
note assm = tagged_division_ofD[OF assms(2)[rule_format]] 

837 
show "finite (\<Union>pfn ` iset)" apply(rule finite_Union) using assms by auto 

838 
have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>pfn ` iset} = \<Union>(\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset" by blast 

839 
also have "\<dots> = \<Union>iset" using assm(6) by auto 

840 
finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>pfn ` iset} = \<Union>iset" . 

841 
fix x k assume xk:"(x,k)\<in>\<Union>pfn ` iset" then obtain i where i:"i \<in> iset" "(x, k) \<in> pfn i" by auto 

842 
show "x\<in>k" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>iset" using assm(24)[OF i] using i(1) by auto 

843 
fix x' k' assume xk':"(x',k')\<in>\<Union>pfn ` iset" "(x, k) \<noteq> (x', k')" then obtain i' where i':"i' \<in> iset" "(x', k') \<in> pfn i'" by auto 

844 
have *:"\<And>a b. i\<noteq>i' \<Longrightarrow> a\<subseteq> i \<Longrightarrow> b\<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}" using i(1) i'(1) 

44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44514
diff
changeset

845 
using assms(3)[rule_format] interior_mono by blast 
35172  846 
show "interior k \<inter> interior k' = {}" apply(cases "i=i'") 
847 
using assm(5)[OF i _ xk'(2)] i'(2) using assm(3)[OF i] assm(3)[OF i'] defer applyapply(rule *) by auto 

848 
qed 

849 

850 
lemma tagged_partial_division_of_union_self: 

851 
assumes "p tagged_partial_division_of s" shows "p tagged_division_of (\<Union>(snd ` p))" 

852 
apply(rule tagged_division_ofI) using tagged_partial_division_ofD[OF assms] by auto 

853 

854 
lemma tagged_division_of_union_self: assumes "p tagged_division_of s" 

855 
shows "p tagged_division_of (\<Union>(snd ` p))" 

856 
apply(rule tagged_division_ofI) using tagged_division_ofD[OF assms] by auto 

857 

858 
subsection {* Fineness of a partition w.r.t. a gauge. *} 

859 

860 
definition fine (infixr "fine" 46) where 

861 
"d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d(x))" 

862 

863 
lemma fineI: assumes "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> d x" 

864 
shows "d fine s" using assms unfolding fine_def by auto 

865 

866 
lemma fineD[dest]: assumes "d fine s" 

867 
shows "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> d x" using assms unfolding fine_def by auto 

868 

869 
lemma fine_inter: "(\<lambda>x. d1 x \<inter> d2 x) fine p \<longleftrightarrow> d1 fine p \<and> d2 fine p" 

870 
unfolding fine_def by auto 

871 

872 
lemma fine_inters: 

873 
"(\<lambda>x. \<Inter> {f d x  d. d \<in> s}) fine p \<longleftrightarrow> (\<forall>d\<in>s. (f d) fine p)" 

874 
unfolding fine_def by blast 

875 

876 
lemma fine_union: 

877 
"d fine p1 \<Longrightarrow> d fine p2 \<Longrightarrow> d fine (p1 \<union> p2)" 

878 
unfolding fine_def by blast 

879 

880 
lemma fine_unions:"(\<And>p. p \<in> ps \<Longrightarrow> d fine p) \<Longrightarrow> d fine (\<Union>ps)" 

881 
unfolding fine_def by auto 

882 

883 
lemma fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p" 

884 
unfolding fine_def by blast 

885 

886 
subsection {* Gauge integral. Define on compact intervals first, then use a limit. *} 

887 

888 
definition has_integral_compact_interval (infixr "has'_integral'_compact'_interval" 46) where 

889 
"(f has_integral_compact_interval y) i \<equiv> 

890 
(\<forall>e>0. \<exists>d. gauge d \<and> 

891 
(\<forall>p. p tagged_division_of i \<and> d fine p 

892 
\<longrightarrow> norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p  y) < e))" 

893 

894 
definition has_integral (infixr "has'_integral" 46) where 

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

895 
"((f::('n::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector)) has_integral y) i \<equiv> 
35172  896 
if (\<exists>a b. i = {a..b}) then (f has_integral_compact_interval y) i 
897 
else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} 

898 
\<longrightarrow> (\<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral_compact_interval z) {a..b} \<and> 

899 
norm(z  y) < e))" 

900 

901 
lemma has_integral: 

902 
"(f has_integral y) ({a..b}) \<longleftrightarrow> 

903 
(\<forall>e>0. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p 

904 
\<longrightarrow> norm(setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p  y) < e))" 

905 
unfolding has_integral_def has_integral_compact_interval_def by auto 

906 

907 
lemma has_integralD[dest]: assumes 

908 
"(f has_integral y) ({a..b})" "e>0" 

909 
obtains d where "gauge d" "\<And>p. p tagged_division_of {a..b} \<Longrightarrow> d fine p 

910 
\<Longrightarrow> norm(setsum (\<lambda>(x,k). content(k) *\<^sub>R f(x)) p  y) < e" 

911 
using assms unfolding has_integral by auto 

912 

913 
lemma has_integral_alt: 

914 
"(f has_integral y) i \<longleftrightarrow> 

915 
(if (\<exists>a b. i = {a..b}) then (f has_integral y) i 

916 
else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} 

917 
\<longrightarrow> (\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0) 

918 
has_integral z) ({a..b}) \<and> 

919 
norm(z  y) < e)))" 

920 
unfolding has_integral unfolding has_integral_compact_interval_def has_integral_def by auto 

921 

922 
lemma has_integral_altD: 

923 
assumes "(f has_integral y) i" "\<not> (\<exists>a b. i = {a..b})" "e>0" 

924 
obtains B where "B>0" "\<forall>a b. ball 0 B \<subseteq> {a..b}\<longrightarrow> (\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0) has_integral z) ({a..b}) \<and> norm(z  y) < e)" 

925 
using assms unfolding has_integral unfolding has_integral_compact_interval_def has_integral_def by auto 

926 

927 
definition integrable_on (infixr "integrable'_on" 46) where 

928 
"(f integrable_on i) \<equiv> \<exists>y. (f has_integral y) i" 

929 

930 
definition "integral i f \<equiv> SOME y. (f has_integral y) i" 

931 

932 
lemma integrable_integral[dest]: 

933 
"f integrable_on i \<Longrightarrow> (f has_integral (integral i f)) i" 

934 
unfolding integrable_on_def integral_def by(rule someI_ex) 

935 

936 
lemma has_integral_integrable[intro]: "(f has_integral i) s \<Longrightarrow> f integrable_on s" 

937 
unfolding integrable_on_def by auto 

938 

939 
lemma has_integral_integral:"f integrable_on s \<longleftrightarrow> (f has_integral (integral s f)) s" 

940 
by auto 

941 

942 
lemma setsum_content_null: 

943 
assumes "content({a..b}) = 0" "p tagged_division_of {a..b}" 

944 
shows "setsum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)" 

945 
proof(rule setsum_0',rule) fix y assume y:"y\<in>p" 

946 
obtain x k where xk:"y = (x,k)" using surj_pair[of y] by blast 

947 
note assm = tagged_division_ofD(34)[OF assms(2) y[unfolded xk]] 

948 
from this(2) guess c .. then guess d .. note c_d=this 

949 
have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x" unfolding xk by auto 

950 
also have "\<dots> = 0" using content_subset[OF assm(1)[unfolded c_d]] content_pos_le[of c d] 

951 
unfolding assms(1) c_d by auto 

952 
finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" . 

953 
qed 

954 

955 
subsection {* Some basic combining lemmas. *} 

956 

957 
lemma tagged_division_unions_exists: 

958 
assumes "finite iset" "\<forall>i \<in> iset. \<exists>p. p tagged_division_of i \<and> d fine p" 

959 
"\<forall>i1\<in>iset. \<forall>i2\<in>iset. ~(i1 = i2) \<longrightarrow> (interior(i1) \<inter> interior(i2) = {})" "(\<Union>iset = i)" 

960 
obtains p where "p tagged_division_of i" "d fine p" 

961 
proof guess pfn using bchoice[OF assms(2)] .. note pfn = conjunctD2[OF this[rule_format]] 

962 
show thesis apply(rule_tac p="\<Union>(pfn ` iset)" in that) unfolding assms(4)[THEN sym] 

963 
apply(rule tagged_division_unions[OF assms(1) _ assms(3)]) defer 

964 
apply(rule fine_unions) using pfn by auto 

965 
qed 

966 

967 
subsection {* The set we're concerned with must be closed. *} 

968 

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

969 
lemma division_of_closed: "s division_of i \<Longrightarrow> closed (i::('n::ordered_euclidean_space) set)" 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44522
diff
changeset

970 
unfolding division_of_def by fastforce 
35172  971 

972 
subsection {* General bisection principle for intervals; might be useful elsewhere. *} 

973 

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

974 
lemma interval_bisection_step: fixes type::"'a::ordered_euclidean_space" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

975 
assumes "P {}" "(\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P(s \<union> t))" "~(P {a..b::'a})" 
35172  976 
obtains c d where "~(P{c..d})" 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

977 
"\<forall>i<DIM('a). a$$i \<le> c$$i \<and> c$$i \<le> d$$i \<and> d$$i \<le> b$$i \<and> 2 * (d$$i  c$$i) \<le> b$$i  a$$i" 
35172  978 
proof have "{a..b} \<noteq> {}" using assms(1,3) by auto 
979 
note ab=this[unfolded interval_eq_empty not_ex not_less] 

980 
{ fix f have "finite f \<Longrightarrow> 

981 
(\<forall>s\<in>f. P s) \<Longrightarrow> 

982 
(\<forall>s\<in>f. \<exists>a b. s = {a..b}) \<Longrightarrow> 

983 
(\<forall>s\<in>f.\<forall>t\<in>f. ~(s = t) \<longrightarrow> interior(s) \<inter> interior(t) = {}) \<Longrightarrow> P(\<Union>f)" 

984 
proof(induct f rule:finite_induct) 

985 
case empty show ?case using assms(1) by auto 

986 
next case (insert x f) show ?case unfolding Union_insert apply(rule assms(2)[rule_format]) 

987 
apply rule defer apply rule defer apply(rule inter_interior_unions_intervals) 

988 
using insert by auto 

989 
qed } note * = this 

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

990 
let ?A = "{{c..d}  c d::'a. \<forall>i<DIM('a). (c$$i = a$$i) \<and> (d$$i = (a$$i + b$$i) / 2) \<or> (c$$i = (a$$i + b$$i) / 2) \<and> (d$$i = b$$i)}" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

991 
let ?PP = "\<lambda>c d. \<forall>i<DIM('a). a$$i \<le> c$$i \<and> c$$i \<le> d$$i \<and> d$$i \<le> b$$i \<and> 2 * (d$$i  c$$i) \<le> b$$i  a$$i" 
35172  992 
{ presume "\<forall>c d. ?PP c d \<longrightarrow> P {c..d} \<Longrightarrow> False" 
993 
thus thesis unfolding atomize_not not_all applyapply(erule exE)+ apply(rule_tac c=x and d=xa in that) by auto } 

994 
assume as:"\<forall>c d. ?PP c d \<longrightarrow> P {c..d}" 

995 
have "P (\<Union> ?A)" proof(rule *, rule_tac[2] ballI, rule_tac[4] ballI, rule_tac[4] impI) 

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

996 
let ?B = "(\<lambda>s.{(\<chi>\<chi> i. if i \<in> s then a$$i else (a$$i + b$$i) / 2)::'a .. 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

997 
(\<chi>\<chi> i. if i \<in> s then (a$$i + b$$i) / 2 else b$$i)}) ` {s. s \<subseteq> {..<DIM('a)}}" 
35172  998 
have "?A \<subseteq> ?B" proof case goal1 
999 
then guess c unfolding mem_Collect_eq .. then guess d apply by(erule exE,(erule conjE)+) note c_d=this[rule_format] 

1000 
have *:"\<And>a b c d. a = c \<Longrightarrow> b = d \<Longrightarrow> {a..b} = {c..d}" by auto 

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

1001 
show "x\<in>?B" unfolding image_iff apply(rule_tac x="{i. i<DIM('a) \<and> c$$i = a$$i}" in bexI) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1002 
unfolding c_d apply(rule * ) unfolding euclidean_eq[where 'a='a] apply safe unfolding euclidean_lambda_beta' mem_Collect_eq 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1003 
proof fix i assume "i<DIM('a)" thus " c $$ i = (if i < DIM('a) \<and> c $$ i = a $$ i then a $$ i else (a $$ i + b $$ i) / 2)" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1004 
"d $$ i = (if i < DIM('a) \<and> c $$ i = a $$ i then (a $$ i + b $$ i) / 2 else b $$ i)" 
35172  1005 
using c_d(2)[of i] ab[THEN spec[where x=i]] by(auto simp add:field_simps) 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

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

1007 
thus "finite ?A" apply(rule finite_subset) by auto 
35172  1008 
fix s assume "s\<in>?A" then guess c unfolding mem_Collect_eq .. then guess d apply by(erule exE,(erule conjE)+) 
1009 
note c_d=this[rule_format] 

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

1010 
show "P s" unfolding c_d apply(rule as[rule_format]) proof case goal1 thus ?case 
35172  1011 
using c_d(2)[of i] using ab[THEN spec[where x=i]] by auto qed 
1012 
show "\<exists>a b. s = {a..b}" unfolding c_d by auto 

1013 
fix t assume "t\<in>?A" then guess e unfolding mem_Collect_eq .. then guess f apply by(erule exE,(erule conjE)+) 

1014 
note e_f=this[rule_format] 

1015 
assume "s \<noteq> t" hence "\<not> (c = e \<and> d = f)" unfolding c_d e_f by auto 

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

1016 
then obtain i where "c$$i \<noteq> e$$i \<or> d$$i \<noteq> f$$i" and i':"i<DIM('a)" unfolding de_Morgan_conj euclidean_eq[where 'a='a] by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1017 
hence i:"c$$i \<noteq> e$$i" "d$$i \<noteq> f$$i" apply apply(erule_tac[!] disjE) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44522
diff
changeset

1018 
proof assume "c$$i \<noteq> e$$i" thus "d$$i \<noteq> f$$i" using c_d(2)[of i] e_f(2)[of i] by fastforce 
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44522
diff
changeset

1019 
next assume "d$$i \<noteq> f$$i" thus "c$$i \<noteq> e$$i" using c_d(2)[of i] e_f(2)[of i] by fastforce 
35172  1020 
qed have *:"\<And>s t. (\<And>a. a\<in>s \<Longrightarrow> a\<in>t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}" by auto 
1021 
show "interior s \<inter> interior t = {}" unfolding e_f c_d interior_closed_interval proof(rule *) 

1022 
fix x assume "x\<in>{c<..<d}" "x\<in>{e<..<f}" 

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

1023 
hence x:"c$$i < d$$i" "e$$i < f$$i" "c$$i < f$$i" "e$$i < d$$i" unfolding mem_interval using i' 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1024 
applyapply(erule_tac[!] x=i in allE)+ by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1025 
show False using c_d(2)[OF i'] apply apply(erule_tac disjE) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1026 
proof(erule_tac[!] conjE) assume as:"c $$ i = a $$ i" "d $$ i = (a $$ i + b $$ i) / 2" 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44522
diff
changeset

1027 
show False using e_f(2)[of i] and i x unfolding as by(fastforce simp add:field_simps) 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1028 
next assume as:"c $$ i = (a $$ i + b $$ i) / 2" "d $$ i = b $$ i" 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44522
diff
changeset

1029 
show False using e_f(2)[of i] and i x unfolding as by(fastforce simp add:field_simps) 
35172  1030 
qed qed qed 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
38656
diff
changeset

1031 
also have "\<Union> ?A = {a..b}" proof(rule set_eqI,rule) 
35172  1032 
fix x assume "x\<in>\<Union>?A" then guess Y unfolding Union_iff .. 
1033 
from this(1) guess c unfolding mem_Collect_eq .. then guess d .. 

1034 
note c_d = this[THEN conjunct2,rule_format] `x\<in>Y`[unfolded this[THEN conjunct1]] 

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

1035 
show "x\<in>{a..b}" unfolding mem_interval proof safe 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1036 
fix i assume "i<DIM('a)" thus "a $$ i \<le> x $$ i" "x $$ i \<le> b $$ i" 
35172  1037 
using c_d(1)[of i] c_d(2)[unfolded mem_interval,THEN spec[where x=i]] by auto qed 
1038 
next fix x assume x:"x\<in>{a..b}" 

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

1039 
have "\<forall>i<DIM('a). \<exists>c d. (c = a$$i \<and> d = (a$$i + b$$i) / 2 \<or> c = (a$$i + b$$i) / 2 \<and> d = b$$i) \<and> c\<le>x$$i \<and> x$$i \<le> d" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1040 
(is "\<forall>i<DIM('a). \<exists>c d. ?P i c d") unfolding mem_interval proof(rule,rule) fix i 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1041 
have "?P i (a$$i) ((a $$ i + b $$ i) / 2) \<or> ?P i ((a $$ i + b $$ i) / 2) (b$$i)" 
35172  1042 
using x[unfolded mem_interval,THEN spec[where x=i]] by auto thus "\<exists>c d. ?P i c d" by blast 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1043 
qed thus "x\<in>\<Union>?A" unfolding Union_iff unfolding lambda_skolem' unfolding Bex_def mem_Collect_eq 
35172  1044 
applyapply(erule exE)+ apply(rule_tac x="{xa..xaa}" in exI) unfolding mem_interval by auto 
1045 
qed finally show False using assms by auto qed 

1046 

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

1047 
lemma interval_bisection: fixes type::"'a::ordered_euclidean_space" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1048 
assumes "P {}" "(\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P(s \<union> t))" "\<not> P {a..b::'a}" 
35172  1049 
obtains x where "x \<in> {a..b}" "\<forall>e>0. \<exists>c d. x \<in> {c..d} \<and> {c..d} \<subseteq> ball x e \<and> {c..d} \<subseteq> {a..b} \<and> ~P({c..d})" 
1050 
proof 

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

1051 
have "\<forall>x. \<exists>y. \<not> P {fst x..snd x} \<longrightarrow> (\<not> P {fst y..snd y} \<and> 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1052 
(\<forall>i<DIM('a). fst x$$i \<le> fst y$$i \<and> fst y$$i \<le> snd y$$i \<and> snd y$$i \<le> snd x$$i \<and> 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1053 
2 * (snd y$$i  fst y$$i) \<le> snd x$$i  fst x$$i))" proof case goal1 thus ?case proof 
35172  1054 
presume "\<not> P {fst x..snd x} \<Longrightarrow> ?thesis" 
1055 
thus ?thesis apply(cases "P {fst x..snd x}") by auto 

1056 
next assume as:"\<not> P {fst x..snd x}" from interval_bisection_step[of P, OF assms(12) as] guess c d . 

1057 
thus ?thesis apply apply(rule_tac x="(c,d)" in exI) by auto 

1058 
qed qed then guess f applyapply(drule choice) by(erule exE) note f=this 

1059 
def AB \<equiv> "\<lambda>n. (f ^^ n) (a,b)" def A \<equiv> "\<lambda>n. fst(AB n)" and B \<equiv> "\<lambda>n. snd(AB n)" note ab_def = this AB_def 

1060 
have "A 0 = a" "B 0 = b" "\<And>n. \<not> P {A(Suc n)..B(Suc n)} \<and> 

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

1061 
(\<forall>i<DIM('a). A(n)$$i \<le> A(Suc n)$$i \<and> A(Suc n)$$i \<le> B(Suc n)$$i \<and> B(Suc n)$$i \<le> B(n)$$i \<and> 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1062 
2 * (B(Suc n)$$i  A(Suc n)$$i) \<le> B(n)$$i  A(n)$$i)" (is "\<And>n. ?P n") 
35172  1063 
proof show "A 0 = a" "B 0 = b" unfolding ab_def by auto 
1064 
case goal3 note S = ab_def funpow.simps o_def id_apply show ?case 

1065 
proof(induct n) case 0 thus ?case unfolding S apply(rule f[rule_format]) using assms(3) by auto 

1066 
next case (Suc n) show ?case unfolding S apply(rule f[rule_format]) using Suc unfolding S by auto 

1067 
qed qed note AB = this(12) conjunctD2[OF this(3),rule_format] 

1068 

1069 
have interv:"\<And>e. 0 < e \<Longrightarrow> \<exists>n. \<forall>x\<in>{A n..B n}. \<forall>y\<in>{A n..B n}. dist x y < e" 

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

1070 
proof case goal1 guess n using real_arch_pow2[of "(setsum (\<lambda>i. b$$i  a$$i) {..<DIM('a)}) / e"] .. note n=this 
35172  1071 
show ?case apply(rule_tac x=n in exI) proof(rule,rule) 
1072 
fix x y assume xy:"x\<in>{A n..B n}" "y\<in>{A n..B n}" 

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

1073 
have "dist x y \<le> setsum (\<lambda>i. abs((x  y)$$i)) {..<DIM('a)}" unfolding dist_norm by(rule norm_le_l1) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1074 
also have "\<dots> \<le> setsum (\<lambda>i. B n$$i  A n$$i) {..<DIM('a)}" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1075 
proof(rule setsum_mono) fix i show "\<bar>(x  y) $$ i\<bar> \<le> B n $$ i  A n $$ i" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1076 
using xy[unfolded mem_interval,THEN spec[where x=i]] by auto qed 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1077 
also have "\<dots> \<le> setsum (\<lambda>i. b$$i  a$$i) {..<DIM('a)} / 2^n" unfolding setsum_divide_distrib 
35172  1078 
proof(rule setsum_mono) case goal1 thus ?case 
1079 
proof(induct n) case 0 thus ?case unfolding AB by auto 

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

1080 
next case (Suc n) have "B (Suc n) $$ i  A (Suc n) $$ i \<le> (B n $$ i  A n $$ i) / 2" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1081 
using AB(4)[of i n] using goal1 by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1082 
also have "\<dots> \<le> (b $$ i  a $$ i) / 2 ^ Suc n" using Suc by(auto simp add:field_simps) finally show ?case . 
35172  1083 
qed qed 
1084 
also have "\<dots> < e" using n using goal1 by(auto simp add:field_simps) finally show "dist x y < e" . 

1085 
qed qed 

1086 
{ fix n m ::nat assume "m \<le> n" then guess d unfolding le_Suc_ex_iff .. note d=this 

1087 
have "{A n..B n} \<subseteq> {A m..B m}" unfolding d 

1088 
proof(induct d) case 0 thus ?case by auto 

1089 
next case (Suc d) show ?case apply(rule subset_trans[OF _ Suc]) 

1090 
apply(rule) unfolding mem_interval apply(rule,erule_tac x=i in allE) 

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

1091 
proof case goal1 thus ?case using AB(4)[of i "m + d"] by(auto simp add:field_simps) 
35172  1092 
qed qed } note ABsubset = this 
1093 
have "\<exists>a. \<forall>n. a\<in>{A n..B n}" apply(rule decreasing_closed_nest[rule_format,OF closed_interval _ ABsubset interv]) 

1094 
proof fix n show "{A n..B n} \<noteq> {}" apply(cases "0<n") using AB(3)[of "n  1"] assms(1,3) AB(12) by auto qed auto 

1095 
then guess x0 .. note x0=this[rule_format] 

1096 
show thesis proof(rule that[rule_format,of x0]) 

1097 
show "x0\<in>{a..b}" using x0[of 0] unfolding AB . 

1098 
fix e assume "0 < (e::real)" from interv[OF this] guess n .. note n=this 

1099 
show "\<exists>c d. x0 \<in> {c..d} \<and> {c..d} \<subseteq> ball x0 e \<and> {c..d} \<subseteq> {a..b} \<and> \<not> P {c..d}" 

1100 
apply(rule_tac x="A n" in exI,rule_tac x="B n" in exI) apply(rule,rule x0) apply rule defer 

1101 
proof show "\<not> P {A n..B n}" apply(cases "0<n") using AB(3)[of "n  1"] assms(3) AB(12) by auto 

1102 
show "{A n..B n} \<subseteq> ball x0 e" using n using x0[of n] by auto 

1103 
show "{A n..B n} \<subseteq> {a..b}" unfolding AB(12)[symmetric] apply(rule ABsubset) by auto 

1104 
qed qed qed 

1105 

1106 
subsection {* Cousin's lemma. *} 

1107 

1108 
lemma fine_division_exists: assumes "gauge g" 

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

1109 
obtains p where "p tagged_division_of {a..b::'a::ordered_euclidean_space}" "g fine p" 
35172  1110 
proof presume "\<not> (\<exists>p. p tagged_division_of {a..b} \<and> g fine p) \<Longrightarrow> False" 
1111 
then guess p unfolding atomize_not not_not .. thus thesis applyapply(rule that[of p]) by auto 

1112 
next assume as:"\<not> (\<exists>p. p tagged_division_of {a..b} \<and> g fine p)" 

1113 
guess x apply(rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p",rule_format,OF _ _ as]) 

1114 
apply(rule_tac x="{}" in exI) defer apply(erule conjE exE)+ 

1115 
proof show "{} tagged_division_of {} \<and> g fine {}" unfolding fine_def by auto 

1116 
fix s t p p' assume "p tagged_division_of s" "g fine p" "p' tagged_division_of t" "g fine p'" "interior s \<inter> interior t = {}" 

1117 
thus "\<exists>p. p tagged_division_of s \<union> t \<and> g fine p" applyapply(rule_tac x="p \<union> p'" in exI) apply rule 

1118 
apply(rule tagged_division_union) prefer 4 apply(rule fine_union) by auto 

1119 
qed note x=this 

1120 
obtain e where e:"e>0" "ball x e \<subseteq> g x" using gaugeD[OF assms, of x] unfolding open_contains_ball by auto 

1121 
from x(2)[OF e(1)] guess c d applyapply(erule exE conjE)+ . note c_d = this 

1122 
have "g fine {(x, {c..d})}" unfolding fine_def using e using c_d(2) by auto 

1123 
thus False using tagged_division_of_self[OF c_d(1)] using c_d by auto qed 

1124 

1125 
subsection {* Basic theorems about integrals. *} 

1126 

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

1127 
lemma has_integral_unique: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector" 
35172  1128 
assumes "(f has_integral k1) i" "(f has_integral k2) i" shows "k1 = k2" 
1129 
proof(rule ccontr) let ?e = "norm(k1  k2) / 2" assume as:"k1 \<noteq> k2" hence e:"?e > 0" by auto 

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

1130 
have lem:"\<And>f::'n \<Rightarrow> 'a. \<And> a b k1 k2. 
35172  1131 
(f has_integral k1) ({a..b}) \<Longrightarrow> (f has_integral k2) ({a..b}) \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> False" 
1132 
proof case goal1 let ?e = "norm(k1  k2) / 2" from goal1(3) have e:"?e > 0" by auto 

1133 
guess d1 by(rule has_integralD[OF goal1(1) e]) note d1=this 

1134 
guess d2 by(rule has_integralD[OF goal1(2) e]) note d2=this 

1135 
guess p by(rule fine_division_exists[OF gauge_inter[OF d1(1) d2(1)],of a b]) note p=this 

1136 
let ?c = "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" have "norm (k1  k2) \<le> norm (?c  k2) + norm (?c  k1)" 

36350  1137 
using norm_triangle_ineq4[of "k1  ?c" "k2  ?c"] by(auto simp add:algebra_simps norm_minus_commute) 
35172  1138 
also have "\<dots> < norm (k1  k2) / 2 + norm (k1  k2) / 2" 
1139 
apply(rule add_strict_mono) apply(rule_tac[!] d2(2) d1(2)) using p unfolding fine_def by auto 

1140 
finally show False by auto 

1141 
qed { presume "\<not> (\<exists>a b. i = {a..b}) \<Longrightarrow> False" 

1142 
thus False applyapply(cases "\<exists>a b. i = {a..b}") 

1143 
using assms by(auto simp add:has_integral intro:lem[OF _ _ as]) } 

1144 
assume as:"\<not> (\<exists>a b. i = {a..b})" 

1145 
guess B1 by(rule has_integral_altD[OF assms(1) as,OF e]) note B1=this[rule_format] 

1146 
guess B2 by(rule has_integral_altD[OF assms(2) as,OF e]) note B2=this[rule_format] 

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

1147 
have "\<exists>a b::'n. ball 0 B1 \<union> ball 0 B2 \<subseteq> {a..b}" apply(rule bounded_subset_closed_interval) 
35172  1148 
using bounded_Un bounded_ball by auto then guess a b applyby(erule exE)+ 
1149 
note ab=conjunctD2[OF this[unfolded Un_subset_iff]] 

1150 
guess w using B1(2)[OF ab(1)] .. note w=conjunctD2[OF this] 

1151 
guess z using B2(2)[OF ab(2)] .. note z=conjunctD2[OF this] 

1152 
have "z = w" using lem[OF w(1) z(1)] by auto 

1153 
hence "norm (k1  k2) \<le> norm (z  k2) + norm (w  k1)" 

1154 
using norm_triangle_ineq4[of "k1  w" "k2  z"] by(auto simp add: norm_minus_commute) 

1155 
also have "\<dots> < norm (k1  k2) / 2 + norm (k1  k2) / 2" apply(rule add_strict_mono) by(rule_tac[!] z(2) w(2)) 

1156 
finally show False by auto qed 

1157 

1158 
lemma integral_unique[intro]: 

1159 
"(f has_integral y) k \<Longrightarrow> integral k f = y" 

1160 
unfolding integral_def apply(rule some_equality) by(auto intro: has_integral_unique) 

1161 

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

1162 
lemma has_integral_is_0: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector" 
35172  1163 
assumes "\<forall>x\<in>s. f x = 0" shows "(f has_integral 0) s" 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1164 
proof have lem:"\<And>a b. \<And>f::'n \<Rightarrow> 'a. 
35172  1165 
(\<forall>x\<in>{a..b}. f(x) = 0) \<Longrightarrow> (f has_integral 0) ({a..b})" unfolding has_integral 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

1166 
proof(rule,rule) fix a b e and f::"'n \<Rightarrow> 'a" 
35172  1167 
assume as:"\<forall>x\<in>{a..b}. f x = 0" "0 < (e::real)" 
1168 
show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)  0) < e)" 

1169 
apply(rule_tac x="\<lambda>x. ball x 1" in exI) apply(rule,rule gaugeI) unfolding centre_in_ball defer apply(rule open_ball) 

1170 
proof(rule,rule,erule conjE) case goal1 

1171 
have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) = 0" proof(rule setsum_0',rule) 

1172 
fix x assume x:"x\<in>p" have "f (fst x) = 0" using tagged_division_ofD(23)[OF goal1(1), of "fst x" "snd x"] using as x by auto 

1173 
thus "(\<lambda>(x, k). content k *\<^sub>R f x) x = 0" apply(subst surjective_pairing[of x]) unfolding split_conv by auto 

1174 
qed thus ?case using as by auto 

1175 
qed auto qed { presume "\<not> (\<exists>a b. s = {a..b}) \<Longrightarrow> ?thesis" 

1176 
thus ?thesis applyapply(cases "\<exists>a b. s = {a..b}") 

1177 
using assms by(auto simp add:has_integral intro:lem) } 

1178 
have *:"(\<lambda>x. if x \<in> s then f x else 0) = (\<lambda>x. 0)" apply(rule ext) using assms by auto 

1179 
assume "\<not> (\<exists>a b. s = {a..b})" thus ?thesis apply(subst has_integral_alt) unfolding if_not_P * 

1180 
apply(rule,rule,rule_tac x=1 in exI,rule) defer apply(rule,rule,rule) 

1181 
proof fix e::real and a b assume "e>0" 

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

1182 
thus "\<exists>z. ((\<lambda>x::'n. 0::'a) has_integral z) {a..b} \<and> norm (z  0) < e" 
35172  1183 
apply(rule_tac x=0 in exI) apply(rule,rule lem) by auto 
1184 
qed auto qed 

1185 

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

1186 
lemma has_integral_0[simp]: "((\<lambda>x::'n::ordered_euclidean_space. 0) has_integral 0) s" 
35172  1187 
apply(rule has_integral_is_0) by auto 
1188 

1189 
lemma has_integral_0_eq[simp]: "((\<lambda>x. 0) has_integral i) s \<longleftrightarrow> i = 0" 

1190 
using has_integral_unique[OF has_integral_0] by auto 

1191 

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

1192 
lemma has_integral_linear: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector" 
35172  1193 
assumes "(f has_integral y) s" "bounded_linear h" shows "((h o f) has_integral ((h y))) s" 
1194 
proof interpret bounded_linear h using assms(2) . from pos_bounded guess B .. note B=conjunctD2[OF this,rule_format] 

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

1195 
have lem:"\<And>f::'n \<Rightarrow> 'a. \<And> y a b. 
35172  1196 
(f has_integral y) ({a..b}) \<Longrightarrow> ((h o f) has_integral h(y)) ({a..b})" 
1197 
proof(subst has_integral,rule,rule) case goal1 

1198 
from pos_bounded guess B .. note B=conjunctD2[OF this,rule_format] 

1199 
have *:"e / B > 0" apply(rule divide_pos_pos) using goal1(2) B by auto 

1200 
guess g using has_integralD[OF goal1(1) *] . note g=this 

1201 
show ?case apply(rule_tac x=g in exI) apply(rule,rule g(1)) 

1202 
proof(rule,rule,erule conjE) fix p assume as:"p tagged_division_of {a..b}" "g fine p" 

1203 
have *:"\<And>x k. h ((\<lambda>(x, k). content k *\<^sub>R f x) x) = (\<lambda>(x, k). h (content k *\<^sub>R f x)) x" by auto 

1204 
have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) = setsum (h \<circ> (\<lambda>(x, k). content k *\<^sub>R f x)) p" 

1205 
unfolding o_def unfolding scaleR[THEN sym] * by simp 

1206 
also have "\<dots> = h (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" using setsum[of "\<lambda>(x,k). content k *\<^sub>R f x" p] using as by auto 

1207 
finally have *:"(\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) = h (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" . 

1208 
show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x)  h y) < e" unfolding * diff[THEN sym] 

579dd5570f96
Added integration to MultivariateAnalysis (upto FTC)
h 