src/HOL/Real/RealVector.thy

 
 theory RealVector
 imports RealPow
 begin
 
-subsection {* Group homomorphisms *}
-
-locale group_hom =
-  ab_group_add
-    mA (infixl "-\<^sub>A" 65)
-    uA ("-\<^sub>A _" [81] 80)
-    zA ("0\<^sub>A")
-    pA (infixl "+\<^sub>A" 65) +
-  ab_group_add
-    mB (infixl "-\<^sub>B" 65)
-    uB ("-\<^sub>B _" [81] 80)
-    zB ("0\<^sub>B")
-    pB (infixl "+\<^sub>B" 65) +
-  fixes f :: "'a \<Rightarrow> 'b"
-  assumes plus: "f (x +\<^sub>A y) = f x +\<^sub>B f y"
-begin
-
-lemma zero: "f 0\<^sub>A = 0\<^sub>B"
-proof -
-  have "f 0\<^sub>A +\<^sub>B f 0\<^sub>A = f (0\<^sub>A +\<^sub>A 0\<^sub>A)" by (rule plus [symmetric])
-  also have "f (0\<^sub>A +\<^sub>A 0\<^sub>A) = 0\<^sub>B +\<^sub>B f 0\<^sub>A" by simp
-  finally show "f 0\<^sub>A = 0\<^sub>B" by (rule pB.add_right_imp_eq)
-qed
-
-lemma uminus: "f (-\<^sub>A x) = -\<^sub>B f x"
-proof -
-  have "f (-\<^sub>A x) +\<^sub>B f x = f (-\<^sub>A x +\<^sub>A x)" by (rule plus [symmetric])
-  also have "\<dots> = -\<^sub>B f x +\<^sub>B f x" by (simp add: zero)
-  finally show "f (-\<^sub>A x) = -\<^sub>B f x" by (rule pB.add_right_imp_eq)
-qed
-
-lemma diff: "f (x -\<^sub>A y) = f x -\<^sub>B f y"
-by (simp add: mA_uA_zA_pA.diff_minus mB_uB_zB_pB.diff_minus plus uminus)
-
-text {* TODO:
-Locale-ize definition of setsum, so we can prove a lemma for it *}
-
-end
-
-subsection {* Vector spaces *}
-
-locale vector_space =
-  field
-    inverse
-    divide (infixl "'/\<^sub>F" 70)
-    one ("1\<^sub>F")
-    times (infixl "*\<^sub>F" 70)
-    mF (infixl "-\<^sub>F" 65)
-    uF ("-\<^sub>F _" [81] 80)
-    zF ("0\<^sub>F")
-    pF (infixl "+\<^sub>F" 65) +
-  ab_group_add
-    mV (infixl "-\<^sub>V" 65)
-    uV ("-\<^sub>V _" [81] 80)
-    zV ("0\<^sub>V")
-    pV (infixl "+\<^sub>V" 65) +
-  fixes scale :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "%*" 75)
-  assumes scale_right_distrib: "scale a (x +\<^sub>V y) = scale a x +\<^sub>V scale a y"
-  and scale_left_distrib: "scale (a +\<^sub>F b) x = scale a x +\<^sub>V scale b x"
-  and scale_scale [simp]: "scale a (scale b x) = scale (a *\<^sub>F b) x"
-  and scale_one [simp]: "scale 1\<^sub>F x = x"
-begin
-
-lemma scale_left_commute:
-  "scale a (scale b x) = scale b (scale a x)"
-by (simp add: mult_commute)
-
-lemma scale_zero_left [simp]: "scale 0\<^sub>F x = 0\<^sub>V"
-  and scale_minus_left [simp]: "scale (-\<^sub>F a) x = -\<^sub>V (scale a x)"
-  and scale_left_diff_distrib: "scale (a -\<^sub>F b) x = scale a x -\<^sub>V scale b x"
-proof -
-  interpret s: group_hom
-    [mF uF zF pF mV uV zV pV "\<lambda>a. scale a x"]
-    by unfold_locales (rule scale_left_distrib)
-  show "scale 0\<^sub>F x = 0\<^sub>V" by (rule s.zero)
-  show "scale (-\<^sub>F a) x = -\<^sub>V (scale a x)" by (rule s.uminus)
-  show "scale (a -\<^sub>F b) x = scale a x -\<^sub>V scale b x" by (rule s.diff)
-qed
-
-lemma scale_zero_right [simp]: "scale a 0\<^sub>V = 0\<^sub>V"
-  and scale_minus_right [simp]: "scale a (-\<^sub>V x) = -\<^sub>V (scale a x)"
-  and scale_right_diff_distrib: "scale a (x -\<^sub>V y) = scale a x -\<^sub>V scale a y"
-proof -
-  interpret s: group_hom
-    [mV uV zV pV mV uV zV pV "\<lambda>x. scale a x"]
-    by unfold_locales (rule scale_right_distrib)
-  show "scale a 0\<^sub>V = 0\<^sub>V" by (rule s.zero)
-  show "scale a (-\<^sub>V x) = -\<^sub>V (scale a x)" by (rule s.uminus)
-  show "scale a (x -\<^sub>V y) = scale a x -\<^sub>V scale a y" by (rule s.diff)
-qed
-
-lemma scale_eq_0_iff [simp]:
-  "scale a x = 0\<^sub>V \<longleftrightarrow> a = 0\<^sub>F \<or> x = 0\<^sub>V"
-proof cases
-  assume "a = 0\<^sub>F" thus ?thesis by simp
-next
-  assume anz [simp]: "a \<noteq> 0\<^sub>F"
-  { assume "scale a x = 0\<^sub>V"
-    hence "scale (inverse a) (scale a x) = 0\<^sub>V" by simp
-    hence "x = 0\<^sub>V" by simp }
-  thus ?thesis by force
-qed
-
-lemma scale_left_imp_eq:
-  "\<lbrakk>a \<noteq> 0\<^sub>F; scale a x = scale a y\<rbrakk> \<Longrightarrow> x = y"
-proof -
-  assume nonzero: "a \<noteq> 0\<^sub>F"
-  assume "scale a x = scale a y"
-  hence "scale a (x -\<^sub>V y) = 0\<^sub>V"
-     by (simp add: scale_right_diff_distrib)
-  hence "x -\<^sub>V y = 0\<^sub>V" by (simp add: nonzero)
-  thus "x = y" by (simp only: mV_uV_zV_pV.right_minus_eq)
-qed
-
-lemma scale_right_imp_eq:
-  "\<lbrakk>x \<noteq> 0\<^sub>V; scale a x = scale b x\<rbrakk> \<Longrightarrow> a = b"
-proof -
-  assume nonzero: "x \<noteq> 0\<^sub>V"
-  assume "scale a x = scale b x"
-  hence "scale (a -\<^sub>F b) x = 0\<^sub>V"
-     by (simp add: scale_left_diff_distrib)
-  hence "a -\<^sub>F b = 0\<^sub>F" by (simp add: nonzero)
-  thus "a = b" by (simp only: mF_uF_zF_pF.right_minus_eq)
-qed
-
-lemma scale_cancel_left:
-  "scale a x = scale a y \<longleftrightarrow> x = y \<or> a = 0\<^sub>F"
-by (auto intro: scale_left_imp_eq)
-
-lemma scale_cancel_right:
-  "scale a x = scale b x \<longleftrightarrow> a = b \<or> x = 0\<^sub>V"
-by (auto intro: scale_right_imp_eq)
-
-end
-
-(* TODO: locale additive is superseded by group_hom; remove *)
 subsection {* Locale for additive functions *}
 
 locale additive =
   fixes f :: "'a::ab_group_add \<Rightarrow> 'b::ab_group_add"
   assumes add: "f (x + y) = f x + f y"

 apply (simp add: zero)
 done
 
 end
 
