Theory ABC_Words

section ‹Words over the terminals ‹{A,B,C}››

theory ABC_Words
imports Main
begin

text ‹This theory is convenient for examples involving exactly the letters A, B, C.
These examples often involve families ‹A^i B^j C^k›. Hence ‹sorted› is relevant.
›

datatype letter = A | B | C

definition abcword :: "nat ⇒ nat ⇒ nat ⇒ letter list" where
"abcword i j k = replicate i A @ replicate j B @ replicate k C"

text ‹Letter counts of an ‹abcword› recover its three exponents.›

lemma count_abcword:
  "count_list (abcword i j k) A = i"
  "count_list (abcword i j k) B = j"
  "count_list (abcword i j k) C = k"
  by (auto simp: abcword_def)

lemma abcword_inj: "abcword i j k = abcword i' j' k' ⟹ i = i' ∧ j = j' ∧ k = k'"
  by (metis count_abcword)

text ‹Order the alphabet ‹A < B < C›.›

fun rank :: "letter ⇒ nat" where
"rank A = 0" | "rank B = Suc 0" | "rank C = Suc (Suc 0)"

lemma rank_inj: "rank x = rank y ⟹ x = y"
  by (cases x; cases y) simp_all

instantiation letter :: linorder
begin

definition less_eq_letter :: "letter ⇒ letter ⇒ bool" where
"less_eq_letter x y ⟷ rank x ≤ rank y"

definition less_letter :: "letter ⇒ letter ⇒ bool" where
"less_letter x y ⟷ rank x < rank y"

instance
  by intro_classes (auto simp: less_eq_letter_def less_letter_def dest: rank_inj)

end

lemma abcword_sorted: "sorted (abcword i j k)"
  by (auto simp: abcword_def sorted_append less_eq_letter_def)

text ‹A factor that occurs squared inside a sorted word is uniform (all one letter).›

lemma sorted_square_uniform:
  assumes "sorted (ys @ ys)" "a ∈ set ys" "b ∈ set ys"
  shows "a = b"
proof -
  from assms(1) have "∀p∈set ys. ∀q∈set ys. p ≤ q" by (auto simp: sorted_append)
  thus ?thesis using assms(2,3) by (meson antisym)
qed

lemma sorted_factor_uniform:
  assumes "sorted (u @ ys @ ys @ v)" "a ∈ set ys" "b ∈ set ys"
  shows "a = b"
proof -
  have "sorted (ys @ ys)" using assms(1) by (auto simp: sorted_append)
  thus ?thesis using sorted_square_uniform assms(2,3) by blast
qed

end