413 apply(simp add: fresh_star_def fresh_def)

   413 apply(simp add: fresh_star_def fresh_def)

   414 apply(blast)

   414 apply(blast)

   415 apply(simp add: supp_swap)

   415 apply(simp add: supp_swap)

   416 done

   416 done

   417 

   417 

   419 thm supp_perm

   419 thm supp_perm

   420 

   420 

   421 lemma perm_induct_test:

   422 lemma perm_induct_test:

   422   fixes P :: "perm => bool"

   423   fixes P :: "perm => bool"

   423   assumes zero: "P 0"

   424   assumes zero: "P 0"

   424   assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"

   425   assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"

   425   assumes plus: "\<And>p1 p2. \<lbrakk>supp (p1 + p2) = (supp p1 \<union> supp p2); P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"

   426   assumes plus: "\<And>p1 p2. \<lbrakk>supp (p1 + p2) = (supp p1 \<union> supp p2); P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"