src/HOL/Word/BinOperations.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 28042 1471f2974eb1
child 28562 4e74209f113e
permissions -rw-r--r--
moved global ML bindings to global place;
kleing@24333
     1
(* 
kleing@24333
     2
  ID:     $Id$
kleing@24333
     3
  Author: Jeremy Dawson and Gerwin Klein, NICTA
kleing@24333
     4
kleing@24333
     5
  definition and basic theorems for bit-wise logical operations 
kleing@24333
     6
  for integers expressed using Pls, Min, BIT,
kleing@24333
     7
  and converting them to and from lists of bools
kleing@24333
     8
*) 
kleing@24333
     9
huffman@24350
    10
header {* Bitwise Operations on Binary Integers *}
huffman@24350
    11
haftmann@26558
    12
theory BinOperations
haftmann@26558
    13
imports BinGeneral BitSyntax
kleing@24333
    14
begin
kleing@24333
    15
huffman@24364
    16
subsection {* Logical operations *}
huffman@24353
    17
huffman@24353
    18
text "bit-wise logical operations on the int type"
huffman@24353
    19
haftmann@25762
    20
instantiation int :: bit
haftmann@25762
    21
begin
haftmann@25762
    22
haftmann@25762
    23
definition
haftmann@26558
    24
  int_not_def [code func del]: "bitNOT = bin_rec Int.Min Int.Pls 
huffman@24353
    25
    (\<lambda>w b s. s BIT (NOT b))"
haftmann@25762
    26
haftmann@25762
    27
definition
haftmann@26558
    28
  int_and_def [code func del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y) 
