src/HOL/Word/Bit_Comparison.thy
author haftmann
Fri Jun 19 07:53:35 2015 +0200 (2015-06-19)
changeset 60517 f16e4fb20652
parent 55210 d1e3b708d74b
child 61799 4cf66f21b764
permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
wenzelm@55210
     1
(*  Title:      HOL/Word/Bit_Comparison.thy
haftmann@54427
     2
    Author:     Stefan Berghofer
haftmann@54427
     3
    Copyright:  secunet Security Networks AG
haftmann@54427
     4
haftmann@54427
     5
Comparison on bit operations on integers.
haftmann@54427
     6
*)
haftmann@54427
     7
haftmann@54427
     8
theory Bit_Comparison
haftmann@54854
     9
imports Bits_Int
haftmann@54427
    10
begin
haftmann@54427
    11
haftmann@54427
    12
lemma AND_lower [simp]:
haftmann@54427
    13
  fixes x :: int and y :: int
haftmann@54427
    14
  assumes "0 \<le> x"
haftmann@54427
    15
  shows "0 \<le> x AND y"
haftmann@54427
    16
  using assms
haftmann@54427
    17
proof (induct x arbitrary: y rule: bin_induct)
haftmann@54427
    18
  case (3 bin bit)
haftmann@54427
    19
  show ?case
haftmann@54427
    20
  proof (cases y rule: bin_exhaust)
haftmann@54427
    21
    case (1 bin' bit')
haftmann@54427
    22
    from 3 have "0 \<le> bin"
haftmann@54847
    23
      by (cases bit) (simp_all add: Bit_def)
haftmann@54427
    24
    then have "0 \<le> bin AND bin'" by (rule 3)
haftmann@54427
    25
    with 1 show ?thesis
haftmann@54847
    26
      by simp (simp add: Bit_def)
haftmann@54427
    27
  qed
haftmann@54427
    28
next
haftmann@54427
    29
  case 2
haftmann@54427
    30
  then show ?case by (simp only: Min_def)
haftmann@54427
    31
qed simp
haftmann@54427
    32
haftmann@54427
    33
lemma OR_lower [simp]:
haftmann@54427
    34
  fixes x :: int and y :: int
haftmann@54427
    35
  assumes "0 \<le> x" "0 \<le> y"
haftmann@54427
    36
  shows "0 \<le> x OR y"
haftmann@54427
    37
  using assms
haftmann@54427
    38
proof (induct x arbitrary: y rule: bin_induct)
haftmann@54427
    39
  case (3 bin bit)
haftmann@54427
    40
  show ?case
haftmann@54427
    41
  proof (cases y rule: bin_exhaust)
haftmann@54427
    42
    case (1 bin' bit')
haftmann@54427
    43
    from 3 have "0 \<le> bin"
haftmann@54847
    44
      by (cases bit) (simp_all add: Bit_def)
haftmann@54427
    45
    moreover from 1 3 have "0 \<le> bin'"
