1090 qed |
1098 qed |
1091 qed |
1099 qed |
1092 with j show ?thesis by blast |
1100 with j show ?thesis by blast |
1093 qed |
1101 qed |
1094 |
1102 |
|
1103 lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)" |
|
1104 by (auto simp add: numeral_2_eq_2 le_div_geq) |
|
1105 |
|
1106 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)" |
|
1107 by (simp add: nat_mult_2 [symmetric]) |
|
1108 |
|
1109 lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2" |
|
1110 apply (subgoal_tac "m mod 2 < 2") |
|
1111 apply (erule less_2_cases [THEN disjE]) |
|
1112 apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1) |
|
1113 done |
|
1114 |
|
1115 lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1" |
|
1116 proof - |
|
1117 { fix n :: nat have "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (induct n) simp_all } |
|
1118 moreover have "m mod 2 < 2" by simp |
|
1119 ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" . |
|
1120 then show ?thesis by auto |
|
1121 qed |
|
1122 |
|
1123 text{*These lemmas collapse some needless occurrences of Suc: |
|
1124 at least three Sucs, since two and fewer are rewritten back to Suc again! |
|
1125 We already have some rules to simplify operands smaller than 3.*} |
|
1126 |
|
1127 lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)" |
|
1128 by (simp add: Suc3_eq_add_3) |
|
1129 |
|
1130 lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)" |
|
1131 by (simp add: Suc3_eq_add_3) |
|
1132 |
|
1133 lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n" |
|
1134 by (simp add: Suc3_eq_add_3) |
|
1135 |
|
1136 lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n" |
|
1137 by (simp add: Suc3_eq_add_3) |
|
1138 |
|
1139 lemmas Suc_div_eq_add3_div_number_of = |
|
1140 Suc_div_eq_add3_div [of _ "number_of v", standard] |
|
1141 declare Suc_div_eq_add3_div_number_of [simp] |
|
1142 |
|
1143 lemmas Suc_mod_eq_add3_mod_number_of = |
|
1144 Suc_mod_eq_add3_mod [of _ "number_of v", standard] |
|
1145 declare Suc_mod_eq_add3_mod_number_of [simp] |
|
1146 |
|
1147 |
|
1148 subsection {* Proof Tools setup; Combination and Cancellation Simprocs *} |
|
1149 |
|
1150 declare split_div[of _ _ "number_of k", standard, arith_split] |
|
1151 declare split_mod[of _ _ "number_of k", standard, arith_split] |
|
1152 |
|
1153 |
|
1154 subsubsection{*For @{text combine_numerals}*} |
|
1155 |
|
1156 lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)" |
|
1157 by (simp add: add_mult_distrib) |
|
1158 |
|
1159 |
|
1160 subsubsection{*For @{text cancel_numerals}*} |
|
1161 |
|
1162 lemma nat_diff_add_eq1: |
|
1163 "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)" |
|
1164 by (simp split add: nat_diff_split add: add_mult_distrib) |
|
1165 |
|
1166 lemma nat_diff_add_eq2: |
|
1167 "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))" |
|
1168 by (simp split add: nat_diff_split add: add_mult_distrib) |
|
1169 |
|
1170 lemma nat_eq_add_iff1: |
|
1171 "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)" |
|
1172 by (auto split add: nat_diff_split simp add: add_mult_distrib) |
|
1173 |
|
1174 lemma nat_eq_add_iff2: |
|
1175 "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)" |
|
1176 by (auto split add: nat_diff_split simp add: add_mult_distrib) |
|
1177 |
|
1178 lemma nat_less_add_iff1: |
|
1179 "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)" |
|
1180 by (auto split add: nat_diff_split simp add: add_mult_distrib) |
|
1181 |
|
1182 lemma nat_less_add_iff2: |
|
1183 "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)" |
|
1184 by (auto split add: nat_diff_split simp add: add_mult_distrib) |
|
1185 |
|
1186 lemma nat_le_add_iff1: |
|
1187 "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)" |
|
1188 by (auto split add: nat_diff_split simp add: add_mult_distrib) |
|
1189 |
|
1190 lemma nat_le_add_iff2: |
|
1191 "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)" |
|
1192 by (auto split add: nat_diff_split simp add: add_mult_distrib) |
|
1193 |
|
1194 |
|
1195 subsubsection{*For @{text cancel_numeral_factors} *} |
|
1196 |
|
1197 lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)" |
|
1198 by auto |
|
1199 |
|
1200 lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)" |
|
1201 by auto |
|
1202 |
|
1203 lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)" |
|
1204 by auto |
|
1205 |
|
1206 lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)" |
|
1207 by auto |
|
1208 |
|
1209 lemma nat_mult_dvd_cancel_disj[simp]: |
|
1210 "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))" |
|
1211 by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric]) |
|
1212 |
|
1213 lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)" |
|
1214 by(auto) |
|
1215 |
|
1216 |
|
1217 subsubsection{*For @{text cancel_factor} *} |
|
1218 |
|
1219 lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)" |
|
1220 by auto |
|
1221 |
|
1222 lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)" |
|
1223 by auto |
|
1224 |
|
1225 lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)" |
|
1226 by auto |
|
1227 |
|
1228 lemma nat_mult_div_cancel_disj[simp]: |
|
1229 "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)" |
|
1230 by (simp add: nat_mult_div_cancel1) |
|
1231 |
|
1232 |
|
1233 use "Tools/numeral_simprocs.ML" |
|
1234 |
|
1235 use "Tools/nat_numeral_simprocs.ML" |
|
1236 |
|
1237 declaration {* |
|
1238 K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]) |
|
1239 #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, |
|
1240 @{thm nat_0}, @{thm nat_1}, |
|
1241 @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of}, |
|
1242 @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less}, |
|
1243 @{thm le_Suc_number_of}, @{thm le_number_of_Suc}, |
|
1244 @{thm less_Suc_number_of}, @{thm less_number_of_Suc}, |
|
1245 @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc}, |
|
1246 @{thm mult_Suc}, @{thm mult_Suc_right}, |
|
1247 @{thm add_Suc}, @{thm add_Suc_right}, |
|
1248 @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of}, |
|
1249 @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, |
|
1250 @{thm if_True}, @{thm if_False}]) |
|
1251 #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc |
|
1252 :: Numeral_Simprocs.combine_numerals |
|
1253 :: Numeral_Simprocs.cancel_numerals) |
|
1254 #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals)) |
|
1255 *} |
|
1256 |
1095 end |
1257 end |