semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat; attribute code_abbrev superseedes code_unfold_post
authorhaftmann
Thu Dec 29 10:47:55 2011 +0100 (2011-12-29)
changeset 46027ff3c4f2bee01
parent 46026 83caa4f4bd56
child 46028 9f113cdf3d66
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat; attribute code_abbrev superseedes code_unfold_post
src/HOL/Int.thy
     1.1 --- a/src/HOL/Int.thy	Thu Dec 29 10:47:54 2011 +0100
     1.2 +++ b/src/HOL/Int.thy	Thu Dec 29 10:47:55 2011 +0100
     1.3 @@ -1009,21 +1009,21 @@
     1.4    Converting numerals 0 and 1 to their abstract versions.
     1.5  *}
     1.6  
     1.7 -lemma semiring_numeral_0_eq_0:
     1.8 +lemma semiring_numeral_0_eq_0 [simp, code_post]:
     1.9    "Numeral0 = (0::'a::number_semiring)"
    1.10    using number_of_int [where 'a='a and n=0]
    1.11    unfolding numeral_simps by simp
    1.12  
    1.13 -lemma semiring_numeral_1_eq_1:
    1.14 +lemma semiring_numeral_1_eq_1 [simp, code_post]:
    1.15    "Numeral1 = (1::'a::number_semiring)"
    1.16    using number_of_int [where 'a='a and n=1]
    1.17    unfolding numeral_simps by simp
    1.18  
    1.19 -lemma numeral_0_eq_0 [simp, code_post]:
    1.20 +lemma numeral_0_eq_0: (* FIXME delete candidate *)
    1.21    "Numeral0 = (0::'a::number_ring)"
    1.22    by (rule semiring_numeral_0_eq_0)
    1.23  
    1.24 -lemma numeral_1_eq_1 [simp, code_post]:
    1.25 +lemma numeral_1_eq_1: (* FIXME delete candidate *)
    1.26    "Numeral1 = (1::'a::number_ring)"
    1.27    by (rule semiring_numeral_1_eq_1)
    1.28  
    1.29 @@ -2296,11 +2296,11 @@
    1.30  
    1.31  hide_const (open) nat_aux
    1.32  
    1.33 -lemma zero_is_num_zero [code, code_unfold_post]:
    1.34 +lemma zero_is_num_zero [code, code_unfold]:
    1.35    "(0\<Colon>int) = Numeral0" 
    1.36    by simp
    1.37  
    1.38 -lemma one_is_num_one [code, code_unfold_post]:
    1.39 +lemma one_is_num_one [code, code_unfold]:
    1.40    "(1\<Colon>int) = Numeral1" 
    1.41    by simp
    1.42