theory CoWBasic
  imports Main
begin                                                            

chapter "Combinatorics on Words - Basic"

section "Preliminaries"

text\<open>We use lists as a basic datatype. We first give a few abbreviations and definitions concerning lists, followed by some lemmas.\<close>

subsection "Definitions and notations"

abbreviation concat_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<cdot>" 70) where
  "concat_list xs ys \<equiv> xs @ ys"

abbreviation empty_list :: "'a list" ("\<epsilon>") where
  "empty_list \<equiv> []"

abbreviation nonempty_element (infixl "\<in>n" 50) where "u \<in>n S \<equiv> (u \<in> S \<and> u \<noteq> \<epsilon>)"

abbreviation drop_emp :: "'a list set \<Rightarrow> 'a list set" ( "_\<^sub>+" [1000] ) where
  "drop_emp S \<equiv> S - {\<epsilon>}"

lemma nemp_elem_setI[intro]: "u \<in> S \<Longrightarrow> u \<noteq> \<epsilon> \<Longrightarrow> u \<in> S\<^sub>+"
  by simp

lemma nel_drop_emp: "u \<in>n S \<Longrightarrow> u \<in> S\<^sub>+"
  by simp

lemma nel_drop_emp': "u \<in> S\<^sub>+ \<Longrightarrow> u \<in>n S"
  by simp

definition  prefix (infixl "\<le>p" 50) where prefix_def[simp]:  "u \<le>p v \<equiv> \<exists> z. v = u \<cdot> z"

lemma prefI[simp, intro]: " v = u \<cdot> z \<Longrightarrow> u \<le>p v"
  by simp

lemma prefE[simp, elim]: "u \<le>p v \<Longrightarrow> \<exists> z. v = u \<cdot> z"
  by simp

abbreviation prefix_comparable  :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "\<bowtie>" 50) 
  where "(prefix_comparable u v) \<equiv> u \<le>p v \<or> v \<le>p u"

definition nonempty_prefix (infixl "\<le>np" 50) where nonempty_prefix_def[simp]:  "u \<le>np v \<equiv> u \<noteq> \<epsilon> \<and> u \<le>p v"

lemma nemp_prefI_pref[intro]: "u \<noteq> \<epsilon> \<Longrightarrow> u \<le>p v \<Longrightarrow> u \<le>np v"
  by simp

lemma nemp_prefI[intro]: "u \<noteq> \<epsilon> \<Longrightarrow> (\<exists> z. v = u \<cdot> z) \<Longrightarrow> u \<le>np v"
  by simp

definition suffix (infixl "\<le>s" 60) where suffix_def[simp]:  "u \<le>s v \<equiv> \<exists> z. v = z\<cdot>u"

abbreviation suffix_comparable :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "\<bowtie>\<^sub>s" 50) 
  where "(suffix_comparable u v) \<equiv> u \<le>s v \<or> v \<le>s u"

lemma sufI[simp, intro]: " v = z \<cdot> u \<Longrightarrow> u \<le>s v"
  by simp

lemma sufE[simp, elim]: "u \<le>s v \<Longrightarrow> \<exists> z. v = z \<cdot> u"
  by simp

definition nonempty_suffix (infixl "\<le>ns" 60) where nonempty_suffix_def[simp]:  "u \<le>ns v \<equiv> u \<noteq> \<epsilon> \<and> u \<le>s v"

definition factor (infixl "\<le>f" 60) where factor_def[simp]:  "u \<le>f v \<equiv> \<exists> p s. v = p\<cdot>u\<cdot>s"

definition nonempty_factor (infixl "\<le>nf" 60) where nonempty_factor_def[simp]:  "u \<le>nf v \<equiv> u \<noteq> \<epsilon> \<and> (\<exists> p s. v = p\<cdot>u\<cdot>s)"

notation
  length  ("\<^bold>|_\<^bold>|") \<comment> \<open>note that it's bold |\<close>

text\<open>A useful function of left quotient. Note that the function is sometimes undefined.\<close>

fun left_quotient:: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"   ("(_\<inverse>\<^sup>>)(_)" [51,51] 69)
  where  left_quotient_def: "left_quotient u v  = (THE z. u \<cdot> z = v)"

text\<open>Analogously, we define the right quotient.\<close>

definition right_quotient :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"  ("(_) (\<^sup><\<inverse>_) " [51,1000] 69)
  where  right_quotient_def[simp]: "right_quotient u v  = rev (rev v\<inverse>\<^sup>> rev u)"

subsection \<open>Power\<close>

primrec list_power :: "'a list \<Rightarrow> nat \<Rightarrow> 'a list" (infixr "\<^sup>@" 80) where
  power_zero: "u\<^sup>@0 = \<epsilon>" |
  power_Suc_list: "u\<^sup>@(Suc n) = u \<cdot> u\<^sup>@n" 

lemma power_add_list: "u\<^sup>@a \<cdot> u\<^sup>@b = u\<^sup>@(a+b)"
  by (induct a) auto

lemma power_Suc2_list: "u\<^sup>@(Suc n) = u\<^sup>@n \<cdot> u"
  by (induct n) auto

lemma power_eq_if_list: "p\<^sup>@m = (if m = 0 then \<epsilon> else p \<cdot> p\<^sup>@(m-1))"
  unfolding One_nat_def by (cases m) simp_all

lemma power_mult_list: "(u\<^sup>@m)\<^sup>@n = u\<^sup>@(m*n)"
  by (induct n) (simp_all add: power_add_list)

lemma emp_power: "\<epsilon>\<^sup>@n = \<epsilon>"
  by (induct n) auto

lemma power_one_id: "u\<^sup>@1 = u" 
  by auto

lemma power2_list: "u\<^sup>@2 = u \<cdot> u"
  by (metis Suc_1 power_Suc_list power_one_id)

subsection "Length and its properties"

lemma eqd_pref: "(x \<cdot> y = u \<cdot> v) \<Longrightarrow> \<^bold>|x\<^bold>| \<le> \<^bold>|u\<^bold>| \<Longrightarrow> x \<cdot> (x\<inverse>\<^sup>> u) = u \<and> (x\<inverse>\<^sup>> u) \<cdot> v = y"
  by (simp add: append_eq_conv_conj)

lemma eqd_equal: "\<lbrakk>\<^bold>|x\<^bold>| = \<^bold>|u\<^bold>|;  x \<cdot> y = u \<cdot> v\<rbrakk> \<Longrightarrow> x = u \<and> y = v"
  by simp 

lemma len_after_drop: "p + q \<le> \<^bold>|w\<^bold>| \<Longrightarrow>  q \<le> \<^bold>|drop p w\<^bold>|"
  by simp 

lemma hd_prod: "u \<noteq> \<epsilon> \<Longrightarrow> (u \<cdot> v)!0 = u!0"
  by (metis Nil_is_append_conv hd_append2 hd_conv_nth)

lemma sing_word: "\<^bold>|b\<^bold>| = 1 \<Longrightarrow> b = [hd b]"
  by (metis diff_self_eq_0 length_0_conv length_tl list.expand list.sel(1) list.sel(3) not_Cons_self2 zero_neq_one)   

lemma nonsing_concat_len: "\<^bold>|us\<^bold>| \<noteq> 1 \<Longrightarrow> concat us \<noteq> \<epsilon> \<Longrightarrow> 1 < \<^bold>|us\<^bold>|"
  using nat_neq_iff by fastforce

lemma sing_len: "\<^bold>|[a]\<^bold>| = 1"
  by simp

lemma pref_len: "w \<le>p z \<Longrightarrow> \<^bold>|w\<^bold>| \<le> \<^bold>|z\<^bold>|"
  by force

lemma drop_len: "\<^bold>|u \<cdot> w\<^bold>| \<le> \<^bold>|u \<cdot> v \<cdot> w\<^bold>|"
  by simp

lemma take_len: "p \<le> \<^bold>|w\<^bold>| \<Longrightarrow> \<^bold>|take p w\<^bold>| = p"
  by simp

subsection "Left Quotient"

lemma lqI:  "v = u \<cdot> z \<Longrightarrow> u\<inverse>\<^sup>>  v  = z"
  by simp

lemma lq_id: "u\<inverse>\<^sup>> u = \<epsilon>"     
  by auto

lemma lq_emp: "\<epsilon>\<inverse>\<^sup>> u = u"  
  by auto       

lemma lq_pref: "u \<le>p v \<Longrightarrow> u \<cdot> (u\<inverse>\<^sup>> v) = v"
  by auto

lemma lq_reassoc: "u \<le>p v \<Longrightarrow> (u\<inverse>\<^sup>> v)\<cdot>w = u\<inverse>\<^sup>> v\<cdot>w"
  by auto

lemma lq_prod: "u \<le>p v\<cdot>u \<Longrightarrow> u \<le>p w\<cdot>u \<Longrightarrow>  u\<inverse>\<^sup>> v\<cdot>w\<cdot>u = (u\<inverse>\<^sup>> v\<cdot>u)\<cdot>(u\<inverse>\<^sup>> w\<cdot>u)"
  by (metis append.assoc lq_pref lq_reassoc)

lemma lq_ne: "p \<le>p u\<cdot>p \<Longrightarrow> u \<noteq> \<epsilon> \<Longrightarrow> p\<inverse>\<^sup>>u\<cdot>p \<noteq> \<epsilon>"
  by auto

lemma rev_lq: "r \<le>p s \<Longrightarrow> rev (r\<inverse>\<^sup>>s) \<le>p rev s"
  by auto

lemma rev_lq': "r \<le>p s \<Longrightarrow> rev (r\<inverse>\<^sup>>s) = (rev s)\<^sup><\<inverse>(rev r)"
  by auto

lemma lq_len: "r \<le>p s \<Longrightarrow> \<^bold>|s\<^bold>| = \<^bold>|r\<^bold>| +  \<^bold>|r\<inverse>\<^sup>>s\<^bold>|"
  by auto    

subsection "Right quotient"

lemma rqI: "v = u \<cdot> z \<Longrightarrow> v \<^sup><\<inverse>z  = u"
  by simp

lemma rq_id: "u \<^sup><\<inverse>u  = \<epsilon>"
  by simp

lemma rq_emp: "u \<^sup><\<inverse>\<epsilon> = u"
  by simp

lemma rq_suf: "v \<le>s u \<Longrightarrow> (u \<^sup><\<inverse>v ) \<cdot> v = u"
  by auto

lemma lq_rev_rq: "u \<le>p v \<Longrightarrow>  (rev v) \<^sup><\<inverse>(rev u) = rev (u\<inverse>\<^sup>> v)"
  by simp

lemma rq_rev_lq: "v \<le>s u \<Longrightarrow> (rev v)\<inverse>\<^sup>> rev u = rev (u \<^sup><\<inverse>v )"
  by auto 

lemma rq_the: "v \<le>s u \<Longrightarrow> u \<^sup><\<inverse>v = (THE z. u = z \<cdot> v)"
  unfolding rq_suf by auto

subsection "Prefix and its properties"

text\<open>Empty and nonempty prefixes.\<close>

lemma triv_pref: "r \<le>p r \<cdot> s"
  by simp

lemma self_pref: "r \<le>p r"
  by simp

lemma pref_antisym: "r \<le>p s \<Longrightarrow> s \<le>p r \<Longrightarrow> r = s"
  by auto

lemma pref_take_len: "p \<le>p w \<Longrightarrow> p = take \<^bold>|p\<^bold>| w"
  by auto

lemma pref_same_len: "u \<le>p v \<Longrightarrow> \<^bold>|u\<^bold>| = \<^bold>|v\<^bold>| \<Longrightarrow> u = v"
  by auto    

lemma add_nth: "n < \<^bold>|w\<^bold>| \<Longrightarrow>  (take n w) \<cdot> [w!n] \<le>p w"
  using id_take_nth_drop by fastforce

lemma add_nth_pref: "u \<le>p w \<Longrightarrow> u \<noteq> w \<Longrightarrow> u \<cdot> [w!\<^bold>|u\<^bold>|] \<le>p w"
  by (metis add_nth le_eq_less_or_eq pref_len pref_same_len pref_take_len)

lemma nth_pref_ex: assumes "k < Suc \<^bold>|w\<^bold>|" shows "\<exists>u. (u \<le>p w \<and> \<^bold>|u\<^bold>| = k)"
proof-
  have "\<^bold>|take k w\<^bold>| = k" 
    using assms by auto 
  moreover have "take k w \<le>p w"
    using  prefI[OF sym[OF append_take_drop_id[of k w]]]. 
  ultimately show ?thesis
    by blast
qed

lemma pref_shorter: "u \<le>p v \<Longrightarrow> u \<noteq> v \<Longrightarrow> \<^bold>|u\<^bold>| < \<^bold>|v\<^bold>|"
  by auto

lemma pref_trans[trans]: "u \<le>p v \<Longrightarrow> v \<le>p w \<Longrightarrow> u \<le>p w"
  by auto

lemma pref_prod_shorter: assumes "u \<le>p z \<cdot> w" "v \<le>p w" "\<^bold>|u\<^bold>| \<le> \<^bold>|z \<cdot> v\<^bold>|"
  shows "u \<le>p z \<cdot> v"
proof-
  have "u \<le>p z \<cdot> v \<cdot> (v\<inverse>\<^sup>> w)"
    using \<open>u \<le>p z \<cdot> w\<close> \<open>v \<le>p w\<close>
    by (metis append_assoc lq_pref)  
  thus "u \<le>p z \<cdot> v" 
    using \<open>\<^bold>|u\<^bold>| \<le> \<^bold>|z \<cdot> v\<^bold>|\<close>
    by (metis eqd_pref lq_pref prefI)
