Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
authorskalberg
Mon Mar 29 15:35:04 2004 +0200 (2004-03-29)
changeset 1449448ae8d678d88
parent 14493 216179c782a6
child 14495 e2a1c31cf6d3
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
to HOL/ex.
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Word.thy
src/HOL/Library/word_setup.ML
src/HOL/ex/Adder.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Mar 29 10:17:35 2004 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Mar 29 15:35:04 2004 +0200
     1.3 @@ -179,7 +179,7 @@
     1.4    Library/FuncSet.thy Library/Library.thy \
     1.5    Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \
     1.6    Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
     1.7 -  Library/Nat_Infinity.thy \
     1.8 +  Library/Nat_Infinity.thy Library/Word.thy Library/word_setup.ML \
     1.9    Library/README.html Library/Continuity.thy \
    1.10    Library/Nested_Environment.thy Library/Zorn.thy\
    1.11    Library/Library/ROOT.ML Library/Library/document/root.tex \
     2.1 --- a/src/HOL/Library/Library.thy	Mon Mar 29 10:17:35 2004 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Mon Mar 29 15:35:04 2004 +0200
     2.3 @@ -10,6 +10,7 @@
     2.4    Permutation +
     2.5    NatPair +
     2.6    Primes +
     2.7 +  Word +
     2.8    While_Combinator:
     2.9  end
    2.10  (*>*)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Word.thy	Mon Mar 29 15:35:04 2004 +0200
     3.3 @@ -0,0 +1,2991 @@
     3.4 +(*  Title:      HOL/Library/Word.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     3.7 +*)
     3.8 +
     3.9 +theory Word = Main files "word_setup.ML":
    3.10 +
    3.11 +subsection {* Auxilary Lemmas *}
    3.12 +
    3.13 +text {* Amazing that these are necessary, but I can't find equivalent
    3.14 +ones in the other HOL theories. *}
    3.15 +
    3.16 +lemma max_le [intro!]: "[| x \<le> z; y \<le> z |] ==> max x y \<le> z"
    3.17 +  by (simp add: max_def)
    3.18 +
    3.19 +lemma max_mono:
    3.20 +  assumes mf: "mono f"
    3.21 +  shows       "max (f (x::'a::linorder)) (f y) \<le> f (max x y)"
    3.22 +proof -
    3.23 +  from mf and le_maxI1 [of x y]
    3.24 +  have fx: "f x \<le> f (max x y)"
    3.25 +    by (rule monoD)
    3.26 +  from mf and le_maxI2 [of y x]
    3.27 +  have fy: "f y \<le> f (max x y)"
    3.28 +    by (rule monoD)
    3.29 +  from fx and fy
    3.30 +  show "max (f x) (f y) \<le> f (max x y)"
    3.31 +    by auto
    3.32 +qed
    3.33 +
    3.34 +lemma le_imp_power_le:
    3.35 +  assumes b0: "0 < (b::nat)"
    3.36 +  and     xy: "x \<le> y"
    3.37 +  shows       "b ^ x \<le> b ^ y"
    3.38 +proof (rule ccontr)
    3.39 +  assume "~ b ^ x \<le> b ^ y"
    3.40 +  hence bybx: "b ^ y < b ^ x"
    3.41 +    by simp
    3.42 +  have "y < x"
    3.43 +  proof (rule nat_power_less_imp_less [OF _ bybx])
    3.44 +    from b0
    3.45 +    show "0 < b"
    3.46 +      .
    3.47 +  qed
    3.48 +  with xy
    3.49 +  show False
    3.50 +    by simp
    3.51 +qed
    3.52 +
    3.53 +lemma less_imp_power_less:
    3.54 +  assumes b1: "1 < (b::nat)"
    3.55 +  and     xy: "x < y"
    3.56 +  shows       "b ^ x < b ^ y"
    3.57 +proof (rule ccontr)
    3.58 +  assume "~ b ^ x < b ^ y"
    3.59 +  hence bybx: "b ^ y \<le> b ^ x"
    3.60 +    by simp
    3.61 +  have "y \<le> x"
    3.62 +  proof (rule power_le_imp_le_exp [OF _ bybx])
    3.63 +    from b1
    3.64 +    show "1 < b"
    3.65 +      .
    3.66 +  qed
    3.67 +  with xy
    3.68 +  show False
    3.69 +    by simp
    3.70 +qed
    3.71 +
    3.72 +lemma [simp]: "1 < (b::nat) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
    3.73 +  apply rule
    3.74 +  apply (erule power_le_imp_le_exp)
    3.75 +  apply assumption
    3.76 +  apply (subgoal_tac "0 < b")
    3.77 +  apply (erule le_imp_power_le)
    3.78 +  apply assumption
    3.79 +  apply simp
    3.80 +  done
    3.81 +
    3.82 +lemma [simp]: "1 < (b::nat) ==> (b ^ x < b ^ y) = (x < y)"
    3.83 +  apply rule
    3.84 +  apply (subgoal_tac "0 < b")
    3.85 +  apply (erule nat_power_less_imp_less)
    3.86 +  apply assumption
    3.87 +  apply simp
    3.88 +  apply (erule less_imp_power_less)
    3.89 +  apply assumption
    3.90 +  done
    3.91 +
    3.92 +lemma power_le_imp_zle:
    3.93 +  assumes b1:   "1 < (b::int)"
    3.94 +  and     bxby: "b ^ x \<le> b ^ y"
    3.95 +  shows         "x \<le> y"
    3.96 +proof -
    3.97 +  from b1
    3.98 +  have nb1: "1 < nat b"
    3.99 +    by arith
   3.100 +  from b1
   3.101 +  have nb0: "0 \<le> b"
   3.102 +    by simp
   3.103 +  from bxby
   3.104 +  have "nat (b ^ x) \<le> nat (b ^ y)"
   3.105 +    by arith
   3.106 +  hence "nat b ^ x \<le> nat b ^ y"
   3.107 +    by (simp add: nat_power_eq [OF nb0])
   3.108 +  with power_le_imp_le_exp and nb1
   3.109 +  show "x \<le> y"
   3.110 +    by auto
   3.111 +qed
   3.112 +
   3.113 +lemma zero_le_zpower [intro]:
   3.114 +  assumes b0: "0 \<le> (b::int)"
   3.115 +  shows       "0 \<le> b ^ n"
   3.116 +proof (induct n,simp)
   3.117 +  fix n
   3.118 +  assume ind: "0 \<le> b ^ n"
   3.119 +  have "b * 0 \<le> b * b ^ n"
   3.120 +  proof (subst mult_le_cancel_left,auto intro!: ind)
   3.121 +    assume "b < 0"
   3.122 +    with b0
   3.123 +    show "b ^ n \<le> 0"
   3.124 +      by simp
   3.125 +  qed
   3.126 +  thus "0 \<le> b ^ Suc n"
   3.127 +    by simp
   3.128 +qed
   3.129 +
   3.130 +lemma zero_less_zpower [intro]:
   3.131 +  assumes b0: "0 < (b::int)"
   3.132 +  shows       "0 < b ^ n"
   3.133 +proof -
   3.134 +  from b0
   3.135 +  have b0': "0 \<le> b"
   3.136 +    by simp
   3.137 +  from b0
   3.138 +  have "0 < nat b"
   3.139 +    by simp
   3.140 +  hence "0 < nat b ^ n"
   3.141 +    by (rule zero_less_power)
   3.142 +  hence xx: "nat 0 < nat (b ^ n)"
   3.143 +    by (subst nat_power_eq [OF b0'],simp)
   3.144 +  show "0 < b ^ n"
   3.145 +    apply (subst nat_less_eq_zless [symmetric])
   3.146 +    apply simp
   3.147 +    apply (rule xx)
   3.148 +    done
   3.149 +qed
   3.150 +
   3.151 +lemma power_less_imp_zless:
   3.152 +  assumes b0:   "0 < (b::int)"
   3.153 +  and     bxby: "b ^ x < b ^ y"
   3.154 +  shows         "x < y"
   3.155 +proof -
   3.156 +  from b0
   3.157 +  have nb0: "0 < nat b"
   3.158 +    by arith
   3.159 +  from b0
   3.160 +  have b0': "0 \<le> b"
   3.161 +    by simp
   3.162 +  have "nat (b ^ x) < nat (b ^ y)"
   3.163 +  proof (subst nat_less_eq_zless)
   3.164 +    show "0 \<le> b ^ x"
   3.165 +      by (rule zero_le_zpower [OF b0'])
   3.166 +  next
   3.167 +    show "b ^ x < b ^ y"
   3.168 +      by (rule bxby)
   3.169 +  qed
   3.170 +  hence "nat b ^ x < nat b ^ y"
   3.171 +    by (simp add: nat_power_eq [OF b0'])
   3.172 +  with nat_power_less_imp_less [OF nb0]
   3.173 +  show "x < y"
   3.174 +    .
   3.175 +qed
   3.176 +
   3.177 +lemma le_imp_power_zle:
   3.178 +  assumes b0: "0 < (b::int)"
   3.179 +  and     xy: "x \<le> y"
   3.180 +  shows       "b ^ x \<le> b ^ y"
   3.181 +proof (rule ccontr)
   3.182 +  assume "~ b ^ x \<le> b ^ y"
   3.183 +  hence bybx: "b ^ y < b ^ x"
   3.184 +    by simp
   3.185 +  have "y < x"
   3.186 +  proof (rule power_less_imp_zless [OF _ bybx])
   3.187 +    from b0
   3.188 +    show "0 < b"
   3.189 +      .
   3.190 +  qed
   3.191 +  with xy
   3.192 +  show False
   3.193 +    by simp
   3.194 +qed
   3.195 +
   3.196 +lemma less_imp_power_zless:
   3.197 +  assumes b1: "1 < (b::int)"
   3.198 +  and     xy: "x < y"
   3.199 +  shows       "b ^ x < b ^ y"
   3.200 +proof (rule ccontr)
   3.201 +  assume "~ b ^ x < b ^ y"
   3.202 +  hence bybx: "b ^ y \<le> b ^ x"
   3.203 +    by simp
   3.204 +  have "y \<le> x"
   3.205 +  proof (rule power_le_imp_zle [OF _ bybx])
   3.206 +    from b1
   3.207 +    show "1 < b"
   3.208 +      .
   3.209 +  qed
   3.210 +  with xy
   3.211 +  show False
   3.212 +    by simp
   3.213 +qed
   3.214 +
   3.215 +lemma [simp]: "1 < (b::int) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
   3.216 +  apply rule
   3.217 +  apply (erule power_le_imp_zle)
   3.218 +  apply assumption
   3.219 +  apply (subgoal_tac "0 < b")
   3.220 +  apply (erule le_imp_power_zle)
   3.221 +  apply assumption
   3.222 +  apply simp
   3.223 +  done
   3.224 +
   3.225 +lemma [simp]: "1 < (b::int) ==> (b ^ x < b ^ y) = (x < y)"
   3.226 +  apply rule
   3.227 +  apply (subgoal_tac "0 < b")
   3.228 +  apply (erule power_less_imp_zless)
   3.229 +  apply assumption
   3.230 +  apply simp
   3.231 +  apply (erule less_imp_power_zless)
   3.232 +  apply assumption
   3.233 +  done
   3.234 +
   3.235 +lemma suc_zero_le: "[| 0 < x ; 0 < y |] ==> Suc 0 < x + y"
   3.236 +  by simp
   3.237 +
   3.238 +lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)"
   3.239 +  by (induct k,simp_all)
   3.240 +
   3.241 +section {* Bits *}
   3.242 +
   3.243 +datatype bit
   3.244 +  = Zero ("\<zero>")
   3.245 +  | One ("\<one>")
   3.246 +
   3.247 +consts
   3.248 +  bitval :: "bit => int"
   3.249 +
   3.250 +primrec
   3.251 +  "bitval \<zero> = 0"
   3.252 +  "bitval \<one> = 1"
   3.253 +
   3.254 +consts
   3.255 +  bitnot :: "bit => bit"
   3.256 +  bitand :: "bit => bit => bit" (infixr "bitand" 35)
   3.257 +  bitor  :: "bit => bit => bit" (infixr "bitor"  30)
   3.258 +  bitxor :: "bit => bit => bit" (infixr "bitxor" 30)
   3.259 +
   3.260 +syntax (xsymbols)
   3.261 +  bitnot :: "bit => bit"        ("\<not>\<^sub>b _" [40] 40)
   3.262 +  bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35)
   3.263 +  bitor  :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
   3.264 +  bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
   3.265 +
   3.266 +primrec
   3.267 +  bitnot_zero: "(bitnot \<zero>) = \<one>"
   3.268 +  bitnot_one : "(bitnot \<one>)  = \<zero>"
   3.269 +
   3.270 +primrec
   3.271 +  bitand_zero: "(\<zero> bitand y) = \<zero>"
   3.272 +  bitand_one:  "(\<one> bitand y) = y"
   3.273 +
   3.274 +primrec
   3.275 +  bitor_zero: "(\<zero> bitor y) = y"
   3.276 +  bitor_one:  "(\<one> bitor y) = \<one>"
   3.277 +
   3.278 +primrec
   3.279 +  bitxor_zero: "(\<zero> bitxor y) = y"
   3.280 +  bitxor_one:  "(\<one> bitxor y) = (bitnot y)"
   3.281 +
   3.282 +lemma [simp]: "(bitnot (bitnot b)) = b"
   3.283 +  by (cases b,simp_all)
   3.284 +
   3.285 +lemma [simp]: "(b bitand b) = b"
   3.286 +  by (cases b,simp_all)
   3.287 +
   3.288 +lemma [simp]: "(b bitor b) = b"
   3.289 +  by (cases b,simp_all)
   3.290 +
   3.291 +lemma [simp]: "(b bitxor b) = \<zero>"
   3.292 +  by (cases b,simp_all)
   3.293 +
   3.294 +section {* Bit Vectors *}
   3.295 +
   3.296 +text {* First, a couple of theorems expressing case analysis and
   3.297 +induction principles for bit vectors. *}
   3.298 +
   3.299 +lemma bit_list_cases:
   3.300 +  assumes empty: "w = [] ==> P w"
   3.301 +  and     zero:  "!!bs. w = \<zero> # bs ==> P w"
   3.302 +  and     one:   "!!bs. w = \<one> # bs ==> P w"
   3.303 +  shows   "P w"
   3.304 +proof (cases w)
   3.305 +  assume "w = []"
   3.306 +  thus ?thesis
   3.307 +    by (rule empty)
   3.308 +next
   3.309 +  fix b bs
   3.310 +  assume [simp]: "w = b # bs"
   3.311 +  show "P w"
   3.312 +  proof (cases b)
   3.313 +    assume "b = \<zero>"
   3.314 +    hence "w = \<zero> # bs"
   3.315 +      by simp
   3.316 +    thus ?thesis
   3.317 +      by (rule zero)
   3.318 +  next
   3.319 +    assume "b = \<one>"
   3.320 +    hence "w = \<one> # bs"
   3.321 +      by simp
   3.322 +    thus ?thesis
   3.323 +      by (rule one)
   3.324 +  qed
   3.325 +qed
   3.326 +
   3.327 +lemma bit_list_induct:
   3.328 +  assumes empty: "P []"
   3.329 +  and     zero:  "!!bs. P bs ==> P (\<zero>#bs)"
   3.330 +  and     one:   "!!bs. P bs ==> P (\<one>#bs)"
   3.331 +  shows   "P w"
   3.332 +proof (induct w,simp_all add: empty)
   3.333 +  fix b bs
   3.334 +  assume [intro!]: "P bs"
   3.335 +  show "P (b#bs)"
   3.336 +    by (cases b,auto intro!: zero one)
   3.337 +qed
   3.338 +
   3.339 +constdefs
   3.340 +  bv_msb :: "bit list => bit"
   3.341 +  "bv_msb w == if w = [] then \<zero> else hd w"
   3.342 +  bv_extend :: "[nat,bit,bit list]=>bit list"
   3.343 +  "bv_extend i b w == (replicate (i - length w) b) @ w"
   3.344 +  bv_not :: "bit list => bit list"
   3.345 +  "bv_not w == map bitnot w"
   3.346 +
   3.347 +lemma bv_length_extend [simp]: "length w \<le> i ==> length (bv_extend i b w) = i"
   3.348 +  by (simp add: bv_extend_def)
   3.349 +
   3.350 +lemma [simp]: "bv_not [] = []"
   3.351 +  by (simp add: bv_not_def)
   3.352 +
   3.353 +lemma [simp]: "bv_not (b#bs) = (bitnot b) # bv_not bs"
   3.354 +  by (simp add: bv_not_def)
   3.355 +
   3.356 +lemma [simp]: "bv_not (bv_not w) = w"
   3.357 +  by (rule bit_list_induct [of _ w],simp_all)
   3.358 +
   3.359 +lemma [simp]: "bv_msb [] = \<zero>"
   3.360 +  by (simp add: bv_msb_def)
   3.361 +
   3.362 +lemma [simp]: "bv_msb (b#bs) = b"
   3.363 +  by (simp add: bv_msb_def)
   3.364 +
   3.365 +lemma [simp]: "0 < length w ==> bv_msb (bv_not w) = (bitnot (bv_msb w))"
   3.366 +  by (cases w,simp_all)
   3.367 +
   3.368 +lemma [simp,intro]: "bv_msb w = \<one> ==> 0 < length w"
   3.369 +  by (cases w,simp_all)
   3.370 +
   3.371 +lemma [simp]: "length (bv_not w) = length w"
   3.372 +  by (induct w,simp_all)
   3.373 +
   3.374 +constdefs
   3.375 +  bv_to_nat :: "bit list => int"
   3.376 +  "bv_to_nat bv == number_of (foldl (%bn b. bn BIT (b = \<one>)) bin.Pls bv)"
   3.377 +
   3.378 +lemma [simp]: "bv_to_nat [] = 0"
   3.379 +  by (simp add: bv_to_nat_def)
   3.380 +
   3.381 +lemma pos_number_of: "(0::int)\<le> number_of w ==> number_of (w BIT b) = (2::int) * number_of w + (if b then 1 else 0)"
   3.382 +  by (induct w,auto,simp add: iszero_def)
   3.383 +
   3.384 +lemma bv_to_nat_helper [simp]: "bv_to_nat (b # bs) = bitval b * 2 ^ length bs + bv_to_nat bs"
   3.385 +proof -
   3.386 +  def bv_to_nat' == "%base bv. number_of (foldl (% bn b. bn BIT (b = \<one>)) base bv)::int"
   3.387 +  have bv_to_nat'_def: "!!base bv. bv_to_nat' base bv == number_of (foldl (% bn b. bn BIT (b = \<one>)) base bv)::int"
   3.388 +    by (simp add: bv_to_nat'_def)
   3.389 +  have [rule_format]: "\<forall> base bs. (0::int) \<le> number_of base --> (\<forall> b. bv_to_nat' base (b # bs) = bv_to_nat' (base BIT (b = \<one>)) bs)"
   3.390 +    by (simp add: bv_to_nat'_def)
   3.391 +  have helper [rule_format]: "\<forall> base. (0::int) \<le> number_of base --> bv_to_nat' base bs = number_of base * 2 ^ length bs + bv_to_nat' bin.Pls bs"
   3.392 +  proof (induct bs,simp add: bv_to_nat'_def,clarify)
   3.393 +    fix x xs base
   3.394 +    assume ind [rule_format]: "\<forall> base. (0::int) \<le> number_of base --> bv_to_nat' base xs = number_of base * 2 ^ length xs + bv_to_nat' bin.Pls xs"
   3.395 +    assume base_pos: "(0::int) \<le> number_of base"
   3.396 +    def qq == "number_of base::int"
   3.397 +    show "bv_to_nat' base (x # xs) = number_of base * 2 ^ (length (x # xs)) + bv_to_nat' bin.Pls (x # xs)"
   3.398 +      apply (unfold bv_to_nat'_def)
   3.399 +      apply (simp only: foldl.simps)
   3.400 +      apply (fold bv_to_nat'_def)
   3.401 +      apply (subst ind [of "base BIT (x = \<one>)"])
   3.402 +      using base_pos
   3.403 +      apply simp
   3.404 +      apply (subst ind [of "bin.Pls BIT (x = \<one>)"])
   3.405 +      apply simp
   3.406 +      apply (subst pos_number_of [of "base" "x = \<one>"])
   3.407 +      using base_pos
   3.408 +      apply simp
   3.409 +      apply (subst pos_number_of [of "bin.Pls" "x = \<one>"])
   3.410 +      apply simp
   3.411 +      apply (fold qq_def)
   3.412 +      apply (simp add: ring_distrib)
   3.413 +      done
   3.414 +  qed
   3.415 +  show ?thesis
   3.416 +    apply (unfold bv_to_nat_def [of "b # bs"])
   3.417 +    apply (simp only: foldl.simps)
   3.418 +    apply (fold bv_to_nat'_def)
   3.419 +    apply (subst helper)
   3.420 +    apply simp
   3.421 +    apply (cases "b::bit")
   3.422 +    apply (simp add: bv_to_nat'_def bv_to_nat_def)
   3.423 +    apply (simp add: iszero_def)
   3.424 +    apply (simp add: bv_to_nat'_def bv_to_nat_def)
   3.425 +    done
   3.426 +qed
   3.427 +
   3.428 +lemma bv_to_nat0 [simp]: "bv_to_nat (\<zero>#bs) = bv_to_nat bs"
   3.429 +  by simp
   3.430 +
   3.431 +lemma bv_to_nat1 [simp]: "bv_to_nat (\<one>#bs) = 2 ^ length bs + bv_to_nat bs"
   3.432 +  by simp
   3.433 +
   3.434 +lemma bv_to_nat_lower_range [intro,simp]: "0 \<le> bv_to_nat w"
   3.435 +  apply (induct w,simp_all)
   3.436 +  apply (case_tac a,simp_all)
   3.437 +  apply (rule add_increasing)
   3.438 +  apply auto
   3.439 +  done
   3.440 +
   3.441 +lemma bv_to_nat_upper_range: "bv_to_nat w < 2 ^ length w"
   3.442 +proof (induct w,simp_all)
   3.443 +  fix b bs
   3.444 +  assume "bv_to_nat bs < 2 ^ length bs"
   3.445 +  show "bitval b * 2 ^ length bs + bv_to_nat bs < 2 * 2 ^ length bs"
   3.446 +  proof (cases b,simp_all)
   3.447 +    have "bv_to_nat bs < 2 ^ length bs"
   3.448 +      .
   3.449 +    also have "... < 2 * 2 ^ length bs"
   3.450 +      by auto
   3.451 +    finally show "bv_to_nat bs < 2 * 2 ^ length bs"
   3.452 +      by simp
   3.453 +  next
   3.454 +    have "bv_to_nat bs < 2 ^ length bs"
   3.455 +      .
   3.456 +    hence "2 ^ length bs + bv_to_nat bs < 2 ^ length bs + 2 ^ length bs"
   3.457 +      by arith
   3.458 +    also have "... = 2 * (2 ^ length bs)"
   3.459 +      by simp
   3.460 +    finally show "bv_to_nat bs < 2 ^ length bs"
   3.461 +      by simp
   3.462 +  qed
   3.463 +qed
   3.464 +
   3.465 +lemma [simp]:
   3.466 +  assumes wn: "n \<le> length w"
   3.467 +  shows       "bv_extend n b w = w"
   3.468 +  by (simp add: bv_extend_def wn)
   3.469 +
   3.470 +lemma [simp]:
   3.471 +  assumes wn: "length w < n"
   3.472 +  shows       "bv_extend n b w = bv_extend n b (b#w)"
   3.473 +proof -
   3.474 +  from wn
   3.475 +  have s: "n - Suc (length w) + 1 = n - length w"
   3.476 +    by arith
   3.477 +  have "bv_extend n b w = replicate (n - length w) b @ w"
   3.478 +    by (simp add: bv_extend_def)
   3.479 +  also have "... = replicate (n - Suc (length w) + 1) b @ w"
   3.480 +    by (subst s,rule)
   3.481 +  also have "... = (replicate (n - Suc (length w)) b @ replicate 1 b) @ w"
   3.482 +    by (subst replicate_add,rule)
   3.483 +  also have "... = replicate (n - Suc (length w)) b @ b # w"
   3.484 +    by simp
   3.485 +  also have "... = bv_extend n b (b#w)"
   3.486 +    by (simp add: bv_extend_def)
   3.487 +  finally show "bv_extend n b w = bv_extend n b (b#w)"
   3.488 +    .
   3.489 +qed
   3.490 +
   3.491 +consts
   3.492 +  rem_initial :: "bit => bit list => bit list"
   3.493 +
   3.494 +primrec
   3.495 +  "rem_initial b [] = []"
   3.496 +  "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)"
   3.497 +
   3.498 +lemma rem_initial_length: "length (rem_initial b w) \<le> length w"
   3.499 +  by (rule bit_list_induct [of _ w],simp_all (no_asm),safe,simp_all)
   3.500 +
   3.501 +lemma rem_initial_equal:
   3.502 +  assumes p: "length (rem_initial b w) = length w"
   3.503 +  shows      "rem_initial b w = w"
   3.504 +proof -
   3.505 +  have "length (rem_initial b w) = length w --> rem_initial b w = w"
   3.506 +  proof (induct w,simp_all,clarify)
   3.507 +    fix xs
   3.508 +    assume "length (rem_initial b xs) = length xs --> rem_initial b xs = xs"
   3.509 +    assume f: "length (rem_initial b xs) = Suc (length xs)"
   3.510 +    with rem_initial_length [of b xs]
   3.511 +    show "rem_initial b xs = b#xs"
   3.512 +      by auto
   3.513 +  qed
   3.514 +  thus ?thesis
   3.515 +    ..
   3.516 +qed
   3.517 +
   3.518 +lemma bv_extend_rem_initial: "bv_extend (length w) b (rem_initial b w) = w"
   3.519 +proof (induct w,simp_all,safe)
   3.520 +  fix xs
   3.521 +  assume ind: "bv_extend (length xs) b (rem_initial b xs) = xs"
   3.522 +  from rem_initial_length [of b xs]
   3.523 +  have [simp]: "Suc (length xs) - length (rem_initial b xs) = 1 + (length xs - length (rem_initial b xs))"
   3.524 +    by arith
   3.525 +  have "bv_extend (Suc (length xs)) b (rem_initial b xs) = replicate (Suc (length xs) - length (rem_initial b xs)) b @ (rem_initial b xs)"
   3.526 +    by (simp add: bv_extend_def)
   3.527 +  also have "... = replicate (1 + (length xs - length (rem_initial b xs))) b @ rem_initial b xs"
   3.528 +    by simp
   3.529 +  also have "... = (replicate 1 b @ replicate (length xs - length (rem_initial b xs)) b) @ rem_initial b xs"
   3.530 +    by (subst replicate_add,rule refl)
   3.531 +  also have "... = b # bv_extend (length xs) b (rem_initial b xs)"
   3.532 +    by (auto simp add: bv_extend_def [symmetric])
   3.533 +  also have "... = b # xs"
   3.534 +    by (simp add: ind)
   3.535 +  finally show "bv_extend (Suc (length xs)) b (rem_initial b xs) = b # xs"
   3.536 +    .
   3.537 +qed
   3.538 +
   3.539 +lemma rem_initial_append1:
   3.540 +  assumes "rem_initial b xs ~= []"
   3.541 +  shows   "rem_initial b (xs @ ys) = rem_initial b xs @ ys"
   3.542 +proof -
   3.543 +  have "rem_initial b xs ~= [] --> rem_initial b (xs @ ys) = rem_initial b xs @ ys" (is "?P xs ys")
   3.544 +    by (induct xs,auto)
   3.545 +  thus ?thesis
   3.546 +    ..
   3.547 +qed
   3.548 +
   3.549 +lemma rem_initial_append2:
   3.550 +  assumes "rem_initial b xs = []"
   3.551 +  shows   "rem_initial b (xs @ ys) = rem_initial b ys"
   3.552 +proof -
   3.553 +  have "rem_initial b xs = [] --> rem_initial b (xs @ ys) = rem_initial b ys" (is "?P xs ys")
   3.554 +    by (induct xs,auto)
   3.555 +  thus ?thesis
   3.556 +    ..
   3.557 +qed
   3.558 +
   3.559 +constdefs
   3.560 +  norm_unsigned :: "bit list => bit list"
   3.561 +  "norm_unsigned == rem_initial \<zero>"
   3.562 +
   3.563 +lemma [simp]: "norm_unsigned [] = []"
   3.564 +  by (simp add: norm_unsigned_def)
   3.565 +
   3.566 +lemma [simp]: "norm_unsigned (\<zero>#bs) = norm_unsigned bs"
   3.567 +  by (simp add: norm_unsigned_def)
   3.568 +
   3.569 +lemma [simp]: "norm_unsigned (\<one>#bs) = \<one>#bs"
   3.570 +  by (simp add: norm_unsigned_def)
   3.571 +
   3.572 +lemma [simp]: "norm_unsigned (norm_unsigned w) = norm_unsigned w"
   3.573 +  by (rule bit_list_induct [of _ w],simp_all)
   3.574 +
   3.575 +consts
   3.576 +  nat_to_bv_helper :: "int => bit list => bit list"
   3.577 +
   3.578 +recdef nat_to_bv_helper "measure nat"
   3.579 +  "nat_to_bv_helper n = (%bs. (if n \<le> 0 then bs
   3.580 +                               else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs)))"
   3.581 +
   3.582 +constdefs
   3.583 +  nat_to_bv :: "int => bit list"
   3.584 +  "nat_to_bv n == nat_to_bv_helper n []"
   3.585 +
   3.586 +lemma nat_to_bv0 [simp]: "nat_to_bv 0 = []"
   3.587 +  by (simp add: nat_to_bv_def)
   3.588 +
   3.589 +lemmas [simp del] = nat_to_bv_helper.simps
   3.590 +
   3.591 +lemma n_div_2_cases:
   3.592 +  assumes n0  : "0 \<le> n"
   3.593 +  and     zero: "(n::int) = 0 ==> R"
   3.594 +  and     div : "[| n div 2 < n ; 0 < n |] ==> R"
   3.595 +  shows         "R"
   3.596 +proof (cases "n = 0")
   3.597 +  assume "n = 0"
   3.598 +  thus R
   3.599 +    by (rule zero)
   3.600 +next
   3.601 +  assume "n ~= 0"
   3.602 +  with n0
   3.603 +  have nn0: "0 < n"
   3.604 +    by simp
   3.605 +  hence "n div 2 < n"
   3.606 +    by arith
   3.607 +  from this and nn0
   3.608 +  show R
   3.609 +    by (rule div)
   3.610 +qed
   3.611 +
   3.612 +lemma int_wf_ge_induct:
   3.613 +  assumes base:  "P (k::int)"
   3.614 +  and     ind :  "!!i. (!!j. [| k \<le> j ; j < i |] ==> P j) ==> P i"
   3.615 +  and     valid: "k \<le> i"
   3.616 +  shows          "P i"
   3.617 +proof -
   3.618 +  have a: "\<forall> j. k \<le> j \<and> j < i --> P j"
   3.619 +  proof (rule int_ge_induct)
   3.620 +    show "k \<le> i"
   3.621 +      .
   3.622 +  next
   3.623 +    show "\<forall> j. k \<le> j \<and> j < k --> P j"
   3.624 +      by auto
   3.625 +  next
   3.626 +    fix i
   3.627 +    assume "k \<le> i"
   3.628 +    assume a: "\<forall> j. k \<le> j \<and> j < i --> P j"
   3.629 +    have pi: "P i"
   3.630 +    proof (rule ind)
   3.631 +      fix j
   3.632 +      assume "k \<le> j" and "j < i"
   3.633 +      with a
   3.634 +      show "P j"
   3.635 +	by auto
   3.636 +    qed
   3.637 +    show "\<forall> j. k \<le> j \<and> j < i + 1 --> P j"
   3.638 +    proof auto
   3.639 +      fix j
   3.640 +      assume kj: "k \<le> j"
   3.641 +      assume ji: "j \<le> i"
   3.642 +      show "P j"
   3.643 +      proof (cases "j = i")
   3.644 +	assume "j = i"
   3.645 +	with pi
   3.646 +	show "P j"
   3.647 +	  by simp
   3.648 +      next
   3.649 +	assume "j ~= i"
   3.650 +	with ji
   3.651 +	have "j < i"
   3.652 +	  by simp
   3.653 +	with kj and a
   3.654 +	show "P j"
   3.655 +	  by blast
   3.656 +      qed
   3.657 +    qed
   3.658 +  qed
   3.659 +  show "P i"
   3.660 +  proof (rule ind)
   3.661 +    fix j
   3.662 +    assume "k \<le> j" and "j < i"
   3.663 +    with a
   3.664 +    show "P j"
   3.665 +      by auto
   3.666 +  qed
   3.667 +qed
   3.668 +
   3.669 +lemma unfold_nat_to_bv_helper:
   3.670 +  "0 \<le> b ==> nat_to_bv_helper b l = nat_to_bv_helper b [] @ l"
   3.671 +proof -
   3.672 +  assume "0 \<le> b"
   3.673 +  have "\<forall>l. nat_to_bv_helper b l = nat_to_bv_helper b [] @ l"
   3.674 +  proof (rule int_wf_ge_induct [where ?i = b])
   3.675 +    show "0 \<le> b"
   3.676 +      .
   3.677 +  next
   3.678 +    show "\<forall> l. nat_to_bv_helper 0 l = nat_to_bv_helper 0 [] @ l"
   3.679 +      by (simp add: nat_to_bv_helper.simps)
   3.680 +  next
   3.681 +    fix n
   3.682 +    assume ind: "!!j. [| 0 \<le> j ; j < n |] ==> \<forall> l. nat_to_bv_helper j l = nat_to_bv_helper j [] @ l"
   3.683 +    show "\<forall>l. nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
   3.684 +    proof
   3.685 +      fix l
   3.686 +      show "nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
   3.687 +      proof (cases "n < 0")
   3.688 +	assume "n < 0"
   3.689 +	thus ?thesis
   3.690 +	  by (simp add: nat_to_bv_helper.simps)
   3.691 +      next
   3.692 +	assume "~n < 0"
   3.693 +	show ?thesis
   3.694 +	proof (rule n_div_2_cases [of n])
   3.695 +	  from prems
   3.696 +	  show "0 \<le> n"
   3.697 +	    by simp
   3.698 +	next
   3.699 +	  assume [simp]: "n = 0"
   3.700 +	  show ?thesis
   3.701 +	    apply (subst nat_to_bv_helper.simps [of n])
   3.702 +	    apply simp
   3.703 +	    done
   3.704 +	next
   3.705 +	  assume n2n: "n div 2 < n"
   3.706 +	  assume [simp]: "0 < n"
   3.707 +	  hence n20: "0 \<le> n div 2"
   3.708 +	    by arith
   3.709 +	  from ind [of "n div 2"] and n2n n20
   3.710 +	  have ind': "\<forall>l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l"
   3.711 +	    by blast
   3.712 +	  show ?thesis
   3.713 +	    apply (subst nat_to_bv_helper.simps [of n])
   3.714 +	    apply simp
   3.715 +	    apply (subst spec [OF ind',of "\<zero>#l"])
   3.716 +	    apply (subst spec [OF ind',of "\<one>#l"])
   3.717 +	    apply (subst spec [OF ind',of "[\<one>]"])
   3.718 +	    apply (subst spec [OF ind',of "[\<zero>]"])
   3.719 +	    apply simp
   3.720 +	    done
   3.721 +	qed
   3.722 +      qed
   3.723 +    qed
   3.724 +  qed
   3.725 +  thus ?thesis
   3.726 +    ..
   3.727 +qed
   3.728 +
   3.729 +lemma nat_to_bv_non0 [simp]: "0 < n ==> nat_to_bv n = nat_to_bv (n div 2) @ [if n mod 2 = 0 then \<zero> else \<one>]"
   3.730 +proof -
   3.731 +  assume [simp]: "0 < n"
   3.732 +  show ?thesis
   3.733 +    apply (subst nat_to_bv_def [of n])
   3.734 +    apply (subst nat_to_bv_helper.simps [of n])
   3.735 +    apply (subst unfold_nat_to_bv_helper)
   3.736 +    using prems
   3.737 +    apply arith
   3.738 +    apply simp
   3.739 +    apply (subst nat_to_bv_def [of "n div 2"])
   3.740 +    apply auto
   3.741 +    using prems
   3.742 +    apply auto
   3.743 +    done
   3.744 +qed
   3.745 +
   3.746 +lemma bv_to_nat_dist_append: "bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
   3.747 +proof -
   3.748 +  have "\<forall>l2. bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
   3.749 +  proof (induct l1,simp_all)
   3.750 +    fix x xs
   3.751 +    assume ind: "\<forall>l2. bv_to_nat (xs @ l2) = bv_to_nat xs * 2 ^ length l2 + bv_to_nat l2"
   3.752 +    show "\<forall>l2. bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
   3.753 +    proof
   3.754 +      fix l2
   3.755 +      show "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
   3.756 +      proof -
   3.757 +	have "(2::int) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
   3.758 +	  by (induct "length xs",simp_all)
   3.759 +	hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 =
   3.760 +	  bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
   3.761 +	  by simp
   3.762 +	also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
   3.763 +	  by (simp add: ring_distrib)
   3.764 +	finally show ?thesis .
   3.765 +      qed
   3.766 +    qed
   3.767 +  qed
   3.768 +  thus ?thesis
   3.769 +    ..
   3.770 +qed
   3.771 +
   3.772 +lemma bv_nat_bv [simp]:
   3.773 +  assumes n0: "0 \<le> n"
   3.774 +  shows       "bv_to_nat (nat_to_bv n) = n"
   3.775 +proof -
   3.776 +  have "0 \<le> n --> bv_to_nat (nat_to_bv n) = n"
   3.777 +  proof (rule int_wf_ge_induct [where ?k = 0],simp_all,clarify)
   3.778 +    fix n
   3.779 +    assume ind: "!!j. [| 0 \<le> j; j < n |] ==> bv_to_nat (nat_to_bv j) = j"
   3.780 +    assume n0: "0 \<le> n"
   3.781 +    show "bv_to_nat (nat_to_bv n) = n"
   3.782 +    proof (rule n_div_2_cases [of n])
   3.783 +      show "0 \<le> n"
   3.784 +	.
   3.785 +    next
   3.786 +      assume [simp]: "n = 0"
   3.787 +      show ?thesis
   3.788 +	by simp
   3.789 +    next
   3.790 +      assume nn: "n div 2 < n"
   3.791 +      assume n0: "0 < n"
   3.792 +      hence n20: "0 \<le> n div 2"
   3.793 +	by arith
   3.794 +      from ind and n20 nn
   3.795 +      have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2"
   3.796 +	by blast
   3.797 +      from n0 have n0': "~ n \<le> 0"
   3.798 +	by simp
   3.799 +      show ?thesis
   3.800 +	apply (subst nat_to_bv_def)
   3.801 +	apply (subst nat_to_bv_helper.simps [of n])
   3.802 +	apply (simp add: n0' split del: split_if)
   3.803 +	apply (subst unfold_nat_to_bv_helper)
   3.804 +	apply (rule n20)
   3.805 +	apply (subst bv_to_nat_dist_append)
   3.806 +	apply (fold nat_to_bv_def)
   3.807 +	apply (simp add: ind' split del: split_if)
   3.808 +	apply (cases "n mod 2 = 0")
   3.809 +      proof simp_all
   3.810 +	assume "n mod 2 = 0"
   3.811 +	with zmod_zdiv_equality [of n 2]
   3.812 +	show "n div 2 * 2 = n"
   3.813 +	  by simp
   3.814 +      next
   3.815 +	assume "n mod 2 = 1"
   3.816 +	with zmod_zdiv_equality [of n 2]
   3.817 +	show "n div 2 * 2 + 1 = n"
   3.818 +	  by simp
   3.819 +      qed
   3.820 +    qed
   3.821 +  qed
   3.822 +  with n0
   3.823 +  show ?thesis
   3.824 +    by auto
   3.825 +qed
   3.826 +
   3.827 +lemma [simp]: "bv_to_nat (norm_unsigned w) = bv_to_nat w"
   3.828 +  by (rule bit_list_induct,simp_all)
   3.829 +
   3.830 +lemma [simp]: "length (norm_unsigned w) \<le> length w"
   3.831 +  by (rule bit_list_induct,simp_all)
   3.832 +
   3.833 +lemma bv_to_nat_rew_msb: "bv_msb w = \<one> ==> bv_to_nat w = 2 ^ (length w - 1) + bv_to_nat (tl w)"
   3.834 +  by (rule bit_list_cases [of w],simp_all)
   3.835 +
   3.836 +lemma norm_unsigned_result: "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>"
   3.837 +proof (rule length_induct [of _ xs])
   3.838 +  fix xs :: "bit list"
   3.839 +  assume ind: "\<forall>ys. length ys < length xs --> norm_unsigned ys = [] \<or> bv_msb (norm_unsigned ys) = \<one>"
   3.840 +  show "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>"
   3.841 +  proof (rule bit_list_cases [of xs],simp_all)
   3.842 +    fix bs
   3.843 +    assume [simp]: "xs = \<zero>#bs"
   3.844 +    from ind
   3.845 +    have "length bs < length xs --> norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>"
   3.846 +      ..
   3.847 +    thus "norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>"
   3.848 +      by simp
   3.849 +  qed
   3.850 +qed
   3.851 +
   3.852 +lemma norm_empty_bv_to_nat_zero:
   3.853 +  assumes nw: "norm_unsigned w = []"
   3.854 +  shows       "bv_to_nat w = 0"
   3.855 +proof -
   3.856 +  have "bv_to_nat w = bv_to_nat (norm_unsigned w)"
   3.857 +    by simp
   3.858 +  also have "... = bv_to_nat []"
   3.859 +    by (subst nw,rule)
   3.860 +  also have "... = 0"
   3.861 +    by simp
   3.862 +  finally show ?thesis .
   3.863 +qed
   3.864 +
   3.865 +lemma bv_to_nat_lower_limit:
   3.866 +  assumes w0: "0 < bv_to_nat w"
   3.867 +  shows         "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat w"
   3.868 +proof -
   3.869 +  from w0 and norm_unsigned_result [of w]
   3.870 +  have msbw: "bv_msb (norm_unsigned w) = \<one>"
   3.871 +    by (auto simp add: norm_empty_bv_to_nat_zero)
   3.872 +  have "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat (norm_unsigned w)"
   3.873 +    by (subst bv_to_nat_rew_msb [OF msbw],simp)
   3.874 +  thus ?thesis
   3.875 +    by simp
   3.876 +qed
   3.877 +
   3.878 +lemmas [simp del] = nat_to_bv_non0
   3.879 +
   3.880 +lemma norm_unsigned_length [intro!]: "length (norm_unsigned w) \<le> length w"
   3.881 +  by (subst norm_unsigned_def,rule rem_initial_length)
   3.882 +
   3.883 +lemma norm_unsigned_equal: "length (norm_unsigned w) = length w ==> norm_unsigned w = w"
   3.884 +  by (simp add: norm_unsigned_def,rule rem_initial_equal)
   3.885 +
   3.886 +lemma bv_extend_norm_unsigned: "bv_extend (length w) \<zero> (norm_unsigned w) = w"
   3.887 +  by (simp add: norm_unsigned_def,rule bv_extend_rem_initial)
   3.888 +
   3.889 +lemma norm_unsigned_append1 [simp]: "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys"
   3.890 +  by (simp add: norm_unsigned_def,rule rem_initial_append1)
   3.891 +
   3.892 +lemma norm_unsigned_append2 [simp]: "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"
   3.893 +  by (simp add: norm_unsigned_def,rule rem_initial_append2)
   3.894 +
   3.895 +lemma bv_to_nat_zero_imp_empty:
   3.896 +  assumes "bv_to_nat w = 0"
   3.897 +  shows   "norm_unsigned w = []"
   3.898 +proof -
   3.899 +  have "bv_to_nat w = 0 --> norm_unsigned w = []"
   3.900 +    apply (rule bit_list_induct [of _ w],simp_all)
   3.901 +    apply (subgoal_tac "0 < 2 ^ length bs + bv_to_nat bs")
   3.902 +    apply simp
   3.903 +    apply (subgoal_tac "(0::int) < 2 ^ length bs")
   3.904 +    apply (subgoal_tac "0 \<le> bv_to_nat bs")
   3.905 +    apply arith
   3.906 +    apply auto
   3.907 +    done
   3.908 +  thus ?thesis
   3.909 +    ..
   3.910 +qed
   3.911 +
   3.912 +lemma bv_to_nat_nzero_imp_nempty:
   3.913 +  assumes "bv_to_nat w \<noteq> 0"
   3.914 +  shows   "norm_unsigned w \<noteq> []"
   3.915 +proof -
   3.916 +  have "bv_to_nat w \<noteq> 0 --> norm_unsigned w \<noteq> []"
   3.917 +    by (rule bit_list_induct [of _ w],simp_all)
   3.918 +  thus ?thesis
   3.919 +    ..
   3.920 +qed
   3.921 +
   3.922 +lemma nat_helper1:
   3.923 +  assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
   3.924 +  shows        "nat_to_bv (2 * bv_to_nat w + bitval x) = norm_unsigned (w @ [x])"
   3.925 +proof (cases x)
   3.926 +  assume [simp]: "x = \<one>"
   3.927 +  show ?thesis
   3.928 +    apply (simp add: nat_to_bv_non0)
   3.929 +    apply safe
   3.930 +  proof -
   3.931 +    fix q
   3.932 +    assume "(2 * bv_to_nat w) + 1 = 2 * q"
   3.933 +    hence orig: "(2 * bv_to_nat w + 1) mod 2 = 2 * q mod 2" (is "?lhs = ?rhs")
   3.934 +      by simp
   3.935 +    have "?lhs = (1 + 2 * bv_to_nat w) mod 2"
   3.936 +      by (simp add: add_commute)
   3.937 +    also have "... = 1"
   3.938 +      by (simp add: zmod_zadd1_eq)
   3.939 +    finally have eq1: "?lhs = 1" .
   3.940 +    have "?rhs  = 0"
   3.941 +      by simp
   3.942 +    with orig and eq1
   3.943 +    have "(1::int) = 0"
   3.944 +      by simp
   3.945 +    thus "nat_to_bv ((2 * bv_to_nat w + 1) div 2) @ [\<zero>] = norm_unsigned (w @ [\<one>])"
   3.946 +      by simp
   3.947 +  next
   3.948 +    have "nat_to_bv ((2 * bv_to_nat w + 1) div 2) @ [\<one>] = nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\<one>]"
   3.949 +      by (simp add: add_commute)
   3.950 +    also have "... = nat_to_bv (bv_to_nat w) @ [\<one>]"
   3.951 +      by (subst zdiv_zadd1_eq,simp)
   3.952 +    also have "... = norm_unsigned w @ [\<one>]"
   3.953 +      by (subst ass,rule refl)
   3.954 +    also have "... = norm_unsigned (w @ [\<one>])"
   3.955 +      by (cases "norm_unsigned w",simp_all)
   3.956 +    finally show "nat_to_bv ((2 * bv_to_nat w + 1) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])"
   3.957 +      .
   3.958 +  qed
   3.959 +next
   3.960 +  assume [simp]: "x = \<zero>"
   3.961 +  show ?thesis
   3.962 +  proof (cases "bv_to_nat w = 0")
   3.963 +    assume "bv_to_nat w = 0"
   3.964 +    thus ?thesis
   3.965 +      by (simp add: bv_to_nat_zero_imp_empty)
   3.966 +  next
   3.967 +    assume "bv_to_nat w \<noteq> 0"
   3.968 +    thus ?thesis
   3.969 +      apply simp
   3.970 +      apply (subst nat_to_bv_non0)
   3.971 +      apply simp
   3.972 +      apply auto
   3.973 +      apply (cut_tac bv_to_nat_lower_range [of w])
   3.974 +      apply arith
   3.975 +      apply (subst ass)
   3.976 +      apply (cases "norm_unsigned w")
   3.977 +      apply (simp_all add: norm_empty_bv_to_nat_zero)
   3.978 +      done
   3.979 +  qed
   3.980 +qed
   3.981 +
   3.982 +lemma nat_helper2: "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs"
   3.983 +proof -
   3.984 +  have "\<forall>xs. nat_to_bv (2 ^ length (rev xs) + bv_to_nat (rev xs)) = \<one> # (rev xs)" (is "\<forall>xs. ?P xs")
   3.985 +  proof
   3.986 +    fix xs
   3.987 +    show "?P xs"
   3.988 +    proof (rule length_induct [of _ xs])
   3.989 +      fix xs :: "bit list"
   3.990 +      assume ind: "\<forall>ys. length ys < length xs --> ?P ys"
   3.991 +      show "?P xs"
   3.992 +      proof (cases xs)
   3.993 +	assume [simp]: "xs = []"
   3.994 +	show ?thesis
   3.995 +	  by (simp add: nat_to_bv_non0)
   3.996 +      next
   3.997 +	fix y ys
   3.998 +	assume [simp]: "xs = y # ys"
   3.999 +	show ?thesis
  3.1000 +	  apply simp
  3.1001 +	  apply (subst bv_to_nat_dist_append)
  3.1002 +	  apply simp
  3.1003 +	proof -
  3.1004 +	  have "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
  3.1005 +	    nat_to_bv (2 * (2 ^ length ys + bv_to_nat (rev ys)) + bitval y)"
  3.1006 +	    by (simp add: add_ac mult_ac)
  3.1007 +	  also have "... = nat_to_bv (2 * (bv_to_nat (\<one>#rev ys)) + bitval y)"
  3.1008 +	    by simp
  3.1009 +	  also have "... = norm_unsigned (\<one>#rev ys) @ [y]"
  3.1010 +	  proof -
  3.1011 +	    from ind
  3.1012 +	    have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = \<one> # rev ys"
  3.1013 +	      by auto
  3.1014 +	    hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = \<one> # rev ys"
  3.1015 +	      by simp
  3.1016 +	    show ?thesis
  3.1017 +	      apply (subst nat_helper1)
  3.1018 +	      apply simp_all
  3.1019 +	      done
  3.1020 +	  qed
  3.1021 +	  also have "... = (\<one>#rev ys) @ [y]"
  3.1022 +	    by simp
  3.1023 +	  also have "... = \<one> # rev ys @ [y]"
  3.1024 +	    by simp
  3.1025 +	  finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = \<one> # rev ys @ [y]"
  3.1026 +	    .
  3.1027 +	qed
  3.1028 +      qed
  3.1029 +    qed
  3.1030 +  qed
  3.1031 +  hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) = \<one> # rev (rev xs)"
  3.1032 +    ..
  3.1033 +  thus ?thesis
  3.1034 +    by simp
  3.1035 +qed
  3.1036 +
  3.1037 +lemma nat_bv_nat [simp]: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
  3.1038 +proof (rule bit_list_induct [of _ w],simp_all)
  3.1039 +  fix xs
  3.1040 +  assume "nat_to_bv (bv_to_nat xs) = norm_unsigned xs"
  3.1041 +  have "bv_to_nat xs = bv_to_nat (norm_unsigned xs)"
  3.1042 +    by simp
  3.1043 +  have "bv_to_nat xs < 2 ^ length xs"
  3.1044 +    by (rule bv_to_nat_upper_range)
  3.1045 +  show "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs"
  3.1046 +    by (rule nat_helper2)
  3.1047 +qed
  3.1048 +
  3.1049 +lemma [simp]: "bv_to_nat (norm_unsigned xs) = bv_to_nat xs"
  3.1050 +  by (rule bit_list_induct [of _ w],simp_all)
  3.1051 +
  3.1052 +lemma bv_to_nat_qinj:
  3.1053 +  assumes one: "bv_to_nat xs = bv_to_nat ys"
  3.1054 +  and     len: "length xs = length ys"
  3.1055 +  shows        "xs = ys"
  3.1056 +proof -
  3.1057 +  from one
  3.1058 +  have "nat_to_bv (bv_to_nat xs) = nat_to_bv (bv_to_nat ys)"
  3.1059 +    by simp
  3.1060 +  hence xsys: "norm_unsigned xs = norm_unsigned ys"
  3.1061 +    by simp
  3.1062 +  have "xs = bv_extend (length xs) \<zero> (norm_unsigned xs)"
  3.1063 +    by (simp add: bv_extend_norm_unsigned)
  3.1064 +  also have "... = bv_extend (length ys) \<zero> (norm_unsigned ys)"
  3.1065 +    by (simp add: xsys len)
  3.1066 +  also have "... = ys"
  3.1067 +    by (simp add: bv_extend_norm_unsigned)
  3.1068 +  finally show ?thesis .
  3.1069 +qed
  3.1070 +
  3.1071 +lemma norm_unsigned_nat_to_bv [simp]:
  3.1072 +  assumes [simp]: "0 \<le> n"
  3.1073 +  shows "norm_unsigned (nat_to_bv n) = nat_to_bv n"
  3.1074 +proof -
  3.1075 +  have "norm_unsigned (nat_to_bv n) = nat_to_bv (bv_to_nat (norm_unsigned (nat_to_bv n)))"
  3.1076 +    by (subst nat_bv_nat,simp)
  3.1077 +  also have "... = nat_to_bv n"
  3.1078 +    by simp
  3.1079 +  finally show ?thesis .
  3.1080 +qed
  3.1081 +
  3.1082 +lemma length_nat_to_bv_upper_limit:
  3.1083 +  assumes nk: "n \<le> 2 ^ k - 1"
  3.1084 +  shows       "length (nat_to_bv n) \<le> k"
  3.1085 +proof (cases "n \<le> 0")
  3.1086 +  assume "n \<le> 0"
  3.1087 +  thus ?thesis
  3.1088 +    by (simp add: nat_to_bv_def nat_to_bv_helper.simps)
  3.1089 +next
  3.1090 +  assume "~ n \<le> 0"
  3.1091 +  hence n0: "0 < n"
  3.1092 +    by simp
  3.1093 +  hence n00: "0 \<le> n"
  3.1094 +    by simp
  3.1095 +  show ?thesis
  3.1096 +  proof (rule ccontr)
  3.1097 +    assume "~ length (nat_to_bv n) \<le> k"
  3.1098 +    hence "k < length (nat_to_bv n)"
  3.1099 +      by simp
  3.1100 +    hence "k \<le> length (nat_to_bv n) - 1"
  3.1101 +      by arith
  3.1102 +    hence "(2::int) ^ k \<le> 2 ^ (length (nat_to_bv n) - 1)"
  3.1103 +      by simp
  3.1104 +    also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)"
  3.1105 +      by (simp add: n00)
  3.1106 +    also have "... \<le> bv_to_nat (nat_to_bv n)"
  3.1107 +      by (rule bv_to_nat_lower_limit,simp add: n00 n0)
  3.1108 +    also have "... = n"
  3.1109 +      by (simp add: n00)
  3.1110 +    finally have "2 ^ k \<le> n" .
  3.1111 +    with n0
  3.1112 +    have "2 ^ k - 1 < n"
  3.1113 +      by arith
  3.1114 +    with nk
  3.1115 +    show False
  3.1116 +      by simp
  3.1117 +  qed
  3.1118 +qed
  3.1119 +
  3.1120 +lemma length_nat_to_bv_lower_limit:
  3.1121 +  assumes nk: "2 ^ k \<le> n"
  3.1122 +  shows       "k < length (nat_to_bv n)"
  3.1123 +proof (rule ccontr)
  3.1124 +  have "(0::int) \<le> 2 ^ k"
  3.1125 +    by auto
  3.1126 +  with nk
  3.1127 +  have [simp]: "0 \<le> n"
  3.1128 +    by auto
  3.1129 +  assume "~ k < length (nat_to_bv n)"
  3.1130 +  hence lnk: "length (nat_to_bv n) \<le> k"
  3.1131 +    by simp
  3.1132 +  have "n = bv_to_nat (nat_to_bv n)"
  3.1133 +    by simp
  3.1134 +  also have "... < 2 ^ length (nat_to_bv n)"
  3.1135 +    by (rule bv_to_nat_upper_range)
  3.1136 +  also from lnk have "... \<le> 2 ^ k"
  3.1137 +    by simp
  3.1138 +  finally have "n < 2 ^ k" .
  3.1139 +  with nk
  3.1140 +  show False
  3.1141 +    by simp
  3.1142 +qed
  3.1143 +
  3.1144 +section {* Unsigned Arithmetic Operations *}
  3.1145 +
  3.1146 +constdefs
  3.1147 +  bv_add :: "[bit list, bit list ] => bit list"
  3.1148 +  "bv_add w1 w2 == nat_to_bv (bv_to_nat w1 + bv_to_nat w2)"
  3.1149 +
  3.1150 +lemma [simp]: "bv_add (norm_unsigned w1) w2 = bv_add w1 w2"
  3.1151 +  by (simp add: bv_add_def)
  3.1152 +
  3.1153 +lemma [simp]: "bv_add w1 (norm_unsigned w2) = bv_add w1 w2"
  3.1154 +  by (simp add: bv_add_def)
  3.1155 +
  3.1156 +lemma [simp]: "norm_unsigned (bv_add w1 w2) = bv_add w1 w2"
  3.1157 +  apply (simp add: bv_add_def)
  3.1158 +  apply (rule norm_unsigned_nat_to_bv)
  3.1159 +  apply (subgoal_tac "0 \<le> bv_to_nat w1")
  3.1160 +  apply (subgoal_tac "0 \<le> bv_to_nat w2")
  3.1161 +  apply arith
  3.1162 +  apply simp_all
  3.1163 +  done
  3.1164 +
  3.1165 +lemma bv_add_length: "length (bv_add w1 w2) \<le> Suc (max (length w1) (length w2))"
  3.1166 +proof (unfold bv_add_def,rule length_nat_to_bv_upper_limit)
  3.1167 +  from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2]
  3.1168 +  have "bv_to_nat w1 + bv_to_nat w2 \<le> (2 ^ length w1 - 1) + (2 ^ length w2 - 1)"
  3.1169 +    by arith
  3.1170 +  also have "... \<le> max (2 ^ length w1 - 1) (2 ^ length w2 - 1) + max (2 ^ length w1 - 1) (2 ^ length w2 - 1)"
  3.1171 +    by (rule add_mono,safe intro!: le_maxI1 le_maxI2)
  3.1172 +  also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)"
  3.1173 +    by simp
  3.1174 +  also have "... \<le> 2 ^ Suc (max (length w1) (length w2)) - 2"
  3.1175 +  proof (cases "length w1 \<le> length w2")
  3.1176 +    assume [simp]: "length w1 \<le> length w2"
  3.1177 +    hence "(2::int) ^ length w1 \<le> 2 ^ length w2"
  3.1178 +      by simp
  3.1179 +    hence [simp]: "(2::int) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
  3.1180 +      by arith
  3.1181 +    show ?thesis
  3.1182 +      by (simp split: split_max)
  3.1183 +  next
  3.1184 +    assume [simp]: "~ (length w1 \<le> length w2)"
  3.1185 +    have "~ ((2::int) ^ length w1 - 1 \<le> 2 ^ length w2 - 1)"
  3.1186 +    proof
  3.1187 +      assume "(2::int) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
  3.1188 +      hence "((2::int) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1"
  3.1189 +	by (rule add_right_mono)
  3.1190 +      hence "(2::int) ^ length w1 \<le> 2 ^ length w2"
  3.1191 +	by simp
  3.1192 +      hence "length w1 \<le> length w2"
  3.1193 +	by simp
  3.1194 +      thus False
  3.1195 +	by simp
  3.1196 +    qed
  3.1197 +    thus ?thesis
  3.1198 +      by (simp split: split_max)
  3.1199 +  qed
  3.1200 +  finally show "bv_to_nat w1 + bv_to_nat w2 \<le> 2 ^ Suc (max (length w1) (length w2)) - 1"
  3.1201 +    by arith
  3.1202 +qed
  3.1203 +
  3.1204 +constdefs
  3.1205 +  bv_mult :: "[bit list, bit list ] => bit list"
  3.1206 +  "bv_mult w1 w2 == nat_to_bv (bv_to_nat w1 * bv_to_nat w2)"
  3.1207 +
  3.1208 +lemma [simp]: "bv_mult (norm_unsigned w1) w2 = bv_mult w1 w2"
  3.1209 +  by (simp add: bv_mult_def)
  3.1210 +
  3.1211 +lemma [simp]: "bv_mult w1 (norm_unsigned w2) = bv_mult w1 w2"
  3.1212 +  by (simp add: bv_mult_def)
  3.1213 +
  3.1214 +lemma [simp]: "norm_unsigned (bv_mult w1 w2) = bv_mult w1 w2"
  3.1215 +  apply (simp add: bv_mult_def)
  3.1216 +  apply (rule norm_unsigned_nat_to_bv)
  3.1217 +  apply (subgoal_tac "0 * 0 \<le> bv_to_nat w1 * bv_to_nat w2")
  3.1218 +  apply simp
  3.1219 +  apply (rule mult_mono,simp_all)
  3.1220 +  done
  3.1221 +
  3.1222 +lemma bv_mult_length: "length (bv_mult w1 w2) \<le> length w1 + length w2"
  3.1223 +proof (unfold bv_mult_def,rule length_nat_to_bv_upper_limit)
  3.1224 +  from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2]
  3.1225 +  have h: "bv_to_nat w1 \<le> 2 ^ length w1 - 1 \<and> bv_to_nat w2 \<le> 2 ^ length w2 - 1"
  3.1226 +    by arith
  3.1227 +  have "bv_to_nat w1 * bv_to_nat w2 \<le> (2 ^ length w1 - 1) * (2 ^ length w2 - 1)"
  3.1228 +    apply (cut_tac h)
  3.1229 +    apply (rule mult_mono)
  3.1230 +    apply auto
  3.1231 +    done
  3.1232 +  also have "... < 2 ^ length w1 * 2 ^ length w2"
  3.1233 +    by (rule mult_strict_mono,auto)
  3.1234 +  also have "... = 2 ^ (length w1 + length w2)"
  3.1235 +    by (simp add: power_add)
  3.1236 +  finally show "bv_to_nat w1 * bv_to_nat w2 \<le> 2 ^ (length w1 + length w2) - 1"
  3.1237 +    by arith
  3.1238 +qed
  3.1239 +
  3.1240 +section {* Signed Vectors *}
  3.1241 +
  3.1242 +consts
  3.1243 +  norm_signed :: "bit list => bit list"
  3.1244 +
  3.1245 +primrec
  3.1246 +  norm_signed_Nil: "norm_signed [] = []"
  3.1247 +  norm_signed_Cons: "norm_signed (b#bs) = (case b of \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs | \<one> => b#rem_initial b bs)"
  3.1248 +
  3.1249 +lemma [simp]: "norm_signed [\<zero>] = []"
  3.1250 +  by simp
  3.1251 +
  3.1252 +lemma [simp]: "norm_signed [\<one>] = [\<one>]"
  3.1253 +  by simp
  3.1254 +
  3.1255 +lemma [simp]: "norm_signed (\<zero>#\<one>#xs) = \<zero>#\<one>#xs"
  3.1256 +  by simp
  3.1257 +
  3.1258 +lemma [simp]: "norm_signed (\<zero>#\<zero>#xs) = norm_signed (\<zero>#xs)"
  3.1259 +  by simp
  3.1260 +
  3.1261 +lemma [simp]: "norm_signed (\<one>#\<zero>#xs) = \<one>#\<zero>#xs"
  3.1262 +  by simp
  3.1263 +
  3.1264 +lemma [simp]: "norm_signed (\<one>#\<one>#xs) = norm_signed (\<one>#xs)"
  3.1265 +  by simp
  3.1266 +
  3.1267 +lemmas [simp del] = norm_signed_Cons
  3.1268 +
  3.1269 +constdefs
  3.1270 +  int_to_bv :: "int => bit list"
  3.1271 +  "int_to_bv n == if 0 \<le> n
  3.1272 +                 then norm_signed (\<zero>#nat_to_bv n)
  3.1273 +                 else norm_signed (bv_not (\<zero>#nat_to_bv (-n- 1)))"
  3.1274 +
  3.1275 +lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # nat_to_bv n)"
  3.1276 +  by (simp add: int_to_bv_def)
  3.1277 +
  3.1278 +lemma int_to_bv_lt0 [simp]: "n < 0 ==> int_to_bv n = norm_signed (bv_not (\<zero>#nat_to_bv (-n- 1)))"
  3.1279 +  by (simp add: int_to_bv_def)
  3.1280 +
  3.1281 +lemma [simp]: "norm_signed (norm_signed w) = norm_signed w"
  3.1282 +proof (rule bit_list_induct [of _ w],simp_all)
  3.1283 +  fix xs
  3.1284 +  assume "norm_signed (norm_signed xs) = norm_signed xs"
  3.1285 +  show "norm_signed (norm_signed (\<zero>#xs)) = norm_signed (\<zero>#xs)"
  3.1286 +  proof (rule bit_list_cases [of xs],simp_all)
  3.1287 +    fix ys
  3.1288 +    assume [symmetric,simp]: "xs = \<zero>#ys"
  3.1289 +    show "norm_signed (norm_signed (\<zero>#ys)) = norm_signed (\<zero>#ys)"
  3.1290 +      by simp
  3.1291 +  qed
  3.1292 +next
  3.1293 +  fix xs
  3.1294 +  assume "norm_signed (norm_signed xs) = norm_signed xs"
  3.1295 +  show "norm_signed (norm_signed (\<one>#xs)) = norm_signed (\<one>#xs)"
  3.1296 +  proof (rule bit_list_cases [of xs],simp_all)
  3.1297 +    fix ys
  3.1298 +    assume [symmetric,simp]: "xs = \<one>#ys"
  3.1299 +    show "norm_signed (norm_signed (\<one>#ys)) = norm_signed (\<one>#ys)"
  3.1300 +      by simp
  3.1301 +  qed
  3.1302 +qed
  3.1303 +
  3.1304 +constdefs
  3.1305 +  bv_to_int :: "bit list => int"
  3.1306 +  "bv_to_int w == case bv_msb w of \<zero> => bv_to_nat w | \<one> => -(bv_to_nat (bv_not w) + 1)"
  3.1307 +
  3.1308 +lemma [simp]: "bv_to_int [] = 0"
  3.1309 +  by (simp add: bv_to_int_def)
  3.1310 +
  3.1311 +lemma [simp]: "bv_to_int (\<zero>#bs) = bv_to_nat bs"
  3.1312 +  by (simp add: bv_to_int_def)
  3.1313 +
  3.1314 +lemma [simp]: "bv_to_int (\<one>#bs) = -(bv_to_nat (bv_not bs) + 1)"
  3.1315 +  by (simp add: bv_to_int_def)
  3.1316 +
  3.1317 +lemma [simp]: "bv_to_int (norm_signed w) = bv_to_int w"
  3.1318 +proof (rule bit_list_induct [of _ w],simp_all)
  3.1319 +  fix xs
  3.1320 +  assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
  3.1321 +  show "bv_to_int (norm_signed (\<zero>#xs)) = bv_to_nat xs"
  3.1322 +  proof (rule bit_list_cases [of xs],simp_all)
  3.1323 +    fix ys
  3.1324 +    assume [simp]: "xs = \<zero>#ys"
  3.1325 +    from ind
  3.1326 +    show "bv_to_int (norm_signed (\<zero>#ys)) = bv_to_nat ys"
  3.1327 +      by simp
  3.1328 +  qed
  3.1329 +next
  3.1330 +  fix xs
  3.1331 +  assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
  3.1332 +  show "bv_to_int (norm_signed (\<one>#xs)) = - bv_to_nat (bv_not xs) + -1"
  3.1333 +  proof (rule bit_list_cases [of xs],simp_all)
  3.1334 +    fix ys
  3.1335 +    assume [simp]: "xs = \<one>#ys"
  3.1336 +    from ind
  3.1337 +    show "bv_to_int (norm_signed (\<one>#ys)) = - bv_to_nat (bv_not ys) + -1"
  3.1338 +      by simp
  3.1339 +  qed
  3.1340 +qed
  3.1341 +
  3.1342 +lemma bv_to_int_upper_range: "bv_to_int w < 2 ^ (length w - 1)"
  3.1343 +proof (rule bit_list_cases [of w],simp_all)
  3.1344 +  fix bs
  3.1345 +  show "bv_to_nat bs < 2 ^ length bs"
  3.1346 +    by (rule bv_to_nat_upper_range)
  3.1347 +next
  3.1348 +  fix bs
  3.1349 +  have "- (bv_to_nat (bv_not bs)) + -1 \<le> 0 + 0"
  3.1350 +    by (rule add_mono,simp_all)
  3.1351 +  also have "... < 2 ^ length bs"
  3.1352 +    by (induct bs,simp_all)
  3.1353 +  finally show "- (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs"
  3.1354 +    .
  3.1355 +qed
  3.1356 +
  3.1357 +lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) \<le> bv_to_int w"
  3.1358 +proof (rule bit_list_cases [of w],simp_all)
  3.1359 +  fix bs :: "bit list"
  3.1360 +  have "- (2 ^ length bs) \<le> (0::int)"
  3.1361 +    by (induct bs,simp_all)
  3.1362 +  also have "... \<le> bv_to_nat bs"
  3.1363 +    by simp
  3.1364 +  finally show "- (2 ^ length bs) \<le> bv_to_nat bs"
  3.1365 +    .
  3.1366 +next
  3.1367 +  fix bs
  3.1368 +  from bv_to_nat_upper_range [of "bv_not bs"]
  3.1369 +  have "bv_to_nat (bv_not bs) < 2 ^ length bs"
  3.1370 +    by simp
  3.1371 +  hence "bv_to_nat (bv_not bs) + 1 \<le> 2 ^ length bs"
  3.1372 +    by simp
  3.1373 +  thus "- (2 ^ length bs) \<le> - bv_to_nat (bv_not bs) + -1"
  3.1374 +    by simp
  3.1375 +qed
  3.1376 +
  3.1377 +lemma int_bv_int [simp]: "int_to_bv (bv_to_int w) = norm_signed w"
  3.1378 +proof (rule bit_list_cases [of w],simp)
  3.1379 +  fix xs
  3.1380 +  assume [simp]: "w = \<zero>#xs"
  3.1381 +  show ?thesis
  3.1382 +    apply simp
  3.1383 +    apply (subst norm_signed_Cons [of "\<zero>" "xs"])
  3.1384 +    apply simp
  3.1385 +    using norm_unsigned_result [of xs]
  3.1386 +    apply safe
  3.1387 +    apply (rule bit_list_cases [of "norm_unsigned xs"])
  3.1388 +    apply simp_all
  3.1389 +    done
  3.1390 +next
  3.1391 +  fix xs
  3.1392 +  assume [simp]: "w = \<one>#xs"
  3.1393 +  show ?thesis
  3.1394 +    apply simp
  3.1395 +    apply (rule bit_list_induct [of _ xs])
  3.1396 +    apply simp
  3.1397 +    apply (subst int_to_bv_lt0)
  3.1398 +    apply (subgoal_tac "- bv_to_nat (bv_not (\<zero> # bs)) + -1 < 0 + 0")
  3.1399 +    apply simp
  3.1400 +    apply (rule add_le_less_mono)
  3.1401 +    apply simp
  3.1402 +    apply (rule order_trans [of _ 0])
  3.1403 +    apply simp
  3.1404 +    apply (rule zero_le_zpower,simp)
  3.1405 +    apply simp
  3.1406 +    apply simp
  3.1407 +    apply (simp del: bv_to_nat1 bv_to_nat_helper)
  3.1408 +    apply simp
  3.1409 +    done
  3.1410 +qed
  3.1411 +
  3.1412 +lemma bv_int_bv [simp]: "bv_to_int (int_to_bv i) = i"
  3.1413 +  by (cases "0 \<le> i",simp_all)
  3.1414 +
  3.1415 +lemma bv_msb_norm [simp]: "bv_msb (norm_signed w) = bv_msb w"
  3.1416 +  by (rule bit_list_cases [of w],simp_all add: norm_signed_Cons)
  3.1417 +
  3.1418 +lemma norm_signed_length: "length (norm_signed w) \<le> length w"
  3.1419 +  apply (cases w,simp_all)
  3.1420 +  apply (subst norm_signed_Cons)
  3.1421 +  apply (case_tac "a",simp_all)
  3.1422 +  apply (rule rem_initial_length)
  3.1423 +  done
  3.1424 +
  3.1425 +lemma norm_signed_equal: "length (norm_signed w) = length w ==> norm_signed w = w"
  3.1426 +proof (rule bit_list_cases [of w],simp_all)
  3.1427 +  fix xs
  3.1428 +  assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)"
  3.1429 +  thus "norm_signed (\<zero>#xs) = \<zero>#xs"
  3.1430 +    apply (simp add: norm_signed_Cons)
  3.1431 +    apply safe
  3.1432 +    apply simp_all
  3.1433 +    apply (rule norm_unsigned_equal)
  3.1434 +    apply assumption
  3.1435 +    done
  3.1436 +next
  3.1437 +  fix xs
  3.1438 +  assume "length (norm_signed (\<one>#xs)) = Suc (length xs)"
  3.1439 +  thus "norm_signed (\<one>#xs) = \<one>#xs"
  3.1440 +    apply (simp add: norm_signed_Cons)
  3.1441 +    apply (rule rem_initial_equal)
  3.1442 +    apply assumption
  3.1443 +    done
  3.1444 +qed
  3.1445 +
  3.1446 +lemma bv_extend_norm_signed: "bv_msb w = b ==> bv_extend (length w) b (norm_signed w) = w"
  3.1447 +proof (rule bit_list_cases [of w],simp_all)
  3.1448 +  fix xs
  3.1449 +  show "bv_extend (Suc (length xs)) \<zero> (norm_signed (\<zero>#xs)) = \<zero>#xs"
  3.1450 +  proof (simp add: norm_signed_list_def,auto)
  3.1451 +    assume "norm_unsigned xs = []"
  3.1452 +    hence xx: "rem_initial \<zero> xs = []"
  3.1453 +      by (simp add: norm_unsigned_def)
  3.1454 +    have "bv_extend (Suc (length xs)) \<zero> (\<zero>#rem_initial \<zero> xs) = \<zero>#xs"
  3.1455 +      apply (simp add: bv_extend_def replicate_app_Cons_same)
  3.1456 +      apply (fold bv_extend_def)
  3.1457 +      apply (rule bv_extend_rem_initial)
  3.1458 +      done
  3.1459 +    thus "bv_extend (Suc (length xs)) \<zero> [\<zero>] = \<zero>#xs"
  3.1460 +      by (simp add: xx)
  3.1461 +  next
  3.1462 +    show "bv_extend (Suc (length xs)) \<zero> (\<zero>#norm_unsigned xs) = \<zero>#xs"
  3.1463 +      apply (simp add: norm_unsigned_def)
  3.1464 +      apply (simp add: bv_extend_def replicate_app_Cons_same)
  3.1465 +      apply (fold bv_extend_def)
  3.1466 +      apply (rule bv_extend_rem_initial)
  3.1467 +      done
  3.1468 +  qed
  3.1469 +next
  3.1470 +  fix xs
  3.1471 +  show "bv_extend (Suc (length xs)) \<one> (norm_signed (\<one>#xs)) = \<one>#xs"
  3.1472 +    apply (simp add: norm_signed_Cons)
  3.1473 +    apply (simp add: bv_extend_def replicate_app_Cons_same)
  3.1474 +    apply (fold bv_extend_def)
  3.1475 +    apply (rule bv_extend_rem_initial)
  3.1476 +    done
  3.1477 +qed
  3.1478 +
  3.1479 +lemma bv_to_int_qinj:
  3.1480 +  assumes one: "bv_to_int xs = bv_to_int ys"
  3.1481 +  and     len: "length xs = length ys"
  3.1482 +  shows        "xs = ys"
  3.1483 +proof -
  3.1484 +  from one
  3.1485 +  have "int_to_bv (bv_to_int xs) = int_to_bv (bv_to_int ys)"
  3.1486 +    by simp
  3.1487 +  hence xsys: "norm_signed xs = norm_signed ys"
  3.1488 +    by simp
  3.1489 +  hence xsys': "bv_msb xs = bv_msb ys"
  3.1490 +  proof -
  3.1491 +    have "bv_msb xs = bv_msb (norm_signed xs)"
  3.1492 +      by simp
  3.1493 +    also have "... = bv_msb (norm_signed ys)"
  3.1494 +      by (simp add: xsys)
  3.1495 +    also have "... = bv_msb ys"
  3.1496 +      by simp
  3.1497 +    finally show ?thesis .
  3.1498 +  qed
  3.1499 +  have "xs = bv_extend (length xs) (bv_msb xs) (norm_signed xs)"
  3.1500 +    by (simp add: bv_extend_norm_signed)
  3.1501 +  also have "... = bv_extend (length ys) (bv_msb ys) (norm_signed ys)"
  3.1502 +    by (simp add: xsys xsys' len)
  3.1503 +  also have "... = ys"
  3.1504 +    by (simp add: bv_extend_norm_signed)
  3.1505 +  finally show ?thesis .
  3.1506 +qed
  3.1507 +
  3.1508 +lemma [simp]: "norm_signed (int_to_bv w) = int_to_bv w"
  3.1509 +  by (simp add: int_to_bv_def)
  3.1510 +
  3.1511 +lemma bv_to_int_msb0: "0 \<le> bv_to_int w1 ==> bv_msb w1 = \<zero>"
  3.1512 +  apply (rule bit_list_cases,simp_all)
  3.1513 +  apply (subgoal_tac "0 \<le> bv_to_nat (bv_not bs)")
  3.1514 +  apply simp_all
  3.1515 +  done
  3.1516 +
  3.1517 +lemma bv_to_int_msb1: "bv_to_int w1 < 0 ==> bv_msb w1 = \<one>"
  3.1518 +  apply (rule bit_list_cases,simp_all)
  3.1519 +  apply (subgoal_tac "0 \<le> bv_to_nat bs")
  3.1520 +  apply simp_all
  3.1521 +  done
  3.1522 +
  3.1523 +lemma bv_to_int_lower_limit_gt0:
  3.1524 +  assumes w0: "0 < bv_to_int w"
  3.1525 +  shows       "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int w"
  3.1526 +proof -
  3.1527 +  from w0
  3.1528 +  have "0 \<le> bv_to_int w"
  3.1529 +    by simp
  3.1530 +  hence [simp]: "bv_msb w = \<zero>"
  3.1531 +    by (rule bv_to_int_msb0)
  3.1532 +  have "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int (norm_signed w)"
  3.1533 +  proof (rule bit_list_cases [of w])
  3.1534 +    assume "w = []"
  3.1535 +    with w0
  3.1536 +    show ?thesis
  3.1537 +      by simp
  3.1538 +  next
  3.1539 +    fix w'
  3.1540 +    assume weq: "w = \<zero> # w'"
  3.1541 +    thus ?thesis
  3.1542 +    proof (simp add: norm_signed_Cons,safe)
  3.1543 +      assume "norm_unsigned w' = []"
  3.1544 +      with weq and w0
  3.1545 +      show False
  3.1546 +	by (simp add: norm_empty_bv_to_nat_zero)
  3.1547 +    next
  3.1548 +      assume w'0: "norm_unsigned w' \<noteq> []"
  3.1549 +      have "0 < bv_to_nat w'"
  3.1550 +      proof (rule ccontr)
  3.1551 +	assume "~ (0 < bv_to_nat w')"
  3.1552 +	with bv_to_nat_lower_range [of w']
  3.1553 +	have "bv_to_nat w' = 0"
  3.1554 +	  by arith
  3.1555 +	hence "norm_unsigned w' = []"
  3.1556 +	  by (simp add: bv_to_nat_zero_imp_empty)
  3.1557 +	with w'0
  3.1558 +	show False
  3.1559 +	  by simp
  3.1560 +      qed
  3.1561 +      with bv_to_nat_lower_limit [of w']
  3.1562 +      have "2 ^ (length (norm_unsigned w') - 1) \<le> bv_to_nat w'"
  3.1563 +	.
  3.1564 +      thus "2 ^ (length (norm_unsigned w') - Suc 0) \<le> bv_to_nat w'"
  3.1565 +	by simp
  3.1566 +    qed
  3.1567 +  next
  3.1568 +    fix w'
  3.1569 +    assume "w = \<one> # w'"
  3.1570 +    from w0
  3.1571 +    have "bv_msb w = \<zero>"
  3.1572 +      by simp
  3.1573 +    with prems
  3.1574 +    show ?thesis
  3.1575 +      by simp
  3.1576 +  qed
  3.1577 +  also have "...  = bv_to_int w"
  3.1578 +    by simp
  3.1579 +  finally show ?thesis .
  3.1580 +qed
  3.1581 +
  3.1582 +lemma norm_signed_result: "norm_signed w = [] \<or> norm_signed w = [\<one>] \<or> bv_msb (norm_signed w) \<noteq> bv_msb (tl (norm_signed w))"
  3.1583 +  apply (rule bit_list_cases [of w],simp_all)
  3.1584 +  apply (case_tac "bs",simp_all)
  3.1585 +  apply (case_tac "a",simp_all)
  3.1586 +  apply (simp add: norm_signed_Cons)
  3.1587 +  apply safe
  3.1588 +  apply simp
  3.1589 +proof -
  3.1590 +  fix l
  3.1591 +  assume msb: "\<zero> = bv_msb (norm_unsigned l)"
  3.1592 +  assume "norm_unsigned l \<noteq> []"
  3.1593 +  with norm_unsigned_result [of l]
  3.1594 +  have "bv_msb (norm_unsigned l) = \<one>"
  3.1595 +    by simp
  3.1596 +  with msb
  3.1597 +  show False
  3.1598 +    by simp
  3.1599 +next
  3.1600 +  fix xs
  3.1601 +  assume p: "\<one> = bv_msb (tl (norm_signed (\<one> # xs)))"
  3.1602 +  have "\<one> \<noteq> bv_msb (tl (norm_signed (\<one> # xs)))"
  3.1603 +    by (rule bit_list_induct [of _ xs],simp_all)
  3.1604 +  with p
  3.1605 +  show False
  3.1606 +    by simp
  3.1607 +qed
  3.1608 +
  3.1609 +lemma bv_to_int_upper_limit_lem1:
  3.1610 +  assumes w0: "bv_to_int w < -1"
  3.1611 +  shows       "bv_to_int w < - (2 ^ (length (norm_signed w) - 2))"
  3.1612 +proof -
  3.1613 +  from w0
  3.1614 +  have "bv_to_int w < 0"
  3.1615 +    by simp
  3.1616 +  hence msbw [simp]: "bv_msb w = \<one>"
  3.1617 +    by (rule bv_to_int_msb1)
  3.1618 +  have "bv_to_int w = bv_to_int (norm_signed w)"
  3.1619 +    by simp
  3.1620 +  also from norm_signed_result [of w]
  3.1621 +  have "... < - (2 ^ (length (norm_signed w) - 2))"
  3.1622 +  proof (safe)
  3.1623 +    assume "norm_signed w = []"
  3.1624 +    hence "bv_to_int (norm_signed w) = 0"
  3.1625 +      by simp
  3.1626 +    with w0
  3.1627 +    show ?thesis
  3.1628 +      by simp
  3.1629 +  next
  3.1630 +    assume "norm_signed w = [\<one>]"
  3.1631 +    hence "bv_to_int (norm_signed w) = -1"
  3.1632 +      by simp
  3.1633 +    with w0
  3.1634 +    show ?thesis
  3.1635 +      by simp
  3.1636 +  next
  3.1637 +    assume "bv_msb (norm_signed w) \<noteq> bv_msb (tl (norm_signed w))"
  3.1638 +    hence msb_tl: "\<one> \<noteq> bv_msb (tl (norm_signed w))"
  3.1639 +      by simp
  3.1640 +    show "bv_to_int (norm_signed w) < - (2 ^ (length (norm_signed w) - 2))"
  3.1641 +    proof (rule bit_list_cases [of "norm_signed w"])
  3.1642 +      assume "norm_signed w = []"
  3.1643 +      hence "bv_to_int (norm_signed w) = 0"
  3.1644 +	by simp
  3.1645 +      with w0
  3.1646 +      show ?thesis
  3.1647 +	by simp
  3.1648 +    next
  3.1649 +      fix w'
  3.1650 +      assume nw: "norm_signed w = \<zero> # w'"
  3.1651 +      from msbw
  3.1652 +      have "bv_msb (norm_signed w) = \<one>"
  3.1653 +	by simp
  3.1654 +      with nw
  3.1655 +      show ?thesis
  3.1656 +	by simp
  3.1657 +    next
  3.1658 +      fix w'
  3.1659 +      assume weq: "norm_signed w = \<one> # w'"
  3.1660 +      show ?thesis
  3.1661 +      proof (rule bit_list_cases [of w'])
  3.1662 +	assume w'eq: "w' = []"
  3.1663 +	from w0
  3.1664 +	have "bv_to_int (norm_signed w) < -1"
  3.1665 +	  by simp
  3.1666 +	with w'eq and weq
  3.1667 +	show ?thesis
  3.1668 +	  by simp
  3.1669 +      next
  3.1670 +	fix w''
  3.1671 +	assume w'eq: "w' = \<zero> # w''"
  3.1672 +	show ?thesis
  3.1673 +	  apply (simp add: weq w'eq)
  3.1674 +	  apply (subgoal_tac "-bv_to_nat (bv_not w'') + -1 < 0 + 0")
  3.1675 +	  apply simp
  3.1676 +	  apply (rule add_le_less_mono)
  3.1677 +	  apply simp_all
  3.1678 +	  done
  3.1679 +      next
  3.1680 +	fix w''
  3.1681 +	assume w'eq: "w' = \<one> # w''"
  3.1682 +	with weq and msb_tl
  3.1683 +	show ?thesis
  3.1684 +	  by simp
  3.1685 +      qed
  3.1686 +    qed
  3.1687 +  qed
  3.1688 +  finally show ?thesis .
  3.1689 +qed
  3.1690 +
  3.1691 +lemma length_int_to_bv_upper_limit_gt0:
  3.1692 +  assumes w0: "0 < i"
  3.1693 +  and     wk: "i \<le> 2 ^ (k - 1) - 1"
  3.1694 +  shows       "length (int_to_bv i) \<le> k"
  3.1695 +proof (rule ccontr)
  3.1696 +  from w0 wk
  3.1697 +  have k1: "1 < k"
  3.1698 +    by (cases "k - 1",simp_all,arith)
  3.1699 +  assume "~ length (int_to_bv i) \<le> k"
  3.1700 +  hence "k < length (int_to_bv i)"
  3.1701 +    by simp
  3.1702 +  hence "k \<le> length (int_to_bv i) - 1"
  3.1703 +    by arith
  3.1704 +  hence a: "k - 1 \<le> length (int_to_bv i) - 2"
  3.1705 +    by arith
  3.1706 +  have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)"
  3.1707 +    apply (rule le_imp_power_zle,simp)
  3.1708 +    apply (rule a)
  3.1709 +    done
  3.1710 +  also have "... \<le> i"
  3.1711 +  proof -
  3.1712 +    have "2 ^ (length (norm_signed (int_to_bv i)) - 2) \<le> bv_to_int (int_to_bv i)"
  3.1713 +    proof (rule bv_to_int_lower_limit_gt0)
  3.1714 +      from w0
  3.1715 +      show "0 < bv_to_int (int_to_bv i)"
  3.1716 +	by simp
  3.1717 +    qed
  3.1718 +    thus ?thesis
  3.1719 +      by simp
  3.1720 +  qed
  3.1721 +  finally have "2 ^ (k - 1) \<le> i" .
  3.1722 +  with wk
  3.1723 +  show False
  3.1724 +    by simp
  3.1725 +qed
  3.1726 +
  3.1727 +lemma pos_length_pos:
  3.1728 +  assumes i0: "0 < bv_to_int w"
  3.1729 +  shows       "0 < length w"
  3.1730 +proof -
  3.1731 +  from norm_signed_result [of w]
  3.1732 +  have "0 < length (norm_signed w)"
  3.1733 +  proof (auto)
  3.1734 +    assume ii: "norm_signed w = []"
  3.1735 +    have "bv_to_int (norm_signed w) = 0"
  3.1736 +      by (subst ii,simp)
  3.1737 +    hence "bv_to_int w = 0"
  3.1738 +      by simp
  3.1739 +    with i0
  3.1740 +    show False
  3.1741 +      by simp
  3.1742 +  next
  3.1743 +    assume ii: "norm_signed w = []"
  3.1744 +    assume jj: "bv_msb w \<noteq> \<zero>"
  3.1745 +    have "\<zero> = bv_msb (norm_signed w)"
  3.1746 +      by (subst ii,simp)
  3.1747 +    also have "... \<noteq> \<zero>"
  3.1748 +      by (simp add: jj)
  3.1749 +    finally show False by simp
  3.1750 +  qed
  3.1751 +  also have "... \<le> length w"
  3.1752 +    by (rule norm_signed_length)
  3.1753 +  finally show ?thesis
  3.1754 +    .
  3.1755 +qed
  3.1756 +
  3.1757 +lemma neg_length_pos:
  3.1758 +  assumes i0: "bv_to_int w < -1"
  3.1759 +  shows       "0 < length w"
  3.1760 +proof -
  3.1761 +  from norm_signed_result [of w]
  3.1762 +  have "0 < length (norm_signed w)"
  3.1763 +  proof (auto)
  3.1764 +    assume ii: "norm_signed w = []"
  3.1765 +    have "bv_to_int (norm_signed w) = 0"
  3.1766 +      by (subst ii,simp)
  3.1767 +    hence "bv_to_int w = 0"
  3.1768 +      by simp
  3.1769 +    with i0
  3.1770 +    show False
  3.1771 +      by simp
  3.1772 +  next
  3.1773 +    assume ii: "norm_signed w = []"
  3.1774 +    assume jj: "bv_msb w \<noteq> \<zero>"
  3.1775 +    have "\<zero> = bv_msb (norm_signed w)"
  3.1776 +      by (subst ii,simp)
  3.1777 +    also have "... \<noteq> \<zero>"
  3.1778 +      by (simp add: jj)
  3.1779 +    finally show False by simp
  3.1780 +  qed
  3.1781 +  also have "... \<le> length w"
  3.1782 +    by (rule norm_signed_length)
  3.1783 +  finally show ?thesis
  3.1784 +    .
  3.1785 +qed
  3.1786 +
  3.1787 +lemma length_int_to_bv_lower_limit_gt0:
  3.1788 +  assumes wk: "2 ^ (k - 1) \<le> i"
  3.1789 +  shows       "k < length (int_to_bv i)"
  3.1790 +proof (rule ccontr)
  3.1791 +  have "0 < (2::int) ^ (k - 1)"
  3.1792 +    by (rule zero_less_zpower,simp)
  3.1793 +  also have "... \<le> i"
  3.1794 +    by (rule wk)
  3.1795 +  finally have i0: "0 < i"
  3.1796 +    .
  3.1797 +  have lii0: "0 < length (int_to_bv i)"
  3.1798 +    apply (rule pos_length_pos)
  3.1799 +    apply (simp,rule i0)
  3.1800 +    done
  3.1801 +  assume "~ k < length (int_to_bv i)"
  3.1802 +  hence "length (int_to_bv i) \<le> k"
  3.1803 +    by simp
  3.1804 +  with lii0
  3.1805 +  have a: "length (int_to_bv i) - 1 \<le> k - 1"
  3.1806 +    by arith
  3.1807 +  have "i < 2 ^ (length (int_to_bv i) - 1)"
  3.1808 +  proof -
  3.1809 +    have "i = bv_to_int (int_to_bv i)"
  3.1810 +      by simp
  3.1811 +    also have "... < 2 ^ (length (int_to_bv i) - 1)"
  3.1812 +      by (rule bv_to_int_upper_range)
  3.1813 +    finally show ?thesis .
  3.1814 +  qed
  3.1815 +  also have "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)"
  3.1816 +    apply (rule le_imp_power_zle,simp)
  3.1817 +    apply (rule a)
  3.1818 +    done
  3.1819 +  finally have "i < 2 ^ (k - 1)" .
  3.1820 +  with wk
  3.1821 +  show False
  3.1822 +    by simp
  3.1823 +qed
  3.1824 +
  3.1825 +lemma length_int_to_bv_upper_limit_lem1:
  3.1826 +  assumes w1: "i < -1"
  3.1827 +  and     wk: "- (2 ^ (k - 1)) \<le> i"
  3.1828 +  shows       "length (int_to_bv i) \<le> k"
  3.1829 +proof (rule ccontr)
  3.1830 +  from w1 wk
  3.1831 +  have k1: "1 < k"
  3.1832 +    by (cases "k - 1",simp_all,arith)
  3.1833 +  assume "~ length (int_to_bv i) \<le> k"
  3.1834 +  hence "k < length (int_to_bv i)"
  3.1835 +    by simp
  3.1836 +  hence "k \<le> length (int_to_bv i) - 1"
  3.1837 +    by arith
  3.1838 +  hence a: "k - 1 \<le> length (int_to_bv i) - 2"
  3.1839 +    by arith
  3.1840 +  have "i < - (2 ^ (length (int_to_bv i) - 2))"
  3.1841 +  proof -
  3.1842 +    have "i = bv_to_int (int_to_bv i)"
  3.1843 +      by simp
  3.1844 +    also have "... < - (2 ^ (length (norm_signed (int_to_bv i)) - 2))"
  3.1845 +      by (rule bv_to_int_upper_limit_lem1,simp,rule w1)
  3.1846 +    finally show ?thesis by simp
  3.1847 +  qed
  3.1848 +  also have "... \<le> -(2 ^ (k - 1))"
  3.1849 +  proof -
  3.1850 +    have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)"
  3.1851 +      apply (rule le_imp_power_zle,simp)
  3.1852 +      apply (rule a)
  3.1853 +      done
  3.1854 +    thus ?thesis
  3.1855 +      by simp
  3.1856 +  qed
  3.1857 +  finally have "i < -(2 ^ (k - 1))" .
  3.1858 +  with wk
  3.1859 +  show False
  3.1860 +    by simp
  3.1861 +qed
  3.1862 +
  3.1863 +lemma length_int_to_bv_lower_limit_lem1:
  3.1864 +  assumes wk: "i < -(2 ^ (k - 1))"
  3.1865 +  shows       "k < length (int_to_bv i)"
  3.1866 +proof (rule ccontr)
  3.1867 +  from wk
  3.1868 +  have "i \<le> -(2 ^ (k - 1)) - 1"
  3.1869 +    by simp
  3.1870 +  also have "... < -1"
  3.1871 +  proof -
  3.1872 +    have "0 < (2::int) ^ (k - 1)"
  3.1873 +      by (rule zero_less_zpower,simp)
  3.1874 +    hence "-((2::int) ^ (k - 1)) < 0"
  3.1875 +      by simp
  3.1876 +    thus ?thesis by simp
  3.1877 +  qed
  3.1878 +  finally have i1: "i < -1" .
  3.1879 +  have lii0: "0 < length (int_to_bv i)"
  3.1880 +    apply (rule neg_length_pos)
  3.1881 +    apply (simp,rule i1)
  3.1882 +    done
  3.1883 +  assume "~ k < length (int_to_bv i)"
  3.1884 +  hence "length (int_to_bv i) \<le> k"
  3.1885 +    by simp
  3.1886 +  with lii0
  3.1887 +  have a: "length (int_to_bv i) - 1 \<le> k - 1"
  3.1888 +    by arith
  3.1889 +  have "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)"
  3.1890 +    apply (rule le_imp_power_zle,simp)
  3.1891 +    apply (rule a)
  3.1892 +    done
  3.1893 +  hence "-((2::int) ^ (k - 1)) \<le> - (2 ^ (length (int_to_bv i) - 1))"
  3.1894 +    by simp
  3.1895 +  also have "... \<le> i"
  3.1896 +  proof -
  3.1897 +    have "- (2 ^ (length (int_to_bv i) - 1)) \<le> bv_to_int (int_to_bv i)"
  3.1898 +      by (rule bv_to_int_lower_range)
  3.1899 +    also have "... = i"
  3.1900 +      by simp
  3.1901 +    finally show ?thesis .
  3.1902 +  qed
  3.1903 +  finally have "-(2 ^ (k - 1)) \<le> i" .
  3.1904 +  with wk
  3.1905 +  show False
  3.1906 +    by simp
  3.1907 +qed
  3.1908 +
  3.1909 +section {* Signed Arithmetic Operations *}
  3.1910 +
  3.1911 +subsection {* Conversion from unsigned to signed *}
  3.1912 +
  3.1913 +constdefs
  3.1914 +  utos :: "bit list => bit list"
  3.1915 +  "utos w == norm_signed (\<zero> # w)"
  3.1916 +
  3.1917 +lemma [simp]: "utos (norm_unsigned w) = utos w"
  3.1918 +  by (simp add: utos_def norm_signed_Cons)
  3.1919 +
  3.1920 +lemma [simp]: "norm_signed (utos w) = utos w"
  3.1921 +  by (simp add: utos_def)
  3.1922 +
  3.1923 +lemma utos_length: "length (utos w) \<le> Suc (length w)"
  3.1924 +  by (simp add: utos_def norm_signed_Cons)
  3.1925 +
  3.1926 +lemma bv_to_int_utos: "bv_to_int (utos w) = bv_to_nat w"
  3.1927 +proof (simp add: utos_def norm_signed_Cons,safe)
  3.1928 +  assume "norm_unsigned w = []"
  3.1929 +  hence "bv_to_nat (norm_unsigned w) = 0"
  3.1930 +    by simp
  3.1931 +  thus "bv_to_nat w = 0"
  3.1932 +    by simp
  3.1933 +qed
  3.1934 +
  3.1935 +subsection {* Unary minus *}
  3.1936 +
  3.1937 +constdefs
  3.1938 +  bv_uminus :: "bit list => bit list"
  3.1939 +  "bv_uminus w == int_to_bv (- bv_to_int w)"
  3.1940 +
  3.1941 +lemma [simp]: "bv_uminus (norm_signed w) = bv_uminus w"
  3.1942 +  by (simp add: bv_uminus_def)
  3.1943 +
  3.1944 +lemma [simp]: "norm_signed (bv_uminus w) = bv_uminus w"
  3.1945 +  by (simp add: bv_uminus_def)
  3.1946 +
  3.1947 +lemma bv_uminus_length: "length (bv_uminus w) \<le> Suc (length w)"
  3.1948 +proof -
  3.1949 +  have "1 < -bv_to_int w \<or> -bv_to_int w = 1 \<or> -bv_to_int w = 0 \<or> -bv_to_int w = -1 \<or> -bv_to_int w < -1"
  3.1950 +    by arith
  3.1951 +  thus ?thesis
  3.1952 +  proof safe
  3.1953 +    assume p: "1 < - bv_to_int w"
  3.1954 +    have lw: "0 < length w"
  3.1955 +      apply (rule neg_length_pos)
  3.1956 +      using p
  3.1957 +      apply simp
  3.1958 +      done
  3.1959 +    show ?thesis
  3.1960 +    proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all)
  3.1961 +      from prems
  3.1962 +      show "bv_to_int w < 0"
  3.1963 +	by simp
  3.1964 +    next
  3.1965 +      have "-(2^(length w - 1)) \<le> bv_to_int w"
  3.1966 +	by (rule bv_to_int_lower_range)
  3.1967 +      hence "- bv_to_int w \<le> 2^(length w - 1)"
  3.1968 +	by simp
  3.1969 +      also from lw have "... < 2 ^ length w"
  3.1970 +	by simp
  3.1971 +      finally show "- bv_to_int w < 2 ^ length w"
  3.1972 +	by simp
  3.1973 +    qed
  3.1974 +  next
  3.1975 +    assume p: "- bv_to_int w = 1"
  3.1976 +    hence lw: "0 < length w"
  3.1977 +      by (cases w,simp_all)
  3.1978 +    from p
  3.1979 +    show ?thesis
  3.1980 +      apply (simp add: bv_uminus_def)
  3.1981 +      using lw
  3.1982 +      apply (simp (no_asm) add: nat_to_bv_non0)
  3.1983 +      done
  3.1984 +  next
  3.1985 +    assume "- bv_to_int w = 0"
  3.1986 +    thus ?thesis
  3.1987 +      by (simp add: bv_uminus_def)
  3.1988 +  next
  3.1989 +    assume p: "- bv_to_int w = -1"
  3.1990 +    thus ?thesis
  3.1991 +      by (simp add: bv_uminus_def)
  3.1992 +  next
  3.1993 +    assume p: "- bv_to_int w < -1"
  3.1994 +    show ?thesis
  3.1995 +      apply (simp add: bv_uminus_def)
  3.1996 +      apply (rule length_int_to_bv_upper_limit_lem1)
  3.1997 +      apply (rule p)
  3.1998 +      apply simp
  3.1999 +    proof -
  3.2000 +      have "bv_to_int w < 2 ^ (length w - 1)"
  3.2001 +	by (rule bv_to_int_upper_range)
  3.2002 +      also have "... \<le> 2 ^ length w"
  3.2003 +	by (rule le_imp_power_zle,simp_all)
  3.2004 +      finally show "bv_to_int w \<le> 2 ^ length w"
  3.2005 +	by simp
  3.2006 +    qed
  3.2007 +  qed
  3.2008 +qed
  3.2009 +
  3.2010 +lemma bv_uminus_length_utos: "length (bv_uminus (utos w)) \<le> Suc (length w)"
  3.2011 +proof -
  3.2012 +  have "-bv_to_int (utos w) = 0 \<or> -bv_to_int (utos w) = -1 \<or> -bv_to_int (utos w) < -1"
  3.2013 +    apply (simp add: bv_to_int_utos)
  3.2014 +    apply (cut_tac bv_to_nat_lower_range [of w])
  3.2015 +    by arith
  3.2016 +  thus ?thesis
  3.2017 +  proof safe
  3.2018 +    assume "-bv_to_int (utos w) = 0"
  3.2019 +    thus ?thesis
  3.2020 +      by (simp add: bv_uminus_def)
  3.2021 +  next
  3.2022 +    assume "-bv_to_int (utos w) = -1"
  3.2023 +    thus ?thesis
  3.2024 +      by (simp add: bv_uminus_def)
  3.2025 +  next
  3.2026 +    assume p: "-bv_to_int (utos w) < -1"
  3.2027 +    show ?thesis
  3.2028 +      apply (simp add: bv_uminus_def)
  3.2029 +      apply (rule length_int_to_bv_upper_limit_lem1)
  3.2030 +      apply (rule p)
  3.2031 +      apply (simp add: bv_to_int_utos)
  3.2032 +      using bv_to_nat_upper_range [of w]
  3.2033 +      apply simp
  3.2034 +      done
  3.2035 +  qed
  3.2036 +qed
  3.2037 +
  3.2038 +constdefs
  3.2039 +  bv_sadd :: "[bit list, bit list ] => bit list"
  3.2040 +  "bv_sadd w1 w2 == int_to_bv (bv_to_int w1 + bv_to_int w2)"
  3.2041 +
  3.2042 +lemma [simp]: "bv_sadd (norm_signed w1) w2 = bv_sadd w1 w2"
  3.2043 +  by (simp add: bv_sadd_def)
  3.2044 +
  3.2045 +lemma [simp]: "bv_sadd w1 (norm_signed w2) = bv_sadd w1 w2"
  3.2046 +  by (simp add: bv_sadd_def)
  3.2047 +
  3.2048 +lemma [simp]: "norm_signed (bv_sadd w1 w2) = bv_sadd w1 w2"
  3.2049 +  by (simp add: bv_sadd_def)
  3.2050 +
  3.2051 +lemma adder_helper:
  3.2052 +  assumes lw: "0 < max (length w1) (length w2)"
  3.2053 +  shows   "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le> 2 ^ max (length w1) (length w2)"
  3.2054 +proof -
  3.2055 +  have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le> 2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)"
  3.2056 +    apply (cases "length w1 \<le> length w2")
  3.2057 +    apply (auto simp add: max_def)
  3.2058 +    apply arith
  3.2059 +    apply arith
  3.2060 +    done
  3.2061 +  also have "... = 2 ^ max (length w1) (length w2)"
  3.2062 +  proof -
  3.2063 +    from lw
  3.2064 +    show ?thesis
  3.2065 +      apply simp
  3.2066 +      apply (subst power_Suc [symmetric])
  3.2067 +      apply (simp del: power.simps)
  3.2068 +      done
  3.2069 +  qed
  3.2070 +  finally show ?thesis .
  3.2071 +qed
  3.2072 +
  3.2073 +lemma bv_sadd_length: "length (bv_sadd w1 w2) \<le> Suc (max (length w1) (length w2))"
  3.2074 +proof -
  3.2075 +  let ?Q = "bv_to_int w1 + bv_to_int w2"
  3.2076 +
  3.2077 +  have helper: "?Q \<noteq> 0 ==> 0 < max (length w1) (length w2)"
  3.2078 +  proof -
  3.2079 +    assume p: "?Q \<noteq> 0"
  3.2080 +    show "0 < max (length w1) (length w2)"
  3.2081 +    proof (simp add: less_max_iff_disj,rule)
  3.2082 +      assume [simp]: "w1 = []"
  3.2083 +      show "w2 \<noteq> []"
  3.2084 +      proof (rule ccontr,simp)
  3.2085 +	assume [simp]: "w2 = []"
  3.2086 +	from p
  3.2087 +	show False
  3.2088 +	  by simp
  3.2089 +      qed
  3.2090 +    qed
  3.2091 +  qed
  3.2092 +
  3.2093 +  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1"
  3.2094 +    by arith
  3.2095 +  thus ?thesis
  3.2096 +  proof safe
  3.2097 +    assume "?Q = 0"
  3.2098 +    thus ?thesis
  3.2099 +      by (simp add: bv_sadd_def)
  3.2100 +  next
  3.2101 +    assume "?Q = -1"
  3.2102 +    thus ?thesis
  3.2103 +      by (simp add: bv_sadd_def)
  3.2104 +  next
  3.2105 +    assume p: "0 < ?Q"
  3.2106 +    show ?thesis
  3.2107 +      apply (simp add: bv_sadd_def)
  3.2108 +      apply (rule length_int_to_bv_upper_limit_gt0)
  3.2109 +      apply (rule p)
  3.2110 +    proof simp
  3.2111 +      from bv_to_int_upper_range [of w2]
  3.2112 +      have "bv_to_int w2 \<le> 2 ^ (length w2 - 1)"
  3.2113 +	by simp
  3.2114 +      with bv_to_int_upper_range [of w1]
  3.2115 +      have "bv_to_int w1 + bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
  3.2116 +	by (rule zadd_zless_mono)
  3.2117 +      also have "... \<le> 2 ^ max (length w1) (length w2)"
  3.2118 +	apply (rule adder_helper)
  3.2119 +	apply (rule helper)
  3.2120 +	using p
  3.2121 +	apply simp
  3.2122 +	done
  3.2123 +      finally show "?Q < 2 ^ max (length w1) (length w2)"
  3.2124 +	.
  3.2125 +    qed
  3.2126 +  next
  3.2127 +    assume p: "?Q < -1"
  3.2128 +    show ?thesis
  3.2129 +      apply (simp add: bv_sadd_def)
  3.2130 +      apply (rule length_int_to_bv_upper_limit_lem1,simp_all)
  3.2131 +      apply (rule p)
  3.2132 +    proof -
  3.2133 +      have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)"
  3.2134 +	apply (rule adder_helper)
  3.2135 +	apply (rule helper)
  3.2136 +	using p
  3.2137 +	apply simp
  3.2138 +	done
  3.2139 +      hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
  3.2140 +	by simp
  3.2141 +      also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> ?Q"
  3.2142 +	apply (rule add_mono)
  3.2143 +	apply (rule bv_to_int_lower_range [of w1])
  3.2144 +	apply (rule bv_to_int_lower_range [of w2])
  3.2145 +	done
  3.2146 +      finally show "- (2^max (length w1) (length w2)) \<le> ?Q" .
  3.2147 +    qed
  3.2148 +  qed
  3.2149 +qed
  3.2150 +
  3.2151 +constdefs
  3.2152 +  bv_sub :: "[bit list, bit list] => bit list"
  3.2153 +  "bv_sub w1 w2 == bv_sadd w1 (bv_uminus w2)"
  3.2154 +
  3.2155 +lemma [simp]: "bv_sub (norm_signed w1) w2 = bv_sub w1 w2"
  3.2156 +  by (simp add: bv_sub_def)
  3.2157 +
  3.2158 +lemma [simp]: "bv_sub w1 (norm_signed w2) = bv_sub w1 w2"
  3.2159 +  by (simp add: bv_sub_def)
  3.2160 +
  3.2161 +lemma [simp]: "norm_signed (bv_sub w1 w2) = bv_sub w1 w2"
  3.2162 +  by (simp add: bv_sub_def)
  3.2163 +
  3.2164 +lemma bv_sub_length: "length (bv_sub w1 w2) \<le> Suc (max (length w1) (length w2))"
  3.2165 +proof (cases "bv_to_int w2 = 0")
  3.2166 +  assume p: "bv_to_int w2 = 0"
  3.2167 +  show ?thesis
  3.2168 +  proof (simp add: bv_sub_def bv_sadd_def bv_uminus_def p)
  3.2169 +    have "length (norm_signed w1) \<le> length w1"
  3.2170 +      by (rule norm_signed_length)
  3.2171 +    also have "... \<le> max (length w1) (length w2)"
  3.2172 +      by (rule le_maxI1)
  3.2173 +    also have "... \<le> Suc (max (length w1) (length w2))"
  3.2174 +      by arith
  3.2175 +    finally show "length (norm_signed w1) \<le> Suc (max (length w1) (length w2))"
  3.2176 +      .
  3.2177 +  qed
  3.2178 +next
  3.2179 +  assume "bv_to_int w2 \<noteq> 0"
  3.2180 +  hence "0 < length w2"
  3.2181 +    by (cases w2,simp_all)
  3.2182 +  hence lmw: "0 < max (length w1) (length w2)"
  3.2183 +    by arith
  3.2184 +
  3.2185 +  let ?Q = "bv_to_int w1 - bv_to_int w2"
  3.2186 +
  3.2187 +  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1"
  3.2188 +    by arith
  3.2189 +  thus ?thesis
  3.2190 +  proof safe
  3.2191 +    assume "?Q = 0"
  3.2192 +    thus ?thesis
  3.2193 +      by (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
  3.2194 +  next
  3.2195 +    assume "?Q = -1"
  3.2196 +    thus ?thesis
  3.2197 +      by (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
  3.2198 +  next
  3.2199 +    assume p: "0 < ?Q"
  3.2200 +    show ?thesis
  3.2201 +      apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
  3.2202 +      apply (rule length_int_to_bv_upper_limit_gt0)
  3.2203 +      apply (rule p)
  3.2204 +    proof simp
  3.2205 +      from bv_to_int_lower_range [of w2]
  3.2206 +      have v2: "- bv_to_int w2 \<le> 2 ^ (length w2 - 1)"
  3.2207 +	by simp
  3.2208 +      have "bv_to_int w1 + - bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
  3.2209 +	apply (rule zadd_zless_mono)
  3.2210 +	apply (rule bv_to_int_upper_range [of w1])
  3.2211 +	apply (rule v2)
  3.2212 +	done
  3.2213 +      also have "... \<le> 2 ^ max (length w1) (length w2)"
  3.2214 +	apply (rule adder_helper)
  3.2215 +	apply (rule lmw)
  3.2216 +	done
  3.2217 +      finally show "?Q < 2 ^ max (length w1) (length w2)"
  3.2218 +	by simp
  3.2219 +    qed
  3.2220 +  next
  3.2221 +    assume p: "?Q < -1"
  3.2222 +    show ?thesis
  3.2223 +      apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
  3.2224 +      apply (rule length_int_to_bv_upper_limit_lem1)
  3.2225 +      apply (rule p)
  3.2226 +    proof simp
  3.2227 +      have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)"
  3.2228 +	apply (rule adder_helper)
  3.2229 +	apply (rule lmw)
  3.2230 +	done
  3.2231 +      hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
  3.2232 +	by simp
  3.2233 +      also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> bv_to_int w1 + -bv_to_int w2"
  3.2234 +	apply (rule add_mono)
  3.2235 +	apply (rule bv_to_int_lower_range [of w1])
  3.2236 +	using bv_to_int_upper_range [of w2]
  3.2237 +	apply simp
  3.2238 +	done
  3.2239 +      finally show "- (2^max (length w1) (length w2)) \<le> ?Q"
  3.2240 +	by simp
  3.2241 +    qed
  3.2242 +  qed
  3.2243 +qed
  3.2244 +
  3.2245 +constdefs
  3.2246 +  bv_smult :: "[bit list, bit list] => bit list"
  3.2247 +  "bv_smult w1 w2 == int_to_bv (bv_to_int w1 * bv_to_int w2)"
  3.2248 +
  3.2249 +lemma [simp]: "bv_smult (norm_signed w1) w2 = bv_smult w1 w2"
  3.2250 +  by (simp add: bv_smult_def)
  3.2251 +
  3.2252 +lemma [simp]: "bv_smult w1 (norm_signed w2) = bv_smult w1 w2"
  3.2253 +  by (simp add: bv_smult_def)
  3.2254 +
  3.2255 +lemma [simp]: "norm_signed (bv_smult w1 w2) = bv_smult w1 w2"
  3.2256 +  by (simp add: bv_smult_def)
  3.2257 +
  3.2258 +lemma bv_smult_length: "length (bv_smult w1 w2) \<le> length w1 + length w2"
  3.2259 +proof -
  3.2260 +  let ?Q = "bv_to_int w1 * bv_to_int w2"
  3.2261 +
  3.2262 +  have lmw: "?Q \<noteq> 0 ==> 0 < length w1 \<and> 0 < length w2"
  3.2263 +    by auto
  3.2264 +
  3.2265 +  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1"
  3.2266 +    by arith
  3.2267 +  thus ?thesis
  3.2268 +  proof (safe dest!: iffD1 [OF mult_eq_0_iff])
  3.2269 +    assume "bv_to_int w1 = 0"
  3.2270 +    thus ?thesis
  3.2271 +      by (simp add: bv_smult_def)
  3.2272 +  next
  3.2273 +    assume "bv_to_int w2 = 0"
  3.2274 +    thus ?thesis
  3.2275 +      by (simp add: bv_smult_def)
  3.2276 +  next
  3.2277 +    assume p: "?Q = -1"
  3.2278 +    show ?thesis
  3.2279 +      apply (simp add: bv_smult_def p)
  3.2280 +      apply (cut_tac lmw)
  3.2281 +      apply arith
  3.2282 +      using p
  3.2283 +      apply simp
  3.2284 +      done
  3.2285 +  next
  3.2286 +    assume p: "0 < ?Q"
  3.2287 +    thus ?thesis
  3.2288 +    proof (simp add: zero_less_mult_iff,safe)
  3.2289 +      assume bi1: "0 < bv_to_int w1"
  3.2290 +      assume bi2: "0 < bv_to_int w2"
  3.2291 +      show ?thesis
  3.2292 +	apply (simp add: bv_smult_def)
  3.2293 +	apply (rule length_int_to_bv_upper_limit_gt0)
  3.2294 +	apply (rule p)
  3.2295 +      proof simp
  3.2296 +	have "?Q < 2 ^ (length w1 - 1) * 2 ^ (length w2 - 1)"
  3.2297 +	  apply (rule mult_strict_mono)
  3.2298 +	  apply (rule bv_to_int_upper_range)
  3.2299 +	  apply (rule bv_to_int_upper_range)
  3.2300 +	  apply (rule zero_less_zpower)
  3.2301 +	  apply simp
  3.2302 +	  using bi2
  3.2303 +	  apply simp
  3.2304 +	  done
  3.2305 +	also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
  3.2306 +	  apply simp
  3.2307 +	  apply (subst zpower_zadd_distrib [symmetric])
  3.2308 +	  apply simp
  3.2309 +	  apply arith
  3.2310 +	  done
  3.2311 +	finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
  3.2312 +	  .
  3.2313 +      qed
  3.2314 +    next
  3.2315 +      assume bi1: "bv_to_int w1 < 0"
  3.2316 +      assume bi2: "bv_to_int w2 < 0"
  3.2317 +      show ?thesis
  3.2318 +	apply (simp add: bv_smult_def)
  3.2319 +	apply (rule length_int_to_bv_upper_limit_gt0)
  3.2320 +	apply (rule p)
  3.2321 +      proof simp
  3.2322 +	have "-bv_to_int w1 * -bv_to_int w2 \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
  3.2323 +	  apply (rule mult_mono)
  3.2324 +	  using bv_to_int_lower_range [of w1]
  3.2325 +	  apply simp
  3.2326 +	  using bv_to_int_lower_range [of w2]
  3.2327 +	  apply simp
  3.2328 +	  apply (rule zero_le_zpower,simp)
  3.2329 +	  using bi2
  3.2330 +	  apply simp
  3.2331 +	  done
  3.2332 +	hence "?Q \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
  3.2333 +	  by simp
  3.2334 +	also have "... < 2 ^ (length w1 + length w2 - Suc 0)"
  3.2335 +	  apply simp
  3.2336 +	  apply (subst zpower_zadd_distrib [symmetric])
  3.2337 +	  apply simp
  3.2338 +	  apply (cut_tac lmw)
  3.2339 +	  apply arith
  3.2340 +	  apply (cut_tac p)
  3.2341 +	  apply arith
  3.2342 +	  done
  3.2343 +	finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
  3.2344 +      qed
  3.2345 +    qed
  3.2346 +  next
  3.2347 +    assume p: "?Q < -1"
  3.2348 +    show ?thesis
  3.2349 +      apply (subst bv_smult_def)
  3.2350 +      apply (rule length_int_to_bv_upper_limit_lem1)
  3.2351 +      apply (rule p)
  3.2352 +    proof simp
  3.2353 +      have "(2::int) ^ (length w1 - 1) * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
  3.2354 +	apply simp
  3.2355 +	apply (subst zpower_zadd_distrib [symmetric])
  3.2356 +	apply simp
  3.2357 +	apply (cut_tac lmw)
  3.2358 +	apply arith
  3.2359 +	apply (cut_tac p)
  3.2360 +	apply arith
  3.2361 +	done
  3.2362 +      hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^(length w1 - 1) * 2 ^ (length w2 - 1))"
  3.2363 +	by simp
  3.2364 +      also have "... \<le> ?Q"
  3.2365 +      proof -
  3.2366 +	from p
  3.2367 +	have q: "bv_to_int w1 * bv_to_int w2 < 0"
  3.2368 +	  by simp
  3.2369 +	thus ?thesis
  3.2370 +	proof (simp add: mult_less_0_iff,safe)
  3.2371 +	  assume bi1: "0 < bv_to_int w1"
  3.2372 +	  assume bi2: "bv_to_int w2 < 0"
  3.2373 +	  have "-bv_to_int w2 * bv_to_int w1 \<le> ((2::int)^(length w2 - 1)) * (2 ^ (length w1 - 1))"
  3.2374 +	    apply (rule mult_mono)
  3.2375 +	    using bv_to_int_lower_range [of w2]
  3.2376 +	    apply simp
  3.2377 +	    using bv_to_int_upper_range [of w1]
  3.2378 +	    apply simp
  3.2379 +	    apply (rule zero_le_zpower,simp)
  3.2380 +	    using bi1
  3.2381 +	    apply simp
  3.2382 +	    done
  3.2383 +	  hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
  3.2384 +	    by (simp add: zmult_ac)
  3.2385 +	  thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
  3.2386 +	    by simp
  3.2387 +	next
  3.2388 +	  assume bi1: "bv_to_int w1 < 0"
  3.2389 +	  assume bi2: "0 < bv_to_int w2"
  3.2390 +	  have "-bv_to_int w1 * bv_to_int w2 \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
  3.2391 +	    apply (rule mult_mono)
  3.2392 +	    using bv_to_int_lower_range [of w1]
  3.2393 +	    apply simp
  3.2394 +	    using bv_to_int_upper_range [of w2]
  3.2395 +	    apply simp
  3.2396 +	    apply (rule zero_le_zpower,simp)
  3.2397 +	    using bi2
  3.2398 +	    apply simp
  3.2399 +	    done
  3.2400 +	  hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
  3.2401 +	    by (simp add: zmult_ac)
  3.2402 +	  thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
  3.2403 +	    by simp
  3.2404 +	qed
  3.2405 +      qed
  3.2406 +      finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q"
  3.2407 +	.
  3.2408 +    qed
  3.2409 +  qed
  3.2410 +qed
  3.2411 +
  3.2412 +lemma bv_msb_one: "bv_msb w = \<one> ==> 0 < bv_to_nat w"
  3.2413 +  apply (cases w,simp_all)
  3.2414 +  apply (subgoal_tac "0 + 0 < 2 ^ length list + bv_to_nat list")
  3.2415 +  apply simp
  3.2416 +  apply (rule add_less_le_mono)
  3.2417 +  apply (rule zero_less_zpower)
  3.2418 +  apply simp_all
  3.2419 +  done
  3.2420 +
  3.2421 +lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \<le> length w1 + length w2"
  3.2422 +proof -
  3.2423 +  let ?Q = "bv_to_int (utos w1) * bv_to_int w2"
  3.2424 +
  3.2425 +  have lmw: "?Q \<noteq> 0 ==> 0 < length (utos w1) \<and> 0 < length w2"
  3.2426 +    by auto
  3.2427 +
  3.2428 +  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1"
  3.2429 +    by arith
  3.2430 +  thus ?thesis
  3.2431 +  proof (safe dest!: iffD1 [OF mult_eq_0_iff])
  3.2432 +    assume "bv_to_int (utos w1) = 0"
  3.2433 +    thus ?thesis
  3.2434 +      by (simp add: bv_smult_def)
  3.2435 +  next
  3.2436 +    assume "bv_to_int w2 = 0"
  3.2437 +    thus ?thesis
  3.2438 +      by (simp add: bv_smult_def)
  3.2439 +  next
  3.2440 +    assume p: "0 < ?Q"
  3.2441 +    thus ?thesis
  3.2442 +    proof (simp add: zero_less_mult_iff,safe)
  3.2443 +      assume biw2: "0 < bv_to_int w2"
  3.2444 +      show ?thesis
  3.2445 +	apply (simp add: bv_smult_def)
  3.2446 +	apply (rule length_int_to_bv_upper_limit_gt0)
  3.2447 +	apply (rule p)
  3.2448 +      proof simp
  3.2449 +	have "?Q < 2 ^ length w1 * 2 ^ (length w2 - 1)"
  3.2450 +	  apply (rule mult_strict_mono)
  3.2451 +	  apply (simp add: bv_to_int_utos)
  3.2452 +	  apply (rule bv_to_nat_upper_range)
  3.2453 +	  apply (rule bv_to_int_upper_range)
  3.2454 +	  apply (rule zero_less_zpower,simp)
  3.2455 +	  using biw2
  3.2456 +	  apply simp
  3.2457 +	  done
  3.2458 +	also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
  3.2459 + 	  apply simp
  3.2460 +	  apply (subst zpower_zadd_distrib [symmetric])
  3.2461 +	  apply simp
  3.2462 +	  apply (cut_tac lmw)
  3.2463 +	  apply arith
  3.2464 +	  using p
  3.2465 +	  apply auto
  3.2466 +	  done
  3.2467 +	finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
  3.2468 +	  .
  3.2469 +      qed
  3.2470 +    next
  3.2471 +      assume "bv_to_int (utos w1) < 0"
  3.2472 +      thus ?thesis
  3.2473 +	apply (simp add: bv_to_int_utos)
  3.2474 +	using bv_to_nat_lower_range [of w1]
  3.2475 +	apply simp
  3.2476 +	done
  3.2477 +    qed
  3.2478 +  next
  3.2479 +    assume p: "?Q = -1"
  3.2480 +    thus ?thesis
  3.2481 +      apply (simp add: bv_smult_def)
  3.2482 +      apply (cut_tac lmw)
  3.2483 +      apply arith
  3.2484 +      apply simp
  3.2485 +      done
  3.2486 +  next
  3.2487 +    assume p: "?Q < -1"
  3.2488 +    show ?thesis
  3.2489 +      apply (subst bv_smult_def)
  3.2490 +      apply (rule length_int_to_bv_upper_limit_lem1)
  3.2491 +      apply (rule p)
  3.2492 +    proof simp
  3.2493 +      have "(2::int) ^ length w1 * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
  3.2494 +	apply simp
  3.2495 +	apply (subst zpower_zadd_distrib [symmetric])
  3.2496 +	apply simp
  3.2497 +	apply (cut_tac lmw)
  3.2498 +	apply arith
  3.2499 +	apply (cut_tac p)
  3.2500 +	apply arith
  3.2501 +	done
  3.2502 +      hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^ length w1 * 2 ^ (length w2 - 1))"
  3.2503 +	by simp
  3.2504 +      also have "... \<le> ?Q"
  3.2505 +      proof -
  3.2506 +	from p
  3.2507 +	have q: "bv_to_int (utos w1) * bv_to_int w2 < 0"
  3.2508 +	  by simp
  3.2509 +	thus ?thesis
  3.2510 +	proof (simp add: mult_less_0_iff,safe)
  3.2511 +	  assume bi1: "0 < bv_to_int (utos w1)"
  3.2512 +	  assume bi2: "bv_to_int w2 < 0"
  3.2513 +	  have "-bv_to_int w2 * bv_to_int (utos w1) \<le> ((2::int)^(length w2 - 1)) * (2 ^ length w1)"
  3.2514 +	    apply (rule mult_mono)
  3.2515 +	    using bv_to_int_lower_range [of w2]
  3.2516 +	    apply simp
  3.2517 +	    apply (simp add: bv_to_int_utos)
  3.2518 +	    using bv_to_nat_upper_range [of w1]
  3.2519 +	    apply simp
  3.2520 +	    apply (rule zero_le_zpower,simp)
  3.2521 +	    using bi1
  3.2522 +	    apply simp
  3.2523 +	    done
  3.2524 +	  hence "-?Q \<le> ((2::int)^length w1) * (2 ^ (length w2 - 1))"
  3.2525 +	    by (simp add: zmult_ac)
  3.2526 +	  thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
  3.2527 +	    by simp
  3.2528 +	next
  3.2529 +	  assume bi1: "bv_to_int (utos w1) < 0"
  3.2530 +	  thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
  3.2531 +	    apply (simp add: bv_to_int_utos)
  3.2532 +	    using bv_to_nat_lower_range [of w1]
  3.2533 +	    apply simp
  3.2534 +	    done
  3.2535 +	qed
  3.2536 +      qed
  3.2537 +      finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q"
  3.2538 +	.
  3.2539 +    qed
  3.2540 +  qed
  3.2541 +qed
  3.2542 +
  3.2543 +lemma bv_smult_sym: "bv_smult w1 w2 = bv_smult w2 w1"
  3.2544 +  by (simp add: bv_smult_def zmult_ac)
  3.2545 +
  3.2546 +section {* Structural operations *}
  3.2547 +
  3.2548 +constdefs
  3.2549 +  bv_select :: "[bit list,nat] => bit"
  3.2550 +  "bv_select w i == w ! (length w - 1 - i)"
  3.2551 +  bv_chop :: "[bit list,nat] => bit list * bit list"
  3.2552 +  "bv_chop w i == let len = length w in (take (len - i) w,drop (len - i) w)"
  3.2553 +  bv_slice :: "[bit list,nat*nat] => bit list"
  3.2554 +  "bv_slice w == \<lambda>(b,e). fst (bv_chop (snd (bv_chop w (b+1))) e)"
  3.2555 +
  3.2556 +lemma bv_select_rev:
  3.2557 +  assumes notnull: "n < length w"
  3.2558 +  shows            "bv_select w n = rev w ! n"
  3.2559 +proof -
  3.2560 +  have "\<forall>n. n < length w --> bv_select w n = rev w ! n"
  3.2561 +  proof (rule length_induct [of _ w],auto simp add: bv_select_def)
  3.2562 +    fix xs :: "bit list"
  3.2563 +    fix n
  3.2564 +    assume ind: "\<forall>ys::bit list. length ys < length xs --> (\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n)"
  3.2565 +    assume notx: "n < length xs"
  3.2566 +    show "xs ! (length xs - Suc n) = rev xs ! n"
  3.2567 +    proof (cases xs)
  3.2568 +      assume "xs = []"
  3.2569 +      with notx
  3.2570 +      show ?thesis
  3.2571 +	by simp
  3.2572 +    next
  3.2573 +      fix y ys
  3.2574 +      assume [simp]: "xs = y # ys"
  3.2575 +      show ?thesis
  3.2576 +      proof (auto simp add: nth_append)
  3.2577 +	assume noty: "n < length ys"
  3.2578 +	from spec [OF ind,of ys]
  3.2579 +	have "\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
  3.2580 +	  by simp
  3.2581 +	hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
  3.2582 +	  ..
  3.2583 +	hence "ys ! (length ys - Suc n) = rev ys ! n"
  3.2584 +	  ..
  3.2585 +	thus "(y # ys) ! (length ys - n) = rev ys ! n"
  3.2586 +	  by (simp add: nth_Cons' noty not_less_iff_le [symmetric])
  3.2587 +      next
  3.2588 +	assume "~ n < length ys"
  3.2589 +	hence x: "length ys \<le> n"
  3.2590 +	  by simp
  3.2591 +	from notx
  3.2592 +	have "n < Suc (length ys)"
  3.2593 +	  by simp
  3.2594 +	hence "n \<le> length ys"
  3.2595 +	  by simp
  3.2596 +	with x
  3.2597 +	have "length ys = n"
  3.2598 +	  by simp
  3.2599 +	thus "y = [y] ! (n - length ys)"
  3.2600 +	  by simp
  3.2601 +      qed
  3.2602 +    qed
  3.2603 +  qed
  3.2604 +  hence "n < length w --> bv_select w n = rev w ! n"
  3.2605 +    ..
  3.2606 +  thus ?thesis
  3.2607 +    ..
  3.2608 +qed
  3.2609 +
  3.2610 +lemma bv_chop_append: "bv_chop (w1 @ w2) (length w2) = (w1,w2)"
  3.2611 +  by (simp add: bv_chop_def Let_def)
  3.2612 +
  3.2613 +lemma append_bv_chop_id: "fst (bv_chop w l) @ snd (bv_chop w l) = w"
  3.2614 +  by (simp add: bv_chop_def Let_def)
  3.2615 +
  3.2616 +lemma bv_chop_length_fst [simp]: "length (fst (bv_chop w i)) = length w - i"
  3.2617 +  by (simp add: bv_chop_def Let_def,arith)
  3.2618 +
  3.2619 +lemma bv_chop_length_snd [simp]: "length (snd (bv_chop w i)) = min i (length w)"
  3.2620 +  by (simp add: bv_chop_def Let_def,arith)
  3.2621 +
  3.2622 +lemma bv_slice_length [simp]: "[| j \<le> i; i < length w |] ==> length (bv_slice w (i,j)) = i - j + 1"
  3.2623 +  by (auto simp add: bv_slice_def,arith)
  3.2624 +
  3.2625 +constdefs
  3.2626 +  length_nat :: "int => nat"
  3.2627 +  "length_nat x == LEAST n. x < 2 ^ n"
  3.2628 +
  3.2629 +lemma length_nat: "length (nat_to_bv n) = length_nat n"
  3.2630 +  apply (simp add: length_nat_def)
  3.2631 +  apply (rule Least_equality [symmetric])
  3.2632 +  prefer 2
  3.2633 +  apply (rule length_nat_to_bv_upper_limit)
  3.2634 +  apply arith
  3.2635 +  apply (rule ccontr)
  3.2636 +proof -
  3.2637 +  assume "~ n < 2 ^ length (nat_to_bv n)"
  3.2638 +  hence "2 ^ length (nat_to_bv n) \<le> n"
  3.2639 +    by simp
  3.2640 +  hence "length (nat_to_bv n) < length (nat_to_bv n)"
  3.2641 +    by (rule length_nat_to_bv_lower_limit)
  3.2642 +  thus False
  3.2643 +    by simp
  3.2644 +qed
  3.2645 +
  3.2646 +lemma length_nat_0 [simp]: "length_nat 0 = 0"
  3.2647 +  by (simp add: length_nat_def Least_equality)
  3.2648 +
  3.2649 +lemma length_nat_non0:
  3.2650 +  assumes n0: "0 < n"
  3.2651 +  shows       "length_nat n = Suc (length_nat (n div 2))"
  3.2652 +  apply (simp add: length_nat [symmetric])
  3.2653 +  apply (subst nat_to_bv_non0 [of n])
  3.2654 +  apply (simp_all add: n0)
  3.2655 +  done
  3.2656 +
  3.2657 +constdefs
  3.2658 +  length_int :: "int => nat"
  3.2659 +  "length_int x == if 0 < x then Suc (length_nat x) else if x = 0 then 0 else Suc (length_nat (-x - 1))"
  3.2660 +
  3.2661 +lemma length_int: "length (int_to_bv i) = length_int i"
  3.2662 +proof (cases "0 < i")
  3.2663 +  assume i0: "0 < i"
  3.2664 +  hence "length (int_to_bv i) = length (norm_signed (\<zero> # norm_unsigned (nat_to_bv i)))"
  3.2665 +    by simp
  3.2666 +  also from norm_unsigned_result [of "nat_to_bv i"]
  3.2667 +  have "... = Suc (length_nat i)"
  3.2668 +    apply safe
  3.2669 +    apply simp
  3.2670 +    apply (drule norm_empty_bv_to_nat_zero)
  3.2671 +    using prems
  3.2672 +    apply simp
  3.2673 +    apply (cases "norm_unsigned (nat_to_bv i)")
  3.2674 +    apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv i"])
  3.2675 +    using prems
  3.2676 +    apply simp
  3.2677 +    apply simp
  3.2678 +    using prems
  3.2679 +    apply (simp add: length_nat [symmetric])
  3.2680 +    done
  3.2681 +  finally show ?thesis
  3.2682 +    using i0
  3.2683 +    by (simp add: length_int_def)
  3.2684 +next
  3.2685 +  assume "~ 0 < i"
  3.2686 +  hence i0: "i \<le> 0"
  3.2687 +    by simp
  3.2688 +  show ?thesis
  3.2689 +  proof (cases "i = 0")
  3.2690 +    assume "i = 0"
  3.2691 +    thus ?thesis
  3.2692 +      by (simp add: length_int_def)
  3.2693 +  next
  3.2694 +    assume "i \<noteq> 0"
  3.2695 +    with i0
  3.2696 +    have i0: "i < 0"
  3.2697 +      by simp
  3.2698 +    hence "length (int_to_bv i) = length (norm_signed (\<one> # bv_not (norm_unsigned (nat_to_bv (- i - 1)))))"
  3.2699 +      by (simp add: int_to_bv_def)
  3.2700 +    also from norm_unsigned_result [of "nat_to_bv (- i - 1)"]
  3.2701 +    have "... = Suc (length_nat (- i - 1))"
  3.2702 +      apply safe
  3.2703 +      apply simp
  3.2704 +      apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (-i - 1)"])
  3.2705 +      using prems
  3.2706 +      apply simp
  3.2707 +      apply (cases "- i - 1 = 0")
  3.2708 +      apply simp
  3.2709 +      apply (simp add: length_nat [symmetric])
  3.2710 +      apply (cases "norm_unsigned (nat_to_bv (- i - 1))")
  3.2711 +      apply simp
  3.2712 +      apply simp
  3.2713 +      using prems
  3.2714 +      apply (simp add: length_nat [symmetric])
  3.2715 +      done
  3.2716 +    finally
  3.2717 +    show ?thesis
  3.2718 +      using i0
  3.2719 +      by (simp add: length_int_def)
  3.2720 +  qed
  3.2721 +qed
  3.2722 +
  3.2723 +lemma length_int_0 [simp]: "length_int 0 = 0"
  3.2724 +  by (simp add: length_int_def)
  3.2725 +
  3.2726 +lemma length_int_gt0: "0 < i ==> length_int i = Suc (length_nat i)"
  3.2727 +  by (simp add: length_int_def)
  3.2728 +
  3.2729 +lemma length_int_lt0: "i < 0 ==> length_int i = Suc (length_nat (- i - 1))"
  3.2730 +  by (simp add: length_int_def)
  3.2731 +
  3.2732 +lemma bv_chopI: "[| w = w1 @ w2 ; i = length w2 |] ==> bv_chop w i = (w1,w2)"
  3.2733 +  by (simp add: bv_chop_def Let_def)
  3.2734 +
  3.2735 +lemma bv_sliceI: "[| j \<le> i ; i < length w ; w = w1 @ w2 @ w3 ; Suc i = length w2 + j ; j = length w3  |] ==> bv_slice w (i,j) = w2"
  3.2736 +  apply (simp add: bv_slice_def)
  3.2737 +  apply (subst bv_chopI [of "w1 @ w2 @ w3" w1 "w2 @ w3"])
  3.2738 +  apply simp
  3.2739 +  apply simp
  3.2740 +  apply simp
  3.2741 +  apply (subst bv_chopI [of "w2 @ w3" w2 w3],simp_all)
  3.2742 +  done
  3.2743 +
  3.2744 +lemma bv_slice_bv_slice:
  3.2745 +  assumes ki: "k \<le> i"
  3.2746 +  and     ij: "i \<le> j"
  3.2747 +  and     jl: "j \<le> l"
  3.2748 +  and     lw: "l < length w"
  3.2749 +  shows       "bv_slice w (j,i) = bv_slice (bv_slice w (l,k)) (j-k,i-k)"
  3.2750 +proof -
  3.2751 +  def w1  == "fst (bv_chop w (Suc l))"
  3.2752 +  def w2  == "fst (bv_chop (snd (bv_chop w (Suc l))) (Suc j))"
  3.2753 +  def w3  == "fst (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)"
  3.2754 +  def w4  == "fst (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
  3.2755 +  def w5  == "snd (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
  3.2756 +
  3.2757 +  note w_defs = w1_def w2_def w3_def w4_def w5_def
  3.2758 +
  3.2759 +  have w_def: "w = w1 @ w2 @ w3 @ w4 @ w5"
  3.2760 +    by (simp add: w_defs append_bv_chop_id)
  3.2761 +
  3.2762 +  from ki ij jl lw
  3.2763 +  show ?thesis
  3.2764 +    apply (subst bv_sliceI [where ?j = i and ?i = j and ?w = w and ?w1.0 = "w1 @ w2" and ?w2.0 = w3 and ?w3.0 = "w4 @ w5"])
  3.2765 +    apply simp_all
  3.2766 +    apply (rule w_def)
  3.2767 +    apply (simp add: w_defs min_def)
  3.2768 +    apply (simp add: w_defs min_def)
  3.2769 +    apply (subst bv_sliceI [where ?j = k and ?i = l and ?w = w and ?w1.0 = w1 and ?w2.0 = "w2 @ w3 @ w4" and ?w3.0 = w5])
  3.2770 +    apply simp_all
  3.2771 +    apply (rule w_def)
  3.2772 +    apply (simp add: w_defs min_def)
  3.2773 +    apply (simp add: w_defs min_def)
  3.2774 +    apply (subst bv_sliceI [where ?j = "i-k" and ?i = "j-k" and ?w = "w2 @ w3 @ w4" and ?w1.0 = w2 and ?w2.0 = w3 and ?w3.0 = w4])
  3.2775 +    apply simp_all
  3.2776 +    apply (simp_all add: w_defs min_def)
  3.2777 +    apply arith+
  3.2778 +    done
  3.2779 +qed
  3.2780 +
  3.2781 +lemma bv_to_nat_extend [simp]: "bv_to_nat (bv_extend n \<zero> w) = bv_to_nat w"
  3.2782 +  apply (simp add: bv_extend_def)
  3.2783 +  apply (subst bv_to_nat_dist_append)
  3.2784 +  apply simp
  3.2785 +  apply (induct "n - length w",simp_all)
  3.2786 +  done
  3.2787 +
  3.2788 +lemma bv_msb_extend_same [simp]: "bv_msb w = b ==> bv_msb (bv_extend n b w) = b"
  3.2789 +  apply (simp add: bv_extend_def)
  3.2790 +  apply (induct "n - length w",simp_all)
  3.2791 +  done
  3.2792 +
  3.2793 +lemma bv_to_int_extend [simp]:
  3.2794 +  assumes a: "bv_msb w = b"
  3.2795 +  shows      "bv_to_int (bv_extend n b w) = bv_to_int w"
  3.2796 +proof (cases "bv_msb w")
  3.2797 +  assume [simp]: "bv_msb w = \<zero>"
  3.2798 +  with a have [simp]: "b = \<zero>"
  3.2799 +    by simp
  3.2800 +  show ?thesis
  3.2801 +    by (simp add: bv_to_int_def)
  3.2802 +next
  3.2803 +  assume [simp]: "bv_msb w = \<one>"
  3.2804 +  with a have [simp]: "b = \<one>"
  3.2805 +    by simp
  3.2806 +  show ?thesis
  3.2807 +    apply (simp add: bv_to_int_def)
  3.2808 +    apply (simp add: bv_extend_def)
  3.2809 +    apply (induct "n - length w",simp_all)
  3.2810 +    done
  3.2811 +qed
  3.2812 +
  3.2813 +lemma length_nat_mono [simp]: "x \<le> y ==> length_nat x \<le> length_nat y"
  3.2814 +proof (rule ccontr)
  3.2815 +  assume xy: "x \<le> y"
  3.2816 +  assume "~ length_nat x \<le> length_nat y"
  3.2817 +  hence lxly: "length_nat y < length_nat x"
  3.2818 +    by simp
  3.2819 +  hence "length_nat y < (LEAST n. x < 2 ^ n)"
  3.2820 +    by (simp add: length_nat_def)
  3.2821 +  hence "~ x < 2 ^ length_nat y"
  3.2822 +    by (rule not_less_Least)
  3.2823 +  hence xx: "2 ^ length_nat y \<le> x"
  3.2824 +    by simp
  3.2825 +  have yy: "y < 2 ^ length_nat y"
  3.2826 +    apply (simp add: length_nat_def)
  3.2827 +    apply (rule LeastI)
  3.2828 +    apply (subgoal_tac "y < 2 ^ (nat y)",assumption)
  3.2829 +    apply (cases "0 \<le> y")
  3.2830 +    apply (subgoal_tac "int (nat y) < int (2 ^ nat y)")
  3.2831 +    apply (simp add: int_nat_two_exp)
  3.2832 +    apply (induct "nat y",simp_all)
  3.2833 +    done
  3.2834 +  with xx
  3.2835 +  have "y < x" by simp
  3.2836 +  with xy
  3.2837 +  show False
  3.2838 +    by simp
  3.2839 +qed
  3.2840 +
  3.2841 +lemma length_nat_mono_int [simp]: "x \<le> y ==> length_nat x \<le> length_nat y"
  3.2842 +  apply (rule length_nat_mono)
  3.2843 +  apply arith
  3.2844 +  done
  3.2845 +
  3.2846 +lemma length_nat_pos [simp,intro!]: "0 < x ==> 0 < length_nat x"
  3.2847 +  by (simp add: length_nat_non0)
  3.2848 +
  3.2849 +lemma length_int_mono_gt0: "[| 0 \<le> x ; x \<le> y |] ==> length_int x \<le> length_int y"
  3.2850 +  by (cases "x = 0",simp_all add: length_int_gt0)
  3.2851 +
  3.2852 +lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x"
  3.2853 +  by (cases "y = 0",simp_all add: length_int_lt0)
  3.2854 +
  3.2855 +lemmas [simp] = length_nat_non0
  3.2856 +
  3.2857 +lemma "nat_to_bv (number_of bin.Pls) = []"
  3.2858 +  by simp
  3.2859 +
  3.2860 +consts
  3.2861 +  fast_nat_to_bv_helper :: "bin => bit list => bit list"
  3.2862 +
  3.2863 +primrec
  3.2864 +  fast_nat_to_bv_Pls: "fast_nat_to_bv_helper bin.Pls res = res"
  3.2865 +  fast_nat_to_bv_Bit: "fast_nat_to_bv_helper (w BIT b) res = fast_nat_to_bv_helper w ((if b then \<one> else \<zero>) # res)"
  3.2866 +
  3.2867 +lemma fast_nat_to_bv_def:
  3.2868 +  assumes pos_w: "(0::int) \<le> number_of w"
  3.2869 +  shows "nat_to_bv (number_of w) == norm_unsigned (fast_nat_to_bv_helper w [])"
  3.2870 +proof -
  3.2871 +  have h [rule_format]: "(0::int) \<le> number_of w ==> \<forall> l. norm_unsigned (nat_to_bv_helper (number_of w) l) = norm_unsigned (fast_nat_to_bv_helper w l)"
  3.2872 +  proof (induct w,simp add: nat_to_bv_helper.simps,simp)
  3.2873 +    fix bin b
  3.2874 +    assume ind: "(0::int) \<le> number_of bin ==> \<forall> l. norm_unsigned (nat_to_bv_helper (number_of bin) l) = norm_unsigned (fast_nat_to_bv_helper bin l)"
  3.2875 +    def qq == "number_of bin::int"
  3.2876 +    assume posbb: "(0::int) \<le> number_of (bin BIT b)"
  3.2877 +    hence indq [rule_format]: "\<forall> l. norm_unsigned (nat_to_bv_helper qq l) = norm_unsigned (fast_nat_to_bv_helper bin l)"
  3.2878 +      apply (unfold qq_def)
  3.2879 +      apply (rule ind)
  3.2880 +      apply simp
  3.2881 +      done
  3.2882 +    from posbb
  3.2883 +    have "0 \<le> qq"
  3.2884 +      by (simp add: qq_def)
  3.2885 +    with posbb
  3.2886 +    show "\<forall> l. norm_unsigned (nat_to_bv_helper (number_of (bin BIT b)) l) = norm_unsigned (fast_nat_to_bv_helper (bin BIT b) l)"
  3.2887 +      apply (subst pos_number_of,simp)
  3.2888 +      apply safe
  3.2889 +      apply (fold qq_def)
  3.2890 +      apply (cases "qq = 0")
  3.2891 +      apply (simp add: nat_to_bv_helper.simps)
  3.2892 +      apply (subst indq [symmetric])
  3.2893 +      apply (subst indq [symmetric])
  3.2894 +      apply (simp add: nat_to_bv_helper.simps)
  3.2895 +      apply (subgoal_tac "0 < qq")
  3.2896 +      prefer 2
  3.2897 +      apply simp
  3.2898 +      apply simp
  3.2899 +      apply (subst indq [symmetric])
  3.2900 +      apply (subst indq [symmetric])
  3.2901 +      apply auto
  3.2902 +      apply (subst nat_to_bv_helper.simps [of "2 * qq + 1"])
  3.2903 +      apply simp
  3.2904 +      apply safe
  3.2905 +      apply (subgoal_tac "2 * qq + 1 ~= 2 * q")
  3.2906 +      apply simp
  3.2907 +      apply arith
  3.2908 +      apply (subgoal_tac "(2 * qq + 1) div 2 = qq")
  3.2909 +      apply simp
  3.2910 +      apply (subst zdiv_zadd1_eq,simp)
  3.2911 +      apply (subst nat_to_bv_helper.simps [of "2 * qq"])
  3.2912 +      apply simp
  3.2913 +      done
  3.2914 +  qed
  3.2915 +  from pos_w
  3.2916 +  have "nat_to_bv (number_of w) = norm_unsigned (nat_to_bv (number_of w))"
  3.2917 +    by simp
  3.2918 +  also have "... = norm_unsigned (fast_nat_to_bv_helper w [])"
  3.2919 +    apply (unfold nat_to_bv_def)
  3.2920 +    apply (rule h)
  3.2921 +    apply (rule pos_w)
  3.2922 +    done
  3.2923 +  finally show "nat_to_bv (number_of w) == norm_unsigned (fast_nat_to_bv_helper w [])"
  3.2924 +    by simp
  3.2925 +qed
  3.2926 +
  3.2927 +lemma fast_nat_to_bv_Bit0: "fast_nat_to_bv_helper (w BIT False) res = fast_nat_to_bv_helper w (\<zero> # res)"
  3.2928 +  by simp
  3.2929 +
  3.2930 +lemma fast_nat_to_bv_Bit1: "fast_nat_to_bv_helper (w BIT True) res = fast_nat_to_bv_helper w (\<one> # res)"
  3.2931 +  by simp
  3.2932 +
  3.2933 +declare fast_nat_to_bv_Bit [simp del]
  3.2934 +declare fast_nat_to_bv_Bit0 [simp]
  3.2935 +declare fast_nat_to_bv_Bit1 [simp]
  3.2936 +
  3.2937 +consts
  3.2938 +  fast_bv_to_nat_helper :: "[bit list, bin] => bin"
  3.2939 +
  3.2940 +primrec
  3.2941 +  fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] bin = bin"
  3.2942 +  fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) bin = fast_bv_to_nat_helper bs (bin BIT (bit_case False True b))"
  3.2943 +
  3.2944 +lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = fast_bv_to_nat_helper bs (bin BIT False)"
  3.2945 +  by simp
  3.2946 +
  3.2947 +lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = fast_bv_to_nat_helper bs (bin BIT True)"
  3.2948 +  by simp
  3.2949 +
  3.2950 +lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs bin.Pls)"
  3.2951 +proof (simp add: bv_to_nat_def)
  3.2952 +  have "\<forall> bin. (foldl (%bn b. bn BIT (b = \<one>)) bin bs) = (fast_bv_to_nat_helper bs bin)"
  3.2953 +    apply (induct bs,simp)
  3.2954 +    apply (case_tac a,simp_all)
  3.2955 +    done
  3.2956 +  thus "number_of (foldl (%bn b. bn BIT (b = \<one>)) bin.Pls bs) == number_of (fast_bv_to_nat_helper bs bin.Pls)::int"
  3.2957 +    by simp
  3.2958 +qed
  3.2959 +
  3.2960 +declare fast_bv_to_nat_Cons [simp del]
  3.2961 +declare fast_bv_to_nat_Cons0 [simp]
  3.2962 +declare fast_bv_to_nat_Cons1 [simp]
  3.2963 +
  3.2964 +setup setup_word
  3.2965 +
  3.2966 +declare bv_to_nat1 [simp del]
  3.2967 +declare bv_to_nat_helper [simp del]
  3.2968 +
  3.2969 +constdefs
  3.2970 +  bv_mapzip :: "[bit => bit => bit,bit list, bit list] => bit list"
  3.2971 +  "bv_mapzip f w1 w2 == let g = bv_extend (max (length w1) (length w2)) \<zero>
  3.2972 +                        in map (split f) (zip (g w1) (g w2))"
  3.2973 +
  3.2974 +lemma bv_length_bv_mapzip [simp]: "length (bv_mapzip f w1 w2) = max (length w1) (length w2)"
  3.2975 +  by (simp add: bv_mapzip_def Let_def split: split_max)
  3.2976 +
  3.2977 +lemma [simp]: "bv_mapzip f [] [] = []"
  3.2978 +  by (simp add: bv_mapzip_def Let_def)
  3.2979 +
  3.2980 +lemma [simp]: "length w1 = length w2 ==> bv_mapzip f (x#w1) (y#w2) = f x y # bv_mapzip f w1 w2"
  3.2981 +  by (simp add: bv_mapzip_def Let_def)
  3.2982 +
  3.2983 +lemma [code]: "bv_to_nat bs = list_rec (0::int) (\<lambda>b bs n. bitval b * 2 ^ length bs + n) bs"
  3.2984 +  by (induct bs,simp_all add: bv_to_nat_helper)
  3.2985 +
  3.2986 +text {* The following can be added for speedup, but depends on the
  3.2987 +exact definition of division and modulo of the ML compiler for soundness. *}
  3.2988 +
  3.2989 +(*
  3.2990 +consts_code "op div" ("'('(_') div '(_')')")
  3.2991 +consts_code "op mod" ("'('(_') mod '(_')')")
  3.2992 +*)
  3.2993 +
  3.2994 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/word_setup.ML	Mon Mar 29 15:35:04 2004 +0200
     4.3 @@ -0,0 +1,43 @@
     4.4 +(*  Title:      HOL/Library/word_setup.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     4.7 +*)
     4.8 +
     4.9 +local
    4.10 +    fun is_const_bool (Const("True",_)) = true
    4.11 +      | is_const_bool (Const("False",_)) = true
    4.12 +      | is_const_bool _ = false
    4.13 +    fun is_const_bit (Const("Word.bit.Zero",_)) = true
    4.14 +      | is_const_bit (Const("Word.bit.One",_)) = true
    4.15 +      | is_const_bit _ = false
    4.16 +    fun num_is_usable (Const("Numeral.bin.Pls",_)) = true
    4.17 +      | num_is_usable (Const("Numeral.bin.Min",_)) = false
    4.18 +      | num_is_usable (Const("Numeral.bin.Bit",_) $ w $ b) =
    4.19 +	num_is_usable w andalso is_const_bool b
    4.20 +      | num_is_usable _ = false
    4.21 +    fun vec_is_usable (Const("List.list.Nil",_)) = true
    4.22 +      | vec_is_usable (Const("List.list.Cons",_) $ b $ bs) =
    4.23 +	vec_is_usable bs andalso is_const_bit b
    4.24 +      | vec_is_usable _ = false
    4.25 +    fun add_word thy =
    4.26 +	let
    4.27 +	    val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"
    4.28 +	    val fast2_th = PureThy.get_thm thy "Word.fast_bv_to_nat_def"
    4.29 +	    fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
    4.30 +		if num_is_usable t
    4.31 +		then Some (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("Numeral.bin",[]))),cterm_of sg t)] fast1_th)
    4.32 +		else None
    4.33 +	      | f _ _ _ = None
    4.34 +	    fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) =
    4.35 +		if vec_is_usable t
    4.36 +		then Some (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
    4.37 +		else None
    4.38 +	      | g _ _ _ = None
    4.39 +	    val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of ?w)"] f
    4.40 +	    val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (?x # ?xs)"] g
    4.41 +	in
    4.42 +	    Simplifier.change_simpset_of (op addsimprocs) [simproc1,simproc2] thy
    4.43 +	end
    4.44 +in
    4.45 +val setup_word = [add_word]
    4.46 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/ex/Adder.thy	Mon Mar 29 15:35:04 2004 +0200
     5.3 @@ -0,0 +1,115 @@
     5.4 +(*  Title:      HOL/ex/Adder.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Sergey Tverdyshev (Universitaet des Saarlandes)
     5.7 +
     5.8 +Implementation of carry chain incrementor and adder.
     5.9 +*)
    5.10 +
    5.11 +theory Adder = Main + Word:
    5.12 +
    5.13 +lemma [simp]: "bv_to_nat [b] = bitval b"
    5.14 +  by (simp add: bv_to_nat_helper)
    5.15 +
    5.16 +lemma bv_to_nat_helper': "bv \<noteq> [] ==> bv_to_nat bv = bitval (hd bv) * 2 ^ (length bv - 1) + bv_to_nat (tl bv)"
    5.17 +  by (cases bv,simp_all add: bv_to_nat_helper)
    5.18 +
    5.19 +constdefs
    5.20 +  half_adder :: "[bit,bit] => bit list"
    5.21 +  "half_adder a b == [a bitand b,a bitxor b]"
    5.22 +
    5.23 +lemma half_adder_correct: "bv_to_nat (half_adder a b) = bitval a + bitval b"
    5.24 +  apply (simp add: half_adder_def)
    5.25 +  apply (cases a, auto)
    5.26 +  apply (cases b, auto)
    5.27 +  done
    5.28 +
    5.29 +lemma [simp]: "length (half_adder a b) = 2"
    5.30 +  by (simp add: half_adder_def)
    5.31 +
    5.32 +constdefs
    5.33 +  full_adder :: "[bit,bit,bit] => bit list"
    5.34 +  "full_adder a b c == let x = a bitxor b in [a bitand b bitor c bitand x,x bitxor c]"
    5.35 +
    5.36 +lemma full_adder_correct: "bv_to_nat (full_adder a b c) = bitval a + bitval b + bitval c"
    5.37 +  apply (simp add: full_adder_def Let_def)
    5.38 +  apply (cases a, auto)
    5.39 +  apply (case_tac[!] b, auto)
    5.40 +  apply (case_tac[!] c, auto)
    5.41 +  done
    5.42 +
    5.43 +lemma [simp]: "length (full_adder a b c) = 2"
    5.44 +  by (simp add: full_adder_def Let_def)
    5.45 +
    5.46 +(*carry chain incrementor*)
    5.47 +
    5.48 +consts
    5.49 +  carry_chain_inc :: "[bit list,bit] => bit list"
    5.50 +
    5.51 +primrec 
    5.52 +  "carry_chain_inc [] c = [c]"
    5.53 +  "carry_chain_inc (a#as) c = (let chain = carry_chain_inc as c
    5.54 +                               in  half_adder a (hd chain) @ tl chain)"
    5.55 +
    5.56 +lemma cci_nonnull: "carry_chain_inc as c \<noteq> []"
    5.57 +  by (cases as,auto simp add: Let_def half_adder_def)
    5.58 +  
    5.59 +lemma cci_length [simp]: "length (carry_chain_inc as c) = length as + 1"
    5.60 +  by (induct as, simp_all add: Let_def)
    5.61 +
    5.62 +lemma cci_correct: "bv_to_nat (carry_chain_inc as c) = bv_to_nat as + bitval c"
    5.63 +  apply (induct as)
    5.64 +  apply (cases c,simp_all add: Let_def)
    5.65 +  apply (subst bv_to_nat_dist_append,simp)
    5.66 +  apply (simp add: half_adder_correct bv_to_nat_helper' [OF cci_nonnull] ring_distrib bv_to_nat_helper)
    5.67 +  done
    5.68 +
    5.69 +consts
    5.70 +  carry_chain_adder :: "[bit list,bit list,bit] => bit list"
    5.71 +
    5.72 +primrec
    5.73 +  "carry_chain_adder []     bs c = [c]"
    5.74 +  "carry_chain_adder (a#as) bs c = (let chain = carry_chain_adder as (tl bs) c
    5.75 +                                    in  full_adder a (hd bs) (hd chain) @ tl chain)"
    5.76 +
    5.77 +lemma cca_nonnull: "carry_chain_adder as bs c \<noteq> []"
    5.78 +  by (cases as,auto simp add: full_adder_def Let_def)
    5.79 +
    5.80 +lemma cca_length [rule_format]: "\<forall>bs. length as = length bs --> length (carry_chain_adder as bs c) = length as + 1"
    5.81 +proof (induct as,auto simp add: Let_def)
    5.82 +  fix as :: "bit list"
    5.83 +  fix xs :: "bit list"
    5.84 +  assume ind: "\<forall>bs. length as = length bs --> length (carry_chain_adder as bs c) = Suc (length bs)"
    5.85 +  assume len: "Suc (length as) = length xs"
    5.86 +  thus "Suc (length (carry_chain_adder as (tl xs) c) - Suc 0) = length xs"
    5.87 +  proof (cases xs,simp_all)
    5.88 +    fix b bs
    5.89 +    assume [simp]: "xs = b # bs"
    5.90 +    assume "length as = length bs"
    5.91 +    with ind
    5.92 +    show "length (carry_chain_adder as bs c) - Suc 0 = length bs"
    5.93 +      by auto
    5.94 +  qed
    5.95 +qed
    5.96 +
    5.97 +lemma cca_correct [rule_format]: "\<forall>bs. length as = length bs --> bv_to_nat (carry_chain_adder as bs c) = bv_to_nat as + bv_to_nat bs + bitval c"
    5.98 +proof (induct as,auto simp add: Let_def)
    5.99 +  fix a :: bit
   5.100 +  fix as :: "bit list"
   5.101 +  fix xs :: "bit list"
   5.102 +  assume ind: "\<forall>bs. length as = length bs --> bv_to_nat (carry_chain_adder as bs c) = bv_to_nat as + bv_to_nat bs + bitval c"
   5.103 +  assume len: "Suc (length as) = length xs"
   5.104 +  thus "bv_to_nat (full_adder a (hd xs) (hd (carry_chain_adder as (tl xs) c)) @ tl (carry_chain_adder as (tl xs) c)) = bv_to_nat (a # as) + bv_to_nat xs + bitval c"
   5.105 +  proof (cases xs,simp_all)
   5.106 +    fix b bs
   5.107 +    assume [simp]: "xs = b # bs"
   5.108 +    assume len: "length as = length bs"
   5.109 +    with ind
   5.110 +    have "bv_to_nat (carry_chain_adder as bs c) = bv_to_nat as + bv_to_nat bs + bitval c"
   5.111 +      by blast
   5.112 +    with len
   5.113 +    show "bv_to_nat (full_adder a b (hd (carry_chain_adder as bs c)) @ tl (carry_chain_adder as bs c)) = bv_to_nat (a # as) + bv_to_nat (b # bs) + bitval c"
   5.114 +      by (subst bv_to_nat_dist_append,simp add: full_adder_correct bv_to_nat_helper' [OF cca_nonnull] ring_distrib bv_to_nat_helper cca_length)
   5.115 +  qed
   5.116 +qed
   5.117 +
   5.118 +end
     6.1 --- a/src/HOL/ex/ROOT.ML	Mon Mar 29 10:17:35 2004 +0200
     6.2 +++ b/src/HOL/ex/ROOT.ML	Mon Mar 29 15:35:04 2004 +0200
     6.3 @@ -40,3 +40,5 @@
     6.4  if_svc_enabled time_use_thy "svc_test";
     6.5  
     6.6  time_use_thy "Refute_Examples";
     6.7 +
     6.8 +time_use_thy "Adder";