# HG changeset patch
# User blanchet
# Date 1384820990 -3600
# Node ID ef90494cc827edcc26c7c119944186bc3b5955ce
# Parent  9f24325c2550959f005357ff0f3da64342b86e80
killed unused lemmas

diff -r 9f24325c2550 -r ef90494cc827 src/HOL/BNF/BNF_GFP.thy
--- a/src/HOL/BNF/BNF_GFP.thy	Tue Nov 19 01:29:50 2013 +0100
+++ b/src/HOL/BNF/BNF_GFP.thy	Tue Nov 19 01:29:50 2013 +0100
@@ -56,9 +56,6 @@
 lemma Id_on_Gr: "Id_on A = Gr A id"
 unfolding Id_on_def Gr_def by auto
 
-lemma Id_on_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> Id_on UNIV"
-unfolding Id_on_def by auto
-
 lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
 unfolding image2_def by auto
 
@@ -130,9 +127,6 @@
 "R \<subseteq> relInvImage UNIV (relImage R f) f"
 unfolding relInvImage_def relImage_def by auto
 
-lemma equiv_Image: "equiv A R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> a \<in> A \<and> b \<in> A \<and> R `` {a} = R `` {b})"
-unfolding equiv_def refl_on_def Image_def by (auto intro: transD symD)
-
 lemma relImage_proj:
 assumes "equiv A R"
 shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
@@ -293,18 +287,12 @@
 lemma image2pI: "R x y \<Longrightarrow> (image2p f g R) (f x) (g y)"
   unfolding image2p_def by blast
 
-lemma image2p_eqI: "\<lbrakk>fx = f x; gy = g y; R x y\<rbrakk> \<Longrightarrow> (image2p f g R) fx gy"
-  unfolding image2p_def by blast
-
 lemma image2pE: "\<lbrakk>(image2p f g R) fx gy; (\<And>x y. fx = f x \<Longrightarrow> gy = g y \<Longrightarrow> R x y \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
   unfolding image2p_def by blast
 
 lemma fun_rel_iff_geq_image2p: "(fun_rel R S) f g = (image2p f g R \<le> S)"
   unfolding fun_rel_def image2p_def by auto
 
-lemma convol_image_image2p: "<f o fst, g o snd> ` Collect (split R) \<subseteq> Collect (split (image2p f g R))"
-  unfolding convol_def image2p_def by fastforce
-
 lemma fun_rel_image2p: "(fun_rel R (image2p f g R)) f g"
   unfolding fun_rel_def image2p_def by auto