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" |
343 lemma supp_nat_of: |
337 lemma supp_nat_of: |
344 shows "supp nat_of = UNIV" |
338 shows "supp nat_of = UNIV" |
345 using not_fresh_nat_of [unfolded fresh_def] by auto |
339 using not_fresh_nat_of [unfolded fresh_def] by auto |
346 |
340 |
347 |
341 |
|
342 section {* Support for sets of atoms *} |
|
343 |
|
344 lemma supp_finite_atom_set: |
|
345 fixes S::"atom set" |
|
346 assumes "finite S" |
|
347 shows "supp S = S" |
|
348 apply(rule finite_supp_unique) |
|
349 apply(simp add: supports_def) |
|
350 apply(simp add: swap_set_not_in) |
|
351 apply(rule assms) |
|
352 apply(simp add: swap_set_in) |
|
353 done |
|
354 |
|
355 |
348 (* |
356 (* |
349 section {* Characterisation of the support of sets of atoms *} |
|
350 |
|
351 lemma swap_set_ineq: |
|
352 fixes a b::"'a::at" |
|
353 assumes "a \<in> S" "b \<notin> S" |
|
354 shows "(a \<leftrightarrow> b) \<bullet> S \<noteq> S" |
|
355 using assms |
|
356 unfolding permute_set_eq |
|
357 by (auto simp add: permute_flip_at) |
|
358 |
|
359 lemma supp_finite: |
|
360 fixes S::"'a::at set" |
|
361 assumes asm: "finite S" |
|
362 shows "(supp S) = atom ` S" |
|
363 sorry |
|
364 |
|
365 lemma supp_infinite: |
357 lemma supp_infinite: |
366 fixes S::"atom set" |
358 fixes S::"atom set" |
367 assumes asm: "finite (UNIV - S)" |
359 assumes asm: "finite (UNIV - S)" |
368 shows "(supp S) = (UNIV - S)" |
360 shows "(supp S) = (UNIV - S)" |
369 apply(rule finite_supp_unique) |
361 apply(rule finite_supp_unique) |