414 end |
414 end |
415 |
415 |
416 |
416 |
417 subsection{*The Reals Form an Ordered Field*} |
417 subsection{*The Reals Form an Ordered Field*} |
418 |
418 |
419 instance real :: ordered_field |
419 instance real :: linordered_field |
420 proof |
420 proof |
421 fix x y z :: real |
421 fix x y z :: real |
422 show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono) |
422 show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono) |
423 show "x < y ==> 0 < z ==> z * x < z * y" by (rule real_mult_less_mono2) |
423 show "x < y ==> 0 < z ==> z * x < z * y" by (rule real_mult_less_mono2) |
424 show "\<bar>x\<bar> = (if x < 0 then -x else x)" by (simp only: real_abs_def) |
424 show "\<bar>x\<bar> = (if x < 0 then -x else x)" by (simp only: real_abs_def) |
425 show "sgn x = (if x=0 then 0 else if 0<x then 1 else - 1)" |
425 show "sgn x = (if x=0 then 0 else if 0<x then 1 else - 1)" |
426 by (simp only: real_sgn_def) |
426 by (simp only: real_sgn_def) |
427 qed |
427 qed |
428 |
428 |
429 instance real :: lordered_ab_group_add .. |
|
430 |
|
431 text{*The function @{term real_of_preal} requires many proofs, but it seems |
429 text{*The function @{term real_of_preal} requires many proofs, but it seems |
432 to be essential for proving completeness of the reals from that of the |
430 to be essential for proving completeness of the reals from that of the |
433 positive reals.*} |
431 positive reals.*} |
434 |
432 |
435 lemma real_of_preal_add: |
433 lemma real_of_preal_add: |
521 lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)" |
519 lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)" |
522 by auto |
520 by auto |
523 |
521 |
524 lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)" |
522 lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)" |
525 by (force elim: order_less_asym |
523 by (force elim: order_less_asym |
526 simp add: Ring_and_Field.mult_less_cancel_right) |
524 simp add: mult_less_cancel_right) |
527 |
525 |
528 lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)" |
526 lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)" |
529 apply (simp add: mult_le_cancel_right) |
527 apply (simp add: mult_le_cancel_right) |
530 apply (blast intro: elim: order_less_asym) |
528 apply (blast intro: elim: order_less_asym) |
531 done |
529 done |
583 lemma real_of_int_diff [simp]: "real(x - y) = real (x::int) - real y" |
581 lemma real_of_int_diff [simp]: "real(x - y) = real (x::int) - real y" |
584 by (simp add: real_of_int_def) |
582 by (simp add: real_of_int_def) |
585 |
583 |
586 lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y" |
584 lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y" |
587 by (simp add: real_of_int_def) |
585 by (simp add: real_of_int_def) |
|
586 |
|
587 lemma real_of_int_power [simp]: "real (x ^ n) = real (x::int) ^ n" |
|
588 by (simp add: real_of_int_def of_int_power) |
|
589 |
|
590 lemmas power_real_of_int = real_of_int_power [symmetric] |
588 |
591 |
589 lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))" |
592 lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))" |
590 apply (subst real_eq_of_int)+ |
593 apply (subst real_eq_of_int)+ |
591 apply (rule of_int_setsum) |
594 apply (rule of_int_setsum) |
592 done |
595 done |
696 done |
699 done |
697 |
700 |
698 lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" |
701 lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" |
699 by (insert real_of_int_div2 [of n x], simp) |
702 by (insert real_of_int_div2 [of n x], simp) |
700 |
703 |
|
704 lemma Ints_real_of_int [simp]: "real (x::int) \<in> Ints" |
|
705 unfolding real_of_int_def by (rule Ints_of_int) |
|
706 |
701 |
707 |
702 subsection{*Embedding the Naturals into the Reals*} |
708 subsection{*Embedding the Naturals into the Reals*} |
703 |
709 |
704 lemma real_of_nat_zero [simp]: "real (0::nat) = 0" |
710 lemma real_of_nat_zero [simp]: "real (0::nat) = 0" |
705 by (simp add: real_of_nat_def) |
711 by (simp add: real_of_nat_def) |
730 lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)" |
736 lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)" |
731 by (simp add: real_of_nat_def del: of_nat_Suc) |
737 by (simp add: real_of_nat_def del: of_nat_Suc) |
732 |
738 |
733 lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n" |
739 lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n" |
734 by (simp add: real_of_nat_def of_nat_mult) |
740 by (simp add: real_of_nat_def of_nat_mult) |
|
741 |
|
742 lemma real_of_nat_power [simp]: "real (m ^ n) = real (m::nat) ^ n" |
|
743 by (simp add: real_of_nat_def of_nat_power) |
|
744 |
|
745 lemmas power_real_of_nat = real_of_nat_power [symmetric] |
735 |
746 |
736 lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = |
747 lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = |
737 (SUM x:A. real(f x))" |
748 (SUM x:A. real(f x))" |
738 apply (subst real_eq_of_nat)+ |
749 apply (subst real_eq_of_nat)+ |
739 apply (rule of_nat_setsum) |
750 apply (rule of_nat_setsum) |
767 by (simp add: add: real_of_nat_def) |
778 by (simp add: add: real_of_nat_def) |
768 |
779 |
769 lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0" |
780 lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0" |
770 by (simp add: add: real_of_nat_def) |
781 by (simp add: add: real_of_nat_def) |
771 |
782 |
772 lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat))" |
783 (* FIXME: duplicates real_of_nat_ge_zero *) |
|
784 lemma real_of_nat_ge_zero_cancel_iff: "(0 \<le> real (n::nat))" |
773 by (simp add: add: real_of_nat_def) |
785 by (simp add: add: real_of_nat_def) |
774 |
786 |
775 lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)" |
787 lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)" |
776 apply (subgoal_tac "real n + 1 = real (Suc n)") |
788 apply (subgoal_tac "real n + 1 = real (Suc n)") |
777 apply simp |
789 apply simp |
840 lemma real_nat_eq_real [simp]: "0 <= x ==> real(nat x) = real x" |
852 lemma real_nat_eq_real [simp]: "0 <= x ==> real(nat x) = real x" |
841 apply (subgoal_tac "real(int(nat x)) = real(nat x)") |
853 apply (subgoal_tac "real(int(nat x)) = real(nat x)") |
842 apply force |
854 apply force |
843 apply (simp only: real_of_int_real_of_nat) |
855 apply (simp only: real_of_int_real_of_nat) |
844 done |
856 done |
|
857 |
|
858 lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> Nats" |
|
859 unfolding real_of_nat_def by (rule of_nat_in_Nats) |
|
860 |
|
861 lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> Ints" |
|
862 unfolding real_of_nat_def by (rule Ints_of_nat) |
845 |
863 |
846 |
864 |
847 subsection{* Rationals *} |
865 subsection{* Rationals *} |
848 |
866 |
849 lemma Rats_real_nat[simp]: "real(n::nat) \<in> \<rat>" |
867 lemma Rats_real_nat[simp]: "real(n::nat) \<in> \<rat>" |
951 unfolding number_of_is_id real_number_of_def .. |
969 unfolding number_of_is_id real_number_of_def .. |
952 |
970 |
953 |
971 |
954 text{*Collapse applications of @{term real} to @{term number_of}*} |
972 text{*Collapse applications of @{term real} to @{term number_of}*} |
955 lemma real_number_of [simp]: "real (number_of v :: int) = number_of v" |
973 lemma real_number_of [simp]: "real (number_of v :: int) = number_of v" |
956 by (simp add: real_of_int_def of_int_number_of_eq) |
974 by (simp add: real_of_int_def) |
957 |
975 |
958 lemma real_of_nat_number_of [simp]: |
976 lemma real_of_nat_number_of [simp]: |
959 "real (number_of v :: nat) = |
977 "real (number_of v :: nat) = |
960 (if neg (number_of v :: int) then 0 |
978 (if neg (number_of v :: int) then 0 |
961 else (number_of v :: real))" |
979 else (number_of v :: real))" |
962 by (simp add: real_of_int_real_of_nat [symmetric] int_nat_number_of) |
980 by (simp add: real_of_int_real_of_nat [symmetric]) |
963 |
981 |
964 declaration {* |
982 declaration {* |
965 K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2] |
983 K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2] |
966 (* not needed because x < (y::nat) can be rewritten as Suc x <= y: real_of_nat_less_iff RS iffD2 *) |
984 (* not needed because x < (y::nat) can be rewritten as Suc x <= y: real_of_nat_less_iff RS iffD2 *) |
967 #> Lin_Arith.add_inj_thms [@{thm real_of_int_le_iff} RS iffD2, @{thm real_of_int_inject} RS iffD2] |
985 #> Lin_Arith.add_inj_thms [@{thm real_of_int_le_iff} RS iffD2, @{thm real_of_int_inject} RS iffD2] |
1015 apply (rule_tac x = " (min d1 d2) /2" in exI) |
1033 apply (rule_tac x = " (min d1 d2) /2" in exI) |
1016 apply (simp add: min_def) |
1034 apply (simp add: min_def) |
1017 done |
1035 done |
1018 |
1036 |
1019 |
1037 |
1020 text{*Similar results are proved in @{text Ring_and_Field}*} |
1038 text{*Similar results are proved in @{text Fields}*} |
1021 lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)" |
1039 lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)" |
1022 by auto |
1040 by auto |
1023 |
1041 |
1024 lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y" |
1042 lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y" |
1025 by auto |
1043 by auto |
1030 lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))" |
1048 lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))" |
1031 by (simp add: abs_if) |
1049 by (simp add: abs_if) |
1032 |
1050 |
1033 (* FIXME: redundant, but used by Integration/RealRandVar.thy in AFP *) |
1051 (* FIXME: redundant, but used by Integration/RealRandVar.thy in AFP *) |
1034 lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))" |
1052 lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))" |
1035 by (force simp add: OrderedGroup.abs_le_iff) |
1053 by (force simp add: abs_le_iff) |
1036 |
1054 |
1037 lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)" |
1055 lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)" |
1038 by (simp add: abs_if) |
1056 by (simp add: abs_if) |
1039 |
1057 |
1040 lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)" |
1058 lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)" |
1043 lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x" |
1061 lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x" |
1044 by simp |
1062 by simp |
1045 |
1063 |
1046 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)" |
1064 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)" |
1047 by simp |
1065 by simp |
1048 |
|
1049 instance real :: lordered_ring |
|
1050 proof |
|
1051 fix a::real |
|
1052 show "abs a = sup a (-a)" |
|
1053 by (auto simp add: real_abs_def sup_real_def) |
|
1054 qed |
|
1055 |
1066 |
1056 |
1067 |
1057 subsection {* Implementation of rational real numbers *} |
1068 subsection {* Implementation of rational real numbers *} |
1058 |
1069 |
1059 definition Ratreal :: "rat \<Rightarrow> real" where |
1070 definition Ratreal :: "rat \<Rightarrow> real" where |