theory AbsRepTest
imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List
begin

ML {* open Quotient_Term *}

ML {*
fun test_funs flag ctxt (rty, qty) =
  (absrep_fun_chk flag ctxt (rty, qty)
   |> Syntax.string_of_term ctxt
   |> writeln;
   equiv_relation_chk ctxt (rty, qty) 
   |> Syntax.string_of_term ctxt
   |> writeln;
   new_equiv_relation_chk ctxt (rty, qty) 
   |> Syntax.string_of_term ctxt
   |> writeln)
*}

definition
  erel1 (infixl "\<approx>1" 50)
where
  "erel1 \<equiv> \<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"

quotient_type 
  'a fset = "'a list" / erel1
  apply(rule equivpI)
  unfolding erel1_def reflp_def symp_def transp_def
  by auto

definition
  erel2 (infixl "\<approx>2" 50)
where
  "erel2 \<equiv> \<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"

quotient_type 
  'a foo = "('a * 'a) list" / erel2
  apply(rule equivpI)
  unfolding erel2_def reflp_def symp_def transp_def
  by auto

definition
  erel3 (infixl "\<approx>3" 50)
where
  "erel3 \<equiv> \<lambda>(xs::('a * int) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"

quotient_type 
  'a bar = "('a * int) list" / "erel3"
  apply(rule equivpI)
  unfolding erel3_def reflp_def symp_def transp_def
  by auto

fun
  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infixl "\<approx>4" 50)
where
  "intrel (x, y) (u, v) = (x + v = u + y)"

quotient_type myint = "nat \<times> nat" / intrel
  by (auto simp add: equivp_def expand_fun_eq)

ML {*
test_funs absF @{context} 
     (@{typ "nat \<times> nat"}, 
      @{typ "myint"})
*}

ML {*
test_funs absF @{context} 
     (@{typ "('a * 'a) list"}, 
      @{typ "'a foo"})
*}

ML {*
test_funs repF @{context} 
     (@{typ "(('a * 'a) list * 'b)"}, 
      @{typ "('a foo * 'b)"})
*}

ML {*
test_funs absF @{context} 
     (@{typ "(('a list) * int) list"}, 
      @{typ "('a fset) bar"})
*}

ML {*
test_funs absF @{context} 
     (@{typ "('a list)"}, 
      @{typ "('a fset)"})
*}

ML {*
test_funs absF @{context} 
     (@{typ "('a list) list"}, 
      @{typ "('a fset) fset"})
*}


ML {*
test_funs absF @{context} 
     (@{typ "((nat * nat) list) list"}, 
      @{typ "((myint) fset) fset"})
*}

ML {*
test_funs absF @{context} 
     (@{typ "(('a * 'a) list) list"}, 
      @{typ "(('a * 'a) fset) fset"})
*}

ML {*
test_funs absF @{context} 
      (@{typ "(nat * nat) list"}, 
       @{typ "myint fset"})
*}

ML {*
test_funs absF @{context} 
     (@{typ "('a list) list \<Rightarrow> 'a list"}, 
      @{typ "('a fset) fset \<Rightarrow> 'a fset"})
*}

lemma
  assumes sr: "symp r"
  and     ss: "symp s"
  shows "(r OO s) x y = (s OO r) y x"
using sr ss
unfolding symp_def
apply (metis pred_comp.intros pred_compE ss symp_def)
done

lemma abs_o_rep:
  assumes a: "Quotient r absf repf"
  shows "absf o repf = id"
  apply(rule ext)
  apply(simp add: Quotient_abs_rep[OF a])
done

lemma help1: "list_rel op \<approx>1 ba [] \<equiv> ba = []"
apply(induct ba)
apply (auto)
done

lemma help2: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) (x # xs) [] \<equiv> False"
sorry
lemma help2a: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) [] (x # xs) \<equiv> False"
sorry

(* not used anymore *)
lemma help3: "list_rel op \<approx>1 [] b \<equiv> b = []"
apply (induct b)
apply auto
done

lemma help4: "abs_fset (a # b) = abs_fset [] \<equiv> False"
sorry
lemma help4a: "abs_fset [] = abs_fset (a # b) \<equiv> False"
sorry

lemma help5: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) x x"
sorry

lemma bla0pre:
 "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s =
       ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and>
        (list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
apply(induct r s rule: list_induct2')
  apply(simp)
  apply(simp add: help2 help4 help5)
  apply(simp add: help2a help4a help5)
  apply(simp add: help5)
  apply rule
apply (auto simp add: help2a help4a help5 help1 help2 help4 )
sorry

lemma bla0:
  shows  "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1)) 
               (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
  unfolding Quotient_def comp_def
apply (rule)+
apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset])
apply (rule)
apply (rule)
apply (rule)
apply (rule list_rel_refl)
apply (metis equivp_def fset_equivp)
apply (rule)
apply (rule equivp_reflp[OF fset_equivp])
apply (rule list_rel_refl)
apply (metis equivp_def fset_equivp)
apply rule
apply rule
apply(rule bla0pre)
done

lemma bla0pre2:
 "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s =
       ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and>
        (list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
apply rule
apply rule
apply rule
apply (rule list_rel_refl)
apply (metis equivp_def fset_equivp)
apply rule
apply (rule equivp_reflp[OF fset_equivp])
apply (rule list_rel_refl)
apply (metis equivp_def fset_equivp)
apply(rule)
apply rule
apply (rule list_rel_refl)
apply (metis equivp_def fset_equivp)
apply rule
apply (rule equivp_reflp[OF fset_equivp])
apply (rule list_rel_refl)
apply (metis equivp_def fset_equivp) 
thm pred_comp_def
term "op OO"
apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s")
apply (metis Quotient_rel[OF Quotient_fset])
prefer 2
apply rule
thm rep_abs_rsp
thm rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"]
apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"])
apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
apply (rule list_rel_refl)
apply (metis equivp_def fset_equivp)
apply rule
prefer 2
apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"])
apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
apply (rule list_rel_refl)
apply (metis equivp_def fset_equivp)
sorry

lemma bla:
  assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset"
  and     a2:  "Quotient r2 abs2 rep2"
  shows  "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2)) 
               (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"
  unfolding Quotient_def comp_def
apply (rule)+
apply (simp add: abs_o_rep[OF a2] id_simps Quotient_abs_rep[OF Quotient_fset])
apply (rule)
apply (rule)
using a1
apply -
sorry

lemma bla2:
  assumes a2: "Quotient r1 abs1 rep_fset"
  and         "Quotient r2 abs2 rep2"
  shows  "Quotient ((list_rel r2) OO r1 OO (list_rel r2)) (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"
sorry

thm bla [OF Quotient_fset]
thm bla2[OF Quotient_fset]

thm bla [OF Quotient_fset Quotient_fset]
(* Doesn't work: *)
(* thm bla2[OF Quotient_fset Quotient_fset] *)

end