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