src/HOL/Library/Quotient_Sum.thy
 changeset 51994 82cc2aeb7d13 parent 51956 a4d81cdebf8b child 53010 ec5e6f69bd65
equal 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 `