author  huffman 
Fri, 11 Jul 2008 16:56:20 +0200  
changeset 27553  d315a513a150 
parent 27552  15cf4ed9c2a1 
child 28009  e93b121074fb 
permissions  rwrr 
27552
15cf4ed9c2a1
reremoved subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef
haftmann
parents:
27515
diff
changeset

1 
(* Title: RealVector.thy 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

2 
ID: $Id$ 
27552
15cf4ed9c2a1
reremoved subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef
haftmann
parents:
27515
diff
changeset

3 
Author: Brian Huffman 
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 

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

8 
theory RealVector 
20684  9 
imports RealPow 
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" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

34 
by (simp add: diff_def add minus) 
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 

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

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

47 

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

51 

20763  52 
abbreviation 
25062  53 
divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a" (infixl "'/\<^sub>R" 70) 
24748  54 
where 
25062  55 
"x /\<^sub>R r == scaleR (inverse r) x" 
24748  56 

57 
end 

58 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

59 
instantiation real :: scaleR 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

60 
begin 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

61 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

62 
definition 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

63 
real_scaleR_def [simp]: "scaleR a x = a * x" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

64 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

65 
instance .. 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

66 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

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

68 

24588  69 
class real_vector = scaleR + ab_group_add + 
25062  70 
assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y" 
71 
and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x" 

24588  72 
and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x" 
73 
and scaleR_one [simp]: "scaleR 1 x = x" 

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

74 

24588  75 
class real_algebra = real_vector + ring + 
25062  76 
assumes mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)" 
77 
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

78 

24588  79 
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

80 

24588  81 
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

82 

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

84 

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

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

86 
apply (intro_classes, unfold real_scaleR_def) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

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

88 
apply (rule left_distrib) 
20763  89 
apply (rule mult_assoc [symmetric]) 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

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

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

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

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

94 

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

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

96 
fixes x :: "'a::real_vector" 
21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

97 
shows "scaleR a (scaleR b x) = scaleR b (scaleR a x)" 
20763  98 
by (simp add: mult_commute) 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

99 

23127  100 
interpretation scaleR_left: additive ["(\<lambda>a. scaleR a x::'a::real_vector)"] 
101 
by unfold_locales (rule scaleR_left_distrib) 

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

102 

23127  103 
interpretation scaleR_right: additive ["(\<lambda>x. scaleR a x::'a::real_vector)"] 
104 
by unfold_locales (rule scaleR_right_distrib) 

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

105 

23127  106 
lemmas scaleR_zero_left [simp] = scaleR_left.zero 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

107 

23127  108 
lemmas scaleR_zero_right [simp] = scaleR_right.zero 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

109 

23127  110 
lemmas scaleR_minus_left [simp] = scaleR_left.minus 
23113
d5cdaa3b7517
interpretations additive_scaleR_left, additive_scaleR_right
huffman
parents:
22973
diff
changeset

111 

23127  112 
lemmas scaleR_minus_right [simp] = scaleR_right.minus 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

113 

23127  114 
lemmas scaleR_left_diff_distrib = scaleR_left.diff 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

115 

23127  116 
lemmas scaleR_right_diff_distrib = scaleR_right.diff 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

117 

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

118 
lemma scaleR_eq_0_iff [simp]: 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

119 
fixes x :: "'a::real_vector" 
21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

120 
shows "(scaleR a x = 0) = (a = 0 \<or> x = 0)" 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

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

122 
assume "a = 0" thus ?thesis by simp 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

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

124 
assume anz [simp]: "a \<noteq> 0" 
21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

125 
{ assume "scaleR a x = 0" 
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

126 
hence "scaleR (inverse a) (scaleR a x) = 0" by simp 
20763  127 
hence "x = 0" by simp } 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

128 
thus ?thesis by force 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

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

130 

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

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

132 
fixes x y :: "'a::real_vector" 
21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

133 
shows "\<lbrakk>a \<noteq> 0; scaleR a x = scaleR a y\<rbrakk> \<Longrightarrow> x = y" 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

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

