equal
deleted
inserted
replaced
52 where |
52 where |
53 "x /\<^sub>R r == scaleR (inverse r) x" |
53 "x /\<^sub>R r == scaleR (inverse r) x" |
54 |
54 |
55 end |
55 end |
56 |
56 |
57 instance real :: scaleR |
57 instantiation real :: scaleR |
58 real_scaleR_def [simp]: "scaleR a x \<equiv> a * x" .. |
58 begin |
|
59 |
|
60 definition |
|
61 real_scaleR_def [simp]: "scaleR a x = a * x" |
|
62 |
|
63 instance .. |
|
64 |
|
65 end |
59 |
66 |
60 class real_vector = scaleR + ab_group_add + |
67 class real_vector = scaleR + ab_group_add + |
61 assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y" |
68 assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y" |
62 and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x" |
69 and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x" |
63 and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x" |
70 and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x" |
369 subsection {* Real normed vector spaces *} |
376 subsection {* Real normed vector spaces *} |
370 |
377 |
371 class norm = type + |
378 class norm = type + |
372 fixes norm :: "'a \<Rightarrow> real" |
379 fixes norm :: "'a \<Rightarrow> real" |
373 |
380 |
374 instance real :: norm |
381 instantiation real :: norm |
375 real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" .. |
382 begin |
|
383 |
|
384 definition |
|
385 real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" |
|
386 |
|
387 instance .. |
|
388 |
|
389 end |
376 |
390 |
377 class sgn_div_norm = scaleR + norm + sgn + |
391 class sgn_div_norm = scaleR + norm + sgn + |
378 assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x" |
392 assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x" |
379 |
393 |
380 class real_normed_vector = real_vector + sgn_div_norm + |
394 class real_normed_vector = real_vector + sgn_div_norm + |