--- 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
--- 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 *}
--- 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)
--- 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