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.20    by (simp add: Fun.swap_def)
    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.231    by (simp add: sign_def)
   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"