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

ML {* open Quotient_Term *}

print_maps


quotient_type 
  'a fset = "'a list" / "\<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
  apply(rule equivpI)
  unfolding reflp_def symp_def transp_def
  by auto

quotient_type 
  'a foo = "('a * 'a) list" / "\<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
  apply(rule equivpI)
  unfolding reflp_def symp_def transp_def
  by auto

quotient_type 
  'a bar = "('a * int) list" / "\<lambda>(xs::('a * int) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
  apply(rule equivpI)
  unfolding reflp_def symp_def transp_def
  by auto

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
  by (auto simp add: equivp_def expand_fun_eq)

print_quotients

ML {*
absrep_fun_chk absF @{context} 
     (@{typ "('a * 'a) list"}, 
      @{typ "'a foo"})
|> Syntax.string_of_term @{context}
|> writeln
*}

(* PROBLEM
ML {*
absrep_fun_chk absF @{context} 
     (@{typ "(('a list) * int) list"}, 
      @{typ "('a fset) bar"})
|> Syntax.string_of_term @{context}
|> writeln
*}*)

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 "nat \<times> nat"}, 
      @{typ "int"})
|> Syntax.string_of_term @{context}
|> writeln
*}


term abs_foo
term rep_foo
term "abs_foo o map (prod_fun id id)"
term "map (prod_fun id id) o rep_foo"

ML {*
absrep_fun_chk absF @{context} 
     (@{typ "('a * 'a) list"}, 
      @{typ "'a foo"})
|> Syntax.string_of_term @{context}
|> writeln
*}

typ "('a fset) foo"

print_quotients

ML{*
Quotient_Info.quotient_rules_get @{context}
*}

print_quotients

ML {*
open Quotient_Term;
*}

ML {*
absrep_fun_chk absF @{context} 
     (@{typ "(('a * 'a) list) list"}, 
      @{typ "(('a * 'a) fset) fset"})
|> Syntax.string_of_term @{context}
|> writeln
*}

(*
ML {*
absrep_fun_chk absF @{context} 
     (@{typ "('a * 'a) list"}, 
      @{typ "'a foo"})
|> 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