enable eq_bin_simps for simplifying equalities on numerals
authorhuffman
Wed Dec 03 21:50:36 2008 -0800 (2008-12-03)
changeset 289673bdb1eae352c
parent 28963 f6d9e0e0b153
child 28968 a4f3db5d1393
enable eq_bin_simps for simplifying equalities on numerals
src/HOL/Int.thy
src/HOL/Library/Float.thy
src/HOL/Presburger.thy
     1.1 --- a/src/HOL/Int.thy	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/HOL/Int.thy	Wed Dec 03 21:50:36 2008 -0800
     1.3 @@ -1307,10 +1307,15 @@
     1.4    "(number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y \<longleftrightarrow> x \<le> y"
     1.5    unfolding number_of_eq by (rule of_int_le_iff)
     1.6  
     1.7 +lemma eq_number_of [simp]:
     1.8 +  "(number_of x::'a::{ring_char_0,number_ring}) = number_of y \<longleftrightarrow> x = y"
     1.9 +  unfolding number_of_eq by (rule of_int_eq_iff)
    1.10 +
    1.11  lemmas rel_simps [simp] = 
    1.12    less_number_of less_bin_simps
    1.13    le_number_of le_bin_simps
    1.14 -  eq_number_of_eq iszero_0 nonzero_number_of_Min
    1.15 +  eq_number_of eq_bin_simps
    1.16 +  iszero_0 nonzero_number_of_Min
    1.17    iszero_number_of_Bit0 iszero_number_of_Bit1
    1.18    not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
    1.19    neg_number_of_Min neg_number_of_Bit0 neg_number_of_Bit1
     2.1 --- a/src/HOL/Library/Float.thy	Wed Dec 03 21:00:39 2008 -0800
     2.2 +++ b/src/HOL/Library/Float.thy	Wed Dec 03 21:50:36 2008 -0800
     2.3 @@ -499,7 +499,7 @@
     2.4  
     2.5  lemma int_eq_number_of_eq:
     2.6    "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)"
     2.7 -  by simp
     2.8 +  by (rule eq_number_of_eq)
     2.9  
    2.10  lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
    2.11    by (simp only: iszero_number_of_Pls)
    2.12 @@ -514,7 +514,7 @@
    2.13    by simp
    2.14  
    2.15  lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
    2.16 -  unfolding neg_def number_of_is_id by simp
    2.17 +  by (rule less_number_of_eq_neg)
    2.18  
    2.19  lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
    2.20    by simp
     3.1 --- a/src/HOL/Presburger.thy	Wed Dec 03 21:00:39 2008 -0800
     3.2 +++ b/src/HOL/Presburger.thy	Wed Dec 03 21:50:36 2008 -0800
     3.3 @@ -411,7 +411,7 @@
     3.4    by (simp cong: conj_cong)
     3.5  lemma int_eq_number_of_eq:
     3.6    "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
     3.7 -  by simp
     3.8 +  by (rule eq_number_of_eq)
     3.9  
    3.10  lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m"
    3.11  unfolding dvd_eq_mod_eq_0[symmetric] ..