src/HOL/Library/Permutations.thy
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 59730 b7c394c7a619
child 60601 6e83d94760c4
permissions -rw-r--r--
isabelle update_cartouches;
     1 (*  Title:      HOL/Library/Permutations.thy
     2     Author:     Amine Chaieb, University of Cambridge
     3 *)
     4 
     5 section \<open>Permutations, both general and specifically on finite sets.\<close>
     6 
     7 theory Permutations
     8 imports Binomial
     9 begin
    10 
    11 subsection \<open>Transpositions\<close>
    12 
    13 lemma swap_id_idempotent [simp]:
    14   "Fun.swap a b id \<circ> Fun.swap a b id = id"
    15   by (rule ext, auto simp add: Fun.swap_def)
    16 
    17 lemma inv_swap_id:
    18   "inv (Fun.swap a b id) = Fun.swap a b id"
    19   by (rule inv_unique_comp) simp_all
    20 
    21 lemma swap_id_eq:
    22   "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
    23   by (simp add: Fun.swap_def)
    24 
    25 
    26 subsection \<open>Basic consequences of the definition\<close>
    27 
    28 definition permutes  (infixr "permutes" 41)
    29   where "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"
    30 
    31 lemma permutes_in_image: "p permutes S \<Longrightarrow> p x \<in> S \<longleftrightarrow> x \<in> S"
    32   unfolding permutes_def by metis
    33 
    34 lemma permutes_image: "p permutes S \<Longrightarrow> p ` S = S"
    35   unfolding permutes_def
    36   apply (rule set_eqI)
    37   apply (simp add: image_iff)
    38   apply metis
    39   done
    40 
    41 lemma permutes_inj: "p permutes S \<Longrightarrow> inj p"
    42   unfolding permutes_def inj_on_def by blast
    43 
    44 lemma permutes_surj: "p permutes s \<Longrightarrow> surj p"
    45   unfolding permutes_def surj_def by metis
    46 
    47 lemma permutes_imp_bij: "p permutes S \<Longrightarrow> bij_betw p S S"
    48   by (metis UNIV_I bij_betw_def permutes_image permutes_inj subsetI subset_inj_on)
    49 
    50 lemma bij_imp_permutes: "bij_betw p S S \<Longrightarrow> (\<And>x. x \<notin> S \<Longrightarrow> p x = x) \<Longrightarrow> p permutes S"
    51   unfolding permutes_def bij_betw_def inj_on_def
    52   by auto (metis image_iff)+
    53 
    54 lemma permutes_inv_o:
    55   assumes pS: "p permutes S"
    56   shows "p \<circ> inv p = id"
    57     and "inv p \<circ> p = id"
    58   using permutes_inj[OF pS] permutes_surj[OF pS]
    59   unfolding inj_iff[symmetric] surj_iff[symmetric] by blast+
    60 
    61 lemma permutes_inverses:
    62   fixes p :: "'a \<Rightarrow> 'a"
    63   assumes pS: "p permutes S"
    64   shows "p (inv p x) = x"
    65     and "inv p (p x) = x"
    66   using permutes_inv_o[OF pS, unfolded fun_eq_iff o_def] by auto
    67 
    68 lemma permutes_subset: "p permutes S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> p permutes T"
    69   unfolding permutes_def by blast
    70 
    71 lemma permutes_empty[simp]: "p permutes {} \<longleftrightarrow> p = id"
    72   unfolding fun_eq_iff permutes_def by simp metis
    73 
    74 lemma permutes_sing[simp]: "p permutes {a} \<longleftrightarrow> p = id"
    75   unfolding fun_eq_iff permutes_def by simp metis
    76 
    77 lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)"
    78   unfolding permutes_def by simp
    79 
    80 lemma permutes_inv_eq: "p permutes S \<Longrightarrow> inv p y = x \<longleftrightarrow> p x = y"
    81   unfolding permutes_def inv_def
    82   apply auto
    83   apply (erule allE[where x=y])
    84   apply (erule allE[where x=y])
    85   apply (rule someI_ex)
    86   apply blast
    87   apply (rule some1_equality)
    88   apply blast
    89   apply blast
    90   done
    91 
    92 lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> Fun.swap a b id permutes S"
    93   unfolding permutes_def Fun.swap_def fun_upd_def by auto metis
    94 
    95 lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
    96   by (simp add: Ball_def permutes_def) metis
    97 
    98 
    99 subsection \<open>Group properties\<close>
   100 
   101 lemma permutes_id: "id permutes S"
   102   unfolding permutes_def by simp
   103 
   104 lemma permutes_compose: "p permutes S \<Longrightarrow> q permutes S \<Longrightarrow> q \<circ> p permutes S"
   105   unfolding permutes_def o_def by metis
   106 
   107 lemma permutes_inv:
   108   assumes pS: "p permutes S"
   109   shows "inv p permutes S"
   110   using pS unfolding permutes_def permutes_inv_eq[OF pS] by metis
   111 
   112 lemma permutes_inv_inv:
   113   assumes pS: "p permutes S"
   114   shows "inv (inv p) = p"
   115   unfolding fun_eq_iff permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]]
   116   by blast
   117 
   118 
   119 subsection \<open>The number of permutations on a finite set\<close>
   120 
   121 lemma permutes_insert_lemma:
   122   assumes pS: "p permutes (insert a S)"
   123   shows "Fun.swap a (p a) id \<circ> p permutes S"
   124   apply (rule permutes_superset[where S = "insert a S"])
   125   apply (rule permutes_compose[OF pS])
   126   apply (rule permutes_swap_id, simp)
   127   using permutes_in_image[OF pS, of a]
   128   apply simp
   129   apply (auto simp add: Ball_def Fun.swap_def)
   130   done
   131 
   132 lemma permutes_insert: "{p. p permutes (insert a S)} =
   133   (\<lambda>(b,p). Fun.swap a b id \<circ> p) ` {(b,p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}"
   134 proof -
   135   {
   136     fix p
   137     {
   138       assume pS: "p permutes insert a S"
   139       let ?b = "p a"
   140       let ?q = "Fun.swap a (p a) id \<circ> p"
   141       have th0: "p = Fun.swap a ?b id \<circ> ?q"
   142         unfolding fun_eq_iff o_assoc by simp
   143       have th1: "?b \<in> insert a S"
   144         unfolding permutes_in_image[OF pS] by simp
   145       from permutes_insert_lemma[OF pS] th0 th1
   146       have "\<exists>b q. p = Fun.swap a b id \<circ> q \<and> b \<in> insert a S \<and> q permutes S" by blast
   147     }
   148     moreover
   149     {
   150       fix b q
   151       assume bq: "p = Fun.swap a b id \<circ> q" "b \<in> insert a S" "q permutes S"
   152       from permutes_subset[OF bq(3), of "insert a S"]
   153       have qS: "q permutes insert a S"
   154         by auto
   155       have aS: "a \<in> insert a S"
   156         by simp
   157       from bq(1) permutes_compose[OF qS permutes_swap_id[OF aS bq(2)]]
   158       have "p permutes insert a S"
   159         by simp
   160     }
   161     ultimately have "p permutes insert a S \<longleftrightarrow>
   162         (\<exists>b q. p = Fun.swap a b id \<circ> q \<and> b \<in> insert a S \<and> q permutes S)"
   163       by blast
   164   }
   165   then show ?thesis
   166     by auto
   167 qed
   168 
   169 lemma card_permutations:
   170   assumes Sn: "card S = n"
   171     and fS: "finite S"
   172   shows "card {p. p permutes S} = fact n"
   173   using fS Sn
   174 proof (induct arbitrary: n)
   175   case empty
   176   then show ?case by simp
   177 next
   178   case (insert x F)
   179   {
   180     fix n
   181     assume H0: "card (insert x F) = n"
   182     let ?xF = "{p. p permutes insert x F}"
   183     let ?pF = "{p. p permutes F}"
   184     let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}"
   185     let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)"
   186     from permutes_insert[of x F]
   187     have xfgpF': "?xF = ?g ` ?pF'" .
   188     have Fs: "card F = n - 1"
   189       using \<open>x \<notin> F\<close> H0 \<open>finite F\<close> by auto
   190     from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)"
   191       using \<open>finite F\<close> by auto
   192     then have "finite ?pF"
   193       by (auto intro: card_ge_0_finite)
   194     then have pF'f: "finite ?pF'"
   195       using H0 \<open>finite F\<close>
   196       apply (simp only: Collect_split Collect_mem_eq)
   197       apply (rule finite_cartesian_product)
   198       apply simp_all
   199       done
   200 
   201     have ginj: "inj_on ?g ?pF'"
   202     proof -
   203       {
   204         fix b p c q
   205         assume bp: "(b,p) \<in> ?pF'"
   206         assume cq: "(c,q) \<in> ?pF'"
   207         assume eq: "?g (b,p) = ?g (c,q)"
   208         from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F"
   209           "p permutes F" "q permutes F"
   210           by auto
   211         from ths(4) \<open>x \<notin> F\<close> eq have "b = ?g (b,p) x"
   212           unfolding permutes_def
   213           by (auto simp add: Fun.swap_def fun_upd_def fun_eq_iff)
   214         also have "\<dots> = ?g (c,q) x"
   215           using ths(5) \<open>x \<notin> F\<close> eq
   216           by (auto simp add: swap_def fun_upd_def fun_eq_iff)
   217         also have "\<dots> = c"
   218           using ths(5) \<open>x \<notin> F\<close>
   219           unfolding permutes_def
   220           by (auto simp add: Fun.swap_def fun_upd_def fun_eq_iff)
   221         finally have bc: "b = c" .
   222         then have "Fun.swap x b id = Fun.swap x c id"
   223           by simp
   224         with eq have "Fun.swap x b id \<circ> p = Fun.swap x b id \<circ> q"
   225           by simp
   226         then have "Fun.swap x b id \<circ> (Fun.swap x b id \<circ> p) =
   227           Fun.swap x b id \<circ> (Fun.swap x b id \<circ> q)"
   228           by simp
   229         then have "p = q"
   230           by (simp add: o_assoc)
   231         with bc have "(b, p) = (c, q)"
   232           by simp
   233       }
   234       then show ?thesis
   235         unfolding inj_on_def by blast
   236     qed
   237     from \<open>x \<notin> F\<close> H0 have n0: "n \<noteq> 0"
   238       using \<open>finite F\<close> by auto
   239     then have "\<exists>m. n = Suc m"
   240       by presburger
   241     then obtain m where n[simp]: "n = Suc m"
   242       by blast
   243     from pFs H0 have xFc: "card ?xF = fact n"
   244       unfolding xfgpF' card_image[OF ginj]
   245       using \<open>finite F\<close> \<open>finite ?pF\<close>
   246       apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
   247       apply simp
   248       done
   249     from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF"
   250       unfolding xfgpF' by simp
   251     have "card ?xF = fact n"
   252       using xFf xFc unfolding xFf by blast
   253   }
   254   then show ?case
   255     using insert by simp
   256 qed
   257 
   258 lemma finite_permutations:
   259   assumes fS: "finite S"
   260   shows "finite {p. p permutes S}"
   261   using card_permutations[OF refl fS] 
   262   by (auto intro: card_ge_0_finite)
   263 
   264 
   265 subsection \<open>Permutations of index set for iterated operations\<close>
   266 
   267 lemma (in comm_monoid_set) permute:
   268   assumes "p permutes S"
   269   shows "F g S = F (g \<circ> p) S"
   270 proof -
   271   from \<open>p permutes S\<close> have "inj p"
   272     by (rule permutes_inj)
   273   then have "inj_on p S"
   274     by (auto intro: subset_inj_on)
   275   then have "F g (p ` S) = F (g \<circ> p) S"
   276     by (rule reindex)
   277   moreover from \<open>p permutes S\<close> have "p ` S = S"
   278     by (rule permutes_image)
   279   ultimately show ?thesis
   280     by simp
   281 qed
   282 
   283 
   284 subsection \<open>Various combinations of transpositions with 2, 1 and 0 common elements\<close>
   285 
   286 lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow>
   287   Fun.swap a b id \<circ> Fun.swap a c id = Fun.swap b c id \<circ> Fun.swap a b id"
   288   by (simp add: fun_eq_iff Fun.swap_def)
   289 
   290 lemma swap_id_common': "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow>
   291   Fun.swap a c id \<circ> Fun.swap b c id = Fun.swap b c id \<circ> Fun.swap a b id"
   292   by (simp add: fun_eq_iff Fun.swap_def)
   293 
   294 lemma swap_id_independent: "a \<noteq> c \<Longrightarrow> a \<noteq> d \<Longrightarrow> b \<noteq> c \<Longrightarrow> b \<noteq> d \<Longrightarrow>
   295   Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap c d id \<circ> Fun.swap a b id"
   296   by (simp add: fun_eq_iff Fun.swap_def)
   297 
   298 
   299 subsection \<open>Permutations as transposition sequences\<close>
   300 
   301 inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
   302 where
   303   id[simp]: "swapidseq 0 id"
   304 | comp_Suc: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (Fun.swap a b id \<circ> p)"
   305 
   306 declare id[unfolded id_def, simp]
   307 
   308 definition "permutation p \<longleftrightarrow> (\<exists>n. swapidseq n p)"
   309 
   310 
   311 subsection \<open>Some closure properties of the set of permutations, with lengths\<close>
   312 
   313 lemma permutation_id[simp]: "permutation id"
   314   unfolding permutation_def by (rule exI[where x=0]) simp
   315 
   316 declare permutation_id[unfolded id_def, simp]
   317 
   318 lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (Fun.swap a b id)"
   319   apply clarsimp
   320   using comp_Suc[of 0 id a b]
   321   apply simp
   322   done
   323 
   324 lemma permutation_swap_id: "permutation (Fun.swap a b id)"
   325   apply (cases "a = b")
   326   apply simp_all
   327   unfolding permutation_def
   328   using swapidseq_swap[of a b]
   329   apply blast
   330   done
   331 
   332 lemma swapidseq_comp_add: "swapidseq n p \<Longrightarrow> swapidseq m q \<Longrightarrow> swapidseq (n + m) (p \<circ> q)"
   333 proof (induct n p arbitrary: m q rule: swapidseq.induct)
   334   case (id m q)
   335   then show ?case by simp
   336 next
   337   case (comp_Suc n p a b m q)
   338   have th: "Suc n + m = Suc (n + m)"
   339     by arith
   340   show ?case
   341     unfolding th comp_assoc
   342     apply (rule swapidseq.comp_Suc)
   343     using comp_Suc.hyps(2)[OF comp_Suc.prems] comp_Suc.hyps(3)
   344     apply blast+
   345     done
   346 qed
   347 
   348 lemma permutation_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> permutation (p \<circ> q)"
   349   unfolding permutation_def using swapidseq_comp_add[of _ p _ q] by metis
   350 
   351 lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (p \<circ> Fun.swap a b id)"
   352   apply (induct n p rule: swapidseq.induct)
   353   using swapidseq_swap[of a b]
   354   apply (auto simp add: comp_assoc intro: swapidseq.comp_Suc)
   355   done
   356 
   357 lemma swapidseq_inverse_exists: "swapidseq n p \<Longrightarrow> \<exists>q. swapidseq n q \<and> p \<circ> q = id \<and> q \<circ> p = id"
   358 proof (induct n p rule: swapidseq.induct)
   359   case id
   360   then show ?case
   361     by (rule exI[where x=id]) simp
   362 next
   363   case (comp_Suc n p a b)
   364   from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id"
   365     by blast
   366   let ?q = "q \<circ> Fun.swap a b id"
   367   note H = comp_Suc.hyps
   368   from swapidseq_swap[of a b] H(3) have th0: "swapidseq 1 (Fun.swap a b id)"
   369     by simp
   370   from swapidseq_comp_add[OF q(1) th0] have th1: "swapidseq (Suc n) ?q"
   371     by simp
   372   have "Fun.swap a b id \<circ> p \<circ> ?q = Fun.swap a b id \<circ> (p \<circ> q) \<circ> Fun.swap a b id"
   373     by (simp add: o_assoc)
   374   also have "\<dots> = id"
   375     by (simp add: q(2))
   376   finally have th2: "Fun.swap a b id \<circ> p \<circ> ?q = id" .
   377   have "?q \<circ> (Fun.swap a b id \<circ> p) = q \<circ> (Fun.swap a b id \<circ> Fun.swap a b id) \<circ> p"
   378     by (simp only: o_assoc)
   379   then have "?q \<circ> (Fun.swap a b id \<circ> p) = id"
   380     by (simp add: q(3))
   381   with th1 th2 show ?case
   382     by blast
   383 qed
   384 
   385 lemma swapidseq_inverse:
   386   assumes H: "swapidseq n p"
   387   shows "swapidseq n (inv p)"
   388   using swapidseq_inverse_exists[OF H] inv_unique_comp[of p] by auto
   389 
   390 lemma permutation_inverse: "permutation p \<Longrightarrow> permutation (inv p)"
   391   using permutation_def swapidseq_inverse by blast
   392 
   393 
   394 subsection \<open>The identity map only has even transposition sequences\<close>
   395 
   396 lemma symmetry_lemma:
   397   assumes "\<And>a b c d. P a b c d \<Longrightarrow> P a b d c"
   398     and "\<And>a b c d. a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow>
   399       a = c \<and> b = d \<or> a = c \<and> b \<noteq> d \<or> a \<noteq> c \<and> b = d \<or> a \<noteq> c \<and> a \<noteq> d \<and> b \<noteq> c \<and> b \<noteq> d \<Longrightarrow>
   400       P a b c d"
   401   shows "\<And>a b c d. a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow>  P a b c d"
   402   using assms by metis
   403 
   404 lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow>
   405   Fun.swap a b id \<circ> Fun.swap c d id = id \<or>
   406   (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and>
   407     Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id)"
   408 proof -
   409   assume H: "a \<noteq> b" "c \<noteq> d"
   410   have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow>
   411     (Fun.swap a b id \<circ> Fun.swap c d id = id \<or>
   412       (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and>
   413         Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id))"
   414     apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d])
   415     apply (simp_all only: swap_commute)
   416     apply (case_tac "a = c \<and> b = d")
   417     apply (clarsimp simp only: swap_commute swap_id_idempotent)
   418     apply (case_tac "a = c \<and> b \<noteq> d")
   419     apply (rule disjI2)
   420     apply (rule_tac x="b" in exI)
   421     apply (rule_tac x="d" in exI)
   422     apply (rule_tac x="b" in exI)
   423     apply (clarsimp simp add: fun_eq_iff Fun.swap_def)
   424     apply (case_tac "a \<noteq> c \<and> b = d")
   425     apply (rule disjI2)
   426     apply (rule_tac x="c" in exI)
   427     apply (rule_tac x="d" in exI)
   428     apply (rule_tac x="c" in exI)
   429     apply (clarsimp simp add: fun_eq_iff Fun.swap_def)
   430     apply (rule disjI2)
   431     apply (rule_tac x="c" in exI)
   432     apply (rule_tac x="d" in exI)
   433     apply (rule_tac x="b" in exI)
   434     apply (clarsimp simp add: fun_eq_iff Fun.swap_def)
   435     done
   436   with H show ?thesis by metis
   437 qed
   438 
   439 lemma swapidseq_id_iff[simp]: "swapidseq 0 p \<longleftrightarrow> p = id"
   440   using swapidseq.cases[of 0 p "p = id"]
   441   by auto
   442 
   443 lemma swapidseq_cases: "swapidseq n p \<longleftrightarrow>
   444   n = 0 \<and> p = id \<or> (\<exists>a b q m. n = Suc m \<and> p = Fun.swap a b id \<circ> q \<and> swapidseq m q \<and> a \<noteq> b)"
   445   apply (rule iffI)
   446   apply (erule swapidseq.cases[of n p])
   447   apply simp
   448   apply (rule disjI2)
   449   apply (rule_tac x= "a" in exI)
   450   apply (rule_tac x= "b" in exI)
   451   apply (rule_tac x= "pa" in exI)
   452   apply (rule_tac x= "na" in exI)
   453   apply simp
   454   apply auto
   455   apply (rule comp_Suc, simp_all)
   456   done
   457 
   458 lemma fixing_swapidseq_decrease:
   459   assumes spn: "swapidseq n p"
   460     and ab: "a \<noteq> b"
   461     and pa: "(Fun.swap a b id \<circ> p) a = a"
   462   shows "n \<noteq> 0 \<and> swapidseq (n - 1) (Fun.swap a b id \<circ> p)"
   463   using spn ab pa
   464 proof (induct n arbitrary: p a b)
   465   case 0
   466   then show ?case
   467     by (auto simp add: Fun.swap_def fun_upd_def)
   468 next
   469   case (Suc n p a b)
   470   from Suc.prems(1) swapidseq_cases[of "Suc n" p]
   471   obtain c d q m where
   472     cdqm: "Suc n = Suc m" "p = Fun.swap c d id \<circ> q" "swapidseq m q" "c \<noteq> d" "n = m"
   473     by auto
   474   {
   475     assume H: "Fun.swap a b id \<circ> Fun.swap c d id = id"
   476     have ?case by (simp only: cdqm o_assoc H) (simp add: cdqm)
   477   }
   478   moreover
   479   {
   480     fix x y z
   481     assume H: "x \<noteq> a" "y \<noteq> a" "z \<noteq> a" "x \<noteq> y"
   482       "Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id"
   483     from H have az: "a \<noteq> z"
   484       by simp
   485 
   486     {
   487       fix h
   488       have "(Fun.swap x y id \<circ> h) a = a \<longleftrightarrow> h a = a"
   489         using H by (simp add: Fun.swap_def)
   490     }
   491     note th3 = this
   492     from cdqm(2) have "Fun.swap a b id \<circ> p = Fun.swap a b id \<circ> (Fun.swap c d id \<circ> q)"
   493       by simp
   494     then have "Fun.swap a b id \<circ> p = Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)"
   495       by (simp add: o_assoc H)
   496     then have "(Fun.swap a b id \<circ> p) a = (Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)) a"
   497       by simp
   498     then have "(Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)) a = a"
   499       unfolding Suc by metis
   500     then have th1: "(Fun.swap a z id \<circ> q) a = a"
   501       unfolding th3 .
   502     from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az th1]
   503     have th2: "swapidseq (n - 1) (Fun.swap a z id \<circ> q)" "n \<noteq> 0"
   504       by blast+
   505     have th: "Suc n - 1 = Suc (n - 1)"
   506       using th2(2) by auto
   507     have ?case
   508       unfolding cdqm(2) H o_assoc th
   509       apply (simp only: Suc_not_Zero simp_thms comp_assoc)
   510       apply (rule comp_Suc)
   511       using th2 H
   512       apply blast+
   513       done
   514   }
   515   ultimately show ?case
   516     using swap_general[OF Suc.prems(2) cdqm(4)] by metis
   517 qed
   518 
   519 lemma swapidseq_identity_even:
   520   assumes "swapidseq n (id :: 'a \<Rightarrow> 'a)"
   521   shows "even n"
   522   using \<open>swapidseq n id\<close>
   523 proof (induct n rule: nat_less_induct)
   524   fix n
   525   assume H: "\<forall>m<n. swapidseq m (id::'a \<Rightarrow> 'a) \<longrightarrow> even m" "swapidseq n (id :: 'a \<Rightarrow> 'a)"
   526   {
   527     assume "n = 0"
   528     then have "even n" by presburger
   529   }
   530   moreover
   531   {
   532     fix a b :: 'a and q m
   533     assume h: "n = Suc m" "(id :: 'a \<Rightarrow> 'a) = Fun.swap a b id \<circ> q" "swapidseq m q" "a \<noteq> b"
   534     from fixing_swapidseq_decrease[OF h(3,4), unfolded h(2)[symmetric]]
   535     have m: "m \<noteq> 0" "swapidseq (m - 1) (id :: 'a \<Rightarrow> 'a)"
   536       by auto
   537     from h m have mn: "m - 1 < n"
   538       by arith
   539     from H(1)[rule_format, OF mn m(2)] h(1) m(1) have "even n"
   540       by presburger
   541   }
   542   ultimately show "even n"
   543     using H(2)[unfolded swapidseq_cases[of n id]] by auto
   544 qed
   545 
   546 
   547 subsection \<open>Therefore we have a welldefined notion of parity\<close>
   548 
   549 definition "evenperm p = even (SOME n. swapidseq n p)"
   550 
   551 lemma swapidseq_even_even:
   552   assumes m: "swapidseq m p"
   553     and n: "swapidseq n p"
   554   shows "even m \<longleftrightarrow> even n"
   555 proof -
   556   from swapidseq_inverse_exists[OF n]
   557   obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id"
   558     by blast
   559   from swapidseq_identity_even[OF swapidseq_comp_add[OF m q(1), unfolded q]]
   560   show ?thesis
   561     by arith
   562 qed
   563 
   564 lemma evenperm_unique:
   565   assumes p: "swapidseq n p"
   566     and n:"even n = b"
   567   shows "evenperm p = b"
   568   unfolding n[symmetric] evenperm_def
   569   apply (rule swapidseq_even_even[where p = p])
   570   apply (rule someI[where x = n])
   571   using p
   572   apply blast+
   573   done
   574 
   575 
   576 subsection \<open>And it has the expected composition properties\<close>
   577 
   578 lemma evenperm_id[simp]: "evenperm id = True"
   579   by (rule evenperm_unique[where n = 0]) simp_all
   580 
   581 lemma evenperm_swap: "evenperm (Fun.swap a b id) = (a = b)"
   582   by (rule evenperm_unique[where n="if a = b then 0 else 1"]) (simp_all add: swapidseq_swap)
   583 
   584 lemma evenperm_comp:
   585   assumes p: "permutation p"
   586     and q:"permutation q"
   587   shows "evenperm (p \<circ> q) = (evenperm p = evenperm q)"
   588 proof -
   589   from p q obtain n m where n: "swapidseq n p" and m: "swapidseq m q"
   590     unfolding permutation_def by blast
   591   note nm =  swapidseq_comp_add[OF n m]
   592   have th: "even (n + m) = (even n \<longleftrightarrow> even m)"
   593     by arith
   594   from evenperm_unique[OF n refl] evenperm_unique[OF m refl]
   595     evenperm_unique[OF nm th]
   596   show ?thesis
   597     by blast
   598 qed
   599 
   600 lemma evenperm_inv:
   601   assumes p: "permutation p"
   602   shows "evenperm (inv p) = evenperm p"
   603 proof -
   604   from p obtain n where n: "swapidseq n p"
   605     unfolding permutation_def by blast
   606   from evenperm_unique[OF swapidseq_inverse[OF n] evenperm_unique[OF n refl, symmetric]]
   607   show ?thesis .
   608 qed
   609 
   610 
   611 subsection \<open>A more abstract characterization of permutations\<close>
   612 
   613 lemma bij_iff: "bij f \<longleftrightarrow> (\<forall>x. \<exists>!y. f y = x)"
   614   unfolding bij_def inj_on_def surj_def
   615   apply auto
   616   apply metis
   617   apply metis
   618   done
   619 
   620 lemma permutation_bijective:
   621   assumes p: "permutation p"
   622   shows "bij p"
   623 proof -
   624   from p obtain n where n: "swapidseq n p"
   625     unfolding permutation_def by blast
   626   from swapidseq_inverse_exists[OF n]
   627   obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id"
   628     by blast
   629   then show ?thesis unfolding bij_iff
   630     apply (auto simp add: fun_eq_iff)
   631     apply metis
   632     done
   633 qed
   634 
   635 lemma permutation_finite_support:
   636   assumes p: "permutation p"
   637   shows "finite {x. p x \<noteq> x}"
   638 proof -
   639   from p obtain n where n: "swapidseq n p"
   640     unfolding permutation_def by blast
   641   from n show ?thesis
   642   proof (induct n p rule: swapidseq.induct)
   643     case id
   644     then show ?case by simp
   645   next
   646     case (comp_Suc n p a b)
   647     let ?S = "insert a (insert b {x. p x \<noteq> x})"
   648     from comp_Suc.hyps(2) have fS: "finite ?S"
   649       by simp
   650     from \<open>a \<noteq> b\<close> have th: "{x. (Fun.swap a b id \<circ> p) x \<noteq> x} \<subseteq> ?S"
   651       by (auto simp add: Fun.swap_def)
   652     from finite_subset[OF th fS] show ?case  .
   653   qed
   654 qed
   655 
   656 lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y"
   657   using surj_f_inv_f[of p] by (auto simp add: bij_def)
   658 
   659 lemma bij_swap_comp:
   660   assumes bp: "bij p"
   661   shows "Fun.swap a b id \<circ> p = Fun.swap (inv p a) (inv p b) p"
   662   using surj_f_inv_f[OF bij_is_surj[OF bp]]
   663   by (simp add: fun_eq_iff Fun.swap_def bij_inv_eq_iff[OF bp])
   664 
   665 lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id \<circ> p)"
   666 proof -
   667   assume H: "bij p"
   668   show ?thesis
   669     unfolding bij_swap_comp[OF H] bij_swap_iff
   670     using H .
   671 qed
   672 
   673 lemma permutation_lemma:
   674   assumes fS: "finite S"
   675     and p: "bij p"
   676     and pS: "\<forall>x. x\<notin> S \<longrightarrow> p x = x"
   677   shows "permutation p"
   678   using fS p pS
   679 proof (induct S arbitrary: p rule: finite_induct)
   680   case (empty p)
   681   then show ?case by simp
   682 next
   683   case (insert a F p)
   684   let ?r = "Fun.swap a (p a) id \<circ> p"
   685   let ?q = "Fun.swap a (p a) id \<circ> ?r"
   686   have raa: "?r a = a"
   687     by (simp add: Fun.swap_def)
   688   from bij_swap_ompose_bij[OF insert(4)]
   689   have br: "bij ?r"  .
   690 
   691   from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x"
   692     apply (clarsimp simp add: Fun.swap_def)
   693     apply (erule_tac x="x" in allE)
   694     apply auto
   695     unfolding bij_iff
   696     apply metis
   697     done
   698   from insert(3)[OF br th]
   699   have rp: "permutation ?r" .
   700   have "permutation ?q"
   701     by (simp add: permutation_compose permutation_swap_id rp)
   702   then show ?case
   703     by (simp add: o_assoc)
   704 qed
   705 
   706 lemma permutation: "permutation p \<longleftrightarrow> bij p \<and> finite {x. p x \<noteq> x}"
   707   (is "?lhs \<longleftrightarrow> ?b \<and> ?f")
   708 proof
   709   assume p: ?lhs
   710   from p permutation_bijective permutation_finite_support show "?b \<and> ?f"
   711     by auto
   712 next
   713   assume "?b \<and> ?f"
   714   then have "?f" "?b" by blast+
   715   from permutation_lemma[OF this] show ?lhs
   716     by blast
   717 qed
   718 
   719 lemma permutation_inverse_works:
   720   assumes p: "permutation p"
   721   shows "inv p \<circ> p = id"
   722     and "p \<circ> inv p = id"
   723   using permutation_bijective [OF p]
   724   unfolding bij_def inj_iff surj_iff by auto
   725 
   726 lemma permutation_inverse_compose:
   727   assumes p: "permutation p"
   728     and q: "permutation q"
   729   shows "inv (p \<circ> q) = inv q \<circ> inv p"
   730 proof -
   731   note ps = permutation_inverse_works[OF p]
   732   note qs = permutation_inverse_works[OF q]
   733   have "p \<circ> q \<circ> (inv q \<circ> inv p) = p \<circ> (q \<circ> inv q) \<circ> inv p"
   734     by (simp add: o_assoc)
   735   also have "\<dots> = id"
   736     by (simp add: ps qs)
   737   finally have th0: "p \<circ> q \<circ> (inv q \<circ> inv p) = id" .
   738   have "inv q \<circ> inv p \<circ> (p \<circ> q) = inv q \<circ> (inv p \<circ> p) \<circ> q"
   739     by (simp add: o_assoc)
   740   also have "\<dots> = id"
   741     by (simp add: ps qs)
   742   finally have th1: "inv q \<circ> inv p \<circ> (p \<circ> q) = id" .
   743   from inv_unique_comp[OF th0 th1] show ?thesis .
   744 qed
   745 
   746 
   747 subsection \<open>Relation to "permutes"\<close>
   748 
   749 lemma permutation_permutes: "permutation p \<longleftrightarrow> (\<exists>S. finite S \<and> p permutes S)"
   750   unfolding permutation permutes_def bij_iff[symmetric]
   751   apply (rule iffI, clarify)
   752   apply (rule exI[where x="{x. p x \<noteq> x}"])
   753   apply simp
   754   apply clarsimp
   755   apply (rule_tac B="S" in finite_subset)
   756   apply auto
   757   done
   758 
   759 
   760 subsection \<open>Hence a sort of induction principle composing by swaps\<close>
   761 
   762 lemma permutes_induct: "finite S \<Longrightarrow> P id \<Longrightarrow>
   763   (\<And> a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> P p \<Longrightarrow> P p \<Longrightarrow> permutation p \<Longrightarrow> P (Fun.swap a b id \<circ> p)) \<Longrightarrow>
   764   (\<And>p. p permutes S \<Longrightarrow> P p)"
   765 proof (induct S rule: finite_induct)
   766   case empty
   767   then show ?case by auto
   768 next
   769   case (insert x F p)
   770   let ?r = "Fun.swap x (p x) id \<circ> p"
   771   let ?q = "Fun.swap x (p x) id \<circ> ?r"
   772   have qp: "?q = p"
   773     by (simp add: o_assoc)
   774   from permutes_insert_lemma[OF insert.prems(3)] insert have Pr: "P ?r"
   775     by blast
   776   from permutes_in_image[OF insert.prems(3), of x]
   777   have pxF: "p x \<in> insert x F"
   778     by simp
   779   have xF: "x \<in> insert x F"
   780     by simp
   781   have rp: "permutation ?r"
   782     unfolding permutation_permutes using insert.hyps(1)
   783       permutes_insert_lemma[OF insert.prems(3)]
   784     by blast
   785   from insert.prems(2)[OF xF pxF Pr Pr rp]
   786   show ?case
   787     unfolding qp .
   788 qed
   789 
   790 
   791 subsection \<open>Sign of a permutation as a real number\<close>
   792 
   793 definition "sign p = (if evenperm p then (1::int) else -1)"
   794 
   795 lemma sign_nz: "sign p \<noteq> 0"
   796   by (simp add: sign_def)
   797 
   798 lemma sign_id: "sign id = 1"
   799   by (simp add: sign_def)
   800 
   801 lemma sign_inverse: "permutation p \<Longrightarrow> sign (inv p) = sign p"
   802   by (simp add: sign_def evenperm_inv)
   803 
   804 lemma sign_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> sign (p \<circ> q) = sign p * sign q"
   805   by (simp add: sign_def evenperm_comp)
   806 
   807 lemma sign_swap_id: "sign (Fun.swap a b id) = (if a = b then 1 else -1)"
   808   by (simp add: sign_def evenperm_swap)
   809 
   810 lemma sign_idempotent: "sign p * sign p = 1"
   811   by (simp add: sign_def)
   812 
   813 
   814 subsection \<open>More lemmas about permutations\<close>
   815 
   816 lemma permutes_natset_le:
   817   fixes S :: "'a::wellorder set"
   818   assumes p: "p permutes S"
   819     and le: "\<forall>i \<in> S. p i \<le> i"
   820   shows "p = id"
   821 proof -
   822   {
   823     fix n
   824     have "p n = n"
   825       using p le
   826     proof (induct n arbitrary: S rule: less_induct)
   827       fix n S
   828       assume H:
   829         "\<And>m S. m < n \<Longrightarrow> p permutes S \<Longrightarrow> \<forall>i\<in>S. p i \<le> i \<Longrightarrow> p m = m"
   830         "p permutes S" "\<forall>i \<in>S. p i \<le> i"
   831       {
   832         assume "n \<notin> S"
   833         with H(2) have "p n = n"
   834           unfolding permutes_def by metis
   835       }
   836       moreover
   837       {
   838         assume ns: "n \<in> S"
   839         from H(3)  ns have "p n < n \<or> p n = n"
   840           by auto
   841         moreover {
   842           assume h: "p n < n"
   843           from H h have "p (p n) = p n"
   844             by metis
   845           with permutes_inj[OF H(2)] have "p n = n"
   846             unfolding inj_on_def by blast
   847           with h have False
   848             by simp
   849         }
   850         ultimately have "p n = n"
   851           by blast
   852       }
   853       ultimately show "p n = n"
   854         by blast
   855     qed
   856   }
   857   then show ?thesis
   858     by (auto simp add: fun_eq_iff)
   859 qed
   860 
   861 lemma permutes_natset_ge:
   862   fixes S :: "'a::wellorder set"
   863   assumes p: "p permutes S"
   864     and le: "\<forall>i \<in> S. p i \<ge> i"
   865   shows "p = id"
   866 proof -
   867   {
   868     fix i
   869     assume i: "i \<in> S"
   870     from i permutes_in_image[OF permutes_inv[OF p]] have "inv p i \<in> S"
   871       by simp
   872     with le have "p (inv p i) \<ge> inv p i"
   873       by blast
   874     with permutes_inverses[OF p] have "i \<ge> inv p i"
   875       by simp
   876   }
   877   then have th: "\<forall>i\<in>S. inv p i \<le> i"
   878     by blast
   879   from permutes_natset_le[OF permutes_inv[OF p] th]
   880   have "inv p = inv id"
   881     by simp
   882   then show ?thesis
   883     apply (subst permutes_inv_inv[OF p, symmetric])
   884     apply (rule inv_unique_comp)
   885     apply simp_all
   886     done
   887 qed
   888 
   889 lemma image_inverse_permutations: "{inv p |p. p permutes S} = {p. p permutes S}"
   890   apply (rule set_eqI)
   891   apply auto
   892   using permutes_inv_inv permutes_inv
   893   apply auto
   894   apply (rule_tac x="inv x" in exI)
   895   apply auto
   896   done
   897 
   898 lemma image_compose_permutations_left:
   899   assumes q: "q permutes S"
   900   shows "{q \<circ> p | p. p permutes S} = {p . p permutes S}"
   901   apply (rule set_eqI)
   902   apply auto
   903   apply (rule permutes_compose)
   904   using q
   905   apply auto
   906   apply (rule_tac x = "inv q \<circ> x" in exI)
   907   apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o)
   908   done
   909 
   910 lemma image_compose_permutations_right:
   911   assumes q: "q permutes S"
   912   shows "{p \<circ> q | p. p permutes S} = {p . p permutes S}"
   913   apply (rule set_eqI)
   914   apply auto
   915   apply (rule permutes_compose)
   916   using q
   917   apply auto
   918   apply (rule_tac x = "x \<circ> inv q" in exI)
   919   apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o comp_assoc)
   920   done
   921 
   922 lemma permutes_in_seg: "p permutes {1 ..n} \<Longrightarrow> i \<in> {1..n} \<Longrightarrow> 1 \<le> p i \<and> p i \<le> n"
   923   by (simp add: permutes_def) metis
   924 
   925 lemma setsum_permutations_inverse:
   926   "setsum f {p. p permutes S} = setsum (\<lambda>p. f(inv p)) {p. p permutes S}"
   927   (is "?lhs = ?rhs")
   928 proof -
   929   let ?S = "{p . p permutes S}"
   930   have th0: "inj_on inv ?S"
   931   proof (auto simp add: inj_on_def)
   932     fix q r
   933     assume q: "q permutes S"
   934       and r: "r permutes S"
   935       and qr: "inv q = inv r"
   936     then have "inv (inv q) = inv (inv r)"
   937       by simp
   938     with permutes_inv_inv[OF q] permutes_inv_inv[OF r] show "q = r"
   939       by metis
   940   qed
   941   have th1: "inv ` ?S = ?S"
   942     using image_inverse_permutations by blast
   943   have th2: "?rhs = setsum (f \<circ> inv) ?S"
   944     by (simp add: o_def)
   945   from setsum.reindex[OF th0, of f] show ?thesis unfolding th1 th2 .
   946 qed
   947 
   948 lemma setum_permutations_compose_left:
   949   assumes q: "q permutes S"
   950   shows "setsum f {p. p permutes S} = setsum (\<lambda>p. f(q \<circ> p)) {p. p permutes S}"
   951   (is "?lhs = ?rhs")
   952 proof -
   953   let ?S = "{p. p permutes S}"
   954   have th0: "?rhs = setsum (f \<circ> (op \<circ> q)) ?S"
   955     by (simp add: o_def)
   956   have th1: "inj_on (op \<circ> q) ?S"
   957   proof (auto simp add: inj_on_def)
   958     fix p r
   959     assume "p permutes S"
   960       and r: "r permutes S"
   961       and rp: "q \<circ> p = q \<circ> r"
   962     then have "inv q \<circ> q \<circ> p = inv q \<circ> q \<circ> r"
   963       by (simp add: comp_assoc)
   964     with permutes_inj[OF q, unfolded inj_iff] show "p = r"
   965       by simp
   966   qed
   967   have th3: "(op \<circ> q) ` ?S = ?S"
   968     using image_compose_permutations_left[OF q] by auto
   969   from setsum.reindex[OF th1, of f] show ?thesis unfolding th0 th1 th3 .
   970 qed
   971 
   972 lemma sum_permutations_compose_right:
   973   assumes q: "q permutes S"
   974   shows "setsum f {p. p permutes S} = setsum (\<lambda>p. f(p \<circ> q)) {p. p permutes S}"
   975   (is "?lhs = ?rhs")
   976 proof -
   977   let ?S = "{p. p permutes S}"
   978   have th0: "?rhs = setsum (f \<circ> (\<lambda>p. p \<circ> q)) ?S"
   979     by (simp add: o_def)
   980   have th1: "inj_on (\<lambda>p. p \<circ> q) ?S"
   981   proof (auto simp add: inj_on_def)
   982     fix p r
   983     assume "p permutes S"
   984       and r: "r permutes S"
   985       and rp: "p \<circ> q = r \<circ> q"
   986     then have "p \<circ> (q \<circ> inv q) = r \<circ> (q \<circ> inv q)"
   987       by (simp add: o_assoc)
   988     with permutes_surj[OF q, unfolded surj_iff] show "p = r"
   989       by simp
   990   qed
   991   have th3: "(\<lambda>p. p \<circ> q) ` ?S = ?S"
   992     using image_compose_permutations_right[OF q] by auto
   993   from setsum.reindex[OF th1, of f]
   994   show ?thesis unfolding th0 th1 th3 .
   995 qed
   996 
   997 
   998 subsection \<open>Sum over a set of permutations (could generalize to iteration)\<close>
   999 
  1000 lemma setsum_over_permutations_insert:
  1001   assumes fS: "finite S"
  1002     and aS: "a \<notin> S"
  1003   shows "setsum f {p. p permutes (insert a S)} =
  1004     setsum (\<lambda>b. setsum (\<lambda>q. f (Fun.swap a b id \<circ> q)) {p. p permutes S}) (insert a S)"
  1005 proof -
  1006   have th0: "\<And>f a b. (\<lambda>(b,p). f (Fun.swap a b id \<circ> p)) = f \<circ> (\<lambda>(b,p). Fun.swap a b id \<circ> p)"
  1007     by (simp add: fun_eq_iff)
  1008   have th1: "\<And>P Q. P \<times> Q = {(a,b). a \<in> P \<and> b \<in> Q}"
  1009     by blast
  1010   have th2: "\<And>P Q. P \<Longrightarrow> (P \<Longrightarrow> Q) \<Longrightarrow> P \<and> Q"
  1011     by blast
  1012   show ?thesis
  1013     unfolding permutes_insert
  1014     unfolding setsum.cartesian_product
  1015     unfolding th1[symmetric]
  1016     unfolding th0
  1017   proof (rule setsum.reindex)
  1018     let ?f = "(\<lambda>(b, y). Fun.swap a b id \<circ> y)"
  1019     let ?P = "{p. p permutes S}"
  1020     {
  1021       fix b c p q
  1022       assume b: "b \<in> insert a S"
  1023       assume c: "c \<in> insert a S"
  1024       assume p: "p permutes S"
  1025       assume q: "q permutes S"
  1026       assume eq: "Fun.swap a b id \<circ> p = Fun.swap a c id \<circ> q"
  1027       from p q aS have pa: "p a = a" and qa: "q a = a"
  1028         unfolding permutes_def by metis+
  1029       from eq have "(Fun.swap a b id \<circ> p) a  = (Fun.swap a c id \<circ> q) a"
  1030         by simp
  1031       then have bc: "b = c"
  1032         by (simp add: permutes_def pa qa o_def fun_upd_def Fun.swap_def id_def
  1033             cong del: if_weak_cong split: split_if_asm)
  1034       from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> p) =
  1035         (\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> q)" by simp
  1036       then have "p = q"
  1037         unfolding o_assoc swap_id_idempotent
  1038         by (simp add: o_def)
  1039       with bc have "b = c \<and> p = q"
  1040         by blast
  1041     }
  1042     then show "inj_on ?f (insert a S \<times> ?P)"
  1043       unfolding inj_on_def by clarify metis
  1044   qed
  1045 qed
  1046 
  1047 end
  1048