--- a/Quot/Examples/AbsRepTest.thy	Fri Dec 25 00:58:06 2009 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Sat Dec 26 07:15:30 2009 +0100
@@ -2,21 +2,87 @@
 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
-  apply(auto)
-  done
+  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
-  apply(auto)
-  done
+  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
 
@@ -24,12 +90,6 @@
 Quotient_Info.quotient_rules_get @{context}
 *}
 
-quotient_type int = "nat \<times> nat" / "\<lambda>(x, y) (u, v). x + v = u + (y::nat)"
-  apply(rule equivpI)
-  unfolding reflp_def symp_def transp_def
-  apply(auto)
-  done
-
 print_quotients
 
 ML {*