# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1282702653 -32400
# Node ID 72fd257f4343bb8ceaabf2e3a11f5fec7380350a
# Parent  20ff5600bd150d285cf5784c5987c1fe6b27824d
Quotient Package / lemma for regularization of bex1_rel for equivalence relations

diff -r 20ff5600bd15 -r 72fd257f4343 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Tue Aug 24 20:09:30 2010 +0200
+++ b/src/HOL/Quotient.thy	Wed Aug 25 11:17:33 2010 +0900
@@ -571,7 +571,8 @@
 apply metis
 done
 
-lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
+lemma bex1_bexeq_reg:
+  shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
   apply (simp add: Ex1_def Bex1_rel_def in_respects)
   apply clarify
   apply auto
@@ -582,6 +583,23 @@
   apply auto
   done
 
+lemma bex1_bexeq_reg_eqv:
+  assumes a: "equivp R"
+  shows "(\<exists>!x. P x) \<longrightarrow> Bex1_rel R P"
+  using equivp_reflp[OF a]
+  apply (intro impI)
+  apply (elim ex1E)
+  apply (rule mp[OF bex1_bexeq_reg])
+  apply (rule_tac a="x" in ex1I)
+  apply (subst in_respects)
+  apply (rule conjI)
+  apply assumption
+  apply assumption
+  apply clarify
+  apply (erule_tac x="xa" in allE)
+  apply simp
+  done
+
 subsection {* Various respects and preserve lemmas *}
 
 lemma quot_rel_rsp: