--- a/Quot/Examples/FSet3.thy	Sat Dec 26 09:03:35 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Sat Dec 26 20:24:53 2009 +0100
@@ -121,6 +121,12 @@
   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
 by (lifting singleton_list_eq)
 
+section {* Union *}
+
+quotient_definition
+   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65)
+as
+  "op @"
 
 section {* Cardinality of finite sets *}
 
@@ -213,18 +219,49 @@
 as
  "map"
 
-(* PROPBLEM
 quotient_definition
   "fconcat :: ('a fset) fset => 'a fset"
 as
  "concat"
 
-term concat
-term fconcat
-*)
+lemma fconcat_rsp[quot_respect]:
+  shows "((list_rel op \<approx>) ===> op \<approx>) concat concat"
+apply(auto)
+sorry
+
+(* PROBLEM: these lemmas needs to be restated, since  *)
+(* concat.simps(1) and concat.simps(2) contain the    *)
+(* type variables ?'a1.0 (which are turned into frees *)
+(* 'a_1                                               *)
+lemma concat1: 
+  shows "concat [] = []"
+by (simp)
+
+lemma concat2: 
+  shows "concat (x # xs) =  x @ concat xs"
+by (simp)
 
-consts
-  fconcat :: "('a fset) fset => 'a fset"
+lemma fconcat_empty:
+  shows "fconcat {||} = {||}"
+apply(lifting concat1)
+apply(injection)
+defer
+apply(cleaning)
+apply(simp add: comp_def)
+apply(cleaning)
+apply(fold fempty_def[simplified id_simps])
+apply(rule refl)
+sorry
+
+lemma fconcat_insert:
+  shows "fconcat (finsert x S) = x |\<union>| fconcat S"
+apply(lifting concat2)
+apply(injection)
+defer
+apply(cleaning)
+apply(simp add: comp_def)
+apply(cleaning)
+sorry
 
 text {* raw section *}