# HG changeset patch
# User huffman
# Date 1219787386 -7200
# Node ID e93b121074fb75549f221d74def3df533e2d988b
# Parent  f945f8d9ad4da21252a0eed30e902459b61e6811
move real_vector class proofs into vector_space and group_hom locales

diff -r f945f8d9ad4d -r e93b121074fb src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Tue Aug 26 18:59:52 2008 +0200
+++ b/src/HOL/Real/RealVector.thy	Tue Aug 26 23:49:46 2008 +0200
@@ -9,6 +9,142 @@
 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 =
@@ -72,6 +208,31 @@
   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"]
+apply unfold_locales
+apply (rule scaleR_right_distrib)
+apply (rule scaleR_left_distrib)
+apply (rule scaleR_scaleR)
+apply (rule scaleR_one)
+done
+
+text {* Recover original theorem names *}
+
+lemmas scaleR_left_commute = real_vector.scale_left_commute
+lemmas scaleR_zero_left = real_vector.scale_zero_left
+lemmas scaleR_minus_left = real_vector.scale_minus_left
+lemmas scaleR_left_diff_distrib = real_vector.scale_left_diff_distrib
+lemmas scaleR_zero_right = real_vector.scale_zero_right
+lemmas scaleR_minus_right = real_vector.scale_minus_right
+lemmas scaleR_right_diff_distrib = real_vector.scale_right_diff_distrib
+lemmas scaleR_eq_0_iff = real_vector.scale_eq_0_iff
+lemmas scaleR_left_imp_eq = real_vector.scale_left_imp_eq
+lemmas scaleR_right_imp_eq = real_vector.scale_right_imp_eq
+lemmas scaleR_cancel_left = real_vector.scale_cancel_left
+lemmas scaleR_cancel_right = real_vector.scale_cancel_right
+
 class real_algebra = real_vector + ring +
   assumes mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)"
   and mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)"
@@ -92,76 +253,12 @@
 apply (rule mult_left_commute)
 done
 
-lemma scaleR_left_commute:
-  fixes x :: "'a::real_vector"
-  shows "scaleR a (scaleR b x) = scaleR b (scaleR a x)"
-by (simp add: mult_commute)
-
 interpretation scaleR_left: additive ["(\<lambda>a. scaleR a x::'a::real_vector)"]
 by unfold_locales (rule scaleR_left_distrib)
 
 interpretation scaleR_right: additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
 by unfold_locales (rule scaleR_right_distrib)
 
-lemmas scaleR_zero_left [simp] = scaleR_left.zero
-
-lemmas scaleR_zero_right [simp] = scaleR_right.zero
-
-lemmas scaleR_minus_left [simp] = scaleR_left.minus
-
-lemmas scaleR_minus_right [simp] = scaleR_right.minus
-
-lemmas scaleR_left_diff_distrib = scaleR_left.diff
-
-lemmas scaleR_right_diff_distrib = scaleR_right.diff
-
-lemma scaleR_eq_0_iff [simp]:
-  fixes x :: "'a::real_vector"
-  shows "(scaleR a x = 0) = (a = 0 \<or> x = 0)"
-proof cases
-  assume "a = 0" thus ?thesis by simp
-next
-  assume anz [simp]: "a \<noteq> 0"
-  { assume "scaleR a x = 0"
-    hence "scaleR (inverse a) (scaleR a x) = 0" by simp
-    hence "x = 0" by simp }
-  thus ?thesis by force
-qed
-
-lemma scaleR_left_imp_eq:
-  fixes x y :: "'a::real_vector"
-  shows "\<lbrakk>a \<noteq> 0; scaleR a x = scaleR a y\<rbrakk> \<Longrightarrow> x = y"
-proof -
-  assume nonzero: "a \<noteq> 0"
-  assume "scaleR a x = scaleR a y"
-  hence "scaleR a (x - y) = 0"
-     by (simp add: scaleR_right_diff_distrib)
-  hence "x - y = 0" by (simp add: nonzero)
-  thus "x = y" by simp
-qed
-
-lemma scaleR_right_imp_eq:
-  fixes x y :: "'a::real_vector"
-  shows "\<lbrakk>x \<noteq> 0; scaleR a x = scaleR b x\<rbrakk> \<Longrightarrow> a = b"
-proof -
-  assume nonzero: "x \<noteq> 0"
-  assume "scaleR a x = scaleR b x"
-  hence "scaleR (a - b) x = 0"
-     by (simp add: scaleR_left_diff_distrib)
-  hence "a - b = 0" by (simp add: nonzero)
-  thus "a = b" by simp
-qed
-
-lemma scaleR_cancel_left:
-  fixes x y :: "'a::real_vector"
-  shows "(scaleR a x = scaleR a y) = (x = y \<or> a = 0)"
-by (auto intro: scaleR_left_imp_eq)
-
-lemma scaleR_cancel_right:
-  fixes x y :: "'a::real_vector"
-  shows "(scaleR a x = scaleR b x) = (a = b \<or> x = 0)"
-by (auto intro: scaleR_right_imp_eq)
-
 lemma nonzero_inverse_scaleR_distrib:
   fixes x :: "'a::real_div_algebra" shows
   "\<lbrakk>a \<noteq> 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> inverse (scaleR a x) = scaleR (inverse a) (inverse x)"