19 where

    19 where

    20   start[intro]: "[] \<in> L\<star>"

    20   start[intro]: "[] \<in> L\<star>"

    21 | step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> L\<star>"

    21 | step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> L\<star>"

    22 

    22 

    23 

    23 

    25 

    25 

    26 lemma lang_star_cases:

    26 lemma lang_star_cases:

    27   shows "L\<star> =  {[]} \<union> L ; L\<star>"

    27   shows "L\<star> =  {[]} \<union> L ; L\<star>"

    28 by (auto) (metis Star.simps)

    28 by (auto) (metis Star.simps)

    29 

    29