Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Combinatorics/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 23 kB

Quelle Orbits.thy Sprache: Isabelle

(*  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 \ '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 \<open>cyclic_on g C\<close> 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 \<open>Decomposition of arbitrary permutations\<close>

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 \<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 \ 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 \<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 \ 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 \<open>f permutes S\<close> 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) \<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: "\(insert (orbit f s) C) = S"
      using \<open>\<Union>C = _\<close>  \<open>orbit f s \<subseteq> S\<close> 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 \<open>Function-power distance between values\<close>

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 \<open>0 < n\<close> 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 \<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 \ 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' \<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 "\ = (f ^^ ((funpow_dist f x y - n') + n')) x"
    using \<open>n' \<le> _\<close> by simp
  also have "\ = (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 \ 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 \<open>y \<in> _\<close> by (simp only: funpow_dist1_prop)
  also have "\ = (f ^^ ((funpow_dist1 f x y - n') + n')) x"
    using \<open>n' < _\<close> by simp
  also have "\ = (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 \ 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..
  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..
  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 \<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 "\ = 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 \<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

quality100%

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.