equal
deleted
inserted
replaced
566 lemma Abs_eq_iff: |
566 lemma Abs_eq_iff: |
567 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
567 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
568 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
568 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
569 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
569 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
570 by (lifting alphas_abs) |
570 by (lifting alphas_abs) |
571 |
|
572 lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===> |
|
573 prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split" |
|
574 by auto |
|
575 |
|
576 lemma split_prs2[quot_preserve]: |
|
577 assumes q1: "Quotient R1 Abs1 Rep1" |
|
578 and q2: "Quotient R2 Abs2 Rep2" |
|
579 shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split" |
|
580 by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
|
581 *) |
571 *) |
582 |
572 |
583 |
573 |
584 end |
574 end |
585 |
575 |