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