src/HOL/Nat_Numeral.thy
changeset 44884 02efd5a6b6e5
parent 44857 73d5b722c4b4
child 45607 16b4f5774621
     1.1 --- a/src/HOL/Nat_Numeral.thy	Sun Sep 11 07:21:45 2011 -0700
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Sun Sep 11 09:40:18 2011 -0700
     1.3 @@ -334,10 +334,10 @@
     1.4  by (simp add: nat_number_of_def)
     1.5  
     1.6  lemma nat_numeral_0_eq_0 [simp, code_post]: "Numeral0 = (0::nat)"
     1.7 -by (simp add: nat_number_of_def)
     1.8 +  by (rule semiring_numeral_0_eq_0)
     1.9  
    1.10  lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
    1.11 -by (simp add: nat_number_of_def)
    1.12 +  by (rule semiring_numeral_1_eq_1)
    1.13  
    1.14  lemma Numeral1_eq1_nat:
    1.15    "(1::nat) = Numeral1"
    1.16 @@ -354,7 +354,7 @@
    1.17           (if neg (number_of v :: int) then 0  
    1.18            else (number_of v :: int))"
    1.19    unfolding nat_number_of_def number_of_is_id neg_def
    1.20 -  by simp
    1.21 +  by simp (* FIXME: redundant with of_nat_number_of_eq *)
    1.22  
    1.23  lemma nonneg_int_cases:
    1.24    fixes k :: int assumes "0 \<le> k" obtains n where "k = of_nat n"