33 by (simp add: diff_def add minus) |
33 by (simp add: diff_def add minus) |
34 |
34 |
35 |
35 |
36 subsection {* Real vector spaces *} |
36 subsection {* Real vector spaces *} |
37 |
37 |
38 axclass scaleR < type |
38 class scaleR = type + |
39 |
39 fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" |
40 consts |
40 |
41 scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a::scaleR" (infixr "*#" 75) |
41 notation |
|
42 scaleR (infixr "*#" 75) |
42 |
43 |
43 abbreviation |
44 abbreviation |
44 divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a::scaleR" (infixl "'/#" 70) where |
45 divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a::scaleR" (infixl "'/#" 70) where |
45 "x /# r == scaleR (inverse r) x" |
46 "x /# r == scaleR (inverse r) x" |
46 |
47 |
47 notation (xsymbols) |
48 notation (xsymbols) |
48 scaleR (infixr "*\<^sub>R" 75) and |
49 scaleR (infixr "*\<^sub>R" 75) and |
49 divideR (infixl "'/\<^sub>R" 70) |
50 divideR (infixl "'/\<^sub>R" 70) |
50 |
51 |
51 instance real :: scaleR .. |
52 instance real :: scaleR |
52 |
53 real_scaleR_def: "scaleR a x \<equiv> a * x" .. |
53 defs (overloaded) |
|
54 real_scaleR_def: "scaleR a x \<equiv> a * x" |
|
55 |
54 |
56 axclass real_vector < scaleR, ab_group_add |
55 axclass real_vector < scaleR, ab_group_add |
57 scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y" |
56 scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y" |
58 scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x" |
57 scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x" |
59 scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x" |
58 scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x" |
360 by (rule Reals_cases) auto |
359 by (rule Reals_cases) auto |
361 |
360 |
362 |
361 |
363 subsection {* Real normed vector spaces *} |
362 subsection {* Real normed vector spaces *} |
364 |
363 |
365 axclass norm < type |
364 class norm = type + |
366 consts norm :: "'a::norm \<Rightarrow> real" |
365 fixes norm :: "'a \<Rightarrow> real" |
367 |
366 |
368 instance real :: norm .. |
367 instance real :: norm |
369 |
368 real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" .. |
370 defs (overloaded) |
|
371 real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" |
|
372 |
369 |
373 axclass normed < plus, zero, norm |
370 axclass normed < plus, zero, norm |
374 norm_ge_zero [simp]: "0 \<le> norm x" |
371 norm_ge_zero [simp]: "0 \<le> norm x" |
375 norm_eq_zero [simp]: "(norm x = 0) = (x = 0)" |
372 norm_eq_zero [simp]: "(norm x = 0) = (x = 0)" |
376 norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y" |
373 norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y" |