src/HOL/Library/More_List.thy
changeset 37025 8a5718d54e71
child 37028 a6e0696d7110
     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.105 +  by (induct xs) (simp_all add: add.assoc)
   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