232 quotient_definition |
232 quotient_definition |
233 "fconcat :: ('a fset) fset => 'a fset" |
233 "fconcat :: ('a fset) fset => 'a fset" |
234 as |
234 as |
235 "concat" |
235 "concat" |
236 |
236 |
237 lemma fconcat_rsp[quot_respect]: |
237 (*lemma fconcat_rsp[quot_respect]: |
238 shows "((list_rel op \<approx>) ===> op \<approx>) concat concat" |
238 shows "((list_rel op \<approx>) ===> op \<approx>) concat concat" |
239 apply(auto) |
239 apply(auto) |
240 sorry |
240 sorry |
|
241 *) |
241 |
242 |
242 (* PROBLEM: these lemmas needs to be restated, since *) |
243 (* PROBLEM: these lemmas needs to be restated, since *) |
243 (* concat.simps(1) and concat.simps(2) contain the *) |
244 (* concat.simps(1) and concat.simps(2) contain the *) |
244 (* type variables ?'a1.0 (which are turned into frees *) |
245 (* type variables ?'a1.0 (which are turned into frees *) |
245 (* 'a_1 *) |
246 (* 'a_1 *) |
249 |
250 |
250 lemma concat2: |
251 lemma concat2: |
251 shows "concat (x # xs) \<approx> x @ concat xs" |
252 shows "concat (x # xs) \<approx> x @ concat xs" |
252 by (simp) |
253 by (simp) |
253 |
254 |
|
255 lemma concat_rsp[quot_respect]: |
|
256 shows "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> op \<approx>) concat concat" |
|
257 sorry |
|
258 |
|
259 lemma nil_rsp2: "(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) |
|
262 atp_minimize [atp=remote_vampire] FSet3.nil_rsp list_rel.simps(1) pred_comp.intros |
|
263 thm pred_comp_def |
|
264 |
254 lemma fconcat_empty: |
265 lemma fconcat_empty: |
255 shows "fconcat {||} = {||}" |
266 shows "fconcat {||} = {||}" |
256 apply(lifting_setup concat1) |
267 apply(lifting_setup concat1) |
257 apply(regularize) |
268 apply(regularize) |
258 apply(injection) |
|
259 defer |
269 defer |
260 apply(cleaning) |
270 apply(cleaning) |
261 apply(simp add: comp_def) |
271 apply(simp add: comp_def) |
262 apply(cleaning) |
272 apply(cleaning) |
263 apply(fold fempty_def[simplified id_simps]) |
273 apply(fold fempty_def[simplified id_simps]) |
264 apply(rule refl) |
274 apply(rule refl) |
|
275 apply(injection) |
|
276 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) []))"]) |
|
277 prefer 2 |
|
278 ML_prf {* fun dest_comb (f $ a) = (f, a) *} |
|
279 apply(tactic {* Quotient_Tacs.quot_true_tac @{context} (fst o dest_comb) 1 *}) |
|
280 prefer 3 |
|
281 apply(tactic {* Quotient_Tacs.quot_true_tac @{context} (snd o dest_comb) 1 *}) |
|
282 apply(rule rep_abs_rsp[of _ "(abs_fset \<circ> map abs_fset)" "(map rep_fset \<circ> rep_fset)"]) |
|
283 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"]) |
|
285 prefer 2 |
|
286 apply(rule concat_rsp) |
|
287 prefer 3 |
|
288 thm nil_rsp |
|
289 apply(tactic {* rep_abs_rsp_tac @{context} 1 *}) |
|
290 apply(rule rep_abs_rsp) |
265 sorry |
291 sorry |
266 |
292 |
267 lemma fconcat_insert: |
293 lemma fconcat_insert: |
268 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
294 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
269 apply(lifting concat2) |
295 apply(lifting concat2) |