src/HOL/Library/Quotient_Set.thy
changeset 47982 7aa35601ff65
parent 47936 756f30eac792
child 51377 7da251a6c16e
     1.1 --- a/src/HOL/Library/Quotient_Set.thy	Thu May 24 13:56:21 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Thu May 24 14:20:23 2012 +0200
     1.3 @@ -34,9 +34,22 @@
     1.4  lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
     1.5    unfolding set_rel_def fun_eq_iff by auto
     1.6  
     1.7 -lemma reflp_set_rel[reflp_preserve]: "reflp R \<Longrightarrow> reflp (set_rel R)"
     1.8 +lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
     1.9    unfolding reflp_def set_rel_def by fast
    1.10  
    1.11 +lemma left_total_set_rel[reflexivity_rule]:
    1.12 +  assumes lt_R: "left_total R"
    1.13 +  shows "left_total (set_rel R)"
    1.14 +proof -
    1.15 +  {
    1.16 +    fix A
    1.17 +    let ?B = "{y. \<exists>x \<in> A. R x y}"
    1.18 +    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
    1.19 +  }
    1.20 +  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
    1.21 +  then show ?thesis by (auto simp: set_rel_def intro: left_totalI)
    1.22 +qed
    1.23 +
    1.24  lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)"
    1.25    unfolding symp_def set_rel_def by fast
    1.26