src/HOL/Library/Word.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 34942 d62eddd9e253
child 35175 61255c81da01
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     1 (*  Title:      HOL/Library/Word.thy
     2     Author:     Sebastian Skalberg, TU Muenchen
     3 *)
     4 
     5 header {* Binary Words *}
     6 
     7 theory Word
     8 imports Main
     9 begin
    10 
    11 subsection {* Auxilary Lemmas *}
    12 
    13 lemma max_le [intro!]: "[| x \<le> z; y \<le> z |] ==> max x y \<le> z"
    14   by (simp add: max_def)
    15 
    16 lemma max_mono:
    17   fixes x :: "'a::linorder"
    18   assumes mf: "mono f"
    19   shows       "max (f x) (f y) \<le> f (max x y)"
    20 proof -
    21   from mf and le_maxI1 [of x y]
    22   have fx: "f x \<le> f (max x y)" by (rule monoD)
    23   from mf and le_maxI2 [of y x]
    24   have fy: "f y \<le> f (max x y)" by (rule monoD)
    25   from fx and fy
    26   show "max (f x) (f y) \<le> f (max x y)" by auto
    27 qed
    28 
    29 declare zero_le_power [intro]
    30   and zero_less_power [intro]
    31 
    32 lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)"
    33   by (simp add: zpower_int [symmetric])
    34 
    35 
    36 subsection {* Bits *}
    37 
    38 datatype bit =
    39     Zero ("\<zero>")
    40   | One ("\<one>")
    41 
    42 primrec bitval :: "bit => nat" where
    43     "bitval \<zero> = 0"
    44   | "bitval \<one> = 1"
    45 
    46 primrec bitnot :: "bit => bit" where
    47     bitnot_zero: "(bitnot \<zero>) = \<one>"
    48   | bitnot_one : "(bitnot \<one>)  = \<zero>"
    49 
    50 primrec bitand :: "bit => bit => bit" (infixr "bitand" 35) where
    51     bitand_zero: "(\<zero> bitand y) = \<zero>"
    52   | bitand_one:  "(\<one> bitand y) = y"
    53 
    54 primrec bitor  :: "bit => bit => bit" (infixr "bitor"  30) where
    55     bitor_zero: "(\<zero> bitor y) = y"
    56   | bitor_one:  "(\<one> bitor y) = \<one>"
    57 
    58 primrec bitxor :: "bit => bit => bit" (infixr "bitxor" 30) where
    59     bitxor_zero: "(\<zero> bitxor y) = y"
    60   | bitxor_one:  "(\<one> bitxor y) = (bitnot y)"
    61 
    62 notation (xsymbols)
    63   bitnot ("\<not>\<^sub>b _" [40] 40) and
    64   bitand (infixr "\<and>\<^sub>b" 35) and
    65   bitor  (infixr "\<or>\<^sub>b" 30) and
    66   bitxor (infixr "\<oplus>\<^sub>b" 30)
    67 
    68 notation (HTML output)
    69   bitnot ("\<not>\<^sub>b _" [40] 40) and
    70   bitand (infixr "\<and>\<^sub>b" 35) and
    71   bitor  (infixr "\<or>\<^sub>b" 30) and
    72   bitxor (infixr "\<oplus>\<^sub>b" 30)
    73 
    74 lemma bitnot_bitnot [simp]: "(bitnot (bitnot b)) = b"
    75   by (cases b) simp_all
    76 
    77 lemma bitand_cancel [simp]: "(b bitand b) = b"
    78   by (cases b) simp_all
    79 
    80 lemma bitor_cancel [simp]: "(b bitor b) = b"
    81   by (cases b) simp_all
    82 
    83 lemma bitxor_cancel [simp]: "(b bitxor b) = \<zero>"
    84   by (cases b) simp_all
    85 
    86 
    87 subsection {* Bit Vectors *}
    88 
    89 text {* First, a couple of theorems expressing case analysis and
    90 induction principles for bit vectors. *}
    91 
    92 lemma bit_list_cases:
    93   assumes empty: "w = [] ==> P w"
    94   and     zero:  "!!bs. w = \<zero> # bs ==> P w"
    95   and     one:   "!!bs. w = \<one> # bs ==> P w"
    96   shows   "P w"
    97 proof (cases w)
    98   assume "w = []"
    99   thus ?thesis by (rule empty)
   100 next
   101   fix b bs
   102   assume [simp]: "w = b # bs"
   103   show "P w"
   104   proof (cases b)
   105     assume "b = \<zero>"
   106     hence "w = \<zero> # bs" by simp
   107     thus ?thesis by (rule zero)
   108   next
   109     assume "b = \<one>"
   110     hence "w = \<one> # bs" by simp
   111     thus ?thesis by (rule one)
   112   qed
   113 qed
   114 
   115 lemma bit_list_induct:
   116   assumes empty: "P []"
   117   and     zero:  "!!bs. P bs ==> P (\<zero>#bs)"
   118   and     one:   "!!bs. P bs ==> P (\<one>#bs)"
   119   shows   "P w"
   120 proof (induct w, simp_all add: empty)
   121   fix b bs
   122   assume "P bs"
   123   then show "P (b#bs)"
   124     by (cases b) (auto intro!: zero one)
   125 qed
   126 
   127 definition
   128   bv_msb :: "bit list => bit" where
   129   "bv_msb w = (if w = [] then \<zero> else hd w)"
   130 
   131 definition
   132   bv_extend :: "[nat,bit,bit list]=>bit list" where
   133   "bv_extend i b w = (replicate (i - length w) b) @ w"
   134 
   135 definition
   136   bv_not :: "bit list => bit list" where
   137   "bv_not w = map bitnot w"
   138 
   139 lemma bv_length_extend [simp]: "length w \<le> i ==> length (bv_extend i b w) = i"
   140   by (simp add: bv_extend_def)
   141 
   142 lemma bv_not_Nil [simp]: "bv_not [] = []"
   143   by (simp add: bv_not_def)
   144 
   145 lemma bv_not_Cons [simp]: "bv_not (b#bs) = (bitnot b) # bv_not bs"
   146   by (simp add: bv_not_def)
   147 
   148 lemma bv_not_bv_not [simp]: "bv_not (bv_not w) = w"
   149   by (rule bit_list_induct [of _ w]) simp_all
   150 
   151 lemma bv_msb_Nil [simp]: "bv_msb [] = \<zero>"
   152   by (simp add: bv_msb_def)
   153 
   154 lemma bv_msb_Cons [simp]: "bv_msb (b#bs) = b"
   155   by (simp add: bv_msb_def)
   156 
   157 lemma bv_msb_bv_not [simp]: "0 < length w ==> bv_msb (bv_not w) = (bitnot (bv_msb w))"
   158   by (cases w) simp_all
   159 
   160 lemma bv_msb_one_length [simp,intro]: "bv_msb w = \<one> ==> 0 < length w"
   161   by (cases w) simp_all
   162 
   163 lemma length_bv_not [simp]: "length (bv_not w) = length w"
   164   by (induct w) simp_all
   165 
   166 definition
   167   bv_to_nat :: "bit list => nat" where
   168   "bv_to_nat = foldl (%bn b. 2 * bn + bitval b) 0"
   169 
   170 lemma bv_to_nat_Nil [simp]: "bv_to_nat [] = 0"
   171   by (simp add: bv_to_nat_def)
   172 
   173 lemma bv_to_nat_helper [simp]: "bv_to_nat (b # bs) = bitval b * 2 ^ length bs + bv_to_nat bs"
   174 proof -
   175   let ?bv_to_nat' = "foldl (\<lambda>bn b. 2 * bn + bitval b)"
   176   have helper: "\<And>base. ?bv_to_nat' base bs = base * 2 ^ length bs + ?bv_to_nat' 0 bs"
   177   proof (induct bs)
   178     case Nil
   179     show ?case by simp
   180   next
   181     case (Cons x xs base)
   182     show ?case
   183       apply (simp only: foldl.simps)
   184       apply (subst Cons [of "2 * base + bitval x"])
   185       apply simp
   186       apply (subst Cons [of "bitval x"])
   187       apply (simp add: add_mult_distrib)
   188       done
   189   qed
   190   show ?thesis by (simp add: bv_to_nat_def) (rule helper)
   191 qed
   192 
   193 lemma bv_to_nat0 [simp]: "bv_to_nat (\<zero>#bs) = bv_to_nat bs"
   194   by simp
   195 
   196 lemma bv_to_nat1 [simp]: "bv_to_nat (\<one>#bs) = 2 ^ length bs + bv_to_nat bs"
   197   by simp
   198 
   199 lemma bv_to_nat_upper_range: "bv_to_nat w < 2 ^ length w"
   200 proof (induct w, simp_all)
   201   fix b bs
   202   assume "bv_to_nat bs < 2 ^ length bs"
   203   show "bitval b * 2 ^ length bs + bv_to_nat bs < 2 * 2 ^ length bs"
   204   proof (cases b, simp_all)
   205     have "bv_to_nat bs < 2 ^ length bs" by fact
   206     also have "... < 2 * 2 ^ length bs" by auto
   207     finally show "bv_to_nat bs < 2 * 2 ^ length bs" by simp
   208   next
   209     have "bv_to_nat bs < 2 ^ length bs" by fact
   210     hence "2 ^ length bs + bv_to_nat bs < 2 ^ length bs + 2 ^ length bs" by arith
   211     also have "... = 2 * (2 ^ length bs)" by simp
   212     finally show "bv_to_nat bs < 2 ^ length bs" by simp
   213   qed
   214 qed
   215 
   216 lemma bv_extend_longer [simp]:
   217   assumes wn: "n \<le> length w"
   218   shows       "bv_extend n b w = w"
   219   by (simp add: bv_extend_def wn)
   220 
   221 lemma bv_extend_shorter [simp]:
   222   assumes wn: "length w < n"
   223   shows       "bv_extend n b w = bv_extend n b (b#w)"
   224 proof -
   225   from wn
   226   have s: "n - Suc (length w) + 1 = n - length w"
   227     by arith
   228   have "bv_extend n b w = replicate (n - length w) b @ w"
   229     by (simp add: bv_extend_def)
   230   also have "... = replicate (n - Suc (length w) + 1) b @ w"
   231     by (subst s) rule
   232   also have "... = (replicate (n - Suc (length w)) b @ replicate 1 b) @ w"
   233     by (subst replicate_add) rule
   234   also have "... = replicate (n - Suc (length w)) b @ b # w"
   235     by simp
   236   also have "... = bv_extend n b (b#w)"
   237     by (simp add: bv_extend_def)
   238   finally show "bv_extend n b w = bv_extend n b (b#w)" .
   239 qed
   240 
   241 primrec rem_initial :: "bit => bit list => bit list" where
   242     "rem_initial b [] = []"
   243   | "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)"
   244 
   245 lemma rem_initial_length: "length (rem_initial b w) \<le> length w"
   246   by (rule bit_list_induct [of _ w],simp_all (no_asm),safe,simp_all)
   247 
   248 lemma rem_initial_equal:
   249   assumes p: "length (rem_initial b w) = length w"
   250   shows      "rem_initial b w = w"
   251 proof -
   252   have "length (rem_initial b w) = length w --> rem_initial b w = w"
   253   proof (induct w, simp_all, clarify)
   254     fix xs
   255     assume "length (rem_initial b xs) = length xs --> rem_initial b xs = xs"
   256     assume f: "length (rem_initial b xs) = Suc (length xs)"
   257     with rem_initial_length [of b xs]
   258     show "rem_initial b xs = b#xs"
   259       by auto
   260   qed
   261   from this and p show ?thesis ..
   262 qed
   263 
   264 lemma bv_extend_rem_initial: "bv_extend (length w) b (rem_initial b w) = w"
   265 proof (induct w, simp_all, safe)
   266   fix xs
   267   assume ind: "bv_extend (length xs) b (rem_initial b xs) = xs"
   268   from rem_initial_length [of b xs]
   269   have [simp]: "Suc (length xs) - length (rem_initial b xs) =
   270       1 + (length xs - length (rem_initial b xs))"
   271     by arith
   272   have "bv_extend (Suc (length xs)) b (rem_initial b xs) =
   273       replicate (Suc (length xs) - length (rem_initial b xs)) b @ (rem_initial b xs)"
   274     by (simp add: bv_extend_def)
   275   also have "... =
   276       replicate (1 + (length xs - length (rem_initial b xs))) b @ rem_initial b xs"
   277     by simp
   278   also have "... =
   279       (replicate 1 b @ replicate (length xs - length (rem_initial b xs)) b) @ rem_initial b xs"
   280     by (subst replicate_add) (rule refl)
   281   also have "... = b # bv_extend (length xs) b (rem_initial b xs)"
   282     by (auto simp add: bv_extend_def [symmetric])
   283   also have "... = b # xs"
   284     by (simp add: ind)
   285   finally show "bv_extend (Suc (length xs)) b (rem_initial b xs) = b # xs" .
   286 qed
   287 
   288 lemma rem_initial_append1:
   289   assumes "rem_initial b xs ~= []"
   290   shows   "rem_initial b (xs @ ys) = rem_initial b xs @ ys"
   291   using assms by (induct xs) auto
   292 
   293 lemma rem_initial_append2:
   294   assumes "rem_initial b xs = []"
   295   shows   "rem_initial b (xs @ ys) = rem_initial b ys"
   296   using assms by (induct xs) auto
   297 
   298 definition
   299   norm_unsigned :: "bit list => bit list" where
   300   "norm_unsigned = rem_initial \<zero>"
   301 
   302 lemma norm_unsigned_Nil [simp]: "norm_unsigned [] = []"
   303   by (simp add: norm_unsigned_def)
   304 
   305 lemma norm_unsigned_Cons0 [simp]: "norm_unsigned (\<zero>#bs) = norm_unsigned bs"
   306   by (simp add: norm_unsigned_def)
   307 
   308 lemma norm_unsigned_Cons1 [simp]: "norm_unsigned (\<one>#bs) = \<one>#bs"
   309   by (simp add: norm_unsigned_def)
   310 
   311 lemma norm_unsigned_idem [simp]: "norm_unsigned (norm_unsigned w) = norm_unsigned w"
   312   by (rule bit_list_induct [of _ w],simp_all)
   313 
   314 consts
   315   nat_to_bv_helper :: "nat => bit list => bit list"
   316 recdef nat_to_bv_helper "measure (\<lambda>n. n)"
   317   "nat_to_bv_helper n = (%bs. (if n = 0 then bs
   318                                else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs)))"
   319 
   320 definition
   321   nat_to_bv :: "nat => bit list" where
   322   "nat_to_bv n = nat_to_bv_helper n []"
   323 
   324 lemma nat_to_bv0 [simp]: "nat_to_bv 0 = []"
   325   by (simp add: nat_to_bv_def)
   326 
   327 lemmas [simp del] = nat_to_bv_helper.simps
   328 
   329 lemma n_div_2_cases:
   330   assumes zero: "(n::nat) = 0 ==> R"
   331   and     div : "[| n div 2 < n ; 0 < n |] ==> R"
   332   shows         "R"
   333 proof (cases "n = 0")
   334   assume "n = 0"
   335   thus R by (rule zero)
   336 next
   337   assume "n ~= 0"
   338   hence "0 < n" by simp
   339   hence "n div 2 < n" by arith
   340   from this and `0 < n` show R by (rule div)
   341 qed
   342 
   343 lemma int_wf_ge_induct:
   344   assumes ind :  "!!i::int. (!!j. [| k \<le> j ; j < i |] ==> P j) ==> P i"
   345   shows          "P i"
   346 proof (rule wf_induct_rule [OF wf_int_ge_less_than])
   347   fix x
   348   assume ih: "(\<And>y\<Colon>int. (y, x) \<in> int_ge_less_than k \<Longrightarrow> P y)"
   349   thus "P x"
   350     by (rule ind) (simp add: int_ge_less_than_def)
   351 qed
   352 
   353 lemma unfold_nat_to_bv_helper:
   354   "nat_to_bv_helper b l = nat_to_bv_helper b [] @ l"
   355 proof -
   356   have "\<forall>l. nat_to_bv_helper b l = nat_to_bv_helper b [] @ l"
   357   proof (induct b rule: less_induct)
   358     fix n
   359     assume ind: "!!j. j < n \<Longrightarrow> \<forall> l. nat_to_bv_helper j l = nat_to_bv_helper j [] @ l"
   360     show "\<forall>l. nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
   361     proof
   362       fix l
   363       show "nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
   364       proof (cases "n < 0")
   365         assume "n < 0"
   366         thus ?thesis
   367           by (simp add: nat_to_bv_helper.simps)
   368       next
   369         assume "~n < 0"
   370         show ?thesis
   371         proof (rule n_div_2_cases [of n])
   372           assume [simp]: "n = 0"
   373           show ?thesis
   374             apply (simp only: nat_to_bv_helper.simps [of n])
   375             apply simp
   376             done
   377         next
   378           assume n2n: "n div 2 < n"
   379           assume [simp]: "0 < n"
   380           hence n20: "0 \<le> n div 2"
   381             by arith
   382           from ind [of "n div 2"] and n2n n20
   383           have ind': "\<forall>l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l"
   384             by blast
   385           show ?thesis
   386             apply (simp only: nat_to_bv_helper.simps [of n])
   387             apply (cases "n=0")
   388             apply simp
   389             apply (simp only: if_False)
   390             apply simp
   391             apply (subst spec [OF ind',of "\<zero>#l"])
   392             apply (subst spec [OF ind',of "\<one>#l"])
   393             apply (subst spec [OF ind',of "[\<one>]"])
   394             apply (subst spec [OF ind',of "[\<zero>]"])
   395             apply simp
   396             done
   397         qed
   398       qed
   399     qed
   400   qed
   401   thus ?thesis ..
   402 qed
   403 
   404 lemma nat_to_bv_non0 [simp]: "n\<noteq>0 ==> nat_to_bv n = nat_to_bv (n div 2) @ [if n mod 2 = 0 then \<zero> else \<one>]"
   405 proof -
   406   assume [simp]: "n\<noteq>0"
   407   show ?thesis
   408     apply (subst nat_to_bv_def [of n])
   409     apply (simp only: nat_to_bv_helper.simps [of n])
   410     apply (subst unfold_nat_to_bv_helper)
   411     using prems
   412     apply (simp)
   413     apply (subst nat_to_bv_def [of "n div 2"])
   414     apply auto
   415     done
   416 qed
   417 
   418 lemma bv_to_nat_dist_append:
   419   "bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
   420 proof -
   421   have "\<forall>l2. bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
   422   proof (induct l1, simp_all)
   423     fix x xs
   424     assume ind: "\<forall>l2. bv_to_nat (xs @ l2) = bv_to_nat xs * 2 ^ length l2 + bv_to_nat l2"
   425     show "\<forall>l2::bit list. 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"
   426     proof
   427       fix l2
   428       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"
   429       proof -
   430         have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
   431           by (induct ("length xs")) simp_all
   432         hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 =
   433           bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
   434           by simp
   435         also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
   436           by (simp add: ring_distribs)
   437         finally show ?thesis by simp
   438       qed
   439     qed
   440   qed
   441   thus ?thesis ..
   442 qed
   443 
   444 lemma bv_nat_bv [simp]: "bv_to_nat (nat_to_bv n) = n"
   445 proof (induct n rule: less_induct)
   446   fix n
   447   assume ind: "!!j. j < n \<Longrightarrow> bv_to_nat (nat_to_bv j) = j"
   448   show "bv_to_nat (nat_to_bv n) = n"
   449   proof (rule n_div_2_cases [of n])
   450     assume "n = 0" then show ?thesis by simp
   451   next
   452     assume nn: "n div 2 < n"
   453     assume n0: "0 < n"
   454     from ind and nn
   455     have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2" by blast
   456     from n0 have n0': "n \<noteq> 0" by simp
   457     show ?thesis
   458       apply (subst nat_to_bv_def)
   459       apply (simp only: nat_to_bv_helper.simps [of n])
   460       apply (simp only: n0' if_False)
   461       apply (subst unfold_nat_to_bv_helper)
   462       apply (subst bv_to_nat_dist_append)
   463       apply (fold nat_to_bv_def)
   464       apply (simp add: ind' split del: split_if)
   465       apply (cases "n mod 2 = 0")
   466       proof (simp_all)
   467         assume "n mod 2 = 0"
   468         with mod_div_equality [of n 2]
   469         show "n div 2 * 2 = n" by simp
   470       next
   471         assume "n mod 2 = Suc 0"
   472         with mod_div_equality [of n 2]
   473         show "Suc (n div 2 * 2) = n" by arith
   474       qed
   475   qed
   476 qed
   477 
   478 lemma bv_to_nat_type [simp]: "bv_to_nat (norm_unsigned w) = bv_to_nat w"
   479   by (rule bit_list_induct) simp_all
   480 
   481 lemma length_norm_unsigned_le [simp]: "length (norm_unsigned w) \<le> length w"
   482   by (rule bit_list_induct) simp_all
   483 
   484 lemma bv_to_nat_rew_msb: "bv_msb w = \<one> ==> bv_to_nat w = 2 ^ (length w - 1) + bv_to_nat (tl w)"
   485   by (rule bit_list_cases [of w]) simp_all
   486 
   487 lemma norm_unsigned_result: "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>"
   488 proof (rule length_induct [of _ xs])
   489   fix xs :: "bit list"
   490   assume ind: "\<forall>ys. length ys < length xs --> norm_unsigned ys = [] \<or> bv_msb (norm_unsigned ys) = \<one>"
   491   show "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>"
   492   proof (rule bit_list_cases [of xs],simp_all)
   493     fix bs
   494     assume [simp]: "xs = \<zero>#bs"
   495     from ind
   496     have "length bs < length xs --> norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" ..
   497     thus "norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" by simp
   498   qed
   499 qed
   500 
   501 lemma norm_empty_bv_to_nat_zero:
   502   assumes nw: "norm_unsigned w = []"
   503   shows       "bv_to_nat w = 0"
   504 proof -
   505   have "bv_to_nat w = bv_to_nat (norm_unsigned w)" by simp
   506   also have "... = bv_to_nat []" by (subst nw) (rule refl)
   507   also have "... = 0" by simp
   508   finally show ?thesis .
   509 qed
   510 
   511 lemma bv_to_nat_lower_limit:
   512   assumes w0: "0 < bv_to_nat w"
   513   shows "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat w"
   514 proof -
   515   from w0 and norm_unsigned_result [of w]
   516   have msbw: "bv_msb (norm_unsigned w) = \<one>"
   517     by (auto simp add: norm_empty_bv_to_nat_zero)
   518   have "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat (norm_unsigned w)"
   519     by (subst bv_to_nat_rew_msb [OF msbw],simp)
   520   thus ?thesis by simp
   521 qed
   522 
   523 lemmas [simp del] = nat_to_bv_non0
   524 
   525 lemma norm_unsigned_length [intro!]: "length (norm_unsigned w) \<le> length w"
   526 by (subst norm_unsigned_def,rule rem_initial_length)
   527 
   528 lemma norm_unsigned_equal:
   529   "length (norm_unsigned w) = length w ==> norm_unsigned w = w"
   530 by (simp add: norm_unsigned_def,rule rem_initial_equal)
   531 
   532 lemma bv_extend_norm_unsigned: "bv_extend (length w) \<zero> (norm_unsigned w) = w"
   533 by (simp add: norm_unsigned_def,rule bv_extend_rem_initial)
   534 
   535 lemma norm_unsigned_append1 [simp]:
   536   "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys"
   537 by (simp add: norm_unsigned_def,rule rem_initial_append1)
   538 
   539 lemma norm_unsigned_append2 [simp]:
   540   "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"
   541 by (simp add: norm_unsigned_def,rule rem_initial_append2)
   542 
   543 lemma bv_to_nat_zero_imp_empty:
   544   "bv_to_nat w = 0 \<Longrightarrow> norm_unsigned w = []"
   545 by (atomize (full), induct w rule: bit_list_induct) simp_all
   546 
   547 lemma bv_to_nat_nzero_imp_nempty:
   548   "bv_to_nat w \<noteq> 0 \<Longrightarrow> norm_unsigned w \<noteq> []"
   549 by (induct w rule: bit_list_induct) simp_all
   550 
   551 lemma nat_helper1:
   552   assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
   553   shows        "nat_to_bv (2 * bv_to_nat w + bitval x) = norm_unsigned (w @ [x])"
   554 proof (cases x)
   555   assume [simp]: "x = \<one>"
   556   have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] =
   557       nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\<one>]"
   558     by (simp add: add_commute)
   559   also have "... = nat_to_bv (bv_to_nat w) @ [\<one>]"
   560     by (subst div_add1_eq) simp
   561   also have "... = norm_unsigned w @ [\<one>]"
   562     by (subst ass) (rule refl)
   563   also have "... = norm_unsigned (w @ [\<one>])"
   564     by (cases "norm_unsigned w") simp_all
   565   finally have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])" .
   566   then show ?thesis by (simp add: nat_to_bv_non0)
   567 next
   568   assume [simp]: "x = \<zero>"
   569   show ?thesis
   570   proof (cases "bv_to_nat w = 0")
   571     assume "bv_to_nat w = 0"
   572     thus ?thesis
   573       by (simp add: bv_to_nat_zero_imp_empty)
   574   next
   575     assume "bv_to_nat w \<noteq> 0"
   576     thus ?thesis
   577       apply simp
   578       apply (subst nat_to_bv_non0)
   579       apply simp
   580       apply auto
   581       apply (subst ass)
   582       apply (cases "norm_unsigned w")
   583       apply (simp_all add: norm_empty_bv_to_nat_zero)
   584       done
   585   qed
   586 qed
   587 
   588 lemma nat_helper2: "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs"
   589 proof -
   590   have "\<forall>xs. nat_to_bv (2 ^ length (rev xs) + bv_to_nat (rev xs)) = \<one> # (rev xs)" (is "\<forall>xs. ?P xs")
   591   proof
   592     fix xs
   593     show "?P xs"
   594     proof (rule length_induct [of _ xs])
   595       fix xs :: "bit list"
   596       assume ind: "\<forall>ys. length ys < length xs --> ?P ys"
   597       show "?P xs"
   598       proof (cases xs)
   599         assume "xs = []"
   600         then show ?thesis by (simp add: nat_to_bv_non0)
   601       next
   602         fix y ys
   603         assume [simp]: "xs = y # ys"
   604         show ?thesis
   605           apply simp
   606           apply (subst bv_to_nat_dist_append)
   607           apply simp
   608         proof -
   609           have "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
   610             nat_to_bv (2 * (2 ^ length ys + bv_to_nat (rev ys)) + bitval y)"
   611             by (simp add: add_ac mult_ac)
   612           also have "... = nat_to_bv (2 * (bv_to_nat (\<one>#rev ys)) + bitval y)"
   613             by simp
   614           also have "... = norm_unsigned (\<one>#rev ys) @ [y]"
   615           proof -
   616             from ind
   617             have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = \<one> # rev ys"
   618               by auto
   619             hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = \<one> # rev ys"
   620               by simp
   621             show ?thesis
   622               apply (subst nat_helper1)
   623               apply simp_all
   624               done
   625           qed
   626           also have "... = (\<one>#rev ys) @ [y]"
   627             by simp
   628           also have "... = \<one> # rev ys @ [y]"
   629             by simp
   630           finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
   631               \<one> # rev ys @ [y]" .
   632         qed
   633       qed
   634     qed
   635   qed
   636   hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) =
   637       \<one> # rev (rev xs)" ..
   638   thus ?thesis by simp
   639 qed
   640 
   641 lemma nat_bv_nat [simp]: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
   642 proof (rule bit_list_induct [of _ w],simp_all)
   643   fix xs
   644   assume "nat_to_bv (bv_to_nat xs) = norm_unsigned xs"
   645   have "bv_to_nat xs = bv_to_nat (norm_unsigned xs)" by simp
   646   have "bv_to_nat xs < 2 ^ length xs"
   647     by (rule bv_to_nat_upper_range)
   648   show "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs"
   649     by (rule nat_helper2)
   650 qed
   651 
   652 lemma bv_to_nat_qinj:
   653   assumes one: "bv_to_nat xs = bv_to_nat ys"
   654   and     len: "length xs = length ys"
   655   shows        "xs = ys"
   656 proof -
   657   from one
   658   have "nat_to_bv (bv_to_nat xs) = nat_to_bv (bv_to_nat ys)"
   659     by simp
   660   hence xsys: "norm_unsigned xs = norm_unsigned ys"
   661     by simp
   662   have "xs = bv_extend (length xs) \<zero> (norm_unsigned xs)"
   663     by (simp add: bv_extend_norm_unsigned)
   664   also have "... = bv_extend (length ys) \<zero> (norm_unsigned ys)"
   665     by (simp add: xsys len)
   666   also have "... = ys"
   667     by (simp add: bv_extend_norm_unsigned)
   668   finally show ?thesis .
   669 qed
   670 
   671 lemma norm_unsigned_nat_to_bv [simp]:
   672   "norm_unsigned (nat_to_bv n) = nat_to_bv n"
   673 proof -
   674   have "norm_unsigned (nat_to_bv n) = nat_to_bv (bv_to_nat (norm_unsigned (nat_to_bv n)))"
   675     by (subst nat_bv_nat) simp
   676   also have "... = nat_to_bv n" by simp
   677   finally show ?thesis .
   678 qed
   679 
   680 lemma length_nat_to_bv_upper_limit:
   681   assumes nk: "n \<le> 2 ^ k - 1"
   682   shows       "length (nat_to_bv n) \<le> k"
   683 proof (cases "n = 0")
   684   case True
   685   thus ?thesis
   686     by (simp add: nat_to_bv_def nat_to_bv_helper.simps)
   687 next
   688   case False
   689   hence n0: "0 < n" by simp
   690   show ?thesis
   691   proof (rule ccontr)
   692     assume "~ length (nat_to_bv n) \<le> k"
   693     hence "k < length (nat_to_bv n)" by simp
   694     hence "k \<le> length (nat_to_bv n) - 1" by arith
   695     hence "(2::nat) ^ k \<le> 2 ^ (length (nat_to_bv n) - 1)" by simp
   696     also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)" by simp
   697     also have "... \<le> bv_to_nat (nat_to_bv n)"
   698       by (rule bv_to_nat_lower_limit) (simp add: n0)
   699     also have "... = n" by simp
   700     finally have "2 ^ k \<le> n" .
   701     with n0 have "2 ^ k - 1 < n" by arith
   702     with nk show False by simp
   703   qed
   704 qed
   705 
   706 lemma length_nat_to_bv_lower_limit:
   707   assumes nk: "2 ^ k \<le> n"
   708   shows       "k < length (nat_to_bv n)"
   709 proof (rule ccontr)
   710   assume "~ k < length (nat_to_bv n)"
   711   hence lnk: "length (nat_to_bv n) \<le> k" by simp
   712   have "n = bv_to_nat (nat_to_bv n)" by simp
   713   also have "... < 2 ^ length (nat_to_bv n)"
   714     by (rule bv_to_nat_upper_range)
   715   also from lnk have "... \<le> 2 ^ k" by simp
   716   finally have "n < 2 ^ k" .
   717   with nk show False by simp
   718 qed
   719 
   720 
   721 subsection {* Unsigned Arithmetic Operations *}
   722 
   723 definition
   724   bv_add :: "[bit list, bit list ] => bit list" where
   725   "bv_add w1 w2 = nat_to_bv (bv_to_nat w1 + bv_to_nat w2)"
   726 
   727 lemma bv_add_type1 [simp]: "bv_add (norm_unsigned w1) w2 = bv_add w1 w2"
   728   by (simp add: bv_add_def)
   729 
   730 lemma bv_add_type2 [simp]: "bv_add w1 (norm_unsigned w2) = bv_add w1 w2"
   731   by (simp add: bv_add_def)
   732 
   733 lemma bv_add_returntype [simp]: "norm_unsigned (bv_add w1 w2) = bv_add w1 w2"
   734   by (simp add: bv_add_def)
   735 
   736 lemma bv_add_length: "length (bv_add w1 w2) \<le> Suc (max (length w1) (length w2))"
   737 proof (unfold bv_add_def,rule length_nat_to_bv_upper_limit)
   738   from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2]
   739   have "bv_to_nat w1 + bv_to_nat w2 \<le> (2 ^ length w1 - 1) + (2 ^ length w2 - 1)"
   740     by arith
   741   also have "... \<le>
   742       max (2 ^ length w1 - 1) (2 ^ length w2 - 1) + max (2 ^ length w1 - 1) (2 ^ length w2 - 1)"
   743     by (rule add_mono,safe intro!: le_maxI1 le_maxI2)
   744   also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" by simp
   745   also have "... \<le> 2 ^ Suc (max (length w1) (length w2)) - 2"
   746   proof (cases "length w1 \<le> length w2")
   747     assume w1w2: "length w1 \<le> length w2"
   748     hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" by simp
   749     hence "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1" by arith
   750     with w1w2 show ?thesis
   751       by (simp add: diff_mult_distrib2 split: split_max)
   752   next
   753     assume [simp]: "~ (length w1 \<le> length w2)"
   754     have "~ ((2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1)"
   755     proof
   756       assume "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
   757       hence "((2::nat) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1"
   758         by (rule add_right_mono)
   759       hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" by simp
   760       hence "length w1 \<le> length w2" by simp
   761       thus False by simp
   762     qed
   763     thus ?thesis
   764       by (simp add: diff_mult_distrib2 split: split_max)
   765   qed
   766   finally show "bv_to_nat w1 + bv_to_nat w2 \<le> 2 ^ Suc (max (length w1) (length w2)) - 1"
   767     by arith
   768 qed
   769 
   770 definition
   771   bv_mult :: "[bit list, bit list ] => bit list" where
   772   "bv_mult w1 w2 = nat_to_bv (bv_to_nat w1 * bv_to_nat w2)"
   773 
   774 lemma bv_mult_type1 [simp]: "bv_mult (norm_unsigned w1) w2 = bv_mult w1 w2"
   775   by (simp add: bv_mult_def)
   776 
   777 lemma bv_mult_type2 [simp]: "bv_mult w1 (norm_unsigned w2) = bv_mult w1 w2"
   778   by (simp add: bv_mult_def)
   779 
   780 lemma bv_mult_returntype [simp]: "norm_unsigned (bv_mult w1 w2) = bv_mult w1 w2"
   781   by (simp add: bv_mult_def)
   782 
   783 lemma bv_mult_length: "length (bv_mult w1 w2) \<le> length w1 + length w2"
   784 proof (unfold bv_mult_def,rule length_nat_to_bv_upper_limit)
   785   from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2]
   786   have h: "bv_to_nat w1 \<le> 2 ^ length w1 - 1 \<and> bv_to_nat w2 \<le> 2 ^ length w2 - 1"
   787     by arith
   788   have "bv_to_nat w1 * bv_to_nat w2 \<le> (2 ^ length w1 - 1) * (2 ^ length w2 - 1)"
   789     apply (cut_tac h)
   790     apply (rule mult_mono)
   791     apply auto
   792     done
   793   also have "... < 2 ^ length w1 * 2 ^ length w2"
   794     by (rule mult_strict_mono,auto)
   795   also have "... = 2 ^ (length w1 + length w2)"
   796     by (simp add: power_add)
   797   finally show "bv_to_nat w1 * bv_to_nat w2 \<le> 2 ^ (length w1 + length w2) - 1"
   798     by arith
   799 qed
   800 
   801 subsection {* Signed Vectors *}
   802 
   803 primrec norm_signed :: "bit list => bit list" where
   804     norm_signed_Nil: "norm_signed [] = []"
   805   | norm_signed_Cons: "norm_signed (b#bs) =
   806       (case b of
   807         \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs
   808       | \<one> => b#rem_initial b bs)"
   809 
   810 lemma norm_signed0 [simp]: "norm_signed [\<zero>] = []"
   811   by simp
   812 
   813 lemma norm_signed1 [simp]: "norm_signed [\<one>] = [\<one>]"
   814   by simp
   815 
   816 lemma norm_signed01 [simp]: "norm_signed (\<zero>#\<one>#xs) = \<zero>#\<one>#xs"
   817   by simp
   818 
   819 lemma norm_signed00 [simp]: "norm_signed (\<zero>#\<zero>#xs) = norm_signed (\<zero>#xs)"
   820   by simp
   821 
   822 lemma norm_signed10 [simp]: "norm_signed (\<one>#\<zero>#xs) = \<one>#\<zero>#xs"
   823   by simp
   824 
   825 lemma norm_signed11 [simp]: "norm_signed (\<one>#\<one>#xs) = norm_signed (\<one>#xs)"
   826   by simp
   827 
   828 lemmas [simp del] = norm_signed_Cons
   829 
   830 definition
   831   int_to_bv :: "int => bit list" where
   832   "int_to_bv n = (if 0 \<le> n
   833                  then norm_signed (\<zero>#nat_to_bv (nat n))
   834                  else norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1)))))"
   835 
   836 lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # nat_to_bv (nat n))"
   837   by (simp add: int_to_bv_def)
   838 
   839 lemma int_to_bv_lt0 [simp]:
   840     "n < 0 ==> int_to_bv n = norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1))))"
   841   by (simp add: int_to_bv_def)
   842 
   843 lemma norm_signed_idem [simp]: "norm_signed (norm_signed w) = norm_signed w"
   844 proof (rule bit_list_induct [of _ w], simp_all)
   845   fix xs
   846   assume eq: "norm_signed (norm_signed xs) = norm_signed xs"
   847   show "norm_signed (norm_signed (\<zero>#xs)) = norm_signed (\<zero>#xs)"
   848   proof (rule bit_list_cases [of xs],simp_all)
   849     fix ys
   850     assume "xs = \<zero>#ys"
   851     from this [symmetric] and eq
   852     show "norm_signed (norm_signed (\<zero>#ys)) = norm_signed (\<zero>#ys)"
   853       by simp
   854   qed
   855 next
   856   fix xs
   857   assume eq: "norm_signed (norm_signed xs) = norm_signed xs"
   858   show "norm_signed (norm_signed (\<one>#xs)) = norm_signed (\<one>#xs)"
   859   proof (rule bit_list_cases [of xs],simp_all)
   860     fix ys
   861     assume "xs = \<one>#ys"
   862     from this [symmetric] and eq
   863     show "norm_signed (norm_signed (\<one>#ys)) = norm_signed (\<one>#ys)"
   864       by simp
   865   qed
   866 qed
   867 
   868 definition
   869   bv_to_int :: "bit list => int" where
   870   "bv_to_int w =
   871     (case bv_msb w of \<zero> => int (bv_to_nat w)
   872     | \<one> => - int (bv_to_nat (bv_not w) + 1))"
   873 
   874 lemma bv_to_int_Nil [simp]: "bv_to_int [] = 0"
   875   by (simp add: bv_to_int_def)
   876 
   877 lemma bv_to_int_Cons0 [simp]: "bv_to_int (\<zero>#bs) = int (bv_to_nat bs)"
   878   by (simp add: bv_to_int_def)
   879 
   880 lemma bv_to_int_Cons1 [simp]: "bv_to_int (\<one>#bs) = - int (bv_to_nat (bv_not bs) + 1)"
   881   by (simp add: bv_to_int_def)
   882 
   883 lemma bv_to_int_type [simp]: "bv_to_int (norm_signed w) = bv_to_int w"
   884 proof (rule bit_list_induct [of _ w], simp_all)
   885   fix xs
   886   assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
   887   show "bv_to_int (norm_signed (\<zero>#xs)) = int (bv_to_nat xs)"
   888   proof (rule bit_list_cases [of xs], simp_all)
   889     fix ys
   890     assume [simp]: "xs = \<zero>#ys"
   891     from ind
   892     show "bv_to_int (norm_signed (\<zero>#ys)) = int (bv_to_nat ys)"
   893       by simp
   894   qed
   895 next
   896   fix xs
   897   assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
   898   show "bv_to_int (norm_signed (\<one>#xs)) = -1 - int (bv_to_nat (bv_not xs))"
   899   proof (rule bit_list_cases [of xs], simp_all)
   900     fix ys
   901     assume [simp]: "xs = \<one>#ys"
   902     from ind
   903     show "bv_to_int (norm_signed (\<one>#ys)) = -1 - int (bv_to_nat (bv_not ys))"
   904       by simp
   905   qed
   906 qed
   907 
   908 lemma bv_to_int_upper_range: "bv_to_int w < 2 ^ (length w - 1)"
   909 proof (rule bit_list_cases [of w],simp_all)
   910   fix bs
   911   from bv_to_nat_upper_range
   912   show "int (bv_to_nat bs) < 2 ^ length bs"
   913     by (simp add: int_nat_two_exp)
   914 next
   915   fix bs
   916   have "-1 - int (bv_to_nat (bv_not bs)) \<le> 0" by simp
   917   also have "... < 2 ^ length bs" by (induct bs) simp_all
   918   finally show "-1 - int (bv_to_nat (bv_not bs)) < 2 ^ length bs" .
   919 qed
   920 
   921 lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) \<le> bv_to_int w"
   922 proof (rule bit_list_cases [of w],simp_all)
   923   fix bs :: "bit list"
   924   have "- (2 ^ length bs) \<le> (0::int)" by (induct bs) simp_all
   925   also have "... \<le> int (bv_to_nat bs)" by simp
   926   finally show "- (2 ^ length bs) \<le> int (bv_to_nat bs)" .
   927 next
   928   fix bs
   929   from bv_to_nat_upper_range [of "bv_not bs"]
   930   show "- (2 ^ length bs) \<le> -1 - int (bv_to_nat (bv_not bs))"
   931     by (simp add: int_nat_two_exp)
   932 qed
   933 
   934 lemma int_bv_int [simp]: "int_to_bv (bv_to_int w) = norm_signed w"
   935 proof (rule bit_list_cases [of w],simp)
   936   fix xs
   937   assume [simp]: "w = \<zero>#xs"
   938   show ?thesis
   939     apply simp
   940     apply (subst norm_signed_Cons [of "\<zero>" "xs"])
   941     apply simp
   942     using norm_unsigned_result [of xs]
   943     apply safe
   944     apply (rule bit_list_cases [of "norm_unsigned xs"])
   945     apply simp_all
   946     done
   947 next
   948   fix xs
   949   assume [simp]: "w = \<one>#xs"
   950   show ?thesis
   951     apply (simp del: int_to_bv_lt0)
   952     apply (rule bit_list_induct [of _ xs])
   953     apply simp
   954     apply (subst int_to_bv_lt0)
   955     apply (subgoal_tac "- int (bv_to_nat (bv_not (\<zero> # bs))) + -1 < 0 + 0")
   956     apply simp
   957     apply (rule add_le_less_mono)
   958     apply simp
   959     apply simp
   960     apply (simp del: bv_to_nat1 bv_to_nat_helper)
   961     apply simp
   962     done
   963 qed
   964 
   965 lemma bv_int_bv [simp]: "bv_to_int (int_to_bv i) = i"
   966   by (cases "0 \<le> i") simp_all
   967 
   968 lemma bv_msb_norm [simp]: "bv_msb (norm_signed w) = bv_msb w"
   969   by (rule bit_list_cases [of w]) (simp_all add: norm_signed_Cons)
   970 
   971 lemma norm_signed_length: "length (norm_signed w) \<le> length w"
   972   apply (cases w, simp_all)
   973   apply (subst norm_signed_Cons)
   974   apply (case_tac a, simp_all)
   975   apply (rule rem_initial_length)
   976   done
   977 
   978 lemma norm_signed_equal: "length (norm_signed w) = length w ==> norm_signed w = w"
   979 proof (rule bit_list_cases [of w], simp_all)
   980   fix xs
   981   assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)"
   982   thus "norm_signed (\<zero>#xs) = \<zero>#xs"
   983     by (simp add: norm_signed_Cons norm_unsigned_equal split: split_if_asm)
   984 next
   985   fix xs
   986   assume "length (norm_signed (\<one>#xs)) = Suc (length xs)"
   987   thus "norm_signed (\<one>#xs) = \<one>#xs"
   988     apply (simp add: norm_signed_Cons)
   989     apply (rule rem_initial_equal)
   990     apply assumption
   991     done
   992 qed
   993 
   994 lemma bv_extend_norm_signed: "bv_msb w = b ==> bv_extend (length w) b (norm_signed w) = w"
   995 proof (rule bit_list_cases [of w],simp_all)
   996   fix xs
   997   show "bv_extend (Suc (length xs)) \<zero> (norm_signed (\<zero>#xs)) = \<zero>#xs"
   998   proof (simp add: norm_signed_def,auto)
   999     assume "norm_unsigned xs = []"
  1000     hence xx: "rem_initial \<zero> xs = []"
  1001       by (simp add: norm_unsigned_def)
  1002     have "bv_extend (Suc (length xs)) \<zero> (\<zero>#rem_initial \<zero> xs) = \<zero>#xs"
  1003       apply (simp add: bv_extend_def replicate_app_Cons_same)
  1004       apply (fold bv_extend_def)
  1005       apply (rule bv_extend_rem_initial)
  1006       done
  1007     thus "bv_extend (Suc (length xs)) \<zero> [\<zero>] = \<zero>#xs"
  1008       by (simp add: xx)
  1009   next
  1010     show "bv_extend (Suc (length xs)) \<zero> (\<zero>#norm_unsigned xs) = \<zero>#xs"
  1011       apply (simp add: norm_unsigned_def)
  1012       apply (simp add: bv_extend_def replicate_app_Cons_same)
  1013       apply (fold bv_extend_def)
  1014       apply (rule bv_extend_rem_initial)
  1015       done
  1016   qed
  1017 next
  1018   fix xs
  1019   show "bv_extend (Suc (length xs)) \<one> (norm_signed (\<one>#xs)) = \<one>#xs"
  1020     apply (simp add: norm_signed_Cons)
  1021     apply (simp add: bv_extend_def replicate_app_Cons_same)
  1022     apply (fold bv_extend_def)
  1023     apply (rule bv_extend_rem_initial)
  1024     done
  1025 qed
  1026 
  1027 lemma bv_to_int_qinj:
  1028   assumes one: "bv_to_int xs = bv_to_int ys"
  1029   and     len: "length xs = length ys"
  1030   shows        "xs = ys"
  1031 proof -
  1032   from one
  1033   have "int_to_bv (bv_to_int xs) = int_to_bv (bv_to_int ys)" by simp
  1034   hence xsys: "norm_signed xs = norm_signed ys" by simp
  1035   hence xsys': "bv_msb xs = bv_msb ys"
  1036   proof -
  1037     have "bv_msb xs = bv_msb (norm_signed xs)" by simp
  1038     also have "... = bv_msb (norm_signed ys)" by (simp add: xsys)
  1039     also have "... = bv_msb ys" by simp
  1040     finally show ?thesis .
  1041   qed
  1042   have "xs = bv_extend (length xs) (bv_msb xs) (norm_signed xs)"
  1043     by (simp add: bv_extend_norm_signed)
  1044   also have "... = bv_extend (length ys) (bv_msb ys) (norm_signed ys)"
  1045     by (simp add: xsys xsys' len)
  1046   also have "... = ys"
  1047     by (simp add: bv_extend_norm_signed)
  1048   finally show ?thesis .
  1049 qed
  1050 
  1051 lemma int_to_bv_returntype [simp]: "norm_signed (int_to_bv w) = int_to_bv w"
  1052   by (simp add: int_to_bv_def)
  1053 
  1054 lemma bv_to_int_msb0: "0 \<le> bv_to_int w1 ==> bv_msb w1 = \<zero>"
  1055   by (rule bit_list_cases,simp_all)
  1056 
  1057 lemma bv_to_int_msb1: "bv_to_int w1 < 0 ==> bv_msb w1 = \<one>"
  1058   by (rule bit_list_cases,simp_all)
  1059 
  1060 lemma bv_to_int_lower_limit_gt0:
  1061   assumes w0: "0 < bv_to_int w"
  1062   shows       "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int w"
  1063 proof -
  1064   from w0
  1065   have "0 \<le> bv_to_int w" by simp
  1066   hence [simp]: "bv_msb w = \<zero>" by (rule bv_to_int_msb0)
  1067   have "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int (norm_signed w)"
  1068   proof (rule bit_list_cases [of w])
  1069     assume "w = []"
  1070     with w0 show ?thesis by simp
  1071   next
  1072     fix w'
  1073     assume weq: "w = \<zero> # w'"
  1074     thus ?thesis
  1075     proof (simp add: norm_signed_Cons,safe)
  1076       assume "norm_unsigned w' = []"
  1077       with weq and w0 show False
  1078         by (simp add: norm_empty_bv_to_nat_zero)
  1079     next
  1080       assume w'0: "norm_unsigned w' \<noteq> []"
  1081       have "0 < bv_to_nat w'"
  1082       proof (rule ccontr)
  1083         assume "~ (0 < bv_to_nat w')"
  1084         hence "bv_to_nat w' = 0"
  1085           by arith
  1086         hence "norm_unsigned w' = []"
  1087           by (simp add: bv_to_nat_zero_imp_empty)
  1088         with w'0
  1089         show False by simp
  1090       qed
  1091       with bv_to_nat_lower_limit [of w']
  1092       show "2 ^ (length (norm_unsigned w') - Suc 0) \<le> int (bv_to_nat w')"
  1093         by (simp add: int_nat_two_exp)
  1094     qed
  1095   next
  1096     fix w'
  1097     assume "w = \<one> # w'"
  1098     from w0 have "bv_msb w = \<zero>" by simp
  1099     with prems show ?thesis by simp
  1100   qed
  1101   also have "...  = bv_to_int w" by simp
  1102   finally show ?thesis .
  1103 qed
  1104 
  1105 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))"
  1106   apply (rule bit_list_cases [of w],simp_all)
  1107   apply (case_tac "bs",simp_all)
  1108   apply (case_tac "a",simp_all)
  1109   apply (simp add: norm_signed_Cons)
  1110   apply safe
  1111   apply simp
  1112 proof -
  1113   fix l
  1114   assume msb: "\<zero> = bv_msb (norm_unsigned l)"
  1115   assume "norm_unsigned l \<noteq> []"
  1116   with norm_unsigned_result [of l]
  1117   have "bv_msb (norm_unsigned l) = \<one>" by simp
  1118   with msb show False by simp
  1119 next
  1120   fix xs
  1121   assume p: "\<one> = bv_msb (tl (norm_signed (\<one> # xs)))"
  1122   have "\<one> \<noteq> bv_msb (tl (norm_signed (\<one> # xs)))"
  1123     by (rule bit_list_induct [of _ xs],simp_all)
  1124   with p show False by simp
  1125 qed
  1126 
  1127 lemma bv_to_int_upper_limit_lem1:
  1128   assumes w0: "bv_to_int w < -1"
  1129   shows       "bv_to_int w < - (2 ^ (length (norm_signed w) - 2))"
  1130 proof -
  1131   from w0
  1132   have "bv_to_int w < 0" by simp
  1133   hence msbw [simp]: "bv_msb w = \<one>"
  1134     by (rule bv_to_int_msb1)
  1135   have "bv_to_int w = bv_to_int (norm_signed w)" by simp
  1136   also from norm_signed_result [of w]
  1137   have "... < - (2 ^ (length (norm_signed w) - 2))"
  1138   proof safe
  1139     assume "norm_signed w = []"
  1140     hence "bv_to_int (norm_signed w) = 0" by simp
  1141     with w0 show ?thesis by simp
  1142   next
  1143     assume "norm_signed w = [\<one>]"
  1144     hence "bv_to_int (norm_signed w) = -1" by simp
  1145     with w0 show ?thesis by simp
  1146   next
  1147     assume "bv_msb (norm_signed w) \<noteq> bv_msb (tl (norm_signed w))"
  1148     hence msb_tl: "\<one> \<noteq> bv_msb (tl (norm_signed w))" by simp
  1149     show "bv_to_int (norm_signed w) < - (2 ^ (length (norm_signed w) - 2))"
  1150     proof (rule bit_list_cases [of "norm_signed w"])
  1151       assume "norm_signed w = []"
  1152       hence "bv_to_int (norm_signed w) = 0" by simp
  1153       with w0 show ?thesis by simp
  1154     next
  1155       fix w'
  1156       assume nw: "norm_signed w = \<zero> # w'"
  1157       from msbw have "bv_msb (norm_signed w) = \<one>" by simp
  1158       with nw show ?thesis by simp
  1159     next
  1160       fix w'
  1161       assume weq: "norm_signed w = \<one> # w'"
  1162       show ?thesis
  1163       proof (rule bit_list_cases [of w'])
  1164         assume w'eq: "w' = []"
  1165         from w0 have "bv_to_int (norm_signed w) < -1" by simp
  1166         with w'eq and weq show ?thesis by simp
  1167       next
  1168         fix w''
  1169         assume w'eq: "w' = \<zero> # w''"
  1170         show ?thesis
  1171           apply (simp add: weq w'eq)
  1172           apply (subgoal_tac "- int (bv_to_nat (bv_not w'')) + -1 < 0 + 0")
  1173           apply (simp add: int_nat_two_exp)
  1174           apply (rule add_le_less_mono)
  1175           apply simp_all
  1176           done
  1177       next
  1178         fix w''
  1179         assume w'eq: "w' = \<one> # w''"
  1180         with weq and msb_tl show ?thesis by simp
  1181       qed
  1182     qed
  1183   qed
  1184   finally show ?thesis .
  1185 qed
  1186 
  1187 lemma length_int_to_bv_upper_limit_gt0:
  1188   assumes w0: "0 < i"
  1189   and     wk: "i \<le> 2 ^ (k - 1) - 1"
  1190   shows       "length (int_to_bv i) \<le> k"
  1191 proof (rule ccontr)
  1192   from w0 wk
  1193   have k1: "1 < k"
  1194     by (cases "k - 1",simp_all)
  1195   assume "~ length (int_to_bv i) \<le> k"
  1196   hence "k < length (int_to_bv i)" by simp
  1197   hence "k \<le> length (int_to_bv i) - 1" by arith
  1198   hence a: "k - 1 \<le> length (int_to_bv i) - 2" by arith
  1199   hence "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" by simp
  1200   also have "... \<le> i"
  1201   proof -
  1202     have "2 ^ (length (norm_signed (int_to_bv i)) - 2) \<le> bv_to_int (int_to_bv i)"
  1203     proof (rule bv_to_int_lower_limit_gt0)
  1204       from w0 show "0 < bv_to_int (int_to_bv i)" by simp
  1205     qed
  1206     thus ?thesis by simp
  1207   qed
  1208   finally have "2 ^ (k - 1) \<le> i" .
  1209   with wk show False by simp
  1210 qed
  1211 
  1212 lemma pos_length_pos:
  1213   assumes i0: "0 < bv_to_int w"
  1214   shows       "0 < length w"
  1215 proof -
  1216   from norm_signed_result [of w]
  1217   have "0 < length (norm_signed w)"
  1218   proof (auto)
  1219     assume ii: "norm_signed w = []"
  1220     have "bv_to_int (norm_signed w) = 0" by (subst ii) simp
  1221     hence "bv_to_int w = 0" by simp
  1222     with i0 show False by simp
  1223   next
  1224     assume ii: "norm_signed w = []"
  1225     assume jj: "bv_msb w \<noteq> \<zero>"
  1226     have "\<zero> = bv_msb (norm_signed w)"
  1227       by (subst ii) simp
  1228     also have "... \<noteq> \<zero>"
  1229       by (simp add: jj)
  1230     finally show False by simp
  1231   qed
  1232   also have "... \<le> length w"
  1233     by (rule norm_signed_length)
  1234   finally show ?thesis .
  1235 qed
  1236 
  1237 lemma neg_length_pos:
  1238   assumes i0: "bv_to_int w < -1"
  1239   shows       "0 < length w"
  1240 proof -
  1241   from norm_signed_result [of w]
  1242   have "0 < length (norm_signed w)"
  1243   proof (auto)
  1244     assume ii: "norm_signed w = []"
  1245     have "bv_to_int (norm_signed w) = 0"
  1246       by (subst ii) simp
  1247     hence "bv_to_int w = 0" by simp
  1248     with i0 show False by simp
  1249   next
  1250     assume ii: "norm_signed w = []"
  1251     assume jj: "bv_msb w \<noteq> \<zero>"
  1252     have "\<zero> = bv_msb (norm_signed w)" by (subst ii) simp
  1253     also have "... \<noteq> \<zero>" by (simp add: jj)
  1254     finally show False by simp
  1255   qed
  1256   also have "... \<le> length w"
  1257     by (rule norm_signed_length)
  1258   finally show ?thesis .
  1259 qed
  1260 
  1261 lemma length_int_to_bv_lower_limit_gt0:
  1262   assumes wk: "2 ^ (k - 1) \<le> i"
  1263   shows       "k < length (int_to_bv i)"
  1264 proof (rule ccontr)
  1265   have "0 < (2::int) ^ (k - 1)"
  1266     by (rule zero_less_power) simp
  1267   also have "... \<le> i" by (rule wk)
  1268   finally have i0: "0 < i" .
  1269   have lii0: "0 < length (int_to_bv i)"
  1270     apply (rule pos_length_pos)
  1271     apply (simp,rule i0)
  1272     done
  1273   assume "~ k < length (int_to_bv i)"
  1274   hence "length (int_to_bv i) \<le> k" by simp
  1275   with lii0
  1276   have a: "length (int_to_bv i) - 1 \<le> k - 1"
  1277     by arith
  1278   have "i < 2 ^ (length (int_to_bv i) - 1)"
  1279   proof -
  1280     have "i = bv_to_int (int_to_bv i)"
  1281       by simp
  1282     also have "... < 2 ^ (length (int_to_bv i) - 1)"
  1283       by (rule bv_to_int_upper_range)
  1284     finally show ?thesis .
  1285   qed
  1286   also have "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" using a
  1287     by simp
  1288   finally have "i < 2 ^ (k - 1)" .
  1289   with wk show False by simp
  1290 qed
  1291 
  1292 lemma length_int_to_bv_upper_limit_lem1:
  1293   assumes w1: "i < -1"
  1294   and     wk: "- (2 ^ (k - 1)) \<le> i"
  1295   shows       "length (int_to_bv i) \<le> k"
  1296 proof (rule ccontr)
  1297   from w1 wk
  1298   have k1: "1 < k" by (cases "k - 1") simp_all
  1299   assume "~ length (int_to_bv i) \<le> k"
  1300   hence "k < length (int_to_bv i)" by simp
  1301   hence "k \<le> length (int_to_bv i) - 1" by arith
  1302   hence a: "k - 1 \<le> length (int_to_bv i) - 2" by arith
  1303   have "i < - (2 ^ (length (int_to_bv i) - 2))"
  1304   proof -
  1305     have "i = bv_to_int (int_to_bv i)"
  1306       by simp
  1307     also have "... < - (2 ^ (length (norm_signed (int_to_bv i)) - 2))"
  1308       by (rule bv_to_int_upper_limit_lem1,simp,rule w1)
  1309     finally show ?thesis by simp
  1310   qed
  1311   also have "... \<le> -(2 ^ (k - 1))"
  1312   proof -
  1313     have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" using a by simp
  1314     thus ?thesis by simp
  1315   qed
  1316   finally have "i < -(2 ^ (k - 1))" .
  1317   with wk show False by simp
  1318 qed
  1319 
  1320 lemma length_int_to_bv_lower_limit_lem1:
  1321   assumes wk: "i < -(2 ^ (k - 1))"
  1322   shows       "k < length (int_to_bv i)"
  1323 proof (rule ccontr)
  1324   from wk have "i \<le> -(2 ^ (k - 1)) - 1" by simp
  1325   also have "... < -1"
  1326   proof -
  1327     have "0 < (2::int) ^ (k - 1)"
  1328       by (rule zero_less_power) simp
  1329     hence "-((2::int) ^ (k - 1)) < 0" by simp
  1330     thus ?thesis by simp
  1331   qed
  1332   finally have i1: "i < -1" .
  1333   have lii0: "0 < length (int_to_bv i)"
  1334     apply (rule neg_length_pos)
  1335     apply (simp, rule i1)
  1336     done
  1337   assume "~ k < length (int_to_bv i)"
  1338   hence "length (int_to_bv i) \<le> k"
  1339     by simp
  1340   with lii0 have a: "length (int_to_bv i) - 1 \<le> k - 1" by arith
  1341   hence "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" by simp
  1342   hence "-((2::int) ^ (k - 1)) \<le> - (2 ^ (length (int_to_bv i) - 1))" by simp
  1343   also have "... \<le> i"
  1344   proof -
  1345     have "- (2 ^ (length (int_to_bv i) - 1)) \<le> bv_to_int (int_to_bv i)"
  1346       by (rule bv_to_int_lower_range)
  1347     also have "... = i"
  1348       by simp
  1349     finally show ?thesis .
  1350   qed
  1351   finally have "-(2 ^ (k - 1)) \<le> i" .
  1352   with wk show False by simp
  1353 qed
  1354 
  1355 
  1356 subsection {* Signed Arithmetic Operations *}
  1357 
  1358 subsubsection {* Conversion from unsigned to signed *}
  1359 
  1360 definition
  1361   utos :: "bit list => bit list" where
  1362   "utos w = norm_signed (\<zero> # w)"
  1363 
  1364 lemma utos_type [simp]: "utos (norm_unsigned w) = utos w"
  1365   by (simp add: utos_def norm_signed_Cons)
  1366 
  1367 lemma utos_returntype [simp]: "norm_signed (utos w) = utos w"
  1368   by (simp add: utos_def)
  1369 
  1370 lemma utos_length: "length (utos w) \<le> Suc (length w)"
  1371   by (simp add: utos_def norm_signed_Cons)
  1372 
  1373 lemma bv_to_int_utos: "bv_to_int (utos w) = int (bv_to_nat w)"
  1374 proof (simp add: utos_def norm_signed_Cons, safe)
  1375   assume "norm_unsigned w = []"
  1376   hence "bv_to_nat (norm_unsigned w) = 0" by simp
  1377   thus "bv_to_nat w = 0" by simp
  1378 qed
  1379 
  1380 
  1381 subsubsection {* Unary minus *}
  1382 
  1383 definition
  1384   bv_uminus :: "bit list => bit list" where
  1385   "bv_uminus w = int_to_bv (- bv_to_int w)"
  1386 
  1387 lemma bv_uminus_type [simp]: "bv_uminus (norm_signed w) = bv_uminus w"
  1388   by (simp add: bv_uminus_def)
  1389 
  1390 lemma bv_uminus_returntype [simp]: "norm_signed (bv_uminus w) = bv_uminus w"
  1391   by (simp add: bv_uminus_def)
  1392 
  1393 lemma bv_uminus_length: "length (bv_uminus w) \<le> Suc (length w)"
  1394 proof -
  1395   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"
  1396     by arith
  1397   thus ?thesis
  1398   proof safe
  1399     assume p: "1 < - bv_to_int w"
  1400     have lw: "0 < length w"
  1401       apply (rule neg_length_pos)
  1402       using p
  1403       apply simp
  1404       done
  1405     show ?thesis
  1406     proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all)
  1407       from prems show "bv_to_int w < 0" by simp
  1408     next
  1409       have "-(2^(length w - 1)) \<le> bv_to_int w"
  1410         by (rule bv_to_int_lower_range)
  1411       hence "- bv_to_int w \<le> 2^(length w - 1)" by simp
  1412       also from lw have "... < 2 ^ length w" by simp
  1413       finally show "- bv_to_int w < 2 ^ length w" by simp
  1414     qed
  1415   next
  1416     assume p: "- bv_to_int w = 1"
  1417     hence lw: "0 < length w" by (cases w) simp_all
  1418     from p
  1419     show ?thesis
  1420       apply (simp add: bv_uminus_def)
  1421       using lw
  1422       apply (simp (no_asm) add: nat_to_bv_non0)
  1423       done
  1424   next
  1425     assume "- bv_to_int w = 0"
  1426     thus ?thesis by (simp add: bv_uminus_def)
  1427   next
  1428     assume p: "- bv_to_int w = -1"
  1429     thus ?thesis by (simp add: bv_uminus_def)
  1430   next
  1431     assume p: "- bv_to_int w < -1"
  1432     show ?thesis
  1433       apply (simp add: bv_uminus_def)
  1434       apply (rule length_int_to_bv_upper_limit_lem1)
  1435       apply (rule p)
  1436       apply simp
  1437     proof -
  1438       have "bv_to_int w < 2 ^ (length w - 1)"
  1439         by (rule bv_to_int_upper_range)
  1440       also have "... \<le> 2 ^ length w" by simp
  1441       finally show "bv_to_int w \<le> 2 ^ length w" by simp
  1442     qed
  1443   qed
  1444 qed
  1445 
  1446 lemma bv_uminus_length_utos: "length (bv_uminus (utos w)) \<le> Suc (length w)"
  1447 proof -
  1448   have "-bv_to_int (utos w) = 0 \<or> -bv_to_int (utos w) = -1 \<or> -bv_to_int (utos w) < -1"
  1449     by (simp add: bv_to_int_utos, arith)
  1450   thus ?thesis
  1451   proof safe
  1452     assume "-bv_to_int (utos w) = 0"
  1453     thus ?thesis by (simp add: bv_uminus_def)
  1454   next
  1455     assume "-bv_to_int (utos w) = -1"
  1456     thus ?thesis by (simp add: bv_uminus_def)
  1457   next
  1458     assume p: "-bv_to_int (utos w) < -1"
  1459     show ?thesis
  1460       apply (simp add: bv_uminus_def)
  1461       apply (rule length_int_to_bv_upper_limit_lem1)
  1462       apply (rule p)
  1463       apply (simp add: bv_to_int_utos)
  1464       using bv_to_nat_upper_range [of w]
  1465       apply (simp add: int_nat_two_exp)
  1466       done
  1467   qed
  1468 qed
  1469 
  1470 definition
  1471   bv_sadd :: "[bit list, bit list ] => bit list" where
  1472   "bv_sadd w1 w2 = int_to_bv (bv_to_int w1 + bv_to_int w2)"
  1473 
  1474 lemma bv_sadd_type1 [simp]: "bv_sadd (norm_signed w1) w2 = bv_sadd w1 w2"
  1475   by (simp add: bv_sadd_def)
  1476 
  1477 lemma bv_sadd_type2 [simp]: "bv_sadd w1 (norm_signed w2) = bv_sadd w1 w2"
  1478   by (simp add: bv_sadd_def)
  1479 
  1480 lemma bv_sadd_returntype [simp]: "norm_signed (bv_sadd w1 w2) = bv_sadd w1 w2"
  1481   by (simp add: bv_sadd_def)
  1482 
  1483 lemma adder_helper:
  1484   assumes lw: "0 < max (length w1) (length w2)"
  1485   shows   "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le> 2 ^ max (length w1) (length w2)"
  1486 proof -
  1487   have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le>
  1488       2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)"
  1489     by (auto simp:max_def)
  1490   also have "... = 2 ^ max (length w1) (length w2)"
  1491   proof -
  1492     from lw
  1493     show ?thesis
  1494       apply simp
  1495       apply (subst power_Suc [symmetric])
  1496       apply simp
  1497       done
  1498   qed
  1499   finally show ?thesis .
  1500 qed
  1501 
  1502 lemma bv_sadd_length: "length (bv_sadd w1 w2) \<le> Suc (max (length w1) (length w2))"
  1503 proof -
  1504   let ?Q = "bv_to_int w1 + bv_to_int w2"
  1505 
  1506   have helper: "?Q \<noteq> 0 ==> 0 < max (length w1) (length w2)"
  1507   proof -
  1508     assume p: "?Q \<noteq> 0"
  1509     show "0 < max (length w1) (length w2)"
  1510     proof (simp add: less_max_iff_disj,rule)
  1511       assume [simp]: "w1 = []"
  1512       show "w2 \<noteq> []"
  1513       proof (rule ccontr,simp)
  1514         assume [simp]: "w2 = []"
  1515         from p show False by simp
  1516       qed
  1517     qed
  1518   qed
  1519 
  1520   have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
  1521   thus ?thesis
  1522   proof safe
  1523     assume "?Q = 0"
  1524     thus ?thesis
  1525       by (simp add: bv_sadd_def)
  1526   next
  1527     assume "?Q = -1"
  1528     thus ?thesis
  1529       by (simp add: bv_sadd_def)
  1530   next
  1531     assume p: "0 < ?Q"
  1532     show ?thesis
  1533       apply (simp add: bv_sadd_def)
  1534       apply (rule length_int_to_bv_upper_limit_gt0)
  1535       apply (rule p)
  1536     proof simp
  1537       from bv_to_int_upper_range [of w2]
  1538       have "bv_to_int w2 \<le> 2 ^ (length w2 - 1)"
  1539         by simp
  1540       with bv_to_int_upper_range [of w1]
  1541       have "bv_to_int w1 + bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
  1542         by (rule zadd_zless_mono)
  1543       also have "... \<le> 2 ^ max (length w1) (length w2)"
  1544         apply (rule adder_helper)
  1545         apply (rule helper)
  1546         using p
  1547         apply simp
  1548         done
  1549       finally show "?Q < 2 ^ max (length w1) (length w2)" .
  1550     qed
  1551   next
  1552     assume p: "?Q < -1"
  1553     show ?thesis
  1554       apply (simp add: bv_sadd_def)
  1555       apply (rule length_int_to_bv_upper_limit_lem1,simp_all)
  1556       apply (rule p)
  1557     proof -
  1558       have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)"
  1559         apply (rule adder_helper)
  1560         apply (rule helper)
  1561         using p
  1562         apply simp
  1563         done
  1564       hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
  1565         by simp
  1566       also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> ?Q"
  1567         apply (rule add_mono)
  1568         apply (rule bv_to_int_lower_range [of w1])
  1569         apply (rule bv_to_int_lower_range [of w2])
  1570         done
  1571       finally show "- (2^max (length w1) (length w2)) \<le> ?Q" .
  1572     qed
  1573   qed
  1574 qed
  1575 
  1576 definition
  1577   bv_sub :: "[bit list, bit list] => bit list" where
  1578   "bv_sub w1 w2 = bv_sadd w1 (bv_uminus w2)"
  1579 
  1580 lemma bv_sub_type1 [simp]: "bv_sub (norm_signed w1) w2 = bv_sub w1 w2"
  1581   by (simp add: bv_sub_def)
  1582 
  1583 lemma bv_sub_type2 [simp]: "bv_sub w1 (norm_signed w2) = bv_sub w1 w2"
  1584   by (simp add: bv_sub_def)
  1585 
  1586 lemma bv_sub_returntype [simp]: "norm_signed (bv_sub w1 w2) = bv_sub w1 w2"
  1587   by (simp add: bv_sub_def)
  1588 
  1589 lemma bv_sub_length: "length (bv_sub w1 w2) \<le> Suc (max (length w1) (length w2))"
  1590 proof (cases "bv_to_int w2 = 0")
  1591   assume p: "bv_to_int w2 = 0"
  1592   show ?thesis
  1593   proof (simp add: bv_sub_def bv_sadd_def bv_uminus_def p)
  1594     have "length (norm_signed w1) \<le> length w1"
  1595       by (rule norm_signed_length)
  1596     also have "... \<le> max (length w1) (length w2)"
  1597       by (rule le_maxI1)
  1598     also have "... \<le> Suc (max (length w1) (length w2))"
  1599       by arith
  1600     finally show "length (norm_signed w1) \<le> Suc (max (length w1) (length w2))" .
  1601   qed
  1602 next
  1603   assume "bv_to_int w2 \<noteq> 0"
  1604   hence "0 < length w2" by (cases w2,simp_all)
  1605   hence lmw: "0 < max (length w1) (length w2)" by arith
  1606 
  1607   let ?Q = "bv_to_int w1 - bv_to_int w2"
  1608 
  1609   have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
  1610   thus ?thesis
  1611   proof safe
  1612     assume "?Q = 0"
  1613     thus ?thesis
  1614       by (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
  1615   next
  1616     assume "?Q = -1"
  1617     thus ?thesis
  1618       by (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
  1619   next
  1620     assume p: "0 < ?Q"
  1621     show ?thesis
  1622       apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
  1623       apply (rule length_int_to_bv_upper_limit_gt0)
  1624       apply (rule p)
  1625     proof simp
  1626       from bv_to_int_lower_range [of w2]
  1627       have v2: "- bv_to_int w2 \<le> 2 ^ (length w2 - 1)" by simp
  1628       have "bv_to_int w1 + - bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
  1629         apply (rule zadd_zless_mono)
  1630         apply (rule bv_to_int_upper_range [of w1])
  1631         apply (rule v2)
  1632         done
  1633       also have "... \<le> 2 ^ max (length w1) (length w2)"
  1634         apply (rule adder_helper)
  1635         apply (rule lmw)
  1636         done
  1637       finally show "?Q < 2 ^ max (length w1) (length w2)" by simp
  1638     qed
  1639   next
  1640     assume p: "?Q < -1"
  1641     show ?thesis
  1642       apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
  1643       apply (rule length_int_to_bv_upper_limit_lem1)
  1644       apply (rule p)
  1645     proof simp
  1646       have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)"
  1647         apply (rule adder_helper)
  1648         apply (rule lmw)
  1649         done
  1650       hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
  1651         by simp
  1652       also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> bv_to_int w1 + -bv_to_int w2"
  1653         apply (rule add_mono)
  1654         apply (rule bv_to_int_lower_range [of w1])
  1655         using bv_to_int_upper_range [of w2]
  1656         apply simp
  1657         done
  1658       finally show "- (2^max (length w1) (length w2)) \<le> ?Q" by simp
  1659     qed
  1660   qed
  1661 qed
  1662 
  1663 definition
  1664   bv_smult :: "[bit list, bit list] => bit list" where
  1665   "bv_smult w1 w2 = int_to_bv (bv_to_int w1 * bv_to_int w2)"
  1666 
  1667 lemma bv_smult_type1 [simp]: "bv_smult (norm_signed w1) w2 = bv_smult w1 w2"
  1668   by (simp add: bv_smult_def)
  1669 
  1670 lemma bv_smult_type2 [simp]: "bv_smult w1 (norm_signed w2) = bv_smult w1 w2"
  1671   by (simp add: bv_smult_def)
  1672 
  1673 lemma bv_smult_returntype [simp]: "norm_signed (bv_smult w1 w2) = bv_smult w1 w2"
  1674   by (simp add: bv_smult_def)
  1675 
  1676 lemma bv_smult_length: "length (bv_smult w1 w2) \<le> length w1 + length w2"
  1677 proof -
  1678   let ?Q = "bv_to_int w1 * bv_to_int w2"
  1679 
  1680   have lmw: "?Q \<noteq> 0 ==> 0 < length w1 \<and> 0 < length w2" by auto
  1681 
  1682   have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
  1683   thus ?thesis
  1684   proof (safe dest!: iffD1 [OF mult_eq_0_iff])
  1685     assume "bv_to_int w1 = 0"
  1686     thus ?thesis by (simp add: bv_smult_def)
  1687   next
  1688     assume "bv_to_int w2 = 0"
  1689     thus ?thesis by (simp add: bv_smult_def)
  1690   next
  1691     assume p: "?Q = -1"
  1692     show ?thesis
  1693       apply (simp add: bv_smult_def p)
  1694       apply (cut_tac lmw)
  1695       apply arith
  1696       using p
  1697       apply simp
  1698       done
  1699   next
  1700     assume p: "0 < ?Q"
  1701     thus ?thesis
  1702     proof (simp add: zero_less_mult_iff,safe)
  1703       assume bi1: "0 < bv_to_int w1"
  1704       assume bi2: "0 < bv_to_int w2"
  1705       show ?thesis
  1706         apply (simp add: bv_smult_def)
  1707         apply (rule length_int_to_bv_upper_limit_gt0)
  1708         apply (rule p)
  1709       proof simp
  1710         have "?Q < 2 ^ (length w1 - 1) * 2 ^ (length w2 - 1)"
  1711           apply (rule mult_strict_mono)
  1712           apply (rule bv_to_int_upper_range)
  1713           apply (rule bv_to_int_upper_range)
  1714           apply (rule zero_less_power)
  1715           apply simp
  1716           using bi2
  1717           apply simp
  1718           done
  1719         also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
  1720           apply simp
  1721           apply (subst zpower_zadd_distrib [symmetric])
  1722           apply simp
  1723           done
  1724         finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
  1725       qed
  1726     next
  1727       assume bi1: "bv_to_int w1 < 0"
  1728       assume bi2: "bv_to_int w2 < 0"
  1729       show ?thesis
  1730         apply (simp add: bv_smult_def)
  1731         apply (rule length_int_to_bv_upper_limit_gt0)
  1732         apply (rule p)
  1733       proof simp
  1734         have "-bv_to_int w1 * -bv_to_int w2 \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
  1735           apply (rule mult_mono)
  1736           using bv_to_int_lower_range [of w1]
  1737           apply simp
  1738           using bv_to_int_lower_range [of w2]
  1739           apply simp
  1740           apply (rule zero_le_power,simp)
  1741           using bi2
  1742           apply simp
  1743           done
  1744         hence "?Q \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
  1745           by simp
  1746         also have "... < 2 ^ (length w1 + length w2 - Suc 0)"
  1747           apply simp
  1748           apply (subst zpower_zadd_distrib [symmetric])
  1749           apply simp
  1750           apply (cut_tac lmw)
  1751           apply arith
  1752           apply (cut_tac p)
  1753           apply arith
  1754           done
  1755         finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
  1756       qed
  1757     qed
  1758   next
  1759     assume p: "?Q < -1"
  1760     show ?thesis
  1761       apply (subst bv_smult_def)
  1762       apply (rule length_int_to_bv_upper_limit_lem1)
  1763       apply (rule p)
  1764     proof simp
  1765       have "(2::int) ^ (length w1 - 1) * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
  1766         apply simp
  1767         apply (subst zpower_zadd_distrib [symmetric])
  1768         apply simp
  1769         done
  1770       hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^(length w1 - 1) * 2 ^ (length w2 - 1))"
  1771         by simp
  1772       also have "... \<le> ?Q"
  1773       proof -
  1774         from p
  1775         have q: "bv_to_int w1 * bv_to_int w2 < 0"
  1776           by simp
  1777         thus ?thesis
  1778         proof (simp add: mult_less_0_iff,safe)
  1779           assume bi1: "0 < bv_to_int w1"
  1780           assume bi2: "bv_to_int w2 < 0"
  1781           have "-bv_to_int w2 * bv_to_int w1 \<le> ((2::int)^(length w2 - 1)) * (2 ^ (length w1 - 1))"
  1782             apply (rule mult_mono)
  1783             using bv_to_int_lower_range [of w2]
  1784             apply simp
  1785             using bv_to_int_upper_range [of w1]
  1786             apply simp
  1787             apply (rule zero_le_power,simp)
  1788             using bi1
  1789             apply simp
  1790             done
  1791           hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
  1792             by (simp add: zmult_ac)
  1793           thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
  1794             by simp
  1795         next
  1796           assume bi1: "bv_to_int w1 < 0"
  1797           assume bi2: "0 < bv_to_int w2"
  1798           have "-bv_to_int w1 * bv_to_int w2 \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
  1799             apply (rule mult_mono)
  1800             using bv_to_int_lower_range [of w1]
  1801             apply simp
  1802             using bv_to_int_upper_range [of w2]
  1803             apply simp
  1804             apply (rule zero_le_power,simp)
  1805             using bi2
  1806             apply simp
  1807             done
  1808           hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
  1809             by (simp add: zmult_ac)
  1810           thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
  1811             by simp
  1812         qed
  1813       qed
  1814       finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" .
  1815     qed
  1816   qed
  1817 qed
  1818 
  1819 lemma bv_msb_one: "bv_msb w = \<one> ==> bv_to_nat w \<noteq> 0"
  1820 by (cases w) simp_all
  1821 
  1822 lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \<le> length w1 + length w2"
  1823 proof -
  1824   let ?Q = "bv_to_int (utos w1) * bv_to_int w2"
  1825 
  1826   have lmw: "?Q \<noteq> 0 ==> 0 < length (utos w1) \<and> 0 < length w2" by auto
  1827 
  1828   have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
  1829   thus ?thesis
  1830   proof (safe dest!: iffD1 [OF mult_eq_0_iff])
  1831     assume "bv_to_int (utos w1) = 0"
  1832     thus ?thesis by (simp add: bv_smult_def)
  1833   next
  1834     assume "bv_to_int w2 = 0"
  1835     thus ?thesis by (simp add: bv_smult_def)
  1836   next
  1837     assume p: "0 < ?Q"
  1838     thus ?thesis
  1839     proof (simp add: zero_less_mult_iff,safe)
  1840       assume biw2: "0 < bv_to_int w2"
  1841       show ?thesis
  1842         apply (simp add: bv_smult_def)
  1843         apply (rule length_int_to_bv_upper_limit_gt0)
  1844         apply (rule p)
  1845       proof simp
  1846         have "?Q < 2 ^ length w1 * 2 ^ (length w2 - 1)"
  1847           apply (rule mult_strict_mono)
  1848           apply (simp add: bv_to_int_utos int_nat_two_exp)
  1849           apply (rule bv_to_nat_upper_range)
  1850           apply (rule bv_to_int_upper_range)
  1851           apply (rule zero_less_power,simp)
  1852           using biw2
  1853           apply simp
  1854           done
  1855         also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
  1856           apply simp
  1857           apply (subst zpower_zadd_distrib [symmetric])
  1858           apply simp
  1859           apply (cut_tac lmw)
  1860           apply arith
  1861           using p
  1862           apply auto
  1863           done
  1864         finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
  1865       qed
  1866     next
  1867       assume "bv_to_int (utos w1) < 0"
  1868       thus ?thesis by (simp add: bv_to_int_utos)
  1869     qed
  1870   next
  1871     assume p: "?Q = -1"
  1872     thus ?thesis
  1873       apply (simp add: bv_smult_def)
  1874       apply (cut_tac lmw)
  1875       apply arith
  1876       apply simp
  1877       done
  1878   next
  1879     assume p: "?Q < -1"
  1880     show ?thesis
  1881       apply (subst bv_smult_def)
  1882       apply (rule length_int_to_bv_upper_limit_lem1)
  1883       apply (rule p)
  1884     proof simp
  1885       have "(2::int) ^ length w1 * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
  1886         apply simp
  1887         apply (subst zpower_zadd_distrib [symmetric])
  1888         apply simp
  1889         apply (cut_tac lmw)
  1890         apply arith
  1891         apply (cut_tac p)
  1892         apply arith
  1893         done
  1894       hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^ length w1 * 2 ^ (length w2 - 1))"
  1895         by simp
  1896       also have "... \<le> ?Q"
  1897       proof -
  1898         from p
  1899         have q: "bv_to_int (utos w1) * bv_to_int w2 < 0"
  1900           by simp
  1901         thus ?thesis
  1902         proof (simp add: mult_less_0_iff,safe)
  1903           assume bi1: "0 < bv_to_int (utos w1)"
  1904           assume bi2: "bv_to_int w2 < 0"
  1905           have "-bv_to_int w2 * bv_to_int (utos w1) \<le> ((2::int)^(length w2 - 1)) * (2 ^ length w1)"
  1906             apply (rule mult_mono)
  1907             using bv_to_int_lower_range [of w2]
  1908             apply simp
  1909             apply (simp add: bv_to_int_utos)
  1910             using bv_to_nat_upper_range [of w1]
  1911             apply (simp add: int_nat_two_exp)
  1912             apply (rule zero_le_power,simp)
  1913             using bi1
  1914             apply simp
  1915             done
  1916           hence "-?Q \<le> ((2::int)^length w1) * (2 ^ (length w2 - 1))"
  1917             by (simp add: zmult_ac)
  1918           thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
  1919             by simp
  1920         next
  1921           assume bi1: "bv_to_int (utos w1) < 0"
  1922           thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
  1923             by (simp add: bv_to_int_utos)
  1924         qed
  1925       qed
  1926       finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" .
  1927     qed
  1928   qed
  1929 qed
  1930 
  1931 lemma bv_smult_sym: "bv_smult w1 w2 = bv_smult w2 w1"
  1932   by (simp add: bv_smult_def zmult_ac)
  1933 
  1934 subsection {* Structural operations *}
  1935 
  1936 definition
  1937   bv_select :: "[bit list,nat] => bit" where
  1938   "bv_select w i = w ! (length w - 1 - i)"
  1939 
  1940 definition
  1941   bv_chop :: "[bit list,nat] => bit list * bit list" where
  1942   "bv_chop w i = (let len = length w in (take (len - i) w,drop (len - i) w))"
  1943 
  1944 definition
  1945   bv_slice :: "[bit list,nat*nat] => bit list" where
  1946   "bv_slice w = (\<lambda>(b,e). fst (bv_chop (snd (bv_chop w (b+1))) e))"
  1947 
  1948 lemma bv_select_rev:
  1949   assumes notnull: "n < length w"
  1950   shows            "bv_select w n = rev w ! n"
  1951 proof -
  1952   have "\<forall>n. n < length w --> bv_select w n = rev w ! n"
  1953   proof (rule length_induct [of _ w],auto simp add: bv_select_def)
  1954     fix xs :: "bit list"
  1955     fix n
  1956     assume ind: "\<forall>ys::bit list. length ys < length xs --> (\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n)"
  1957     assume notx: "n < length xs"
  1958     show "xs ! (length xs - Suc n) = rev xs ! n"
  1959     proof (cases xs)
  1960       assume "xs = []"
  1961       with notx show ?thesis by simp
  1962     next
  1963       fix y ys
  1964       assume [simp]: "xs = y # ys"
  1965       show ?thesis
  1966       proof (auto simp add: nth_append)
  1967         assume noty: "n < length ys"
  1968         from spec [OF ind,of ys]
  1969         have "\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
  1970           by simp
  1971         hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" ..
  1972         from this and noty
  1973         have "ys ! (length ys - Suc n) = rev ys ! n" ..
  1974         thus "(y # ys) ! (length ys - n) = rev ys ! n"
  1975           by (simp add: nth_Cons' noty linorder_not_less [symmetric])
  1976       next
  1977         assume "~ n < length ys"
  1978         hence x: "length ys \<le> n" by simp
  1979         from notx have "n < Suc (length ys)" by simp
  1980         hence "n \<le> length ys" by simp
  1981         with x have "length ys = n" by simp
  1982         thus "y = [y] ! (n - length ys)" by simp
  1983       qed
  1984     qed
  1985   qed
  1986   then have "n < length w --> bv_select w n = rev w ! n" ..
  1987   from this and notnull show ?thesis ..
  1988 qed
  1989 
  1990 lemma bv_chop_append: "bv_chop (w1 @ w2) (length w2) = (w1,w2)"
  1991   by (simp add: bv_chop_def Let_def)
  1992 
  1993 lemma append_bv_chop_id: "fst (bv_chop w l) @ snd (bv_chop w l) = w"
  1994   by (simp add: bv_chop_def Let_def)
  1995 
  1996 lemma bv_chop_length_fst [simp]: "length (fst (bv_chop w i)) = length w - i"
  1997   by (simp add: bv_chop_def Let_def)
  1998 
  1999 lemma bv_chop_length_snd [simp]: "length (snd (bv_chop w i)) = min i (length w)"
  2000   by (simp add: bv_chop_def Let_def)
  2001 
  2002 lemma bv_slice_length [simp]: "[| j \<le> i; i < length w |] ==> length (bv_slice w (i,j)) = i - j + 1"
  2003   by (auto simp add: bv_slice_def)
  2004 
  2005 definition
  2006   length_nat :: "nat => nat" where
  2007   [code del]: "length_nat x = (LEAST n. x < 2 ^ n)"
  2008 
  2009 lemma length_nat: "length (nat_to_bv n) = length_nat n"
  2010   apply (simp add: length_nat_def)
  2011   apply (rule Least_equality [symmetric])
  2012   prefer 2
  2013   apply (rule length_nat_to_bv_upper_limit)
  2014   apply arith
  2015   apply (rule ccontr)
  2016 proof -
  2017   assume "~ n < 2 ^ length (nat_to_bv n)"
  2018   hence "2 ^ length (nat_to_bv n) \<le> n" by simp
  2019   hence "length (nat_to_bv n) < length (nat_to_bv n)"
  2020     by (rule length_nat_to_bv_lower_limit)
  2021   thus False by simp
  2022 qed
  2023 
  2024 lemma length_nat_0 [simp]: "length_nat 0 = 0"
  2025   by (simp add: length_nat_def Least_equality)
  2026 
  2027 lemma length_nat_non0:
  2028   assumes n0: "n \<noteq> 0"
  2029   shows       "length_nat n = Suc (length_nat (n div 2))"
  2030   apply (simp add: length_nat [symmetric])
  2031   apply (subst nat_to_bv_non0 [of n])
  2032   apply (simp_all add: n0)
  2033   done
  2034 
  2035 definition
  2036   length_int :: "int => nat" where
  2037   "length_int x =
  2038     (if 0 < x then Suc (length_nat (nat x))
  2039     else if x = 0 then 0
  2040     else Suc (length_nat (nat (-x - 1))))"
  2041 
  2042 lemma length_int: "length (int_to_bv i) = length_int i"
  2043 proof (cases "0 < i")
  2044   assume i0: "0 < i"
  2045   hence "length (int_to_bv i) =
  2046       length (norm_signed (\<zero> # norm_unsigned (nat_to_bv (nat i))))" by simp
  2047   also from norm_unsigned_result [of "nat_to_bv (nat i)"]
  2048   have "... = Suc (length_nat (nat i))"
  2049     apply safe
  2050     apply (simp del: norm_unsigned_nat_to_bv)
  2051     apply (drule norm_empty_bv_to_nat_zero)
  2052     using prems
  2053     apply simp
  2054     apply (cases "norm_unsigned (nat_to_bv (nat i))")
  2055     apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat i)"])
  2056     using prems
  2057     apply simp
  2058     apply simp
  2059     using prems
  2060     apply (simp add: length_nat [symmetric])
  2061     done
  2062   finally show ?thesis
  2063     using i0
  2064     by (simp add: length_int_def)
  2065 next
  2066   assume "~ 0 < i"
  2067   hence i0: "i \<le> 0" by simp
  2068   show ?thesis
  2069   proof (cases "i = 0")
  2070     assume "i = 0"
  2071     thus ?thesis by (simp add: length_int_def)
  2072   next
  2073     assume "i \<noteq> 0"
  2074     with i0 have i0: "i < 0" by simp
  2075     hence "length (int_to_bv i) =
  2076         length (norm_signed (\<one> # bv_not (norm_unsigned (nat_to_bv (nat (- i) - 1)))))"
  2077       by (simp add: int_to_bv_def nat_diff_distrib)
  2078     also from norm_unsigned_result [of "nat_to_bv (nat (- i) - 1)"]
  2079     have "... = Suc (length_nat (nat (- i) - 1))"
  2080       apply safe
  2081       apply (simp del: norm_unsigned_nat_to_bv)
  2082       apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat (-i) - Suc 0)"])
  2083       using prems
  2084       apply simp
  2085       apply (cases "- i - 1 = 0")
  2086       apply simp
  2087       apply (simp add: length_nat [symmetric])
  2088       apply (cases "norm_unsigned (nat_to_bv (nat (- i) - 1))")
  2089       apply simp
  2090       apply simp
  2091       done
  2092     finally
  2093     show ?thesis
  2094       using i0 by (simp add: length_int_def nat_diff_distrib del: int_to_bv_lt0)
  2095   qed
  2096 qed
  2097 
  2098 lemma length_int_0 [simp]: "length_int 0 = 0"
  2099   by (simp add: length_int_def)
  2100 
  2101 lemma length_int_gt0: "0 < i ==> length_int i = Suc (length_nat (nat i))"
  2102   by (simp add: length_int_def)
  2103 
  2104 lemma length_int_lt0: "i < 0 ==> length_int i = Suc (length_nat (nat (- i) - 1))"
  2105   by (simp add: length_int_def nat_diff_distrib)
  2106 
  2107 lemma bv_chopI: "[| w = w1 @ w2 ; i = length w2 |] ==> bv_chop w i = (w1,w2)"
  2108   by (simp add: bv_chop_def Let_def)
  2109 
  2110 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"
  2111   apply (simp add: bv_slice_def)
  2112   apply (subst bv_chopI [of "w1 @ w2 @ w3" w1 "w2 @ w3"])
  2113   apply simp
  2114   apply simp
  2115   apply simp
  2116   apply (subst bv_chopI [of "w2 @ w3" w2 w3],simp_all)
  2117   done
  2118 
  2119 lemma bv_slice_bv_slice:
  2120   assumes ki: "k \<le> i"
  2121   and     ij: "i \<le> j"
  2122   and     jl: "j \<le> l"
  2123   and     lw: "l < length w"
  2124   shows       "bv_slice w (j,i) = bv_slice (bv_slice w (l,k)) (j-k,i-k)"
  2125 proof -
  2126   def w1  == "fst (bv_chop w (Suc l))"
  2127   and w2  == "fst (bv_chop (snd (bv_chop w (Suc l))) (Suc j))"
  2128   and w3  == "fst (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)"
  2129   and w4  == "fst (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
  2130   and w5  == "snd (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
  2131   note w_defs = this
  2132 
  2133   have w_def: "w = w1 @ w2 @ w3 @ w4 @ w5"
  2134     by (simp add: w_defs append_bv_chop_id)
  2135 
  2136   from ki ij jl lw
  2137   show ?thesis
  2138     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"])
  2139     apply simp_all
  2140     apply (rule w_def)
  2141     apply (simp add: w_defs)
  2142     apply (simp add: w_defs)
  2143     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])
  2144     apply simp_all
  2145     apply (rule w_def)
  2146     apply (simp add: w_defs)
  2147     apply (simp add: w_defs)
  2148     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])
  2149     apply simp_all
  2150     apply (simp_all add: w_defs)
  2151     done
  2152 qed
  2153 
  2154 lemma bv_to_nat_extend [simp]: "bv_to_nat (bv_extend n \<zero> w) = bv_to_nat w"
  2155   apply (simp add: bv_extend_def)
  2156   apply (subst bv_to_nat_dist_append)
  2157   apply simp
  2158   apply (induct ("n - length w"))
  2159    apply simp_all
  2160   done
  2161 
  2162 lemma bv_msb_extend_same [simp]: "bv_msb w = b ==> bv_msb (bv_extend n b w) = b"
  2163   apply (simp add: bv_extend_def)
  2164   apply (cases "n - length w")
  2165    apply simp_all
  2166   done
  2167 
  2168 lemma bv_to_int_extend [simp]:
  2169   assumes a: "bv_msb w = b"
  2170   shows      "bv_to_int (bv_extend n b w) = bv_to_int w"
  2171 proof (cases "bv_msb w")
  2172   assume [simp]: "bv_msb w = \<zero>"
  2173   with a have [simp]: "b = \<zero>" by simp
  2174   show ?thesis by (simp add: bv_to_int_def)
  2175 next
  2176   assume [simp]: "bv_msb w = \<one>"
  2177   with a have [simp]: "b = \<one>" by simp
  2178   show ?thesis
  2179     apply (simp add: bv_to_int_def)
  2180     apply (simp add: bv_extend_def)
  2181     apply (induct ("n - length w"), simp_all)
  2182     done
  2183 qed
  2184 
  2185 lemma length_nat_mono [simp]: "x \<le> y ==> length_nat x \<le> length_nat y"
  2186 proof (rule ccontr)
  2187   assume xy: "x \<le> y"
  2188   assume "~ length_nat x \<le> length_nat y"
  2189   hence lxly: "length_nat y < length_nat x"
  2190     by simp
  2191   hence "length_nat y < (LEAST n. x < 2 ^ n)"
  2192     by (simp add: length_nat_def)
  2193   hence "~ x < 2 ^ length_nat y"
  2194     by (rule not_less_Least)
  2195   hence xx: "2 ^ length_nat y \<le> x"
  2196     by simp
  2197   have yy: "y < 2 ^ length_nat y"
  2198     apply (simp add: length_nat_def)
  2199     apply (rule LeastI)
  2200     apply (subgoal_tac "y < 2 ^ y",assumption)
  2201     apply (cases "0 \<le> y")
  2202     apply (induct y,simp_all)
  2203     done
  2204   with xx have "y < x" by simp
  2205   with xy show False by simp
  2206 qed
  2207 
  2208 lemma length_nat_mono_int [simp]: "x \<le> y ==> length_nat x \<le> length_nat y"
  2209   by (rule length_nat_mono) arith
  2210 
  2211 lemma length_nat_pos [simp,intro!]: "0 < x ==> 0 < length_nat x"
  2212   by (simp add: length_nat_non0)
  2213 
  2214 lemma length_int_mono_gt0: "[| 0 \<le> x ; x \<le> y |] ==> length_int x \<le> length_int y"
  2215   by (cases "x = 0") (simp_all add: length_int_gt0 nat_le_eq_zle)
  2216 
  2217 lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x"
  2218   by (cases "y = 0") (simp_all add: length_int_lt0)
  2219 
  2220 lemmas [simp] = length_nat_non0
  2221 
  2222 lemma "nat_to_bv (number_of Int.Pls) = []"
  2223   by simp
  2224 
  2225 primrec fast_bv_to_nat_helper :: "[bit list, int] => int" where
  2226     fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
  2227   | fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
  2228       fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
  2229 
  2230 declare fast_bv_to_nat_helper.simps [code del]
  2231 
  2232 lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
  2233     fast_bv_to_nat_helper bs (Int.Bit0 bin)"
  2234   by simp
  2235 
  2236 lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin =
  2237     fast_bv_to_nat_helper bs (Int.Bit1 bin)"
  2238   by simp
  2239 
  2240 lemma fast_bv_to_nat_def:
  2241   "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Int.Pls)"
  2242 proof (simp add: bv_to_nat_def)
  2243   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)"
  2244     apply (induct bs,simp)
  2245     apply (case_tac a,simp_all)
  2246     done
  2247   thus "foldl (\<lambda>bn b. 2 * bn + bitval b) 0 bs \<equiv> number_of (fast_bv_to_nat_helper bs Int.Pls)"
  2248     by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
  2249 qed
  2250 
  2251 declare fast_bv_to_nat_Cons [simp del]
  2252 declare fast_bv_to_nat_Cons0 [simp]
  2253 declare fast_bv_to_nat_Cons1 [simp]
  2254 
  2255 setup {*
  2256 (*comments containing lcp are the removal of fast_bv_of_nat*)
  2257 let
  2258   fun is_const_bool (Const("True",_)) = true
  2259     | is_const_bool (Const("False",_)) = true
  2260     | is_const_bool _ = false
  2261   fun is_const_bit (Const("Word.bit.Zero",_)) = true
  2262     | is_const_bit (Const("Word.bit.One",_)) = true
  2263     | is_const_bit _ = false
  2264   fun num_is_usable (Const(@{const_name Int.Pls},_)) = true
  2265     | num_is_usable (Const(@{const_name Int.Min},_)) = false
  2266     | num_is_usable (Const(@{const_name Int.Bit0},_) $ w) =
  2267         num_is_usable w
  2268     | num_is_usable (Const(@{const_name Int.Bit1},_) $ w) =
  2269         num_is_usable w
  2270     | num_is_usable _ = false
  2271   fun vec_is_usable (Const("List.list.Nil",_)) = true
  2272     | vec_is_usable (Const("List.list.Cons",_) $ b $ bs) =
  2273         vec_is_usable bs andalso is_const_bit b
  2274     | vec_is_usable _ = false
  2275   (*lcp** val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"*)
  2276   val fast2_th = @{thm "Word.fast_bv_to_nat_def"};
  2277   (*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const(@{const_name Int.number_of},_) $ t)) =
  2278     if num_is_usable t
  2279       then SOME (Drule.cterm_instantiate [(cterm_of sg (Var (("w", 0), @{typ int})), cterm_of sg t)] fast1_th)
  2280       else NONE
  2281     | f _ _ _ = NONE *)
  2282   fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) =
  2283         if vec_is_usable t then
  2284           SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
  2285         else NONE
  2286     | g _ _ _ = NONE
  2287   (*lcp** val simproc1 = Simplifier.simproc thy "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f *)
  2288   val simproc2 = Simplifier.simproc @{theory} "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
  2289 in
  2290   Simplifier.map_simpset (fn ss => ss addsimprocs [(*lcp*simproc1,*)simproc2])
  2291 end*}
  2292 
  2293 declare bv_to_nat1 [simp del]
  2294 declare bv_to_nat_helper [simp del]
  2295 
  2296 definition
  2297   bv_mapzip :: "[bit => bit => bit,bit list, bit list] => bit list" where
  2298   "bv_mapzip f w1 w2 =
  2299     (let g = bv_extend (max (length w1) (length w2)) \<zero>
  2300      in map (split f) (zip (g w1) (g w2)))"
  2301 
  2302 lemma bv_length_bv_mapzip [simp]:
  2303     "length (bv_mapzip f w1 w2) = max (length w1) (length w2)"
  2304   by (simp add: bv_mapzip_def Let_def split: split_max)
  2305 
  2306 lemma bv_mapzip_Nil [simp]: "bv_mapzip f [] [] = []"
  2307   by (simp add: bv_mapzip_def Let_def)
  2308 
  2309 lemma bv_mapzip_Cons [simp]: "length w1 = length w2 ==>
  2310     bv_mapzip f (x#w1) (y#w2) = f x y # bv_mapzip f w1 w2"
  2311   by (simp add: bv_mapzip_def Let_def)
  2312 
  2313 end