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