src/HOL/Lifting_Product.thy
changeset 56520 3373f5d1e074
parent 56519 c1048f5bbb45
child 56525 b5b6ad5dc2ae
equal deleted inserted replaced
56519:c1048f5bbb45 56520:3373f5d1e074
    22 
    22 
    23 lemma rel_prod_OO[relator_distr]:
    23 lemma rel_prod_OO[relator_distr]:
    24   "(rel_prod A B) OO (rel_prod C D) = rel_prod (A OO C) (B OO D)"
    24   "(rel_prod A B) OO (rel_prod C D) = rel_prod (A OO C) (B OO D)"
    25 by (rule ext)+ (auto simp: rel_prod_def OO_def)
    25 by (rule ext)+ (auto simp: rel_prod_def OO_def)
    26 
    26 
    27 lemma Domainp_prod[relator_domain]:
    27 lemma Domainp_prod[relator_domain]: 
    28   assumes "Domainp T1 = P1"
    28   "Domainp (rel_prod T1 T2) = (pred_prod (Domainp T1) (Domainp T2))"
    29   assumes "Domainp T2 = P2"
    29 unfolding rel_prod_def pred_prod_def by blast
    30   shows "Domainp (rel_prod T1 T2) = (pred_prod P1 P2)"
       
    31 using assms unfolding rel_prod_def pred_prod_def by blast
       
    32 
    30 
    33 lemma left_total_rel_prod [transfer_rule]:
    31 lemma left_total_rel_prod [transfer_rule]:
    34   assumes "left_total R1"
    32   assumes "left_total R1"
    35   assumes "left_total R2"
    33   assumes "left_total R2"
    36   shows "left_total (rel_prod R1 R2)"
    34   shows "left_total (rel_prod R1 R2)"