--- a/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 25 16:35:53 2014 +0200
@@ -169,9 +169,6 @@
ultimately show P by (blast intro: assms(3))
qed
-lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
- unfolding rel_fun_def vimage2p_def by auto
-
lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
unfolding vimage2p_def by auto
@@ -184,10 +181,6 @@
lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd"
unfolding rel_fun_def rel_prod_def by simp
-lemma case_sum_transfer:
- "rel_fun (rel_fun R T) (rel_fun (rel_fun S T) (rel_fun (rel_sum R S) T)) case_sum case_sum"
- unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
-
lemma map_sum_transfer:
"rel_fun (rel_fun R T) (rel_fun (rel_fun S U) (rel_fun (rel_sum R S) (rel_sum T U))) map_sum map_sum"
unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
@@ -196,10 +189,6 @@
"rel_fun (rel_fun R S) (rel_fun (rel_fun R T) (rel_fun R (rel_prod S T))) BNF_Def.convol BNF_Def.convol"
unfolding rel_prod_def rel_fun_def convol_def by auto
-lemma comp_transfer:
- "rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (op \<circ>) (op \<circ>)"
- unfolding rel_fun_def by simp
-
lemma Inl_transfer:
"rel_fun S (rel_sum S T) Inl Inl"
by auto