author  haftmann 
Sat, 25 May 2013 15:44:29 +0200  
changeset 52141  eff000cab70f 
parent 51642  400ec5ae7f8f 
child 53015  a1119cf551e8 
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 

51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

11 
lemma cSup_abs_le: (* TODO: is this really needed? *) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

12 
fixes S :: "real set" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

13 
shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

14 
by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

15 

6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

16 
lemma cInf_abs_ge: (* TODO: is this really needed? *) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

17 
fixes S :: "real set" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

18 
shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

19 
by (simp add: Inf_real_def) (rule cSup_abs_le, auto) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

20 

6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

21 
lemma cSup_asclose: (* TODO: is this really needed? *) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

22 
fixes S :: "real set" 
51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

23 
assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x  l\<bar> \<le> e" shows "\<bar>Sup S  l\<bar> \<le> e" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

24 
proof 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

25 
have th: "\<And>(x::real) l e. \<bar>x  l\<bar> \<le> e \<longleftrightarrow> l  e \<le> x \<and> x \<le> l + e" by arith 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

26 
thus ?thesis using S b cSup_bounds[of S "l  e" "l+e"] unfolding th 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

27 
by (auto simp add: setge_def setle_def) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

28 
qed 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

29 

6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

30 
lemma cInf_asclose: (* TODO: is this really needed? *) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

31 
fixes S :: "real set" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

32 
assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x  l\<bar> \<le> e" shows "\<bar>Inf S  l\<bar> \<le> e" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

33 
proof  
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

34 
have "\<bar> Sup (uminus ` S)  l\<bar> = \<bar>Sup (uminus ` S)  (l)\<bar>" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

35 
by auto 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

36 
also have "... \<le> e" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

37 
apply (rule cSup_asclose) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

38 
apply (auto simp add: S) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

39 
apply (metis abs_minus_add_cancel b add_commute diff_minus) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

40 
done 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

41 
finally have "\<bar> Sup (uminus ` S)  l\<bar> \<le> e" . 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

42 
thus ?thesis 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

43 
by (simp add: Inf_real_def) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

44 
qed 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

45 

6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

46 
lemma cSup_finite_ge_iff: 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

47 
fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Sup S \<longleftrightarrow> (\<exists>x\<in>S. a \<le> x)" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

48 
by (metis cSup_eq_Max Max_ge_iff) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

49 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

50 
lemma cSup_finite_le_iff: 
51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

51 
fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Sup S \<longleftrightarrow> (\<forall>x\<in>S. a \<ge> x)" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

52 
by (metis cSup_eq_Max Max_le_iff) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

53 

6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

54 
lemma cInf_finite_ge_iff: 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

55 
fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

56 
by (metis cInf_eq_Min Min_ge_iff) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

57 

6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

58 
lemma cInf_finite_le_iff: 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

59 
fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51489
diff
changeset

60 
by (metis cInf_eq_Min Min_le_iff) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

61 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

62 
lemma Inf: (* rename *) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

63 
fixes S :: "real set" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

64 
shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

65 
by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def intro: cInf_lower cInf_greatest) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

66 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

67 
lemma real_le_inf_subset: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

68 
assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. b <=* s" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

69 
shows "Inf s <= Inf (t::real set)" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

70 
apply (rule isGlb_le_isLb) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

71 
apply (rule Inf[OF assms(1)]) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

72 
apply (insert assms) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

73 
apply (erule exE) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

74 
apply (rule_tac x = b in exI) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

75 
apply (auto simp: isLb_def setge_def intro: cInf_lower cInf_greatest) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

76 
done 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

77 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

78 
lemma real_ge_sup_subset: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

79 
assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. s *<= b" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

80 
shows "Sup s >= Sup (t::real set)" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

81 
apply (rule isLub_le_isUb) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

82 
apply (rule isLub_cSup[OF assms(1)]) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

83 
apply (insert assms) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

84 
apply (erule exE) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

85 
apply (rule_tac x = b in exI) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

86 
apply (auto simp: isUb_def setle_def intro: cSup_upper cSup_least) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

87 
done 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

88 

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

