# HG changeset patch # User haftmann # Date 1325152074 -3600 # Node ID 83caa4f4bd5686fd33133f69a2fe02425902d43d # Parent 64a19ea435fc3ead864a327cba9c0d9af6bf6680 semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat diff -r 64a19ea435fc -r 83caa4f4bd56 src/HOL/Divides.thy --- 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 diff -r 64a19ea435fc -r 83caa4f4bd56 src/HOL/Nat_Numeral.thy --- 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 diff -r 64a19ea435fc -r 83caa4f4bd56 src/HOL/Set.thy --- 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 \ bool) \ 'a set \ 'a set" where - "project P A = {a \ A. P a}" + [code_abbrev]: "project P A = {a \ A. P a}" hide_const (open) project diff -r 64a19ea435fc -r 83caa4f4bd56 src/HOL/Word/Word.thy --- 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) diff -r 64a19ea435fc -r 83caa4f4bd56 src/Tools/Code/code_preproc.ML --- 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 _ =