semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
authorhaftmann
Thu Dec 29 10:47:54 2011 +0100 (2011-12-29)
changeset 4602683caa4f4bd56
parent 46025 64a19ea435fc
child 46027 ff3c4f2bee01
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
src/HOL/Divides.thy
src/HOL/Nat_Numeral.thy
src/HOL/Set.thy
src/HOL/Word/Word.thy
src/Tools/Code/code_preproc.ML
     1.1 --- a/src/HOL/Divides.thy	Wed Dec 28 22:08:44 2011 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Dec 29 10:47:54 2011 +0100
     1.3 @@ -2418,7 +2418,7 @@
     1.4  
     1.5  lemma one_div_nat_number_of [simp]:
     1.6       "Suc 0 div number_of v' = nat (1 div number_of v')" 
     1.7 -by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
     1.8 +  by (simp del: semiring_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric] semiring_numeral_1_eq_1 [symmetric]) 
     1.9  
    1.10  lemma mod_nat_number_of [simp]:
    1.11       "(number_of v :: nat)  mod  number_of v' =  
    1.12 @@ -2432,7 +2432,7 @@
    1.13       "Suc 0 mod number_of v' =  
    1.14          (if neg (number_of v' :: int) then Suc 0
    1.15           else nat (1 mod number_of v'))"
    1.16 -by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
    1.17 +by (simp del: semiring_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric] semiring_numeral_1_eq_1 [symmetric]) 
    1.18  
    1.19  lemmas dvd_eq_mod_eq_0_number_of [simp] =
    1.20    dvd_eq_mod_eq_0 [of "number_of x" "number_of y"] for x y
     2.1 --- a/src/HOL/Nat_Numeral.thy	Wed Dec 28 22:08:44 2011 +0100
     2.2 +++ b/src/HOL/Nat_Numeral.thy	Thu Dec 29 10:47:54 2011 +0100
     2.3 @@ -331,20 +331,20 @@
     2.4  declare nat_1 [simp]
     2.5  
     2.6  lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
     2.7 -by (simp add: nat_number_of_def)
     2.8 +  by (simp add: nat_number_of_def)
     2.9  
    2.10 -lemma nat_numeral_0_eq_0 [simp, code_post]: "Numeral0 = (0::nat)"
    2.11 -  by (rule semiring_numeral_0_eq_0)
    2.12 +lemma nat_numeral_0_eq_0: "Numeral0 = (0::nat)" (* FIXME delete candidate *)
    2.13 +  by (fact semiring_numeral_0_eq_0)
    2.14  
    2.15 -lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
    2.16 -  by (rule semiring_numeral_1_eq_1)
    2.17 +lemma nat_numeral_1_eq_1: "Numeral1 = (1::nat)" (* FIXME delete candidate *)
    2.18 +  by (fact semiring_numeral_1_eq_1)
    2.19  
    2.20  lemma Numeral1_eq1_nat:
    2.21    "(1::nat) = Numeral1"
    2.22    by simp
    2.23  
    2.24 -lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0"
    2.25 -by (simp only: nat_numeral_1_eq_1 One_nat_def)
    2.26 +lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
    2.27 +  by (simp only: nat_numeral_1_eq_1 One_nat_def)
    2.28  
    2.29  
    2.30  subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
    2.31 @@ -570,8 +570,7 @@
    2.32    by simp
    2.33  
    2.34  lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
    2.35 -by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
    2.36 -
    2.37 +  by (simp del: semiring_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
    2.38  
    2.39  
    2.40  subsection{*Comparisons involving  @{term Suc} *}
    2.41 @@ -827,7 +826,7 @@
    2.42        Suc m - (number_of v) = m - (number_of (Int.pred v))"
    2.43  apply (subst Suc_diff_eq_diff_pred)
    2.44  apply simp
    2.45 -apply (simp del: nat_numeral_1_eq_1)
    2.46 +apply (simp del: semiring_numeral_1_eq_1)
    2.47  apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
    2.48                          neg_number_of_pred_iff_0)
    2.49  done
    2.50 @@ -850,8 +849,8 @@
    2.51           if neg pv then nat_case a f n else f (nat pv + n))"
    2.52  apply (subst add_eq_if)
    2.53  apply (simp split add: nat.split
    2.54 -            del: nat_numeral_1_eq_1
    2.55 -            add: nat_numeral_1_eq_1 [symmetric]
    2.56 +            del: semiring_numeral_1_eq_1
    2.57 +            add: semiring_numeral_1_eq_1 [symmetric]
    2.58                   numeral_1_eq_Suc_0 [symmetric]
    2.59                   neg_number_of_pred_iff_0)
    2.60  done
    2.61 @@ -872,8 +871,8 @@
    2.62                     else f (nat pv + n) (nat_rec a f (nat pv + n)))"
    2.63  apply (subst add_eq_if)
    2.64  apply (simp split add: nat.split
    2.65 -            del: nat_numeral_1_eq_1
    2.66 -            add: nat_numeral_1_eq_1 [symmetric]
    2.67 +            del: semiring_numeral_1_eq_1
    2.68 +            add: semiring_numeral_1_eq_1 [symmetric]
    2.69                   numeral_1_eq_Suc_0 [symmetric]
    2.70                   neg_number_of_pred_iff_0)
    2.71  done
     3.1 --- a/src/HOL/Set.thy	Wed Dec 28 22:08:44 2011 +0100
     3.2 +++ b/src/HOL/Set.thy	Thu Dec 29 10:47:54 2011 +0100
     3.3 @@ -1804,7 +1804,7 @@
     3.4  hide_const (open) remove
     3.5  
     3.6  definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
     3.7 -  "project P A = {a \<in> A. P a}"
     3.8 +  [code_abbrev]: "project P A = {a \<in> A. P a}"
     3.9  
    3.10  hide_const (open) project
    3.11  
     4.1 --- a/src/HOL/Word/Word.thy	Wed Dec 28 22:08:44 2011 +0100
     4.2 +++ b/src/HOL/Word/Word.thy	Thu Dec 29 10:47:54 2011 +0100
     4.3 @@ -507,10 +507,12 @@
     4.4  
     4.5  lemmas td_sint = word_sint.td
     4.6  
     4.7 -lemma word_number_of_alt [code_unfold_post]:
     4.8 +lemma word_number_of_alt:
     4.9    "number_of b = word_of_int (number_of b)"
    4.10    by (simp add: number_of_eq word_number_of_def)
    4.11  
    4.12 +declare word_number_of_alt [symmetric, code_abbrev]
    4.13 +
    4.14  lemma word_no_wi: "number_of = word_of_int"
    4.15    by (auto simp: word_number_of_def)
    4.16  
     5.1 --- a/src/Tools/Code/code_preproc.ML	Wed Dec 28 22:08:44 2011 +0100
     5.2 +++ b/src/Tools/Code/code_preproc.ML	Thu Dec 29 10:47:54 2011 +0100
     5.3 @@ -88,13 +88,13 @@
     5.4  val add_post = map_post o Simplifier.add_simp;
     5.5  val del_post = map_post o Simplifier.del_simp;
     5.6  
     5.7 -fun add_unfold_post raw_thm thy =
     5.8 +fun add_code_abbrev raw_thm thy =
     5.9    let
    5.10      val thm = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy) raw_thm;
    5.11      val thm_sym = Thm.symmetric thm;
    5.12    in
    5.13      thy |> map_pre_post (fn (pre, post) =>
    5.14 -      (pre |> Simplifier.add_simp thm, post |> Simplifier.add_simp thm_sym))
    5.15 +      (pre |> Simplifier.add_simp thm_sym, post |> Simplifier.add_simp thm))
    5.16    end;
    5.17  
    5.18  fun add_functrans (name, f) = (map_data o apsnd)
    5.19 @@ -520,8 +520,8 @@
    5.20          "preprocessing equations for code generator"
    5.21      #> Attrib.setup @{binding code_post} (add_del_attribute_parser add_post del_post)
    5.22          "postprocessing equations for code generator"
    5.23 -    #> Attrib.setup @{binding code_unfold_post} (Scan.succeed (mk_attribute add_unfold_post))
    5.24 -        "pre- and postprocessing equations for code generator"
    5.25 +    #> Attrib.setup @{binding code_abbrev} (Scan.succeed (mk_attribute add_code_abbrev))
    5.26 +        "post- and preprocessing equations for code generator"
    5.27    end;
    5.28  
    5.29  val _ =