diff -r bdd610910e2c -r 2d2d9d1de1a9 src/HOL/BNF/BNF_FP_Basic.thy
--- a/src/HOL/BNF/BNF_FP_Basic.thy	Thu Aug 08 15:30:25 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Basic.thy	Thu Aug 08 16:38:28 2013 +0200
@@ -113,6 +113,36 @@
 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
 by blast
 
+lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
+  unfolding o_def fun_eq_iff by auto
+
+lemma rewriteR_comp_comp2: "\<lbrakk>g o h = r1 o r2; f o r1 = l\<rbrakk> \<Longrightarrow> f o g o h = l o r2"
+  unfolding o_def fun_eq_iff by auto
+
+lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
+  unfolding o_def fun_eq_iff by auto
+
+lemma rewriteL_comp_comp2: "\<lbrakk>f o g = l1 o l2; l2 o h = r\<rbrakk> \<Longrightarrow> f o (g o h) = l1 o r"
+  unfolding o_def fun_eq_iff by auto
+
+lemma convol_o: "<f, g> o h = <f o h, g o h>"
+  unfolding convol_def by auto
+
+lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>"
+  unfolding convol_def by auto
+
+lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
+  unfolding map_pair_o_convol id_o o_id ..
+
+lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
+  unfolding o_def by (auto split: sum.splits)
+
+lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
+  unfolding o_def by (auto split: sum.splits)
+
+lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
+  unfolding sum_case_o_sum_map id_o o_id ..
+
 lemma fun_rel_def_butlast:
   "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
   unfolding fun_rel_def ..