src/HOL/Word/BinGeneral.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 30034 60f64f112174
child 30940 663af91c0720
permissions -rw-r--r--
added lemmas
kleing@24333
     1
(* 
kleing@24333
     2
  Author: Jeremy Dawson, NICTA
kleing@24333
     3
kleing@24333
     4
  contains basic definition to do with integers
kleing@24333
     5
  expressed using Pls, Min, BIT and important resulting theorems, 
kleing@24333
     6
  in particular, bin_rec and related work
kleing@24333
     7
*) 
kleing@24333
     8
huffman@24350
     9
header {* Basic Definitions for Binary Integers *}
huffman@24350
    10
haftmann@26557
    11
theory BinGeneral
haftmann@26557
    12
imports Num_Lemmas
kleing@24333
    13
begin
kleing@24333
    14
haftmann@26557
    15
subsection {* Further properties of numerals *}
haftmann@26557
    16
haftmann@26557
    17
datatype bit = B0 | B1
haftmann@26557
    18
haftmann@26557
    19
definition
haftmann@26557
    20
  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
haftmann@26557
    21
  "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
haftmann@26557
    22
haftmann@26557
    23
lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w"
haftmann@26557
    24
  unfolding Bit_def Bit0_def by simp
haftmann@26557
    25
haftmann@26557
    26
lemma BIT_B1_eq_Bit1 [simp]: "w BIT B1 = Int.Bit1 w"
haftmann@26557
    27
  unfolding Bit_def Bit1_def by simp
haftmann@26557
    28
haftmann@26557
    29
lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
huffman@24384
    30
haftmann@26557
    31
hide (open) const B0 B1
haftmann@26557
    32
haftmann@26557
    33
lemma Min_ne_Pls [iff]:  
haftmann@26557
    34
  "Int.Min ~= Int.Pls"
haftmann@26557
    35
  unfolding Min_def Pls_def by auto
haftmann@26557
    36
haftmann@26557
    37
lemmas Pls_ne_Min [iff] = Min_ne_Pls [symmetric]
haftmann@26557
    38
haftmann@26557
    39
lemmas PlsMin_defs [intro!] = 
haftmann@26557
    40
  Pls_def Min_def Pls_def [symmetric] Min_def [symmetric]
haftmann@26557
    41
haftmann@26557
    42
lemmas PlsMin_simps [simp] = PlsMin_defs [THEN Eq_TrueI]
haftmann@26557
    43
haftmann@26557
    44
lemma number_of_False_cong: 
haftmann@26557
    45
  "False \<Longrightarrow> number_of x = number_of y"
haftmann@26557
    46
  by (rule FalseE)
haftmann@26557
    47
haftmann@26557
    48
(** ways in which type Bin resembles a datatype **)
huffman@24350
    49
haftmann@26557
    50
lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c"
haftmann@26557
    51
  apply (unfold Bit_def)
haftmann@26557
    52
  apply (simp (no_asm_use) split: bit.split_asm)
haftmann@26557
    53
     apply simp_all
haftmann@26557
    54
   apply (drule_tac f=even in arg_cong, clarsimp)+
haftmann@26557
    55
  done
haftmann@26557
    56
     
haftmann@26557
    57
lemmas BIT_eqE [elim!] = BIT_eq [THEN conjE, standard]
haftmann@26557
    58
haftmann@26557
    59
lemma BIT_eq_iff [simp]: 
haftmann@26557
    60
  "(u BIT b = v BIT c) = (u = v \<and> b = c)"
haftmann@26557
    61
  by (rule iffI) auto
haftmann@26557
    62
haftmann@26557
    63
lemmas BIT_eqI [intro!] = conjI [THEN BIT_eq_iff [THEN iffD2]]
haftmann@26557
    64
haftmann@26557
    65
lemma less_Bits: 
haftmann@26557
    66
  "(v BIT b < w BIT c) = (v < w | v <= w & b = bit.B0 & c = bit.B1)"
haftmann@26557
    67
  unfolding Bit_def by (auto split: bit.split)
kleing@24333
    68
haftmann@26557
    69
lemma le_Bits: 
haftmann@26557
    70
  "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= bit.B1 | c ~= bit.B0))" 
haftmann@26557
    71
  unfolding Bit_def by (auto split: bit.split)
haftmann@26557
    72
haftmann@26557
    73
lemma no_no [simp]: "number_of (number_of i) = i"
haftmann@26557
    74
  unfolding number_of_eq by simp
haftmann@26557
    75
haftmann@26557
    76
lemma Bit_B0:
haftmann@26557
    77
  "k BIT bit.B0 = k + k"
haftmann@26557
    78
   by (unfold Bit_def) simp
haftmann@26557
    79
haftmann@26557
    80
lemma Bit_B1:
haftmann@26557
    81
  "k BIT bit.B1 = k + k + 1"
haftmann@26557
    82
   by (unfold Bit_def) simp
haftmann@26557
    83
  
haftmann@26557
    84
lemma Bit_B0_2t: "k BIT bit.B0 = 2 * k"
haftmann@26557
    85
  by (rule trans, rule Bit_B0) simp
haftmann@26557
    86
haftmann@26557
    87
lemma Bit_B1_2t: "k BIT bit.B1 = 2 * k + 1"
haftmann@26557
    88
  by (rule trans, rule Bit_B1) simp
haftmann@26557
    89
haftmann@26557
    90
lemma B_mod_2': 
haftmann@26557
    91
  "X = 2 ==> (w BIT bit.B1) mod X = 1 & (w BIT bit.B0) mod X = 0"
haftmann@26557
    92
  apply (simp (no_asm) only: Bit_B0 Bit_B1)
haftmann@26557
    93
  apply (simp add: z1pmod2)
huffman@24465
    94
  done
kleing@24333
    95
haftmann@26557
    96
lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1"
haftmann@26557
    97
  unfolding numeral_simps number_of_is_id by (simp add: z1pmod2)
kleing@24333
    98
haftmann@26557
    99
lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0"
haftmann@26557
   100
  unfolding numeral_simps number_of_is_id by simp
huffman@26086
   101
haftmann@26557
   102
lemma neB1E [elim!]:
haftmann@26557
   103
  assumes ne: "y \<noteq> bit.B1"
haftmann@26557
   104
  assumes y: "y = bit.B0 \<Longrightarrow> P"
haftmann@26557
   105
  shows "P"
haftmann@26557
   106
  apply (rule y)
haftmann@26557
   107
  apply (cases y rule: bit.exhaust, simp)
haftmann@26557
   108
  apply (simp add: ne)
haftmann@26557
   109
  done
huffman@26086
   110
haftmann@26557
   111
lemma bin_ex_rl: "EX w b. w BIT b = bin"
haftmann@26557
   112
  apply (unfold Bit_def)
haftmann@26557
   113
  apply (cases "even bin")
haftmann@26557
   114
   apply (clarsimp simp: even_equiv_def)
haftmann@26557
   115
   apply (auto simp: odd_equiv_def split: bit.split)
huffman@26086
   116
  done
huffman@26086
   117
haftmann@26557
   118
lemma bin_exhaust:
haftmann@26557
   119
  assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
haftmann@26557
   120
  shows "Q"
haftmann@26557
   121
  apply (insert bin_ex_rl [of bin])  
haftmann@26557
   122
  apply (erule exE)+
haftmann@26557
   123
  apply (rule Q)
haftmann@26557
   124
  apply force
