src/HOL/Real/RealVector.thy
 author huffman Sat Sep 16 02:35:58 2006 +0200 (2006-09-16) changeset 20551 ba543692bfa1 parent 20533 49442b3024bb child 20554 c433e78d4203 permissions -rw-r--r--
 huffman@20504 ` 1` ```(* Title : RealVector.thy ``` huffman@20504 ` 2` ``` ID: \$Id\$ ``` huffman@20504 ` 3` ``` Author : Brian Huffman ``` huffman@20504 ` 4` ```*) ``` huffman@20504 ` 5` huffman@20504 ` 6` ```header {* Vector Spaces and Algebras over the Reals *} ``` huffman@20504 ` 7` huffman@20504 ` 8` ```theory RealVector ``` huffman@20504 ` 9` ```imports RealDef ``` huffman@20504 ` 10` ```begin ``` huffman@20504 ` 11` huffman@20504 ` 12` ```subsection {* Locale for additive functions *} ``` huffman@20504 ` 13` huffman@20504 ` 14` ```locale additive = ``` huffman@20504 ` 15` ``` fixes f :: "'a::ab_group_add \ 'b::ab_group_add" ``` huffman@20504 ` 16` ``` assumes add: "f (x + y) = f x + f y" ``` huffman@20504 ` 17` huffman@20504 ` 18` ```lemma (in additive) zero: "f 0 = 0" ``` huffman@20504 ` 19` ```proof - ``` huffman@20504 ` 20` ``` have "f 0 = f (0 + 0)" by simp ``` huffman@20504 ` 21` ``` also have "\ = f 0 + f 0" by (rule add) ``` huffman@20504 ` 22` ``` finally show "f 0 = 0" by simp ``` huffman@20504 ` 23` ```qed ``` huffman@20504 ` 24` huffman@20504 ` 25` ```lemma (in additive) minus: "f (- x) = - f x" ``` huffman@20504 ` 26` ```proof - ``` huffman@20504 ` 27` ``` have "f (- x) + f x = f (- x + x)" by (rule add [symmetric]) ``` huffman@20504 ` 28` ``` also have "\ = - f x + f x" by (simp add: zero) ``` huffman@20504 ` 29` ``` finally show "f (- x) = - f x" by (rule add_right_imp_eq) ``` huffman@20504 ` 30` ```qed ``` huffman@20504 ` 31` huffman@20504 ` 32` ```lemma (in additive) diff: "f (x - y) = f x - f y" ``` huffman@20504 ` 33` ```by (simp add: diff_def add minus) ``` huffman@20504 ` 34` huffman@20504 ` 35` huffman@20504 ` 36` ```subsection {* Real vector spaces *} ``` huffman@20504 ` 37` huffman@20504 ` 38` ```axclass scaleR < type ``` huffman@20504 ` 39` huffman@20504 ` 40` ```consts ``` huffman@20504 ` 41` ``` scaleR :: "real \ 'a \ 'a::scaleR" (infixr "*#" 75) ``` huffman@20504 ` 42` huffman@20504 ` 43` ```syntax (xsymbols) ``` huffman@20504 ` 44` ``` scaleR :: "real \ 'a \ 'a::scaleR" (infixr "*\<^sub>R" 75) ``` huffman@20504 ` 45` huffman@20504 ` 46` ```axclass real_vector < scaleR, ab_group_add ``` huffman@20504 ` 47` ``` scaleR_right_distrib: "a *# (x + y) = a *# x + a *# y" ``` huffman@20504 ` 48` ``` scaleR_left_distrib: "(a + b) *# x = a *# x + b *# x" ``` huffman@20504 ` 49` ``` scaleR_assoc: "(a * b) *# x = a *# b *# x" ``` huffman@20504 ` 50` ``` scaleR_one [simp]: "1 *# x = x" ``` huffman@20504 ` 51` huffman@20504 ` 52` ```axclass real_algebra < real_vector, ring ``` huffman@20504 ` 53` ``` mult_scaleR_left: "a *# x * y = a *# (x * y)" ``` huffman@20504 ` 54` ``` mult_scaleR_right: "x * a *# y = a *# (x * y)" ``` huffman@20504 ` 55` huffman@20504 ` 56` ```lemmas scaleR_scaleR = scaleR_assoc [symmetric] ``` huffman@20504 ` 57` huffman@20504 ` 58` ```lemma scaleR_left_commute: ``` huffman@20504 ` 59` ``` fixes x :: "'a::real_vector" ``` huffman@20504 ` 60` ``` shows "a *# b *# x = b *# a *# x" ``` huffman@20504 ` 61` ```by (simp add: scaleR_scaleR mult_commute) ``` huffman@20504 ` 62` huffman@20504 ` 63` ```lemma additive_scaleR_right: "additive (\x. a *# x :: 'a::real_vector)" ``` huffman@20504 ` 64` ```by (rule additive.intro, rule scaleR_right_distrib) ``` huffman@20504 ` 65` huffman@20504 ` 66` ```lemma additive_scaleR_left: "additive (\a. a *# x :: 'a::real_vector)" ``` huffman@20504 ` 67` ```by (rule additive.intro, rule scaleR_left_distrib) ``` huffman@20504 ` 68` huffman@20504 ` 69` ```lemmas scaleR_zero_left [simp] = ``` huffman@20504 ` 70` ``` additive.zero [OF additive_scaleR_left, standard] ``` huffman@20504 ` 71` huffman@20504 ` 72` ```lemmas scaleR_zero_right [simp] = ``` huffman@20504 ` 73` ``` additive.zero [OF additive_scaleR_right, standard] ``` huffman@20504 ` 74` huffman@20504 ` 75` ```lemmas scaleR_minus_left [simp] = ``` huffman@20504 ` 76` ``` additive.minus [OF additive_scaleR_left, standard] ``` huffman@20504 ` 77` huffman@20504 ` 78` ```lemmas scaleR_minus_right [simp] = ``` huffman@20504 ` 79` ``` additive.minus [OF additive_scaleR_right, standard] ``` huffman@20504 ` 80` huffman@20504 ` 81` ```lemmas scaleR_left_diff_distrib = ``` huffman@20504 ` 82` ``` additive.diff [OF additive_scaleR_left, standard] ``` huffman@20504 ` 83` huffman@20504 ` 84` ```lemmas scaleR_right_diff_distrib = ``` huffman@20504 ` 85` ``` additive.diff [OF additive_scaleR_right, standard] ``` huffman@20504 ` 86` huffman@20504 ` 87` huffman@20504 ` 88` ```subsection {* Real normed vector spaces *} ``` huffman@20504 ` 89` huffman@20504 ` 90` ```axclass norm < type ``` huffman@20533 ` 91` ```consts norm :: "'a::norm \ real" ``` huffman@20504 ` 92` huffman@20504 ` 93` ```axclass real_normed_vector < real_vector, norm ``` huffman@20533 ` 94` ``` norm_ge_zero [simp]: "0 \ norm x" ``` huffman@20533 ` 95` ``` norm_eq_zero [simp]: "(norm x = 0) = (x = 0)" ``` huffman@20533 ` 96` ``` norm_triangle_ineq: "norm (x + y) \ norm x + norm y" ``` huffman@20533 ` 97` ``` norm_scaleR: "norm (a *# x) = \a\ * norm x" ``` huffman@20504 ` 98` huffman@20504 ` 99` ```axclass real_normed_algebra < real_normed_vector, real_algebra ``` huffman@20533 ` 100` ``` norm_mult_ineq: "norm (x * y) \ norm x * norm y" ``` huffman@20504 ` 101` huffman@20504 ` 102` ```axclass real_normed_div_algebra ``` huffman@20504 ` 103` ``` < real_normed_vector, real_algebra, division_ring ``` huffman@20533 ` 104` ``` norm_mult: "norm (x * y) = norm x * norm y" ``` huffman@20533 ` 105` ``` norm_one [simp]: "norm 1 = 1" ``` huffman@20504 ` 106` huffman@20504 ` 107` ```instance real_normed_div_algebra < real_normed_algebra ``` huffman@20504 ` 108` ```by (intro_classes, simp add: norm_mult) ``` huffman@20504 ` 109` huffman@20533 ` 110` ```lemma norm_zero [simp]: "norm (0::'a::real_normed_vector) = 0" ``` huffman@20504 ` 111` ```by simp ``` huffman@20504 ` 112` huffman@20504 ` 113` ```lemma zero_less_norm_iff [simp]: ``` huffman@20533 ` 114` ``` fixes x :: "'a::real_normed_vector" shows "(0 < norm x) = (x \ 0)" ``` huffman@20504 ` 115` ```by (simp add: order_less_le) ``` huffman@20504 ` 116` huffman@20504 ` 117` ```lemma norm_minus_cancel [simp]: ``` huffman@20533 ` 118` ``` fixes x :: "'a::real_normed_vector" shows "norm (- x) = norm x" ``` huffman@20504 ` 119` ```proof - ``` huffman@20533 ` 120` ``` have "norm (- x) = norm (- 1 *# x)" ``` huffman@20504 ` 121` ``` by (simp only: scaleR_minus_left scaleR_one) ``` huffman@20533 ` 122` ``` also have "\ = \- 1\ * norm x" ``` huffman@20504 ` 123` ``` by (rule norm_scaleR) ``` huffman@20504 ` 124` ``` finally show ?thesis by simp ``` huffman@20504 ` 125` ```qed ``` huffman@20504 ` 126` huffman@20504 ` 127` ```lemma norm_minus_commute: ``` huffman@20533 ` 128` ``` fixes a b :: "'a::real_normed_vector" shows "norm (a - b) = norm (b - a)" ``` huffman@20504 ` 129` ```proof - ``` huffman@20533 ` 130` ``` have "norm (a - b) = norm (- (a - b))" ``` huffman@20533 ` 131` ``` by (simp only: norm_minus_cancel) ``` huffman@20533 ` 132` ``` also have "\ = norm (b - a)" by simp ``` huffman@20504 ` 133` ``` finally show ?thesis . ``` huffman@20504 ` 134` ```qed ``` huffman@20504 ` 135` huffman@20504 ` 136` ```lemma norm_triangle_ineq2: ``` huffman@20533 ` 137` ``` fixes a :: "'a::real_normed_vector" ``` huffman@20533 ` 138` ``` shows "norm a - norm b \ norm (a - b)" ``` huffman@20504 ` 139` ```proof - ``` huffman@20533 ` 140` ``` have "norm (a - b + b) \ norm (a - b) + norm b" ``` huffman@20504 ` 141` ``` by (rule norm_triangle_ineq) ``` huffman@20504 ` 142` ``` also have "(a - b + b) = a" ``` huffman@20504 ` 143` ``` by simp ``` huffman@20504 ` 144` ``` finally show ?thesis ``` huffman@20504 ` 145` ``` by (simp add: compare_rls) ``` huffman@20504 ` 146` ```qed ``` huffman@20504 ` 147` huffman@20504 ` 148` ```lemma norm_triangle_ineq4: ``` huffman@20533 ` 149` ``` fixes a :: "'a::real_normed_vector" ``` huffman@20533 ` 150` ``` shows "norm (a - b) \ norm a + norm b" ``` huffman@20504 ` 151` ```proof - ``` huffman@20533 ` 152` ``` have "norm (a - b) = norm (a + - b)" ``` huffman@20504 ` 153` ``` by (simp only: diff_minus) ``` huffman@20533 ` 154` ``` also have "\ \ norm a + norm (- b)" ``` huffman@20504 ` 155` ``` by (rule norm_triangle_ineq) ``` huffman@20504 ` 156` ``` finally show ?thesis ``` huffman@20504 ` 157` ``` by simp ``` huffman@20504 ` 158` ```qed ``` huffman@20504 ` 159` huffman@20551 ` 160` ```lemma norm_diff_triangle_ineq: ``` huffman@20551 ` 161` ``` fixes a b c d :: "'a::real_normed_vector" ``` huffman@20551 ` 162` ``` shows "norm ((a + b) - (c + d)) \ norm (a - c) + norm (b - d)" ``` huffman@20551 ` 163` ```proof - ``` huffman@20551 ` 164` ``` have "norm ((a + b) - (c + d)) = norm ((a - c) + (b - d))" ``` huffman@20551 ` 165` ``` by (simp add: diff_minus add_ac) ``` huffman@20551 ` 166` ``` also have "\ \ norm (a - c) + norm (b - d)" ``` huffman@20551 ` 167` ``` by (rule norm_triangle_ineq) ``` huffman@20551 ` 168` ``` finally show ?thesis . ``` huffman@20551 ` 169` ```qed ``` huffman@20551 ` 170` huffman@20504 ` 171` ```lemma nonzero_norm_inverse: ``` huffman@20504 ` 172` ``` fixes a :: "'a::real_normed_div_algebra" ``` huffman@20533 ` 173` ``` shows "a \ 0 \ norm (inverse a) = inverse (norm a)" ``` huffman@20504 ` 174` ```apply (rule inverse_unique [symmetric]) ``` huffman@20504 ` 175` ```apply (simp add: norm_mult [symmetric]) ``` huffman@20504 ` 176` ```done ``` huffman@20504 ` 177` huffman@20504 ` 178` ```lemma norm_inverse: ``` huffman@20504 ` 179` ``` fixes a :: "'a::{real_normed_div_algebra,division_by_zero}" ``` huffman@20533 ` 180` ``` shows "norm (inverse a) = inverse (norm a)" ``` huffman@20504 ` 181` ```apply (case_tac "a = 0", simp) ``` huffman@20504 ` 182` ```apply (erule nonzero_norm_inverse) ``` huffman@20504 ` 183` ```done ``` huffman@20504 ` 184` huffman@20504 ` 185` huffman@20504 ` 186` ```subsection {* Instances for type @{typ real} *} ``` huffman@20504 ` 187` huffman@20504 ` 188` ```instance real :: scaleR .. ``` huffman@20504 ` 189` huffman@20504 ` 190` ```defs (overloaded) ``` huffman@20504 ` 191` ``` real_scaleR_def: "a *# x \ a * x" ``` huffman@20504 ` 192` huffman@20504 ` 193` ```instance real :: real_algebra ``` huffman@20504 ` 194` ```apply (intro_classes, unfold real_scaleR_def) ``` huffman@20504 ` 195` ```apply (rule right_distrib) ``` huffman@20504 ` 196` ```apply (rule left_distrib) ``` huffman@20504 ` 197` ```apply (rule mult_assoc) ``` huffman@20504 ` 198` ```apply (rule mult_1_left) ``` huffman@20504 ` 199` ```apply (rule mult_assoc) ``` huffman@20504 ` 200` ```apply (rule mult_left_commute) ``` huffman@20504 ` 201` ```done ``` huffman@20504 ` 202` huffman@20504 ` 203` ```instance real :: norm .. ``` huffman@20504 ` 204` huffman@20504 ` 205` ```defs (overloaded) ``` huffman@20533 ` 206` ``` real_norm_def: "norm r \ \r\" ``` huffman@20504 ` 207` huffman@20504 ` 208` ```instance real :: real_normed_div_algebra ``` huffman@20504 ` 209` ```apply (intro_classes, unfold real_norm_def real_scaleR_def) ``` huffman@20504 ` 210` ```apply (rule abs_ge_zero) ``` huffman@20504 ` 211` ```apply (rule abs_eq_0) ``` huffman@20504 ` 212` ```apply (rule abs_triangle_ineq) ``` huffman@20504 ` 213` ```apply (rule abs_mult) ``` huffman@20504 ` 214` ```apply (rule abs_mult) ``` huffman@20504 ` 215` ```apply (rule abs_one) ``` huffman@20504 ` 216` ```done ``` huffman@20504 ` 217` huffman@20504 ` 218` ```end ```