337 using alpha_abs_res_minimal[OF asm] unfolding alpha_res by clarify |
337 using alpha_abs_res_minimal[OF asm] unfolding alpha_res by clarify |
338 have "p \<bullet> (as \<inter> supp x) = as' \<inter> supp (p \<bullet> x)" |
338 have "p \<bullet> (as \<inter> supp x) = as' \<inter> supp (p \<bullet> x)" |
339 by (metis Int_commute asm c supp_property_res) |
339 by (metis Int_commute asm c supp_property_res) |
340 then show ?thesis using a b c unfolding alpha_set by simp |
340 then show ?thesis using a b c unfolding alpha_set by simp |
341 qed |
341 qed |
|
342 |
|
343 lemma alpha_abs_set_abs_res: |
|
344 assumes asm: "(as \<inter> supp x, x) \<approx>set (op =) supp p (as' \<inter> supp x', x')" |
|
345 shows "(as, x) \<approx>res (op =) supp p (as', x')" |
|
346 using asm unfolding alphas by (auto simp add: Diff_Int) |
342 |
347 |
343 lemma alpha_abs_res_stronger1: |
348 lemma alpha_abs_res_stronger1: |
344 assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')" |
349 assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')" |
345 shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" |
350 shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" |
346 using alpha_abs_res_stronger1_aux[OF asm] by auto |
351 using alpha_abs_res_stronger1_aux[OF asm] by auto |
500 shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)" |
505 shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)" |
501 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)" |
506 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)" |
502 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> |
507 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> |
503 (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y) \<and> supp p \<subseteq> set bsl \<union> set csl)" |
508 (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y) \<and> supp p \<subseteq> set bsl \<union> set csl)" |
504 by (lifting alphas_abs_stronger) |
509 by (lifting alphas_abs_stronger) |
|
510 |
|
511 lemma Abs_eq_res_set: |
|
512 "(([bs]res. x) = ([cs]res. y)) = (([(bs \<inter> supp x)]set. x) = ([(cs \<inter> supp y)]set. y))" |
|
513 unfolding Abs_eq_iff |
|
514 using alpha_abs_set_abs_res alpha_abs_res_abs_set |
|
515 apply auto |
|
516 apply (rule_tac x="p" in exI) |
|
517 apply assumption |
|
518 apply (rule_tac x="p" in exI) |
|
519 apply assumption |
|
520 done |
|
521 |
|
522 lemma Abs_eq_res_supp: |
|
523 assumes asm: "supp x \<subseteq> bs" |
|
524 shows "([as]res. x) = ([as \<inter> bs]res. x)" |
|
525 unfolding Abs_eq_iff alphas |
|
526 apply (rule_tac x="0::perm" in exI) |
|
527 apply (simp add: fresh_star_zero) |
|
528 using asm by blast |
505 |
529 |
506 lemma Abs_exhausts: |
530 lemma Abs_exhausts: |
507 shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1" |
531 shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1" |
508 and "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2" |
532 and "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2" |
509 and "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3" |
533 and "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3" |