author haftmann Thu May 20 16:43:00 2010 +0200 (2010-05-20) changeset 37025 8a5718d54e71 parent 37024 e938a0b5286e child 37026 7e8979a155ae
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Library/More_List.thy	Thu May 20 16:43:00 2010 +0200
1.3 @@ -0,0 +1,267 @@
1.4 +(*  Author:  Florian Haftmann, TU Muenchen *)
1.5 +
1.6 +header {* Operations on lists beyond the standard List theory *}
1.7 +
1.8 +theory More_List
1.9 +imports Main
1.10 +begin
1.11 +
1.12 +hide_const (open) Finite_Set.fold
1.13 +
1.14 +text {* Repairing code generator setup *}
1.15 +
1.16 +declare (in lattice) Inf_fin_set_fold [code_unfold del]
1.17 +declare (in lattice) Sup_fin_set_fold [code_unfold del]
1.18 +declare (in linorder) Min_fin_set_fold [code_unfold del]
1.19 +declare (in linorder) Max_fin_set_fold [code_unfold del]
1.20 +declare (in complete_lattice) Inf_set_fold [code_unfold del]
1.21 +declare (in complete_lattice) Sup_set_fold [code_unfold del]
1.22 +declare rev_foldl_cons [code del]
1.23 +
1.24 +text {* Fold combinator with canonical argument order *}
1.25 +
1.26 +primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
1.27 +    "fold f [] = id"
1.28 +  | "fold f (x # xs) = fold f xs \<circ> f x"
1.29 +
1.30 +lemma foldl_fold:
1.31 +  "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
1.32 +  by (induct xs arbitrary: s) simp_all
1.33 +
1.34 +lemma foldr_fold_rev:
1.35 +  "foldr f xs = fold f (rev xs)"
1.36 +  by (simp add: foldr_foldl foldl_fold expand_fun_eq)
1.37 +
1.38 +lemma fold_rev_conv [code_unfold]:
1.39 +  "fold f (rev xs) = foldr f xs"
1.40 +  by (simp add: foldr_fold_rev)
1.41 +
1.42 +lemma fold_cong [fundef_cong, recdef_cong]:
1.43 +  "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
1.44 +    \<Longrightarrow> fold f xs a = fold g ys b"
1.45 +  by (induct ys arbitrary: a b xs) simp_all
1.46 +
1.47 +lemma fold_id:
1.48 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id"
1.49 +  shows "fold f xs = id"
1.50 +  using assms by (induct xs) simp_all
1.51 +
1.52 +lemma fold_apply:
1.53 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
1.54 +  shows "h \<circ> fold g xs = fold f xs \<circ> h"
1.55 +  using assms by (induct xs) (simp_all add: expand_fun_eq)
1.56 +
1.57 +lemma fold_invariant:
1.58 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
1.59 +    and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
1.60 +  shows "P (fold f xs s)"
1.61 +  using assms by (induct xs arbitrary: s) simp_all
1.62 +
1.63 +lemma fold_weak_invariant:
1.64 +  assumes "P s"
1.65 +    and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
1.66 +  shows "P (fold f xs s)"
1.67 +  using assms by (induct xs arbitrary: s) simp_all
1.68 +
1.69 +lemma fold_append [simp]:
1.70 +  "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
1.71 +  by (induct xs) simp_all
1.72 +
1.73 +lemma fold_map [code_unfold]:
1.74 +  "fold g (map f xs) = fold (g o f) xs"
1.75 +  by (induct xs) simp_all
1.76 +
1.77 +lemma fold_rev:
1.78 +  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
1.79 +  shows "fold f (rev xs) = fold f xs"
1.80 +  using assms by (induct xs) (simp_all del: o_apply add: fold_apply)
1.81 +
1.82 +lemma foldr_fold:
1.83 +  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
1.84 +  shows "foldr f xs = fold f xs"
1.85 +  using assms unfolding foldr_fold_rev by (rule fold_rev)
1.86 +
1.87 +lemma fold_Cons_rev:
1.88 +  "fold Cons xs = append (rev xs)"
1.89 +  by (induct xs) simp_all
1.90 +
1.91 +lemma rev_conv_fold [code]:
1.92 +  "rev xs = fold Cons xs []"
1.93 +  by (simp add: fold_Cons_rev)
1.94 +
1.95 +lemma fold_append_concat_rev:
1.96 +  "fold append xss = append (concat (rev xss))"
1.97 +  by (induct xss) simp_all
1.98 +
1.99 +lemma concat_conv_foldr [code]:
1.100 +  "concat xss = foldr append xss []"
1.101 +  by (simp add: fold_append_concat_rev foldr_fold_rev)
1.102 +
1.103 +lemma fold_plus_listsum_rev:
1.104 +  "fold plus xs = plus (listsum (rev xs))"
1.106 +
1.107 +lemma listsum_conv_foldr [code]:
1.108 +  "listsum xs = foldr plus xs 0"
1.109 +  by (fact listsum_foldr)
1.110 +
1.111 +lemma sort_key_conv_fold:
1.112 +  assumes "inj_on f (set xs)"
1.113 +  shows "sort_key f xs = fold (insort_key f) xs []"
1.114 +proof -
1.115 +  have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
1.116 +  proof (rule fold_rev, rule ext)
1.117 +    fix zs
1.118 +    fix x y
1.119 +    assume "x \<in> set xs" "y \<in> set xs"
1.120 +    with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
1.121 +    show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
1.122 +      by (induct zs) (auto dest: *)
1.123 +  qed
1.124 +  then show ?thesis by (simp add: sort_key_def foldr_fold_rev)
1.125 +qed
1.126 +
1.127 +lemma sort_conv_fold:
1.128 +  "sort xs = fold insort xs []"
1.129 +  by (rule sort_key_conv_fold) simp
1.130 +
1.131 +text {* @{const Finite_Set.fold} and @{const fold} *}
1.132 +
1.133 +lemma (in fun_left_comm) fold_set_remdups:
1.134 +  "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
1.135 +  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
1.136 +
1.137 +lemma (in fun_left_comm_idem) fold_set:
1.138 +  "Finite_Set.fold f y (set xs) = fold f xs y"
1.139 +  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
1.140 +
1.141 +lemma (in ab_semigroup_idem_mult) fold1_set:
1.142 +  assumes "xs \<noteq> []"
1.143 +  shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
1.144 +proof -
1.145 +  interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
1.146 +  from assms obtain y ys where xs: "xs = y # ys"
1.147 +    by (cases xs) auto
1.148 +  show ?thesis
1.149 +  proof (cases "set ys = {}")
1.150 +    case True with xs show ?thesis by simp
1.151 +  next
1.152 +    case False
1.153 +    then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
1.154 +      by (simp only: finite_set fold1_eq_fold_idem)
1.155 +    with xs show ?thesis by (simp add: fold_set mult_commute)
1.156 +  qed
1.157 +qed
1.158 +
1.159 +lemma (in lattice) Inf_fin_set_fold:
1.160 +  "Inf_fin (set (x # xs)) = fold inf xs x"
1.161 +proof -
1.162 +  interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.163 +    by (fact ab_semigroup_idem_mult_inf)
1.164 +  show ?thesis
1.165 +    by (simp add: Inf_fin_def fold1_set del: set.simps)
1.166 +qed
1.167 +
1.168 +lemma (in lattice) Inf_fin_set_foldr [code_unfold]:
1.169 +  "Inf_fin (set (x # xs)) = foldr inf xs x"
1.170 +  by (simp add: Inf_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
1.171 +
1.172 +lemma (in lattice) Sup_fin_set_fold:
1.173 +  "Sup_fin (set (x # xs)) = fold sup xs x"
1.174 +proof -
1.175 +  interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.176 +    by (fact ab_semigroup_idem_mult_sup)
1.177 +  show ?thesis
1.178 +    by (simp add: Sup_fin_def fold1_set del: set.simps)
1.179 +qed
1.180 +
1.181 +lemma (in lattice) Sup_fin_set_foldr [code_unfold]:
1.182 +  "Sup_fin (set (x # xs)) = foldr sup xs x"
1.183 +  by (simp add: Sup_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
1.184 +
1.185 +lemma (in linorder) Min_fin_set_fold:
1.186 +  "Min (set (x # xs)) = fold min xs x"
1.187 +proof -
1.188 +  interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.189 +    by (fact ab_semigroup_idem_mult_min)
1.190 +  show ?thesis
1.191 +    by (simp add: Min_def fold1_set del: set.simps)
1.192 +qed
1.193 +
1.194 +lemma (in linorder) Min_fin_set_foldr [code_unfold]:
1.195 +  "Min (set (x # xs)) = foldr min xs x"
1.196 +  by (simp add: Min_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
1.197 +
1.198 +lemma (in linorder) Max_fin_set_fold:
1.199 +  "Max (set (x # xs)) = fold max xs x"
1.200 +proof -
1.201 +  interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.202 +    by (fact ab_semigroup_idem_mult_max)
1.203 +  show ?thesis
1.204 +    by (simp add: Max_def fold1_set del: set.simps)
1.205 +qed
1.206 +
1.207 +lemma (in linorder) Max_fin_set_foldr [code_unfold]:
1.208 +  "Max (set (x # xs)) = foldr max xs x"
1.209 +  by (simp add: Max_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
1.210 +
1.211 +lemma (in complete_lattice) Inf_set_fold:
1.212 +  "Inf (set xs) = fold inf xs top"
1.213 +proof -
1.214 +  interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.215 +    by (fact fun_left_comm_idem_inf)
1.216 +  show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
1.217 +qed
1.218 +
1.219 +lemma (in complete_lattice) Inf_set_foldr [code_unfold]:
1.220 +  "Inf (set xs) = foldr inf xs top"
1.221 +  by (simp add: Inf_set_fold ac_simps foldr_fold expand_fun_eq)
1.222 +
1.223 +lemma (in complete_lattice) Sup_set_fold:
1.224 +  "Sup (set xs) = fold sup xs bot"
1.225 +proof -
1.226 +  interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.227 +    by (fact fun_left_comm_idem_sup)
1.228 +  show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
1.229 +qed
1.230 +
1.231 +lemma (in complete_lattice) Sup_set_foldr [code_unfold]:
1.232 +  "Sup (set xs) = foldr sup xs bot"
1.233 +  by (simp add: Sup_set_fold ac_simps foldr_fold expand_fun_eq)
1.234 +
1.235 +lemma (in complete_lattice) INFI_set_fold:
1.236 +  "INFI (set xs) f = fold (inf \<circ> f) xs top"
1.237 +  unfolding INFI_def set_map [symmetric] Inf_set_fold fold_map ..
1.238 +
1.239 +lemma (in complete_lattice) SUPR_set_fold:
1.240 +  "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
1.241 +  unfolding SUPR_def set_map [symmetric] Sup_set_fold fold_map ..
1.242 +
1.243 +text {* nth_map *}
1.244 +
1.245 +definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
1.246 +  "nth_map n f xs = (if n < length xs then
1.247 +       take n xs @ [f (xs ! n)] @ drop (Suc n) xs
1.248 +     else xs)"
1.249 +
1.250 +lemma nth_map_id:
1.251 +  "n \<ge> length xs \<Longrightarrow> nth_map n f xs = xs"
1.252 +  by (simp add: nth_map_def)
1.253 +
1.254 +lemma nth_map_unfold:
1.255 +  "n < length xs \<Longrightarrow> nth_map n f xs = take n xs @ [f (xs ! n)] @ drop (Suc n) xs"
1.256 +  by (simp add: nth_map_def)
1.257 +
1.258 +lemma nth_map_Nil [simp]:
1.259 +  "nth_map n f [] = []"
1.260 +  by (simp add: nth_map_def)
1.261 +
1.262 +lemma nth_map_zero [simp]:
1.263 +  "nth_map 0 f (x # xs) = f x # xs"
1.264 +  by (simp add: nth_map_def)
1.265 +
1.266 +lemma nth_map_Suc [simp]:
1.267 +  "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
1.268 +  by (simp add: nth_map_def)
1.269 +
1.270 +end
```