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