src/HOL/Library/Quotient_Sum.thy
changeset 47635 ebb79474262c
parent 47634 091bcd569441
child 47777 f29e7dcd7c40
equal deleted inserted replaced
47634:091bcd569441 47635:ebb79474262c
    76 
    76 
    77 lemma bi_unique_sum_rel [transfer_rule]:
    77 lemma bi_unique_sum_rel [transfer_rule]:
    78   "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)"
    78   "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)"
    79   using assms unfolding bi_unique_def split_sum_all by simp
    79   using assms unfolding bi_unique_def split_sum_all by simp
    80 
    80 
    81 subsection {* Correspondence rules for transfer package *}
    81 subsection {* Transfer rules for transfer package *}
    82 
    82 
    83 lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl"
    83 lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl"
    84   unfolding fun_rel_def by simp
    84   unfolding fun_rel_def by simp
    85 
    85 
    86 lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr"
    86 lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr"