src/HOL/Library/Quotient_Sum.thy
changeset 35243 024fef37a65d
parent 35222 4f1fba00f66d
child 35788 f1deaca15ca3
equal deleted inserted replaced
35242:1c80c29086d7 35243:024fef37a65d
    22 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
    22 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
    23 
    23 
    24 declare [[map "+" = (sum_map, sum_rel)]]
    24 declare [[map "+" = (sum_map, sum_rel)]]
    25 
    25 
    26 
    26 
    27 text {* should probably be in Sum_Type.thy *}
    27 text {* should probably be in @{theory Sum_Type} *}
    28 lemma split_sum_all:
    28 lemma split_sum_all:
    29   shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
    29   shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
    30   apply(auto)
    30   apply(auto)
    31   apply(case_tac x)
    31   apply(case_tac x)
    32   apply(simp_all)
    32   apply(simp_all)