383 lemma add_perm_append: |
383 lemma add_perm_append: |
384 shows "add_perm (xs @ ys) = add_perm xs + add_perm ys" |
384 shows "add_perm (xs @ ys) = add_perm xs + add_perm ys" |
385 by (induct xs arbitrary: ys) |
385 by (induct xs arbitrary: ys) |
386 (auto simp add: add_assoc) |
386 (auto simp add: add_assoc) |
387 |
387 |
|
388 (* this induction is the fixed version of the one in Finite_Set.thy *) |
|
389 lemma finite_psubset_induct2[consumes 1, case_names psubset]: |
|
390 assumes major: "finite A" |
|
391 and minor: "\<And>A. finite A \<Longrightarrow> (\<And>B. B \<subset> A \<Longrightarrow> P B) \<Longrightarrow> P A" |
|
392 shows "P A" |
|
393 using major |
|
394 proof (induct A taking: card rule: measure_induct_rule) |
|
395 case (less A) |
|
396 have fact: "finite A" by fact |
|
397 have ih: "\<And>B. \<lbrakk>card B < card A; finite B\<rbrakk> \<Longrightarrow> P B" by fact |
|
398 { fix B |
|
399 assume asm: "B \<subset> A" |
|
400 from asm have "card B < card A" using psubset_card_mono fact by blast |
|
401 moreover |
|
402 from asm have "B \<subseteq> A" by auto |
|
403 then have "finite B" using fact finite_subset by blast |
|
404 ultimately |
|
405 have "P B" using ih by simp |
|
406 } |
|
407 then show "P A" using minor fact by blast |
|
408 qed |
|
409 |
388 lemma perm_list_exists: |
410 lemma perm_list_exists: |
389 fixes p::perm |
411 fixes p::perm |
390 shows "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p" |
412 shows "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p" |
391 apply(induct p taking: "\<lambda>p::perm. card (supp p)" rule: measure_induct) |
413 proof - |
392 apply(rename_tac p) |
414 have "finite (supp p)" by (simp add: finite_supp) |
393 apply(case_tac "supp p = {}") |
415 then show "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p" |
394 apply(simp) |
416 proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct2) |
395 apply(simp add: supp_perm) |
417 case (psubset p) |
396 apply(rule_tac x="[]" in exI) |
418 have ih: "\<And>q. (supp q) \<subset> (supp p) \<Longrightarrow> (\<exists>xs. q = add_perm xs \<and> supp xs \<subseteq> supp q)" by fact |
397 apply(simp add: supp_Nil) |
419 { assume "supp p = {}" |
398 apply(simp add: expand_perm_eq) |
420 then have "p = 0" by (simp add: supp_perm expand_perm_eq) |
399 apply(subgoal_tac "\<exists>x. x \<in> supp p") |
421 then have "p = add_perm [] \<and> supp [] \<subseteq> supp p" by (simp add: supp_Nil) |
400 defer |
422 } |
401 apply(auto)[1] |
423 moreover |
402 apply(erule exE) |
424 { assume "supp p \<noteq> {}" |
403 apply(drule_tac x="p + (((- p) \<bullet> x) \<rightleftharpoons> x)" in spec) |
425 then obtain a where a0: "a \<in> supp p" by blast |
404 apply(drule mp) |
426 let ?q = "p + (((- p) \<bullet> a) \<rightleftharpoons> a)" |
405 defer |
427 have a1: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom) |
406 apply(erule exE) |
428 moreover |
407 apply(rule_tac x="xs @ [((- p) \<bullet> x, x)]" in exI) |
429 have "a \<notin> supp ?q" by (simp add: supp_perm) |
408 apply(simp add: add_perm_append) |
430 then have "supp ?q \<noteq> supp p" using a0 by auto |
409 apply(erule conjE) |
431 ultimately have "(supp ?q) \<subset> (supp p)" by auto |
410 apply(drule sym) |
432 then obtain xs where a: "?q = add_perm xs" and b: "supp xs \<subseteq> supp ?q" using ih by blast |
411 apply(simp) |
433 let ?xs' = "xs @ [((- p) \<bullet> a, a)]" |
412 apply(simp add: expand_perm_eq) |
434 have "supp [(- p \<bullet> a, a)] \<subseteq> supp p" using a0 |
413 apply(simp add: supp_append) |
435 by (simp add: supp_Cons supp_Nil supp_Pair supp_atom supp_perm) (metis permute_minus_cancel(1)) |
414 apply(simp add: supp_perm supp_Cons supp_Nil supp_Pair supp_atom) |
436 moreover |
415 apply(rule conjI) |
437 have "supp xs \<subseteq> supp p" using b a1 by blast |
416 prefer 2 |
438 ultimately |
417 apply(auto)[1] |
439 have"supp ?xs' \<subseteq> supp p" by (simp add: supp_append) |
418 apply (metis permute_atom_def_raw permute_minus_cancel(2)) |
440 moreover |
419 defer |
441 have "p = add_perm ?xs'" using a[symmetric] |
420 apply(rule psubset_card_mono) |
442 by (simp add: add_perm_append expand_perm_eq) |
421 apply(simp add: finite_supp) |
443 ultimately |
422 apply(rule psubsetI) |
444 have "p = add_perm ?xs' \<and> supp ?xs' \<subseteq> supp p" by simp |
423 defer |
445 then have "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p" by blast |
424 apply(subgoal_tac "x \<notin> supp (p + (- p \<bullet> x \<rightleftharpoons> x))") |
446 } |
425 apply(blast) |
447 ultimately show "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p" by blast |
426 apply(simp add: supp_perm) |
448 qed |
427 defer |
449 qed |
428 apply(auto simp add: supp_perm)[1] |
|
429 apply(case_tac "x = xa") |
|
430 apply(simp) |
|
431 apply(case_tac "((- p) \<bullet> x) = xa") |
|
432 apply(simp) |
|
433 apply(case_tac "sort_of xa = sort_of x") |
|
434 apply(simp) |
|
435 apply(auto)[1] |
|
436 apply(simp) |
|
437 apply(simp) |
|
438 apply(subgoal_tac "{a. p \<bullet> (- p \<bullet> x \<rightleftharpoons> x) \<bullet> a \<noteq> a} \<subseteq> {a. p \<bullet> a \<noteq> a}") |
|
439 apply(blast) |
|
440 apply(auto simp add: supp_perm)[1] |
|
441 apply(case_tac "x = xa") |
|
442 apply(simp) |
|
443 apply(case_tac "((- p) \<bullet> x) = xa") |
|
444 apply(simp) |
|
445 apply(case_tac "sort_of xa = sort_of x") |
|
446 apply(simp) |
|
447 apply(auto)[1] |
|
448 apply(simp) |
|
449 apply(simp) |
|
450 done |
|
451 |
450 |
452 section {* Lemma about support and permutations *} |
451 section {* Lemma about support and permutations *} |
453 |
452 |
454 lemma supp_perm_eq: |
453 lemma supp_perm_eq: |
455 assumes a: "(supp x) \<sharp>* p" |
454 assumes a: "(supp x) \<sharp>* p" |