author  haftmann 
Fri, 14 Oct 2011 22:42:56 +0200  
changeset 45145  d5086da3c32d 
parent 44928  7ef6505bde7f 
child 45146  5465824c1c8d 
permissions  rwrr 
37025  1 
(* Author: Florian Haftmann, TU Muenchen *) 
2 

3 
header {* Operations on lists beyond the standard List theory *} 

4 

5 
theory More_List 

40949
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

6 
imports Main Multiset 
37025  7 
begin 
8 

9 
hide_const (open) Finite_Set.fold 

10 

11 
text {* Repairing code generator setup *} 

12 

13 
declare (in lattice) Inf_fin_set_fold [code_unfold del] 

14 
declare (in lattice) Sup_fin_set_fold [code_unfold del] 

15 
declare (in linorder) Min_fin_set_fold [code_unfold del] 

16 
declare (in linorder) Max_fin_set_fold [code_unfold del] 

17 
declare (in complete_lattice) Inf_set_fold [code_unfold del] 

18 
declare (in complete_lattice) Sup_set_fold [code_unfold del] 

19 

45145  20 

37025  21 
text {* Fold combinator with canonical argument order *} 
22 

23 
primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where 

24 
"fold f [] = id" 

25 
 "fold f (x # xs) = fold f xs \<circ> f x" 

26 

27 
lemma foldl_fold: 

28 
"foldl f s xs = fold (\<lambda>x s. f s x) xs s" 

29 
by (induct xs arbitrary: s) simp_all 

30 

31 
lemma foldr_fold_rev: 

32 
"foldr f xs = fold f (rev xs)" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

33 
by (simp add: foldr_foldl foldl_fold fun_eq_iff) 
37025  34 

35 
lemma fold_rev_conv [code_unfold]: 

36 
"fold f (rev xs) = foldr f xs" 

37 
by (simp add: foldr_fold_rev) 

38 

44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
42871
diff
changeset

39 
lemma fold_cong [fundef_cong]: 
37025  40 
"a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x) 
41 
\<Longrightarrow> fold f xs a = fold g ys b" 

42 
by (induct ys arbitrary: a b xs) simp_all 

43 

44 
lemma fold_id: 

45 
assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id" 

46 
shows "fold f xs = id" 

47 
using assms by (induct xs) simp_all 

48 

39921  49 
lemma fold_commute: 
37025  50 
assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h" 
51 
shows "h \<circ> fold g xs = fold f xs \<circ> h" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

52 
using assms by (induct xs) (simp_all add: fun_eq_iff) 
37025  53 

39921  54 
lemma fold_commute_apply: 
55 
assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h" 

56 
shows "h (fold g xs s) = fold f xs (h s)" 

57 
proof  

58 
from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute) 

59 
then show ?thesis by (simp add: fun_eq_iff) 

60 
qed 

61 

37025  62 
lemma fold_invariant: 
63 
assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s" 

64 
and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)" 

65 
shows "P (fold f xs s)" 

66 
using assms by (induct xs arbitrary: s) simp_all 

67 

68 
lemma fold_weak_invariant: 

69 
assumes "P s" 

70 
and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f x s)" 

71 
shows "P (fold f xs s)" 

72 
using assms by (induct xs arbitrary: s) simp_all 

73 

74 
lemma fold_append [simp]: 

75 
"fold f (xs @ ys) = fold f ys \<circ> fold f xs" 

76 
by (induct xs) simp_all 

77 

78 
lemma fold_map [code_unfold]: 

79 
"fold g (map f xs) = fold (g o f) xs" 

80 
by (induct xs) simp_all 

81 

40949
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

82 
lemma fold_remove1_split: 
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

83 
assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

84 
and x: "x \<in> set xs" 
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

85 
shows "fold f xs = fold f (remove1 x xs) \<circ> f x" 
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

86 
using assms by (induct xs) (auto simp add: o_assoc [symmetric]) 
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

87 

1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

88 
lemma fold_multiset_equiv: 
40951  89 
assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 
40949
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

90 
and equiv: "multiset_of xs = multiset_of ys" 
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

91 
shows "fold f xs = fold f ys" 
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

92 
using f equiv [symmetric] proof (induct xs arbitrary: ys) 
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

93 
case Nil then show ?case by simp 
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

94 
next 
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

95 
case (Cons x xs) 
40951  96 
then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD) 
40949
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

97 
have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 
40951  98 
by (rule Cons.prems(1)) (simp_all add: *) 
99 
moreover from * have "x \<in> set ys" by simp 

40949
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

100 
ultimately have "fold f ys = fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split) 
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

101 
moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps) 
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

102 
ultimately show ?case by simp 
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

