src/HOL/BNF/BNF_LFP.thy
changeset 51739 3514b90d0a8b
parent 49635 fc0777f04205
child 51804 be6e703908f4
--- a/src/HOL/BNF/BNF_LFP.thy	Tue Apr 23 11:14:51 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy	Tue Apr 23 11:43:09 2013 +0200
@@ -44,9 +44,15 @@
 lemma snd_convol': "snd (<f, g> x) = g x"
 using snd_convol unfolding convol_def by simp
 
+lemma convol_o: "<f, g> o h = <f o h, g o h>"
+  unfolding convol_def by auto
+
 lemma convol_expand_snd: "fst o f = g \<Longrightarrow>  <g, snd o f> = f"
 unfolding convol_def by auto
 
+lemma convol_expand_snd': "(fst o f = g) \<Longrightarrow> (h = snd o f) \<longleftrightarrow> (<g, h> = f)"
+  by (metis convol_expand_snd snd_convol)
+
 definition inver where
   "inver g f A = (ALL a : A. g (f a) = a)"