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)  
*}

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 absF @{context} 
     (@{typ "(('a list) * int) list"}, 
      @{typ "('a fset) bar"})
*}

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





end