src/HOL/Library/Quotient_Set.thy
changeset 51994 82cc2aeb7d13
parent 51956 a4d81cdebf8b
child 52359 0eafa146b399
     1.1 --- a/src/HOL/Library/Quotient_Set.thy	Tue May 14 21:56:19 2013 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Wed May 15 12:10:39 2013 +0200
     1.3 @@ -53,18 +53,17 @@
     1.4  lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
     1.5    unfolding reflp_def set_rel_def by fast
     1.6  
     1.7 -lemma left_total_set_rel[reflexivity_rule]:
     1.8 -  assumes lt_R: "left_total R"
     1.9 -  shows "left_total (set_rel R)"
    1.10 -proof -
    1.11 -  {
    1.12 -    fix A
    1.13 -    let ?B = "{y. \<exists>x \<in> A. R x y}"
    1.14 -    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.15 -  }
    1.16 -  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.17 -  then show ?thesis by (auto simp: set_rel_def intro: left_totalI)
    1.18 -qed
    1.19 +lemma left_total_set_rel[reflexivity_rule]: 
    1.20 +  "left_total A \<Longrightarrow> left_total (set_rel A)"
    1.21 +  unfolding left_total_def set_rel_def
    1.22 +  apply safe
    1.23 +  apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
    1.24 +done
    1.25 +
    1.26 +lemma left_unique_set_rel[reflexivity_rule]: 
    1.27 +  "left_unique A \<Longrightarrow> left_unique (set_rel A)"
    1.28 +  unfolding left_unique_def set_rel_def
    1.29 +  by fast
    1.30  
    1.31  lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)"
    1.32    unfolding symp_def set_rel_def by fast