src/HOL/Library/Quotient_Sum.thy
changeset 39198 f967a16dfcdd
parent 37678 0040bafffdef
child 39302 d7728f65b353
equal deleted inserted replaced
39166:19efc2af3e6c 39198:f967a16dfcdd
    72 
    72 
    73 lemma sum_Inl_prs[quot_preserve]:
    73 lemma sum_Inl_prs[quot_preserve]:
    74   assumes q1: "Quotient R1 Abs1 Rep1"
    74   assumes q1: "Quotient R1 Abs1 Rep1"
    75   assumes q2: "Quotient R2 Abs2 Rep2"
    75   assumes q2: "Quotient R2 Abs2 Rep2"
    76   shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
    76   shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
    77   apply(simp add: expand_fun_eq)
    77   apply(simp add: ext_iff)
    78   apply(simp add: Quotient_abs_rep[OF q1])
    78   apply(simp add: Quotient_abs_rep[OF q1])
    79   done
    79   done
    80 
    80 
    81 lemma sum_Inr_prs[quot_preserve]:
    81 lemma sum_Inr_prs[quot_preserve]:
    82   assumes q1: "Quotient R1 Abs1 Rep1"
    82   assumes q1: "Quotient R1 Abs1 Rep1"
    83   assumes q2: "Quotient R2 Abs2 Rep2"
    83   assumes q2: "Quotient R2 Abs2 Rep2"
    84   shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
    84   shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
    85   apply(simp add: expand_fun_eq)
    85   apply(simp add: ext_iff)
    86   apply(simp add: Quotient_abs_rep[OF q2])
    86   apply(simp add: Quotient_abs_rep[OF q2])
    87   done
    87   done
    88 
    88 
    89 lemma sum_map_id[id_simps]:
    89 lemma sum_map_id[id_simps]:
    90   shows "sum_map id id = id"
    90   shows "sum_map id id = id"
    91   by (simp add: expand_fun_eq split_sum_all)
    91   by (simp add: ext_iff split_sum_all)
    92 
    92 
    93 lemma sum_rel_eq[id_simps]:
    93 lemma sum_rel_eq[id_simps]:
    94   shows "sum_rel (op =) (op =) = (op =)"
    94   shows "sum_rel (op =) (op =) = (op =)"
    95   by (simp add: expand_fun_eq split_sum_all)
    95   by (simp add: ext_iff split_sum_all)
    96 
    96 
    97 end
    97 end