135 
assume nonzero: "a \<noteq> 0" 
21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

136 
assume "scaleR a x = scaleR a y" 
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

137 
hence "scaleR a (x  y) = 0" 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

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

139 
hence "x  y = 0" by (simp add: nonzero) 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

140 
thus "x = y" by simp 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

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

142 

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

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

144 
fixes x y :: "'a::real_vector" 
21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

145 
shows "\<lbrakk>x \<noteq> 0; scaleR a x = scaleR b x\<rbrakk> \<Longrightarrow> a = b" 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

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

147 
assume nonzero: "x \<noteq> 0" 
21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

148 
assume "scaleR a x = scaleR b x" 
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

149 
hence "scaleR (a  b) x = 0" 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

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

151 
hence "a  b = 0" by (simp add: nonzero) 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

152 
thus "a = b" by simp 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

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

154 

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

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

156 
fixes x y :: "'a::real_vector" 
21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

157 
shows "(scaleR a x = scaleR a y) = (x = y \<or> a = 0)" 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

158 
by (auto intro: scaleR_left_imp_eq) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

159 

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

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

161 
fixes x y :: "'a::real_vector" 
21809
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

162 
shows "(scaleR a x = scaleR b x) = (a = b \<or> x = 0)" 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

163 
by (auto intro: scaleR_right_imp_eq) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

164 

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

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

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

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

169 

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

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

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

172 
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

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

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

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

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

177 

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

178 

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

179 
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

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

181 

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

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

183 
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

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

185 

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

186 
lemma scaleR_conv_of_real: "scaleR r x = of_real r * x" 
20763  187 
by (simp add: of_real_def) 
188 

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

189 
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

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

191 

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

192 
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

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

194 

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

195 
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

196 
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

197 

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

198 
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

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

200 

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

201 
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

202 
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

203 

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

204 
lemma of_real_mult [simp]: "of_real (x * y) = of_real x * of_real y" 
20763  205 
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

206 

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

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

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

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

210 
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

211 

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

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

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

