author Cezary Kaliszyk Fri, 19 Aug 2011 17:05:10 +0900 changeset 44293 83c4f8ba0aa3 parent 44292 453803d28c4b child 44294 a0ddd5760444 child 44305 3bdc02eb1637 child 44322 43b465f4c480
Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.
--- 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
--- 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)"
@@ -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: 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: 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