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)"
    using n by (simp add: funpow_add)
  also have "… = (f ^^ funpow_dist1 f x y) x"
    using ‹n < _› by (simp add: funpow_add)
      (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
   apply (simp add: assms(2) orbit_eqI(1))
  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))
  ultimately show False by contradiction
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