89 
(*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

90 

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

91 
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

92 
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

93 
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

94 

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

95 
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

96 
"0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)" 
49675  97 
by (subst(asm) real_arch_inv) 
98 

99 

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

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

101 

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

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

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

106 

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

107 
declare norm_triangle_ineq4[intro] 
35172  108 

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

109 
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

110 

49970  111 
lemma linear_simps: 
112 
assumes "bounded_linear f" 

113 
shows 

114 
"f (a + b) = f a + f b" 

115 
"f (a  b) = f a  f b" 

116 
"f 0 = 0" 

117 
"f ( a) =  f a" 

118 
"f (s *\<^sub>R v) = s *\<^sub>R (f v)" 

119 
apply (rule_tac[!] additive.add additive.minus additive.diff additive.zero bounded_linear.scaleR) 

49675  120 
using assms unfolding bounded_linear_def additive_def 
121 
apply auto 

122 
done 

123 

124 
lemma bounded_linearI: 

125 
assumes "\<And>x y. f (x + y) = f x + f y" 

126 
and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x" "\<And>x. norm (f x) \<le> norm x * K" 

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

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

128 
unfolding bounded_linear_def additive_def bounded_linear_axioms_def using assms by auto 
51348  129 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

130 
lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

131 
by (rule bounded_linear_inner_left) 
36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

132 

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

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

134 
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

135 
shows "((\<forall>m. \<forall>n>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n)))" (is "?l = ?r") 
49675  136 
proof (safe) 
137 
assume ?r 

138 
fix n m :: nat 

139 
assume "m < n" 

140 
then show "R m n" 

141 
proof (induct n arbitrary: m) 

142 
case (Suc n) 

143 
show ?case 

144 
proof (cases "m < n") 

145 
case True 

146 
show ?thesis 

147 
apply (rule assms[OF Suc(1)[OF True]]) 

50945  148 
using `?r` 
149 
apply auto 

49675  150 
done 
151 
next 

152 
case False 

49970  153 
then have "m = n" using Suc(2) by auto 
154 
then show ?thesis using `?r` by auto 

49675  155 
qed 
156 
qed auto 

157 
qed auto 

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

158 

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

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

160 
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

161 
shows "\<forall>n>m. R m n" 
49675  162 
proof  
163 
have "\<forall>m. \<forall>n>m. R m n" 

164 
apply (subst transitive_stepwise_lt_eq) 

165 
apply (rule assms) 

166 
apply assumption 

167 
apply assumption 

168 
using assms(2) apply auto 

169 
done 

49970  170 
then show ?thesis by auto 
49675  171 
qed 
36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

172 

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

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

174 
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

175 
shows "(\<forall>m. \<forall>n\<ge>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n))" (is "?l = ?r") 
49675  176 
proof safe 
177 
assume ?r 

178 
fix m n :: nat 

179 
assume "m \<le> n" 

180 
thus "R m n" 

181 
proof (induct n arbitrary: m) 

49970  182 
case 0 
183 
with assms show ?case by auto 

184 
next 

49675  185 
case (Suc n) 
186 
show ?case 

187 
proof (cases "m \<le> n") 

188 
case True 

189 
show ?thesis 

190 
apply (rule assms(2)) 

191 
apply (rule Suc(1)[OF True]) 

192 
using `?r` apply auto 

193 
done 

194 
next 

195 
case False 

196 
hence "m = Suc n" using Suc(2) by auto 

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

197 
thus ?thesis using assms(1) by auto 
49675  198 
qed 
49970  199 
qed 
49675  200 
qed auto 
36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

201 

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

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

203 
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

204 
shows "\<forall>n\<ge>m. R m n" 
49675  205 
proof  
206 
have "\<forall>m. \<forall>n\<ge>m. R m n" 

207 
apply (subst transitive_stepwise_le_eq) 

208 
apply (rule assms) 

209 
apply (rule assms,assumption,assumption) 

210 
using assms(3) apply auto 

211 
done 

49970  212 
then show ?thesis by auto 
49675  213 
qed 
214 

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

215 

35172  216 
subsection {* Some useful lemmas about intervals. *} 
217 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

218 
abbreviation One where "One \<equiv> ((\<Sum>Basis)::_::euclidean_space)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

219 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

220 
lemma empty_as_interval: "{} = {One..(0::'a::ordered_euclidean_space)}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

221 
by (auto simp: set_eq_iff eucl_le[where 'a='a] intro!: bexI[OF _ SOME_Basis]) 
35172  222 

223 
lemma interior_subset_union_intervals: 

49675  224 
assumes "i = {a..b::'a::ordered_euclidean_space}" "j = {c..d}" 
225 
"interior j \<noteq> {}" "i \<subseteq> j \<union> s" "interior(i) \<inter> interior(j) = {}" 

226 
shows "interior i \<subseteq> interior s" 

227 
proof  

228 
have "{a<..<b} \<inter> {c..d} = {}" 

229 
using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5) 

35172  230 
unfolding assms(1,2) interior_closed_interval by auto 
49675  231 
moreover 
49970  232 
have "{a<..<b} \<subseteq> {c..d} \<union> s" 
233 
apply (rule order_trans,rule interval_open_subset_closed) 

234 
using assms(4) unfolding assms(1,2) 

235 
apply auto 

236 
done 

49675  237 
ultimately 
238 
show ?thesis 

239 
apply  

49970  240 
apply (rule interior_maximal) 
241 
defer 

49675  242 
apply (rule open_interior) 
49970  243 
unfolding assms(1,2) interior_closed_interval 
244 
apply auto 

49675  245 
done 
246 
qed 

247 

248 
lemma inter_interior_unions_intervals: 

249 
fixes f::"('a::ordered_euclidean_space) set set" 

35172  250 
assumes "finite f" "open s" "\<forall>t\<in>f. \<exists>a b. t = {a..b}" "\<forall>t\<in>f. s \<inter> (interior t) = {}" 
49675  251 
shows "s \<inter> interior(\<Union>f) = {}" 
49970  252 
proof (rule ccontr, unfold ex_in_conv[THEN sym]) 
253 
case goal1 

254 
have lem1: "\<And>x e s U. ball x e \<subseteq> s \<inter> interior U \<longleftrightarrow> ball x e \<subseteq> s \<inter> U" 

255 
apply rule 

256 
defer 

257 
apply (rule_tac Int_greatest) 

258 
unfolding open_subset_interior[OF open_ball] 

259 
using interior_subset 

260 
apply auto 

261 
done 

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

263 
have "\<And>f. finite f \<Longrightarrow> (\<forall>t\<in>f. \<exists>a b. t = {a..b}) \<Longrightarrow> 

264 
(\<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)" 

265 
proof  

266 
case goal1 

267 
then show ?case 

268 
proof (induct rule: finite_induct) 

269 
case empty from this(2) guess x .. 

270 
hence False unfolding Union_empty interior_empty by auto 

271 
thus ?case by auto 

272 
next 

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

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

275 
guess a using insert(4)[rule_format,OF insertI1] .. 

276 
then guess b .. note ab = this 

277 
show ?case 

278 
proof (cases "x\<in>i") 

279 
case False 

280 
hence "x \<in> UNIV  {a..b}" unfolding ab by auto 

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

282 
hence "0 < d" "ball x (min d e) \<subseteq> UNIV  i" unfolding ab ball_min_Int by auto 

283 
hence "ball x (min d e) \<subseteq> s \<inter> interior (\<Union>f)" 

284 
using e unfolding lem1 unfolding ball_min_Int by auto 

285 
hence "x \<in> s \<inter> interior (\<Union>f)" using `d>0` e by auto 

286 
hence "\<exists>t\<in>f. \<exists>x e. 0 < e \<and> ball x e \<subseteq> s \<inter> t" 

287 
apply  

288 
apply (rule insert(3)) 

289 
using insert(4) 

290 
apply auto 

291 
done 

292 
thus ?thesis by auto 

293 
next 

294 
case True show ?thesis 

295 
proof (cases "x\<in>{a<..<b}") 

296 
case True 

297 
then guess d unfolding open_contains_ball_eq[OF open_interval,rule_format] .. 

298 
thus ?thesis 

299 
apply (rule_tac x=i in bexI, rule_tac x=x in exI, rule_tac x="min d e" in exI) 

300 
unfolding ab 

50945  301 
using interval_open_subset_closed[of a b] and e 
302 
apply fastforce+ 

49970  303 
done 
304 
next 

305 
case False 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

