125 using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}` |
126 using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}` |
126 unfolding q by simp |
127 unfolding q by simp |
127 moreover |
128 moreover |
128 have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs" |
129 have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs" |
129 using p2 unfolding q |
130 using p2 unfolding q |
130 apply (intro subset_trans [OF supp_plus_perm]) |
131 by (intro subset_trans [OF supp_plus_perm]) |
131 apply (auto simp add: supp_swap) |
132 (auto simp add: supp_swap) |
132 done |
|
133 ultimately show ?case by blast |
133 ultimately show ?case by blast |
134 qed |
134 qed |
135 qed |
135 qed |
136 |
136 |
137 lemma at_set_avoiding: |
137 lemma at_set_avoiding: |
156 apply(auto simp add: fresh_star_def fresh_def) |
156 apply(auto simp add: fresh_star_def fresh_def) |
157 done |
157 done |
158 |
158 |
159 lemma at_set_avoiding2_atom: |
159 lemma at_set_avoiding2_atom: |
160 assumes "finite (supp c)" "finite (supp x)" |
160 assumes "finite (supp c)" "finite (supp x)" |
161 and b: "xa \<sharp> x" |
161 and b: "a \<sharp> x" |
162 shows "\<exists>p. (p \<bullet> xa) \<sharp> c \<and> supp x \<sharp>* p" |
162 shows "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" |
163 proof - |
163 proof - |
164 have a: "{xa} \<sharp>* x" unfolding fresh_star_def by (simp add: b) |
164 have a: "{a} \<sharp>* x" unfolding fresh_star_def by (simp add: b) |
165 obtain p where p1: "(p \<bullet> {xa}) \<sharp>* c" and p2: "supp x \<sharp>* p" |
165 obtain p where p1: "(p \<bullet> {a}) \<sharp>* c" and p2: "supp x \<sharp>* p" |
166 using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast |
166 using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast |
167 have c: "(p \<bullet> xa) \<sharp> c" using p1 |
167 have c: "(p \<bullet> a) \<sharp> c" using p1 |
168 unfolding fresh_star_def Ball_def |
168 unfolding fresh_star_def Ball_def |
169 by (erule_tac x="p \<bullet> xa" in allE) (simp add: eqvts) |
169 by (erule_tac x="p \<bullet> a" in allE) (simp add: eqvts) |
170 hence "p \<bullet> xa \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast |
170 hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast |
171 then show ?thesis by blast |
171 then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast |
172 qed |
172 qed |
173 |
173 |
174 section {* The freshness lemma according to Andrew Pitts *} |
174 |
|
175 section {* The freshness lemma according to Andy Pitts *} |
175 |
176 |
176 lemma freshness_lemma: |
177 lemma freshness_lemma: |
177 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
178 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
178 assumes a: "\<exists>a. atom a \<sharp> (h, h a)" |
179 assumes a: "\<exists>a. atom a \<sharp> (h, h a)" |
179 shows "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" |
180 shows "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" |
337 assumes P: "finite (supp P)" and Q: "finite (supp Q)" |
338 assumes P: "finite (supp P)" and Q: "finite (supp Q)" |
338 shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)" |
339 shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)" |
339 using P Q by (rule FRESH_binop_iff) |
340 using P Q by (rule FRESH_binop_iff) |
340 |
341 |
341 |
342 |
342 section {* An example of a function without finite support *} |
343 section {* @{const nat_of} is an example of a function |
343 |
344 without finite support *} |
344 primrec |
345 |
345 nat_of :: "atom \<Rightarrow> nat" |
|
346 where |
|
347 "nat_of (Atom s n) = n" |
|
348 |
|
349 lemma atom_eq_iff: |
|
350 fixes a b :: atom |
|
351 shows "a = b \<longleftrightarrow> sort_of a = sort_of b \<and> nat_of a = nat_of b" |
|
352 by (induct a, induct b, simp) |
|
353 |
346 |
354 lemma not_fresh_nat_of: |
347 lemma not_fresh_nat_of: |
355 shows "\<not> a \<sharp> nat_of" |
348 shows "\<not> a \<sharp> nat_of" |
356 unfolding fresh_def supp_def |
349 unfolding fresh_def supp_def |
357 proof (clarsimp) |
350 proof (clarsimp) |
366 have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def) |
359 have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def) |
367 also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq) |
360 also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq) |
368 also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp |
361 also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp |
369 also have "\<dots> = nat_of b" using b2 by simp |
362 also have "\<dots> = nat_of b" using b2 by simp |
370 finally have "nat_of a = nat_of b" by simp |
363 finally have "nat_of a = nat_of b" by simp |
371 with b2 have "a = b" by (simp add: atom_eq_iff) |
364 with b2 have "a = b" by (simp add: atom_components_eq_iff) |
372 with b1 show "False" by simp |
365 with b1 show "False" by simp |
373 qed |
366 qed |
374 |
367 |
375 lemma supp_nat_of: |
368 lemma supp_nat_of: |
376 shows "supp nat_of = UNIV" |
369 shows "supp nat_of = UNIV" |
377 using not_fresh_nat_of [unfolded fresh_def] by auto |
370 using not_fresh_nat_of [unfolded fresh_def] by auto |
378 |
371 |
379 |
372 |
380 section {* Support for finite sets of atoms *} |
373 section {* Induction principle for permutations *} |
381 |
|
382 lemma supp_finite_atom_set: |
|
383 fixes S::"atom set" |
|
384 assumes "finite S" |
|
385 shows "supp S = S" |
|
386 apply(rule finite_supp_unique) |
|
387 apply(simp add: supports_def) |
|
388 apply(simp add: swap_set_not_in) |
|
389 apply(rule assms) |
|
390 apply(simp add: swap_set_in) |
|
391 done |
|
392 |
|
393 text {* Induction principle for permutations *} |
|
394 |
374 |
395 |
375 |
396 lemma perm_struct_induct[consumes 1, case_names zero swap]: |
376 lemma perm_struct_induct[consumes 1, case_names zero swap]: |
397 assumes S: "supp p \<subseteq> S" |
377 assumes S: "supp p \<subseteq> S" |
398 assumes zero: "P 0" |
378 and zero: "P 0" |
399 assumes swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> |
379 and swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)" |
400 \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)" |
|
401 shows "P p" |
380 shows "P p" |
402 proof - |
381 proof - |
403 have "finite (supp p)" by (simp add: finite_supp) |
382 have "finite (supp p)" by (simp add: finite_supp) |
404 then show "P p" using S |
383 then show "P p" using S |
405 proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct) |
384 proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct) |
431 } |
410 } |
432 ultimately show "P p" by blast |
411 ultimately show "P p" by blast |
433 qed |
412 qed |
434 qed |
413 qed |
435 |
414 |
436 lemma perm_struct_induct2[case_names zero swap]: |
415 lemma perm_simple_struct_induct[case_names zero swap]: |
437 assumes zero: "P 0" |
416 assumes zero: "P 0" |
438 assumes swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)" |
417 and swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)" |
439 shows "P p" |
418 shows "P p" |
440 by (rule_tac S="supp p" in perm_struct_induct) |
419 by (rule_tac S="supp p" in perm_struct_induct) |
441 (auto intro: zero swap) |
420 (auto intro: zero swap) |
442 |
421 |
443 lemma perm_subset_induct [consumes 1, case_names zero swap plus]: |
422 lemma perm_subset_induct[consumes 1, case_names zero swap plus]: |
444 assumes S: "supp p \<subseteq> S" |
423 assumes S: "supp p \<subseteq> S" |
445 assumes zero: "P 0" |
424 assumes zero: "P 0" |
446 assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)" |
425 assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)" |
447 assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
426 assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
448 shows "P p" |
427 shows "P p" |