src/HOL/Word/Misc_Numeric.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 61799 4cf66f21b764 child 64593 50c715579715 permissions -rw-r--r--
tuned proofs;
```     1 (*
```
```     2   Author:  Jeremy Dawson, NICTA
```
```     3 *)
```
```     4
```
```     5 section \<open>Useful Numerical Lemmas\<close>
```
```     6
```
```     7 theory Misc_Numeric
```
```     8 imports Main
```
```     9 begin
```
```    10
```
```    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)
```
```    15
```
```    16 lemma z1pmod2:
```
```    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)"
```
```    23   by arith
```
```    24
```
```    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"
```
```    28   by (auto simp add: pos_zmod_mult_2 add.commute dvd_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)
```
```    33
```
```    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)
```
```    37
```
```    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)
```
```    41
```
```    42 lemma zless2:
```
```    43   "0 < (2 :: int)"
```
```    44   by (fact zero_less_numeral)
```
```    45
```
```    46 lemma zless2p:
```
```    47   "0 < (2 ^ n :: int)"
```
```    48   by arith
```
```    49
```
```    50 lemma zle2p:
```
```    51   "0 \<le> (2 ^ n :: int)"
```
```    52   by arith
```
```    53
```
```    54 lemma m1mod2k:
```
```    55   "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
```
```    56   using zless2p by (rule zmod_minus1)
```
```    57
```
```    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)
```
```    62
```
```    63 lemma p1mod22k:
```
```    64   fixes b :: int
```
```    65   shows "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1"
```
```    66   by (simp add: p1mod22k' add.commute)
```
```    67
```
```    68 lemma int_mod_lem:
```
```    69   "(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)"
```
```    70   apply safe
```
```    71     apply (erule (1) mod_pos_pos_trivial)
```
```    72    apply (erule_tac [!] subst)
```
```    73    apply auto
```
```    74   done
```
```    75
```
```    76 end
```
```    77
```