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 - |
316 have "supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" using 2 by auto |
316 have "supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" using 2 by auto |
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 |
|
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 |
321 qed |
341 qed |
322 |
342 |
323 lemma alpha_abs_res_stronger1: |
343 lemma alpha_abs_res_stronger1: |
324 assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')" |
344 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'" |
345 shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" |