huffman@26086
   125
  done
kleing@24333
   126
kleing@24333
   127
huffman@24465
   128
subsection {* Destructors for binary integers *}
huffman@24364
   129
haftmann@26557
   130
definition bin_rl :: "int \<Rightarrow> int \<times> bit" where 
haftmann@28562
   131
  [code del]: "bin_rl w = (THE (r, l). w = r BIT l)"
haftmann@26557
   132
haftmann@26557
   133
lemma bin_rl_char: "(bin_rl w = (r, l)) = (r BIT l = w)"
haftmann@26557
   134
  apply (unfold bin_rl_def)
haftmann@26557
   135
  apply safe
haftmann@26557
   136
   apply (cases w rule: bin_exhaust)
haftmann@26557
   137
   apply auto
haftmann@26557
   138
  done
haftmann@26557
   139
haftmann@26514
   140
definition
haftmann@28562
   141
  bin_rest_def [code del]: "bin_rest w = fst (bin_rl w)"
haftmann@26514
   142
haftmann@26514
   143
definition
haftmann@28562
   144
  bin_last_def [code del] : "bin_last w = snd (bin_rl w)"
huffman@24465
   145
haftmann@26514
   146
primrec bin_nth where
haftmann@26557
   147
  Z: "bin_nth w 0 = (bin_last w = bit.B1)"
haftmann@26557
   148
  | Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
huffman@24364
   149
huffman@24465
   150
lemma bin_rl: "bin_rl w = (bin_rest w, bin_last w)"
huffman@24465
   151
  unfolding bin_rest_def bin_last_def by auto
huffman@24465
   152
haftmann@26557
   153
lemma bin_rl_simps [simp]:
haftmann@26557
   154
  "bin_rl Int.Pls = (Int.Pls, bit.B0)"
haftmann@26557
   155
  "bin_rl Int.Min = (Int.Min, bit.B1)"
haftmann@26557
   156
  "bin_rl (Int.Bit0 r) = (r, bit.B0)"
haftmann@26557
   157
  "bin_rl (Int.Bit1 r) = (r, bit.B1)"
haftmann@26557
   158
  "bin_rl (r BIT b) = (r, b)"
haftmann@26557
   159
  unfolding bin_rl_char by simp_all
haftmann@26557
   160
haftmann@28562
   161
declare bin_rl_simps(1-4) [code]
haftmann@26557
   162
huffman@24465
   163
lemmas bin_rl_simp [simp] = iffD1 [OF bin_rl_char bin_rl]
huffman@24364
   164
haftmann@26557
   165
lemma bin_abs_lem:
haftmann@26557
   166
  "bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
haftmann@26557
   167
    nat (abs w) < nat (abs bin)"
haftmann@26557
   168
  apply (clarsimp simp add: bin_rl_char)
haftmann@26557
   169
  apply (unfold Pls_def Min_def Bit_def)
haftmann@26557
   170
  apply (cases b)
haftmann@26557
   171
   apply (clarsimp, arith)
haftmann@26557
   172
  apply (clarsimp, arith)
haftmann@26557
   173
  done
haftmann@26557
   174
haftmann@26557
   175
lemma bin_induct:
haftmann@26557
   176
  assumes PPls: "P Int.Pls"
haftmann@26557
   177
    and PMin: "P Int.Min"
haftmann@26557
   178
    and PBit: "!!bin bit. P bin ==> P (bin BIT bit)"
haftmann@26557
   179
  shows "P bin"
haftmann@26557
   180
  apply (rule_tac P=P and a=bin and f1="nat o abs" 
haftmann@26557
   181
                  in wf_measure [THEN wf_induct])
haftmann@26557
   182
  apply (simp add: measure_def inv_image_def)
haftmann@26557
   183
  apply (case_tac x rule: bin_exhaust)
haftmann@26557
   184
  apply (frule bin_abs_lem)
haftmann@26557
   185
  apply (auto simp add : PPls PMin PBit)
haftmann@26557
   186
  done
haftmann@26557
   187
haftmann@26557
   188
lemma numeral_induct:
haftmann@26557
   189
  assumes Pls: "P Int.Pls"
haftmann@26557
   190
  assumes Min: "P Int.Min"
haftmann@26557
   191
  assumes Bit0: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Pls\<rbrakk> \<Longrightarrow> P (Int.Bit0 w)"
haftmann@26557
   192
  assumes Bit1: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Min\<rbrakk> \<Longrightarrow> P (Int.Bit1 w)"
haftmann@26557
   193
  shows "P x"
haftmann@26557
   194
  apply (induct x rule: bin_induct)
haftmann@26557
   195
    apply (rule Pls)
haftmann@26557
   196
   apply (rule Min)
haftmann@26557
   197
  apply (case_tac bit)
haftmann@26557
   198
   apply (case_tac "bin = Int.Pls")
haftmann@26557
   199
    apply simp
haftmann@26557
   200
   apply (simp add: Bit0)
haftmann@26557
   201
  apply (case_tac "bin = Int.Min")
haftmann@26557
   202
   apply simp
haftmann@26557
   203
  apply (simp add: Bit1)
haftmann@26557
   204
  done
haftmann@26557
   205
huffman@24465
   206
lemma bin_rest_simps [simp]: 
haftmann@25919
   207
  "bin_rest Int.Pls = Int.Pls"
haftmann@25919
   208
  "bin_rest Int.Min = Int.Min"
huffman@26086
   209
  "bin_rest (Int.Bit0 w) = w"
huffman@26086
   210
  "bin_rest (Int.Bit1 w) = w"
haftmann@26514
   211
  "bin_rest (w BIT b) = w"
huffman@24465
   212
  unfolding bin_rest_def by auto
huffman@24465
   213
haftmann@28562
   214
declare bin_rest_simps(1-4) [code]
haftmann@26514
   215
huffman@24465
   216
lemma bin_last_simps [simp]: 
haftmann@25919
   217
  "bin_last Int.Pls = bit.B0"
haftmann@25919
   218
  "bin_last Int.Min = bit.B1"
huffman@26086
   219
  "bin_last (Int.Bit0 w) = bit.B0"
huffman@26086
   220
  "bin_last (Int.Bit1 w) = bit.B1"
haftmann@26514
   221
  "bin_last (w BIT b) = b"
huffman@24465
   222
  unfolding bin_last_def by auto
huffman@26086
   223
haftmann@28562
   224
declare bin_last_simps(1-4) [code]
haftmann@26514
   225
kleing@24333
   226
lemma bin_r_l_extras [simp]:
kleing@24333
   227
  "bin_last 0 = bit.B0"
kleing@24333
   228
  "bin_last (- 1) = bit.B1"
kleing@24333
   229
  "bin_last -1 = bit.B1"
kleing@24333
   230
  "bin_last 1 = bit.B1"
kleing@24333
   231
  "bin_rest 1 = 0"
kleing@24333
   232
  "bin_rest 0 = 0"
kleing@24333
   233
  "bin_rest (- 1) = - 1"
kleing@24333
   234
  "bin_rest -1 = -1"
kleing@24333
   235
  apply (unfold number_of_Min)
kleing@24333
   236
  apply (unfold Pls_def [symmetric] Min_def [symmetric])
kleing@24333
   237
  apply (unfold numeral_1_eq_1 [symmetric])
kleing@24333
   238
  apply (auto simp: number_of_eq) 
kleing@24333
   239
  done
kleing@24333
   240
kleing@24333
   241
