author  huffman 
Tue, 26 Aug 2008 23:49:46 +0200  
changeset 28009  e93b121074fb 
parent 27553  d315a513a150 
child 28029  4c55cdec4ce7 
permissions  rwrr 
27552
15cf4ed9c2a1
reremoved subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef
haftmann
parents:
27515
diff
changeset

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

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

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

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

5 

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

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

7 

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

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

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

11 

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

12 
subsection {* Group homomorphisms *} 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

13 

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

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

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

16 
mA (infixl "\<^sub>A" 65) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

17 
uA ("\<^sub>A _" [81] 80) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

18 
zA ("0\<^sub>A") 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

19 
pA (infixl "+\<^sub>A" 65) + 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

21 
mB (infixl "\<^sub>B" 65) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

22 
uB ("\<^sub>B _" [81] 80) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

23 
zB ("0\<^sub>B") 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

24 
pB (infixl "+\<^sub>B" 65) + 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

25 
fixes f :: "'a \<Rightarrow> 'b" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

26 
assumes plus: "f (x +\<^sub>A y) = f x +\<^sub>B f y" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

28 

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

29 
lemma zero: "f 0\<^sub>A = 0\<^sub>B" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

31 
have "f 0\<^sub>A +\<^sub>B f 0\<^sub>A = f (0\<^sub>A +\<^sub>A 0\<^sub>A)" by (rule plus [symmetric]) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

32 
also have "f (0\<^sub>A +\<^sub>A 0\<^sub>A) = 0\<^sub>B +\<^sub>B f 0\<^sub>A" by simp 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

33 
finally show "f 0\<^sub>A = 0\<^sub>B" by (rule pB.add_right_imp_eq) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

35 

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

36 
lemma uminus: "f (\<^sub>A x) = \<^sub>B f x" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

38 
have "f (\<^sub>A x) +\<^sub>B f x = f (\<^sub>A x +\<^sub>A x)" by (rule plus [symmetric]) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

39 
also have "\<dots> = \<^sub>B f x +\<^sub>B f x" by (simp add: zero) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

40 
finally show "f (\<^sub>A x) = \<^sub>B f x" by (rule pB.add_right_imp_eq) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

42 

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

43 
lemma diff: "f (x \<^sub>A y) = f x \<^sub>B f y" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

44 
by (simp add: mA_uA_zA_pA.diff_minus mB_uB_zB_pB.diff_minus plus uminus) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

45 

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

46 
text {* TODO: 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

47 
Localeize definition of setsum, so we can prove a lemma for it *} 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

48 

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

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

50 

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

51 
subsection {* Vector spaces *} 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

52 

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

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

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

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

56 
divide (infixl "'/\<^sub>F" 70) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

57 
one ("1\<^sub>F") 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

58 
times (infixl "*\<^sub>F" 70) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

59 
mF (infixl "\<^sub>F" 65) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

60 
uF ("\<^sub>F _" [81] 80) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

61 
zF ("0\<^sub>F") 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

62 
pF (infixl "+\<^sub>F" 65) + 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

64 
mV (infixl "\<^sub>V" 65) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

65 
uV ("\<^sub>V _" [81] 80) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

66 
zV ("0\<^sub>V") 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

67 
pV (infixl "+\<^sub>V" 65) + 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

68 
fixes scale :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "%*" 75) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

69 
assumes scale_right_distrib: "scale a (x +\<^sub>V y) = scale a x +\<^sub>V scale a y" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

70 
and scale_left_distrib: "scale (a +\<^sub>F b) x = scale a x +\<^sub>V scale b x" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

71 
and scale_scale [simp]: "scale a (scale b x) = scale (a *\<^sub>F b) x" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

72 
and scale_one [simp]: "scale 1\<^sub>F x = x" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

74 

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

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

76 
"scale a (scale b x) = scale b (scale a x)" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

77 
by (simp add: mult_commute) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

78 

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

79 
lemma scale_zero_left [simp]: "scale 0\<^sub>F x = 0\<^sub>V" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

80 
and scale_minus_left [simp]: "scale (\<^sub>F a) x = \<^sub>V (scale a x)" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

81 
and scale_left_diff_distrib: "scale (a \<^sub>F b) x = scale a x \<^sub>V scale b x" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

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

84 
[mF uF zF pF mV uV zV pV "\<lambda>a. scale a x"] 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

85 
by unfold_locales (rule scale_left_distrib) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

86 
show "scale 0\<^sub>F x = 0\<^sub>V" by (rule s.zero) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

