154 unfolding cr_fset'_def |
154 unfolding cr_fset'_def |
155 apply (intro fun_relI) |
155 apply (intro fun_relI) |
156 apply (elim relcomppE) |
156 apply (elim relcomppE) |
157 apply (rule relcomppI) |
157 apply (rule relcomppI) |
158 apply (erule (1) map_transfer [THEN fun_relD, THEN fun_relD]) |
158 apply (erule (1) map_transfer [THEN fun_relD, THEN fun_relD]) |
159 apply (erule fmap.transfer [THEN fun_relD, THEN fun_relD, OF refl]) |
159 apply (erule fmap.transfer [THEN fun_relD, THEN fun_relD, unfolded relator_eq, OF refl]) |
160 done |
160 done |
161 |
161 |
162 lemma ffilter_transfer [transfer_rule]: |
162 lemma ffilter_transfer [transfer_rule]: |
163 "((A ===> op =) ===> cr_fset' A ===> cr_fset' A) filter ffilter" |
163 "((A ===> op =) ===> cr_fset' A ===> cr_fset' A) filter ffilter" |
164 unfolding cr_fset'_def |
164 unfolding cr_fset'_def |
165 apply (intro fun_relI) |
165 apply (intro fun_relI) |
166 apply (elim relcomppE) |
166 apply (elim relcomppE) |
167 apply (rule relcomppI) |
167 apply (rule relcomppI) |
168 apply (erule (1) filter_transfer [THEN fun_relD, THEN fun_relD]) |
168 apply (erule (1) filter_transfer [THEN fun_relD, THEN fun_relD]) |
169 apply (erule ffilter.transfer [THEN fun_relD, THEN fun_relD, OF refl]) |
169 apply (erule ffilter.transfer [THEN fun_relD, THEN fun_relD, unfolded relator_eq, OF refl]) |
170 done |
170 done |
171 |
171 |
172 lemma fset_transfer [transfer_rule]: |
172 lemma fset_transfer [transfer_rule]: |
173 "(cr_fset' A ===> set_rel A) set fset" |
173 "(cr_fset' A ===> set_rel A) set fset" |
174 unfolding cr_fset'_def |
174 unfolding cr_fset'_def |
175 apply (intro fun_relI) |
175 apply (intro fun_relI) |
176 apply (elim relcomppE) |
176 apply (elim relcomppE) |
177 apply (drule fset.transfer [THEN fun_relD]) |
177 apply (drule fset.transfer [THEN fun_relD, unfolded relator_eq]) |
178 apply (erule subst) |
178 apply (erule subst) |
179 apply (erule set_transfer [THEN fun_relD]) |
179 apply (erule set_transfer [THEN fun_relD]) |
180 done |
180 done |
181 |
181 |
182 lemma fconcat_transfer [transfer_rule]: |
182 lemma fconcat_transfer [transfer_rule]: |