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