src/HOL/List.thy
changeset 14187 26dfcd0ac436
parent 14111 993471c762b8
child 14208 144f45277d5a
equal deleted inserted replaced
14186:6d2a494e33be 14187:26dfcd0ac436
   735 
   735 
   736 lemma list_update_overwrite [simp]:
   736 lemma list_update_overwrite [simp]:
   737 "!!i. i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]"
   737 "!!i. i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]"
   738 by (induct xs) (auto split: nat.split)
   738 by (induct xs) (auto split: nat.split)
   739 
   739 
       
   740 lemma list_update_id[simp]: "!!i. i < length xs \<Longrightarrow> xs[i := xs!i] = xs"
       
   741 apply(induct xs)
       
   742  apply simp
       
   743 apply(simp split:nat.splits)
       
   744 done
       
   745 
   740 lemma list_update_same_conv:
   746 lemma list_update_same_conv:
   741 "!!i. i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
   747 "!!i. i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
   742 by (induct xs) (auto split: nat.split)
   748 by (induct xs) (auto split: nat.split)
       
   749 
       
   750 lemma list_update_append1:
       
   751  "!!i. i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
       
   752 apply(induct xs)
       
   753  apply simp
       
   754 apply(simp split:nat.split)
       
   755 done
   743 
   756 
   744 lemma update_zip:
   757 lemma update_zip:
   745 "!!i xy xs. length xs = length ys ==>
   758 "!!i xy xs. length xs = length ys ==>
   746 (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
   759 (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
   747 by (induct ys) (auto, case_tac xs, auto split: nat.split)
   760 by (induct ys) (auto, case_tac xs, auto split: nat.split)
   794 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"
   807 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"
   795 by simp
   808 by simp
   796 
   809 
   797 declare take_Cons [simp del] and drop_Cons [simp del]
   810 declare take_Cons [simp del] and drop_Cons [simp del]
   798 
   811 
       
   812 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
       
   813 by(cases xs, simp_all)
       
   814 
       
   815 lemma drop_tl: "!!n. drop n (tl xs) = tl(drop n xs)"
       
   816 by(induct xs, simp_all add:drop_Cons drop_Suc split:nat.split)
       
   817 
       
   818 lemma nth_via_drop: "!!n. drop n xs = y#ys \<Longrightarrow> xs!n = y"
       
   819 apply(induct xs)
       
   820  apply simp
       
   821 apply(simp add:drop_Cons nth_Cons split:nat.splits)
       
   822 done
       
   823 
   799 lemma take_Suc_conv_app_nth:
   824 lemma take_Suc_conv_app_nth:
   800  "!!i. i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
   825  "!!i. i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
   801 apply(induct xs)
   826 apply(induct xs)
   802  apply simp
   827  apply simp
   803 apply(case_tac i)
   828 apply(case_tac i)
   902 lemma set_take_subset: "\<And>n. set(take n xs) \<subseteq> set xs"
   927 lemma set_take_subset: "\<And>n. set(take n xs) \<subseteq> set xs"
   903 by(induct xs)(auto simp:take_Cons split:nat.split)
   928 by(induct xs)(auto simp:take_Cons split:nat.split)
   904 
   929 
   905 lemma set_drop_subset: "\<And>n. set(drop n xs) \<subseteq> set xs"
   930 lemma set_drop_subset: "\<And>n. set(drop n xs) \<subseteq> set xs"
   906 by(induct xs)(auto simp:drop_Cons split:nat.split)
   931 by(induct xs)(auto simp:drop_Cons split:nat.split)
       
   932 
       
   933 lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
       
   934 using set_take_subset by fast
       
   935 
       
   936 lemma in_set_dropD: "x : set(drop n xs) \<Longrightarrow> x : set xs"
       
   937 using set_drop_subset by fast
   907 
   938 
   908 lemma append_eq_conv_conj:
   939 lemma append_eq_conv_conj:
   909 "!!zs. (xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
   940 "!!zs. (xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
   910 apply(induct xs)
   941 apply(induct xs)
   911  apply simp
   942  apply simp