# HG changeset patch
# User haftmann
# Date 1273180316 -7200
# Node ID d396f6f63d94339625cfea1708e678a0d3d2f8d3
# Parent  30cdc863a4f80b9b798f032b9b4441c489df403a
moved some lemmas from Groebner_Basis here

diff -r 30cdc863a4f8 -r d396f6f63d94 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Thu May 06 19:35:43 2010 +0200
+++ b/src/HOL/Fields.thy	Thu May 06 23:11:56 2010 +0200
@@ -234,6 +234,18 @@
   "1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
   by (simp add: eq_commute [of 1])
 
+lemma times_divide_times_eq:
+  "(x / y) * (z / w) = (x * z) / (y * w)"
+  by simp
+
+lemma add_frac_num:
+  "y \<noteq> 0 \<Longrightarrow> x / y + z = (x + z * y) / y"
+  by (simp add: add_divide_distrib)
+
+lemma add_num_frac:
+  "y \<noteq> 0 \<Longrightarrow> z + x / y = (x + z * y) / y"
+  by (simp add: add_divide_distrib add.commute)
+
 end
 
 
diff -r 30cdc863a4f8 -r d396f6f63d94 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu May 06 19:35:43 2010 +0200
+++ b/src/HOL/Int.thy	Thu May 06 23:11:56 2010 +0200
@@ -2025,6 +2025,14 @@
 
 lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
 
+lemma divide_Numeral1:
+  "(x::'a::{field, number_ring}) / Numeral1 = x"
+  by simp
+
+lemma divide_Numeral0:
+  "(x::'a::{field_inverse_zero, number_ring}) / Numeral0 = 0"
+  by simp
+
 
 subsection {* The divides relation *}
 
diff -r 30cdc863a4f8 -r d396f6f63d94 src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Thu May 06 19:35:43 2010 +0200
+++ b/src/HOL/Nat_Numeral.thy	Thu May 06 23:11:56 2010 +0200
@@ -319,6 +319,10 @@
 lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
 by (simp add: nat_number_of_def)
 
+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)
 
diff -r 30cdc863a4f8 -r d396f6f63d94 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Thu May 06 19:35:43 2010 +0200
+++ b/src/HOL/Rings.thy	Thu May 06 23:11:56 2010 +0200
@@ -183,9 +183,21 @@
 
 end
 
-
 class no_zero_divisors = zero + times +
   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
+begin
+
+lemma divisors_zero:
+  assumes "a * b = 0"
+  shows "a = 0 \<or> b = 0"
+proof (rule classical)
+  assume "\<not> (a = 0 \<or> b = 0)"
+  then have "a \<noteq> 0" and "b \<noteq> 0" by auto
+  with no_zero_divisors have "a * b \<noteq> 0" by blast
+  with assms show ?thesis by simp
+qed
+
+end
 
 class semiring_1_cancel = semiring + cancel_comm_monoid_add
   + zero_neq_one + monoid_mult