src/HOL/List.thy
changeset 18423 d7859164447f
parent 18336 1a2e30b37ed3
child 18447 da548623916a
     1.1 --- a/src/HOL/List.thy	Fri Dec 16 16:00:58 2005 +0100
     1.2 +++ b/src/HOL/List.thy	Fri Dec 16 16:59:32 2005 +0100
     1.3 @@ -628,6 +628,9 @@
     1.4  
     1.5  lemmas rev_cases = rev_exhaust
     1.6  
     1.7 +lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
     1.8 +by(rule rev_cases[of xs]) auto
     1.9 +
    1.10  
    1.11  subsubsection {* @{text set} *}
    1.12  
    1.13 @@ -734,6 +737,10 @@
    1.14  lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"
    1.15  by (induct xs) (auto simp add: le_SucI)
    1.16  
    1.17 +lemma sum_length_filter_compl:
    1.18 +  "length(filter P xs) + length(filter (%x. ~P x) xs) = length xs"
    1.19 +by(induct xs) simp_all
    1.20 +
    1.21  lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs"
    1.22  by (induct xs) auto
    1.23  
    1.24 @@ -906,6 +913,9 @@
    1.25  apply (case_tac n, auto)
    1.26  done
    1.27  
    1.28 +lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
    1.29 +by(cases xs) simp_all
    1.30 +
    1.31  
    1.32  lemma list_eq_iff_nth_eq:
    1.33   "!!ys. (xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
    1.34 @@ -1202,6 +1212,9 @@
    1.35  apply (case_tac xs, auto)
    1.36  done
    1.37  
    1.38 +lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
    1.39 +by(simp add: hd_conv_nth)
    1.40 +
    1.41  lemma set_take_subset: "\<And>n. set(take n xs) \<subseteq> set xs"
    1.42  by(induct xs)(auto simp:take_Cons split:nat.split)
    1.43  
    1.44 @@ -1322,6 +1335,14 @@
    1.45  apply auto
    1.46  done
    1.47  
    1.48 +lemma takeWhile_not_last:
    1.49 + "\<lbrakk> xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
    1.50 +apply(induct xs)
    1.51 + apply simp
    1.52 +apply(case_tac xs)
    1.53 +apply(auto)
    1.54 +done
    1.55 +
    1.56  lemma takeWhile_cong [recdef_cong]:
    1.57    "[| l = k; !!x. x : set l ==> P x = Q x |] 
    1.58    ==> takeWhile P l = takeWhile Q k"
    1.59 @@ -2044,6 +2065,12 @@
    1.60  apply(simp add:rotate_drop_take rev_drop rev_take)
    1.61  done
    1.62  
    1.63 +lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
    1.64 +apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
    1.65 +apply(subgoal_tac "length xs \<noteq> 0")
    1.66 + prefer 2 apply simp
    1.67 +using mod_less_divisor[of "length xs" n] by arith
    1.68 +
    1.69  
    1.70  subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
    1.71  
    1.72 @@ -2335,7 +2362,7 @@
    1.73    "lexn r n =
    1.74      {(xs,ys). length xs = n \<and> length ys = n \<and>
    1.75      (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
    1.76 -apply (induct n, simp, blast)
    1.77 +apply (induct n, simp)
    1.78  apply (simp add: image_Collect lex_prod_def, safe, blast)
    1.79   apply (rule_tac x = "ab # xys" in exI, simp)
    1.80  apply (case_tac xys, simp_all, blast)