added a number of lemmas
authornipkow
Tue Sep 20 13:17:55 2005 +0200 (2005-09-20)
changeset 17501acbebb72e85a
parent 17500 964bad535ac6
child 17502 8836793df947
added a number of lemmas
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Tue Sep 20 13:17:32 2005 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Sep 20 13:17:55 2005 +0200
     1.3 @@ -778,6 +778,12 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma filter_cong:
     1.8 + "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
     1.9 +apply simp
    1.10 +apply(erule thin_rl)
    1.11 +by (induct ys) simp_all
    1.12 +
    1.13  
    1.14  subsubsection {* @{text concat} *}
    1.15  
    1.16 @@ -840,6 +846,9 @@
    1.17  apply (rule_tac x = j in exI, simp)
    1.18  done
    1.19  
    1.20 +lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
    1.21 +by(auto simp:set_conv_nth)
    1.22 +
    1.23  lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"
    1.24  by (auto simp add: set_conv_nth)
    1.25  
    1.26 @@ -879,6 +888,13 @@
    1.27  apply(simp split:nat.splits)
    1.28  done
    1.29  
    1.30 +lemma list_update_beyond[simp]: "\<And>i. length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"
    1.31 +apply (induct xs)
    1.32 + apply simp
    1.33 +apply (case_tac i)
    1.34 +apply simp_all
    1.35 +done
    1.36 +
    1.37  lemma list_update_same_conv:
    1.38  "!!i. i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
    1.39  by (induct xs) (auto split: nat.split)
    1.40 @@ -955,6 +971,12 @@
    1.41  "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"
    1.42  by (auto dest: in_set_butlastD simp add: butlast_append)
    1.43  
    1.44 +lemma last_drop[simp]: "!!n. n < length xs \<Longrightarrow> last (drop n xs) = last xs"
    1.45 +apply (induct xs)
    1.46 + apply simp
    1.47 +apply (auto split:nat.split)
    1.48 +done
    1.49 +
    1.50  
    1.51  subsubsection {* @{text take} and @{text drop} *}
    1.52  
    1.53 @@ -1131,6 +1153,28 @@
    1.54  apply(simp add:drop_Cons split:nat.split)
    1.55  done
    1.56  
    1.57 +lemma id_take_nth_drop:
    1.58 + "i < length xs \<Longrightarrow> xs = take i xs @ xs!i # drop (Suc i) xs" 
    1.59 +proof -
    1.60 +  assume si: "i < length xs"
    1.61 +  hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto
    1.62 +  moreover
    1.63 +  from si have "take (Suc i) xs = take i xs @ [xs!i]"
    1.64 +    apply (rule_tac take_Suc_conv_app_nth) by arith
    1.65 +  ultimately show ?thesis by auto
    1.66 +qed
    1.67 +  
    1.68 +lemma upd_conv_take_nth_drop:
    1.69 + "i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"
    1.70 +proof -
    1.71 +  assume i: "i < length xs"
    1.72 +  have "xs[i:=a] = (take i xs @ xs!i # drop (Suc i) xs)[i:=a]"
    1.73 +    by(rule arg_cong[OF id_take_nth_drop[OF i]])
    1.74 +  also have "\<dots> = take i xs @ a # drop (Suc i) xs"
    1.75 +    using i by (simp add: list_update_append)
    1.76 +  finally show ?thesis .
    1.77 +qed
    1.78 +
    1.79  
    1.80  subsubsection {* @{text takeWhile} and @{text dropWhile} *}
    1.81  
    1.82 @@ -1171,6 +1215,22 @@
    1.83   "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)"
    1.84  by(induct xs, auto)
    1.85  
    1.86 +text{* The following two lemmmas could be generalized to an arbitrary
    1.87 +property. *}
    1.88 +
    1.89 +lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
    1.90 + takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))"
    1.91 +by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
    1.92 +
    1.93 +lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
    1.94 +  dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)"
    1.95 +apply(induct xs)
    1.96 + apply simp
    1.97 +apply auto
    1.98 +apply(subst dropWhile_append2)
    1.99 +apply auto
   1.100 +done
   1.101 +
   1.102  
   1.103  subsubsection {* @{text zip} *}
   1.104  
   1.105 @@ -1461,6 +1521,12 @@
   1.106  apply (simp del: upt.simps)
   1.107  done
   1.108  
   1.109 +lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
   1.110 +apply(induct j)
   1.111 +apply auto
   1.112 +apply arith
   1.113 +done
   1.114 +
   1.115  lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..n]"
   1.116  by (induct n) auto
   1.117  
   1.118 @@ -1565,11 +1631,45 @@
   1.119  apply force
   1.120  done
   1.121  
   1.122 -text {*
   1.123 -It is best to avoid this indexed version of distinct, but sometimes
   1.124 -it is useful. *}
   1.125 +lemma distinct_upt[simp]: "distinct[i..<j]"
   1.126 +by (induct j) auto
   1.127 +
   1.128 +lemma distinct_take[simp]: "\<And>i. distinct xs \<Longrightarrow> distinct (take i xs)"
   1.129 +apply(induct xs)
   1.130 + apply simp
   1.131 +apply (case_tac i)
   1.132 + apply simp_all
   1.133 +apply(blast dest:in_set_takeD)
   1.134 +done
   1.135 +
   1.136 +lemma distinct_drop[simp]: "\<And>i. distinct xs \<Longrightarrow> distinct (drop i xs)"
   1.137 +apply(induct xs)
   1.138 + apply simp
   1.139 +apply (case_tac i)
   1.140 + apply simp_all
   1.141 +done
   1.142 +
   1.143 +lemma distinct_list_update:
   1.144 +assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
   1.145 +shows "distinct (xs[i:=a])"
   1.146 +proof (cases "i < length xs")
   1.147 +  case True
   1.148 +  with a have "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
   1.149 +    apply (drule_tac id_take_nth_drop) by simp
   1.150 +  with d True show ?thesis
   1.151 +    apply (simp add: upd_conv_take_nth_drop)
   1.152 +    apply (drule subst [OF id_take_nth_drop]) apply assumption
   1.153 +    apply simp apply (cases "a = xs!i") apply simp by blast
   1.154 +next
   1.155 +  case False with d show ?thesis by auto
   1.156 +qed
   1.157 +
   1.158 +
   1.159 +text {* It is best to avoid this indexed version of distinct, but
   1.160 +sometimes it is useful. *}
   1.161 +
   1.162  lemma distinct_conv_nth:
   1.163 -"distinct xs = (\<forall>i j. i < size xs \<and> j < size xs \<and> i \<noteq> j --> xs!i \<noteq> xs!j)"
   1.164 +"distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j --> xs!i \<noteq> xs!j)"
   1.165  apply (induct xs, simp, simp)
   1.166  apply (rule iffI, clarsimp)
   1.167   apply (case_tac i)
   1.168 @@ -1579,9 +1679,9 @@
   1.169  apply (clarsimp simp add: set_conv_nth, simp)
   1.170  apply (rule conjI)
   1.171   apply (clarsimp simp add: set_conv_nth)
   1.172 - apply (erule_tac x = 0 in allE)
   1.173 + apply (erule_tac x = 0 in allE, simp)
   1.174   apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
   1.175 -apply (erule_tac x = "Suc i" in allE)
   1.176 +apply (erule_tac x = "Suc i" in allE, simp)
   1.177  apply (erule_tac x = "Suc j" in allE, simp)
   1.178  done
   1.179  
   1.180 @@ -1885,6 +1985,16 @@
   1.181  apply (simp split: nat_diff_split add: sublist_append)
   1.182  done
   1.183  
   1.184 +lemma filter_in_sublist: "\<And>s. distinct xs \<Longrightarrow>
   1.185 +  filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
   1.186 +proof (induct xs)
   1.187 +  case Nil thus ?case by simp
   1.188 +next
   1.189 +  case (Cons a xs)
   1.190 +  moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
   1.191 +  ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
   1.192 +qed
   1.193 +
   1.194  
   1.195  subsubsection{*Sets of Lists*}
   1.196