306 
then obtain k where "x\<bullet>k \<le> a\<bullet>k \<or> x\<bullet>k \<ge> b\<bullet>k" and k:"k\<in>Basis" 
49970  307 
unfolding mem_interval by (auto simp add: not_less) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

308 
hence "x\<bullet>k = a\<bullet>k \<or> x\<bullet>k = b\<bullet>k" 
49970  309 
using True unfolding ab and mem_interval 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

310 
apply (erule_tac x = k in ballE) 
49970  311 
apply auto 
312 
done 

313 
hence "\<exists>x. ball x (e/2) \<subseteq> s \<inter> (\<Union>f)" 

314 
proof (erule_tac disjE) 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

315 
let ?z = "x  (e/2) *\<^sub>R k" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

316 
assume as: "x\<bullet>k = a\<bullet>k" 
49970  317 
have "ball ?z (e / 2) \<inter> i = {}" 
318 
apply (rule ccontr) 

319 
unfolding ex_in_conv[THEN sym] 

320 
proof (erule exE) 

321 
fix y 

322 
assume "y \<in> ball ?z (e / 2) \<inter> i" 

323 
hence "dist ?z y < e/2" and yi:"y\<in>i" by auto 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

324 
hence "\<bar>(?z  y) \<bullet> k\<bar> < e/2" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

325 
using Basis_le_norm[OF k, of "?z  y"] unfolding dist_norm by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

326 
hence "y\<bullet>k < a\<bullet>k" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

327 
using e[THEN conjunct1] k by (auto simp add: field_simps as inner_Basis inner_simps) 
49970  328 
hence "y \<notin> i" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

329 
unfolding ab mem_interval by (auto intro!: bexI[OF _ k]) 
49970  330 
thus False using yi by auto 
331 
qed 

332 
moreover 

333 
have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)" 

334 
apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) 

335 
proof 

336 
fix y 

337 
assume as: "y\<in> ball ?z (e/2)" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

338 
have "norm (x  y) \<le> \<bar>e\<bar> / 2 + norm (x  y  (e / 2) *\<^sub>R k)" 
49970  339 
apply  
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

340 
apply (rule order_trans,rule norm_triangle_sub[of "x  y" "(e/2) *\<^sub>R k"]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

341 
unfolding norm_scaleR norm_Basis[OF k] 
49970  342 
apply auto 
343 
done 

344 
also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2" 

345 
apply (rule add_strict_left_mono) 

50945  346 
using as 
347 
unfolding mem_ball dist_norm 

348 
using e 

349 
apply (auto simp add: field_simps) 

49970  350 
done 
351 
finally show "y\<in>ball x e" 

352 
unfolding mem_ball dist_norm using e by (auto simp add:field_simps) 

353 
qed 

354 
ultimately show ?thesis 

355 
apply (rule_tac x="?z" in exI) 

356 
unfolding Union_insert 

357 
apply auto 

358 
done 

359 
next 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

360 
let ?z = "x + (e/2) *\<^sub>R k" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

361 
assume as: "x\<bullet>k = b\<bullet>k" 
49970  362 
have "ball ?z (e / 2) \<inter> i = {}" 
363 
apply (rule ccontr) 

364 
unfolding ex_in_conv[THEN sym] 

365 
proof(erule exE) 

366 
fix y 

367 
assume "y \<in> ball ?z (e / 2) \<inter> i" 

368 
hence "dist ?z y < e/2" and yi:"y\<in>i" by auto 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

369 
hence "\<bar>(?z  y) \<bullet> k\<bar> < e/2" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

370 
using Basis_le_norm[OF k, of "?z  y"] unfolding dist_norm by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

371 
hence "y\<bullet>k > b\<bullet>k" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

372 
using e[THEN conjunct1] k by(auto simp add:field_simps inner_simps inner_Basis as) 
49970  373 
hence "y \<notin> i" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

374 
unfolding ab mem_interval by (auto intro!: bexI[OF _ k]) 
49970  375 
thus False using yi by auto 
376 
qed 

377 
moreover 

378 
have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)" 

379 
apply (rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) 

380 
proof 

381 
fix y 

382 
assume as: "y\<in> ball ?z (e/2)" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

383 
have "norm (x  y) \<le> \<bar>e\<bar> / 2 + norm (x  y + (e / 2) *\<^sub>R k)" 
49970  384 
apply  
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

385 
apply(rule order_trans,rule norm_triangle_sub[of "x  y" " (e/2) *\<^sub>R k"]) 
49970  386 
unfolding norm_scaleR 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

387 
apply (auto simp: k) 
49970  388 
done 
389 
also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2" 

390 
apply (rule add_strict_left_mono) 

391 
using as unfolding mem_ball dist_norm 

392 
using e apply (auto simp add: field_simps) 

393 
done 

394 
finally show "y\<in>ball x e" 

395 
unfolding mem_ball dist_norm using e by(auto simp add:field_simps) 

396 
qed 

397 
ultimately show ?thesis 

398 
apply (rule_tac x="?z" in exI) 

399 
unfolding Union_insert 

400 
apply auto 

401 
done 

402 
qed 

403 
then guess x .. 

404 
hence "x \<in> s \<inter> interior (\<Union>f)" 

405 
unfolding lem1[where U="\<Union>f",THEN sym] 

406 
using centre_in_ball e[THEN conjunct1] by auto 

407 
thus ?thesis 

408 
apply  

409 
apply (rule lem2, rule insert(3)) 

410 
using insert(4) apply auto 

411 
done 

412 
qed 

413 
qed 

414 
qed 

415 
qed 

416 
note * = this 

417 
guess t using *[OF assms(1,3) goal1] .. 

418 
from this(2) guess x .. 

419 
then guess e .. 

420 
hence "x \<in> s" "x\<in>interior t" 

421 
defer 

422 
using open_subset_interior[OF open_ball, of x e t] apply auto 

423 
done 

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

425 
qed 

426 

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

427 

35172  428 
subsection {* Bounds on intervals where they exist. *} 
429 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

430 
definition interval_upperbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a" where 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

431 
"interval_upperbound s = (\<Sum>i\<in>Basis. Sup {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

432 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

433 
definition interval_lowerbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a" where 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

434 
"interval_lowerbound s = (\<Sum>i\<in>Basis. Inf {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)" 
49970  435 

436 
lemma interval_upperbound[simp]: 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

437 
"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

