equal
deleted
inserted
replaced
192 "Cset.union (coset xs) A = coset (List.filter (\<lambda>x. \<not> member x A) xs)" |
192 "Cset.union (coset xs) A = coset (List.filter (\<lambda>x. \<not> member x A) xs)" |
193 unfolding coset_def |
193 unfolding coset_def |
194 apply (lifting union_set_foldr) |
194 apply (lifting union_set_foldr) |
195 by descending auto |
195 by descending auto |
196 |
196 |
197 end |
197 lemma UNION_code [code]: |
|
198 "Cset.UNION (Cset.set []) f = Cset.set []" |
|
199 "Cset.UNION (Cset.set (x#xs)) f = |
|
200 Cset.union (f x) (Cset.UNION (Cset.set xs) f)" |
|
201 by (descending, simp)+ |
|
202 |
|
203 |
|
204 end |