808 by auto |
808 by auto |
809 |
809 |
810 |
810 |
811 subsection{*Absolute Value Function for the Reals*} |
811 subsection{*Absolute Value Function for the Reals*} |
812 |
812 |
813 text{*FIXME: these should go!*} |
|
814 lemma abs_eqI1: "(0::real)\<le>x ==> abs x = x" |
|
815 by (simp add: abs_if) |
|
816 |
|
817 lemma abs_eqI2: "(0::real) < x ==> abs x = x" |
|
818 by (simp add: abs_if) |
|
819 |
|
820 lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x" |
|
821 by (simp add: abs_if linorder_not_less [symmetric]) |
|
822 |
|
823 lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))" |
813 lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))" |
824 by (simp add: abs_if) |
814 by (simp add: abs_if) |
825 |
815 |
826 lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))" |
816 lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))" |
827 by (force simp add: Ring_and_Field.abs_less_iff) |
817 by (force simp add: Ring_and_Field.abs_less_iff) |
832 (*FIXME: used only once, in SEQ.ML*) |
822 (*FIXME: used only once, in SEQ.ML*) |
833 lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)" |
823 lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)" |
834 by (simp add: abs_if) |
824 by (simp add: abs_if) |
835 |
825 |
836 lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)" |
826 lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)" |
837 by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero) |
827 by (simp add: real_of_nat_ge_zero) |
838 |
828 |
839 lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x" |
829 lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x" |
840 apply (simp add: linorder_not_less) |
830 apply (simp add: linorder_not_less) |
841 apply (auto intro: abs_ge_self [THEN order_trans]) |
831 apply (auto intro: abs_ge_self [THEN order_trans]) |
842 done |
832 done |
855 {* |
845 {* |
856 val real_lbound_gt_zero = thm"real_lbound_gt_zero"; |
846 val real_lbound_gt_zero = thm"real_lbound_gt_zero"; |
857 val real_less_half_sum = thm"real_less_half_sum"; |
847 val real_less_half_sum = thm"real_less_half_sum"; |
858 val real_gt_half_sum = thm"real_gt_half_sum"; |
848 val real_gt_half_sum = thm"real_gt_half_sum"; |
859 |
849 |
860 val abs_eqI1 = thm"abs_eqI1"; |
|
861 val abs_eqI2 = thm"abs_eqI2"; |
|
862 val abs_minus_eqI2 = thm"abs_minus_eqI2"; |
|
863 val abs_ge_zero = thm"abs_ge_zero"; |
|
864 val abs_idempotent = thm"abs_idempotent"; |
|
865 val abs_eq_0 = thm"abs_eq_0"; |
|
866 val abs_ge_self = thm"abs_ge_self"; |
|
867 val abs_ge_minus_self = thm"abs_ge_minus_self"; |
|
868 val abs_mult = thm"abs_mult"; |
|
869 val abs_inverse = thm"abs_inverse"; |
|
870 val abs_triangle_ineq = thm"abs_triangle_ineq"; |
|
871 val abs_minus_cancel = thm"abs_minus_cancel"; |
|
872 val abs_minus_add_cancel = thm"abs_minus_add_cancel"; |
|
873 val abs_interval_iff = thm"abs_interval_iff"; |
850 val abs_interval_iff = thm"abs_interval_iff"; |
874 val abs_le_interval_iff = thm"abs_le_interval_iff"; |
851 val abs_le_interval_iff = thm"abs_le_interval_iff"; |
875 val abs_add_one_gt_zero = thm"abs_add_one_gt_zero"; |
852 val abs_add_one_gt_zero = thm"abs_add_one_gt_zero"; |
876 val abs_le_zero_iff = thm"abs_le_zero_iff"; |
|
877 val abs_add_one_not_less_self = thm"abs_add_one_not_less_self"; |
853 val abs_add_one_not_less_self = thm"abs_add_one_not_less_self"; |
878 val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq"; |
854 val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq"; |
879 |
|
880 val abs_mult_less = thm"abs_mult_less"; |
|
881 *} |
855 *} |
882 |
856 |
883 |
857 |
884 end |
858 end |