--- a/src/HOL/Arith_Tools.thy Mon Mar 17 22:34:27 2008 +0100
+++ b/src/HOL/Arith_Tools.thy Tue Mar 18 20:33:28 2008 +0100
@@ -327,24 +327,12 @@
text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
-lemmas le_divide_eq_number_of = le_divide_eq [of _ _ "number_of w", standard]
-declare le_divide_eq_number_of [simp]
-
-lemmas divide_le_eq_number_of = divide_le_eq [of _ "number_of w", standard]
-declare divide_le_eq_number_of [simp]
-
-lemmas less_divide_eq_number_of = less_divide_eq [of _ _ "number_of w", standard]
-declare less_divide_eq_number_of [simp]
-
-lemmas divide_less_eq_number_of = divide_less_eq [of _ "number_of w", standard]
-declare divide_less_eq_number_of [simp]
-
-lemmas eq_divide_eq_number_of = eq_divide_eq [of _ _ "number_of w", standard]
-declare eq_divide_eq_number_of [simp]
-
-lemmas divide_eq_eq_number_of = divide_eq_eq [of _ "number_of w", standard]
-declare divide_eq_eq_number_of [simp]
-
+lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
+lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
+lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
+lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
+lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
+lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
subsubsection{*Optional Simplification Rules Involving Constants*}
@@ -600,7 +588,7 @@
in
val field_comp_conv = comp_conv;
val fieldgb_declaration =
- NormalizerData.funs @{thm class_fieldgb.axioms}
+ NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms}
{is_const = K numeral_is_const,
dest_const = K dest_const,
mk_const = mk_const,
--- a/src/HOL/Groebner_Basis.thy Mon Mar 17 22:34:27 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy Tue Mar 18 20:33:28 2008 +0100
@@ -159,10 +159,10 @@
qed
-lemma "axioms" [normalizer
+lemmas gb_semiring_axioms =
+ gb_semiring_axioms [normalizer
semiring ops: semiring_ops
- semiring rules: semiring_rules]:
- "gb_semiring add mul pwr r0 r1" by (rule gb_semiring_axioms)
+ semiring rules: semiring_rules]
end
@@ -216,7 +216,7 @@
end
*}
-declaration {* normalizer_funs @{thm class_semiring.axioms} *}
+declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms} *}
locale gb_ring = gb_semiring +
@@ -232,12 +232,12 @@
lemmas ring_rules = neg_mul sub_add
-lemma "axioms" [normalizer
- semiring ops: semiring_ops
- semiring rules: semiring_rules
- ring ops: ring_ops
- ring rules: ring_rules]:
- "gb_ring add mul pwr r0 r1 sub neg" by (rule gb_ring_axioms)
+lemmas gb_ring_axioms =
+ gb_ring_axioms [normalizer
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules
+ ring ops: ring_ops
+ ring rules: ring_rules]
end
@@ -247,7 +247,7 @@
by unfold_locales simp_all
-declaration {* normalizer_funs @{thm class_ring.axioms} *}
+declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms} *}
use "Tools/Groebner_Basis/normalizer.ML"
@@ -263,12 +263,12 @@
and inverse: "inverse x = divide r1 x"
begin
-lemma "axioms" [normalizer
- semiring ops: semiring_ops
- semiring rules: semiring_rules
- ring ops: ring_ops
- ring rules: ring_rules]:
- "gb_field add mul pwr r0 r1 sub neg divide inverse" by (rule gb_field_axioms)
+lemmas gb_field_axioms =
+ gb_field_axioms [normalizer
+ semiring ops: semiring_ops
+ semiring rules: semiring_rules
+ ring ops: ring_ops
+ ring rules: ring_rules]
end
@@ -307,13 +307,12 @@
thus "x = add x a \<longleftrightarrow> a = r0" by (auto simp add: add_c add_0)
qed
-declare "axioms" [normalizer del]
+declare gb_semiring_axioms [normalizer del]
-lemma "axioms" [normalizer
+lemmas semiringb_axioms = semiringb_axioms [normalizer
semiring ops: semiring_ops
semiring rules: semiring_rules
- idom rules: noteq_reduce add_scale_eq_noteq]:
- "semiringb add mul pwr r0 r1" by (rule semiringb_axioms)
+ idom rules: noteq_reduce add_scale_eq_noteq]
end
@@ -321,16 +320,15 @@
assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y"
begin
-declare "axioms" [normalizer del]
+declare gb_ring_axioms [normalizer del]
-lemma "axioms" [normalizer
+lemmas ringb_axioms = ringb_axioms [normalizer
semiring ops: semiring_ops
semiring rules: semiring_rules
ring ops: ring_ops
ring rules: ring_rules
idom rules: noteq_reduce add_scale_eq_noteq
- ideal rules: subr0_iff add_r0_iff]:
- "ringb add mul pwr r0 r1 sub neg" by (rule ringb_axioms)
+ ideal rules: subr0_iff add_r0_iff]
end
@@ -358,7 +356,7 @@
thus "w = x" by simp
qed
-declaration {* normalizer_funs @{thm class_ringb.axioms} *}
+declaration {* normalizer_funs @{thm class_ringb.ringb_axioms} *}
interpretation natgb: semiringb
["op +" "op *" "op ^" "0::nat" "1"]
@@ -382,21 +380,21 @@
thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
qed
-declaration {* normalizer_funs @{thm natgb.axioms} *}
+declaration {* normalizer_funs @{thm natgb.semiringb_axioms} *}
locale fieldgb = ringb + gb_field
begin
-declare "axioms" [normalizer del]
+declare gb_field_axioms [normalizer del]
-lemma "axioms" [normalizer
+lemmas fieldgb_axioms = fieldgb_axioms [normalizer
semiring ops: semiring_ops
semiring rules: semiring_rules
ring ops: ring_ops
ring rules: ring_rules
idom rules: noteq_reduce add_scale_eq_noteq
- ideal rules: subr0_iff add_r0_iff]:
- "fieldgb add mul pwr r0 r1 sub neg divide inverse" by unfold_locales
+ ideal rules: subr0_iff add_r0_iff]
+
end