haftmann@54847
    46
      by (cases bit') (simp_all add: Bit_def)
haftmann@54427
    47
    ultimately have "0 \<le> bin OR bin'" by (rule 3)
haftmann@54427
    48
    with 1 show ?thesis
haftmann@54847
    49
      by simp (simp add: Bit_def)
haftmann@54427
    50
  qed
haftmann@54427
    51
qed simp_all
haftmann@54427
    52
haftmann@54427
    53
lemma XOR_lower [simp]:
haftmann@54427
    54
  fixes x :: int and y :: int
haftmann@54427
    55
  assumes "0 \<le> x" "0 \<le> y"
haftmann@54427
    56
  shows "0 \<le> x XOR y"
haftmann@54427
    57
  using assms
haftmann@54427
    58
proof (induct x arbitrary: y rule: bin_induct)
haftmann@54427
    59
  case (3 bin bit)
haftmann@54427
    60
  show ?case
haftmann@54427
    61
  proof (cases y rule: bin_exhaust)
haftmann@54427
    62
    case (1 bin' bit')
haftmann@54427
    63
    from 3 have "0 \<le> bin"
haftmann@54847
    64
      by (cases bit) (simp_all add: Bit_def)
haftmann@54427
    65
    moreover from 1 3 have "0 \<le> bin'"
haftmann@54847
    66
      by (cases bit') (simp_all add: Bit_def)
haftmann@54427
    67
    ultimately have "0 \<le> bin XOR bin'" by (rule 3)
haftmann@54427
    68
    with 1 show ?thesis
haftmann@54847
    69
      by simp (simp add: Bit_def)
haftmann@54427
    70
  qed
haftmann@54427
    71
next
haftmann@54427
    72
  case 2
haftmann@54427
    73
  then show ?case by (simp only: Min_def)
haftmann@54427
    74
qed simp
haftmann@54427
    75
haftmann@54427
    76
lemma AND_upper1 [simp]:
haftmann@54427
    77
  fixes x :: int and y :: int
haftmann@54427
    78
  assumes "0 \<le> x"
haftmann@54427
    79
  shows "x AND y \<le> x"
haftmann@54427
    80
  using assms
haftmann@54427
    81
proof (induct x arbitrary: y rule: bin_induct)
haftmann@54427
    82
  case (3 bin bit)
haftmann@54427
    83
  show ?case
haftmann@54427
    84
  proof (cases y rule: bin_exhaust)
haftmann@54427
    85
    case (1 bin' bit')
haftmann@54427
    86
    from 3 have "0 \<le> bin"
haftmann@54847
    87
      by (cases bit) (simp_all add: Bit_def)
haftmann@54427
    88
    then have "bin AND bin' \<le> bin" by (rule 3)
haftmann@54427
    89
    with 1 show ?thesis
haftmann@54847
    90
      by simp (simp add: Bit_def)
haftmann@54427
    91
  qed
haftmann@54427
    92
next
haftmann@54427
    93
  case 2
haftmann@54427
    94
  then show ?case by (simp only: Min_def)
haftmann@54427
    95
qed simp
haftmann@54427
    96
haftmann@54427
    97
lemmas AND_upper1' [simp] = order_trans [OF AND_upper1]
haftmann@54427
    98
lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1]
haftmann@54427
    99
haftmann@54427
   100
lemma AND_upper2 [simp]:
haftmann@54427
   101
  fixes x :: int and y :: int
haftmann@54427
   102
  assumes "0 \<le> y"
haftmann@54427
   103
  shows "x AND y \<le> y"
haftmann@54427
   104
  using assms
haftmann@54427
   105
proof (induct y arbitrary: x rule: bin_induct)
haftmann@54427
   106
  case (3 bin bit)
haftmann@54427
   107
  show ?case
haftmann@54427
   108
  proof (cases x rule: bin_exhaust)
haftmann@54427
   109
    case (1 bin' bit')
haftmann@54427
   110
    from 3 have "0 \<le> bin"
haftmann@54847
   111
      by (cases bit) (simp_all add: Bit_def)
haftmann@54427
   112
    then have "bin' AND bin \<le> bin" by (rule 3)
haftmann@54427
   113
    with 1 show ?thesis
haftmann@54847
   114
      by simp (simp add: Bit_def)
haftmann@54427
   115
  qed
haftmann@54427
   116
next
haftmann@54427
   117
  case 2
haftmann@54427
   118
  then show ?case by (simp only: Min_def)
haftmann@54427
   119
qed simp
haftmann@54427
   120
haftmann@54427
   121
lemmas AND_upper2' [simp] = order_trans [OF AND_upper2]
haftmann@54427
   122
lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2]
haftmann@54427
   123
haftmann@54427
   124
lemma OR_upper:
haftmann@54427
   125
  fixes x :: int and y :: int
haftmann@54427
   126
  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
haftmann@54427
   127
  shows "x OR y < 2 ^ n"
haftmann@54427
   128
  using assms
haftmann@54427
   129
proof (induct x arbitrary: y n rule: bin_induct)
haftmann@54427
   130
  case (3 bin bit)