lemma bin_last_mod: 
kleing@24333
   242
  "bin_last w = (if w mod 2 = 0 then bit.B0 else bit.B1)"
huffman@24465
   243
  apply (case_tac w rule: bin_exhaust)
huffman@24465
   244
  apply (case_tac b)
huffman@24465
   245
   apply auto
kleing@24333
   246
  done
kleing@24333
   247
kleing@24333
   248
lemma bin_rest_div: 
kleing@24333
   249
  "bin_rest w = w div 2"
huffman@24465
   250
  apply (case_tac w rule: bin_exhaust)
huffman@24465
   251
  apply (rule trans)
huffman@24465
   252
   apply clarsimp
huffman@24465
   253
   apply (rule refl)
huffman@24465
   254
  apply (drule trans)
huffman@24465
   255
   apply (rule Bit_def)
huffman@24465
   256
  apply (simp add: z1pdiv2 split: bit.split)
kleing@24333
   257
  done
kleing@24333
   258
kleing@24333
   259
lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
kleing@24333
   260
  unfolding bin_rest_div [symmetric] by auto
kleing@24333
   261
huffman@26086
   262
lemma Bit0_div2 [simp]: "(Int.Bit0 w) div 2 = w"
huffman@26086
   263
  using Bit_div2 [where b=bit.B0] by simp
huffman@26086
   264
huffman@26086
   265
lemma Bit1_div2 [simp]: "(Int.Bit1 w) div 2 = w"
huffman@26086
   266
  using Bit_div2 [where b=bit.B1] by simp
huffman@26086
   267
kleing@24333
   268
lemma bin_nth_lem [rule_format]:
kleing@24333
   269
  "ALL y. bin_nth x = bin_nth y --> x = y"
kleing@24333
   270
  apply (induct x rule: bin_induct)
kleing@24333
   271
    apply safe
kleing@24333
   272
    apply (erule rev_mp)
kleing@24333
   273
    apply (induct_tac y rule: bin_induct)
berghofe@26827
   274
      apply (safe del: subset_antisym)
kleing@24333
   275
      apply (drule_tac x=0 in fun_cong, force)
kleing@24333
   276
     apply (erule notE, rule ext, 
kleing@24333
   277
            drule_tac x="Suc x" in fun_cong, force)
kleing@24333
   278
    apply (drule_tac x=0 in fun_cong, force)
kleing@24333
   279
   apply (erule rev_mp)
kleing@24333
   280
   apply (induct_tac y rule: bin_induct)
berghofe@26827
   281
     apply (safe del: subset_antisym)
kleing@24333
   282
     apply (drule_tac x=0 in fun_cong, force)
kleing@24333
   283
    apply (erule notE, rule ext, 
kleing@24333
   284
           drule_tac x="Suc x" in fun_cong, force)
kleing@24333
   285
   apply (drule_tac x=0 in fun_cong, force)
kleing@24333
   286
  apply (case_tac y rule: bin_exhaust)
kleing@24333
   287
  apply clarify
kleing@24333
   288
  apply (erule allE)
kleing@24333
   289
  apply (erule impE)
kleing@24333
   290
   prefer 2
kleing@24333
   291
   apply (erule BIT_eqI)
kleing@24333
   292
   apply (drule_tac x=0 in fun_cong, force)
kleing@24333
   293
  apply (rule ext)
kleing@24333
   294
  apply (drule_tac x="Suc ?x" in fun_cong, force)
kleing@24333
   295
  done
kleing@24333
   296
kleing@24333
   297
lemma bin_nth_eq_iff: "(bin_nth x = bin_nth y) = (x = y)"
kleing@24333
   298
  by (auto elim: bin_nth_lem)
kleing@24333
   299
kleing@24333
   300
lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1], standard]
kleing@24333
   301
haftmann@25919
   302
lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n"
kleing@24333
   303
  by (induct n) auto
kleing@24333
   304
haftmann@25919
   305
lemma bin_nth_Min [simp]: "bin_nth Int.Min n"
kleing@24333
   306
  by (induct n) auto
kleing@24333
   307
kleing@24333
   308
lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = bit.B1)"
kleing@24333
   309
  by auto
kleing@24333
   310
kleing@24333
   311
lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n"
kleing@24333
   312
  by auto
kleing@24333
   313
kleing@24333
   314
lemma bin_nth_minus [simp]: "0 < n ==> bin_nth (w BIT b) n = bin_nth w (n - 1)"
kleing@24333
   315
  by (cases n) auto
kleing@24333
   316
huffman@26086
   317
lemma bin_nth_minus_Bit0 [simp]:
huffman@26086
   318
  "0 < n ==> bin_nth (Int.Bit0 w) n = bin_nth w (n - 1)"
huffman@26086
   319
  using bin_nth_minus [where b=bit.B0] by simp
huffman@26086
   320
huffman@26086
   321
lemma bin_nth_minus_Bit1 [simp]:
huffman@26086
   322
  "0 < n ==> bin_nth (Int.Bit1 w) n = bin_nth w (n - 1)"
huffman@26086
   323
  using bin_nth_minus [where b=bit.B1] by simp
huffman@26086
   324
kleing@24333
   325
lemmas bin_nth_0 = bin_nth.simps(1)
kleing@24333
   326
lemmas bin_nth_Suc = bin_nth.simps(2)
kleing@24333
   327
kleing@24333
   328
lemmas bin_nth_simps = 
kleing@24333
   329
  bin_nth_0 bin_nth_Suc bin_nth_Pls bin_nth_Min bin_nth_minus
huffman@26086
   330
  bin_nth_minus_Bit0 bin_nth_minus_Bit1
kleing@24333
   331
haftmann@26557
   332
haftmann@26557
   333
subsection {* Recursion combinator for binary integers *}
haftmann@26557
   334
haftmann@26557
   335
lemma brlem: "(bin = Int.Min) = (- bin + Int.pred 0 = 0)"
haftmann@26557
   336
  unfolding Min_def pred_def by arith
haftmann@26557
   337
haftmann@26557
   338
function
haftmann@26557
   339
  bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a"  
haftmann@26557
   340
where 
haftmann@26557
   341
  "bin_rec f1 f2 f3 bin = (if bin = Int.Pls then f1 
haftmann@26557
   342
    else if bin = Int.Min then f2
haftmann@26557
   343
    else case bin_rl bin of (w, b) => f3 w b (bin_rec f1 f2 f3 w))"
haftmann@26557
   344
  by pat_completeness auto
haftmann@26557
   345
haftmann@26557
   346
termination 
haftmann@26557
   347
  apply (relation "measure (nat o abs o snd o snd o snd)")
haftmann@26557
   348
   apply simp
haftmann@26557
   349
  apply (simp add: Pls_def brlem)
haftmann@26557
   350
  apply (clarsimp simp: bin_rl_char pred_def)
haftmann@26557
   351
  apply (frule thin_rl [THEN refl [THEN bin_abs_lem [rule_format]]]) 
haftmann@26557
   352
    apply (unfold Pls_def Min_def number_of_eq)
haftmann@26557
   353
    prefer 2
haftmann@26557
   354
    apply (erule asm_rl)
haftmann@26557
   355
   apply auto
haftmann@26557
   356
  done
haftmann@26557
   357
haftmann@26557
   358
declare bin_rec.simps [simp del]
haftmann@26557
   359
haftmann@26557
   360
lemma bin_rec_PM:
haftmann@26557
   361
  "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
