equal
deleted
inserted
replaced
274 "(map f (a @ b)) \<approx> (map f a) @ (map f b)" |
274 "(map f (a @ b)) \<approx> (map f a) @ (map f b)" |
275 by simp (rule list_eq_refl) |
275 by simp (rule list_eq_refl) |
276 |
276 |
277 lemma ho_fold_rsp[quotient_rsp]: |
277 lemma ho_fold_rsp[quotient_rsp]: |
278 "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1" |
278 "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1" |
279 apply (auto simp add: FUN_REL_EQ) |
279 apply (auto) |
280 apply (case_tac "rsp_fold x") |
280 apply (case_tac "rsp_fold x") |
281 prefer 2 |
281 prefer 2 |
282 apply (erule_tac list_eq.induct) |
282 apply (erule_tac list_eq.induct) |
283 apply (simp_all) |
283 apply (simp_all) |
284 apply (erule_tac list_eq.induct) |
284 apply (erule_tac list_eq.induct) |
454 "fset_case \<equiv> list_case" |
454 "fset_case \<equiv> list_case" |
455 |
455 |
456 (* Probably not true without additional assumptions about the function *) |
456 (* Probably not true without additional assumptions about the function *) |
457 lemma list_rec_rsp[quotient_rsp]: |
457 lemma list_rec_rsp[quotient_rsp]: |
458 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |
458 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |
459 apply (auto simp add: FUN_REL_EQ) |
459 apply (auto) |
460 apply (erule_tac list_eq.induct) |
460 apply (erule_tac list_eq.induct) |
461 apply (simp_all) |
461 apply (simp_all) |
462 sorry |
462 sorry |
463 |
463 |
464 lemma list_case_rsp[quotient_rsp]: |
464 lemma list_case_rsp[quotient_rsp]: |
465 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
465 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
466 apply (auto simp add: FUN_REL_EQ) |
466 apply (auto) |
467 sorry |
467 sorry |
468 |
468 |
469 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
469 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
470 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} |
470 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} |
471 |
471 |