src/HOL/Library/Quotient_Sum.thy
changeset 51994 82cc2aeb7d13
parent 51956 a4d81cdebf8b
child 53010 ec5e6f69bd65
equal deleted inserted replaced
51993:ea123790121b 51994:82cc2aeb7d13
    71   assumes "Domainp R2 = P2"
    71   assumes "Domainp R2 = P2"
    72   shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)"
    72   shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)"
    73 using assms
    73 using assms
    74 by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split)
    74 by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split)
    75 
    75 
    76 lemma sum_reflp[reflexivity_rule]:
    76 lemma reflp_sum_rel[reflexivity_rule]:
    77   "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    77   "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    78   unfolding reflp_def split_sum_all sum_rel.simps by fast
    78   unfolding reflp_def split_sum_all sum_rel.simps by fast
    79 
    79 
    80 lemma sum_left_total[reflexivity_rule]:
    80 lemma left_total_sum_rel[reflexivity_rule]:
    81   "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
    81   "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
    82   apply (intro left_totalI)
    82   using assms unfolding left_total_def split_sum_all split_sum_ex by simp
    83   unfolding split_sum_ex 
    83 
    84   by (case_tac x) (auto elim: left_totalE)
    84 lemma left_unique_sum_rel [reflexivity_rule]:
       
    85   "left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (sum_rel R1 R2)"
       
    86   using assms unfolding left_unique_def split_sum_all by simp
    85 
    87 
    86 lemma sum_symp:
    88 lemma sum_symp:
    87   "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
    89   "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
    88   unfolding symp_def split_sum_all sum_rel.simps by fast
    90   unfolding symp_def split_sum_all sum_rel.simps by fast
    89 
    91 
    91   "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
    93   "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
    92   unfolding transp_def split_sum_all sum_rel.simps by fast
    94   unfolding transp_def split_sum_all sum_rel.simps by fast
    93 
    95 
    94 lemma sum_equivp [quot_equiv]:
    96 lemma sum_equivp [quot_equiv]:
    95   "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
    97   "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
    96   by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE)
    98   by (blast intro: equivpI reflp_sum_rel sum_symp sum_transp elim: equivpE)
    97 
    99 
    98 lemma right_total_sum_rel [transfer_rule]:
   100 lemma right_total_sum_rel [transfer_rule]:
    99   "right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (sum_rel R1 R2)"
   101   "right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (sum_rel R1 R2)"
   100   unfolding right_total_def split_sum_all split_sum_ex by simp
   102   unfolding right_total_def split_sum_all split_sum_ex by simp
   101 
   103