258 |
258 |
259 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) [] []" |
259 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) [] []" |
260 apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros) |
260 apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros) |
261 done |
261 done |
262 |
262 |
|
263 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B" |
|
264 apply (rule eq_reflection) |
|
265 apply auto |
|
266 done |
|
267 |
|
268 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba" |
|
269 unfolding list_eq.simps |
|
270 apply(simp only: set_map set_in_eq) |
|
271 done |
|
272 |
|
273 lemma quotient_compose_list_pre: |
|
274 "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) r s = |
|
275 ((list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) r r \<and> |
|
276 (list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) s s \<and> |
|
277 abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" |
|
278 apply rule |
|
279 apply rule |
|
280 apply rule |
|
281 apply (rule list_rel_refl) |
|
282 apply (metis equivp_def fset_equivp) |
|
283 apply rule |
|
284 apply (rule equivp_reflp[OF fset_equivp]) |
|
285 apply (rule list_rel_refl) |
|
286 apply (metis equivp_def fset_equivp) |
|
287 apply(rule) |
|
288 apply rule |
|
289 apply (rule list_rel_refl) |
|
290 apply (metis equivp_def fset_equivp) |
|
291 apply rule |
|
292 apply (rule equivp_reflp[OF fset_equivp]) |
|
293 apply (rule list_rel_refl) |
|
294 apply (metis equivp_def fset_equivp) |
|
295 apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s") |
|
296 apply (metis Quotient_rel[OF Quotient_fset]) |
|
297 apply (auto simp only:)[1] |
|
298 apply (subgoal_tac "map abs_fset r = map abs_fset b") |
|
299 prefer 2 |
|
300 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
|
301 apply (subgoal_tac "map abs_fset s = map abs_fset ba") |
|
302 prefer 2 |
|
303 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
|
304 apply (simp only: map_rel_cong) |
|
305 apply rule |
|
306 apply (rule rep_abs_rsp[of "list_rel op \<approx>" "map abs_fset"]) |
|
307 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
|
308 apply (rule list_rel_refl) |
|
309 apply (metis equivp_def fset_equivp) |
|
310 apply rule |
|
311 prefer 2 |
|
312 apply (rule rep_abs_rsp_left[of "list_rel op \<approx>" "map abs_fset"]) |
|
313 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
|
314 apply (rule list_rel_refl) |
|
315 apply (metis equivp_def fset_equivp) |
|
316 apply (erule conjE)+ |
|
317 apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s") |
|
318 prefer 2 |
|
319 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp) |
|
320 apply (rule map_rel_cong) |
|
321 apply (assumption) |
|
322 done |
|
323 |
|
324 lemma quotient_compose_list[quot_thm]: |
|
325 shows "Quotient ((list_rel op \<approx>) OO (op \<approx>) OO (list_rel op \<approx>)) |
|
326 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
|
327 unfolding Quotient_def comp_def |
|
328 apply (rule)+ |
|
329 apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset]) |
|
330 apply (rule) |
|
331 apply (rule) |
|
332 apply (rule) |
|
333 apply (rule list_rel_refl) |
|
334 apply (metis equivp_def fset_equivp) |
|
335 apply (rule) |
|
336 apply (rule equivp_reflp[OF fset_equivp]) |
|
337 apply (rule list_rel_refl) |
|
338 apply (metis equivp_def fset_equivp) |
|
339 apply rule |
|
340 apply rule |
|
341 apply(rule quotient_compose_list_pre) |
|
342 done |
|
343 |
263 lemma fconcat_empty: |
344 lemma fconcat_empty: |
264 shows "fconcat {||} = {||}" |
345 shows "fconcat {||} = {||}" |
265 apply(lifting_setup concat1) |
346 apply(lifting concat1) |
266 apply(regularize) |
|
267 defer |
|
268 apply(cleaning) |
347 apply(cleaning) |
269 apply(simp add: comp_def) |
348 apply(simp add: comp_def) |
270 apply(cleaning) |
|
271 apply(fold fempty_def[simplified id_simps]) |
349 apply(fold fempty_def[simplified id_simps]) |
272 apply(rule refl) |
350 apply(rule refl) |
273 apply(injection) |
351 done |
274 apply(rule apply_rsp[of "(list_rel (op \<approx>)) OO (op \<approx>) OO (list_rel (op \<approx>))" _ _ "op \<approx>" "concat" _ "[]" "((map rep_fset \<circ> rep_fset) ((abs_fset \<circ> map abs_fset) []))"]) |
|
275 prefer 2 |
|
276 ML_prf {* fun dest_comb (f $ a) = (f, a) *} |
|
277 apply(tactic {* Quotient_Tacs.quot_true_tac @{context} (fst o dest_comb) 1 *}) |
|
278 prefer 3 |
|
279 apply(tactic {* Quotient_Tacs.quot_true_tac @{context} (snd o dest_comb) 1 *}) |
|
280 apply(rule rep_abs_rsp[of _ "(abs_fset \<circ> map abs_fset)" "(map rep_fset \<circ> rep_fset)"]) |
|
281 prefer 3 |
|
282 apply(rule rep_abs_rsp[of _ "((map rep_fset \<circ> rep_fset) ---> abs_fset)" "(abs_fset \<circ> map abs_fset) ---> rep_fset"]) |
|
283 prefer 2 |
|
284 apply(rule concat_rsp) |
|
285 prefer 3 |
|
286 apply(injection) |
|
287 prefer 2 |
|
288 apply(thin_tac "Quot_True {||}") |
|
289 apply(unfold Quotient_def) |
|
290 |
|
291 apply(auto) |
|
292 sorry |
|
293 |
352 |
294 lemma fconcat_insert: |
353 lemma fconcat_insert: |
295 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
354 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
296 apply(lifting concat2) |
355 apply(lifting concat2) |
297 apply(injection) |
356 apply(injection) |