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