214 
inverse (of_real x :: 'a::{real_div_algebra,division_by_zero})" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

215 
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

216 

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

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

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

219 
(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

220 
by (simp add: divide_inverse nonzero_of_real_inverse) 
20722  221 

222 
lemma of_real_divide [simp]: 

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

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

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

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

226 

20722  227 
lemma of_real_power [simp]: 
228 
"of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1,recpower}) ^ n" 

20772  229 
by (induct n) (simp_all add: power_Suc) 
20722  230 

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

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

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

233 

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

234 
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

235 

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

236 
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

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

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

239 
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

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

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

242 

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

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

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

246 

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

247 
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

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

249 

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

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

251 
"of_real (number_of w) = (number_of w :: 'a::{number_ring,real_algebra_1})" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

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

253 

22912  254 
text{*Every real algebra has characteristic zero*} 
255 
instance real_algebra_1 < ring_char_0 

256 
proof 

23282
dfc459989d24
add axclass semiring_char_0 for types where of_nat is injective
huffman
parents:
23127
diff
changeset

257 
fix m n :: nat 
dfc459989d24
add axclass semiring_char_0 for types where of_nat is injective
huffman
parents:
23127
diff
changeset

258 
have "(of_real (of_nat m) = (of_real (of_nat n)::'a)) = (m = n)" 
dfc459989d24
add axclass semiring_char_0 for types where of_nat is injective
huffman
parents:
23127
diff
changeset

259 
by (simp only: of_real_eq_iff of_nat_eq_iff) 
dfc459989d24
add axclass semiring_char_0 for types where of_nat is injective
huffman
parents:
23127
diff
changeset

260 
thus "(of_nat m = (of_nat n::'a)) = (m = n)" 
dfc459989d24
add axclass semiring_char_0 for types where of_nat is injective
huffman
parents:
23127
diff
changeset

261 
by (simp only: of_real_of_nat_eq) 
22912  262 
qed 
263 

27553  264 
instance real_field < field_char_0 .. 
265 

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

266 

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

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

268 

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

270 
Reals :: "'a::real_algebra_1 set" where 
27435  271 
[code func del]: "Reals \<equiv> range of_real" 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

272 

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

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

275 

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

276 
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

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

278 

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

279 
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

280 
by (subst of_real_of_int_eq [symmetric], rule Reals_of_real) 
20718  281 

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

282 
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

283 
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

284 

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

285 
lemma Reals_number_of [simp]: 
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

286 
"(number_of w::'a::{number_ring,real_algebra_1}) \<in> Reals" 
4b93e949ac33
remove uses of scaleR infix syntax; add lemma Reals_number_of
huffman
parents:
21404
diff
changeset

287 
by (subst of_real_number_of_eq [symmetric], rule Reals_of_real) 
20718  288 

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

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

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

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

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

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

294 

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

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

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

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

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

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

300 

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

301 
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

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

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

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

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

306 

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

307 
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

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

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

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

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

312 

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

313 
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

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

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

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

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

318 

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

319 
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

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

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

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

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

324 

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

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

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

327 
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

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

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

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

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

332 

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

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

334 
fixes a :: "'a::{real_div_algebra,division_by_zero}" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

335 
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

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

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

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

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

340 

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

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

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

343 
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

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

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

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

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

348 

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

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

350 
fixes a b :: "'a::{real_field,division_by_zero}" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

351 
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

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

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

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

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

356 

20722  357 
lemma Reals_power [simp]: 
358 
fixes a :: "'a::{real_algebra_1,recpower}" 

359 
shows "a \<in> Reals \<Longrightarrow> a ^ n \<in> Reals" 

360 
apply (auto simp add: Reals_def) 

361 
apply (rule range_eqI) 

362 
apply (rule of_real_power [symmetric]) 

363 
done 

364 

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

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

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

367 
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

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

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

370 
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

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

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

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

374 

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

375 
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

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

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

378 

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

379 

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

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

381 

22636  382 
class norm = type + 
383 
fixes norm :: "'a \<Rightarrow> real" 

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

384 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

385 
instantiation real :: norm 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

386 
begin 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

387 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

388 
definition 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

389 
real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

390 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

391 
instance .. 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

392 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25062
diff
changeset

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

394 

24520  395 
class sgn_div_norm = scaleR + norm + sgn + 
25062  396 
assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x" 
24506  397 

24588  398 
class real_normed_vector = real_vector + sgn_div_norm + 
399 
assumes norm_ge_zero [simp]: "0 \<le> norm x" 

25062  400 
and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0" 
401 
and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y" 

24588  402 
and norm_scaleR: "norm (scaleR a x) = \<bar>a\<bar> * norm x" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

403 

24588  404 
class real_normed_algebra = real_algebra + real_normed_vector + 
25062  405 
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

406 

24588  407 
class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra + 
25062  408 
assumes norm_one [simp]: "norm 1 = 1" 
22852  409 

24588  410 
class real_normed_div_algebra = real_div_algebra + real_normed_vector + 
25062  411 
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

412 

24588  413 
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

414 

22852  415 
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

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

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

418 
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

419 
by (simp add: norm_mult) 
22852  420 
next 
421 
have "norm (1 * 1::'a) = norm (1::'a) * norm (1::'a)" 

422 
by (rule norm_mult) 

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

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

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

425 

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

426 
instance real :: real_normed_field 
22852  427 
apply (intro_classes, unfold real_norm_def real_scaleR_def) 
24506  428 
apply (simp add: real_sgn_def) 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

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

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

431 
apply (rule abs_triangle_ineq) 
22852  432 
apply (rule abs_mult) 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

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

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

435 

22852  436 
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

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

438 

22852  439 
lemma zero_less_norm_iff [simp]: 
440 
fixes x :: "'a::real_normed_vector" 

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

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

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

443 

22852  444 
lemma norm_not_less_zero [simp]: 
445 
fixes x :: "'a::real_normed_vector" 

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

20828  447 
by (simp add: linorder_not_less) 
448 

22852  449 
lemma norm_le_zero_iff [simp]: 
450 
fixes x :: "'a::real_normed_vector" 

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

20828  452 
by (simp add: order_le_less) 
453 

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

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

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

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

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

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

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

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

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

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

464 

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

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

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

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

468 
proof  
22898  469 
have "norm ( (b  a)) = norm (b  a)" 
470 
by (rule norm_minus_cancel) 

471 
thus ?thesis by simp 

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

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

473 

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

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

475 
fixes a b :: "'a::real_normed_vector" 
20533  476 
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

477 
proof  
20533  478 
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

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

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

482 

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

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

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

485 
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

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

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

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

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

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

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

492 

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

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

494 
fixes a b :: "'a::real_normed_vector" 
20533  495 
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

496 
proof  
22898  497 
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

498 
by (rule norm_triangle_ineq) 
22898  499 
thus ?thesis 
500 
by (simp only: diff_minus norm_minus_cancel) 

501 
qed 

502 

503 
lemma norm_diff_ineq: 

504 
fixes a b :: "'a::real_normed_vector" 

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

506 
proof  

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

508 
by (rule norm_triangle_ineq2) 

509 
thus ?thesis by simp 

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

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

511 

20551  512 
lemma norm_diff_triangle_ineq: 
513 
fixes a b c d :: "'a::real_normed_vector" 

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

515 
proof  

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

517 
by (simp add: diff_minus add_ac) 

518 
also have "\<dots> \<le> norm (a  c) + norm (b  d)" 

519 
by (rule norm_triangle_ineq) 

520 
finally show ?thesis . 

521 
qed 

522 

22857  523 
lemma abs_norm_cancel [simp]: 
524 
fixes a :: "'a::real_normed_vector" 

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

526 
by (rule abs_of_nonneg [OF norm_ge_zero]) 

527 

22880  528 
lemma norm_add_less: 
529 
fixes x y :: "'a::real_normed_vector" 

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

531 
by (rule order_le_less_trans [OF norm_triangle_ineq add_strict_mono]) 

532 

533 
lemma norm_mult_less: 

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

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

536 
apply (rule order_le_less_trans [OF norm_mult_ineq]) 

537 
apply (simp add: mult_strict_mono') 

538 
done 

539 

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

22852  542 
unfolding of_real_def by (simp add: norm_scaleR) 
20560  543 

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

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

545 
"norm (number_of w::'a::{number_ring,real_normed_algebra_1}) 
2b4c831ceca7
add lemmas norm_number_of, norm_of_int, norm_of_nat
huffman
parents:
22857
diff
changeset

546 
= \<bar>number_of w\<bar>" 
2b4c831ceca7
add lemmas norm_number_of, norm_of_int, norm_of_nat
huffman
parents:
22857
diff
changeset

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

548 

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

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

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

551 
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

552 

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

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

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

555 
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

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

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

558 

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

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

560 
fixes a :: "'a::real_normed_div_algebra" 
20533  561 
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

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

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

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

565 

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

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

567 
fixes a :: "'a::{real_normed_div_algebra,division_by_zero}" 
20533  568 
shows "norm (inverse a) = inverse (norm a)" 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

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

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

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

572 

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

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

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

575 
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

576 
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

577 

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

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

579 
fixes a b :: "'a::{real_normed_field,division_by_zero}" 
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20560
diff
changeset

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

581 
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

582 

22852  583 
lemma norm_power_ineq: 
584 
fixes x :: "'a::{real_normed_algebra_1,recpower}" 

585 
shows "norm (x ^ n) \<le> norm x ^ n" 

586 
proof (induct n) 

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

588 
next 

589 
case (Suc n) 

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

591 
by (rule norm_mult_ineq) 

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

593 
using norm_ge_zero by (rule mult_left_mono) 

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

595 
by (simp add: power_Suc) 

596 
qed 

597 

20684  598 
lemma norm_power: 
599 
fixes x :: "'a::{real_normed_div_algebra,recpower}" 

600 
shows "norm (x ^ n) = norm x ^ n" 

20772  601 
by (induct n) (simp_all add: power_Suc norm_mult) 
20684  602 

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

603 

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

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

605 

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

608 
by (simp add: sgn_div_norm norm_scaleR) 

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

609 

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

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

612 

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

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

615 

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

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

618 

24506  619 
lemma sgn_scaleR: 
620 
"sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))" 

621 
by (simp add: sgn_div_norm norm_scaleR 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

622 

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

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

625 

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

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

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

628 
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

629 

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

630 
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

631 
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

632 
shows "sgn (x * y) = sgn x * sgn y" 
24506  633 
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

634 

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

635 
lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>" 
24506  636 
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

637 

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

638 
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

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

640 

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

641 
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

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

643 

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

644 

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

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

646 

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

647 
locale bounded_linear = additive + 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

648 
constrains f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

649 
assumes scaleR: "f (scaleR r x) = scaleR r (f x)" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

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

652 

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

654 
"\<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

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

656 
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

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

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

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

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

661 
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

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

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

664 
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

665 
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

666 
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

667 
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

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

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

670 

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

672 
"\<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

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

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

675 
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

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

677 

27443  678 
end 
679 

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

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

681 
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

682 
\<Rightarrow> 'c::real_normed_vector" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

683 
(infixl "**" 70) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

684 
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

685 
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

686 
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

687 
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

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

690 

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

692 
"\<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

693 
apply (cut_tac bounded, erule exE) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

694 
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

695 
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

696 
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

697 
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

698 
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

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

700 

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

702 
"\<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

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

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

705 
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

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

707 

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

709 
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

710 

27443  711 
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

712 
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

713 

27443  714 
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

715 
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

716 

27443  717 
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

718 
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

719 

27443  720 
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

721 
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

722 

27443  723 
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

724 
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

725 

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

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

728 
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

729 

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

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

732 
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

733 

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

735 
"bounded_linear (\<lambda>a. a ** b)" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

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

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

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

739 
apply (cut_tac bounded, safe) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

740 
apply (rule_tac x="norm b * K" in exI) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

741 
apply (simp add: mult_ac) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

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

743 

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

745 
"bounded_linear (\<lambda>b. a ** b)" 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

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

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

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

749 
apply (cut_tac bounded, safe) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

750 
apply (rule_tac x="norm a * K" in exI) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

751 
apply (simp add: mult_ac) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

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

753 

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

755 
"(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

756 
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

757 

27443  758 
end 
759 

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

761 
bounded_bilinear ["op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"] 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

762 
apply (rule bounded_bilinear.intro) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

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

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

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

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

767 
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

768 
apply (simp add: norm_mult_ineq) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

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

770 

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

772 
bounded_linear ["(\<lambda>x::'a::real_normed_algebra. x * y)"] 
23127  773 
by (rule mult.bounded_linear_left) 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

774 

23127  775 
interpretation mult_right: 
776 
bounded_linear ["(\<lambda>y::'a::real_normed_algebra. x * y)"] 

777 
by (rule mult.bounded_linear_right) 

778 

779 
interpretation divide: 

23120  780 
bounded_linear ["(\<lambda>x::'a::real_normed_field. x / y)"] 
23127  781 
unfolding divide_inverse by (rule mult.bounded_linear_left) 
23120  782 

23127  783 
interpretation scaleR: bounded_bilinear ["scaleR"] 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

784 
apply (rule bounded_bilinear.intro) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

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

786 
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

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

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

789 
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

790 
apply (simp add: norm_scaleR) 
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

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

792 

23127  793 
interpretation scaleR_left: bounded_linear ["\<lambda>r. scaleR r x"] 
794 
by (rule scaleR.bounded_linear_left) 

795 

796 
interpretation scaleR_right: bounded_linear ["\<lambda>x. scaleR r x"] 

797 
by (rule scaleR.bounded_linear_right) 

798 

799 
interpretation of_real: bounded_linear ["\<lambda>r. of_real r"] 

800 
unfolding of_real_def by (rule scaleR.bounded_linear_left) 

22625  801 

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

802 
end 