author  huffman 
Wed, 04 Mar 2009 17:12:23 0800  
changeset 30273  ecd6f0ca62ea 
parent 30242  aea5d7fa7ef5 
child 30729  461ee3e49ad3 
permissions  rwrr 
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
28952
diff
changeset

1 
(* Title: HOL/RealVector.thy 
27552
15cf4ed9c2a1
reremoved subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef
haftmann
parents:
27515
diff
changeset

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

3 
*) 
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 
header {* Vector Spaces and Algebras over the Reals *} 
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

6 

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

7 
theory RealVector 
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
28952
diff
changeset

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

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

10 

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

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

12 

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

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

14 
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

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

17 

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

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

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

21 
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

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

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

24 

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

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

27 
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

28 
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

29 
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

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

31 

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

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

34 

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

38 
apply (simp add: zero) 

39 
apply (simp add: add) 

40 
apply (simp add: zero) 

41 
done 

42 

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

44 

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

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

46 

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

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

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

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

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

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

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

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

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

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

56 

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

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

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

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

60 

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

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

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

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

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

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

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

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

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

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

72 

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

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

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

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

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

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

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

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

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

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

84 

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

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

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

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

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

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

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

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

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

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

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

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

96 

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

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

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

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

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

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

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

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

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

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

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

107 

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

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

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

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

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

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

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

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

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

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

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

118 

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

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

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

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

122 

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

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

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

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

126 

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

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

128 

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

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

130 

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

134 

20763  135 
abbreviation 
25062  136 
divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a" (infixl "'/\<^sub>R" 70) 
24748  137 
where 
25062  138 
"x /\<^sub>R r == scaleR (inverse r) x" 
24748  139 

140 
end 

141 

24588  142 
class real_vector = scaleR + ab_group_add + 
25062  143 
assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y" 
144 
and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x" 

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

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

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

147 

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

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

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

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

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

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

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

156 

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

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

158 

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

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

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

161 
lemmas scaleR_minus_left = real_vector.scale_minus_left 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

162 
lemmas scaleR_left_diff_distrib = real_vector.scale_left_diff_distrib 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

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

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

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

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

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

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

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

171 

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

175 

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

177 

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

179 

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

181 

30069  182 
instantiation real :: real_field 
183 
begin 

184 

185 
definition 

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

187 

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

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

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

190 

30069  191 
end 
192 

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

195 

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

198 

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

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

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

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

203 

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

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

205 
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

206 
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

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

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

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

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

211 

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

212 

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

213 
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

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

215 

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

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

217 
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

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

219 

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

220 
lemma scaleR_conv_of_real: "scaleR r x = of_real r * x" 
20763  221 
by (simp add: of_real_def) 
222 

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

223 
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

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

225 

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

226 
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

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

228 

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

229 
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

230 
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

231 

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

232 
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

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

234 

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

235 
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

236 
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

237 

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

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

240 

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

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

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

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

244 
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

245 

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

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

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

248 
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

249 
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

250 

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

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

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

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

254 
by (simp add: divide_inverse nonzero_of_real_inverse) 
20722  255 

256 
lemma of_real_divide [simp]: 

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

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

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

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

260 

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

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

263 
by (induct n) simp_all 
20722  264 

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

265 
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

266 
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

267 

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

268 
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

269 

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

270 
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

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

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

273 
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

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

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

276 

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

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

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

280 

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

281 
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

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

283 

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

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

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

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

287 

22912  288 
text{*Every real algebra has characteristic zero*} 
289 
instance real_algebra_1 < ring_char_0 

290 
proof 

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

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

292 
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

293 
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

294 
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

295 
by (simp only: of_real_of_nat_eq) 
22912  296 
qed 
297 

27553  298 
instance real_field < field_char_0 .. 
299 

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

300 

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

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

302 

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

304 
Reals :: "'a::real_algebra_1 set" where 
30070
76cee7c62782
declare scaleR distrib rules [algebra_simps]; cleaned up
huffman
parents:
30069
diff
changeset

305 
[code del]: "Reals = range of_real" 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

306 

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

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

