author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47108  2a1953f0d20d 
child 49962  a8cc904a6820 
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 
36839
34dc65df7014
no more RealPow.thy (remaining lemmas moved to RealDef.thy)
huffman
parents:
36795
diff
changeset

8 
imports RComplete 
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" 
37887  33 
by (simp add: add minus diff_minus) 
20504
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" 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

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

66 
proof  
29229  67 
interpret s: additive "\<lambda>a. scale a x" 
28823  68 
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

69 
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

70 
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

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

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

73 
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

74 

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

75 
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

76 
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

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

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

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

80 
proof  
29229  81 
interpret s: additive "\<lambda>x. scale a x" 
28823  82 
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

83 
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

84 
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

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

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

87 
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

88 

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

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

91 
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

92 
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

93 
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

94 
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

95 
{ 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

96 
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

97 
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

98 
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

99 
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

100 

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

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

103 
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

104 
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

105 
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

106 
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

107 
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

108 
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

109 
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

110 
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

111 

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

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

114 
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

115 
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

116 
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

117 
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

118 
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

119 
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

120 
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

121 
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

122 

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

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

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

125 
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

126 

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

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

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

129 
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

130 

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

131 
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

132 

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

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

134 

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

138 

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

144 
end 

145 

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

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

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

149 
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

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

151 

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

152 
interpretation real_vector: 
29229  153 
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

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

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

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

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

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

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

160 

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

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

162 

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

163 
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

164 
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

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

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

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

168 
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

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

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

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

172 
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

173 
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

174 
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

175 
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

176 
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

177 

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

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

179 

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

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

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

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

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

184 

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

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

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

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

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

189 

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

193 

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

195 

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

197 

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

199 

30069  200 
instantiation real :: real_field 
201 
begin 

202 

203 
definition 

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

205 

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

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

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

208 

30069  209 
end 
210 

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

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

213 

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

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

216 

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

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

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

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

221 

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

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

224 
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

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

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

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

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

229 

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

230 

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

231 
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

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

233 

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

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

235 
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

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

237 

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

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

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

241 
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

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

243 

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

244 
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

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

246 

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

247 
lemma of_real_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

248 
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

249 

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

250 
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

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

252 

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

253 
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

254 
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

255 

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

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

258 

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

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

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

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

262 
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

263 

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

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

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

267 
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

268 

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

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

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

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

272 
by (simp add: divide_inverse nonzero_of_real_inverse) 
20722  273 

274 
lemma of_real_divide [simp]: 

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

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

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

278 

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

281 
by (induct n) simp_all 
20722  282 

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

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

285 

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

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

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

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

289 

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

290 
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

291 

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

292 
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

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

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

295 
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

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

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

298 

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

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

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

302 

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

303 
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

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

305 

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

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

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

308 

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

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

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

311 

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

313 

22912  314 
instance real_algebra_1 < ring_char_0 
315 
proof 

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

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

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

27553  320 
instance real_field < field_char_0 .. 
321 

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

322 

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

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

324 

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

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

327 

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

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

330 

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

331 
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

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

333 

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

334 
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

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

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

337 
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

338 
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

339 

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

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

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

342 

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

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

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

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

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

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

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

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

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

351 

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

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

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

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

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

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

357 

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

358 
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

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

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

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

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

363 

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

364 
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

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

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

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

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

369 

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

370 
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

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

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

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

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

375 

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

376 
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

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

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

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

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

381 

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

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

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

384 
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

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

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

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

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

389 

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

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

392 
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

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

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

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

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

397 

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

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

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

400 
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

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

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

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

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

405 

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

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

408 
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

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

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

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

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

413 

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

418 
apply (rule range_eqI) 

419 
apply (rule of_real_power [symmetric]) 

420 
done 

421 

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

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

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

424 
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

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

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

427 
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

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

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

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

431 

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

432 
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

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

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

435 

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

436 

31413
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

437 
subsection {* Topological spaces *} 
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

438 

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

439 
class "open" = 
31494  440 
fixes "open" :: "'a set \<Rightarrow> bool" 
31490
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

441 

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

442 
class topological_space = "open" + 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

443 
assumes open_UNIV [simp, intro]: "open UNIV" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

444 
assumes open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

445 
assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union> K)" 
31490
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

446 
begin 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

447 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

448 
definition 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

449 
closed :: "'a set \<Rightarrow> bool" where 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

450 
"closed S \<longleftrightarrow> open ( S)" 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

