Theory Binary_Imprimitive_Decision

(*  Title:      Binary_Imprimitive_Decision
    File:       Binary_Code_Imprimitive.Binary_Imprimitive_Decision
    Author:     Martin Raška, Charles University

Part of Combinatorics on Words Formalized. See https://gitlab.com/formalcow/combinatorics-on-words-formalized/
*)

theory Binary_Imprimitive_Decision
  imports
    "Binary_Code_Imprimitive.Binary_Code_Imprimitive"

begin

section ‹Upper bound of the power exponent in the canonical imprimitivity witness›

lemma LS_power_len_ge:
  assumes "y ⇧@ k ⋅ x = z ⇧@ l"
    and "k * ❙|y❙| ≥ ❙|z❙| + ❙|y❙| - 1"
  shows "x ⋅ y = y ⋅ x"
proof (rule nemp_comm)
  assume "y ≠ ε"
  have "y ⇧@ k ≤p z ⋅ y ⇧@ k"
    using ‹y ⇧@ k ⋅ x = z ⇧@ l›
    by (blast intro!: pref_prod_root)
  moreover have "y ⇧@ k ≤p y ⋅ y ⇧@ k"
    by (blast intro!: pref_pow_ext')
  moreover have "1 ≤ gcd ❙|z❙| ❙|y❙|"
    using ‹y ≠ ε›
    by (simp flip: less_eq_Suc_le)
  from this ‹k * ❙|y❙| ≥ ❙|z❙| + ❙|y❙| - 1›
  have "❙|z❙| + ❙|y❙| - (gcd ❙|z❙| ❙|y❙|) ≤ k * ❙|y❙|"
    by (rule le_trans[OF diff_le_mono2])
  ultimately have "z ⋅ y = y ⋅ z"
    unfolding pow_len[symmetric] by (fact per_lemma_comm)
  with ‹y ⇧@ k ⋅ x = z ⇧@ l›
  show "x ⋅ y = y ⋅ x"
    by (fact LS_comm)
qed

lemma LS_root_len_ge:
  assumes "y ⇧@ k ⋅ x = z ⇧@ l"
    and "1 ≤ k" and "2 ≤ l"
    and "x ⋅ y ≠ y ⋅ x"
  shows "(k - 1) * ❙|y❙| + 2 ≤ ❙|z❙|"
proof (intro leI notI)
  assume "❙|z❙| < (k - 1) * ❙|y❙| + 2"
  then have "❙|z❙| + ❙|y❙| ≤ Suc (k - 1) * ❙|y❙| + 1"
    by simp
  also have "… = k * ❙|y❙| + 1"
    using ‹1 ≤ k› by simp
  finally have "k * ❙|y❙| ≥ ❙|z❙| + ❙|y❙| - 1"
    unfolding le_diff_conv.
  from ‹x ⋅ y ≠ y ⋅ x› LS_power_len_ge[OF ‹y ⇧@ k ⋅ x = z ⇧@ l› this]
  show False..
qed

lemma LS_root_len_le:
  assumes "y ⇧@ k ⋅ x = z ⇧@ l"
    and "1 ≤ k" and "2 ≤ l"
    and "x ⋅ y ≠ y ⋅ x"
  shows "❙|z❙| ≤ ❙|x❙| + ❙|y❙| - 2"
proof -
  have "❙|x❙| + k * ❙|y❙| = l * ❙|z❙|"
    using lenarg[OF ‹y ⇧@ k ⋅ x = z ⇧@ l›]
    by (simp only: pow_len lenmorph add.commute[of "❙|x❙|"])
  have "❙|z❙| ≤ (l - 1) * ❙|z❙|"
    using diff_le_mono[OF ‹2 ≤ l›, of 1] by simp
  also have "… = ❙|x❙| + k * ❙|y❙| - ❙|z❙|"
    unfolding diff_mult_distrib ‹❙|x❙| + k * ❙|y❙| = l * ❙|z❙|›[symmetric] by simp
  also have "… ≤ ❙|x❙| + k * ❙|y❙| - ((k - 1) * ❙|y❙| + 2)"
    using LS_root_len_ge[OF assms]
    by (rule diff_le_mono2)
  also have "… ≤ ❙|x❙| + ❙|y❙| - 2"
    using ‹1 ≤ k› unfolding diff_diff_eq[symmetric]
    by (intro diff_le_mono) (simp add: le_diff_conv add.assoc diff_mult_distrib)
  finally show "❙|z❙| ≤ ❙|x❙| + ❙|y❙| - 2".
qed

lemma LS_exp_le':
  assumes "y ⇧@ k ⋅ x = z ⇧@ l"
    and "2 ≤ l"
    and "x ⋅ y ≠ y ⋅ x"
  shows "k ≤ (❙|x❙| - 4) div ❙|y❙| + 2"
proof (cases "1 ≤ k")
  assume "1 ≤ k"
  have "❙|y❙| > 0"
    using ‹x ⋅ y ≠ y ⋅ x› by blast
  have "(k - 1) * ❙|y❙| + 2 ≤ ❙|z❙|"
    using LS_root_len_ge ‹y ⇧@ k ⋅ x = z ⇧@ l› ‹1 ≤ k› ‹2 ≤ l› ‹x ⋅ y ≠ y ⋅ x›.
  also have "❙|z❙| ≤ ❙|x❙| + ❙|y❙| - 2"
    using LS_root_len_le ‹y ⇧@ k ⋅ x = z ⇧@ l› ‹1 ≤ k› ‹2 ≤ l› ‹x ⋅ y ≠ y ⋅ x›.
  finally have "(k - 1) * ❙|y❙| + 2 ≤ ❙|x❙| + ❙|y❙| - 2".
  then have "(k - 1) * ❙|y❙| + 2 - ❙|y❙| - 2 ≤ ❙|x❙| + ❙|y❙| - 2 - ❙|y❙| - 2"
    by (intro diff_le_mono)
  then have "(k - 1) * ❙|y❙| + 2 - 2 - ❙|y❙| ≤ ❙|x❙| - (2 + 2)"
    unfolding diff_commute[of _ 2 "❙|y❙|"] unfolding diff_add_inverse2 diff_diff_eq.
  then have "(k - (1 + 1)) * ❙|y❙| ≤ ❙|x❙| - 4"
    unfolding diff_add_inverse2 nat_distrib diff_diff_eq mult_1
    by presburger
  then show "k ≤ (❙|x❙| - 4) div ❙|y❙| + 2"
    using ‹❙|y❙| > 0›
    by (simp only: less_eq_div_iff_mult_less_eq one_add_one flip: le_diff_conv)
qed (simp add: trans_le_add2)

lemma LS_exp_le:
  assumes "x ⋅ y ⇧@ k = z ⇧@ l"
    and "2 ≤ l"
    and "x ⋅ y ≠ y ⋅ x"
  shows "k ≤ (❙|x❙| - 4) div ❙|y❙| + 2"
  using LS_exp_le'[reversed, OF ‹x ⋅ y ⇧@ k = z ⇧@ l› ‹2 ≤ l› ‹x ⋅ y ≠ y ⋅ x›[symmetric]].

thm bin_imprim_expsE
lemma bin_imprim_code_witnessE:
  assumes "x ⋅ y ≠ y ⋅ x" and "❙|y❙| ≤ ❙|x❙|"
    and "ws ∈ lists {x,y}" and "2 ≤ ❙|ws❙|"
    and "primitive ws" and  "¬ primitive (concat ws)"
  obtains   "ws ∼ [x, x, y]"
  | k where "1 ≤ k" and "k ≤ (❙|x❙| - 4) div ❙|y❙| + 2"
    and "ws ∼ [x] ⋅ [y] ⇧@ k"
proof -
  obtain j k
    where "1 ≤ j" and "1 ≤ k" and "j = 1 ∨ k = 1"
      and witness_iff: "⋀ws. ws ∈ lists {x,y} ⟹  2 ≤ ❙|ws❙| ⟹
          (primitive ws ∧ ¬ primitive (concat ws) ⟷ ws ∼ [x] ⇧@ j ⋅ [y] ⇧@ k)"
      and
      j_ge: "❙|y❙| ≤ ❙|x❙| ⟹ 2 ≤ j ⟹ j = 2 ∧ primitive x ∧ primitive y" and
      k_ge: "❙|y❙| ≤ ❙|x❙| ⟹ 2 ≤ k ⟹ j = 1 ∧ primitive x"
    by (fact bin_imprim_code[OF assms(1, 3 - 6)])
  have "ws ∼ [x] ⇧@ j ⋅ [y] ⇧@ k"
    using witness_iff[OF ‹ws ∈ lists {x, y}› ‹2 ≤ ❙|ws❙|›] ‹primitive ws› ‹¬ primitive (concat ws)›
    by simp
  show thesis
  proof (cases)
    assume "2 ≤ j"
    from j_ge[OF ‹❙|y❙| ≤ ❙|x❙|› this] ‹j = 1 ∨ k = 1›
    have "j = 2" and "k = 1"
      by simp_all
    then have "ws ∼ [x, x, y]"
      using ‹ws ∼ [x] ⇧@ j ⋅ [y] ⇧@ k› by simp
    then show thesis..
  next
    assume "¬ 2 ≤ j"
    with ‹1 ≤ j› have "j = 1"
      by simp
    then have "ws ∼ [x] ⋅ [y] ⇧@ k"
      using ‹ws ∼ [x] ⇧@ j ⋅ [y] ⇧@ k› by simp
    then have "¬ primitive (x ⋅ y ⇧@ k)"
      using ‹¬ primitive (concat ws)› unfolding conjug_concat_prim_iff[OF ‹ws ∼ [x] ⋅ [y] ⇧@ k›]
      by simp
    moreover have "x ⋅ y ⇧@ k ≠ ε"
      using ‹x ⋅ y ≠ y ⋅ x› by (intro notI) simp
    ultimately obtain z l
      where "2 ≤ l" and "z ⇧@ l = x ⋅ y ⇧@ k"
      by (elim not_prim_expE)
    have "k ≤ (❙|x❙| - 4) div ❙|y❙| + 2"
      using LS_exp_le[OF ‹z ⇧@ l = x ⋅ y ⇧@ k›[symmetric] ‹2 ≤ l› ‹x ⋅ y ≠ y ⋅ x›].
    from ‹1 ≤ k› this ‹ws ∼ [x] ⋅ [y] ⇧@ k›
    show thesis..
  qed
qed

subsection ‹Optimality of the exponent upper bound›

lemma examples_bound_optimality:
  fixes m k and x y z :: "binA list"
  assumes "1 ≤ m" and "k' = 0 ⟹ m = 1"
  defines "x ≡ 𝔞 ⋅ 𝔟 ⋅ (𝔟 ⋅ (𝔞 ⋅ 𝔟) ⇧@ m) ⇧@ k' ⋅ 𝔟 ⋅ 𝔞"
    and "y ≡ 𝔟 ⋅ (𝔞 ⋅ 𝔟) ⇧@ m"
    and "z ≡ 𝔞 ⋅ 𝔟 ⋅ (𝔟 ⋅ (𝔞 ⋅ 𝔟) ⇧@ m) ⇧@ (k' + 1)"
    and "k ≡ k' + 2"
  shows "❙|y❙| ≤ ❙|x❙|" and "x ⋅ y ⇧@ k = z ⋅ z" and "k = (❙|x❙| - 4) div ❙|y❙| + 2"
proof -
  obtain m' where m: "m = m' + 1"
    using ‹1 ≤ m› using add.commute le_Suc_ex by blast
  have x_len: "❙|x❙| = k' * (2 * m + 1) + 4"
    unfolding x_def by (simp add: pow_len)
  have y_len: "❙|y❙| = 2 * m + 1"
    unfolding y_def by (simp add: pow_len)
  have z_len: "❙|z❙| = (k' + 1) * (2 * m + 1) + 2"
    unfolding z_def by (simp add: pow_len)
  show "❙|y❙| ≤ ❙|x❙|"
    using ‹k' = 0 ⟹ m = 1› unfolding x_len y_len
    by (cases k') (simp_all add: pow_len)
  show "x ⋅ y ⇧@ k = z ⋅ z"
    unfolding x_def y_def z_def k_def
    by comparison
  show "k = (❙|x❙| - 4) div ❙|y❙| + 2"
  proof -
    have "❙|x❙| - 4 = k' * ❙|y❙|"
      unfolding x_len y_len by simp
    have "❙|y❙| ≠ 0"
      unfolding y_def by blast
    have "k' = (❙|x❙| - 4) div ❙|y❙|"
      unfolding ‹❙|x❙| - 4 = k' * ❙|y❙|› nonzero_mult_div_cancel_right[OF ‹❙|y❙| ≠ 0›]..
    then show "k = (❙|x❙| - 4) div ❙|y❙| + 2"
      unfolding k_def by blast
  qed
qed

section ‹Characterization of binary primitivity preserving morphisms given by a pair of words›

lemma len_le_not_bin_primE:
  assumes "❙|y❙| ≤ ❙|x❙|"
    and "¬ bin_prim x y"
  obtains  "¬ primitive (x ⋅ x ⋅ y)"
  | k where "1 ≤ k" and "k ≤ (❙|x❙| - 4) div ❙|y❙| + 2"
    and "¬ primitive (x ⋅ y ⇧@ k)"
proof (cases)
  assume "x ⋅ y = y ⋅ x"
  have "¬ primitive (x ⋅ x ⋅ y)"
    using ‹x ⋅ y = y ⋅ x› ‹❙|y❙| ≤ ❙|x❙|›
    by (cases "x ≠ ε") (intro comm_not_prim, simp_all)
  then show thesis..
next
  assume "x ⋅ y ≠ y ⋅ x"
  then have "x ≠ y"
    by blast
  obtain ws where
      "ws ∈ lists {x, y}" and "2 ≤ ❙|ws❙|" and "primitive ws" and "¬ primitive (concat ws)"
    using ‹¬ bin_prim x y› unfolding bin_prim_concat_prim_pres_conv[OF ‹x ≠ y›]
    by blast
  then consider "ws ∼ [x, x, y]"
    | k where "1 ≤ k" and "k ≤ (❙|x❙| - 4) div ❙|y❙| + 2"
      and   "ws ∼ [x] ⋅ [y] ⇧@ k"
    by (rule bin_imprim_code_witnessE[OF ‹x ⋅ y ≠ y ⋅ x› ‹❙|y❙| ≤ ❙|x❙|›])
  then show thesis
  proof (cases)
    assume "ws ∼ [x, x, y]"
    then have "¬ primitive (x ⋅ x ⋅ y)"
      using ‹¬ primitive (concat ws)›
      by (simp add: conjug_concat_prim_iff)
    then show thesis..
  next
    fix k
    assume "1 ≤ k" and "k ≤ (❙|x❙| - 4) div ❙|y❙| + 2" and "ws ∼ [x] ⋅ [y] ⇧@ k"
    have "¬ primitive (x ⋅ y ⇧@ k)"
      using ‹ws ∼ [x] ⋅ [y] ⇧@ k› ‹¬ primitive (concat ws)›
      by (simp add: conjug_concat_prim_iff)
    from ‹1 ≤ k› ‹k ≤ (❙|x❙| - 4) div ❙|y❙| + 2› this
    show thesis..
  qed
qed

lemma bin_prim_xyk:
  assumes "bin_prim x y" and "0 < k"
  shows "primitive (x ⋅ y ⇧@ k)"
proof -
  have "primitive ([x] ⋅ [y] ⇧@ k)"
    using bin_prim_code[OF ‹bin_prim x y›]
    by (intro prim_abk) blast
  from bin_prim_concat_prim_pres[OF ‹bin_prim x y› _ _ this] ‹0 < k›
  show "primitive (x ⋅ y ⇧@ k)"
    by (simp add: pow_in_lists)
qed

lemma len_le_bin_prim_iff:
  assumes "❙|y❙| ≤ ❙|x❙|"
  shows
    "bin_prim x y ⟷ primitive (x ⋅ x ⋅ y) ∧ (∀k. 1 ≤ k ∧ k ≤ (❙|x❙| - 4) div ❙|y❙| + 2 ⟶ primitive (x ⋅ y ⇧@ k))"
    (is "bin_prim x y ⟷ (?xxy ∧ ?xyk)")
proof (intro iffI[OF _ contrapos_pp])
  assume "bin_prim x y"
  show "?xxy ∧ ?xyk"
  proof (intro conjI allI impI)
    show "primitive (x ⋅ x ⋅ y)"
      using bin_prim_xyk[OF ‹bin_prim x y›[symmetric], of 2] conjug_prim_iff'
      by (simp add: conjug_prim_iff'[of y])
    show "primitive (x ⋅ y ⇧@ k)" if "1 ≤ k ∧ k ≤ (❙|x❙| - 4) div ❙|y❙| + 2" for k
      using bin_prim_xyk[OF ‹bin_prim x y›, of k] conjunct1[OF that]
      by fastforce
  qed
next
  assume "¬ bin_prim x y"
  then consider "¬ primitive (x ⋅ x ⋅ y)"
  | k where "1 ≤ k" and "k ≤ (❙|x❙| - 4) div ❙|y❙| + 2"
    and "¬ primitive (x ⋅ y ⇧@ k)"
  by (elim len_le_not_bin_primE[OF ‹❙|y❙| ≤ ❙|x❙|›])
  then show "¬ (?xxy ∧ ?xyk)"
    by (cases) blast+
qed

lemma len_eq_bin_prim_iff:
  assumes "❙|x❙| = ❙|y❙|"
  shows "bin_prim x y ⟷ primitive (x ⋅ y)"
proof
  show "bin_prim x y ⟹ primitive (x ⋅ y)"
    using bin_prim_xyk[of _ _ 1]
    by simp
  assume "primitive (x ⋅ y)"
  then have "x ⋅ y ≠ y ⋅ x"
    using assms eq_append_not_prim by auto
  from this bin_uniform_prim_morph[OF this ‹❙|x❙| = ❙|y❙|› ‹primitive (x ⋅ y)›]
  show "bin_prim x y"
    unfolding bin_prim_altdef2
    by simp
qed

theorem bin_prim_iff:
  "bin_prim x y ⟷
    (if ❙|y❙| < ❙|x❙|
      then primitive (x ⋅ x ⋅ y) ∧ (∀k. 1 ≤ k ∧ k ≤ (❙|x❙| - 4) div ❙|y❙| + 2 ⟶ primitive (x ⋅ y ⇧@ k))
    else if ❙|x❙| < ❙|y❙|
      then primitive (y ⋅ y ⋅ x) ∧ (∀k. 1 ≤ k ∧ k ≤ (❙|y❙| - 4) div ❙|x❙| + 2 ⟶ primitive (y ⋅ x ⇧@ k))
    else primitive (x ⋅ y)
    )"
proof (cases rule: linorder_cases)
  assume "❙|x❙| < ❙|y❙|"
  then show ?thesis
    unfolding bin_prim_commutes[of x y]
    unfolding len_le_bin_prim_iff[OF less_imp_le[OF ‹❙|x❙| < ❙|y❙|›]]
    by (simp only: if_not_P[OF less_not_sym] if_P)
next
  assume "❙|y❙| < ❙|x❙|"
  then show ?thesis
    unfolding len_le_bin_prim_iff[OF less_imp_le[OF ‹❙|y❙| < ❙|x❙|›]]
    by (simp only: if_P)
next
  assume "❙|x❙| = ❙|y❙|"
  then show ?thesis
    unfolding len_eq_bin_prim_iff[OF ‹❙|x❙| = ❙|y❙|›]
    by simp
qed

subsection ‹Code equation for @{term bin_prim} predicate›

context
begin

private lemma all_less_Suc_conv: "(∀k < n. P (Suc k)) ⟷ (∀k ≤ n. k ≥ 1 ⟶ P k)"
proof (intro iffI allI impI)
  fix k
  assume "∀k<n. P (Suc k)" and "k ≤ n" and "1 ≤ k"
  then show "P k"
    by (elim allE[of _ "k - 1"]) (simp only: Suc_diff_1)
qed simp

lemma bin_prim_iff' [code]:
  "bin_prim x y ⟷
    (if ❙|y❙| < ❙|x❙|
      then primitive (x ⋅ x ⋅ y) ∧ (∀k < (❙|x❙| - 4) div ❙|y❙| + 2. primitive (x ⋅ y ⇧@ (Suc k)))
    else if ❙|x❙| < ❙|y❙|
      then bin_prim y x
    else primitive (x ⋅ y)
    )"
proof (cases rule: linorder_cases)
  show "❙|x❙| < ❙|y❙| ⟹ ?thesis"
    unfolding bin_prim_commutes[of x y]
    by simp
next
  assume "❙|y❙| < ❙|x❙|"
  then show ?thesis
    using len_le_bin_prim_iff[OF less_imp_le[OF ‹❙|y❙| < ❙|x❙|›]]
    unfolding all_less_Suc_conv[where P = "λk. primitive (_ ⋅ _ ⇧@ k)"]
    unfolding conj_comms[of "1 ≤ _"] imp_conjL
    by (simp only: if_P)
next
  assume "❙|x❙| = ❙|y❙|"
  then show ?thesis
    unfolding len_eq_bin_prim_iff[OF ‹❙|x❙| = ❙|y❙|›]
    by simp
qed

end
value "bin_prim (𝔞⋅𝔟⋅𝔟⋅𝔞⋅𝔞) 𝔟" ― ‹True›
value "bin_prim (𝔞⋅𝔟⋅𝔟⋅𝔞) 𝔟" ― ‹False›
value "bin_prim (𝔞⋅𝔟⋅𝔟⋅𝔞) (𝔟⋅𝔞⋅𝔟⋅𝔞⋅𝔟)" ― ‹False›
value "bin_prim (𝔞⋅𝔟) (𝔞⋅𝔟)" ― ‹False›
value "bin_prim (𝔞⋅𝔟) (𝔞⋅𝔟⋅𝔞⋅𝔟)" ― ‹False›
value "bin_prim (𝔞⋅𝔟⋅𝔟⋅𝔞⋅𝔞) (𝔟⋅𝔟⋅𝔟⋅𝔟⋅𝔟⋅𝔟)" ― ‹True›

section ‹Characterization of binary imprimitivity codes›

theorem bin_imprim_code_iff:
  "bin_imprim_code x y ⟷ x ⋅ y ≠ y ⋅ x ∧
    (if ❙|y❙| < ❙|x❙|
      then ¬ primitive (x ⋅ x ⋅ y) ∨ (∃k. 1 ≤ k ∧ k ≤ (❙|x❙| - 4) div ❙|y❙| + 2 ∧ ¬ primitive (x ⋅ y ⇧@ k))
    else if ❙|x❙| < ❙|y❙|
      then ¬ primitive (y ⋅ y ⋅ x) ∨ (∃k. 1 ≤ k ∧ k ≤ (❙|y❙| - 4) div ❙|x❙| + 2 ∧ ¬ primitive (y ⋅ x ⇧@ k))
    else ¬ primitive (x ⋅ y)
    )"
  unfolding bin_imprim_code_def bin_prim_iff
  by (simp only: de_Morgan_conj not_all not_imp conj_assoc flip: if_image[of _ Not])

value "bin_imprim_code (𝔞⋅𝔟⋅𝔟⋅𝔞⋅𝔞) 𝔟" ― ‹False›
value "bin_imprim_code  (𝔞⋅𝔟⋅𝔟⋅𝔞) 𝔟" ― ‹True›
value "bin_imprim_code  (𝔞⋅𝔟⋅𝔟⋅𝔞) (𝔟⋅𝔞⋅𝔟⋅𝔞⋅𝔟)" ― ‹True›
value "bin_imprim_code  (𝔞⋅𝔟) (𝔞⋅𝔟)" ― ‹False›
value "bin_imprim_code  (𝔞⋅𝔟) (𝔞⋅𝔟⋅𝔞⋅𝔟)" ― ‹False›
value "bin_imprim_code  (𝔞⋅𝔟⋅𝔟⋅𝔞⋅𝔞) (𝔟⋅𝔟⋅𝔟⋅𝔟⋅𝔟⋅𝔟)" ― ‹False›


end