438 
interval_upperbound {a..b} = (b::'a::ordered_euclidean_space)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

439 
unfolding interval_upperbound_def euclidean_representation_setsum 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

440 
by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setle_def 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

441 
intro!: cSup_unique) 
49970  442 

443 
lemma interval_lowerbound[simp]: 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

444 
"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

445 
interval_lowerbound {a..b} = (a::'a::ordered_euclidean_space)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

446 
unfolding interval_lowerbound_def euclidean_representation_setsum 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

447 
by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setge_def 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
51348
diff
changeset

448 
intro!: cInf_unique) 
35172  449 

450 
lemmas interval_bounds = interval_upperbound interval_lowerbound 

451 

49970  452 
lemma interval_bounds'[simp]: 
453 
assumes "{a..b}\<noteq>{}" 

454 
shows "interval_upperbound {a..b} = b" "interval_lowerbound {a..b} = a" 

35172  455 
using assms unfolding interval_ne_empty by auto 
456 

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

458 

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

459 
definition "content (s::('a::ordered_euclidean_space) set) = 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

460 
(if s = {} then 0 else (\<Prod>i\<in>Basis. (interval_upperbound s)\<bullet>i  (interval_lowerbound s)\<bullet>i))" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

461 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

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

463 
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

464 

49970  465 
lemma content_closed_interval: 
466 
fixes a::"'a::ordered_euclidean_space" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

467 
assumes "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

468 
shows "content {a..b} = (\<Prod>i\<in>Basis. b\<bullet>i  a\<bullet>i)" 
49970  469 
using interval_not_empty[OF assms] 
470 
unfolding content_def interval_upperbound[OF assms] interval_lowerbound[OF assms] 

471 
by auto 

472 

473 
lemma content_closed_interval': 

474 
fixes a::"'a::ordered_euclidean_space" 

475 
assumes "{a..b}\<noteq>{}" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

476 
shows "content {a..b} = (\<Prod>i\<in>Basis. b\<bullet>i  a\<bullet>i)" 
49970  477 
apply (rule content_closed_interval) 
50945  478 
using assms 
479 
unfolding interval_ne_empty 

49970  480 
apply assumption 
481 
done 

482 

483 
lemma content_real: 

484 
assumes "a\<le>b" 

485 
shows "content {a..b} = ba" 

486 
proof  

487 
have *: "{..<Suc 0} = {0}" by auto 

488 
show ?thesis unfolding content_def using assms by (auto simp: *) 

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

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

490 

50104  491 
lemma content_singleton[simp]: "content {a} = 0" 
492 
proof  

493 
have "content {a .. a} = 0" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

494 
by (subst content_closed_interval) (auto simp: ex_in_conv) 
50104  495 
then show ?thesis by simp 
496 
qed 

497 

49970  498 
lemma content_unit[intro]: "content{0..One::'a::ordered_euclidean_space} = 1" 
499 
proof  

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

500 
have *: "\<forall>i\<in>Basis. (0::'a)\<bullet>i \<le> (One::'a)\<bullet>i" 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

501 
have "0 \<in> {0..One::'a}" unfolding mem_interval by auto 
49970  502 
thus ?thesis unfolding content_def interval_bounds[OF *] using setprod_1 by auto 
503 
qed 

504 

505 
lemma content_pos_le[intro]: 

506 
fixes a::"'a::ordered_euclidean_space" 

507 
shows "0 \<le> content {a..b}" 

508 
proof (cases "{a..b} = {}") 

509 
case False 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

510 
hence *: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i" unfolding interval_ne_empty . 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

511 
have "(\<Prod>i\<in>Basis. interval_upperbound {a..b} \<bullet> i  interval_lowerbound {a..b} \<bullet> i) \<ge> 0" 
49970  512 
apply (rule setprod_nonneg) 
513 
unfolding interval_bounds[OF *] 

514 
using * 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

515 
apply (erule_tac x=x in ballE) 
49970  516 
apply auto 
517 
done 

518 
thus ?thesis unfolding content_def by (auto simp del:interval_bounds') 

519 
qed (unfold content_def, auto) 

520 

521 
lemma content_pos_lt: 

522 
fixes a::"'a::ordered_euclidean_space" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

523 
assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" 
49970  524 
shows "0 < content {a..b}" 
525 
proof  

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

526 
have help_lemma1: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i \<Longrightarrow> \<forall>i\<in>Basis. a\<bullet>i \<le> ((b\<bullet>i)::real)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

527 
apply (rule, erule_tac x=i in ballE) 
49970  528 
apply auto 
529 
done 

530 
show ?thesis unfolding content_closed_interval[OF help_lemma1[OF assms]] 

531 
apply(rule setprod_pos) 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

532 
using assms apply (erule_tac x=x in ballE) 
49970  533 
apply auto 
534 
done 

535 
qed 

536 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

537 
lemma content_eq_0: "content{a..b::'a::ordered_euclidean_space} = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)" 
49970  538 
proof (cases "{a..b} = {}") 
539 
case True 

540 
thus ?thesis 

541 
unfolding content_def if_P[OF True] 

542 
unfolding interval_eq_empty 

543 
apply  

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

544 
apply (rule, erule bexE) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

545 
apply (rule_tac x = i in bexI) 
49970  546 
apply auto 
547 
done 

548 
next 

549 
case False 

550 
from this[unfolded interval_eq_empty not_ex not_less] 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

551 
have as: "\<forall>i\<in>Basis. b \<bullet> i \<ge> a \<bullet> i" by fastforce 
49970  552 
show ?thesis 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

553 
unfolding content_def if_not_P[OF False] setprod_zero_iff[OF finite_Basis] 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

554 
using as 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

555 
by (auto intro!: bexI) 
49970  556 
qed 
35172  557 

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

559 

560 
lemma content_closed_interval_cases: 

49970  561 
"content {a..b::'a::ordered_euclidean_space} = 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

562 
(if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i  a\<bullet>i) Basis else 0)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

563 
by (auto simp: not_le content_eq_0 intro: less_imp_le content_closed_interval) 
35172  564 

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

566 
unfolding content_eq_0 interior_closed_interval interval_eq_empty by auto 

567 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

568 
lemma content_pos_lt_eq: "0 < content {a..b::'a::ordered_euclidean_space} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)" 
49970  569 
apply rule 
570 
defer 

571 
apply (rule content_pos_lt, assumption) 

