455 "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)" |
455 "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)" |
456 using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast |
456 using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast |
457 |
457 |
458 section {* Quotient types *} |
458 section {* Quotient types *} |
459 |
459 |
460 quotient_type |
460 (* FIXME: The three could be defined together, but due to bugs |
|
461 introduced by the lifting package it doesn't work anymore *) |
|
462 quotient_type |
461 'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set" |
463 'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set" |
462 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res" |
464 apply(rule_tac [!] equivpI) |
463 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst" |
465 unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def |
|
466 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) |
|
467 |
|
468 quotient_type |
|
469 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res" |
|
470 apply(rule_tac [!] equivpI) |
|
471 unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def |
|
472 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) |
|
473 |
|
474 quotient_type |
|
475 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst" |
464 apply(rule_tac [!] equivpI) |
476 apply(rule_tac [!] equivpI) |
465 unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def |
477 unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def |
466 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) |
478 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) |
467 |
479 |
468 quotient_definition |
480 quotient_definition |