theory AbsRepTest

imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List

begin

(*

quotient_type 

  fset = "'a list" / "\<lambda>(xs::'a list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 

  apply(rule equivpI)

  unfolding reflp_def symp_def transp_def

  apply(auto)

  sorry

  done

*)

inductive

  list_eq (infix "\<approx>" 50)

where

  "a#b#xs \<approx> b#a#xs"

| "[] \<approx> []"

| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"

| "a#a#xs \<approx> a#xs"

| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"

| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"

quotient_type 

  fset = "'a list" / "list_eq"

  sorry

fun

  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"

where

  "intrel (x, y) (u, v) = (x + v = u + y)"

quotient_type int = "nat \<times> nat" / intrel

  sorry

ML {*

open Quotient_Term;

*}

ML {*

absrep_fun_chk absF @{context} (@{typ "(((nat * nat) list) * 'a) option"}, @{typ "((int fset) * 'a) option"})

|> Syntax.string_of_term @{context}

|> writeln

*}

term "option_map (prod_fun (abs_fset \<circ> map abs_int) id)"

term "option_map (prod_fun (map rep_int \<circ> rep_fset) id)"

term "option_map (map rep_int \<circ> rep_fset)"

term "option_map (abs_fset o (map abs_int))"

term "abs_fset"

ML {*

absrep_fun_chk absF @{context} (@{typ "(nat * nat) list"}, @{typ "int fset"})

|> Syntax.string_of_term @{context}

|> writeln

*}

term "map abs_int"

term "abs_fset o map abs_int"

ML {*

absrep_fun_chk absF @{context} (@{typ "('a list) list"}, @{typ "('a fset) fset"})

|> Syntax.string_of_term @{context}

|> writeln

*}

ML {*

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

|> Syntax.string_of_term @{context}

|> writeln

*}

end