309 

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

310 
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

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

312 

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

313 
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

314 
by (subst of_real_of_int_eq [symmetric], rule Reals_of_real) 
20718  315 

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

316 
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

317 
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

318 

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

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

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

321 
by (subst of_real_number_of_eq [symmetric], rule Reals_of_real) 
20718  322 

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

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

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

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

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

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

328 

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

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

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

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

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

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

334 

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

335 
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

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

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

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

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

340 

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

341 
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

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

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

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

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

346 

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

347 
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

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

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

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

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

352 

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

353 
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

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

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

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

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

358 

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

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

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

361 
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

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

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

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

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

366 

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

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

368 
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

369 
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

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

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

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

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

374 

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

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

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

377 
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

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

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

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

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

382 

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

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

384 
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

385 
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

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

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

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

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

390 

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

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

394 
apply (auto simp add: Reals_def) 

395 
apply (rule range_eqI) 

396 
apply (rule of_real_power [symmetric]) 

397 
done 

398 

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

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

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

401 
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

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

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

404 
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

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

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

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

408 

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

409 
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

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

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

412 

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

413 

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

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

415 

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

418 

24520  419 
class sgn_div_norm = scaleR + norm + sgn + 
25062  420 
assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x" 
24506  421 

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

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

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

427 

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

430 

24588  431 
class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra + 
25062  432 
assumes norm_one [simp]: "norm 1 = 1" 
22852  433 

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

436 

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

438 

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

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

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

442 
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

443 
by (simp add: norm_mult) 
22852  444 
next 
445 
have "norm (1 * 1::'a) = norm (1::'a) * norm (1::'a)" 

446 
by (rule norm_mult) 

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

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

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

449 

30069  450 
instantiation real :: real_normed_field 
451 
begin 

452 

453 
definition 

454 
real_norm_def [simp]: "norm r = \<bar>r\<bar>" 

455 

456 
instance 

22852  457 
apply (intro_classes, unfold real_norm_def real_scaleR_def) 
24506  458 
apply (simp add: real_sgn_def) 
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20551
diff
changeset

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

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

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

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

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

465 

30069  466 
end 
467 

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

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

470 

22852  471 
lemma zero_less_norm_iff [simp]: 
472 
fixes x :: "'a::real_normed_vector" 

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

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

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

475 

22852  476 
lemma norm_not_less_zero [simp]: 
477 
fixes x :: "'a::real_normed_vector" 

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

20828  479 
by (simp add: linorder_not_less) 
480 

22852  481 
lemma norm_le_zero_iff [simp]: 
482 
fixes x :: "'a::real_normed_vector" 

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

20828  484 
by (simp add: order_le_less) 
485 

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

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

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

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

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

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

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

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

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

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

496 

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

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

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

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

500 
proof  
22898  501 
have "norm ( (b  a)) = norm (b  a)" 
502 
by (rule norm_minus_cancel) 

503 
thus ?thesis by simp 

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

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

505 

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

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

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

509 
proof  
20533  510 
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

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

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

514 

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

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

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

517 
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

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

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

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

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

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

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

524 

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

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

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

528 
proof  
22898  529 
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

530 
by (rule norm_triangle_ineq) 
22898  531 
thus ?thesis 
532 
by (simp only: diff_minus norm_minus_cancel) 

533 
qed 

534 

535 
lemma norm_diff_ineq: 

536 
fixes a b :: "'a::real_normed_vector" 

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

538 
proof  

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

540 
by (rule norm_triangle_ineq2) 

541 
thus ?thesis by simp 

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

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

543 

20551  544 
lemma norm_diff_triangle_ineq: 
545 
fixes a b c d :: "'a::real_normed_vector" 

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

547 
proof  

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

549 
by (simp add: diff_minus add_ac) 

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

551 
by (rule norm_triangle_ineq) 

552 
finally show ?thesis . 

553 
qed 

554 

22857  555 
lemma abs_norm_cancel [simp]: 
556 
fixes a :: "'a::real_normed_vector" 

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

558 
by (rule abs_of_nonneg [OF norm_ge_zero]) 

