diff -r 3bdb1eae352c -r a4f3db5d1393 src/HOL/NatBin.thy --- a/src/HOL/NatBin.thy Wed Dec 03 21:50:36 2008 -0800 +++ b/src/HOL/NatBin.thy Wed Dec 03 22:16:20 2008 -0800 @@ -441,13 +441,11 @@ text{*Simplification already does @{term "n<0"}, @{term "n\0"} and @{term "0\n"}.*} lemma eq_number_of_0 [simp]: - "(number_of v = (0::nat)) = - (if neg (number_of v :: int) then True else iszero (number_of v :: int))" -by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0) + "number_of v = (0::nat) \ number_of v \ (0::int)" + unfolding nat_number_of_def number_of_is_id by auto lemma eq_0_number_of [simp]: - "((0::nat) = number_of v) = - (if neg (number_of v :: int) then True else iszero (number_of v :: int))" + "(0::nat) = number_of v \ number_of v \ (0::int)" by (rule trans [OF eq_sym_conv eq_number_of_0]) lemma less_0_number_of [simp]: @@ -656,13 +654,9 @@ "number_of (Int.Bit1 w) = (if neg (number_of w :: int) then 0 else let n = number_of w in Suc (n + n))" - apply (simp only: nat_number_of_def Let_def split: split_if) - apply (intro conjI impI) - apply (simp add: neg_nat neg_number_of_Bit1) - apply (rule int_int_eq [THEN iffD1]) - apply (simp only: not_neg_nat neg_number_of_Bit1 int_Suc zadd_int [symmetric] simp_thms) - apply (simp only: number_of_Bit1 zadd_assoc) - done + unfolding nat_number_of_def number_of_Bit1 + unfolding number_of_is_id neg_def Let_def + by auto lemmas nat_number = nat_number_of_Pls nat_number_of_Min @@ -708,7 +702,8 @@ (if neg (number_of v :: int) then number_of v' + k else if neg (number_of v' :: int) then number_of v + k else number_of (v + v') + k)" -by simp + unfolding nat_number_of_def number_of_is_id neg_def + by auto lemma nat_number_of_mult_left: "number_of v * (number_of v' * (k::nat)) =