src/HOL/Word/Misc_Numeric.thy
author wenzelm
Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787 64b47495676d
parent 65363 5eb619751b14
child 67160 f37bf261bdf6
permissions -rw-r--r--
obsolete;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
     1
(*  Title:      HOL/Word/Misc_Numeric.thy
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
     2
    Author:     Jeremy Dawson, NICTA
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
     3
*)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     4
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 58874
diff changeset
     5
section \<open>Useful Numerical Lemmas\<close>
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     6
37655
f4d616d41a59 more speaking theory names
haftmann
parents: 37591
diff changeset
     7
theory Misc_Numeric
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
     8
  imports Main
25592
e8ddaf6bf5df explicit import of theory Main
haftmann
parents: 25349
diff changeset
     9
begin
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    10
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    11
lemma one_mod_exp_eq_one [simp]: "1 mod (2 * 2 ^ n) = (1::int)"
64593
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 61799
diff changeset
    12
  by (smt mod_pos_pos_trivial zero_less_power)
50c715579715 reoriented congruence rules in non-explosive direction
haftmann
parents: 61799
diff changeset
    13
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    14
lemma mod_2_neq_1_eq_eq_0: "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    15
  for k :: int
54869
0046711700c8 tuned proofs and declarations
haftmann
parents: 54863
diff changeset
    16
  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
    17
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    18
lemma z1pmod2: "(2 * b + 1) mod 2 = (1::int)"
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    19
  for b :: int
54871
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    20
  by arith
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    21
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    22
lemma diff_le_eq': "a - b \<le> c \<longleftrightarrow> a \<le> b + c"
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    23
  for a b c :: int
54869
0046711700c8 tuned proofs and declarations
haftmann
parents: 54863
diff changeset
    24
  by arith
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    25
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    26
lemma emep1: "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    27
  for n d :: int
58740
cb9d84d3e7f2 turn even into an abbreviation
haftmann
parents: 58681
diff changeset
    28
  by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)
54871
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    29
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    30
lemma int_mod_ge: "a < n \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a mod n"
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    31
  for a n :: int
54871
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
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    34
lemma int_mod_ge': "b < 0 \<Longrightarrow> 0 < n \<Longrightarrow> b + n \<le> b mod n"
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    35
  for b n :: int
54871
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
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    38
lemma int_mod_le': "0 \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    39
  for b n :: int
54871
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
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    42
lemma zless2: "0 < (2 :: int)"
54869
0046711700c8 tuned proofs and declarations
haftmann
parents: 54863
diff changeset
    43
  by (fact zero_less_numeral)
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24414
diff changeset
    44
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    45
lemma zless2p: "0 < (2 ^ n :: 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
    46
  by arith
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    47
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    48
lemma zle2p: "0 \<le> (2 ^ n :: 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
    49
  by arith
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24414
diff changeset
    50
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    51
lemma m1mod2k: "- 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
    52
  using zless2p by (rule zmod_minus1)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    53
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    54
lemma p1mod22k': "(1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)"
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    55
  for b :: int
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    56
  using zle2p by (rule pos_zmod_mult_2)
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24414
diff changeset
    57
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    58
lemma p1mod22k: "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1"
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    59
  for b :: int
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 54872
diff changeset
    60
  by (simp add: p1mod22k' add.commute)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    61
65363
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    62
lemma int_mod_lem: "0 < n \<Longrightarrow> 0 \<le> b \<and> b < n \<longleftrightarrow> b mod n = b"
5eb619751b14 misc tuning and modernization;
wenzelm
parents: 64593
diff changeset
    63
  for b n :: int
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    64
  apply safe
54871
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    65
    apply (erule (1) mod_pos_pos_trivial)
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    66
   apply (erule_tac [!] subst)
51612b889361 cleanup
haftmann
parents: 54869
diff changeset
    67
   apply auto
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    68
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    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
end