559 

22880  560 
lemma norm_add_less: 
561 
fixes x y :: "'a::real_normed_vector" 

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

563 
by (rule order_le_less_trans [OF norm_triangle_ineq add_strict_mono]) 

564 

565 
lemma norm_mult_less: 

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

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

568 
apply (rule order_le_less_trans [OF norm_mult_ineq]) 

569 
apply (simp add: mult_strict_mono') 

570 
done 

571 

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

22852  574 
unfolding of_real_def by (simp add: norm_scaleR) 
20560  575 

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

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

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

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

579 
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

580 

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

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

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

583 
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

584 

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

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

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

587 
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

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

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

590 

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

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

592 
fixes a :: "'a::real_normed_div_algebra" 
20533  593 
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

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

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

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

597 

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

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

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

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

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

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

604 

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

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

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

607 
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

608 
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

609 

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

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

611 
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

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

613 
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

614 

22852  615 
lemma norm_power_ineq: 
616 
fixes x :: "'a::{real_normed_algebra_1,recpower}" 

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

618 
proof (induct n) 

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

620 
next 

621 
case (Suc n) 

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

623 
by (rule norm_mult_ineq) 

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

625 
using norm_ge_zero by (rule mult_left_mono) 

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

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

627 
by simp 
22852  628 
qed 
629 

20684  630 
lemma norm_power: 
631 
fixes x :: "'a::{real_normed_div_algebra,recpower}" 

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

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

633 
by (induct n) (simp_all add: norm_mult) 
20684  634 

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

635 

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

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

637 

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

640 
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

641 

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

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

644 

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

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

647 

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

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

650 

24506  651 
lemma sgn_scaleR: 
652 
"sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))" 

653 
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

654 

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

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

657 

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

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

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

660 
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

661 

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

662 
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

663 
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

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

666 

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

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

669 

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

670 
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

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

672 

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

673 
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

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

675 

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

676 

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

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

678 

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

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

680 
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

681 
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

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

684 

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

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

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

688 
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

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

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

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

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

693 
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

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

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

696 
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

697 
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

698 
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

699 
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

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

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

702 

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

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

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

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

707 
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

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

709 

27443  710 
end 
711 

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

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

713 
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

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

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

716 
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

717 
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

718 
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

719 
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

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

722 

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

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

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

726 
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

727 
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

728 
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

729 
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

730 
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

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

732 

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

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

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

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

737 
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

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

739 

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

741 
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

742 

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

744 
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

745 

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

747 
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

748 

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

750 
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

751 

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

753 
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

754 

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

756 
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

757 

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

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

760 
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

761 

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

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

764 
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

765 

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

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

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

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

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

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

772 
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

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

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

775 

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

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

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

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

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

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

782 
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

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

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

785 

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

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

788 
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

789 

27443  790 
end 
791 

29233  792 
interpretation mult!: 
29229  793 
bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra" 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

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

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

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

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

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

799 
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

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

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

802 

29233  803 
interpretation mult_left!: 
29229  804 
bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)" 
23127  805 
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

806 

29233  807 
interpretation mult_right!: 
29229  808 
bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)" 
23127  809 
by (rule mult.bounded_linear_right) 
810 

29233  811 
interpretation divide!: 
29229  812 
bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)" 
23127  813 
unfolding divide_inverse by (rule mult.bounded_linear_left) 
23120  814 

29233  815 
interpretation scaleR!: bounded_bilinear "scaleR" 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

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

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

818 
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

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

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

821 
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

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

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

824 

29233  825 
interpretation scaleR_left!: bounded_linear "\<lambda>r. scaleR r x" 
23127  826 
by (rule scaleR.bounded_linear_left) 
827 

29233  828 
interpretation scaleR_right!: bounded_linear "\<lambda>x. scaleR r x" 
23127  829 
by (rule scaleR.bounded_linear_right) 
830 

29233  831 
interpretation of_real!: bounded_linear "\<lambda>r. of_real r" 
23127  832 
unfolding of_real_def by (rule scaleR.bounded_linear_left) 
22625  833 

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

834 
end 