374 class norm = type + |
374 class norm = type + |
375 fixes norm :: "'a \<Rightarrow> real" |
375 fixes norm :: "'a \<Rightarrow> real" |
376 |
376 |
377 instance real :: norm |
377 instance real :: norm |
378 real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" .. |
378 real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" .. |
379 |
379 ML"set Toplevel.debug" |
380 axclass real_normed_vector < real_vector, norm |
380 |
|
381 class sgn_div_norm = scaleR + inverse + norm + sgn + |
|
382 assumes sgn_div_norm: "sgn x = x /# norm x" |
|
383 (* FIXME junk needed because of bug in locales *) |
|
384 and "(sgn :: 'a::scaleR \<Rightarrow> 'a) = sgn" |
|
385 and "(inverse :: 'a::scaleR \<Rightarrow> 'a) = inverse" |
|
386 and "(scaleR :: real \<Rightarrow> 'a::scaleR \<Rightarrow> 'a) = scaleR" |
|
387 |
|
388 axclass real_normed_vector < real_vector, sgn_div_norm |
381 norm_ge_zero [simp]: "0 \<le> norm x" |
389 norm_ge_zero [simp]: "0 \<le> norm x" |
382 norm_eq_zero [simp]: "(norm x = 0) = (x = 0)" |
390 norm_eq_zero [simp]: "(norm x = 0) = (x = 0)" |
383 norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y" |
391 norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y" |
384 norm_scaleR: "norm (scaleR a x) = \<bar>a\<bar> * norm x" |
392 norm_scaleR: "norm (scaleR a x) = \<bar>a\<bar> * norm x" |
385 |
393 |
405 thus "norm (1::'a) = 1" by simp |
413 thus "norm (1::'a) = 1" by simp |
406 qed |
414 qed |
407 |
415 |
408 instance real :: real_normed_field |
416 instance real :: real_normed_field |
409 apply (intro_classes, unfold real_norm_def real_scaleR_def) |
417 apply (intro_classes, unfold real_norm_def real_scaleR_def) |
|
418 apply (simp add: real_sgn_def) |
|
419 (* FIXME junk *) |
|
420 apply(rule refl)+ |
410 apply (rule abs_ge_zero) |
421 apply (rule abs_ge_zero) |
411 apply (rule abs_eq_0) |
422 apply (rule abs_eq_0) |
412 apply (rule abs_triangle_ineq) |
423 apply (rule abs_triangle_ineq) |
413 apply (rule abs_mult) |
424 apply (rule abs_mult) |
414 apply (rule abs_mult) |
425 apply (rule abs_mult) |
582 by (induct n) (simp_all add: power_Suc norm_mult) |
593 by (induct n) (simp_all add: power_Suc norm_mult) |
583 |
594 |
584 |
595 |
585 subsection {* Sign function *} |
596 subsection {* Sign function *} |
586 |
597 |
587 definition |
598 lemma norm_sgn: |
588 sgn :: "'a::real_normed_vector \<Rightarrow> 'a" where |
599 "norm (sgn(x::'a::real_normed_vector)) = (if x = 0 then 0 else 1)" |
589 "sgn x = scaleR (inverse (norm x)) x" |
600 by (simp add: sgn_div_norm norm_scaleR) |
590 |
601 |
591 lemma norm_sgn: "norm (sgn x) = (if x = 0 then 0 else 1)" |
602 lemma sgn_zero [simp]: "sgn(0::'a::real_normed_vector) = 0" |
592 unfolding sgn_def by (simp add: norm_scaleR) |
603 by (simp add: sgn_div_norm) |
593 |
604 |
594 lemma sgn_zero [simp]: "sgn 0 = 0" |
605 lemma sgn_zero_iff: "(sgn(x::'a::real_normed_vector) = 0) = (x = 0)" |
595 unfolding sgn_def by simp |
606 by (simp add: sgn_div_norm) |
596 |
607 |
597 lemma sgn_zero_iff: "(sgn x = 0) = (x = 0)" |
608 lemma sgn_minus: "sgn (- x) = - sgn(x::'a::real_normed_vector)" |
598 unfolding sgn_def by simp |
609 by (simp add: sgn_div_norm) |
599 |
610 |
600 lemma sgn_minus: "sgn (- x) = - sgn x" |
611 lemma sgn_scaleR: |
601 unfolding sgn_def by simp |
612 "sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))" |
602 |
613 by (simp add: sgn_div_norm norm_scaleR mult_ac) |
603 lemma sgn_scaleR: "sgn (scaleR r x) = scaleR (sgn r) (sgn x)" |
|
604 unfolding sgn_def by (simp add: norm_scaleR mult_ac) |
|
605 |
614 |
606 lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1" |
615 lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1" |
607 unfolding sgn_def by simp |
616 by (simp add: sgn_div_norm) |
608 |
617 |
609 lemma sgn_of_real: |
618 lemma sgn_of_real: |
610 "sgn (of_real r::'a::real_normed_algebra_1) = of_real (sgn r)" |
619 "sgn (of_real r::'a::real_normed_algebra_1) = of_real (sgn r)" |
611 unfolding of_real_def by (simp only: sgn_scaleR sgn_one) |
620 unfolding of_real_def by (simp only: sgn_scaleR sgn_one) |
612 |
621 |
613 lemma sgn_mult: |
622 lemma sgn_mult: |
614 fixes x y :: "'a::real_normed_div_algebra" |
623 fixes x y :: "'a::real_normed_div_algebra" |
615 shows "sgn (x * y) = sgn x * sgn y" |
624 shows "sgn (x * y) = sgn x * sgn y" |
616 unfolding sgn_def by (simp add: norm_mult mult_commute) |
625 by (simp add: sgn_div_norm norm_mult mult_commute) |
617 |
626 |
618 lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>" |
627 lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>" |
619 unfolding sgn_def by (simp add: divide_inverse) |
628 by (simp add: sgn_div_norm divide_inverse) |
620 |
629 |
621 lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1" |
630 lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1" |
622 unfolding real_sgn_eq by simp |
631 unfolding real_sgn_eq by simp |
623 |
632 |
624 lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1" |
633 lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1" |