# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1261855493 -3600
# Node ID 09dff5ef8f74d7bc91724ffd5bf0a6df8d48e0c2
# Parent  a31cf260eeb377477df4e40ea0300276057f99c0
as expected problems occure when lifting concat lemmas

diff -r a31cf260eeb3 -r 09dff5ef8f74 Quot/Examples/FSet3.thy
--- 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 *}