haftmann@26557
   362
  by (auto simp add: bin_rec.simps)
haftmann@26557
   363
haftmann@26557
   364
lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
haftmann@26557
   365
  by (simp add: bin_rec.simps)
haftmann@26557
   366
haftmann@26557
   367
lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
haftmann@26557
   368
  by (simp add: bin_rec.simps)
haftmann@26557
   369
haftmann@26557
   370
lemma bin_rec_Bit0:
haftmann@26557
   371
  "f3 Int.Pls bit.B0 f1 = f1 \<Longrightarrow>
haftmann@26557
   372
    bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)"
huffman@28959
   373
  by (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
haftmann@26557
   374
haftmann@26557
   375
lemma bin_rec_Bit1:
haftmann@26557
   376
  "f3 Int.Min bit.B1 f2 = f2 \<Longrightarrow>
haftmann@26557
   377
    bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)"
huffman@28959
   378
  by (simp add: bin_rec_Min bin_rec.simps [of _ _ _ "Int.Bit1 w"])
haftmann@26557
   379
  
haftmann@26557
   380
lemma bin_rec_Bit:
haftmann@26557
   381
  "f = bin_rec f1 f2 f3  ==> f3 Int.Pls bit.B0 f1 = f1 ==> 
haftmann@26557
   382
    f3 Int.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
haftmann@26557
   383
  by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1)
haftmann@26557
   384
haftmann@26557
   385
lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
haftmann@26557
   386
  bin_rec_Bit0 bin_rec_Bit1
haftmann@26557
   387
haftmann@26557
   388
haftmann@26557
   389
subsection {* Truncating binary integers *}
haftmann@26557
   390
haftmann@26557
   391
definition
haftmann@28562
   392
  bin_sign_def [code del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
haftmann@26557
   393
haftmann@26557
   394
lemma bin_sign_simps [simp]:
haftmann@26557
   395
  "bin_sign Int.Pls = Int.Pls"
haftmann@26557
   396
  "bin_sign Int.Min = Int.Min"
haftmann@26557
   397
  "bin_sign (Int.Bit0 w) = bin_sign w"
haftmann@26557
   398
  "bin_sign (Int.Bit1 w) = bin_sign w"
haftmann@26557
   399
  "bin_sign (w BIT b) = bin_sign w"
haftmann@26557
   400
  unfolding bin_sign_def by (auto simp: bin_rec_simps)
haftmann@26557
   401
haftmann@28562
   402
declare bin_sign_simps(1-4) [code]
haftmann@26557
   403
huffman@24364
   404
lemma bin_sign_rest [simp]: 
huffman@24364
   405
  "bin_sign (bin_rest w) = (bin_sign w)"
haftmann@26557
   406
  by (cases w rule: bin_exhaust) auto
huffman@24364
   407
huffman@24364
   408
consts
huffman@24364
   409
  bintrunc :: "nat => int => int"
huffman@24364
   410
primrec 
haftmann@25919
   411
  Z : "bintrunc 0 bin = Int.Pls"
huffman@24364
   412
  Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"
huffman@24364
   413
huffman@24364
   414
consts
huffman@24364
   415
  sbintrunc :: "nat => int => int" 
huffman@24364
   416
primrec 
huffman@24364
   417
  Z : "sbintrunc 0 bin = 
haftmann@25919
   418
    (case bin_last bin of bit.B1 => Int.Min | bit.B0 => Int.Pls)"
huffman@24364
   419
  Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
huffman@24364
   420
kleing@24333
   421
lemma sign_bintr:
haftmann@25919
   422
  "!!w. bin_sign (bintrunc n w) = Int.Pls"
kleing@24333
   423
  by (induct n) auto
kleing@24333
   424
kleing@24333
   425
lemma bintrunc_mod2p:
kleing@24333
   426
  "!!w. bintrunc n w = (w mod 2 ^ n :: int)"
kleing@24333
   427
  apply (induct n, clarsimp)
kleing@24333
   428
  apply (simp add: bin_last_mod bin_rest_div Bit_def zmod_zmult2_eq
kleing@24333
   429
              cong: number_of_False_cong)
kleing@24333
   430
  done
kleing@24333
   431
kleing@24333
   432
lemma sbintrunc_mod2p:
kleing@24333
   433
  "!!w. sbintrunc n w = ((w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n :: int)"
kleing@24333
   434
  apply (induct n)
kleing@24333
   435
   apply clarsimp
nipkow@30034
   436
   apply (subst mod_add_left_eq)
kleing@24333
   437
   apply (simp add: bin_last_mod)
kleing@24333
   438
   apply (simp add: number_of_eq)
kleing@24333
   439
  apply clarsimp
kleing@24333
   440
  apply (simp add: bin_last_mod bin_rest_div Bit_def 
kleing@24333
   441
              cong: number_of_False_cong)
kleing@24333
   442
  apply (clarsimp simp: zmod_zmult_zmult1 [symmetric] 
kleing@24333
   443
         zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
kleing@24333
   444
  apply (rule trans [symmetric, OF _ emep1])
kleing@24333
   445
     apply auto
kleing@24333
   446
  apply (auto simp: even_def)
kleing@24333
   447
  done
kleing@24333
   448
huffman@24465
   449
subsection "Simplifications for (s)bintrunc"
huffman@24465
   450
huffman@24465
   451
lemma bit_bool:
huffman@24465
   452
  "(b = (b' = bit.B1)) = (b' = (if b then bit.B1 else bit.B0))"
huffman@24465
   453
  by (cases b') auto
huffman@24465
   454
huffman@24465
   455
lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric]
kleing@24333
   456
kleing@24333
   457
lemma bin_sign_lem:
haftmann@25919
   458
  "!!bin. (bin_sign (sbintrunc n bin) = Int.Min) = bin_nth bin n"
kleing@24333
   459
  apply (induct n)
kleing@24333
   460
   apply (case_tac bin rule: bin_exhaust, case_tac b, auto)+
kleing@24333
   461
  done
kleing@24333
   462
kleing@24333
   463
lemma nth_bintr:
kleing@24333
   464
  "!!w m. bin_nth (bintrunc m w) n = (n < m & bin_nth w n)"
kleing@24333
   465
  apply (induct n)
kleing@24333
   466
   apply (case_tac m, auto)[1]
kleing@24333
   467
  apply (case_tac m, auto)[1]
kleing@24333
   468
  done
kleing@24333
   469
kleing@24333
   470
lemma nth_sbintr:
kleing@24333
   471
  "!!w m. bin_nth (sbintrunc m w) n = 
kleing@24333
   472
          (if n < m then bin_nth w n else bin_nth w m)"
kleing@24333
   473
  apply (induct n)
kleing@24333
   474
   apply (case_tac m, simp_all split: bit.splits)[1]
kleing@24333
   475
  apply (case_tac m, simp_all split: bit.splits)[1]
kleing@24333
   476
  done
kleing@24333
   477
kleing@24333
   478
lemma bin_nth_Bit:
kleing@24333
   479
  "bin_nth (w BIT b) n = (n = 0 & b = bit.B1 | (EX m. n = Suc m & bin_nth w m))"
kleing@24333
   480
  by (cases n) auto
kleing@24333
   481
huffman@26086
   482
lemma bin_nth_Bit0:
huffman@26086
   483
  "bin_nth (Int.Bit0 w) n = (EX m. n = Suc m & bin_nth w m)"
huffman@26086
   484
  using bin_nth_Bit [where b=bit.B0] by simp
huffman@26086
   485
huffman@26086
   486
lemma bin_nth_Bit1:
huffman@26086
   487
  "bin_nth (Int.Bit1 w) n = (n = 0 | (EX m. n = Suc m & bin_nth w m))"
huffman@26086
   488
  using bin_nth_Bit [where b=bit.B1] by simp
huffman@26086
   489
kleing@24333
   490
lemma bintrunc_bintrunc_l:
kleing@24333
   491
  "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)"
kleing@24333
   492
  by (rule bin_eqI) (auto simp add : nth_bintr)
kleing@24333
   493
kleing@24333
   494
lemma sbintrunc_sbintrunc_l:
kleing@24333
   495
  "n <= m ==> (sbintrunc m (sbintrunc n w) = sbintrunc n w)"
kleing@24333
   496
  by (rule bin_eqI) (auto simp: nth_sbintr min_def)
kleing@24333
   497
kleing@24333
   498
lemma bintrunc_bintrunc_ge:
kleing@24333
   499
  "n <= m ==> (bintrunc n (bintrunc m w) = bintrunc n w)"
kleing@24333
   500
  by (rule bin_eqI) (auto simp: nth_bintr)
kleing@24333
   501
kleing@24333
   502
lemma bintrunc_bintrunc_min [simp]:
kleing@24333
   503
  "bintrunc m (bintrunc n w) = bintrunc (min m n) w"
kleing@24333
   504
  apply (unfold min_def)
kleing@24333
   505
  apply (rule bin_eqI)
kleing@24333
   506
  apply (auto simp: nth_bintr)
kleing@24333
   507
  done
kleing@24333
   508
kleing@24333
   509
lemma sbintrunc_sbintrunc_min [simp]:
kleing@24333
   510
  "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
kleing@24333
   511
  apply (unfold min_def)
kleing@24333
   512
  apply (rule bin_eqI)
kleing@24333
   513
  apply (auto simp: nth_sbintr)
kleing@24333
   514
  done
kleing@24333
   515
kleing@24333
   516
lemmas bintrunc_Pls = 
haftmann@25919
   517
  bintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps, standard]
kleing@24333
   518
kleing@24333
   519
lemmas bintrunc_Min [simp] = 
haftmann@25919
   520
  bintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps, standard]
