equal
deleted
inserted
replaced
260 "Sup (set xs) = foldr sup xs bot" |
260 "Sup (set xs) = foldr sup xs bot" |
261 by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff) |
261 by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff) |
262 |
262 |
263 lemma (in complete_lattice) INFI_set_fold: |
263 lemma (in complete_lattice) INFI_set_fold: |
264 "INFI (set xs) f = fold (inf \<circ> f) xs top" |
264 "INFI (set xs) f = fold (inf \<circ> f) xs top" |
265 unfolding INFI_def set_map [symmetric] Inf_set_fold fold_map .. |
265 unfolding INF_def set_map [symmetric] Inf_set_fold fold_map .. |
266 |
266 |
267 lemma (in complete_lattice) SUPR_set_fold: |
267 lemma (in complete_lattice) SUPR_set_fold: |
268 "SUPR (set xs) f = fold (sup \<circ> f) xs bot" |
268 "SUPR (set xs) f = fold (sup \<circ> f) xs bot" |
269 unfolding SUPR_def set_map [symmetric] Sup_set_fold fold_map .. |
269 unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map .. |
270 |
270 |
271 text {* @{text nth_map} *} |
271 text {* @{text nth_map} *} |
272 |
272 |
273 definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
273 definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
274 "nth_map n f xs = (if n < length xs then |
274 "nth_map n f xs = (if n < length xs then |