# HG changeset patch
# User haftmann
# Date 1205565075 -3600
# Node ID 2bdb61a28971a08769d00f683d094c3dd634abb0
# Parent  6c4d534af98d7f8cf9a3733a977c7f8b3a9e1090
continued localization

diff -r 6c4d534af98d -r 2bdb61a28971 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Mar 14 19:58:01 2008 +0100
+++ b/src/HOL/Ring_and_Field.thy	Sat Mar 15 08:11:15 2008 +0100
@@ -240,6 +240,25 @@
 end
 
 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
+begin
+
+lemma mult_cancel_right1 [simp]:
+  "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
+  by (insert mult_cancel_right [of 1 c b], force)
+
+lemma mult_cancel_right2 [simp]:
+  "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
+  by (insert mult_cancel_right [of a c 1], simp)
+ 
+lemma mult_cancel_left1 [simp]:
+  "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
+  by (insert mult_cancel_left [of c 1 b], force)
+
+lemma mult_cancel_left2 [simp]:
+  "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1"
+  by (insert mult_cancel_left [of c a 1], simp)
+
+end
 
 class idom = comm_ring_1 + no_zero_divisors
 begin
@@ -271,6 +290,95 @@
   qed
 qed
 
+lemma nonzero_imp_inverse_nonzero:
+  "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"
+proof
+  assume ianz: "inverse a = 0"
+  assume "a \<noteq> 0"
+  hence "1 = a * inverse a" by simp
+  also have "... = 0" by (simp add: ianz)
+  finally have "1 = 0" .
+  thus False by (simp add: eq_commute)
+qed
+
+lemma inverse_zero_imp_zero:
+  "inverse a = 0 \<Longrightarrow> a = 0"
+apply (rule classical)
+apply (drule nonzero_imp_inverse_nonzero)
+apply auto
+done
+
+lemma nonzero_inverse_minus_eq:
+  assumes "a \<noteq> 0"
+  shows "inverse (- a) = - inverse a"
+proof -
+  have "- a * inverse (- a) = - a * - inverse a"
+    using assms by simp
+  then show ?thesis unfolding mult_cancel_left using assms by simp 
+qed
+
+lemma nonzero_inverse_inverse_eq:
+  assumes "a \<noteq> 0"
+  shows "inverse (inverse a) = a"
+proof -
+  have "(inverse (inverse a) * inverse a) * a = a" 
+    using assms by (simp add: nonzero_imp_inverse_nonzero)
+  then show ?thesis using assms by (simp add: mult_assoc)
+qed
+
+lemma nonzero_inverse_eq_imp_eq:
+  assumes inveq: "inverse a = inverse b"
+    and anz:  "a \<noteq> 0"
+    and bnz:  "b \<noteq> 0"
+  shows "a = b"
+proof -
+  have "a * inverse b = a * inverse a"
+    by (simp add: inveq)
+  hence "(a * inverse b) * b = (a * inverse a) * b"
+    by simp
+  then show "a = b"
+    by (simp add: mult_assoc anz bnz)
+qed
+
+lemma inverse_1 [simp]: "inverse 1 = 1"
+proof -
+  have "inverse 1 * 1 = 1" 
+    by (rule left_inverse) (rule one_neq_zero)
+  then show ?thesis by simp
+qed
+
+lemma inverse_unique: 
+  assumes ab: "a * b = 1"
+  shows "inverse a = b"
+proof -
+  have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
+  moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) 
+  ultimately show ?thesis by (simp add: mult_assoc [symmetric]) 
+qed
+
+lemma nonzero_inverse_mult_distrib: 
+  assumes anz: "a \<noteq> 0"
+    and bnz: "b \<noteq> 0"
+  shows "inverse (a * b) = inverse b * inverse a"
+proof -
+  have "inverse (a * b) * (a * b) * inverse b = inverse b" 
+    by (simp add: anz bnz)
+  hence "inverse (a * b) * a = inverse b" 
+    by (simp add: mult_assoc bnz)
+  hence "inverse (a * b) * a * inverse a = inverse b * inverse a" 
+    by simp
+  thus ?thesis
+    by (simp add: mult_assoc anz)
+qed
+
+lemma division_ring_inverse_add:
+  "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"
+  by (simp add: ring_simps mult_assoc)
+
+lemma division_ring_inverse_diff:
+  "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
+  by (simp add: ring_simps mult_assoc)
+
 end
 
 class field = comm_ring_1 + inverse +
