29 lemmas nat_simps = diff_add_inverse2 diff_add_inverse |
29 lemmas nat_simps = diff_add_inverse2 diff_add_inverse |
30 lemmas nat_iffs = le_add1 le_add2 |
30 lemmas nat_iffs = le_add1 le_add2 |
31 |
31 |
32 lemma sum_imp_diff: "j = k + i ==> j - i = (k :: nat)" by arith |
32 lemma sum_imp_diff: "j = k + i ==> j - i = (k :: nat)" by arith |
33 |
33 |
34 lemma nobm1: |
|
35 "0 < (number_of w :: nat) ==> |
|
36 number_of w - (1 :: nat) = number_of (Int.pred w)" |
|
37 apply (unfold nat_number_of_def One_nat_def nat_1 [symmetric] pred_def) |
|
38 apply (simp add: number_of_eq nat_diff_distrib [symmetric]) |
|
39 done |
|
40 |
|
41 lemma zless2: "0 < (2 :: int)" by arith |
34 lemma zless2: "0 < (2 :: int)" by arith |
42 |
35 |
43 lemmas zless2p [simp] = zless2 [THEN zero_less_power] |
36 lemmas zless2p [simp] = zless2 [THEN zero_less_power] |
44 lemmas zle2p [simp] = zless2p [THEN order_less_imp_le] |
37 lemmas zle2p [simp] = zless2p [THEN order_less_imp_le] |
45 |
38 |
46 lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]] |
39 lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]] |
47 lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]] |
40 lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]] |
48 |
41 |
49 -- "the inverse(s) of @{text number_of}" |
|
50 lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1" by arith |
42 lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1" by arith |
51 |
43 |
52 lemma emep1: |
44 lemma emep1: |
53 "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1" |
45 "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1" |
54 apply (simp add: add_commute) |
46 apply (simp add: add_commute) |
280 lemmas pl_pl_mm' = add_commute [THEN [2] trans, THEN pl_pl_mm] |
272 lemmas pl_pl_mm' = add_commute [THEN [2] trans, THEN pl_pl_mm] |
281 |
273 |
282 lemma min_minus [simp] : "min m (m - k) = (m - k :: nat)" by arith |
274 lemma min_minus [simp] : "min m (m - k) = (m - k :: nat)" by arith |
283 |
275 |
284 lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus] |
276 lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus] |
285 |
|
286 lemma nat_no_eq_iff: |
|
287 "(number_of b :: int) >= 0 ==> (number_of c :: int) >= 0 ==> |
|
288 (number_of b = (number_of c :: nat)) = (b = c)" |
|
289 apply (unfold nat_number_of_def) |
|
290 apply safe |
|
291 apply (drule (2) eq_nat_nat_iff [THEN iffD1]) |
|
292 apply (simp add: number_of_eq) |
|
293 done |
|
294 |
277 |
295 lemmas dme = box_equals [OF div_mod_equality add_0_right add_0_right] |
278 lemmas dme = box_equals [OF div_mod_equality add_0_right add_0_right] |
296 lemmas dtle = xtr3 [OF dme [symmetric] le_add1] |
279 lemmas dtle = xtr3 [OF dme [symmetric] le_add1] |
297 lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle] |
280 lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle] |
298 |
281 |