author | kuncar |
Wed, 23 Apr 2014 17:57:56 +0200 | |
changeset 56677 | 660ffb526069 |
parent 54872 | af81b2357e08 |
child 57512 | cc97b347b301 |
permissions | -rw-r--r-- |
24333 | 1 |
(* |
2 |
Author: Jeremy Dawson, NICTA |
|
24350 | 3 |
*) |
24333 | 4 |
|
24350 | 5 |
header {* Useful Numerical Lemmas *} |
24333 | 6 |
|
37655 | 7 |
theory Misc_Numeric |
51301 | 8 |
imports Main Parity |
25592 | 9 |
begin |
24333 | 10 |
|
54847
d6cf9a5b9be9
prefer plain bool over dedicated type for binary digits
haftmann
parents:
54221
diff
changeset
|
11 |
lemma mod_2_neq_1_eq_eq_0: |
d6cf9a5b9be9
prefer plain bool over dedicated type for binary digits
haftmann
parents:
54221
diff
changeset
|
12 |
fixes k :: int |
d6cf9a5b9be9
prefer plain bool over dedicated type for binary digits
haftmann
parents:
54221
diff
changeset
|
13 |
shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0" |
54869 | 14 |
by (fact not_mod_2_eq_1_eq_0) |
54847
d6cf9a5b9be9
prefer plain bool over dedicated type for binary digits
haftmann
parents:
54221
diff
changeset
|
15 |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
16 |
lemma z1pmod2: |
54871 | 17 |
fixes b :: int |
18 |
shows "(2 * b + 1) mod 2 = (1::int)" |
|
19 |
by arith |
|
20 |
||
21 |
lemma diff_le_eq': |
|
22 |
"a - b \<le> c \<longleftrightarrow> a \<le> b + (c::int)" |
|
54869 | 23 |
by arith |
24333 | 24 |
|
25 |
lemma emep1: |
|
54871 | 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" |
|
28 |
by (auto simp add: pos_zmod_mult_2 add_commute even_equiv_def) |
|
29 |
||
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) |
|
24333 | 33 |
|
54871 | 34 |
lemma int_mod_ge': |
35 |
"b < 0 \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> b + n \<le> b mod n" |
|
36 |
by (metis add_less_same_cancel2 int_mod_ge mod_add_self2) |
|
24333 | 37 |
|
54871 | 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) |
|
24333 | 41 |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
42 |
lemma zless2: |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
43 |
"0 < (2 :: int)" |
54869 | 44 |
by (fact zero_less_numeral) |
24465 | 45 |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
46 |
lemma zless2p: |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
47 |
"0 < (2 ^ n :: int)" |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
48 |
by arith |
24333 | 49 |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
50 |
lemma zle2p: |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
51 |
"0 \<le> (2 ^ n :: int)" |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
52 |
by arith |
24465 | 53 |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
54 |
lemma m1mod2k: |
54871 | 55 |
"- 1 mod 2 ^ n = (2 ^ n - 1 :: int)" |
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
56 |
using zless2p by (rule zmod_minus1) |
24333 | 57 |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
58 |
lemma p1mod22k': |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
59 |
fixes b :: int |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
60 |
shows "(1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)" |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
61 |
using zle2p by (rule pos_zmod_mult_2) |
24465 | 62 |
|
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
63 |
lemma p1mod22k: |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
64 |
fixes b :: int |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
65 |
shows "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1" |
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
66 |
by (simp add: p1mod22k' add_commute) |
24333 | 67 |
|
54871 | 68 |
lemma int_mod_lem: |
69 |
"(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)" |
|
24333 | 70 |
apply safe |
54871 | 71 |
apply (erule (1) mod_pos_pos_trivial) |
72 |
apply (erule_tac [!] subst) |
|
73 |
apply auto |
|
24333 | 74 |
done |
75 |
||
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51301
diff
changeset
|
76 |
end |
24333 | 77 |