author  hoelzl 
Tue, 05 Nov 2013 09:45:02 +0100  
changeset 54263  c4159fe6fa46 
parent 54230  b1d955791529 
child 54489  03ff4d1e6784 
permissions  rwrr 
51524  1 
(* Title: HOL/Real_Vector_Spaces.thy 
27552
15cf4ed9c2a1
reremoved subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef
haftmann
parents:
27515
diff
changeset

2 
Author: Brian Huffman 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

3 
Author: Johannes Hölzl 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

4 
*) 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

5 

6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

6 
header {* Vector Spaces and Algebras over the Reals *} 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

7 

51524  8 
theory Real_Vector_Spaces 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

9 
imports Real Topological_Spaces 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

10 
begin 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

11 

6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

12 
subsection {* Locale for additive functions *} 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

13 

6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

14 
locale additive = 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

15 
fixes f :: "'a::ab_group_add \<Rightarrow> 'b::ab_group_add" 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

16 
assumes add: "f (x + y) = f x + f y" 
27443  17 
begin 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

18 

27443  19 
lemma zero: "f 0 = 0" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

20 
proof  
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

21 
have "f 0 = f (0 + 0)" by simp 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

22 
also have "\<dots> = f 0 + f 0" by (rule add) 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

23 
finally show "f 0 = 0" by simp 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

24 
qed 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

25 

27443  26 
lemma minus: "f ( x) =  f x" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

27 
proof  
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

28 
have "f ( x) + f x = f ( x + x)" by (rule add [symmetric]) 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

29 
also have "\<dots> =  f x + f x" by (simp add: zero) 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

30 
finally show "f ( x) =  f x" by (rule add_right_imp_eq) 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

31 
qed 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

32 

27443  33 
lemma diff: "f (x  y) = f x  f y" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53600
diff
changeset

34 
using add [of x " y"] by (simp add: minus) 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

35 

27443  36 
lemma setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))" 
22942  37 
apply (cases "finite A") 
38 
apply (induct set: finite) 

39 
apply (simp add: zero) 

40 
apply (simp add: add) 

41 
apply (simp add: zero) 

42 
done 

43 

27443  44 
end 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

45 

28029
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

46 
subsection {* Vector spaces *} 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

47 

4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

48 
locale vector_space = 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

49 
fixes scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" 
30070
76cee7c62782
declare scaleR distrib rules [algebra_simps]; cleaned up
huffman
parents:
30069
diff
changeset

50 
assumes scale_right_distrib [algebra_simps]: 
76cee7c62782
declare scaleR distrib rules [algebra_simps]; cleaned up
huffman
parents:
30069
diff
changeset

51 
"scale a (x + y) = scale a x + scale a y" 
76cee7c62782
declare scaleR distrib rules [algebra_simps]; cleaned up
huffman
parents:
30069
diff
changeset

52 
and scale_left_distrib [algebra_simps]: 
76cee7c62782
declare scaleR distrib rules [algebra_simps]; cleaned up
huffman
parents:
30069
diff
changeset

53 
"scale (a + b) x = scale a x + scale b x" 
28029
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

54 
and scale_scale [simp]: "scale a (scale b x) = scale (a * b) x" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

55 
and scale_one [simp]: "scale 1 x = x" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

56 
begin 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

57 

4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

58 
lemma scale_left_commute: 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

59 
"scale a (scale b x) = scale b (scale a x)" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

60 
by (simp add: mult_commute) 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

61 

4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

62 
lemma scale_zero_left [simp]: "scale 0 x = 0" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

63 
and scale_minus_left [simp]: "scale ( a) x =  (scale a x)" 
30070
76cee7c62782
declare scaleR distrib rules [algebra_simps]; cleaned up
huffman
parents:
30069
diff
changeset

64 
and scale_left_diff_distrib [algebra_simps]: 
76cee7c62782
declare scaleR distrib rules [algebra_simps]; cleaned up
huffman
parents:
30069
diff
changeset

65 
"scale (a  b) x = scale a x  scale b x" 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

66 
and scale_setsum_left: "scale (setsum f A) x = (\<Sum>a\<in>A. scale (f a) x)" 
28029
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

67 
proof  
29229  68 
interpret s: additive "\<lambda>a. scale a x" 
28823  69 
proof qed (rule scale_left_distrib) 
28029
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

70 
show "scale 0 x = 0" by (rule s.zero) 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

71 
show "scale ( a) x =  (scale a x)" by (rule s.minus) 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

72 
show "scale (a  b) x = scale a x  scale b x" by (rule s.diff) 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

73 
show "scale (setsum f A) x = (\<Sum>a\<in>A. scale (f a) x)" by (rule s.setsum) 
28029
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

74 
qed 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

75 

4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

76 
lemma scale_zero_right [simp]: "scale a 0 = 0" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

77 
and scale_minus_right [simp]: "scale a ( x) =  (scale a x)" 
30070
76cee7c62782
declare scaleR distrib rules [algebra_simps]; cleaned up
huffman
parents:
30069
diff
changeset

78 
and scale_right_diff_distrib [algebra_simps]: 
76cee7c62782
declare scaleR distrib rules [algebra_simps]; cleaned up
huffman
parents:
30069
diff
changeset

79 
"scale a (x  y) = scale a x  scale a y" 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

80 
and scale_setsum_right: "scale a (setsum f A) = (\<Sum>x\<in>A. scale a (f x))" 
28029
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

81 
proof  
29229  82 
interpret s: additive "\<lambda>x. scale a x" 
28823  83 
proof qed (rule scale_right_distrib) 
28029
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

84 
show "scale a 0 = 0" by (rule s.zero) 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

85 
show "scale a ( x) =  (scale a x)" by (rule s.minus) 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

86 
show "scale a (x  y) = scale a x  scale a y" by (rule s.diff) 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

87 
show "scale a (setsum f A) = (\<Sum>x\<in>A. scale a (f x))" by (rule s.setsum) 
28029
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

88 
qed 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

89 

4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

90 
lemma scale_eq_0_iff [simp]: 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

91 
"scale a x = 0 \<longleftrightarrow> a = 0 \<or> x = 0" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

92 
proof cases 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

93 
assume "a = 0" thus ?thesis by simp 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

94 
next 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

95 
assume anz [simp]: "a \<noteq> 0" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

96 
{ assume "scale a x = 0" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

97 
hence "scale (inverse a) (scale a x) = 0" by simp 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

98 
hence "x = 0" by simp } 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

99 
thus ?thesis by force 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

100 
qed 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

101 

4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

102 
lemma scale_left_imp_eq: 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

103 
"\<lbrakk>a \<noteq> 0; scale a x = scale a y\<rbrakk> \<Longrightarrow> x = y" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

104 
proof  
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

105 
assume nonzero: "a \<noteq> 0" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

106 
assume "scale a x = scale a y" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

107 
hence "scale a (x  y) = 0" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

108 
by (simp add: scale_right_diff_distrib) 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

109 
hence "x  y = 0" by (simp add: nonzero) 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

110 
thus "x = y" by (simp only: right_minus_eq) 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

111 
qed 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

112 

4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

113 
lemma scale_right_imp_eq: 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

114 
"\<lbrakk>x \<noteq> 0; scale a x = scale b x\<rbrakk> \<Longrightarrow> a = b" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

115 
proof  
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

116 
assume nonzero: "x \<noteq> 0" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

117 
assume "scale a x = scale b x" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

118 
hence "scale (a  b) x = 0" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

119 
by (simp add: scale_left_diff_distrib) 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

120 
hence "a  b = 0" by (simp add: nonzero) 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

121 
thus "a = b" by (simp only: right_minus_eq) 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

122 
qed 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

123 

31586
d4707b99e631
declare norm_scaleR [simp]; declare scaleR_cancel lemmas [simp]
huffman
parents:
31567
diff
changeset

124 
lemma scale_cancel_left [simp]: 
28029
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

125 
"scale a x = scale a y \<longleftrightarrow> x = y \<or> a = 0" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

126 
by (auto intro: scale_left_imp_eq) 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

127 

31586
d4707b99e631
declare norm_scaleR [simp]; declare scaleR_cancel lemmas [simp]
huffman
parents:
31567
diff
changeset

128 
lemma scale_cancel_right [simp]: 
28029
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

129 
"scale a x = scale b x \<longleftrightarrow> a = b \<or> x = 0" 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

130 
by (auto intro: scale_right_imp_eq) 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

131 

