src/HOL/Presburger.thy
changeset 20485 3078fd2eec7b
parent 20217 25b068a99d2b
child 20595 db6bedfba498
     1.1 --- a/src/HOL/Presburger.thy	Wed Sep 06 10:01:27 2006 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Wed Sep 06 13:48:02 2006 +0200
     1.3 @@ -992,7 +992,8 @@
     1.4  lemma not_true_eq_false: "(~ True) = False" by simp
     1.5  
     1.6  
     1.7 -lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
     1.8 +lemma int_eq_number_of_eq:
     1.9 +  "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
    1.10    by simp
    1.11  lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" 
    1.12    by (simp only: iszero_number_of_Pls)
    1.13 @@ -1006,7 +1007,7 @@
    1.14  lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)" 
    1.15    by simp
    1.16  
    1.17 -lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
    1.18 +lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
    1.19    by simp
    1.20  
    1.21  lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))" 
    1.22 @@ -1018,18 +1019,20 @@
    1.23  lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
    1.24    by simp
    1.25  
    1.26 -lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
    1.27 +lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
    1.28    by simp
    1.29 -lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)"
    1.30 +lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
    1.31    by simp
    1.32  
    1.33 -lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))"
    1.34 +lemma int_number_of_diff_sym:
    1.35 +  "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
    1.36    by simp
    1.37  
    1.38 -lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)"
    1.39 +lemma int_number_of_mult_sym:
    1.40 +  "((number_of v)::int) * number_of w = number_of (v * w)"
    1.41    by simp
    1.42  
    1.43 -lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)"
    1.44 +lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
    1.45    by simp
    1.46  lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
    1.47    by simp