@@ -831,80 +939,46 @@
   assumes "x \<noteq> y" obtains "x < y" | "y < x"
   using assms by (rule neqE)
 
+text {* These cancellation simprules also produce two cases when the comparison is a goal. *}
+
+lemma mult_le_cancel_right1:
+  "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
+  by (insert mult_le_cancel_right [of 1 c b], simp)
+
+lemma mult_le_cancel_right2:
+  "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
+  by (insert mult_le_cancel_right [of a c 1], simp)
+
+lemma mult_le_cancel_left1:
+  "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)"
+  by (insert mult_le_cancel_left [of c 1 b], simp)
+
+lemma mult_le_cancel_left2:
+  "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)"
+  by (insert mult_le_cancel_left [of c a 1], simp)
+
+lemma mult_less_cancel_right1:
+  "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
+  by (insert mult_less_cancel_right [of 1 c b], simp)
+
+lemma mult_less_cancel_right2:
+  "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
+  by (insert mult_less_cancel_right [of a c 1], simp)
+
+lemma mult_less_cancel_left1:
+  "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)"
+  by (insert mult_less_cancel_left [of c 1 b], simp)
+
+lemma mult_less_cancel_left2:
+  "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)"
+  by (insert mult_less_cancel_left [of c a 1], simp)
+
 end
 
 class ordered_field = field + ordered_idom
 
-text{*All three types of comparision involving 0 and 1 are covered.*}
-
--- {* FIXME continue localization here *}
-
-subsubsection{*Special Cancellation Simprules for Multiplication*}
-
-text{*These also produce two cases when the comparison is a goal.*}
-
-lemma mult_le_cancel_right1:
-  fixes c :: "'a :: ordered_idom"
-  shows "(c \<le> b*c) = ((0<c --> 1\<le>b) & (c<0 --> b \<le> 1))"
-by (insert mult_le_cancel_right [of 1 c b], simp)
-
-lemma mult_le_cancel_right2:
-  fixes c :: "'a :: ordered_idom"
-  shows "(a*c \<le> c) = ((0<c --> a\<le>1) & (c<0 --> 1 \<le> a))"
-by (insert mult_le_cancel_right [of a c 1], simp)
-
-lemma mult_le_cancel_left1:
-  fixes c :: "'a :: ordered_idom"
-  shows "(c \<le> c*b) = ((0<c --> 1\<le>b) & (c<0 --> b \<le> 1))"
-by (insert mult_le_cancel_left [of c 1 b], simp)
-
-lemma mult_le_cancel_left2:
-  fixes c :: "'a :: ordered_idom"
-  shows "(c*a \<le> c) = ((0<c --> a\<le>1) & (c<0 --> 1 \<le> a))"
-by (insert mult_le_cancel_left [of c a 1], simp)
-
-lemma mult_less_cancel_right1:
-  fixes c :: "'a :: ordered_idom"
-  shows "(c < b*c) = ((0 \<le> c --> 1<b) & (c \<le> 0 --> b < 1))"
-by (insert mult_less_cancel_right [of 1 c b], simp)
+text {* Simprules for comparisons where common factors can be cancelled. *}
 
