src/HOL/Lifting_Sum.thy
changeset 56520 3373f5d1e074
parent 56519 c1048f5bbb45
child 56525 b5b6ad5dc2ae
equal deleted 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