375 (*

   375 section {* transpositions of permutations *}

   376 lemma supp_infinite:

   376 

   377   fixes S::"atom set"

   377 fun

   378   assumes asm: "finite (UNIV - S)"

   378   add_perm 

   379   shows "(supp S) = (UNIV - S)"

   379 where

   380 apply(rule finite_supp_unique)

   380   "add_perm [] = 0"

   381 apply(auto simp add: supports_def permute_set_eq swap_atom)[1]

   381 | "add_perm ((a, b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"

   382 apply(rule asm)

   382 

   383 apply(auto simp add: permute_set_eq swap_atom)[1]

   383 lemma add_perm_append:

   384   shows "add_perm (xs @ ys) = add_perm xs + add_perm ys"

   385 by (induct xs arbitrary: ys)

   386    (auto simp add: add_assoc)

   387 

   388 lemma perm_list_exists:

   389   fixes p::perm

   390   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)

   392 apply(rename_tac p)

   393 apply(case_tac "supp p = {}")

   394 apply(simp)

   395 apply(simp add: supp_perm)

   396 apply(rule_tac x="[]" in exI)

   397 apply(simp add: supp_Nil)

   398 apply(simp add: expand_perm_eq)

   399 apply(subgoal_tac "\<exists>x. x \<in> supp p")

   400 defer

   401 apply(auto)[1]

   402 apply(erule exE)

   403 apply(drule_tac x="p + (((- p) \<bullet> x) \<rightleftharpoons> x)" in spec)

   404 apply(drule mp)

   405 defer

   406 apply(erule exE)

   407 apply(rule_tac x="xs @ [((- p) \<bullet> x, x)]" in exI)

   408 apply(simp add: add_perm_append)

   409 apply(erule conjE)

   410 apply(drule sym)

   411 apply(simp)

   412 apply(simp add: expand_perm_eq)

   413 apply(simp add: supp_append)

   414 apply(simp add: supp_perm supp_Cons supp_Nil supp_Pair supp_atom)

   415 apply(rule conjI)

   416 prefer 2

   417 apply(auto)[1]

   418 apply (metis left_minus minus_unique permute_atom_def_raw permute_minus_cancel(2))

   419 defer

   420 apply(rule psubset_card_mono)

   421 apply(simp add: finite_supp)

   422 apply(rule psubsetI)

   423 defer

   424 apply(subgoal_tac "x \<notin> supp (p + (- p \<bullet> x \<rightleftharpoons> x))")

   425 apply(blast)

   426 apply(simp add: supp_perm)

   427 defer

   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)

   386 lemma supp_infinite_coinfinite:

   452 section {* Lemma about support and permutations *}

   387   fixes S::"atom set"

   453 

   388   assumes asm1: "infinite S"

   454 lemma supp_perm_eq:

   389   and     asm2: "infinite (UNIV-S)"

   455   assumes a: "(supp x) \<sharp>* p"

   390   shows "(supp S) = (UNIV::atom set)"

   456   shows "p \<bullet> x = x"

   391 *)

   457 proof -

   458   obtain xs where eq: "p = add_perm xs" and sub: "supp xs \<subseteq> supp p"

   459     using perm_list_exists by blast

   460   from a have "\<forall>a \<in> supp p. a \<sharp> x"

   461     by (auto simp add: fresh_star_def fresh_def supp_perm)

   462   with eq sub have "\<forall>a \<in> supp xs. a \<sharp> x" by auto

   463   then have "add_perm xs \<bullet> x = x" 

   464     by (induct xs rule: add_perm.induct)

   465        (simp_all add: supp_Cons supp_Pair supp_atom swap_fresh_fresh)

   466   then show "p \<bullet> x = x" using eq by simp

   467 qed

   468