348 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')" |
348 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')" |
349 proof - |
349 proof - |
350 from asm have 0: "(supp x - as) \<sharp>* p'" by (auto simp only: alphas) |
350 from asm have 0: "(supp x - as) \<sharp>* p'" by (auto simp only: alphas) |
351 then have #: "p' \<bullet> (supp x - as) = (supp x - as)" |
351 then have #: "p' \<bullet> (supp x - as) = (supp x - as)" |
352 by (simp add: atom_set_perm_eq) |
352 by (simp add: atom_set_perm_eq) |
353 have "finite (supp x)" by (simp add: finite_supp) |
353 obtain p where *: "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" and **: "supp p \<subseteq> supp x \<union> p' \<bullet> supp x" |
354 then obtain p where *: "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" and **: "supp p \<subseteq> supp x \<union> p' \<bullet> supp x" |
354 using set_renaming_perm2 by blast |
355 using set_renaming_perm by blast |
|
356 from * have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto |
355 from * have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto |
357 from 0 have 1: "(supp x - as) \<sharp>* p" using * |
356 from 0 have 1: "(supp x - as) \<sharp>* p" using * |
358 by (auto simp add: fresh_star_def fresh_perm) |
357 by (auto simp add: fresh_star_def fresh_perm) |
359 then have 2: "(supp x - as) \<inter> supp p = {}" |
358 then have 2: "(supp x - as) \<inter> supp p = {}" |
360 by (auto simp add: fresh_star_def fresh_def) |
359 by (auto simp add: fresh_star_def fresh_def) |
377 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 |
376 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 |
378 qed |
377 qed |
379 |
378 |
380 lemma alpha_abs_set_stronger1: |
379 lemma alpha_abs_set_stronger1: |
381 fixes x::"'a::fs" |
380 fixes x::"'a::fs" |
382 assumes fin: "finite as" |
381 assumes asm: "(as, x) \<approx>set (op =) supp p' (as', x')" |
383 and asm: "(as, x) \<approx>set (op =) supp p' (as', x')" |
|
384 shows "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" |
382 shows "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" |
385 proof - |
383 proof - |
386 from asm have 0: "(supp x - as) \<sharp>* p'" by (auto simp only: alphas) |
384 from asm have 0: "(supp x - as) \<sharp>* p'" by (auto simp only: alphas) |
387 then have #: "p' \<bullet> (supp x - as) = (supp x - as)" |
385 then have #: "p' \<bullet> (supp x - as) = (supp x - as)" |
388 by (simp add: atom_set_perm_eq) |
386 by (simp add: atom_set_perm_eq) |
389 have za: "finite ((supp x) \<union> as)" using fin by (simp add: finite_supp) |
387 obtain p where *: "\<forall>b \<in> (supp x \<union> as). p \<bullet> b = p' \<bullet> b" |
390 obtain p where *: "\<forall>b \<in> ((supp x) \<union> as). p \<bullet> b = p' \<bullet> b" and **: "supp p \<subseteq> ((supp x) \<union> as) \<union> p' \<bullet> ((supp x) \<union> as)" |
388 and **: "supp p \<subseteq> (supp x \<union> as) \<union> p' \<bullet> (supp x \<union> as)" |
391 using set_renaming_perm[OF za] by blast |
389 using set_renaming_perm2 by blast |
392 from * have "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" by blast |
390 from * have "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" by blast |
393 then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto |
391 then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto |
394 from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast |
392 from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast |
395 then have zb: "p \<bullet> as = p' \<bullet> as" using supp_perm_perm_eq by (metis fin supp_finite_atom_set) |
393 then have zb: "p \<bullet> as = p' \<bullet> as" |
|
394 apply(auto simp add: permute_set_eq) |
|
395 apply(rule_tac x="xa" in exI) |
|
396 apply(simp) |
|
397 done |
396 have zc: "p' \<bullet> as = as'" using asm by (simp add: alphas) |
398 have zc: "p' \<bullet> as = as'" using asm by (simp add: alphas) |
397 from 0 have 1: "(supp x - as) \<sharp>* p" using * |
399 from 0 have 1: "(supp x - as) \<sharp>* p" using * |
398 by (auto simp add: fresh_star_def fresh_perm) |
400 by (auto simp add: fresh_star_def fresh_perm) |
399 then have 2: "(supp x - as) \<inter> supp p = {}" |
401 then have 2: "(supp x - as) \<inter> supp p = {}" |
400 by (auto simp add: fresh_star_def fresh_def) |
402 by (auto simp add: fresh_star_def fresh_def) |
401 have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto |
403 have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto |
402 have "supp p \<subseteq> supp x \<union> as \<union> p' \<bullet> supp x \<union> p' \<bullet> as" using ** using union_eqvt by blast |
404 have "supp p \<subseteq> supp x \<union> as \<union> p' \<bullet> supp x \<union> p' \<bullet> as" using ** using union_eqvt by blast |
403 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as))) \<union> p' \<bullet> as" |
405 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as))) \<union> p' \<bullet> as" |
404 using b by simp |
406 using b by simp |
405 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> ((p' \<bullet> (supp x - as)) \<union> (p' \<bullet> (supp x \<inter> as))) \<union> p' \<bullet> as" |
407 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> |
406 by (simp add: union_eqvt) |
408 ((p' \<bullet> (supp x - as)) \<union> (p' \<bullet> (supp x \<inter> as))) \<union> p' \<bullet> as" by (simp add: union_eqvt) |
407 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> (p' \<bullet> (supp x \<inter> as)) \<union> p' \<bullet> as" |
409 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> (p' \<bullet> (supp x \<inter> as)) \<union> p' \<bullet> as" |
408 using # by auto |
410 using # by auto |
409 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> p' \<bullet> ((supp x \<inter> as) \<union> as)" using union_eqvt |
411 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> p' \<bullet> ((supp x \<inter> as) \<union> as)" using union_eqvt |
410 by auto |
412 by auto |
411 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> p' \<bullet> as" |
413 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> p' \<bullet> as" |
412 by (metis Int_commute Un_commute sup_inf_absorb) |
414 by (metis Int_commute Un_commute sup_inf_absorb) |
413 also have "\<dots> = (supp x - as) \<union> as \<union> p' \<bullet> as" |
415 also have "\<dots> = (supp x - as) \<union> as \<union> p' \<bullet> as" by blast |
414 by blast |
|
415 finally have "supp p \<subseteq> (supp x - as) \<union> as \<union> p' \<bullet> as" . |
416 finally have "supp p \<subseteq> (supp x - as) \<union> as \<union> p' \<bullet> as" . |
416 then have "supp p \<subseteq> as \<union> p' \<bullet> as" using 2 by blast |
417 then have "supp p \<subseteq> as \<union> p' \<bullet> as" using 2 by blast |
417 moreover |
418 moreover |
418 have "(as, x) \<approx>set (op =) supp p (as', x')" using asm 1 a zb by (simp add: alphas) |
419 have "(as, x) \<approx>set (op =) supp p (as', x')" using asm 1 a zb by (simp add: alphas) |
419 ultimately |
420 ultimately |