87 
show "scale (\<^sub>F a) x = \<^sub>V (scale a x)" by (rule s.uminus) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

88 
show "scale (a \<^sub>F b) x = scale a x \<^sub>V scale b x" by (rule s.diff) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

90 

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

91 
lemma scale_zero_right [simp]: "scale a 0\<^sub>V = 0\<^sub>V" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

92 
and scale_minus_right [simp]: "scale a (\<^sub>V x) = \<^sub>V (scale a x)" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

93 
and scale_right_diff_distrib: "scale a (x \<^sub>V y) = scale a x \<^sub>V scale a y" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

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

96 
[mV uV zV pV mV uV zV pV "\<lambda>x. scale a x"] 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

97 
by unfold_locales (rule scale_right_distrib) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

98 
show "scale a 0\<^sub>V = 0\<^sub>V" by (rule s.zero) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

99 
show "scale a (\<^sub>V x) = \<^sub>V (scale a x)" by (rule s.uminus) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

100 
show "scale a (x \<^sub>V y) = scale a x \<^sub>V scale a y" by (rule s.diff) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

102 

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

103 
lemma scale_eq_0_iff [simp]: 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

104 
"scale a x = 0\<^sub>V \<longleftrightarrow> a = 0\<^sub>F \<or> x = 0\<^sub>V" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

106 
assume "a = 0\<^sub>F" thus ?thesis by simp 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

108 
assume anz [simp]: "a \<noteq> 0\<^sub>F" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

109 
{ assume "scale a x = 0\<^sub>V" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

110 
hence "scale (inverse a) (scale a x) = 0\<^sub>V" by simp 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

111 
hence "x = 0\<^sub>V" by simp } 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

112 
thus ?thesis by force 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

114 

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

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

116 
"\<lbrakk>a \<noteq> 0\<^sub>F; scale a x = scale a y\<rbrakk> \<Longrightarrow> x = y" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

118 
assume nonzero: "a \<noteq> 0\<^sub>F" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

119 
assume "scale a x = scale a y" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

120 
hence "scale a (x \<^sub>V y) = 0\<^sub>V" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

121 
by (simp add: scale_right_diff_distrib) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

122 
hence "x \<^sub>V y = 0\<^sub>V" by (simp add: nonzero) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

123 
thus "x = y" by (simp only: mV_uV_zV_pV.right_minus_eq) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

125 

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

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

127 
"\<lbrakk>x \<noteq> 0\<^sub>V; scale a x = scale b x\<rbrakk> \<Longrightarrow> a = b" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

129 
assume nonzero: "x \<noteq> 0\<^sub>V" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

130 
assume "scale a x = scale b x" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

131 
hence "scale (a \<^sub>F b) x = 0\<^sub>V" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

132 
by (simp add: scale_left_diff_distrib) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

133 
hence "a \<^sub>F b = 0\<^sub>F" by (simp add: nonzero) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

134 
thus "a = b" by (simp only: mF_uF_zF_pF.right_minus_eq) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

136 

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

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

138 
"scale a x = scale a y \<longleftrightarrow> x = y \<or> a = 0\<^sub>F" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

139 
by (auto intro: scale_left_imp_eq) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

140 

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

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

142 
"scale a x = scale b x \<longleftrightarrow> a = b \<or> x = 0\<^sub>V" 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

143 
by (auto intro: scale_right_imp_eq) 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

144 

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

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

146 

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

147 
(* TODO: locale additive is superseded by group_hom; remove *) 
20504
6342e872e71d
formalization of vector spaces and algebras over the real numbers
huffman
parents:
diff
changeset

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

149 

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

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

151 
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

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

154 

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

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

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

158 
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

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

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

161 

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

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

164 
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

165 
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

166 
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

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

168 

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

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

171 

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

175 
apply (simp add: zero) 

176 
apply (simp add: add) 

177 
apply (simp add: zero) 

178 
done 

179 

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

181 

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

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

183 

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

187 

20763  188 
abbreviation 
25062  189 
divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a" (infixl "'/\<^sub>R" 70) 
24748  190 
where 
25062  191 
"x /\<^sub>R r == scaleR (inverse r) x" 
24748  192 

193 
end 

194 

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

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

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

197 

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

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

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

200 

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

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

202 

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

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

204 

24588  205 
class real_vector = scaleR + ab_group_add + 
25062  206 
assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y" 
207 
and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x" 

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

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

210 

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

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

