added lemmas
authornoschinl
Tue Dec 13 22:44:16 2011 +0100 (2011-12-13)
changeset 45841fe1ef1f3ee55
parent 45840 dadd139192d1
child 45842 3fd2cd187299
added lemmas
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Tue Dec 13 21:15:38 2011 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Dec 13 22:44:16 2011 +0100
     1.3 @@ -1354,6 +1354,10 @@
     1.4  apply (case_tac n, auto)
     1.5  done
     1.6  
     1.7 +lemma nth_tl:
     1.8 +  assumes "n < length (tl x)" shows "tl x ! n = x ! Suc n"
     1.9 +using assms by (induct x) auto
    1.10 +
    1.11  lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
    1.12  by(cases xs) simp_all
    1.13  
    1.14 @@ -1545,6 +1549,12 @@
    1.15  lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
    1.16  by(simp add:last_append)
    1.17  
    1.18 +lemma last_tl: "xs = [] \<or> tl xs \<noteq> [] \<Longrightarrow>last (tl xs) = last xs"
    1.19 +by (induct xs) simp_all
    1.20 +
    1.21 +lemma butlast_tl: "butlast (tl xs) = tl (butlast xs)"
    1.22 +by (induct xs) simp_all
    1.23 +
    1.24  lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
    1.25  by(rule rev_exhaust[of xs]) simp_all
    1.26  
    1.27 @@ -1578,6 +1588,15 @@
    1.28  apply (auto split:nat.split)
    1.29  done
    1.30  
    1.31 +lemma nth_butlast:
    1.32 +  assumes "n < length (butlast xs)" shows "butlast xs ! n = xs ! n"
    1.33 +proof (cases xs)
    1.34 +  case (Cons y ys)
    1.35 +  moreover from assms have "butlast xs ! n = (butlast xs @ [last xs]) ! n"
    1.36 +    by (simp add: nth_append)
    1.37 +  ultimately show ?thesis using append_butlast_last_id by simp
    1.38 +qed simp
    1.39 +
    1.40  lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
    1.41  by(induct xs)(auto simp:neq_Nil_conv)
    1.42  
    1.43 @@ -1899,6 +1918,17 @@
    1.44  "(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
    1.45  by (induct xs) auto
    1.46  
    1.47 +lemma dropWhile_append3:
    1.48 +  "\<not> P y \<Longrightarrow>dropWhile P (xs @ y # ys) = dropWhile P xs @ y # ys"
    1.49 +by (induct xs) auto
    1.50 +
    1.51 +lemma dropWhile_last:
    1.52 +  "x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> last (dropWhile P xs) = last xs"
    1.53 +by (auto simp add: dropWhile_append3 in_set_conv_decomp)
    1.54 +
    1.55 +lemma set_dropWhileD: "x \<in> set (dropWhile P xs) \<Longrightarrow> x \<in> set xs"
    1.56 +by (induct xs) (auto split: split_if_asm)
    1.57 +
    1.58  lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"
    1.59  by (induct xs) (auto split: split_if_asm)
    1.60  
    1.61 @@ -2890,6 +2920,30 @@
    1.62  apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
    1.63  done
    1.64  
    1.65 +lemma not_distinct_conv_prefix:
    1.66 +  defines "dec as xs y ys \<equiv> y \<in> set xs \<and> distinct xs \<and> as = xs @ y # ys"
    1.67 +  shows "\<not>distinct as \<longleftrightarrow> (\<exists>xs y ys. dec as xs y ys)" (is "?L = ?R")
    1.68 +proof
    1.69 +  assume "?L" then show "?R"
    1.70 +  proof (induct "length as" arbitrary: as rule: less_induct)
    1.71 +    case less
    1.72 +    obtain xs ys zs y where decomp: "as = (xs @ y # ys) @ y # zs"
    1.73 +      using not_distinct_decomp[OF less.prems] by auto
    1.74 +    show ?case
    1.75 +    proof (cases "distinct (xs @ y # ys)")
    1.76 +      case True
    1.77 +      with decomp have "dec as (xs @ y # ys) y zs" by (simp add: dec_def)
    1.78 +      then show ?thesis by blast
    1.79 +    next
    1.80 +      case False
    1.81 +      with less decomp obtain xs' y' ys' where "dec (xs @ y # ys) xs' y' ys'"
    1.82 +        by atomize_elim auto
    1.83 +      with decomp have "dec as xs' y' (ys' @ y # zs)" by (simp add: dec_def)
    1.84 +      then show ?thesis by blast
    1.85 +    qed
    1.86 +  qed
    1.87 +qed (auto simp: dec_def)
    1.88 +
    1.89  lemma length_remdups_concat:
    1.90    "length (remdups (concat xss)) = card (\<Union>xs\<in>set xss. set xs)"
    1.91    by (simp add: distinct_card [symmetric])