huffman@24353
    29
    (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
haftmann@25762
    30
haftmann@25762
    31
definition
haftmann@26558
    32
  int_or_def [code func del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min) 
huffman@24353
    33
    (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
haftmann@25762
    34
haftmann@25762
    35
definition
haftmann@26558
    36
  int_xor_def [code func del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT 
huffman@24353
    37
    (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
haftmann@25762
    38
haftmann@25762
    39
instance ..
haftmann@25762
    40
haftmann@25762
    41
end
huffman@24353
    42
kleing@24333
    43
lemma int_not_simps [simp]:
haftmann@25919
    44
  "NOT Int.Pls = Int.Min"
haftmann@25919
    45
  "NOT Int.Min = Int.Pls"
huffman@26086
    46
  "NOT (Int.Bit0 w) = Int.Bit1 (NOT w)"
huffman@26086
    47
  "NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
haftmann@26558
    48
  "NOT (w BIT b) = (NOT w) BIT (NOT b)"
huffman@26086
    49
  unfolding int_not_def by (simp_all add: bin_rec_simps)
kleing@24333
    50
haftmann@26558
    51
declare int_not_simps(1-4) [code func]
haftmann@26558
    52
haftmann@26558
    53
lemma int_xor_Pls [simp, code func]: 
haftmann@25919
    54
  "Int.Pls XOR x = x"
huffman@24465
    55
  unfolding int_xor_def by (simp add: bin_rec_PM)
kleing@24333
    56
haftmann@26558
    57
lemma int_xor_Min [simp, code func]: 
haftmann@25919
    58
  "Int.Min XOR x = NOT x"
huffman@24465
    59
  unfolding int_xor_def by (simp add: bin_rec_PM)
kleing@24333
    60
kleing@24333
    61
lemma int_xor_Bits [simp]: 
huffman@24353
    62
  "(x BIT b) XOR (y BIT c) = (x XOR y) BIT (b XOR c)"
kleing@24333
    63
  apply (unfold int_xor_def)
kleing@24333
    64
  apply (rule bin_rec_simps (1) [THEN fun_cong, THEN trans])
kleing@24333
    65
    apply (rule ext, simp)
kleing@24333
    66
   prefer 2
kleing@24333
    67
   apply simp
kleing@24333
    68
  apply (rule ext)
kleing@24333
    69
  apply (simp add: int_not_simps [symmetric])
kleing@24333
    70
  done
kleing@24333
    71
haftmann@26558
    72
lemma int_xor_Bits2 [simp, code func]: 
huffman@26086
    73
  "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
huffman@26086
    74
  "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
huffman@26086
    75
  "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
huffman@26086
    76
  "(Int.Bit1 x) XOR (Int.Bit1 y) = Int.Bit0 (x XOR y)"
huffman@26086
    77
  unfolding BIT_simps [symmetric] int_xor_Bits by simp_all
huffman@26086
    78
kleing@24333
    79
lemma int_xor_x_simps':
haftmann@25919
    80
  "w XOR (Int.Pls BIT bit.B0) = w"
haftmann@25919
    81
  "w XOR (Int.Min BIT bit.B1) = NOT w"
kleing@24333
    82
  apply (induct w rule: bin_induct)
kleing@24333
    83
       apply simp_all[4]
kleing@24333
    84
   apply (unfold int_xor_Bits)
kleing@24333
    85
   apply clarsimp+
kleing@24333
    86
  done
kleing@24333
    87
haftmann@26558
    88
lemma int_xor_extra_simps [simp, code func]:
huffman@26086
    89
  "w XOR Int.Pls = w"
huffman@26086
    90
  "w XOR Int.Min = NOT w"
huffman@26086
    91
  using int_xor_x_simps' by simp_all
kleing@24333
    92
haftmann@26558
    93
lemma int_or_Pls [simp, code func]: 
haftmann@25919
    94
  "Int.Pls OR x = x"
huffman@24465
    95
  by (unfold int_or_def) (simp add: bin_rec_PM)
kleing@24333
    96
  
haftmann@26558
    97
lemma int_or_Min [simp, code func]:
haftmann@25919
    98
  "Int.Min OR x = Int.Min"
huffman@24465
    99
  by (unfold int_or_def) (simp add: bin_rec_PM)
kleing@24333
   100
kleing@24333
   101
lemma int_or_Bits [simp]: 
huffman@24353
   102
  "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
kleing@24333
   103
  unfolding int_or_def by (simp add: bin_rec_simps)
kleing@24333
   104
haftmann@26558
   105
lemma int_or_Bits2 [simp, code func]: 
huffman@26086
   106
  "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
huffman@26086
   107
  "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
huffman@26086
   108
  "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
huffman@26086
   109
  "(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
huffman@26086
   110
  unfolding BIT_simps [symmetric] int_or_Bits by simp_all
huffman@26086
   111
kleing@24333
   112
lemma int_or_x_simps': 
haftmann@25919
   113
  "w OR (Int.Pls BIT bit.B0) = w"
haftmann@25919
   114
  "w OR (Int.Min BIT bit.B1) = Int.Min"
kleing@24333
   115
  apply (induct w rule: bin_induct)
kleing@24333
   116
       apply simp_all[4]
kleing@24333
   117
   apply (unfold int_or_Bits)
kleing@24333
   118
   apply clarsimp+
kleing@24333
   119
  done
kleing@24333
   120
haftmann@26558
   121
lemma int_or_extra_simps [simp, code func]:
huffman@26086
   122
  "w OR Int.Pls = w"
huffman@26086
   123
  "w OR Int.Min = Int.Min"
huffman@26086
   124
  using int_or_x_simps' by simp_all
kleing@24333
   125
haftmann@26558
   126
lemma int_and_Pls [simp, code func]:
haftmann@25919
   127
  "Int.Pls AND x = Int.Pls"
huffman@24465
   128
  unfolding int_and_def by (simp add: bin_rec_PM)
kleing@24333
   129
haftmann@26558
   130
lemma int_and_Min [simp, code func]:
haftmann@25919
   131
  "Int.Min AND x = x"
huffman@24465
   132
  unfolding int_and_def by (simp add: bin_rec_PM)
kleing@24333
   133
kleing@24333
   134
lemma int_and_Bits [simp]: 
huffman@24353
   135
  "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
kleing@24333
   136
  unfolding int_and_def by (simp add: bin_rec_simps)
kleing@24333
   137
haftmann@26558
   138
lemma int_and_Bits2 [simp, code func]: 
huffman@26086
   139
  "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
huffman@26086
   140
  "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
huffman@26086
   141
  "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
huffman@26086
   142
  "(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)"
huffman@26086
   143
  unfolding BIT_simps [symmetric] int_and_Bits by simp_all
huffman@26086
   144
kleing@24333
   145
lemma int_and_x_simps': 
haftmann@25919
   146
  "w AND (Int.Pls BIT bit.B0) = Int.Pls"
haftmann@25919
   147
  "w AND (Int.Min BIT bit.B1) = w"
kleing@24333
   148
  apply (induct w rule: bin_induct)
kleing@24333
   149
       apply simp_all[4]
kleing@24333
   150
   apply (unfold int_and_Bits)
kleing@24333
   151
   apply clarsimp+
kleing@24333
   152
  done
kleing@24333
   153
haftmann@26558
   154
lemma int_and_extra_simps [simp, code func]:
huffman@26086
   155
  "w AND Int.Pls = Int.Pls"
huffman@26086
   156
  "w AND Int.Min = w"
huffman@26086
   157
  using int_and_x_simps' by simp_all
kleing@24333
   158
kleing@24333
   159
(* commutativity of the above *)
kleing@24333
   160
lemma bin_ops_comm:
kleing@24333
   161
  shows
huffman@24353
   162
  int_and_comm: "!!y::int. x AND y = y AND x" and
huffman@24353
   163
  int_or_comm:  "!!y::int. x OR y = y OR x" and
huffman@24353
   164
  int_xor_comm: "!!y::int. x XOR y = y XOR x"
kleing@24333
   165
  apply (induct x rule: bin_induct)
kleing@24333
   166
          apply simp_all[6]
kleing@24333
   167
    apply (case_tac y rule: bin_exhaust, simp add: bit_ops_comm)+
kleing@24333
   168
  done
kleing@24333
   169
kleing@24333
   170
lemma bin_ops_same [simp]:
huffman@24353
   171
  "(x::int) AND x = x" 
huffman@24353
   172
  "(x::int) OR x = x" 
haftmann@25919
   173
  "(x::int) XOR x = Int.Pls"
kleing@24333
   174
  by (induct x rule: bin_induct) auto
kleing@24333
   175
huffman@24353
   176
lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
kleing@24333
   177
  by (induct x rule: bin_induct) auto
kleing@24333
   178
kleing@24333
   179
lemmas bin_log_esimps = 
kleing@24333
   180
  int_and_extra_simps  int_or_extra_simps  int_xor_extra_simps
kleing@24333
   181
  int_and_Pls int_and_Min  int_or_Pls int_or_Min  int_xor_Pls int_xor_Min
kleing@24333
   182
kleing@24333
   183
(* basic properties of logical (bit-wise) operations *)
kleing@24333
   184
kleing@24333
   185
lemma bbw_ao_absorb: 
huffman@24353
   186
  "!!y::int. x AND (y OR x) = x & x OR (y AND x) = x"
kleing@24333
   187
  apply (induct x rule: bin_induct)
kleing@24333
   188
    apply auto 
kleing@24333
   189
   apply (case_tac [!] y rule: bin_exhaust)
kleing@24333
   190
   apply auto
kleing@24333
   191
   apply (case_tac [!] bit)
kleing@24333
   192
     apply auto
kleing@24333
   193
  done
kleing@24333
   194
kleing@24333
   195
lemma bbw_ao_absorbs_other:
huffman@24353
   196
  "x AND (x OR y) = x \<and> (y AND x) OR x = (x::int)"
huffman@24353
   197
  "(y OR x) AND x = x \<and> x OR (x AND y) = (x::int)"
huffman@24353
   198
  "(x OR y) AND x = x \<and> (x AND y) OR x = (x::int)"
kleing@24333
   199
  apply (auto simp: bbw_ao_absorb int_or_comm)  
kleing@24333
   200
      apply (subst int_or_comm)
kleing@24333
   201
    apply (simp add: bbw_ao_absorb)
kleing@24333
   202
   apply (subst int_and_comm)
kleing@24333
   203
   apply (subst int_or_comm)
kleing@24333
   204
   apply (simp add: bbw_ao_absorb)
kleing@24333
   205
  apply (subst int_and_comm)
kleing@24333
   206
  apply (simp add: bbw_ao_absorb)
kleing@24333
   207
  done
huffman@24353
   208
kleing@24333
   209
lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other
kleing@24333
   210
kleing@24333
   211
lemma int_xor_not:
huffman@24353
   212
  "!!y::int. (NOT x) XOR y = NOT (x XOR y) & 
huffman@24353
   213
        x XOR (NOT y) = NOT (x XOR y)"
kleing@24333
   214
  apply (induct x rule: bin_induct)
kleing@24333
   215
    apply auto
kleing@24333
   216
   apply (case_tac y rule: bin_exhaust, auto, 
kleing@24333
   217
          case_tac b, auto)+
kleing@24333
   218
  done
kleing@24333
   219
kleing@24333
   220
lemma bbw_assocs': 
huffman@24353
   221
  "!!y z::int. (x AND y) AND z = x AND (y AND z) & 
huffman@24353
   222
          (x OR y) OR z = x OR (y OR z) & 
huffman@24353
   223
          (x XOR y) XOR z = x XOR (y XOR z)"
kleing@24333
   224
  apply (induct x rule: bin_induct)
kleing@24333
   225
    apply (auto simp: int_xor_not)
kleing@24333
   226
    apply (case_tac [!] y rule: bin_exhaust)
kleing@24333
   227
    apply (case_tac [!] z rule: bin_exhaust)
kleing@24333
   228
    apply (case_tac [!] bit)
kleing@24333
   229
       apply (case_tac [!] b)
huffman@26086
   230
             apply (auto simp del: BIT_simps)
kleing@24333
   231
  done
kleing@24333
   232
kleing@24333
   233
lemma int_and_assoc:
huffman@24353
   234
  "(x AND y) AND (z::int) = x AND (y AND z)"
kleing@24333
   235
  by (simp add: bbw_assocs')
kleing@24333
   236
kleing@24333
   237
lemma int_or_assoc:
huffman@24353
   238
  "(x OR y) OR (z::int) = x OR (y OR z)"
kleing@24333
   239
  by (simp add: bbw_assocs')
kleing@24333
   240
kleing@24333
   241
lemma int_xor_assoc:
huffman@24353
   242
  "(x XOR y) XOR (z::int) = x XOR (y XOR z)"
kleing@24333
   243
  by (simp add: bbw_assocs')
kleing@24333
   244
kleing@24333
   245
lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc
kleing@24333
   246
kleing@24333
   247
lemma bbw_lcs [simp]: 
huffman@24353
   248
  "(y::int) AND (x AND z) = x AND (y AND z)"
huffman@24353
   249
  "(y::int) OR (x OR z) = x OR (y OR z)"
huffman@24353
   250
  "(y::int) XOR (x XOR z) = x XOR (y XOR z)" 
kleing@24333
   251
  apply (auto simp: bbw_assocs [symmetric])
kleing@24333
   252
  apply (auto simp: bin_ops_comm)
kleing@24333
   253
  done
kleing@24333
   254
kleing@24333
   255
lemma bbw_not_dist: 
huffman@24353
   256
  "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)" 
huffman@24353
   257
  "!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)"
kleing@24333
   258
  apply (induct x rule: bin_induct)
kleing@24333
   259
       apply auto
kleing@24333
   260
   apply (case_tac [!] y rule: bin_exhaust)
huffman@26086
   261
   apply (case_tac [!] bit, auto simp del: BIT_simps)
kleing@24333
   262
  done
kleing@24333
   263
kleing@24333
   264
lemma bbw_oa_dist: 
huffman@24353
   265
  "!!y z::int. (x AND y) OR z = 
huffman@24353
   266
          (x OR z) AND (y OR z)"
kleing@24333
   267
  apply (induct x rule: bin_induct)
kleing@24333
   268
    apply auto
kleing@24333
   269
  apply (case_tac y rule: bin_exhaust)
kleing@24333
   270
  apply (case_tac z rule: bin_exhaust)
huffman@26086
   271
  apply (case_tac ba, auto simp del: BIT_simps)
kleing@24333
   272
  done
kleing@24333
   273
kleing@24333
   274
lemma bbw_ao_dist: 
huffman@24353
   275
  "!!y z::int. (x OR y) AND z = 
huffman@24353
   276
          (x AND z) OR (y AND z)"
kleing@24333
   277
   apply (induct x rule: bin_induct)
kleing@24333
   278
    apply auto
kleing@24333
   279
  apply (case_tac y rule: bin_exhaust)
kleing@24333
   280
  apply (case_tac z rule: bin_exhaust)
huffman@26086
   281
  apply (case_tac ba, auto simp del: BIT_simps)
kleing@24333
   282
  done
kleing@24333
   283
huffman@24367
   284
(*
huffman@24367
   285
Why were these declared simp???
kleing@24333
   286
declare bin_ops_comm [simp] bbw_assocs [simp] 
huffman@24367
   287
*)
kleing@24333
   288
kleing@24333
   289
lemma plus_and_or [rule_format]:
huffman@24353
   290
  "ALL y::int. (x AND y) + (x OR y) = x + y"
kleing@24333
   291
  apply (induct x rule: bin_induct)
kleing@24333
   292
    apply clarsimp
kleing@24333
   293
   apply clarsimp
kleing@24333
   294
  apply clarsimp
kleing@24333
   295
  apply (case_tac y rule: bin_exhaust)
kleing@24333
   296
  apply clarsimp
kleing@24333
   297
  apply (unfold Bit_def)
kleing@24333
   298
  apply clarsimp
kleing@24333
   299
  apply (erule_tac x = "x" in allE)
kleing@24333
   300
  apply (simp split: bit.split)
kleing@24333
   301
  done
kleing@24333
   302
kleing@24333
   303
lemma le_int_or:
haftmann@25919
   304
  "!!x.  bin_sign y = Int.Pls ==> x <= x OR y"
kleing@24333
   305
  apply (induct y rule: bin_induct)
kleing@24333
   306
    apply clarsimp
kleing@24333
   307
   apply clarsimp
kleing@24333
   308
  apply (case_tac x rule: bin_exhaust)
kleing@24333
   309
  apply (case_tac b)
kleing@24333
   310
   apply (case_tac [!] bit)
haftmann@26514
   311
     apply (auto simp: less_eq_int_code)
kleing@24333
   312
  done
kleing@24333
   313
kleing@24333
   314
lemmas int_and_le =
kleing@24333
   315
  xtr3 [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or] ;
kleing@24333
   316
huffman@24364
   317
lemma bin_nth_ops:
huffman@24364
   318
  "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)" 
huffman@24364
   319
  "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
huffman@24364
   320
  "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)" 
huffman@24364
   321
  "!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
huffman@24364
   322
  apply (induct n)
huffman@24364
   323
         apply safe
huffman@24364
   324
                         apply (case_tac [!] x rule: bin_exhaust)
huffman@26086
   325
                         apply (simp_all del: BIT_simps)
huffman@24364
   326
                      apply (case_tac [!] y rule: bin_exhaust)
huffman@26086
   327
                      apply (simp_all del: BIT_simps)
huffman@24364
   328
        apply (auto dest: not_B1_is_B0 intro: B1_ass_B0)
huffman@24364
   329
  done
huffman@24364
   330
huffman@24364
   331
(* interaction between bit-wise and arithmetic *)
huffman@24364
   332
(* good example of bin_induction *)
haftmann@25919
   333
lemma bin_add_not: "x + NOT x = Int.Min"
huffman@24364
   334
  apply (induct x rule: bin_induct)
huffman@24364
   335
    apply clarsimp
huffman@24364
   336
   apply clarsimp
huffman@24364
   337
  apply (case_tac bit, auto)
huffman@24364
   338
  done
huffman@24364
   339
huffman@24364
   340
(* truncating results of bit-wise operations *)
huffman@24364
   341
lemma bin_trunc_ao: 
huffman@24364
   342
  "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)" 
huffman@24364
   343
  "!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)"
huffman@24364
   344
  apply (induct n)
huffman@24364
   345
      apply auto
huffman@24364
   346
      apply (case_tac [!] x rule: bin_exhaust)
huffman@24364
   347
      apply (case_tac [!] y rule: bin_exhaust)
huffman@24364
   348
      apply auto
huffman@24364
   349
  done
huffman@24364
   350
huffman@24364
   351
lemma bin_trunc_xor: 
huffman@24364
   352
  "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) = 
huffman@24364
   353
          bintrunc n (x XOR y)"
huffman@24364
   354
  apply (induct n)
huffman@24364
   355
   apply auto
huffman@24364
   356
   apply (case_tac [!] x rule: bin_exhaust)
huffman@24364
   357
   apply (case_tac [!] y rule: bin_exhaust)
huffman@24364
   358
   apply auto
huffman@24364
   359
  done
huffman@24364
   360
huffman@24364
   361
lemma bin_trunc_not: 
huffman@24364
   362
  "!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
huffman@24364
   363
  apply (induct n)
huffman@24364
   364
   apply auto
huffman@24364
   365
   apply (case_tac [!] x rule: bin_exhaust)
huffman@24364
   366
   apply auto
huffman@24364
   367
  done
huffman@24364
   368
huffman@24364
   369
(* want theorems of the form of bin_trunc_xor *)
huffman@24364
   370
lemma bintr_bintr_i:
huffman@24364
   371
  "x = bintrunc n y ==> bintrunc n x = bintrunc n y"
huffman@24364
   372
  by auto
huffman@24364
   373
huffman@24364
   374
lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i]
huffman@24364
   375
lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i]
huffman@24364
   376
huffman@24364
   377
subsection {* Setting and clearing bits *}
huffman@24364
   378
haftmann@26558
   379
primrec
huffman@24364
   380
  bin_sc :: "nat => bit => int => int"
haftmann@26558
   381
where
haftmann@26558
   382
  Z: "bin_sc 0 b w = bin_rest w BIT b"
haftmann@26558
   383
  | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
huffman@24364
   384
kleing@24333
   385
(** nth bit, set/clear **)
kleing@24333
   386
kleing@24333
   387
lemma bin_nth_sc [simp]: 
kleing@24333
   388
  "!!w. bin_nth (bin_sc n b w) n = (b = bit.B1)"
kleing@24333
   389
  by (induct n)  auto
kleing@24333
   390
kleing@24333
   391
lemma bin_sc_sc_same [simp]: 
kleing@24333
   392
  "!!w. bin_sc n c (bin_sc n b w) = bin_sc n c w"
kleing@24333
   393
  by (induct n) auto
kleing@24333
   394
kleing@24333
   395
lemma bin_sc_sc_diff:
kleing@24333
   396
  "!!w m. m ~= n ==> 
kleing@24333
   397
    bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
kleing@24333
   398
  apply (induct n)
kleing@24333
   399
   apply (case_tac [!] m)
kleing@24333
   400
     apply auto
kleing@24333
   401
  done
kleing@24333
   402
kleing@24333
   403
lemma bin_nth_sc_gen: 
kleing@24333
   404
  "!!w m. bin_nth (bin_sc n b w) m = (if m = n then b = bit.B1 else bin_nth w m)"
kleing@24333
   405
  by (induct n) (case_tac [!] m, auto)
kleing@24333
   406
  
kleing@24333
   407
lemma bin_sc_nth [simp]:
kleing@24333
   408
  "!!w. (bin_sc n (If (bin_nth w n) bit.B1 bit.B0) w) = w"
huffman@24465
   409
  by (induct n) auto
kleing@24333
   410
kleing@24333
   411
lemma bin_sign_sc [simp]:
kleing@24333
   412
  "!!w. bin_sign (bin_sc n b w) = bin_sign w"
kleing@24333
   413
  by (induct n) auto
kleing@24333
   414
  
kleing@24333
   415
lemma bin_sc_bintr [simp]: 
kleing@24333
   416
  "!!w m. bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
kleing@24333
   417
  apply (induct n)
kleing@24333
   418
   apply (case_tac [!] w rule: bin_exhaust)
kleing@24333
   419
   apply (case_tac [!] m, auto)
kleing@24333
   420
  done
kleing@24333
   421
kleing@24333
   422
lemma bin_clr_le:
kleing@24333
   423
  "!!w. bin_sc n bit.B0 w <= w"
kleing@24333
   424
  apply (induct n) 
kleing@24333
   425
   apply (case_tac [!] w rule: bin_exhaust)
huffman@26086
   426
   apply (auto simp del: BIT_simps)
kleing@24333
   427
   apply (unfold Bit_def)
kleing@24333
   428
   apply (simp_all split: bit.split)
kleing@24333
   429
  done
kleing@24333
   430
kleing@24333
   431
lemma bin_set_ge:
kleing@24333
   432
  "!!w. bin_sc n bit.B1 w >= w"
kleing@24333
   433
  apply (induct n) 
kleing@24333
   434
   apply (case_tac [!] w rule: bin_exhaust)
huffman@26086
   435
   apply (auto simp del: BIT_simps)
kleing@24333
   436
   apply (unfold Bit_def)
kleing@24333
   437
   apply (simp_all split: bit.split)
kleing@24333
   438
  done
kleing@24333
   439
kleing@24333
   440
lemma bintr_bin_clr_le:
kleing@24333
   441
  "!!w m. bintrunc n (bin_sc m bit.B0 w) <= bintrunc n w"
kleing@24333
   442
  apply (induct n)
kleing@24333
   443
   apply simp
kleing@24333
   444
  apply (case_tac w rule: bin_exhaust)
kleing@24333
   445
  apply (case_tac m)
huffman@26086
   446
   apply (auto simp del: BIT_simps)
kleing@24333
   447
   apply (unfold Bit_def)
kleing@24333
   448
   apply (simp_all split: bit.split)
kleing@24333
   449
  done
kleing@24333
   450
kleing@24333
   451
lemma bintr_bin_set_ge:
kleing@24333
   452
  "!!w m. bintrunc n (bin_sc m bit.B1 w) >= bintrunc n w"
kleing@24333
   453
  apply (induct n)
kleing@24333
   454
   apply simp
kleing@24333
   455
  apply (case_tac w rule: bin_exhaust)
kleing@24333
   456
  apply (case_tac m)
huffman@26086
   457
   apply (auto simp del: BIT_simps)
kleing@24333
   458
   apply (unfold Bit_def)
kleing@24333
   459
   apply (simp_all split: bit.split)
kleing@24333
   460
  done
kleing@24333
   461
haftmann@25919
   462
lemma bin_sc_FP [simp]: "bin_sc n bit.B0 Int.Pls = Int.Pls"
kleing@24333
   463
  by (induct n) auto
kleing@24333
   464
haftmann@25919
   465
lemma bin_sc_TM [simp]: "bin_sc n bit.B1 Int.Min = Int.Min"
kleing@24333
   466
  by (induct n) auto
kleing@24333
   467
  
kleing@24333
   468
lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
kleing@24333
   469
kleing@24333
   470
lemma bin_sc_minus:
kleing@24333
   471
  "0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
kleing@24333
   472
  by auto
kleing@24333
   473
kleing@24333
   474
lemmas bin_sc_Suc_minus = 
kleing@24333
   475
  trans [OF bin_sc_minus [symmetric] bin_sc.Suc, standard]
kleing@24333
   476
kleing@24333
   477
lemmas bin_sc_Suc_pred [simp] = 
kleing@24333
   478
  bin_sc_Suc_minus [of "number_of bin", simplified nobm1, standard]
kleing@24333
   479
huffman@24465
   480
subsection {* Operations on lists of booleans *}
huffman@24465
   481
haftmann@26558
   482
primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where
haftmann@26558
   483
  Nil: "bl_to_bin_aux [] w = w"
haftmann@26558
   484
  | Cons: "bl_to_bin_aux (b # bs) w = 
haftmann@26558
   485
      bl_to_bin_aux bs (w BIT (if b then bit.B1 else bit.B0))"
huffman@24465
   486
haftmann@26558
   487
definition bl_to_bin :: "bool list \<Rightarrow> int" where
haftmann@26558
   488
  bl_to_bin_def : "bl_to_bin bs = bl_to_bin_aux bs Int.Pls"
huffman@24465
   489
haftmann@26558
   490
primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
haftmann@26558
   491
  Z: "bin_to_bl_aux 0 w bl = bl"
haftmann@26558
   492
  | Suc: "bin_to_bl_aux (Suc n) w bl =
haftmann@26558
   493
      bin_to_bl_aux n (bin_rest w) ((bin_last w = bit.B1) # bl)"
huffman@24465
   494
haftmann@26558
   495
definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" where
haftmann@26558
   496
  bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
huffman@24465
   497
haftmann@26558
   498
primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" where
haftmann@26558
   499
  Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
haftmann@26558
   500
  | Z: "bl_of_nth 0 f = []"
huffman@24465
   501
haftmann@26558
   502
primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
haftmann@26558
   503
  Z: "takefill fill 0 xs = []"
haftmann@26558
   504
  | Suc: "takefill fill (Suc n) xs = (
haftmann@26558
   505
      case xs of [] => fill # takefill fill n xs
haftmann@26558
   506
        | y # ys => y # takefill fill n ys)"
huffman@24465
   507
haftmann@26558
   508
definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
haftmann@26558
   509
  "map2 f as bs = map (split f) (zip as bs)"
huffman@24465
   510
huffman@24465
   511
huffman@24364
   512
subsection {* Splitting and concatenation *}
kleing@24333
   513
haftmann@26558
   514
definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
haftmann@26558
   515
  "bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls"
haftmann@26558
   516
krauss@28042
   517
fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
haftmann@26558
   518
  "bin_rsplit_aux n m c bs =
huffman@24364
   519
    (if m = 0 | n = 0 then bs else
huffman@24364
   520
      let (a, b) = bin_split n c 
haftmann@26558
   521
      in bin_rsplit_aux n (m - n) a (b # bs))"
huffman@24364
   522
haftmann@26558
   523
definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
haftmann@26558
   524
  "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
haftmann@26558
   525
krauss@28042
   526
fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
haftmann@26558
   527
  "bin_rsplitl_aux n m c bs =
huffman@24364
   528
    (if m = 0 | n = 0 then bs else
huffman@24364
   529
      let (a, b) = bin_split (min m n) c 
haftmann@26558
   530
      in bin_rsplitl_aux n (m - n) a (b # bs))"
huffman@24364
   531
haftmann@26558
   532
definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
haftmann@26558
   533
  "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
haftmann@26558
   534
huffman@24364
   535
declare bin_rsplit_aux.simps [simp del]
huffman@24364
   536
declare bin_rsplitl_aux.simps [simp del]
huffman@24364
   537
huffman@24364
   538
lemma bin_sign_cat: 
huffman@24364
   539
  "!!y. bin_sign (bin_cat x n y) = bin_sign x"
huffman@24364
   540
  by (induct n) auto
huffman@24364
   541
huffman@24364
   542
lemma bin_cat_Suc_Bit:
huffman@24364
   543
  "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
huffman@24364
   544
  by auto
huffman@24364
   545
huffman@24364
   546
lemma bin_nth_cat: 
huffman@24364
   547
  "!!n y. bin_nth (bin_cat x k y) n = 
huffman@24364
   548
    (if n < k then bin_nth y n else bin_nth x (n - k))"
huffman@24364
   549
  apply (induct k)
huffman@24364
   550
   apply clarsimp
huffman@24364
   551
  apply (case_tac n, auto)
kleing@24333
   552
  done
kleing@24333
   553
huffman@24364
   554
lemma bin_nth_split:
huffman@24364
   555
  "!!b c. bin_split n c = (a, b) ==> 
huffman@24364
   556
    (ALL k. bin_nth a k = bin_nth c (n + k)) & 
huffman@24364
   557
    (ALL k. bin_nth b k = (k < n & bin_nth c k))"
kleing@24333
   558
  apply (induct n)
huffman@24364
   559
   apply clarsimp
huffman@24364
   560
  apply (clarsimp simp: Let_def split: ls_splits)
huffman@24364
   561
  apply (case_tac k)
huffman@24364
   562
  apply auto
huffman@24364
   563
  done
huffman@24364
   564
huffman@24364
   565
lemma bin_cat_assoc: 
huffman@24364
   566
  "!!z. bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)" 
huffman@24364
   567
  by (induct n) auto
huffman@24364
   568
huffman@24364
   569
lemma bin_cat_assoc_sym: "!!z m. 
huffman@24364
   570
  bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
huffman@24364
   571
  apply (induct n, clarsimp)
huffman@24364
   572
  apply (case_tac m, auto)
kleing@24333
   573
  done
kleing@24333
   574
huffman@24364
   575
lemma bin_cat_Pls [simp]: 
haftmann@25919
   576
  "!!w. bin_cat Int.Pls n w = bintrunc n w"
huffman@24364
   577
  by (induct n) auto
huffman@24364
   578
huffman@24364
   579
lemma bintr_cat1: 
huffman@24364
   580
  "!!b. bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
huffman@24364
   581
  by (induct n) auto
huffman@24364
   582
    
huffman@24364
   583
lemma bintr_cat: "bintrunc m (bin_cat a n b) = 
huffman@24364
   584
    bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
huffman@24364
   585
  by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
huffman@24364
   586
    
huffman@24364
   587
lemma bintr_cat_same [simp]: 
huffman@24364
   588
  "bintrunc n (bin_cat a n b) = bintrunc n b"
huffman@24364
   589
  by (auto simp add : bintr_cat)
huffman@24364
   590
huffman@24364
   591
lemma cat_bintr [simp]: 
huffman@24364
   592
  "!!b. bin_cat a n (bintrunc n b) = bin_cat a n b"
huffman@24364
   593
  by (induct n) auto
huffman@24364
   594
huffman@24364
   595
lemma split_bintrunc: 
huffman@24364
   596
  "!!b c. bin_split n c = (a, b) ==> b = bintrunc n c"
huffman@24364
   597
  by (induct n) (auto simp: Let_def split: ls_splits)
huffman@24364
   598
huffman@24364
   599
lemma bin_cat_split:
huffman@24364
   600
  "!!v w. bin_split n w = (u, v) ==> w = bin_cat u n v"
huffman@24364
   601
  by (induct n) (auto simp: Let_def split: ls_splits)
huffman@24364
   602
huffman@24364
   603
lemma bin_split_cat:
huffman@24364
   604
  "!!w. bin_split n (bin_cat v n w) = (v, bintrunc n w)"
huffman@24364
   605
  by (induct n) auto
huffman@24364
   606
huffman@24364
   607
lemma bin_split_Pls [simp]:
haftmann@25919
   608
  "bin_split n Int.Pls = (Int.Pls, Int.Pls)"
huffman@24364
   609
  by (induct n) (auto simp: Let_def split: ls_splits)
huffman@24364
   610
huffman@24364
   611
lemma bin_split_Min [simp]:
haftmann@25919
   612
  "bin_split n Int.Min = (Int.Min, bintrunc n Int.Min)"
huffman@24364
   613
  by (induct n) (auto simp: Let_def split: ls_splits)
huffman@24364
   614
huffman@24364
   615
lemma bin_split_trunc:
huffman@24364
   616
  "!!m b c. bin_split (min m n) c = (a, b) ==> 
huffman@24364
   617
    bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
huffman@24364
   618
  apply (induct n, clarsimp)
huffman@24364
   619
  apply (simp add: bin_rest_trunc Let_def split: ls_splits)
huffman@24364
   620
  apply (case_tac m)
huffman@24364
   621
   apply (auto simp: Let_def split: ls_splits)
kleing@24333
   622
  done
kleing@24333
   623
huffman@24364
   624
lemma bin_split_trunc1:
huffman@24364
   625
  "!!m b c. bin_split n c = (a, b) ==> 
huffman@24364
   626
    bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
huffman@24364
   627
  apply (induct n, clarsimp)
huffman@24364
   628
  apply (simp add: bin_rest_trunc Let_def split: ls_splits)
huffman@24364
   629
  apply (case_tac m)
huffman@24364
   630
   apply (auto simp: Let_def split: ls_splits)
huffman@24364
   631
  done
kleing@24333
   632
huffman@24364
   633
lemma bin_cat_num:
huffman@24364
   634
  "!!b. bin_cat a n b = a * 2 ^ n + bintrunc n b"
huffman@24364
   635
  apply (induct n, clarsimp)
huffman@24364
   636
  apply (simp add: Bit_def cong: number_of_False_cong)
huffman@24364
   637
  done
huffman@24364
   638
huffman@24364
   639
lemma bin_split_num:
huffman@24364
   640
  "!!b. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
huffman@24364
   641
  apply (induct n, clarsimp)
huffman@24364
   642
  apply (simp add: bin_rest_div zdiv_zmult2_eq)
huffman@24364
   643
  apply (case_tac b rule: bin_exhaust)
huffman@24364
   644
  apply simp
huffman@24364
   645
  apply (simp add: Bit_def zmod_zmult_zmult1 p1mod22k
huffman@24364
   646
              split: bit.split 
huffman@24364
   647
              cong: number_of_False_cong)
huffman@24364
   648
  done 
huffman@24364
   649
huffman@24364
   650
subsection {* Miscellaneous lemmas *}
kleing@24333
   651
kleing@24333
   652
lemma nth_2p_bin: 
kleing@24333
   653
  "!!m. bin_nth (2 ^ n) m = (m = n)"
kleing@24333
   654
  apply (induct n)
kleing@24333
   655
   apply clarsimp
kleing@24333
   656
   apply safe
kleing@24333
   657
     apply (case_tac m) 
kleing@24333
   658
      apply (auto simp: trans [OF numeral_1_eq_1 [symmetric] number_of_eq])
kleing@24333
   659
   apply (case_tac m) 
kleing@24333
   660
    apply (auto simp: Bit_B0_2t [symmetric])
kleing@24333
   661
  done
kleing@24333
   662
kleing@24333
   663
(* for use when simplifying with bin_nth_Bit *)
kleing@24333
   664
kleing@24333
   665
lemma ex_eq_or:
kleing@24333
   666
  "(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))"
kleing@24333
   667
  by auto
kleing@24333
   668
kleing@24333
   669
end
kleing@24333
   670