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;
kleing@24333
     1
(* 
kleing@24333
     2
  Author:  Jeremy Dawson, NICTA
huffman@24350
     3
*) 
kleing@24333
     4
wenzelm@61799
     5
section \<open>Useful Numerical Lemmas\<close>
kleing@24333
     6
haftmann@37655
     7
theory Misc_Numeric
haftmann@58770
     8
imports Main
haftmann@25592
     9
begin
kleing@24333
    10
haftmann@54847
    11
lemma mod_2_neq_1_eq_eq_0:
haftmann@54847
    12
  fixes k :: int
haftmann@54847
    13
  shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
haftmann@54869
    14
  by (fact not_mod_2_eq_1_eq_0)
haftmann@54847
    15
haftmann@53062
    16
lemma z1pmod2:
haftmann@54871
    17
  fixes b :: int
haftmann@54871
    18
  shows "(2 * b + 1) mod 2 = (1::int)"
haftmann@54871
    19
  by arith
haftmann@54871
    20
haftmann@54871
    21
lemma diff_le_eq':
haftmann@54871
    22
  "a - b \<le> c \<longleftrightarrow> a \<le> b + (c::int)"
haftmann@54869
    23
  by arith
kleing@24333
    24
kleing@24333
    25
lemma emep1:
haftmann@54871
    26
  fixes n d :: int
haftmann@54871
    27
  shows "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
haftmann@58740
    28
  by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)
haftmann@54871
    29
haftmann@54871
    30
lemma int_mod_ge:
haftmann@54871
    31
  "a < n \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> a \<le> a mod n"
haftmann@54871
    32
  by (metis dual_order.trans le_cases mod_pos_pos_trivial pos_mod_conj)
kleing@24333
    33
haftmann@54871
    34
lemma int_mod_ge':
haftmann@54871
    35
  "b < 0 \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> b + n \<le> b mod n"
haftmann@54871
    36
  by (metis add_less_same_cancel2 int_mod_ge mod_add_self2)
kleing@24333
    37
haftmann@54871
    38
lemma int_mod_le':
haftmann@54871
    39
  "(0::int) \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
haftmann@54871
    40
  by (metis minus_mod_self2 zmod_le_nonneg_dividend)
kleing@24333
    41
haftmann@53062
    42
lemma zless2:
haftmann@53062
    43
  "0 < (2 :: int)"
haftmann@54869
    44
  by (fact zero_less_numeral)
huffman@24465
    45
haftmann@53062
    46
lemma zless2p:
haftmann@53062
    47
  "0 < (2 ^ n :: int)"
haftmann@53062
    48
  by arith
kleing@24333
    49
haftmann@53062
    50
lemma zle2p:
haftmann@53062
    51
  "0 \<le> (2 ^ n :: int)"
haftmann@53062
    52
  by arith
huffman@24465
    53
haftmann@53062
    54
lemma m1mod2k:
haftmann@54871
    55
  "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
haftmann@53062
    56
  using zless2p by (rule zmod_minus1)
kleing@24333
    57
haftmann@53062
    58
lemma p1mod22k':
haftmann@53062
    59
  fixes b :: int
haftmann@53062
    60
  shows "(1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)"
haftmann@53062
    61
  using zle2p by (rule pos_zmod_mult_2) 
huffman@24465
    62
haftmann@53062
    63
lemma p1mod22k:
haftmann@53062
    64
  fixes b :: int
haftmann@53062
    65
  shows "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1"
haftmann@57512
    66
  by (simp add: p1mod22k' add.commute)
kleing@24333
    67
haftmann@54871
    68
lemma int_mod_lem: 
haftmann@54871
    69
  "(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)"
kleing@24333
    70
  apply safe
haftmann@54871
    71
    apply (erule (1) mod_pos_pos_trivial)
haftmann@54871
    72
   apply (erule_tac [!] subst)
haftmann@54871
    73
   apply auto
kleing@24333
    74
  done
kleing@24333
    75
haftmann@53062
    76
end
kleing@24333
    77