equal
deleted
inserted
replaced
243 quotient_definition |
243 quotient_definition |
244 "fconcat :: ('a fset) fset => 'a fset" |
244 "fconcat :: ('a fset) fset => 'a fset" |
245 is |
245 is |
246 "concat" |
246 "concat" |
247 |
247 |
248 (*lemma fconcat_rsp[quot_respect]: |
|
249 shows "((list_rel op \<approx>) ===> op \<approx>) concat concat" |
|
250 apply(auto) |
|
251 sorry |
|
252 *) |
|
253 |
|
254 (* PROBLEM: these lemmas needs to be restated, since *) |
248 (* PROBLEM: these lemmas needs to be restated, since *) |
255 (* concat.simps(1) and concat.simps(2) contain the *) |
249 (* concat.simps(1) and concat.simps(2) contain the *) |
256 (* type variables ?'a1.0 (which are turned into frees *) |
250 (* type variables ?'a1.0 (which are turned into frees *) |
257 (* 'a_1 *) |
251 (* 'a_1 *) |
258 lemma concat1: |
252 lemma concat1: |
261 |
255 |
262 lemma concat2: |
256 lemma concat2: |
263 shows "concat (x # xs) \<approx> x @ concat xs" |
257 shows "concat (x # xs) \<approx> x @ concat xs" |
264 by (simp) |
258 by (simp) |
265 |
259 |
266 lemma concat_rsp[quot_respect]: |
260 lemma concat_rsp: |
|
261 "\<lbrakk>list_rel op \<approx> x x'; x' \<approx> y'; list_rel op \<approx> y' y\<rbrakk> \<Longrightarrow> concat x \<approx> concat y" |
|
262 apply (induct x y arbitrary: x' y' rule: list_induct2') |
|
263 apply simp |
|
264 defer defer |
|
265 apply (simp only: concat.simps) |
|
266 sorry |
|
267 |
|
268 lemma [quot_respect]: |
267 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
269 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
268 sorry |
270 apply (simp only: fun_rel_def) |
|
271 apply clarify |
|
272 apply (rule concat_rsp) |
|
273 apply assumption+ |
|
274 done |
269 |
275 |
270 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []" |
276 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []" |
271 apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros) |
277 apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros) |
272 done |
278 done |
273 |
279 |
357 apply(cleaning) |
363 apply(cleaning) |
358 apply(simp add: comp_def) |
364 apply(simp add: comp_def) |
359 apply(fold fempty_def[simplified id_simps]) |
365 apply(fold fempty_def[simplified id_simps]) |
360 apply(rule refl) |
366 apply(rule refl) |
361 done |
367 done |
362 |
|
363 (* Should be true *) |
|
364 |
368 |
365 lemma insert_rsp2[quot_respect]: |
369 lemma insert_rsp2[quot_respect]: |
366 "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #" |
370 "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #" |
367 apply auto |
371 apply auto |
368 apply (simp add: set_in_eq) |
372 apply (simp add: set_in_eq) |
707 (* We also have map and some properties of it in FSet *) |
711 (* We also have map and some properties of it in FSet *) |
708 (* and the following which still lifts ok *) |
712 (* and the following which still lifts ok *) |
709 lemma "funion (funion x xa) xb = funion x (funion xa xb)" |
713 lemma "funion (funion x xa) xb = funion x (funion xa xb)" |
710 by (lifting append_assoc) |
714 by (lifting append_assoc) |
711 |
715 |
712 quotient_definition |
|
713 "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
|
714 is |
|
715 "list_case" |
|
716 |
|
717 (* NOT SURE IF TRUE *) |
|
718 lemma list_case_rsp[quot_respect]: |
|
719 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
|
720 apply (auto) |
|
721 sorry |
|
722 |
|
723 lemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa" |
|
724 apply (lifting list.cases(2)) |
|
725 done |
|
726 |
|
727 end |
716 end |