# HG changeset patch
# User haftmann
# Date 1618126524 0
# Node ID 92783562ab78aa0ab1759407b4b25030b3fa9d22
# Parent  c973b530002512437cc79109b10d1ab54d4cbd51
collected combinatorial material

diff -r c973b5300025 -r 92783562ab78 src/HOL/Combinatorics/Orbits.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Combinatorics/Orbits.thy	Sun Apr 11 07:35:24 2021 +0000
@@ -0,0 +1,594 @@
+(*  Author:     Lars Noschinski
+*)
+
+section \<open>Permutation orbits\<close>
+
+theory Orbits
+imports
+  "HOL-Library.FuncSet"
+  "HOL-Combinatorics.Permutations"
+begin
+
+subsection \<open>Orbits and cyclic permutations\<close>
+
+inductive_set orbit :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a set" for f x where
+  base: "f x \<in> orbit f x" |
+  step: "y \<in> orbit f x \<Longrightarrow> f y \<in> orbit f x"
+
+definition cyclic_on :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> bool" where
+  "cyclic_on f S \<longleftrightarrow> (\<exists>s\<in>S. S = orbit f s)"
+
+lemma orbit_altdef: "orbit f x = {(f ^^ n) x | n. 0 < n}" (is "?L = ?R")
+proof (intro set_eqI iffI)
+  fix y assume "y \<in> ?L" then show "y \<in> ?R"
+    by (induct rule: orbit.induct) (auto simp: exI[where x=1] exI[where x="Suc n" for n])
+next
+  fix y assume "y \<in> ?R"
+  then obtain n where "y = (f ^^ n) x" "0 < n" by blast
+  then show "y \<in> ?L"
+  proof (induction n arbitrary: y)
+    case (Suc n) then show ?case by (cases "n = 0") (auto intro: orbit.intros)
+  qed simp
+qed
+
+lemma orbit_trans:
+  assumes "s \<in> orbit f t" "t \<in> orbit f u" shows "s \<in> orbit f u"
+  using assms by induct (auto intro: orbit.intros)
+
+lemma orbit_subset:
+  assumes "s \<in> orbit f (f t)" shows "s \<in> orbit f t"
+  using assms by (induct) (auto intro: orbit.intros)
+
+lemma orbit_sim_step:
+  assumes "s \<in> orbit f t" shows "f s \<in> orbit f (f t)"
+  using assms by induct (auto intro: orbit.intros)
+
+lemma orbit_step:
+  assumes "y \<in> orbit f x" "f x \<noteq> y" shows "y \<in> orbit f (f x)"
+  using assms
+proof induction
+  case (step y) then show ?case by (cases "x = y") (auto intro: orbit.intros)
+qed simp
+
+lemma self_in_orbit_trans:
+  assumes "s \<in> orbit f s" "t \<in> orbit f s" shows "t \<in> orbit f t"
+  using assms(2,1) by induct (auto intro: orbit_sim_step)
+
+lemma orbit_swap:
+  assumes "s \<in> orbit f s" "t \<in> orbit f s" shows "s \<in> orbit f t"
+  using assms(2,1)
+proof induction
+  case base then show ?case by (cases "f s = s") (auto intro: orbit_step)
+next
+  case (step x) then show ?case by (cases "f x = s") (auto intro: orbit_step)
+qed
+
+lemma permutation_self_in_orbit:
+  assumes "permutation f" shows "s \<in> orbit f s"
+  unfolding orbit_altdef using permutation_self[OF assms, of s] by simp metis
+
+lemma orbit_altdef_self_in:
+  assumes "s \<in> orbit f s" shows "orbit f s = {(f ^^ n) s | n. True}"
+proof (intro set_eqI iffI)
+  fix x assume "x \<in> {(f ^^ n) s | n. True}"
+  then obtain n where "x = (f ^^ n) s" by auto
+  then show "x \<in> orbit f s" using assms by (cases "n = 0") (auto simp: orbit_altdef)
+qed (auto simp: orbit_altdef)
+
+lemma orbit_altdef_permutation:
+  assumes "permutation f" shows "orbit f s = {(f ^^ n) s | n. True}"
+  using assms by (intro orbit_altdef_self_in permutation_self_in_orbit)
+
+lemma orbit_altdef_bounded:
+  assumes "(f ^^ n) s = s" "0 < n" shows "orbit f s = {(f ^^ m) s| m. m < n}"
+proof -
+  from assms have "s \<in> orbit f s"
+    by (auto simp add: orbit_altdef) metis 
+  then have "orbit f s = {(f ^^ m) s|m. True}" by (rule orbit_altdef_self_in)
+  also have "\<dots> = {(f ^^ m) s| m. m < n}"
+    using assms
+    by (auto simp: funpow_mod_eq intro: exI[where x="m mod n" for m])
+  finally show ?thesis .
+qed
+
+lemma funpow_in_orbit:
+  assumes "s \<in> orbit f t" shows "(f ^^ n) s \<in> orbit f t"
+  using assms by (induct n) (auto intro: orbit.intros)
+
+lemma finite_orbit:
+  assumes "s \<in> orbit f s" shows "finite (orbit f s)"
+proof -
+  from assms obtain n where n: "0 < n" "(f ^^ n) s = s"
+    by (auto simp: orbit_altdef)
+  then show ?thesis by (auto simp: orbit_altdef_bounded)
+qed
+
+lemma self_in_orbit_step:
+  assumes "s \<in> orbit f s" shows "orbit f (f s) = orbit f s"
+proof (intro set_eqI iffI)
+  fix t assume "t \<in> orbit f s" then show "t \<in> orbit f (f s)"
+    using assms by (auto intro: orbit_step orbit_sim_step)
+qed (auto intro: orbit_subset)
+
+lemma permutation_orbit_step:
+  assumes "permutation f" shows "orbit f (f s) = orbit f s"
+  using assms by (intro self_in_orbit_step permutation_self_in_orbit)
+
+lemma orbit_nonempty:
+  "orbit f s \<noteq> {}"
+  using orbit.base by fastforce
+
+lemma orbit_inv_eq:
+  assumes "permutation f"
+  shows "orbit (inv f) x = orbit f x" (is "?L = ?R")
+proof -
+  { fix g y assume A: "permutation g" "y \<in> orbit (inv g) x"
+    have "y \<in> orbit g x"
+    proof -
+      have inv_g: "\<And>y. x = g y \<Longrightarrow> inv g x = y" "\<And>y. inv g (g y) = y"
+        by (metis A(1) bij_inv_eq_iff permutation_bijective)+
+
+      { fix y assume "y \<in> orbit g x"
+        then have "inv g y \<in> orbit g x"
+          by (cases) (simp_all add: inv_g A(1) permutation_self_in_orbit)
+      } note inv_g_in_orb = this
+
+      from A(2) show ?thesis
+        by induct (simp_all add: inv_g_in_orb A permutation_self_in_orbit)
+    qed
+  } note orb_inv_ss = this
+
+  have "inv (inv f) = f"
+    by (simp add: assms inv_inv_eq permutation_bijective)
+  then show ?thesis
+    using orb_inv_ss[OF assms] orb_inv_ss[OF permutation_inverse[OF assms]] by auto
+qed
+
+lemma cyclic_on_alldef:
+  "cyclic_on f S \<longleftrightarrow> S \<noteq> {} \<and> (\<forall>s\<in>S. S = orbit f s)"
+  unfolding cyclic_on_def by (auto intro: orbit.step orbit_swap orbit_trans)
+
+lemma cyclic_on_funpow_in:
+  assumes "cyclic_on f S" "s \<in> S" shows "(f^^n) s \<in> S"
+  using assms unfolding cyclic_on_def by (auto intro: funpow_in_orbit)
+
+lemma finite_cyclic_on:
+  assumes "cyclic_on f S" shows "finite S"
+  using assms by (auto simp: cyclic_on_def finite_orbit)
+
+lemma cyclic_on_singleI:
+  assumes "s \<in> S" "S = orbit f s" shows "cyclic_on f S"
+  using assms unfolding cyclic_on_def by blast
+
+lemma cyclic_on_inI:
+  assumes "cyclic_on f S" "s \<in> S" shows "f s \<in> S"
+  using assms by (auto simp: cyclic_on_def intro: orbit.intros)
+
+lemma orbit_inverse:
+  assumes self: "a \<in> orbit g a"
+    and eq: "\<And>x. x \<in> orbit g a \<Longrightarrow> g' (f x) = f (g x)"
+  shows "f ` orbit g a = orbit g' (f a)" (is "?L = ?R")
+proof (intro set_eqI iffI)
+  fix x assume "x \<in> ?L"
+  then obtain x0 where "x0 \<in> orbit g a" "x = f x0" by auto
+  then show "x \<in> ?R"
+  proof (induct arbitrary: x)
+    case base then show ?case by (auto simp: self orbit.base eq[symmetric])
+  next
+    case step then show ?case by cases (auto simp: eq[symmetric] orbit.intros)
+  qed
+next
+  fix x assume "x \<in> ?R"
+  then show "x \<in> ?L"
+  proof (induct arbitrary: )
+    case base then show ?case by (auto simp: self orbit.base eq)
+  next
+    case step then show ?case by cases (auto simp: eq orbit.intros)
+  qed
+qed
+
+lemma cyclic_on_image:
+  assumes "cyclic_on f S"
+  assumes "\<And>x. x \<in> S \<Longrightarrow> g (h x) = h (f x)"
+  shows "cyclic_on g (h ` S)"
+  using assms by (auto simp: cyclic_on_def) (meson orbit_inverse)
+
+lemma cyclic_on_f_in:
+  assumes "f permutes S" "cyclic_on f A" "f x \<in> A"
+  shows "x \<in> A"
+proof -
+  from assms have fx_in_orb: "f x \<in> orbit f (f x)" by (auto simp: cyclic_on_alldef)
+  from assms have "A = orbit f (f x)" by (auto simp: cyclic_on_alldef)
+  moreover
+  then have "\<dots> = orbit f x" using \<open>f x \<in> A\<close> by (auto intro: orbit_step orbit_subset)
+  ultimately
+    show ?thesis by (metis (no_types) orbit.simps permutes_inverses(2)[OF assms(1)])
+qed
+
+lemma orbit_cong0:
+  assumes "x \<in> A" "f \<in> A \<rightarrow> A" "\<And>y. y \<in> A \<Longrightarrow> f y = g y" shows "orbit f x = orbit g x"
+proof -
+  { fix n have "(f ^^ n) x = (g ^^ n) x \<and> (f ^^ n) x \<in> A"
+      by (induct n rule: nat.induct) (insert assms, auto)
+  } then show ?thesis by (auto simp: orbit_altdef)
+qed
+
+lemma orbit_cong:
+  assumes self_in: "t \<in> orbit f t" and eq: "\<And>s. s \<in> orbit f t \<Longrightarrow> g s = f s"
+  shows "orbit g t = orbit f t"
+  using assms(1) _ assms(2) by (rule orbit_cong0) (auto simp: orbit.step eq)
+
+lemma cyclic_cong:
+  assumes "\<And>s. s \<in> S \<Longrightarrow> f s = g s" shows "cyclic_on f S = cyclic_on g S"
+proof -
+  have "(\<exists>s\<in>S. orbit f s = orbit g s) \<Longrightarrow> cyclic_on f S = cyclic_on g S"
+    by (metis cyclic_on_alldef cyclic_on_def)
+  then show ?thesis by (metis assms orbit_cong cyclic_on_def)
+qed
+
+lemma permutes_comp_preserves_cyclic1:
+  assumes "g permutes B" "cyclic_on f C"
+  assumes "A \<inter> B = {}" "C \<subseteq> A"
+  shows "cyclic_on (f o g) C"
+proof -
+  have *: "\<And>c. c \<in> C \<Longrightarrow> f (g c) = f c"
+    using assms by (subst permutes_not_in [of g]) auto
+  with assms(2) show ?thesis by (simp cong: cyclic_cong)
+qed
+
+lemma permutes_comp_preserves_cyclic2:
+  assumes "f permutes A" "cyclic_on g C"
+  assumes "A \<inter> B = {}" "C \<subseteq> B"
+  shows "cyclic_on (f o g) C"
+proof -
+  obtain c where c: "c \<in> C" "C = orbit g c" "c \<in> orbit g c"
+    using \<open>cyclic_on g C\<close> by (auto simp: cyclic_on_def)
+  then have "\<And>c. c \<in> C \<Longrightarrow> f (g c) = g c"
+    using assms c by (subst permutes_not_in [of f]) (auto intro: orbit.intros)
+  with assms(2) show ?thesis by (simp cong: cyclic_cong)
+qed
+
+lemma permutes_orbit_subset:
+  assumes "f permutes S" "x \<in> S" shows "orbit f x \<subseteq> S"
+proof
+  fix y assume "y \<in> orbit f x"
+  then show "y \<in> S" by induct (auto simp: permutes_in_image assms)
+qed
+
+lemma cyclic_on_orbit':
+  assumes "permutation f" shows "cyclic_on f (orbit f x)"
+  unfolding cyclic_on_alldef using orbit_nonempty[of f x]
+  by (auto intro: assms orbit_swap orbit_trans permutation_self_in_orbit)
+
+lemma cyclic_on_orbit:
+  assumes "f permutes S" "finite S" shows "cyclic_on f (orbit f x)"
+  using assms by (intro cyclic_on_orbit') (auto simp: permutation_permutes)
+
+lemma orbit_cyclic_eq3:
+  assumes "cyclic_on f S" "y \<in> S" shows "orbit f y = S"
+  using assms unfolding cyclic_on_alldef by simp
+
+lemma orbit_eq_singleton_iff: "orbit f x = {x} \<longleftrightarrow> f x = x" (is "?L \<longleftrightarrow> ?R")
+proof
+  assume A: ?R
+  { fix y assume "y \<in> orbit f x" then have "y = x"
+      by induct (auto simp: A)
+  } then show ?L by (metis orbit_nonempty singletonI subsetI subset_singletonD)
+next
+  assume A: ?L
+  then have "\<And>y. y \<in> orbit f x \<Longrightarrow> f x = y"
+    by - (erule orbit.cases, simp_all)
+  then show ?R using A by blast
+qed
+
+lemma eq_on_cyclic_on_iff1:
+  assumes "cyclic_on f S" "x \<in> S"
+  obtains "f x \<in> S" "f x = x \<longleftrightarrow> card S = 1"
+proof
+  from assms show "f x \<in> S" by (auto simp: cyclic_on_def intro: orbit.intros)
+  from assms have "S = orbit f x" by (auto simp: cyclic_on_alldef)
+  then have "f x = x \<longleftrightarrow> S = {x}" by (metis orbit_eq_singleton_iff)
+  then show "f x = x \<longleftrightarrow> card S = 1" using \<open>x \<in> S\<close> by (auto simp: card_Suc_eq)
+qed
+
+lemma orbit_eqI:
+  "y = f x \<Longrightarrow> y \<in> orbit f x"
+  "z = f y \<Longrightarrow>y \<in> orbit f x \<Longrightarrow>z \<in> orbit f x"
+  by (metis orbit.base) (metis orbit.step)
+
+
+subsection \<open>Decomposition of arbitrary permutations\<close>
+
+definition perm_restrict :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'a)" where
+  "perm_restrict f S x \<equiv> if x \<in> S then f x else x"
+
+lemma perm_restrict_comp:
+  assumes "A \<inter> B = {}" "cyclic_on f B"
+  shows "perm_restrict f A o perm_restrict f B = perm_restrict f (A \<union> B)"
+proof -
+  have "\<And>x. x \<in> B \<Longrightarrow> f x \<in> B" using \<open>cyclic_on f B\<close> by (rule cyclic_on_inI)
+  with assms show ?thesis by (auto simp: perm_restrict_def fun_eq_iff)
+qed
+
+lemma perm_restrict_simps:
+  "x \<in> S \<Longrightarrow> perm_restrict f S x = f x"
+  "x \<notin> S \<Longrightarrow> perm_restrict f S x = x"
+  by (auto simp: perm_restrict_def)
+
+lemma perm_restrict_perm_restrict:
+  "perm_restrict (perm_restrict f A) B = perm_restrict f (A \<inter> B)"
+  by (auto simp: perm_restrict_def)
+
+lemma perm_restrict_union:
+  assumes "perm_restrict f A permutes A" "perm_restrict f B permutes B" "A \<inter> B = {}"
+  shows "perm_restrict f A o perm_restrict f B = perm_restrict f (A \<union> B)"
+  using assms by (auto simp: fun_eq_iff perm_restrict_def permutes_def) (metis Diff_iff Diff_triv)
+
+lemma perm_restrict_id[simp]:
+  assumes "f permutes S" shows "perm_restrict f S = f"
+  using assms by (auto simp: permutes_def perm_restrict_def)
+
+lemma cyclic_on_perm_restrict:
+  "cyclic_on (perm_restrict f S) S \<longleftrightarrow> cyclic_on f S"
+  by (simp add: perm_restrict_def cong: cyclic_cong)
+
+lemma perm_restrict_diff_cyclic:
+  assumes "f permutes S" "cyclic_on f A"
+  shows "perm_restrict f (S - A) permutes (S - A)"
+proof -
+  { fix y
+    have "\<exists>x. perm_restrict f (S - A) x = y"
+    proof cases
+      assume A: "y \<in> S - A"
+      with \<open>f permutes S\<close> obtain x where "f x = y" "x \<in> S"
+        unfolding permutes_def by auto metis
+      moreover
+      with A have "x \<notin> A" by (metis Diff_iff assms(2) cyclic_on_inI)
+      ultimately
+      have "perm_restrict f (S - A) x = y"  by (simp add: perm_restrict_simps)
+      then show ?thesis ..
+    next
+      assume "y \<notin> S - A"
+      then have "perm_restrict f (S - A) y = y" by (simp add: perm_restrict_simps)
+      then show ?thesis ..
+    qed
+  } note X = this
+
+  { fix x y assume "perm_restrict f (S - A) x = perm_restrict f (S - A) y"
+    with assms have "x = y"
+      by (auto simp: perm_restrict_def permutes_def split: if_splits intro: cyclic_on_f_in)
+  } note Y = this
+
+  show ?thesis by (auto simp: permutes_def perm_restrict_simps X intro: Y)
+qed
+
+lemma permutes_decompose:
+  assumes "f permutes S" "finite S"
+  shows "\<exists>C. (\<forall>c \<in> C. cyclic_on f c) \<and> \<Union>C = S \<and> (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {})"
+  using assms(2,1)
+proof (induction arbitrary: f rule: finite_psubset_induct)
+  case (psubset S)
+
+  show ?case
+  proof (cases "S = {}")
+    case True then show ?thesis by (intro exI[where x="{}"]) auto
+  next
+    case False
+    then obtain s where "s \<in> S" by auto
+    with \<open>f permutes S\<close> have "orbit f s \<subseteq> S"
+      by (rule permutes_orbit_subset)
+    have cyclic_orbit: "cyclic_on f (orbit f s)"
+      using \<open>f permutes S\<close> \<open>finite S\<close> by (rule cyclic_on_orbit)
+
+    let ?f' = "perm_restrict f (S - orbit f s)"
+
+    have "f s \<in> S" using \<open>f permutes S\<close> \<open>s \<in> S\<close> by (auto simp: permutes_in_image)
+    then have "S - orbit f s \<subset> S" using orbit.base[of f s] \<open>s \<in> S\<close> by blast
+    moreover
+    have "?f' permutes (S - orbit f s)"
+      using \<open>f permutes S\<close> cyclic_orbit by (rule perm_restrict_diff_cyclic)
+    ultimately
+    obtain C where C: "\<And>c. c \<in> C \<Longrightarrow> cyclic_on ?f' c" "\<Union>C = S - orbit f s"
+        "\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {}"
+      using psubset.IH by metis
+
+    { fix c assume "c \<in> C"
+      then have *: "\<And>x. x \<in> c \<Longrightarrow> perm_restrict f (S - orbit f s) x = f x"
+        using C(2) \<open>f permutes S\<close> by (auto simp add: perm_restrict_def)
+      then have "cyclic_on f c" using C(1)[OF \<open>c \<in> C\<close>] by (simp cong: cyclic_cong add: *)
+    } note in_C_cyclic = this
+
+    have Un_ins: "\<Union>(insert (orbit f s) C) = S"
+      using \<open>\<Union>C = _\<close>  \<open>orbit f s \<subseteq> S\<close> by blast
+
+    have Disj_ins: "(\<forall>c1 \<in> insert (orbit f s) C. \<forall>c2 \<in> insert (orbit f s) C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {})"
+      using C by auto
+
+    show ?thesis
+      by (intro conjI Un_ins Disj_ins exI[where x="insert (orbit f s) C"])
+        (auto simp: cyclic_orbit in_C_cyclic)
+  qed
+qed
+
+
+subsection \<open>Function-power distance between values\<close>
+
+definition funpow_dist :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> nat" where
+  "funpow_dist f x y \<equiv> LEAST n. (f ^^ n) x = y"
+
+abbreviation funpow_dist1 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> nat" where
+  "funpow_dist1 f x y \<equiv> Suc (funpow_dist f (f x) y)"
+
+lemma funpow_dist_0:
+  assumes "x = y" shows "funpow_dist f x y = 0"
+  using assms unfolding funpow_dist_def by (intro Least_eq_0) simp
+
+lemma funpow_dist_least:
+  assumes "n < funpow_dist f x y" shows "(f ^^ n) x \<noteq> y"
+proof (rule notI)
+  assume "(f ^^ n) x = y"
+  then have "funpow_dist f x y \<le> n" unfolding funpow_dist_def by (rule Least_le)
+  with assms show False by linarith
+qed
+
+lemma funpow_dist1_least:
+  assumes "0 < n" "n < funpow_dist1 f x y" shows "(f ^^ n) x \<noteq> y"
+proof (rule notI)
+  assume "(f ^^ n) x = y"
+  then have "(f ^^ (n - 1)) (f x) = y"
+    using \<open>0 < n\<close> by (cases n) (simp_all add: funpow_swap1)
+  then have "funpow_dist f (f x) y \<le> n - 1" unfolding funpow_dist_def by (rule Least_le)
+  with assms show False by simp
+qed
+
+lemma funpow_dist_prop:
+  "y \<in> orbit f x \<Longrightarrow> (f ^^ funpow_dist f x y) x = y"
+  unfolding funpow_dist_def by (rule LeastI_ex) (auto simp: orbit_altdef)
+
+lemma funpow_dist_0_eq:
+  assumes "y \<in> orbit f x" shows "funpow_dist f x y = 0 \<longleftrightarrow> x = y"
+  using assms by (auto simp: funpow_dist_0 dest: funpow_dist_prop)
+
+lemma funpow_dist_step:
+  assumes "x \<noteq> y" "y \<in> orbit f x" shows "funpow_dist f x y = Suc (funpow_dist f (f x) y)"
+proof -
+  from \<open>y \<in> _\<close> obtain n where "(f ^^ n) x = y" by (auto simp: orbit_altdef)
+  with \<open>x \<noteq> y\<close> obtain n' where [simp]: "n = Suc n'" by (cases n) auto
+
+  show ?thesis
+    unfolding funpow_dist_def
+  proof (rule Least_Suc2)
+    show "(f ^^ n) x = y" by fact
+    then show "(f ^^ n') (f x) = y" by (simp add: funpow_swap1)
+    show "(f ^^ 0) x \<noteq> y" using \<open>x \<noteq> y\<close> by simp
+    show "\<forall>k. ((f ^^ Suc k) x = y) = ((f ^^ k) (f x) = y)"
+      by (simp add: funpow_swap1)
+  qed
+qed
+
+lemma funpow_dist1_prop:
+  assumes "y \<in> orbit f x" shows "(f ^^ funpow_dist1 f x y) x = y"
+  by (metis assms funpow_dist_prop funpow_dist_step funpow_simps_right(2) o_apply self_in_orbit_step)
+
+(*XXX simplify? *)
+lemma funpow_neq_less_funpow_dist:
+  assumes "y \<in> orbit f x" "m \<le> funpow_dist f x y" "n \<le> funpow_dist f x y" "m \<noteq> n"
+  shows "(f ^^ m) x \<noteq> (f ^^ n) x"
+proof (rule notI)
+  assume A: "(f ^^ m) x = (f ^^ n) x"
+
+  define m' n' where "m' = min m n" and "n' = max m n"
+  with A assms have A': "m' < n'" "(f ^^ m') x = (f ^^ n') x" "n' \<le> funpow_dist f x y"
+    by (auto simp: min_def max_def)
+
+  have "y = (f ^^ funpow_dist f x y) x"
+    using \<open>y \<in> _\<close> by (simp only: funpow_dist_prop)
+  also have "\<dots> = (f ^^ ((funpow_dist f x y - n') + n')) x"
+    using \<open>n' \<le> _\<close> by simp
+  also have "\<dots> = (f ^^ ((funpow_dist f x y - n') + m')) x"
+    by (simp add: funpow_add \<open>(f ^^ m') x = _\<close>)
+  also have "(f ^^ ((funpow_dist f x y - n') + m')) x \<noteq> y"
+    using A' by (intro funpow_dist_least) linarith
+  finally show "False" by simp
+qed
+
+(* XXX reduce to funpow_neq_less_funpow_dist? *)
+lemma funpow_neq_less_funpow_dist1:
+  assumes "y \<in> orbit f x" "m < funpow_dist1 f x y" "n < funpow_dist1 f x y" "m \<noteq> n"
+  shows "(f ^^ m) x \<noteq> (f ^^ n) x"
+proof (rule notI)
+  assume A: "(f ^^ m) x = (f ^^ n) x"
+
+  define m' n' where "m' = min m n" and "n' = max m n"
+  with A assms have A': "m' < n'" "(f ^^ m') x = (f ^^ n') x" "n' < funpow_dist1 f x y"
+    by (auto simp: min_def max_def)
+
+  have "y = (f ^^ funpow_dist1 f x y) x"
+    using \<open>y \<in> _\<close> by (simp only: funpow_dist1_prop)
+  also have "\<dots> = (f ^^ ((funpow_dist1 f x y - n') + n')) x"
+    using \<open>n' < _\<close> by simp
+  also have "\<dots> = (f ^^ ((funpow_dist1 f x y - n') + m')) x"
+    by (simp add: funpow_add \<open>(f ^^ m') x = _\<close>)
+  also have "(f ^^ ((funpow_dist1 f x y - n') + m')) x \<noteq> y"
+    using A' by (intro funpow_dist1_least) linarith+
+  finally show "False" by simp
+qed
+
+lemma inj_on_funpow_dist:
+  assumes "y \<in> orbit f x" shows "inj_on (\<lambda>n. (f ^^ n) x) {0..funpow_dist f x y}"
+  using funpow_neq_less_funpow_dist[OF assms] by (intro inj_onI) auto
+
+lemma inj_on_funpow_dist1:
+  assumes "y \<in> orbit f x" shows "inj_on (\<lambda>n. (f ^^ n) x) {0..<funpow_dist1 f x y}"
+  using funpow_neq_less_funpow_dist1[OF assms] by (intro inj_onI) auto
+
+lemma orbit_conv_funpow_dist1:
+  assumes "x \<in> orbit f x"
+  shows "orbit f x = (\<lambda>n. (f ^^ n) x) ` {0..<funpow_dist1 f x x}" (is "?L = ?R")
+  using funpow_dist1_prop[OF assms]
+  by (auto simp: orbit_altdef_bounded[where n="funpow_dist1 f x x"])
+
+lemma funpow_dist1_prop1:
+  assumes "(f ^^ n) x = y" "0 < n" shows "(f ^^ funpow_dist1 f x y) x = y"
+proof -
+  from assms have "y \<in> orbit f x" by (auto simp: orbit_altdef)
+  then show ?thesis by (rule funpow_dist1_prop)
+qed
+
+lemma funpow_dist1_dist:
+  assumes "funpow_dist1 f x y < funpow_dist1 f x z"
+  assumes "{y,z} \<subseteq> orbit f x"
+  shows "funpow_dist1 f x z = funpow_dist1 f x y + funpow_dist1 f y z" (is "?L = ?R")
+proof -
+  define n where \<open>n = funpow_dist1 f x z - funpow_dist1 f x y - 1\<close>
+  with assms have *: \<open>funpow_dist1 f x z = Suc (funpow_dist1 f x y + n)\<close>
+    by simp
+  have x_z: "(f ^^ funpow_dist1 f x z) x = z" using assms by (blast intro: funpow_dist1_prop)
+  have x_y: "(f ^^ funpow_dist1 f x y) x = y" using assms by (blast intro: funpow_dist1_prop)
+
+  have "(f ^^ (funpow_dist1 f x z - funpow_dist1 f x y)) y
+      = (f ^^ (funpow_dist1 f x z - funpow_dist1 f x y)) ((f ^^ funpow_dist1 f x y) x)"
+    using x_y by simp
+  also have "\<dots> = z"
+    using assms x_z by (simp add: * funpow_add ac_simps funpow_swap1)
+  finally have y_z_diff: "(f ^^ (funpow_dist1 f x z - funpow_dist1 f x y)) y = z" .
+  then have "(f ^^ funpow_dist1 f y z) y = z"
+    using assms by (intro funpow_dist1_prop1) auto
+  then have "(f ^^ funpow_dist1 f y z) ((f ^^ funpow_dist1 f x y) x) = z"
+    using x_y by simp
+  then have "(f ^^ (funpow_dist1 f y z + funpow_dist1 f x y)) x = z"
+    by (simp add: * funpow_add funpow_swap1)
+  show ?thesis
+  proof (rule antisym)
+    from y_z_diff have "(f ^^ funpow_dist1 f y z) y = z"
+      using assms by (intro funpow_dist1_prop1) auto
+    then have "(f ^^ funpow_dist1 f y z) ((f ^^ funpow_dist1 f x y) x) = z"
+      using x_y by simp
+    then have "(f ^^ (funpow_dist1 f y z + funpow_dist1 f x y)) x = z"
+      by (simp add: * funpow_add funpow_swap1)
+    then have "funpow_dist1 f x z \<le> funpow_dist1 f y z + funpow_dist1 f x y"
+      using funpow_dist1_least not_less by fastforce
+    then show "?L \<le> ?R" by presburger
+  next
+    have "funpow_dist1 f y z \<le> funpow_dist1 f x z - funpow_dist1 f x y"
+      using y_z_diff assms(1) by (metis not_less zero_less_diff funpow_dist1_least)
+    then show "?R \<le> ?L" by linarith
+  qed
+qed
+
+lemma funpow_dist1_le_self:
+  assumes "(f ^^ m) x = x" "0 < m" "y \<in> orbit f x"
+  shows "funpow_dist1 f x y \<le> m"
+proof (cases "x = y")
+  case True with assms show ?thesis by (auto dest!: funpow_dist1_least)
+next
+  case False
+  have "(f ^^ funpow_dist1 f x y) x = (f ^^ (funpow_dist1 f x y mod m)) x"
+    using assms by (simp add: funpow_mod_eq)
+  with False \<open>y \<in> orbit f x\<close> have "funpow_dist1 f x y \<le> funpow_dist1 f x y mod m"
+    by auto (metis \<open>(f ^^ funpow_dist1 f x y) x = (f ^^ (funpow_dist1 f x y mod m)) x\<close> funpow_dist1_prop funpow_dist_least funpow_dist_step leI)
+  with \<open>m > 0\<close> show ?thesis
+    by (auto intro: order_trans)
+qed
+
+end
\ No newline at end of file
diff -r c973b5300025 -r 92783562ab78 src/HOL/Combinatorics/Permutations.thy
--- a/src/HOL/Combinatorics/Permutations.thy	Sat Apr 10 20:22:07 2021 +0200
+++ b/src/HOL/Combinatorics/Permutations.thy	Sun Apr 11 07:35:24 2021 +0000
@@ -1150,6 +1150,48 @@
 
 subsection \<open>More lemmas about permutations\<close>
 
+lemma permutes_in_funpow_image: \<^marker>\<open>contributor \<open>Lars Noschinski\<close>\<close>
+  assumes "f permutes S" "x \<in> S"
+  shows "(f ^^ n) x \<in> S"
+  using assms by (induction n) (auto simp: permutes_in_image)
+
+lemma permutation_self: \<^marker>\<open>contributor \<open>Lars Noschinski\<close>\<close>
+  assumes \<open>permutation p\<close>
+  obtains n where \<open>n > 0\<close> \<open>(p ^^ n) x = x\<close>
+proof (cases \<open>p x = x\<close>)
+  case True
+  with that [of 1] show thesis by simp
+next
+  case False
+  from \<open>permutation p\<close> have \<open>inj p\<close>
+    by (intro permutation_bijective bij_is_inj)
+  moreover from \<open>p x \<noteq> x\<close> have \<open>(p ^^ Suc n) x \<noteq> (p ^^ n) x\<close> for n
+  proof (induction n arbitrary: x)
+    case 0 then show ?case by simp
+  next
+    case (Suc n)
+    have "p (p x) \<noteq> p x"
+    proof (rule notI)
+      assume "p (p x) = p x"
+      then show False using \<open>p x \<noteq> x\<close> \<open>inj p\<close> by (simp add: inj_eq)
+    qed
+    have "(p ^^ Suc (Suc n)) x = (p ^^ Suc n) (p x)"
+      by (simp add: funpow_swap1)
+    also have "\<dots> \<noteq> (p ^^ n) (p x)"
+      by (rule Suc) fact
+    also have "(p ^^ n) (p x) = (p ^^ Suc n) x"
+      by (simp add: funpow_swap1)
+    finally show ?case by simp
+  qed
+  then have "{y. \<exists>n. y = (p ^^ n) x} \<subseteq> {x. p x \<noteq> x}"
+    by auto
+  then have "finite {y. \<exists>n. y = (p ^^ n) x}"
+    using permutation_finite_support[OF assms] by (rule finite_subset)
+  ultimately obtain n where \<open>n > 0\<close> \<open>(p ^^ n) x = x\<close>
+    by (rule funpow_inj_finite)
+  with that [of n] show thesis by blast
+qed
+
 text \<open>The following few lemmas were contributed by Lukas Bulwahn.\<close>
 
 lemma count_image_mset_eq_card_vimage:
diff -r c973b5300025 -r 92783562ab78 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Sat Apr 10 20:22:07 2021 +0200
+++ b/src/HOL/Euclidean_Division.thy	Sun Apr 11 07:35:24 2021 +0000
@@ -1459,6 +1459,19 @@
   qed
 qed
 
+lemma funpow_mod_eq: \<^marker>\<open>contributor \<open>Lars Noschinski\<close>\<close>
+  \<open>(f ^^ (m mod n)) x = (f ^^ m) x\<close> if \<open>(f ^^ n) x = x\<close>
+proof -
+  have \<open>(f ^^ m) x = (f ^^ (m mod n + m div n * n)) x\<close>
+    by simp
+  also have \<open>\<dots> = (f ^^ (m mod n)) (((f ^^ n) ^^ (m div n)) x)\<close>
+    by (simp only: funpow_add funpow_mult ac_simps) simp
+  also have \<open>((f ^^ n) ^^ q) x = x\<close> for q
+    by (induction q) (use \<open>(f ^^ n) x = x\<close> in simp_all)
+  finally show ?thesis
+    by simp
+qed
+
 
 subsection \<open>Euclidean division on \<^typ>\<open>int\<close>\<close>
 
diff -r c973b5300025 -r 92783562ab78 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Apr 10 20:22:07 2021 +0200
+++ b/src/HOL/Finite_Set.thy	Sun Apr 11 07:35:24 2021 +0000
@@ -2312,6 +2312,7 @@
   for S :: "'a::linordered_ring set"
   by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom)
 
+
 subsection \<open>The finite powerset operator\<close>
 
 definition Fpow :: "'a set \<Rightarrow> 'a set set"
diff -r c973b5300025 -r 92783562ab78 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sat Apr 10 20:22:07 2021 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Sun Apr 11 07:35:24 2021 +0000
@@ -355,6 +355,52 @@
   then show ?thesis by auto
 qed
 
+lemma funpow_inj_finite: \<^marker>\<open>contributor \<open>Lars Noschinski\<close>\<close>
+  assumes \<open>inj p\<close> \<open>finite {y. \<exists>n. y = (p ^^ n) x}\<close>
+  obtains n where \<open>n > 0\<close> \<open>(p ^^ n) x = x\<close> 
+proof -
+  have \<open>infinite (UNIV :: nat set)\<close>
+    by simp
+  moreover have \<open>{y. \<exists>n. y = (p ^^ n) x} = (\<lambda>n. (p ^^ n) x) ` UNIV\<close>
+    by auto
+  with assms have \<open>finite \<dots>\<close>
+    by simp
+  ultimately have "\<exists>n \<in> UNIV. \<not> finite {m \<in> UNIV. (p ^^ m) x = (p ^^ n) x}"
+    by (rule pigeonhole_infinite)
+  then obtain n where "infinite {m. (p ^^ m) x = (p ^^ n) x}" by auto
+  then have "infinite ({m. (p ^^ m) x = (p ^^ n) x} - {n})" by auto
+  then have "({m. (p ^^ m) x = (p ^^ n) x} - {n}) \<noteq> {}"
+    by (auto simp add: subset_singleton_iff)
+  then obtain m where m: "(p ^^ m) x = (p ^^ n) x" "m \<noteq> n" by auto
+
+  { fix m n assume "(p ^^ n) x = (p ^^ m) x" "m < n"
+    have "(p ^^ (n - m)) x = inv (p ^^ m) ((p ^^ m) ((p ^^ (n - m)) x))"
+      using \<open>inj p\<close> by (simp add: inv_f_f)
+    also have "((p ^^ m) ((p ^^ (n - m)) x)) = (p ^^ n) x"
+      using \<open>m < n\<close> funpow_add [of m \<open>n - m\<close> p] by simp
+    also have "inv (p ^^ m) \<dots> = x"
+      using \<open>inj p\<close>  by (simp add: \<open>(p ^^ n) x = _\<close>)
+    finally have "(p ^^ (n - m)) x = x" "0 < n - m"
+      using \<open>m < n\<close> by auto }
+  note general = this
+
+  show thesis
+  proof (cases m n rule: linorder_cases)
+    case less
+    then have \<open>n - m > 0\<close> \<open>(p ^^ (n - m)) x = x\<close>
+      using general [of n m] m by simp_all
+    then show thesis by (blast intro: that)
+  next
+    case equal
+    then show thesis using m by simp
+  next
+    case greater
+    then have \<open>m - n > 0\<close> \<open>(p ^^ (m - n)) x = x\<close>
+      using general [of m n] m by simp_all
+    then show thesis by (blast intro: that)
+  qed
+qed
+
 
 lemma mono_inv:
   fixes f::"'a::linorder \<Rightarrow> 'b::linorder"
@@ -1226,6 +1272,4 @@
 qed
 end
 
-
-
 end
diff -r c973b5300025 -r 92783562ab78 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Apr 10 20:22:07 2021 +0200
+++ b/src/HOL/Nat.thy	Sun Apr 11 07:35:24 2021 +0000
@@ -1483,7 +1483,10 @@
 
 text \<open>For code generation.\<close>
 
-definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
+context
+begin
+
+qualified definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
   where funpow_code_def [code_abbrev]: "funpow = compow"
 
 lemma [code]:
@@ -1491,7 +1494,7 @@
   "funpow 0 f = id"
   by (simp_all add: funpow_code_def)
 
-hide_const (open) funpow
+end
 
 lemma funpow_add: "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
   by (induct m) simp_all
@@ -1570,6 +1573,15 @@
   shows "bij (f^^n)"
 by (rule bijI[OF inj_fn[OF bij_is_inj[OF assms]] surj_fn[OF bij_is_surj[OF assms]]])
 
+lemma bij_betw_funpow: \<^marker>\<open>contributor \<open>Lars Noschinski\<close>\<close>
+  assumes "bij_betw f S S" shows "bij_betw (f ^^ n) S S"
+proof (induct n)
+  case 0 then show ?case by (auto simp: id_def[symmetric])
+next
+  case (Suc n)
+  then show ?case unfolding funpow.simps using assms by (rule bij_betw_trans)
+qed
+
 
 subsection \<open>Kleene iteration\<close>
 
diff -r c973b5300025 -r 92783562ab78 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Sat Apr 10 20:22:07 2021 +0200
+++ b/src/HOL/Set_Interval.thy	Sun Apr 11 07:35:24 2021 +0000
@@ -1435,6 +1435,26 @@
   with 1 show ?thesis using card_inj_on_le[of ?f A B] assms(1) by simp
 qed
 
+lemma inj_on_funpow_least: \<^marker>\<open>contributor \<open>Lars Noschinski\<close>\<close>
+  \<open>inj_on (\<lambda>k. (f ^^ k) s) {0..<n}\<close>
+  if \<open>(f ^^ n) s = s\<close> \<open>\<And>m. 0 < m \<Longrightarrow> m < n \<Longrightarrow> (f ^^ m) s \<noteq> s\<close>
+proof -
+  { fix k l assume A: "k < n" "l < n" "k \<noteq> l" "(f ^^ k) s = (f ^^ l) s"
+    define k' l' where "k' = min k l" and "l' = max k l"
+    with A have A': "k' < l'" "(f ^^ k') s = (f ^^ l') s" "l' < n"
+      by (auto simp: min_def max_def)
+
+    have "s = (f ^^ ((n - l') + l')) s" using that \<open>l' < n\<close> by simp
+    also have "\<dots> = (f ^^ (n - l')) ((f ^^ l') s)" by (simp add: funpow_add)
+    also have "(f ^^ l') s = (f ^^ k') s" by (simp add: A')
+    also have "(f ^^ (n - l')) \<dots> = (f ^^ (n - l' + k')) s" by (simp add: funpow_add)
+    finally have "(f ^^ (n - l' + k')) s = s" by simp
+    moreover have "n - l' + k' < n" "0 < n - l' + k'"using A' by linarith+
+    ultimately have False using that(2) by auto
+  }
+  then show ?thesis by (intro inj_onI) auto
+qed
+
 
 subsection \<open>Intervals of integers\<close>