374 

   374 text {* Induction principle for permutations *}

   375 section {* transpositions of permutations *}

   375 

   376 

   376 lemma perm_subset_induct_aux [consumes 1, case_names zero swap plus]:

   377 fun

   377   assumes S: "supp p \<subseteq> S"

   378   add_perm 

   378   assumes zero: "P 0"

   379 where

   379   assumes swap: "\<And>a b. supp (a \<rightleftharpoons> b) \<subseteq> S \<Longrightarrow> P (a \<rightleftharpoons> b)"

   380   "add_perm [] = 0"

   380   assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"

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

   381   shows "P p"

   382 

   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 (* 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 

   410 lemma perm_list_exists:

   411   fixes p::perm

   412   shows "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p"

   415   then show "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p"

   384   then show ?thesis using S

   416   proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct2)

   385   proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct)

   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

   387     then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto

   388     have as: "supp p \<subseteq> S" by fact

   421       then have "p = add_perm [] \<and> supp [] \<subseteq> supp p" by (simp add: supp_Nil)

   391       then have "P p" using zero by simp

   426       let ?q = "p + (((- p) \<bullet> a) \<rightleftharpoons> a)"

   396       then have a1: "supp (- p \<bullet> a \<rightleftharpoons> a) \<subseteq> S" using as

   427       have a1: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)

   397 	by (auto simp add: supp_atom supp_perm swap_atom)

   398       let ?q = "p + (- p \<bullet> a \<rightleftharpoons> a)"

   399       have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)

   431       ultimately have "(supp ?q) \<subset> (supp p)" by auto

   403       ultimately have "supp ?q \<subset> supp p" using as by auto

   432       then obtain xs where a: "?q = add_perm xs" and b: "supp xs \<subseteq> supp ?q" using ih by blast

   404       then have "P ?q" using ih by simp

   433       let ?xs' = "xs @ [((- p) \<bullet> a, a)]"

   405       moreover

   434       have "supp [(- p \<bullet> a, a)] \<subseteq> supp p" using a0

   406       have "supp ?q \<subseteq> S" using as a2 by simp

   435 	by (simp add: supp_Cons supp_Nil supp_Pair supp_atom supp_perm) (metis permute_minus_cancel(1))

   407       moreover

   408       have "P (- p \<bullet> a \<rightleftharpoons> a)" using a1 swap by simp

   409       ultimately 

   410       have "P (?q + (- p \<bullet> a \<rightleftharpoons> a))" using a1 plus by simp

   437       have "supp xs \<subseteq> supp p" using b a1 by blast 

   412       have "p = ?q + (- p \<bullet> a \<rightleftharpoons> a)" by (simp add: expand_perm_eq)

   438       ultimately  

   413       ultimately have "P p" by simp

   439       have"supp ?xs' \<subseteq> supp p" by (simp add: supp_append)

   440       moreover

   441       have "p = add_perm ?xs'" using a[symmetric]

   442 	by (simp add: add_perm_append expand_perm_eq)

   443       ultimately 

   444       have "p = add_perm ?xs' \<and> supp ?xs' \<subseteq> supp p" by simp

   445       then have "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p" by blast

   447     ultimately show "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p" by blast

   415     ultimately show "P p" by blast

   451 section {* Lemma about support and permutations *}

   419 lemma perm_subset_induct [consumes 1, case_names zero swap plus]:

   420   assumes S: "supp p \<subseteq> S"

   421   assumes zero: "P 0"

   422   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)"

   423   assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"

   424   shows "P p"

   425 apply(rule perm_subset_induct_aux[OF S])

   426 apply(auto simp add: zero swap plus supp_swap split: if_splits)

   427 done

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

   430   assumes "(supp x) \<sharp>* p"

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

   433   from assms have "supp p \<subseteq> {a. a \<sharp> x}"

   458     using perm_list_exists by blast

   434     unfolding supp_perm fresh_star_def fresh_def by auto

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

   435   then show "p \<bullet> x = x"

   460     by (auto simp add: fresh_star_def fresh_def supp_perm)

   436   proof (induct p rule: perm_subset_induct)

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

   437     case zero

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

   438     show "0 \<bullet> x = x" by simp

   463     by (induct xs rule: add_perm.induct)

   439   next

   464        (simp_all add: supp_Cons supp_Pair supp_atom swap_fresh_fresh)

   440     case (swap a b)

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

   441     then have "a \<sharp> x" "b \<sharp> x" by simp_all

   442     then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)

   443   next

   444     case (plus p1 p2)

   445     have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+

   446     then show "(p1 + p2) \<bullet> x = x" by simp

   447   qed