semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat

--- a/src/HOL/Divides.thy	Wed Dec 28 22:08:44 2011 +0100
+++ b/src/HOL/Divides.thy	Thu Dec 29 10:47:54 2011 +0100
@@ -2418,7 +2418,7 @@
 
 lemma one_div_nat_number_of [simp]:
      "Suc 0 div number_of v' = nat (1 div number_of v')" 
-by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
+  by (simp del: semiring_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric] semiring_numeral_1_eq_1 [symmetric]) 
 
 lemma mod_nat_number_of [simp]:
      "(number_of v :: nat)  mod  number_of v' =  
@@ -2432,7 +2432,7 @@
      "Suc 0 mod number_of v' =  
         (if neg (number_of v' :: int) then Suc 0
          else nat (1 mod number_of v'))"
-by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
+by (simp del: semiring_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric] semiring_numeral_1_eq_1 [symmetric]) 
 
 lemmas dvd_eq_mod_eq_0_number_of [simp] =
   dvd_eq_mod_eq_0 [of "number_of x" "number_of y"] for x y

--- a/src/HOL/Nat_Numeral.thy	Wed Dec 28 22:08:44 2011 +0100
+++ b/src/HOL/Nat_Numeral.thy	Thu Dec 29 10:47:54 2011 +0100
@@ -331,20 +331,20 @@
 declare nat_1 [simp]
 
 lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
-by (simp add: nat_number_of_def)
+  by (simp add: nat_number_of_def)
 
-lemma nat_numeral_0_eq_0 [simp, code_post]: "Numeral0 = (0::nat)"
-  by (rule semiring_numeral_0_eq_0)
+lemma nat_numeral_0_eq_0: "Numeral0 = (0::nat)" (* FIXME delete candidate *)
+  by (fact semiring_numeral_0_eq_0)
 
-lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
-  by (rule semiring_numeral_1_eq_1)
+lemma nat_numeral_1_eq_1: "Numeral1 = (1::nat)" (* FIXME delete candidate *)
+  by (fact semiring_numeral_1_eq_1)
 
 lemma Numeral1_eq1_nat:
   "(1::nat) = Numeral1"
   by simp
 
-lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0"
-by (simp only: nat_numeral_1_eq_1 One_nat_def)
+lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
+  by (simp only: nat_numeral_1_eq_1 One_nat_def)
 
 
 subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
@@ -570,8 +570,7 @@
   by simp
 
 lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
-by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
-
+  by (simp del: semiring_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
 
 
 subsection{*Comparisons involving  @{term Suc} *}
@@ -827,7 +826,7 @@
       Suc m - (number_of v) = m - (number_of (Int.pred v))"
 apply (subst Suc_diff_eq_diff_pred)
 apply simp
-apply (simp del: nat_numeral_1_eq_1)
+apply (simp del: semiring_numeral_1_eq_1)
 apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
                         neg_number_of_pred_iff_0)
 done
@@ -850,8 +849,8 @@
          if neg pv then nat_case a f n else f (nat pv + n))"
 apply (subst add_eq_if)
 apply (simp split add: nat.split
-            del: nat_numeral_1_eq_1
-            add: nat_numeral_1_eq_1 [symmetric]
+            del: semiring_numeral_1_eq_1
+            add: semiring_numeral_1_eq_1 [symmetric]
                  numeral_1_eq_Suc_0 [symmetric]
                  neg_number_of_pred_iff_0)
 done
@@ -872,8 +871,8 @@
                    else f (nat pv + n) (nat_rec a f (nat pv + n)))"
 apply (subst add_eq_if)
 apply (simp split add: nat.split
-            del: nat_numeral_1_eq_1
-            add: nat_numeral_1_eq_1 [symmetric]
+            del: semiring_numeral_1_eq_1
+            add: semiring_numeral_1_eq_1 [symmetric]
                  numeral_1_eq_Suc_0 [symmetric]
                  neg_number_of_pred_iff_0)
 done

--- a/src/HOL/Set.thy	Wed Dec 28 22:08:44 2011 +0100
+++ b/src/HOL/Set.thy	Thu Dec 29 10:47:54 2011 +0100
@@ -1804,7 +1804,7 @@
 hide_const (open) remove
 
 definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
-  "project P A = {a \<in> A. P a}"
+  [code_abbrev]: "project P A = {a \<in> A. P a}"
 
 hide_const (open) project
 

--- a/src/HOL/Word/Word.thy	Wed Dec 28 22:08:44 2011 +0100
+++ b/src/HOL/Word/Word.thy	Thu Dec 29 10:47:54 2011 +0100
@@ -507,10 +507,12 @@
 
 lemmas td_sint = word_sint.td
 
-lemma word_number_of_alt [code_unfold_post]:
+lemma word_number_of_alt:
   "number_of b = word_of_int (number_of b)"
   by (simp add: number_of_eq word_number_of_def)
 
+declare word_number_of_alt [symmetric, code_abbrev]
+
 lemma word_no_wi: "number_of = word_of_int"
   by (auto simp: word_number_of_def)
 

--- a/src/Tools/Code/code_preproc.ML	Wed Dec 28 22:08:44 2011 +0100
+++ b/src/Tools/Code/code_preproc.ML	Thu Dec 29 10:47:54 2011 +0100
@@ -88,13 +88,13 @@
 val add_post = map_post o Simplifier.add_simp;
 val del_post = map_post o Simplifier.del_simp;
 
-fun add_unfold_post raw_thm thy =
+fun add_code_abbrev raw_thm thy =
   let
     val thm = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy) raw_thm;
     val thm_sym = Thm.symmetric thm;
   in
     thy |> map_pre_post (fn (pre, post) =>
-      (pre |> Simplifier.add_simp thm, post |> Simplifier.add_simp thm_sym))
+      (pre |> Simplifier.add_simp thm_sym, post |> Simplifier.add_simp thm))
   end;
 
 fun add_functrans (name, f) = (map_data o apsnd)
@@ -520,8 +520,8 @@
         "preprocessing equations for code generator"
     #> Attrib.setup @{binding code_post} (add_del_attribute_parser add_post del_post)
         "postprocessing equations for code generator"
-    #> Attrib.setup @{binding code_unfold_post} (Scan.succeed (mk_attribute add_unfold_post))
-        "pre- and postprocessing equations for code generator"
+    #> Attrib.setup @{binding code_abbrev} (Scan.succeed (mk_attribute add_code_abbrev))
+        "post- and preprocessing equations for code generator"
   end;
 
 val _ =