390 apply(simp add: swap_set_in) |
390 apply(simp add: swap_set_in) |
391 done |
391 done |
392 |
392 |
393 text {* Induction principle for permutations *} |
393 text {* Induction principle for permutations *} |
394 |
394 |
395 lemma perm_subset_induct_aux [consumes 1, case_names zero swap plus]: |
395 |
|
396 lemma perm_struct_induct[consumes 1, case_names zero swap]: |
396 assumes S: "supp p \<subseteq> S" |
397 assumes S: "supp p \<subseteq> S" |
397 assumes zero: "P 0" |
398 assumes zero: "P 0" |
398 assumes swap: "\<And>a b. supp (a \<rightleftharpoons> b) \<subseteq> S \<Longrightarrow> P (a \<rightleftharpoons> b)" |
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> |
399 assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
400 \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)" |
400 shows "P p" |
401 shows "P p" |
401 proof - |
402 proof - |
402 have "finite (supp p)" by (simp add: finite_supp) |
403 have "finite (supp p)" by (simp add: finite_supp) |
403 then show ?thesis using S |
404 then show "P p" using S |
404 proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct) |
405 proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct) |
405 case (psubset p) |
406 case (psubset p) |
406 then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto |
407 then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto |
407 have as: "supp p \<subseteq> S" by fact |
408 have as: "supp p \<subseteq> S" by fact |
408 { assume "supp p = {}" |
409 { assume "supp p = {}" |
410 then have "P p" using zero by simp |
411 then have "P p" using zero by simp |
411 } |
412 } |
412 moreover |
413 moreover |
413 { assume "supp p \<noteq> {}" |
414 { assume "supp p \<noteq> {}" |
414 then obtain a where a0: "a \<in> supp p" by blast |
415 then obtain a where a0: "a \<in> supp p" by blast |
415 then have a1: "supp (- p \<bullet> a \<rightleftharpoons> a) \<subseteq> S" using as |
416 then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a" using as |
416 by (auto simp add: supp_atom supp_perm swap_atom) |
417 by (auto simp add: supp_atom supp_perm swap_atom) |
417 let ?q = "p + (- p \<bullet> a \<rightleftharpoons> a)" |
418 let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p" |
418 have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom) |
419 have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom) |
419 moreover |
420 moreover |
420 have "a \<notin> supp ?q" by (simp add: supp_perm) |
421 have "a \<notin> supp ?q" by (simp add: supp_perm) |
421 then have "supp ?q \<noteq> supp p" using a0 by auto |
422 then have "supp ?q \<noteq> supp p" using a0 by auto |
422 ultimately have "supp ?q \<subset> supp p" using as by auto |
423 ultimately have "supp ?q \<subset> supp p" using a2 by auto |
423 then have "P ?q" using ih by simp |
424 then have "P ?q" using ih by simp |
424 moreover |
425 moreover |
425 have "supp ?q \<subseteq> S" using as a2 by simp |
426 have "supp ?q \<subseteq> S" using as a2 by simp |
426 moreover |
427 ultimately have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp |
427 have "P (- p \<bullet> a \<rightleftharpoons> a)" using a1 swap by simp |
|
428 ultimately |
|
429 have "P (?q + (- p \<bullet> a \<rightleftharpoons> a))" using a1 plus by simp |
|
430 moreover |
428 moreover |
431 have "p = ?q + (- p \<bullet> a \<rightleftharpoons> a)" by (simp add: expand_perm_eq) |
429 have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: expand_perm_eq) |
432 ultimately have "P p" by simp |
430 ultimately have "P p" by simp |
433 } |
431 } |
434 ultimately show "P p" by blast |
432 ultimately show "P p" by blast |
435 qed |
433 qed |
436 qed |
434 qed |
439 assumes S: "supp p \<subseteq> S" |
437 assumes S: "supp p \<subseteq> S" |
440 assumes zero: "P 0" |
438 assumes zero: "P 0" |
441 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)" |
439 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)" |
442 assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
440 assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
443 shows "P p" |
441 shows "P p" |
444 apply(rule perm_subset_induct_aux[OF S]) |
442 using S |
445 apply(auto simp add: zero swap plus supp_swap split: if_splits) |
443 by (induct p rule: perm_struct_induct) |
446 done |
444 (auto intro: zero plus swap simp add: supp_swap) |
447 |
445 |
448 lemma supp_perm_eq: |
446 lemma supp_perm_eq: |
|
447 assumes "(supp x) \<sharp>* p" |
|
448 shows "p \<bullet> x = x" |
|
449 proof - |
|
450 from assms have "supp p \<subseteq> {a. a \<sharp> x}" |
|
451 unfolding supp_perm fresh_star_def fresh_def by auto |
|
452 then show "p \<bullet> x = x" |
|
453 proof (induct p rule: perm_struct_induct) |
|
454 case zero |
|
455 show "0 \<bullet> x = x" by simp |
|
456 next |
|
457 case (swap p a b) |
|
458 then have "a \<sharp> x" "b \<sharp> x" "p \<bullet> x = x" by simp_all |
|
459 then show "((a \<rightleftharpoons> b) + p) \<bullet> x = x" by (simp add: swap_fresh_fresh) |
|
460 qed |
|
461 qed |
|
462 |
|
463 lemma supp_perm_eq_test: |
449 assumes "(supp x) \<sharp>* p" |
464 assumes "(supp x) \<sharp>* p" |
450 shows "p \<bullet> x = x" |
465 shows "p \<bullet> x = x" |
451 proof - |
466 proof - |
452 from assms have "supp p \<subseteq> {a. a \<sharp> x}" |
467 from assms have "supp p \<subseteq> {a. a \<sharp> x}" |
453 unfolding supp_perm fresh_star_def fresh_def by auto |
468 unfolding supp_perm fresh_star_def fresh_def by auto |