equal
deleted
inserted
replaced
417 |
417 |
418 (* TODO: The following lemmas can be moved somewhere... *) |
418 (* TODO: The following lemmas can be moved somewhere... *) |
419 |
419 |
420 lemma Abs_eq_iff: |
420 lemma Abs_eq_iff: |
421 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
421 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
422 by (lifting alpha_abs.simps(1)) |
422 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
423 |
423 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
|
424 by (lifting alphas_abs) |
424 |
425 |
425 lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===> |
426 lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===> |
426 prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split" |
427 prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split" |
427 by auto |
428 by auto |
428 |
429 |