1 (* Title : Real/RealDef.thy |
1 (* Title : Real/RealDef.thy |
2 ID : $Id$ |
2 ID : $Id$ |
3 Author : Jacques D. Fleuriot |
3 Author : Jacques D. Fleuriot |
4 Copyright : 1998 University of Cambridge |
4 Copyright : 1998 University of Cambridge |
5 Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 |
5 Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 |
|
6 Additional contributions by Jeremy Avigad |
6 *) |
7 *) |
7 |
8 |
8 header{*Defining the Reals from the Positive Reals*} |
9 header{*Defining the Reals from the Positive Reals*} |
9 |
10 |
10 theory RealDef |
11 theory RealDef |
633 |
634 |
634 defs (overloaded) |
635 defs (overloaded) |
635 real_of_nat_def: "real z == of_nat z" |
636 real_of_nat_def: "real z == of_nat z" |
636 real_of_int_def: "real z == of_int z" |
637 real_of_int_def: "real z == of_int z" |
637 |
638 |
|
639 lemma real_eq_of_nat: "real = of_nat" |
|
640 apply (rule ext) |
|
641 apply (unfold real_of_nat_def) |
|
642 apply (rule refl) |
|
643 done |
|
644 |
|
645 lemma real_eq_of_int: "real = of_int" |
|
646 apply (rule ext) |
|
647 apply (unfold real_of_int_def) |
|
648 apply (rule refl) |
|
649 done |
|
650 |
638 lemma real_of_int_zero [simp]: "real (0::int) = 0" |
651 lemma real_of_int_zero [simp]: "real (0::int) = 0" |
639 by (simp add: real_of_int_def) |
652 by (simp add: real_of_int_def) |
640 |
653 |
641 lemma real_of_one [simp]: "real (1::int) = (1::real)" |
654 lemma real_of_one [simp]: "real (1::int) = (1::real)" |
642 by (simp add: real_of_int_def) |
655 by (simp add: real_of_int_def) |
643 |
656 |
644 lemma real_of_int_add: "real (x::int) + real y = real (x + y)" |
657 lemma real_of_int_add [simp]: "real(x + y) = real (x::int) + real y" |
645 by (simp add: real_of_int_def) |
658 by (simp add: real_of_int_def) |
646 declare real_of_int_add [symmetric, simp] |
659 |
647 |
660 lemma real_of_int_minus [simp]: "real(-x) = -real (x::int)" |
648 lemma real_of_int_minus: "-real (x::int) = real (-x)" |
661 by (simp add: real_of_int_def) |
649 by (simp add: real_of_int_def) |
662 |
650 declare real_of_int_minus [symmetric, simp] |
663 lemma real_of_int_diff [simp]: "real(x - y) = real (x::int) - real y" |
651 |
664 by (simp add: real_of_int_def) |
652 lemma real_of_int_diff: "real (x::int) - real y = real (x - y)" |
665 |
653 by (simp add: real_of_int_def) |
666 lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y" |
654 declare real_of_int_diff [symmetric, simp] |
667 by (simp add: real_of_int_def) |
655 |
668 |
656 lemma real_of_int_mult: "real (x::int) * real y = real (x * y)" |
669 lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))" |
657 by (simp add: real_of_int_def) |
670 apply (subst real_eq_of_int)+ |
658 declare real_of_int_mult [symmetric, simp] |
671 apply (rule of_int_setsum) |
|
672 done |
|
673 |
|
674 lemma real_of_int_setprod [simp]: "real ((PROD x:A. f x)::int) = |
|
675 (PROD x:A. real(f x))" |
|
676 apply (subst real_eq_of_int)+ |
|
677 apply (rule of_int_setprod) |
|
678 done |
659 |
679 |
660 lemma real_of_int_zero_cancel [simp]: "(real x = 0) = (x = (0::int))" |
680 lemma real_of_int_zero_cancel [simp]: "(real x = 0) = (x = (0::int))" |
661 by (simp add: real_of_int_def) |
681 by (simp add: real_of_int_def) |
662 |
682 |
663 lemma real_of_int_inject [iff]: "(real (x::int) = real y) = (x = y)" |
683 lemma real_of_int_inject [iff]: "(real (x::int) = real y) = (x = y)" |
667 by (simp add: real_of_int_def) |
687 by (simp add: real_of_int_def) |
668 |
688 |
669 lemma real_of_int_le_iff [simp]: "(real (x::int) \<le> real y) = (x \<le> y)" |
689 lemma real_of_int_le_iff [simp]: "(real (x::int) \<le> real y) = (x \<le> y)" |
670 by (simp add: real_of_int_def) |
690 by (simp add: real_of_int_def) |
671 |
691 |
|
692 lemma real_of_int_gt_zero_cancel_iff [simp]: "(0 < real (n::int)) = (0 < n)" |
|
693 by (simp add: real_of_int_def) |
|
694 |
|
695 lemma real_of_int_ge_zero_cancel_iff [simp]: "(0 <= real (n::int)) = (0 <= n)" |
|
696 by (simp add: real_of_int_def) |
|
697 |
|
698 lemma real_of_int_lt_zero_cancel_iff [simp]: "(real (n::int) < 0) = (n < 0)" |
|
699 by (simp add: real_of_int_def) |
|
700 |
|
701 lemma real_of_int_le_zero_cancel_iff [simp]: "(real (n::int) <= 0) = (n <= 0)" |
|
702 by (simp add: real_of_int_def) |
|
703 |
|
704 lemma int_less_real_le: "((n::int) < m) = (real n + 1 <= real m)" |
|
705 apply (subgoal_tac "real n + 1 = real (n + 1)") |
|
706 apply (simp del: real_of_int_add) |
|
707 apply auto |
|
708 done |
|
709 |
|
710 lemma int_le_real_less: "((n::int) <= m) = (real n < real m + 1)" |
|
711 apply (subgoal_tac "real m + 1 = real (m + 1)") |
|
712 apply (simp del: real_of_int_add) |
|
713 apply simp |
|
714 done |
|
715 |
|
716 lemma real_of_int_div_aux: "d ~= 0 ==> (real (x::int)) / (real d) = |
|
717 real (x div d) + (real (x mod d)) / (real d)" |
|
718 proof - |
|
719 assume "d ~= 0" |
|
720 have "x = (x div d) * d + x mod d" |
|
721 by auto |
|
722 then have "real x = real (x div d) * real d + real(x mod d)" |
|
723 by (simp only: real_of_int_mult [THEN sym] real_of_int_add [THEN sym]) |
|
724 then have "real x / real d = ... / real d" |
|
725 by simp |
|
726 then show ?thesis |
|
727 by (auto simp add: add_divide_distrib ring_eq_simps prems) |
|
728 qed |
|
729 |
|
730 lemma real_of_int_div: "(d::int) ~= 0 ==> d dvd n ==> |
|
731 real(n div d) = real n / real d" |
|
732 apply (frule real_of_int_div_aux [of d n]) |
|
733 apply simp |
|
734 apply (simp add: zdvd_iff_zmod_eq_0) |
|
735 done |
|
736 |
|
737 lemma real_of_int_div2: |
|
738 "0 <= real (n::int) / real (x) - real (n div x)" |
|
739 apply (case_tac "x = 0") |
|
740 apply simp |
|
741 apply (case_tac "0 < x") |
|
742 apply (simp add: compare_rls) |
|
743 apply (subst real_of_int_div_aux) |
|
744 apply simp |
|
745 apply simp |
|
746 apply (subst zero_le_divide_iff) |
|
747 apply auto |
|
748 apply (simp add: compare_rls) |
|
749 apply (subst real_of_int_div_aux) |
|
750 apply simp |
|
751 apply simp |
|
752 apply (subst zero_le_divide_iff) |
|
753 apply auto |
|
754 done |
|
755 |
|
756 lemma real_of_int_div3: |
|
757 "real (n::int) / real (x) - real (n div x) <= 1" |
|
758 apply(case_tac "x = 0") |
|
759 apply simp |
|
760 apply (simp add: compare_rls) |
|
761 apply (subst real_of_int_div_aux) |
|
762 apply assumption |
|
763 apply simp |
|
764 apply (subst divide_le_eq) |
|
765 apply clarsimp |
|
766 apply (rule conjI) |
|
767 apply (rule impI) |
|
768 apply (rule order_less_imp_le) |
|
769 apply simp |
|
770 apply (rule impI) |
|
771 apply (rule order_less_imp_le) |
|
772 apply simp |
|
773 done |
|
774 |
|
775 lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" |
|
776 by (insert real_of_int_div2 [of n x], simp) |
672 |
777 |
673 subsection{*Embedding the Naturals into the Reals*} |
778 subsection{*Embedding the Naturals into the Reals*} |
674 |
779 |
675 lemma real_of_nat_zero [simp]: "real (0::nat) = 0" |
780 lemma real_of_nat_zero [simp]: "real (0::nat) = 0" |
676 by (simp add: real_of_nat_def) |
781 by (simp add: real_of_nat_def) |
699 by (simp add: real_of_nat_def del: of_nat_Suc) |
804 by (simp add: real_of_nat_def del: of_nat_Suc) |
700 |
805 |
701 lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n" |
806 lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n" |
702 by (simp add: real_of_nat_def) |
807 by (simp add: real_of_nat_def) |
703 |
808 |
|
809 lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = |
|
810 (SUM x:A. real(f x))" |
|
811 apply (subst real_eq_of_nat)+ |
|
812 apply (rule of_nat_setsum) |
|
813 done |
|
814 |
|
815 lemma real_of_nat_setprod [simp]: "real ((PROD x:A. f x)::nat) = |
|
816 (PROD x:A. real(f x))" |
|
817 apply (subst real_eq_of_nat)+ |
|
818 apply (rule of_nat_setprod) |
|
819 done |
|
820 |
|
821 lemma real_of_card: "real (card A) = setsum (%x.1) A" |
|
822 apply (subst card_eq_setsum) |
|
823 apply (subst real_of_nat_setsum) |
|
824 apply simp |
|
825 done |
|
826 |
704 lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)" |
827 lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)" |
705 by (simp add: real_of_nat_def) |
828 by (simp add: real_of_nat_def) |
706 |
829 |
707 lemma real_of_nat_zero_iff [iff]: "(real (n::nat) = 0) = (n = 0)" |
830 lemma real_of_nat_zero_iff [iff]: "(real (n::nat) = 0) = (n = 0)" |
708 by (simp add: real_of_nat_def) |
831 by (simp add: real_of_nat_def) |
720 by (simp add: add: real_of_nat_def) |
843 by (simp add: add: real_of_nat_def) |
721 |
844 |
722 lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat)) = (0 \<le> n)" |
845 lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat)) = (0 \<le> n)" |
723 by (simp add: add: real_of_nat_def) |
846 by (simp add: add: real_of_nat_def) |
724 |
847 |
|
848 lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)" |
|
849 apply (subgoal_tac "real n + 1 = real (Suc n)") |
|
850 apply simp |
|
851 apply (auto simp add: real_of_nat_Suc) |
|
852 done |
|
853 |
|
854 lemma nat_le_real_less: "((n::nat) <= m) = (real n < real m + 1)" |
|
855 apply (subgoal_tac "real m + 1 = real (Suc m)") |
|
856 apply (simp add: less_Suc_eq_le) |
|
857 apply (simp add: real_of_nat_Suc) |
|
858 done |
|
859 |
|
860 lemma real_of_nat_div_aux: "0 < d ==> (real (x::nat)) / (real d) = |
|
861 real (x div d) + (real (x mod d)) / (real d)" |
|
862 proof - |
|
863 assume "0 < d" |
|
864 have "x = (x div d) * d + x mod d" |
|
865 by auto |
|
866 then have "real x = real (x div d) * real d + real(x mod d)" |
|
867 by (simp only: real_of_nat_mult [THEN sym] real_of_nat_add [THEN sym]) |
|
868 then have "real x / real d = \<dots> / real d" |
|
869 by simp |
|
870 then show ?thesis |
|
871 by (auto simp add: add_divide_distrib ring_eq_simps prems) |
|
872 qed |
|
873 |
|
874 lemma real_of_nat_div: "0 < (d::nat) ==> d dvd n ==> |
|
875 real(n div d) = real n / real d" |
|
876 apply (frule real_of_nat_div_aux [of d n]) |
|
877 apply simp |
|
878 apply (subst dvd_eq_mod_eq_0 [THEN sym]) |
|
879 apply assumption |
|
880 done |
|
881 |
|
882 lemma real_of_nat_div2: |
|
883 "0 <= real (n::nat) / real (x) - real (n div x)" |
|
884 apply(case_tac "x = 0") |
|
885 apply simp |
|
886 apply (simp add: compare_rls) |
|
887 apply (subst real_of_nat_div_aux) |
|
888 apply assumption |
|
889 apply simp |
|
890 apply (subst zero_le_divide_iff) |
|
891 apply simp |
|
892 done |
|
893 |
|
894 lemma real_of_nat_div3: |
|
895 "real (n::nat) / real (x) - real (n div x) <= 1" |
|
896 apply(case_tac "x = 0") |
|
897 apply simp |
|
898 apply (simp add: compare_rls) |
|
899 apply (subst real_of_nat_div_aux) |
|
900 apply assumption |
|
901 apply simp |
|
902 done |
|
903 |
|
904 lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x" |
|
905 by (insert real_of_nat_div2 [of n x], simp) |
|
906 |
725 lemma real_of_int_real_of_nat: "real (int n) = real n" |
907 lemma real_of_int_real_of_nat: "real (int n) = real n" |
726 by (simp add: real_of_nat_def real_of_int_def int_eq_of_nat) |
908 by (simp add: real_of_nat_def real_of_int_def int_eq_of_nat) |
727 |
909 |
728 lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n" |
910 lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n" |
729 by (simp add: real_of_int_def real_of_nat_def) |
911 by (simp add: real_of_int_def real_of_nat_def) |
730 |
912 |
731 |
913 lemma real_nat_eq_real [simp]: "0 <= x ==> real(nat x) = real x" |
|
914 apply (subgoal_tac "real(int(nat x)) = real(nat x)") |
|
915 apply force |
|
916 apply (simp only: real_of_int_real_of_nat) |
|
917 done |
732 |
918 |
733 subsection{*Numerals and Arithmetic*} |
919 subsection{*Numerals and Arithmetic*} |
734 |
920 |
735 instance real :: number .. |
921 instance real :: number .. |
736 |
922 |