author | noschinl |

Tue Dec 13 22:44:16 2011 +0100 (2011-12-13) | |

changeset 45841 | fe1ef1f3ee55 |

parent 45840 | dadd139192d1 |

child 45842 | 3fd2cd187299 |

added lemmas

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])