src/HOL/Lifting_Sum.thy
 changeset 56520 3373f5d1e074 parent 56519 c1048f5bbb45 child 56525 b5b6ad5dc2ae
equal inserted replaced
56519:c1048f5bbb45 56520:3373f5d1e074
18 lemma rel_sum_OO[relator_distr]:
18 lemma rel_sum_OO[relator_distr]:
19   "(rel_sum A B) OO (rel_sum C D) = rel_sum (A OO C) (B OO D)"
19   "(rel_sum A B) OO (rel_sum C D) = rel_sum (A OO C) (B OO D)"
20   by (rule ext)+ (auto simp add: rel_sum_def OO_def split_sum_ex split: sum.split)
20   by (rule ext)+ (auto simp add: rel_sum_def OO_def split_sum_ex split: sum.split)
21
21
22 lemma Domainp_sum[relator_domain]:
22 lemma Domainp_sum[relator_domain]:
23   assumes "Domainp R1 = P1"
23   "Domainp (rel_sum R1 R2) = (sum_pred (Domainp R1) (Domainp R2))"
24   assumes "Domainp R2 = P2"

25   shows "Domainp (rel_sum R1 R2) = (sum_pred P1 P2)"

26 using assms

27 by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
24 by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
28
25
29 lemma left_total_rel_sum[transfer_rule]:
26 lemma left_total_rel_sum[transfer_rule]:
30   "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (rel_sum R1 R2)"
27   "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (rel_sum R1 R2)"
31   using assms unfolding left_total_def split_sum_all split_sum_ex by simp
28   using assms unfolding left_total_def split_sum_all split_sum_ex by simp