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