moved some lemmas from Groebner_Basis here
authorhaftmann
Thu May 06 23:11:56 2010 +0200 (2010-05-06)
changeset 36719d396f6f63d94
parent 36718 30cdc863a4f8
child 36720 41da7025e59c
moved some lemmas from Groebner_Basis here
src/HOL/Fields.thy
src/HOL/Int.thy
src/HOL/Nat_Numeral.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Fields.thy	Thu May 06 19:35:43 2010 +0200
     1.2 +++ b/src/HOL/Fields.thy	Thu May 06 23:11:56 2010 +0200
     1.3 @@ -234,6 +234,18 @@
     1.4    "1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
     1.5    by (simp add: eq_commute [of 1])
     1.6  
     1.7 +lemma times_divide_times_eq:
     1.8 +  "(x / y) * (z / w) = (x * z) / (y * w)"
     1.9 +  by simp
    1.10 +
    1.11 +lemma add_frac_num:
    1.12 +  "y \<noteq> 0 \<Longrightarrow> x / y + z = (x + z * y) / y"
    1.13 +  by (simp add: add_divide_distrib)
    1.14 +
    1.15 +lemma add_num_frac:
    1.16 +  "y \<noteq> 0 \<Longrightarrow> z + x / y = (x + z * y) / y"
    1.17 +  by (simp add: add_divide_distrib add.commute)
    1.18 +
    1.19  end
    1.20  
    1.21  
     2.1 --- a/src/HOL/Int.thy	Thu May 06 19:35:43 2010 +0200
     2.2 +++ b/src/HOL/Int.thy	Thu May 06 23:11:56 2010 +0200
     2.3 @@ -2025,6 +2025,14 @@
     2.4  
     2.5  lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
     2.6  
     2.7 +lemma divide_Numeral1:
     2.8 +  "(x::'a::{field, number_ring}) / Numeral1 = x"
     2.9 +  by simp
    2.10 +
    2.11 +lemma divide_Numeral0:
    2.12 +  "(x::'a::{field_inverse_zero, number_ring}) / Numeral0 = 0"
    2.13 +  by simp
    2.14 +
    2.15  
    2.16  subsection {* The divides relation *}
    2.17  
     3.1 --- a/src/HOL/Nat_Numeral.thy	Thu May 06 19:35:43 2010 +0200
     3.2 +++ b/src/HOL/Nat_Numeral.thy	Thu May 06 23:11:56 2010 +0200
     3.3 @@ -319,6 +319,10 @@
     3.4  lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
     3.5  by (simp add: nat_number_of_def)
     3.6  
     3.7 +lemma Numeral1_eq1_nat:
     3.8 +  "(1::nat) = Numeral1"
     3.9 +  by simp
    3.10 +
    3.11  lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0"
    3.12  by (simp only: nat_numeral_1_eq_1 One_nat_def)
    3.13  
     4.1 --- a/src/HOL/Rings.thy	Thu May 06 19:35:43 2010 +0200
     4.2 +++ b/src/HOL/Rings.thy	Thu May 06 23:11:56 2010 +0200
     4.3 @@ -183,9 +183,21 @@
     4.4  
     4.5  end
     4.6  
     4.7 -
     4.8  class no_zero_divisors = zero + times +
     4.9    assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
    4.10 +begin
    4.11 +
    4.12 +lemma divisors_zero:
    4.13 +  assumes "a * b = 0"
    4.14 +  shows "a = 0 \<or> b = 0"
    4.15 +proof (rule classical)
    4.16 +  assume "\<not> (a = 0 \<or> b = 0)"
    4.17 +  then have "a \<noteq> 0" and "b \<noteq> 0" by auto
    4.18 +  with no_zero_divisors have "a * b \<noteq> 0" by blast
    4.19 +  with assms show ?thesis by simp
    4.20 +qed
    4.21 +
    4.22 +end
    4.23  
    4.24  class semiring_1_cancel = semiring + cancel_comm_monoid_add
    4.25    + zero_neq_one + monoid_mult