# Theory Auxiliary

```theory Auxiliary
imports
"HOL-Library.FuncSet"
"HOL-Combinatorics.Orbits"
begin

lemma funpow_invs:
assumes "m ≤ n" and inv: "⋀x. f (g x) = x"
shows "(f ^^ m) ((g ^^ n) x) = (g ^^ (n - m)) x"
using ‹m ≤ n›
proof (induction m)
case (Suc m)
moreover then have "n - m = Suc (n - Suc m)" by auto
ultimately show ?case by (auto simp: inv)
qed simp

section ‹Permutation Domains›

definition has_dom :: "('a ⇒ 'a) ⇒ 'a set ⇒ bool" where
"has_dom f S ≡ ∀s. s ∉ S ⟶ f s = s"

lemma has_domD: "has_dom f S ⟹ x ∉ S ⟹ f x = x"
by (auto simp: has_dom_def)

lemma has_domI: "(⋀x. x ∉ S ⟹ f x = x) ⟹ has_dom f S"
by (auto simp: has_dom_def)

lemma permutes_conv_has_dom:
"f permutes S ⟷ bij f ∧ has_dom f S"
by (auto simp: permutes_def has_dom_def bij_iff)

section ‹Segments›

inductive_set segment :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a ⇒ 'a set" for f a b where
base: "f a ≠ b ⟹ f a ∈ segment f a b" |
step: "x ∈ segment f a b ⟹ f x ≠ b ⟹ f x ∈ segment f a b"

lemma segment_step_2D:
assumes "x ∈ segment f a (f b)" shows "x ∈ segment f a b ∨ x = b"
using assms by induct (auto intro: segment.intros)

lemma not_in_segment2D:
assumes "x ∈ segment f a b" shows "x ≠ b"
using assms by induct auto

lemma segment_altdef:
assumes "b ∈ orbit f a"
shows "segment f a b = (λn. (f ^^ n) a) ` {1..<funpow_dist1 f a b}" (is "?L = ?R")
proof (intro set_eqI iffI)
fix x assume "x ∈ ?L"
have "f a ≠b ⟹ b ∈ orbit f (f a)"
using assms  by (simp add: orbit_step)
then have *: "f a ≠ b ⟹ 0 < funpow_dist f (f a) b"
using assms using gr0I funpow_dist_0_eq[OF ‹_ ⟹ b ∈ orbit f (f a)›] by (simp add: orbit.intros)
from ‹x ∈ ?L› show "x ∈ ?R"
proof induct
case base then show ?case by (intro image_eqI[where x=1]) (auto simp: *)
next
case step then show ?case using assms funpow_dist1_prop less_antisym
by (fastforce intro!: image_eqI[where x="Suc n" for n])
qed
next
fix x assume "x ∈ ?R"
then obtain n where "(f ^^ n ) a = x" "0 < n" "n < funpow_dist1 f a b" by auto
then show "x ∈ ?L"
proof (induct n arbitrary: x)
case 0 then show ?case by simp
next
case (Suc n)
have "(f ^^ Suc n) a ≠ b" using Suc by (meson funpow_dist1_least)
with Suc show ?case by (cases "n = 0") (auto intro: segment.intros)
qed
qed

(*XXX move up*)
lemma segmentD_orbit:
assumes "x ∈ segment f y z" shows "x ∈ orbit f y"
using assms by induct (auto intro: orbit.intros)

lemma segment1_empty: "segment f x (f x) = {}"
by (auto simp: segment_altdef orbit.base funpow_dist_0)

lemma segment_subset:
assumes "y ∈ segment f x z"
assumes "w ∈ segment f x y"
shows "w ∈ segment f x z"
using assms by (induct arbitrary: w) (auto simp: segment1_empty intro: segment.intros dest: segment_step_2D elim: segment.cases)

(* XXX move up*)
lemma not_in_segment1:
assumes "y ∈ orbit f x" shows "x ∉ segment f x y"
proof
assume "x ∈ segment f x y"
then obtain n where n: "0 < n" "n < funpow_dist1 f x y" "(f ^^ n) x = x"
using assms by (auto simp: segment_altdef Suc_le_eq)
then have neq_y: "(f ^^ (funpow_dist1 f x y - n)) x ≠ y" by (simp add: funpow_dist1_least)

have "(f ^^ (funpow_dist1 f x y - n)) x = (f ^^ (funpow_dist1 f x y - n)) ((f ^^ n) x)"
also have "… = (f ^^ funpow_dist1 f x y) x"
(metis assms funpow_0 funpow_neq_less_funpow_dist1 n(1) n(3) nat_neq_iff zero_less_Suc)
also have "… = y" using assms by (rule funpow_dist1_prop)
finally show False using neq_y by contradiction
qed