4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

132 
end 
4c55cdec4ce7
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
huffman
parents:
28009
diff
changeset

133 

20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

134 
subsection {* Real vector spaces *} 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

135 

29608  136 
class scaleR = 
25062  137 
fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "*\<^sub>R" 75) 
24748  138 
begin 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

139 

20763  140 
abbreviation 
25062  141 
divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a" (infixl "'/\<^sub>R" 70) 
24748  142 
where 
25062  143 
"x /\<^sub>R r == scaleR (inverse r) x" 
24748  144 

145 
end 

146 

24588  147 
class real_vector = scaleR + ab_group_add + 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

148 
assumes scaleR_add_right: "scaleR a (x + y) = scaleR a x + scaleR a y" 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

149 
and scaleR_add_left: "scaleR (a + b) x = scaleR a x + scaleR b x" 
30070
76cee7c62782
declare scaleR distrib rules [algebra_simps]; cleaned up
huffman
parents:
30069
diff
changeset

150 
and scaleR_scaleR: "scaleR a (scaleR b x) = scaleR (a * b) x" 
76cee7c62782
declare scaleR distrib rules [algebra_simps]; cleaned up
huffman
parents:
30069
diff
changeset

151 
and scaleR_one: "scaleR 1 x = x" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

152 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30273
diff
changeset

153 
interpretation real_vector: 
29229  154 
vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector" 
28009
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

155 
apply unfold_locales 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

156 
apply (rule scaleR_add_right) 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

157 
apply (rule scaleR_add_left) 
28009
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

158 
apply (rule scaleR_scaleR) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

159 
apply (rule scaleR_one) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

160 
done 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

161 

e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

162 
text {* Recover original theorem names *} 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

163 

e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

164 
lemmas scaleR_left_commute = real_vector.scale_left_commute 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

165 
lemmas scaleR_zero_left = real_vector.scale_zero_left 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

166 
lemmas scaleR_minus_left = real_vector.scale_minus_left 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

167 
lemmas scaleR_diff_left = real_vector.scale_left_diff_distrib 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

168 
lemmas scaleR_setsum_left = real_vector.scale_setsum_left 
28009
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

169 
lemmas scaleR_zero_right = real_vector.scale_zero_right 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

170 
lemmas scaleR_minus_right = real_vector.scale_minus_right 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

171 
lemmas scaleR_diff_right = real_vector.scale_right_diff_distrib 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

172 
lemmas scaleR_setsum_right = real_vector.scale_setsum_right 
28009
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

173 
lemmas scaleR_eq_0_iff = real_vector.scale_eq_0_iff 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

174 
lemmas scaleR_left_imp_eq = real_vector.scale_left_imp_eq 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

175 
lemmas scaleR_right_imp_eq = real_vector.scale_right_imp_eq 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

176 
lemmas scaleR_cancel_left = real_vector.scale_cancel_left 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

177 
lemmas scaleR_cancel_right = real_vector.scale_cancel_right 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

178 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

179 
text {* Legacy names *} 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

180 

f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

181 
lemmas scaleR_left_distrib = scaleR_add_left 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

182 
lemmas scaleR_right_distrib = scaleR_add_right 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

183 
lemmas scaleR_left_diff_distrib = scaleR_diff_left 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

184 
lemmas scaleR_right_diff_distrib = scaleR_diff_right 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

185 

31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31017
diff
changeset

186 
lemma scaleR_minus1_left [simp]: 
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31017
diff
changeset

187 
fixes x :: "'a::real_vector" 
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31017
diff
changeset

188 
shows "scaleR (1) x =  x" 
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31017
diff
changeset

189 
using scaleR_minus_left [of 1 x] by simp 
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31017
diff
changeset

190 

24588  191 
class real_algebra = real_vector + ring + 
25062  192 
assumes mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)" 
193 
and mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)" 

20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

194 

24588  195 
class real_algebra_1 = real_algebra + ring_1 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

196 

24588  197 
class real_div_algebra = real_algebra_1 + division_ring 
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

198 

24588  199 
class real_field = real_div_algebra + field 
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

200 

30069  201 
instantiation real :: real_field 
202 
begin 

203 

204 
definition 

205 
real_scaleR_def [simp]: "scaleR a x = a * x" 

206 

30070
76cee7c62782
declare scaleR distrib rules [algebra_simps]; cleaned up
huffman
parents:
30069
diff
changeset

207 
instance proof 
76cee7c62782
declare scaleR distrib rules [algebra_simps]; cleaned up
huffman
parents:
30069
diff
changeset

208 
qed (simp_all add: algebra_simps) 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

209 

30069  210 
end 
211 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30273
diff
changeset

212 
interpretation scaleR_left: additive "(\<lambda>a. scaleR a x::'a::real_vector)" 
28823  213 
proof qed (rule scaleR_left_distrib) 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

214 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30273
diff
changeset

215 
interpretation scaleR_right: additive "(\<lambda>x. scaleR a x::'a::real_vector)" 
28823  216 
proof qed (rule scaleR_right_distrib) 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

217 

20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

218 
lemma nonzero_inverse_scaleR_distrib: 
21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

219 
fixes x :: "'a::real_div_algebra" shows 
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

220 
"\<lbrakk>a \<noteq> 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> inverse (scaleR a x) = scaleR (inverse a) (inverse x)" 
20763  221 
by (rule inverse_unique, simp) 
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

222 

60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

223 
lemma inverse_scaleR_distrib: 
36409  224 
fixes x :: "'a::{real_div_algebra, division_ring_inverse_zero}" 
21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

225 
shows "inverse (scaleR a x) = scaleR (inverse a) (inverse x)" 
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

226 
apply (case_tac "a = 0", simp) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

227 
apply (case_tac "x = 0", simp) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

228 
apply (erule (1) nonzero_inverse_scaleR_distrib) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

229 
done 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

230 

20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

231 

c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

232 
subsection {* Embedding of the Reals into any @{text real_algebra_1}: 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

233 
@{term of_real} *} 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

234 

c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

235 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

236 
of_real :: "real \<Rightarrow> 'a::real_algebra_1" where 
21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

237 
"of_real r = scaleR r 1" 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

238 

21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

239 
lemma scaleR_conv_of_real: "scaleR r x = of_real r * x" 
20763  240 
by (simp add: of_real_def) 
241 

20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

242 
lemma of_real_0 [simp]: "of_real 0 = 0" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

243 
by (simp add: of_real_def) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

244 

c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

245 
lemma of_real_1 [simp]: "of_real 1 = 1" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

246 
by (simp add: of_real_def) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

247 

c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

248 
lemma of_real_add [simp]: "of_real (x + y) = of_real x + of_real y" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

249 
by (simp add: of_real_def scaleR_left_distrib) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

250 

c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

251 
lemma of_real_minus [simp]: "of_real ( x) =  of_real x" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

252 
by (simp add: of_real_def) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

253 

c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

254 
lemma of_real_diff [simp]: "of_real (x  y) = of_real x  of_real y" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

255 
by (simp add: of_real_def scaleR_left_diff_distrib) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

256 

c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

257 
lemma of_real_mult [simp]: "of_real (x * y) = of_real x * of_real y" 
20763  258 
by (simp add: of_real_def mult_commute) 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

259 

20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

260 
lemma nonzero_of_real_inverse: 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

261 
"x \<noteq> 0 \<Longrightarrow> of_real (inverse x) = 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

