503     \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; 

   503     \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; 

   504     length (vs1 @ vs2) = n; length (vs1 @ vs2) \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NMTIMES r n m"

   504     length (vs1 @ vs2) = n; length (vs1 @ vs2) \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NMTIMES r n m"

   505 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [];

   505 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [];

   506     length vs > n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : NMTIMES r n m"

   506     length vs > n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : NMTIMES r n m"

   507 

   507 

   509 inductive_cases Prf_elims:

   512 inductive_cases Prf_elims:

   510   "\<Turnstile> v : ZERO"

   513   "\<Turnstile> v : ZERO"

   511   "\<Turnstile> v : SEQ r1 r2"

   514   "\<Turnstile> v : SEQ r1 r2"

   512   "\<Turnstile> v : ALT r1 r2"

   515   "\<Turnstile> v : ALT r1 r2"

   513   "\<Turnstile> v : ONE"

   516   "\<Turnstile> v : ONE"

   762 

   765 

   763 lemma L_flat_Prf:

   766 lemma L_flat_Prf:

   764   shows "L(r) = {flat v | v. \<Turnstile> v : r}"

   767   shows "L(r) = {flat v | v. \<Turnstile> v : r}"

   765 using L_flat_Prf1 L_flat_Prf2 by blast

   768 using L_flat_Prf1 L_flat_Prf2 by blast

   766 

   769 

   768 

   798 

   769 section {* Sets of Lexical Values *}

   799 section {* Sets of Lexical Values *}

   770 

   800 

   771 text {*

   801 text {*

   772   Shows that lexical values are finite for a given regex and string.

   802   Shows that lexical values are finite for a given regex and string.