1.1 --- a/src/HOL/Quotient_Examples/Cset.thy	Thu Aug 18 22:32:19 2011 -0700
     1.2 +++ b/src/HOL/Quotient_Examples/Cset.thy	Fri Aug 19 17:05:10 2011 +0900
     1.3 @@ -40,8 +40,8 @@
     1.4    "set_eq UNIV UNIV"
     1.5    "(set_eq ===> set_eq) uminus uminus"
     1.6    "(set_eq ===> set_eq ===> set_eq) minus minus"
     1.7 -  "((set_eq ===> op =) ===> set_eq) Inf Inf"
     1.8 -  "((set_eq ===> op =) ===> set_eq) Sup Sup"
     1.9 +  "(set_eq ===> op =) Inf Inf"
    1.10 +  "(set_eq ===> op =) Sup Sup"
    1.11    "(op = ===> set_eq) List.set List.set"
    1.12    "(set_eq ===> (op = ===> set_eq) ===> set_eq) UNION UNION"
    1.13  by (auto simp: fun_rel_eq)
    1.14 @@ -84,33 +84,13 @@
    1.15  is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set"
    1.16  quotient_definition minus where "minus :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
    1.17  is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
    1.18 -quotient_definition Inf where "Inf :: 'a Cset.set set \<Rightarrow> 'a Cset.set"
    1.19 -is "Inf_class.Inf :: 'a set set \<Rightarrow> 'a set"
    1.20 -quotient_definition Sup where "Sup :: 'a Cset.set set \<Rightarrow> 'a Cset.set"
    1.21 -is "Sup_class.Sup :: 'a set set \<Rightarrow> 'a set"
    1.22 +quotient_definition Inf where "Inf :: ('a :: Inf) Cset.set \<Rightarrow> 'a"
    1.23 +is "Inf_class.Inf :: ('a :: Inf) set \<Rightarrow> 'a"
    1.24 +quotient_definition Sup where "Sup :: ('a :: Sup) Cset.set \<Rightarrow> 'a"
    1.25 +is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a"
    1.26  quotient_definition UNION where "UNION :: 'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set"
    1.27  is "Complete_Lattice.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
    1.28  
    1.29 -
    1.30 -context complete_lattice
    1.31 -begin
    1.32 -
    1.33 -(* FIXME: Would like to use 
    1.34 -
    1.35 -quotient_definition "Infimum :: 'a Cset.set \<Rightarrow> 'a"
    1.36 -is "Inf"
    1.37 -
    1.38 -but it fails, presumably because @{term "Inf"} is a Free.
    1.39 -*)
    1.40 -
    1.41 -definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
    1.42 -  [simp]: "Infimum A = Inf (\<lambda>x. member x A)"
    1.43 -
    1.44 -definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
    1.45 -  [simp]: "Supremum A = Sup (\<lambda>x. member x A)"
    1.46 -
    1.47 -end
    1.48 -
    1.49  hide_const (open) is_empty insert remove map filter forall exists card
    1.50    set subset psubset inter union empty UNIV uminus minus Inf Sup UNION
    1.51  
    1.52 @@ -119,5 +99,4 @@
    1.53    inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def
    1.54    UNION_def
    1.55  
    1.56 -
    1.57  end

     2.1 --- a/src/HOL/Quotient_Examples/List_Cset.thy	Thu Aug 18 22:32:19 2011 -0700
     2.2 +++ b/src/HOL/Quotient_Examples/List_Cset.thy	Fri Aug 19 17:05:10 2011 +0900
     2.3 @@ -89,7 +89,7 @@
     2.4  lemma map_set [code]:
     2.5    "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
     2.6  by descending simp
     2.7 -  
     2.8 +
     2.9  lemma filter_set [code]:
    2.10    "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)"
    2.11  by descending (simp add: project_set)
    2.12 @@ -115,30 +115,17 @@
    2.13    "Cset.uminus (coset xs) = Cset.set xs"
    2.14  unfolding coset_def by descending simp
    2.15  
    2.16 -context complete_lattice
    2.17 -begin
    2.18 +lemma Inf_inf [code]:
    2.19 +  "Cset.Inf (Cset.set (xs\<Colon>'a\<Colon>complete_lattice list)) = foldr inf xs top"
    2.20 +  "Cset.Inf (coset ([]\<Colon>'a\<Colon>complete_lattice list)) = bot"
    2.21 +  unfolding List_Cset.UNIV_set[symmetric]
    2.22 +  by (lifting Inf_set_foldr Inf_UNIV)
    2.23  
    2.24 -(* FIXME: automated lifting fails, since @{term inf} and @{term top}
    2.25 -  are variables (???) *)
    2.26 -lemma Infimum_inf [code]:
    2.27 -  "Infimum (Cset.set As) = foldr inf As top"
    2.28 -  "Infimum (coset []) = bot"
    2.29 -unfolding Infimum_def member_code List.member_def
    2.30 -apply (simp add: mem_def Inf_set_foldr)
    2.31 -apply (simp add: Inf_UNIV[unfolded UNIV_def Collect_def])
    2.32 -done
    2.33 -
    2.34 -lemma Supremum_sup [code]:
    2.35 -  "Supremum (Cset.set As) = foldr sup As bot"
    2.36 -  "Supremum (coset []) = top"
    2.37 -unfolding Supremum_def member_code List.member_def
    2.38 -apply (simp add: mem_def Sup_set_foldr)
    2.39 -apply (simp add: Sup_UNIV[unfolded UNIV_def Collect_def])
    2.40 -done
    2.41 -
    2.42 -end
    2.43 -
    2.44 -
    2.45 +lemma Sup_sup [code]:
    2.46 +  "Cset.Sup (Cset.set (xs\<Colon>'a\<Colon>complete_lattice list)) = foldr sup xs bot"
    2.47 +  "Cset.Sup (coset ([]\<Colon>'a\<Colon>complete_lattice list)) = top"
    2.48 +  unfolding List_Cset.UNIV_set[symmetric]
    2.49 +  by (lifting Sup_set_foldr Sup_UNIV)
    2.50  
    2.51  subsection {* Derived operations *}
    2.52  
    2.53 @@ -201,4 +188,4 @@
    2.54    by (descending, simp)+
    2.55  
    2.56  
    2.57 -end
    2.58 \ No newline at end of file
    2.59 +end