451 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

452 
lemma open_empty [intro, simp]: "open {}" 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

453 
using open_Union [of "{}"] by simp 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

454 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

455 
lemma open_Un [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)" 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

456 
using open_Union [of "{S, T}"] by simp 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

457 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

458 
lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)" 
44937
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44571
diff
changeset

459 
unfolding SUP_def by (rule open_Union) auto 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44571
diff
changeset

460 

22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44571
diff
changeset

461 
lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)" 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44571
diff
changeset

462 
by (induct set: finite) auto 
31490
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

463 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

464 
lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)" 
44937
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44571
diff
changeset

465 
unfolding INF_def by (rule open_Inter) auto 
31490
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

466 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

467 
lemma closed_empty [intro, simp]: "closed {}" 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

468 
unfolding closed_def by simp 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

469 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

470 
lemma closed_Un [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)" 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

471 
unfolding closed_def by auto 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

472 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

473 
lemma closed_UNIV [intro, simp]: "closed UNIV" 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

474 
unfolding closed_def by simp 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

475 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

476 
lemma closed_Int [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<inter> T)" 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

477 
unfolding closed_def by auto 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

478 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

479 
lemma closed_INT [intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)" 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

480 
unfolding closed_def by auto 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

481 

44937
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44571
diff
changeset

482 
lemma closed_Inter [intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)" 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44571
diff
changeset

483 
unfolding closed_def uminus_Inf by auto 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44571
diff
changeset

484 

22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44571
diff
changeset

485 
lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)" 
31490
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

486 
by (induct set: finite) auto 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

487 

44937
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44571
diff
changeset

488 
lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)" 
22c0857b8aab
removed further legacy rules from Complete_Lattices
hoelzl
parents:
44571
diff
changeset

489 
unfolding SUP_def by (rule closed_Union) auto 
31490
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

490 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

491 
lemma open_closed: "open S \<longleftrightarrow> closed ( S)" 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

492 
unfolding closed_def by simp 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

493 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

494 
lemma closed_open: "closed S \<longleftrightarrow> open ( S)" 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

495 
unfolding closed_def by simp 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

496 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

497 
lemma open_Diff [intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S  T)" 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

498 
unfolding closed_open Diff_eq by (rule open_Int) 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

499 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

500 
lemma closed_Diff [intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed (S  T)" 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

501 
unfolding open_closed Diff_eq by (rule closed_Int) 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

502 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

503 
lemma open_Compl [intro]: "closed S \<Longrightarrow> open ( S)" 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

504 
unfolding closed_open . 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

505 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

506 
lemma closed_Compl [intro]: "open S \<Longrightarrow> closed ( S)" 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

507 
unfolding open_closed . 
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

508 

c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31446
diff
changeset

509 
end 
31413
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

510 

729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

511 

31289  512 
subsection {* Metric spaces *} 
513 

514 
class dist = 

515 
fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real" 

516 

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

517 
class open_dist = "open" + dist + 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

518 
assumes open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" 
31413
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

519 

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

520 
class metric_space = open_dist + 
31289  521 
assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y" 
522 
assumes dist_triangle2: "dist x y \<le> dist x z + dist y z" 

523 
begin 

524 

525 
lemma dist_self [simp]: "dist x x = 0" 

526 
by simp 

527 

528 
lemma zero_le_dist [simp]: "0 \<le> dist x y" 

529 
using dist_triangle2 [of x x y] by simp 

530 

531 
lemma zero_less_dist_iff: "0 < dist x y \<longleftrightarrow> x \<noteq> y" 

532 
by (simp add: less_le) 

533 

534 
lemma dist_not_less_zero [simp]: "\<not> dist x y < 0" 

535 
by (simp add: not_less) 

536 

537 
lemma dist_le_zero_iff [simp]: "dist x y \<le> 0 \<longleftrightarrow> x = y" 

538 
by (simp add: le_less) 

539 

540 
lemma dist_commute: "dist x y = dist y x" 

541 
proof (rule order_antisym) 

542 
show "dist x y \<le> dist y x" 

543 
using dist_triangle2 [of x y x] by simp 

544 
show "dist y x \<le> dist x y" 

545 
using dist_triangle2 [of y x y] by simp 

546 
qed 

547 

548 
lemma dist_triangle: "dist x z \<le> dist x y + dist y z" 

549 
using dist_triangle2 [of x z y] by (simp add: dist_commute) 

550 

31565  551 
lemma dist_triangle3: "dist x y \<le> dist a x + dist a y" 
552 
using dist_triangle2 [of x y a] by (simp add: dist_commute) 

553 

41969  554 
lemma dist_triangle_alt: 
555 
shows "dist y z <= dist x y + dist x z" 

556 
by (rule dist_triangle3) 

557 

558 
lemma dist_pos_lt: 

559 
shows "x \<noteq> y ==> 0 < dist x y" 

560 
by (simp add: zero_less_dist_iff) 

561 

562 
lemma dist_nz: 

563 
shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y" 

564 
by (simp add: zero_less_dist_iff) 

565 

566 
lemma dist_triangle_le: 

567 
shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e" 

568 
by (rule order_trans [OF dist_triangle2]) 

569 

570 
lemma dist_triangle_lt: 

571 
shows "dist x z + dist y z < e ==> dist x y < e" 

572 
by (rule le_less_trans [OF dist_triangle2]) 

573 

574 
lemma dist_triangle_half_l: 

575 
shows "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e" 

576 
by (rule dist_triangle_lt [where z=y], simp) 

577 

578 
lemma dist_triangle_half_r: 

579 
shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e" 

580 
by (rule dist_triangle_half_l, simp_all add: dist_commute) 

581 

31413
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

582 
subclass topological_space 
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

583 
proof 
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

584 
have "\<exists>e::real. 0 < e" 
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

585 
by (fast intro: zero_less_one) 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

586 
then show "open UNIV" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

587 
unfolding open_dist by simp 
31413
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

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

589 
fix S T assume "open S" "open T" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

590 
then show "open (S \<inter> T)" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

591 
unfolding open_dist 
31413
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

592 
apply clarify 
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

593 
apply (drule (1) bspec)+ 
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

594 
apply (clarify, rename_tac r s) 
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

595 
apply (rule_tac x="min r s" in exI, simp) 
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

596 
done 
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

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

598 
fix K assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)" 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