kleing@24333
   521
kleing@24333
   522
lemmas bintrunc_BIT  [simp] = 
wenzelm@25349
   523
  bintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
kleing@24333
   524
huffman@26086
   525
lemma bintrunc_Bit0 [simp]:
huffman@26086
   526
  "bintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (bintrunc n w)"
huffman@26086
   527
  using bintrunc_BIT [where b=bit.B0] by simp
huffman@26086
   528
huffman@26086
   529
lemma bintrunc_Bit1 [simp]:
huffman@26086
   530
  "bintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (bintrunc n w)"
huffman@26086
   531
  using bintrunc_BIT [where b=bit.B1] by simp
huffman@26086
   532
kleing@24333
   533
lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT
huffman@26086
   534
  bintrunc_Bit0 bintrunc_Bit1
kleing@24333
   535
kleing@24333
   536
lemmas sbintrunc_Suc_Pls = 
haftmann@25919
   537
  sbintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps, standard]
kleing@24333
   538
kleing@24333
   539
lemmas sbintrunc_Suc_Min = 
haftmann@25919
   540
  sbintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps, standard]
kleing@24333
   541
kleing@24333
   542
lemmas sbintrunc_Suc_BIT [simp] = 
wenzelm@25349
   543
  sbintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
kleing@24333
   544
huffman@26086
   545
lemma sbintrunc_Suc_Bit0 [simp]:
huffman@26086
   546
  "sbintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (sbintrunc n w)"
huffman@26086
   547
  using sbintrunc_Suc_BIT [where b=bit.B0] by simp
huffman@26086
   548
huffman@26086
   549
lemma sbintrunc_Suc_Bit1 [simp]:
huffman@26086
   550
  "sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)"
huffman@26086
   551
  using sbintrunc_Suc_BIT [where b=bit.B1] by simp
huffman@26086
   552
kleing@24333
   553
lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
huffman@26086
   554
  sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1
kleing@24333
   555
kleing@24333
   556
lemmas sbintrunc_Pls = 
haftmann@25919
   557
  sbintrunc.Z [where bin="Int.Pls", 
wenzelm@25349
   558
               simplified bin_last_simps bin_rest_simps bit.simps, standard]
kleing@24333
   559
kleing@24333
   560
lemmas sbintrunc_Min = 
haftmann@25919
   561
  sbintrunc.Z [where bin="Int.Min", 
wenzelm@25349
   562
               simplified bin_last_simps bin_rest_simps bit.simps, standard]
kleing@24333
   563
kleing@24333
   564
lemmas sbintrunc_0_BIT_B0 [simp] = 
wenzelm@25349
   565
  sbintrunc.Z [where bin="w BIT bit.B0", 
wenzelm@25349
   566
               simplified bin_last_simps bin_rest_simps bit.simps, standard]
kleing@24333
   567
kleing@24333
   568
lemmas sbintrunc_0_BIT_B1 [simp] = 
wenzelm@25349
   569
  sbintrunc.Z [where bin="w BIT bit.B1", 
wenzelm@25349
   570
               simplified bin_last_simps bin_rest_simps bit.simps, standard]
kleing@24333
   571
huffman@26086
   572
lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = Int.Pls"
huffman@26086
   573
  using sbintrunc_0_BIT_B0 by simp
huffman@26086
   574
huffman@26086
   575
lemma sbintrunc_0_Bit1 [simp]: "sbintrunc 0 (Int.Bit1 w) = Int.Min"
huffman@26086
   576
  using sbintrunc_0_BIT_B1 by simp
huffman@26086
   577
kleing@24333
   578
lemmas sbintrunc_0_simps =
kleing@24333
   579
  sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1
huffman@26086
   580
  sbintrunc_0_Bit0 sbintrunc_0_Bit1
kleing@24333
   581
kleing@24333
   582
lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs
kleing@24333
   583
lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs
kleing@24333
   584
kleing@24333
   585
lemma bintrunc_minus:
kleing@24333
   586
  "0 < n ==> bintrunc (Suc (n - 1)) w = bintrunc n w"
kleing@24333
   587
  by auto
kleing@24333
   588
kleing@24333
   589
lemma sbintrunc_minus:
kleing@24333
   590
  "0 < n ==> sbintrunc (Suc (n - 1)) w = sbintrunc n w"
kleing@24333
   591
  by auto
kleing@24333
   592
kleing@24333
   593
lemmas bintrunc_minus_simps = 
kleing@24333
   594
  bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans], standard]
kleing@24333
   595
lemmas sbintrunc_minus_simps = 
kleing@24333
   596
  sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans], standard]
kleing@24333
   597
kleing@24333
   598
lemma bintrunc_n_Pls [simp]:
haftmann@25919
   599
  "bintrunc n Int.Pls = Int.Pls"
kleing@24333
   600
  by (induct n) auto
kleing@24333
   601
kleing@24333
   602
lemma sbintrunc_n_PM [simp]:
haftmann@25919
   603
  "sbintrunc n Int.Pls = Int.Pls"
haftmann@25919
   604
  "sbintrunc n Int.Min = Int.Min"
kleing@24333
   605
  by (induct n) auto
kleing@24333
   606
