1.1 --- a/src/HOL/Real/RealVector.thy Tue Aug 26 18:59:52 2008 +0200
1.2 +++ b/src/HOL/Real/RealVector.thy Tue Aug 26 23:49:46 2008 +0200
1.3 @@ -9,6 +9,142 @@
1.4 imports RealPow
1.5 begin
1.6
1.7 +subsection {* Group homomorphisms *}
1.8 +
1.9 +locale group_hom =
1.10 + ab_group_add
1.11 + mA (infixl "-\<^sub>A" 65)
1.12 + uA ("-\<^sub>A _" [81] 80)
1.13 + zA ("0\<^sub>A")
1.14 + pA (infixl "+\<^sub>A" 65) +
1.15 + ab_group_add
1.16 + mB (infixl "-\<^sub>B" 65)
1.17 + uB ("-\<^sub>B _" [81] 80)
1.18 + zB ("0\<^sub>B")
1.19 + pB (infixl "+\<^sub>B" 65) +
1.20 + fixes f :: "'a \<Rightarrow> 'b"
1.21 + assumes plus: "f (x +\<^sub>A y) = f x +\<^sub>B f y"
1.22 +begin
1.23 +
1.24 +lemma zero: "f 0\<^sub>A = 0\<^sub>B"
1.25 +proof -
1.26 + have "f 0\<^sub>A +\<^sub>B f 0\<^sub>A = f (0\<^sub>A +\<^sub>A 0\<^sub>A)" by (rule plus [symmetric])
1.27 + also have "f (0\<^sub>A +\<^sub>A 0\<^sub>A) = 0\<^sub>B +\<^sub>B f 0\<^sub>A" by simp
1.28 + finally show "f 0\<^sub>A = 0\<^sub>B" by (rule pB.add_right_imp_eq)
1.29 +qed
1.30 +
1.31 +lemma uminus: "f (-\<^sub>A x) = -\<^sub>B f x"
1.32 +proof -
1.33 + have "f (-\<^sub>A x) +\<^sub>B f x = f (-\<^sub>A x +\<^sub>A x)" by (rule plus [symmetric])
1.34 + also have "\<dots> = -\<^sub>B f x +\<^sub>B f x" by (simp add: zero)
1.35 + finally show "f (-\<^sub>A x) = -\<^sub>B f x" by (rule pB.add_right_imp_eq)
1.36 +qed
1.37 +
1.38 +lemma diff: "f (x -\<^sub>A y) = f x -\<^sub>B f y"
1.39 +by (simp add: mA_uA_zA_pA.diff_minus mB_uB_zB_pB.diff_minus plus uminus)
1.40 +
1.41 +text {* TODO:
1.42 +Locale-ize definition of setsum, so we can prove a lemma for it *}
1.43 +
1.44 +end
1.45 +
1.46 +subsection {* Vector spaces *}
1.47 +
1.48 +locale vector_space =
1.49 + field
1.50 + inverse
1.51 + divide (infixl "'/\<^sub>F" 70)
1.52 + one ("1\<^sub>F")
1.53 + times (infixl "*\<^sub>F" 70)
1.54 + mF (infixl "-\<^sub>F" 65)
1.55 + uF ("-\<^sub>F _" [81] 80)
1.56 + zF ("0\<^sub>F")
1.57 + pF (infixl "+\<^sub>F" 65) +
1.58 + ab_group_add
1.59 + mV (infixl "-\<^sub>V" 65)
1.60 + uV ("-\<^sub>V _" [81] 80)
1.61 + zV ("0\<^sub>V")
1.62 + pV (infixl "+\<^sub>V" 65) +
1.63 + fixes scale :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "%*" 75)
1.64 + assumes scale_right_distrib: "scale a (x +\<^sub>V y) = scale a x +\<^sub>V scale a y"
1.65 + and scale_left_distrib: "scale (a +\<^sub>F b) x = scale a x +\<^sub>V scale b x"
1.66 + and scale_scale [simp]: "scale a (scale b x) = scale (a *\<^sub>F b) x"
1.67 + and scale_one [simp]: "scale 1\<^sub>F x = x"
1.68 +begin
1.69 +
1.70 +lemma scale_left_commute:
1.71 + "scale a (scale b x) = scale b (scale a x)"
1.72 +by (simp add: mult_commute)
1.73 +
1.74 +lemma scale_zero_left [simp]: "scale 0\<^sub>F x = 0\<^sub>V"
1.75 + and scale_minus_left [simp]: "scale (-\<^sub>F a) x = -\<^sub>V (scale a x)"
1.76 + and scale_left_diff_distrib: "scale (a -\<^sub>F b) x = scale a x -\<^sub>V scale b x"
1.77 +proof -
1.78 + interpret s: group_hom
1.79 + [mF uF zF pF mV uV zV pV "\<lambda>a. scale a x"]
1.80 + by unfold_locales (rule scale_left_distrib)
1.81 + show "scale 0\<^sub>F x = 0\<^sub>V" by (rule s.zero)
1.82 + show "scale (-\<^sub>F a) x = -\<^sub>V (scale a x)" by (rule s.uminus)
1.83 + show "scale (a -\<^sub>F b) x = scale a x -\<^sub>V scale b x" by (rule s.diff)
1.84 +qed
1.85 +
1.86 +lemma scale_zero_right [simp]: "scale a 0\<^sub>V = 0\<^sub>V"
1.87 + and scale_minus_right [simp]: "scale a (-\<^sub>V x) = -\<^sub>V (scale a x)"
1.88 + and scale_right_diff_distrib: "scale a (x -\<^sub>V y) = scale a x -\<^sub>V scale a y"
1.89 +proof -
1.90 + interpret s: group_hom
1.91 + [mV uV zV pV mV uV zV pV "\<lambda>x. scale a x"]
1.92 + by unfold_locales (rule scale_right_distrib)
1.93 + show "scale a 0\<^sub>V = 0\<^sub>V" by (rule s.zero)
1.94 + show "scale a (-\<^sub>V x) = -\<^sub>V (scale a x)" by (rule s.uminus)
1.95 + show "scale a (x -\<^sub>V y) = scale a x -\<^sub>V scale a y" by (rule s.diff)
1.96 +qed
1.97 +
1.98 +lemma scale_eq_0_iff [simp]:
1.99 + "scale a x = 0\<^sub>V \<longleftrightarrow> a = 0\<^sub>F \<or> x = 0\<^sub>V"
1.100 +proof cases
1.101 + assume "a = 0\<^sub>F" thus ?thesis by simp
1.102 +next
1.103 + assume anz [simp]: "a \<noteq> 0\<^sub>F"
1.104 + { assume "scale a x = 0\<^sub>V"
1.105 + hence "scale (inverse a) (scale a x) = 0\<^sub>V" by simp
1.106 + hence "x = 0\<^sub>V" by simp }
1.107 + thus ?thesis by force
1.108 +qed
1.109 +
1.110 +lemma scale_left_imp_eq:
1.111 + "\<lbrakk>a \<noteq> 0\<^sub>F; scale a x = scale a y\<rbrakk> \<Longrightarrow> x = y"
1.112 +proof -
1.113 + assume nonzero: "a \<noteq> 0\<^sub>F"
1.114 + assume "scale a x = scale a y"
1.115 + hence "scale a (x -\<^sub>V y) = 0\<^sub>V"
1.116 + by (simp add: scale_right_diff_distrib)
1.117 + hence "x -\<^sub>V y = 0\<^sub>V" by (simp add: nonzero)
1.118 + thus "x = y" by (simp only: mV_uV_zV_pV.right_minus_eq)
1.119 +qed
1.120 +
1.121 +lemma scale_right_imp_eq:
1.122 + "\<lbrakk>x \<noteq> 0\<^sub>V; scale a x = scale b x\<rbrakk> \<Longrightarrow> a = b"
1.123 +proof -
1.124 + assume nonzero: "x \<noteq> 0\<^sub>V"
1.125 + assume "scale a x = scale b x"
1.126 + hence "scale (a -\<^sub>F b) x = 0\<^sub>V"
1.127 + by (simp add: scale_left_diff_distrib)
1.128 + hence "a -\<^sub>F b = 0\<^sub>F" by (simp add: nonzero)
1.129 + thus "a = b" by (simp only: mF_uF_zF_pF.right_minus_eq)
1.130 +qed
1.131 +
1.132 +lemma scale_cancel_left:
1.133 + "scale a x = scale a y \<longleftrightarrow> x = y \<or> a = 0\<^sub>F"
1.134 +by (auto intro: scale_left_imp_eq)
1.135 +
1.136 +lemma scale_cancel_right:
1.137 + "scale a x = scale b x \<longleftrightarrow> a = b \<or> x = 0\<^sub>V"
1.138 +by (auto intro: scale_right_imp_eq)
1.139 +
1.140 +end
1.141 +
1.142 +(* TODO: locale additive is superseded by group_hom; remove *)
1.143 subsection {* Locale for additive functions *}
1.144
1.145 locale additive =
1.146 @@ -72,6 +208,31 @@
1.147 and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"
1.148 and scaleR_one [simp]: "scaleR 1 x = x"
1.149
1.150 +interpretation real_vector: vector_space
1.151 + [inverse divide "1" times minus uminus "0" plus
1.152 + minus uminus "0" plus "scaleR::real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"]
1.153 +apply unfold_locales
1.154 +apply (rule scaleR_right_distrib)
1.155 +apply (rule scaleR_left_distrib)
1.156 +apply (rule scaleR_scaleR)
1.157 +apply (rule scaleR_one)
1.158 +done
1.159 +
1.160 +text {* Recover original theorem names *}
1.161 +
1.162 +lemmas scaleR_left_commute = real_vector.scale_left_commute
1.163 +lemmas scaleR_zero_left = real_vector.scale_zero_left
1.164 +lemmas scaleR_minus_left = real_vector.scale_minus_left
1.165 +lemmas scaleR_left_diff_distrib = real_vector.scale_left_diff_distrib
1.166 +lemmas scaleR_zero_right = real_vector.scale_zero_right
1.167 +lemmas scaleR_minus_right = real_vector.scale_minus_right
1.168 +lemmas scaleR_right_diff_distrib = real_vector.scale_right_diff_distrib
1.169 +lemmas scaleR_eq_0_iff = real_vector.scale_eq_0_iff
1.170 +lemmas scaleR_left_imp_eq = real_vector.scale_left_imp_eq
1.171 +lemmas scaleR_right_imp_eq = real_vector.scale_right_imp_eq
1.172 +lemmas scaleR_cancel_left = real_vector.scale_cancel_left
1.173 +lemmas scaleR_cancel_right = real_vector.scale_cancel_right
1.174 +
1.175 class real_algebra = real_vector + ring +
1.176 assumes mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)"
1.177 and mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)"
1.178 @@ -92,76 +253,12 @@
1.179 apply (rule mult_left_commute)
1.180 done
1.181
1.182 -lemma scaleR_left_commute:
1.183 - fixes x :: "'a::real_vector"
1.184 - shows "scaleR a (scaleR b x) = scaleR b (scaleR a x)"
1.185 -by (simp add: mult_commute)
1.186 -
1.187 interpretation scaleR_left: additive ["(\<lambda>a. scaleR a x::'a::real_vector)"]
1.188 by unfold_locales (rule scaleR_left_distrib)
1.189
1.190 interpretation scaleR_right: additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
1.191 by unfold_locales (rule scaleR_right_distrib)
1.192
1.193 -lemmas scaleR_zero_left [simp] = scaleR_left.zero
1.194 -
1.195 -lemmas scaleR_zero_right [simp] = scaleR_right.zero
1.196 -
1.197 -lemmas scaleR_minus_left [simp] = scaleR_left.minus
1.198 -
1.199 -lemmas scaleR_minus_right [simp] = scaleR_right.minus
1.200 -
1.201 -lemmas scaleR_left_diff_distrib = scaleR_left.diff
1.202 -
1.203 -lemmas scaleR_right_diff_distrib = scaleR_right.diff
1.204 -
1.205 -lemma scaleR_eq_0_iff [simp]:
1.206 - fixes x :: "'a::real_vector"
1.207 - shows "(scaleR a x = 0) = (a = 0 \<or> x = 0)"
1.208 -proof cases
1.209 - assume "a = 0" thus ?thesis by simp
1.210 -next
1.211 - assume anz [simp]: "a \<noteq> 0"
1.212 - { assume "scaleR a x = 0"
1.213 - hence "scaleR (inverse a) (scaleR a x) = 0" by simp
1.214 - hence "x = 0" by simp }
1.215 - thus ?thesis by force
1.216 -qed
1.217 -
1.218 -lemma scaleR_left_imp_eq:
1.219 - fixes x y :: "'a::real_vector"
1.220 - shows "\<lbrakk>a \<noteq> 0; scaleR a x = scaleR a y\<rbrakk> \<Longrightarrow> x = y"
1.221 -proof -
1.222 - assume nonzero: "a \<noteq> 0"
1.223 - assume "scaleR a x = scaleR a y"
1.224 - hence "scaleR a (x - y) = 0"
1.225 - by (simp add: scaleR_right_diff_distrib)
1.226 - hence "x - y = 0" by (simp add: nonzero)
1.227 - thus "x = y" by simp
1.228 -qed
1.229 -
1.230 -lemma scaleR_right_imp_eq:
1.231 - fixes x y :: "'a::real_vector"
1.232 - shows "\<lbrakk>x \<noteq> 0; scaleR a x = scaleR b x\<rbrakk> \<Longrightarrow> a = b"
1.233 -proof -
1.234 - assume nonzero: "x \<noteq> 0"
1.235 - assume "scaleR a x = scaleR b x"
1.236 - hence "scaleR (a - b) x = 0"
1.237 - by (simp add: scaleR_left_diff_distrib)
1.238 - hence "a - b = 0" by (simp add: nonzero)
1.239 - thus "a = b" by simp
1.240 -qed
1.241 -
1.242 -lemma scaleR_cancel_left:
1.243 - fixes x y :: "'a::real_vector"
1.244 - shows "(scaleR a x = scaleR a y) = (x = y \<or> a = 0)"
1.245 -by (auto intro: scaleR_left_imp_eq)
1.246 -
1.247 -lemma scaleR_cancel_right:
1.248 - fixes x y :: "'a::real_vector"
1.249 - shows "(scaleR a x = scaleR b x) = (a = b \<or> x = 0)"
1.250 -by (auto intro: scaleR_right_imp_eq)
1.251 -
1.252 lemma nonzero_inverse_scaleR_distrib:
1.253 fixes x :: "'a::real_div_algebra" shows
1.254 "\<lbrakk>a \<noteq> 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> inverse (scaleR a x) = scaleR (inverse a) (inverse x)"