summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | huffman |

Thu, 26 Feb 2009 08:44:12 -0800 | |

changeset 30128 | 365ee7319b86 |

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 | file | annotate | diff | comparison | revisions | |

src/HOL/Nat.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/List.thy Thu Feb 26 06:39:06 2009 -0800 +++ b/src/HOL/List.thy Thu Feb 26 08:44:12 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 06:39:06 2009 -0800 +++ b/src/HOL/Nat.thy Thu Feb 26 08:44:12 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] _)