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