inductive_set star :: "'v list set ⇒ 'v list set"
  for r :: "'v list set" where
zero[intro!]:"[] ∈ star r"|
step[intro!]:"x ∈ r ∧ y ∈ star r ⟹ x @ y ∈ star r"

primrec sem_reg :: "('v) regexp => 'v set⇒ 'v list set" where
"sem_reg ESet v = {[]}"| (*Empty Set*)
"sem_reg (Dot) vset = (λx .[x]) ` vset" |
"sem_reg (Concat r1 r2) v ={q@p| q p. q ∈ sem_reg r1 v ∧ p ∈ sem_reg r2 v}"|
"sem_reg (LChr a) v = {[a]}"|
"sem_reg (Alter v1 v2) a = (sem_reg v1 a) ∪ (sem_reg v2 a)"|
"sem_reg (Star a) v = star (sem_reg a v)"|
"sem_reg (Ques v) a = {[]} ∪ (sem_reg v a)"|
"sem_reg ε v = {[]}"

fun concat_transition ::"(('v regexp × 'v set × 'v regexp) set * 'v regexp * 'v regexp) list set \<Rightarrow> (('v regexp × 'v set × 'v regexp) set * 'v regexp * 'v regexp) list set \<Rightarrow> (('v regexp × 'v set × 'v regexp) set * 'v regexp * 'v regexp) list set" where
"concat_transition lset1 lset2 = {x@y| x y. x\<in> lset1 \<and> y\<in>lset2}"

primrec trans2LTS :: "'v regexp ⇒ 'v set ⇒ (('v regexp × 'v set × 'v regexp) set * 'v regexp * 'v regexp) list set"  where
    "trans2LTS (LChr v) alp_set= {[({(LChr v, {v}, \<epsilon>)}, LChr v, \<epsilon>)]}"|
    "trans2LTS (ESet) alp_set= {[({(ESet, {} ,\<epsilon>)},ESet,\<epsilon>)]}"|
    "trans2LTS (\<epsilon>) alp_set = {[({},\<epsilon>,\<epsilon>)]}"|
    "trans2LTS (Dot) alp_set = {[({(Dot, alp_set, \<epsilon>)},Dot,\<epsilon>)]}"|
    "trans2LTS (Alter r1 r2) alp_set = trans2LTS r1 alp_set \<union>  trans2LTS r2 alp_set"|
    "trans2LTS (Concat r1 r2) alp_set = concat_transition (trans2LTS r1 alp_set) (trans2LTS r2 alp_set)" |
    "trans2LTS (Star r) alp_set = star (trans2LTS r alp_set)" |
    "trans2LTS (Ques r) alp_set = {[({(Ques r, {}, \<epsilon>)},Ques r, \<epsilon>)]} \<union> trans2LTS r alp_set"
  ```

And the definition of single_LTS_reahchable:

Basically, I try to use star induction help to prove this but failed.  An auxiliary lemma help to prove I think is on the  single_LTS_reahchable, like some function on x, then get the result of the function on w. But I am new Isabeller and couldn't think about any idea to prove it. Hope anyone could help me solve it, thx a lot.