src/HOL/List.thy
 changeset 34978 874150ddd50a parent 34942 d62eddd9e253 child 35028 108662d50512
equal 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 `