src/HOL/Library/Quotient_Sum.thy
changeset 51994 82cc2aeb7d13
parent 51956 a4d81cdebf8b
child 53010 ec5e6f69bd65
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Tue May 14 21:56:19 2013 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Wed May 15 12:10:39 2013 +0200
     1.3 @@ -73,15 +73,17 @@
     1.4  using assms
     1.5  by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split)
     1.6  
     1.7 -lemma sum_reflp[reflexivity_rule]:
     1.8 +lemma reflp_sum_rel[reflexivity_rule]:
     1.9    "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    1.10    unfolding reflp_def split_sum_all sum_rel.simps by fast
    1.11  
    1.12 -lemma sum_left_total[reflexivity_rule]:
    1.13 +lemma left_total_sum_rel[reflexivity_rule]:
    1.14    "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
    1.15 -  apply (intro left_totalI)
    1.16 -  unfolding split_sum_ex 
    1.17 -  by (case_tac x) (auto elim: left_totalE)
    1.18 +  using assms unfolding left_total_def split_sum_all split_sum_ex by simp
    1.19 +
    1.20 +lemma left_unique_sum_rel [reflexivity_rule]:
    1.21 +  "left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (sum_rel R1 R2)"
    1.22 +  using assms unfolding left_unique_def split_sum_all by simp
    1.23  
    1.24  lemma sum_symp:
    1.25    "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
    1.26 @@ -93,7 +95,7 @@
    1.27  
    1.28  lemma sum_equivp [quot_equiv]:
    1.29    "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
    1.30 -  by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE)
    1.31 +  by (blast intro: equivpI reflp_sum_rel sum_symp sum_transp elim: equivpE)
    1.32  
    1.33  lemma right_total_sum_rel [transfer_rule]:
    1.34    "right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (sum_rel R1 R2)"