src/HOL/Nat_Numeral.thy
changeset 43531 cc46a678faaf
parent 43526 2b92a6943915
child 44345 881c324470a2
equal deleted inserted replaced
43530:f05a707fdf91 43531:cc46a678faaf
    13 
    13 
    14 text {*
    14 text {*
    15   Arithmetic for naturals is reduced to that for the non-negative integers.
    15   Arithmetic for naturals is reduced to that for the non-negative integers.
    16 *}
    16 *}
    17 
    17 
    18 instantiation nat :: number
    18 instantiation nat :: number_semiring
    19 begin
    19 begin
    20 
    20 
    21 definition
    21 definition
    22   nat_number_of_def [code_unfold, code del]: "number_of v = nat (number_of v)"
    22   nat_number_of_def [code_unfold, code del]: "number_of v = nat (number_of v)"
    23 
    23 
    24 instance ..
    24 instance proof
    25 
    25   fix n show "number_of (int n) = (of_nat n :: nat)"
       
    26     unfolding nat_number_of_def number_of_eq by simp
       
    27 qed
       
    28  
    26 end
    29 end
    27 
    30 
    28 lemma [code_post]:
    31 lemma [code_post]:
    29   "nat (number_of v) = number_of v"
    32   "nat (number_of v) = number_of v"
    30   unfolding nat_number_of_def ..
    33   unfolding nat_number_of_def ..
   248   unfolding power2_eq_square by (rule sum_squares_gt_zero_iff)
   251   unfolding power2_eq_square by (rule sum_squares_gt_zero_iff)
   249 
   252 
   250 end
   253 end
   251 
   254 
   252 lemma power2_sum:
   255 lemma power2_sum:
   253   fixes x y :: "'a::number_ring"
   256   fixes x y :: "'a::number_semiring"
   254   shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
   257   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)
   258   by (simp add: algebra_simps power2_eq_square semiring_mult_2_right)
   256 
   259 
   257 lemma power2_diff:
   260 lemma power2_diff:
   258   fixes x y :: "'a::number_ring"
   261   fixes x y :: "'a::number_ring"
   259   shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
   262   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)
   263   by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
   343          (if neg (number_of v :: int) then 0  
   346          (if neg (number_of v :: int) then 0  
   344           else (number_of v :: int))"
   347           else (number_of v :: int))"
   345   unfolding nat_number_of_def number_of_is_id neg_def
   348   unfolding nat_number_of_def number_of_is_id neg_def
   346   by simp
   349   by simp
   347 
   350 
       
   351 lemma nonneg_int_cases:
       
   352   fixes k :: int assumes "0 \<le> k" obtains n where "k = of_nat n"
       
   353   using assms by (cases k, simp, simp)
   348 
   354 
   349 subsubsection{*Successor *}
   355 subsubsection{*Successor *}
   350 
   356 
   351 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
   357 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
   352 apply (rule sym)
   358 apply (rule sym)
   388     (if v < Int.Pls then 1 else number_of (Int.succ v))"
   394     (if v < Int.Pls then 1 else number_of (Int.succ v))"
   389   unfolding nat_number_of_def number_of_is_id numeral_simps
   395   unfolding nat_number_of_def number_of_is_id numeral_simps
   390   by (simp add: nat_add_distrib)
   396   by (simp add: nat_add_distrib)
   391 
   397 
   392 lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
   398 lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
   393   by (rule int_int_eq [THEN iffD1]) simp
   399   by (rule semiring_one_add_one_is_two)
       
   400 
       
   401 text {* TODO: replace simp rules above with these generic ones: *}
       
   402 
       
   403 lemma semiring_add_number_of:
       
   404   "\<lbrakk>Int.Pls \<le> v; Int.Pls \<le> v'\<rbrakk> \<Longrightarrow>
       
   405     (number_of v :: 'a::number_semiring) + number_of v' = number_of (v + v')"
       
   406   unfolding Int.Pls_def
       
   407   by (elim nonneg_int_cases,
       
   408     simp only: number_of_int of_nat_add [symmetric])
       
   409 
       
   410 lemma semiring_number_of_add_1:
       
   411   "Int.Pls \<le> v \<Longrightarrow>
       
   412     number_of v + (1::'a::number_semiring) = number_of (Int.succ v)"
       
   413   unfolding Int.Pls_def Int.succ_def
       
   414   by (elim nonneg_int_cases,
       
   415     simp only: number_of_int add_commute [where b=1] of_nat_Suc [symmetric])
       
   416 
       
   417 lemma semiring_1_add_number_of:
       
   418   "Int.Pls \<le> v \<Longrightarrow>
       
   419     (1::'a::number_semiring) + number_of v = number_of (Int.succ v)"
       
   420   unfolding Int.Pls_def Int.succ_def
       
   421   by (elim nonneg_int_cases,
       
   422     simp only: number_of_int add_commute [where b=1] of_nat_Suc [symmetric])
   394 
   423 
   395 
   424 
   396 subsubsection{*Subtraction *}
   425 subsubsection{*Subtraction *}
   397 
   426 
   398 lemma diff_nat_eq_if:
   427 lemma diff_nat_eq_if:
   423 lemma mult_nat_number_of [simp]:
   452 lemma mult_nat_number_of [simp]:
   424      "(number_of v :: nat) * number_of v' =  
   453      "(number_of v :: nat) * number_of v' =  
   425        (if v < Int.Pls then 0 else number_of (v * v'))"
   454        (if v < Int.Pls then 0 else number_of (v * v'))"
   426   unfolding nat_number_of_def number_of_is_id numeral_simps
   455   unfolding nat_number_of_def number_of_is_id numeral_simps
   427   by (simp add: nat_mult_distrib)
   456   by (simp add: nat_mult_distrib)
       
   457 
       
   458 (* TODO: replace mult_nat_number_of with this next rule *)
       
   459 lemma semiring_mult_number_of:
       
   460   "\<lbrakk>Int.Pls \<le> v; Int.Pls \<le> v'\<rbrakk> \<Longrightarrow>
       
   461     (number_of v :: 'a::number_semiring) * number_of v' = number_of (v * v')"
       
   462   unfolding Int.Pls_def
       
   463   by (elim nonneg_int_cases,
       
   464     simp only: number_of_int of_nat_mult [symmetric])
   428 
   465 
   429 
   466 
   430 subsection{*Comparisons*}
   467 subsection{*Comparisons*}
   431 
   468 
   432 subsubsection{*Equals (=) *}
   469 subsubsection{*Equals (=) *}
   840 
   877 
   841 text {*Evens and Odds, for Mutilated Chess Board*}
   878 text {*Evens and Odds, for Mutilated Chess Board*}
   842 
   879 
   843 text{*Lemmas for specialist use, NOT as default simprules*}
   880 text{*Lemmas for specialist use, NOT as default simprules*}
   844 lemma nat_mult_2: "2 * z = (z+z::nat)"
   881 lemma nat_mult_2: "2 * z = (z+z::nat)"
   845 unfolding nat_1_add_1 [symmetric] left_distrib by simp
   882 by (rule semiring_mult_2)
   846 
   883 
   847 lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
   884 lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
   848 by (subst mult_commute, rule nat_mult_2)
   885 by (rule semiring_mult_2_right)
   849 
   886 
   850 text{*Case analysis on @{term "n<2"}*}
   887 text{*Case analysis on @{term "n<2"}*}
   851 lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
   888 lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
   852 by (auto simp add: nat_1_add_1 [symmetric])
   889 by (auto simp add: nat_1_add_1 [symmetric])
   853 
   890