# HG changeset patch
# User bulwahn
# Date 1319553431 -7200
# Node ID 66823a0066db163da40563371c0710970988c514
# Parent  13b5fb92b9f5ca165fe78fc58046bc84115cdbe1
renaming Cset and List_Cset in Quotient_Examples to Quotient_Set and List_Quotient_Set to avoid a name clash of theory names with the ones in HOL-Library

diff -r 13b5fb92b9f5 -r 66823a0066db src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Oct 25 16:09:02 2011 +0200
+++ b/src/HOL/IsaMakefile	Tue Oct 25 16:37:11 2011 +0200
@@ -1503,8 +1503,8 @@
 HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz
 
 $(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL				\
-  Quotient_Examples/DList.thy Quotient_Examples/Cset.thy \
-  Quotient_Examples/FSet.thy Quotient_Examples/List_Cset.thy \
+  Quotient_Examples/DList.thy Quotient_Examples/Quotient_Set.thy \
+  Quotient_Examples/FSet.thy Quotient_Examples/List_Quotient_Set.thy \
   Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
 
diff -r 13b5fb92b9f5 -r 66823a0066db src/HOL/Quotient_Examples/Cset.thy
--- a/src/HOL/Quotient_Examples/Cset.thy	Tue Oct 25 16:09:02 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-(*  Title:      HOL/Quotient_Examples/Cset.thy
-    Author:     Florian Haftmann, Alexander Krauss, TU Muenchen
-*)
-
-header {* A variant of theory Cset from Library, defined as a quotient *}
-
-theory Cset
-imports "~~/src/HOL/Library/More_Set" "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Quotient_Syntax"
-begin
-
-subsection {* Lifting *}
-
-(*FIXME: quotient package requires a dedicated constant*)
-definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
-where [simp]: "set_eq \<equiv> op ="
-
-quotient_type 'a set = "'a Set.set" / "set_eq"
-by (simp add: identity_equivp)
-
-hide_type (open) set
-
-subsection {* Operations *}
-
-lemma [quot_respect]:
-  "(op = ===> set_eq ===> op =) (op \<in>) (op \<in>)"
-  "(op = ===> set_eq) Collect Collect"
-  "(set_eq ===> op =) More_Set.is_empty More_Set.is_empty"
-  "(op = ===> set_eq ===> set_eq) Set.insert Set.insert"
-  "(op = ===> set_eq ===> set_eq) More_Set.remove More_Set.remove"
-  "(op = ===> set_eq ===> set_eq) image image"
-  "(op = ===> set_eq ===> set_eq) More_Set.project More_Set.project"
-  "(set_eq ===> op =) Ball Ball"
-  "(set_eq ===> op =) Bex Bex"
-  "(set_eq ===> op =) Finite_Set.card Finite_Set.card"
-  "(set_eq ===> set_eq ===> op =) (op \<subseteq>) (op \<subseteq>)"
-  "(set_eq ===> set_eq ===> op =) (op \<subset>) (op \<subset>)"
-  "(set_eq ===> set_eq ===> set_eq) (op \<inter>) (op \<inter>)"
-  "(set_eq ===> set_eq ===> set_eq) (op \<union>) (op \<union>)"
-  "set_eq {} {}"
-  "set_eq UNIV UNIV"
-  "(set_eq ===> set_eq) uminus uminus"
-  "(set_eq ===> set_eq ===> set_eq) minus minus"
-  "(set_eq ===> op =) Inf Inf"
-  "(set_eq ===> op =) 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"
-is "op \<in>"
-quotient_definition "Set :: ('a => bool) => 'a Cset.set"
-is Collect
-quotient_definition is_empty where "is_empty :: 'a Cset.set \<Rightarrow> bool"
-is More_Set.is_empty
-quotient_definition insert where "insert :: 'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
-is Set.insert
-quotient_definition remove where "remove :: 'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
-is More_Set.remove
-quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set"
-is image
-quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
-is More_Set.project
-quotient_definition "forall :: 'a Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-is Ball
-quotient_definition "exists :: 'a Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-is Bex
-quotient_definition card where "card :: 'a Cset.set \<Rightarrow> nat"
-is Finite_Set.card
-quotient_definition set where "set :: 'a list => 'a Cset.set"
-is List.set
-quotient_definition subset where "subset :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool"
-is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
-quotient_definition psubset where "psubset :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool"
-is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
-quotient_definition inter where "inter :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
-is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
-quotient_definition union where "union :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
-is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
-quotient_definition empty where "empty :: 'a Cset.set"
-is "{} :: 'a set"
-quotient_definition UNIV where "UNIV :: 'a Cset.set"
-is "Set.UNIV :: 'a set"
-quotient_definition uminus where "uminus :: 'a Cset.set \<Rightarrow> 'a Cset.set"
-is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set"
-quotient_definition minus where "minus :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
-is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
-quotient_definition Inf where "Inf :: ('a :: Inf) Cset.set \<Rightarrow> 'a"
-is "Inf_class.Inf :: ('a :: Inf) set \<Rightarrow> 'a"
-quotient_definition Sup where "Sup :: ('a :: Sup) Cset.set \<Rightarrow> 'a"
-is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a"
-quotient_definition UNION where "UNION :: 'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set"
-is "Complete_Lattices.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
-
-hide_const (open) is_empty insert remove map filter forall exists card
-  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_eq
-
-end
diff -r 13b5fb92b9f5 -r 66823a0066db src/HOL/Quotient_Examples/List_Cset.thy
--- a/src/HOL/Quotient_Examples/List_Cset.thy	Tue Oct 25 16:09:02 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,191 +0,0 @@
-(*  Title:      HOL/Quotient_Examples/List_Cset.thy
-    Author:     Florian Haftmann, Alexander Krauss, TU Muenchen
-*)
-
-header {* Implementation of type Cset.set based on lists. Code equations obtained via quotient lifting. *}
-
-theory List_Cset
-imports Cset
-begin
-
-lemma [quot_respect]: "((op = ===> set_eq ===> set_eq) ===> op = ===> set_eq ===> set_eq)
-  foldr foldr"
-by (simp add: fun_rel_eq)
-
-lemma [quot_preserve]: "((id ---> abs_set ---> rep_set) ---> id ---> rep_set ---> abs_set) foldr = foldr"
-apply (rule ext)+
-by (induct_tac xa) (auto simp: Quotient_abs_rep[OF Quotient_set])
-
-
-subsection {* Relationship to lists *}
-
-(*FIXME: maybe define on sets first and then lift -> more canonical*)
-definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
-  "coset xs = Cset.uminus (Cset.set xs)"
-
-code_datatype Cset.set List_Cset.coset
-
-lemma member_code [code]:
-  "member x (Cset.set xs) \<longleftrightarrow> List.member xs x"
-  "member x (coset xs) \<longleftrightarrow> \<not> List.member xs x"
-unfolding coset_def
-apply (lifting in_set_member)
-by descending (simp add: in_set_member)
-
-definition (in term_syntax)
-  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
-    \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
-  [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
-
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-instantiation Cset.set :: (random) random
-begin
-
-definition
-  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
-
-instance ..
-
-end
-
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-subsection {* Basic operations *}
-
-lemma is_empty_set [code]:
-  "Cset.is_empty (Cset.set xs) \<longleftrightarrow> List.null xs"
-  by (lifting is_empty_set)
-hide_fact (open) is_empty_set
-
-lemma empty_set [code]:
-  "Cset.empty = Cset.set []"
-  by (lifting set.simps(1)[symmetric])
-hide_fact (open) empty_set
-
-lemma UNIV_set [code]:
-  "Cset.UNIV = coset []"
-  unfolding coset_def by descending simp
-hide_fact (open) UNIV_set
-
-lemma remove_set [code]:
-  "Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)"
-  "Cset.remove x (coset xs) = coset (List.insert x xs)"
-unfolding coset_def
-apply descending
-apply (simp add: More_Set.remove_def)
-apply descending
-by (simp add: remove_set_compl)
-
-lemma insert_set [code]:
-  "Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)"
-  "Cset.insert x (coset xs) = coset (removeAll x xs)"
-unfolding coset_def
-apply (lifting set_insert[symmetric])
-by descending simp
-
-lemma map_set [code]:
-  "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
-by descending simp
-
-lemma filter_set [code]:
-  "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)"
-by descending (simp add: project_set)
-
-lemma forall_set [code]:
-  "Cset.forall (Cset.set xs) P \<longleftrightarrow> list_all P xs"
-(* FIXME: why does (lifting Ball_set_list_all) fail? *)
-by descending (fact Ball_set_list_all)
-
-lemma exists_set [code]:
-  "Cset.exists (Cset.set xs) P \<longleftrightarrow> list_ex P xs"
-by descending (fact Bex_set_list_ex)
-
-lemma card_set [code]:
-  "Cset.card (Cset.set xs) = length (remdups xs)"
-by (lifting length_remdups_card_conv[symmetric])
-
-lemma compl_set [simp, code]:
-  "Cset.uminus (Cset.set xs) = coset xs"
-unfolding coset_def by descending simp
-
-lemma compl_coset [simp, code]:
-  "Cset.uminus (coset xs) = Cset.set xs"
-unfolding coset_def by descending simp
-
-lemma Inf_inf [code]:
-  "Cset.Inf (Cset.set (xs\<Colon>'a\<Colon>complete_lattice list)) = foldr inf xs top"
-  "Cset.Inf (coset ([]\<Colon>'a\<Colon>complete_lattice list)) = bot"
-  unfolding List_Cset.UNIV_set[symmetric]
-  by (lifting Inf_set_foldr Inf_UNIV)
-
-lemma Sup_sup [code]:
-  "Cset.Sup (Cset.set (xs\<Colon>'a\<Colon>complete_lattice list)) = foldr sup xs bot"
-  "Cset.Sup (coset ([]\<Colon>'a\<Colon>complete_lattice list)) = top"
-  unfolding List_Cset.UNIV_set[symmetric]
-  by (lifting Sup_set_foldr Sup_UNIV)
-
-subsection {* Derived operations *}
-
-lemma subset_eq_forall [code]:
-  "Cset.subset A B \<longleftrightarrow> Cset.forall A (\<lambda>x. member x B)"
-by descending blast
-
-lemma subset_subset_eq [code]:
-  "Cset.psubset A B \<longleftrightarrow> Cset.subset A B \<and> \<not> Cset.subset B A"
-by descending blast
-
-instantiation Cset.set :: (type) equal
-begin
-
-definition [code]:
-  "HOL.equal A B \<longleftrightarrow> Cset.subset A B \<and> Cset.subset B A"
-
-instance
-apply intro_classes
-unfolding equal_set_def
-by descending auto
-
-end
-
-lemma [code nbe]:
-  "HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
-  by (fact equal_refl)
-
-
-subsection {* Functorial operations *}
-
-lemma inter_project [code]:
-  "Cset.inter A (Cset.set xs) = Cset.set (List.filter (\<lambda>x. Cset.member x A) xs)"
-  "Cset.inter A (coset xs) = foldr Cset.remove xs A"
-apply descending
-apply auto
-unfolding coset_def
-apply descending
-apply simp
-by (metis diff_eq minus_set_foldr)
-
-lemma subtract_remove [code]:
-  "Cset.minus A (Cset.set xs) = foldr Cset.remove xs A"
-  "Cset.minus A (coset xs) = Cset.set (List.filter (\<lambda>x. member x A) xs)"
-unfolding coset_def
-apply (lifting minus_set_foldr)
-by descending auto
-
-lemma union_insert [code]:
-  "Cset.union (Cset.set xs) A = foldr Cset.insert xs A"
-  "Cset.union (coset xs) A = coset (List.filter (\<lambda>x. \<not> member x A) xs)"
-unfolding coset_def
-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
diff -r 13b5fb92b9f5 -r 66823a0066db src/HOL/Quotient_Examples/List_Quotient_Set.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/List_Quotient_Set.thy	Tue Oct 25 16:37:11 2011 +0200
@@ -0,0 +1,191 @@
+(*  Title:      HOL/Quotient_Examples/List_Quotient_Set.thy
+    Author:     Florian Haftmann, Alexander Krauss, TU Muenchen
+*)
+
+header {* Implementation of type Quotient_Set.set based on lists. Code equations obtained via quotient lifting. *}
+
+theory List_Quotient_Set
+imports Quotient_Set
+begin
+
+lemma [quot_respect]: "((op = ===> set_eq ===> set_eq) ===> op = ===> set_eq ===> set_eq)
+  foldr foldr"
+by (simp add: fun_rel_eq)
+
+lemma [quot_preserve]: "((id ---> abs_set ---> rep_set) ---> id ---> rep_set ---> abs_set) foldr = foldr"
+apply (rule ext)+
+by (induct_tac xa) (auto simp: Quotient_abs_rep[OF Quotient_set])
+
+
+subsection {* Relationship to lists *}
+
+(*FIXME: maybe define on sets first and then lift -> more canonical*)
+definition coset :: "'a list \<Rightarrow> 'a Quotient_Set.set" where
+  "coset xs = Quotient_Set.uminus (Quotient_Set.set xs)"
+
+code_datatype Quotient_Set.set List_Quotient_Set.coset
+
+lemma member_code [code]:
+  "member x (Quotient_Set.set xs) \<longleftrightarrow> List.member xs x"
+  "member x (coset xs) \<longleftrightarrow> \<not> List.member xs x"
+unfolding coset_def
+apply (lifting in_set_member)
+by descending (simp add: in_set_member)
+
+definition (in term_syntax)
+  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
+    \<Rightarrow> 'a Quotient_Set.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
+  [code_unfold]: "setify xs = Code_Evaluation.valtermify Quotient_Set.set {\<cdot>} xs"
+
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
+
+instantiation Quotient_Set.set :: (random) random
+begin
+
+definition
+  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+
+subsection {* Basic operations *}
+
+lemma is_empty_set [code]:
+  "Quotient_Set.is_empty (Quotient_Set.set xs) \<longleftrightarrow> List.null xs"
+  by (lifting is_empty_set)
+hide_fact (open) is_empty_set
+
+lemma empty_set [code]:
+  "Quotient_Set.empty = Quotient_Set.set []"
+  by (lifting set.simps(1)[symmetric])
+hide_fact (open) empty_set
+
+lemma UNIV_set [code]:
+  "Quotient_Set.UNIV = coset []"
+  unfolding coset_def by descending simp
+hide_fact (open) UNIV_set
+
+lemma remove_set [code]:
+  "Quotient_Set.remove x (Quotient_Set.set xs) = Quotient_Set.set (removeAll x xs)"
+  "Quotient_Set.remove x (coset xs) = coset (List.insert x xs)"
+unfolding coset_def
+apply descending
+apply (simp add: More_Set.remove_def)
+apply descending
+by (simp add: remove_set_compl)
+
+lemma insert_set [code]:
+  "Quotient_Set.insert x (Quotient_Set.set xs) = Quotient_Set.set (List.insert x xs)"
+  "Quotient_Set.insert x (coset xs) = coset (removeAll x xs)"
+unfolding coset_def
+apply (lifting set_insert[symmetric])
+by descending simp
+
+lemma map_set [code]:
+  "Quotient_Set.map f (Quotient_Set.set xs) = Quotient_Set.set (remdups (List.map f xs))"
+by descending simp
+
+lemma filter_set [code]:
+  "Quotient_Set.filter P (Quotient_Set.set xs) = Quotient_Set.set (List.filter P xs)"
+by descending (simp add: project_set)
+
+lemma forall_set [code]:
+  "Quotient_Set.forall (Quotient_Set.set xs) P \<longleftrightarrow> list_all P xs"
+(* FIXME: why does (lifting Ball_set_list_all) fail? *)
+by descending (fact Ball_set_list_all)
+
+lemma exists_set [code]:
+  "Quotient_Set.exists (Quotient_Set.set xs) P \<longleftrightarrow> list_ex P xs"
+by descending (fact Bex_set_list_ex)
+
+lemma card_set [code]:
+  "Quotient_Set.card (Quotient_Set.set xs) = length (remdups xs)"
+by (lifting length_remdups_card_conv[symmetric])
+
+lemma compl_set [simp, code]:
+  "Quotient_Set.uminus (Quotient_Set.set xs) = coset xs"
+unfolding coset_def by descending simp
+
+lemma compl_coset [simp, code]:
+  "Quotient_Set.uminus (coset xs) = Quotient_Set.set xs"
+unfolding coset_def by descending simp
+
+lemma Inf_inf [code]:
+  "Quotient_Set.Inf (Quotient_Set.set (xs\<Colon>'a\<Colon>complete_lattice list)) = foldr inf xs top"
+  "Quotient_Set.Inf (coset ([]\<Colon>'a\<Colon>complete_lattice list)) = bot"
+  unfolding List_Quotient_Set.UNIV_set[symmetric]
+  by (lifting Inf_set_foldr Inf_UNIV)
+
+lemma Sup_sup [code]:
+  "Quotient_Set.Sup (Quotient_Set.set (xs\<Colon>'a\<Colon>complete_lattice list)) = foldr sup xs bot"
+  "Quotient_Set.Sup (coset ([]\<Colon>'a\<Colon>complete_lattice list)) = top"
+  unfolding List_Quotient_Set.UNIV_set[symmetric]
+  by (lifting Sup_set_foldr Sup_UNIV)
+
+subsection {* Derived operations *}
+
+lemma subset_eq_forall [code]:
+  "Quotient_Set.subset A B \<longleftrightarrow> Quotient_Set.forall A (\<lambda>x. member x B)"
+by descending blast
+
+lemma subset_subset_eq [code]:
+  "Quotient_Set.psubset A B \<longleftrightarrow> Quotient_Set.subset A B \<and> \<not> Quotient_Set.subset B A"
+by descending blast
+
+instantiation Quotient_Set.set :: (type) equal
+begin
+
+definition [code]:
+  "HOL.equal A B \<longleftrightarrow> Quotient_Set.subset A B \<and> Quotient_Set.subset B A"
+
+instance
+apply intro_classes
+unfolding equal_set_def
+by descending auto
+
+end
+
+lemma [code nbe]:
+  "HOL.equal (A :: 'a Quotient_Set.set) A \<longleftrightarrow> True"
+  by (fact equal_refl)
+
+
+subsection {* Functorial operations *}
+
+lemma inter_project [code]:
+  "Quotient_Set.inter A (Quotient_Set.set xs) = Quotient_Set.set (List.filter (\<lambda>x. Quotient_Set.member x A) xs)"
+  "Quotient_Set.inter A (coset xs) = foldr Quotient_Set.remove xs A"
+apply descending
+apply auto
+unfolding coset_def
+apply descending
+apply simp
+by (metis diff_eq minus_set_foldr)
+
+lemma subtract_remove [code]:
+  "Quotient_Set.minus A (Quotient_Set.set xs) = foldr Quotient_Set.remove xs A"
+  "Quotient_Set.minus A (coset xs) = Quotient_Set.set (List.filter (\<lambda>x. member x A) xs)"
+unfolding coset_def
+apply (lifting minus_set_foldr)
+by descending auto
+
+lemma union_insert [code]:
+  "Quotient_Set.union (Quotient_Set.set xs) A = foldr Quotient_Set.insert xs A"
+  "Quotient_Set.union (coset xs) A = coset (List.filter (\<lambda>x. \<not> member x A) xs)"
+unfolding coset_def
+apply (lifting union_set_foldr)
+by descending auto
+
+lemma UNION_code [code]:
+  "Quotient_Set.UNION (Quotient_Set.set []) f = Quotient_Set.set []"
+  "Quotient_Set.UNION (Quotient_Set.set (x#xs)) f =
+     Quotient_Set.union (f x) (Quotient_Set.UNION (Quotient_Set.set xs) f)"
+  by (descending, simp)+
+
+
+end
diff -r 13b5fb92b9f5 -r 66823a0066db src/HOL/Quotient_Examples/Quotient_Set.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/Quotient_Set.thy	Tue Oct 25 16:37:11 2011 +0200
@@ -0,0 +1,102 @@
+(*  Title:      HOL/Quotient_Examples/Quotient_Set.thy
+    Author:     Florian Haftmann, Alexander Krauss, TU Muenchen
+*)
+
+header {* A variant of theory Cset from Library, defined as a quotient *}
+
+theory Quotient_Set
+imports "~~/src/HOL/Library/More_Set" "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Quotient_Syntax"
+begin
+
+subsection {* Lifting *}
+
+(*FIXME: quotient package requires a dedicated constant*)
+definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+where [simp]: "set_eq \<equiv> op ="
+
+quotient_type 'a set = "'a Set.set" / "set_eq"
+by (simp add: identity_equivp)
+
+hide_type (open) set
+
+subsection {* Operations *}
+
+lemma [quot_respect]:
+  "(op = ===> set_eq ===> op =) (op \<in>) (op \<in>)"
+  "(op = ===> set_eq) Collect Collect"
+  "(set_eq ===> op =) More_Set.is_empty More_Set.is_empty"
+  "(op = ===> set_eq ===> set_eq) Set.insert Set.insert"
+  "(op = ===> set_eq ===> set_eq) More_Set.remove More_Set.remove"
+  "(op = ===> set_eq ===> set_eq) image image"
+  "(op = ===> set_eq ===> set_eq) More_Set.project More_Set.project"
+  "(set_eq ===> op =) Ball Ball"
+  "(set_eq ===> op =) Bex Bex"
+  "(set_eq ===> op =) Finite_Set.card Finite_Set.card"
+  "(set_eq ===> set_eq ===> op =) (op \<subseteq>) (op \<subseteq>)"
+  "(set_eq ===> set_eq ===> op =) (op \<subset>) (op \<subset>)"
+  "(set_eq ===> set_eq ===> set_eq) (op \<inter>) (op \<inter>)"
+  "(set_eq ===> set_eq ===> set_eq) (op \<union>) (op \<union>)"
+  "set_eq {} {}"
+  "set_eq UNIV UNIV"
+  "(set_eq ===> set_eq) uminus uminus"
+  "(set_eq ===> set_eq ===> set_eq) minus minus"
+  "(set_eq ===> op =) Inf Inf"
+  "(set_eq ===> op =) 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 Quotient_Set.set => bool"
+is "op \<in>"
+quotient_definition "Set :: ('a => bool) => 'a Quotient_Set.set"
+is Collect
+quotient_definition is_empty where "is_empty :: 'a Quotient_Set.set \<Rightarrow> bool"
+is More_Set.is_empty
+quotient_definition insert where "insert :: 'a \<Rightarrow> 'a Quotient_Set.set \<Rightarrow> 'a Quotient_Set.set"
+is Set.insert
+quotient_definition remove where "remove :: 'a \<Rightarrow> 'a Quotient_Set.set \<Rightarrow> 'a Quotient_Set.set"
+is More_Set.remove
+quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a Quotient_Set.set \<Rightarrow> 'b Quotient_Set.set"
+is image
+quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a Quotient_Set.set \<Rightarrow> 'a Quotient_Set.set"
+is More_Set.project
+quotient_definition "forall :: 'a Quotient_Set.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+is Ball
+quotient_definition "exists :: 'a Quotient_Set.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+is Bex
+quotient_definition card where "card :: 'a Quotient_Set.set \<Rightarrow> nat"
+is Finite_Set.card
+quotient_definition set where "set :: 'a list => 'a Quotient_Set.set"
+is List.set
+quotient_definition subset where "subset :: 'a Quotient_Set.set \<Rightarrow> 'a Quotient_Set.set \<Rightarrow> bool"
+is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+quotient_definition psubset where "psubset :: 'a Quotient_Set.set \<Rightarrow> 'a Quotient_Set.set \<Rightarrow> bool"
+is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+quotient_definition inter where "inter :: 'a Quotient_Set.set \<Rightarrow> 'a Quotient_Set.set \<Rightarrow> 'a Quotient_Set.set"
+is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+quotient_definition union where "union :: 'a Quotient_Set.set \<Rightarrow> 'a Quotient_Set.set \<Rightarrow> 'a Quotient_Set.set"
+is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+quotient_definition empty where "empty :: 'a Quotient_Set.set"
+is "{} :: 'a set"
+quotient_definition UNIV where "UNIV :: 'a Quotient_Set.set"
+is "Set.UNIV :: 'a set"
+quotient_definition uminus where "uminus :: 'a Quotient_Set.set \<Rightarrow> 'a Quotient_Set.set"
+is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set"
+quotient_definition minus where "minus :: 'a Quotient_Set.set \<Rightarrow> 'a Quotient_Set.set \<Rightarrow> 'a Quotient_Set.set"
+is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+quotient_definition Inf where "Inf :: ('a :: Inf) Quotient_Set.set \<Rightarrow> 'a"
+is "Inf_class.Inf :: ('a :: Inf) set \<Rightarrow> 'a"
+quotient_definition Sup where "Sup :: ('a :: Sup) Quotient_Set.set \<Rightarrow> 'a"
+is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a"
+quotient_definition UNION where "UNION :: 'a Quotient_Set.set \<Rightarrow> ('a \<Rightarrow> 'b Quotient_Set.set) \<Rightarrow> 'b Quotient_Set.set"
+is "Complete_Lattices.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
+
+hide_const (open) is_empty insert remove map filter forall exists card
+  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_eq
+
+end
diff -r 13b5fb92b9f5 -r 66823a0066db src/HOL/Quotient_Examples/ROOT.ML
--- a/src/HOL/Quotient_Examples/ROOT.ML	Tue Oct 25 16:09:02 2011 +0200
+++ b/src/HOL/Quotient_Examples/ROOT.ML	Tue Oct 25 16:37:11 2011 +0200
@@ -4,5 +4,5 @@
 Testing the quotient package.
 *)
 
-use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Cset", "List_Cset"];
+use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Set", "List_Quotient_Set"];