src/HOL/Library/Quotient_Set.thy
changeset 51377 7da251a6c16e
parent 47982 7aa35601ff65
child 51956 a4d81cdebf8b
     1.1 --- a/src/HOL/Library/Quotient_Set.thy	Fri Mar 08 13:21:45 2013 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Fri Mar 08 13:21:52 2013 +0100
     1.3 @@ -22,7 +22,16 @@
     1.4  lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"
     1.5    unfolding set_rel_def by auto
     1.6  
     1.7 -lemma set_rel_OO: "set_rel (R OO S) = set_rel R OO set_rel S"
     1.8 +lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
     1.9 +  unfolding set_rel_def fun_eq_iff by auto
    1.10 +
    1.11 +lemma set_rel_mono[relator_mono]:
    1.12 +  assumes "A \<le> B"
    1.13 +  shows "set_rel A \<le> set_rel B"
    1.14 +using assms unfolding set_rel_def by blast
    1.15 +
    1.16 +lemma set_rel_OO[relator_distr]: "set_rel R OO set_rel S = set_rel (R OO S)"
    1.17 +  apply (rule sym)
    1.18    apply (intro ext, rename_tac X Z)
    1.19    apply (rule iffI)
    1.20    apply (rule_tac b="{y. (\<exists>x\<in>X. R x y) \<and> (\<exists>z\<in>Z. S y z)}" in relcomppI)
    1.21 @@ -31,9 +40,6 @@
    1.22    apply (simp add: set_rel_def, fast)
    1.23    done
    1.24  
    1.25 -lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
    1.26 -  unfolding set_rel_def fun_eq_iff by auto
    1.27 -
    1.28  lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
    1.29    unfolding reflp_def set_rel_def by fast
    1.30  
    1.31 @@ -207,7 +213,7 @@
    1.32    assumes "Quotient R Abs Rep T"
    1.33    shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"
    1.34    using assms unfolding Quotient_alt_def4
    1.35 -  apply (simp add: set_rel_OO set_rel_conversep)
    1.36 +  apply (simp add: set_rel_OO[symmetric] set_rel_conversep)
    1.37    apply (simp add: set_rel_def, fast)
    1.38    done
    1.39