author traytel Wed, 18 Sep 2013 16:09:02 +0200 changeset 53695 a66d211ab34e parent 53694 7b453b619b5f child 53696 ee9eaab634e5
tuned proofs
 src/HOL/BNF/BNF_GFP.thy file | annotate | diff | comparison | revisions src/HOL/BNF/BNF_LFP.thy file | annotate | diff | comparison | revisions
```--- 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"```