572 
proof  

573 
assume "0 < content {a..b}" 

574 
hence "content {a..b} \<noteq> 0" by auto 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

575 
thus "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" 
49970  576 
unfolding content_eq_0 not_ex not_le by fastforce 
577 
qed 

578 

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

35172  580 

49698  581 
lemma content_subset: 
582 
assumes "{a..b} \<subseteq> {c..d}" 

583 
shows "content {a..b::'a::ordered_euclidean_space} \<le> content {c..d}" 

584 
proof (cases "{a..b} = {}") 

585 
case True 

586 
thus ?thesis using content_pos_le[of c d] by auto 

587 
next 

588 
case False 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

589 
hence ab_ne:"\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i" unfolding interval_ne_empty by auto 
35172  590 
hence ab_ab:"a\<in>{a..b}" "b\<in>{a..b}" unfolding mem_interval by auto 
591 
have "{c..d} \<noteq> {}" using assms False by auto 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

592 
hence cd_ne:"\<forall>i\<in>Basis. c \<bullet> i \<le> d \<bullet> i" using assms unfolding interval_ne_empty by auto 
49698  593 
show ?thesis 
594 
unfolding content_def 

595 
unfolding interval_bounds[OF ab_ne] interval_bounds[OF cd_ne] 

596 
unfolding if_not_P[OF False] if_not_P[OF `{c..d} \<noteq> {}`] 

50945  597 
apply (rule setprod_mono, rule) 
49698  598 
proof 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

599 
fix i :: 'a 
50945  600 
assume i: "i\<in>Basis" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

601 
show "0 \<le> b \<bullet> i  a \<bullet> i" using ab_ne[THEN bspec, OF i] i by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

602 
show "b \<bullet> i  a \<bullet> i \<le> d \<bullet> i  c \<bullet> i" 
35172  603 
using assms[unfolded subset_eq mem_interval,rule_format,OF ab_ab(2),of i] 
49698  604 
using assms[unfolded subset_eq mem_interval,rule_format,OF ab_ab(1),of i] 
605 
using i by auto 

606 
qed 

607 
qed 

35172  608 

609 
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

610 
unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce 
35172  611 

49698  612 

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

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

616 

49698  617 
lemma gaugeI: assumes "\<And>x. x\<in>g x" "\<And>x. open (g x)" shows "gauge g" 
35172  618 
using assms unfolding gauge_def by auto 
619 

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

35172  622 

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

624 
unfolding gauge_def by auto 

625 

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

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

35172  630 

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

49698  634 
lemma gauge_inters: 
635 
assumes "finite s" "\<forall>d\<in>s. gauge (f d)" 

636 
shows "gauge(\<lambda>x. \<Inter> {f d x  d. d \<in> s})" 

637 
proof  

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

639 
show ?thesis 

640 
unfolding gauge_def unfolding * 

641 
using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto 

642 
qed 

643 

644 
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)" 

645 
by(meson zero_less_one) 

646 

35172  647 

648 
subsection {* Divisions. *} 

649 

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

651 
"s division_of i \<equiv> 

652 
finite s \<and> 

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

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

655 
(\<Union>s = i)" 

656 

49698  657 
lemma division_ofD[dest]: 
658 
assumes "s division_of i" 

659 
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})" 

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

661 
using assms unfolding division_of_def by auto 

35172  662 

663 
lemma division_ofI: 

664 
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})" 

49698  665 
"\<And>k1 k2. \<lbrakk>k1\<in>s; k2\<in>s; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}" "\<Union>s = i" 
35172  666 
shows "s division_of i" using assms unfolding division_of_def by auto 
667 

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

669 
unfolding division_of_def by auto 

670 

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

672 
unfolding division_of_def by auto 

673 

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

675 

49698  676 
lemma division_of_sing[simp]: 
677 
"s division_of {a..a::'a::ordered_euclidean_space} \<longleftrightarrow> s = {{a..a}}" (is "?l = ?r") 

678 
proof 

679 
assume ?r 

680 
moreover { 

681 
assume "s = {{a}}" 

682 
moreover fix k assume "k\<in>s" 

683 
ultimately have"\<exists>x y. k = {x..y}" 

50945  684 
apply (rule_tac x=a in exI)+ 
685 
unfolding interval_sing 

686 
apply auto 

687 
done 

49698  688 
} 
689 
ultimately show ?l unfolding division_of_def interval_sing by auto 

690 
next 

691 
assume ?l 

692 
note as=conjunctD4[OF this[unfolded division_of_def interval_sing]] 

35172  693 
{ fix x assume x:"x\<in>s" have "x={a}" using as(2)[rule_format,OF x] by auto } 
49698  694 
moreover have "s \<noteq> {}" using as(4) by auto 
695 
ultimately show ?r unfolding interval_sing by auto 

696 
qed 

35172  697 

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

699 
unfolding division_of_trivial by auto 

700 

49698  701 
lemma elementary_interval: obtains p where "p division_of {a..b}" 
702 
by (metis division_of_trivial division_of_self) 

35172  703 

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

705 
unfolding division_of_def by auto 

706 

707 
lemma forall_in_division: 

708 
"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

709 
unfolding division_of_def by fastforce 
35172  710 

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

49698  712 
apply (rule division_ofI) 
713 
proof  

714 
note as=division_ofD[OF assms(1)] 

715 
show "finite q" 

716 
apply (rule finite_subset) 

717 
using as(1) assms(2) apply auto 

718 
done 

719 
{ fix k 

720 
assume "k \<in> q" 

721 
hence kp:"k\<in>p" using assms(2) by auto 

722 
show "k\<subseteq>\<Union>q" using `k \<in> q` by auto 

723 
show "\<exists>a b. k = {a..b}" using as(4)[OF kp] 

724 
by auto show "k \<noteq> {}" using as(3)[OF kp] by auto } 

725 
fix k1 k2 

726 
assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2" 

727 
hence *: "k1\<in>p" "k2\<in>p" "k1\<noteq>k2" using assms(2) by auto 

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

729 
qed auto 

730 

731 
lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)" 

732 
unfolding division_of_def by auto 

35172  733 

49970  734 
lemma division_of_content_0: 
735 
assumes "content {a..b} = 0" "d division_of {a..b}" 

736 
shows "\<forall>k\<in>d. content k = 0" 

