87 by descending simp |
87 by descending simp |
88 |
88 |
89 lemma map_set [code]: |
89 lemma map_set [code]: |
90 "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))" |
90 "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))" |
91 by descending simp |
91 by descending simp |
92 |
92 |
93 lemma filter_set [code]: |
93 lemma filter_set [code]: |
94 "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)" |
94 "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)" |
95 by descending (simp add: project_set) |
95 by descending (simp add: project_set) |
96 |
96 |
97 lemma forall_set [code]: |
97 lemma forall_set [code]: |
113 |
113 |
114 lemma compl_coset [simp, code]: |
114 lemma compl_coset [simp, code]: |
115 "Cset.uminus (coset xs) = Cset.set xs" |
115 "Cset.uminus (coset xs) = Cset.set xs" |
116 unfolding coset_def by descending simp |
116 unfolding coset_def by descending simp |
117 |
117 |
118 context complete_lattice |
118 lemma Inf_inf [code]: |
119 begin |
119 "Cset.Inf (Cset.set (xs\<Colon>'a\<Colon>complete_lattice list)) = foldr inf xs top" |
|
120 "Cset.Inf (coset ([]\<Colon>'a\<Colon>complete_lattice list)) = bot" |
|
121 unfolding List_Cset.UNIV_set[symmetric] |
|
122 by (lifting Inf_set_foldr Inf_UNIV) |
120 |
123 |
121 (* FIXME: automated lifting fails, since @{term inf} and @{term top} |
124 lemma Sup_sup [code]: |
122 are variables (???) *) |
125 "Cset.Sup (Cset.set (xs\<Colon>'a\<Colon>complete_lattice list)) = foldr sup xs bot" |
123 lemma Infimum_inf [code]: |
126 "Cset.Sup (coset ([]\<Colon>'a\<Colon>complete_lattice list)) = top" |
124 "Infimum (Cset.set As) = foldr inf As top" |
127 unfolding List_Cset.UNIV_set[symmetric] |
125 "Infimum (coset []) = bot" |
128 by (lifting Sup_set_foldr Sup_UNIV) |
126 unfolding Infimum_def member_code List.member_def |
|
127 apply (simp add: mem_def Inf_set_foldr) |
|
128 apply (simp add: Inf_UNIV[unfolded UNIV_def Collect_def]) |
|
129 done |
|
130 |
|
131 lemma Supremum_sup [code]: |
|
132 "Supremum (Cset.set As) = foldr sup As bot" |
|
133 "Supremum (coset []) = top" |
|
134 unfolding Supremum_def member_code List.member_def |
|
135 apply (simp add: mem_def Sup_set_foldr) |
|
136 apply (simp add: Sup_UNIV[unfolded UNIV_def Collect_def]) |
|
137 done |
|
138 |
|
139 end |
|
140 |
|
141 |
|
142 |
129 |
143 subsection {* Derived operations *} |
130 subsection {* Derived operations *} |
144 |
131 |
145 lemma subset_eq_forall [code]: |
132 lemma subset_eq_forall [code]: |
146 "Cset.subset A B \<longleftrightarrow> Cset.forall A (\<lambda>x. member x B)" |
133 "Cset.subset A B \<longleftrightarrow> Cset.forall A (\<lambda>x. member x B)" |