# HG changeset patch
# User traytel
# Date 1379513342 -7200
# Node ID a66d211ab34eb294670b514ca1b6fb64d65887a0
# Parent  7b453b619b5f2fe8d7f24a5b6ad5dae2af1cd642
tuned proofs

diff -r 7b453b619b5f -r a66d211ab34e src/HOL/BNF/BNF_GFP.thy
--- 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: *)
diff -r 7b453b619b5f -r a66d211ab34e src/HOL/BNF/BNF_LFP.thy
--- 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"