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