262 
inverse (of_real x :: 'a::real_div_algebra)" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

263 
by (simp add: of_real_def nonzero_inverse_scaleR_distrib) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

264 

60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

265 
lemma of_real_inverse [simp]: 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

266 
"of_real (inverse x) = 
36409  267 
inverse (of_real x :: 'a::{real_div_algebra, division_ring_inverse_zero})" 
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

268 
by (simp add: of_real_def inverse_scaleR_distrib) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

269 

60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

270 
lemma nonzero_of_real_divide: 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

271 
"y \<noteq> 0 \<Longrightarrow> of_real (x / y) = 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

272 
(of_real x / of_real y :: 'a::real_field)" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

273 
by (simp add: divide_inverse nonzero_of_real_inverse) 
20722  274 

275 
lemma of_real_divide [simp]: 

20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

276 
"of_real (x / y) = 
36409  277 
(of_real x / of_real y :: 'a::{real_field, field_inverse_zero})" 
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

278 
by (simp add: divide_inverse) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

279 

20722  280 
lemma of_real_power [simp]: 
31017  281 
"of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1}) ^ n" 
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30242
diff
changeset

282 
by (induct n) simp_all 
20722  283 

20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

284 
lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)" 
35216  285 
by (simp add: of_real_def) 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

286 

38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37887
diff
changeset

287 
lemma inj_of_real: 
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37887
diff
changeset

288 
"inj of_real" 
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37887
diff
changeset

289 
by (auto intro: injI) 
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37887
diff
changeset

290 

20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

291 
lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified] 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

292 

c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

293 
lemma of_real_eq_id [simp]: "of_real = (id :: real \<Rightarrow> real)" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

294 
proof 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

295 
fix r 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

296 
show "of_real r = id r" 
22973
64d300e16370
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
huffman
parents:
22972
diff
changeset

297 
by (simp add: of_real_def) 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

298 
qed 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

299 

c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

300 
text{*Collapse nested embeddings*} 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

301 
lemma of_real_of_nat_eq [simp]: "of_real (of_nat n) = of_nat n" 
20772  302 
by (induct n) auto 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

303 

c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

304 
lemma of_real_of_int_eq [simp]: "of_real (of_int z) = of_int z" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

305 
by (cases z rule: int_diff_cases, simp) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

306 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

307 
lemma of_real_numeral: "of_real (numeral w) = numeral w" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

308 
using of_real_of_int_eq [of "numeral w"] by simp 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

309 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

310 
lemma of_real_neg_numeral: "of_real (neg_numeral w) = neg_numeral w" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

311 
using of_real_of_int_eq [of "neg_numeral w"] by simp 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

312 

22912  313 
text{*Every real algebra has characteristic zero*} 
38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37887
diff
changeset

314 

22912  315 
instance real_algebra_1 < ring_char_0 
316 
proof 

38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37887
diff
changeset

317 
from inj_of_real inj_of_nat have "inj (of_real \<circ> of_nat)" by (rule inj_comp) 
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37887
diff
changeset

318 
then show "inj (of_nat :: nat \<Rightarrow> 'a)" by (simp add: comp_def) 
22912  319 
qed 
320 

27553  321 
instance real_field < field_char_0 .. 
322 

20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

323 

c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

324 
subsection {* The Set of Real Numbers *} 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

325 

37767  326 
definition Reals :: "'a::real_algebra_1 set" where 
327 
"Reals = range of_real" 

20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

328 

21210  329 
notation (xsymbols) 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

330 
Reals ("\<real>") 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

331 

21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

332 
lemma Reals_of_real [simp]: "of_real r \<in> Reals" 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

333 
by (simp add: Reals_def) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

334 

21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

335 
lemma Reals_of_int [simp]: "of_int z \<in> Reals" 
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

336 
by (subst of_real_of_int_eq [symmetric], rule Reals_of_real) 
20718  337 

21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

338 
lemma Reals_of_nat [simp]: "of_nat n \<in> Reals" 
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

339 
by (subst of_real_of_nat_eq [symmetric], rule Reals_of_real) 
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

340 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

341 
lemma Reals_numeral [simp]: "numeral w \<in> Reals" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

342 
by (subst of_real_numeral [symmetric], rule Reals_of_real) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

343 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

344 
lemma Reals_neg_numeral [simp]: "neg_numeral w \<in> Reals" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

345 
by (subst of_real_neg_numeral [symmetric], rule Reals_of_real) 
20718  346 

20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

347 
lemma Reals_0 [simp]: "0 \<in> Reals" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

348 
apply (unfold Reals_def) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

349 
apply (rule range_eqI) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

350 
apply (rule of_real_0 [symmetric]) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

351 
done 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

352 

c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

353 
lemma Reals_1 [simp]: "1 \<in> Reals" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

354 
apply (unfold Reals_def) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

355 
apply (rule range_eqI) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

356 
apply (rule of_real_1 [symmetric]) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

357 
done 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

358 

20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

359 
lemma Reals_add [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a + b \<in> Reals" 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

360 
apply (auto simp add: Reals_def) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

361 
apply (rule range_eqI) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

362 
apply (rule of_real_add [symmetric]) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

363 
done 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

364 

20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

365 
lemma Reals_minus [simp]: "a \<in> Reals \<Longrightarrow>  a \<in> Reals" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

366 
apply (auto simp add: Reals_def) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

367 
apply (rule range_eqI) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

368 
apply (rule of_real_minus [symmetric]) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

369 
done 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

370 

60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

371 
lemma Reals_diff [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a  b \<in> Reals" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

372 
apply (auto simp add: Reals_def) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

373 
apply (rule range_eqI) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

374 
apply (rule of_real_diff [symmetric]) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

375 
done 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

376 

60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

377 
lemma Reals_mult [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a * b \<in> Reals" 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

378 
apply (auto simp add: Reals_def) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

379 
apply (rule range_eqI) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

380 
apply (rule of_real_mult [symmetric]) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

381 
done 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

382 

20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

383 
lemma nonzero_Reals_inverse: 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

384 
fixes a :: "'a::real_div_algebra" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

385 
shows "\<lbrakk>a \<in> Reals; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Reals" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

386 
apply (auto simp add: Reals_def) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

387 
apply (rule range_eqI) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

388 
apply (erule nonzero_of_real_inverse [symmetric]) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

389 
done 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

390 

60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

391 
lemma Reals_inverse [simp]: 
36409  392 
fixes a :: "'a::{real_div_algebra, division_ring_inverse_zero}" 
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

393 
shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

394 
apply (auto simp add: Reals_def) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

395 
apply (rule range_eqI) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

396 
apply (rule of_real_inverse [symmetric]) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

397 
done 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

398 

60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

399 
lemma nonzero_Reals_divide: 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

400 
fixes a b :: "'a::real_field" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

401 
shows "\<lbrakk>a \<in> Reals; b \<in> Reals; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Reals" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

402 
apply (auto simp add: Reals_def) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

403 
apply (rule range_eqI) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

404 
apply (erule nonzero_of_real_divide [symmetric]) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

405 
done 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

406 

60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

407 
lemma Reals_divide [simp]: 
36409  408 
fixes a b :: "'a::{real_field, field_inverse_zero}" 
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

409 
shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

410 
apply (auto simp add: Reals_def) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

411 
apply (rule range_eqI) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

412 
apply (rule of_real_divide [symmetric]) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

413 
done 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

414 

20722  415 
lemma Reals_power [simp]: 
31017  416 
fixes a :: "'a::{real_algebra_1}" 
20722  417 
shows "a \<in> Reals \<Longrightarrow> a ^ n \<in> Reals" 
418 
apply (auto simp add: Reals_def) 

419 
apply (rule range_eqI) 

420 
apply (rule of_real_power [symmetric]) 

421 
done 

422 

20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

423 
lemma Reals_cases [cases set: Reals]: 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

424 
assumes "q \<in> \<real>" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

425 
obtains (of_real) r where "q = of_real r" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

426 
unfolding Reals_def 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

427 
proof  
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

428 
from `q \<in> \<real>` have "q \<in> range of_real" unfolding Reals_def . 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

429 
then obtain r where "q = of_real r" .. 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

430 
then show thesis .. 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

431 
qed 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

432 

c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

433 
lemma Reals_induct [case_names of_real, induct set: Reals]: 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

434 
"q \<in> \<real> \<Longrightarrow> (\<And>r. P (of_real r)) \<Longrightarrow> P q" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

435 
by (rule Reals_cases) auto 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

436 

20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

437 

6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

438 
subsection {* Real normed vector spaces *} 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

439 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

440 
class dist = 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

441 
fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

442 

29608  443 
class norm = 
22636  444 
fixes norm :: "'a \<Rightarrow> real" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

445 

24520  446 
class sgn_div_norm = scaleR + norm + sgn + 
25062  447 
assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x" 
24506  448 

31289  449 
class dist_norm = dist + norm + minus + 
450 
assumes dist_norm: "dist x y = norm (x  y)" 

451 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

452 
class open_dist = "open" + dist + 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

453 
assumes open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

454 

31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

455 
class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_dist + 
51002
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50999
diff
changeset

456 
assumes norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0" 
25062  457 
and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y" 
31586
d4707b99e631
declare norm_scaleR [simp]; declare scaleR_cancel lemmas [simp]
huffman
parents:
31567
diff
changeset

458 
and norm_scaleR [simp]: "norm (scaleR a x) = \<bar>a\<bar> * norm x" 
51002
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50999
diff
changeset

459 
begin 
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50999
diff
changeset

460 

496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50999
diff
changeset

461 
lemma norm_ge_zero [simp]: "0 \<le> norm x" 
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50999
diff
changeset

462 
proof  
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50999
diff
changeset

463 
have "0 = norm (x + 1 *\<^sub>R x)" 
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50999
diff
changeset

464 
using scaleR_add_left[of 1 "1" x] norm_scaleR[of 0 x] by (simp add: scaleR_one) 
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50999
diff
changeset

465 
also have "\<dots> \<le> norm x + norm (1 *\<^sub>R x)" by (rule norm_triangle_ineq) 
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50999
diff
changeset

466 
finally show ?thesis by simp 
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50999
diff
changeset

467 
qed 
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50999
diff
changeset

468 

496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50999
diff
changeset

469 
end 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

470 

24588  471 
class real_normed_algebra = real_algebra + real_normed_vector + 
25062  472 
assumes norm_mult_ineq: "norm (x * y) \<le> norm x * norm y" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

473 

24588  474 
class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra + 
25062  475 
assumes norm_one [simp]: "norm 1 = 1" 
22852  476 

24588  477 
class real_normed_div_algebra = real_div_algebra + real_normed_vector + 
25062  478 
assumes norm_mult: "norm (x * y) = norm x * norm y" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

479 

24588  480 
class real_normed_field = real_field + real_normed_div_algebra 
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

481 

22852  482 
instance real_normed_div_algebra < real_normed_algebra_1 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

483 
proof 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

484 
fix x y :: 'a 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

485 
show "norm (x * y) \<le> norm x * norm y" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

486 
by (simp add: norm_mult) 
22852  487 
next 
488 
have "norm (1 * 1::'a) = norm (1::'a) * norm (1::'a)" 

489 
by (rule norm_mult) 

490 
thus "norm (1::'a) = 1" by simp 

20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

491 
qed 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

492 

22852  493 
lemma norm_zero [simp]: "norm (0::'a::real_normed_vector) = 0" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

494 
by simp 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

495 

22852  496 
lemma zero_less_norm_iff [simp]: 
497 
fixes x :: "'a::real_normed_vector" 

498 
shows "(0 < norm x) = (x \<noteq> 0)" 

20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

499 
by (simp add: order_less_le) 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

500 

22852  501 
lemma norm_not_less_zero [simp]: 
502 
fixes x :: "'a::real_normed_vector" 

503 
shows "\<not> norm x < 0" 

20828  504 
by (simp add: linorder_not_less) 
505 

22852  506 
lemma norm_le_zero_iff [simp]: 
507 
fixes x :: "'a::real_normed_vector" 

508 
shows "(norm x \<le> 0) = (x = 0)" 

20828  509 
by (simp add: order_le_less) 
510 

20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

511 
lemma norm_minus_cancel [simp]: 
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

512 
fixes x :: "'a::real_normed_vector" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

513 
shows "norm ( x) = norm x" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

514 
proof  
21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

515 
have "norm ( x) = norm (scaleR ( 1) x)" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

516 
by (simp only: scaleR_minus_left scaleR_one) 
20533  517 
also have "\<dots> = \<bar> 1\<bar> * norm x" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

518 
by (rule norm_scaleR) 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

519 
finally show ?thesis by simp 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

520 
qed 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

521 

6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

522 
lemma norm_minus_commute: 
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

523 
fixes a b :: "'a::real_normed_vector" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

524 
shows "norm (a  b) = norm (b  a)" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

525 
proof  
22898  526 
have "norm ( (b  a)) = norm (b  a)" 
527 
by (rule norm_minus_cancel) 

528 
thus ?thesis by simp 

20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

529 
qed 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

530 

6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

531 
lemma norm_triangle_ineq2: 
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

532 
fixes a b :: "'a::real_normed_vector" 
20533  533 
shows "norm a  norm b \<le> norm (a  b)" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

534 
proof  
20533  535 
have "norm (a  b + b) \<le> norm (a  b) + norm b" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

536 
by (rule norm_triangle_ineq) 
22898  537 
thus ?thesis by simp 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

538 
qed 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

539 

20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

540 
lemma norm_triangle_ineq3: 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

541 
fixes a b :: "'a::real_normed_vector" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

542 
shows "\<bar>norm a  norm b\<bar> \<le> norm (a  b)" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

543 
apply (subst abs_le_iff) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

544 
apply auto 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

545 
apply (rule norm_triangle_ineq2) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

546 
apply (subst norm_minus_commute) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

547 
apply (rule norm_triangle_ineq2) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

548 
done 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

549 

20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

550 
lemma norm_triangle_ineq4: 
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

551 
fixes a b :: "'a::real_normed_vector" 
20533  552 
shows "norm (a  b) \<le> norm a + norm b" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

553 
proof  
22898  554 
have "norm (a +  b) \<le> norm a + norm ( b)" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

555 
by (rule norm_triangle_ineq) 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53600
diff
changeset

556 
then show ?thesis by simp 
22898  557 
qed 
558 

559 
lemma norm_diff_ineq: 

560 
fixes a b :: "'a::real_normed_vector" 

561 
shows "norm a  norm b \<le> norm (a + b)" 

562 
proof  

563 
have "norm a  norm ( b) \<le> norm (a   b)" 

564 
by (rule norm_triangle_ineq2) 

565 
thus ?thesis by simp 

20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

566 
qed 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

567 

20551  568 
lemma norm_diff_triangle_ineq: 
569 
fixes a b c d :: "'a::real_normed_vector" 

570 
shows "norm ((a + b)  (c + d)) \<le> norm (a  c) + norm (b  d)" 

571 
proof  

572 
have "norm ((a + b)  (c + d)) = norm ((a  c) + (b  d))" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53600
diff
changeset

573 
by (simp add: algebra_simps) 
20551  574 
also have "\<dots> \<le> norm (a  c) + norm (b  d)" 
575 
by (rule norm_triangle_ineq) 

576 
finally show ?thesis . 

577 
qed 

578 

22857  579 
lemma abs_norm_cancel [simp]: 
580 
fixes a :: "'a::real_normed_vector" 

581 
shows "\<bar>norm a\<bar> = norm a" 

582 
by (rule abs_of_nonneg [OF norm_ge_zero]) 

583 

22880  584 
lemma norm_add_less: 
585 
fixes x y :: "'a::real_normed_vector" 

586 
shows "\<lbrakk>norm x < r; norm y < s\<rbrakk> \<Longrightarrow> norm (x + y) < r + s" 

587 
by (rule order_le_less_trans [OF norm_triangle_ineq add_strict_mono]) 

588 

589 
lemma norm_mult_less: 

590 
fixes x y :: "'a::real_normed_algebra" 

591 
shows "\<lbrakk>norm x < r; norm y < s\<rbrakk> \<Longrightarrow> norm (x * y) < r * s" 

592 
apply (rule order_le_less_trans [OF norm_mult_ineq]) 

593 
apply (simp add: mult_strict_mono') 

594 
done 

595 

22857  596 
lemma norm_of_real [simp]: 
597 
"norm (of_real r :: 'a::real_normed_algebra_1) = \<bar>r\<bar>" 

31586
d4707b99e631
declare norm_scaleR [simp]; declare scaleR_cancel lemmas [simp]
huffman
parents:
31567
diff
changeset

598 
unfolding of_real_def by simp 
20560  599 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

600 
lemma norm_numeral [simp]: 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

601 
"norm (numeral w::'a::real_normed_algebra_1) = numeral w" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

602 
by (subst of_real_numeral [symmetric], subst norm_of_real, simp) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

603 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

604 
lemma norm_neg_numeral [simp]: 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

605 
"norm (neg_numeral w::'a::real_normed_algebra_1) = numeral w" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46868
diff
changeset

606 
by (subst of_real_neg_numeral [symmetric], subst norm_of_real, simp) 
22876
2b4c831ceca7
add lemmas norm_number_of, norm_of_int, norm_of_nat
huffman
parents:
22857
diff
changeset

607 

2b4c831ceca7
add lemmas norm_number_of, norm_of_int, norm_of_nat
huffman
parents:
22857
diff
changeset

608 
lemma norm_of_int [simp]: 
2b4c831ceca7
add lemmas norm_number_of, norm_of_int, norm_of_nat
huffman
parents:
22857
diff
changeset

609 
"norm (of_int z::'a::real_normed_algebra_1) = \<bar>of_int z\<bar>" 
2b4c831ceca7
add lemmas norm_number_of, norm_of_int, norm_of_nat
huffman
parents:
22857
diff
changeset

610 
by (subst of_real_of_int_eq [symmetric], rule norm_of_real) 
2b4c831ceca7
add lemmas norm_number_of, norm_of_int, norm_of_nat
huffman
parents:
22857
diff
changeset

611 

2b4c831ceca7
add lemmas norm_number_of, norm_of_int, norm_of_nat
huffman
parents:
22857
diff
changeset

612 
lemma norm_of_nat [simp]: 
2b4c831ceca7
add lemmas norm_number_of, norm_of_int, norm_of_nat
huffman
parents:
22857
diff
changeset

613 
"norm (of_nat n::'a::real_normed_algebra_1) = of_nat n" 
2b4c831ceca7
add lemmas norm_number_of, norm_of_int, norm_of_nat
huffman
parents:
22857
diff
changeset

614 
apply (subst of_real_of_nat_eq [symmetric]) 
2b4c831ceca7
add lemmas norm_number_of, norm_of_int, norm_of_nat
huffman
parents:
22857
diff
changeset

615 
apply (subst norm_of_real, simp) 
2b4c831ceca7
add lemmas norm_number_of, norm_of_int, norm_of_nat
huffman
parents:
22857
diff
changeset

616 
done 
2b4c831ceca7
add lemmas norm_number_of, norm_of_int, norm_of_nat
huffman
parents:
22857
diff
changeset

617 

20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

618 
lemma nonzero_norm_inverse: 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

619 
fixes a :: "'a::real_normed_div_algebra" 
20533  620 
shows "a \<noteq> 0 \<Longrightarrow> norm (inverse a) = inverse (norm a)" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

621 
apply (rule inverse_unique [symmetric]) 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

622 
apply (simp add: norm_mult [symmetric]) 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

623 
done 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

624 

6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

625 
lemma norm_inverse: 
36409  626 
fixes a :: "'a::{real_normed_div_algebra, division_ring_inverse_zero}" 
20533  627 
shows "norm (inverse a) = inverse (norm a)" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

628 
apply (case_tac "a = 0", simp) 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

629 
apply (erule nonzero_norm_inverse) 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

630 
done 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

631 

20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

632 
lemma nonzero_norm_divide: 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

633 
fixes a b :: "'a::real_normed_field" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

634 
shows "b \<noteq> 0 \<Longrightarrow> norm (a / b) = norm a / norm b" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

635 
by (simp add: divide_inverse norm_mult nonzero_norm_inverse) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

636 

60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

637 
lemma norm_divide: 
36409  638 
fixes a b :: "'a::{real_normed_field, field_inverse_zero}" 
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

639 
shows "norm (a / b) = norm a / norm b" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

640 
by (simp add: divide_inverse norm_mult norm_inverse) 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

641 

22852  642 
lemma norm_power_ineq: 
31017  643 
fixes x :: "'a::{real_normed_algebra_1}" 
22852  644 
shows "norm (x ^ n) \<le> norm x ^ n" 
645 
proof (induct n) 

646 
case 0 show "norm (x ^ 0) \<le> norm x ^ 0" by simp 

647 
next 

648 
case (Suc n) 

649 
have "norm (x * x ^ n) \<le> norm x * norm (x ^ n)" 

650 
by (rule norm_mult_ineq) 

651 
also from Suc have "\<dots> \<le> norm x * norm x ^ n" 

652 
using norm_ge_zero by (rule mult_left_mono) 

653 
finally show "norm (x ^ Suc n) \<le> norm x ^ Suc n" 

30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30242
diff
changeset

654 
by simp 
22852  655 
qed 
656 

20684  657 
lemma norm_power: 
31017  658 
fixes x :: "'a::{real_normed_div_algebra}" 
20684  659 
shows "norm (x ^ n) = norm x ^ n" 
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30242
diff
changeset

660 
by (induct n) (simp_all add: norm_mult) 
20684  661 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

662 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

663 
subsection {* Metric spaces *} 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

664 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

665 
class metric_space = open_dist + 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

666 
assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

667 
assumes dist_triangle2: "dist x y \<le> dist x z + dist y z" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

668 
begin 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

669 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

670 
lemma dist_self [simp]: "dist x x = 0" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

671 
by simp 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

672 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

673 
lemma zero_le_dist [simp]: "0 \<le> dist x y" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

674 
using dist_triangle2 [of x x y] by simp 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

675 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

676 
lemma zero_less_dist_iff: "0 < dist x y \<longleftrightarrow> x \<noteq> y" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

677 
by (simp add: less_le) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

678 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

679 
lemma dist_not_less_zero [simp]: "\<not> dist x y < 0" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

680 
by (simp add: not_less) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

681 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

682 
lemma dist_le_zero_iff [simp]: "dist x y \<le> 0 \<longleftrightarrow> x = y" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

683 
by (simp add: le_less) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

684 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

685 
lemma dist_commute: "dist x y = dist y x" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

686 
proof (rule order_antisym) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

687 
show "dist x y \<le> dist y x" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

688 
using dist_triangle2 [of x y x] by simp 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

689 
show "dist y x \<le> dist x y" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

690 
using dist_triangle2 [of y x y] by simp 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

691 
qed 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

692 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

693 
lemma dist_triangle: "dist x z \<le> dist x y + dist y z" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

694 
using dist_triangle2 [of x z y] by (simp add: dist_commute) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

695 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

696 
lemma dist_triangle3: "dist x y \<le> dist a x + dist a y" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

697 
using dist_triangle2 [of x y a] by (simp add: dist_commute) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

698 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

699 
lemma dist_triangle_alt: 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

700 
shows "dist y z <= dist x y + dist x z" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

701 
by (rule dist_triangle3) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

702 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

703 
lemma dist_pos_lt: 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

704 
shows "x \<noteq> y ==> 0 < dist x y" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

705 
by (simp add: zero_less_dist_iff) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

706 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

707 
lemma dist_nz: 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

708 
shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

709 
by (simp add: zero_less_dist_iff) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

710 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

711 
lemma dist_triangle_le: 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

712 
shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

713 
by (rule order_trans [OF dist_triangle2]) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

714 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

715 
lemma dist_triangle_lt: 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

716 
shows "dist x z + dist y z < e ==> dist x y < e" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

717 
by (rule le_less_trans [OF dist_triangle2]) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

718 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

719 
lemma dist_triangle_half_l: 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

720 
shows "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

721 
by (rule dist_triangle_lt [where z=y], simp) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

722 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

723 
lemma dist_triangle_half_r: 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

724 
shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

725 
by (rule dist_triangle_half_l, simp_all add: dist_commute) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

726 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

727 
subclass topological_space 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

728 
proof 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

729 
have "\<exists>e::real. 0 < e" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

730 
by (fast intro: zero_less_one) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

731 
then show "open UNIV" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

732 
unfolding open_dist by simp 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

733 
next 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

734 
fix S T assume "open S" "open T" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

735 
then show "open (S \<inter> T)" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

736 
unfolding open_dist 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

737 
apply clarify 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

738 
apply (drule (1) bspec)+ 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

739 
apply (clarify, rename_tac r s) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

740 
apply (rule_tac x="min r s" in exI, simp) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

741 
done 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

742 
next 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

743 
fix K assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

744 
unfolding open_dist by fast 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

745 
qed 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

746 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

747 
lemma open_ball: "open {y. dist x y < d}" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

748 
proof (unfold open_dist, intro ballI) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

749 
fix y assume *: "y \<in> {y. dist x y < d}" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

750 
then show "\<exists>e>0. \<forall>z. dist z y < e \<longrightarrow> z \<in> {y. dist x y < d}" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

751 
by (auto intro!: exI[of _ "d  dist x y"] simp: field_simps dist_triangle_lt) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

752 
qed 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

753 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

754 
subclass first_countable_topology 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

755 
proof 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

756 
fix x 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

757 
show "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

758 
proof (safe intro!: exI[of _ "\<lambda>n. {y. dist x y < inverse (Suc n)}"]) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

759 
fix S assume "open S" "x \<in> S" 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
52381
diff
changeset

760 
then obtain e where e: "0 < e" and "{y. dist x y < e} \<subseteq> S" 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

761 
by (auto simp: open_dist subset_eq dist_commute) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

762 
moreover 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
52381
diff
changeset

763 
from e obtain i where "inverse (Suc i) < e" 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

764 
by (auto dest!: reals_Archimedean) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

765 
then have "{y. dist x y < inverse (Suc i)} \<subseteq> {y. dist x y < e}" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

766 
by auto 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

767 
ultimately show "\<exists>i. {y. dist x y < inverse (Suc i)} \<subseteq> S" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

768 
by blast 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

769 
qed (auto intro: open_ball) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

770 
qed 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

771 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

772 
end 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

773 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

774 
instance metric_space \<subseteq> t2_space 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

775 
proof 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

776 
fix x y :: "'a::metric_space" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

777 
assume xy: "x \<noteq> y" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

778 
let ?U = "{y'. dist x y' < dist x y / 2}" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

779 
let ?V = "{x'. dist y x' < dist x y / 2}" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

780 
have th0: "\<And>d x y z. (d x z :: real) \<le> d x y + d y z \<Longrightarrow> d y z = d z y 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

781 
\<Longrightarrow> \<not>(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

782 
have "open ?U \<and> open ?V \<and> x \<in> ?U \<and> y \<in> ?V \<and> ?U \<inter> ?V = {}" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

783 
using dist_pos_lt[OF xy] th0[of dist, OF dist_triangle dist_commute] 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

784 
using open_ball[of _ "dist x y / 2"] by auto 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

785 
then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

786 
by blast 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

787 
qed 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

788 

31289  789 
text {* Every normed vector space is a metric space. *} 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31017
diff
changeset

790 

31289  791 
instance real_normed_vector < metric_space 
792 
proof 

793 
fix x y :: 'a show "dist x y = 0 \<longleftrightarrow> x = y" 

794 
unfolding dist_norm by simp 

795 
next 

796 
fix x y z :: 'a show "dist x y \<le> dist x z + dist y z" 

797 
unfolding dist_norm 

798 
using norm_triangle_ineq4 [of "x  z" "y  z"] by simp 

799 
qed 

31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31017
diff
changeset

800 

31564
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

801 
subsection {* Class instances for real numbers *} 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

802 

d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

803 
instantiation real :: real_normed_field 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

804 
begin 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

805 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

806 
definition dist_real_def: 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

807 
"dist x y = \<bar>x  y\<bar>" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

808 

52381
63eec9cea2c7
pragmatic executability for instance real :: open
haftmann
parents:
51775
diff
changeset

809 
definition open_real_def [code del]: 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

810 
"open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

811 

31564
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

812 
definition real_norm_def [simp]: 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

813 
"norm r = \<bar>r\<bar>" 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

814 

d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

815 
instance 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

816 
apply (intro_classes, unfold real_norm_def real_scaleR_def) 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

817 
apply (rule dist_real_def) 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

818 
apply (rule open_real_def) 
36795
e05e1283c550
new construction of real numbers using Cauchy sequences
huffman
parents:
36409
diff
changeset

819 
apply (simp add: sgn_real_def) 
31564
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

820 
apply (rule abs_eq_0) 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

821 
apply (rule abs_triangle_ineq) 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

822 
apply (rule abs_mult) 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

823 
apply (rule abs_mult) 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

824 
done 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

825 

d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

826 
end 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

827 

52381
63eec9cea2c7
pragmatic executability for instance real :: open
haftmann
parents:
51775
diff
changeset

828 
code_abort "open :: real set \<Rightarrow> bool" 
63eec9cea2c7
pragmatic executability for instance real :: open
haftmann
parents:
51775
diff
changeset

829 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

830 
instance real :: linorder_topology 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

831 
proof 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

832 
show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

833 
proof (rule ext, safe) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

834 
fix S :: "real set" assume "open S" 
53381  835 
then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)" 
836 
unfolding open_real_def bchoice_iff .. 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

837 
then have *: "S = (\<Union>x\<in>S. {x  f x <..} \<inter> {..< x + f x})" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

838 
by (fastforce simp: dist_real_def) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

839 
show "generate_topology (range lessThan \<union> range greaterThan) S" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

840 
apply (subst *) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

841 
apply (intro generate_topology_Union generate_topology.Int) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

842 
apply (auto intro: generate_topology.Basis) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

843 
done 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

844 
next 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

845 
fix S :: "real set" assume "generate_topology (range lessThan \<union> range greaterThan) S" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

846 
moreover have "\<And>a::real. open {..<a}" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

847 
unfolding open_real_def dist_real_def 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

848 
proof clarify 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

849 
fix x a :: real assume "x < a" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

850 
hence "0 < a  x \<and> (\<forall>y. \<bar>y  x\<bar> < a  x \<longrightarrow> y \<in> {..<a})" by auto 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

851 
thus "\<exists>e>0. \<forall>y. \<bar>y  x\<bar> < e \<longrightarrow> y \<in> {..<a}" .. 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

852 
qed 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

853 
moreover have "\<And>a::real. open {a <..}" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

854 
unfolding open_real_def dist_real_def 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

855 
proof clarify 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

856 
fix x a :: real assume "a < x" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

857 
hence "0 < x  a \<and> (\<forall>y. \<bar>y  x\<bar> < x  a \<longrightarrow> y \<in> {a<..})" by auto 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

858 
thus "\<exists>e>0. \<forall>y. \<bar>y  x\<bar> < e \<longrightarrow> y \<in> {a<..}" .. 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

859 
qed 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

860 
ultimately show "open S" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

861 
by induct auto 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

862 
qed 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

863 
qed 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

864 

51775
408d937c9486
revert #916271d52466; add nontopological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51774
diff
changeset

865 
instance real :: linear_continuum_topology .. 
51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51481
diff
changeset

866 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

867 
lemmas open_real_greaterThan = open_greaterThan[where 'a=real] 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

868 
lemmas open_real_lessThan = open_lessThan[where 'a=real] 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

869 
lemmas open_real_greaterThanLessThan = open_greaterThanLessThan[where 'a=real] 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

870 
lemmas closed_real_atMost = closed_atMost[where 'a=real] 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

871 
lemmas closed_real_atLeast = closed_atLeast[where 'a=real] 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

872 
lemmas closed_real_atLeastAtMost = closed_atLeastAtMost[where 'a=real] 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

873 

31446  874 
subsection {* Extra type constraints *} 
875 

31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

876 
text {* Only allow @{term "open"} in class @{text topological_space}. *} 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

877 

5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

878 
setup {* Sign.add_const_constraint 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

879 
(@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"}) *} 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

880 

31446  881 
text {* Only allow @{term dist} in class @{text metric_space}. *} 
882 

883 
setup {* Sign.add_const_constraint 

884 
(@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *} 

885 

886 
text {* Only allow @{term norm} in class @{text real_normed_vector}. *} 

887 

888 
setup {* Sign.add_const_constraint 

889 
(@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *} 

890 

22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

891 
subsection {* Sign function *} 
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

892 

24506  893 
lemma norm_sgn: 
894 
"norm (sgn(x::'a::real_normed_vector)) = (if x = 0 then 0 else 1)" 

31586
d4707b99e631
declare norm_scaleR [simp]; declare scaleR_cancel lemmas [simp]
huffman
parents:
31567
diff
changeset

895 
by (simp add: sgn_div_norm) 
22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

896 

24506  897 
lemma sgn_zero [simp]: "sgn(0::'a::real_normed_vector) = 0" 
898 
by (simp add: sgn_div_norm) 

22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

899 

24506  900 
lemma sgn_zero_iff: "(sgn(x::'a::real_normed_vector) = 0) = (x = 0)" 
901 
by (simp add: sgn_div_norm) 

22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

902 

24506  903 
lemma sgn_minus: "sgn ( x) =  sgn(x::'a::real_normed_vector)" 
904 
by (simp add: sgn_div_norm) 

22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

905 

24506  906 
lemma sgn_scaleR: 
907 
"sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))" 

31586
d4707b99e631
declare norm_scaleR [simp]; declare scaleR_cancel lemmas [simp]
huffman
parents:
31567
diff
changeset

908 
by (simp add: sgn_div_norm mult_ac) 
22973
64d300e16370
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
huffman
parents:
22972
diff
changeset

909 

22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

910 
lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1" 
24506  911 
by (simp add: sgn_div_norm) 
22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

912 

3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

913 
lemma sgn_of_real: 
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

914 
"sgn (of_real r::'a::real_normed_algebra_1) = of_real (sgn r)" 
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

915 
unfolding of_real_def by (simp only: sgn_scaleR sgn_one) 
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

916 

22973
64d300e16370
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
huffman
parents:
22972
diff
changeset

917 
lemma sgn_mult: 
64d300e16370
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
huffman
parents:
22972
diff
changeset

918 
fixes x y :: "'a::real_normed_div_algebra" 
64d300e16370
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
huffman
parents:
22972
diff
changeset

919 
shows "sgn (x * y) = sgn x * sgn y" 
24506  920 
by (simp add: sgn_div_norm norm_mult mult_commute) 
22973
64d300e16370
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
huffman
parents:
22972
diff
changeset

921 

22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

922 
lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>" 
24506  923 
by (simp add: sgn_div_norm divide_inverse) 
22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

924 

3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

925 
lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1" 
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

926 
unfolding real_sgn_eq by simp 
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

927 

3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

928 
lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = 1" 
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

929 
unfolding real_sgn_eq by simp 
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

930 

51474
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset

931 
lemma norm_conv_dist: "norm x = dist x 0" 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset

932 
unfolding dist_norm by simp 
22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22942
diff
changeset

933 

22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

934 
subsection {* Bounded Linear and Bilinear Operators *} 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

935 

53600
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53381
diff
changeset

936 
locale linear = additive f for f :: "'a::real_vector \<Rightarrow> 'b::real_vector" + 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

937 
assumes scaleR: "f (scaleR r x) = scaleR r (f x)" 
53600
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53381
diff
changeset

938 

8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53381
diff
changeset

939 
lemma linearI: 
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53381
diff
changeset

940 
assumes "\<And>x y. f (x + y) = f x + f y" 
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53381
diff
changeset

941 
assumes "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x" 
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53381
diff
changeset

942 
shows "linear f" 
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53381
diff
changeset

943 
by default (rule assms)+ 
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53381
diff
changeset

944 

8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53381
diff
changeset

945 
locale bounded_linear = linear f for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" + 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

946 
assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K" 
27443  947 
begin 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

948 

27443  949 
lemma pos_bounded: 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

950 
"\<exists>K>0. \<forall>x. norm (f x) \<le> norm x * K" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

951 
proof  
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

952 
obtain K where K: "\<And>x. norm (f x) \<le> norm x * K" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

953 
using bounded by fast 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

954 
show ?thesis 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

955 
proof (intro exI impI conjI allI) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

956 
show "0 < max 1 K" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

957 
by (rule order_less_le_trans [OF zero_less_one le_maxI1]) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

958 
next 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

959 
fix x 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

960 
have "norm (f x) \<le> norm x * K" using K . 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

961 
also have "\<dots> \<le> norm x * max 1 K" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

962 
by (rule mult_left_mono [OF le_maxI2 norm_ge_zero]) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

963 
finally show "norm (f x) \<le> norm x * max 1 K" . 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

964 
qed 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

965 
qed 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

966 

27443  967 
lemma nonneg_bounded: 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

968 
"\<exists>K\<ge>0. \<forall>x. norm (f x) \<le> norm x * K" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

969 
proof  
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

970 
from pos_bounded 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

971 
show ?thesis by (auto intro: order_less_imp_le) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

972 
qed 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

973 

27443  974 
end 
975 

44127  976 
lemma bounded_linear_intro: 
977 
assumes "\<And>x y. f (x + y) = f x + f y" 

978 
assumes "\<And>r x. f (scaleR r x) = scaleR r (f x)" 

979 
assumes "\<And>x. norm (f x) \<le> norm x * K" 

980 
shows "bounded_linear f" 

981 
by default (fast intro: assms)+ 

982 

22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

983 
locale bounded_bilinear = 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

984 
fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector] 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

985 
\<Rightarrow> 'c::real_normed_vector" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

986 
(infixl "**" 70) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

987 
assumes add_left: "prod (a + a') b = prod a b + prod a' b" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

988 
assumes add_right: "prod a (b + b') = prod a b + prod a b'" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

989 
assumes scaleR_left: "prod (scaleR r a) b = scaleR r (prod a b)" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

990 
assumes scaleR_right: "prod a (scaleR r b) = scaleR r (prod a b)" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

991 
assumes bounded: "\<exists>K. \<forall>a b. norm (prod a b) \<le> norm a * norm b * K" 
27443  992 
begin 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

993 

27443  994 
lemma pos_bounded: 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

995 
"\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

996 
apply (cut_tac bounded, erule exE) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

997 
apply (rule_tac x="max 1 K" in exI, safe) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

998 
apply (rule order_less_le_trans [OF zero_less_one le_maxI1]) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

999 
apply (drule spec, drule spec, erule order_trans) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1000 
apply (rule mult_left_mono [OF le_maxI2]) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1001 
apply (intro mult_nonneg_nonneg norm_ge_zero) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1002 
done 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1003 

27443  1004 
lemma nonneg_bounded: 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1005 
"\<exists>K\<ge>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1006 
proof  
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1007 
from pos_bounded 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1008 
show ?thesis by (auto intro: order_less_imp_le) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1009 
qed 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1010 

27443  1011 
lemma additive_right: "additive (\<lambda>b. prod a b)" 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1012 
by (rule additive.intro, rule add_right) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1013 

27443  1014 
lemma additive_left: "additive (\<lambda>a. prod a b)" 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1015 
by (rule additive.intro, rule add_left) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1016 

27443  1017 
lemma zero_left: "prod 0 b = 0" 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1018 
by (rule additive.zero [OF additive_left]) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1019 

27443  1020 
lemma zero_right: "prod a 0 = 0" 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1021 
by (rule additive.zero [OF additive_right]) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1022 

27443  1023 
lemma minus_left: "prod ( a) b =  prod a b" 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1024 
by (rule additive.minus [OF additive_left]) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1025 

27443  1026 
lemma minus_right: "prod a ( b) =  prod a b" 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1027 
by (rule additive.minus [OF additive_right]) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1028 

27443  1029 
lemma diff_left: 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1030 
"prod (a  a') b = prod a b  prod a' b" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1031 
by (rule additive.diff [OF additive_left]) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1032 

27443  1033 
lemma diff_right: 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1034 
"prod a (b  b') = prod a b  prod a b'" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1035 
by (rule additive.diff [OF additive_right]) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1036 

27443  1037 
lemma bounded_linear_left: 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1038 
"bounded_linear (\<lambda>a. a ** b)" 
44127  1039 
apply (cut_tac bounded, safe) 
1040 
apply (rule_tac K="norm b * K" in bounded_linear_intro) 

22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1041 
apply (rule add_left) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1042 
apply (rule scaleR_left) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1043 
apply (simp add: mult_ac) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1044 
done 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1045 

27443  1046 
lemma bounded_linear_right: 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1047 
"bounded_linear (\<lambda>b. a ** b)" 
44127  1048 
apply (cut_tac bounded, safe) 
1049 
apply (rule_tac K="norm a * K" in bounded_linear_intro) 

22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1050 
apply (rule add_right) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1051 
apply (rule scaleR_right) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1052 
apply (simp add: mult_ac) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1053 
done 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1054 

27443  1055 
lemma prod_diff_prod: 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1056 
"(x ** y  a ** b) = (x  a) ** (y  b) + (x  a) ** b + a ** (y  b)" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1057 
by (simp add: diff_left diff_right) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1058 

27443  1059 
end 
1060 

51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1061 
lemma bounded_linear_ident[simp]: "bounded_linear (\<lambda>x. x)" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1062 
by default (auto intro!: exI[of _ 1]) 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1063 

400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1064 
lemma bounded_linear_zero[simp]: "bounded_linear (\<lambda>x. 0)" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1065 
by default (auto intro!: exI[of _ 1]) 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1066 

400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1067 
lemma bounded_linear_add: 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1068 
assumes "bounded_linear f" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1069 
assumes "bounded_linear g" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1070 
shows "bounded_linear (\<lambda>x. f x + g x)" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1071 
proof  
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1072 
interpret f: bounded_linear f by fact 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1073 
interpret g: bounded_linear g by fact 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1074 
show ?thesis 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1075 
proof 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1076 
from f.bounded obtain Kf where Kf: "\<And>x. norm (f x) \<le> norm x * Kf" by blast 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1077 
from g.bounded obtain Kg where Kg: "\<And>x. norm (g x) \<le> norm x * Kg" by blast 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1078 
show "\<exists>K. \<forall>x. norm (f x + g x) \<le> norm x * K" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1079 
using add_mono[OF Kf Kg] 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1080 
by (intro exI[of _ "Kf + Kg"]) (auto simp: field_simps intro: norm_triangle_ineq order_trans) 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1081 
qed (simp_all add: f.add g.add f.scaleR g.scaleR scaleR_right_distrib) 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1082 
qed 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1083 

400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1084 
lemma bounded_linear_minus: 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1085 
assumes "bounded_linear f" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1086 
shows "bounded_linear (\<lambda>x.  f x)" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1087 
proof  
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1088 
interpret f: bounded_linear f by fact 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1089 
show ?thesis apply (unfold_locales) 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1090 
apply (simp add: f.add) 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1091 
apply (simp add: f.scaleR) 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1092 
apply (simp add: f.bounded) 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1093 
done 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1094 
qed 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1095 

400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1096 
lemma bounded_linear_compose: 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1097 
assumes "bounded_linear f" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1098 
assumes "bounded_linear g" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1099 
shows "bounded_linear (\<lambda>x. f (g x))" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1100 
proof  
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1101 
interpret f: bounded_linear f by fact 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1102 
interpret g: bounded_linear g by fact 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1103 
show ?thesis proof (unfold_locales) 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1104 
fix x y show "f (g (x + y)) = f (g x) + f (g y)" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1105 
by (simp only: f.add g.add) 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1106 
next 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1107 
fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1108 
by (simp only: f.scaleR g.scaleR) 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1109 
next 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1110 
from f.pos_bounded 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1111 
obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1112 
from g.pos_bounded 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1113 
obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1114 
show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1115 
proof (intro exI allI) 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1116 
fix x 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1117 
have "norm (f (g x)) \<le> norm (g x) * Kf" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1118 
using f . 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1119 
also have "\<dots> \<le> (norm x * Kg) * Kf" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1120 
using g Kf [THEN order_less_imp_le] by (rule mult_right_mono) 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1121 
also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1122 
by (rule mult_assoc) 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1123 
finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" . 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1124 
qed 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1125 
qed 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1126 
qed 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1127 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1128 
lemma bounded_bilinear_mult: 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1129 
"bounded_bilinear (op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)" 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1130 
apply (rule bounded_bilinear.intro) 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47108
diff
changeset

1131 
apply (rule distrib_right) 
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47108
diff
changeset

1132 
apply (rule distrib_left) 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1133 
apply (rule mult_scaleR_left) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1134 
apply (rule mult_scaleR_right) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1135 
apply (rule_tac x="1" in exI) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1136 
apply (simp add: norm_mult_ineq) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1137 
done 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1138 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1139 
lemma bounded_linear_mult_left: 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1140 
"bounded_linear (\<lambda>x::'a::real_normed_algebra. x * y)" 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1141 
using bounded_bilinear_mult 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1142 
by (rule bounded_bilinear.bounded_linear_left) 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1143 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1144 
lemma bounded_linear_mult_right: 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1145 
"bounded_linear (\<lambda>y::'a::real_normed_algebra. x * y)" 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1146 
using bounded_bilinear_mult 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1147 
by (rule bounded_bilinear.bounded_linear_right) 
23127  1148 

51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1149 
lemmas bounded_linear_mult_const = 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1150 
bounded_linear_mult_left [THEN bounded_linear_compose] 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1151 

400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1152 
lemmas bounded_linear_const_mult = 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1153 
bounded_linear_mult_right [THEN bounded_linear_compose] 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1154 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1155 
lemma bounded_linear_divide: 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1156 
"bounded_linear (\<lambda>x::'a::real_normed_field. x / y)" 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1157 
unfolding divide_inverse by (rule bounded_linear_mult_left) 
23120  1158 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1159 
lemma bounded_bilinear_scaleR: "bounded_bilinear scaleR" 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1160 
apply (rule bounded_bilinear.intro) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1161 
apply (rule scaleR_left_distrib) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1162 
apply (rule scaleR_right_distrib) 
22973
64d300e16370
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
huffman
parents:
22972
diff
changeset

1163 
apply simp 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1164 
apply (rule scaleR_left_commute) 
31586
d4707b99e631
declare norm_scaleR [simp]; declare scaleR_cancel lemmas [simp]
huffman
parents:
31567
diff
changeset

1165 
apply (rule_tac x="1" in exI, simp) 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1166 
done 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

1167 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1168 
lemma bounded_linear_scaleR_left: "bounded_linear (\<lambda>r. scaleR r x)" 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1169 
using bounded_bilinear_scaleR 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1170 
by (rule bounded_bilinear.bounded_linear_left) 
23127  1171 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1172 
lemma bounded_linear_scaleR_right: "bounded_linear (\<lambda>x. scaleR r x)" 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1173 
using bounded_bilinear_scaleR 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1174 
by (rule bounded_bilinear.bounded_linear_right) 
23127  1175 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1176 
lemma bounded_linear_of_real: "bounded_linear (\<lambda>r. of_real r)" 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1177 
unfolding of_real_def by (rule bounded_linear_scaleR_left) 
22625  1178 

51642
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1179 
lemma real_bounded_linear: 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1180 
fixes f :: "real \<Rightarrow> real" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1181 
shows "bounded_linear f \<longleftrightarrow> (\<exists>c::real. f = (\<lambda>x. x * c))" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1182 
proof  
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1183 
{ fix x assume "bounded_linear f" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1184 
then interpret bounded_linear f . 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1185 
from scaleR[of x 1] have "f x = x * f 1" 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1186 
by simp } 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1187 
then show ?thesis 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1188 
by (auto intro: exI[of _ "f 1"] bounded_linear_mult_left) 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1189 
qed 
400ec5ae7f8f
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents:
51641
diff
changeset

1190 

44571  1191 
instance real_normed_algebra_1 \<subseteq> perfect_space 
1192 
proof 

1193 
fix x::'a 

1194 
show "\<not> open {x}" 

1195 
unfolding open_dist dist_norm 

1196 
by (clarsimp, rule_tac x="x + of_real (e/2)" in exI, simp) 

1197 
qed 

1198 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1199 
subsection {* Filters and Limits on Metric Space *} 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1200 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1201 
lemma eventually_nhds_metric: 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1202 
fixes a :: "'a :: metric_space" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1203 
shows "eventually P (nhds a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. dist x a < d \<longrightarrow> P x)" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1204 
unfolding eventually_nhds open_dist 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1205 
apply safe 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1206 
apply fast 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1207 
apply (rule_tac x="{x. dist x a < d}" in exI, simp) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1208 
apply clarsimp 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1209 
apply (rule_tac x="d  dist x a" in exI, clarsimp) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1210 
apply (simp only: less_diff_eq) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1211 
apply (erule le_less_trans [OF dist_triangle]) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1212 
done 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1213 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1214 
lemma eventually_at: 
51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51531
diff
changeset

1215 
fixes a :: "'a :: metric_space" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51531
diff
changeset

1216 
shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51531
diff
changeset

1217 
unfolding eventually_at_filter eventually_nhds_metric by (auto simp: dist_nz) 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1218 

51641
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51531
diff
changeset

1219 
lemma eventually_at_le: 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51531
diff
changeset

1220 
fixes a :: "'a::metric_space" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51531
diff
changeset

1221 
shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<and> dist x a \<le> d \<longrightarrow> P x)" 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51531
diff
changeset

1222 
unfolding eventually_at_filter eventually_nhds_metric 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51531
diff
changeset

1223 
apply auto 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51531
diff
changeset

1224 
apply (rule_tac x="d / 2" in exI) 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51531
diff
changeset

1225 
apply auto 
cd05e9fcc63d
remove the withinfilter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51531
diff
changeset

1226 
done 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1227 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1228 
lemma tendstoI: 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1229 
fixes l :: "'a :: metric_space" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1230 
assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1231 
shows "(f > l) F" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1232 
apply (rule topological_tendstoI) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1233 
apply (simp add: open_dist) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1234 
apply (drule (1) bspec, clarify) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1235 
apply (drule assms) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1236 
apply (erule eventually_elim1, simp) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1237 
done 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1238 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1239 
lemma tendstoD: 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1240 
fixes l :: "'a :: metric_space" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1241 
shows "(f > l) F \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1242 
apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1243 
apply (clarsimp simp add: open_dist) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1244 
apply (rule_tac x="e  dist x l" in exI, clarsimp) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1245 
apply (simp only: less_diff_eq) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1246 
apply (erule le_less_trans [OF dist_triangle]) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1247 
apply simp 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51524
diff
changeset

1248 
apply simp 