equal
deleted
inserted
replaced
210 apply (rule list_rel_refl) |
210 apply (rule list_rel_refl) |
211 apply (metis equivp_def fset_equivp) |
211 apply (metis equivp_def fset_equivp) |
212 apply rule |
212 apply rule |
213 apply (rule equivp_reflp[OF fset_equivp]) |
213 apply (rule equivp_reflp[OF fset_equivp]) |
214 apply (rule list_rel_refl) |
214 apply (rule list_rel_refl) |
215 apply (metis equivp_def fset_equivp) |
215 apply (metis equivp_def fset_equivp) |
|
216 thm pred_comp_def |
|
217 term "op OO" |
216 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s") |
218 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s") |
217 apply (metis Quotient_rel[OF Quotient_fset]) |
219 apply (metis Quotient_rel[OF Quotient_fset]) |
218 prefer 2 |
220 prefer 2 |
219 apply rule |
221 apply rule |
220 thm rep_abs_rsp |
222 thm rep_abs_rsp |
227 prefer 2 |
229 prefer 2 |
228 apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"]) |
230 apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"]) |
229 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
231 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
230 apply (rule list_rel_refl) |
232 apply (rule list_rel_refl) |
231 apply (metis equivp_def fset_equivp) |
233 apply (metis equivp_def fset_equivp) |
232 apply auto |
|
233 sorry |
234 sorry |
234 |
235 |
235 lemma bla: |
236 lemma bla: |
236 assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset" |
237 assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset" |
237 and a2: "Quotient r2 abs2 rep2" |
238 and a2: "Quotient r2 abs2 rep2" |
240 unfolding Quotient_def comp_def |
241 unfolding Quotient_def comp_def |
241 apply (rule)+ |
242 apply (rule)+ |
242 apply (simp add: abs_o_rep[OF a2] id_simps Quotient_abs_rep[OF Quotient_fset]) |
243 apply (simp add: abs_o_rep[OF a2] id_simps Quotient_abs_rep[OF Quotient_fset]) |
243 apply (rule) |
244 apply (rule) |
244 apply (rule) |
245 apply (rule) |
245 sledgehammer |
|
246 apply (metis Quotient_def a2 equivp_reflp fset_equivp list_quotient list_rel_rel pred_comp.cases pred_comp.intros rep_fset_def) |
|
247 using a1 |
246 using a1 |
248 apply - |
247 apply - |
249 sorry |
248 sorry |
250 |
249 |
251 lemma bla2: |
250 lemma bla2: |
256 |
255 |
257 thm bla [OF Quotient_fset] |
256 thm bla [OF Quotient_fset] |
258 thm bla2[OF Quotient_fset] |
257 thm bla2[OF Quotient_fset] |
259 |
258 |
260 thm bla [OF Quotient_fset Quotient_fset] |
259 thm bla [OF Quotient_fset Quotient_fset] |
261 thm bla2[OF Quotient_fset Quotient_fset] |
260 (* Doesn't work: *) |
262 |
261 (* thm bla2[OF Quotient_fset Quotient_fset] *) |
263 lemma bla: |
|
264 assumes a1: "Quotient r1 abs1 rep1" |
|
265 and a2: "Quotient r2 abs2 rep2" |
|
266 shows "Quotient r2 (abs1 \<circ> abs2) (rep2 \<circ> rep1)" |
|
267 sorry |
|
268 |
|
269 |
|
270 unfolding Quotient_def |
|
271 apply auto |
|
272 term rep_fset |
|
273 |
|
274 lemma |
|
275 assumes sr: "equivp r" |
|
276 and ss: "equivp s" |
|
277 shows "r OO s = s OO r" |
|
278 apply(rule ext) |
|
279 apply(rule ext) |
|
280 using sr ss |
|
281 nitpick |
|
282 |
|
283 apply(auto) |
|
284 apply(rule pred_compI) |
|
285 |
|
286 definition |
|
287 relation_compose |
|
288 where |
|
289 "relation_compose R1 R2 = \<lambda>x y. \<exists> z. (R1 x z \<and> R2 z y)" |
|
290 |
|
291 |
|
292 |
262 |
293 end |
263 end |