src/HOL/Library/Quotient_Sum.thy
changeset 55564 e81ee43ab290
parent 53026 e1a548c11845
child 55931 62156e694f3d
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Tue Feb 18 23:03:47 2014 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Tue Feb 18 23:03:49 2014 +0100
     1.3 @@ -26,6 +26,10 @@
     1.4    "sum_rel (op =) (op =) = (op =)"
     1.5    by (simp add: sum_rel_def fun_eq_iff split: sum.split)
     1.6  
     1.7 +lemma reflp_sum_rel:
     1.8 +  "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
     1.9 +  unfolding reflp_def split_sum_all sum_rel_simps by fast
    1.10 +
    1.11  lemma sum_symp:
    1.12    "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
    1.13    unfolding symp_def split_sum_all sum_rel_simps by fast