599 
unfolding open_dist by fast 
31413
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

600 
qed 
729d90a531e4
introduce class topological_space as a superclass of metric_space
huffman
parents:
31289
diff
changeset

601 

41969  602 
lemma (in metric_space) open_ball: "open {y. dist x y < d}" 
603 
proof (unfold open_dist, intro ballI) 

604 
fix y assume *: "y \<in> {y. dist x y < d}" 

605 
then show "\<exists>e>0. \<forall>z. dist z y < e \<longrightarrow> z \<in> {y. dist x y < d}" 

606 
by (auto intro!: exI[of _ "d  dist x y"] simp: field_simps dist_triangle_lt) 

607 
qed 

608 

31289  609 
end 
610 

611 

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

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

613 

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

616 

24520  617 
class sgn_div_norm = scaleR + norm + sgn + 
25062  618 
assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x" 
24506  619 

31289  620 
class dist_norm = dist + norm + minus + 
621 
assumes dist_norm: "dist x y = norm (x  y)" 

622 

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

623 
class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_dist + 
24588  624 
assumes norm_ge_zero [simp]: "0 \<le> norm x" 
25062  625 
and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0" 
626 
and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y" 

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

627 
and norm_scaleR [simp]: "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

628 

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

631 

24588  632 
class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra + 
25062  633 
assumes norm_one [simp]: "norm 1 = 1" 
22852  634 

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

637 

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

639 

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

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

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

643 
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

644 
by (simp add: norm_mult) 
22852  645 
next 
646 
have "norm (1 * 1::'a) = norm (1::'a) * norm (1::'a)" 

647 
by (rule norm_mult) 

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

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

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

650 

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

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

653 

22852  654 
lemma zero_less_norm_iff [simp]: 
655 
fixes x :: "'a::real_normed_vector" 

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

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

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

658 

22852  659 
lemma norm_not_less_zero [simp]: 
660 
fixes x :: "'a::real_normed_vector" 

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

20828  662 
by (simp add: linorder_not_less) 
663 

22852  664 
lemma norm_le_zero_iff [simp]: 
665 
fixes x :: "'a::real_normed_vector" 

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

20828  667 
by (simp add: order_le_less) 
668 

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

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

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

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

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

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

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

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

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

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

679 

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

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

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

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

683 
proof  
22898  684 
have "norm ( (b  a)) = norm (b  a)" 
685 
by (rule norm_minus_cancel) 

686 
thus ?thesis by simp 

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

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

688 

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

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

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