+subsection {* Vector spaces *}
+
+locale vector_space =
+  fixes scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b"
+  assumes scale_right_distrib: "scale a (x + y) = scale a x + scale a y"
+  and scale_left_distrib: "scale (a + b) x = scale a x + scale b x"
+  and scale_scale [simp]: "scale a (scale b x) = scale (a * b) x"
+  and scale_one [simp]: "scale 1 x = x"
+begin
+
+lemma scale_left_commute:
+  "scale a (scale b x) = scale b (scale a x)"
+by (simp add: mult_commute)
+
+lemma scale_zero_left [simp]: "scale 0 x = 0"
+  and scale_minus_left [simp]: "scale (- a) x = - (scale a x)"
+  and scale_left_diff_distrib: "scale (a - b) x = scale a x - scale b x"
+proof -
+  interpret s: additive ["\<lambda>a. scale a x"]
+    by unfold_locales (rule scale_left_distrib)
+  show "scale 0 x = 0" by (rule s.zero)
+  show "scale (- a) x = - (scale a x)" by (rule s.minus)
+  show "scale (a - b) x = scale a x - scale b x" by (rule s.diff)
+qed
+
+lemma scale_zero_right [simp]: "scale a 0 = 0"
+  and scale_minus_right [simp]: "scale a (- x) = - (scale a x)"
+  and scale_right_diff_distrib: "scale a (x - y) = scale a x - scale a y"
+proof -
+  interpret s: additive ["\<lambda>x. scale a x"]
+    by unfold_locales (rule scale_right_distrib)
+  show "scale a 0 = 0" by (rule s.zero)
+  show "scale a (- x) = - (scale a x)" by (rule s.minus)
+  show "scale a (x - y) = scale a x - scale a y" by (rule s.diff)
+qed
+
+lemma scale_eq_0_iff [simp]:
+  "scale a x = 0 \<longleftrightarrow> a = 0 \<or> x = 0"
+proof cases
+  assume "a = 0" thus ?thesis by simp
+next
+  assume anz [simp]: "a \<noteq> 0"
+  { assume "scale a x = 0"
+    hence "scale (inverse a) (scale a x) = 0" by simp
+    hence "x = 0" by simp }
+  thus ?thesis by force
+qed
+
+lemma scale_left_imp_eq:
+  "\<lbrakk>a \<noteq> 0; scale a x = scale a y\<rbrakk> \<Longrightarrow> x = y"
+proof -
+  assume nonzero: "a \<noteq> 0"
+  assume "scale a x = scale a y"
+  hence "scale a (x - y) = 0"
+     by (simp add: scale_right_diff_distrib)
+  hence "x - y = 0" by (simp add: nonzero)
+  thus "x = y" by (simp only: right_minus_eq)
+qed
+
+lemma scale_right_imp_eq:
+  "\<lbrakk>x \<noteq> 0; scale a x = scale b x\<rbrakk> \<Longrightarrow> a = b"
+proof -
+  assume nonzero: "x \<noteq> 0"
+  assume "scale a x = scale b x"
+  hence "scale (a - b) x = 0"
+     by (simp add: scale_left_diff_distrib)
+  hence "a - b = 0" by (simp add: nonzero)
+  thus "a = b" by (simp only: right_minus_eq)
+qed
+
+lemma scale_cancel_left:
+  "scale a x = scale a y \<longleftrightarrow> x = y \<or> a = 0"
+by (auto intro: scale_left_imp_eq)
+
+lemma scale_cancel_right:
+  "scale a x = scale b x \<longleftrightarrow> a = b \<or> x = 0"
+by (auto intro: scale_right_imp_eq)
+
+end
+
 subsection {* Real vector spaces *}
 
 class scaleR = type +
   fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "*\<^sub>R" 75)
 begin

   assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
   and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x"
   and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"
   and scaleR_one [simp]: "scaleR 1 x = x"
 
-interpretation real_vector: vector_space
-  [inverse divide "1" times minus uminus "0" plus
-   minus uminus "0" plus "scaleR::real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"]
+interpretation real_vector:
+  vector_space ["scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"]
 apply unfold_locales
 apply (rule scaleR_right_distrib)
 apply (rule scaleR_left_distrib)
 apply (rule scaleR_scaleR)
 apply (rule scaleR_one)