author | haftmann |
Wed, 25 Dec 2013 17:39:06 +0100 | |
changeset 54863 | 82acc20ded73 |
parent 54847 | d6cf9a5b9be9 |
child 54869 | 0046711700c8 |
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 |
|
24465 | 11 |
declare iszero_0 [iff] |
12 |
||
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
|
13 |
lemma min_pm [simp]: "min a b + (a - b) = (a :: nat)" by arith |
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
|
14 |
|
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
|
15 |
lemmas min_pm1 [simp] = trans [OF add_commute min_pm] |
24333 | 16 |
|
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
|
17 |
lemma rev_min_pm [simp]: "min b a + (a - b) = (a::nat)" by arith |
24465 | 18 |
|
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
|
19 |
lemmas rev_min_pm1 [simp] = trans [OF add_commute rev_min_pm] |
24333 | 20 |
|
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
|
21 |
lemma min_minus [simp] : "min m (m - k) = (m - k :: nat)" by arith |
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
|
22 |
|
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54847
diff
changeset
|
23 |
lemmas min_minus' [simp] = trans [OF min.commute min_minus] |
24465 | 24 |
|
54847
d6cf9a5b9be9
prefer plain bool over dedicated type for binary digits
haftmann
parents:
54221
diff
changeset
|
25 |
lemma mod_2_neq_1_eq_eq_0: |
d6cf9a5b9be9
prefer plain bool over dedicated type for binary digits
haftmann
parents:
54221
diff
changeset
|
26 |
fixes k :: int |
d6cf9a5b9be9
prefer plain bool over dedicated type for binary digits
haftmann
parents:
54221
diff
changeset
|
27 |
shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0" |
d6cf9a5b9be9
prefer plain bool over dedicated type for binary digits
haftmann
parents:
54221
diff
changeset
|
28 |
by arith |
d6cf9a5b9be9
prefer plain bool over dedicated type for binary digits
haftmann
parents:
54221
diff
changeset
|
29 |
|
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
|
30 |
lemma z1pmod2: |
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
|
31 |
"(2 * b + 1) mod 2 = (1::int)" by arith |
24333 | 32 |
|
33 |
lemma emep1: |
|
34 |
"even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1" |
|
35 |
apply (simp add: add_commute) |
|
36 |
apply (safe dest!: even_equiv_def [THEN iffD1]) |
|
37 |
apply (subst pos_zmod_mult_2) |
|
38 |
apply arith |
|
30943
eb3dbbe971f6
zmod_zmult_zmult1 now subsumed by mod_mult_mult1
haftmann
parents:
30445
diff
changeset
|
39 |
apply (simp add: mod_mult_mult1) |
24333 | 40 |
done |
41 |
||
42 |
lemma int_mod_lem: |
|
43 |
"(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)" |
|
44 |
apply safe |
|
45 |
apply (erule (1) mod_pos_pos_trivial) |
|
46 |
apply (erule_tac [!] subst) |
|
47 |
apply auto |
|
48 |
done |
|
49 |
||
50 |
lemma int_mod_ge: "a < n ==> 0 < (n :: int) ==> a <= a mod n" |
|
51 |
apply (cases "0 <= a") |
|
52 |
apply (drule (1) mod_pos_pos_trivial) |
|
53 |
apply simp |
|
54 |
apply (rule order_trans [OF _ pos_mod_sign]) |
|
55 |
apply simp |
|
56 |
apply assumption |
|
57 |
done |
|
58 |
||
25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
24465
diff
changeset
|
59 |
lemma int_mod_ge': "b < 0 ==> 0 < (n :: int) ==> b + n <= b mod n" |
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
24465
diff
changeset
|
60 |
by (rule int_mod_ge [where a = "b + n" and n = n, simplified]) |
24333 | 61 |
|
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
|
62 |
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
|
63 |
"0 < (2 :: 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
|
64 |
by arith |
24465 | 65 |
|
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
|
66 |
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
|
67 |
"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
|
68 |
by arith |
24333 | 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 |
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
|
71 |
"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
|
72 |
by arith |
24465 | 73 |
|
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
|
74 |
lemma int_mod_le': "(0::int) <= b - n ==> b mod n <= b - 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
|
75 |
using zmod_le_nonneg_dividend [of "b - n" "n"] by simp |
24333 | 76 |
|
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
|
77 |
lemma diff_le_eq': "(a - b \<le> c) = (a \<le> b + (c::int))" by arith |
24333 | 78 |
|
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
|
79 |
lemma m1mod2k: |
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
|
80 |
"-1 mod 2 ^ n = (2 ^ n - 1 :: 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
|
81 |
using zless2p by (rule zmod_minus1) |
24333 | 82 |
|
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
|
83 |
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
|
84 |
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
|
85 |
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
|
86 |
using zle2p by (rule pos_zmod_mult_2) |
24465 | 87 |
|
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
|
88 |
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
|
89 |
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
|
90 |
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
|
91 |
by (simp add: p1mod22k' add_commute) |
24333 | 92 |
|
93 |
lemma lrlem': |
|
94 |
assumes d: "(i::nat) \<le> j \<or> m < j'" |
|
95 |
assumes R1: "i * k \<le> j * k \<Longrightarrow> R" |
|
96 |
assumes R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R" |
|
97 |
shows "R" using d |
|
98 |
apply safe |
|
99 |
apply (rule R1, erule mult_le_mono1) |
|
100 |
apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]]) |
|
101 |
done |
|
102 |
||
103 |
lemma lrlem: "(0::nat) < sc ==> |
|
104 |
(sc - n + (n + lb * n) <= m * n) = (sc + lb * n <= m * n)" |
|
105 |
apply safe |
|
106 |
apply arith |
|
107 |
apply (case_tac "sc >= n") |
|
108 |
apply arith |
|
109 |
apply (insert linorder_le_less_linear [of m lb]) |
|
110 |
apply (erule_tac k=n and k'=n in lrlem') |
|
111 |
apply arith |
|
112 |
apply simp |
|
113 |
done |
|
114 |
||
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
|
115 |
end |
24333 | 116 |