# HG changeset patch
# User krauss
# Date 1311161089 -7200
# Node ID 3264fbfd87d6e4ff42123b2687e8a18261c330f1
# Parent  f651cb0539277012b02857e63dbaadac8d638b28
added UNION

diff -r f651cb053927 -r 3264fbfd87d6 src/HOL/Quotient_Examples/Cset.thy
--- a/src/HOL/Quotient_Examples/Cset.thy	Wed Jul 20 10:48:00 2011 +0200
+++ b/src/HOL/Quotient_Examples/Cset.thy	Wed Jul 20 13:24:49 2011 +0200
@@ -43,6 +43,7 @@
   "((set_eq ===> op =) ===> set_eq) Inf Inf"
   "((set_eq ===> op =) ===> set_eq) Sup Sup"
   "(op = ===> set_eq) List.set List.set"
+  "(set_eq ===> (op = ===> set_eq) ===> set_eq) UNION UNION"
 by (auto simp: fun_rel_eq)
 
 quotient_definition "member :: 'a => 'a Cset.set => bool"
@@ -87,6 +88,8 @@
 is "Inf_class.Inf :: 'a set set \<Rightarrow> 'a set"
 quotient_definition Sup where "Sup :: 'a Cset.set set \<Rightarrow> 'a Cset.set"
 is "Sup_class.Sup :: 'a set set \<Rightarrow> 'a set"
+quotient_definition UNION where "UNION :: 'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set"
+is "Complete_Lattice.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
 
 
 context complete_lattice
@@ -109,11 +112,12 @@
 end
 
 hide_const (open) is_empty insert remove map filter forall exists card
-  set subset psubset inter union empty UNIV uminus minus Inf Sup
+  set subset psubset inter union empty UNIV uminus minus Inf Sup UNION
 
 hide_fact (open) is_empty_def insert_def remove_def map_def filter_def
   forall_def exists_def card_def set_def subset_def psubset_def
   inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def
+  UNION_def
 
 
 end
diff -r f651cb053927 -r 3264fbfd87d6 src/HOL/Quotient_Examples/List_Cset.thy
--- a/src/HOL/Quotient_Examples/List_Cset.thy	Wed Jul 20 10:48:00 2011 +0200
+++ b/src/HOL/Quotient_Examples/List_Cset.thy	Wed Jul 20 13:24:49 2011 +0200
@@ -194,4 +194,11 @@
 apply (lifting union_set_foldr)
 by descending auto
 
+lemma UNION_code [code]:
+  "Cset.UNION (Cset.set []) f = Cset.set []"
+  "Cset.UNION (Cset.set (x#xs)) f =
+     Cset.union (f x) (Cset.UNION (Cset.set xs) f)"
+  by (descending, simp)+
+
+
 end
\ No newline at end of file