# HG changeset patch
# User haftmann
# Date 1620151036 0
# Node ID b4b70d13c9959990bbd65baf7a0b68643c98af74
# Parent  58aed6f71f903b72c5f97b77cad73fc2ff857143
collected lemmas on permutations

diff -r 58aed6f71f90 -r b4b70d13c995 src/HOL/Combinatorics/Permutations.thy
--- a/src/HOL/Combinatorics/Permutations.thy	Mon May 03 21:49:30 2021 +0100
+++ b/src/HOL/Combinatorics/Permutations.thy	Tue May 04 17:57:16 2021 +0000
@@ -860,6 +860,10 @@
 lemma evenperm_id[simp]: "evenperm id = True"
   by (rule evenperm_unique[where n = 0]) simp_all
 
+lemma evenperm_identity [simp]:
+  \<open>evenperm (\<lambda>x. x)\<close>
+  using evenperm_id by (simp add: id_def [abs_def])
+
 lemma evenperm_swap: "evenperm (Fun.swap a b id) = (a = b)"
   by (rule evenperm_unique[where n="if a = b then 0 else 1"]) (simp_all add: swapidseq_swap)
 
@@ -1034,12 +1038,20 @@
 subsection \<open>Sign of a permutation as a real number\<close>
 
 definition sign :: \<open>('a \<Rightarrow> 'a) \<Rightarrow> int\<close> \<comment> \<open>TODO: prefer less generic name\<close>
-  where \<open>sign p = (if evenperm p then (1::int) else -1)\<close>
+  where \<open>sign p = (if evenperm p then 1 else - 1)\<close>
 
-lemma sign_nz: "sign p \<noteq> 0"
+lemma sign_cases [case_names even odd]:
+  obtains \<open>sign p = 1\<close> | \<open>sign p = - 1\<close>
+  by (cases \<open>evenperm p\<close>) (simp_all add: sign_def)
+
+lemma sign_nz [simp]: "sign p \<noteq> 0"
+  by (cases p rule: sign_cases) simp_all
+
+lemma sign_id [simp]: "sign id = 1"
   by (simp add: sign_def)
 
-lemma sign_id: "sign id = 1"
+lemma sign_identity [simp]:
+  \<open>sign (\<lambda>x. x) = 1\<close>
   by (simp add: sign_def)
 
 lemma sign_inverse: "permutation p \<Longrightarrow> sign (inv p) = sign p"
@@ -1048,12 +1060,18 @@
 lemma sign_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> sign (p \<circ> q) = sign p * sign q"
   by (simp add: sign_def evenperm_comp)
 
-lemma sign_swap_id: "sign (Fun.swap a b id) = (if a = b then 1 else -1)"
+lemma sign_swap_id: "sign (Fun.swap a b id) = (if a = b then 1 else - 1)"
   by (simp add: sign_def evenperm_swap)
 
-lemma sign_idempotent: "sign p * sign p = 1"
+lemma sign_idempotent [simp]: "sign p * sign p = 1"
   by (simp add: sign_def)
 
+lemma sign_left_idempotent [simp]:
+  \<open>sign p * (sign p * sign q) = sign q\<close>
+  by (simp add: sign_def)
+
+term "(bij, bij_betw, permutation)"
+
 
 subsection \<open>Permuting a list\<close>
 
@@ -1472,6 +1490,97 @@
     by (simp only:)
 qed
 
+lemma inv_inj_on_permutes:
+  \<open>inj_on inv {p. p permutes S}\<close>
+proof (intro inj_onI, unfold mem_Collect_eq)
+  fix p q
+  assume p: "p permutes S" and q: "q permutes S" and eq: "inv p = inv q"
+  have "inv (inv p) = inv (inv q)" using eq by simp
+  thus "p = q"
+    using inv_inv_eq[OF permutes_bij] p q by metis
+qed
+
+lemma permutes_pair_eq:
+  \<open>{(p s, s) |s. s \<in> S} = {(s, inv p s) |s. s \<in> S}\<close> (is \<open>?L = ?R\<close>) if \<open>p permutes S\<close>
+proof
+  show "?L \<subseteq> ?R"
+  proof
+    fix x assume "x \<in> ?L"
+    then obtain s where x: "x = (p s, s)" and s: "s \<in> S" by auto
+    note x
+    also have "(p s, s) = (p s, Hilbert_Choice.inv p (p s))"
+      using permutes_inj [OF that] inv_f_f by auto
+    also have "... \<in> ?R" using s permutes_in_image[OF that] by auto
+    finally show "x \<in> ?R".
+  qed
+  show "?R \<subseteq> ?L"
+  proof
+    fix x assume "x \<in> ?R"
+    then obtain s
+      where x: "x = (s, Hilbert_Choice.inv p s)" (is "_ = (s, ?ips)")
+        and s: "s \<in> S" by auto
+    note x
+    also have "(s, ?ips) = (p ?ips, ?ips)"
+      using inv_f_f[OF permutes_inj[OF permutes_inv[OF that]]]
+      using inv_inv_eq[OF permutes_bij[OF that]] by auto
+    also have "... \<in> ?L"
+      using s permutes_in_image[OF permutes_inv[OF that]] by auto
+    finally show "x \<in> ?L".
+  qed
+qed
+
+context
+  fixes p and n i :: nat
+  assumes p: \<open>p permutes {0..<n}\<close> and i: \<open>i < n\<close>
+begin
+
+lemma permutes_nat_less:
+  \<open>p i < n\<close>
+proof -
+  have \<open>?thesis \<longleftrightarrow> p i \<in> {0..<n}\<close>
+    by simp
+  also from p have \<open>p i \<in> {0..<n} \<longleftrightarrow> i \<in> {0..<n}\<close>
+    by (rule permutes_in_image)
+  finally show ?thesis
+    using i by simp
+qed
+
+lemma permutes_nat_inv_less:
+  \<open>inv p i < n\<close>
+proof -
+  from p have \<open>inv p permutes {0..<n}\<close>
+    by (rule permutes_inv)
+  then show ?thesis
+    using i by (rule Permutations.permutes_nat_less)
+qed
+
+end
+
+context comm_monoid_set
+begin
+
+lemma permutes_inv:
+  \<open>F (\<lambda>s. g (p s) s) S = F (\<lambda>s. g s (inv p s)) S\<close> (is \<open>?l = ?r\<close>)
+  if \<open>p permutes S\<close>
+proof -
+  let ?g = "\<lambda>(x, y). g x y"
+  let ?ps = "\<lambda>s. (p s, s)"
+  let ?ips = "\<lambda>s. (s, inv p s)"
+  have inj1: "inj_on ?ps S" by (rule inj_onI) auto
+  have inj2: "inj_on ?ips S" by (rule inj_onI) auto
+  have "?l = F ?g (?ps ` S)"
+    using reindex [OF inj1, of ?g] by simp
+  also have "?ps ` S = {(p s, s) |s. s \<in> S}" by auto
+  also have "... = {(s, inv p s) |s. s \<in> S}"
+    unfolding permutes_pair_eq [OF that] by simp
+  also have "... = ?ips ` S" by auto
+  also have "F ?g ... = ?r"
+    using reindex [OF inj2, of ?g] by simp
+  finally show ?thesis.
+qed
+
+end
+
 
 subsection \<open>Sum over a set of permutations (could generalize to iteration)\<close>