equal
deleted
inserted
replaced
80 |
80 |
81 definition vimage2p where |
81 definition vimage2p where |
82 "vimage2p f g R = (\<lambda>x y. R (f x) (g y))" |
82 "vimage2p f g R = (\<lambda>x y. R (f x) (g y))" |
83 |
83 |
84 lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)" |
84 lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)" |
85 by (rule ext) (auto simp only: comp_apply collect_def) |
85 by (rule ext) (simp add: collect_def) |
86 |
86 |
87 definition convol ("\<langle>(_,/ _)\<rangle>") where |
87 definition convol ("\<langle>(_,/ _)\<rangle>") where |
88 "\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)" |
88 "\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)" |
89 |
89 |
90 lemma fst_convol: "fst \<circ> \<langle>f, g\<rangle> = f" |
90 lemma fst_convol: "fst \<circ> \<langle>f, g\<rangle> = f" |