haftmann@54427
   131
  show ?case
haftmann@54427
   132
  proof (cases y rule: bin_exhaust)
haftmann@54427
   133
    case (1 bin' bit')
haftmann@54427
   134
    show ?thesis
haftmann@54427
   135
    proof (cases n)
haftmann@54427
   136
      case 0
haftmann@54427
   137
      with 3 have "bin BIT bit = 0" by simp
haftmann@54847
   138
      then have "bin = 0" and "\<not> bit"
haftmann@54847
   139
        by (auto simp add: Bit_def split: if_splits) arith
haftmann@54427
   140
      then show ?thesis using 0 1 `y < 2 ^ n`
haftmann@54427
   141
        by simp
haftmann@54427
   142
    next
haftmann@54427
   143
      case (Suc m)
haftmann@54427
   144
      from 3 have "0 \<le> bin"
haftmann@54847
   145
        by (cases bit) (simp_all add: Bit_def)
haftmann@54427
   146
      moreover from 3 Suc have "bin < 2 ^ m"
haftmann@54847
   147
        by (cases bit) (simp_all add: Bit_def)
haftmann@54427
   148
      moreover from 1 3 Suc have "bin' < 2 ^ m"
haftmann@54847
   149
        by (cases bit') (simp_all add: Bit_def)
haftmann@54427
   150
      ultimately have "bin OR bin' < 2 ^ m" by (rule 3)
haftmann@54427
   151
      with 1 Suc show ?thesis
haftmann@54847
   152
        by simp (simp add: Bit_def)
haftmann@54427
   153
    qed
haftmann@54427
   154
  qed
haftmann@54427
   155
qed simp_all
haftmann@54427
   156
haftmann@54427
   157
lemma XOR_upper:
haftmann@54427
   158
  fixes x :: int and y :: int
haftmann@54427
   159
  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
haftmann@54427
   160
  shows "x XOR y < 2 ^ n"
haftmann@54427
   161
  using assms
haftmann@54427
   162
proof (induct x arbitrary: y n rule: bin_induct)
haftmann@54427
   163
  case (3 bin bit)
haftmann@54427
   164
  show ?case
haftmann@54427
   165
  proof (cases y rule: bin_exhaust)
haftmann@54427
   166
    case (1 bin' bit')
haftmann@54427
   167
    show ?thesis
haftmann@54427
   168
    proof (cases n)
haftmann@54427
   169
      case 0
haftmann@54427
   170
      with 3 have "bin BIT bit = 0" by simp
haftmann@54847
   171
      then have "bin = 0" and "\<not> bit"
haftmann@54847
   172
        by (auto simp add: Bit_def split: if_splits) arith
haftmann@54427
   173
      then show ?thesis using 0 1 `y < 2 ^ n`
haftmann@54427
   174
        by simp
haftmann@54427
   175
    next
haftmann@54427
   176
      case (Suc m)
haftmann@54427
   177
      from 3 have "0 \<le> bin"
haftmann@54847
   178
        by (cases bit) (simp_all add: Bit_def)
haftmann@54427
   179
      moreover from 3 Suc have "bin < 2 ^ m"
haftmann@54847
   180
        by (cases bit) (simp_all add: Bit_def)
haftmann@54427
   181
      moreover from 1 3 Suc have "bin' < 2 ^ m"
haftmann@54847
   182
        by (cases bit') (simp_all add: Bit_def)
haftmann@54427
   183
      ultimately have "bin XOR bin' < 2 ^ m" by (rule 3)
haftmann@54427
   184
      with 1 Suc show ?thesis
haftmann@54847
   185
        by simp (simp add: Bit_def)
haftmann@54427
   186
    qed
haftmann@54427
   187
  qed
haftmann@54427
   188
next
haftmann@54427
   189
  case 2
haftmann@54427
   190
  then show ?case by (simp only: Min_def)
haftmann@54427
   191
qed simp
haftmann@54427
   192
haftmann@54427
   193
end