692 
proof  
20533  693 
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

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

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

697 

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

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

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

700 
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

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

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

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

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

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

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

707 

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

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

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

711 
proof  
22898  712 
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

713 
by (rule norm_triangle_ineq) 
22898  714 
thus ?thesis 
715 
by (simp only: diff_minus norm_minus_cancel) 

716 
qed 

717 

718 
lemma norm_diff_ineq: 

719 
fixes a b :: "'a::real_normed_vector" 

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

721 
proof  

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

723 
by (rule norm_triangle_ineq2) 

724 
thus ?thesis by simp 

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

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

726 

20551  727 
lemma norm_diff_triangle_ineq: 
728 
fixes a b c d :: "'a::real_normed_vector" 

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

730 
proof  

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

732 
by (simp add: diff_minus add_ac) 

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

734 
by (rule norm_triangle_ineq) 

735 
finally show ?thesis . 

736 
qed 

737 

22857  738 
lemma abs_norm_cancel [simp]: 
739 
fixes a :: "'a::real_normed_vector" 

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

741 
by (rule abs_of_nonneg [OF norm_ge_zero]) 

742 

22880  743 
lemma norm_add_less: 
744 
fixes x y :: "'a::real_normed_vector" 

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

746 
by (rule order_le_less_trans [OF norm_triangle_ineq add_strict_mono]) 

747 

748 
lemma norm_mult_less: 

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

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

751 
apply (rule order_le_less_trans [OF norm_mult_ineq]) 

