(* Title: Stream_Fusion_List.thy Authors: Alexandra Maximova, ETH Zurich Andreas Lochbihler, ETH Zurich *) section ‹Stream fusion for finite lists› theory Stream_Fusion_List imports Stream_Fusion begin lemma map_option_mono [partial_function_mono]: (* To be moved to HOL *) "mono_option f ⟹ mono_option (λx. map_option g (f x))" apply (rule monotoneI) apply (drule (1) monotoneD) apply (auto simp add: flat_ord_def split: option.split) done subsection ‹The type of generators for finite lists›