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