752 
apply (simp add: mult_strict_mono') 

753 
done 

754 

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

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

757 
unfolding of_real_def by simp 
20560  758 

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

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

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

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

762 

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

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

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

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

766 

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

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

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

769 
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

770 

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

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

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

773 
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

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

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

776 

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

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

778 
fixes a :: "'a::real_normed_div_algebra" 
20533  779 
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

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

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

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

783 

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

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

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

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

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

790 

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

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

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

793 
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

794 
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

795 

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

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

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

799 
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

800 

22852  801 
lemma norm_power_ineq: 
31017  802 
fixes x :: "'a::{real_normed_algebra_1}" 
22852  803 
shows "norm (x ^ n) \<le> norm x ^ n" 
804 
proof (induct n) 

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

806 
next 

807 
case (Suc n) 

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

809 
by (rule norm_mult_ineq) 

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

811 
using norm_ge_zero by (rule mult_left_mono) 

812 
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

813 
by simp 
22852  814 
qed 
815 

20684  816 
lemma norm_power: 
31017  817 
fixes x :: "'a::{real_normed_div_algebra}" 
20684  818 
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

819 
by (induct n) (simp_all add: norm_mult) 
20684  820 

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

822 

31289  823 
instance real_normed_vector < metric_space 
824 
proof 

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

826 
unfolding dist_norm by simp 

827 
next 

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

829 
unfolding dist_norm 

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

831 
qed 

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

832 

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

833 

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

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

835 

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

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

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

838 

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

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

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

841 

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

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

843 
"dist x y = \<bar>x  y\<bar>" 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

844 

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

846 
"open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

847 

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

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

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

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

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

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

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

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

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

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

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

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

859 

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

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

861 

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

862 
lemma open_real_lessThan [simp]: 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

863 
fixes a :: real shows "open {..<a}" 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

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

865 
proof (clarify) 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

866 
fix x assume "x < a" 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

867 
hence "0 < a  x \<and> (\<forall>y. \<bar>y  x\<bar> < a  x \<longrightarrow> y \<in> {..<a})" by auto 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

868 
thus "\<exists>e>0. \<forall>y. \<bar>y  x\<bar> < e \<longrightarrow> y \<in> {..<a}" .. 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

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

870 

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

871 
lemma open_real_greaterThan [simp]: 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

872 
fixes a :: real shows "open {a<..}" 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

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

874 
proof (clarify) 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

875 
fix x assume "a < x" 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

876 
hence "0 < x  a \<and> (\<forall>y. \<bar>y  x\<bar> < x  a \<longrightarrow> y \<in> {a<..})" by auto 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

877 
thus "\<exists>e>0. \<forall>y. \<bar>y  x\<bar> < e \<longrightarrow> y \<in> {a<..}" .. 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

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

879 

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

880 
lemma open_real_greaterThanLessThan [simp]: 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

881 
fixes a b :: real shows "open {a<..<b}" 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

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

883 
have "{a<..<b} = {a<..} \<inter> {..<b}" by auto 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

884 
thus "open {a<..<b}" by (simp add: open_Int) 
d2abf6f6f619
subsection for real instances; new lemmas for open sets of reals
huffman
parents:
31494
diff
changeset

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

886 

31567  887 
lemma closed_real_atMost [simp]: 
888 
fixes a :: real shows "closed {..a}" 

889 
unfolding closed_open by simp 

890 

891 
lemma closed_real_atLeast [simp]: 

892 
fixes a :: real shows "closed {a..}" 

893 
unfolding closed_open by simp 

894 

895 
lemma closed_real_atLeastAtMost [simp]: 

896 
fixes a b :: real shows "closed {a..b}" 

897 
proof  

898 
have "{a..b} = {a..} \<inter> {..b}" by auto 

899 
thus "closed {a..b}" by (simp add: closed_Int) 

900 
qed 

901 

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

902 

31446  903 
subsection {* Extra type constraints *} 
904 

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

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

906 

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

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

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

909 

31446  910 
text {* Only allow @{term dist} in class @{text metric_space}. *} 
911 

912 
setup {* Sign.add_const_constraint 

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

914 

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

916 

917 
setup {* Sign.add_const_constraint 

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

919 

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

920 

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

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

922 

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

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

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

926 

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

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

929 

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

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

932 

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

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

935 

24506  936 
lemma sgn_scaleR: 
937 
"sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))" 

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

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

939 

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

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

942 

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

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

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

945 
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

946 

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

947 
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

948 
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

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

951 

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

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

954 

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

955 
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

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

957 

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

958 
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

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

960 

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

961 

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

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

963 

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

965 
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

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

968 

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

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

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

972 
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

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

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

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

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

977 
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

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

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

980 
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

981 
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

982 
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

983 
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

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

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

986 

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

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

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

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

991 
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

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

993 

27443  994 
end 
995 

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

998 
assumes "\<And>r x. f (scaleR r x) = scaleR r (f x)" 

999 
assumes "\<And>x. norm (f x) \<le> norm x * K" 

1000 
shows "bounded_linear f" 

1001 
by default (fast intro: assms)+ 

1002 

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

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

1004 
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

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

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

1007 
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

1008 
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

1009 
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

1010 
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

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

1013 

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

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

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

1017 
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

1018 
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

1019 
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

1020 
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

1021 
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

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

1023 

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

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

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

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

1028 
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

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

1030 

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

1032 
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

1033 

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

1035 
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

1036 

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

1038 
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

1039 

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

1041 
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

1042 

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

1044 
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

1045 

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

1047 
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

1048 

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

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

1051 
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

1052 

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

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

1055 
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

1056 

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

1058 
"bounded_linear (\<lambda>a. a ** b)" 
44127  1059 
apply (cut_tac bounded, safe) 
1060 
apply (rule_tac K="norm b * K" in bounded_linear_intro) 

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

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

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

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

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

1065 

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

1067 
"bounded_linear (\<lambda>b. a ** b)" 
44127  1068 
apply (cut_tac bounded, safe) 
1069 
apply (rule_tac K="norm a * K" in bounded_linear_intro) 

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

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

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

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

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

1074 

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

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

1077 
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

1078 

27443  1079 
end 
1080 

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

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

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

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

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

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

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

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

1088 
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

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

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

1091 

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

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

1093 
"bounded_linear (\<lambda>x::'a::real_normed_algebra. x * y)" 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

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

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

1096 

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

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

1098 
"bounded_linear (\<lambda>y::'a::real_normed_algebra. x * y)" 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

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

1100 
by (rule bounded_bilinear.bounded_linear_right) 
23127  1101 

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

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

1103 
"bounded_linear (\<lambda>x::'a::real_normed_field. x / y)" 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1104 
unfolding divide_inverse by (rule bounded_linear_mult_left) 
23120  1105 

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

1106 
lemma bounded_bilinear_scaleR: "bounded_bilinear scaleR" 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

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

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

1109 
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

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

1111 
apply (rule scaleR_left_commute) 
31586
d4707b99e631
declare norm_scaleR [simp]; declare scaleR_cancel lemmas [simp]
huffman
parents:
31567
diff
changeset

1112 
apply (rule_tac x="1" in exI, simp) 
22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21809
diff
changeset

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

1114 

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

1115 
lemma bounded_linear_scaleR_left: "bounded_linear (\<lambda>r. scaleR r x)" 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

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

1117 
by (rule bounded_bilinear.bounded_linear_left) 
23127  1118 

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

1119 
lemma bounded_linear_scaleR_right: "bounded_linear (\<lambda>x. scaleR r x)" 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

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

1121 
by (rule bounded_bilinear.bounded_linear_right) 
23127  1122 

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

1123 
lemma bounded_linear_of_real: "bounded_linear (\<lambda>r. of_real r)" 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44127
diff
changeset

1124 
unfolding of_real_def by (rule bounded_linear_scaleR_left) 
22625  1125 

41969  1126 
subsection{* Hausdorff and other separation properties *} 
1127 

1128 
class t0_space = topological_space + 

1129 
assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)" 

1130 

1131 
class t1_space = topological_space + 

1132 
assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> x \<in> U \<and> y \<notin> U" 

1133 

1134 
instance t1_space \<subseteq> t0_space 

1135 
proof qed (fast dest: t1_space) 

1136 

1137 
lemma separation_t1: 

1138 
fixes x y :: "'a::t1_space" 

1139 
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)" 

1140 
using t1_space[of x y] by blast 

1141 

1142 
lemma closed_singleton: 

1143 
fixes a :: "'a::t1_space" 

1144 
shows "closed {a}" 

1145 
proof  

1146 
let ?T = "\<Union>{S. open S \<and> a \<notin> S}" 

1147 
have "open ?T" by (simp add: open_Union) 

1148 
also have "?T =  {a}" 

1149 
by (simp add: set_eq_iff separation_t1, auto) 

1150 
finally show "closed {a}" unfolding closed_def . 

1151 
qed 

1152 

1153 
lemma closed_insert [simp]: 

1154 
fixes a :: "'a::t1_space" 

1155 
assumes "closed S" shows "closed (insert a S)" 

1156 
proof  

1157 
from closed_singleton assms 

1158 
have "closed ({a} \<union> S)" by (rule closed_Un) 

1159 
thus "closed (insert a S)" by simp 

1160 
qed 

1161 

1162 
lemma finite_imp_closed: 

1163 
fixes S :: "'a::t1_space set" 

1164 
shows "finite S \<Longrightarrow> closed S" 

1165 
by (induct set: finite, simp_all) 

1166 

1167 
text {* T2 spaces are also known as Hausdorff spaces. *} 

1168 

1169 
class t2_space = topological_space + 

1170 
assumes hausdorff: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" 

1171 

1172 
instance t2_space \<subseteq> t1_space 

1173 
proof qed (fast dest: hausdorff) 

1174 

1175 
instance metric_space \<subseteq> t2_space 

1176 
proof 

1177 
fix x y :: "'a::metric_space" 

1178 
assume xy: "x \<noteq> y" 

1179 
let ?U = "{y'. dist x y' < dist x y / 2}" 

1180 
let ?V = "{x'. dist y x' < dist x y / 2}" 

1181 
have th0: "\<And>d x y z. (d x z :: real) \<le> d x y + d y z \<Longrightarrow> d y z = d z y 

1182 
\<Longrightarrow> \<not>(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith 

1183 
have "open ?U \<and> open ?V \<and> x \<in> ?U \<and> y \<in> ?V \<and> ?U \<inter> ?V = {}" 

1184 
using dist_pos_lt[OF xy] th0[of dist, OF dist_triangle dist_commute] 

1185 
using open_ball[of _ "dist x y / 2"] by auto 

1186 
then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" 

1187 
by blast 

1188 
qed 

1189 

1190 
lemma separation_t2: 

1191 
fixes x y :: "'a::t2_space" 

1192 
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})" 

1193 
using hausdorff[of x y] by blast 

1194 

1195 
lemma separation_t0: 

1196 
fixes x y :: "'a::t0_space" 

1197 
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))" 

1198 
using t0_space[of x y] by blast 

1199 

44571  1200 
text {* A perfect space is a topological space with no isolated points. *} 
1201 

1202 
class perfect_space = topological_space + 

1203 
assumes not_open_singleton: "\<not> open {x}" 

1204 

1205 
instance real_normed_algebra_1 \<subseteq> perfect_space 

1206 
proof 

1207 
fix x::'a 

1208 
show "\<not> open {x}" 

1209 
unfolding open_dist dist_norm 

1210 
by (clarsimp, rule_tac x="x + of_real (e/2)" in exI, simp) 

1211 
qed 

1212 

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

1213 
end 