711 |
711 |
712 lemma mod_1 [simp]: "m mod Suc 0 = 0" |
712 lemma mod_1 [simp]: "m mod Suc 0 = 0" |
713 by (induct m) (simp_all add: mod_geq) |
713 by (induct m) (simp_all add: mod_geq) |
714 |
714 |
715 lemma mod_mult_distrib: "(m mod n) * (k\<Colon>nat) = (m * k) mod (n * k)" |
715 lemma mod_mult_distrib: "(m mod n) * (k\<Colon>nat) = (m * k) mod (n * k)" |
716 apply (cases "n = 0", simp) |
716 by (fact mod_mult_mult2 [symmetric]) (* FIXME: generalize *) |
717 apply (cases "k = 0", simp) |
|
718 apply (induct m rule: nat_less_induct) |
|
719 apply (subst mod_if, simp) |
|
720 apply (simp add: mod_geq diff_mult_distrib) |
|
721 done |
|
722 |
717 |
723 lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)" |
718 lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)" |
724 by (simp add: mult_commute [of k] mod_mult_distrib) |
719 by (fact mod_mult_mult1 [symmetric]) (* FIXME: generalize *) |
725 |
720 |
726 (* a simple rearrangement of mod_div_equality: *) |
721 (* a simple rearrangement of mod_div_equality: *) |
727 lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)" |
722 lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)" |
728 by (cut_tac a = m and b = n in mod_div_equality2, arith) |
723 using mod_div_equality2 [of n m] by arith |
729 |
724 |
730 lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)" |
725 lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)" |
731 apply (drule mod_less_divisor [where m = m]) |
726 apply (drule mod_less_divisor [where m = m]) |
732 apply simp |
727 apply simp |
733 done |
728 done |
816 apply (rule div_le_mono2) |
811 apply (rule div_le_mono2) |
817 apply (simp_all (no_asm_simp)) |
812 apply (simp_all (no_asm_simp)) |
818 done |
813 done |
819 |
814 |
820 (* Similar for "less than" *) |
815 (* Similar for "less than" *) |
821 lemma div_less_dividend [rule_format]: |
816 lemma div_less_dividend [simp]: |
822 "!!n::nat. 1<n ==> 0 < m --> m div n < m" |
817 "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m" |
823 apply (induct_tac m rule: nat_less_induct) |
818 apply (induct m rule: nat_less_induct) |
824 apply (rename_tac "m") |
819 apply (rename_tac "m") |
825 apply (case_tac "m<n", simp) |
820 apply (case_tac "m<n", simp) |
826 apply (subgoal_tac "0<n") |
821 apply (subgoal_tac "0<n") |
827 prefer 2 apply simp |
822 prefer 2 apply simp |
828 apply (simp add: div_geq) |
823 apply (simp add: div_geq) |
830 apply (subgoal_tac "(m-n) div n < (m-n) ") |
825 apply (subgoal_tac "(m-n) div n < (m-n) ") |
831 apply (rule impI less_trans_Suc)+ |
826 apply (rule impI less_trans_Suc)+ |
832 apply assumption |
827 apply assumption |
833 apply (simp_all) |
828 apply (simp_all) |
834 done |
829 done |
835 |
|
836 declare div_less_dividend [simp] |
|
837 |
830 |
838 text{*A fact for the mutilated chess board*} |
831 text{*A fact for the mutilated chess board*} |
839 lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))" |
832 lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))" |
840 apply (case_tac "n=0", simp) |
833 apply (case_tac "n=0", simp) |
841 apply (induct "m" rule: nat_less_induct) |
834 apply (induct "m" rule: nat_less_induct) |
961 show ?P by simp |
954 show ?P by simp |
962 qed |
955 qed |
963 qed |
956 qed |
964 |
957 |
965 theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n" |
958 theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n" |
966 apply (rule_tac P="%x. m mod n = x - (m div n) * n" in |
959 using mod_div_equality [of m n] by arith |
967 subst [OF mod_div_equality [of _ n]]) |
960 |
968 apply arith |
961 lemma div_mod_equality': "(m::nat) div n * n = m - m mod n" |
969 done |
962 using mod_div_equality [of m n] by arith |
970 |
963 (* FIXME: very similar to mult_div_cancel *) |
971 lemma div_mod_equality': |
|
972 fixes m n :: nat |
|
973 shows "m div n * n = m - m mod n" |
|
974 proof - |
|
975 have "m mod n \<le> m mod n" .. |
|
976 from div_mod_equality have |
|
977 "m div n * n + m mod n - m mod n = m - m mod n" by simp |
|
978 with diff_add_assoc [OF `m mod n \<le> m mod n`, of "m div n * n"] have |
|
979 "m div n * n + (m mod n - m mod n) = m - m mod n" |
|
980 by simp |
|
981 then show ?thesis by simp |
|
982 qed |
|
983 |
964 |
984 |
965 |
985 subsubsection {* An ``induction'' law for modulus arithmetic. *} |
966 subsubsection {* An ``induction'' law for modulus arithmetic. *} |
986 |
967 |
987 lemma mod_induct_0: |
968 lemma mod_induct_0: |
1069 qed |
1050 qed |
1070 with j show ?thesis by blast |
1051 with j show ?thesis by blast |
1071 qed |
1052 qed |
1072 |
1053 |
1073 lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)" |
1054 lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)" |
1074 by (auto simp add: numeral_2_eq_2 le_div_geq) |
1055 by (simp add: numeral_2_eq_2 le_div_geq) |
|
1056 |
|
1057 lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2" |
|
1058 by (simp add: numeral_2_eq_2 le_mod_geq) |
1075 |
1059 |
1076 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)" |
1060 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)" |
1077 by (simp add: nat_mult_2 [symmetric]) |
1061 by (simp add: nat_mult_2 [symmetric]) |
1078 |
|
1079 lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2" |
|
1080 apply (subgoal_tac "m mod 2 < 2") |
|
1081 apply (erule less_2_cases [THEN disjE]) |
|
1082 apply (simp_all (no_asm_simp) add: Let_def mod_Suc) |
|
1083 done |
|
1084 |
1062 |
1085 lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1" |
1063 lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1" |
1086 proof - |
1064 proof - |
1087 { fix n :: nat have "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all } |
1065 { fix n :: nat have "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all } |
1088 moreover have "m mod 2 < 2" by simp |
1066 moreover have "m mod 2 < 2" by simp |
1115 apply (simp_all add: mod_Suc) |
1093 apply (simp_all add: mod_Suc) |
1116 done |
1094 done |
1117 |
1095 |
1118 declare Suc_times_mod_eq [of "numeral w", simp] for w |
1096 declare Suc_times_mod_eq [of "numeral w", simp] for w |
1119 |
1097 |
1120 lemma [simp]: "n div k \<le> (Suc n) div k" |
1098 lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k" |
1121 by (simp add: div_le_mono) |
1099 by (simp add: div_le_mono) |
1122 |
1100 |
1123 lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2" |
1101 lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2" |
1124 by (cases n) simp_all |
1102 by (cases n) simp_all |
1125 |
1103 |
1126 lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2" |
1104 lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2" |