equal
deleted
inserted
replaced
254 |
254 |
255 lemma concat_rsp[quot_respect]: |
255 lemma concat_rsp[quot_respect]: |
256 shows "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> op \<approx>) concat concat" |
256 shows "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> op \<approx>) concat concat" |
257 sorry |
257 sorry |
258 |
258 |
259 lemma nil_rsp2: "(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 sledgehammer |
|
261 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) |
262 atp_minimize [atp=remote_vampire] FSet3.nil_rsp list_rel.simps(1) pred_comp.intros |
261 done |
263 thm pred_comp_def |
|
264 |
262 |
265 lemma fconcat_empty: |
263 lemma fconcat_empty: |
266 shows "fconcat {||} = {||}" |
264 shows "fconcat {||} = {||}" |
267 apply(lifting_setup concat1) |
265 apply(lifting_setup concat1) |
268 apply(regularize) |
266 apply(regularize) |
283 prefer 3 |
281 prefer 3 |
284 apply(rule rep_abs_rsp[of _ "((map rep_fset \<circ> rep_fset) ---> abs_fset)" "(abs_fset \<circ> map abs_fset) ---> rep_fset"]) |
282 apply(rule rep_abs_rsp[of _ "((map rep_fset \<circ> rep_fset) ---> abs_fset)" "(abs_fset \<circ> map abs_fset) ---> rep_fset"]) |
285 prefer 2 |
283 prefer 2 |
286 apply(rule concat_rsp) |
284 apply(rule concat_rsp) |
287 prefer 3 |
285 prefer 3 |
288 thm nil_rsp |
286 apply(injection) |
289 apply(tactic {* rep_abs_rsp_tac @{context} 1 *}) |
287 prefer 2 |
290 apply(rule rep_abs_rsp) |
288 apply(thin_tac "Quot_True {||}") |
|
289 apply(unfold Quotient_def) |
|
290 |
|
291 apply(auto) |
291 sorry |
292 sorry |
292 |
293 |
293 lemma fconcat_insert: |
294 lemma fconcat_insert: |
294 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
295 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
295 apply(lifting concat2) |
296 apply(lifting concat2) |