Theory HOL-Combinatorics.Orbits

(*  Author:     Lars Noschinski
*)

section ‹Permutation orbits›

theory Orbits
imports
  "HOL-Library.FuncSet"
  "HOL-Combinatorics.Permutations"
begin

subsection ‹Orbits and cyclic permutations›

inductive_set orbit :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a set" for f x where
  base: "f x ∈ orbit f x" |
  step: "y ∈ orbit f x ⟹ f y ∈ orbit f x"

definition cyclic_on :: "('a ⇒ 'a) ⇒ 'a set ⇒ bool" where
  "cyclic_on f S ⟷ (∃s∈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 ∈ ?L" then show "y ∈ ?R"
    by (induct rule: orbit.induct) (auto simp: exI[where x=1] exI[where x="Suc n" for n])
next
  fix y assume "y ∈ ?R"
  then obtain n where "y = (f ^^ n) x" "0 < n" by blast
  then show "y ∈ ?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 ∈ orbit f t" "t ∈ orbit f u" shows "s ∈ orbit f u"
  using assms by induct (auto intro: orbit.intros)

lemma orbit_subset:
  assumes "s ∈ orbit f (f t)" shows "s ∈ orbit f t"
  using assms by (induct) (auto intro: orbit.intros)

lemma orbit_sim_step:
  assumes "s ∈ orbit f t" shows "f s ∈ orbit f (f t)"
  using assms by induct (auto intro: orbit.intros)

lemma orbit_step:
  assumes "y ∈ orbit f x" "f x ≠ y" shows "y ∈ 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 ∈ orbit f s" "t ∈ orbit f s" shows "t ∈ orbit f t"
  using assms(2,1) by induct (auto intro: orbit_sim_step)

lemma orbit_swap:
  assumes "s ∈ orbit f s" "t ∈ orbit f s" shows "s ∈ 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 ∈ orbit f s"
  unfolding orbit_altdef using permutation_self[OF assms, of s] by simp metis

lemma orbit_altdef_self_in:
  assumes "s ∈ orbit f s" shows "orbit f s = {(f ^^ n) s | n. True}"
