merged

--- a/src/HOL/Library/Bit.thy	Thu Feb 26 17:42:43 2009 +0100
+++ b/src/HOL/Library/Bit.thy	Thu Feb 26 08:48:33 2009 -0800
@@ -79,14 +79,8 @@
 
 end
 
-lemma bit_1_plus_1 [simp]: "1 + 1 = (0 :: bit)"
-  unfolding plus_bit_def by simp
-
-lemma bit_add_self [simp]: "x + x = (0 :: bit)"
-  by (cases x) simp_all
-
-lemma bit_add_self_left [simp]: "x + (x + y) = (y :: bit)"
-  by simp
+lemma bit_add_self: "x + x = (0 :: bit)"
+  unfolding plus_bit_def by (simp split: bit.split)
 
 lemma bit_mult_eq_1_iff [simp]: "x * y = (1 :: bit) \<longleftrightarrow> x = 1 \<and> y = 1"
   unfolding times_bit_def by (simp split: bit.split)

--- a/src/HOL/List.thy	Thu Feb 26 17:42:43 2009 +0100
+++ b/src/HOL/List.thy	Thu Feb 26 08:48:33 2009 -0800
@@ -1438,10 +1438,10 @@
 apply (auto split:nat.split)
 done
 
-lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - Suc 0)"
+lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
 by(induct xs)(auto simp:neq_Nil_conv)
 
-lemma butlast_conv_take: "butlast xs = take (length xs - Suc 0) xs"
+lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
 by (induct xs, simp, case_tac xs, simp_all)
 
 
@@ -1461,6 +1461,12 @@
 
 declare take_Cons [simp del] and drop_Cons [simp del]
 
+lemma take_1_Cons [simp]: "take 1 (x # xs) = [x]"
+  unfolding One_nat_def by simp
+
+lemma drop_1_Cons [simp]: "drop 1 (x # xs) = xs"
+  unfolding One_nat_def by simp
+
 lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"
 by(clarsimp simp add:neq_Nil_conv)
 
@@ -1588,17 +1594,17 @@
 done
 
 lemma butlast_take:
-  "n <= length xs ==> butlast (take n xs) = take (n - Suc 0) xs"
+  "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
 by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
 
 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
-by (simp add: butlast_conv_take drop_take)
+by (simp add: butlast_conv_take drop_take add_ac)
 
 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
 by (simp add: butlast_conv_take min_max.inf_absorb1)
 
 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
-by (simp add: butlast_conv_take drop_take)
+by (simp add: butlast_conv_take drop_take add_ac)
 
 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
 by(simp add: hd_conv_nth)
@@ -2458,7 +2464,7 @@
 done
 
 lemma length_remove1:
-  "length(remove1 x xs) = (if x : set xs then length xs - Suc 0 else length xs)"
+  "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
 apply (induct xs)
  apply (auto dest!:length_pos_if_in_set)
 done

--- a/src/HOL/Nat.thy	Thu Feb 26 17:42:43 2009 +0100
+++ b/src/HOL/Nat.thy	Thu Feb 26 08:48:33 2009 -0800
@@ -701,6 +701,9 @@
 lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
 by (simp add: diff_Suc split: nat.split)
 
+lemma Suc_diff_1 [simp]: "0 < n ==> Suc (n - 1) = n"
+unfolding One_nat_def by (rule Suc_pred)
+
 lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
 by (induct k) simp_all
 
@@ -1135,7 +1138,7 @@
   by (cases m) (auto intro: le_add1)
 
 text {* Lemma for @{text gcd} *}
-lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = Suc 0 | m = 0"
+lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
   apply (drule sym)
   apply (rule disjCI)
   apply (rule nat_less_cases, erule_tac [2] _)