--- a/src/HOL/BNF_GFP.thy Tue Feb 18 14:51:26 2014 +0100
+++ b/src/HOL/BNF_GFP.thy Tue Feb 18 17:56:48 2014 +0100
@@ -51,21 +51,6 @@
(* Operators: *)
definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
-lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b"
-unfolding Id_on_def by simp
-
-lemma Id_onD': "x \<in> Id_on A \<Longrightarrow> fst x = snd x"
-unfolding Id_on_def by auto
-
-lemma Id_on_fst: "x \<in> Id_on A \<Longrightarrow> fst x \<in> A"
-unfolding Id_on_def by auto
-
-lemma Id_on_UNIV: "Id_on UNIV = Id"
-unfolding Id_on_def by auto
-
-lemma Id_on_Comp: "Id_on A = Id_on A O Id_on A"
-unfolding Id_on_def by auto
-
lemma Id_on_Gr: "Id_on A = Gr A id"
unfolding Id_on_def Gr_def by auto
@@ -102,9 +87,6 @@
lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
by force
-lemma Collect_split_in_relI: "x \<in> X \<Longrightarrow> x \<in> Collect (split (in_rel X))"
-by auto
-
lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
unfolding fun_eq_iff by auto
@@ -114,9 +96,6 @@
lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
unfolding Gr_def Grp_def fun_eq_iff by auto
-lemma in_rel_Id_on_UNIV: "in_rel (Id_on UNIV) = op ="
-unfolding fun_eq_iff by auto
-
definition relImage where
"relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"