src/HOL/Integ/NatBin.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16413 47ffc49c7d7b
child 16642 849ec3962b55
permissions -rw-r--r--
Constant "If" is now local
     1 (*  Title:      HOL/NatBin.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1999  University of Cambridge
     5 *)
     6 
     7 header {* Binary arithmetic for the natural numbers *}
     8 
     9 theory NatBin
    10 imports IntDiv
    11 begin
    12 
    13 text {*
    14   Arithmetic for naturals is reduced to that for the non-negative integers.
    15 *}
    16 
    17 instance nat :: number ..
    18 
    19 defs (overloaded)
    20   nat_number_of_def:
    21      "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
    22 
    23 
    24 subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
    25 
    26 declare nat_0 [simp] nat_1 [simp]
    27 
    28 lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
    29 by (simp add: nat_number_of_def)
    30 
    31 lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
    32 by (simp add: nat_number_of_def)
    33 
    34 lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
    35 by (simp add: nat_1 nat_number_of_def)
    36 
    37 lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
    38 by (simp add: nat_numeral_1_eq_1)
    39 
    40 lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
    41 apply (unfold nat_number_of_def)
    42 apply (rule nat_2)
    43 done
    44 
    45 
    46 text{*Distributive laws for type @{text nat}.  The others are in theory
    47    @{text IntArith}, but these require div and mod to be defined for type
    48    "int".  They also need some of the lemmas proved above.*}
    49 
    50 lemma nat_div_distrib: "(0::int) <= z ==> nat (z div z') = nat z div nat z'"
    51 apply (case_tac "0 <= z'")
    52 apply (auto simp add: div_nonneg_neg_le0 DIVISION_BY_ZERO_DIV)
    53 apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
    54 apply (auto elim!: nonneg_eq_int)
    55 apply (rename_tac m m')
    56 apply (subgoal_tac "0 <= int m div int m'")
    57  prefer 2 apply (simp add: nat_numeral_0_eq_0 pos_imp_zdiv_nonneg_iff) 
    58 apply (rule inj_int [THEN injD], simp)
    59 apply (rule_tac r = "int (m mod m') " in quorem_div)
    60  prefer 2 apply force
    61 apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0 zadd_int 
    62                  zmult_int)
    63 done
    64 
    65 (*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
    66 lemma nat_mod_distrib:
    67      "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
    68 apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
    69 apply (auto elim!: nonneg_eq_int)
    70 apply (rename_tac m m')
    71 apply (subgoal_tac "0 <= int m mod int m'")
    72  prefer 2 apply (simp add: nat_less_iff nat_numeral_0_eq_0 pos_mod_sign) 
    73 apply (rule inj_int [THEN injD], simp)
    74 apply (rule_tac q = "int (m div m') " in quorem_mod)
    75  prefer 2 apply force
    76 apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0 zadd_int zmult_int)
    77 done
    78 
    79 text{*Suggested by Matthias Daum*}
    80 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
    81 apply (subgoal_tac "nat x div nat k < nat x") 
    82  apply (simp add: nat_div_distrib [symmetric])
    83 apply (rule Divides.div_less_dividend, simp_all) 
    84 done
    85 
    86 
    87 subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
    88 
    89 (*"neg" is used in rewrite rules for binary comparisons*)
    90 lemma int_nat_number_of [simp]:
    91      "int (number_of v :: nat) =  
    92          (if neg (number_of v :: int) then 0  
    93           else (number_of v :: int))"
    94 by (simp del: nat_number_of
    95 	 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
    96 
    97 
    98 subsubsection{*Successor *}
    99 
   100 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
   101 apply (rule sym)
   102 apply (simp add: nat_eq_iff int_Suc)
   103 done
   104 
   105 lemma Suc_nat_number_of_add:
   106      "Suc (number_of v + n) =  
   107         (if neg (number_of v :: int) then 1+n else number_of (bin_succ v) + n)" 
   108 by (simp del: nat_number_of 
   109          add: nat_number_of_def neg_nat
   110               Suc_nat_eq_nat_zadd1 number_of_succ) 
   111 
   112 lemma Suc_nat_number_of [simp]:
   113      "Suc (number_of v) =  
   114         (if neg (number_of v :: int) then 1 else number_of (bin_succ v))"
   115 apply (cut_tac n = 0 in Suc_nat_number_of_add)
   116 apply (simp cong del: if_weak_cong)
   117 done
   118 
   119 
   120 subsubsection{*Addition *}
   121 
   122 (*"neg" is used in rewrite rules for binary comparisons*)
   123 lemma add_nat_number_of [simp]:
   124      "(number_of v :: nat) + number_of v' =  
   125          (if neg (number_of v :: int) then number_of v'  
   126           else if neg (number_of v' :: int) then number_of v  
   127           else number_of (bin_add v v'))"
   128 by (force dest!: neg_nat
   129           simp del: nat_number_of
   130           simp add: nat_number_of_def nat_add_distrib [symmetric]) 
   131 
   132 
   133 subsubsection{*Subtraction *}
   134 
   135 lemma diff_nat_eq_if:
   136      "nat z - nat z' =  
   137         (if neg z' then nat z   
   138          else let d = z-z' in     
   139               if neg d then 0 else nat d)"
   140 apply (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
   141 apply (simp add: diff_is_0_eq nat_le_eq_zle)
   142 done
   143 
   144 lemma diff_nat_number_of [simp]: 
   145      "(number_of v :: nat) - number_of v' =  
   146         (if neg (number_of v' :: int) then number_of v  
   147          else let d = number_of (bin_add v (bin_minus v')) in     
   148               if neg d then 0 else nat d)"
   149 by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def) 
   150 
   151 
   152 
   153 subsubsection{*Multiplication *}
   154 
   155 lemma mult_nat_number_of [simp]:
   156      "(number_of v :: nat) * number_of v' =  
   157        (if neg (number_of v :: int) then 0 else number_of (bin_mult v v'))"
   158 by (force dest!: neg_nat
   159           simp del: nat_number_of
   160           simp add: nat_number_of_def nat_mult_distrib [symmetric]) 
   161 
   162 
   163 
   164 subsubsection{*Quotient *}
   165 
   166 lemma div_nat_number_of [simp]:
   167      "(number_of v :: nat)  div  number_of v' =  
   168           (if neg (number_of v :: int) then 0  
   169            else nat (number_of v div number_of v'))"
   170 by (force dest!: neg_nat
   171           simp del: nat_number_of
   172           simp add: nat_number_of_def nat_div_distrib [symmetric]) 
   173 
   174 lemma one_div_nat_number_of [simp]:
   175      "(Suc 0)  div  number_of v' = (nat (1 div number_of v'))" 
   176 by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
   177 
   178 
   179 subsubsection{*Remainder *}
   180 
   181 lemma mod_nat_number_of [simp]:
   182      "(number_of v :: nat)  mod  number_of v' =  
   183         (if neg (number_of v :: int) then 0  
   184          else if neg (number_of v' :: int) then number_of v  
   185          else nat (number_of v mod number_of v'))"
   186 by (force dest!: neg_nat
   187           simp del: nat_number_of
   188           simp add: nat_number_of_def nat_mod_distrib [symmetric]) 
   189 
   190 lemma one_mod_nat_number_of [simp]:
   191      "(Suc 0)  mod  number_of v' =  
   192         (if neg (number_of v' :: int) then Suc 0
   193          else nat (1 mod number_of v'))"
   194 by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
   195 
   196 
   197 
   198 ML
   199 {*
   200 val nat_number_of_def = thm"nat_number_of_def";
   201 
   202 val nat_number_of = thm"nat_number_of";
   203 val nat_numeral_0_eq_0 = thm"nat_numeral_0_eq_0";
   204 val nat_numeral_1_eq_1 = thm"nat_numeral_1_eq_1";
   205 val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0";
   206 val numeral_2_eq_2 = thm"numeral_2_eq_2";
   207 val nat_div_distrib = thm"nat_div_distrib";
   208 val nat_mod_distrib = thm"nat_mod_distrib";
   209 val int_nat_number_of = thm"int_nat_number_of";
   210 val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1";
   211 val Suc_nat_number_of_add = thm"Suc_nat_number_of_add";
   212 val Suc_nat_number_of = thm"Suc_nat_number_of";
   213 val add_nat_number_of = thm"add_nat_number_of";
   214 val diff_nat_eq_if = thm"diff_nat_eq_if";
   215 val diff_nat_number_of = thm"diff_nat_number_of";
   216 val mult_nat_number_of = thm"mult_nat_number_of";
   217 val div_nat_number_of = thm"div_nat_number_of";
   218 val mod_nat_number_of = thm"mod_nat_number_of";
   219 *}
   220 
   221 
   222 subsection{*Comparisons*}
   223 
   224 subsubsection{*Equals (=) *}
   225 
   226 lemma eq_nat_nat_iff:
   227      "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')"
   228 by (auto elim!: nonneg_eq_int)
   229 
   230 (*"neg" is used in rewrite rules for binary comparisons*)
   231 lemma eq_nat_number_of [simp]:
   232      "((number_of v :: nat) = number_of v') =  
   233       (if neg (number_of v :: int) then (iszero (number_of v' :: int) | neg (number_of v' :: int))  
   234        else if neg (number_of v' :: int) then iszero (number_of v :: int)  
   235        else iszero (number_of (bin_add v (bin_minus v')) :: int))"
   236 apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
   237                   eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def
   238             split add: split_if cong add: imp_cong)
   239 apply (simp only: nat_eq_iff nat_eq_iff2)
   240 apply (simp add: not_neg_eq_ge_0 [symmetric])
   241 done
   242 
   243 
   244 subsubsection{*Less-than (<) *}
   245 
   246 (*"neg" is used in rewrite rules for binary comparisons*)
   247 lemma less_nat_number_of [simp]:
   248      "((number_of v :: nat) < number_of v') =  
   249          (if neg (number_of v :: int) then neg (number_of (bin_minus v') :: int)  
   250           else neg (number_of (bin_add v (bin_minus v')) :: int))"
   251 by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
   252                 nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
   253          cong add: imp_cong, simp) 
   254 
   255 
   256 
   257 
   258 (*Maps #n to n for n = 0, 1, 2*)
   259 lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
   260 
   261 
   262 subsection{*Powers with Numeric Exponents*}
   263 
   264 text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
   265 We cannot prove general results about the numeral @{term "-1"}, so we have to
   266 use @{term "- 1"} instead.*}
   267 
   268 lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = a * a"
   269   by (simp add: numeral_2_eq_2 Power.power_Suc)
   270 
   271 lemma [simp]: "(0::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 0"
   272   by (simp add: power2_eq_square)
   273 
   274 lemma [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 1"
   275   by (simp add: power2_eq_square)
   276 
   277 text{*Squares of literal numerals will be evaluated.*}
   278 declare power2_eq_square [of "number_of w", standard, simp]
   279 
   280 lemma zero_le_power2 [simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
   281   by (simp add: power2_eq_square zero_le_square)
   282 
   283 lemma zero_less_power2 [simp]:
   284      "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
   285   by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   286 
   287 lemma power2_less_0 [simp]:
   288   fixes a :: "'a::{ordered_idom,recpower}"
   289   shows "~ (a\<twosuperior> < 0)"
   290 by (force simp add: power2_eq_square mult_less_0_iff) 
   291 
   292 lemma zero_eq_power2 [simp]:
   293      "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
   294   by (force simp add: power2_eq_square mult_eq_0_iff)
   295 
   296 lemma abs_power2 [simp]:
   297      "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})"
   298   by (simp add: power2_eq_square abs_mult abs_mult_self)
   299 
   300 lemma power2_abs [simp]:
   301      "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})"
   302   by (simp add: power2_eq_square abs_mult_self)
   303 
   304 lemma power2_minus [simp]:
   305      "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})"
   306   by (simp add: power2_eq_square)
   307 
   308 lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
   309 apply (induct "n")
   310 apply (auto simp add: power_Suc power_add)
   311 done
   312 
   313 lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
   314 by (simp add: power_mult power_mult_distrib power2_eq_square)
   315 
   316 lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
   317 by (simp add: power_even_eq) 
   318 
   319 lemma power_minus_even [simp]:
   320      "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
   321 by (simp add: power_minus1_even power_minus [of a]) 
   322 
   323 lemma zero_le_even_power:
   324      "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
   325 proof (induct "n")
   326   case 0
   327     show ?case by (simp add: zero_le_one)
   328 next
   329   case (Suc n)
   330     have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
   331       by (simp add: mult_ac power_add power2_eq_square)
   332     thus ?case
   333       by (simp add: prems zero_le_square zero_le_mult_iff)
   334 qed
   335 
   336 lemma odd_power_less_zero:
   337      "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
   338 proof (induct "n")
   339   case 0
   340     show ?case by (simp add: Power.power_Suc)
   341 next
   342   case (Suc n)
   343     have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" 
   344       by (simp add: mult_ac power_add power2_eq_square Power.power_Suc)
   345     thus ?case
   346       by (simp add: prems mult_less_0_iff mult_neg)
   347 qed
   348 
   349 lemma odd_0_le_power_imp_0_le:
   350      "0 \<le> a  ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,recpower})"
   351 apply (insert odd_power_less_zero [of a n]) 
   352 apply (force simp add: linorder_not_less [symmetric]) 
   353 done
   354 
   355 text{*Simprules for comparisons where common factors can be cancelled.*}
   356 lemmas zero_compare_simps =
   357     add_strict_increasing add_strict_increasing2 add_increasing
   358     zero_le_mult_iff zero_le_divide_iff 
   359     zero_less_mult_iff zero_less_divide_iff 
   360     mult_le_0_iff divide_le_0_iff 
   361     mult_less_0_iff divide_less_0_iff 
   362     zero_le_power2 power2_less_0
   363 
   364 subsubsection{*Nat *}
   365 
   366 lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
   367 by (simp add: numerals)
   368 
   369 (*Expresses a natural number constant as the Suc of another one.
   370   NOT suitable for rewriting because n recurs in the condition.*)
   371 lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
   372 
   373 subsubsection{*Arith *}
   374 
   375 lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
   376 by (simp add: numerals)
   377 
   378 lemma Suc_eq_add_numeral_1_left: "Suc n = 1 + n"
   379 by (simp add: numerals)
   380 
   381 (* These two can be useful when m = number_of... *)
   382 
   383 lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
   384 apply (case_tac "m")
   385 apply (simp_all add: numerals)
   386 done
   387 
   388 lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
   389 apply (case_tac "m")
   390 apply (simp_all add: numerals)
   391 done
   392 
   393 lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
   394 apply (case_tac "m")
   395 apply (simp_all add: numerals)
   396 done
   397 
   398 
   399 subsection{*Comparisons involving (0::nat) *}
   400 
   401 text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
   402 
   403 lemma eq_number_of_0 [simp]:
   404      "(number_of v = (0::nat)) =  
   405       (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
   406 by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
   407 
   408 lemma eq_0_number_of [simp]:
   409      "((0::nat) = number_of v) =  
   410       (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
   411 by (rule trans [OF eq_sym_conv eq_number_of_0])
   412 
   413 lemma less_0_number_of [simp]:
   414      "((0::nat) < number_of v) = neg (number_of (bin_minus v) :: int)"
   415 by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
   416 
   417 
   418 lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
   419 by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
   420 
   421 
   422 
   423 subsection{*Comparisons involving Suc *}
   424 
   425 lemma eq_number_of_Suc [simp]:
   426      "(number_of v = Suc n) =  
   427         (let pv = number_of (bin_pred v) in  
   428          if neg pv then False else nat pv = n)"
   429 apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   430                   number_of_pred nat_number_of_def 
   431             split add: split_if)
   432 apply (rule_tac x = "number_of v" in spec)
   433 apply (auto simp add: nat_eq_iff)
   434 done
   435 
   436 lemma Suc_eq_number_of [simp]:
   437      "(Suc n = number_of v) =  
   438         (let pv = number_of (bin_pred v) in  
   439          if neg pv then False else nat pv = n)"
   440 by (rule trans [OF eq_sym_conv eq_number_of_Suc])
   441 
   442 lemma less_number_of_Suc [simp]:
   443      "(number_of v < Suc n) =  
   444         (let pv = number_of (bin_pred v) in  
   445          if neg pv then True else nat pv < n)"
   446 apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   447                   number_of_pred nat_number_of_def  
   448             split add: split_if)
   449 apply (rule_tac x = "number_of v" in spec)
   450 apply (auto simp add: nat_less_iff)
   451 done
   452 
   453 lemma less_Suc_number_of [simp]:
   454      "(Suc n < number_of v) =  
   455         (let pv = number_of (bin_pred v) in  
   456          if neg pv then False else n < nat pv)"
   457 apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   458                   number_of_pred nat_number_of_def
   459             split add: split_if)
   460 apply (rule_tac x = "number_of v" in spec)
   461 apply (auto simp add: zless_nat_eq_int_zless)
   462 done
   463 
   464 lemma le_number_of_Suc [simp]:
   465      "(number_of v <= Suc n) =  
   466         (let pv = number_of (bin_pred v) in  
   467          if neg pv then True else nat pv <= n)"
   468 by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
   469 
   470 lemma le_Suc_number_of [simp]:
   471      "(Suc n <= number_of v) =  
   472         (let pv = number_of (bin_pred v) in  
   473          if neg pv then False else n <= nat pv)"
   474 by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
   475 
   476 
   477 (* Push int(.) inwards: *)
   478 declare zadd_int [symmetric, simp]
   479 
   480 lemma lemma1: "(m+m = n+n) = (m = (n::int))"
   481 by auto
   482 
   483 lemma lemma2: "m+m ~= (1::int) + (n + n)"
   484 apply auto
   485 apply (drule_tac f = "%x. x mod 2" in arg_cong)
   486 apply (simp add: zmod_zadd1_eq)
   487 done
   488 
   489 lemma eq_number_of_BIT_BIT:
   490      "((number_of (v BIT x) ::int) = number_of (w BIT y)) =  
   491       (x=y & (((number_of v) ::int) = number_of w))"
   492 apply (simp only: number_of_BIT lemma1 lemma2 eq_commute
   493                OrderedGroup.add_left_cancel add_assoc OrderedGroup.add_0
   494             split add: bit.split) 
   495 apply simp
   496 done
   497 
   498 lemma eq_number_of_BIT_Pls:
   499      "((number_of (v BIT x) ::int) = Numeral0) =  
   500       (x=bit.B0 & (((number_of v) ::int) = Numeral0))"
   501 apply (simp only: simp_thms  add: number_of_BIT number_of_Pls eq_commute
   502             split add: bit.split cong: imp_cong)
   503 apply (rule_tac x = "number_of v" in spec, safe)
   504 apply (simp_all (no_asm_use))
   505 apply (drule_tac f = "%x. x mod 2" in arg_cong)
   506 apply (simp add: zmod_zadd1_eq)
   507 done
   508 
   509 lemma eq_number_of_BIT_Min:
   510      "((number_of (v BIT x) ::int) = number_of Numeral.Min) =  
   511       (x=bit.B1 & (((number_of v) ::int) = number_of Numeral.Min))"
   512 apply (simp only: simp_thms  add: number_of_BIT number_of_Min eq_commute
   513             split add: bit.split cong: imp_cong)
   514 apply (rule_tac x = "number_of v" in spec, auto)
   515 apply (drule_tac f = "%x. x mod 2" in arg_cong, auto)
   516 done
   517 
   518 lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Numeral.Min"
   519 by auto
   520 
   521 
   522 
   523 subsection{*Literal arithmetic involving powers*}
   524 
   525 lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
   526 apply (induct "n")
   527 apply (simp_all (no_asm_simp) add: nat_mult_distrib)
   528 done
   529 
   530 lemma power_nat_number_of:
   531      "(number_of v :: nat) ^ n =  
   532        (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))"
   533 by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
   534          split add: split_if cong: imp_cong)
   535 
   536 
   537 declare power_nat_number_of [of _ "number_of w", standard, simp]
   538 
   539 
   540 text{*For the integers*}
   541 
   542 lemma zpower_number_of_even:
   543      "(z::int) ^ number_of (w BIT bit.B0) =  
   544       (let w = z ^ (number_of w) in  w*w)"
   545 apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
   546 apply (simp only: number_of_add) 
   547 apply (rule_tac x = "number_of w" in spec, clarify)
   548 apply (case_tac " (0::int) <= x")
   549 apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
   550 done
   551 
   552 lemma zpower_number_of_odd:
   553      "(z::int) ^ number_of (w BIT bit.B1) =  
   554           (if (0::int) <= number_of w                    
   555            then (let w = z ^ (number_of w) in  z*w*w)    
   556            else 1)"
   557 apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
   558 apply (simp only: number_of_add nat_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0) 
   559 apply (rule_tac x = "number_of w" in spec, clarify)
   560 apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat)
   561 done
   562 
   563 declare zpower_number_of_even [of "number_of v", standard, simp]
   564 declare zpower_number_of_odd  [of "number_of v", standard, simp]
   565 
   566 
   567 
   568 ML
   569 {*
   570 val numerals = thms"numerals";
   571 val numeral_ss = simpset() addsimps numerals;
   572 
   573 val nat_bin_arith_setup =
   574  [Fast_Arith.map_data 
   575    (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   576      {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
   577       inj_thms = inj_thms,
   578       lessD = lessD, neqE = neqE,
   579       simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
   580                                   not_neg_number_of_Pls,
   581                                   neg_number_of_Min,neg_number_of_BIT]})]
   582 *}
   583 
   584 setup nat_bin_arith_setup
   585 
   586 (* Enable arith to deal with div/mod k where k is a numeral: *)
   587 declare split_div[of _ _ "number_of k", standard, arith_split]
   588 declare split_mod[of _ _ "number_of k", standard, arith_split]
   589 
   590 lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
   591   by (simp add: number_of_Pls nat_number_of_def)
   592 
   593 lemma nat_number_of_Min: "number_of Numeral.Min = (0::nat)"
   594   apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   595   apply (simp add: neg_nat)
   596   done
   597 
   598 lemma nat_number_of_BIT_1:
   599   "number_of (w BIT bit.B1) =
   600     (if neg (number_of w :: int) then 0
   601      else let n = number_of w in Suc (n + n))"
   602   apply (simp only: nat_number_of_def Let_def split: split_if)
   603   apply (intro conjI impI)
   604    apply (simp add: neg_nat neg_number_of_BIT)
   605   apply (rule int_int_eq [THEN iffD1])
   606   apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
   607   apply (simp only: number_of_BIT zadd_assoc split: bit.split)
   608   apply simp
   609   done
   610 
   611 lemma nat_number_of_BIT_0:
   612     "number_of (w BIT bit.B0) = (let n::nat = number_of w in n + n)"
   613   apply (simp only: nat_number_of_def Let_def)
   614   apply (cases "neg (number_of w :: int)")
   615    apply (simp add: neg_nat neg_number_of_BIT)
   616   apply (rule int_int_eq [THEN iffD1])
   617   apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
   618   apply (simp only: number_of_BIT zadd_assoc)
   619   apply simp
   620   done
   621 
   622 lemmas nat_number =
   623   nat_number_of_Pls nat_number_of_Min
   624   nat_number_of_BIT_1 nat_number_of_BIT_0
   625 
   626 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   627   by (simp add: Let_def)
   628 
   629 lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,recpower})"
   630 by (simp add: power_mult); 
   631 
   632 lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,recpower})"
   633 by (simp add: power_mult power_Suc); 
   634 
   635 
   636 subsection{*Literal arithmetic and @{term of_nat}*}
   637 
   638 lemma of_nat_double:
   639      "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
   640 by (simp only: mult_2 nat_add_distrib of_nat_add) 
   641 
   642 lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
   643 by (simp only:  nat_number_of_def, simp)
   644 
   645 lemma of_nat_number_of_lemma:
   646      "of_nat (number_of v :: nat) =  
   647          (if 0 \<le> (number_of v :: int) 
   648           then (number_of v :: 'a :: number_ring)
   649           else 0)"
   650 by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat);
   651 
   652 lemma of_nat_number_of_eq [simp]:
   653      "of_nat (number_of v :: nat) =  
   654          (if neg (number_of v :: int) then 0  
   655           else (number_of v :: 'a :: number_ring))"
   656 by (simp only: of_nat_number_of_lemma neg_def, simp) 
   657 
   658 
   659 subsection {*Lemmas for the Combination and Cancellation Simprocs*}
   660 
   661 lemma nat_number_of_add_left:
   662      "number_of v + (number_of v' + (k::nat)) =  
   663          (if neg (number_of v :: int) then number_of v' + k  
   664           else if neg (number_of v' :: int) then number_of v + k  
   665           else number_of (bin_add v v') + k)"
   666 by simp
   667 
   668 lemma nat_number_of_mult_left:
   669      "number_of v * (number_of v' * (k::nat)) =  
   670          (if neg (number_of v :: int) then 0
   671           else number_of (bin_mult v v') * k)"
   672 by simp
   673 
   674 
   675 subsubsection{*For @{text combine_numerals}*}
   676 
   677 lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
   678 by (simp add: add_mult_distrib)
   679 
   680 
   681 subsubsection{*For @{text cancel_numerals}*}
   682 
   683 lemma nat_diff_add_eq1:
   684      "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
   685 by (simp split add: nat_diff_split add: add_mult_distrib)
   686 
   687 lemma nat_diff_add_eq2:
   688      "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
   689 by (simp split add: nat_diff_split add: add_mult_distrib)
   690 
   691 lemma nat_eq_add_iff1:
   692      "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
   693 by (auto split add: nat_diff_split simp add: add_mult_distrib)
   694 
   695 lemma nat_eq_add_iff2:
   696      "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
   697 by (auto split add: nat_diff_split simp add: add_mult_distrib)
   698 
   699 lemma nat_less_add_iff1:
   700      "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
   701 by (auto split add: nat_diff_split simp add: add_mult_distrib)
   702 
   703 lemma nat_less_add_iff2:
   704      "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
   705 by (auto split add: nat_diff_split simp add: add_mult_distrib)
   706 
   707 lemma nat_le_add_iff1:
   708      "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
   709 by (auto split add: nat_diff_split simp add: add_mult_distrib)
   710 
   711 lemma nat_le_add_iff2:
   712      "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
   713 by (auto split add: nat_diff_split simp add: add_mult_distrib)
   714 
   715 
   716 subsubsection{*For @{text cancel_numeral_factors} *}
   717 
   718 lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
   719 by auto
   720 
   721 lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
   722 by auto
   723 
   724 lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
   725 by auto
   726 
   727 lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
   728 by auto
   729 
   730 
   731 subsubsection{*For @{text cancel_factor} *}
   732 
   733 lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
   734 by auto
   735 
   736 lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
   737 by auto
   738 
   739 lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
   740 by auto
   741 
   742 lemma nat_mult_div_cancel_disj:
   743      "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
   744 by (simp add: nat_mult_div_cancel1)
   745 
   746 
   747 ML
   748 {*
   749 val eq_nat_nat_iff = thm"eq_nat_nat_iff";
   750 val eq_nat_number_of = thm"eq_nat_number_of";
   751 val less_nat_number_of = thm"less_nat_number_of";
   752 val power2_eq_square = thm "power2_eq_square";
   753 val zero_le_power2 = thm "zero_le_power2";
   754 val zero_less_power2 = thm "zero_less_power2";
   755 val zero_eq_power2 = thm "zero_eq_power2";
   756 val abs_power2 = thm "abs_power2";
   757 val power2_abs = thm "power2_abs";
   758 val power2_minus = thm "power2_minus";
   759 val power_minus1_even = thm "power_minus1_even";
   760 val power_minus_even = thm "power_minus_even";
   761 val zero_le_even_power = thm "zero_le_even_power";
   762 val odd_power_less_zero = thm "odd_power_less_zero";
   763 val odd_0_le_power_imp_0_le = thm "odd_0_le_power_imp_0_le";
   764 
   765 val Suc_pred' = thm"Suc_pred'";
   766 val expand_Suc = thm"expand_Suc";
   767 val Suc_eq_add_numeral_1 = thm"Suc_eq_add_numeral_1";
   768 val Suc_eq_add_numeral_1_left = thm"Suc_eq_add_numeral_1_left";
   769 val add_eq_if = thm"add_eq_if";
   770 val mult_eq_if = thm"mult_eq_if";
   771 val power_eq_if = thm"power_eq_if";
   772 val eq_number_of_0 = thm"eq_number_of_0";
   773 val eq_0_number_of = thm"eq_0_number_of";
   774 val less_0_number_of = thm"less_0_number_of";
   775 val neg_imp_number_of_eq_0 = thm"neg_imp_number_of_eq_0";
   776 val eq_number_of_Suc = thm"eq_number_of_Suc";
   777 val Suc_eq_number_of = thm"Suc_eq_number_of";
   778 val less_number_of_Suc = thm"less_number_of_Suc";
   779 val less_Suc_number_of = thm"less_Suc_number_of";
   780 val le_number_of_Suc = thm"le_number_of_Suc";
   781 val le_Suc_number_of = thm"le_Suc_number_of";
   782 val eq_number_of_BIT_BIT = thm"eq_number_of_BIT_BIT";
   783 val eq_number_of_BIT_Pls = thm"eq_number_of_BIT_Pls";
   784 val eq_number_of_BIT_Min = thm"eq_number_of_BIT_Min";
   785 val eq_number_of_Pls_Min = thm"eq_number_of_Pls_Min";
   786 val of_nat_number_of_eq = thm"of_nat_number_of_eq";
   787 val nat_power_eq = thm"nat_power_eq";
   788 val power_nat_number_of = thm"power_nat_number_of";
   789 val zpower_number_of_even = thm"zpower_number_of_even";
   790 val zpower_number_of_odd = thm"zpower_number_of_odd";
   791 val nat_number_of_Pls = thm"nat_number_of_Pls";
   792 val nat_number_of_Min = thm"nat_number_of_Min";
   793 val Let_Suc = thm"Let_Suc";
   794 
   795 val nat_number = thms"nat_number";
   796 
   797 val nat_number_of_add_left = thm"nat_number_of_add_left";
   798 val nat_number_of_mult_left = thm"nat_number_of_mult_left";
   799 val left_add_mult_distrib = thm"left_add_mult_distrib";
   800 val nat_diff_add_eq1 = thm"nat_diff_add_eq1";
   801 val nat_diff_add_eq2 = thm"nat_diff_add_eq2";
   802 val nat_eq_add_iff1 = thm"nat_eq_add_iff1";
   803 val nat_eq_add_iff2 = thm"nat_eq_add_iff2";
   804 val nat_less_add_iff1 = thm"nat_less_add_iff1";
   805 val nat_less_add_iff2 = thm"nat_less_add_iff2";
   806 val nat_le_add_iff1 = thm"nat_le_add_iff1";
   807 val nat_le_add_iff2 = thm"nat_le_add_iff2";
   808 val nat_mult_le_cancel1 = thm"nat_mult_le_cancel1";
   809 val nat_mult_less_cancel1 = thm"nat_mult_less_cancel1";
   810 val nat_mult_eq_cancel1 = thm"nat_mult_eq_cancel1";
   811 val nat_mult_div_cancel1 = thm"nat_mult_div_cancel1";
   812 val nat_mult_le_cancel_disj = thm"nat_mult_le_cancel_disj";
   813 val nat_mult_less_cancel_disj = thm"nat_mult_less_cancel_disj";
   814 val nat_mult_eq_cancel_disj = thm"nat_mult_eq_cancel_disj";
   815 val nat_mult_div_cancel_disj = thm"nat_mult_div_cancel_disj";
   816 
   817 val power_minus_even = thm"power_minus_even";
   818 val zero_le_even_power = thm"zero_le_even_power";
   819 *}
   820 
   821 
   822 subsection {* Configuration of the code generator *}
   823 
   824 ML {*
   825 infix 7 `*;
   826 infix 6 `+;
   827 
   828 val op `* = op * : int * int -> int;
   829 val op `+ = op + : int * int -> int;
   830 val `~ = ~ : int -> int;
   831 *}
   832 
   833 types_code
   834   "int" ("int")
   835 
   836 constdefs
   837   int_aux :: "int \<Rightarrow> nat \<Rightarrow> int"
   838   "int_aux i n == (i + int n)"
   839   nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat"
   840   "nat_aux n i == (n + nat i)"
   841 
   842 lemma [code]:
   843   "int_aux i 0 = i"
   844   "int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *}
   845   "int n = int_aux 0 n"
   846   by (simp add: int_aux_def)+
   847 
   848 lemma [code]: "nat_aux n i = (if i <= 0 then n else nat_aux (Suc n) (i - 1))"
   849   by (simp add: nat_aux_def Suc_nat_eq_nat_zadd1) -- {* tail recursive *}
   850 lemma [code]: "nat i = nat_aux 0 i"
   851   by (simp add: nat_aux_def)
   852 
   853 consts_code
   854   "0" :: "int"                  ("0")
   855   "1" :: "int"                  ("1")
   856   "uminus" :: "int => int"      ("`~")
   857   "op +" :: "int => int => int" ("(_ `+/ _)")
   858   "op *" :: "int => int => int" ("(_ `*/ _)")
   859 (* Fails for 0:
   860   "op div" :: "int => int => int" ("(_ div/ _)")
   861   "op mod" :: "int => int => int" ("(_ mod/ _)")
   862 *)
   863   "op <" :: "int => int => bool" ("(_ </ _)")
   864   "op <=" :: "int => int => bool" ("(_ <=/ _)")
   865   "neg"                         ("(_ < 0)")
   866 
   867 ML {*
   868 fun number_of_codegen thy gr s b (Const ("Numeral.number_of",
   869       Type ("fun", [_, Type ("IntDef.int", [])])) $ bin) =
   870         (SOME (gr, Pretty.str (IntInf.toString (HOLogic.dest_binum bin)))
   871         handle TERM _ => NONE)
   872   | number_of_codegen thy gr s b (Const ("Numeral.number_of",
   873       Type ("fun", [_, Type ("nat", [])])) $ bin) =
   874         SOME (Codegen.invoke_codegen thy s b (gr,
   875           Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
   876             (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin)))
   877   | number_of_codegen _ _ _ _ _ = NONE;
   878 *}
   879 
   880 setup {* [Codegen.add_codegen "number_of_codegen" number_of_codegen] *}
   881 
   882 end