737 
unfolding forall_in_division[OF assms(2)] 

50945  738 
apply (rule,rule,rule) 
739 
apply (drule division_ofD(2)[OF assms(2)]) 

740 
apply (drule content_subset) unfolding assms(1) 

49970  741 
proof  
742 
case goal1 

743 
thus ?case using content_pos_le[of a b] by auto 

744 
qed 

745 

746 
lemma division_inter: 

747 
assumes "p1 division_of s1" "p2 division_of (s2::('a::ordered_euclidean_space) set)" 

748 
shows "{k1 \<inter> k2  k1 k2 .k1 \<in> p1 \<and> k2 \<in> p2 \<and> k1 \<inter> k2 \<noteq> {}} division_of (s1 \<inter> s2)" 

749 
(is "?A' division_of _") 

750 
proof  

751 
let ?A = "{s. s \<in> (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}" 

752 
have *:"?A' = ?A" by auto 

753 
show ?thesis unfolding * 

754 
proof (rule division_ofI) 

755 
have "?A \<subseteq> (\<lambda>(x, y). x \<inter> y) ` (p1 \<times> p2)" by auto 

756 
moreover have "finite (p1 \<times> p2)" using assms unfolding division_of_def by auto 

757 
ultimately show "finite ?A" by auto 

758 
have *:"\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s" by auto 

759 
show "\<Union>?A = s1 \<inter> s2" 

760 
apply (rule set_eqI) 

761 
unfolding * and Union_image_eq UN_iff 

762 
using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] 

763 
apply auto 

764 
done 

765 
{ fix k 

766 
assume "k\<in>?A" 

767 
then obtain k1 k2 where k: "k = k1 \<inter> k2" "k1\<in>p1" "k2\<in>p2" "k\<noteq>{}" by auto 

768 
thus "k \<noteq> {}" by auto 

769 
show "k \<subseteq> s1 \<inter> s2" 

770 
using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)] 

771 
unfolding k by auto 

772 
guess a1 using division_ofD(4)[OF assms(1) k(2)] .. 

773 
then guess b1 .. note ab1=this 

774 
guess a2 using division_ofD(4)[OF assms(2) k(3)] .. 

775 
then guess b2 .. note ab2=this 

776 
show "\<exists>a b. k = {a..b}" 

777 
unfolding k ab1 ab2 unfolding inter_interval by auto } 

778 
fix k1 k2 

779 
assume "k1\<in>?A" 

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

781 
assume "k2\<in>?A" 

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

783 
assume "k1 \<noteq> k2" 

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

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

35172  786 
interior(x1 \<inter> y1) \<subseteq> interior(x1) \<Longrightarrow> interior(x1 \<inter> y1) \<subseteq> interior(y1) \<Longrightarrow> 
787 
interior(x2 \<inter> y2) \<subseteq> interior(x2) \<Longrightarrow> interior(x2 \<inter> y2) \<subseteq> interior(y2) 

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

49970  789 
show "interior k1 \<inter> interior k2 = {}" 
790 
unfolding k1 k2 

791 
apply (rule *) 

792 
defer 

793 
apply (rule_tac[14] interior_mono) 

794 
using division_ofD(5)[OF assms(1) k1(2) k2(2)] 

795 
using division_ofD(5)[OF assms(2) k1(3) k2(3)] 

796 
using th apply auto done 

797 
qed 

798 
qed 

799 

800 
lemma division_inter_1: 

801 
assumes "d division_of i" "{a..b::'a::ordered_euclidean_space} \<subseteq> i" 

802 
shows "{ {a..b} \<inter> k k. k \<in> d \<and> {a..b} \<inter> k \<noteq> {} } division_of {a..b}" 

803 
proof (cases "{a..b} = {}") 

804 
case True 

805 
show ?thesis unfolding True and division_of_trivial by auto 

806 
next 

807 
case False 

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

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

810 
qed 

811 

812 
lemma elementary_inter: 

813 
assumes "p1 division_of s" "p2 division_of (t::('a::ordered_euclidean_space) set)" 

35172  814 
shows "\<exists>p. p division_of (s \<inter> t)" 
50945  815 
apply rule 
816 
apply (rule division_inter[OF assms]) 

817 
done 

49970  818 

819 
lemma elementary_inters: 

820 
assumes "finite f" "f\<noteq>{}" "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::ordered_euclidean_space) set)" 

821 
shows "\<exists>p. p division_of (\<Inter> f)" 

822 
using assms 

823 
proof (induct f rule: finite_induct) 

824 
case (insert x f) 

825 
show ?case 

826 
proof (cases "f = {}") 

827 
case True 

828 
thus ?thesis unfolding True using insert by auto 

829 
next 

830 
case False 

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

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

833 
ultimately show ?thesis 

834 
unfolding Inter_insert 

835 
apply (rule_tac elementary_inter) 

836 
apply assumption 

837 
apply assumption 

838 
done 

839 
qed 

840 
qed auto 

35172  841 

842 
lemma division_disjoint_union: 

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

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

35172  846 
note d1 = division_ofD[OF assms(1)] and d2 = division_ofD[OF assms(2)] 
847 
show "finite (p1 \<union> p2)" using d1(1) d2(1) by auto 

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

50945  849 
{ 
850 
fix k1 k2 

851 
assume as: "k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2" 

852 
moreover 

853 
let ?g="interior k1 \<inter> interior k2 = {}" 

854 
{ 

855 
assume as: "k1\<in>p1" "k2\<in>p2" 

856 
have ?g 

857 
using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]] 

858 
using assms(3) by blast 

859 
} 

860 
moreover 

861 
{ 

862 
assume as: "k1\<in>p2" "k2\<in>p1" 

863 
have ?g 

864 
using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]] 

865 
using assms(3) by blast 

866 
} 

867 
ultimately show ?g using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto 

868 
} 

869 
fix k 

870 
assume k: "k \<in> p1 \<union> p2" 

871 
show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto 

872 
show "k \<noteq> {}" using k d1(3) d2(3) by auto 

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

874 
qed 

35172  875 

876 
lemma partial_division_extend_1: 

50945  877 
assumes incl: "{c..d} \<subseteq> {a..b::'a::ordered_euclidean_space}" 
878 
and nonempty: "{c..d} \<noteq> {}" 

35172  879 
obtains p where "p division_of {a..b}" "{c..d} \<in> p" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