qed

lemma pref_index: "u \<le>p w \<Longrightarrow> i < \<^bold>|u\<^bold>| \<Longrightarrow> u!i = w!i"
  by (metis nth_append prefE)

lemma index_pref: assumes "\<^bold>|u\<^bold>| \<le> \<^bold>|w\<^bold>|" "\<forall>i < \<^bold>|u\<^bold>|. u!i = w!i" shows "u \<le>p w"
  using  append_eq_conv_conj[of u \<epsilon> u] append_Nil2[of u] 
    nth_take_lemma[of "\<^bold>|u\<^bold>|" u w, OF order_refl[of "\<^bold>|u\<^bold>|"] \<open>\<^bold>|u\<^bold>| \<le> \<^bold>|w\<^bold>|\<close>]  \<open>\<forall>i < \<^bold>|u\<^bold>|. u!i = w!i\<close>
    prefI[of w "take \<^bold>|u\<^bold>| w" "drop \<^bold>|u\<^bold>| w", OF sym[OF append_take_drop_id[of "\<^bold>|u\<^bold>|" w]]]
  by simp

lemma pref_cancel: "u\<cdot>v \<le>p u\<cdot>w \<Longrightarrow> v \<le>p w"
  by simp

lemma pref_drop: assumes "p \<le> \<^bold>|w\<^bold>|" "w \<le>p w'" shows "drop p w \<le>p drop p w'"
proof-
  have "take p w = take p w'"
    using assms by auto
  show ?thesis
    using pref_cancel[of "take p w" "drop p w" "drop p w'"]
    unfolding append_take_drop_id[of p w] 
    unfolding \<open>take p w = take p w'\<close> append_take_drop_id[of p w'] using \<open>w \<le>p w'\<close> 
    by blast
qed

lemma pref_ext: "u \<le>p v \<Longrightarrow> z \<cdot> u \<le>p z \<cdot> v"
  by simp

lemma pref_prod_shorter1: assumes "u \<le>p z\<cdot>u\<cdot>w" shows "u \<le>p z\<cdot>u"
proof-
  have "u \<le>p z \<cdot> (u \<cdot> w)"
    using \<open>u \<le>p z\<cdot>u\<cdot>w\<close> unfolding  append_assoc[of z u w] .
  have "\<^bold>|u\<^bold>| \<le> \<^bold>|z \<cdot> u\<^bold>|" using length_append by simp 
  show "u \<le>p z\<cdot>u" 
    using pref_prod_shorter[OF \<open>u \<le>p z \<cdot> (u \<cdot> w)\<close> triv_pref \<open>\<^bold>|u\<^bold>| \<le> \<^bold>|z \<cdot> u\<^bold>|\<close>].
qed

lemma pref_prod_shorter2: "u \<le>p z \<cdot> s \<Longrightarrow> u \<le>p s \<Longrightarrow> u \<le>p z \<cdot> u"
  using pref_prod_shorter1[of u z "u\<inverse>\<^sup>>s"] lq_pref[of u s] append_assoc[of z u "u\<inverse>\<^sup>>s"]
  by presburger

lemma pref_prolong:  "w \<le>p z \<cdot> r \<Longrightarrow> r \<le>p s \<Longrightarrow> w \<le>p z \<cdot> s"
  using pref_ext pref_trans by blast

lemma pref_prolong': "u \<le>p w \<cdot> z \<Longrightarrow> v \<cdot> u \<le>p z \<Longrightarrow> u \<le>p w \<cdot> v \<cdot> u"
  by (metis append_assoc lq_pref pref_prod_shorter1)

