equal
deleted
inserted
replaced
41 lemma fst_convol': "fst (<f, g> x) = f x" |
41 lemma fst_convol': "fst (<f, g> x) = f x" |
42 using fst_convol unfolding convol_def by simp |
42 using fst_convol unfolding convol_def by simp |
43 |
43 |
44 lemma snd_convol': "snd (<f, g> x) = g x" |
44 lemma snd_convol': "snd (<f, g> x) = g x" |
45 using snd_convol unfolding convol_def by simp |
45 using snd_convol unfolding convol_def by simp |
46 |
|
47 lemma convol_o: "<f, g> o h = <f o h, g o h>" |
|
48 unfolding convol_def by auto |
|
49 |
46 |
50 lemma convol_expand_snd: "fst o f = g \<Longrightarrow> <g, snd o f> = f" |
47 lemma convol_expand_snd: "fst o f = g \<Longrightarrow> <g, snd o f> = f" |
51 unfolding convol_def by auto |
48 unfolding convol_def by auto |
52 |
49 |
53 lemma convol_expand_snd': "(fst o f = g) \<Longrightarrow> (h = snd o f) \<longleftrightarrow> (<g, h> = f)" |
50 lemma convol_expand_snd': "(fst o f = g) \<Longrightarrow> (h = snd o f) \<longleftrightarrow> (<g, h> = f)" |