wenzelm@25349
   607
lemmas thobini1 = arg_cong [where f = "%w. w BIT b", standard]
kleing@24333
   608
kleing@24333
   609
lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1]
kleing@24333
   610
lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1]
kleing@24333
   611
huffman@26086
   612
lemmas bmsts = bintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans], standard]
kleing@24333
   613
lemmas bintrunc_Pls_minus_I = bmsts(1)
kleing@24333
   614
lemmas bintrunc_Min_minus_I = bmsts(2)
kleing@24333
   615
lemmas bintrunc_BIT_minus_I = bmsts(3)
kleing@24333
   616
haftmann@25919
   617
lemma bintrunc_0_Min: "bintrunc 0 Int.Min = Int.Pls"
kleing@24333
   618
  by auto
haftmann@25919
   619
lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Int.Pls"
kleing@24333
   620
  by auto
kleing@24333
   621
kleing@24333
   622
lemma bintrunc_Suc_lem:
kleing@24333
   623
  "bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y"
kleing@24333
   624
  by auto
kleing@24333
   625
kleing@24333
   626
lemmas bintrunc_Suc_Ialts = 
kleing@26294
   627
  bintrunc_Min_I [THEN bintrunc_Suc_lem, standard]
kleing@26294
   628
  bintrunc_BIT_I [THEN bintrunc_Suc_lem, standard]
kleing@24333
   629
kleing@24333
   630
lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1]
kleing@24333
   631
kleing@24333
   632
lemmas sbintrunc_Suc_Is = 
huffman@26086
   633
  sbintrunc_Sucs(1-3) [THEN thobini1 [THEN [2] trans], standard]
kleing@24333
   634
kleing@24333
   635
lemmas sbintrunc_Suc_minus_Is = 
huffman@26086
   636
  sbintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans], standard]
kleing@24333
   637
kleing@24333
   638
lemma sbintrunc_Suc_lem:
kleing@24333
   639
  "sbintrunc (Suc n) x = y ==> m = Suc n ==> sbintrunc m x = y"
kleing@24333
   640
  by auto
kleing@24333
   641
kleing@24333
   642
lemmas sbintrunc_Suc_Ialts = 
kleing@24333
   643
  sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem, standard]
kleing@24333
   644
kleing@24333
   645
lemma sbintrunc_bintrunc_lt:
kleing@24333
   646
  "m > n ==> sbintrunc n (bintrunc m w) = sbintrunc n w"
kleing@24333
   647
  by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr)
kleing@24333
   648
kleing@24333
   649
lemma bintrunc_sbintrunc_le:
kleing@24333
   650
  "m <= Suc n ==> bintrunc m (sbintrunc n w) = bintrunc m w"
kleing@24333
   651
  apply (rule bin_eqI)
kleing@24333
   652
  apply (auto simp: nth_sbintr nth_bintr)
kleing@24333
   653
   apply (subgoal_tac "x=n", safe, arith+)[1]
kleing@24333
   654
  apply (subgoal_tac "x=n", safe, arith+)[1]
kleing@24333
   655
  done
kleing@24333
   656
kleing@24333
   657
lemmas bintrunc_sbintrunc [simp] = order_refl [THEN bintrunc_sbintrunc_le]
kleing@24333
   658
lemmas sbintrunc_bintrunc [simp] = lessI [THEN sbintrunc_bintrunc_lt]
kleing@24333
   659
lemmas bintrunc_bintrunc [simp] = order_refl [THEN bintrunc_bintrunc_l]
kleing@24333
   660
lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l] 
kleing@24333
   661
kleing@24333
   662
lemma bintrunc_sbintrunc' [simp]:
kleing@24333
   663
  "0 < n \<Longrightarrow> bintrunc n (sbintrunc (n - 1) w) = bintrunc n w"
kleing@24333
   664
  by (cases n) (auto simp del: bintrunc.Suc)
kleing@24333
   665
kleing@24333
   666
lemma sbintrunc_bintrunc' [simp]:
kleing@24333
   667
  "0 < n \<Longrightarrow> sbintrunc (n - 1) (bintrunc n w) = sbintrunc (n - 1) w"
kleing@24333
   668
  by (cases n) (auto simp del: bintrunc.Suc)
kleing@24333
   669
kleing@24333
   670
lemma bin_sbin_eq_iff: 
kleing@24333
   671
  "bintrunc (Suc n) x = bintrunc (Suc n) y <-> 
kleing@24333
   672
   sbintrunc n x = sbintrunc n y"
kleing@24333
   673
  apply (rule iffI)
kleing@24333
   674
   apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc])
kleing@24333
   675
   apply simp
kleing@24333
   676
  apply (rule box_equals [OF _ bintrunc_sbintrunc bintrunc_sbintrunc])
kleing@24333
   677
  apply simp
kleing@24333
   678
  done
kleing@24333
   679
kleing@24333
   680
lemma bin_sbin_eq_iff':
kleing@24333
   681
  "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y <-> 
kleing@24333
   682
            sbintrunc (n - 1) x = sbintrunc (n - 1) y"
kleing@24333
   683
  by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc)
kleing@24333
   684
kleing@24333
   685
lemmas bintrunc_sbintruncS0 [simp] = bintrunc_sbintrunc' [unfolded One_nat_def]
kleing@24333
   686
lemmas sbintrunc_bintruncS0 [simp] = sbintrunc_bintrunc' [unfolded One_nat_def]
kleing@24333
   687
kleing@24333
   688
lemmas bintrunc_bintrunc_l' = le_add1 [THEN bintrunc_bintrunc_l]
kleing@24333
   689
lemmas sbintrunc_sbintrunc_l' = le_add1 [THEN sbintrunc_sbintrunc_l]
kleing@24333
   690
kleing@24333
   691
(* although bintrunc_minus_simps, if added to default simpset,
kleing@24333
   692
  tends to get applied where it's not wanted in developing the theories,
kleing@24333
   693
  we get a version for when the word length is given literally *)
kleing@24333
   694
kleing@24333
   695
lemmas nat_non0_gr = 
nipkow@25134
   696
  trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl, standard]
kleing@24333
   697
kleing@24333
   698
lemmas bintrunc_pred_simps [simp] = 
kleing@24333
   699
  bintrunc_minus_simps [of "number_of bin", simplified nobm1, standard]
kleing@24333
   700
kleing@24333
   701
lemmas sbintrunc_pred_simps [simp] = 
kleing@24333
   702
  sbintrunc_minus_simps [of "number_of bin", simplified nobm1, standard]
kleing@24333
   703
kleing@24333
   704
lemma no_bintr_alt:
kleing@24333
   705
  "number_of (bintrunc n w) = w mod 2 ^ n"
kleing@24333
   706
  by (simp add: number_of_eq bintrunc_mod2p)
kleing@24333
   707
kleing@24333
   708
lemma no_bintr_alt1: "bintrunc n = (%w. w mod 2 ^ n :: int)"
kleing@24333
   709
  by (rule ext) (rule bintrunc_mod2p)
kleing@24333
   710
kleing@24333
   711
lemma range_bintrunc: "range (bintrunc n) = {i. 0 <= i & i < 2 ^ n}"
kleing@24333
   712
  apply (unfold no_bintr_alt1)
kleing@24333
   713
  apply (auto simp add: image_iff)
kleing@24333
   714
  apply (rule exI)
kleing@24333
   715
  apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
kleing@24333
   716
  done
