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