58 |
58 |
59 lemma scale_zero_left [simp]: "scale 0 x = 0" |
59 lemma scale_zero_left [simp]: "scale 0 x = 0" |
60 and scale_minus_left [simp]: "scale (- a) x = - (scale a x)" |
60 and scale_minus_left [simp]: "scale (- a) x = - (scale a x)" |
61 and scale_left_diff_distrib: "scale (a - b) x = scale a x - scale b x" |
61 and scale_left_diff_distrib: "scale (a - b) x = scale a x - scale b x" |
62 proof - |
62 proof - |
63 interpret s: additive ["\<lambda>a. scale a x"] |
63 interpret s: additive "\<lambda>a. scale a x" |
64 proof qed (rule scale_left_distrib) |
64 proof qed (rule scale_left_distrib) |
65 show "scale 0 x = 0" by (rule s.zero) |
65 show "scale 0 x = 0" by (rule s.zero) |
66 show "scale (- a) x = - (scale a x)" by (rule s.minus) |
66 show "scale (- a) x = - (scale a x)" by (rule s.minus) |
67 show "scale (a - b) x = scale a x - scale b x" by (rule s.diff) |
67 show "scale (a - b) x = scale a x - scale b x" by (rule s.diff) |
68 qed |
68 qed |
69 |
69 |
70 lemma scale_zero_right [simp]: "scale a 0 = 0" |
70 lemma scale_zero_right [simp]: "scale a 0 = 0" |
71 and scale_minus_right [simp]: "scale a (- x) = - (scale a x)" |
71 and scale_minus_right [simp]: "scale a (- x) = - (scale a x)" |
72 and scale_right_diff_distrib: "scale a (x - y) = scale a x - scale a y" |
72 and scale_right_diff_distrib: "scale a (x - y) = scale a x - scale a y" |
73 proof - |
73 proof - |
74 interpret s: additive ["\<lambda>x. scale a x"] |
74 interpret s: additive "\<lambda>x. scale a x" |
75 proof qed (rule scale_right_distrib) |
75 proof qed (rule scale_right_distrib) |
76 show "scale a 0 = 0" by (rule s.zero) |
76 show "scale a 0 = 0" by (rule s.zero) |
77 show "scale a (- x) = - (scale a x)" by (rule s.minus) |
77 show "scale a (- x) = - (scale a x)" by (rule s.minus) |
78 show "scale a (x - y) = scale a x - scale a y" by (rule s.diff) |
78 show "scale a (x - y) = scale a x - scale a y" by (rule s.diff) |
79 qed |
79 qed |
150 and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x" |
150 and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x" |
151 and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x" |
151 and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x" |
152 and scaleR_one [simp]: "scaleR 1 x = x" |
152 and scaleR_one [simp]: "scaleR 1 x = x" |
153 |
153 |
154 interpretation real_vector: |
154 interpretation real_vector: |
155 vector_space ["scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"] |
155 vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector" |
156 apply unfold_locales |
156 apply unfold_locales |
157 apply (rule scaleR_right_distrib) |
157 apply (rule scaleR_right_distrib) |
158 apply (rule scaleR_left_distrib) |
158 apply (rule scaleR_left_distrib) |
159 apply (rule scaleR_scaleR) |
159 apply (rule scaleR_scaleR) |
160 apply (rule scaleR_one) |
160 apply (rule scaleR_one) |
193 apply (rule mult_1_left) |
193 apply (rule mult_1_left) |
194 apply (rule mult_assoc) |
194 apply (rule mult_assoc) |
195 apply (rule mult_left_commute) |
195 apply (rule mult_left_commute) |
196 done |
196 done |
197 |
197 |
198 interpretation scaleR_left: additive ["(\<lambda>a. scaleR a x::'a::real_vector)"] |
198 interpretation scaleR_left: additive "(\<lambda>a. scaleR a x::'a::real_vector)" |
199 proof qed (rule scaleR_left_distrib) |
199 proof qed (rule scaleR_left_distrib) |
200 |
200 |
201 interpretation scaleR_right: additive ["(\<lambda>x. scaleR a x::'a::real_vector)"] |
201 interpretation scaleR_right: additive "(\<lambda>x. scaleR a x::'a::real_vector)" |
202 proof qed (rule scaleR_right_distrib) |
202 proof qed (rule scaleR_right_distrib) |
203 |
203 |
204 lemma nonzero_inverse_scaleR_distrib: |
204 lemma nonzero_inverse_scaleR_distrib: |
205 fixes x :: "'a::real_div_algebra" shows |
205 fixes x :: "'a::real_div_algebra" shows |
206 "\<lbrakk>a \<noteq> 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> inverse (scaleR a x) = scaleR (inverse a) (inverse x)" |
206 "\<lbrakk>a \<noteq> 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> inverse (scaleR a x) = scaleR (inverse a) (inverse x)" |
795 by (simp add: diff_left diff_right) |
795 by (simp add: diff_left diff_right) |
796 |
796 |
797 end |
797 end |
798 |
798 |
799 interpretation mult: |
799 interpretation mult: |
800 bounded_bilinear ["op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"] |
800 bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra" |
801 apply (rule bounded_bilinear.intro) |
801 apply (rule bounded_bilinear.intro) |
802 apply (rule left_distrib) |
802 apply (rule left_distrib) |
803 apply (rule right_distrib) |
803 apply (rule right_distrib) |
804 apply (rule mult_scaleR_left) |
804 apply (rule mult_scaleR_left) |
805 apply (rule mult_scaleR_right) |
805 apply (rule mult_scaleR_right) |
806 apply (rule_tac x="1" in exI) |
806 apply (rule_tac x="1" in exI) |
807 apply (simp add: norm_mult_ineq) |
807 apply (simp add: norm_mult_ineq) |
808 done |
808 done |
809 |
809 |
810 interpretation mult_left: |
810 interpretation mult_left: |
811 bounded_linear ["(\<lambda>x::'a::real_normed_algebra. x * y)"] |
811 bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)" |
812 by (rule mult.bounded_linear_left) |
812 by (rule mult.bounded_linear_left) |
813 |
813 |
814 interpretation mult_right: |
814 interpretation mult_right: |
815 bounded_linear ["(\<lambda>y::'a::real_normed_algebra. x * y)"] |
815 bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)" |
816 by (rule mult.bounded_linear_right) |
816 by (rule mult.bounded_linear_right) |
817 |
817 |
818 interpretation divide: |
818 interpretation divide: |
819 bounded_linear ["(\<lambda>x::'a::real_normed_field. x / y)"] |
819 bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)" |
820 unfolding divide_inverse by (rule mult.bounded_linear_left) |
820 unfolding divide_inverse by (rule mult.bounded_linear_left) |
821 |
821 |
822 interpretation scaleR: bounded_bilinear ["scaleR"] |
822 interpretation scaleR: bounded_bilinear "scaleR" |
823 apply (rule bounded_bilinear.intro) |
823 apply (rule bounded_bilinear.intro) |
824 apply (rule scaleR_left_distrib) |
824 apply (rule scaleR_left_distrib) |
825 apply (rule scaleR_right_distrib) |
825 apply (rule scaleR_right_distrib) |
826 apply simp |
826 apply simp |
827 apply (rule scaleR_left_commute) |
827 apply (rule scaleR_left_commute) |
828 apply (rule_tac x="1" in exI) |
828 apply (rule_tac x="1" in exI) |
829 apply (simp add: norm_scaleR) |
829 apply (simp add: norm_scaleR) |
830 done |
830 done |
831 |
831 |
832 interpretation scaleR_left: bounded_linear ["\<lambda>r. scaleR r x"] |
832 interpretation scaleR_left: bounded_linear "\<lambda>r. scaleR r x" |
833 by (rule scaleR.bounded_linear_left) |
833 by (rule scaleR.bounded_linear_left) |
834 |
834 |
835 interpretation scaleR_right: bounded_linear ["\<lambda>x. scaleR r x"] |
835 interpretation scaleR_right: bounded_linear "\<lambda>x. scaleR r x" |
836 by (rule scaleR.bounded_linear_right) |
836 by (rule scaleR.bounded_linear_right) |
837 |
837 |
838 interpretation of_real: bounded_linear ["\<lambda>r. of_real r"] |
838 interpretation of_real: bounded_linear "\<lambda>r. of_real r" |
839 unfolding of_real_def by (rule scaleR.bounded_linear_left) |
839 unfolding of_real_def by (rule scaleR.bounded_linear_left) |
840 |
840 |
841 end |
841 end |