kleing@24333
   717
kleing@24333
   718
lemma no_bintr: 
kleing@24333
   719
  "number_of (bintrunc n w) = (number_of w mod 2 ^ n :: int)"
kleing@24333
   720
  by (simp add : bintrunc_mod2p number_of_eq)
kleing@24333
   721
kleing@24333
   722
lemma no_sbintr_alt2: 
kleing@24333
   723
  "sbintrunc n = (%w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
kleing@24333
   724
  by (rule ext) (simp add : sbintrunc_mod2p)
kleing@24333
   725
kleing@24333
   726
lemma no_sbintr: 
kleing@24333
   727
  "number_of (sbintrunc n w) = 
kleing@24333
   728
   ((number_of w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
kleing@24333
   729
  by (simp add : no_sbintr_alt2 number_of_eq)
kleing@24333
   730
kleing@24333
   731
lemma range_sbintrunc: 
kleing@24333
   732
  "range (sbintrunc n) = {i. - (2 ^ n) <= i & i < 2 ^ n}"
kleing@24333
   733
  apply (unfold no_sbintr_alt2)
kleing@24333
   734
  apply (auto simp add: image_iff eq_diff_eq)
kleing@24333
   735
  apply (rule exI)
kleing@24333
   736
  apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
kleing@24333
   737
  done
kleing@24333
   738
wenzelm@25349
   739
lemma sb_inc_lem:
wenzelm@25349
   740
  "(a::int) + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)"
wenzelm@25349
   741
  apply (erule int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified zless2p])
wenzelm@25349
   742
  apply (rule TrueI)
wenzelm@25349
   743
  done
kleing@24333
   744
wenzelm@25349
   745
lemma sb_inc_lem':
wenzelm@25349
   746
  "(a::int) < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)"
wenzelm@25349
   747
  by (rule iffD1 [OF less_diff_eq, THEN sb_inc_lem, simplified OrderedGroup.diff_0])
kleing@24333
   748
kleing@24333
   749
lemma sbintrunc_inc:
wenzelm@25349
   750
  "x < - (2^n) ==> x + 2^(Suc n) <= sbintrunc n x"
kleing@24333
   751
  unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp
kleing@24333
   752
wenzelm@25349
   753
lemma sb_dec_lem:
wenzelm@25349
   754
  "(0::int) <= - (2^k) + a ==> (a + 2^k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
wenzelm@25349
   755
  by (rule int_mod_le' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k",
wenzelm@25349
   756
    simplified zless2p, OF _ TrueI, simplified])
kleing@24333
   757
wenzelm@25349
   758
lemma sb_dec_lem':
wenzelm@25349
   759
  "(2::int) ^ k <= a ==> (a + 2 ^ k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
wenzelm@25349
   760
  by (rule iffD1 [OF diff_le_eq', THEN sb_dec_lem, simplified])
kleing@24333
   761
kleing@24333
   762
lemma sbintrunc_dec:
kleing@24333
   763
  "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x"
kleing@24333
   764
  unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
kleing@24333
   765
wenzelm@25349
   766
lemmas zmod_uminus' = zmod_uminus [where b="c", standard]
wenzelm@25349
   767
lemmas zpower_zmod' = zpower_zmod [where m="c" and y="k", standard]
kleing@24333
   768
kleing@24333
   769
lemmas brdmod1s' [symmetric] = 
nipkow@30034
   770
  mod_add_left_eq mod_add_right_eq 
kleing@24333
   771
  zmod_zsub_left_eq zmod_zsub_right_eq 
kleing@24333
   772
  zmod_zmult1_eq zmod_zmult1_eq_rev 
kleing@24333
   773
kleing@24333
   774
lemmas brdmods' [symmetric] = 
kleing@24333
   775
  zpower_zmod' [symmetric]
nipkow@30034
   776
  trans [OF mod_add_left_eq mod_add_right_eq] 
kleing@24333
   777
  trans [OF zmod_zsub_left_eq zmod_zsub_right_eq] 
kleing@24333
   778
  trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev] 
kleing@24333
   779
  zmod_uminus' [symmetric]
nipkow@30034
   780
  mod_add_left_eq [where b = "1::int"]
kleing@24333
   781
  zmod_zsub_left_eq [where b = "1"]
kleing@24333
   782
kleing@24333
   783
lemmas bintr_arith1s =
nipkow@30034
   784
  brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard]
kleing@24333
   785
lemmas bintr_ariths =
nipkow@30034
   786
  brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard]
kleing@24333
   787
wenzelm@25349
   788
lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p, standard] 
huffman@24364
   789
kleing@24333
   790
lemma bintr_ge0: "(0 :: int) <= number_of (bintrunc n w)"
kleing@24333
   791
  by (simp add : no_bintr m2pths)
kleing@24333
   792
kleing@24333
   793
lemma bintr_lt2p: "number_of (bintrunc n w) < (2 ^ n :: int)"
kleing@24333
   794
  by (simp add : no_bintr m2pths)
kleing@24333
   795
kleing@24333
   796
lemma bintr_Min: 
haftmann@25919
   797
  "number_of (bintrunc n Int.Min) = (2 ^ n :: int) - 1"
kleing@24333
   798
  by (simp add : no_bintr m1mod2k)
kleing@24333
   799
kleing@24333
   800
lemma sbintr_ge: "(- (2 ^ n) :: int) <= number_of (sbintrunc n w)"
kleing@24333
   801
  by (simp add : no_sbintr m2pths)
kleing@24333
   802
kleing@24333
   803
lemma sbintr_lt: "number_of (sbintrunc n w) < (2 ^ n :: int)"
kleing@24333
   804
  by (simp add : no_sbintr m2pths)
kleing@24333
   805
kleing@24333
   806
lemma bintrunc_Suc:
kleing@24333
   807
  "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT bin_last bin"
kleing@24333
   808
  by (case_tac bin rule: bin_exhaust) auto
kleing@24333
   809
kleing@24333
   810
lemma sign_Pls_ge_0: 
haftmann@25919
   811
  "(bin_sign bin = Int.Pls) = (number_of bin >= (0 :: int))"
huffman@26086
   812
  by (induct bin rule: numeral_induct) auto
kleing@24333
   813
kleing@24333
   814
lemma sign_Min_lt_0: 
haftmann@25919
   815
  "(bin_sign bin = Int.Min) = (number_of bin < (0 :: int))"
huffman@26086
   816
  by (induct bin rule: numeral_induct) auto
kleing@24333
   817
kleing@24333
   818
lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]] 
kleing@24333
   819
kleing@24333
   820
lemma bin_rest_trunc:
kleing@24333
   821
  "!!bin. (bin_rest (bintrunc n bin)) = bintrunc (n - 1) (bin_rest bin)"
kleing@24333
   822
  by (induct n) auto
kleing@24333
   823
kleing@24333
   824
lemma bin_rest_power_trunc [rule_format] :
kleing@24333
   825
  "(bin_rest ^ k) (bintrunc n bin) = 
kleing@24333
   826
    bintrunc (n - k) ((bin_rest ^ k) bin)"
kleing@24333
   827
  by (induct k) (auto simp: bin_rest_trunc)
kleing@24333
   828
kleing@24333
   829
lemma bin_rest_trunc_i:
kleing@24333
   830
  "bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)"
kleing@24333
   831
  by auto
kleing@24333
   832
kleing@24333
   833
lemma bin_rest_strunc:
kleing@24333
   834
  "!!bin. bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)"
