revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)
authorhuffman
Thu Feb 26 08:44:12 2009 -0800 (2009-02-26)
changeset 30128365ee7319b86
parent 30104 b094999e1d33
child 30129 419116f1157a
revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)
src/HOL/List.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/List.thy	Thu Feb 26 06:39:06 2009 -0800
     1.2 +++ b/src/HOL/List.thy	Thu Feb 26 08:44:12 2009 -0800
     1.3 @@ -1438,10 +1438,10 @@
     1.4  apply (auto split:nat.split)
     1.5  done
     1.6  
     1.7 -lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - Suc 0)"
     1.8 +lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
     1.9  by(induct xs)(auto simp:neq_Nil_conv)
    1.10  
    1.11 -lemma butlast_conv_take: "butlast xs = take (length xs - Suc 0) xs"
    1.12 +lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
    1.13  by (induct xs, simp, case_tac xs, simp_all)
    1.14  
    1.15  
    1.16 @@ -1461,6 +1461,12 @@
    1.17  
    1.18  declare take_Cons [simp del] and drop_Cons [simp del]
    1.19  
    1.20 +lemma take_1_Cons [simp]: "take 1 (x # xs) = [x]"
    1.21 +  unfolding One_nat_def by simp
    1.22 +
    1.23 +lemma drop_1_Cons [simp]: "drop 1 (x # xs) = xs"
    1.24 +  unfolding One_nat_def by simp
    1.25 +
    1.26  lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"
    1.27  by(clarsimp simp add:neq_Nil_conv)
    1.28  
    1.29 @@ -1588,17 +1594,17 @@
    1.30  done
    1.31  
    1.32  lemma butlast_take:
    1.33 -  "n <= length xs ==> butlast (take n xs) = take (n - Suc 0) xs"
    1.34 +  "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
    1.35  by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
    1.36  
    1.37  lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
    1.38 -by (simp add: butlast_conv_take drop_take)
    1.39 +by (simp add: butlast_conv_take drop_take add_ac)
    1.40  
    1.41  lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
    1.42  by (simp add: butlast_conv_take min_max.inf_absorb1)
    1.43  
    1.44  lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
    1.45 -by (simp add: butlast_conv_take drop_take)
    1.46 +by (simp add: butlast_conv_take drop_take add_ac)
    1.47  
    1.48  lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
    1.49  by(simp add: hd_conv_nth)
    1.50 @@ -2458,7 +2464,7 @@
    1.51  done
    1.52  
    1.53  lemma length_remove1:
    1.54 -  "length(remove1 x xs) = (if x : set xs then length xs - Suc 0 else length xs)"
    1.55 +  "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
    1.56  apply (induct xs)
    1.57   apply (auto dest!:length_pos_if_in_set)
    1.58  done
     2.1 --- a/src/HOL/Nat.thy	Thu Feb 26 06:39:06 2009 -0800
     2.2 +++ b/src/HOL/Nat.thy	Thu Feb 26 08:44:12 2009 -0800
     2.3 @@ -701,6 +701,9 @@
     2.4  lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
     2.5  by (simp add: diff_Suc split: nat.split)
     2.6  
     2.7 +lemma Suc_diff_1 [simp]: "0 < n ==> Suc (n - 1) = n"
     2.8 +unfolding One_nat_def by (rule Suc_pred)
     2.9 +
    2.10  lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
    2.11  by (induct k) simp_all
    2.12  
    2.13 @@ -1135,7 +1138,7 @@
    2.14    by (cases m) (auto intro: le_add1)
    2.15  
    2.16  text {* Lemma for @{text gcd} *}
    2.17 -lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = Suc 0 | m = 0"
    2.18 +lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
    2.19    apply (drule sym)
    2.20    apply (rule disjCI)
    2.21    apply (rule nat_less_cases, erule_tac [2] _)