212 
[inverse divide "1" times minus uminus "0" plus 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

213 
minus uminus "0" plus "scaleR::real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"] 
e93b121074fb
move real_vector class proofs into vector_space and group_hom locales
huffman
parents:
27553
diff
changeset

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

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

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

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

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

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

220 

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

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

222 

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

223 
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

224 
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

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

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

227 
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

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

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

230 
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

231 
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

232 
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

233 
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

234 
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

235 

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

239 

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

241 

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

243 

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

245 

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

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

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

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

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

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

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

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

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

255 

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

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

258 

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

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

261 

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

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

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

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

266 

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

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

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

269 
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

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

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

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

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

274 

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

275 

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

276 
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

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

278 

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

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

280 
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

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

282 

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

283 
lemma scaleR_conv_of_real: "scaleR r x = of_real r * x" 
20763  284 
by (simp add: of_real_def) 
285 

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

286 
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

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

288 

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

289 
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

290 
by (simp add: of_real_def) 
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_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

293 
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

294 

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

295 
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

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

297 

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

298 
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

299 
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

300 

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

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

303 

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

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

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

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

307 
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

308 

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

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

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

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

312 
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

313 

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

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

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

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

317 
by (simp add: divide_inverse nonzero_of_real_inverse) 
20722  318 

319 
lemma of_real_divide [simp]: 

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

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

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

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

323 

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

20772  326 
by (induct n) (simp_all add: power_Suc) 
20722  327 

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

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

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

330 

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

331 
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

332 

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

333 
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

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

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

336 
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

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

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

339 

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

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

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

343 

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

344 
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

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

346 

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

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

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

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

350 

22912  351 
text{*Every real algebra has characteristic zero*} 
352 
instance real_algebra_1 < ring_char_0 

353 
proof 

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

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

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

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

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

358 
by (simp only: of_real_of_nat_eq) 
22912  359 
qed 
360 

27553  361 
instance real_field < field_char_0 .. 
362 

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

363 

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

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

365 

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

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

369 

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

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

372 

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

373 
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

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

375 

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

376 
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

377 
by (subst of_real_of_int_eq [symmetric], rule Reals_of_real) 
20718  378 

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

379 
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

380 
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

381 

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

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

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

384 
by (subst of_real_number_of_eq [symmetric], rule Reals_of_real) 
20718  385 

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

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

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

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

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

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

391 

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

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

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

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

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

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

397 

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

398 
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

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

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

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

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

403 

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

404 
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

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

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

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

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

409 

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

410 
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

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

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

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

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

415 

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

416 
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

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

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

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

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

421 

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

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

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

424 
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

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

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

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

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

429 

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

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

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

432 
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

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

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

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

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

437 

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

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

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

440 
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

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

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

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

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

445 

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

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

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

448 
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

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

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

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

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

453 

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

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

457 
apply (auto simp add: Reals_def) 

458 
apply (rule range_eqI) 

459 
apply (rule of_real_power [symmetric]) 

460 
done 

461 

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

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

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

464 
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

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

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

467 
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

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

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

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

471 

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

472 
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

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

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

475 

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

476 

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

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

478 

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

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

481 

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

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

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

484 

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

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

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

487 

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

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

489 

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

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

491 

24520  492 
class sgn_div_norm = scaleR + norm + sgn + 
25062  493 
assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x" 
24506  494 

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

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

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

500 

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

503 

24588  504 
class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra + 
25062  505 
assumes norm_one [simp]: "norm 1 = 1" 
22852  506 

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

509 

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

511 

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

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

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

515 
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

516 
by (simp add: norm_mult) 
22852  517 
next 
518 
have "norm (1 * 1::'a) = norm (1::'a) * norm (1::'a)" 

519 
by (rule norm_mult) 

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

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

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

522 

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

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

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

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

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

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

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

532 

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

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

535 

22852  536 
lemma zero_less_norm_iff [simp]: 
537 
fixes x :: "'a::real_normed_vector" 

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

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

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

540 

22852  541 
lemma norm_not_less_zero [simp]: 
542 
fixes x :: "'a::real_normed_vector" 

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

20828  544 
by (simp add: linorder_not_less) 
545 

22852  546 
lemma norm_le_zero_iff [simp]: 
547 
fixes x :: "'a::real_normed_vector" 

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

20828  549 
by (simp add: order_le_less) 
550 

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

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

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

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

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

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

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

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

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

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

561 

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

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

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

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

565 
proof  
22898  566 
have "norm ( (b  a)) = norm (b  a)" 
567 
by (rule norm_minus_cancel) 

568 
thus ?thesis by simp 

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

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

