theory Quotients
imports Main
begin

definition
  "NONEMPTY E \<equiv> \<exists>x. E x x"

fun 
  OPTION_REL 
where
  "OPTION_REL R None None = True"
| "OPTION_REL R (Some x) None = False"
| "OPTION_REL R None (Some x) = False"
| "OPTION_REL R (Some x) (Some y) = R x y"

fun
  option_map
where
  "option_map f None = None"
| "option_map f (Some x) = Some (f x)"

fun 
  PROD_REL
where
  "PROD_REL R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \<and> R2 a2 b2)"

fun
  prod_map
where
  "prod_map f1 f2 (a,b) = (f1 a, f2 b)"

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)"

definition
  "QUOTIENT R Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> 
                        (\<forall>a. R (Rep a) (Rep a)) \<and> 
                        (\<forall>r s. R r s = (R r r \<and> R s s \<and> (Abs r = Abs s)))"

lemma QUOTIENT_PROD:
  assumes a: "QUOTIENT E1 Abs1 Rep1"
  and     b: "QUOTIENT E2 Abs2 Rep2"
  shows "QUOTIENT (PROD_REL E1 E2) (prod_map Abs1 Abs2) (prod_map Rep1 Rep2)"
using a b unfolding QUOTIENT_def
oops

lemma QUOTIENT_ABS_REP_LIST:
  assumes a: "QUOTIENT_ABS_REP Abs Rep"
  shows "QUOTIENT_ABS_REP (map Abs) (map Rep)"
using a
unfolding QUOTIENT_ABS_REP_def
apply(rule_tac allI)
apply(induct_tac a rule: list.induct)
apply(auto)
done