lemma not_in_segment2: "y ∉ segment f x y"
using not_in_segment2D by metis

(*XXX move*)
lemma in_segmentE:
assumes "y ∈ segment f x z" "z ∈ orbit f x"
obtains "(f ^^ funpow_dist1 f x y) x = y" "funpow_dist1 f x y < funpow_dist1 f x z"
proof
from assms show "(f ^^ funpow_dist1 f x y) x = y"
by (intro segmentD_orbit funpow_dist1_prop)
moreover
obtain n where "(f ^^ n) x = y" "0 < n" "n < funpow_dist1 f x z"
using assms by (auto simp: segment_altdef)
moreover then have "funpow_dist1 f x y ≤ n" by (meson funpow_dist1_least not_less)
ultimately show "funpow_dist1 f x y < funpow_dist1 f x z" by linarith
qed

(*XXX move*)
lemma cyclic_split_segment:
assumes S: "cyclic_on f S" "a ∈ S" "b ∈ S" and "a ≠ b"
shows "S = {a,b} ∪ segment f a b ∪ segment f b a" (is "?L = ?R")
proof (intro set_eqI iffI)
fix c assume "c ∈ ?L"
with S have "c ∈ orbit f a" unfolding cyclic_on_alldef by auto
then show "c ∈ ?R" by induct (auto intro: segment.intros)
next
fix c assume "c ∈ ?R"
moreover have "segment f a b ⊆ orbit f a" "segment f b a ⊆ orbit f b"
by (auto dest: segmentD_orbit)
ultimately show "c ∈ ?L" using S by (auto simp: cyclic_on_alldef)
qed

(*XXX move*)
lemma segment_split:
assumes y_in_seg: "y ∈ segment f x z"
shows "segment f x z = segment f x y ∪ {y} ∪ segment f y z" (is "?L = ?R")
proof (intro set_eqI iffI)
fix w assume "w ∈ ?L" then show "w ∈ ?R" by induct (auto intro: segment.intros)
next
fix w assume "w ∈ ?R"
moreover
{ assume "w ∈ segment f x y" then have "w ∈ segment f x z"
using segment_subset[OF y_in_seg] by auto }
moreover
{ assume "w ∈ segment f y z" then have "w ∈ segment f x z"
using y_in_seg by induct (auto intro: segment.intros) }
ultimately
show "w ∈ ?L" using y_in_seg by (auto intro: segment.intros)
qed

lemma in_segmentD_inv:
assumes "x ∈ segment f a b" "x ≠ f a"
assumes "inj f"
shows "inv f x ∈ segment f a b"
using assms by (auto elim: segment.cases)

lemma in_orbit_invI:
assumes "b ∈ orbit f a"
assumes "inj f"
shows "a ∈ orbit (inv f) b"
using assms(1)
apply induct
by (metis assms(2) inv_f_f orbit.base orbit_trans)

lemma segment_step_2:
assumes A: "x ∈ segment f a b" "b ≠ a" and "inj f"
shows "x ∈ segment f a (f b)"
using A by induct (auto intro: segment.intros dest: not_in_segment2D injD[OF ‹inj f›])

lemma inv_end_in_segment:
assumes "b ∈ orbit f a" "f a ≠ b" "bij f"
shows "inv f b ∈ segment f a b"
using assms(1,2)
proof induct
case base then show ?case by simp
next
case (step x)
moreover
from ‹bij f› have "inj f" by (rule bij_is_inj)
moreover
then have "x ≠ f x ⟹ f a = x ⟹ x ∈ segment f a (f x)" by (meson segment.simps)
moreover
have "x ≠ f x"
using step ‹inj f› by (metis in_orbit_invI inv_f_eq not_in_segment1 segment.base)
then have "inv f x ∈ segment f a (f x) ⟹ x ∈ segment f a (f x)"
using ‹bij f› ‹inj f› by (auto dest: segment.step simp: surj_f_inv_f bij_is_surj)
then have "inv f x ∈ segment f a x ⟹ x ∈ segment f a (f x)"
using ‹f a ≠ f x› ‹inj f› by (auto dest: segment_step_2 injD)
ultimately show ?case by (cases "f a = x") simp_all
qed