lemma pref_prolong_comp: "u \<le>p w \<cdot> z \<Longrightarrow> v \<cdot> u \<bowtie> z \<Longrightarrow> u \<le>p w \<cdot> v \<cdot> u"
  by (metis append_assoc pref_prolong pref_prolong')

lemma pref_comm_product: "u\<cdot>v \<le>p v\<cdot>u\<cdot>w \<Longrightarrow> u\<cdot>v = v\<cdot>u"
  by (metis Groups.add_ac(2) eqd_equal length_append lq_pref)

lemma comme_ruler: "r \<cdot> s \<le>p w1 \<Longrightarrow> s \<cdot> r \<le>p w2 \<Longrightarrow> w1 \<bowtie> w2 \<Longrightarrow> r \<cdot> s = s \<cdot> r"
  by (metis lq_pref pref_comm_product pref_trans)

lemma pref_share_take: "u \<le>p v \<Longrightarrow> q \<le> \<^bold>|u\<^bold>| \<Longrightarrow> take q u = take q v"
  by auto

lemma ruler_le:  "\<lbrakk>u \<le>p x; v \<le>p x; \<^bold>|u\<^bold>| \<le> \<^bold>|v\<^bold>| \<rbrakk> \<Longrightarrow> (u \<le>p v)"
  by (metis eqd_pref prefix_def)

lemma pref_pref_short_pref: "v \<le>p u \<cdot> z \<Longrightarrow> \<^bold>|u\<^bold>| \<le> \<^bold>|v\<^bold>| \<Longrightarrow> u \<le>p v"
  using ruler_le[of u "u \<cdot> z" v, OF triv_pref]. 

lemma ruler:  "\<lbrakk> u \<le>p x; v\<le>p x \<rbrakk> \<Longrightarrow> (u \<le>p v) \<or> (v \<le>p u) "
  by (meson le_cases ruler_le)

lemma pref_prod_longer: "u \<le>p z \<cdot> w \<Longrightarrow> v \<le>p w \<Longrightarrow> \<^bold>|z \<cdot> v\<^bold>| \<le> \<^bold>|u\<^bold>|  \<Longrightarrow> z \<cdot> v \<le>p u" 
  using ruler_le[of  "z \<cdot> v" "z \<cdot> w" u] pref_ext[of v w z] by blast

lemma ruler_comp: "w \<le>p v\<cdot>z \<Longrightarrow> w \<bowtie> v"
  using ruler by blast

lemma pref_power:  "u \<le>p t\<^sup>@k  \<Longrightarrow> (\<exists> m. t\<^sup>@m \<le>p u \<and> u \<le>p t\<^sup>@m \<cdot> t)"
proof (induct k)
  case 0 
  then show ?case
    by (metis append_self_conv2 power_zero prefI pref_antisym)
next
  case (Suc k)
  then show ?case
    using power_Suc2_list
    by (metis ruler_comp)
qed 

lemma pref_power_eq: "x \<le>p r\<^sup>@l \<Longrightarrow> \<exists> k z. x = r\<^sup>@k\<cdot>z \<and> z \<le>p r"
  using pref_power by (metis lq_pref pref_cancel)

lemma pref_rq: "w \<le>p (w \<^sup><\<inverse>z ) \<Longrightarrow> z \<le>s w \<Longrightarrow> z = \<epsilon>"
  unfolding right_quotient_def by auto

lemma distinct_first: "w \<noteq> \<epsilon> \<Longrightarrow> z \<noteq> \<epsilon> \<Longrightarrow> w!0 \<noteq> z!0 \<Longrightarrow> w \<cdot> w' \<noteq> z \<cdot> z'"
  by (metis hd_prod)

lemma last_no_split: "q \<le>p w \<cdot> [a] \<Longrightarrow> \<not> q \<le>p w \<Longrightarrow> q = w \<cdot> [a]"
  by (metis butlast_append butlast_snoc prefix_def)

subsubsection "Prefix comparability"

lemma pref_comp_len: "w \<bowtie> v \<Longrightarrow> \<^bold>|v\<^bold>| \<le> \<^bold>|w\<^bold>| \<Longrightarrow> v \<le>p w"
  by auto

lemma pref_comp_len_trans: "u \<bowtie> v \<Longrightarrow> \<^bold>|w\<^bold>| \<le> \<^bold>|u\<^bold>| \<Longrightarrow> w \<le>p v \<Longrightarrow>  w \<le>p u"
  using pref_trans ruler_le by blast

lemma comp_ext: "z \<cdot> w1 \<bowtie> z \<cdot> w2 \<longleftrightarrow> w1 \<bowtie> w2"
  using pref_cancel pref_ext by blast

lemma incomp_ext: "\<not> w1 \<bowtie>  w2 \<Longrightarrow> \<not> w1 \<cdot> z \<bowtie> w2 \<cdot> z'"
  by (meson prefI pref_trans ruler)

lemma mismatch_incopm: "\<^bold>|u\<^bold>| = \<^bold>|v\<^bold>| \<Longrightarrow> x \<noteq> y \<Longrightarrow> \<not> u \<cdot> [x] \<bowtie> v \<cdot> [y]"
  by simp

lemma rotate_comp_eq:"w \<bowtie> rotate n w \<Longrightarrow> w = rotate n w"
  by (metis length_rotate pref_same_len)

subsection "Suffix and suffix properties"

lemma pref_rev_suf: "u \<le>p v \<Longrightarrow> rev u \<le>s rev v"
  by (metis lq_pref rev_append sufI)

lemma pref_rev_suf': "rev u \<le>p rev v \<Longrightarrow> u \<le>s v"
  using  pref_rev_suf[of "rev u" "rev v"] unfolding rev_rev_ident. 

lemma suf_rev_pref: "u \<le>s v \<Longrightarrow> rev u \<le>p rev v"
  by (metis lqI prefI rev_lq rq_suf)

lemma suf_rev_pref': "rev u \<le>s rev v \<Longrightarrow>  u \<le>p v"
  using  suf_rev_pref[of "rev u" "rev v"] unfolding rev_rev_ident. 

lemma ruler_le_suf: assumes  "u \<le>s x" and  "v \<le>s x" and "\<^bold>|u\<^bold>| \<le> \<^bold>|v\<^bold>|"
  shows "u \<le>s v"
  using ruler_le[OF suf_rev_pref[OF \<open>u \<le>s x\<close>] suf_rev_pref[OF \<open>v \<le>s x\<close>]] 
  unfolding length_rev  
  using \<open>\<^bold>|u\<^bold>| \<le> \<^bold>|v\<^bold>|\<close> pref_rev_suf[of "rev u" "rev v"] 
  unfolding rev_rev_ident 
  by blast

lemma suf_prod_shorter1: "u \<le>s z \<cdot> u \<cdot> w \<Longrightarrow> u \<le>s u \<cdot> w"
  by (metis pref_prod_shorter2 pref_rev_suf' rev_append sufI suf_rev_pref)

lemma suf_prod_shorter2: "z \<le>s s \<cdot> w \<Longrightarrow> z \<le>s s \<Longrightarrow> z \<le>s z \<cdot> w"
  using sufE suf_prod_shorter1 by blast

lemma suf_prolong:  "w \<le>s  r \<cdot> v \<Longrightarrow> r \<le>s s \<Longrightarrow> w \<le>s s \<cdot> v"
  using pref_prolong[of "rev w" "rev v" "rev r" "rev s"]
  by (metis pref_rev_suf' rev_append rev_rev_ident suf_rev_pref')

lemma suf_prolong': assumes "u \<le>s z \<cdot> w" and "u \<cdot> v \<le>s z" shows "u \<le>s u \<cdot> v \<cdot> w"
proof-
  have "u \<cdot> v \<cdot> w \<le>s z \<cdot> w"
    using \<open>u \<cdot> v \<le>s z\<close> by auto 
  thus "u \<le>s u \<cdot> v \<cdot> w"  
    using ruler_le_suf[OF \<open>u \<le>s z \<cdot> w\<close> \<open>u \<cdot> v \<cdot> w \<le>s z \<cdot> w\<close>] append_assoc prefI pref_len by blast
qed

lemma suf_prolong_comp: "u \<le>s z \<cdot> w \<Longrightarrow> u \<cdot> v \<bowtie>\<^sub>s z \<Longrightarrow> u \<le>s u \<cdot> v \<cdot> w"
  using suf_prolong suf_prolong' by blast   

lemma suf_prod_shorter3: "z \<le>s s \<cdot> w \<Longrightarrow> u \<le>s s \<Longrightarrow>  \<^bold>|z\<^bold>| \<le> \<^bold>|u \<cdot> w\<^bold>| \<Longrightarrow>  z \<le>s u \<cdot> w"
  by (metis append.assoc rq_suf ruler_le_suf sufI)

lemma suf_prod_shorter4: "w \<le>s r \<cdot> s \<Longrightarrow> \<^bold>|w\<^bold>| \<le> \<^bold>|s\<^bold>| \<Longrightarrow> w \<le>s s"
  using ruler_le_suf by blast

lemma suf_comp: "z \<le>s u\<cdot>w \<Longrightarrow> \<not> z \<le>s w \<Longrightarrow> w \<le>s z"
  by (metis pref_rev_suf' rev_append ruler_comp suf_rev_pref)

lemma suf_ext_left: "u \<le>s v \<Longrightarrow> u \<le>s w\<cdot>v"
  by auto

lemma long_pref_short_suf: "x \<le>p w \<Longrightarrow> \<^bold>|w\<^bold>| < \<^bold>|x\<^bold>|+\<^bold>|x\<^bold>| \<Longrightarrow> w = x\<cdot>s \<Longrightarrow> \<^bold>|s\<^bold>| < \<^bold>|x\<^bold>|"
  by simp

lemma suf_trans: "u \<le>s v \<Longrightarrow> v \<le>s w \<Longrightarrow> u \<le>s w"
  using sufE suf_ext_left by blast

lemma suf_trans_eq: "u \<le>s v \<Longrightarrow> v \<le>s w \<Longrightarrow> u = w \<Longrightarrow> u = v"
  by auto

subsubsection "Suffix comparability"

lemma pref_suf_rev_comp: "w \<bowtie> v \<Longrightarrow> (rev w) \<bowtie>\<^sub>s (rev v)"
  using pref_rev_suf by blast

lemma pref_suf_rev_comp1: "(rev w) \<bowtie>\<^sub>s (rev v) \<Longrightarrow> w \<bowtie> v"
  using suf_rev_pref' by blast

lemma pref_suf_rev_comp2: "(rev w) \<bowtie> (rev v) \<Longrightarrow> w \<bowtie>\<^sub>s v"
  using pref_rev_suf' by blast

lemma pref_suf_rev_comp3: "w \<bowtie>\<^sub>s v \<Longrightarrow> (rev w) \<bowtie> (rev v)"
  using suf_rev_pref by blast

subsection \<open>Longest common prefix\<close>

fun get_longest_common_prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ \<and>\<^sub>p _" [61,62] 66)
  where "\<epsilon> \<and>\<^sub>p v = \<epsilon>" |
    "v \<and>\<^sub>p \<epsilon> = \<epsilon>" |
    "(a#u) \<and>\<^sub>p (b#v) = (if a\<noteq>b then \<epsilon> else (a # (u \<and>\<^sub>p v)))"

lemmas lcp_simps = get_longest_common_prefix.simps

lemma lcp_sym: "u \<and>\<^sub>p v = v \<and>\<^sub>p u"
  by (induct u v rule: list_induct2') auto

lemma lcp_pref: "u \<and>\<^sub>p v \<le>p v"
  by (induct u v rule: list_induct2') auto

lemma lcp_pref': "u \<and>\<^sub>p v \<le>p u"
  by (metis lcp_pref lcp_sym)

lemma pref_lcp_pref: "w \<le>p u \<and>\<^sub>p v \<Longrightarrow> w \<le>p u"
  using lcp_pref' pref_trans by blast 

lemma pref_lcp_pref': "w \<le>p u \<and>\<^sub>p v \<Longrightarrow> w \<le>p v"
  using pref_lcp_pref lcp_sym by metis

lemma lcp_self: "w \<and>\<^sub>p w = w"
  by (induct w) auto

lemma lcp_len: "\<^bold>|u \<and>\<^sub>p v\<^bold>| \<le> \<^bold>|u\<^bold>|"
  by (induct u v rule: list_induct2') auto

lemma lcp_eq: "\<^bold>|u \<and>\<^sub>p v\<^bold>| = \<^bold>|u\<^bold>| \<Longrightarrow> u \<le>p v"                                           
  by (metis lcp_pref lcp_sym nth_equalityI pref_index)

lemma lcp_len': "\<not> u \<le>p v \<Longrightarrow> \<^bold>|u \<and>\<^sub>p v\<^bold>| < \<^bold>|u\<^bold>|"
  using lcp_eq lcp_len antisym_conv2 by blast

lemma lcp_ext_right: "r \<le>p r' \<or> r' \<le>p r \<or> (r \<cdot> u) \<and>\<^sub>p (r' \<cdot> v) = r \<and>\<^sub>p r'"
  by (induct r r' rule: list_induct2') auto

lemma lcp_same_len: "\<^bold>|u\<^bold>| = \<^bold>|v\<^bold>| \<Longrightarrow> u \<noteq> v \<Longrightarrow> u \<and>\<^sub>p v = u \<cdot> w \<and>\<^sub>p v \<cdot> w'"
  using lcp_ext_right[of u v w w'] pref_same_len[of u v]  pref_same_len[of v u]
  by presburger

lemma lcp_mismatch: "\<^bold>|u \<and>\<^sub>p v\<^bold>| < \<^bold>|u\<^bold>| \<Longrightarrow> \<^bold>|u \<and>\<^sub>p v\<^bold>| < \<^bold>|v\<^bold>| \<Longrightarrow> u! \<^bold>|u \<and>\<^sub>p v\<^bold>| \<noteq> v! \<^bold>|u \<and>\<^sub>p v\<^bold>|"
  by (induct u v rule: list_induct2') auto

lemma lcp_mismatch': "\<not> u \<le>p v \<Longrightarrow> \<not> v \<le>p u \<Longrightarrow> u! \<^bold>|u \<and>\<^sub>p v\<^bold>| \<noteq> v! \<^bold>|u \<and>\<^sub>p v\<^bold>|"
  by (metis lcp_len' lcp_mismatch lcp_sym)

lemma lcp_ext_left: "(z \<cdot> u) \<and>\<^sub>p (z \<cdot> v) = z \<cdot> (u \<and>\<^sub>p v)"
  by (induct z) auto

lemma lcp_first_letters: "u!0 \<noteq> v!0 \<Longrightarrow> u \<and>\<^sub>p v = \<epsilon>"
  by (induct u v rule: list_induct2') auto

lemma lcp_first_mismatch: "a \<noteq> b \<Longrightarrow> w \<cdot> [a] \<cdot> u \<and>\<^sub>p w \<cdot> [b] \<cdot> v  = w"
  by (simp add: lcp_ext_left)

lemma lcp_first_mismatch': "a \<noteq> b \<Longrightarrow> u \<cdot> [a] \<and>\<^sub>p u \<cdot> [b] = u"
  using lcp_first_mismatch[of a b u \<epsilon> \<epsilon>] by simp

lemma lcp_mismatch_shorter: assumes "\<^bold>|u\<^bold>| = \<^bold>|v\<^bold>|" "x \<noteq> y" shows "u \<cdot> [x] \<and>\<^sub>p v \<cdot> [y] = u \<and>\<^sub>p v"
  by (cases "u = v") 
    (simp add: lcp_self[of v]  lcp_first_mismatch'[OF \<open>x \<noteq> y\<close>, of v], 
      use lcp_same_len[OF \<open>\<^bold>|u\<^bold>| = \<^bold>|v\<^bold>|\<close>, of "[x]" "[y]"] in auto)

lemma lcp_rulers: "r \<le>p s \<Longrightarrow> r' \<le>p s' \<Longrightarrow> (r \<le>p r' \<or> r' \<le>p r \<or> r \<and>\<^sub>p r' = s \<and>\<^sub>p s')"
  by (metis lcp_ext_right prefE)

lemma pref_pref_lcp: "w \<le>p r \<Longrightarrow> w \<le>p s \<Longrightarrow> w \<le>p (r \<and>\<^sub>p s)"
  using lcp_ext_left by auto

lemma pref_pref_lcp': "w \<le>p r \<Longrightarrow> w' \<le>p s \<Longrightarrow> w \<and>\<^sub>p w' \<le>p (r \<and>\<^sub>p s)"
  using pref_pref_lcp lcp_pref lcp_sym pref_trans by metis

lemma lcp_distinct_hd: "hd u \<noteq> hd v \<Longrightarrow> u \<and>\<^sub>p v = \<epsilon>"
proof-
  assume "hd u \<noteq> hd v"
  hence "(u \<noteq> \<epsilon> \<and> v \<noteq> \<epsilon>) \<Longrightarrow> hd u \<noteq> hd v \<Longrightarrow>  u \<and>\<^sub>p v = \<epsilon>"
    by (simp add: lcp_first_letters hd_conv_nth)
  moreover have "u = \<epsilon> \<or> v = \<epsilon> \<Longrightarrow>  u \<and>\<^sub>p v = \<epsilon>"
    using lcp_pref  by auto 
  ultimately show ?thesis using \<open>hd u \<noteq> hd v\<close> by blast
qed   

subsubsection "Relation with prefix comparability"

lemma lcp_ruler: "r \<bowtie> w1 \<Longrightarrow> r \<bowtie> w2 \<Longrightarrow> \<not> w1 \<bowtie> w2 \<Longrightarrow> r \<le>p w1 \<and>\<^sub>p w2"
  by (meson pref_pref_lcp pref_trans ruler)

lemma comp_monotone: "w \<bowtie> r  \<Longrightarrow> u \<le>p w \<Longrightarrow> u \<bowtie> r"
  using pref_trans[of u w r] ruler[of u w r] by blast

lemma comp_monotone': "w \<bowtie> r  \<Longrightarrow> w \<and>\<^sub>p w' \<bowtie> r"
  using lcp_pref' comp_monotone by blast

lemma double_ruler: assumes "w \<bowtie> r" and "w' \<bowtie> r'" and "\<not> r \<bowtie> r'" 
  shows "w \<and>\<^sub>p w' \<le>p r \<and>\<^sub>p r'"
  using comp_monotone'[OF \<open>w' \<bowtie> r'\<close>, of w]  unfolding lcp_sym[of w' w]
  using lcp_ruler[OF comp_monotone'[OF \<open>w \<bowtie> r\<close>, of w'] _ \<open>\<not> r \<bowtie> r'\<close>] by blast

lemma pref_comp_ruler: assumes "w \<bowtie> u \<cdot> [x]" and "w \<bowtie> v \<cdot> [y]" and "x \<noteq> y" and "\<^bold>|u\<^bold>| = \<^bold>|v\<^bold>|" 
  shows "w \<le>p u \<and> w \<le>p v"
  using double_ruler[OF \<open>w \<bowtie> u \<cdot> [x]\<close> \<open>w \<bowtie> v \<cdot> [y]\<close> mismatch_incopm[OF \<open>\<^bold>|u\<^bold>| = \<^bold>|v\<^bold>|\<close> \<open>x \<noteq> y\<close>]] unfolding lcp_self[of w] lcp_mismatch_shorter[OF \<open>\<^bold>|u\<^bold>| = \<^bold>|v\<^bold>|\<close> \<open>x \<noteq> y\<close>]
  using pref_lcp_pref pref_lcp_pref' by blast

lemma rev_sing: "rev [x] = [x]"
  by simp

lemma suf_comp_ruler: assumes "w \<bowtie>\<^sub>s [x] \<cdot> u" and "w \<bowtie>\<^sub>s [y] \<cdot> v" and "x \<noteq> y" and "\<^bold>|u\<^bold>| = \<^bold>|v\<^bold>|"
  shows "w \<le>s u \<and> w \<le>s v"
proof-
  have f1: "rev w \<bowtie> rev u \<cdot> [x]"
    using  pref_suf_rev_comp3[OF \<open>w \<bowtie>\<^sub>s [x] \<cdot> u\<close>] unfolding rev_append[of "[x]" u] rev_sing[of x]. 
  have f2: "rev w \<bowtie> rev v \<cdot> [y]"
    using  pref_suf_rev_comp3[OF \<open>w \<bowtie>\<^sub>s [y] \<cdot> v\<close>] unfolding rev_append[of "[y]" v] rev_sing[of y]. 
  have f3: "\<^bold>|rev u\<^bold>| =  \<^bold>|rev v\<^bold>|"
    using \<open>\<^bold>|u\<^bold>| = \<^bold>|v\<^bold>|\<close> length_rev by simp
  show ?thesis
    using pref_comp_ruler[OF f1 f2 \<open>x \<noteq> y\<close> f3] pref_rev_suf' by blast
qed

subsection "Factor and factor properties"

lemma fac_pref: "u \<le>f v \<equiv> \<exists> p. p\<cdot>u \<le>p v"
  by simp

lemma fac_suf: "u \<le>f v \<Longrightarrow> \<exists> s. u \<cdot> s \<le>s v"
  by auto

lemma fac_suf': "u \<cdot> s \<le>s v \<Longrightarrow> u \<le>f v"
  by auto

lemma fac_pref_suf: "u \<le>f v \<Longrightarrow> \<exists> p. p \<le>p v \<and> u \<le>s p"
  by (meson fac_pref sufI)

lemma fac_pref_suf': "r \<le>p v \<and> u \<le>s r \<Longrightarrow> u \<le>f v"
  using fac_pref sufE by blast 

subsection "Various lemmas on lists"

lemma cancel: "u\<cdot>v = u\<cdot>w \<Longrightarrow> v = w"
  by simp

lemma cancel_right: "v\<cdot>u = w\<cdot>u \<Longrightarrow> v = w"
  by simp

lemma bij_lists: "bij_betw f X Y \<Longrightarrow> bij_betw (map f) (lists X) (lists Y)"
proof-
  assume "bij_betw f X Y"
  hence "inj_on f X"
    by (simp add: bij_betw_def)
  have "\<And> x y. x \<in> lists X \<Longrightarrow> y \<in> lists X \<Longrightarrow> (set x \<union> set y) \<subseteq> X"
    by blast 
  hence "\<And> x y. x \<in> lists X \<Longrightarrow> y \<in> lists X \<Longrightarrow> inj_on f (set x \<union> set y)"
    by (meson \<open>inj_on f X\<close> subset_inj_on)
  hence "\<And> x y. x \<in> lists X \<Longrightarrow> y \<in> lists X \<Longrightarrow> map f x = map f y \<longleftrightarrow> x  = y" 
    by (simp add: inj_on_map_eq_map)
  hence "inj_on (map f) (lists X)"
    by (simp add: inj_on_def) 
  thus ?thesis using  \<open>bij_betw f X Y\<close> bij_betw_def lists_image
    by metis
qed

lemma emp_concat_emp: "us \<in> lists S\<^sub>+ \<Longrightarrow> concat us = \<epsilon> \<Longrightarrow> us = \<epsilon>"
  using DiffD2 by auto

lemma concat_sing:  "s = [hd s] \<Longrightarrow> concat s = hd s"
  using append.right_neutral concat.simps(1) concat.simps(2)[of "hd s" \<epsilon>] by auto

lemma concat_sing_pow: "concat ([a]\<^sup>@k) = a\<^sup>@k"
  by (induct k, simp, simp)

lemma concat_len_one: assumes "\<^bold>|us\<^bold>| = 1" shows "concat us = hd us"
  using concat_sing[OF sing_word[OF \<open>\<^bold>|us\<^bold>| = 1\<close>]].   

lemma overlap: "p\<cdot>x = x\<cdot>s \<Longrightarrow> \<^bold>|p\<^bold>| \<le> \<^bold>|x\<^bold>| \<Longrightarrow> (p\<inverse>\<^sup>> x) \<le>p x \<and> (p\<inverse>\<^sup>> x) \<le>s x"
  using eqd_pref[of p x x s] prefI[of x "(p\<inverse>\<^sup>> x)" s] sufI[of x p "(p\<inverse>\<^sup>> x)" ] by auto

lemma hd_word: "a#ws = [a] \<cdot> ws"
  by simp

lemma hd_word': "w \<noteq> \<epsilon> \<Longrightarrow> w = [hd w] \<cdot> tl w"
  by simp

lemma hd_pref: "w \<noteq> \<epsilon> \<Longrightarrow> [hd w] \<le>p w"
  using hd_word' by blast

lemma hd_pref': "w \<noteq> \<epsilon> \<Longrightarrow> [w!0] \<le>p w"
  using add_nth by fastforce

lemma unique_letter_word: "(\<forall> c. c \<in> set w \<longrightarrow> c = a) \<Longrightarrow> \<exists> k. w = [a]\<^sup>@k"
proof (induct w)
  case Nil
  then show ?case
    by (metis power_zero) 
next
  case (Cons b w) 
  then show ?case  
  proof-
    obtain k where "w = [a]\<^sup>@k" using Cons.hyps Cons.prems by auto 
    hence "b#w = [a]\<^sup>@Suc k"
      by (simp add: \<open>w = (a # \<epsilon>)\<^sup>@k\<close> Cons.prems) 
    thus ?thesis by blast 
  qed
qed

lemma sub_lists_mono: "A \<subseteq> B \<Longrightarrow> x \<in> lists A \<Longrightarrow> x \<in> lists B"
  by auto

lemma lists_hd: "us \<in>n lists Q \<Longrightarrow> hd us \<in> Q"
  by fastforce

lemma replicate_in_lists: "replicate k z \<in> lists {z}"
  by (induction k) auto

lemma tl_lists: "us \<in> lists A \<Longrightarrow> tl us \<in> lists A"
  using list.sel(2) list.sel(3) lists.cases[of us A "tl us \<in> lists A"] by auto

subsubsection "Lemmas on empty lists/words in lists"

lemma del_empty_concat: "concat us = concat (filter (\<lambda>x. x \<noteq> \<epsilon>) us)"
  by (induct us) simp+

lemmas concat_morph = concat_append

lemma lists_drop_emp: "us \<in> lists C\<^sub>+ \<Longrightarrow> us \<in> lists C"
  by blast

lemma lists_drop_emp': "us \<in> lists C \<Longrightarrow> (filter (\<lambda>x. x \<noteq> \<epsilon>) us) \<in> lists C\<^sub>+"
  by (simp add: in_lists_conv_set)

subsection "Powers and their properties"

lemma power_is_concat_replicate: "u\<^sup>@n = concat (replicate n u) "
  by (induct n) auto

text \<open>More lemmas on powers\<close>

lemma power_slide: "u \<cdot> (v \<cdot> u)\<^sup>@n  \<cdot> v = (u \<cdot> v)\<^sup>@(Suc n)"
  by (induct n) simp+

lemma pop_power_one:  "m \<noteq> 0 \<Longrightarrow> r\<^sup>@m = r \<cdot> r\<^sup>@(m-1)"
  by (simp add: power_eq_if_list)

lemma pop_power: "m \<le> k \<Longrightarrow> u\<^sup>@k = u\<^sup>@m \<cdot> u\<^sup>@(k-m)"
  using le_add_diff_inverse power_add_list  by metis 

lemma pop_power_cancel: "u\<^sup>@k \<cdot> v = u\<^sup>@m \<cdot> w \<Longrightarrow> m \<le> k \<Longrightarrow> u\<^sup>@(k-m) \<cdot> v = w" 
  using pop_power cancel[of "u\<^sup>@m" "u\<^sup>@(k-m) \<cdot> v" w]
  by (metis append_assoc)

lemma powers_comm: "t\<^sup>@k \<cdot> t\<^sup>@m = t\<^sup>@m \<cdot> t\<^sup>@k"
  by (metis add.commute power_add_list) 

lemma comm_add_exp: "r \<cdot> u = u \<cdot> r \<Longrightarrow> r\<^sup>@m \<cdot> u = u \<cdot> r\<^sup>@m"
  by (induct m) auto

lemma comm_add_exps: "r \<cdot> u = u \<cdot> r \<Longrightarrow> r\<^sup>@m \<cdot> u\<^sup>@k = u\<^sup>@k \<cdot> r\<^sup>@m"
  by (metis comm_add_exp)

lemma  powers_pref: "\<lbrakk> t \<noteq> \<epsilon>;  m \<noteq> 0;  m \<le> k \<rbrakk> \<Longrightarrow> t\<^sup>@m \<le>np t\<^sup>@k"
  using power_add_list[of t m "k-m"]
  by (metis append_is_Nil_conv nemp_prefI pop_power power_eq_if_list)

lemma rev_power: "rev (x\<^sup>@m) = (rev x)\<^sup>@m"
proof (induct m, simp)
  case (Suc m)
  then show ?case
    by (simp add: comm_add_exp)
qed 

lemmas add_one_exp = power_Suc2_list

lemma power_len:  "\<^bold>|u\<^sup>@k\<^bold>| = k * \<^bold>|u\<^bold>|" 
  by (induct k) simp+

lemma eq_powers: "u\<^sup>@k = u\<^sup>@m \<Longrightarrow> u \<noteq> \<epsilon> \<Longrightarrow> k = m"
  using power_len
  by (metis length_0_conv mult_cancel2)

lemma sing_power_empty: "[a]\<^sup>@n = \<epsilon> \<Longrightarrow> n = 0"
  by (simp add: eq_powers)

lemma long_power: "r \<noteq> \<epsilon> \<Longrightarrow> \<^bold>|x\<^bold>|\<le>\<^bold>|r\<^sup>@\<^bold>|x\<^bold>|\<^bold>|"
  using power_len
  by (metis eq_iff le_square length_0_conv linear mult_cancel2 mult_le_mono2 nat_mult_1 nat_mult_1_right)

lemma long_power_ex: "r \<noteq> \<epsilon> \<Longrightarrow> \<exists> n. m \<le> \<^bold>|r\<^sup>@n\<^bold>|"
  by (metis Ex_list_of_length long_power)   

lemma longer_power: "r \<noteq> \<epsilon> \<Longrightarrow> \<^bold>|x\<^bold>| \<le> m  \<Longrightarrow> \<^bold>|x\<^bold>|\<le>\<^bold>|r\<^sup>@m\<^bold>|"
  by (metis Ex_list_of_length long_power order.trans)

lemma pref_power_ext: "x \<le>p r\<^sup>@k \<Longrightarrow> x \<le>p r\<^sup>@Suc k"
  using add_one_exp pref_trans prefix_def by blast

lemma pref_power_root_ext: "x \<le>p r\<^sup>@k \<Longrightarrow> r \<cdot> x \<le>p r\<^sup>@Suc k"
  by simp

lemma pref_power_exps_less: "x \<le>p r\<^sup>@k \<Longrightarrow> \<not> x \<le>p r\<^sup>@l \<Longrightarrow> l < k"
  by (metis leI pop_power pref_trans prefix_def)

lemma pref_exps_power:  "k \<le> l \<Longrightarrow> r\<^sup>@k \<le>p r\<^sup>@l"
  by (meson leD pref_power_exps_less self_pref)

lemma pref_sing_exp: "[a]\<^sup>@m \<le>p [a]\<^sup>@n \<Longrightarrow> m \<le> n"
  by (metis eq_powers le_cases not_Cons_self2 pref_antisym pref_exps_power)

lemma comm_common_power: assumes "r \<cdot> u = u \<cdot> r" shows "r\<^sup>@\<^bold>|u\<^bold>| = u\<^sup>@\<^bold>|r\<^bold>|"
  using mult.commute[of "\<^bold>|u\<^bold>|" "\<^bold>|r\<^bold>|"] power_len[of r "\<^bold>|u\<^bold>|"] power_len[of u "\<^bold>|r\<^bold>|"]
    eqd_equal[OF _  comm_add_exps[OF assms]] by auto

lemma one_generated_list_power: "u \<in> lists {x} \<Longrightarrow> \<exists>k. concat u = x\<^sup>@k"
proof(induction u)
  case Nil
  then show ?case
    by (metis concat.simps(1) power_zero)
next
  case (Cons a u)
  then show ?case
    by (metis Cons_in_lists_iff concat.simps(2) singletonD power_Suc_list) 
qed

lemma power_lists:  "0 < k \<Longrightarrow> u\<^sup>@k \<in> lists B\<^sub>+ \<Longrightarrow> u \<in> lists B\<^sub>+"
  by (simp add: power_eq_if_list)

lemma concat_morph_power: "xs \<in> lists B \<Longrightarrow> xs = ts\<^sup>@k \<Longrightarrow> concat ts\<^sup>@k = concat xs"
  by (induct k arbitrary: xs ts) simp+

lemma pref_not_idem:  "z \<noteq> \<epsilon> \<Longrightarrow> z \<noteq> x \<Longrightarrow> z \<cdot> x\<^sup>@k \<noteq> x"
  by (metis append_self_conv2  power_eq_if_list prefI pref_antisym pref_prod_shorter1 self_append_conv self_pref)

lemma per_exp_pref: "u \<le>p r \<cdot> u \<Longrightarrow> u \<le>p r\<^sup>@k \<cdot> u"
proof(induct k)
  case (Suc k)
  then show ?case
    by (metis add_one_exp pref_prolong_comp)
qed simp 

lemma per_exp_suf: "z \<le>s z \<cdot> r \<Longrightarrow> z \<le>s z \<cdot> r\<^sup>@j"
  by (metis per_exp_pref pref_rev_suf' rev_append rev_power suf_rev_pref)

lemma hd_sing_power: "k \<noteq> 0 \<Longrightarrow> hd ([a]\<^sup>@k) = a"
  by (induction k) simp+

lemma root_pref_cancel: assumes "t\<^sup>@m \<cdot> y = t\<^sup>@k" shows "y = t\<^sup>@(k - m)"
  using lqI[of "t\<^sup>@k" "t\<^sup>@m" "t\<^sup>@(k-m)"]  unfolding lqI[OF sym[OF \<open>t\<^sup>@m \<cdot> y = t\<^sup>@k\<close>]]
  using  nat_le_linear[of m k] pop_power[of m k t] diff_is_0_eq[of k m]   append.right_neutral[of "t\<^sup>@k"] power_zero[of t] 
    pref_antisym[of "t\<^sup>@m" "t\<^sup>@k", OF prefI[OF sym[OF \<open>t\<^sup>@m \<cdot> y = t\<^sup>@k\<close>]] pref_exps_power[of k m t]] 
  by presburger

subsection "Total morphisms"

locale  morphism =
  fixes f
  assumes morph: "f (u \<cdot> v) = f u \<cdot> f v"
begin
lemma empty_to_empty: "f \<epsilon> = \<epsilon>"
  by  (metis morph self_append_conv2)

lemma power_morph: "f (x\<^sup>@k) = (f x)\<^sup>@k"
  by (induction k) (simp add: morph empty_to_empty)+

lemma pop_head: "f (a#u) = f [a] \<cdot> f u"
  by (metis hd_word morph)

lemma pref_mono: "u \<le>p v \<Longrightarrow> f u \<le>p f v"
  using morph by auto

lemma morph_concat_map: "f x = concat (map (\<lambda> x. f [x]) x)"
proof (induction x, simp add: empty_to_empty)
  case (Cons a x)
  then show ?case 
    unfolding pop_head[of a x] by auto 
qed 

end 

lemma morph_compose: "morphism f \<Longrightarrow> morphism g \<Longrightarrow> morphism (f \<circ> g)"
  by (simp add: morphism_def)

subsection "Arithmetical hints"

lemma zero_diff_eq: "i \<le> j \<Longrightarrow>(0::nat) = j - i  \<Longrightarrow> j = i"
  by simp

lemma nat_prod_le: "n \<noteq> (0 :: nat) \<Longrightarrow> m \<noteq> 0 \<Longrightarrow> m*n \<le> k \<Longrightarrow> n \<le> k"
  using le_trans[of n "m*n" k]  by simp

subsection "Conjugation"

lemma conjug_power: "x \<cdot> z = z \<cdot> y \<Longrightarrow> x\<^sup>@k \<cdot> z = z \<cdot> y\<^sup>@k"
  by (induct k) fastforce+

lemma conjug_rq: "x \<cdot> z = z \<cdot> y \<Longrightarrow> x = z \<cdot> y \<^sup><\<inverse>z"
  using rqI by metis

lemma conjug_lq: "x \<cdot> z = z \<cdot> y \<Longrightarrow> y = z\<inverse>\<^sup>> x \<cdot> z"
  by simp

lemma lq_conjug: "z \<le>p x \<cdot> z \<Longrightarrow>  y = z\<inverse>\<^sup>> x \<cdot> z \<Longrightarrow> x \<cdot> z = z \<cdot> y"
  by auto

lemma rq_conjug: "z \<le>s z \<cdot> y \<Longrightarrow>  x = z \<cdot> y \<^sup><\<inverse>z \<Longrightarrow> x \<cdot> z = z \<cdot> y"
  using rq_suf by blast

lemma lq_conjug_power: "p \<le>p x \<cdot> p \<Longrightarrow> p\<inverse>\<^sup>> x\<^sup>@k \<cdot> p = (p\<inverse>\<^sup>> x \<cdot> p)\<^sup>@k"
  using conjug_power[of x p  "p\<inverse>\<^sup>> x \<cdot> p"] lqI lq_conjug by metis

lemma rq_conjug_power: "p \<le>s  p \<cdot> x \<Longrightarrow> p \<cdot> x\<^sup>@k \<^sup><\<inverse>p = (p \<cdot> x \<^sup><\<inverse>p)\<^sup>@k"
  using conjug_power[of   "p \<cdot> x \<^sup><\<inverse>p" p x]  by (metis rqI rq_suf)

lemma conjug_empty_pref: "p \<le>s p \<cdot> u \<Longrightarrow> p \<cdot> u \<^sup><\<inverse>p = \<epsilon> \<Longrightarrow> u = \<epsilon>"
  by (metis append_self_conv append_self_conv2 rq_suf)

lemma conjug_empty_suf: "p \<le>p u \<cdot> p \<Longrightarrow> p\<inverse>\<^sup>> u \<cdot> p = \<epsilon> \<Longrightarrow> u = \<epsilon>"
  using lq_ne by blast 

lemma lq_rq_conj: "p \<le>p r\<cdot>p \<Longrightarrow>  r = (p\<cdot>(p\<inverse>\<^sup>> r \<cdot> p))\<^sup><\<inverse>p"
  by (metis lq_pref rqI)

lemma rq_lq_conjugate: "p \<le>s p\<cdot>r \<Longrightarrow> r = p\<inverse>\<^sup>>(((p \<cdot> r) \<^sup><\<inverse>p )\<cdot>p)"
  by (metis lqI rq_suf)

section \<open>Root\<close>

definition root :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<in> _*" [51,51] 60 )
  where  "x \<in> r* =  (\<exists> k. x = r\<^sup>@k)"

text\<open>Root can be empty, and the empty word has all roots.\<close>

lemma empty_all_roots: "\<epsilon> \<in> r*"
  by (metis root_def power_zero) 

lemma take_root: "k \<noteq> 0 \<Longrightarrow> r = take (length r) (r\<^sup>@k)"
  by (simp add: power_eq_if_list)

lemma root_nemp: "u \<noteq> \<epsilon> \<Longrightarrow> u \<in> r* \<Longrightarrow> r \<noteq> \<epsilon>"
  unfolding root_def using emp_power by auto 

lemma root_shorter: "u \<noteq> \<epsilon> \<Longrightarrow> u \<in> r* \<Longrightarrow> u \<noteq> r \<Longrightarrow> \<^bold>|r\<^bold>| < \<^bold>|u\<^bold>|"
  by (metis root_def leI take_all take_root power_zero)

lemma root_trans[trans]: "\<lbrakk>v \<in> u*; u \<in> t*\<rbrakk> \<Longrightarrow> v \<in> t*"
  by (metis root_def power_mult_list)

lemma root_len: "u \<in> q* \<Longrightarrow> \<exists>k. \<^bold>|u\<^bold>| = k*\<^bold>|q\<^bold>|"
  unfolding root_def using power_len by auto

lemma root_len_dvd: "u \<in> t* \<Longrightarrow> \<^bold>|t\<^bold>| dvd \<^bold>|u\<^bold>|"
  using root_len root_def by fastforce 

lemma common_root_len_gcd: "u \<in> t* \<Longrightarrow> v \<in> t* \<Longrightarrow> \<^bold>|t\<^bold>| dvd ( gcd \<^bold>|u\<^bold>| \<^bold>|v\<^bold>| )"
  by (simp add: root_len_dvd)

lemma add_root: "w \<in> z* \<Longrightarrow> z \<cdot> w \<in> z*"
  using root_def by (metis power_Suc_list ) 

lemma add_roots: "w \<in> z* \<Longrightarrow> w' \<in> z* \<Longrightarrow> w \<cdot> w' \<in> z*"
  using root_def by (metis power_add_list) 

lemma concat_sing_list: "ws \<in> lists {z} \<Longrightarrow> concat ws \<in> z*"
proof (induct ws)
  case Nil  then show ?case  using empty_all_roots by auto 
next 
  case (Cons a ws) then show ?case  using add_root by auto 
qed

lemma root_pref_cancel': "\<lbrakk> x\<cdot>y \<in> t* ; x \<in> t* \<rbrakk> \<Longrightarrow> y \<in> t*" 
  unfolding root_def using root_pref_cancel by fastforce

section Commutation

text\<open>The solution of the easiest nontrivial word equation, @{term "x \<cdot> y = y \<cdot> x"}, is in fact already contained in List.thy as the fact @{thm comm_append_are_replicate}.\<close>

theorem comm:  "x \<cdot> y = y \<cdot> x   \<Longrightarrow>  \<exists> t m k. x = t\<^sup>@k \<and> y = t\<^sup>@m"
  using  comm_append_are_replicate[of x y] power_is_concat_replicate power_zero power_one_id
  by metis

theorem comm_root0:  "x \<cdot> y = y \<cdot> x \<Longrightarrow> \<exists> t. x \<in> t* \<and> y \<in> t*"
  unfolding root_def using comm by auto

theorem comm_root1:  "(\<exists> t. (x \<in> t*) \<and> (y \<in> t*)) \<Longrightarrow> x \<cdot> y = y \<cdot> x"
  unfolding root_def using powers_comm by auto

corollary comm_root:  "x \<cdot> y = y \<cdot> x   \<longleftrightarrow>  (\<exists> t. x \<in> t* \<and> y \<in> t*)"
  using comm_root0 comm_root1 by blast

section \<open>Periods\<close>

subsection "Period root"

definition period_root :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<le>p _\<^sup>\<omega>" [51,51] 60 )
  where period_root_def[simp]: "period_root x r = (x \<le>p r \<cdot> x \<and> r \<noteq> \<epsilon>)"

lemma per_rootI[simp,intro]: "x \<le>p r \<cdot> x \<Longrightarrow> r \<noteq> \<epsilon> \<Longrightarrow> x \<le>p r\<^sup>\<omega>"
  by simp

text \<open>Empty word has no period, and is not a periodic root.\<close>

lemma emp_any_per: "r \<noteq> \<epsilon> \<Longrightarrow> (\<epsilon> \<le>p r\<^sup>\<omega> )"
  by simp

lemma emp_not_per: "\<not> (x \<le>p \<epsilon>\<^sup>\<omega>)"
  by simp 

text \<open>Any nonempty word is its own periodic root.\<close>

lemma root_self: "w \<noteq> \<epsilon> \<Longrightarrow> w \<le>p (take (length w) w)\<^sup>\<omega>"
  by simp

text\<open>"Short roots are prefixes"\<close>

lemma root_is_take: "length r \<le> length w \<Longrightarrow>  w \<le>p r\<^sup>\<omega> \<Longrightarrow> r = take (length r) w"
  by (simp add: append_eq_conv_conj)

text\<open>An important equivalent characterization of a periodic root, which motivates the notation.\<close>

lemma per_exp: "u \<le>p r\<^sup>\<omega> \<Longrightarrow> u \<le>p r\<^sup>@k \<cdot> u"
proof(induct k)
  case (Suc k)
  then show ?case
    by (meson per_exp_pref period_root_def)
qed simp 

lemma per_add_exp: "\<lbrakk> u \<le>p r\<^sup>\<omega>; m \<noteq> 0 \<rbrakk> \<Longrightarrow> u \<le>p (r\<^sup>@m)\<^sup>\<omega>"
  by (metis eq_powers per_exp_pref period_root_def power_zero)

lemma per_pref_ex: "x \<le>p r\<^sup>\<omega> \<Longrightarrow> \<exists> n. x \<le>p r\<^sup>@Suc n"
  using long_power_ex[of r "\<^bold>|x\<^bold>|"] per_exp
  by (metis emp_not_per prefI pref_comp_len pref_power_ext ruler)

theorem per_pref: "x \<le>p r\<^sup>\<omega> \<longleftrightarrow> (r \<noteq> \<epsilon> \<and> (\<exists> k. x \<le>p r\<^sup>@k))"
  by (metis per_pref_ex period_root_def power_Suc_list pref_power_ext pref_prod_shorter2)

lemma per_eq: "x \<le>p r\<^sup>\<omega> \<longleftrightarrow> (r \<noteq> \<epsilon> \<and> (\<exists> k z. x = r\<^sup>@k\<cdot>z \<and> z \<le>p r ))"
proof
  show "x \<le>p r\<^sup>\<omega> \<Longrightarrow>r \<noteq> \<epsilon> \<and> (\<exists> k z. x = r\<^sup>@k\<cdot>z \<and> z \<le>p r )" using pref_power_eq
    by (metis period_root_def per_pref)
  show "r \<noteq> \<epsilon> \<and> (\<exists>k z. x = r\<^sup>@k \<cdot> z \<and> z \<le>p r) \<Longrightarrow> x \<le>p r\<^sup>\<omega>"
    by (metis add_one_exp append_assoc per_pref prefix_def)
qed

text\<open>The previous theorem allows to prove some basic relations between powers, periods and commutation\<close>

lemma per_drop_exp: "u \<le>p (r\<^sup>@m)\<^sup>\<omega>  \<Longrightarrow> u \<le>p r\<^sup>\<omega>" 
  using per_pref power_mult_list
  by (metis length_0_conv mult_0_right power_len)

lemma per_drop_exp': "i \<noteq> 0 \<Longrightarrow> p \<le>p e\<^sup>@i \<cdot> p \<Longrightarrow>  p \<le>p  e \<cdot> p"
  by (metis period_root_def eq_powers per_drop_exp power_zero) 

lemma per_drop_exp_rev: "i \<noteq> 0 \<Longrightarrow> p \<le>s p \<cdot> e\<^sup>@i \<Longrightarrow>  p \<le>s p \<cdot> e"
  using per_drop_exp' [of i "rev p" "rev e"] rev_power
  by (metis pref_rev_suf' rev_append suf_rev_pref)

corollary comm_drop_exp: "\<lbrakk> m \<noteq> 0; r\<^sup>@m \<cdot> u = u \<cdot> r\<^sup>@m \<rbrakk> \<Longrightarrow> r \<cdot> u = u \<cdot> r"
proof-
  assume "m \<noteq> 0" "r\<^sup>@m \<cdot> u = u \<cdot> r\<^sup>@m"
  { assume "r \<noteq> \<epsilon>" "u \<noteq> \<epsilon>"
    hence "u\<cdot>r \<le>p u\<cdot>r\<^sup>@m" using pop_power_one \<open>m \<noteq> 0\<close>
      by auto
    hence "u\<cdot>r \<le>p r\<^sup>@m\<cdot>(u\<cdot>r)" using \<open>r\<^sup>@m \<cdot> u = u \<cdot> r\<^sup>@m\<close>
      by (metis append_assoc prefix_def)
    hence "u\<cdot>r \<le>p r\<cdot>(u\<cdot>r)" using per_drop_exp[of "u\<cdot>r" r m]
      using \<open>r \<noteq> \<epsilon>\<close> \<open>u \<cdot> r \<le>p u \<cdot> r\<^sup>@m\<close> by auto
    hence "r \<cdot> u = u \<cdot> r"
      using pref_comm_product by fastforce
  }
  thus "r \<cdot> u = u \<cdot> r"
    by fastforce 
qed

corollary powers_comm_comm: "\<lbrakk>x\<^sup>@j = y\<^sup>@k; j \<noteq> 0\<rbrakk> \<Longrightarrow> x\<cdot>y = y\<cdot>x"
  by (metis append_Nil append_Nil2 comm_drop_exp power_zero)

corollary comm_powers_roots: "\<lbrakk> m \<noteq> 0; k \<noteq> 0 \<rbrakk> \<Longrightarrow> u \<cdot> v = v \<cdot> u  \<longleftrightarrow> u\<^sup>@m \<cdot> v\<^sup>@k = v\<^sup>@k \<cdot> u\<^sup>@m"
  using comm_drop_exp comm_add_exp
  by metis 

theorem per_all_exps: "\<lbrakk> m \<noteq> 0; k \<noteq> 0 \<rbrakk> \<Longrightarrow> (u \<le>p (r\<^sup>@m)\<^sup>\<omega>) \<longleftrightarrow> (u \<le>p (r\<^sup>@k)\<^sup>\<omega>)"
  using per_add_exp per_drop_exp by blast

text\<open>Another equivalent characterization of "short" periods.\<close>

theorem per_shift: "\<lbrakk> n  < length w; n \<noteq> 0 \<rbrakk> \<Longrightarrow> w \<le>p (take n w)\<^sup>\<omega> \<longleftrightarrow> drop n w \<le>p w"
proof
  show "\<lbrakk> n  < length w; n \<noteq> 0 \<rbrakk> \<Longrightarrow> w \<le>p (take n w)\<^sup>\<omega> \<Longrightarrow> drop n w \<le>p w"
    using pref_drop[of n w "take n w \<cdot> w"] period_root_def[of w "take n w"]
    by (metis append_take_drop_id pref_cancel)
  have aux:"n < length w \<Longrightarrow>  n \<noteq> 0 \<Longrightarrow> take n w \<noteq> \<epsilon>"
    by auto 
  have "n < length w \<Longrightarrow>  n \<noteq> 0 \<Longrightarrow> drop n w \<le>p w \<Longrightarrow> w \<le>p take n w \<cdot> w"
    by (metis append_take_drop_id pref_ext) 
  thus "n < length w \<Longrightarrow>  n \<noteq> 0 \<Longrightarrow>  drop n w \<le>p w \<Longrightarrow>  w \<le>p (take n w)\<^sup>\<omega>"
    using  period_root_def[of w "take n w"] aux
    by blast
qed

text\<open>Some auxiliary lemmas\<close>

lemma take_per: "\<lbrakk> length r < length w; w \<le>p r\<^sup>\<omega>\<rbrakk> \<Longrightarrow> r = take (length r) w"
  by (simp add: append_eq_conv_conj)  

lemma drop_per: 
  assumes "p < \<^bold>|w\<^bold>|" "w \<le>p (take p w)\<^sup>\<omega>"
  shows "(drop p w) \<le>p (take p w)\<^sup>\<omega>"
  by (metis period_root_def append_take_drop_id \<open>w \<le>p (take p w)\<^sup>\<omega>\<close> pref_cancel)

lemma drop_per_pref: "w \<le>p u\<^sup>\<omega> \<Longrightarrow> drop \<^bold>|u\<^bold>| w \<le>p w"
  by (metis period_root_def append_eq_conv_conj drop_append prefix_def) 

lemma drop_per': 
  assumes as: "length r < length w" "w \<le>p r\<^sup>\<omega>"
  shows "(drop (length r) w) \<le>p r\<^sup>\<omega>"
  using drop_per take_per as
  by metis 

lemma per_root_trans: "w \<le>p u\<^sup>\<omega> \<Longrightarrow> u \<in> t* \<Longrightarrow> w \<le>p t\<^sup>\<omega>"
  by (metis root_def per_drop_exp)

text\<open>Note that 
@{term "w \<le>p u\<^sup>\<omega> \<Longrightarrow> u \<le>p t\<^sup>\<omega> \<Longrightarrow> w \<le>p t\<^sup>\<omega>"}
does not hold.
\<close>

lemma per_root_same_prefix:"w \<le>p r\<^sup>\<omega> \<Longrightarrow> w' \<le>p r\<^sup>\<omega> \<Longrightarrow>  w \<le>p w' \<or> w' \<le>p w"
  by (meson per_exp per_pref pref_trans prefix_def ruler)

lemma take_after_drop:  "\<^bold>|u\<^bold>| + q \<le> \<^bold>|w\<^bold>| \<Longrightarrow> w \<le>p u\<^sup>\<omega> \<Longrightarrow> take q (drop \<^bold>|u\<^bold>| w) = take q w"
  using pref_share_take[OF drop_per_pref[of w u] len_after_drop[of "\<^bold>|u\<^bold>|" q w]].

lemma two_pers: assumes "w \<le>p u\<^sup>\<omega>" "w \<le>p v\<^sup>\<omega>" "\<^bold>|u\<^bold>|+\<^bold>|v\<^bold>| \<le> \<^bold>|w\<^bold>|" shows "u\<cdot>v = v\<cdot>u" 
proof- 
  have t1: "take \<^bold>|u\<^bold>| w = u" 
    using root_is_take \<open>w \<le>p u\<^sup>\<omega>\<close> \<open>\<^bold>|u\<^bold>|+\<^bold>|v\<^bold>| \<le> \<^bold>|w\<^bold>|\<close>
    by (metis add_leD1) 
  have t2: "take \<^bold>|v\<^bold>| w = v" 
    using root_is_take \<open>w \<le>p v\<^sup>\<omega>\<close> \<open>\<^bold>|u\<^bold>|+\<^bold>|v\<^bold>| \<le> \<^bold>|w\<^bold>|\<close>
    by (metis add_leD1 add.commute)
  have t3: "take \<^bold>|v\<^bold>| (drop \<^bold>|u\<^bold>| w) = v"
    using take_after_drop[OF  \<open>\<^bold>|u\<^bold>|+\<^bold>|v\<^bold>| \<le> \<^bold>|w\<^bold>|\<close> \<open>w \<le>p u\<^sup>\<omega>\<close>] unfolding t2.
  have t4: "take \<^bold>|u\<^bold>| (drop \<^bold>|v\<^bold>| w) = u"
    using take_after_drop[OF  _ \<open>w \<le>p v\<^sup>\<omega>\<close>, of "\<^bold>|u\<^bold>|"]  \<open>\<^bold>|u\<^bold>|+\<^bold>|v\<^bold>| \<le> \<^bold>|w\<^bold>|\<close> unfolding t1 by simp
  show ?thesis 
    using take_add[of "\<^bold>|u\<^bold>|" "\<^bold>|v\<^bold>|" w] take_add[of "\<^bold>|v\<^bold>|" "\<^bold>|u\<^bold>|" w] 
    unfolding t1 t2 t3 t4 add.commute[of "\<^bold>|v\<^bold>|" "\<^bold>|u\<^bold>|"] by auto
qed

lemma "x \<noteq> \<epsilon> \<Longrightarrow> x\<cdot>z = z\<cdot>y \<Longrightarrow> z \<le>p x\<^sup>\<omega>"
  by blast

lemma "z \<le>p x\<^sup>\<omega> \<Longrightarrow> \<exists>y. x\<cdot>z = z\<cdot>y"
  by simp

subsection "Period - numeric"

text\<open>Numeric definition of a period\<close>

definition periodN :: "'a list \<Rightarrow> nat \<Rightarrow> bool" 
  where periodN_def[simp]: "periodN w n =  w \<le>p (take n w)\<^sup>\<omega>"

text\<open>The numeric definition respects the following convention about empty words and empty periods.\<close>

lemma emp_no_periodN: "\<not> periodN \<epsilon> n"
  by simp

lemma zero_not_per: "\<not> periodN w 0"
  by simp

text\<open>A nonempty word has all "long" periods\<close>

lemma all_long_pers: "\<lbrakk> w \<noteq> \<epsilon>; length w \<le> n \<rbrakk> \<Longrightarrow> periodN w n"
  by simp

lemma per_nemp: "periodN w n \<Longrightarrow> w \<noteq> \<epsilon>"
  using emp_no_periodN by blast

lemma per_positive: "periodN w n \<Longrightarrow> n \<noteq> 0"
  by (meson zero_not_per)

text\<open>The numeric definition is equivalent to the definition by a root for all "short" roots.\<close>

lemma periodN_is_root: " w \<noteq> \<epsilon> \<Longrightarrow> periodN w n \<longleftrightarrow> (w \<le>p (take n w)\<^sup>\<omega>)"
  using root_self by force 

theorem periodN_pref: assumes "w \<noteq> \<epsilon>" shows "periodN w n \<longleftrightarrow> (\<exists>k r. w \<le>np r\<^sup>@k \<and> \<^bold>|r\<^bold>| = n)"
proof
  assume "periodN w n"
  consider (short) "\<^bold>|w\<^bold>| \<le> n" |  (long) "n < \<^bold>|w\<^bold>|"
    by linarith
  then show "(\<exists>k r. w \<le>np r\<^sup>@k \<and> \<^bold>|r\<^bold>| = n)"
  proof(cases)
    case short
    then show ?thesis 
    proof- 
      obtain z where "\<^bold>|w \<cdot> z\<^bold>| = n" 
        using Ex_list_of_length[of "n - \<^bold>|w\<^bold>|"] length_append
        by (metis add_diff_inverse_nat not_le short)
      thus ?thesis
        using assms power_one_id
        by blast
    qed
  next
    case long
    then show ?thesis 
      using \<open>periodN w n\<close> per_pref[of w "take n w"]
      by (meson assms leD nat_le_linear nemp_prefI_pref periodN_def take_len)
  qed
next 
  show "\<exists>k r. w \<le>np r\<^sup>@k \<and> \<^bold>|r\<^bold>| = n \<Longrightarrow> periodN w n"
    using \<open>w \<noteq> \<epsilon>\<close> periodN_def per_pref
    by (metis emp_power nonempty_prefix_def power_Suc_list pref_len pref_power_ext pref_take_len root_self ruler_comp self_pref take_all)
qed

lemma take_several_pers: assumes "periodN w n" and "m*n \<le> \<^bold>|w\<^bold>|" 
  shows "(take n w)\<^sup>@m = take (m*n) w"
proof-
  {assume "m \<noteq> 0"
    have "n \<noteq> 0"
      using \<open>periodN w n\<close> by auto
    hence "\<^bold>|(take n w)\<^sup>@m\<^bold>| = m*n"
      using  power_len[of "take n w" m] take_len[OF nat_prod_le[OF \<open>n \<noteq> 0\<close> \<open>m \<noteq> 0\<close> \<open>m*n \<le> \<^bold>|w\<^bold>|\<close>]] by metis
    have "(take n w)\<^sup>@m \<le>p w"
      using \<open>periodN w n\<close> unfolding  periodN_def using per_exp[of w "take n w" m] \<open>\<^bold>|take n w\<^sup>@m\<^bold>| = m * n\<close> \<open>m * n \<le> \<^bold>|w\<^bold>|\<close>
        ruler_le[of "take n w\<^sup>@m" "take n w\<^sup>@m \<cdot> w" w, OF triv_pref]
      by linarith
    have ?thesis                                   
      using \<open>\<^bold>|take n w\<^sup>@m\<^bold>| = m * n\<close> pref_take_len[OF \<open>take n w\<^sup>@m \<le>p w\<close>] by metis
  } note nemp = this
  {assume "m = 0"
    hence "take (n*m) w = \<epsilon>" and "(take n w)\<^sup>@m = \<epsilon>"
      by simp+
  }
  thus ?thesis
    using nemp by fastforce
qed

lemma per_mult: "\<lbrakk> periodN w n ; m \<noteq> 0 \<rbrakk> \<Longrightarrow> periodN w (m*n)"
  using take_several_pers
  by (metis all_long_pers emp_no_periodN nat_le_linear periodN_def per_add_exp)

lemma periodN_root: "w \<noteq> \<epsilon>  \<Longrightarrow>  w \<le>p r\<^sup>\<omega> \<Longrightarrow> periodN w \<^bold>|r\<^bold>|"
  by (metis all_long_pers not_less periodN_def take_per)

theorem  two_periodsN:
  assumes "periodN w p" "periodN w q"  "p + q \<le> \<^bold>|w\<^bold>|" 
  shows "periodN w (gcd p q)"
proof-
  obtain t where "t \<noteq> \<epsilon>" "take p w \<in> t*" "take q w \<in> t*" 
    using two_pers[of w "take p w" "take q w"] periodN_def 
      comm_root[of "take p w" "take q w"]
      \<open>periodN w p\<close> \<open>periodN w q\<close> \<open>p + q \<le> \<^bold>|w\<^bold>|\<close> take_len
    by (metis add_leD1 add_leD2 period_root_def root_nemp)
  hence "w \<le>p t\<^sup>\<omega>"
    using \<open>periodN w p\<close> periodN_def per_root_trans by blast
  have "periodN w \<^bold>|t\<^bold>|"
    using \<open>w \<le>p t\<^sup>\<omega>\<close>  periodN_root \<open>periodN w p\<close> per_nemp  by blast 
  have "\<^bold>|t\<^bold>| dvd (gcd p q)"
    using \<open>take p w \<in> t*\<close> \<open>take q w \<in> t*\<close> root_len_dvd
    by (metis add_leD1 add_leD2 \<open>p + q \<le> \<^bold>|w\<^bold>|\<close> take_len gcd_nat.boundedI)
  thus ?thesis 
    using \<open>periodN w \<^bold>|t\<^bold>|\<close> per_mult
    by (metis \<open>periodN w p\<close> dvdE gcd_eq_0_iff mult.commute mult_not_zero)
qed

lemma index_power_mod: "w = r\<^sup>@k \<Longrightarrow> \<forall> i < \<^bold>|w\<^bold>|. w!i = r!(i mod \<^bold>|r\<^bold>| )"
proof(induction k arbitrary:w)
  case 0
  then show ?case
    by auto 
next
  case (Suc k)
  have "w = r\<cdot>r\<^sup>@k"
    by (simp add: Suc.prems power_commutes)
  hence "\<^bold>|r\<^sup>@k\<^bold>|+\<^bold>|r\<^bold>| = \<^bold>|w\<^bold>|"
    by simp
  {
    fix i
    assume "\<^bold>|r\<^bold>| \<le> i" "i < \<^bold>|w\<^bold>|"
    hence q: "w!i  = (r\<^sup>@k)!(i - \<^bold>|r\<^bold>| )"
      by (simp add: \<open>w = r \<cdot> r\<^sup>@k\<close> nth_append)

    have "(r\<^sup>@k)!(i - \<^bold>|r\<^bold>| ) = r!(i mod \<^bold>|r\<^bold>| )"
      by (simp add: Suc.IH \<open>i < \<^bold>|w\<^bold>|\<close> \<open>\<^bold>|r\<^sup>@k\<^bold>| + \<^bold>|r\<^bold>| = \<^bold>|w\<^bold>|\<close> \<open>\<^bold>|r\<^bold>| \<le> i\<close> le_mod_geq less_diff_conv2)
    hence "(w)!i = r!(i mod \<^bold>|r\<^bold>| )" using q
      by metis
  }
  then show ?case
    by (simp add: Suc.prems nth_append)
qed

lemma index_mod_per_root: assumes "r \<noteq> \<epsilon>" and i: "\<forall> i < \<^bold>|w\<^bold>|. w!i = r!(i mod \<^bold>|r\<^bold>|)" shows  "w \<le>p r\<^sup>\<omega>"
proof-
  have "\<^bold>|w\<^bold>| \<le> \<^bold>|r \<cdot> w\<^bold>|"
    by auto
  {fix i assume "i < \<^bold>|w\<^bold>|"
    { assume "\<^bold>|w\<^bold>| \<le> \<^bold>|r\<^bold>|"
      hence "w!i = (r \<cdot> w) ! i"
        by (metis \<open>i < \<^bold>|w\<^bold>|\<close> dual_order.strict_trans1 i mod_less nth_append) 
    } 
    { assume "\<^bold>|r\<^bold>| \<le> \<^bold>|w\<^bold>|"
      hence "w!i = (r \<cdot> w) ! i"
        by (simp add: \<open>i < \<^bold>|w\<^bold>|\<close> i less_imp_diff_less mod_if nth_append)
    }
    hence "w!i = (r \<cdot> w) ! i"
      using \<open>\<^bold>|w\<^bold>| \<le> \<^bold>|r\<^bold>| \<Longrightarrow> w ! i = (r \<cdot> w) ! i\<close> by linarith} 
  thus "w \<le>p r\<^sup>\<omega>"
    using index_pref[OF \<open>\<^bold>|w\<^bold>| \<le> \<^bold>|r \<cdot> w\<^bold>|\<close>] period_root_def \<open>r \<noteq> \<epsilon>\<close> by blast
qed

lemma index_pref_power_mod: "w \<le>p r\<^sup>@k \<Longrightarrow> \<forall> i < \<^bold>|w\<^bold>|. w!i = r!(i mod \<^bold>|r\<^bold>| )"
  by (metis (no_types, hide_lams) add.commute index_power_mod leI length_append less_le_trans not_add_less2 pref_index prefix_def)

lemma index_per_root_mod: "w \<le>p r\<^sup>\<omega> \<Longrightarrow> \<forall> i < \<^bold>|w\<^bold>|. w!i = r!(i mod \<^bold>|r\<^bold>|)"
  using index_pref_power_mod per_pref by metis

lemma per_factor: "y \<noteq> \<epsilon> \<Longrightarrow> v \<noteq> \<epsilon> \<Longrightarrow> u\<cdot>v\<cdot>w = y\<^sup>@k \<Longrightarrow> periodN v \<^bold>|y\<^bold>|" 
proof-
  assume "y\<noteq>\<epsilon>" " u\<cdot>v\<cdot>w=y\<^sup>@k" "v\<noteq>\<epsilon>"
  have "u \<le>p y\<^sup>@k"
    using \<open>u\<cdot>v\<cdot>w=y\<^sup>@k\<close> unfolding append_assoc[of u v w] using prefI[of "y\<^sup>@k" u "v\<cdot>w"]  
    by auto
  hence "v\<cdot>w = u\<inverse>\<^sup>>(y\<^sup>@k)"
    using \<open>u \<cdot> v \<cdot> w = y\<^sup>@k\<close> by auto
  have "u \<le>p y\<^sup>\<omega>"
    using \<open>u \<le>p y\<^sup>@k\<close> \<open>y \<noteq> \<epsilon>\<close> per_pref by blast
  hence "u\<inverse>\<^sup>>y\<^sup>@k\<cdot>u=(u\<inverse>\<^sup>>(y\<cdot>u))\<^sup>@k"
    using lq_conjug_power by auto
  hence "v \<le>p (u\<inverse>\<^sup>>(y\<cdot>u))\<^sup>@k"
    by (metis \<open>u \<cdot> v \<cdot> w = y\<^sup>@k\<close> append.assoc lqI triv_pref)
  have "\<^bold>|u\<inverse>\<^sup>>(y\<cdot>u)\<^bold>| = \<^bold>|y\<^bold>|"
    using period_root_def[of u y] \<open>u \<le>p y\<^sup>\<omega>\<close> lq_pref[of u "y \<cdot> u"] length_append[of y u] length_append[of u "u\<inverse>\<^sup>> y \<cdot> u"]
    by presburger
  thus ?thesis using \<open>v \<le>p (u\<inverse>\<^sup>>(y\<cdot>u))\<^sup>@k\<close>
    using \<open>v \<noteq> \<epsilon>\<close> periodN_pref by blast
qed

lemma root_divisor: "periodN w k \<Longrightarrow> k dvd \<^bold>|w\<^bold>| \<Longrightarrow> w \<in> (take k w)*"
proof-
  assume "periodN w k" "k dvd \<^bold>|w\<^bold>|"
  hence "w = (take k w)\<^sup>@(\<^bold>|w\<^bold>| div k)"
    by (simp add: take_several_pers)
  then show ?thesis
    using root_def by blast
qed

lemma per_pref': "u \<noteq> \<epsilon> \<Longrightarrow> periodN v k \<Longrightarrow> u \<le>p v \<Longrightarrow> periodN u k" 
proof-
  assume "u \<noteq> \<epsilon>" "periodN v k" " u\<le>p v"
  { assume "k \<le> \<^bold>|u\<^bold>|"
    have "take k v = take k u"
      using  pref_share_take[OF \<open>u \<le>p v\<close> \<open>k \<le> \<^bold>|u\<^bold>|\<close>]  by auto
    hence "take k v \<noteq> \<epsilon>"
      using \<open>periodN v k\<close> by auto
    hence "take k u \<noteq> \<epsilon>"
      by (simp add: \<open>take k v = take k u\<close>)
    have "u \<le>p take k u \<cdot> v" 
      using  \<open>periodN v k\<close>  
      unfolding periodN_def period_root_def \<open>take k v = take k u\<close> 
      using pref_trans[OF \<open>u \<le>p v\<close>, of "take k u \<cdot> v"]
      by blast 
    hence "u \<le>p take k u \<cdot> u"
      using \<open>u \<le>p v\<close> pref_prod_shorter2 by blast 
    hence ?thesis
      using \<open>take k u \<noteq> \<epsilon>\<close> periodN_def by blast
  }
  thus ?thesis
    using \<open>u \<noteq> \<epsilon>\<close> all_long_pers nat_le_linear by blast
qed

subsection "Period: overview"
notepad
begin
  fix w r::"'a list" 
  fix n::nat
  assume "w \<noteq> \<epsilon>" "r \<noteq> \<epsilon>" "n > 0"
  have "\<not> w \<le>p \<epsilon>\<^sup>\<omega>"
    by simp
  have "\<not> \<epsilon> \<le>p \<epsilon>\<^sup>\<omega>"
    by simp
  have "\<epsilon> \<le>p r\<^sup>\<omega>"
    by (simp add: \<open>r \<noteq> \<epsilon>\<close>)
  have "\<not> periodN w 0"
    by simp
  have "\<not> periodN \<epsilon> 0"
    by simp
  have "\<not> periodN \<epsilon> n"
    by simp
end

subsection \<open>Singleton\<close>

lemma pref_sing_power: "w \<le>p [a]\<^sup>@m \<Longrightarrow> w \<in> [a]*"
proof(induct w arbitrary: m)
  case Nil
  then show ?case
    using empty_all_roots by auto 
next
  case (Cons x w)
  then show ?case 
  proof-
    have "m \<noteq> 0"
      using power_zero[of "[a]"] \<open>(x # w) \<le>p [a]\<^sup>@m\<close> prefix_def by fastforce
    hence "x = a" 
      using \<open>(x # w) \<le>p [a]\<^sup>@m\<close> hd_word[of x w]  hd_sing_power[OF \<open>m\<noteq>0\<close>, of a]
      by (metis hd_append2 list.discI list.sel(1) prefix_def) 
    hence "w \<le>p [a]\<^sup>@m" using \<open>(x # w) \<le>p [a]\<^sup>@m\<close>
      by (metis hd_word pref_cancel pref_power_ext power_Suc_list )
    thus ?thesis
      using Cons.hyps \<open>x = a\<close> add_root by fastforce
  qed
qed

lemma suf_sing_power: "w \<le>s [a]\<^sup>@m \<Longrightarrow> w \<in> [a]*"
  using pref_sing_power[of "rev w" a m] suf_rev_pref'[of "rev w" "rev [a]\<^sup>@m"]
  by (metis root_def rev_power rev_rev_ident rev_singleton_conv)

lemma sing_factor_power: "w \<in> [a]* \<Longrightarrow> v \<le>f w \<Longrightarrow> v \<in> [a]*"
  by (metis root_def fac_suf prefI pref_sing_power suf_sing_power)

lemma sing_power_factor': "a \<noteq> b \<Longrightarrow> w \<in> [a]* \<Longrightarrow> \<not> ([b] \<le>f w)"
  by (metis (mono_tags, lifting) less_irrefl list.distinct(1) list.inject list.size(4) root_shorter sing_factor_power)

lemma distinct_letter_in: "\<not> w \<in>  [a]* \<Longrightarrow> \<exists> m b. [a]\<^sup>@m \<cdot> [b] \<le>p w \<and> b \<noteq> a"
proof (induct w)
  case Nil
  then show ?case
    using empty_all_roots by auto 
next
  case (Cons x w)
  then show ?case 
  proof-
    {assume "x \<noteq> a" 
      hence ?thesis
        by (metis append_Nil hd_word power_zero prefI)
    } note neq = this
    {assume "x = a" 
      hence "\<not> w \<in> [a]*"
        using Cons.prems add_root by force 
      then obtain m b where "[a]\<^sup>@m \<cdot> [b] \<le>p w" and "b \<noteq> a"
        using Cons.hyps by blast  
      hence "[a]\<^sup>@Suc m \<cdot> [b] \<le>p x#w \<and> b \<noteq> a"
        using \<open>x = a\<close>  by auto 
      hence ?thesis
        by blast  
    } note eq = this
    show ?thesis using eq neq
      by blast   
  qed 
qed

lemma distinct_letter_in': "\<not> w \<in>  [hd w]* \<Longrightarrow> \<exists> m b. [hd w]\<^sup>@m \<cdot> [b] \<le>p w \<and> b \<noteq> hd w \<and> m \<noteq> 0"
  using distinct_letter_in[of w "hd w"] Cons_eq_append_conv by fastforce

lemma distinct_letter_in_suf: assumes "\<not> w \<in>  [a]*" shows "\<exists> m b. [b] \<cdot> [a]\<^sup>@m  \<le>s w \<and> b \<noteq> a" 
proof-
  have  "\<not> rev w \<in>  [a]*"
    using rev_power[of "[a]"] unfolding  rev_sing using assms root_def rev_rev_ident[of w]
    by metis
  obtain m b where "[a]\<^sup>@m \<cdot> [b]  \<le>p rev w" and "b \<noteq> a"
    using distinct_letter_in[OF \<open>\<not> rev w \<in>  [a]*\<close>]  by blast
  have "rev ( [b] \<cdot> [a]\<^sup>@m) = [a]\<^sup>@m \<cdot> [b]"
    by (simp add: rev_power) 
  have "[b] \<cdot> [a]\<^sup>@m  \<le>s w"
    using pref_rev_suf'[of "[b] \<cdot> [a]\<^sup>@m" w] \<open>[a]\<^sup>@m \<cdot> [b]  \<le>p rev w\<close> 
    unfolding \<open>rev ( [b] \<cdot> [a]\<^sup>@m) = [a]\<^sup>@m \<cdot> [b]\<close> by blast
  thus ?thesis
    using \<open>b \<noteq> a\<close> by blast
qed

lemma sing_power:"i < m \<Longrightarrow> ([a]\<^sup>@m) ! i = a"
  by (induct i m rule: diff_induct) auto

lemma sing_power':"w \<in> [a]* \<Longrightarrow> i < \<^bold>|w\<^bold>| \<Longrightarrow> w ! i = a"
  by (metis add_nth factor_def prefix_def sing_power_factor')

lemma rev_sing_power: "x \<in> [a]* \<Longrightarrow> rev x = x"
  unfolding root_def using rev_power rev_singleton_conv  by metis

lemma lcp_letter_power: 
  assumes "w \<noteq> \<epsilon>" and "w \<in> [a]*" and "[a]\<^sup>@m \<cdot> [b] \<le>p z" and  "a \<noteq> b" 
  shows "w \<cdot> z \<and>\<^sub>p z \<cdot> w = [a]\<^sup>@m"                     
proof-
  obtain k z' where "w = [a]\<^sup>@k" "z = [a]\<^sup>@m \<cdot> [b] \<cdot> z'" "k \<noteq> 0"
    using \<open>w \<in> [a]*\<close> \<open>[a]\<^sup>@m \<cdot> [b] \<le>p z\<close> \<open>w \<noteq> \<epsilon>\<close>  
    unfolding root_def by fastforce 
  hence eq1: "w \<cdot> z = [a]\<^sup>@m \<cdot> ([a]\<^sup>@k \<cdot> [b] \<cdot> z')" and eq2: "z \<cdot> w = [a]\<^sup>@m \<cdot> ([b] \<cdot> z'\<cdot> [a]\<^sup>@k)"
    by (simp add: \<open>w = [a]\<^sup>@k\<close> \<open>z = [a]\<^sup>@m \<cdot> [b] \<cdot> z'\<close> powers_comm)+
  have "hd ([a]\<^sup>@k \<cdot> [b] \<cdot> z') = a" 
    using hd_sing_power \<open>k \<noteq> 0\<close>
    by (metis \<open>w = (a # \<epsilon>)\<^sup>@k\<close> append.assoc assms(1) hd_append2)
  moreover have "hd([b] \<cdot> z'\<cdot> [a]\<^sup>@k) = b"
    by simp 
  ultimately have "[a]\<^sup>@k \<cdot> [b] \<cdot> z' \<and>\<^sub>p [b] \<cdot> z'\<cdot> [a]\<^sup>@k = \<epsilon>"
    by (simp add: \<open>a \<noteq> b\<close> lcp_distinct_hd) 
  thus ?thesis using eq1 eq2 lcp_ext_left[of "[a]\<^sup>@m" "[a]\<^sup>@k \<cdot> [b] \<cdot> z'" "[b] \<cdot> z'\<cdot> [a]\<^sup>@k"]
    by simp
qed

lemma per_one: "w \<le>p [a]\<^sup>\<omega> \<Longrightarrow> w \<in> [a]*"
proof(induct w)
  case Nil
  then show ?case
    using empty_all_roots by auto 
next
  case (Cons a w)
  then show ?case
    by (metis period_root_def add_root append_Cons hd_word list.sel(1) pref_cancel prefix_def) 
qed

lemma per_one': "w \<in> [a]* \<Longrightarrow> w \<le>p [a]\<^sup>\<omega>"
  by (metis append_Nil2 not_Cons_self2 per_pref prefI root_def)

lemma per_sing_one: assumes "w \<noteq> \<epsilon>" "w \<le>p [a]\<^sup>\<omega>" shows "periodN w 1"
  using periodN_root[OF \<open>w \<noteq> \<epsilon>\<close> \<open>w \<le>p [a]\<^sup>\<omega>\<close>] unfolding sing_len[of a].

section \<open>Conjugation lemma\<close>

lemma conjugation: assumes "x\<cdot>z = z\<cdot>y" and "x \<noteq> \<epsilon>" 
  shows "\<exists> u v k. x = u \<cdot> v \<and> y = v \<cdot> u \<and> z = (u \<cdot> v)\<^sup>@k \<cdot> u"
proof-
  obtain k where "x\<^sup>@k \<le>p z" and "z \<le>p x\<^sup>@k \<cdot> x" 
    using  triv_pref[of z y] unfolding sym[OF \<open>x\<cdot>z = z\<cdot>y\<close>] 
    using per_rootI[of z x, OF _ \<open>x \<noteq> \<epsilon>\<close>]  per_pref[of z x] 
          pref_power[of z x] by blast 
  then obtain u v where "z = x\<^sup>@k \<cdot> u" and "x = u \<cdot> v" 
    by auto 
  hence "z = (u \<cdot> v)\<^sup>@k \<cdot> u"
    by simp
  have e: "u \<cdot> v \<cdot> ((u \<cdot> v) \<^sup>@ k \<cdot> u) = (u \<cdot> v) \<^sup>@ k \<cdot> u \<cdot> (v \<cdot> u)"
    by (simp add: comm_add_exp)
  hence  "y = v \<cdot> u"
    using \<open>x\<cdot>z = z\<cdot>y\<close> unfolding \<open>x = u \<cdot> v\<close> \<open>z = (u \<cdot> v)\<^sup>@k \<cdot> u\<close> e
    by simp
  thus ?thesis
    using \<open>x = u \<cdot> v\<close> \<open>z = x \<^sup>@ k \<cdot> u\<close> by blast 
qed


section \<open>Primitive words\<close>

definition primitive :: "'a list \<Rightarrow> bool" 
  where  "primitive x = (x \<noteq> \<epsilon> \<and> (\<forall> r. x \<in> r* \<longrightarrow> x = r))"

lemma power_non_prim: "1 < k \<Longrightarrow> \<not> primitive (w\<^sup>@k)"
proof (cases "w = \<epsilon>")
  assume "w = \<epsilon>" 
  thus "\<not> primitive (w\<^sup>@k)"
    unfolding primitive_def using emp_power by auto
next
  assume "w \<noteq> \<epsilon>" and "1 < k"
  hence "w\<^sup>@k \<noteq> w"
    by (metis eq_powers nat_neq_iff power_one_id)
  have "w\<^sup>@k \<in> w*" 
    unfolding root_def by auto
  thus "\<not> primitive (w\<^sup>@k)"
    unfolding primitive_def  using \<open>w\<^sup>@k \<noteq> w\<close> by blast 
qed

lemma comm_non_prim: "u \<noteq> \<epsilon> \<Longrightarrow> v \<noteq> \<epsilon> \<Longrightarrow> u\<cdot>v = v\<cdot>u \<Longrightarrow> \<not> primitive (u\<cdot>v)"
proof-
  assume "u \<noteq> \<epsilon>" "v \<noteq> \<epsilon>" "u\<cdot>v = v\<cdot>u"
  then obtain t k m where "u = t\<^sup>@k" "k > 0" "v = t\<^sup>@m" "m > 0" "t \<noteq> \<epsilon>"
    by (metis comm emp_power neq0_conv power_zero)
  thus ?thesis using power_non_prim[of "k+m" "t"]
    by (simp add: power_add_list)
qed

lemma non_prim: "\<not> primitive w \<Longrightarrow> w \<noteq> \<epsilon> \<Longrightarrow> (\<exists> r k. r \<noteq> \<epsilon> \<and> 1 < k \<and> w = r\<^sup>@k)"
  unfolding primitive_def
  by (metis emp_power less_one nat_neq_iff power_one_id power_zero root_def)

section \<open>Primitive root\<close>

definition primitive_root :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<in>\<^sub>p _ *" [51,51] 60)
  where  "primitive_root x r = (x \<noteq> \<epsilon> \<and> x \<in> r* \<and> primitive r)"

fun get_primitive_root :: "'a list \<Rightarrow> 'a list" ("\<rho>") where "get_primitive_root x = (THE r. x \<in>\<^sub>p r*)"  

lemma primroot_of_root: "\<lbrakk> x \<noteq> \<epsilon>; x \<in> u*; u \<in>\<^sub>p r*\<rbrakk> \<Longrightarrow> x \<in>\<^sub>p r*"
  unfolding primitive_root_def using root_trans by blast 

lemma prim_self_root: "primitive x \<Longrightarrow> x \<in>\<^sub>p x*"
  by (metis comm_root primitive_def primitive_root_def)

lemma comm_prim: "\<lbrakk> primitive r; primitive s; r\<cdot>s = s\<cdot>r \<rbrakk> \<Longrightarrow> r = s"
  by (metis primitive_def comm_root)

lemma primroot_ex: "x \<noteq> \<epsilon> \<longrightarrow> (\<exists> r k.  x \<in>\<^sub>p r* \<and> k \<noteq> 0 \<and> x = r\<^sup>@k)"
proof(induction "\<^bold>|x\<^bold>|" arbitrary: x rule: less_induct)
  case less
  then show ?case
  proof-
    {assume "\<not> primitive x"
      then obtain r where "x \<in> r*" "x \<noteq> r" "r \<noteq> \<epsilon>"
        unfolding primitive_def
        using less.prems root_nemp empty_all_roots  by blast 
      have "x \<noteq> \<epsilon> \<longrightarrow> (\<exists> r k. x \<in>\<^sub>p r* \<and> k \<noteq> 0 \<and> x = r\<^sup>@k)"
        using less.hyps[OF root_shorter[OF _ \<open>x \<in> r*\<close> \<open>x \<noteq> r\<close>]] root_trans
        by (metis \<open>r \<noteq> \<epsilon>\<close> \<open>x \<in> r*\<close> power_zero primitive_root_def root_def)}
    thus "x \<noteq> \<epsilon> \<longrightarrow> (\<exists> r k. x \<in>\<^sub>p r* \<and> k \<noteq> 0 \<and> x = r\<^sup>@k)"
      using prim_self_root
      by (metis power_zero primitive_root_def root_def) 
  qed
qed

text\<open>Uniqueness of the primitive root follows from the following lemma\<close>

lemma primroot_unique: "\<lbrakk> u \<in>\<^sub>p r*; u \<in>\<^sub>p s* \<rbrakk> \<Longrightarrow> r = s" 
proof-
  assume "u \<in>\<^sub>p r*" 
  then obtain kr where "u = r\<^sup>@kr" and "kr \<noteq> 0"
    by (metis power_zero primitive_root_def root_def)
  assume "u \<in>\<^sub>p s*" 
  then obtain ks where "u = s\<^sup>@ks" and "ks \<noteq> 0"
    by (metis power_zero primitive_root_def root_def)
  obtain t where "s \<in> t*" and "r \<in> t*"
    using powers_comm_comm[of r kr s ks, OF _ \<open>kr \<noteq> 0\<close>] \<open>u = r\<^sup>@kr\<close> \<open>u = s\<^sup>@ks\<close> 
      comm_root0[of r s] by auto
  have "primitive r" and "primitive s"
    using \<open>u \<in>\<^sub>p r *\<close> \<open>u \<in>\<^sub>p s *\<close> primitive_root_def by auto
  thus ?thesis 
    unfolding primitive_def using \<open>s \<in> t*\<close> \<open>r \<in> t*\<close> by auto
qed

text\<open>Existence and uniqueness of the primitive root justifies the function @{term "\<rho>"}: it indeed yields the primitive root of a nonempty word.\<close>

lemma primroot_is_primroot: assumes "x \<noteq> \<epsilon>" shows "x \<in>\<^sub>p (\<rho> x)*"
  by (metis assms get_primitive_root.simps primroot_ex primroot_unique theI_unique)

lemma primroot_root:"u \<noteq> \<epsilon> \<Longrightarrow> u \<in> q* \<Longrightarrow> \<rho> q = \<rho> u"
  by (metis root_nemp primroot_is_primroot primroot_of_root primroot_unique)

lemma primroot_len_mult:"u \<noteq> \<epsilon> \<Longrightarrow> u \<in> q* \<Longrightarrow> \<exists>k . \<^bold>|q\<^bold>| = k*\<^bold>|\<rho> u\<^bold>|"
  by (metis primitive_root_def length_0_conv mult_0 primroot_is_primroot primroot_root root_len)

lemma primroot_shorter_root:"u \<noteq> \<epsilon> \<Longrightarrow> u \<in> q* \<Longrightarrow> \<^bold>|\<rho> u\<^bold>| \<le> \<^bold>|q\<^bold>|"
  by (metis primitive_root_def eq_refl root_nemp order.strict_implies_order primroot_is_primroot primroot_root root_shorter)

lemma primroot_shortest_root: assumes "u \<noteq> \<epsilon>" shows "\<^bold>|\<rho> u\<^bold>| = (LEAST d. (\<exists> r. (u \<in> r*) \<and> \<^bold>|r\<^bold>| = d))"
  using  Least_equality[of "\<lambda> k. (\<exists> r. (u \<in> r*) \<and> \<^bold>|r\<^bold>| = k)" "\<^bold>|\<rho> u\<^bold>|"]
proof
  show "\<exists>r. u \<in> r* \<and> \<^bold>|r\<^bold>| = \<^bold>|\<rho> u\<^bold>|"
    using assms primitive_root_def primroot_is_primroot by blast 
  show "\<And>y. \<exists>r. u \<in> r* \<and> \<^bold>|r\<^bold>| = y \<Longrightarrow> \<^bold>|\<rho> u\<^bold>| \<le> y"
    using assms primroot_shorter_root by fastforce
qed

lemma primroot_take: "u \<noteq> \<epsilon> \<Longrightarrow> \<rho> u = (take ( \<^bold>|\<rho> u\<^bold>| ) u)"
proof-
  assume "u \<noteq> \<epsilon>"
  then obtain k where "u = (\<rho> u)\<^sup>@k" and "k \<noteq> 0"
    by (metis power_zero primitive_root_def primroot_is_primroot root_def)
  thus "\<rho> u = (take ( \<^bold>|\<rho> u\<^bold>| ) u)"
    by (metis take_root)
qed

lemma primroot_take_shortest: "u \<noteq> \<epsilon> \<Longrightarrow> \<rho> u = (take (LEAST d. (\<exists> r. (u \<in> r*) \<and> \<^bold>|r\<^bold>| = d)) u)"
  using primroot_shortest_root primroot_take by fastforce

text\<open>We also have the standard characterization of commutation for nonempty words.\<close>

theorem comm_primroots: "\<lbrakk> u \<noteq> \<epsilon>; v \<noteq> \<epsilon> \<rbrakk> \<Longrightarrow> u \<cdot> v = v \<cdot> u \<longleftrightarrow> \<rho> u = \<rho> v"
  using primitive_root_def comm_root[of u v] primroot_is_primroot primroot_root[of u] primroot_root[of v]
  by metis

end