How to define the range lemma like star

Question

Based on the repositoy in AFP, I plan to extend the library of regexp in Isabelle. Here I try to prove the range regexp in below which is similay to star.

The index of star could start from zero(empty list) to infinite. The range starts from nat m to nat n. But I have no idea that figure out a solution like lemma in_star_iff_concat(i.e. use the list to denote the procedure).

Any helps would be appreciated.

type_synonym 'a lang = "'a list set"

definition conc :: "'a lang ⇒ 'a lang ⇒ 'a lang" (infixr "@@" 75) where
"A @@ B = {xs@ys | xs ys. xs:A & ys:B}"

overloading lang_pow == "compow :: nat ⇒ 'a lang ⇒ 'a lang"
begin
  primrec lang_pow :: "nat ⇒ 'a lang ⇒ 'a lang" where
  "lang_pow 0 A = {[]}" |
  "lang_pow (Suc n) A = A @@ (lang_pow n A)"
end

definition lang_pow :: "nat ⇒ 'a lang ⇒ 'a lang" where
  lang_pow_code_def [code_abbrev]: "lang_pow = compow"

lemma [code]:
  "lang_pow (Suc n) A = A @@ (lang_pow n A)"
  "lang_pow 0 A = {[]}"
  by (simp_all add: lang_pow_code_def)


definition star :: "'a lang ⇒ 'a lang" where
"star A = (⋃n. A ^^ n)"


definition range :: "'a lang ⇒ nat ⇒ nat => 'a lang " where
"range A m n= (⋃i∈{m..n}. A ^^ i)"


lemma concat_in_star: "set ws ⊆ A ⟹ concat ws : star A"
  by(induct ws) simp_all


lemma in_star_iff_concat:
  "w ∈ star A = (∃ws. set ws ⊆ A ∧ w = concat ws)"
  (is "_ = (∃ws. ?R w ws)")
proof
  assume "w : star A" thus "∃ws. ?R w ws"
  proof induct
    case Nil have "?R [] []" by simp
    thus ?case ..
  next
    case (append u v)
    then obtain ws where "set ws ⊆ A ∧ v = concat ws" by blast
    with append have "?R (u@v) (u#ws)" by auto
    thus ?case ..
  qed
next
  assume "∃us. ?R w us" thus "w : star A"
  by (auto simp: concat_in_star)
qed

lemma try_range :"w : range A m n = (...)"
sorry