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