separated comparision on bit operations into separate theory
authorhaftmann
Wed Nov 13 19:12:15 2013 +0100 (2013-11-13)
changeset 54427783861a66a60
parent 54426 edb87aac9cca
child 54428 6ccc6130140c
separated comparision on bit operations into separate theory
src/HOL/SPARK/SPARK.thy
src/HOL/SPARK/SPARK_Setup.thy
src/HOL/Word/Bit_Comparison.thy
src/HOL/Word/Bit_Int.thy
     1.1 --- a/src/HOL/SPARK/SPARK.thy	Wed Nov 13 15:36:32 2013 +0100
     1.2 +++ b/src/HOL/SPARK/SPARK.thy	Wed Nov 13 19:12:15 2013 +0100
     1.3 @@ -16,151 +16,6 @@
     1.4    bit__or (integer, integer) : integer = "op OR"
     1.5    bit__xor (integer, integer) : integer = "op XOR"
     1.6  
     1.7 -lemma AND_lower [simp]:
     1.8 -  fixes x :: int and y :: int
     1.9 -  assumes "0 \<le> x"
    1.10 -  shows "0 \<le> x AND y"
    1.11 -  using assms
    1.12 -proof (induct x arbitrary: y rule: bin_induct)
    1.13 -  case (3 bin bit)
    1.14 -  show ?case
    1.15 -  proof (cases y rule: bin_exhaust)
    1.16 -    case (1 bin' bit')
    1.17 -    from 3 have "0 \<le> bin"
    1.18 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.19 -    then have "0 \<le> bin AND bin'" by (rule 3)
    1.20 -    with 1 show ?thesis
    1.21 -      by simp (simp add: Bit_def bitval_def split add: bit.split)
    1.22 -  qed
    1.23 -next
    1.24 -  case 2
    1.25 -  then show ?case by (simp only: Min_def)
    1.26 -qed simp
    1.27 -
    1.28 -lemma OR_lower [simp]:
    1.29 -  fixes x :: int and y :: int
    1.30 -  assumes "0 \<le> x" "0 \<le> y"
    1.31 -  shows "0 \<le> x OR y"
    1.32 -  using assms
    1.33 -proof (induct x arbitrary: y rule: bin_induct)
    1.34 -  case (3 bin bit)
    1.35 -  show ?case
    1.36 -  proof (cases y rule: bin_exhaust)
    1.37 -    case (1 bin' bit')
    1.38 -    from 3 have "0 \<le> bin"
    1.39 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.40 -    moreover from 1 3 have "0 \<le> bin'"
    1.41 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.42 -    ultimately have "0 \<le> bin OR bin'" by (rule 3)
    1.43 -    with 1 show ?thesis
    1.44 -      by simp (simp add: Bit_def bitval_def split add: bit.split)
    1.45 -  qed
    1.46 -qed simp_all
    1.47 -
    1.48 -lemma XOR_lower [simp]:
    1.49 -  fixes x :: int and y :: int
    1.50 -  assumes "0 \<le> x" "0 \<le> y"
    1.51 -  shows "0 \<le> x XOR y"
    1.52 -  using assms
    1.53 -proof (induct x arbitrary: y rule: bin_induct)
    1.54 -  case (3 bin bit)
    1.55 -  show ?case
    1.56 -  proof (cases y rule: bin_exhaust)
    1.57 -    case (1 bin' bit')
    1.58 -    from 3 have "0 \<le> bin"
    1.59 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.60 -    moreover from 1 3 have "0 \<le> bin'"
    1.61 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.62 -    ultimately have "0 \<le> bin XOR bin'" by (rule 3)
    1.63 -    with 1 show ?thesis
    1.64 -      by simp (simp add: Bit_def bitval_def split add: bit.split)
    1.65 -  qed
    1.66 -next
    1.67 -  case 2
    1.68 -  then show ?case by (simp only: Min_def)
    1.69 -qed simp
    1.70 -
    1.71 -lemma AND_upper1 [simp]:
    1.72 -  fixes x :: int and y :: int
    1.73 -  assumes "0 \<le> x"
    1.74 -  shows "x AND y \<le> x"
    1.75 -  using assms
    1.76 -proof (induct x arbitrary: y rule: bin_induct)
    1.77 -  case (3 bin bit)
    1.78 -  show ?case
    1.79 -  proof (cases y rule: bin_exhaust)
    1.80 -    case (1 bin' bit')
    1.81 -    from 3 have "0 \<le> bin"
    1.82 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.83 -    then have "bin AND bin' \<le> bin" by (rule 3)
    1.84 -    with 1 show ?thesis
    1.85 -      by simp (simp add: Bit_def bitval_def split add: bit.split)
    1.86 -  qed
    1.87 -next
    1.88 -  case 2
    1.89 -  then show ?case by (simp only: Min_def)
    1.90 -qed simp
    1.91 -
    1.92 -lemmas AND_upper1' [simp] = order_trans [OF AND_upper1]
    1.93 -lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1]
    1.94 -
    1.95 -lemma AND_upper2 [simp]:
    1.96 -  fixes x :: int and y :: int
    1.97 -  assumes "0 \<le> y"
    1.98 -  shows "x AND y \<le> y"
    1.99 -  using assms
   1.100 -proof (induct y arbitrary: x rule: bin_induct)
   1.101 -  case (3 bin bit)
   1.102 -  show ?case
   1.103 -  proof (cases x rule: bin_exhaust)
   1.104 -    case (1 bin' bit')
   1.105 -    from 3 have "0 \<le> bin"
   1.106 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.107 -    then have "bin' AND bin \<le> bin" by (rule 3)
   1.108 -    with 1 show ?thesis
   1.109 -      by simp (simp add: Bit_def bitval_def split add: bit.split)
   1.110 -  qed
   1.111 -next
   1.112 -  case 2
   1.113 -  then show ?case by (simp only: Min_def)
   1.114 -qed simp
   1.115 -
   1.116 -lemmas AND_upper2' [simp] = order_trans [OF AND_upper2]
   1.117 -lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2]
   1.118 -
   1.119 -lemma OR_upper:
   1.120 -  fixes x :: int and y :: int
   1.121 -  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
   1.122 -  shows "x OR y < 2 ^ n"
   1.123 -  using assms
   1.124 -proof (induct x arbitrary: y n rule: bin_induct)
   1.125 -  case (3 bin bit)
   1.126 -  show ?case
   1.127 -  proof (cases y rule: bin_exhaust)
   1.128 -    case (1 bin' bit')
   1.129 -    show ?thesis
   1.130 -    proof (cases n)
   1.131 -      case 0
   1.132 -      with 3 have "bin BIT bit = 0" by simp
   1.133 -      then have "bin = 0" "bit = 0"
   1.134 -        by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
   1.135 -      then show ?thesis using 0 1 `y < 2 ^ n`
   1.136 -        by simp
   1.137 -    next
   1.138 -      case (Suc m)
   1.139 -      from 3 have "0 \<le> bin"
   1.140 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.141 -      moreover from 3 Suc have "bin < 2 ^ m"
   1.142 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.143 -      moreover from 1 3 Suc have "bin' < 2 ^ m"
   1.144 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.145 -      ultimately have "bin OR bin' < 2 ^ m" by (rule 3)
   1.146 -      with 1 Suc show ?thesis
   1.147 -        by simp (simp add: Bit_def bitval_def split add: bit.split)
   1.148 -    qed
   1.149 -  qed
   1.150 -qed simp_all
   1.151 -
   1.152  lemmas [simp] =
   1.153    OR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified]
   1.154    OR_upper [of _ 8, simplified]
   1.155 @@ -171,42 +26,6 @@
   1.156    OR_upper [of _ 64, simplified zle_diff1_eq [symmetric], simplified]
   1.157    OR_upper [of _ 64, simplified]
   1.158  
   1.159 -lemma XOR_upper:
   1.160 -  fixes x :: int and y :: int
   1.161 -  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
   1.162 -  shows "x XOR y < 2 ^ n"
   1.163 -  using assms
   1.164 -proof (induct x arbitrary: y n rule: bin_induct)
   1.165 -  case (3 bin bit)
   1.166 -  show ?case
   1.167 -  proof (cases y rule: bin_exhaust)
   1.168 -    case (1 bin' bit')
   1.169 -    show ?thesis
   1.170 -    proof (cases n)
   1.171 -      case 0
   1.172 -      with 3 have "bin BIT bit = 0" by simp
   1.173 -      then have "bin = 0" "bit = 0"
   1.174 -        by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
   1.175 -      then show ?thesis using 0 1 `y < 2 ^ n`
   1.176 -        by simp
   1.177 -    next
   1.178 -      case (Suc m)
   1.179 -      from 3 have "0 \<le> bin"
   1.180 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.181 -      moreover from 3 Suc have "bin < 2 ^ m"
   1.182 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.183 -      moreover from 1 3 Suc have "bin' < 2 ^ m"
   1.184 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.185 -      ultimately have "bin XOR bin' < 2 ^ m" by (rule 3)
   1.186 -      with 1 Suc show ?thesis
   1.187 -        by simp (simp add: Bit_def bitval_def split add: bit.split)
   1.188 -    qed
   1.189 -  qed
   1.190 -next
   1.191 -  case 2
   1.192 -  then show ?case by (simp only: Min_def)
   1.193 -qed simp
   1.194 -
   1.195  lemmas [simp] =
   1.196    XOR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified]
   1.197    XOR_upper [of _ 8, simplified]
   1.198 @@ -234,47 +53,6 @@
   1.199    bit_not_spark_eq [where 'a=32, simplified]
   1.200    bit_not_spark_eq [where 'a=64, simplified]
   1.201  
   1.202 -lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT 1"
   1.203 -  unfolding Bit_B1
   1.204 -  by (induct n) simp_all
   1.205 -
   1.206 -lemma mod_BIT:
   1.207 -  "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
   1.208 -proof -
   1.209 -  have "bin mod 2 ^ n < 2 ^ n" by simp
   1.210 -  then have "bin mod 2 ^ n \<le> 2 ^ n - 1" by simp
   1.211 -  then have "2 * (bin mod 2 ^ n) \<le> 2 * (2 ^ n - 1)"
   1.212 -    by (rule mult_left_mono) simp
   1.213 -  then have "2 * (bin mod 2 ^ n) + 1 < 2 * 2 ^ n" by simp
   1.214 -  then show ?thesis
   1.215 -    by (auto simp add: Bit_def bitval_def mod_mult_mult1 mod_add_left_eq [of "2 * bin"]
   1.216 -      mod_pos_pos_trivial split add: bit.split)
   1.217 -qed
   1.218 -
   1.219 -lemma AND_mod:
   1.220 -  fixes x :: int
   1.221 -  shows "x AND 2 ^ n - 1 = x mod 2 ^ n"
   1.222 -proof (induct x arbitrary: n rule: bin_induct)
   1.223 -  case 1
   1.224 -  then show ?case
   1.225 -    by simp
   1.226 -next
   1.227 -  case 2
   1.228 -  then show ?case
   1.229 -    by (simp, simp add: m1mod2k)
   1.230 -next
   1.231 -  case (3 bin bit)
   1.232 -  show ?case
   1.233 -  proof (cases n)
   1.234 -    case 0
   1.235 -    then show ?thesis by (simp add: int_and_extra_simps)
   1.236 -  next
   1.237 -    case (Suc m)
   1.238 -    with 3 show ?thesis
   1.239 -      by (simp only: power_BIT mod_BIT int_and_Bits) simp
   1.240 -  qed
   1.241 -qed
   1.242 -
   1.243  
   1.244  text {* Minimum and maximum *}
   1.245  
   1.246 @@ -283,3 +61,4 @@
   1.247    integer__max = "max :: int \<Rightarrow> int \<Rightarrow> int"
   1.248  
   1.249  end
   1.250 +
     2.1 --- a/src/HOL/SPARK/SPARK_Setup.thy	Wed Nov 13 15:36:32 2013 +0100
     2.2 +++ b/src/HOL/SPARK/SPARK_Setup.thy	Wed Nov 13 19:12:15 2013 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  *)
     2.5  
     2.6  theory SPARK_Setup
     2.7 -imports Word
     2.8 +imports "~~/src/HOL/Word/Word" "~~/src/HOL/Word/Bit_Comparison"
     2.9  keywords
    2.10    "spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and
    2.11    "spark_open_siv" :: thy_load ("siv", "fdl", "rls") and
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Word/Bit_Comparison.thy	Wed Nov 13 19:12:15 2013 +0100
     3.3 @@ -0,0 +1,193 @@
     3.4 +(*  Title:      HOL/SPARK/SPARK.thy
     3.5 +    Author:     Stefan Berghofer
     3.6 +    Copyright:  secunet Security Networks AG
     3.7 +
     3.8 +Comparison on bit operations on integers.
     3.9 +*)
    3.10 +
    3.11 +theory Bit_Comparison
    3.12 +imports Type_Length Bit_Operations Bit_Int
    3.13 +begin
    3.14 +
    3.15 +lemma AND_lower [simp]:
    3.16 +  fixes x :: int and y :: int
    3.17 +  assumes "0 \<le> x"
    3.18 +  shows "0 \<le> x AND y"
    3.19 +  using assms
    3.20 +proof (induct x arbitrary: y rule: bin_induct)
    3.21 +  case (3 bin bit)
    3.22 +  show ?case
    3.23 +  proof (cases y rule: bin_exhaust)
    3.24 +    case (1 bin' bit')
    3.25 +    from 3 have "0 \<le> bin"
    3.26 +      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    3.27 +    then have "0 \<le> bin AND bin'" by (rule 3)
    3.28 +    with 1 show ?thesis
    3.29 +      by simp (simp add: Bit_def bitval_def split add: bit.split)
    3.30 +  qed
    3.31 +next
    3.32 +  case 2
    3.33 +  then show ?case by (simp only: Min_def)
    3.34 +qed simp
    3.35 +
    3.36 +lemma OR_lower [simp]:
    3.37 +  fixes x :: int and y :: int
    3.38 +  assumes "0 \<le> x" "0 \<le> y"
    3.39 +  shows "0 \<le> x OR y"
    3.40 +  using assms
    3.41 +proof (induct x arbitrary: y rule: bin_induct)
    3.42 +  case (3 bin bit)
    3.43 +  show ?case
    3.44 +  proof (cases y rule: bin_exhaust)
    3.45 +    case (1 bin' bit')
    3.46 +    from 3 have "0 \<le> bin"
    3.47 +      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    3.48 +    moreover from 1 3 have "0 \<le> bin'"
    3.49 +      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    3.50 +    ultimately have "0 \<le> bin OR bin'" by (rule 3)
    3.51 +    with 1 show ?thesis
    3.52 +      by simp (simp add: Bit_def bitval_def split add: bit.split)
    3.53 +  qed
    3.54 +qed simp_all
    3.55 +
    3.56 +lemma XOR_lower [simp]:
    3.57 +  fixes x :: int and y :: int
    3.58 +  assumes "0 \<le> x" "0 \<le> y"
    3.59 +  shows "0 \<le> x XOR y"
    3.60 +  using assms
    3.61 +proof (induct x arbitrary: y rule: bin_induct)
    3.62 +  case (3 bin bit)
    3.63 +  show ?case
    3.64 +  proof (cases y rule: bin_exhaust)
    3.65 +    case (1 bin' bit')
    3.66 +    from 3 have "0 \<le> bin"
    3.67 +      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    3.68 +    moreover from 1 3 have "0 \<le> bin'"
    3.69 +      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    3.70 +    ultimately have "0 \<le> bin XOR bin'" by (rule 3)
    3.71 +    with 1 show ?thesis
    3.72 +      by simp (simp add: Bit_def bitval_def split add: bit.split)
    3.73 +  qed
    3.74 +next
    3.75 +  case 2
    3.76 +  then show ?case by (simp only: Min_def)
    3.77 +qed simp
    3.78 +
    3.79 +lemma AND_upper1 [simp]:
    3.80 +  fixes x :: int and y :: int
    3.81 +  assumes "0 \<le> x"
    3.82 +  shows "x AND y \<le> x"
    3.83 +  using assms
    3.84 +proof (induct x arbitrary: y rule: bin_induct)
    3.85 +  case (3 bin bit)
    3.86 +  show ?case
    3.87 +  proof (cases y rule: bin_exhaust)
    3.88 +    case (1 bin' bit')
    3.89 +    from 3 have "0 \<le> bin"
    3.90 +      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    3.91 +    then have "bin AND bin' \<le> bin" by (rule 3)
    3.92 +    with 1 show ?thesis
    3.93 +      by simp (simp add: Bit_def bitval_def split add: bit.split)
    3.94 +  qed
    3.95 +next
    3.96 +  case 2
    3.97 +  then show ?case by (simp only: Min_def)
    3.98 +qed simp
    3.99 +
   3.100 +lemmas AND_upper1' [simp] = order_trans [OF AND_upper1]
   3.101 +lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1]
   3.102 +
   3.103 +lemma AND_upper2 [simp]:
   3.104 +  fixes x :: int and y :: int
   3.105 +  assumes "0 \<le> y"
   3.106 +  shows "x AND y \<le> y"
   3.107 +  using assms
   3.108 +proof (induct y arbitrary: x rule: bin_induct)
   3.109 +  case (3 bin bit)
   3.110 +  show ?case
   3.111 +  proof (cases x rule: bin_exhaust)
   3.112 +    case (1 bin' bit')
   3.113 +    from 3 have "0 \<le> bin"
   3.114 +      by (simp add: Bit_def bitval_def split add: bit.split_asm)
   3.115 +    then have "bin' AND bin \<le> bin" by (rule 3)
   3.116 +    with 1 show ?thesis
   3.117 +      by simp (simp add: Bit_def bitval_def split add: bit.split)
   3.118 +  qed
   3.119 +next
   3.120 +  case 2
   3.121 +  then show ?case by (simp only: Min_def)
   3.122 +qed simp
   3.123 +
   3.124 +lemmas AND_upper2' [simp] = order_trans [OF AND_upper2]
   3.125 +lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2]
   3.126 +
   3.127 +lemma OR_upper:
   3.128 +  fixes x :: int and y :: int
   3.129 +  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
   3.130 +  shows "x OR y < 2 ^ n"
   3.131 +  using assms
   3.132 +proof (induct x arbitrary: y n rule: bin_induct)
   3.133 +  case (3 bin bit)
   3.134 +  show ?case
   3.135 +  proof (cases y rule: bin_exhaust)
   3.136 +    case (1 bin' bit')
   3.137 +    show ?thesis
   3.138 +    proof (cases n)
   3.139 +      case 0
   3.140 +      with 3 have "bin BIT bit = 0" by simp
   3.141 +      then have "bin = 0" "bit = 0"
   3.142 +        by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
   3.143 +      then show ?thesis using 0 1 `y < 2 ^ n`
   3.144 +        by simp
   3.145 +    next
   3.146 +      case (Suc m)
   3.147 +      from 3 have "0 \<le> bin"
   3.148 +        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   3.149 +      moreover from 3 Suc have "bin < 2 ^ m"
   3.150 +        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   3.151 +      moreover from 1 3 Suc have "bin' < 2 ^ m"
   3.152 +        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   3.153 +      ultimately have "bin OR bin' < 2 ^ m" by (rule 3)
   3.154 +      with 1 Suc show ?thesis
   3.155 +        by simp (simp add: Bit_def bitval_def split add: bit.split)
   3.156 +    qed
   3.157 +  qed
   3.158 +qed simp_all
   3.159 +
   3.160 +lemma XOR_upper:
   3.161 +  fixes x :: int and y :: int
   3.162 +  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
   3.163 +  shows "x XOR y < 2 ^ n"
   3.164 +  using assms
   3.165 +proof (induct x arbitrary: y n rule: bin_induct)
   3.166 +  case (3 bin bit)
   3.167 +  show ?case
   3.168 +  proof (cases y rule: bin_exhaust)
   3.169 +    case (1 bin' bit')
   3.170 +    show ?thesis
   3.171 +    proof (cases n)
   3.172 +      case 0
   3.173 +      with 3 have "bin BIT bit = 0" by simp
   3.174 +      then have "bin = 0" "bit = 0"
   3.175 +        by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
   3.176 +      then show ?thesis using 0 1 `y < 2 ^ n`
   3.177 +        by simp
   3.178 +    next
   3.179 +      case (Suc m)
   3.180 +      from 3 have "0 \<le> bin"
   3.181 +        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   3.182 +      moreover from 3 Suc have "bin < 2 ^ m"
   3.183 +        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   3.184 +      moreover from 1 3 Suc have "bin' < 2 ^ m"
   3.185 +        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   3.186 +      ultimately have "bin XOR bin' < 2 ^ m" by (rule 3)
   3.187 +      with 1 Suc show ?thesis
   3.188 +        by simp (simp add: Bit_def bitval_def split add: bit.split)
   3.189 +    qed
   3.190 +  qed
   3.191 +next
   3.192 +  case 2
   3.193 +  then show ?case by (simp only: Min_def)
   3.194 +qed simp
   3.195 +
   3.196 +end
     4.1 --- a/src/HOL/Word/Bit_Int.thy	Wed Nov 13 15:36:32 2013 +0100
     4.2 +++ b/src/HOL/Word/Bit_Int.thy	Wed Nov 13 19:12:15 2013 +0100
     4.3 @@ -632,5 +632,46 @@
     4.4    "(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))"
     4.5    by auto
     4.6  
     4.7 +lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT 1"
     4.8 +  unfolding Bit_B1
     4.9 +  by (induct n) simp_all
    4.10 +
    4.11 +lemma mod_BIT:
    4.12 +  "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
    4.13 +proof -
    4.14 +  have "bin mod 2 ^ n < 2 ^ n" by simp
    4.15 +  then have "bin mod 2 ^ n \<le> 2 ^ n - 1" by simp
    4.16 +  then have "2 * (bin mod 2 ^ n) \<le> 2 * (2 ^ n - 1)"
    4.17 +    by (rule mult_left_mono) simp
    4.18 +  then have "2 * (bin mod 2 ^ n) + 1 < 2 * 2 ^ n" by simp
    4.19 +  then show ?thesis
    4.20 +    by (auto simp add: Bit_def bitval_def mod_mult_mult1 mod_add_left_eq [of "2 * bin"]
    4.21 +      mod_pos_pos_trivial split add: bit.split)
    4.22 +qed
    4.23 +
    4.24 +lemma AND_mod:
    4.25 +  fixes x :: int
    4.26 +  shows "x AND 2 ^ n - 1 = x mod 2 ^ n"
    4.27 +proof (induct x arbitrary: n rule: bin_induct)
    4.28 +  case 1
    4.29 +  then show ?case
    4.30 +    by simp
    4.31 +next
    4.32 +  case 2
    4.33 +  then show ?case
    4.34 +    by (simp, simp add: m1mod2k)
    4.35 +next
    4.36 +  case (3 bin bit)
    4.37 +  show ?case
    4.38 +  proof (cases n)
    4.39 +    case 0
    4.40 +    then show ?thesis by (simp add: int_and_extra_simps)
    4.41 +  next
    4.42 +    case (Suc m)
    4.43 +    with 3 show ?thesis
    4.44 +      by (simp only: power_BIT mod_BIT int_and_Bits) simp
    4.45 +  qed
    4.46 +qed
    4.47 +
    4.48  end
    4.49