src/HOL/List.thy
changeset 34978 874150ddd50a
parent 34942 d62eddd9e253
child 35028 108662d50512
equal deleted inserted replaced
34977:27ceb64d41ea 34978:874150ddd50a
   164 
   164 
   165 primrec
   165 primrec
   166   remdups :: "'a list \<Rightarrow> 'a list" where
   166   remdups :: "'a list \<Rightarrow> 'a list" where
   167     "remdups [] = []"
   167     "remdups [] = []"
   168   | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
   168   | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
       
   169 
       
   170 definition
       
   171   insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
       
   172   "insert x xs = (if x \<in> set xs then xs else x # xs)"
       
   173 
       
   174 hide (open) const insert hide (open) fact insert_def
   169 
   175 
   170 primrec
   176 primrec
   171   remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   177   remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   172     "remove1 x [] = []"
   178     "remove1 x [] = []"
   173   | "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"
   179   | "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"
   240 @{lemma "drop 6 [a,b,c,d] = []" by simp}\\
   246 @{lemma "drop 6 [a,b,c,d] = []" by simp}\\
   241 @{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\
   247 @{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\
   242 @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\
   248 @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\
   243 @{lemma "distinct [2,0,1::nat]" by simp}\\
   249 @{lemma "distinct [2,0,1::nat]" by simp}\\
   244 @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
   250 @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
       
   251 @{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\
       
   252 @{lemma "List.insert 3 [0::nat,1,2] = [3, 0,1,2]" by (simp add: List.insert_def)}\\
   245 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
   253 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
   246 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
   254 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
   247 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
   255 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
   248 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
   256 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
   249 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
   257 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
  1897 
  1905 
  1898 lemma length_zip [simp]:
  1906 lemma length_zip [simp]:
  1899 "length (zip xs ys) = min (length xs) (length ys)"
  1907 "length (zip xs ys) = min (length xs) (length ys)"
  1900 by (induct xs ys rule:list_induct2') auto
  1908 by (induct xs ys rule:list_induct2') auto
  1901 
  1909 
       
  1910 lemma zip_obtain_same_length:
       
  1911   assumes "\<And>zs ws n. length zs = length ws \<Longrightarrow> n = min (length xs) (length ys)
       
  1912     \<Longrightarrow> zs = take n xs \<Longrightarrow> ws = take n ys \<Longrightarrow> P (zip zs ws)"
       
  1913   shows "P (zip xs ys)"
       
  1914 proof -
       
  1915   let ?n = "min (length xs) (length ys)"
       
  1916   have "P (zip (take ?n xs) (take ?n ys))"
       
  1917     by (rule assms) simp_all
       
  1918   moreover have "zip xs ys = zip (take ?n xs) (take ?n ys)"
       
  1919   proof (induct xs arbitrary: ys)
       
  1920     case Nil then show ?case by simp
       
  1921   next
       
  1922     case (Cons x xs) then show ?case by (cases ys) simp_all
       
  1923   qed
       
  1924   ultimately show ?thesis by simp
       
  1925 qed
       
  1926 
  1902 lemma zip_append1:
  1927 lemma zip_append1:
  1903 "zip (xs @ ys) zs =
  1928 "zip (xs @ ys) zs =
  1904 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
  1929 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
  1905 by (induct xs zs rule:list_induct2') auto
  1930 by (induct xs zs rule:list_induct2') auto
  1906 
  1931 
  2211 text{* For efficient code generation: avoid intermediate list. *}
  2236 text{* For efficient code generation: avoid intermediate list. *}
  2212 lemma foldl_map[code_unfold]:
  2237 lemma foldl_map[code_unfold]:
  2213   "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
  2238   "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
  2214 by(induct xs arbitrary:a) simp_all
  2239 by(induct xs arbitrary:a) simp_all
  2215 
  2240 
  2216 lemma foldl_apply_inv:
  2241 lemma foldl_apply:
  2217   assumes "\<And>x. g (h x) = x"
  2242   assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<circ> h = h \<circ> g x"
  2218   shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)"
  2243   shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)"
  2219   by (rule sym, induct xs arbitrary: s) (simp_all add: assms)
  2244   by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: expand_fun_eq)
  2220 
  2245 
  2221 lemma foldl_cong [fundef_cong, recdef_cong]:
  2246 lemma foldl_cong [fundef_cong, recdef_cong]:
  2222   "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
  2247   "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
  2223   ==> foldl f a l = foldl g b k"
  2248   ==> foldl f a l = foldl g b k"
  2224 by (induct k arbitrary: a b l) simp_all
  2249 by (induct k arbitrary: a b l) simp_all
  2279   by (induct xs, simp_all)
  2304   by (induct xs, simp_all)
  2280 
  2305 
  2281 lemma foldl_invariant: 
  2306 lemma foldl_invariant: 
  2282   "\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f y x) \<rbrakk> \<Longrightarrow> Q (foldl f x xs)"
  2307   "\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f y x) \<rbrakk> \<Longrightarrow> Q (foldl f x xs)"
  2283   by (induct xs arbitrary: x, simp_all)
  2308   by (induct xs arbitrary: x, simp_all)
       
  2309 
       
  2310 lemma foldl_weak_invariant:
       
  2311   assumes "P s"
       
  2312     and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f s x)"
       
  2313   shows "P (foldl f s xs)"
       
  2314   using assms by (induct xs arbitrary: s) simp_all
  2284 
  2315 
  2285 text {* @{const foldl} and @{const concat} *}
  2316 text {* @{const foldl} and @{const concat} *}
  2286 
  2317 
  2287 lemma foldl_conv_concat:
  2318 lemma foldl_conv_concat:
  2288   "foldl (op @) xs xss = xs @ concat xss"
  2319   "foldl (op @) xs xss = xs @ concat xss"
  2802 proof -
  2833 proof -
  2803   have xs: "concat[xs] = xs" by simp
  2834   have xs: "concat[xs] = xs" by simp
  2804   from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp
  2835   from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp
  2805 qed
  2836 qed
  2806 
  2837 
       
  2838 subsubsection {* @{const insert} *}
       
  2839 
       
  2840 lemma in_set_insert [simp]:
       
  2841   "x \<in> set xs \<Longrightarrow> List.insert x xs = xs"
       
  2842   by (simp add: List.insert_def)
       
  2843 
       
  2844 lemma not_in_set_insert [simp]:
       
  2845   "x \<notin> set xs \<Longrightarrow> List.insert x xs = x # xs"
       
  2846   by (simp add: List.insert_def)
       
  2847 
       
  2848 lemma insert_Nil [simp]:
       
  2849   "List.insert x [] = [x]"
       
  2850   by simp
       
  2851 
       
  2852 lemma set_insert:
       
  2853   "set (List.insert x xs) = insert x (set xs)"
       
  2854   by (auto simp add: List.insert_def)
       
  2855 
       
  2856 
  2807 subsubsection {* @{text remove1} *}
  2857 subsubsection {* @{text remove1} *}
  2808 
  2858 
  2809 lemma remove1_append:
  2859 lemma remove1_append:
  2810   "remove1 x (xs @ ys) =
  2860   "remove1 x (xs @ ys) =
  2811   (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
  2861   (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
  2850 by (induct xs) simp_all
  2900 by (induct xs) simp_all
  2851 
  2901 
  2852 
  2902 
  2853 subsubsection {* @{text removeAll} *}
  2903 subsubsection {* @{text removeAll} *}
  2854 
  2904 
       
  2905 lemma removeAll_filter_not_eq:
       
  2906   "removeAll x = filter (\<lambda>y. x \<noteq> y)"
       
  2907 proof
       
  2908   fix xs
       
  2909   show "removeAll x xs = filter (\<lambda>y. x \<noteq> y) xs"
       
  2910     by (induct xs) auto
       
  2911 qed
       
  2912 
  2855 lemma removeAll_append[simp]:
  2913 lemma removeAll_append[simp]:
  2856   "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys"
  2914   "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys"
  2857 by (induct xs) auto
  2915 by (induct xs) auto
  2858 
  2916 
  2859 lemma set_removeAll[simp]: "set(removeAll x xs) = set xs - {x}"
  2917 lemma set_removeAll[simp]: "set(removeAll x xs) = set xs - {x}"
  2869 
  2927 
  2870 lemma removeAll_filter_not[simp]:
  2928 lemma removeAll_filter_not[simp]:
  2871   "\<not> P x \<Longrightarrow> removeAll x (filter P xs) = filter P xs"
  2929   "\<not> P x \<Longrightarrow> removeAll x (filter P xs) = filter P xs"
  2872 by(induct xs) auto
  2930 by(induct xs) auto
  2873 
  2931 
       
  2932 lemma distinct_removeAll:
       
  2933   "distinct xs \<Longrightarrow> distinct (removeAll x xs)"
       
  2934   by (simp add: removeAll_filter_not_eq)
  2874 
  2935 
  2875 lemma distinct_remove1_removeAll:
  2936 lemma distinct_remove1_removeAll:
  2876   "distinct xs ==> remove1 x xs = removeAll x xs"
  2937   "distinct xs ==> remove1 x xs = removeAll x xs"
  2877 by (induct xs) simp_all
  2938 by (induct xs) simp_all
  2878 
  2939