283 then have "(p \<bullet> (supp x - as)) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" by (perm_simp) (simp) |
283 then have "(p \<bullet> (supp x - as)) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" by (perm_simp) (simp) |
284 then have "(supp x - as) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using * by simp |
284 then have "(supp x - as) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using * by simp |
285 then have "(supp x' - as') \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using a by (simp add: alphas) |
285 then have "(supp x' - as') \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using a by (simp add: alphas) |
286 ultimately show "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'" |
286 ultimately show "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'" |
287 by (auto dest: disjoint_right_eq) |
287 by (auto dest: disjoint_right_eq) |
288 qed |
288 qed |
289 |
289 |
290 lemma alpha_abs_res_stronger1_aux: |
290 lemma alpha_abs_res_stronger1_aux: |
291 assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')" |
291 assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')" |
292 shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" |
292 shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" |
293 proof - |
293 proof - |
317 moreover |
317 moreover |
318 have "(as, x) \<approx>res (op =) supp p (as', x')" using asm 1 a by (simp add: alphas) |
318 have "(as, x) \<approx>res (op =) supp p (as', x')" using asm 1 a by (simp add: alphas) |
319 ultimately |
319 ultimately |
320 show "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" by blast |
320 show "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" by blast |
321 qed |
321 qed |
|
322 |
|
323 lemma alpha_abs_res_minimal: |
|
324 assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')" |
|
325 shows "(as \<inter> supp x, x) \<approx>res (op =) supp p (as' \<inter> supp x', x')" |
|
326 using asm unfolding alpha_res by (auto simp add: Diff_Int) |
|
327 |
|
328 lemma alpha_abs_res_abs_set: |
|
329 assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')" |
|
330 shows "(as \<inter> supp x, x) \<approx>set (op =) supp p (as' \<inter> supp x', x')" |
|
331 proof - |
|
332 have c: "p \<bullet> x = x'" |
|
333 using alpha_abs_res_minimal[OF asm] unfolding alpha_res by clarify |
|
334 then have a: "supp x - as \<inter> supp x = supp (p \<bullet> x) - as' \<inter> supp (p \<bullet> x)" |
|
335 using alpha_abs_res_minimal[OF asm] by (simp add: alpha_res) |
|
336 have b: "(supp x - as \<inter> supp x) \<sharp>* p" |
|
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)" |
|
339 by (metis Int_commute asm c supp_property_res) |
|
340 then show ?thesis using a b c unfolding alpha_set by simp |
|
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) |
322 |
347 |
323 lemma alpha_abs_res_stronger1: |
348 lemma alpha_abs_res_stronger1: |
324 assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')" |
349 assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')" |
325 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'" |
326 using alpha_abs_res_stronger1_aux[OF asm] by auto |
351 using alpha_abs_res_stronger1_aux[OF asm] by auto |
480 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)" |
481 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)" |
482 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> |
507 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> |
483 (\<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)" |
484 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 |
485 |
529 |
486 lemma Abs_exhausts: |
530 lemma Abs_exhausts: |
487 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" |
488 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" |
489 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" |