880 
proof 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

881 
let ?B = "\<lambda>f::'a\<Rightarrow>'a \<times> 'a. {(\<Sum>i\<in>Basis. (fst (f i) \<bullet> i) *\<^sub>R i) .. (\<Sum>i\<in>Basis. (snd (f i) \<bullet> i) *\<^sub>R i)}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

882 
def p \<equiv> "?B ` (Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)})" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

883 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

884 
show "{c .. d} \<in> p" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

885 
unfolding p_def 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

886 
by (auto simp add: interval_eq_empty eucl_le[where 'a='a] 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

887 
intro!: image_eqI[where x="\<lambda>(i::'a)\<in>Basis. (c, d)"]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

888 

50945  889 
{ 
890 
fix i :: 'a 

891 
assume "i \<in> Basis" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

892 
with incl nonempty have "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> d \<bullet> i" "d \<bullet> i \<le> b \<bullet> i" 
50945  893 
unfolding interval_eq_empty subset_interval by (auto simp: not_le) 
894 
} 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

895 
note ord = this 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

896 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

897 
show "p division_of {a..b}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

898 
proof (rule division_ofI) 
50945  899 
show "finite p" unfolding p_def by (auto intro!: finite_PiE) 
900 
{ 

901 
fix k 

902 
assume "k \<in> p" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

903 
then obtain f where f: "f \<in> Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

904 
by (auto simp: p_def) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

905 
then show "\<exists>a b. k = {a..b}" by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

906 
have "k \<subseteq> {a..b} \<and> k \<noteq> {}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

907 
proof (simp add: k interval_eq_empty subset_interval not_less, safe) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

908 
fix i :: 'a assume i: "i \<in> Basis" 
50945  909 
moreover 
910 
with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

911 
by (auto simp: PiE_iff) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

912 
moreover note ord[of i] 
50945  913 
ultimately 
914 
show "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

915 
by (auto simp: subset_iff eucl_le[where 'a='a]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

916 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

917 
then show "k \<noteq> {}" "k \<subseteq> {a .. b}" by auto 
50945  918 
{ 
919 
fix l assume "l \<in> p" 

920 
then obtain g where g: "g \<in> Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g" 

921 
by (auto simp: p_def) 

922 
assume "l \<noteq> k" 

923 
have "\<exists>i\<in>Basis. f i \<noteq> g i" 

924 
proof (rule ccontr) 

925 
assume "\<not> (\<exists>i\<in>Basis. f i \<noteq> g i)" 

926 
with f g have "f = g" 

927 
by (auto simp: PiE_iff extensional_def intro!: ext) 

928 
with `l \<noteq> k` show False 

929 
by (simp add: l k) 

930 
qed 

931 
then guess i .. note * = this 

932 
moreover from * have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)" 

933 
"g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)" 

934 
using f g by (auto simp: PiE_iff) 

935 
moreover note ord[of i] 

936 
ultimately show "interior l \<inter> interior k = {}" 

937 
by (auto simp add: l k interior_closed_interval disjoint_interval intro!: bexI[of _ i]) 

938 
} 

939 
note `k \<subseteq> { a.. b}` 

940 
} 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

941 
moreover 
50945  942 
{ 
943 
fix x assume x: "x \<in> {a .. b}" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

944 
have "\<forall>i\<in>Basis. \<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

945 
proof 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

946 
fix i :: 'a assume "i \<in> Basis" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

947 
with x ord[of i] 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

948 
have "(a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> c \<bullet> i) \<or> (c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i) \<or> 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

949 
(d \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

950 
by (auto simp: eucl_le[where 'a='a]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

951 
then show "\<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

952 
by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

953 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

954 
then guess f unfolding bchoice_iff .. note f = this 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

955 
moreover then have "restrict f Basis \<in> Basis \<rightarrow>\<^isub>E {(a, c), (c, d), (d, b)}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

956 
by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

957 
moreover from f have "x \<in> ?B (restrict f Basis)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

958 
by (auto simp: mem_interval eucl_le[where 'a='a]) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

959 
ultimately have "\<exists>k\<in>p. x \<in> k" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

960 
unfolding p_def by blast } 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

961 
ultimately show "\<Union>p = {a..b}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

962 
by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

963 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

964 
qed 
35172  965 

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

968 
obtains q where "p \<subseteq> q" "q division_of {a..b::'a::ordered_euclidean_space}" 

969 
proof (cases "p = {}") 

970 
case True 

971 
guess q apply (rule elementary_interval[of a b]) . 

972 
thus ?thesis 

973 
apply  

974 
apply (rule that[of q]) 

975 
unfolding True 

976 
apply auto 

977 
done 

978 
next 

979 
case False 

980 
note p = division_ofD[OF assms(1)] 

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

982 
proof 

983 
case goal1 

984 
guess c using p(4)[OF goal1] .. 

985 
then guess d .. note "cd" = this 

986 
have *: "{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}" 

987 
using p(2,3)[OF goal1, unfolded "cd"] using assms(2) by auto 

988 
guess q apply(rule partial_division_extend_1[OF *]) . 

989 
thus ?case unfolding "cd" by auto 

990 
qed 

35172  991 
guess q using bchoice[OF *] .. note q = conjunctD2[OF this[rule_format]] 
50945  992 
have "\<And>x. x\<in>p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x  {x})" 
993 
apply (rule, rule_tac p="q x" in division_of_subset) 

994 
proof  

995 
fix x 

996 
assume x: "x\<in>p" 

997 
show "q x division_of \<Union>q x" 

998 
apply  

999 
apply (rule division_ofI) 

1000 
using division_ofD[OF q(1)[OF x]] 

1001 
apply auto 

1002 
done 

1003 
show "q x  {x} \<subseteq> q x" by auto 

1004 
qed 

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

1006 
apply  

1007 
apply (rule elementary_inters) 

1008 
apply (rule finite_imageI[OF p(1)]) 

1009 
unfolding image_is_empty 

1010 
apply (rule False) 

1011 
apply auto 

1012 
done 

35172  1013 
then guess d .. note d = this 
50945  1014 
show ?thesis 
1015 
apply (rule that[of "d \<union> p"]) 

1016 
proof  

1017 
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 

52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51642
diff
changeset

1018 
have *: "{a..b} = \<Inter> ((\<lambda>i. \<Union>(q i  {i})) ` p) \<union> \<Union>p" 
50945  1019 
apply (rule *[OF False]) 
1020 
proof 

1021 
fix i 

1022 
assume i: "i\<in>p" 

1023 
show "\<Union>(q i  {i}) \<union> i = {a..b}" 

1024 
using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto 

1025 
qed 

1026 
show "d \<union> p division_of {a..b}" 

1027 
unfolding * 

1028 
apply (rule division_disjoint_union[OF d assms(1)]) 

1029 
apply (rule inter_interior_unions_intervals) 

1030 
apply (rule p open_interior ballI)+ 

1031 
proof (assumption, rule) 

1032 
fix k 

1033 
assume k: "k\<in>p" 

1034 
have *: "\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}" by auto 

52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51642
diff
changeset

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

1038 
apply (subst Int_commute) 

1039 
apply (rule inter_interior_unions_intervals) 

1040 
proof  

1041 
note qk=division_ofD[OF q(1)[OF k]] 

1042 
show "finite (q k  {k})" "open (interior k)" 

1043 
"\<forall>t\<in>q k  {k}. \<exists>a b. t = {a..b}" using qk by auto 

1044 
show "\<forall>t\<in>q k  {k}. interior k \<inter> interior t = {}" 

1045 
using qk(5) using q(2)[OF k] by auto 

1046 
have *: "\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto 

52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51642
diff
changeset

1047 
show "interior (\<Inter> ((\<lambda>i. \<Union>(q i  {i})) ` p)) \<subseteq> interior (\<Union>(q k  {k}))" 
50945  1048 
apply (rule interior_mono *)+ 
1049 
using k by auto 

1050 
qed 

1051 
qed 

1052 
qed auto 

1053 
qed 

35172  1054 

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

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

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

1058 
lemma elementary_subset_interval: "p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> {a..b::'a::ordered_euclidean_space}" 
50945  1059 
by (meson elementary_bounded bounded_subset_closed_interval) 
1060 

1061 
lemma division_union_intervals_exists: 

1062 
assumes "{a..b::'a::ordered_euclidean_space} \<noteq> {}" 

1063 
obtains p where "(insert {a..b} p) division_of ({a..b} \<union> {c..d})" 

1064 
proof (cases "{c..d} = {}") 

1065 
case True 

1066 
show ?thesis 

1067 
apply (rule that[of "{}"]) 

1068 
unfolding True 

1069 
using assms 

1070 
apply auto 

1071 
done 

1072 
next 

1073 
case False 

1074 
note false=this 

1075 
show ?thesis 

1076 
proof (cases "{a..b} \<inter> {c..d} = {}") 

1077 
case True 

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

1079 
show ?thesis 

1080 
apply (rule that[of "{{c..d}}"]) 

1081 
unfolding * 

1082 
apply (rule division_disjoint_union) 

1083 
using false True assms 

1084 
using interior_subset 

1085 
apply auto 

1086 
done 

1087 
next 

1088 
case False 

1089 
obtain u v where uv: "{a..b} \<inter> {c..d} = {u..v}" 

1090 
unfolding inter_interval by auto 

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

1092 
guess p apply (rule partial_division_extend_1[OF * False[unfolded uv]]) . 

1093 
note p=this division_ofD[OF this(1)] 

1094 
have *: "{a..b} \<union> {c..d} = {a..b} \<union> \<Union>(p  {{u..v}})" "\<And>x s. insert x s = {x} \<union> s" 

1095 
using p(8) unfolding uv[THEN sym] by auto 

1096 
show ?thesis 

1097 
apply (rule that[of "p  {{u..v}}"]) 

1098 
unfolding *(1) 

1099 
apply (subst *(2)) 

1100 
apply (rule division_disjoint_union) 

1101 
apply (rule, rule assms) 

1102 
apply (rule division_of_subset[of p]) 

1103 
apply (rule division_of_union_self[OF p(1)]) 

1104 
defer 

1105 
unfolding interior_inter[THEN sym] 

1106 
proof  

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

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

1109 
apply (rule arg_cong[of _ _ interior]) 

1110 
apply (rule *[OF _ uv]) 

1111 
using p(8) 

1112 
apply auto 

1113 
done 

1114 
also have "\<dots> = {}" 

1115 
unfolding interior_inter 

1116 
apply (rule inter_interior_unions_intervals) 

1117 
using p(6) p(7)[OF p(2)] p(3) 

1118 
apply auto 

1119 
done 

1120 
finally show "interior ({a..b} \<inter> \<Union>(p  {{u..v}})) = {}" . 

1121 
qed auto 

1122 
qed 

1123 
qed 

35172  1124 

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

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

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

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

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

1130 

1131 
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

1132 
obtains q where "q division_of ({a..b::'a::ordered_euclidean_space} \<union> \<Union>p)" proof 
35172  1133 
note assm=division_ofD[OF assms] 
52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51642
diff
changeset

1134 
have lem1:"\<And>f s. \<Union>\<Union> (f ` s) = \<Union>((\<lambda>x.\<Union>(f x)) ` s)" by auto 
35172  1135 
have lem2:"\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t t. t \<in> f} = s \<union> \<Union>f" by auto 
1136 
{ presume "p={} \<Longrightarrow> thesis" "{a..b} = {} \<Longrightarrow> thesis" "{a..b} \<noteq> {} \<Longrightarrow> interior {a..b} = {} \<Longrightarrow> thesis" 

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

1138 
thus thesis by auto 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1156 
using q(6) by auto 

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

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

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

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

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

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

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

1164 
next case False 

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

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

1167 
thus ?thesis by auto } 

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

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

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

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

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

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

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

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

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

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

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

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

1180 
qed qed } qed 

1181 

1182 
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

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

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

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

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

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

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

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

1192 
unfolding Union_insert ab * by auto 

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

1194 

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 
lemma elementary_union: assumes "ps division_of s" "pt division_of (t::('a::ordered_euclidean_space) set)" 
35172  1196 
obtains p where "p division_of (s \<union> t)" 
1197 
proof have "s \<union> t = \<Union>ps \<union> \<Union>pt" using assms unfolding division_of_def by auto 

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

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

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

1201 
using assms[unfolded division_of_def] by auto qed 

1202 

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

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

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

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

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

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

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

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

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

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

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

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

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

1217 
thus False using x by auto qed 

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