# HG changeset patch
# User haftmann
# Date 1273670835 -7200
# Node ID 112e613e8d0b100bdc309bdf1e0861322ac88374
# Parent  6520ba1256a6b1309be7fefdfa9aeb8c794cefeb
tuned proofs and fact and class names

diff -r 6520ba1256a6 -r 112e613e8d0b src/HOL/Semiring_Normalization.thy
--- 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