--- a/Quot/Examples/AbsRepTest.thy	Sat Dec 26 20:45:37 2009 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Sat Dec 26 21:36:20 2009 +0100
@@ -4,142 +4,101 @@
 
 ML {* open Quotient_Term *}
 
-print_maps
-
+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)  
+*}
 
-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
+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 foo = "('a * 'a) list" / "\<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
+  'a fset = "'a list" / erel1
   apply(rule equivpI)
-  unfolding reflp_def symp_def transp_def
+  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 bar = "('a * int) list" / "\<lambda>(xs::('a * int) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
+  'a foo = "('a * 'a) list" / erel2
   apply(rule equivpI)
-  unfolding reflp_def symp_def transp_def
+  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" 
+  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 int = "nat \<times> nat" / intrel
+quotient_type myint = "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
+test_funs absF @{context} 
+     (@{typ "nat \<times> nat"}, 
+      @{typ "myint"})
 *}
 
-(* PROBLEM
 ML {*
-absrep_fun_chk absF @{context} 
+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"})
-|> 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
+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"}, 
+      @{typ "('a fset) fset \<Rightarrow> 'a"})
 *}
 
 
-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
\ No newline at end of file