570 

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

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

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

574 
proof  
20533  575 
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

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

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

579 

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

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

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

582 
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

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

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

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

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

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

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

589 

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

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

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

593 
proof  
22898  594 
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

595 
by (rule norm_triangle_ineq) 
22898  596 
thus ?thesis 
597 
by (simp only: diff_minus norm_minus_cancel) 

598 
qed 

599 

600 
lemma norm_diff_ineq: 

601 
fixes a b :: "'a::real_normed_vector" 

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

603 
proof  

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

605 
by (rule norm_triangle_ineq2) 

606 
thus ?thesis by simp 

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

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

608 

20551  609 
lemma norm_diff_triangle_ineq: 
610 
fixes a b c d :: "'a::real_normed_vector" 

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

612 
proof  

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

614 
by (simp add: diff_minus add_ac) 

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

616 
by (rule norm_triangle_ineq) 

617 
finally show ?thesis . 

618 
qed 

619 

22857  620 
lemma abs_norm_cancel [simp]: 
621 
fixes a :: "'a::real_normed_vector" 

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

623 
by (rule abs_of_nonneg [OF norm_ge_zero]) 

624 

22880  625 
lemma norm_add_less: 
626 
fixes x y :: "'a::real_normed_vector" 

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

628 
by (rule order_le_less_trans [OF norm_triangle_ineq add_strict_mono]) 

629 

630 
lemma norm_mult_less: 

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

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

633 
apply (rule order_le_less_trans [OF norm_mult_ineq]) 

634 
apply (simp add: mult_strict_mono') 

635 
done 

636 

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

22852  639 
unfolding of_real_def by (simp add: norm_scaleR) 
20560  640 

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

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

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

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

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

645 

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

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

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

648 
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

649 

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

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

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

652 
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

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

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

655 

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

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

657 
fixes a :: "'a::real_normed_div_algebra" 
20533  658 
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

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

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

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

662 

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

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

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

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

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

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

669 

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

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

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

672 
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

673 
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

674 

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

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

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

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

678 
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

679 

22852  680 
lemma norm_power_ineq: 
681 
fixes x :: "'a::{real_normed_algebra_1,recpower}" 

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

683 
proof (induct n) 

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

685 
next 

686 
case (Suc n) 

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

688 
by (rule norm_mult_ineq) 

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

690 
using norm_ge_zero by (rule mult_left_mono) 

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

692 
by (simp add: power_Suc) 

693 
qed 

694 

20684  695 
lemma norm_power: 
696 
fixes x :: "'a::{real_normed_div_algebra,recpower}" 

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

20772  698 
by (induct n) (simp_all add: power_Suc norm_mult) 
20684  699 

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

700 

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

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

702 

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

705 
by (simp add: sgn_div_norm norm_scaleR) 

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

706 

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

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

709 

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

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

712 

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

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

715 

24506  716 
lemma sgn_scaleR: 
717 
"sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))" 

718 
by (simp add: sgn_div_norm norm_scaleR mult_ac) 

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

719 

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

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

722 

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

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

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

725 
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

726 

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

727 
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

728 
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

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

731 

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

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

734 

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

735 
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

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

737 

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

738 
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

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

740 

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

741 

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

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

743 

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

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

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

746 
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

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

749 

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

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

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

753 
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

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

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

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

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

758 
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

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

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

761 
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

762 
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

763 
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

764 
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

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

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

767 

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

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

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

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

772 
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

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

774 

27443  775 
end 
776 

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

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

778 
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

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

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

781 
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

782 
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

783 
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

784 
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

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

787 

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

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

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

791 
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

792 
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

793 
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

794 
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

795 
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

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

797 

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

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

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

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

802 
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

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

804 

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

806 
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

807 

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

809 
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

810 

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

812 
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

813 

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

815 
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

816 

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

818 
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

819 

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

821 
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

822 

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

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

825 
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

826 

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

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

829 
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

830 

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

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

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

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

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

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

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

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

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

840 

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

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

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

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

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

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

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

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

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

850 

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

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

853 
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

854 

27443  855 
end 
856 

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

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

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

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

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

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

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

864 
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

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

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

867 

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

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

871 

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

874 
by (rule mult.bounded_linear_right) 

875 

876 
interpretation divide: 

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

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

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

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

883 
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

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

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

886 
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

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

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

889 

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

892 

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

894 
by (rule scaleR.bounded_linear_right) 

895 

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

897 
unfolding of_real_def by (rule scaleR.bounded_linear_left) 

22625  898 

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

899 
end 