# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1313741110 -32400
# Node ID 83c4f8ba0aa328114a1bc0dd2b72a68bf838de33
# Parent  453803d28c4b003d4b1080ef1b3d1c3dda6d00c8
Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.

diff -r 453803d28c4b -r 83c4f8ba0aa3 src/HOL/Quotient_Examples/Cset.thy
--- a/src/HOL/Quotient_Examples/Cset.thy	Thu Aug 18 22:32:19 2011 -0700
+++ b/src/HOL/Quotient_Examples/Cset.thy	Fri Aug 19 17:05:10 2011 +0900
@@ -40,8 +40,8 @@
   "set_eq UNIV UNIV"
   "(set_eq ===> set_eq) uminus uminus"
   "(set_eq ===> set_eq ===> set_eq) minus minus"
-  "((set_eq ===> op =) ===> set_eq) Inf Inf"
-  "((set_eq ===> op =) ===> set_eq) Sup Sup"
+  "(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)
@@ -84,33 +84,13 @@
 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 Cset.set set \<Rightarrow> 'a Cset.set"
-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 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_Lattice.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
 
-
-context complete_lattice
-begin
-
-(* FIXME: Would like to use 
-
-quotient_definition "Infimum :: 'a Cset.set \<Rightarrow> 'a"
-is "Inf"
-
-but it fails, presumably because @{term "Inf"} is a Free.
-*)
-
-definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
-  [simp]: "Infimum A = Inf (\<lambda>x. member x A)"
-
-definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
-  [simp]: "Supremum A = Sup (\<lambda>x. member x A)"
-
-end
-
 hide_const (open) is_empty insert remove map filter forall exists card
   set subset psubset inter union empty UNIV uminus minus Inf Sup UNION
 
@@ -119,5 +99,4 @@
   inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def
   UNION_def
 
-
 end
diff -r 453803d28c4b -r 83c4f8ba0aa3 src/HOL/Quotient_Examples/List_Cset.thy
--- a/src/HOL/Quotient_Examples/List_Cset.thy	Thu Aug 18 22:32:19 2011 -0700
+++ b/src/HOL/Quotient_Examples/List_Cset.thy	Fri Aug 19 17:05:10 2011 +0900
@@ -89,7 +89,7 @@
 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)
@@ -115,30 +115,17 @@
   "Cset.uminus (coset xs) = Cset.set xs"
 unfolding coset_def by descending simp
 
-context complete_lattice
-begin
+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)
 
-(* FIXME: automated lifting fails, since @{term inf} and @{term top}
-  are variables (???) *)
-lemma Infimum_inf [code]:
-  "Infimum (Cset.set As) = foldr inf As top"
-  "Infimum (coset []) = bot"
-unfolding Infimum_def member_code List.member_def
-apply (simp add: mem_def Inf_set_foldr)
-apply (simp add: Inf_UNIV[unfolded UNIV_def Collect_def])
-done
-
-lemma Supremum_sup [code]:
-  "Supremum (Cset.set As) = foldr sup As bot"
-  "Supremum (coset []) = top"
-unfolding Supremum_def member_code List.member_def
-apply (simp add: mem_def Sup_set_foldr)
-apply (simp add: Sup_UNIV[unfolded UNIV_def Collect_def])
-done
-
-end
-
-
+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 *}
 
@@ -201,4 +188,4 @@
   by (descending, simp)+
 
 
-end
\ No newline at end of file
+end