equal
deleted
inserted
replaced
167 by (cases z1, cases z2, cases z3, simp add: real_add preal_add_assoc) |
167 by (cases z1, cases z2, cases z3, simp add: real_add preal_add_assoc) |
168 |
168 |
169 lemma real_add_zero_left: "(0::real) + z = z" |
169 lemma real_add_zero_left: "(0::real) + z = z" |
170 by (cases z, simp add: real_add real_zero_def preal_add_ac) |
170 by (cases z, simp add: real_add real_zero_def preal_add_ac) |
171 |
171 |
172 instance real :: plus_ac0 |
172 instance real :: comm_monoid_add |
173 by (intro_classes, |
173 by (intro_classes, |
174 (assumption | |
174 (assumption | |
175 rule real_add_commute real_add_assoc real_add_zero_left)+) |
175 rule real_add_commute real_add_assoc real_add_zero_left)+) |
176 |
176 |
177 |
177 |
279 subsection{*The Real Numbers form a Field*} |
279 subsection{*The Real Numbers form a Field*} |
280 |
280 |
281 instance real :: field |
281 instance real :: field |
282 proof |
282 proof |
283 fix x y z :: real |
283 fix x y z :: real |
284 show "(x + y) + z = x + (y + z)" by (rule real_add_assoc) |
|
285 show "x + y = y + x" by (rule real_add_commute) |
|
286 show "0 + x = x" by simp |
|
287 show "- x + x = 0" by (rule real_add_minus_left) |
284 show "- x + x = 0" by (rule real_add_minus_left) |
288 show "x - y = x + (-y)" by (simp add: real_diff_def) |
285 show "x - y = x + (-y)" by (simp add: real_diff_def) |
289 show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc) |
286 show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc) |
290 show "x * y = y * x" by (rule real_mult_commute) |
287 show "x * y = y * x" by (rule real_mult_commute) |
291 show "1 * x = x" by (rule real_mult_1) |
288 show "1 * x = x" by (rule real_mult_1) |
310 (*Pull negations out*) |
307 (*Pull negations out*) |
311 declare minus_mult_right [symmetric, simp] |
308 declare minus_mult_right [symmetric, simp] |
312 minus_mult_left [symmetric, simp] |
309 minus_mult_left [symmetric, simp] |
313 |
310 |
314 lemma real_mult_1_right: "z * (1::real) = z" |
311 lemma real_mult_1_right: "z * (1::real) = z" |
315 by (rule Ring_and_Field.mult_1_right) |
312 by (rule OrderedGroup.mult_1_right) |
316 |
313 |
317 |
314 |
318 subsection{*The @{text "\<le>"} Ordering*} |
315 subsection{*The @{text "\<le>"} Ordering*} |
319 |
316 |
320 lemma real_le_refl: "w \<le> (w::real)" |
317 lemma real_le_refl: "w \<le> (w::real)" |
552 |
549 |
553 lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x" |
550 lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x" |
554 by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1]) |
551 by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1]) |
555 |
552 |
556 lemma real_add_less_le_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::real)" |
553 lemma real_add_less_le_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::real)" |
557 by (rule Ring_and_Field.add_less_le_mono) |
554 by (rule OrderedGroup.add_less_le_mono) |
558 |
555 |
559 lemma real_add_le_less_mono: |
556 lemma real_add_le_less_mono: |
560 "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z" |
557 "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z" |
561 by (rule Ring_and_Field.add_le_less_mono) |
558 by (rule OrderedGroup.add_le_less_mono) |
562 |
559 |
563 lemma real_le_square [simp]: "(0::real) \<le> x*x" |
560 lemma real_le_square [simp]: "(0::real) \<le> x*x" |
564 by (rule Ring_and_Field.zero_le_square) |
561 by (rule Ring_and_Field.zero_le_square) |
565 |
562 |
566 |
563 |
595 "[| x < y; r1 < r2; (0::real) \<le> r1; 0 \<le> x|] ==> r1 * x < r2 * y" |
592 "[| x < y; r1 < r2; (0::real) \<le> r1; 0 \<le> x|] ==> r1 * x < r2 * y" |
596 by (rule Ring_and_Field.mult_strict_mono') |
593 by (rule Ring_and_Field.mult_strict_mono') |
597 |
594 |
598 text{*FIXME: delete or at least combine the next two lemmas*} |
595 text{*FIXME: delete or at least combine the next two lemmas*} |
599 lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)" |
596 lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)" |
600 apply (drule Ring_and_Field.equals_zero_I [THEN sym]) |
597 apply (drule OrderedGroup.equals_zero_I [THEN sym]) |
601 apply (cut_tac x = y in real_le_square) |
598 apply (cut_tac x = y in real_le_square) |
602 apply (auto, drule order_antisym, auto) |
599 apply (auto, drule order_antisym, auto) |
603 done |
600 done |
604 |
601 |
605 lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)" |
602 lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)" |
846 |
843 |
847 lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))" |
844 lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))" |
848 by (force simp add: Ring_and_Field.abs_less_iff) |
845 by (force simp add: Ring_and_Field.abs_less_iff) |
849 |
846 |
850 lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))" |
847 lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))" |
851 by (force simp add: Ring_and_Field.abs_le_iff) |
848 by (force simp add: OrderedGroup.abs_le_iff) |
852 |
849 |
853 (*FIXME: used only once, in SEQ.ML*) |
850 (*FIXME: used only once, in SEQ.ML*) |
854 lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)" |
851 lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)" |
855 by (simp add: real_abs_def) |
852 by (simp add: real_abs_def) |
856 |
853 |
890 val abs_eqI1 = thm"abs_eqI1"; |
887 val abs_eqI1 = thm"abs_eqI1"; |
891 val abs_eqI2 = thm"abs_eqI2"; |
888 val abs_eqI2 = thm"abs_eqI2"; |
892 val abs_minus_eqI2 = thm"abs_minus_eqI2"; |
889 val abs_minus_eqI2 = thm"abs_minus_eqI2"; |
893 val abs_ge_zero = thm"abs_ge_zero"; |
890 val abs_ge_zero = thm"abs_ge_zero"; |
894 val abs_idempotent = thm"abs_idempotent"; |
891 val abs_idempotent = thm"abs_idempotent"; |
895 val abs_zero_iff = thm"abs_zero_iff"; |
892 val abs_eq_0 = thm"abs_eq_0"; |
896 val abs_ge_self = thm"abs_ge_self"; |
893 val abs_ge_self = thm"abs_ge_self"; |
897 val abs_ge_minus_self = thm"abs_ge_minus_self"; |
894 val abs_ge_minus_self = thm"abs_ge_minus_self"; |
898 val abs_mult = thm"abs_mult"; |
895 val abs_mult = thm"abs_mult"; |
899 val abs_inverse = thm"abs_inverse"; |
896 val abs_inverse = thm"abs_inverse"; |
900 val abs_triangle_ineq = thm"abs_triangle_ineq"; |
897 val abs_triangle_ineq = thm"abs_triangle_ineq"; |