103 
qed 
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

104 

37025  105 
lemma fold_rev: 
106 
assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y" 

107 
shows "fold f (rev xs) = fold f xs" 

40949
1d46d893d682
lemmas fold_remove1_split and fold_multiset_equiv
haftmann
parents:
39921
diff
changeset

108 
by (rule fold_multiset_equiv, rule assms) (simp_all add: in_multiset_in_set) 
37025  109 

110 
lemma foldr_fold: 

111 
assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y" 

112 
shows "foldr f xs = fold f xs" 

113 
using assms unfolding foldr_fold_rev by (rule fold_rev) 

114 

115 
lemma fold_Cons_rev: 

116 
"fold Cons xs = append (rev xs)" 

117 
by (induct xs) simp_all 

118 

119 
lemma rev_conv_fold [code]: 

120 
"rev xs = fold Cons xs []" 

121 
by (simp add: fold_Cons_rev) 

122 

123 
lemma fold_append_concat_rev: 

124 
"fold append xss = append (concat (rev xss))" 

125 
by (induct xss) simp_all 

126 

127 
lemma concat_conv_foldr [code]: 

128 
"concat xss = foldr append xss []" 

129 
by (simp add: fold_append_concat_rev foldr_fold_rev) 

130 

131 
lemma fold_plus_listsum_rev: 

132 
"fold plus xs = plus (listsum (rev xs))" 

133 
by (induct xs) (simp_all add: add.assoc) 

134 

39773  135 
lemma (in monoid_add) listsum_conv_fold [code]: 
136 
"listsum xs = fold (\<lambda>x y. y + x) xs 0" 

137 
by (auto simp add: listsum_foldl foldl_fold fun_eq_iff) 

37025  138 

39773  139 
lemma (in linorder) sort_key_conv_fold: 
37025  140 
assumes "inj_on f (set xs)" 
141 
shows "sort_key f xs = fold (insort_key f) xs []" 

142 
proof  

143 
have "fold (insort_key f) (rev xs) = fold (insort_key f) xs" 

144 
proof (rule fold_rev, rule ext) 

145 
fix zs 

146 
fix x y 

147 
assume "x \<in> set xs" "y \<in> set xs" 

148 
with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD) 

39773  149 
have **: "x = y \<longleftrightarrow> y = x" by auto 
37025  150 
show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs" 
39773  151 
by (induct zs) (auto intro: * simp add: **) 
37025  152 
qed 
153 
then show ?thesis by (simp add: sort_key_def foldr_fold_rev) 

154 
qed 

155 

39773  156 
lemma (in linorder) sort_conv_fold: 
37025  157 
"sort xs = fold insort xs []" 
158 
by (rule sort_key_conv_fold) simp 

159 

45145  160 

37025  161 
text {* @{const Finite_Set.fold} and @{const fold} *} 
162 

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
40951
diff
changeset

163 
lemma (in comp_fun_commute) fold_set_remdups: 
37025  164 
"Finite_Set.fold f y (set xs) = fold f (remdups xs) y" 
165 
by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb) 

166 

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
40951
diff
changeset

167 
lemma (in comp_fun_idem) fold_set: 
37025  168 
"Finite_Set.fold f y (set xs) = fold f xs y" 
169 
by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm) 

170 

171 
lemma (in ab_semigroup_idem_mult) fold1_set: 

172 
assumes "xs \<noteq> []" 

173 
shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)" 

174 
proof  

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
40951
diff
changeset

175 
interpret comp_fun_idem times by (fact comp_fun_idem) 
37025  176 
from assms obtain y ys where xs: "xs = y # ys" 
177 
by (cases xs) auto 

178 
show ?thesis 

179 
proof (cases "set ys = {}") 

180 
case True with xs show ?thesis by simp 

181 
next 

182 
case False 

183 
then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)" 

184 
by (simp only: finite_set fold1_eq_fold_idem) 

185 
with xs show ?thesis by (simp add: fold_set mult_commute) 

186 
qed 

187 
qed 

188 

189 
lemma (in lattice) Inf_fin_set_fold: 

190 
"Inf_fin (set (x # xs)) = fold inf xs x" 

191 
proof  

192 
interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" 

193 
by (fact ab_semigroup_idem_mult_inf) 

194 
show ?thesis 

195 
by (simp add: Inf_fin_def fold1_set del: set.simps) 

196 
qed 

197 

198 
lemma (in lattice) Inf_fin_set_foldr [code_unfold]: 

199 
"Inf_fin (set (x # xs)) = foldr inf xs x" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

200 
by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) 
37025  201 

202 
lemma (in lattice) Sup_fin_set_fold: 

