src/HOL/Word/Bit_Representation.thy
changeset 47108 2a1953f0d20d
parent 46607 6ae8121448af
child 47163 248376f8881d
     1.1 --- a/src/HOL/Word/Bit_Representation.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Word/Bit_Representation.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -47,41 +47,49 @@
     1.4    by (metis bin_rest_BIT bin_last_BIT)
     1.5  
     1.6  lemma BIT_bin_simps [simp]:
     1.7 -  "number_of w BIT 0 = number_of (Int.Bit0 w)"
     1.8 -  "number_of w BIT 1 = number_of (Int.Bit1 w)"
     1.9 -  unfolding Bit_def number_of_is_id numeral_simps by simp_all
    1.10 +  "numeral k BIT 0 = numeral (Num.Bit0 k)"
    1.11 +  "numeral k BIT 1 = numeral (Num.Bit1 k)"
    1.12 +  "neg_numeral k BIT 0 = neg_numeral (Num.Bit0 k)"
    1.13 +  "neg_numeral k BIT 1 = neg_numeral (Num.BitM k)"
    1.14 +  unfolding neg_numeral_def numeral.simps numeral_BitM
    1.15 +  unfolding Bit_def bitval_simps
    1.16 +  by (simp_all del: arith_simps add_numeral_special diff_numeral_special)
    1.17  
    1.18  lemma BIT_special_simps [simp]:
    1.19    shows "0 BIT 0 = 0" and "0 BIT 1 = 1" and "1 BIT 0 = 2" and "1 BIT 1 = 3"
    1.20    unfolding Bit_def by simp_all
    1.21  
    1.22 +lemma BitM_inc: "Num.BitM (Num.inc w) = Num.Bit1 w"
    1.23 +  by (induct w, simp_all)
    1.24 +
    1.25 +lemma expand_BIT:
    1.26 +  "numeral (Num.Bit0 w) = numeral w BIT 0"
    1.27 +  "numeral (Num.Bit1 w) = numeral w BIT 1"
    1.28 +  "neg_numeral (Num.Bit0 w) = neg_numeral w BIT 0"
    1.29 +  "neg_numeral (Num.Bit1 w) = neg_numeral (w + Num.One) BIT 1"
    1.30 +  unfolding add_One by (simp_all add: BitM_inc)
    1.31 +
    1.32  lemma bin_last_numeral_simps [simp]:
    1.33    "bin_last 0 = 0"
    1.34    "bin_last 1 = 1"
    1.35    "bin_last -1 = 1"
    1.36 -  "bin_last (number_of (Int.Bit0 w)) = 0"
    1.37 -  "bin_last (number_of (Int.Bit1 w)) = 1"
    1.38 -  unfolding bin_last_def by simp_all
    1.39 +  "bin_last Numeral1 = 1"
    1.40 +  "bin_last (numeral (Num.Bit0 w)) = 0"
    1.41 +  "bin_last (numeral (Num.Bit1 w)) = 1"
    1.42 +  "bin_last (neg_numeral (Num.Bit0 w)) = 0"
    1.43 +  "bin_last (neg_numeral (Num.Bit1 w)) = 1"
    1.44 +  unfolding expand_BIT bin_last_BIT by (simp_all add: bin_last_def)
    1.45  
    1.46  lemma bin_rest_numeral_simps [simp]:
    1.47    "bin_rest 0 = 0"
    1.48    "bin_rest 1 = 0"
    1.49    "bin_rest -1 = -1"
    1.50 -  "bin_rest (number_of (Int.Bit0 w)) = number_of w"
    1.51 -  "bin_rest (number_of (Int.Bit1 w)) = number_of w"
    1.52 -  unfolding bin_rest_def by simp_all
    1.53 -
    1.54 -lemma BIT_B0_eq_Bit0: "w BIT 0 = Int.Bit0 w"
    1.55 -  unfolding Bit_def Bit0_def by simp
    1.56 -
    1.57 -lemma BIT_B1_eq_Bit1: "w BIT 1 = Int.Bit1 w"
    1.58 -  unfolding Bit_def Bit1_def by simp
    1.59 -
    1.60 -lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
    1.61 -
    1.62 -lemma number_of_False_cong: 
    1.63 -  "False \<Longrightarrow> number_of x = number_of y"
    1.64 -  by (rule FalseE)
    1.65 +  "bin_rest Numeral1 = 0"
    1.66 +  "bin_rest (numeral (Num.Bit0 w)) = numeral w"
    1.67 +  "bin_rest (numeral (Num.Bit1 w)) = numeral w"
    1.68 +  "bin_rest (neg_numeral (Num.Bit0 w)) = neg_numeral w"
    1.69 +  "bin_rest (neg_numeral (Num.Bit1 w)) = neg_numeral (w + Num.One)"
    1.70 +  unfolding expand_BIT bin_rest_BIT by (simp_all add: bin_rest_def)
    1.71  
    1.72  lemma less_Bits: 
    1.73    "(v BIT b < w BIT c) = (v < w | v <= w & b = (0::bit) & c = (1::bit))"
    1.74 @@ -121,11 +129,7 @@
    1.75    done
    1.76  
    1.77  lemma bin_ex_rl: "EX w b. w BIT b = bin"
    1.78 -  apply (unfold Bit_def)
    1.79 -  apply (cases "even bin")
    1.80 -   apply (clarsimp simp: even_equiv_def)
    1.81 -   apply (auto simp: odd_equiv_def bitval_def split: bit.split)
    1.82 -  done
    1.83 +  by (metis bin_rl_simp)
    1.84  
    1.85  lemma bin_exhaust:
    1.86    assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
    1.87 @@ -144,18 +148,18 @@
    1.88    | Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
    1.89  
    1.90  lemma bin_abs_lem:
    1.91 -  "bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
    1.92 +  "bin = (w BIT b) ==> bin ~= -1 --> bin ~= 0 -->
    1.93      nat (abs w) < nat (abs bin)"
    1.94    apply clarsimp
    1.95 -  apply (unfold Pls_def Min_def Bit_def)
    1.96 +  apply (unfold Bit_def)
    1.97    apply (cases b)
    1.98     apply (clarsimp, arith)
    1.99    apply (clarsimp, arith)
   1.100    done
   1.101  
   1.102  lemma bin_induct:
   1.103 -  assumes PPls: "P Int.Pls"
   1.104 -    and PMin: "P Int.Min"
   1.105 +  assumes PPls: "P 0"
   1.106 +    and PMin: "P -1"
   1.107      and PBit: "!!bin bit. P bin ==> P (bin BIT bit)"
   1.108    shows "P bin"
   1.109    apply (rule_tac P=P and a=bin and f1="nat o abs" 
   1.110 @@ -166,54 +170,22 @@
   1.111    apply (auto simp add : PPls PMin PBit)
   1.112    done
   1.113  
   1.114 -lemma numeral_induct:
   1.115 -  assumes Pls: "P Int.Pls"
   1.116 -  assumes Min: "P Int.Min"
   1.117 -  assumes Bit0: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Pls\<rbrakk> \<Longrightarrow> P (Int.Bit0 w)"
   1.118 -  assumes Bit1: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Min\<rbrakk> \<Longrightarrow> P (Int.Bit1 w)"
   1.119 -  shows "P x"
   1.120 -  apply (induct x rule: bin_induct)
   1.121 -    apply (rule Pls)
   1.122 -   apply (rule Min)
   1.123 -  apply (case_tac bit)
   1.124 -   apply (case_tac "bin = Int.Pls")
   1.125 -    apply (simp add: BIT_simps)
   1.126 -   apply (simp add: Bit0 BIT_simps)
   1.127 -  apply (case_tac "bin = Int.Min")
   1.128 -   apply (simp add: BIT_simps)
   1.129 -  apply (simp add: Bit1 BIT_simps)
   1.130 -  done
   1.131 -
   1.132 -lemma bin_rest_simps [simp]: 
   1.133 -  "bin_rest Int.Pls = Int.Pls"
   1.134 -  "bin_rest Int.Min = Int.Min"
   1.135 -  "bin_rest (Int.Bit0 w) = w"
   1.136 -  "bin_rest (Int.Bit1 w) = w"
   1.137 -  unfolding numeral_simps by (auto simp: bin_rest_def)
   1.138 -
   1.139 -lemma bin_last_simps [simp]: 
   1.140 -  "bin_last Int.Pls = (0::bit)"
   1.141 -  "bin_last Int.Min = (1::bit)"
   1.142 -  "bin_last (Int.Bit0 w) = (0::bit)"
   1.143 -  "bin_last (Int.Bit1 w) = (1::bit)"
   1.144 -  unfolding numeral_simps by (auto simp: bin_last_def z1pmod2)
   1.145 -
   1.146  lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
   1.147    unfolding bin_rest_def [symmetric] by (rule bin_rest_BIT)
   1.148  
   1.149  lemma bin_nth_lem [rule_format]:
   1.150    "ALL y. bin_nth x = bin_nth y --> x = y"
   1.151 -  apply (induct x rule: bin_induct [unfolded Pls_def Min_def])
   1.152 +  apply (induct x rule: bin_induct)
   1.153      apply safe
   1.154      apply (erule rev_mp)
   1.155 -    apply (induct_tac y rule: bin_induct [unfolded Pls_def Min_def])
   1.156 +    apply (induct_tac y rule: bin_induct)
   1.157        apply safe
   1.158        apply (drule_tac x=0 in fun_cong, force)
   1.159       apply (erule notE, rule ext, 
   1.160              drule_tac x="Suc x" in fun_cong, force)
   1.161      apply (drule_tac x=0 in fun_cong, force)
   1.162     apply (erule rev_mp)
   1.163 -   apply (induct_tac y rule: bin_induct [unfolded Pls_def Min_def])
   1.164 +   apply (induct_tac y rule: bin_induct)
   1.165       apply safe
   1.166       apply (drule_tac x=0 in fun_cong, force)
   1.167      apply (erule notE, rule ext, 
   1.168 @@ -244,15 +216,9 @@
   1.169  lemma bin_nth_1 [simp]: "bin_nth 1 n \<longleftrightarrow> n = 0"
   1.170    by (cases n) simp_all
   1.171  
   1.172 -lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n"
   1.173 -  by (induct n) auto (* FIXME: delete *)
   1.174 -
   1.175  lemma bin_nth_minus1 [simp]: "bin_nth -1 n"
   1.176    by (induct n) auto
   1.177  
   1.178 -lemma bin_nth_Min [simp]: "bin_nth Int.Min n"
   1.179 -  by (induct n) auto (* FIXME: delete *)
   1.180 -
   1.181  lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = (1::bit))"
   1.182    by auto
   1.183  
   1.184 @@ -262,20 +228,20 @@
   1.185  lemma bin_nth_minus [simp]: "0 < n ==> bin_nth (w BIT b) n = bin_nth w (n - 1)"
   1.186    by (cases n) auto
   1.187  
   1.188 -lemma bin_nth_minus_Bit0 [simp]:
   1.189 -  "0 < n ==> bin_nth (number_of (Int.Bit0 w)) n = bin_nth (number_of w) (n - 1)"
   1.190 -  using bin_nth_minus [where w="number_of w" and b="(0::bit)"] by simp
   1.191 +lemma bin_nth_numeral:
   1.192 +  "bin_rest x = y \<Longrightarrow> bin_nth x (numeral n) = bin_nth y (numeral n - 1)"
   1.193 +  by (subst expand_Suc, simp only: bin_nth.simps)
   1.194  
   1.195 -lemma bin_nth_minus_Bit1 [simp]:
   1.196 -  "0 < n ==> bin_nth (number_of (Int.Bit1 w)) n = bin_nth (number_of w) (n - 1)"
   1.197 -  using bin_nth_minus [where w="number_of w" and b="(1::bit)"] by simp
   1.198 -
   1.199 -lemmas bin_nth_0 = bin_nth.simps(1)
   1.200 -lemmas bin_nth_Suc = bin_nth.simps(2)
   1.201 +lemmas bin_nth_numeral_simps [simp] =
   1.202 +  bin_nth_numeral [OF bin_rest_numeral_simps(2)]
   1.203 +  bin_nth_numeral [OF bin_rest_numeral_simps(5)]
   1.204 +  bin_nth_numeral [OF bin_rest_numeral_simps(6)]
   1.205 +  bin_nth_numeral [OF bin_rest_numeral_simps(7)]
   1.206 +  bin_nth_numeral [OF bin_rest_numeral_simps(8)]
   1.207  
   1.208  lemmas bin_nth_simps = 
   1.209 -  bin_nth_0 bin_nth_Suc bin_nth_zero bin_nth_minus1 bin_nth_minus
   1.210 -  bin_nth_minus_Bit0 bin_nth_minus_Bit1
   1.211 +  bin_nth.Z bin_nth.Suc bin_nth_zero bin_nth_minus1
   1.212 +  bin_nth_numeral_simps
   1.213  
   1.214  
   1.215  subsection {* Truncating binary integers *}
   1.216 @@ -286,9 +252,8 @@
   1.217  lemma bin_sign_simps [simp]:
   1.218    "bin_sign 0 = 0"
   1.219    "bin_sign 1 = 0"
   1.220 -  "bin_sign -1 = -1"
   1.221 -  "bin_sign (number_of (Int.Bit0 w)) = bin_sign (number_of w)"
   1.222 -  "bin_sign (number_of (Int.Bit1 w)) = bin_sign (number_of w)"
   1.223 +  "bin_sign (numeral k) = 0"
   1.224 +  "bin_sign (neg_numeral k) = -1"
   1.225    "bin_sign (w BIT b) = bin_sign w"
   1.226    unfolding bin_sign_def Bit_def bitval_def
   1.227    by (simp_all split: bit.split)
   1.228 @@ -309,17 +274,15 @@
   1.229    by (induct n arbitrary: w) auto
   1.230  
   1.231  lemma bintrunc_mod2p: "bintrunc n w = (w mod 2 ^ n)"
   1.232 -  apply (induct n arbitrary: w)
   1.233 -  apply simp
   1.234 +  apply (induct n arbitrary: w, clarsimp)
   1.235    apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq)
   1.236    done
   1.237  
   1.238  lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n"
   1.239    apply (induct n arbitrary: w)
   1.240 -   apply clarsimp
   1.241 +   apply simp
   1.242     apply (subst mod_add_left_eq)
   1.243     apply (simp add: bin_last_def)
   1.244 -  apply simp
   1.245    apply (simp add: bin_last_def bin_rest_def Bit_def)
   1.246    apply (clarsimp simp: mod_mult_mult1 [symmetric] 
   1.247           zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
   1.248 @@ -342,20 +305,32 @@
   1.249  lemma bintrunc_Suc_numeral:
   1.250    "bintrunc (Suc n) 1 = 1"
   1.251    "bintrunc (Suc n) -1 = bintrunc n -1 BIT 1"
   1.252 -  "bintrunc (Suc n) (number_of (Int.Bit0 w)) = bintrunc n (number_of w) BIT 0"
   1.253 -  "bintrunc (Suc n) (number_of (Int.Bit1 w)) = bintrunc n (number_of w) BIT 1"
   1.254 +  "bintrunc (Suc n) (numeral (Num.Bit0 w)) = bintrunc n (numeral w) BIT 0"
   1.255 +  "bintrunc (Suc n) (numeral (Num.Bit1 w)) = bintrunc n (numeral w) BIT 1"
   1.256 +  "bintrunc (Suc n) (neg_numeral (Num.Bit0 w)) =
   1.257 +    bintrunc n (neg_numeral w) BIT 0"
   1.258 +  "bintrunc (Suc n) (neg_numeral (Num.Bit1 w)) =
   1.259 +    bintrunc n (neg_numeral (w + Num.One)) BIT 1"
   1.260    by simp_all
   1.261  
   1.262  lemma sbintrunc_0_numeral [simp]:
   1.263    "sbintrunc 0 1 = -1"
   1.264 -  "sbintrunc 0 (number_of (Int.Bit0 w)) = 0"
   1.265 -  "sbintrunc 0 (number_of (Int.Bit1 w)) = -1"
   1.266 +  "sbintrunc 0 (numeral (Num.Bit0 w)) = 0"
   1.267 +  "sbintrunc 0 (numeral (Num.Bit1 w)) = -1"
   1.268 +  "sbintrunc 0 (neg_numeral (Num.Bit0 w)) = 0"
   1.269 +  "sbintrunc 0 (neg_numeral (Num.Bit1 w)) = -1"
   1.270    by simp_all
   1.271  
   1.272  lemma sbintrunc_Suc_numeral:
   1.273    "sbintrunc (Suc n) 1 = 1"
   1.274 -  "sbintrunc (Suc n) (number_of (Int.Bit0 w)) = sbintrunc n (number_of w) BIT 0"
   1.275 -  "sbintrunc (Suc n) (number_of (Int.Bit1 w)) = sbintrunc n (number_of w) BIT 1"
   1.276 +  "sbintrunc (Suc n) (numeral (Num.Bit0 w)) =
   1.277 +    sbintrunc n (numeral w) BIT 0"
   1.278 +  "sbintrunc (Suc n) (numeral (Num.Bit1 w)) =
   1.279 +    sbintrunc n (numeral w) BIT 1"
   1.280 +  "sbintrunc (Suc n) (neg_numeral (Num.Bit0 w)) =
   1.281 +    sbintrunc n (neg_numeral w) BIT 0"
   1.282 +  "sbintrunc (Suc n) (neg_numeral (Num.Bit1 w)) =
   1.283 +    sbintrunc n (neg_numeral (w + Num.One)) BIT 1"
   1.284    by simp_all
   1.285  
   1.286  lemma bit_bool:
   1.287 @@ -366,7 +341,7 @@
   1.288  
   1.289  lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = -1) = bin_nth bin n"
   1.290    apply (induct n arbitrary: bin)
   1.291 -   apply (case_tac bin rule: bin_exhaust, case_tac b, auto)+
   1.292 +  apply (case_tac bin rule: bin_exhaust, case_tac b, auto)
   1.293    done
   1.294  
   1.295  lemma nth_bintr: "bin_nth (bintrunc m w) n = (n < m & bin_nth w n)"
   1.296 @@ -388,14 +363,14 @@
   1.297    by (cases n) auto
   1.298  
   1.299  lemma bin_nth_Bit0:
   1.300 -  "bin_nth (number_of (Int.Bit0 w)) n \<longleftrightarrow>
   1.301 -    (\<exists>m. n = Suc m \<and> bin_nth (number_of w) m)"
   1.302 -  using bin_nth_Bit [where w="number_of w" and b="(0::bit)"] by simp
   1.303 +  "bin_nth (numeral (Num.Bit0 w)) n \<longleftrightarrow>
   1.304 +    (\<exists>m. n = Suc m \<and> bin_nth (numeral w) m)"
   1.305 +  using bin_nth_Bit [where w="numeral w" and b="(0::bit)"] by simp
   1.306  
   1.307  lemma bin_nth_Bit1:
   1.308 -  "bin_nth (number_of (Int.Bit1 w)) n \<longleftrightarrow>
   1.309 -    n = 0 \<or> (\<exists>m. n = Suc m \<and> bin_nth (number_of w) m)"
   1.310 -  using bin_nth_Bit [where w="number_of w" and b="(1::bit)"] by simp
   1.311 +  "bin_nth (numeral (Num.Bit1 w)) n \<longleftrightarrow>
   1.312 +    n = 0 \<or> (\<exists>m. n = Suc m \<and> bin_nth (numeral w) m)"
   1.313 +  using bin_nth_Bit [where w="numeral w" and b="(1::bit)"] by simp
   1.314  
   1.315  lemma bintrunc_bintrunc_l:
   1.316    "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)"
   1.317 @@ -422,72 +397,47 @@
   1.318    done
   1.319  
   1.320  lemmas bintrunc_Pls = 
   1.321 -  bintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps]
   1.322 +  bintrunc.Suc [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
   1.323  
   1.324  lemmas bintrunc_Min [simp] = 
   1.325 -  bintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps]
   1.326 +  bintrunc.Suc [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
   1.327  
   1.328  lemmas bintrunc_BIT  [simp] = 
   1.329    bintrunc.Suc [where bin="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
   1.330  
   1.331 -lemma bintrunc_Bit0 [simp]:
   1.332 -  "bintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (bintrunc n w)"
   1.333 -  using bintrunc_BIT [where b="(0::bit)"] by (simp add: BIT_simps)
   1.334 -
   1.335 -lemma bintrunc_Bit1 [simp]:
   1.336 -  "bintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (bintrunc n w)"
   1.337 -  using bintrunc_BIT [where b="(1::bit)"] by (simp add: BIT_simps)
   1.338 -
   1.339  lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT
   1.340 -  bintrunc_Bit0 bintrunc_Bit1
   1.341    bintrunc_Suc_numeral
   1.342  
   1.343  lemmas sbintrunc_Suc_Pls = 
   1.344 -  sbintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps]
   1.345 +  sbintrunc.Suc [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
   1.346  
   1.347  lemmas sbintrunc_Suc_Min = 
   1.348 -  sbintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps]
   1.349 +  sbintrunc.Suc [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
   1.350  
   1.351  lemmas sbintrunc_Suc_BIT [simp] = 
   1.352    sbintrunc.Suc [where bin="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
   1.353  
   1.354 -lemma sbintrunc_Suc_Bit0 [simp]:
   1.355 -  "sbintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (sbintrunc n w)"
   1.356 -  using sbintrunc_Suc_BIT [where b="(0::bit)"] by (simp add: BIT_simps)
   1.357 -
   1.358 -lemma sbintrunc_Suc_Bit1 [simp]:
   1.359 -  "sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)"
   1.360 -  using sbintrunc_Suc_BIT [where b="(1::bit)"] by (simp add: BIT_simps)
   1.361 -
   1.362  lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
   1.363 -  sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1
   1.364    sbintrunc_Suc_numeral
   1.365  
   1.366  lemmas sbintrunc_Pls = 
   1.367 -  sbintrunc.Z [where bin="Int.Pls", 
   1.368 -               simplified bin_last_simps bin_rest_simps bit.simps]
   1.369 +  sbintrunc.Z [where bin="0", 
   1.370 +               simplified bin_last_numeral_simps bin_rest_numeral_simps bit.simps]
   1.371  
   1.372  lemmas sbintrunc_Min = 
   1.373 -  sbintrunc.Z [where bin="Int.Min", 
   1.374 -               simplified bin_last_simps bin_rest_simps bit.simps]
   1.375 +  sbintrunc.Z [where bin="-1",
   1.376 +               simplified bin_last_numeral_simps bin_rest_numeral_simps bit.simps]
   1.377  
   1.378  lemmas sbintrunc_0_BIT_B0 [simp] = 
   1.379    sbintrunc.Z [where bin="w BIT (0::bit)", 
   1.380 -               simplified bin_last_simps bin_rest_simps bit.simps] for w
   1.381 +               simplified bin_last_numeral_simps bin_rest_numeral_simps bit.simps] for w
   1.382  
   1.383  lemmas sbintrunc_0_BIT_B1 [simp] = 
   1.384    sbintrunc.Z [where bin="w BIT (1::bit)", 
   1.385 -               simplified bin_last_simps bin_rest_simps bit.simps] for w
   1.386 -
   1.387 -lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = 0"
   1.388 -  using sbintrunc_0_BIT_B0 by simp
   1.389 -
   1.390 -lemma sbintrunc_0_Bit1 [simp]: "sbintrunc 0 (Int.Bit1 w) = -1"
   1.391 -  using sbintrunc_0_BIT_B1 by simp
   1.392 +               simplified bin_last_BIT bin_rest_numeral_simps bit.simps] for w
   1.393  
   1.394  lemmas sbintrunc_0_simps =
   1.395    sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1
   1.396 -  sbintrunc_0_Bit0 sbintrunc_0_Bit1
   1.397  
   1.398  lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs
   1.399  lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs
   1.400 @@ -505,15 +455,6 @@
   1.401  lemmas sbintrunc_minus_simps = 
   1.402    sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans]]
   1.403  
   1.404 -lemma bintrunc_n_Pls [simp]:
   1.405 -  "bintrunc n Int.Pls = Int.Pls"
   1.406 -  unfolding Pls_def by simp
   1.407 -
   1.408 -lemma sbintrunc_n_PM [simp]:
   1.409 -  "sbintrunc n Int.Pls = Int.Pls"
   1.410 -  "sbintrunc n Int.Min = Int.Min"
   1.411 -  unfolding Pls_def Min_def by simp_all
   1.412 -
   1.413  lemmas thobini1 = arg_cong [where f = "%w. w BIT b"] for b
   1.414  
   1.415  lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1]
   1.416 @@ -600,15 +541,39 @@
   1.417  lemmas nat_non0_gr = 
   1.418    trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl]
   1.419  
   1.420 -lemmas bintrunc_pred_simps [simp] = 
   1.421 -  bintrunc_minus_simps [of "number_of bin", simplified nobm1] for bin
   1.422 +lemma bintrunc_numeral:
   1.423 +  "bintrunc (numeral k) x =
   1.424 +    bintrunc (numeral k - 1) (bin_rest x) BIT bin_last x"
   1.425 +  by (subst expand_Suc, rule bintrunc.simps)
   1.426 +
   1.427 +lemma sbintrunc_numeral:
   1.428 +  "sbintrunc (numeral k) x =
   1.429 +    sbintrunc (numeral k - 1) (bin_rest x) BIT bin_last x"
   1.430 +  by (subst expand_Suc, rule sbintrunc.simps)
   1.431  
   1.432 -lemmas sbintrunc_pred_simps [simp] = 
   1.433 -  sbintrunc_minus_simps [of "number_of bin", simplified nobm1] for bin
   1.434 +lemma bintrunc_numeral_simps [simp]:
   1.435 +  "bintrunc (numeral k) (numeral (Num.Bit0 w)) =
   1.436 +    bintrunc (numeral k - 1) (numeral w) BIT 0"
   1.437 +  "bintrunc (numeral k) (numeral (Num.Bit1 w)) =
   1.438 +    bintrunc (numeral k - 1) (numeral w) BIT 1"
   1.439 +  "bintrunc (numeral k) (neg_numeral (Num.Bit0 w)) =
   1.440 +    bintrunc (numeral k - 1) (neg_numeral w) BIT 0"
   1.441 +  "bintrunc (numeral k) (neg_numeral (Num.Bit1 w)) =
   1.442 +    bintrunc (numeral k - 1) (neg_numeral (w + Num.One)) BIT 1"
   1.443 +  "bintrunc (numeral k) 1 = 1"
   1.444 +  by (simp_all add: bintrunc_numeral)
   1.445  
   1.446 -lemma no_bintr_alt:
   1.447 -  "number_of (bintrunc n w) = w mod 2 ^ n"
   1.448 -  by (simp add: number_of_eq bintrunc_mod2p)
   1.449 +lemma sbintrunc_numeral_simps [simp]:
   1.450 +  "sbintrunc (numeral k) (numeral (Num.Bit0 w)) =
   1.451 +    sbintrunc (numeral k - 1) (numeral w) BIT 0"
   1.452 +  "sbintrunc (numeral k) (numeral (Num.Bit1 w)) =
   1.453 +    sbintrunc (numeral k - 1) (numeral w) BIT 1"
   1.454 +  "sbintrunc (numeral k) (neg_numeral (Num.Bit0 w)) =
   1.455 +    sbintrunc (numeral k - 1) (neg_numeral w) BIT 0"
   1.456 +  "sbintrunc (numeral k) (neg_numeral (Num.Bit1 w)) =
   1.457 +    sbintrunc (numeral k - 1) (neg_numeral (w + Num.One)) BIT 1"
   1.458 +  "sbintrunc (numeral k) 1 = 1"
   1.459 +  by (simp_all add: sbintrunc_numeral)
   1.460  
   1.461  lemma no_bintr_alt1: "bintrunc n = (%w. w mod 2 ^ n :: int)"
   1.462    by (rule ext) (rule bintrunc_mod2p)
   1.463 @@ -620,19 +585,10 @@
   1.464    apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
   1.465    done
   1.466  
   1.467 -lemma no_bintr: 
   1.468 -  "number_of (bintrunc n w) = (number_of w mod 2 ^ n :: int)"
   1.469 -  by (simp add : bintrunc_mod2p number_of_eq)
   1.470 -
   1.471  lemma no_sbintr_alt2: 
   1.472    "sbintrunc n = (%w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
   1.473    by (rule ext) (simp add : sbintrunc_mod2p)
   1.474  
   1.475 -lemma no_sbintr: 
   1.476 -  "number_of (sbintrunc n w) = 
   1.477 -   ((number_of w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
   1.478 -  by (simp add : no_sbintr_alt2 number_of_eq)
   1.479 -
   1.480  lemma range_sbintrunc: 
   1.481    "range (sbintrunc n) = {i. - (2 ^ n) <= i & i < 2 ^ n}"
   1.482    apply (unfold no_sbintr_alt2)
   1.483 @@ -692,21 +648,20 @@
   1.484  
   1.485  lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p]
   1.486  
   1.487 -lemma bintr_ge0: "(0 :: int) <= number_of (bintrunc n w)"
   1.488 -  by (simp add : no_bintr m2pths)
   1.489 +lemma bintr_ge0: "0 \<le> bintrunc n w"
   1.490 +  by (simp add: bintrunc_mod2p)
   1.491  
   1.492 -lemma bintr_lt2p: "number_of (bintrunc n w) < (2 ^ n :: int)"
   1.493 -  by (simp add : no_bintr m2pths)
   1.494 +lemma bintr_lt2p: "bintrunc n w < 2 ^ n"
   1.495 +  by (simp add: bintrunc_mod2p)
   1.496  
   1.497 -lemma bintr_Min: 
   1.498 -  "number_of (bintrunc n Int.Min) = (2 ^ n :: int) - 1"
   1.499 -  by (simp add : no_bintr m1mod2k)
   1.500 +lemma bintr_Min: "bintrunc n -1 = 2 ^ n - 1"
   1.501 +  by (simp add: bintrunc_mod2p m1mod2k)
   1.502  
   1.503 -lemma sbintr_ge: "(- (2 ^ n) :: int) <= number_of (sbintrunc n w)"
   1.504 -  by (simp add : no_sbintr m2pths)
   1.505 +lemma sbintr_ge: "- (2 ^ n) \<le> sbintrunc n w"
   1.506 +  by (simp add: sbintrunc_mod2p)
   1.507  
   1.508 -lemma sbintr_lt: "number_of (sbintrunc n w) < (2 ^ n :: int)"
   1.509 -  by (simp add : no_sbintr m2pths)
   1.510 +lemma sbintr_lt: "sbintrunc n w < 2 ^ n"
   1.511 +  by (simp add: sbintrunc_mod2p)
   1.512  
   1.513  lemma sign_Pls_ge_0: 
   1.514    "(bin_sign bin = 0) = (bin >= (0 :: int))"
   1.515 @@ -716,8 +671,6 @@
   1.516    "(bin_sign bin = -1) = (bin < (0 :: int))"
   1.517    unfolding bin_sign_def by simp
   1.518  
   1.519 -lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]] 
   1.520 -
   1.521  lemma bin_rest_trunc:
   1.522    "(bin_rest (bintrunc n bin)) = bintrunc (n - 1) (bin_rest bin)"
   1.523    by (induct n arbitrary: bin) auto
   1.524 @@ -789,7 +742,7 @@
   1.525  lemma [code]:
   1.526    "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w) in (w1, w2 BIT bin_last w))"
   1.527    "bin_split 0 w = (w, 0)"
   1.528 -  by (simp_all add: Pls_def)
   1.529 +  by simp_all
   1.530  
   1.531  primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int" where
   1.532    Z: "bin_cat w 0 v = w"
   1.533 @@ -801,24 +754,17 @@
   1.534    "0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)"
   1.535    by (cases n) simp_all
   1.536  
   1.537 -lemmas funpow_pred_simp [simp] =
   1.538 -  funpow_minus_simp [of "number_of bin", simplified nobm1] for bin
   1.539 +lemma funpow_numeral [simp]:
   1.540 +  "f ^^ numeral k = f \<circ> f ^^ (numeral k - 1)"
   1.541 +  by (subst expand_Suc, rule funpow.simps)
   1.542  
   1.543 -lemmas replicate_minus_simp = 
   1.544 -  trans [OF gen_minus [where f = "%n. replicate n x"] replicate.replicate_Suc] for x
   1.545 -
   1.546 -lemmas replicate_pred_simp [simp] =
   1.547 -  replicate_minus_simp [of "number_of bin", simplified nobm1] for bin
   1.548 -
   1.549 -lemmas power_Suc_no [simp] = power_Suc [of "number_of a"] for a
   1.550 +lemma replicate_numeral [simp]: (* TODO: move to List.thy *)
   1.551 +  "replicate (numeral k) x = x # replicate (numeral k - 1) x"
   1.552 +  by (subst expand_Suc, rule replicate_Suc)
   1.553  
   1.554  lemmas power_minus_simp = 
   1.555    trans [OF gen_minus [where f = "power f"] power_Suc] for f
   1.556  
   1.557 -lemmas power_pred_simp = 
   1.558 -  power_minus_simp [of "number_of bin", simplified nobm1] for bin
   1.559 -lemmas power_pred_simp_no [simp] = power_pred_simp [where f= "number_of f"] for f
   1.560 -
   1.561  lemma list_exhaust_size_gt0:
   1.562    assumes y: "\<And>a list. y = a # list \<Longrightarrow> P"
   1.563    shows "0 < length y \<Longrightarrow> P"
   1.564 @@ -839,11 +785,6 @@
   1.565    "y = xa # list ==> size y = Suc k ==> size list = k"
   1.566    by auto
   1.567  
   1.568 -lemma size_Cons_lem_eq_bin:
   1.569 -  "y = xa # list ==> size y = number_of (Int.succ k) ==> 
   1.570 -    size list = number_of k"
   1.571 -  by (auto simp: pred_def succ_def split add : split_if_asm)
   1.572 -
   1.573  lemmas ls_splits = prod.split prod.split_asm split_if_asm
   1.574  
   1.575  lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)"