src/HOL/Word/Misc_Numeric.thy
 author haftmann Fri Jun 19 07:53:35 2015 +0200 (2015-06-19) changeset 60517 f16e4fb20652 parent 58874 7172c7ffb047 child 61799 4cf66f21b764 permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
1 (*
2   Author:  Jeremy Dawson, NICTA
3 *)
5 section {* Useful Numerical Lemmas *}
7 theory Misc_Numeric
8 imports Main
9 begin
11 lemma mod_2_neq_1_eq_eq_0:
12   fixes k :: int
13   shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
14   by (fact not_mod_2_eq_1_eq_0)
16 lemma z1pmod2:
17   fixes b :: int
18   shows "(2 * b + 1) mod 2 = (1::int)"
19   by arith
21 lemma diff_le_eq':
22   "a - b \<le> c \<longleftrightarrow> a \<le> b + (c::int)"
23   by arith
25 lemma emep1:
26   fixes n d :: int
27   shows "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
30 lemma int_mod_ge:
31   "a < n \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> a \<le> a mod n"
32   by (metis dual_order.trans le_cases mod_pos_pos_trivial pos_mod_conj)
34 lemma int_mod_ge':
35   "b < 0 \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> b + n \<le> b mod n"
38 lemma int_mod_le':
39   "(0::int) \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
40   by (metis minus_mod_self2 zmod_le_nonneg_dividend)
42 lemma zless2:
43   "0 < (2 :: int)"
44   by (fact zero_less_numeral)
46 lemma zless2p:
47   "0 < (2 ^ n :: int)"
48   by arith
50 lemma zle2p:
51   "0 \<le> (2 ^ n :: int)"
52   by arith
54 lemma m1mod2k:
55   "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
56   using zless2p by (rule zmod_minus1)
58 lemma p1mod22k':
59   fixes b :: int
60   shows "(1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)"
61   using zle2p by (rule pos_zmod_mult_2)
63 lemma p1mod22k:
64   fixes b :: int
65   shows "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1"