author berghofe Wed Nov 24 10:32:33 2004 +0100 (2004-11-24) changeset 15325 50ac7d2c34c9 parent 15324 c27165172e30 child 15326 ff21cddee442
Functions nat_to_bv and bv_to_nat now really operate on natural numbers.
```     1.1 --- a/src/HOL/Library/Word.thy	Wed Nov 24 10:30:19 2004 +0100
1.2 +++ b/src/HOL/Library/Word.thy	Wed Nov 24 10:32:33 2004 +0100
1.3 @@ -35,7 +35,7 @@
1.4      and zero_less_power [intro]
1.5
1.6  lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)"
1.7 -  by (induct k,simp_all)
1.8 +  by (simp add: zpower_int [symmetric])
1.9
1.10  subsection {* Bits *}
1.11
1.12 @@ -44,7 +44,7 @@
1.13    | One ("\<one>")
1.14
1.15  consts
1.16 -  bitval :: "bit => int"
1.17 +  bitval :: "bit => nat"
1.18
1.19  primrec
1.20    "bitval \<zero> = 0"
1.21 @@ -177,56 +177,29 @@
1.22    by (induct w,simp_all)
1.23
1.24  constdefs
1.25 -  bv_to_nat :: "bit list => int"
1.26 -  "bv_to_nat bv == number_of (foldl (%bn b. bn BIT (b = \<one>)) Numeral.Pls bv)"
1.27 +  bv_to_nat :: "bit list => nat"
1.28 +  "bv_to_nat == foldl (%bn b. 2 * bn + bitval b) 0"
1.29
1.30  lemma [simp]: "bv_to_nat [] = 0"
1.32
1.33 -lemma pos_number_of:
1.34 -     "number_of (w BIT b) = (2::int) * number_of w + (if b then 1 else 0)"
1.36 -
1.37  lemma bv_to_nat_helper [simp]: "bv_to_nat (b # bs) = bitval b * 2 ^ length bs + bv_to_nat bs"
1.38  proof -
1.39 -  def bv_to_nat' == "%base bv. number_of (foldl (% bn b. bn BIT (b = \<one>)) base bv)::int"
1.40 -  have bv_to_nat'_def: "!!base bv. bv_to_nat' base bv == number_of (foldl (% bn b. bn BIT (b = \<one>)) base bv)::int"
1.41 -    by (simp add: bv_to_nat'_def)
1.42 -  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)"
1.43 -    by (simp add: bv_to_nat'_def)
1.44 -  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' Numeral.Pls bs"
1.45 -  proof (induct bs,simp add: bv_to_nat'_def,clarify)
1.46 -    fix x xs base
1.47 -    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' Numeral.Pls xs"
1.48 -    assume base_pos: "(0::int) \<le> number_of base"
1.49 -    def qq == "number_of base::int"
1.50 -    show "bv_to_nat' base (x # xs) = number_of base * 2 ^ (length (x # xs)) + bv_to_nat' Numeral.Pls (x # xs)"
1.51 -      apply (unfold bv_to_nat'_def)
1.52 +  let ?bv_to_nat' = "foldl (\<lambda>bn b. 2 * bn + bitval b)"
1.53 +  have helper: "\<And>base. ?bv_to_nat' base bs = base * 2 ^ length bs + ?bv_to_nat' 0 bs"
1.54 +  proof (induct bs)
1.55 +    case Nil show ?case by simp
1.56 +  next
1.57 +    case (Cons x xs base)
1.58 +    show ?case
1.59        apply (simp only: foldl.simps)
1.60 -      apply (fold bv_to_nat'_def)
1.61 -      apply (subst ind [of "base BIT (x = \<one>)"])
1.62 -      using base_pos
1.63 -      apply simp
1.64 -      apply (subst ind [of "Numeral.Pls BIT (x = \<one>)"])
1.65 +      apply (subst Cons [of "2 * base + bitval x"])
1.66        apply simp
1.67 -      apply (subst pos_number_of [of "base" "x = \<one>"])
1.68 -      using base_pos
1.69 -      apply (subst pos_number_of [of "Numeral.Pls" "x = \<one>"])
1.70 -      apply (fold qq_def)
1.71 -      apply (simp add: ring_distrib)
1.72 +      apply (subst Cons [of "bitval x"])
1.74        done
1.75    qed
1.76 -  show ?thesis
1.77 -    apply (unfold bv_to_nat_def [of "b # bs"])
1.78 -    apply (simp only: foldl.simps)
1.79 -    apply (fold bv_to_nat'_def)
1.80 -    apply (subst helper)
1.81 -    apply simp
1.82 -    apply (cases "b::bit")
1.83 -    apply (simp add: bv_to_nat'_def bv_to_nat_def)
1.84 -    apply (simp add: iszero_def)
1.85 -    apply (simp add: bv_to_nat'_def bv_to_nat_def)
1.86 -    done
1.87 +  show ?thesis by (simp add: bv_to_nat_def) (rule helper)
1.88  qed
1.89
1.90  lemma bv_to_nat0 [simp]: "bv_to_nat (\<zero>#bs) = bv_to_nat bs"
1.91 @@ -235,13 +208,6 @@
1.92  lemma bv_to_nat1 [simp]: "bv_to_nat (\<one>#bs) = 2 ^ length bs + bv_to_nat bs"
1.93    by simp
1.94
1.95 -lemma bv_to_nat_lower_range [intro,simp]: "0 \<le> bv_to_nat w"
1.96 -  apply (induct w,simp_all)
1.97 -  apply (case_tac a,simp_all)
1.99 -  apply auto
1.100 -  done
1.101 -
1.102  lemma bv_to_nat_upper_range: "bv_to_nat w < 2 ^ length w"
1.103  proof (induct w,simp_all)
1.104    fix b bs
1.105 @@ -377,14 +343,14 @@
1.106    by (rule bit_list_induct [of _ w],simp_all)
1.107
1.108  consts
1.109 -  nat_to_bv_helper :: "int => bit list => bit list"
1.110 +  nat_to_bv_helper :: "nat => bit list => bit list"
1.111
1.112 -recdef nat_to_bv_helper "measure nat"
1.113 -  "nat_to_bv_helper n = (%bs. (if n \<le> 0 then bs
1.114 +recdef nat_to_bv_helper "measure (\<lambda>n. n)"
1.115 +  "nat_to_bv_helper n = (%bs. (if n = 0 then bs
1.116                                 else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs)))"
1.117
1.118  constdefs
1.119 -  nat_to_bv :: "int => bit list"
1.120 +  nat_to_bv :: "nat => bit list"
1.121    "nat_to_bv n == nat_to_bv_helper n []"
1.122
1.123  lemma nat_to_bv0 [simp]: "nat_to_bv 0 = []"
1.124 @@ -393,8 +359,7 @@
1.125  lemmas [simp del] = nat_to_bv_helper.simps
1.126
1.127  lemma n_div_2_cases:
1.128 -  assumes n0  : "0 \<le> n"
1.129 -  and     zero: "(n::int) = 0 ==> R"
1.130 +  assumes zero: "(n::nat) = 0 ==> R"
1.131    and     div : "[| n div 2 < n ; 0 < n |] ==> R"
1.132    shows         "R"
1.133  proof (cases "n = 0")
1.134 @@ -403,8 +368,7 @@
1.135      by (rule zero)
1.136  next
1.137    assume "n ~= 0"
1.138 -  with n0
1.139 -  have nn0: "0 < n"
1.140 +  hence nn0: "0 < n"
1.141      by simp
1.142    hence "n div 2 < n"
1.143      by arith
1.144 @@ -471,19 +435,12 @@
1.145  qed
1.146
1.147  lemma unfold_nat_to_bv_helper:
1.148 -  "0 \<le> b ==> nat_to_bv_helper b l = nat_to_bv_helper b [] @ l"
1.149 +  "nat_to_bv_helper b l = nat_to_bv_helper b [] @ l"
1.150  proof -
1.151 -  assume "0 \<le> b"
1.152    have "\<forall>l. nat_to_bv_helper b l = nat_to_bv_helper b [] @ l"
1.153 -  proof (rule int_wf_ge_induct [where ?i = b])
1.154 -    show "0 \<le> b"
1.155 -      .
1.156 -  next
1.157 -    show "\<forall> l. nat_to_bv_helper 0 l = nat_to_bv_helper 0 [] @ l"
1.158 -      by (simp add: nat_to_bv_helper.simps)
1.159 -  next
1.160 +  proof (induct b rule: less_induct)
1.161      fix n
1.162 -    assume ind: "!!j. [| 0 \<le> j ; j < n |] ==> \<forall> l. nat_to_bv_helper j l = nat_to_bv_helper j [] @ l"
1.163 +    assume ind: "!!j. j < n \<Longrightarrow> \<forall> l. nat_to_bv_helper j l = nat_to_bv_helper j [] @ l"
1.164      show "\<forall>l. nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
1.165      proof
1.166        fix l
1.167 @@ -496,10 +453,6 @@
1.168  	assume "~n < 0"
1.169  	show ?thesis
1.170  	proof (rule n_div_2_cases [of n])
1.171 -	  from prems
1.172 -	  show "0 \<le> n"
1.173 -	    by simp
1.174 -	next
1.175  	  assume [simp]: "n = 0"
1.176  	  show ?thesis
1.177  	    apply (subst nat_to_bv_helper.simps [of n])
1.178 @@ -515,6 +468,9 @@
1.179  	    by blast
1.180  	  show ?thesis
1.181  	    apply (subst nat_to_bv_helper.simps [of n])
1.182 +	    apply (cases "n=0")
1.183 +	    apply simp
1.184 +	    apply (simp only: if_False)
1.185  	    apply simp
1.186  	    apply (subst spec [OF ind',of "\<zero>#l"])
1.187  	    apply (subst spec [OF ind',of "\<one>#l"])
1.188 @@ -538,12 +494,9 @@
1.189      apply (subst nat_to_bv_helper.simps [of n])
1.190      apply (subst unfold_nat_to_bv_helper)
1.191      using prems
1.192 -    apply arith
1.193      apply simp
1.194      apply (subst nat_to_bv_def [of "n div 2"])
1.195      apply auto
1.196 -    using prems
1.197 -    apply auto
1.198      done
1.199  qed
1.200
1.201 @@ -558,7 +511,7 @@
1.202        fix l2
1.203        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"
1.204        proof -
1.205 -	have "(2::int) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
1.206 +	have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
1.207  	  by (induct "length xs",simp_all)
1.208  	hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 =
1.209  	  bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
1.210 @@ -573,59 +526,44 @@
1.211      ..
1.212  qed
1.213
1.214 -lemma bv_nat_bv [simp]:
1.215 -  assumes n0: "0 \<le> n"
1.216 -  shows       "bv_to_nat (nat_to_bv n) = n"
1.217 -proof -
1.218 -  have "0 \<le> n --> bv_to_nat (nat_to_bv n) = n"
1.219 -  proof (rule int_wf_ge_induct [where ?k = 0],simp_all,clarify)
1.220 -    fix n
1.221 -    assume ind: "!!j. [| 0 \<le> j; j < n |] ==> bv_to_nat (nat_to_bv j) = j"
1.222 -    assume n0: "0 \<le> n"
1.223 -    show "bv_to_nat (nat_to_bv n) = n"
1.224 -    proof (rule n_div_2_cases [of n])
1.225 -      show "0 \<le> n"
1.226 -	.
1.227 -    next
1.228 -      assume [simp]: "n = 0"
1.229 -      show ?thesis
1.230 -	by simp
1.231 -    next
1.232 -      assume nn: "n div 2 < n"
1.233 -      assume n0: "0 < n"
1.234 -      hence n20: "0 \<le> n div 2"
1.235 -	by arith
1.236 -      from ind and n20 nn
1.237 -      have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2"
1.238 -	by blast
1.239 -      from n0 have n0': "~ n \<le> 0"
1.240 -	by simp
1.241 -      show ?thesis
1.242 -	apply (subst nat_to_bv_def)
1.243 -	apply (subst nat_to_bv_helper.simps [of n])
1.244 -	apply (simp add: n0' split del: split_if)
1.245 -	apply (subst unfold_nat_to_bv_helper)
1.246 -	apply (rule n20)
1.247 -	apply (subst bv_to_nat_dist_append)
1.248 -	apply (fold nat_to_bv_def)
1.249 -	apply (simp add: ind' split del: split_if)
1.250 -	apply (cases "n mod 2 = 0")
1.251 +lemma bv_nat_bv [simp]: "bv_to_nat (nat_to_bv n) = n"
1.252 +proof (induct n rule: less_induct)
1.253 +  fix n
1.254 +  assume ind: "!!j. j < n \<Longrightarrow> bv_to_nat (nat_to_bv j) = j"
1.255 +  show "bv_to_nat (nat_to_bv n) = n"
1.256 +  proof (rule n_div_2_cases [of n])
1.257 +    assume [simp]: "n = 0"
1.258 +    show ?thesis
1.259 +      by simp
1.260 +  next
1.261 +    assume nn: "n div 2 < n"
1.262 +    assume n0: "0 < n"
1.263 +    from ind and nn
1.264 +    have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2"
1.265 +      by blast
1.266 +    from n0 have n0': "n \<noteq> 0"
1.267 +      by simp
1.268 +    show ?thesis
1.269 +      apply (subst nat_to_bv_def)
1.270 +      apply (subst nat_to_bv_helper.simps [of n])
1.271 +      apply (simp only: n0' if_False)
1.272 +      apply (subst unfold_nat_to_bv_helper)
1.273 +      apply (subst bv_to_nat_dist_append)
1.274 +      apply (fold nat_to_bv_def)
1.275 +      apply (simp add: ind' split del: split_if)
1.276 +      apply (cases "n mod 2 = 0")
1.277        proof simp_all
1.278  	assume "n mod 2 = 0"
1.279 -	with zmod_zdiv_equality [of n 2]
1.280 +	with mod_div_equality [of n 2]
1.281  	show "n div 2 * 2 = n"
1.282  	  by simp
1.283        next
1.284 -	assume "n mod 2 = 1"
1.285 -	with zmod_zdiv_equality [of n 2]
1.286 -	show "n div 2 * 2 + 1 = n"
1.287 +	assume "n mod 2 = Suc 0"
1.288 +	with mod_div_equality [of n 2]
1.289 +	show "Suc (n div 2 * 2) = n"
1.290  	  by simp
1.291        qed
1.292 -    qed
1.293    qed
1.294 -  with n0
1.295 -  show ?thesis
1.296 -    by auto
1.297  qed
1.298
1.299  lemma [simp]: "bv_to_nat (norm_unsigned w) = bv_to_nat w"
1.300 @@ -696,22 +634,9 @@
1.301  lemma norm_unsigned_append2 [simp]: "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"
1.302    by (simp add: norm_unsigned_def,rule rem_initial_append2)
1.303
1.304 -lemma bv_to_nat_zero_imp_empty:
1.305 -  assumes "bv_to_nat w = 0"
1.306 -  shows   "norm_unsigned w = []"
1.307 -proof -
1.308 -  have "bv_to_nat w = 0 --> norm_unsigned w = []"
1.309 -    apply (rule bit_list_induct [of _ w],simp_all)
1.310 -    apply (subgoal_tac "0 < 2 ^ length bs + bv_to_nat bs")
1.311 -    apply simp
1.312 -    apply (subgoal_tac "(0::int) < 2 ^ length bs")
1.313 -    apply (subgoal_tac "0 \<le> bv_to_nat bs")
1.314 -    apply arith
1.315 -    apply auto
1.316 -    done
1.317 -  thus ?thesis
1.318 -    ..
1.319 -qed
1.320 +lemma bv_to_nat_zero_imp_empty [rule_format]:
1.321 +  "bv_to_nat w = 0 \<longrightarrow> norm_unsigned w = []"
1.322 +  by (rule bit_list_induct [of _ w],simp_all)
1.323
1.324  lemma bv_to_nat_nzero_imp_nempty:
1.325    assumes "bv_to_nat w \<noteq> 0"
1.326 @@ -733,31 +658,29 @@
1.327      apply safe
1.328    proof -
1.329      fix q
1.330 -    assume "(2 * bv_to_nat w) + 1 = 2 * q"
1.331 +    assume "Suc (2 * bv_to_nat w) = 2 * q"
1.332      hence orig: "(2 * bv_to_nat w + 1) mod 2 = 2 * q mod 2" (is "?lhs = ?rhs")
1.333        by simp
1.334      have "?lhs = (1 + 2 * bv_to_nat w) mod 2"
1.336      also have "... = 1"
1.338 +      by (subst mod_add1_eq) simp
1.339      finally have eq1: "?lhs = 1" .
1.340      have "?rhs  = 0"
1.341        by simp
1.342      with orig and eq1
1.343 -    have "(1::int) = 0"
1.344 -      by simp
1.345 -    thus "nat_to_bv ((2 * bv_to_nat w + 1) div 2) @ [\<zero>] = norm_unsigned (w @ [\<one>])"
1.346 +    show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<zero>] = norm_unsigned (w @ [\<one>])"
1.347        by simp
1.348    next
1.349 -    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>]"
1.350 +    have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\<one>]"
1.352      also have "... = nat_to_bv (bv_to_nat w) @ [\<one>]"
1.355      also have "... = norm_unsigned w @ [\<one>]"
1.356        by (subst ass,rule refl)
1.357      also have "... = norm_unsigned (w @ [\<one>])"
1.358        by (cases "norm_unsigned w",simp_all)
1.359 -    finally show "nat_to_bv ((2 * bv_to_nat w + 1) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])"
1.360 +    finally show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])"
1.361        .
1.362    qed
1.363  next
1.364 @@ -774,8 +697,6 @@
1.365        apply (subst nat_to_bv_non0)
1.366        apply simp
1.367        apply auto
1.368 -      apply (cut_tac bv_to_nat_lower_range [of w])
1.369 -      apply arith
1.370        apply (subst ass)
1.371        apply (cases "norm_unsigned w")
1.373 @@ -873,8 +794,7 @@
1.374  qed
1.375
1.376  lemma norm_unsigned_nat_to_bv [simp]:
1.377 -  assumes [simp]: "0 \<le> n"
1.378 -  shows "norm_unsigned (nat_to_bv n) = nat_to_bv n"
1.379 +  "norm_unsigned (nat_to_bv n) = nat_to_bv n"
1.380  proof -
1.381    have "norm_unsigned (nat_to_bv n) = nat_to_bv (bv_to_nat (norm_unsigned (nat_to_bv n)))"
1.382      by (subst nat_bv_nat,simp)
1.383 @@ -886,16 +806,13 @@
1.384  lemma length_nat_to_bv_upper_limit:
1.385    assumes nk: "n \<le> 2 ^ k - 1"
1.386    shows       "length (nat_to_bv n) \<le> k"
1.387 -proof (cases "n \<le> 0")
1.388 -  assume "n \<le> 0"
1.389 +proof (cases "n = 0")
1.390 +  case True
1.391    thus ?thesis
1.392      by (simp add: nat_to_bv_def nat_to_bv_helper.simps)
1.393  next
1.394 -  assume "~ n \<le> 0"
1.395 -  hence n0: "0 < n"
1.396 -    by simp
1.397 -  hence n00: "0 \<le> n"
1.398 -    by simp
1.399 +  case False
1.400 +  hence n0: "0 < n" by simp
1.401    show ?thesis
1.402    proof (rule ccontr)
1.403      assume "~ length (nat_to_bv n) \<le> k"
1.404 @@ -903,14 +820,14 @@
1.405        by simp
1.406      hence "k \<le> length (nat_to_bv n) - 1"
1.407        by arith
1.408 -    hence "(2::int) ^ k \<le> 2 ^ (length (nat_to_bv n) - 1)"
1.409 +    hence "(2::nat) ^ k \<le> 2 ^ (length (nat_to_bv n) - 1)"
1.410        by simp
1.411      also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)"
1.412 -      by (simp add: n00)
1.413 +      by simp
1.414      also have "... \<le> bv_to_nat (nat_to_bv n)"
1.415 -      by (rule bv_to_nat_lower_limit,simp add: n00 n0)
1.416 +      by (rule bv_to_nat_lower_limit,simp add: n0)
1.417      also have "... = n"
1.418 -      by (simp add: n00)
1.419 +      by simp
1.420      finally have "2 ^ k \<le> n" .
1.421      with n0
1.422      have "2 ^ k - 1 < n"
1.423 @@ -925,11 +842,6 @@
1.424    assumes nk: "2 ^ k \<le> n"
1.425    shows       "k < length (nat_to_bv n)"
1.426  proof (rule ccontr)
1.427 -  have "(0::int) \<le> 2 ^ k"
1.428 -    by auto
1.429 -  with nk
1.430 -  have [simp]: "0 \<le> n"
1.431 -    by auto
1.432    assume "~ k < length (nat_to_bv n)"
1.433    hence lnk: "length (nat_to_bv n) \<le> k"
1.434      by simp
1.435 @@ -958,13 +870,7 @@
1.437
1.440 -  apply (rule norm_unsigned_nat_to_bv)
1.441 -  apply (subgoal_tac "0 \<le> bv_to_nat w1")
1.442 -  apply (subgoal_tac "0 \<le> bv_to_nat w2")
1.443 -  apply arith
1.444 -  apply simp_all
1.445 -  done
1.447
1.448  lemma bv_add_length: "length (bv_add w1 w2) \<le> Suc (max (length w1) (length w2))"
1.450 @@ -977,21 +883,21 @@
1.451      by simp
1.452    also have "... \<le> 2 ^ Suc (max (length w1) (length w2)) - 2"
1.453    proof (cases "length w1 \<le> length w2")
1.454 -    assume [simp]: "length w1 \<le> length w2"
1.455 -    hence "(2::int) ^ length w1 \<le> 2 ^ length w2"
1.456 +    assume w1w2: "length w1 \<le> length w2"
1.457 +    hence "(2::nat) ^ length w1 \<le> 2 ^ length w2"
1.458        by simp
1.459 -    hence [simp]: "(2::int) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
1.460 +    hence "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
1.461        by arith
1.462 -    show ?thesis
1.463 -      by (simp split: split_max)
1.464 +    with w1w2 show ?thesis
1.465 +      by (simp add: diff_mult_distrib2 split: split_max)
1.466    next
1.467      assume [simp]: "~ (length w1 \<le> length w2)"
1.468 -    have "~ ((2::int) ^ length w1 - 1 \<le> 2 ^ length w2 - 1)"
1.469 +    have "~ ((2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1)"
1.470      proof
1.471 -      assume "(2::int) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
1.472 -      hence "((2::int) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1"
1.473 +      assume "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
1.474 +      hence "((2::nat) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1"
1.476 -      hence "(2::int) ^ length w1 \<le> 2 ^ length w2"
1.477 +      hence "(2::nat) ^ length w1 \<le> 2 ^ length w2"
1.478  	by simp
1.479        hence "length w1 \<le> length w2"
1.480  	by simp
1.481 @@ -999,7 +905,7 @@
1.482  	by simp
1.483      qed
1.484      thus ?thesis
1.485 -      by (simp split: split_max)
1.486 +      by (simp add: diff_mult_distrib2 split: split_max)
1.487    qed
1.488    finally show "bv_to_nat w1 + bv_to_nat w2 \<le> 2 ^ Suc (max (length w1) (length w2)) - 1"
1.489      by arith
1.490 @@ -1016,12 +922,7 @@
1.492
1.493  lemma [simp]: "norm_unsigned (bv_mult w1 w2) = bv_mult w1 w2"
1.494 -  apply (simp add: bv_mult_def)
1.495 -  apply (rule norm_unsigned_nat_to_bv)
1.496 -  apply (subgoal_tac "0 * 0 \<le> bv_to_nat w1 * bv_to_nat w2")
1.497 -  apply simp
1.498 -  apply (rule mult_mono,simp_all)
1.499 -  done
1.500 +  by (simp add: bv_mult_def)
1.501
1.502  lemma bv_mult_length: "length (bv_mult w1 w2) \<le> length w1 + length w2"
1.503  proof (unfold bv_mult_def,rule length_nat_to_bv_upper_limit)
1.504 @@ -1073,13 +974,13 @@
1.505  constdefs
1.506    int_to_bv :: "int => bit list"
1.507    "int_to_bv n == if 0 \<le> n
1.508 -                 then norm_signed (\<zero>#nat_to_bv n)
1.509 -                 else norm_signed (bv_not (\<zero>#nat_to_bv (-n- 1)))"
1.510 +                 then norm_signed (\<zero>#nat_to_bv (nat n))
1.511 +                 else norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1))))"
1.512
1.513 -lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # nat_to_bv n)"
1.514 +lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # nat_to_bv (nat n))"
1.516
1.517 -lemma int_to_bv_lt0 [simp]: "n < 0 ==> int_to_bv n = norm_signed (bv_not (\<zero>#nat_to_bv (-n- 1)))"
1.518 +lemma int_to_bv_lt0 [simp]: "n < 0 ==> int_to_bv n = norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1))))"
1.520
1.521  lemma [simp]: "norm_signed (norm_signed w) = norm_signed w"
1.522 @@ -1107,38 +1008,38 @@
1.523
1.524  constdefs
1.525    bv_to_int :: "bit list => int"
1.526 -  "bv_to_int w == case bv_msb w of \<zero> => bv_to_nat w | \<one> => -(bv_to_nat (bv_not w) + 1)"
1.527 +  "bv_to_int w == case bv_msb w of \<zero> => int (bv_to_nat w) | \<one> => - int (bv_to_nat (bv_not w) + 1)"
1.528
1.529  lemma [simp]: "bv_to_int [] = 0"
1.531
1.532 -lemma [simp]: "bv_to_int (\<zero>#bs) = bv_to_nat bs"
1.533 +lemma [simp]: "bv_to_int (\<zero>#bs) = int (bv_to_nat bs)"
1.535
1.536 -lemma [simp]: "bv_to_int (\<one>#bs) = -(bv_to_nat (bv_not bs) + 1)"
1.537 +lemma [simp]: "bv_to_int (\<one>#bs) = - int (bv_to_nat (bv_not bs) + 1)"
1.539
1.540  lemma [simp]: "bv_to_int (norm_signed w) = bv_to_int w"
1.541  proof (rule bit_list_induct [of _ w],simp_all)
1.542    fix xs
1.543    assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
1.544 -  show "bv_to_int (norm_signed (\<zero>#xs)) = bv_to_nat xs"
1.545 +  show "bv_to_int (norm_signed (\<zero>#xs)) = int (bv_to_nat xs)"
1.546    proof (rule bit_list_cases [of xs],simp_all)
1.547      fix ys
1.548      assume [simp]: "xs = \<zero>#ys"
1.549      from ind
1.550 -    show "bv_to_int (norm_signed (\<zero>#ys)) = bv_to_nat ys"
1.551 +    show "bv_to_int (norm_signed (\<zero>#ys)) = int (bv_to_nat ys)"
1.552        by simp
1.553    qed
1.554  next
1.555    fix xs
1.556    assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
1.557 -  show "bv_to_int (norm_signed (\<one>#xs)) = - bv_to_nat (bv_not xs) + -1"
1.558 +  show "bv_to_int (norm_signed (\<one>#xs)) = -1 - int (bv_to_nat (bv_not xs))"
1.559    proof (rule bit_list_cases [of xs],simp_all)
1.560      fix ys
1.561      assume [simp]: "xs = \<one>#ys"
1.562      from ind
1.563 -    show "bv_to_int (norm_signed (\<one>#ys)) = - bv_to_nat (bv_not ys) + -1"
1.564 +    show "bv_to_int (norm_signed (\<one>#ys)) = -1 - int (bv_to_nat (bv_not ys))"
1.565        by simp
1.566    qed
1.567  qed
1.568 @@ -1146,15 +1047,16 @@
1.569  lemma bv_to_int_upper_range: "bv_to_int w < 2 ^ (length w - 1)"
1.570  proof (rule bit_list_cases [of w],simp_all)
1.571    fix bs
1.572 -  show "bv_to_nat bs < 2 ^ length bs"
1.573 -    by (rule bv_to_nat_upper_range)
1.574 +  from bv_to_nat_upper_range
1.575 +  show "int (bv_to_nat bs) < 2 ^ length bs"
1.576 +    by (simp add: int_nat_two_exp)
1.577  next
1.578    fix bs
1.579 -  have "- (bv_to_nat (bv_not bs)) + -1 \<le> 0 + 0"
1.581 +  have "-1 - int (bv_to_nat (bv_not bs)) \<le> 0"
1.582 +    by simp
1.583    also have "... < 2 ^ length bs"
1.584      by (induct bs,simp_all)
1.585 -  finally show "- (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs"
1.586 +  finally show "-1 - int (bv_to_nat (bv_not bs)) < 2 ^ length bs"
1.587      .
1.588  qed
1.589
1.590 @@ -1163,19 +1065,15 @@
1.591    fix bs :: "bit list"
1.592    have "- (2 ^ length bs) \<le> (0::int)"
1.593      by (induct bs,simp_all)
1.594 -  also have "... \<le> bv_to_nat bs"
1.595 +  also have "... \<le> int (bv_to_nat bs)"
1.596      by simp
1.597 -  finally show "- (2 ^ length bs) \<le> bv_to_nat bs"
1.598 +  finally show "- (2 ^ length bs) \<le> int (bv_to_nat bs)"
1.599      .
1.600  next
1.601    fix bs
1.602    from bv_to_nat_upper_range [of "bv_not bs"]
1.603 -  have "bv_to_nat (bv_not bs) < 2 ^ length bs"
1.604 -    by simp
1.605 -  hence "bv_to_nat (bv_not bs) + 1 \<le> 2 ^ length bs"
1.606 -    by simp
1.607 -  thus "- (2 ^ length bs) \<le> - bv_to_nat (bv_not bs) + -1"
1.608 -    by simp
1.609 +  show "- (2 ^ length bs) \<le> -1 - int (bv_to_nat (bv_not bs))"
1.610 +    by (simp add: int_nat_two_exp)
1.611  qed
1.612
1.613  lemma int_bv_int [simp]: "int_to_bv (bv_to_int w) = norm_signed w"
1.614 @@ -1195,18 +1093,14 @@
1.615    fix xs
1.616    assume [simp]: "w = \<one>#xs"
1.617    show ?thesis
1.618 -    apply simp
1.619 +    apply (simp del: int_to_bv_lt0)
1.620      apply (rule bit_list_induct [of _ xs])
1.621      apply simp
1.622      apply (subst int_to_bv_lt0)
1.623 -    apply (subgoal_tac "- bv_to_nat (bv_not (\<zero> # bs)) + -1 < 0 + 0")
1.624 +    apply (subgoal_tac "- int (bv_to_nat (bv_not (\<zero> # bs))) + -1 < 0 + 0")
1.625      apply simp
1.627      apply simp
1.628 -    apply (rule order_trans [of _ 0])
1.629 -    apply simp
1.630 -    apply (rule zero_le_power,simp)
1.631 -    apply simp
1.632      apply simp
1.633      apply (simp del: bv_to_nat1 bv_to_nat_helper)
1.634      apply simp
1.635 @@ -1313,16 +1207,10 @@
1.637
1.638  lemma bv_to_int_msb0: "0 \<le> bv_to_int w1 ==> bv_msb w1 = \<zero>"
1.639 -  apply (rule bit_list_cases,simp_all)
1.640 -  apply (subgoal_tac "0 \<le> bv_to_nat (bv_not bs)")
1.641 -  apply simp_all
1.642 -  done
1.643 +  by (rule bit_list_cases,simp_all)
1.644
1.645  lemma bv_to_int_msb1: "bv_to_int w1 < 0 ==> bv_msb w1 = \<one>"
1.646 -  apply (rule bit_list_cases,simp_all)
1.647 -  apply (subgoal_tac "0 \<le> bv_to_nat bs")
1.648 -  apply simp_all
1.649 -  done
1.650 +  by (rule bit_list_cases,simp_all)
1.651
1.652  lemma bv_to_int_lower_limit_gt0:
1.653    assumes w0: "0 < bv_to_int w"
1.654 @@ -1353,8 +1241,7 @@
1.655        have "0 < bv_to_nat w'"
1.656        proof (rule ccontr)
1.657  	assume "~ (0 < bv_to_nat w')"
1.658 -	with bv_to_nat_lower_range [of w']
1.659 -	have "bv_to_nat w' = 0"
1.660 +	hence "bv_to_nat w' = 0"
1.661  	  by arith
1.662  	hence "norm_unsigned w' = []"
1.664 @@ -1363,10 +1250,8 @@
1.665  	  by simp
1.666        qed
1.667        with bv_to_nat_lower_limit [of w']
1.668 -      have "2 ^ (length (norm_unsigned w') - 1) \<le> bv_to_nat w'"
1.669 -	.
1.670 -      thus "2 ^ (length (norm_unsigned w') - Suc 0) \<le> bv_to_nat w'"
1.671 -	by simp
1.672 +      show "2 ^ (length (norm_unsigned w') - Suc 0) \<le> int (bv_to_nat w')"
1.673 +	by (simp add: int_nat_two_exp)
1.674      qed
1.675    next
1.676      fix w'
1.677 @@ -1475,8 +1360,8 @@
1.678  	assume w'eq: "w' = \<zero> # w''"
1.679  	show ?thesis
1.680  	  apply (simp add: weq w'eq)
1.681 -	  apply (subgoal_tac "-bv_to_nat (bv_not w'') + -1 < 0 + 0")
1.682 -	  apply simp
1.683 +	  apply (subgoal_tac "- int (bv_to_nat (bv_not w'')) + -1 < 0 + 0")
1.684 +	  apply (simp add: int_nat_two_exp)
1.686  	  apply simp_all
1.687  	  done
1.688 @@ -1717,7 +1602,7 @@
1.689  lemma utos_length: "length (utos w) \<le> Suc (length w)"
1.690    by (simp add: utos_def norm_signed_Cons)
1.691
1.692 -lemma bv_to_int_utos: "bv_to_int (utos w) = bv_to_nat w"
1.693 +lemma bv_to_int_utos: "bv_to_int (utos w) = int (bv_to_nat w)"
1.694  proof (simp add: utos_def norm_signed_Cons,safe)
1.695    assume "norm_unsigned w = []"
1.696    hence "bv_to_nat (norm_unsigned w) = 0"
1.697 @@ -1804,7 +1689,6 @@
1.698  proof -
1.699    have "-bv_to_int (utos w) = 0 \<or> -bv_to_int (utos w) = -1 \<or> -bv_to_int (utos w) < -1"
1.701 -    apply (cut_tac bv_to_nat_lower_range [of w])
1.702      by arith
1.703    thus ?thesis
1.704    proof safe
1.705 @@ -1823,7 +1707,7 @@
1.706        apply (rule p)
1.708        using bv_to_nat_upper_range [of w]
1.709 -      apply simp
1.710 +      apply (simp add: int_nat_two_exp)
1.711        done
1.712    qed
1.713  qed
1.714 @@ -2203,13 +2087,7 @@
1.715  qed
1.716
1.717  lemma bv_msb_one: "bv_msb w = \<one> ==> 0 < bv_to_nat w"
1.718 -  apply (cases w,simp_all)
1.719 -  apply (subgoal_tac "0 + 0 < 2 ^ length list + bv_to_nat list")
1.720 -  apply simp
1.722 -  apply (rule zero_less_power)
1.723 -  apply simp_all
1.724 -  done
1.725 +  by (cases w,simp_all)
1.726
1.727  lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \<le> length w1 + length w2"
1.728  proof -
1.729 @@ -2241,7 +2119,7 @@
1.730        proof simp
1.731  	have "?Q < 2 ^ length w1 * 2 ^ (length w2 - 1)"
1.732  	  apply (rule mult_strict_mono)
1.733 -	  apply (simp add: bv_to_int_utos)
1.734 +	  apply (simp add: bv_to_int_utos int_nat_two_exp)
1.735  	  apply (rule bv_to_nat_upper_range)
1.736  	  apply (rule bv_to_int_upper_range)
1.737  	  apply (rule zero_less_power,simp)
1.738 @@ -2263,10 +2141,7 @@
1.739      next
1.740        assume "bv_to_int (utos w1) < 0"
1.741        thus ?thesis
1.742 -	apply (simp add: bv_to_int_utos)
1.743 -	using bv_to_nat_lower_range [of w1]
1.744 -	apply simp
1.745 -	done
1.746 +	by (simp add: bv_to_int_utos)
1.747      qed
1.748    next
1.749      assume p: "?Q = -1"
1.750 @@ -2309,7 +2184,7 @@
1.751  	    apply simp
1.753  	    using bv_to_nat_upper_range [of w1]
1.754 -	    apply simp
1.755 +	    apply (simp add: int_nat_two_exp)
1.756  	    apply (rule zero_le_power,simp)
1.757  	    using bi1
1.758  	    apply simp
1.759 @@ -2321,10 +2196,7 @@
1.760  	next
1.761  	  assume bi1: "bv_to_int (utos w1) < 0"
1.762  	  thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
1.763 -	    apply (simp add: bv_to_int_utos)
1.764 -	    using bv_to_nat_lower_range [of w1]
1.765 -	    apply simp
1.766 -	    done
1.767 +	    by (simp add: bv_to_int_utos)
1.768  	qed
1.769        qed
1.770        finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q"
1.771 @@ -2416,7 +2288,7 @@
1.772    by (auto simp add: bv_slice_def,arith)
1.773
1.774  constdefs
1.775 -  length_nat :: "int => nat"
1.776 +  length_nat :: "nat => nat"
1.777    "length_nat x == LEAST n. x < 2 ^ n"
1.778
1.779  lemma length_nat: "length (nat_to_bv n) = length_nat n"
1.780 @@ -2449,22 +2321,23 @@
1.781
1.782  constdefs
1.783    length_int :: "int => nat"
1.784 -  "length_int x == if 0 < x then Suc (length_nat x) else if x = 0 then 0 else Suc (length_nat (-x - 1))"
1.785 +  "length_int x == if 0 < x then Suc (length_nat (nat x)) else if x = 0 then 0 else Suc (length_nat (nat (-x - 1)))"
1.786
1.787  lemma length_int: "length (int_to_bv i) = length_int i"
1.788  proof (cases "0 < i")
1.789    assume i0: "0 < i"
1.790 -  hence "length (int_to_bv i) = length (norm_signed (\<zero> # norm_unsigned (nat_to_bv i)))"
1.791 +  hence "length (int_to_bv i) = length (norm_signed (\<zero> # norm_unsigned (nat_to_bv (nat i))))"
1.792      by simp
1.793 -  also from norm_unsigned_result [of "nat_to_bv i"]
1.794 -  have "... = Suc (length_nat i)"
1.795 +  also from norm_unsigned_result [of "nat_to_bv (nat i)"]
1.796 +  have "... = Suc (length_nat (nat i))"
1.797      apply safe
1.798 -    apply simp
1.799 +    apply (simp del: norm_unsigned_nat_to_bv)
1.800      apply (drule norm_empty_bv_to_nat_zero)
1.801      using prems
1.802      apply simp
1.803 -    apply (cases "norm_unsigned (nat_to_bv i)")
1.804 -    apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv i"])
1.805 +    apply arith
1.806 +    apply (cases "norm_unsigned (nat_to_bv (nat i))")
1.807 +    apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat i)"])
1.808      using prems
1.809      apply simp
1.810      apply simp
1.811 @@ -2488,39 +2361,37 @@
1.812      with i0
1.813      have i0: "i < 0"
1.814        by simp
1.815 -    hence "length (int_to_bv i) = length (norm_signed (\<one> # bv_not (norm_unsigned (nat_to_bv (- i - 1)))))"
1.816 -      by (simp add: int_to_bv_def)
1.817 -    also from norm_unsigned_result [of "nat_to_bv (- i - 1)"]
1.818 -    have "... = Suc (length_nat (- i - 1))"
1.819 +    hence "length (int_to_bv i) = length (norm_signed (\<one> # bv_not (norm_unsigned (nat_to_bv (nat (- i) - 1)))))"
1.820 +      by (simp add: int_to_bv_def nat_diff_distrib)
1.821 +    also from norm_unsigned_result [of "nat_to_bv (nat (- i) - 1)"]
1.822 +    have "... = Suc (length_nat (nat (- i) - 1))"
1.823        apply safe
1.824 -      apply simp
1.825 -      apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (-i - 1)"])
1.826 +      apply (simp del: norm_unsigned_nat_to_bv)
1.827 +      apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat (-i) - Suc 0)"])
1.828        using prems
1.829        apply simp
1.830        apply (cases "- i - 1 = 0")
1.831        apply simp
1.832        apply (simp add: length_nat [symmetric])
1.833 -      apply (cases "norm_unsigned (nat_to_bv (- i - 1))")
1.834 +      apply (cases "norm_unsigned (nat_to_bv (nat (- i) - 1))")
1.835        apply simp
1.836        apply simp
1.837 -      using prems
1.838 -      apply (simp add: length_nat [symmetric])
1.839        done
1.840      finally
1.841      show ?thesis
1.842        using i0
1.843 -      by (simp add: length_int_def)
1.844 +      by (simp add: length_int_def nat_diff_distrib del: int_to_bv_lt0)
1.845    qed
1.846  qed
1.847
1.848  lemma length_int_0 [simp]: "length_int 0 = 0"
1.850
1.851 -lemma length_int_gt0: "0 < i ==> length_int i = Suc (length_nat i)"
1.852 +lemma length_int_gt0: "0 < i ==> length_int i = Suc (length_nat (nat i))"
1.854
1.855 -lemma length_int_lt0: "i < 0 ==> length_int i = Suc (length_nat (- i - 1))"
1.856 -  by (simp add: length_int_def)
1.857 +lemma length_int_lt0: "i < 0 ==> length_int i = Suc (length_nat (nat (- i) - 1))"
1.858 +  by (simp add: length_int_def nat_diff_distrib)
1.859
1.860  lemma bv_chopI: "[| w = w1 @ w2 ; i = length w2 |] ==> bv_chop w i = (w1,w2)"
1.861    by (simp add: bv_chop_def Let_def)
1.862 @@ -2618,11 +2489,9 @@
1.863    have yy: "y < 2 ^ length_nat y"
1.865      apply (rule LeastI)
1.866 -    apply (subgoal_tac "y < 2 ^ (nat y)",assumption)
1.867 +    apply (subgoal_tac "y < 2 ^ y",assumption)
1.868      apply (cases "0 \<le> y")
1.869 -    apply (subgoal_tac "int (nat y) < int (2 ^ nat y)")
1.870 -    apply (simp add: int_nat_two_exp)
1.871 -    apply (induct "nat y",simp_all)
1.872 +    apply (induct y,simp_all)
1.873      done
1.874    with xx
1.875    have "y < x" by simp
1.876 @@ -2640,10 +2509,14 @@
1.878
1.879  lemma length_int_mono_gt0: "[| 0 \<le> x ; x \<le> y |] ==> length_int x \<le> length_int y"
1.880 -  by (cases "x = 0",simp_all add: length_int_gt0)
1.881 +  by (cases "x = 0",simp_all add: length_int_gt0 nat_le_eq_zle)
1.882
1.883  lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x"
1.884 -  by (cases "y = 0",simp_all add: length_int_lt0)
1.885 +  apply (cases "y = 0",simp_all add: length_int_lt0)
1.886 +  apply (subgoal_tac "nat (- y) - Suc 0 \<le> nat (- x) - Suc 0")
1.887 +  apply (simp add: length_nat_mono)
1.888 +  apply arith
1.889 +  done
1.890
1.891  lemmas [simp] = length_nat_non0
1.892
1.893 @@ -2745,12 +2618,12 @@
1.894
1.895  lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)"
1.897 -  have "\<forall> bin. (foldl (%bn b. bn BIT (b = \<one>)) bin bs) = (fast_bv_to_nat_helper bs bin)"
1.898 +  have "\<forall> bin. \<not> (neg (number_of bin :: int)) \<longrightarrow> (foldl (%bn b. 2 * bn + bitval b) (number_of bin) bs) = number_of (fast_bv_to_nat_helper bs bin)"
1.899      apply (induct bs,simp)
1.900      apply (case_tac a,simp_all)
1.901      done
1.902 -  thus "number_of (foldl (%bn b. bn BIT (b = \<one>)) Numeral.Pls bs) == number_of (fast_bv_to_nat_helper bs Numeral.Pls)::int"
1.903 -    by simp
1.904 +  thus "foldl (\<lambda>bn b. 2 * bn + bitval b) 0 bs \<equiv> number_of (fast_bv_to_nat_helper bs Numeral.Pls)"
1.905 +    by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
1.906  qed
1.907
1.908  declare fast_bv_to_nat_Cons [simp del]
1.909 @@ -2776,7 +2649,4 @@
1.910  lemma [simp]: "length w1 = length w2 ==> bv_mapzip f (x#w1) (y#w2) = f x y # bv_mapzip f w1 w2"
1.911    by (simp add: bv_mapzip_def Let_def)
1.912
1.913 -lemma [code]: "bv_to_nat bs = list_rec (0::int) (\<lambda>b bs n. bitval b * 2 ^ length bs + n) bs"
1.914 -  by (induct bs,simp_all add: bv_to_nat_helper)
1.915 -
1.916  end
```