theory QuotSum

imports QuotMain

begin

fun

  sum_rel

where

  "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"

| "sum_rel R1 R2 (Inl a1) (Inr b2) = False"

| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"

| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"

fun

  sum_map

where

  "sum_map f1 f2 (Inl a) = Inl (f1 a)"

| "sum_map f1 f2 (Inr a) = Inr (f2 a)"

declare [[map * = (sum_map, sum_rel)]]

lemma sum_equivp[quot_equiv]:

  assumes a: "equivp R1"

  assumes b: "equivp R2"

  shows "equivp (sum_rel R1 R2)"

unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def

apply(auto)

apply(case_tac x)

apply(auto simp add: equivp_reflp[OF a] equivp_reflp[OF b])

apply(case_tac x)

apply(case_tac y)

prefer 3

apply(case_tac y)

apply(auto simp add: equivp_symp[OF a] equivp_symp[OF b])

apply(case_tac x)

apply(case_tac y)

apply(case_tac z)

prefer 3

apply(case_tac z)

prefer 5

apply(case_tac y)

apply(case_tac z)

prefer 3

apply(case_tac z)

apply(auto)

apply(metis equivp_transp[OF b])

apply(metis equivp_transp[OF a])

done

lemma sum_fun_fun:

  assumes q1: "Quotient R1 Abs1 Rep1"

  assumes q2: "Quotient R2 Abs2 Rep2"

  shows  "sum_rel R1 R2 r s =

          (sum_rel R1 R2 r r \<and> sum_rel R1 R2 s s \<and> sum_map Abs1 Abs2 r = sum_map Abs1 Abs2 s)"

  using q1 q2

  apply(case_tac r)

  apply(case_tac s)

  apply(simp_all)

  prefer 2

  apply(case_tac s)

  apply(auto)

  unfolding Quotient_def 

  apply metis+

  done

lemma sum_quotient[quot_thm]:

  assumes q1: "Quotient R1 Abs1 Rep1"

  assumes q2: "Quotient R2 Abs2 Rep2"

  shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"

  unfolding Quotient_def

  apply(rule conjI)

  apply(rule allI)

  apply(case_tac a)

  apply(simp add: Quotient_abs_rep[OF q1])

  apply(simp add: Quotient_abs_rep[OF q2])

  apply(rule conjI)

  apply(rule allI)

  apply(case_tac a)

  apply(simp add: Quotient_rel_rep[OF q1])

  apply(simp add: Quotient_rel_rep[OF q2])

  apply(rule allI)+

  apply(rule sum_fun_fun[OF q1 q2])

  done

end