Functions nat_to_bv and bv_to_nat now really operate on natural numbers.
authorberghofe
Wed Nov 24 10:32:33 2004 +0100 (2004-11-24)
changeset 1532550ac7d2c34c9
parent 15324 c27165172e30
child 15326 ff21cddee442
Functions nat_to_bv and bv_to_nat now really operate on natural numbers.
src/HOL/Library/Word.thy
     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.31    by (simp add: bv_to_nat_def)
    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.35 -by (simp add: mult_2) 
    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.73 +      apply (simp add: add_mult_distrib)
    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.98 -  apply (rule add_increasing)
    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.335        by (simp add: add_commute)
   1.336      also have "... = 1"
   1.337 -      by (simp add: zmod_zadd1_eq)
   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.351        by (simp add: add_commute)
   1.352      also have "... = nat_to_bv (bv_to_nat w) @ [\<one>]"
   1.353 -      by (subst zdiv_zadd1_eq,simp)
   1.354 +      by (subst div_add1_eq,simp)
   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.372        apply (simp_all add: norm_empty_bv_to_nat_zero)
   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.436    by (simp add: bv_add_def)
   1.437  
   1.438  lemma [simp]: "norm_unsigned (bv_add w1 w2) = bv_add w1 w2"
   1.439 -  apply (simp add: bv_add_def)
   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.446 +  by (simp add: bv_add_def)
   1.447  
   1.448  lemma bv_add_length: "length (bv_add w1 w2) \<le> Suc (max (length w1) (length w2))"
   1.449  proof (unfold bv_add_def,rule length_nat_to_bv_upper_limit)
   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.475  	by (rule add_right_mono)
   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.491    by (simp add: bv_mult_def)
   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.515    by (simp add: int_to_bv_def)
   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.519    by (simp add: int_to_bv_def)
   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.530    by (simp add: bv_to_int_def)
   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.534    by (simp add: bv_to_int_def)
   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.538    by (simp add: bv_to_int_def)
   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.580 -    by (rule add_mono,simp_all)
   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.626      apply (rule add_le_less_mono)
   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.636    by (simp add: int_to_bv_def)
   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.663  	  by (simp add: bv_to_nat_zero_imp_empty)
   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.685  	  apply (rule add_le_less_mono)
   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.700      apply (simp add: bv_to_int_utos)
   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.707        apply (simp add: bv_to_int_utos)
   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.721 -  apply (rule add_less_le_mono)
   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.752  	    apply (simp add: bv_to_int_utos)
   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.849    by (simp add: length_int_def)
   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.853    by (simp add: length_int_def)
   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.864      apply (simp add: length_nat_def)
   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.877    by (simp add: length_nat_non0)
   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.896  proof (simp add: bv_to_nat_def)
   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