--- a/src/HOL/Library/Quotient_Set.thy Thu May 24 13:56:21 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy Thu May 24 14:20:23 2012 +0200
@@ -34,9 +34,22 @@
lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
unfolding set_rel_def fun_eq_iff by auto
-lemma reflp_set_rel[reflp_preserve]: "reflp R \<Longrightarrow> reflp (set_rel R)"
+lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
unfolding reflp_def set_rel_def by fast
+lemma left_total_set_rel[reflexivity_rule]:
+ assumes lt_R: "left_total R"
+ shows "left_total (set_rel R)"
+proof -
+ {
+ fix A
+ let ?B = "{y. \<exists>x \<in> A. R x y}"
+ have "(\<forall>x\<in>A. \<exists>y\<in>?B. R x y) \<and> (\<forall>y\<in>?B. \<exists>x\<in>A. R x y)" using lt_R by(elim left_totalE) blast
+ }
+ then have "\<And>A. \<exists>B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y)" by blast
+ then show ?thesis by (auto simp: set_rel_def intro: left_totalI)
+qed
+
lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)"
unfolding symp_def set_rel_def by fast