moved generic lemmas to appropriate places
authorhaftmann
Thu May 06 18:16:07 2010 +0200 (2010-05-06)
changeset 36716b09f3ad3208f
parent 36715 5f612b6d64a8
child 36717 2a72455be88b
moved generic lemmas to appropriate places
src/HOL/Groebner_Basis.thy
src/HOL/Int.thy
src/HOL/Nat_Numeral.thy
     1.1 --- a/src/HOL/Groebner_Basis.thy	Thu May 06 17:59:20 2010 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu May 06 18:16:07 2010 +0200
     1.3 @@ -162,16 +162,6 @@
     1.4  proof
     1.5  qed (simp_all add: algebra_simps)
     1.6  
     1.7 -lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
     1.8 -  by simp
     1.9 -
    1.10 -lemmas semiring_norm =
    1.11 -  Let_def arith_simps nat_arith rel_simps neg_simps if_False
    1.12 -  if_True add_0 add_Suc add_number_of_left mult_number_of_left
    1.13 -  numeral_1_eq_1[symmetric] Suc_eq_plus1
    1.14 -  numeral_0_eq_0[symmetric] numerals[symmetric]
    1.15 -  iszero_simps not_iszero_Numeral1
    1.16 -
    1.17  ML {*
    1.18  local
    1.19  
    1.20 @@ -589,6 +579,8 @@
    1.21  end
    1.22  *}
    1.23  
    1.24 +lemmas comp_arith = semiring_norm (*FIXME*)
    1.25 +
    1.26  
    1.27  subsection {* Groebner Bases *}
    1.28  
     2.1 --- a/src/HOL/Int.thy	Thu May 06 17:59:20 2010 +0200
     2.2 +++ b/src/HOL/Int.thy	Thu May 06 18:16:07 2010 +0200
     2.3 @@ -1063,20 +1063,24 @@
     2.4  
     2.5  text {* First version by Norbert Voelker *}
     2.6  
     2.7 -definition (*for simplifying equalities*)
     2.8 -  iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
     2.9 -where
    2.10 +definition (*for simplifying equalities*) iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool" where
    2.11    "iszero z \<longleftrightarrow> z = 0"
    2.12  
    2.13  lemma iszero_0: "iszero 0"
    2.14 -by (simp add: iszero_def)
    2.15 -
    2.16 -lemma not_iszero_1: "~ iszero 1"
    2.17 -by (simp add: iszero_def eq_commute)
    2.18 +  by (simp add: iszero_def)
    2.19 +
    2.20 +lemma iszero_Numeral0: "iszero (Numeral0 :: 'a::number_ring)"
    2.21 +  by (simp add: iszero_0)
    2.22 +
    2.23 +lemma not_iszero_1: "\<not> iszero 1"
    2.24 +  by (simp add: iszero_def)
    2.25 +
    2.26 +lemma not_iszero_Numeral1: "\<not> iszero (Numeral1 :: 'a::number_ring)"
    2.27 +  by (simp add: not_iszero_1)
    2.28  
    2.29  lemma eq_number_of_eq [simp]:
    2.30    "((number_of x::'a::number_ring) = number_of y) =
    2.31 -   iszero (number_of (x + uminus y) :: 'a)"
    2.32 +     iszero (number_of (x + uminus y) :: 'a)"
    2.33  unfolding iszero_def number_of_add number_of_minus
    2.34  by (simp add: algebra_simps)
    2.35  
     3.1 --- a/src/HOL/Nat_Numeral.thy	Thu May 06 17:59:20 2010 +0200
     3.2 +++ b/src/HOL/Nat_Numeral.thy	Thu May 06 18:16:07 2010 +0200
     3.3 @@ -694,6 +694,13 @@
     3.4    eq_nat_number_of
     3.5    less_nat_number_of
     3.6  
     3.7 +lemmas semiring_norm =
     3.8 +  Let_def arith_simps nat_arith rel_simps neg_simps if_False
     3.9 +  if_True add_0 add_Suc add_number_of_left mult_number_of_left
    3.10 +  numeral_1_eq_1 [symmetric] Suc_eq_plus1
    3.11 +  numeral_0_eq_0 [symmetric] numerals [symmetric]
    3.12 +  iszero_simps not_iszero_Numeral1
    3.13 +
    3.14  lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
    3.15    by (fact Let_def)
    3.16