-lemma mult_less_cancel_right2:
-  fixes c :: "'a :: ordered_idom"
-  shows "(a*c < c) = ((0 \<le> c --> a<1) & (c \<le> 0 --> 1 < a))"
-by (insert mult_less_cancel_right [of a c 1], simp)
-
-lemma mult_less_cancel_left1:
-  fixes c :: "'a :: ordered_idom"
-  shows "(c < c*b) = ((0 \<le> c --> 1<b) & (c \<le> 0 --> b < 1))"
-by (insert mult_less_cancel_left [of c 1 b], simp)
-
-lemma mult_less_cancel_left2:
-  fixes c :: "'a :: ordered_idom"
-  shows "(c*a < c) = ((0 \<le> c --> a<1) & (c \<le> 0 --> 1 < a))"
-by (insert mult_less_cancel_left [of c a 1], simp)
-
-lemma mult_cancel_right1 [simp]:
-  fixes c :: "'a :: ring_1_no_zero_divisors"
-  shows "(c = b*c) = (c = 0 | b=1)"
-by (insert mult_cancel_right [of 1 c b], force)
-
-lemma mult_cancel_right2 [simp]:
-  fixes c :: "'a :: ring_1_no_zero_divisors"
-  shows "(a*c = c) = (c = 0 | a=1)"
-by (insert mult_cancel_right [of a c 1], simp)
- 
-lemma mult_cancel_left1 [simp]:
-  fixes c :: "'a :: ring_1_no_zero_divisors"
-  shows "(c = c*b) = (c = 0 | b=1)"
-by (insert mult_cancel_left [of c 1 b], force)
-
-lemma mult_cancel_left2 [simp]:
-  fixes c :: "'a :: ring_1_no_zero_divisors"
-  shows "(c*a = c) = (c = 0 | a=1)"
-by (insert mult_cancel_left [of c a 1], simp)
-
-
-text{*Simprules for comparisons where common factors can be cancelled.*}
 lemmas mult_compare_simps =
     mult_le_cancel_right mult_le_cancel_left
     mult_le_cancel_right1 mult_le_cancel_right2
@@ -916,73 +990,11 @@
     mult_cancel_right1 mult_cancel_right2
     mult_cancel_left1 mult_cancel_left2
 
-
-(* what ordering?? this is a straight instance of mult_eq_0_iff
-text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
-      of an ordering.*}
-lemma field_mult_eq_0_iff [simp]:
-  "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)"
-by simp
-*)
-(* subsumed by mult_cancel lemmas on ring_no_zero_divisors
-text{*Cancellation of equalities with a common factor*}
-lemma field_mult_cancel_right_lemma:
-      assumes cnz: "c \<noteq> (0::'a::division_ring)"
-         and eq:  "a*c = b*c"
-        shows "a=b"
-proof -
-  have "(a * c) * inverse c = (b * c) * inverse c"
-    by (simp add: eq)
-  thus "a=b"
-    by (simp add: mult_assoc cnz)
-qed
-
-lemma field_mult_cancel_right [simp]:
-     "(a*c = b*c) = (c = (0::'a::division_ring) | a=b)"
-by simp
-
-lemma field_mult_cancel_left [simp]:
-     "(c*a = c*b) = (c = (0::'a::division_ring) | a=b)"
-by simp
-*)
-lemma nonzero_imp_inverse_nonzero:
-  "a \<noteq> 0 ==> inverse a \<noteq> (0::'a::division_ring)"
-proof
-  assume ianz: "inverse a = 0"
-  assume "a \<noteq> 0"
-  hence "1 = a * inverse a" by simp
-  also have "... = 0" by (simp add: ianz)
-  finally have "1 = (0::'a::division_ring)" .
-  thus False by (simp add: eq_commute)
-qed
-
-
-subsection{*Basic Properties of @{term inverse}*}
-
-lemma inverse_zero_imp_zero: "inverse a = 0 ==> a = (0::'a::division_ring)"
-apply (rule ccontr) 
-apply (blast dest: nonzero_imp_inverse_nonzero) 
-done
-
-lemma inverse_nonzero_imp_nonzero:
-   "inverse a = 0 ==> a = (0::'a::division_ring)"
-apply (rule ccontr) 
-apply (blast dest: nonzero_imp_inverse_nonzero) 
-done
+-- {* FIXME continue localization here *}
 
 lemma inverse_nonzero_iff_nonzero [simp]:
    "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))"
