theory Quotients
imports Main
begin

definition
  "REFL E \<equiv> \<forall>x. E x x"

definition 
  "SYM E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"

definition
  "TRANS E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"

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

definition 
  "EQUIV E \<equiv> REFL E \<and> SYM E \<and> TRANS E" 

definition 
  "EQUIV_PROP E \<equiv> (\<forall>x y. E x y = (E x = E y))"

lemma EQUIV_PROP_EQUALITY:
  shows "EQUIV_PROP (op =)"
unfolding EQUIV_PROP_def expand_fun_eq
by (blast)

lemma EQUIV_implies_EQUIV_PROP:
  assumes a: "REFL E"
  and     b: "SYM E"
  and     c: "TRANS E"
  shows "EQUIV_PROP E"
using a b c
unfolding EQUIV_PROP_def REFL_def SYM_def TRANS_def expand_fun_eq
by (metis)

lemma EQUIV_PROP_implies_REFL:
  assumes a: "EQUIV_PROP E"
  shows "REFL E"
using a
unfolding EQUIV_PROP_def REFL_def expand_fun_eq
by (metis)

lemma EQUIV_PROP_implies_SYM:
  assumes a: "EQUIV_PROP E"
  shows "SYM E"
using a
unfolding EQUIV_PROP_def SYM_def expand_fun_eq
by (metis)

lemma EQUIV_PROP_implies_TRANS:
  assumes a: "EQUIV_PROP E"
  shows "TRANS E"
using a
unfolding EQUIV_PROP_def TRANS_def expand_fun_eq
by (blast)

ML {* 
fun equiv_refl thm = thm RS @{thm EQUIV_PROP_implies_REFL} 
fun equiv_sym thm = thm RS @{thm EQUIV_PROP_implies_SYM} 
fun equiv_trans thm = thm RS @{thm EQUIV_PROP_implies_TRANS} 

fun refl_sym_trans_equiv thm1 thm2 thm3 = [thm1,thm2,thm3] MRS @{thm EQUIV_implies_EQUIV_PROP} 
*}


fun
  LIST_REL
where
  "LIST_REL R [] [] = True"
| "LIST_REL R (x#xs) [] = False"
| "LIST_REL R [] (x#xs) = False"
| "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)"

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

fun
  FUN_REL 
where
  "FUN_REL R1 R2 f g = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"

fun
  fun_map
where
  "fun_map f g h x = g (h (f x))" 

definition 
  "QUOTIENT_ABS_REP Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = 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_ID:
  shows "QUOTIENT (op =) id id"
unfolding QUOTIENT_def id_def
by (blast)

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

definition
  eqclass ("[_]_")
where
  "[x]E \<equiv> E x"

definition
 QUOTIENT_SET :: "'a set \<Rightarrow> ('a \<Rightarrow>'a\<Rightarrow>bool) \<Rightarrow> ('a set) set" ("_'/#'/_")
where
 "S/#/E = {[x]E | x. x\<in>S}"

definition
 QUOTIENT_UNIV
where
 "QUOTIENT_UNIV TYPE('a) E \<equiv> (UNIV::'a set)/#/E"

consts MY::"'a\<Rightarrow>'a\<Rightarrow>bool"
axioms my1: "REFL MY"
axioms my2: "SYM MY"
axioms my3: "TRANS MY"

term "QUOTIENT_UNIV TYPE('a) MY"
term "\<lambda>f. \<exists>x. f = [x]MY"

typedef 'a quot = "\<lambda>f::'a\<Rightarrow>bool. \<exists>x. f = [x]MY"
by (auto simp add: mem_def)

thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot
thm Abs_quot_cases Rep_quot_cases Abs_quot_induct Rep_quot_induct

lemma lem2:
  shows "([x]MY = [y]MY) = MY x y"
apply(rule iffI)
apply(simp add: eqclass_def)
using my1
apply(auto simp add: REFL_def)[1]
apply(simp add: eqclass_def expand_fun_eq)
apply(rule allI)
apply(rule iffI)
apply(subgoal_tac "MY y x")
using my3
apply(simp add: TRANS_def)[1]
apply(drule_tac x="y" in spec)
apply(drule_tac x="x" in spec)
apply(drule_tac x="xa" in spec)
apply(simp)
using my2
apply(simp add: SYM_def)[1]
oops

lemma lem6:
  "\<forall>a. \<exists>r. Rep_quot a = [r]MY"
apply(rule allI)
apply(subgoal_tac "Rep_quot a \<in> quot")
apply(simp add: quot_def mem_def)
apply(rule Rep_quot)
done

lemma lem7:
  "\<forall>x y. (Abs_quot ([x]MY) = Abs_quot ([y]MY)) = ([x]MY = [y]MY)"
apply(subst Abs_quot_inject)
apply(unfold quot_def mem_def)
apply(auto)
done

definition
  "Abs x = Abs_quot ([x]MY)"

definition
  "Rep a = Eps (Rep_quot a)"

lemma lem9:
  "\<forall>r. [(Eps [r]MY)]MY = [r]MY"
