equal
deleted
inserted
replaced
2287 context |
2287 context |
2288 begin |
2288 begin |
2289 interpretation lifting_syntax . |
2289 interpretation lifting_syntax . |
2290 |
2290 |
2291 lemma set_of_transfer[transfer_rule]: "(pcr_multiset op = ===> op =) (\<lambda>f. {a. 0 < f a}) set_of" |
2291 lemma set_of_transfer[transfer_rule]: "(pcr_multiset op = ===> op =) (\<lambda>f. {a. 0 < f a}) set_of" |
2292 unfolding set_of_def pcr_multiset_def cr_multiset_def fun_rel_def by auto |
2292 unfolding set_of_def pcr_multiset_def cr_multiset_def rel_fun_def by auto |
2293 |
2293 |
2294 end |
2294 end |
2295 |
2295 |
2296 lemma set_of_mmap: "set_of o mmap h = image h o set_of" |
2296 lemma set_of_mmap: "set_of o mmap h = image h o set_of" |
2297 proof (rule ext, unfold comp_apply) |
2297 proof (rule ext, unfold comp_apply) |