src/HOL/Nat_Numeral.thy
changeset 46026 83caa4f4bd56
parent 45607 16b4f5774621
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/Nat_Numeral.thy	Wed Dec 28 22:08:44 2011 +0100
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Thu Dec 29 10:47:54 2011 +0100
     1.3 @@ -331,20 +331,20 @@
     1.4  declare nat_1 [simp]
     1.5  
     1.6  lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
     1.7 -by (simp add: nat_number_of_def)
     1.8 +  by (simp add: nat_number_of_def)
     1.9  
    1.10 -lemma nat_numeral_0_eq_0 [simp, code_post]: "Numeral0 = (0::nat)"
    1.11 -  by (rule semiring_numeral_0_eq_0)
    1.12 +lemma nat_numeral_0_eq_0: "Numeral0 = (0::nat)" (* FIXME delete candidate *)
    1.13 +  by (fact semiring_numeral_0_eq_0)
    1.14  
    1.15 -lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
    1.16 -  by (rule semiring_numeral_1_eq_1)
    1.17 +lemma nat_numeral_1_eq_1: "Numeral1 = (1::nat)" (* FIXME delete candidate *)
    1.18 +  by (fact semiring_numeral_1_eq_1)
    1.19  
    1.20  lemma Numeral1_eq1_nat:
    1.21    "(1::nat) = Numeral1"
    1.22    by simp
    1.23  
    1.24 -lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0"
    1.25 -by (simp only: nat_numeral_1_eq_1 One_nat_def)
    1.26 +lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
    1.27 +  by (simp only: nat_numeral_1_eq_1 One_nat_def)
    1.28  
    1.29  
    1.30  subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
    1.31 @@ -570,8 +570,7 @@
    1.32    by simp
    1.33  
    1.34  lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
    1.35 -by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
    1.36 -
    1.37 +  by (simp del: semiring_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
    1.38  
    1.39  
    1.40  subsection{*Comparisons involving  @{term Suc} *}
    1.41 @@ -827,7 +826,7 @@
    1.42        Suc m - (number_of v) = m - (number_of (Int.pred v))"
    1.43  apply (subst Suc_diff_eq_diff_pred)
    1.44  apply simp
    1.45 -apply (simp del: nat_numeral_1_eq_1)
    1.46 +apply (simp del: semiring_numeral_1_eq_1)
    1.47  apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
    1.48                          neg_number_of_pred_iff_0)
    1.49  done
    1.50 @@ -850,8 +849,8 @@
    1.51           if neg pv then nat_case a f n else f (nat pv + n))"
    1.52  apply (subst add_eq_if)
    1.53  apply (simp split add: nat.split
    1.54 -            del: nat_numeral_1_eq_1
    1.55 -            add: nat_numeral_1_eq_1 [symmetric]
    1.56 +            del: semiring_numeral_1_eq_1
    1.57 +            add: semiring_numeral_1_eq_1 [symmetric]
    1.58                   numeral_1_eq_Suc_0 [symmetric]
    1.59                   neg_number_of_pred_iff_0)
    1.60  done
    1.61 @@ -872,8 +871,8 @@
    1.62                     else f (nat pv + n) (nat_rec a f (nat pv + n)))"
    1.63  apply (subst add_eq_if)
    1.64  apply (simp split add: nat.split
    1.65 -            del: nat_numeral_1_eq_1
    1.66 -            add: nat_numeral_1_eq_1 [symmetric]
    1.67 +            del: semiring_numeral_1_eq_1
    1.68 +            add: semiring_numeral_1_eq_1 [symmetric]
    1.69                   numeral_1_eq_Suc_0 [symmetric]
    1.70                   neg_number_of_pred_iff_0)
    1.71  done