--- a/src/HOL/Semiring_Normalization.thy Wed May 12 13:51:22 2010 +0200
+++ b/src/HOL/Semiring_Normalization.thy Wed May 12 15:27:15 2010 +0200
@@ -10,12 +10,33 @@
"Tools/semiring_normalizer.ML"
begin
-text {* FIXME prelude *}
+text {* Prelude *}
+
+class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel +
+ assumes crossproduct_eq: "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
+begin
+
+lemma crossproduct_noteq:
+ "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> a * c + b * d \<noteq> a * d + b * c"
+ by (simp add: crossproduct_eq)
-class comm_semiring_1_cancel_norm (*FIXME name*) = comm_semiring_1_cancel +
- assumes add_mult_solve: "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
+lemma add_scale_eq_noteq:
+ "r \<noteq> 0 \<Longrightarrow> a = b \<and> c \<noteq> d \<Longrightarrow> a + r * c \<noteq> b + r * d"
+proof (rule notI)
+ assume nz: "r\<noteq> 0" and cnd: "a = b \<and> c\<noteq>d"
+ and eq: "a + (r * c) = b + (r * d)"
+ have "(0 * d) + (r * c) = (0 * c) + (r * d)"
+ using add_imp_eq eq mult_zero_left by (simp add: cnd)
+ then show False using crossproduct_eq [of 0 d] nz cnd by simp
+qed
-sublocale idom < comm_semiring_1_cancel_norm
+lemma add_0_iff:
+ "b = b + a \<longleftrightarrow> a = 0"
+ using add_imp_eq [of b a 0] by auto
+
+end
+
+sublocale idom < comm_semiring_1_cancel_crossproduct
proof
fix w x y z
show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
@@ -29,28 +50,24 @@
qed (auto simp add: add_ac)
qed
-instance nat :: comm_semiring_1_cancel_norm
+instance nat :: comm_semiring_1_cancel_crossproduct
proof
fix w x y z :: nat
- { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
- hence "y < z \<or> y > z" by arith
- moreover {
- assume lt:"y <z" hence "\<exists>k. z = y + k \<and> k > 0" by (rule_tac x="z - y" in exI, auto)
- then obtain k where kp: "k>0" and yz:"z = y + k" by blast
- from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz algebra_simps)
- hence "x*k = w*k" by simp
- hence "w = x" using kp by simp }
- moreover {
- assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto)
- then obtain k where kp: "k>0" and yz:"y = z + k" by blast
- from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz algebra_simps)
- hence "w*k = x*k" by simp
- hence "w = x" using kp by simp }
- ultimately have "w=x" by blast }
- then show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" by auto
+ have aux: "\<And>y z. y < z \<Longrightarrow> w * y + x * z = w * z + x * y \<Longrightarrow> w = x"
+ proof -
+ fix y z :: nat
+ assume "y < z" then have "\<exists>k. z = y + k \<and> k \<noteq> 0" by (intro exI [of _ "z - y"]) auto
+ then obtain k where "z = y + k" and "k \<noteq> 0" by blast
+ assume "w * y + x * z = w * z + x * y"
+ then have "(w * y + x * y) + x * k = (w * y + x * y) + w * k" by (simp add: `z = y + k` algebra_simps)
+ then have "x * k = w * k" by simp
+ then show "w = x" using `k \<noteq> 0` by simp
+ qed
+ show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
+ by (auto simp add: neq_iff dest!: aux)
qed
-text {* semiring normalization proper *}
+text {* Semiring normalization proper *}
setup Semiring_Normalizer.setup
@@ -133,39 +150,21 @@
end
-context comm_semiring_1_cancel_norm
+context comm_semiring_1_cancel_crossproduct
begin
-lemma noteq_reduce:
- "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> a * c + b * d \<noteq> a * d + b * c"
- by (simp add: add_mult_solve)
-
-lemma add_scale_eq_noteq:
- "r \<noteq> 0 \<Longrightarrow> a = b \<and> c \<noteq> d \<Longrightarrow> a + r * c \<noteq> b + r * d"
-proof (rule notI)
- assume nz: "r\<noteq> 0" and cnd: "a = b \<and> c\<noteq>d"
- and eq: "a + (r * c) = b + (r * d)"
- have "(0 * d) + (r * c) = (0 * c) + (r * d)"
- using add_imp_eq eq mult_zero_left by (simp add: cnd)
- then show False using add_mult_solve [of 0 d] nz cnd by simp
-qed
-
-lemma add_0_iff:
- "x = x + a \<longleftrightarrow> a = 0"
- using add_imp_eq [of x a 0] by auto
-
declare
normalizing_comm_semiring_1_axioms [normalizer del]
lemmas
- normalizing_comm_semiring_1_cancel_norm_axioms =
- comm_semiring_1_cancel_norm_axioms [normalizer
+ normalizing_comm_semiring_1_cancel_crossproduct_axioms =
+ comm_semiring_1_cancel_crossproduct_axioms [normalizer
semiring ops: normalizing_semiring_ops
semiring rules: normalizing_semiring_rules
- idom rules: noteq_reduce add_scale_eq_noteq]
+ idom rules: crossproduct_noteq add_scale_eq_noteq]
declaration
- {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_cancel_norm_axioms} *}
+ {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_cancel_crossproduct_axioms} *}
end
@@ -179,7 +178,7 @@
semiring rules: normalizing_semiring_rules
ring ops: normalizing_ring_ops
ring rules: normalizing_ring_rules
- idom rules: noteq_reduce add_scale_eq_noteq
+ idom rules: crossproduct_noteq add_scale_eq_noteq
ideal rules: right_minus_eq add_0_iff]
declaration
@@ -203,7 +202,7 @@
ring rules: normalizing_ring_rules
field ops: normalizing_field_ops
field rules: normalizing_field_rules
- idom rules: noteq_reduce add_scale_eq_noteq
+ idom rules: crossproduct_noteq add_scale_eq_noteq
ideal rules: right_minus_eq add_0_iff]
declaration
@@ -212,13 +211,11 @@
end
hide_fact (open) normalizing_comm_semiring_1_axioms
- normalizing_comm_semiring_1_cancel_norm_axioms normalizing_semiring_ops normalizing_semiring_rules
+ normalizing_comm_semiring_1_cancel_crossproduct_axioms normalizing_semiring_ops normalizing_semiring_rules
hide_fact (open) normalizing_comm_ring_1_axioms
normalizing_idom_axioms normalizing_ring_ops normalizing_ring_rules
hide_fact (open) normalizing_field_axioms normalizing_field_ops normalizing_field_rules
-hide_fact (open) add_scale_eq_noteq noteq_reduce
-
end