kleing@24333
   835
  by (induct n) auto
kleing@24333
   836
kleing@24333
   837
lemma bintrunc_rest [simp]: 
kleing@24333
   838
  "!!bin. bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)"
kleing@24333
   839
  apply (induct n, simp)
kleing@24333
   840
  apply (case_tac bin rule: bin_exhaust)
kleing@24333
   841
  apply (auto simp: bintrunc_bintrunc_l)
kleing@24333
   842
  done
kleing@24333
   843
kleing@24333
   844
lemma sbintrunc_rest [simp]:
kleing@24333
   845
  "!!bin. sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)"
kleing@24333
   846
  apply (induct n, simp)
kleing@24333
   847
  apply (case_tac bin rule: bin_exhaust)
kleing@24333
   848
  apply (auto simp: bintrunc_bintrunc_l split: bit.splits)
kleing@24333
   849
  done
kleing@24333
   850
kleing@24333
   851
lemma bintrunc_rest':
kleing@24333
   852
  "bintrunc n o bin_rest o bintrunc n = bin_rest o bintrunc n"
kleing@24333
   853
  by (rule ext) auto
kleing@24333
   854
kleing@24333
   855
lemma sbintrunc_rest' :
kleing@24333
   856
  "sbintrunc n o bin_rest o sbintrunc n = bin_rest o sbintrunc n"
kleing@24333
   857
  by (rule ext) auto
kleing@24333
   858
kleing@24333
   859
lemma rco_lem:
kleing@24333
   860
  "f o g o f = g o f ==> f o (g o f) ^ n = g ^ n o f"
kleing@24333
   861
  apply (rule ext)
kleing@24333
   862
  apply (induct_tac n)
kleing@24333
   863
   apply (simp_all (no_asm))
kleing@24333
   864
  apply (drule fun_cong)
kleing@24333
   865
  apply (unfold o_def)
kleing@24333
   866
  apply (erule trans)
kleing@24333
   867
  apply simp
kleing@24333
   868
  done
kleing@24333
   869
kleing@24333
   870
lemma rco_alt: "(f o g) ^ n o f = f o (g o f) ^ n"
kleing@24333
   871
  apply (rule ext)
kleing@24333
   872
  apply (induct n)
kleing@24333
   873
   apply (simp_all add: o_def)
kleing@24333
   874
  done
kleing@24333
   875
kleing@24333
   876
lemmas rco_bintr = bintrunc_rest' 
kleing@24333
   877
  [THEN rco_lem [THEN fun_cong], unfolded o_def]
kleing@24333
   878
lemmas rco_sbintr = sbintrunc_rest' 
kleing@24333
   879
  [THEN rco_lem [THEN fun_cong], unfolded o_def]
kleing@24333
   880
huffman@24364
   881
subsection {* Splitting and concatenation *}
huffman@24364
   882
haftmann@26557
   883
primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" where
haftmann@26557
   884
  Z: "bin_split 0 w = (w, Int.Pls)"
haftmann@26557
   885
  | Suc: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
haftmann@26557
   886
        in (w1, w2 BIT bin_last w))"
huffman@24364
   887
haftmann@26557
   888
primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int" where
haftmann@26557
   889
  Z: "bin_cat w 0 v = w"
haftmann@26557
   890
  | Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
huffman@24364
   891
huffman@24364
   892
subsection {* Miscellaneous lemmas *}
huffman@24364
   893
huffman@24364
   894
lemmas funpow_minus_simp = 
huffman@24364
   895
  trans [OF gen_minus [where f = "power f"] funpow_Suc, standard]
huffman@24364
   896
huffman@24364
   897
lemmas funpow_pred_simp [simp] =
huffman@24364
   898
  funpow_minus_simp [of "number_of bin", simplified nobm1, standard]
huffman@24364
   899
huffman@24364
   900
lemmas replicate_minus_simp = 
huffman@24364
   901
  trans [OF gen_minus [where f = "%n. replicate n x"] replicate.replicate_Suc,
huffman@24364
   902
         standard]
huffman@24364
   903
huffman@24364
   904
lemmas replicate_pred_simp [simp] =
huffman@24364
   905
  replicate_minus_simp [of "number_of bin", simplified nobm1, standard]
huffman@24364
   906
wenzelm@25349
   907
lemmas power_Suc_no [simp] = power_Suc [of "number_of a", standard]
huffman@24364
   908
huffman@24364
   909
lemmas power_minus_simp = 
huffman@24364
   910
  trans [OF gen_minus [where f = "power f"] power_Suc, standard]
huffman@24364
   911
huffman@24364
   912
lemmas power_pred_simp = 
huffman@24364
   913
  power_minus_simp [of "number_of bin", simplified nobm1, standard]
wenzelm@25349
   914
lemmas power_pred_simp_no [simp] = power_pred_simp [where f= "number_of f", standard]
huffman@24364
   915
huffman@24364
   916
lemma list_exhaust_size_gt0:
huffman@24364
   917
  assumes y: "\<And>a list. y = a # list \<Longrightarrow> P"
huffman@24364
   918
  shows "0 < length y \<Longrightarrow> P"
huffman@24364
   919
  apply (cases y, simp)
huffman@24364
   920
  apply (rule y)
huffman@24364
   921
  apply fastsimp
huffman@24364
   922
  done
huffman@24364
   923
huffman@24364
   924
lemma list_exhaust_size_eq0:
huffman@24364
   925
  assumes y: "y = [] \<Longrightarrow> P"
huffman@24364
   926
  shows "length y = 0 \<Longrightarrow> P"
huffman@24364
   927
  apply (cases y)
huffman@24364
   928
   apply (rule y, simp)
huffman@24364
   929
  apply simp
huffman@24364
   930
  done
huffman@24364
   931
huffman@24364
   932
lemma size_Cons_lem_eq:
huffman@24364
   933
  "y = xa # list ==> size y = Suc k ==> size list = k"
huffman@24364
   934
  by auto
huffman@24364
   935
huffman@24364
   936
lemma size_Cons_lem_eq_bin:
haftmann@25919
   937
  "y = xa # list ==> size y = number_of (Int.succ k) ==> 
huffman@24364
   938
    size list = number_of k"
huffman@24364
   939
  by (auto simp: pred_def succ_def split add : split_if_asm)
huffman@24364
   940
kleing@24333
   941
lemmas ls_splits = 
kleing@24333
   942
  prod.split split_split prod.split_asm split_split_asm split_if_asm
kleing@24333
   943
kleing@24333
   944
lemma not_B1_is_B0: "y \<noteq> bit.B1 \<Longrightarrow> y = bit.B0"
kleing@24333
   945
  by (cases y) auto
kleing@24333
   946
kleing@24333
   947
lemma B1_ass_B0: 
kleing@24333
   948
  assumes y: "y = bit.B0 \<Longrightarrow> y = bit.B1"
kleing@24333
   949
  shows "y = bit.B1"
kleing@24333
   950
  apply (rule classical)
kleing@24333
   951
  apply (drule not_B1_is_B0)
kleing@24333
   952
  apply (erule y)
kleing@24333
   953
  done
kleing@24333
   954
kleing@24333
   955
-- "simplifications for specific word lengths"
kleing@24333
   956
lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc'
kleing@24333
   957
kleing@24333
   958
lemmas s2n_ths = n2s_ths [symmetric]
kleing@24333
   959
kleing@24333
   960
end