author | wenzelm |
Wed, 04 Oct 2017 12:00:53 +0200 | |
changeset 66787 | 64b47495676d |
parent 65363 | 5eb619751b14 |
child 67160 | f37bf261bdf6 |
permissions | -rw-r--r-- |
65363 | 1 |
(* Title: HOL/Word/Misc_Numeric.thy |
2 |
Author: Jeremy Dawson, NICTA |
|
3 |
*) |
|
24333 | 4 |
|
61799 | 5 |
section \<open>Useful Numerical Lemmas\<close> |
24333 | 6 |
|
37655 | 7 |
theory Misc_Numeric |
65363 | 8 |
imports Main |
25592 | 9 |
begin |
24333 | 10 |
|
65363 | 11 |
lemma one_mod_exp_eq_one [simp]: "1 mod (2 * 2 ^ n) = (1::int)" |
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
61799
diff
changeset
|
12 |
by (smt mod_pos_pos_trivial zero_less_power) |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
61799
diff
changeset
|
13 |
|
65363 | 14 |
lemma mod_2_neq_1_eq_eq_0: "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0" |
15 |
for k :: int |
|
54869 | 16 |
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
|
17 |
|
65363 | 18 |
lemma z1pmod2: "(2 * b + 1) mod 2 = (1::int)" |
19 |
for b :: int |
|
54871 | 20 |
by arith |
21 |
||
65363 | 22 |
lemma diff_le_eq': "a - b \<le> c \<longleftrightarrow> a \<le> b + c" |
23 |
for a b c :: int |
|
54869 | 24 |
by arith |
24333 | 25 |
|
65363 | 26 |
lemma emep1: "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1" |
27 |
for n d :: int |
|
58740 | 28 |
by (auto simp add: pos_zmod_mult_2 add.commute dvd_def) |
54871 | 29 |
|
65363 | 30 |
lemma int_mod_ge: "a < n \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a mod n" |
31 |
for a n :: int |
|
54871 | 32 |
by (metis dual_order.trans le_cases mod_pos_pos_trivial pos_mod_conj) |
24333 | 33 |
|
65363 | 34 |
lemma int_mod_ge': "b < 0 \<Longrightarrow> 0 < n \<Longrightarrow> b + n \<le> b mod n" |
35 |
for b n :: int |
|
54871 | 36 |
by (metis add_less_same_cancel2 int_mod_ge mod_add_self2) |
24333 | 37 |
|
65363 | 38 |
lemma int_mod_le': "0 \<le> b - n \<Longrightarrow> b mod n \<le> b - n" |
39 |
for b n :: int |
|
54871 | 40 |
by (metis minus_mod_self2 zmod_le_nonneg_dividend) |
24333 | 41 |
|
65363 | 42 |
lemma zless2: "0 < (2 :: int)" |
54869 | 43 |
by (fact zero_less_numeral) |
24465 | 44 |
|
65363 | 45 |
lemma zless2p: "0 < (2 ^ n :: 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
|
46 |
by arith |
24333 | 47 |
|
65363 | 48 |
lemma zle2p: "0 \<le> (2 ^ n :: 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
|
49 |
by arith |
24465 | 50 |
|
65363 | 51 |
lemma m1mod2k: "- 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
|
52 |
using zless2p by (rule zmod_minus1) |
24333 | 53 |
|
65363 | 54 |
lemma p1mod22k': "(1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)" |
55 |
for b :: int |
|
56 |
using zle2p by (rule pos_zmod_mult_2) |
|
24465 | 57 |
|
65363 | 58 |
lemma p1mod22k: "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1" |
59 |
for b :: int |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
54872
diff
changeset
|
60 |
by (simp add: p1mod22k' add.commute) |
24333 | 61 |
|
65363 | 62 |
lemma int_mod_lem: "0 < n \<Longrightarrow> 0 \<le> b \<and> b < n \<longleftrightarrow> b mod n = b" |
63 |
for b n :: int |
|
24333 | 64 |
apply safe |
54871 | 65 |
apply (erule (1) mod_pos_pos_trivial) |
66 |
apply (erule_tac [!] subst) |
|
67 |
apply auto |
|
24333 | 68 |
done |
69 |
||
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
|
70 |
end |