apply(rule allI)
apply(subgoal_tac "MY r r \<Longrightarrow> MY r (Eps (MY r))")
apply(drule meta_mp)
apply(rule eq1[THEN spec])


apply(rule_tac x="MY r" in someI)

lemma 
  "(f \<in> UNIV/#/MY) = (Rep_quot (Abs_quot f) = f)"
apply(simp add: QUOTIENT_SET_def)
apply(auto)
apply(subgoal_tac "[x]MY \<in> quot")
apply(simp add: Abs_quot_inverse)
apply(simp add: quot_def)
apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
apply(auto)[1]
apply(subgoal_tac "[x]MY \<in> quot")
apply(simp add: Abs_quot_inverse)
apply(simp add: quot_def)
apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
apply(auto)[1]
apply(subst expand_set_eq)
thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot

lemma
  "\<forall>a. \<exists>r. Rep_quot a = [r]MY"
apply(rule allI)
apply(subst Abs_quot_inject[symmetric])
apply(rule Rep_quot)
apply(simp add: quot_def)
apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
apply(auto)[1]
apply(simp add: Rep_quot_inverse)
thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot
apply(subst Abs_quot_inject[symmetric])
proof -
  have "[r]MY \<in> quot"
    apply(simp add: quot_def)
    apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
    apply(auto)

thm Abs_quot_inverse


thm Abs_quot_inverse
apply(simp add: Rep_quot_inverse)


thm Rep_quot_inverse

term ""

lemma
  assumes a: "EQUIV2 E"
  shows "([x]E = [y]E) = E x y"
using a
by (simp add: eqclass_def EQUIV2_def)





lemma 
  shows "QUOTIENT (op =) (\<lambda>x. x) (\<lambda>x. x)"
apply(unfold QUOTIENT_def)
apply(blast)
done

definition
  fun_app ("_ ---> _")
where
  "f ---> g \<equiv> \<lambda>h x. g (h (f x))"

lemma helper:
  assumes q: "QUOTIENT R ab re"
  and     a: "R z z"
  shows "R (re (ab z)) z"
using q a
apply(unfold QUOTIENT_def)[1]
apply(blast)
done


lemma
  assumes q1: "QUOTIENT R1 abs1 rep1"
  and     q2: "QUOTIENT R2 abs2 rep2"
  shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
proof -
  have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
    apply(simp add: expand_fun_eq)
    apply(simp add: fun_app_def)
    using q1 q2
    apply(simp add: QUOTIENT_def)
    done
  moreover
  have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
    apply(simp add: FUN_REL_def)
    apply(auto)
    apply(simp add: fun_app_def)
    using q1 q2
    apply(unfold QUOTIENT_def)
    apply(metis)
    done
  moreover
  have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> 
        (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
    apply(simp add: expand_fun_eq)
    apply(rule allI)+
    apply(rule iffI)
    using q1 q2
    apply(unfold QUOTIENT_def)[1]
    apply(unfold fun_app_def)[1]
    apply(unfold FUN_REL_def)[1]
    apply(rule conjI)
    apply(metis)
    apply(rule conjI)
    apply(metis)
    apply(metis)
    apply(erule conjE)
    apply(simp (no_asm) add: FUN_REL_def)
    apply(rule allI impI)+
    apply(subgoal_tac "R1 x x \<and> R1 y y \<and> abs1 x = abs1 y")(*A*)
    using q2
    apply(unfold QUOTIENT_def)[1]
    apply(unfold fun_app_def)[1]
    apply(unfold FUN_REL_def)[1]
    apply(subgoal_tac "R2 (r x) (r x)")(*B*)
    apply(subgoal_tac "R2 (s y) (s y)")(*C*)
    apply(subgoal_tac "abs2 (r x) = abs2 (s y)")(*D*)
    apply(blast)
    (*D*)
    apply(metis helper q1)
    (*C*)
    apply(blast)
    (*B*)
    apply(blast)
    (*A*)
    using q1
    apply(unfold QUOTIENT_def)[1]
    apply(unfold fun_app_def)[1]
    apply(unfold FUN_REL_def)[1]
    apply(metis)
    done
  ultimately
  show "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
    apply(unfold QUOTIENT_def)[1]
    apply(blast)
    done
qed
    
    
    
    



definition 
  "USER R \<equiv> NONEMPTY R \<and> 



typedecl tau
consts R::"tau \<Rightarrow> tau \<Rightarrow> bool"



definition
  FACTOR :: "'a set \<Rightarrow> ('a \<times>'a \<Rightarrow> bool) \<Rightarrow> ('a set) set" ("_ '/'/'/ _")
where
  "A /// r \<equiv> \<Union>x\<in>A. {r``{x}}"

typedef qtau = "\<lambda>c::tau\<Rightarrow>bool. (\<exists>x. R x x \<and> (c = R x))"
apply(rule exI)

apply(rule_tac x="R x" in exI)
apply(auto)

definition  
 "QUOT TYPE('a) R \<equiv> \<lambda>c::'a\<Rightarrow>bool. (\<exists>x. R x x \<and> (c = R x))"