src/HOL/Library/Permutations.thy
 changeset 60500 903bb1495239 parent 59730 b7c394c7a619 child 60601 6e83d94760c4
```     1.1 --- a/src/HOL/Library/Permutations.thy	Wed Jun 17 10:57:11 2015 +0200
1.2 +++ b/src/HOL/Library/Permutations.thy	Wed Jun 17 11:03:05 2015 +0200
1.3 @@ -2,13 +2,13 @@
1.4      Author:     Amine Chaieb, University of Cambridge
1.5  *)
1.6
1.7 -section {* Permutations, both general and specifically on finite sets.*}
1.8 +section \<open>Permutations, both general and specifically on finite sets.\<close>
1.9
1.10  theory Permutations
1.11  imports Binomial
1.12  begin
1.13
1.14 -subsection {* Transpositions *}
1.15 +subsection \<open>Transpositions\<close>
1.16
1.17  lemma swap_id_idempotent [simp]:
1.18    "Fun.swap a b id \<circ> Fun.swap a b id = id"
1.19 @@ -23,7 +23,7 @@
1.21
1.22
1.23 -subsection {* Basic consequences of the definition *}
1.24 +subsection \<open>Basic consequences of the definition\<close>
1.25
1.26  definition permutes  (infixr "permutes" 41)
1.27    where "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"
1.28 @@ -96,7 +96,7 @@
1.29    by (simp add: Ball_def permutes_def) metis
1.30
1.31
1.32 -subsection {* Group properties *}
1.33 +subsection \<open>Group properties\<close>
1.34
1.35  lemma permutes_id: "id permutes S"
1.36    unfolding permutes_def by simp
1.37 @@ -116,7 +116,7 @@
1.38    by blast
1.39
1.40
1.41 -subsection {* The number of permutations on a finite set *}
1.42 +subsection \<open>The number of permutations on a finite set\<close>
1.43
1.44  lemma permutes_insert_lemma:
1.45    assumes pS: "p permutes (insert a S)"
1.46 @@ -186,13 +186,13 @@
1.47      from permutes_insert[of x F]
1.48      have xfgpF': "?xF = ?g ` ?pF'" .
1.49      have Fs: "card F = n - 1"
1.50 -      using `x \<notin> F` H0 `finite F` by auto
1.51 +      using \<open>x \<notin> F\<close> H0 \<open>finite F\<close> by auto
1.52      from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)"
1.53 -      using `finite F` by auto
1.54 +      using \<open>finite F\<close> by auto
1.55      then have "finite ?pF"
1.56        by (auto intro: card_ge_0_finite)
1.57      then have pF'f: "finite ?pF'"
1.58 -      using H0 `finite F`
1.59 +      using H0 \<open>finite F\<close>
1.60        apply (simp only: Collect_split Collect_mem_eq)
1.61        apply (rule finite_cartesian_product)
1.62        apply simp_all
1.63 @@ -208,14 +208,14 @@
1.64          from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F"
1.65            "p permutes F" "q permutes F"
1.66            by auto
1.67 -        from ths(4) `x \<notin> F` eq have "b = ?g (b,p) x"
1.68 +        from ths(4) \<open>x \<notin> F\<close> eq have "b = ?g (b,p) x"
1.69            unfolding permutes_def
1.70            by (auto simp add: Fun.swap_def fun_upd_def fun_eq_iff)
1.71          also have "\<dots> = ?g (c,q) x"
1.72 -          using ths(5) `x \<notin> F` eq
1.73 +          using ths(5) \<open>x \<notin> F\<close> eq
1.74            by (auto simp add: swap_def fun_upd_def fun_eq_iff)
1.75          also have "\<dots> = c"
1.76 -          using ths(5) `x \<notin> F`
1.77 +          using ths(5) \<open>x \<notin> F\<close>
1.78            unfolding permutes_def
1.79            by (auto simp add: Fun.swap_def fun_upd_def fun_eq_iff)
1.80          finally have bc: "b = c" .
1.81 @@ -234,15 +234,15 @@
1.82        then show ?thesis
1.83          unfolding inj_on_def by blast
1.84      qed
1.85 -    from `x \<notin> F` H0 have n0: "n \<noteq> 0"
1.86 -      using `finite F` by auto
1.87 +    from \<open>x \<notin> F\<close> H0 have n0: "n \<noteq> 0"
1.88 +      using \<open>finite F\<close> by auto
1.89      then have "\<exists>m. n = Suc m"
1.90        by presburger
1.91      then obtain m where n[simp]: "n = Suc m"
1.92        by blast
1.93      from pFs H0 have xFc: "card ?xF = fact n"
1.94        unfolding xfgpF' card_image[OF ginj]
1.95 -      using `finite F` `finite ?pF`
1.96 +      using \<open>finite F\<close> \<open>finite ?pF\<close>
1.97        apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
1.98        apply simp
1.99        done
1.100 @@ -262,26 +262,26 @@
1.101    by (auto intro: card_ge_0_finite)
1.102
1.103
1.104 -subsection {* Permutations of index set for iterated operations *}
1.105 +subsection \<open>Permutations of index set for iterated operations\<close>
1.106
1.107  lemma (in comm_monoid_set) permute:
1.108    assumes "p permutes S"
1.109    shows "F g S = F (g \<circ> p) S"
1.110  proof -
1.111 -  from `p permutes S` have "inj p"
1.112 +  from \<open>p permutes S\<close> have "inj p"
1.113      by (rule permutes_inj)
1.114    then have "inj_on p S"
1.115      by (auto intro: subset_inj_on)
1.116    then have "F g (p ` S) = F (g \<circ> p) S"
1.117      by (rule reindex)
1.118 -  moreover from `p permutes S` have "p ` S = S"
1.119 +  moreover from \<open>p permutes S\<close> have "p ` S = S"
1.120      by (rule permutes_image)
1.121    ultimately show ?thesis
1.122      by simp
1.123  qed
1.124
1.125
1.126 -subsection {* Various combinations of transpositions with 2, 1 and 0 common elements *}
1.127 +subsection \<open>Various combinations of transpositions with 2, 1 and 0 common elements\<close>
1.128
1.129  lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow>
1.130    Fun.swap a b id \<circ> Fun.swap a c id = Fun.swap b c id \<circ> Fun.swap a b id"
1.131 @@ -296,7 +296,7 @@
1.132    by (simp add: fun_eq_iff Fun.swap_def)
1.133
1.134
1.135 -subsection {* Permutations as transposition sequences *}
1.136 +subsection \<open>Permutations as transposition sequences\<close>
1.137
1.138  inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
1.139  where
1.140 @@ -308,7 +308,7 @@
1.141  definition "permutation p \<longleftrightarrow> (\<exists>n. swapidseq n p)"
1.142
1.143
1.144 -subsection {* Some closure properties of the set of permutations, with lengths *}
1.145 +subsection \<open>Some closure properties of the set of permutations, with lengths\<close>
1.146
1.147  lemma permutation_id[simp]: "permutation id"
1.148    unfolding permutation_def by (rule exI[where x=0]) simp
1.149 @@ -391,7 +391,7 @@
1.150    using permutation_def swapidseq_inverse by blast
1.151
1.152
1.153 -subsection {* The identity map only has even transposition sequences *}
1.154 +subsection \<open>The identity map only has even transposition sequences\<close>
1.155
1.156  lemma symmetry_lemma:
1.157    assumes "\<And>a b c d. P a b c d \<Longrightarrow> P a b d c"
1.158 @@ -519,7 +519,7 @@
1.159  lemma swapidseq_identity_even:
1.160    assumes "swapidseq n (id :: 'a \<Rightarrow> 'a)"
1.161    shows "even n"
1.162 -  using `swapidseq n id`
1.163 +  using \<open>swapidseq n id\<close>
1.164  proof (induct n rule: nat_less_induct)
1.165    fix n
1.166    assume H: "\<forall>m<n. swapidseq m (id::'a \<Rightarrow> 'a) \<longrightarrow> even m" "swapidseq n (id :: 'a \<Rightarrow> 'a)"
1.167 @@ -544,7 +544,7 @@
1.168  qed
1.169
1.170
1.171 -subsection {* Therefore we have a welldefined notion of parity *}
1.172 +subsection \<open>Therefore we have a welldefined notion of parity\<close>
1.173
1.174  definition "evenperm p = even (SOME n. swapidseq n p)"
1.175
1.176 @@ -573,7 +573,7 @@
1.177    done
1.178
1.179
1.180 -subsection {* And it has the expected composition properties *}
1.181 +subsection \<open>And it has the expected composition properties\<close>
1.182
1.183  lemma evenperm_id[simp]: "evenperm id = True"
1.184    by (rule evenperm_unique[where n = 0]) simp_all
1.185 @@ -608,7 +608,7 @@
1.186  qed
1.187
1.188
1.189 -subsection {* A more abstract characterization of permutations *}
1.190 +subsection \<open>A more abstract characterization of permutations\<close>
1.191
1.192  lemma bij_iff: "bij f \<longleftrightarrow> (\<forall>x. \<exists>!y. f y = x)"
1.193    unfolding bij_def inj_on_def surj_def
1.194 @@ -647,7 +647,7 @@
1.195      let ?S = "insert a (insert b {x. p x \<noteq> x})"
1.196      from comp_Suc.hyps(2) have fS: "finite ?S"
1.197        by simp
1.198 -    from `a \<noteq> b` have th: "{x. (Fun.swap a b id \<circ> p) x \<noteq> x} \<subseteq> ?S"
1.199 +    from \<open>a \<noteq> b\<close> have th: "{x. (Fun.swap a b id \<circ> p) x \<noteq> x} \<subseteq> ?S"
1.200        by (auto simp add: Fun.swap_def)
1.201      from finite_subset[OF th fS] show ?case  .
1.202    qed
1.203 @@ -744,7 +744,7 @@
1.204  qed
1.205
1.206
1.207 -subsection {* Relation to "permutes" *}
1.208 +subsection \<open>Relation to "permutes"\<close>
1.209
1.210  lemma permutation_permutes: "permutation p \<longleftrightarrow> (\<exists>S. finite S \<and> p permutes S)"
1.211    unfolding permutation permutes_def bij_iff[symmetric]
1.212 @@ -757,7 +757,7 @@
1.213    done
1.214
1.215
1.216 -subsection {* Hence a sort of induction principle composing by swaps *}
1.217 +subsection \<open>Hence a sort of induction principle composing by swaps\<close>
1.218
1.219  lemma permutes_induct: "finite S \<Longrightarrow> P id \<Longrightarrow>
1.220    (\<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>
1.221 @@ -788,7 +788,7 @@
1.222  qed
1.223
1.224
1.225 -subsection {* Sign of a permutation as a real number *}
1.226 +subsection \<open>Sign of a permutation as a real number\<close>
1.227
1.228  definition "sign p = (if evenperm p then (1::int) else -1)"
1.229
1.230 @@ -811,7 +811,7 @@
1.232
1.233
1.234 -subsection {* More lemmas about permutations *}
1.235 +subsection \<open>More lemmas about permutations\<close>
1.236
1.237  lemma permutes_natset_le:
1.238    fixes S :: "'a::wellorder set"
1.239 @@ -995,7 +995,7 @@
1.240  qed
1.241
1.242
1.243 -subsection {* Sum over a set of permutations (could generalize to iteration) *}
1.244 +subsection \<open>Sum over a set of permutations (could generalize to iteration)\<close>
1.245
1.246  lemma setsum_over_permutations_insert:
1.247    assumes fS: "finite S"
```