203 
"Sup_fin (set (x # xs)) = fold sup xs x" 

204 
proof  

205 
interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" 

206 
by (fact ab_semigroup_idem_mult_sup) 

207 
show ?thesis 

208 
by (simp add: Sup_fin_def fold1_set del: set.simps) 

209 
qed 

210 

211 
lemma (in lattice) Sup_fin_set_foldr [code_unfold]: 

212 
"Sup_fin (set (x # xs)) = foldr sup xs x" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

213 
by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) 
37025  214 

215 
lemma (in linorder) Min_fin_set_fold: 

216 
"Min (set (x # xs)) = fold min xs x" 

217 
proof  

218 
interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" 

219 
by (fact ab_semigroup_idem_mult_min) 

220 
show ?thesis 

221 
by (simp add: Min_def fold1_set del: set.simps) 

222 
qed 

223 

224 
lemma (in linorder) Min_fin_set_foldr [code_unfold]: 

225 
"Min (set (x # xs)) = foldr min xs x" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

226 
by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) 
37025  227 

228 
lemma (in linorder) Max_fin_set_fold: 

229 
"Max (set (x # xs)) = fold max xs x" 

230 
proof  

231 
interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" 

232 
by (fact ab_semigroup_idem_mult_max) 

233 
show ?thesis 

234 
by (simp add: Max_def fold1_set del: set.simps) 

235 
qed 

236 

237 
lemma (in linorder) Max_fin_set_foldr [code_unfold]: 

238 
"Max (set (x # xs)) = foldr max xs x" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

239 
by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) 
37025  240 

241 
lemma (in complete_lattice) Inf_set_fold: 

242 
"Inf (set xs) = fold inf xs top" 

243 
proof  

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
40951
diff
changeset

244 
interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" 
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
40951
diff
changeset

245 
by (fact comp_fun_idem_inf) 
37025  246 
show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute) 
247 
qed 

248 

249 
lemma (in complete_lattice) Inf_set_foldr [code_unfold]: 

250 
"Inf (set xs) = foldr inf xs top" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

251 
by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff) 
37025  252 

253 
lemma (in complete_lattice) Sup_set_fold: 

254 
"Sup (set xs) = fold sup xs bot" 

255 
proof  

42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
40951
diff
changeset

256 
interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" 
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
40951
diff
changeset

257 
by (fact comp_fun_idem_sup) 
37025  258 
show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute) 
259 
qed 

260 

261 
lemma (in complete_lattice) Sup_set_foldr [code_unfold]: 

262 
"Sup (set xs) = foldr sup xs bot" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

263 
by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff) 
37025  264 

265 
lemma (in complete_lattice) INFI_set_fold: 

266 
"INFI (set xs) f = fold (inf \<circ> f) xs top" 

44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44013
diff
changeset

267 
unfolding INF_def set_map [symmetric] Inf_set_fold fold_map .. 
37025  268 

269 
lemma (in complete_lattice) SUPR_set_fold: 

270 
"SUPR (set xs) f = fold (sup \<circ> f) xs bot" 

44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44013
diff
changeset

271 
unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map .. 
37025  272 

45145  273 

37028  274 
text {* @{text nth_map} *} 
37025  275 

276 
definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

277 
"nth_map n f xs = (if n < length xs then 

278 
take n xs @ [f (xs ! n)] @ drop (Suc n) xs 

279 
else xs)" 

280 

281 
lemma nth_map_id: 

282 
"n \<ge> length xs \<Longrightarrow> nth_map n f xs = xs" 

283 
by (simp add: nth_map_def) 

284 

285 
lemma nth_map_unfold: 

286 
"n < length xs \<Longrightarrow> nth_map n f xs = take n xs @ [f (xs ! n)] @ drop (Suc n) xs" 

287 
by (simp add: nth_map_def) 

288 

289 
lemma nth_map_Nil [simp]: 

290 
"nth_map n f [] = []" 

291 
by (simp add: nth_map_def) 

292 

293 
lemma nth_map_zero [simp]: 

294 
"nth_map 0 f (x # xs) = f x # xs" 

295 
by (simp add: nth_map_def) 

296 

297 
lemma nth_map_Suc [simp]: 

298 
"nth_map (Suc n) f (x # xs) = x # nth_map n f xs" 

299 
by (simp add: nth_map_def) 

300 

45145  301 

302 
text {* monad operation *} 

303 

304 
definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where 

305 
"bind xs f = concat (map f xs)" 

306 

307 
lemma bind_simps [simp]: 

308 
"bind [] f = []" 

309 
"bind (x # xs) f = f x @ bind xs f" 

310 
by (simp_all add: bind_def) 

311 

37025  312 
end 