lemma segment_overlapping:
assumes "x ∈ orbit f a" "x ∈ orbit f b" "bij f"
shows "segment f a x ⊆ segment f b x ∨ segment f b x ⊆ segment f a x"
using assms(1,2)
proof induction
case base then show ?case by (simp add: segment1_empty)
next
case (step x)
from ‹bij f› have "inj f" by (simp add: bij_is_inj)
have *: "⋀f x y. y ∈ segment f x (f x) ⟹ False" by (simp add: segment1_empty)
{ fix y z
assume A: "y ∈ segment f b (f x)" "y ∉ segment f a (f x)" "z ∈ segment f a (f x)"
from ‹x ∈ orbit f a› ‹f x ∈ orbit f b› ‹y ∈ segment f b (f x)›
have "x ∈ orbit f b"
by (metis * inv_end_in_segment[OF _ _ ‹bij f›] inv_f_eq[OF ‹inj f›] segmentD_orbit)
moreover
with ‹x ∈ orbit f a› step.IH
have "segment f a (f x) ⊆ segment f b (f x) ∨ segment f b (f x) ⊆ segment f a (f x)"
apply auto
apply (metis * inv_end_in_segment[OF _ _ ‹bij f›] inv_f_eq[OF ‹inj f›] segment_step_2D segment_subset step.prems subsetCE)
by (metis (no_types, lifting) ‹inj f› * inv_end_in_segment[OF _ _ ‹bij f›] inv_f_eq orbit_eqI(2) segment_step_2D segment_subset subsetCE)
ultimately
have "segment f a (f x) ⊆ segment f b (f x)" using A by auto
} note C = this
then show ?case by auto
qed

lemma segment_disj:
assumes "a ≠ b" "bij f"
shows "segment f a b ∩ segment f b a = {}"
proof (rule ccontr)
assume "¬?thesis"
then obtain x where x: "x ∈ segment f a b" "x ∈ segment f b a" by blast
then have "segment f a b = segment f a x ∪ {x} ∪ segment f x b"
"segment f b a = segment f b x ∪ {x} ∪ segment f x a"
by (auto dest: segment_split)
then have o: "x ∈ orbit f a" "x ∈ orbit f b" by (auto dest: segmentD_orbit)

note * = segment_overlapping[OF o ‹bij f›]
have "inj f" using ‹bij f› by (simp add: bij_is_inj)

have "segment f a x = segment f b x"
proof (intro set_eqI iffI)
fix y assume A: "y ∈ segment f b x"
then have "y ∈ segment f a x ∨ f a ∈ segment f b a"
using * x(2) by (auto intro: segment.base segment_subset)
then show "y ∈ segment f a x"
using ‹inj f› A by (metis (no_types) not_in_segment2 segment_step_2)
next
fix y assume A: "y ∈ segment f a x "
then have "y ∈ segment f b x ∨ f b ∈ segment f a b"
using * x(1) by (auto intro: segment.base segment_subset)
then show "y ∈ segment f b x"
using ‹inj f› A by (metis (no_types) not_in_segment2 segment_step_2)
qed
moreover
have "segment f a x ≠ segment f b x"
by (metis assms bij_is_inj not_in_segment2 segment.base segment_step_2 segment_subset x(1))
qed

lemma segment_x_x_eq:
assumes "permutation f"
shows "segment f x x = orbit f x - {x}" (is "?L = ?R")
proof (intro set_eqI iffI)
fix y assume "y ∈ ?L" then show "y ∈ ?R" by (auto dest: segmentD_orbit simp: not_in_segment2)
next
fix y assume "y ∈ ?R"
then have "y ∈ orbit f x" "y ≠ x" by auto
then show "y ∈ ?L" by induct (auto intro: segment.intros)
qed

section ‹Lists of Powers›

definition iterate :: "nat ⇒ nat ⇒ ('a ⇒ 'a ) ⇒ 'a ⇒ 'a list" where
"iterate m n f x = map (λn. (f^^n) x) [m..<n]"

lemma set_iterate:
"set (iterate m n f x) = (λk. (f ^^ k) x) ` {m..<n} "
by (auto simp: iterate_def)

lemma iterate_empty[simp]: "iterate n m f x = [] ⟷ m ≤ n"
by (auto simp: iterate_def)

lemma iterate_length[simp]:
"length (iterate m n f x) = n - m"
by (auto simp: iterate_def)

lemma iterate_nth[simp]:
assumes "k < n - m" shows "iterate m n f x ! k = (f^^(m+k)) x"
using assms
by (induct k arbitrary: m) (auto simp: iterate_def)

lemma iterate_applied:
"iterate n m f (f x) = iterate (Suc n) (Suc m) f x"
by (induct m arbitrary: n) (auto simp: iterate_def funpow_swap1)

end
```