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