proof (intro set_eqI iffI)
  fix x assume "x ∈ {(f ^^ n) s | n. True}"
  then obtain n where "x = (f ^^ n) s" by auto
  then show "x ∈ 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 ∈ 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 "… = {(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 ∈ orbit f t" shows "(f ^^ n) s ∈ orbit f t"
  using assms by (induct n) (auto intro: orbit.intros)

lemma finite_orbit:
  assumes "s ∈ 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 ∈ orbit f s" shows "orbit f (f s) = orbit f s"
proof (intro set_eqI iffI)
  fix t assume "t ∈ orbit f s" then show "t ∈ 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 ≠ {}"
  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 ∈ orbit (inv g) x"
    have "y ∈ orbit g x"
    proof -
      have inv_g: "⋀y. x = g y ⟹ inv g x = y" "⋀y. inv g (g y) = y"
        by (metis A(1) bij_inv_eq_iff permutation_bijective)+

      { fix y assume "y ∈ orbit g x"
        then have "inv g y ∈ 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 ⟷ S ≠ {} ∧ (∀s∈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 ∈ S" shows "(f^^n) s ∈ 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 ∈ 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 ∈ S" shows "f s ∈ S"
  using assms by (auto simp: cyclic_on_def intro: orbit.intros)

lemma orbit_inverse:
  assumes self: "a ∈ orbit g a"
    and eq: "⋀x. x ∈ orbit g a ⟹ 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 ∈ ?L"
  then obtain x0 where "x0 ∈ orbit g a" "x = f x0" by auto
  then show "x ∈ ?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 ∈ ?R"
  then show "x ∈ ?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 "⋀x. x ∈ S ⟹ 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 ∈ A"
  shows "x ∈ A"
proof -
  from assms have fx_in_orb: "f x ∈ 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 "… = orbit f x" using ‹f x ∈ A› 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 ∈ A" "f ∈ A → A" "⋀y. y ∈ A ⟹ f y = g y" shows "orbit f x = orbit g x"
proof -
  { fix n have "(f ^^ n) x = (g ^^ n) x ∧ (f ^^ n) x ∈ 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 ∈ orbit f t" and eq: "⋀s. s ∈ orbit f t ⟹ 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 "⋀s. s ∈ S ⟹ f s = g s" shows "cyclic_on f S = cyclic_on g S"
proof -
  have "(∃s∈S. orbit f s = orbit g s) ⟹ 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 ∩ B = {}" "C ⊆ A"
  shows "cyclic_on (f o g) C"
proof -
  have *: "⋀c. c ∈ C ⟹ 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 ∩ B = {}" "C ⊆ B"
  shows "cyclic_on (f o g) C"
proof -
  obtain c where c: "c ∈ C" "C = orbit g c" "c ∈ orbit g c"
    using ‹cyclic_on g C› by (auto simp: cyclic_on_def)
  then have "⋀c. c ∈ C ⟹ 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 ∈ S" shows "orbit f x ⊆ S"
proof
  fix y assume "y ∈ orbit f x"
  then show "y ∈ 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 ∈ S" shows "orbit f y = S"
  using assms unfolding cyclic_on_alldef by simp

lemma orbit_eq_singleton_iff: "orbit f x = {x} ⟷ f x = x" (is "?L ⟷ ?R")
proof
  assume A: ?R
  { fix y assume "y ∈ 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 "⋀y. y ∈ orbit f x ⟹ 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 ∈ S"
  obtains "f x ∈ S" "f x = x ⟷ card S = 1"
proof
  from assms show "f x ∈ 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 ⟷ S = {x}" by (metis orbit_eq_singleton_iff)
  then show "f x = x ⟷ card S = 1" using ‹x ∈ S› by (auto simp: card_Suc_eq)
qed

lemma orbit_eqI:
  "y = f x ⟹ y ∈ orbit f x"
  "z = f y ⟹y ∈ orbit f x ⟹z ∈ orbit f x"
  by (metis orbit.base) (metis orbit.step)


subsection ‹Decomposition of arbitrary permutations›

definition perm_restrict :: "('a ⇒ 'a) ⇒ 'a set ⇒ ('a ⇒ 'a)" where
  "perm_restrict f S x ≡ if x ∈ S then f x else x"

lemma perm_restrict_comp:
  assumes "A ∩ B = {}" "cyclic_on f B"
  shows "perm_restrict f A o perm_restrict f B = perm_restrict f (A ∪ B)"
proof -
  have "⋀x. x ∈ B ⟹ f x ∈ B" using ‹cyclic_on f B› by (rule cyclic_on_inI)
  with assms show ?thesis by (auto simp: perm_restrict_def fun_eq_iff)
qed

lemma perm_restrict_simps:
  "x ∈ S ⟹ perm_restrict f S x = f x"
  "x ∉ S ⟹ 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 ∩ 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 ∩ B = {}"
  shows "perm_restrict f A o perm_restrict f B = perm_restrict f (A ∪ 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 ⟷ 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 "∃x. perm_restrict f (S - A) x = y"
    proof cases
      assume A: "y ∈ S - A"
      with ‹f permutes S› obtain x where "f x = y" "x ∈ S"
        unfolding permutes_def by auto metis
      moreover
      with A have "x ∉ 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 ∉ 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 "∃C. (∀c ∈ C. cyclic_on f c) ∧ ⋃C = S ∧ (∀c1 ∈ C. ∀c2 ∈ C. c1 ≠ c2 ⟶ c1 ∩ 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 ∈ S" by auto
    with ‹f permutes S› have "orbit f s ⊆ S"
      by (rule permutes_orbit_subset)
    have cyclic_orbit: "cyclic_on f (orbit f s)"
      using ‹f permutes S› ‹finite S› by (rule cyclic_on_orbit)

    let ?f' = "perm_restrict f (S - orbit f s)"

    have "f s ∈ S" using ‹f permutes S› ‹s ∈ S› by (auto simp: permutes_in_image)
    then have "S - orbit f s ⊂ S" using orbit.base[of f s] ‹s ∈ S› by blast
    moreover
    have "?f' permutes (S - orbit f s)"
      using ‹f permutes S› cyclic_orbit by (rule perm_restrict_diff_cyclic)
    ultimately
    obtain C where C: "⋀c. c ∈ C ⟹ cyclic_on ?f' c" "⋃C = S - orbit f s"
        "∀c1 ∈ C. ∀c2 ∈ C. c1 ≠ c2 ⟶ c1 ∩ c2 = {}"
      using psubset.IH by metis

    { fix c assume "c ∈ C"
      then have *: "⋀x. x ∈ c ⟹ perm_restrict f (S - orbit f s) x = f x"
        using C(2) ‹f permutes S› by (auto simp add: perm_restrict_def)
      then have "cyclic_on f c" using C(1)[OF ‹c ∈ C›] by (simp cong: cyclic_cong add: *)
    } note in_C_cyclic = this

    have Un_ins: "⋃(insert (orbit f s) C) = S"
      using ‹⋃C = _›  ‹orbit f s ⊆ S› by blast

    have Disj_ins: "(∀c1 ∈ insert (orbit f s) C. ∀c2 ∈ insert (orbit f s) C. c1 ≠ c2 ⟶ c1 ∩ 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 ‹Function-power distance between values›

definition funpow_dist :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a ⇒ nat" where
  "funpow_dist f x y ≡ LEAST n. (f ^^ n) x = y"

abbreviation funpow_dist1 :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a ⇒ nat" where
  "funpow_dist1 f x y ≡ 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 ≠ y"
proof (rule notI)
  assume "(f ^^ n) x = y"
  then have "funpow_dist f x y ≤ 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 ≠ y"
proof (rule notI)
  assume "(f ^^ n) x = y"
  then have "(f ^^ (n - 1)) (f x) = y"
    using ‹0 < n› by (cases n) (simp_all add: funpow_swap1)
  then have "funpow_dist f (f x) y ≤ n - 1" unfolding funpow_dist_def by (rule Least_le)
  with assms show False by simp
qed

lemma funpow_dist_prop:
  "y ∈ orbit f x ⟹ (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 ∈ orbit f x" shows "funpow_dist f x y = 0 ⟷ x = y"
  using assms by (auto simp: funpow_dist_0 dest: funpow_dist_prop)

lemma funpow_dist_step:
  assumes "x ≠ y" "y ∈ orbit f x" shows "funpow_dist f x y = Suc (funpow_dist f (f x) y)"
proof -
  from ‹y ∈ _› obtain n where "(f ^^ n) x = y" by (auto simp: orbit_altdef)
  with ‹x ≠ y› 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 ≠ y" using ‹x ≠ y› by simp
    show "∀k. ((f ^^ Suc k) x = y) = ((f ^^ k) (f x) = y)"
      by (simp add: funpow_swap1)
  qed
qed

lemma funpow_dist1_prop:
  assumes "y ∈ 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 ∈ orbit f x" "m ≤ funpow_dist f x y" "n ≤ funpow_dist f x y" "m ≠ n"
  shows "(f ^^ m) x ≠ (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_dist f x y"
    by (auto simp: min_def max_def)

  have "y = (f ^^ funpow_dist f x y) x"
    using ‹y ∈ _› by (simp only: funpow_dist_prop)
  also have "… = (f ^^ ((funpow_dist f x y - n') + n')) x"
    using ‹n' ≤ _› by simp
  also have "… = (f ^^ ((funpow_dist f x y - n') + m')) x"
    by (simp add: funpow_add ‹(f ^^ m') x = _›)
  also have "(f ^^ ((funpow_dist f x y - n') + m')) x ≠ 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 ∈ orbit f x" "m < funpow_dist1 f x y" "n < funpow_dist1 f x y" "m ≠ n"
  shows "(f ^^ m) x ≠ (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 ‹y ∈ _› by (simp only: funpow_dist1_prop)
  also have "… = (f ^^ ((funpow_dist1 f x y - n') + n')) x"
    using ‹n' < _› by simp
  also have "… = (f ^^ ((funpow_dist1 f x y - n') + m')) x"
    by (simp add: funpow_add ‹(f ^^ m') x = _›)
  also have "(f ^^ ((funpow_dist1 f x y - n') + m')) x ≠ y"
    using A' by (intro funpow_dist1_least) linarith+
  finally show "False" by simp
qed

lemma inj_on_funpow_dist:
  assumes "y ∈ orbit f x" shows "inj_on (λ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 ∈ orbit f x" shows "inj_on (λ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 ∈ orbit f x"
  shows "orbit f x = (λ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 ∈ 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} ⊆ 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 ‹n = funpow_dist1 f x z - funpow_dist1 f x y - 1›
  with assms have *: ‹funpow_dist1 f x z = Suc (funpow_dist1 f x y + n)›
    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 "… = 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 ≤ funpow_dist1 f y z + funpow_dist1 f x y"
      using funpow_dist1_least not_less by fastforce
    then show "?L ≤ ?R" by presburger
  next
    have "funpow_dist1 f y z ≤ 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 ≤ ?L" by linarith
  qed
qed

lemma funpow_dist1_le_self:
  assumes "(f ^^ m) x = x" "0 < m" "y ∈ orbit f x"
  shows "funpow_dist1 f x y ≤ 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 ‹y ∈ orbit f x› have "funpow_dist1 f x y ≤ funpow_dist1 f x y mod m"
    by auto (metis ‹(f ^^ funpow_dist1 f x y) x = (f ^^ (funpow_dist1 f x y mod m)) x› funpow_dist1_prop funpow_dist_least funpow_dist_step leI)
  with ‹m > 0› show ?thesis
    by (auto intro: order_trans)
qed

end