equal
deleted
inserted
replaced
63 text {* |
63 text {* |
64 For every set of atoms, there is another set of atoms |
64 For every set of atoms, there is another set of atoms |
65 avoiding a finitely supported c and there is a permutation |
65 avoiding a finitely supported c and there is a permutation |
66 which 'translates' between both sets. |
66 which 'translates' between both sets. |
67 *} |
67 *} |
68 |
|
69 lemma swap_set_fresh: |
|
70 assumes a: "a \<notin> S" "b \<notin> S" |
|
71 shows "(a \<rightleftharpoons> b) \<bullet> S = S" |
|
72 using a |
|
73 by (auto simp add: permute_set_eq swap_atom) |
|
74 |
68 |
75 lemma at_set_avoiding_aux: |
69 lemma at_set_avoiding_aux: |
76 fixes Xs::"atom set" |
70 fixes Xs::"atom set" |
77 and As::"atom set" |
71 and As::"atom set" |
78 assumes b: "Xs \<subseteq> As" |
72 assumes b: "Xs \<subseteq> As" |
105 let ?q = "(x \<rightleftharpoons> y) + p" |
99 let ?q = "(x \<rightleftharpoons> y) + p" |
106 have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)" |
100 have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)" |
107 unfolding insert_eqvt |
101 unfolding insert_eqvt |
108 using `p \<bullet> x = x` `sort_of y = sort_of x` |
102 using `p \<bullet> x = x` `sort_of y = sort_of x` |
109 using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs` |
103 using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs` |
110 by (simp add: swap_atom swap_set_fresh) |
104 by (simp add: swap_atom swap_set_not_in) |
111 have "?q \<bullet> insert x Xs \<inter> As = {}" |
105 have "?q \<bullet> insert x Xs \<inter> As = {}" |
112 using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}` |
106 using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}` |
113 unfolding q by simp |
107 unfolding q by simp |
114 moreover |
108 moreover |
115 have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs" |
109 have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs" |
351 fixes S::"atom set" |
345 fixes S::"atom set" |
352 assumes "finite S" |
346 assumes "finite S" |
353 shows "supp S = S" |
347 shows "supp S = S" |
354 apply(rule finite_supp_unique) |
348 apply(rule finite_supp_unique) |
355 apply(simp add: supports_def) |
349 apply(simp add: supports_def) |
356 apply(auto simp add: permute_set_eq_vimage vimage_def swap_atom)[1] |
350 apply(simp add: swap_set_not_in) |
357 apply(rule assms) |
351 apply(rule assms) |
358 apply(auto simp add: permute_set_eq swap_atom)[1] |
352 apply(simp add: swap_set_in) |
359 done |
353 done |
360 |
354 |
361 |
355 |
362 (* |
356 (* |
363 lemma supp_infinite: |
357 lemma supp_infinite: |