equal
deleted
inserted
replaced
445 |
445 |
446 (* TODO: The following lemmas can be moved somewhere... *) |
446 (* TODO: The following lemmas can be moved somewhere... *) |
447 |
447 |
448 lemma Abs_eq_iff: |
448 lemma Abs_eq_iff: |
449 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
449 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
450 by (lifting alpha_abs.simps(1)) |
450 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
451 |
451 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
|
452 by (lifting alphas_abs) |
452 |
453 |
453 lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===> |
454 lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===> |
454 prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split" |
455 prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split" |
455 by auto |
456 by auto |
456 |
457 |