--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Examples/AbsRepTest.thy	Wed Dec 23 10:31:54 2009 +0100
@@ -0,0 +1,78 @@
+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
\ No newline at end of file