equal
deleted
inserted
replaced
343 lemma supp_nat_of: |
343 lemma supp_nat_of: |
344 shows "supp nat_of = UNIV" |
344 shows "supp nat_of = UNIV" |
345 using not_fresh_nat_of [unfolded fresh_def] by auto |
345 using not_fresh_nat_of [unfolded fresh_def] by auto |
346 |
346 |
347 |
347 |
|
348 section {* Support for sets of atoms *} |
|
349 |
|
350 lemma supp_finite_atom_set: |
|
351 fixes S::"atom set" |
|
352 assumes "finite S" |
|
353 shows "supp S = S" |
|
354 apply(rule finite_supp_unique) |
|
355 apply(simp add: supports_def) |
|
356 apply(auto simp add: permute_set_eq_vimage vimage_def swap_atom)[1] |
|
357 apply(rule assms) |
|
358 apply(auto simp add: permute_set_eq swap_atom)[1] |
|
359 done |
|
360 |
|
361 |
348 (* |
362 (* |
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: |
363 lemma supp_infinite: |
366 fixes S::"atom set" |
364 fixes S::"atom set" |
367 assumes asm: "finite (UNIV - S)" |
365 assumes asm: "finite (UNIV - S)" |
368 shows "(supp S) = (UNIV - S)" |
366 shows "(supp S) = (UNIV - S)" |
369 apply(rule finite_supp_unique) |
367 apply(rule finite_supp_unique) |