--- a/src/HOL/BNF/BNF_GFP.thy Wed Sep 18 15:56:15 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy Wed Sep 18 16:09:02 2013 +0200
@@ -23,24 +23,14 @@
lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
by auto
-lemma equiv_triv1:
-assumes "equiv A R" and "(a, b) \<in> R" and "(a, c) \<in> R"
-shows "(b, c) \<in> R"
-using assms unfolding equiv_def sym_def trans_def by blast
-
-lemma equiv_triv2:
-assumes "equiv A R" and "(a, b) \<in> R" and "(b, c) \<in> R"
-shows "(a, c) \<in> R"
-using assms unfolding equiv_def trans_def by blast
-
lemma equiv_proj:
assumes e: "equiv A R" and "z \<in> R"
shows "(proj R o fst) z = (proj R o snd) z"
proof -
from assms(2) have z: "(fst z, snd z) \<in> R" by auto
- have P: "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" by (erule equiv_triv1[OF e z])
- have "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" by (erule equiv_triv2[OF e z])
- with P show ?thesis unfolding proj_def[abs_def] by auto
+ with e have "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R"
+ unfolding equiv_def sym_def trans_def by blast+
+ then show ?thesis unfolding proj_def[abs_def] by auto
qed
(* Operators: *)
--- a/src/HOL/BNF/BNF_LFP.thy Wed Sep 18 15:56:15 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy Wed Sep 18 16:09:02 2013 +0200
@@ -136,10 +136,7 @@
"\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
\<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
\<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y"
-unfolding bij_betw_def inj_on_def
-apply (rule conjI)
- apply blast
-by (erule thin_rl) blast
+unfolding bij_betw_def inj_on_def by blast
lemma surj_fun_eq:
assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x"