--- a/Quot/Examples/FSet.thy	Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/Examples/FSet.thy	Mon Dec 21 22:36:31 2009 +0100
@@ -1,5 +1,5 @@
 theory FSet
-imports "../QuotMain" List
+imports "../QuotMain" "../QuotList" List
 begin
 
 inductive
@@ -26,6 +26,61 @@
   fset = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
+
+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
+  apply(unfold equivp_def)
+  apply(auto simp add: mem_def expand_fun_eq)
+  done
+
+
+ML {*
+open Quotient_Def;
+*}
+
+ML {*
+get_fun absF @{context} (@{typ "'a list"}, 
+                         @{typ "'a fset"})
+|> Syntax.check_term @{context}
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+
+term "map id"
+term "abs_fset o (map id)"
+
+ML {*
+get_fun absF @{context} (@{typ "(nat * nat) list"}, 
+                         @{typ "int fset"})
+|> Syntax.check_term @{context}
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+
+term "map abs_int"
+term "abs_fset o map abs_int"
+
+
+ML {*
+get_fun absF @{context} (@{typ "('a list) list"}, 
+                         @{typ "('a fset) fset"})
+|> Syntax.check_term @{context}
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+
+ML {*
+get_fun absF @{context} (@{typ "('a list) list \<Rightarrow> 'a"}, 
+                         @{typ "('a fset) fset \<Rightarrow> 'a"})
+|> Syntax.check_term @{context}
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+
 quotient_definition
    "EMPTY :: 'a fset"
 as
@@ -52,11 +107,19 @@
 as
   "card1"
 
-(* text {*
+quotient_definition
+  "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
+as
+  "concat"
+
+term concat
+term fconcat
+
+text {*
  Maybe make_const_def should require a theorem that says that the particular lifted function
  respects the relation. With it such a definition would be impossible:
- make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}*)
+ make_const_def CARD @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
 
 lemma card1_0:
   fixes a :: "'a list"
@@ -213,7 +276,8 @@
 done
 
 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
-by (lifting member.simps(2))
+apply (lifting member.simps(2))
+done
 
 lemma "INSERT a (INSERT a x) = INSERT a x"
 apply (lifting list_eq.intros(4))