507 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)" |
507 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)" |
508 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> |
508 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> |
509 (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y) \<and> supp p \<subseteq> set bsl \<union> set csl)" |
509 (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y) \<and> supp p \<subseteq> set bsl \<union> set csl)" |
510 by (lifting alphas_abs_stronger) |
510 by (lifting alphas_abs_stronger) |
511 |
511 |
|
512 lemma alpha_res_alpha_set: |
|
513 "(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)" |
|
514 using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast |
|
515 |
512 lemma Abs_eq_res_set: |
516 lemma Abs_eq_res_set: |
513 "(([bs]res. x) = ([cs]res. y)) = (([(bs \<inter> supp x)]set. x) = ([(cs \<inter> supp y)]set. y))" |
517 "(([bs]res. x) = ([cs]res. y)) = (([(bs \<inter> supp x)]set. x) = ([(cs \<inter> supp y)]set. y))" |
514 unfolding Abs_eq_iff |
518 unfolding Abs_eq_iff alpha_res_alpha_set by rule |
515 using alpha_abs_set_abs_res alpha_abs_res_abs_set |
|
516 apply auto |
|
517 apply (rule_tac x="p" in exI) |
|
518 apply assumption |
|
519 apply (rule_tac x="p" in exI) |
|
520 apply assumption |
|
521 done |
|
522 |
519 |
523 lemma Abs_eq_res_supp: |
520 lemma Abs_eq_res_supp: |
524 assumes asm: "supp x \<subseteq> bs" |
521 assumes asm: "supp x \<subseteq> bs" |
525 shows "([as]res. x) = ([as \<inter> bs]res. x)" |
522 shows "([as]res. x) = ([as \<inter> bs]res. x)" |
526 unfolding Abs_eq_iff alphas |
523 unfolding Abs_eq_iff alphas |