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