src/HOL/Nat_Numeral.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 40690 3f472e57446a
child 43526 2b92a6943915
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     1 (*  Title:      HOL/Nat_Numeral.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1999  University of Cambridge
     4 *)
     5 
     6 header {* Binary numerals for the natural numbers *}
     7 
     8 theory Nat_Numeral
     9 imports Int
    10 begin
    11 
    12 subsection {* Numerals for natural numbers *}
    13 
    14 text {*
    15   Arithmetic for naturals is reduced to that for the non-negative integers.
    16 *}
    17 
    18 instantiation nat :: number
    19 begin
    20 
    21 definition
    22   nat_number_of_def [code_unfold, code del]: "number_of v = nat (number_of v)"
    23 
    24 instance ..
    25 
    26 end
    27 
    28 lemma [code_post]:
    29   "nat (number_of v) = number_of v"
    30   unfolding nat_number_of_def ..
    31 
    32 
    33 subsection {* Special case: squares and cubes *}
    34 
    35 lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
    36   by (simp add: nat_number_of_def)
    37 
    38 lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
    39   by (simp add: nat_number_of_def)
    40 
    41 context power
    42 begin
    43 
    44 abbreviation (xsymbols)
    45   power2 :: "'a \<Rightarrow> 'a"  ("(_\<twosuperior>)" [1000] 999) where
    46   "x\<twosuperior> \<equiv> x ^ 2"
    47 
    48 notation (latex output)
    49   power2  ("(_\<twosuperior>)" [1000] 999)
    50 
    51 notation (HTML output)
    52   power2  ("(_\<twosuperior>)" [1000] 999)
    53 
    54 end
    55 
    56 context monoid_mult
    57 begin
    58 
    59 lemma power2_eq_square: "a\<twosuperior> = a * a"
    60   by (simp add: numeral_2_eq_2)
    61 
    62 lemma power3_eq_cube: "a ^ 3 = a * a * a"
    63   by (simp add: numeral_3_eq_3 mult_assoc)
    64 
    65 lemma power_even_eq:
    66   "a ^ (2*n) = (a ^ n) ^ 2"
    67   by (subst mult_commute) (simp add: power_mult)
    68 
    69 lemma power_odd_eq:
    70   "a ^ Suc (2*n) = a * (a ^ n) ^ 2"
    71   by (simp add: power_even_eq)
    72 
    73 end
    74 
    75 context semiring_1
    76 begin
    77 
    78 lemma zero_power2 [simp]: "0\<twosuperior> = 0"
    79   by (simp add: power2_eq_square)
    80 
    81 lemma one_power2 [simp]: "1\<twosuperior> = 1"
    82   by (simp add: power2_eq_square)
    83 
    84 end
    85 
    86 context ring_1
    87 begin
    88 
    89 lemma power2_minus [simp]:
    90   "(- a)\<twosuperior> = a\<twosuperior>"
    91   by (simp add: power2_eq_square)
    92 
    93 text{*
    94   We cannot prove general results about the numeral @{term "-1"},
    95   so we have to use @{term "- 1"} instead.
    96 *}
    97 
    98 lemma power_minus1_even [simp]:
    99   "(- 1) ^ (2*n) = 1"
   100 proof (induct n)
   101   case 0 show ?case by simp
   102 next
   103   case (Suc n) then show ?case by (simp add: power_add)
   104 qed
   105 
   106 lemma power_minus1_odd:
   107   "(- 1) ^ Suc (2*n) = - 1"
   108   by simp
   109 
   110 lemma power_minus_even [simp]:
   111   "(-a) ^ (2*n) = a ^ (2*n)"
   112   by (simp add: power_minus [of a]) 
   113 
   114 end
   115 
   116 context ring_1_no_zero_divisors
   117 begin
   118 
   119 lemma zero_eq_power2 [simp]:
   120   "a\<twosuperior> = 0 \<longleftrightarrow> a = 0"
   121   unfolding power2_eq_square by simp
   122 
   123 lemma power2_eq_1_iff:
   124   "a\<twosuperior> = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
   125   unfolding power2_eq_square by (rule square_eq_1_iff)
   126 
   127 end
   128 
   129 context linordered_ring
   130 begin
   131 
   132 lemma sum_squares_ge_zero:
   133   "0 \<le> x * x + y * y"
   134   by (intro add_nonneg_nonneg zero_le_square)
   135 
   136 lemma not_sum_squares_lt_zero:
   137   "\<not> x * x + y * y < 0"
   138   by (simp add: not_less sum_squares_ge_zero)
   139 
   140 end
   141 
   142 context linordered_ring_strict
   143 begin
   144 
   145 lemma sum_squares_eq_zero_iff:
   146   "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   147   by (simp add: add_nonneg_eq_0_iff)
   148 
   149 lemma sum_squares_le_zero_iff:
   150   "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   151   by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff)
   152 
   153 lemma sum_squares_gt_zero_iff:
   154   "0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   155   by (simp add: not_le [symmetric] sum_squares_le_zero_iff)
   156 
   157 end
   158 
   159 context linordered_semidom
   160 begin
   161 
   162 lemma power2_le_imp_le:
   163   "x\<twosuperior> \<le> y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
   164   unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
   165 
   166 lemma power2_less_imp_less:
   167   "x\<twosuperior> < y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y"
   168   by (rule power_less_imp_less_base)
   169 
   170 lemma power2_eq_imp_eq:
   171   "x\<twosuperior> = y\<twosuperior> \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
   172   unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp
   173 
   174 end
   175 
   176 context linordered_idom
   177 begin
   178 
   179 lemma zero_le_power2 [simp]:
   180   "0 \<le> a\<twosuperior>"
   181   by (simp add: power2_eq_square)
   182 
   183 lemma zero_less_power2 [simp]:
   184   "0 < a\<twosuperior> \<longleftrightarrow> a \<noteq> 0"
   185   by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   186 
   187 lemma power2_less_0 [simp]:
   188   "\<not> a\<twosuperior> < 0"
   189   by (force simp add: power2_eq_square mult_less_0_iff) 
   190 
   191 lemma abs_power2 [simp]:
   192   "abs (a\<twosuperior>) = a\<twosuperior>"
   193   by (simp add: power2_eq_square abs_mult abs_mult_self)
   194 
   195 lemma power2_abs [simp]:
   196   "(abs a)\<twosuperior> = a\<twosuperior>"
   197   by (simp add: power2_eq_square abs_mult_self)
   198 
   199 lemma odd_power_less_zero:
   200   "a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0"
   201 proof (induct n)
   202   case 0
   203   then show ?case by simp
   204 next
   205   case (Suc n)
   206   have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
   207     by (simp add: mult_ac power_add power2_eq_square)
   208   thus ?case
   209     by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
   210 qed
   211 
   212 lemma odd_0_le_power_imp_0_le:
   213   "0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a"
   214   using odd_power_less_zero [of a n]
   215     by (force simp add: linorder_not_less [symmetric]) 
   216 
   217 lemma zero_le_even_power'[simp]:
   218   "0 \<le> a ^ (2*n)"
   219 proof (induct n)
   220   case 0
   221     show ?case by simp
   222 next
   223   case (Suc n)
   224     have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
   225       by (simp add: mult_ac power_add power2_eq_square)
   226     thus ?case
   227       by (simp add: Suc zero_le_mult_iff)
   228 qed
   229 
   230 lemma sum_power2_ge_zero:
   231   "0 \<le> x\<twosuperior> + y\<twosuperior>"
   232   unfolding power2_eq_square by (rule sum_squares_ge_zero)
   233 
   234 lemma not_sum_power2_lt_zero:
   235   "\<not> x\<twosuperior> + y\<twosuperior> < 0"
   236   unfolding power2_eq_square by (rule not_sum_squares_lt_zero)
   237 
   238 lemma sum_power2_eq_zero_iff:
   239   "x\<twosuperior> + y\<twosuperior> = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   240   unfolding power2_eq_square by (rule sum_squares_eq_zero_iff)
   241 
   242 lemma sum_power2_le_zero_iff:
   243   "x\<twosuperior> + y\<twosuperior> \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   244   unfolding power2_eq_square by (rule sum_squares_le_zero_iff)
   245 
   246 lemma sum_power2_gt_zero_iff:
   247   "0 < x\<twosuperior> + y\<twosuperior> \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
   248   unfolding power2_eq_square by (rule sum_squares_gt_zero_iff)
   249 
   250 end
   251 
   252 lemma power2_sum:
   253   fixes x y :: "'a::number_ring"
   254   shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
   255   by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
   256 
   257 lemma power2_diff:
   258   fixes x y :: "'a::number_ring"
   259   shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
   260   by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
   261 
   262 
   263 subsection {* Predicate for negative binary numbers *}
   264 
   265 definition neg  :: "int \<Rightarrow> bool" where
   266   "neg Z \<longleftrightarrow> Z < 0"
   267 
   268 lemma not_neg_int [simp]: "~ neg (of_nat n)"
   269 by (simp add: neg_def)
   270 
   271 lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
   272 by (simp add: neg_def del: of_nat_Suc)
   273 
   274 lemmas neg_eq_less_0 = neg_def
   275 
   276 lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
   277 by (simp add: neg_def linorder_not_less)
   278 
   279 text{*To simplify inequalities when Numeral1 can get simplified to 1*}
   280 
   281 lemma not_neg_0: "~ neg 0"
   282 by (simp add: One_int_def neg_def)
   283 
   284 lemma not_neg_1: "~ neg 1"
   285 by (simp add: neg_def linorder_not_less)
   286 
   287 lemma neg_nat: "neg z ==> nat z = 0"
   288 by (simp add: neg_def order_less_imp_le) 
   289 
   290 lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
   291 by (simp add: linorder_not_less neg_def)
   292 
   293 text {*
   294   If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
   295   @{term Numeral0} IS @{term "number_of Pls"}
   296 *}
   297 
   298 lemma not_neg_number_of_Pls: "~ neg (number_of Int.Pls)"
   299   by (simp add: neg_def)
   300 
   301 lemma neg_number_of_Min: "neg (number_of Int.Min)"
   302   by (simp add: neg_def)
   303 
   304 lemma neg_number_of_Bit0:
   305   "neg (number_of (Int.Bit0 w)) = neg (number_of w)"
   306   by (simp add: neg_def)
   307 
   308 lemma neg_number_of_Bit1:
   309   "neg (number_of (Int.Bit1 w)) = neg (number_of w)"
   310   by (simp add: neg_def)
   311 
   312 lemmas neg_simps [simp] =
   313   not_neg_0 not_neg_1
   314   not_neg_number_of_Pls neg_number_of_Min
   315   neg_number_of_Bit0 neg_number_of_Bit1
   316 
   317 
   318 subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
   319 
   320 declare nat_1 [simp]
   321 
   322 lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
   323 by (simp add: nat_number_of_def)
   324 
   325 lemma nat_numeral_0_eq_0 [simp, code_post]: "Numeral0 = (0::nat)"
   326 by (simp add: nat_number_of_def)
   327 
   328 lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
   329 by (simp add: nat_number_of_def)
   330 
   331 lemma Numeral1_eq1_nat:
   332   "(1::nat) = Numeral1"
   333   by simp
   334 
   335 lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0"
   336 by (simp only: nat_numeral_1_eq_1 One_nat_def)
   337 
   338 
   339 subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
   340 
   341 lemma int_nat_number_of [simp]:
   342      "int (number_of v) =  
   343          (if neg (number_of v :: int) then 0  
   344           else (number_of v :: int))"
   345   unfolding nat_number_of_def number_of_is_id neg_def
   346   by simp
   347 
   348 
   349 subsubsection{*Successor *}
   350 
   351 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
   352 apply (rule sym)
   353 apply (simp add: nat_eq_iff int_Suc)
   354 done
   355 
   356 lemma Suc_nat_number_of_add:
   357      "Suc (number_of v + n) =  
   358         (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)"
   359   unfolding nat_number_of_def number_of_is_id neg_def numeral_simps
   360   by (simp add: Suc_nat_eq_nat_zadd1 add_ac)
   361 
   362 lemma Suc_nat_number_of [simp]:
   363      "Suc (number_of v) =  
   364         (if neg (number_of v :: int) then 1 else number_of (Int.succ v))"
   365 apply (cut_tac n = 0 in Suc_nat_number_of_add)
   366 apply (simp cong del: if_weak_cong)
   367 done
   368 
   369 
   370 subsubsection{*Addition *}
   371 
   372 lemma add_nat_number_of [simp]:
   373      "(number_of v :: nat) + number_of v' =  
   374          (if v < Int.Pls then number_of v'  
   375           else if v' < Int.Pls then number_of v  
   376           else number_of (v + v'))"
   377   unfolding nat_number_of_def number_of_is_id numeral_simps
   378   by (simp add: nat_add_distrib)
   379 
   380 lemma nat_number_of_add_1 [simp]:
   381   "number_of v + (1::nat) =
   382     (if v < Int.Pls then 1 else number_of (Int.succ v))"
   383   unfolding nat_number_of_def number_of_is_id numeral_simps
   384   by (simp add: nat_add_distrib)
   385 
   386 lemma nat_1_add_number_of [simp]:
   387   "(1::nat) + number_of v =
   388     (if v < Int.Pls then 1 else number_of (Int.succ v))"
   389   unfolding nat_number_of_def number_of_is_id numeral_simps
   390   by (simp add: nat_add_distrib)
   391 
   392 lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
   393   by (rule int_int_eq [THEN iffD1]) simp
   394 
   395 
   396 subsubsection{*Subtraction *}
   397 
   398 lemma diff_nat_eq_if:
   399      "nat z - nat z' =  
   400         (if neg z' then nat z   
   401          else let d = z-z' in     
   402               if neg d then 0 else nat d)"
   403 by (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
   404 
   405 
   406 lemma diff_nat_number_of [simp]: 
   407      "(number_of v :: nat) - number_of v' =  
   408         (if v' < Int.Pls then number_of v  
   409          else let d = number_of (v + uminus v') in     
   410               if neg d then 0 else nat d)"
   411   unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
   412   by auto
   413 
   414 lemma nat_number_of_diff_1 [simp]:
   415   "number_of v - (1::nat) =
   416     (if v \<le> Int.Pls then 0 else number_of (Int.pred v))"
   417   unfolding nat_number_of_def number_of_is_id numeral_simps
   418   by auto
   419 
   420 
   421 subsubsection{*Multiplication *}
   422 
   423 lemma mult_nat_number_of [simp]:
   424      "(number_of v :: nat) * number_of v' =  
   425        (if v < Int.Pls then 0 else number_of (v * v'))"
   426   unfolding nat_number_of_def number_of_is_id numeral_simps
   427   by (simp add: nat_mult_distrib)
   428 
   429 
   430 subsection{*Comparisons*}
   431 
   432 subsubsection{*Equals (=) *}
   433 
   434 lemma eq_nat_number_of [simp]:
   435      "((number_of v :: nat) = number_of v') =  
   436       (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
   437        else if neg (number_of v' :: int) then (number_of v :: int) = 0
   438        else v = v')"
   439   unfolding nat_number_of_def number_of_is_id neg_def
   440   by auto
   441 
   442 
   443 subsubsection{*Less-than (<) *}
   444 
   445 lemma less_nat_number_of [simp]:
   446   "(number_of v :: nat) < number_of v' \<longleftrightarrow>
   447     (if v < v' then Int.Pls < v' else False)"
   448   unfolding nat_number_of_def number_of_is_id numeral_simps
   449   by auto
   450 
   451 
   452 subsubsection{*Less-than-or-equal *}
   453 
   454 lemma le_nat_number_of [simp]:
   455   "(number_of v :: nat) \<le> number_of v' \<longleftrightarrow>
   456     (if v \<le> v' then True else v \<le> Int.Pls)"
   457   unfolding nat_number_of_def number_of_is_id numeral_simps
   458   by auto
   459 
   460 (*Maps #n to n for n = 0, 1, 2*)
   461 lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
   462 
   463 
   464 subsection{*Powers with Numeric Exponents*}
   465 
   466 text{*Squares of literal numerals will be evaluated.*}
   467 lemmas power2_eq_square_number_of [simp] =
   468     power2_eq_square [of "number_of w", standard]
   469 
   470 
   471 text{*Simprules for comparisons where common factors can be cancelled.*}
   472 lemmas zero_compare_simps =
   473     add_strict_increasing add_strict_increasing2 add_increasing
   474     zero_le_mult_iff zero_le_divide_iff 
   475     zero_less_mult_iff zero_less_divide_iff 
   476     mult_le_0_iff divide_le_0_iff 
   477     mult_less_0_iff divide_less_0_iff 
   478     zero_le_power2 power2_less_0
   479 
   480 subsubsection{*Nat *}
   481 
   482 lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
   483 by simp
   484 
   485 (*Expresses a natural number constant as the Suc of another one.
   486   NOT suitable for rewriting because n recurs in the condition.*)
   487 lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
   488 
   489 subsubsection{*Arith *}
   490 
   491 lemma Suc_eq_plus1: "Suc n = n + 1"
   492   unfolding One_nat_def by simp
   493 
   494 lemma Suc_eq_plus1_left: "Suc n = 1 + n"
   495   unfolding One_nat_def by simp
   496 
   497 (* These two can be useful when m = number_of... *)
   498 
   499 lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
   500   unfolding One_nat_def by (cases m) simp_all
   501 
   502 lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
   503   unfolding One_nat_def by (cases m) simp_all
   504 
   505 lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
   506   unfolding One_nat_def by (cases m) simp_all
   507 
   508 
   509 subsection{*Comparisons involving (0::nat) *}
   510 
   511 text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
   512 
   513 lemma eq_number_of_0 [simp]:
   514   "number_of v = (0::nat) \<longleftrightarrow> v \<le> Int.Pls"
   515   unfolding nat_number_of_def number_of_is_id numeral_simps
   516   by auto
   517 
   518 lemma eq_0_number_of [simp]:
   519   "(0::nat) = number_of v \<longleftrightarrow> v \<le> Int.Pls"
   520 by (rule trans [OF eq_sym_conv eq_number_of_0])
   521 
   522 lemma less_0_number_of [simp]:
   523    "(0::nat) < number_of v \<longleftrightarrow> Int.Pls < v"
   524   unfolding nat_number_of_def number_of_is_id numeral_simps
   525   by simp
   526 
   527 lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
   528 by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
   529 
   530 
   531 
   532 subsection{*Comparisons involving  @{term Suc} *}
   533 
   534 lemma eq_number_of_Suc [simp]:
   535      "(number_of v = Suc n) =  
   536         (let pv = number_of (Int.pred v) in  
   537          if neg pv then False else nat pv = n)"
   538 apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   539                   number_of_pred nat_number_of_def 
   540             split add: split_if)
   541 apply (rule_tac x = "number_of v" in spec)
   542 apply (auto simp add: nat_eq_iff)
   543 done
   544 
   545 lemma Suc_eq_number_of [simp]:
   546      "(Suc n = number_of v) =  
   547         (let pv = number_of (Int.pred v) in  
   548          if neg pv then False else nat pv = n)"
   549 by (rule trans [OF eq_sym_conv eq_number_of_Suc])
   550 
   551 lemma less_number_of_Suc [simp]:
   552      "(number_of v < Suc n) =  
   553         (let pv = number_of (Int.pred v) in  
   554          if neg pv then True else nat pv < n)"
   555 apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   556                   number_of_pred nat_number_of_def  
   557             split add: split_if)
   558 apply (rule_tac x = "number_of v" in spec)
   559 apply (auto simp add: nat_less_iff)
   560 done
   561 
   562 lemma less_Suc_number_of [simp]:
   563      "(Suc n < number_of v) =  
   564         (let pv = number_of (Int.pred v) in  
   565          if neg pv then False else n < nat pv)"
   566 apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   567                   number_of_pred nat_number_of_def
   568             split add: split_if)
   569 apply (rule_tac x = "number_of v" in spec)
   570 apply (auto simp add: zless_nat_eq_int_zless)
   571 done
   572 
   573 lemma le_number_of_Suc [simp]:
   574      "(number_of v <= Suc n) =  
   575         (let pv = number_of (Int.pred v) in  
   576          if neg pv then True else nat pv <= n)"
   577 by (simp add: Let_def linorder_not_less [symmetric])
   578 
   579 lemma le_Suc_number_of [simp]:
   580      "(Suc n <= number_of v) =  
   581         (let pv = number_of (Int.pred v) in  
   582          if neg pv then False else n <= nat pv)"
   583 by (simp add: Let_def linorder_not_less [symmetric])
   584 
   585 
   586 lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
   587 by auto
   588 
   589 
   590 
   591 subsection{*Max and Min Combined with @{term Suc} *}
   592 
   593 lemma max_number_of_Suc [simp]:
   594      "max (Suc n) (number_of v) =  
   595         (let pv = number_of (Int.pred v) in  
   596          if neg pv then Suc n else Suc(max n (nat pv)))"
   597 apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   598             split add: split_if nat.split)
   599 apply (rule_tac x = "number_of v" in spec) 
   600 apply auto
   601 done
   602  
   603 lemma max_Suc_number_of [simp]:
   604      "max (number_of v) (Suc n) =  
   605         (let pv = number_of (Int.pred v) in  
   606          if neg pv then Suc n else Suc(max (nat pv) n))"
   607 apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   608             split add: split_if nat.split)
   609 apply (rule_tac x = "number_of v" in spec) 
   610 apply auto
   611 done
   612  
   613 lemma min_number_of_Suc [simp]:
   614      "min (Suc n) (number_of v) =  
   615         (let pv = number_of (Int.pred v) in  
   616          if neg pv then 0 else Suc(min n (nat pv)))"
   617 apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   618             split add: split_if nat.split)
   619 apply (rule_tac x = "number_of v" in spec) 
   620 apply auto
   621 done
   622  
   623 lemma min_Suc_number_of [simp]:
   624      "min (number_of v) (Suc n) =  
   625         (let pv = number_of (Int.pred v) in  
   626          if neg pv then 0 else Suc(min (nat pv) n))"
   627 apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   628             split add: split_if nat.split)
   629 apply (rule_tac x = "number_of v" in spec) 
   630 apply auto
   631 done
   632  
   633 subsection{*Literal arithmetic involving powers*}
   634 
   635 lemma power_nat_number_of:
   636      "(number_of v :: nat) ^ n =  
   637        (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))"
   638 by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
   639          split add: split_if cong: imp_cong)
   640 
   641 
   642 lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w", standard]
   643 declare power_nat_number_of_number_of [simp]
   644 
   645 
   646 
   647 text{*For arbitrary rings*}
   648 
   649 lemma power_number_of_even:
   650   fixes z :: "'a::number_ring"
   651   shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
   652 by (cases "w \<ge> 0") (auto simp add: Let_def Bit0_def nat_number_of_def number_of_is_id
   653   nat_add_distrib power_add simp del: nat_number_of)
   654 
   655 lemma power_number_of_odd:
   656   fixes z :: "'a::number_ring"
   657   shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
   658      then (let w = z ^ (number_of w) in z * w * w) else 1)"
   659 unfolding Let_def Bit1_def nat_number_of_def number_of_is_id
   660 apply (cases "0 <= w")
   661 apply (simp only: mult_assoc nat_add_distrib power_add, simp)
   662 apply (simp add: not_le mult_2 [symmetric] add_assoc)
   663 done
   664 
   665 lemmas zpower_number_of_even = power_number_of_even [where 'a=int]
   666 lemmas zpower_number_of_odd = power_number_of_odd [where 'a=int]
   667 
   668 lemmas power_number_of_even_number_of [simp] =
   669     power_number_of_even [of "number_of v", standard]
   670 
   671 lemmas power_number_of_odd_number_of [simp] =
   672     power_number_of_odd [of "number_of v", standard]
   673 
   674 lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
   675   by (simp add: nat_number_of_def)
   676 
   677 lemma nat_number_of_Min [no_atp]: "number_of Int.Min = (0::nat)"
   678   apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   679   done
   680 
   681 lemma nat_number_of_Bit0:
   682     "number_of (Int.Bit0 w) = (let n::nat = number_of w in n + n)"
   683 by (cases "w \<ge> 0") (auto simp add: Let_def Bit0_def nat_number_of_def number_of_is_id
   684   nat_add_distrib simp del: nat_number_of)
   685 
   686 lemma nat_number_of_Bit1:
   687   "number_of (Int.Bit1 w) =
   688     (if neg (number_of w :: int) then 0
   689      else let n = number_of w in Suc (n + n))"
   690 unfolding Let_def Bit1_def nat_number_of_def number_of_is_id neg_def
   691 apply (cases "w < 0")
   692 apply (simp add: mult_2 [symmetric] add_assoc)
   693 apply (simp only: nat_add_distrib, simp)
   694 done
   695 
   696 lemmas eval_nat_numeral =
   697   nat_number_of_Bit0 nat_number_of_Bit1
   698 
   699 lemmas nat_arith =
   700   add_nat_number_of
   701   diff_nat_number_of
   702   mult_nat_number_of
   703   eq_nat_number_of
   704   less_nat_number_of
   705 
   706 lemmas semiring_norm =
   707   Let_def arith_simps nat_arith rel_simps neg_simps if_False
   708   if_True add_0 add_Suc add_number_of_left mult_number_of_left
   709   numeral_1_eq_1 [symmetric] Suc_eq_plus1
   710   numeral_0_eq_0 [symmetric] numerals [symmetric]
   711   not_iszero_Numeral1
   712 
   713 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   714   by (fact Let_def)
   715 
   716 lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring})"
   717   by (simp only: number_of_Min power_minus1_even)
   718 
   719 lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring})"
   720   by (simp only: number_of_Min power_minus1_odd)
   721 
   722 lemma nat_number_of_add_left:
   723      "number_of v + (number_of v' + (k::nat)) =  
   724          (if neg (number_of v :: int) then number_of v' + k  
   725           else if neg (number_of v' :: int) then number_of v + k  
   726           else number_of (v + v') + k)"
   727 by (auto simp add: neg_def)
   728 
   729 lemma nat_number_of_mult_left:
   730      "number_of v * (number_of v' * (k::nat)) =  
   731          (if v < Int.Pls then 0
   732           else number_of (v * v') * k)"
   733 by (auto simp add: not_less Pls_def nat_number_of_def number_of_is_id
   734   nat_mult_distrib simp del: nat_number_of)
   735 
   736 
   737 subsection{*Literal arithmetic and @{term of_nat}*}
   738 
   739 lemma of_nat_double:
   740      "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
   741 by (simp only: mult_2 nat_add_distrib of_nat_add) 
   742 
   743 lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
   744 by (simp only: nat_number_of_def)
   745 
   746 lemma of_nat_number_of_lemma:
   747      "of_nat (number_of v :: nat) =  
   748          (if 0 \<le> (number_of v :: int) 
   749           then (number_of v :: 'a :: number_ring)
   750           else 0)"
   751 by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat)
   752 
   753 lemma of_nat_number_of_eq [simp]:
   754      "of_nat (number_of v :: nat) =  
   755          (if neg (number_of v :: int) then 0  
   756           else (number_of v :: 'a :: number_ring))"
   757 by (simp only: of_nat_number_of_lemma neg_def, simp) 
   758 
   759 
   760 subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
   761 
   762 text{*Where K above is a literal*}
   763 
   764 lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
   765 by (simp split: nat_diff_split)
   766 
   767 text {*Now just instantiating @{text n} to @{text "number_of v"} does
   768   the right simplification, but with some redundant inequality
   769   tests.*}
   770 lemma neg_number_of_pred_iff_0:
   771   "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
   772 apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
   773 apply (simp only: less_Suc_eq_le le_0_eq)
   774 apply (subst less_number_of_Suc, simp)
   775 done
   776 
   777 text{*No longer required as a simprule because of the @{text inverse_fold}
   778    simproc*}
   779 lemma Suc_diff_number_of:
   780      "Int.Pls < v ==>
   781       Suc m - (number_of v) = m - (number_of (Int.pred v))"
   782 apply (subst Suc_diff_eq_diff_pred)
   783 apply simp
   784 apply (simp del: nat_numeral_1_eq_1)
   785 apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
   786                         neg_number_of_pred_iff_0)
   787 done
   788 
   789 lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
   790 by (simp split: nat_diff_split)
   791 
   792 
   793 subsubsection{*For @{term nat_case} and @{term nat_rec}*}
   794 
   795 lemma nat_case_number_of [simp]:
   796      "nat_case a f (number_of v) =
   797         (let pv = number_of (Int.pred v) in
   798          if neg pv then a else f (nat pv))"
   799 by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
   800 
   801 lemma nat_case_add_eq_if [simp]:
   802      "nat_case a f ((number_of v) + n) =
   803        (let pv = number_of (Int.pred v) in
   804          if neg pv then nat_case a f n else f (nat pv + n))"
   805 apply (subst add_eq_if)
   806 apply (simp split add: nat.split
   807             del: nat_numeral_1_eq_1
   808             add: nat_numeral_1_eq_1 [symmetric]
   809                  numeral_1_eq_Suc_0 [symmetric]
   810                  neg_number_of_pred_iff_0)
   811 done
   812 
   813 lemma nat_rec_number_of [simp]:
   814      "nat_rec a f (number_of v) =
   815         (let pv = number_of (Int.pred v) in
   816          if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
   817 apply (case_tac " (number_of v) ::nat")
   818 apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
   819 apply (simp split add: split_if_asm)
   820 done
   821 
   822 lemma nat_rec_add_eq_if [simp]:
   823      "nat_rec a f (number_of v + n) =
   824         (let pv = number_of (Int.pred v) in
   825          if neg pv then nat_rec a f n
   826                    else f (nat pv + n) (nat_rec a f (nat pv + n)))"
   827 apply (subst add_eq_if)
   828 apply (simp split add: nat.split
   829             del: nat_numeral_1_eq_1
   830             add: nat_numeral_1_eq_1 [symmetric]
   831                  numeral_1_eq_Suc_0 [symmetric]
   832                  neg_number_of_pred_iff_0)
   833 done
   834 
   835 
   836 subsubsection{*Various Other Lemmas*}
   837 
   838 lemma card_UNIV_bool[simp]: "card (UNIV :: bool set) = 2"
   839 by(simp add: UNIV_bool)
   840 
   841 text {*Evens and Odds, for Mutilated Chess Board*}
   842 
   843 text{*Lemmas for specialist use, NOT as default simprules*}
   844 lemma nat_mult_2: "2 * z = (z+z::nat)"
   845 unfolding nat_1_add_1 [symmetric] left_distrib by simp
   846 
   847 lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
   848 by (subst mult_commute, rule nat_mult_2)
   849 
   850 text{*Case analysis on @{term "n<2"}*}
   851 lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
   852 by (auto simp add: nat_1_add_1 [symmetric])
   853 
   854 text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
   855 
   856 lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
   857 by simp
   858 
   859 lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
   860 by simp
   861 
   862 text{*Can be used to eliminate long strings of Sucs, but not by default*}
   863 lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
   864 by simp
   865 
   866 end