theory Pair
imports Quotient_Product "../../../Nominal/FSet"
begin

fun alpha :: "('a \<times> 'a) \<Rightarrow> ('a \<times> 'a) \<Rightarrow> bool" (infix "\<approx>" 100)
where
  "(a, b) \<approx> (c, d) = (a = c \<and> b = d \<or> a = d \<and> b = c)"

lemma alpha_refl:
  shows "z \<approx> z"
  by (case_tac z, auto)

lemma alpha_equivp:
  shows "equivp op \<approx>"
  unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
  by auto

quotient_type
  'a pair_set = "'a \<times> 'a" / alpha
  by (auto intro: alpha_equivp)

quotient_definition
  "Two :: 'a \<Rightarrow> 'a \<Rightarrow> 'a pair_set"
is
  "Pair :: 'a \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'a)"

fun
  memb_both_lists
where
  "memb_both_lists a (b, c) = (memb a b \<and> memb a c)"

quotient_definition
  "mem_fsets :: 'a \<Rightarrow> 'a fset pair_set \<Rightarrow> bool"
is memb_both_lists

lemma prod_hlp: "prod_fun abs_fset abs_fset (prod_fun rep_fset rep_fset x) = x"
  by (cases x, auto simp add: Quotient_abs_rep[OF Quotient_fset])

lemma prod_hlp2:
  "prod_rel list_eq list_eq (prod_fun rep_fset rep_fset z) (prod_fun rep_fset rep_fset z)"
  by (cases z, simp)

lemma [quot_thm]:
  shows  "Quotient ((op \<approx>) OOO (prod_rel list_eq list_eq))
    (abs_pair_set \<circ> prod_fun abs_fset abs_fset)
    (prod_fun rep_fset rep_fset \<circ> rep_pair_set)"
  unfolding Quotient_def comp_def
  apply (intro conjI allI)
  apply (simp add: prod_hlp Quotient_abs_rep[OF Quotient_pair_set])
  apply rule
  apply (rule alpha_refl)
  apply rule
  apply (rule prod_hlp2)
  apply (rule alpha_refl)
  apply (intro iffI conjI)
  sorry

lemma [quot_respect]:
  "(op = ===> op \<approx> OOO prod_rel list_eq list_eq ===> op =) memb_both_lists memb_both_lists"
  apply (intro fun_relI)
  apply clarify
  apply (simp only: memb_both_lists.simps)
  sorry

lemma [quot_respect]:
  "(list_eq ===> list_eq ===> op \<approx> OOO prod_rel list_eq list_eq) Pair Pair"
  apply (intro fun_relI)
  apply rule
  apply (rule alpha_refl)
  apply rule
  prefer 2
  apply (rule alpha_refl)
  apply simp
  done

lemma [quot_preserve]:
  "(rep_fset ---> rep_fset ---> abs_pair_set \<circ> prod_fun abs_fset abs_fset) Pair = Two"
  by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] Two_def)

lemma "mem_fsets a (Two b c) = (a |\<in>| b \<and> a |\<in>| c)"
  by (lifting memb_both_lists.simps)

(* Doing it in 2 steps *)

quotient_definition
  "mem_lists :: 'a \<Rightarrow> 'a list pair_set \<Rightarrow> bool"
is memb_both_lists

lemma [quot_respect]: "(op = ===> op \<approx> ===> op =) memb_both_lists memb_both_lists"
  by auto

lemma [quot_respect]: "(op = ===> op = ===> op \<approx>) Pair Pair"
  by auto

lemma step1: "mem_lists a (Two b c) = (memb a b \<and> memb a c)"
  by (lifting memb_both_lists.simps)

lemma step2: "mem_fsets a (Two b c) = (a |\<in>| b \<and> a |\<in>| c)"
  (* apply (lifting step1) ??? *)
  oops

(* Doing it in 2 steps the other way *)

quotient_definition
  "memb_both_fsets :: 'a \<Rightarrow> 'a fset \<times> 'a fset \<Rightarrow> bool"
is memb_both_lists

lemma [quot_respect]:
  "(op = ===> prod_rel list_eq list_eq ===> op =) memb_both_lists memb_both_lists"
  by (auto simp add: memb_def[symmetric])

lemma bla: "memb_both_fsets a (b, c) = (a |\<in>| b \<and> a |\<in>| c)"
  by (lifting memb_both_lists.simps)

lemma step2: "mem_fsets a (Two b c) = (a |\<in>| b \<and> a |\<in>| c)"
  (* ??? *)
  oops

end