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