src/HOL/Library/Quotient_Sum.thy
changeset 51377 7da251a6c16e
parent 47982 7aa35601ff65
child 51956 a4d81cdebf8b
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Fri Mar 08 13:21:45 2013 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Fri Mar 08 13:21:52 2013 +0100
     1.3 @@ -46,6 +46,16 @@
     1.4  lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
     1.5    by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
     1.6  
     1.7 +lemma sum_rel_mono[relator_mono]:
     1.8 +  assumes "A \<le> C"
     1.9 +  assumes "B \<le> D"
    1.10 +  shows "(sum_rel A B) \<le> (sum_rel C D)"
    1.11 +using assms by (auto simp: sum_rel_unfold split: sum.splits)
    1.12 +
    1.13 +lemma sum_rel_OO[relator_distr]:
    1.14 +  "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)"
    1.15 +by (rule ext)+ (auto simp add: sum_rel_unfold OO_def split_sum_ex split: sum.split)
    1.16 +
    1.17  lemma sum_reflp[reflexivity_rule]:
    1.18    "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    1.19    unfolding reflp_def split_sum_all sum_rel.simps by fast