src/HOL/Word/Misc_Numeric.thy
author kuncar
Wed, 23 Apr 2014 17:57:56 +0200
changeset 56677 660ffb526069
parent 54872 af81b2357e08
child 57512 cc97b347b301
permissions -rw-r--r--
predicator simplification rules: support also partially specialized types e.g. 'a * nat
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     1
(* 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     2
  Author:  Jeremy Dawson, NICTA
24350
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
     3
*) 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     4
24350
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
     5
header {* Useful Numerical Lemmas *}
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     6
37655
f4d616d41a59 more speaking theory names
haftmann
parents: 37591
diff changeset
     7
theory Misc_Numeric
51301
6822aa82aafa simplified imports;
wenzelm
parents: 49962
diff changeset
     8
imports Main Parity
25592
e8ddaf6bf5df explicit import of theory Main
haftmann
parents: 25349
diff changeset
     9
begin
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    10
54847
d6cf9a5b9be9 prefer plain bool over dedicated type for binary digits
haftmann
parents: 54221
diff changeset
    11
lemma mod_2_neq_1_eq_eq_0:
d6cf9a5b9be9 prefer plain bool over dedicated type for binary digits
haftmann
parents: 54221
diff changeset
    12
  fixes k :: int
d6cf9a5b9be9 prefer plain bool over dedicated type for binary digits
haftmann
parents: 54221
diff changeset
    13
  shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
54869
0046711700c8 tuned proofs and declarations
haftmann
parents: 54863
diff changeset
    14
  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
    15
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
    16
lemma z1pmod2:
54871
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    17
  fixes b :: int
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    18
  shows "(2 * b + 1) mod 2 = (1::int)"
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    19
  by arith
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    20
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    21
lemma diff_le_eq':
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    22
  "a - b \<le> c \<longleftrightarrow> a \<le> b + (c::int)"
54869
0046711700c8 tuned proofs and declarations
haftmann
parents: 54863
diff changeset
    23
  by arith
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    24
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    25
lemma emep1:
54871
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    26
  fixes n d :: int
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    27
  shows "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    28
  by (auto simp add: pos_zmod_mult_2 add_commute even_equiv_def)
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    29
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    30
lemma int_mod_ge:
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    31
  "a < n \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> a \<le> a mod n"
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    32
  by (metis dual_order.trans le_cases mod_pos_pos_trivial pos_mod_conj)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    33
54871
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    34
lemma int_mod_ge':
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    35
  "b < 0 \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> b + n \<le> b mod n"
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    36
  by (metis add_less_same_cancel2 int_mod_ge mod_add_self2)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    37
54871
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    38
lemma int_mod_le':
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    39
  "(0::int) \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    40
  by (metis minus_mod_self2 zmod_le_nonneg_dividend)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    41
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
    42
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
    43
  "0 < (2 :: int)"
54869
0046711700c8 tuned proofs and declarations
haftmann
parents: 54863
diff changeset
    44
  by (fact zero_less_numeral)
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24414
diff changeset
    45
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
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
    47
  "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
    48
  by arith
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    49
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
    50
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
    51
  "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
    52
  by arith
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24414
diff changeset
    53
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
    54
lemma m1mod2k:
54871
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    55
  "- 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
    56
  using zless2p by (rule zmod_minus1)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    57
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
    58
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
    59
  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
    60
  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
    61
  using zle2p by (rule pos_zmod_mult_2) 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24414
diff changeset
    62
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
    63
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
    64
  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
    65
  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
    66
  by (simp add: p1mod22k' add_commute)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    67
54871
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    68
lemma int_mod_lem: 
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    69
  "(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    70
  apply safe
54871
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    71
    apply (erule (1) mod_pos_pos_trivial)
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    72
   apply (erule_tac [!] subst)
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    73
   apply auto
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    74
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    75
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
    76
end
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    77