src/HOL/Library/Quotient_Sum.thy
changeset 51994 82cc2aeb7d13
parent 51956 a4d81cdebf8b
child 53010 ec5e6f69bd65
--- a/src/HOL/Library/Quotient_Sum.thy	Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy	Wed May 15 12:10:39 2013 +0200
@@ -73,15 +73,17 @@
 using assms
 by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split)
 
-lemma sum_reflp[reflexivity_rule]:
+lemma reflp_sum_rel[reflexivity_rule]:
   "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
   unfolding reflp_def split_sum_all sum_rel.simps by fast
 
-lemma sum_left_total[reflexivity_rule]:
+lemma left_total_sum_rel[reflexivity_rule]:
   "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
-  apply (intro left_totalI)
-  unfolding split_sum_ex 
-  by (case_tac x) (auto elim: left_totalE)
+  using assms unfolding left_total_def split_sum_all split_sum_ex by simp
+
+lemma left_unique_sum_rel [reflexivity_rule]:
+  "left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (sum_rel R1 R2)"
+  using assms unfolding left_unique_def split_sum_all by simp
 
 lemma sum_symp:
   "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
@@ -93,7 +95,7 @@
 
 lemma sum_equivp [quot_equiv]:
   "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
-  by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE)
+  by (blast intro: equivpI reflp_sum_rel sum_symp sum_transp elim: equivpE)
 
 lemma right_total_sum_rel [transfer_rule]:
   "right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (sum_rel R1 R2)"