-by (force dest: inverse_nonzero_imp_nonzero) 
-
-lemma nonzero_inverse_minus_eq:
-      assumes [simp]: "a\<noteq>0"
-      shows "inverse(-a) = -inverse(a::'a::division_ring)"
-proof -
-  have "-a * inverse (- a) = -a * - inverse a"
-    by simp
-  thus ?thesis 
-    by (simp only: mult_cancel_left, simp)
-qed
+by (force dest: inverse_zero_imp_zero) 
 
 lemma inverse_minus_eq [simp]:
    "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"
@@ -993,20 +1005,6 @@
   thus ?thesis by (simp add: nonzero_inverse_minus_eq)
 qed
 
-lemma nonzero_inverse_eq_imp_eq:
-      assumes inveq: "inverse a = inverse b"
-	  and anz:  "a \<noteq> 0"
-	  and bnz:  "b \<noteq> 0"
-	 shows "a = (b::'a::division_ring)"
-proof -
-  have "a * inverse b = a * inverse a"
-    by (simp add: inveq)
-  hence "(a * inverse b) * b = (a * inverse a) * b"
-    by simp
-  thus "a = b"
-    by (simp add: mult_assoc anz bnz)
-qed
-
 lemma inverse_eq_imp_eq:
   "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})"
 apply (cases "a=0 | b=0") 
@@ -1019,16 +1017,6 @@
   "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))"
 by (force dest!: inverse_eq_imp_eq)
 
-lemma nonzero_inverse_inverse_eq:
-      assumes [simp]: "a \<noteq> 0"
-      shows "inverse(inverse (a::'a::division_ring)) = a"
-  proof -
-  have "(inverse (inverse a) * inverse a) * a = a" 
-    by (simp add: nonzero_imp_inverse_nonzero)
-  thus ?thesis
-    by (simp add: mult_assoc)
-  qed
-
 lemma inverse_inverse_eq [simp]:
      "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a"
   proof cases
@@ -1038,37 +1026,6 @@
     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
   qed
 
-lemma inverse_1 [simp]: "inverse 1 = (1::'a::division_ring)"
-  proof -
-  have "inverse 1 * 1 = (1::'a::division_ring)" 
-    by (rule left_inverse [OF zero_neq_one [symmetric]])
-  thus ?thesis  by simp
-  qed
-
-lemma inverse_unique: 
-  assumes ab: "a*b = 1"
-  shows "inverse a = (b::'a::division_ring)"
-proof -
-  have "a \<noteq> 0" using ab by auto
-  moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) 
-  ultimately show ?thesis by (simp add: mult_assoc [symmetric]) 
-qed
-
-lemma nonzero_inverse_mult_distrib: 
-      assumes anz: "a \<noteq> 0"
-          and bnz: "b \<noteq> 0"
-      shows "inverse(a*b) = inverse(b) * inverse(a::'a::division_ring)"
-  proof -
-  have "inverse(a*b) * (a * b) * inverse(b) = inverse(b)" 
-    by (simp add: anz bnz)
-  hence "inverse(a*b) * a = inverse(b)" 
-    by (simp add: mult_assoc bnz)
-  hence "inverse(a*b) * a * inverse(a) = inverse(b) * inverse(a)" 
-    by simp
-  thus ?thesis
-    by (simp add: mult_assoc anz)
-  qed
-
 text{*This version builds in division by zero while also re-orienting
       the right-hand side.*}
 lemma inverse_mult_distrib [simp]:
@@ -1083,16 +1040,6 @@
       by force
   qed
 
-lemma division_ring_inverse_add:
-  "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]
-   ==> inverse a + inverse b = inverse a * (a+b) * inverse b"
-by (simp add: ring_simps)
-
-lemma division_ring_inverse_diff:
-  "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]
-   ==> inverse a - inverse b = inverse a * (b-a) * inverse b"
-by (simp add: ring_simps)
-
 text{*There is no slick version using division by zero.*}
 lemma inverse_add:
   "[|a \<noteq> 0;  b \<noteq> 0|]