809 definition |
809 definition |
810 int :: "nat \<Rightarrow> int" |
810 int :: "nat \<Rightarrow> int" |
811 where |
811 where |
812 [code func del]: "int m = Abs_Integ (intrel `` {(m, 0)})" |
812 [code func del]: "int m = Abs_Integ (intrel `` {(m, 0)})" |
813 |
813 |
|
814 text{*Agreement with the specific embedding for the integers*} |
|
815 lemma int_eq_of_nat: "int = (of_nat :: nat => int)" |
|
816 by (simp add: expand_fun_eq int_of_nat_def int_def) |
|
817 |
814 lemma inj_int: "inj int" |
818 lemma inj_int: "inj int" |
815 by (simp add: inj_on_def int_def) |
819 by (simp add: inj_on_def int_def) |
816 |
820 |
817 lemma int_int_eq [iff]: "(int m = int n) = (m = n)" |
821 lemma int_int_eq [iff]: "(int m = int n) = (m = n)" |
818 by (fast elim!: inj_int [THEN injD]) |
822 unfolding int_eq_of_nat by (rule of_nat_eq_iff) |
819 |
823 |
820 lemma zadd_int: "(int m) + (int n) = int (m + n)" |
824 lemma zadd_int: "(int m) + (int n) = int (m + n)" |
821 by (simp add: int_def add) |
825 unfolding int_eq_of_nat by (rule of_nat_add [symmetric]) |
822 |
826 |
823 lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z" |
827 lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z" |
824 by (simp add: zadd_int zadd_assoc [symmetric]) |
828 unfolding int_eq_of_nat by simp |
825 |
829 |
826 lemma int_mult: "int (m * n) = (int m) * (int n)" |
830 lemma int_mult: "int (m * n) = (int m) * (int n)" |
827 by (simp add: int_def mult) |
831 unfolding int_eq_of_nat by (rule of_nat_mult) |
828 |
832 |
829 text{*Compatibility binding*} |
833 text{*Compatibility binding*} |
830 lemmas zmult_int = int_mult [symmetric] |
834 lemmas zmult_int = int_mult [symmetric] |
831 |
835 |
832 lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)" |
836 lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)" |
833 by (simp add: Zero_int_def [folded int_def]) |
837 unfolding int_eq_of_nat by (rule of_nat_eq_0_iff) |
834 |
838 |
835 lemma zless_int [simp]: "(int m < int n) = (m<n)" |
839 lemma zless_int [simp]: "(int m < int n) = (m<n)" |
836 by (simp add: le add int_def linorder_not_le [symmetric]) |
840 unfolding int_eq_of_nat by (rule of_nat_less_iff) |
837 |
841 |
838 lemma int_less_0_conv [simp]: "~ (int k < 0)" |
842 lemma int_less_0_conv [simp]: "~ (int k < 0)" |
839 by (simp add: Zero_int_def [folded int_def]) |
843 unfolding int_eq_of_nat by (rule of_nat_less_0_iff) |
840 |
844 |
841 lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)" |
845 lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)" |
842 by (simp add: Zero_int_def [folded int_def]) |
846 unfolding int_eq_of_nat by (rule of_nat_0_less_iff) |
843 |
847 |
844 lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)" |
848 lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)" |
845 by (simp add: linorder_not_less [symmetric]) |
849 unfolding int_eq_of_nat by (rule of_nat_le_iff) |
846 |
850 |
847 lemma zero_zle_int [simp]: "(0 \<le> int n)" |
851 lemma zero_zle_int [simp]: "(0 \<le> int n)" |
848 by (simp add: Zero_int_def [folded int_def]) |
852 unfolding int_eq_of_nat by (rule of_nat_0_le_iff) |
849 |
853 |
850 lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)" |
854 lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)" |
851 by (simp add: Zero_int_def [folded int_def]) |
855 unfolding int_eq_of_nat by (rule of_nat_le_0_iff) |
852 |
856 |
853 lemma int_0 [simp]: "int 0 = (0::int)" |
857 lemma int_0 [simp]: "int 0 = (0::int)" |
854 by (simp add: Zero_int_def [folded int_def]) |
858 unfolding int_eq_of_nat by (rule of_nat_0) |
855 |
859 |
856 lemma int_1 [simp]: "int 1 = 1" |
860 lemma int_1 [simp]: "int 1 = 1" |
857 by (simp add: One_int_def [folded int_def]) |
861 unfolding int_eq_of_nat by (rule of_nat_1) |
858 |
862 |
859 lemma int_Suc0_eq_1: "int (Suc 0) = 1" |
863 lemma int_Suc0_eq_1: "int (Suc 0) = 1" |
860 by (simp add: One_int_def [folded int_def]) |
864 unfolding int_eq_of_nat by simp |
861 |
865 |
862 lemma int_Suc: "int (Suc m) = 1 + (int m)" |
866 lemma int_Suc: "int (Suc m) = 1 + (int m)" |
863 by (simp add: One_int_def [folded int_def] zadd_int) |
867 unfolding int_eq_of_nat by simp |
864 |
868 |
865 lemma nat_int [simp]: "nat(int n) = n" |
869 lemma nat_int [simp]: "nat(int n) = n" |
866 by (simp add: nat int_def) |
870 unfolding int_eq_of_nat by (rule nat_int_of_nat) |
867 |
871 |
868 lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)" |
872 lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)" |
869 by (cases z, simp add: nat le int_def Zero_int_def) |
873 unfolding int_eq_of_nat by (rule int_of_nat_nat_eq) |
870 |
874 |
871 corollary nat_0_le: "0 \<le> z ==> int (nat z) = z" |
875 corollary nat_0_le: "0 \<le> z ==> int (nat z) = z" |
872 by simp |
876 unfolding int_eq_of_nat by (rule nat_0_le') |
873 |
877 |
874 lemma nonneg_eq_int: "[| 0 \<le> z; !!m. z = int m ==> P |] ==> P" |
878 lemma nonneg_eq_int: "[| 0 \<le> z; !!m. z = int m ==> P |] ==> P" |
875 by (blast dest: nat_0_le sym) |
879 unfolding int_eq_of_nat by (blast elim: nonneg_eq_int_of_nat) |
876 |
880 |
877 lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)" |
881 lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)" |
878 by (cases w, simp add: nat le int_def Zero_int_def, arith) |
882 unfolding int_eq_of_nat by (rule nat_eq_iff') |
879 |
883 |
880 corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)" |
884 corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)" |
881 by (simp only: eq_commute [of m] nat_eq_iff) |
885 unfolding int_eq_of_nat by (rule nat_eq_iff2') |
882 |
886 |
883 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)" |
887 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)" |
884 apply (cases w) |
888 unfolding int_eq_of_nat by (rule nat_less_iff') |
885 apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith) |
|
886 done |
|
887 |
889 |
888 lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)" |
890 lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)" |
889 by (auto simp add: nat_eq_iff2) |
891 unfolding int_eq_of_nat by (rule int_of_nat_eq_iff) |
890 |
892 |
891 lemma nat_zminus_int [simp]: "nat (- (int n)) = 0" |
893 lemma nat_zminus_int [simp]: "nat (- (int n)) = 0" |
892 by (simp add: int_def minus nat Zero_int_def) |
894 unfolding int_eq_of_nat by (rule nat_zminus_int_of_nat) |
893 |
895 |
894 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)" |
896 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)" |
895 by (cases z, simp add: nat le int_def linorder_not_le [symmetric], arith) |
897 unfolding int_eq_of_nat by (rule zless_nat_eq_int_zless') |
896 |
898 |
897 lemma negative_zless_0: "- (int (Suc n)) < 0" |
899 lemma negative_zless_0: "- (int (Suc n)) < 0" |
898 by (simp add: order_less_le) |
900 unfolding int_eq_of_nat by (rule negative_zless_0') |
899 |
901 |
900 lemma negative_zless [iff]: "- (int (Suc n)) < int m" |
902 lemma negative_zless [iff]: "- (int (Suc n)) < int m" |
901 by (rule negative_zless_0 [THEN order_less_le_trans], simp) |
903 unfolding int_eq_of_nat by (rule negative_zless') |
902 |
904 |
903 lemma negative_zle_0: "- int n \<le> 0" |
905 lemma negative_zle_0: "- int n \<le> 0" |
904 by (simp add: minus_le_iff) |
906 unfolding int_eq_of_nat by (rule negative_zle_0') |
905 |
907 |
906 lemma negative_zle [iff]: "- int n \<le> int m" |
908 lemma negative_zle [iff]: "- int n \<le> int m" |
907 by (rule order_trans [OF negative_zle_0 zero_zle_int]) |
909 unfolding int_eq_of_nat by (rule negative_zle') |
908 |
910 |
909 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))" |
911 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))" |
910 by (subst le_minus_iff, simp) |
912 unfolding int_eq_of_nat by (rule not_zle_0_negative') |
911 |
913 |
912 lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)" |
914 lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)" |
913 by (simp add: int_def le minus Zero_int_def) |
915 unfolding int_eq_of_nat by (rule int_zle_neg') |
914 |
916 |
915 lemma not_int_zless_negative [simp]: "~ (int n < - int m)" |
917 lemma not_int_zless_negative [simp]: "~ (int n < - int m)" |
916 by (simp add: linorder_not_less) |
918 unfolding int_eq_of_nat by (rule not_int_zless_negative') |
917 |
919 |
918 lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)" |
920 lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)" |
919 by (force simp add: order_eq_iff [of "- int n"] int_zle_neg) |
921 unfolding int_eq_of_nat by (rule negative_eq_positive') |
920 |
922 |
921 lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)" |
923 lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)" |
922 proof (cases w, cases z, simp add: le add int_def) |
924 unfolding int_eq_of_nat by (rule zle_iff_zadd') |
923 fix a b c d |
|
924 assume "w = Abs_Integ (intrel `` {(a,b)})" "z = Abs_Integ (intrel `` {(c,d)})" |
|
925 show "(a+d \<le> c+b) = (\<exists>n. c+b = a+n+d)" |
|
926 proof |
|
927 assume "a + d \<le> c + b" |
|
928 thus "\<exists>n. c + b = a + n + d" |
|
929 by (auto intro!: exI [where x="c+b - (a+d)"]) |
|
930 next |
|
931 assume "\<exists>n. c + b = a + n + d" |
|
932 then obtain n where "c + b = a + n + d" .. |
|
933 thus "a + d \<le> c + b" by arith |
|
934 qed |
|
935 qed |
|
936 |
925 |
937 lemma abs_int_eq [simp]: "abs (int m) = int m" |
926 lemma abs_int_eq [simp]: "abs (int m) = int m" |
938 by (simp add: abs_if) |
927 unfolding int_eq_of_nat by (rule abs_of_nat) |
939 |
928 |
940 lemma not_neg_int [simp]: "~ neg(int n)" |
929 lemma not_neg_int [simp]: "~ neg(int n)" |
941 by (simp add: neg_def) |
930 unfolding int_eq_of_nat by (rule not_neg_int_of_nat) |
942 |
931 |
943 lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))" |
932 lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))" |
944 by (simp add: neg_def neg_less_0_iff_less) |
933 unfolding int_eq_of_nat by (rule neg_zminus_int_of_nat) |
945 |
934 |
946 lemma not_neg_nat: "~ neg z ==> int (nat z) = z" |
935 lemma not_neg_nat: "~ neg z ==> int (nat z) = z" |
947 by (simp add: linorder_not_less neg_def) |
936 unfolding int_eq_of_nat by (rule not_neg_nat') |
948 |
|
949 text{*Agreement with the specific embedding for the integers*} |
|
950 lemma int_eq_of_nat: "int = (of_nat :: nat => int)" |
|
951 proof |
|
952 fix n |
|
953 show "int n = of_nat n" by (induct n, simp_all add: int_Suc add_ac) |
|
954 qed |
|
955 |
937 |
956 lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n" |
938 lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n" |
957 unfolding int_eq_of_nat by (rule of_int_of_nat_eq) |
939 unfolding int_eq_of_nat by (rule of_int_of_nat_eq) |
958 |
940 |
959 lemma int_setsum: "int (setsum f A) = (\<Sum>x\<in>A. int(f x))" |
941 lemma int_setsum: "int (setsum f A) = (\<Sum>x\<in>A. int(f x))" |