1    

     2 theory SpecExt

     3   imports Main (*"~~/src/HOL/Library/Sublist"*)

     4 begin

     5 

     6 section {* Sequential Composition of Languages *}

     7 

     8 definition

     9   Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)

    10 where 

    11   "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"

    12 

    13 text {* Two Simple Properties about Sequential Composition *}

    14 

    15 lemma Sequ_empty_string [simp]:

    16   shows "A ;; {[]} = A"

    17   and   "{[]} ;; A = A"

    18 by (simp_all add: Sequ_def)

    19 

    20 lemma Sequ_empty [simp]:

    21   shows "A ;; {} = {}"

    22   and   "{} ;; A = {}"

    23 by (simp_all add: Sequ_def)

    24 

    25 lemma Sequ_assoc:

    26   shows "(A ;; B) ;; C = A ;; (B ;; C)"

    27 apply(auto simp add: Sequ_def)

    28 apply blast

    29 by (metis append_assoc)

    30 

    31 lemma Sequ_Union_in:

    32   shows "(A ;; (\<Union>x\<in> B. C x)) = (\<Union>x\<in> B. A ;; C x)" 

    33 by (auto simp add: Sequ_def)

    34 

    35 section {* Semantic Derivative (Left Quotient) of Languages *}

    36 

    37 definition

    38   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"

    39 where

    40   "Der c A \<equiv> {s. c # s \<in> A}"

    41 

    42 definition

    43   Ders :: "string \<Rightarrow> string set \<Rightarrow> string set"

    44 where

    45   "Ders s A \<equiv> {s'. s @ s' \<in> A}"

    46 

    47 lemma Der_null [simp]:

    48   shows "Der c {} = {}"

    49 unfolding Der_def

    50 by auto

    51 

    52 lemma Der_empty [simp]:

    53   shows "Der c {[]} = {}"

    54 unfolding Der_def

    55 by auto

    56 

    57 lemma Der_char [simp]:

    58   shows "Der c {[d]} = (if c = d then {[]} else {})"

    59 unfolding Der_def

    60 by auto

    61 

    62 lemma Der_union [simp]:

    63   shows "Der c (A \<union> B) = Der c A \<union> Der c B"

    64 unfolding Der_def

    65 by auto

    66 

    67 lemma Der_UNION [simp]: 

    68   shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"

    69 by (auto simp add: Der_def)

    70 

    71 lemma Der_Sequ [simp]:

    72   shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"

    73 unfolding Der_def Sequ_def

    74   by (auto simp add: Cons_eq_append_conv)

    75 

    76 

    77 section {* Kleene Star for Languages *}

    78 

    79 inductive_set

    80   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)

    81   for A :: "string set"

    82 where

    83   start[intro]: "[] \<in> A\<star>"

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

    85 

    86 (* Arden's lemma *)

    87 

    88 lemma Star_cases:

    89   shows "A\<star> = {[]} \<union> A ;; A\<star>"

    90 unfolding Sequ_def

    91 by (auto) (metis Star.simps)

    92 

    93 lemma Star_decomp: 

    94   assumes "c # x \<in> A\<star>" 

    95   shows "\<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A\<star>"

    96 using assms

    97 by (induct x\<equiv>"c # x" rule: Star.induct) 

    98    (auto simp add: append_eq_Cons_conv)

    99 

   100 lemma Star_Der_Sequ: 

   101   shows "Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>"

   102 unfolding Der_def Sequ_def

   103 by(auto simp add: Star_decomp)

   104 

   105 

   106 lemma Der_star [simp]:

   107   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"

   108 proof -    

   109   have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"  

   110     by (simp only: Star_cases[symmetric])

   111   also have "... = Der c (A ;; A\<star>)"

   112     by (simp only: Der_union Der_empty) (simp)

   113   also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"

   114     by simp

   115   also have "... =  (Der c A) ;; A\<star>"

   116     using Star_Der_Sequ by auto

   117   finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .

   118 qed

   119 

   120 section {* Power operation for Sets *}

   121 

   122 fun 

   123   Pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [101, 102] 101)

   124 where

   125    "A \<up> 0 = {[]}"

   126 |  "A \<up> (Suc n) = A ;; (A \<up> n)"

   127 

   128 lemma Pow_empty [simp]:

   129   shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)"

   130 by(induct n) (auto simp add: Sequ_def)

   131 

   132 lemma Pow_Suc_rev:

   133   "A \<up> (Suc n) =  (A \<up> n) ;; A"

   134 apply(induct n arbitrary: A)

   135 apply(simp_all)

   136 by (metis Sequ_assoc)

   137 

   138 

   139 lemma Pow_decomp: 

   140   assumes "c # x \<in> A \<up> n" 

   141   shows "\<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A \<up> (n - 1)"

   142 using assms

   143 apply(induct n) 

   144 apply(auto simp add: Cons_eq_append_conv Sequ_def)

   145 apply(case_tac n)

   146 apply(auto simp add: Sequ_def)

   147 apply(blast)

   148 done

   149 

   150 lemma Star_Pow:

   151   assumes "s \<in> A\<star>"

   152   shows "\<exists>n. s \<in> A \<up> n"

   153 using assms

   154 apply(induct)

   155 apply(auto)

   156 apply(rule_tac x="Suc n" in exI)

   157 apply(auto simp add: Sequ_def)

   158 done

   159 

   160 lemma Pow_Star:

   161   assumes "s \<in> A \<up> n"

   162   shows "s \<in> A\<star>"

   163 using assms

   164 apply(induct n arbitrary: s)

   165 apply(auto simp add: Sequ_def)

   166   done

   167 

   168 lemma

   169   assumes "[] \<in> A" "n \<noteq> 0" "A \<noteq> {}"

   170   shows "A \<up> (Suc n) = A \<up> n"

   171 

   172 lemma Der_Pow_0:

   173   shows "Der c (A \<up> 0) = {}"

   174 by(simp add: Der_def)

   175 

   176 lemma Der_Pow_Suc:

   177   shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n)"

   178 unfolding Der_def Sequ_def 

   179 apply(auto simp add: Cons_eq_append_conv Sequ_def dest!: Pow_decomp)

   180 apply(case_tac n)

   181 apply(force simp add: Sequ_def)+

   182 done

   183 

   184 lemma Der_Pow [simp]:

   185   shows "Der c (A \<up> n) = (if n = 0 then {} else (Der c A) ;; (A \<up> (n - 1)))"

   186 apply(case_tac n)

   187 apply(simp_all del: Pow.simps add: Der_Pow_0 Der_Pow_Suc)

   188 done

   189 

   190 lemma Der_Pow_Sequ [simp]:

   191   shows "Der c (A ;; A \<up> n) = (Der c A) ;; (A \<up> n)"

   192 by (simp only: Pow.simps[symmetric] Der_Pow) (simp)

   193 

   194 

   195 lemma Pow_Sequ_Un:

   196   assumes "0 < x"

   197   shows "(\<Union>n \<in> {..x}. (A \<up> n)) = ({[]} \<union> (\<Union>n \<in> {..x - Suc 0}. A ;; (A \<up> n)))"

   198 using assms

   199 apply(auto simp add: Sequ_def)

   200 apply(smt Pow.elims Sequ_def Suc_le_mono Suc_pred atMost_iff empty_iff insert_iff mem_Collect_eq)

   201 apply(rule_tac x="Suc xa" in bexI)

   202 apply(auto simp add: Sequ_def)

   203 done

   204 

   205 lemma Pow_Sequ_Un2:

   206   assumes "0 < x"

   207   shows "(\<Union>n \<in> {x..}. (A \<up> n)) = (\<Union>n \<in> {x - Suc 0..}. A ;; (A \<up> n))"

   208 using assms

   209 apply(auto simp add: Sequ_def)

   210 apply(case_tac n)

   211 apply(auto simp add: Sequ_def)

   212 apply fastforce

   213 apply(case_tac x)

   214 apply(auto)

   215 apply(rule_tac x="Suc xa" in bexI)

   216 apply(auto simp add: Sequ_def)

   217 done

   218 

   219 section {* Regular Expressions *}

   220 

   221 datatype rexp =

   222   ZERO

   223 | ONE

   224 | CHAR char

   225 | SEQ rexp rexp

   226 | ALT rexp rexp

   227 | STAR rexp

   228 | UPNTIMES rexp nat

   229 | NTIMES rexp nat

   230 | FROMNTIMES rexp nat

   231 | NMTIMES rexp nat nat

   232 | NOT rexp

   233 

   234 section {* Semantics of Regular Expressions *}

   235  

   236 fun

   237   L :: "rexp \<Rightarrow> string set"

   238 where

   239   "L (ZERO) = {}"

   240 | "L (ONE) = {[]}"

   241 | "L (CHAR c) = {[c]}"

   242 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"

   243 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"

   244 | "L (STAR r) = (L r)\<star>"

   245 | "L (UPNTIMES r n) = (\<Union>i\<in>{..n} . (L r) \<up> i)"

   246 | "L (NTIMES r n) = (L r) \<up> n"

   247 | "L (FROMNTIMES r n) = (\<Union>i\<in>{n..} . (L r) \<up> i)"

   248 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" 

   249 | "L (NOT r) = ((UNIV:: string set)  - L r)"

   250 

   251 section {* Nullable, Derivatives *}

   252 

   253 fun

   254  nullable :: "rexp \<Rightarrow> bool"

   255 where

   256   "nullable (ZERO) = False"

   257 | "nullable (ONE) = True"

   258 | "nullable (CHAR c) = False"

   259 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"

   260 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"

   261 | "nullable (STAR r) = True"

   262 | "nullable (UPNTIMES r n) = True"

   263 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"

   264 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)"

   265 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"

   266 | "nullable (NOT r) = (\<not> nullable r)"

   267 

   268 fun

   269  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"

   270 where

   271   "der c (ZERO) = ZERO"

   272 | "der c (ONE) = ZERO"

   273 | "der c (CHAR d) = (if c = d then ONE else ZERO)"

   274 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"

   275 | "der c (SEQ r1 r2) = 

   276      (if nullable r1

   277       then ALT (SEQ (der c r1) r2) (der c r2)

   278       else SEQ (der c r1) r2)"

   279 | "der c (STAR r) = SEQ (der c r) (STAR r)"

   280 | "der c (UPNTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (UPNTIMES r (n - 1)))"

   281 | "der c (NTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (NTIMES r (n - 1)))"

   282 | "der c (FROMNTIMES r n) =

   283      (if n = 0 

   284       then SEQ (der c r) (STAR r)

   285       else SEQ (der c r) (FROMNTIMES r (n - 1)))"

   286 | "der c (NMTIMES r n m) = 

   287      (if m < n then ZERO 

   288       else (if n = 0 then (if m = 0 then ZERO else 

   289                            SEQ (der c r) (UPNTIMES r (m - 1))) else 

   290                            SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" 

   291 | "der c (NOT r) = NOT (der c r)"

   292 

   293 lemma

   294  "L(der c (UPNTIMES r m))  =

   295      L(if (m = 0) then ZERO else ALT ONE (SEQ(der c r) (UPNTIMES r (m - 1))))"

   296   apply(case_tac m)

   297   apply(simp)

   298   apply(simp del: der.simps)

   299   apply(simp only: der.simps)

   300   apply(simp add: Sequ_def)

   301   apply(auto)

   302   defer

   303   apply blast

   304   oops

   305 

   306 

   307 

   308 lemma 

   309   assumes "der c r = ONE \<or> der c r = ZERO"

   310   shows "L (der c (NOT r)) \<noteq> L(if (der c r = ZERO) then ONE else 

   311                                if (der c r = ONE) then ZERO

   312                                else NOT(der c r))"

   313   using assms

   314   apply(simp)

   315   apply(auto)

   316   done

   317 

   318 lemma 

   319   "L (der c (NOT r)) = L(if (der c r = ZERO) then ONE else 

   320                          if (der c r = ONE) then ZERO

   321                          else NOT(der c r))"

   322   apply(simp)

   323   apply(auto)

   324   oops

   325 

   326 lemma pow_add:

   327   assumes "s1 \<in> A \<up> n" "s2 \<in> A \<up> m"

   328   shows "s1 @ s2 \<in> A \<up> (n + m)"

   329   using assms

   330   apply(induct n arbitrary: m s1 s2)

   331   apply(auto simp add: Sequ_def)

   332   by blast

   333 

   334 lemma pow_add2:

   335   assumes "x \<in> A \<up> (m + n)"

   336   shows "x \<in> A \<up> m ;; A \<up> n"

   337   using assms

   338   apply(induct m arbitrary: n x)

   339   apply(auto simp add: Sequ_def)

   340   by (metis append.assoc)

   341   

   342 

   343 

   344 lemma

   345  "L(FROMNTIMES r n) = L(SEQ (NTIMES r n) (STAR r))"

   346   apply(auto simp add: Sequ_def)

   347   defer

   348    apply(subgoal_tac "\<exists>m. s2 \<in> (L r) \<up> m")

   349   prefer 2

   350     apply (simp add: Star_Pow)

   351   apply(auto)

   352   apply(rule_tac x="n + m" in bexI)

   353     apply (simp add: pow_add)

   354    apply simp

   355   apply(subgoal_tac "\<exists>m. m + n = xa")

   356    apply(auto)

   357    prefer 2

   358   using le_add_diff_inverse2 apply auto[1]

   359   by (smt Pow_Star Sequ_def add.commute mem_Collect_eq pow_add2)

   360   

   361 lemma

   362    "L (der c (FROMNTIMES r n)) = 

   363      L (SEQ (der c r) (FROMNTIMES r (n - 1)))"

   364   apply(auto simp add: Sequ_def)

   365   using Star_Pow apply blast

   366   using Pow_Star by blast

   367   

   368 lemma

   369  "L (der c (UPNTIMES r n)) = 

   370     L(if n = 0 then ZERO  else 

   371       ALT (der c r) (SEQ (der c r) (UPNTIMES r (n - 1))))"

   372   apply(auto simp add: Sequ_def)

   373   using SpecExt.Pow_empty by blast 

   374 

   375 abbreviation "FROM \<equiv> FROMNTIMES"

   376 

   377 lemma

   378   shows "L (der c (FROM r n)) = 

   379          L (if n <= 0 then SEQ (der c r) (ALT ONE (FROM r 0))

   380                       else SEQ (der c r) (ALT ZERO (FROM r (n -1))))"

   381   apply(auto simp add: Sequ_def)

   382   oops

   383 

   384 

   385 fun 

   386  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"

   387 where

   388   "ders [] r = r"

   389 | "ders (c # s) r = ders s (der c r)"

   390 

   391 

   392 lemma nullable_correctness:

   393   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"

   394 by(induct r) (auto simp add: Sequ_def) 

   395 

   396 

   397 lemma der_correctness:

   398   shows "L (der c r) = Der c (L r)"

   399 apply(induct r) 

   400 apply(simp add: nullable_correctness del: Der_UNION)

   401 apply(simp add: nullable_correctness del: Der_UNION)

   402 apply(simp add: nullable_correctness del: Der_UNION)

   403 apply(simp add: nullable_correctness del: Der_UNION)

   404 apply(simp add: nullable_correctness del: Der_UNION)

   405 apply(simp add: nullable_correctness del: Der_UNION)

   406       prefer 2

   407       apply(simp only: der.simps)

   408       apply(case_tac "x2 = 0")

   409        apply(simp)

   410       apply(simp del: Der_Sequ L.simps)

   411       apply(subst L.simps)

   412   apply(subst (2) L.simps)

   413   thm Der_UNION

   414 

   415 apply(simp add: nullable_correctness del: Der_UNION)

   416 apply(simp add: nullable_correctness del: Der_UNION)

   417 apply(rule impI)

   418 apply(subst Sequ_Union_in)

   419 apply(subst Der_Pow_Sequ[symmetric])

   420 apply(subst Pow.simps[symmetric])

   421 apply(subst Der_UNION[symmetric])

   422 apply(subst Pow_Sequ_Un)

   423 apply(simp)

   424 apply(simp only: Der_union Der_empty)

   425     apply(simp)

   426 (* FROMNTIMES *)    

   427    apply(simp add: nullable_correctness del: Der_UNION)

   428   apply(rule conjI)

   429 prefer 2    

   430 apply(subst Sequ_Union_in)

   431 apply(subst Der_Pow_Sequ[symmetric])

   432 apply(subst Pow.simps[symmetric])

   433 apply(case_tac x2)

   434 prefer 2

   435 apply(subst Pow_Sequ_Un2)

   436 apply(simp)

   437 apply(simp)

   438     apply(auto simp add: Sequ_def Der_def)[1]

   439    apply(auto simp add: Sequ_def split: if_splits)[1]

   440   using Star_Pow apply fastforce

   441   using Pow_Star apply blast

   442 (* NMTIMES *)    

   443 apply(simp add: nullable_correctness del: Der_UNION)

   444 apply(rule impI)

   445 apply(rule conjI)

   446 apply(rule impI)

   447 apply(subst Sequ_Union_in)

   448 apply(subst Der_Pow_Sequ[symmetric])

   449 apply(subst Pow.simps[symmetric])

   450 apply(subst Der_UNION[symmetric])

   451 apply(case_tac x3a)

   452 apply(simp)

   453 apply(clarify)

   454 apply(auto simp add: Sequ_def Der_def Cons_eq_append_conv)[1]

   455 apply(rule_tac x="Suc xa" in bexI)

   456 apply(auto simp add: Sequ_def)[2]

   457 apply (metis append_Cons)

   458 apply (metis (no_types, hide_lams) Pow_decomp atMost_iff diff_Suc_eq_diff_pred diff_is_0_eq)

   459 apply(rule impI)+

   460 apply(subst Sequ_Union_in)

   461 apply(subst Der_Pow_Sequ[symmetric])

   462 apply(subst Pow.simps[symmetric])

   463 apply(subst Der_UNION[symmetric])

   464 apply(case_tac x2)

   465 apply(simp)

   466 apply(simp del: Pow.simps)

   467 apply(auto simp add: Sequ_def Der_def)

   468 apply (metis One_nat_def Suc_le_D Suc_le_mono atLeastAtMost_iff diff_Suc_1 not_le)

   469 by fastforce

   470 

   471 

   472 

   473 lemma ders_correctness:

   474   shows "L (ders s r) = Ders s (L r)"

   475 by (induct s arbitrary: r)

   476    (simp_all add: Ders_def der_correctness Der_def)

   477 

   478 

   479 section {* Values *}

   480 

   481 datatype val = 

   482   Void

   483 | Char char

   484 | Seq val val

   485 | Right val

   486 | Left val

   487 | Stars "val list"

   488 

   489 

   490 section {* The string behind a value *}

   491 

   492 fun 

   493   flat :: "val \<Rightarrow> string"

   494 where

   495   "flat (Void) = []"

   496 | "flat (Char c) = [c]"

   497 | "flat (Left v) = flat v"

   498 | "flat (Right v) = flat v"

   499 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)"

   500 | "flat (Stars []) = []"

   501 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" 

   502 

   503 abbreviation

   504   "flats vs \<equiv> concat (map flat vs)"

   505 

   506 lemma flat_Stars [simp]:

   507  "flat (Stars vs) = flats vs"

   508 by (induct vs) (auto)

   509 

   510 lemma Star_concat:

   511   assumes "\<forall>s \<in> set ss. s \<in> A"  

   512   shows "concat ss \<in> A\<star>"

   513 using assms by (induct ss) (auto)

   514 

   515 lemma Star_cstring:

   516   assumes "s \<in> A\<star>"

   517   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A \<and> s \<noteq> [])"

   518 using assms

   519 apply(induct rule: Star.induct)

   520 apply(auto)[1]

   521 apply(rule_tac x="[]" in exI)

   522 apply(simp)

   523 apply(erule exE)

   524 apply(clarify)

   525 apply(case_tac "s1 = []")

   526 apply(rule_tac x="ss" in exI)

   527 apply(simp)

   528 apply(rule_tac x="s1#ss" in exI)

   529 apply(simp)

   530 done

   531 

   532 lemma Aux:

   533   assumes "\<forall>s\<in>set ss. s = []"

   534   shows "concat ss = []"

   535 using assms

   536 by (induct ss) (auto)

   537 

   538 lemma Pow_cstring_nonempty:

   539   assumes "s \<in> A \<up> n"

   540   shows "\<exists>ss. concat ss = s \<and> length ss \<le> n \<and> (\<forall>s \<in> set ss. s \<in> A \<and> s \<noteq> [])"

   541 using assms

   542 apply(induct n arbitrary: s)

   543 apply(auto)

   544 apply(simp add: Sequ_def)

   545 apply(erule exE)+

   546 apply(clarify)

   547 apply(drule_tac x="s2" in meta_spec)

   548 apply(simp)

   549 apply(clarify)

   550 apply(case_tac "s1 = []")

   551 apply(simp)

   552 apply(rule_tac x="ss" in exI)

   553 apply(simp)

   554 apply(rule_tac x="s1 # ss" in exI)

   555 apply(simp)

   556 done

   557 

   558 lemma Pow_cstring:

   559   assumes "s \<in> A \<up> n"

   560   shows "\<exists>ss1 ss2. concat (ss1 @ ss2) = s \<and> length (ss1 @ ss2) = n \<and> 

   561          (\<forall>s \<in> set ss1. s \<in> A \<and> s \<noteq> []) \<and> (\<forall>s \<in> set ss2. s \<in> A \<and> s = [])"

   562 using assms

   563 apply(induct n arbitrary: s)

   564 apply(auto)[1]

   565 apply(simp only: Pow_Suc_rev)

   566 apply(simp add: Sequ_def)

   567 apply(erule exE)+

   568 apply(clarify)

   569 apply(drule_tac x="s1" in meta_spec)

   570 apply(simp)

   571 apply(erule exE)+

   572 apply(clarify)

   573 apply(case_tac "s2 = []")

   574 apply(simp)

   575 apply(rule_tac x="ss1" in exI)

   576 apply(rule_tac x="s2#ss2" in exI)

   577 apply(simp)

   578 apply(rule_tac x="ss1 @ [s2]" in exI)

   579 apply(rule_tac x="ss2" in exI)

   580 apply(simp)

   581 apply(subst Aux)

   582 apply(auto)[1]

   583 apply(subst Aux)

   584 apply(auto)[1]

   585 apply(simp)

   586 done

   587 

   588 

   589 section {* Lexical Values *}

   590 

   591 

   592 

   593 inductive 

   594   Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)

   595 where

   596  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>  Seq v1 v2 : SEQ r1 r2"

   597 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"

   598 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"

   599 | "\<Turnstile> Void : ONE"

   600 | "\<Turnstile> Char c : CHAR c"

   601 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : STAR r"

   602 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []; length vs \<le> n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : UPNTIMES r n"

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

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

   605     length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NTIMES r n"

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

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

   608     length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : FROMNTIMES r n"

   609 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r  \<and> flat v \<noteq> []; length vs > n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : FROMNTIMES r n"

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

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

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

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

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

   615 

   616 

   617  

   618 

   619 

   620 inductive_cases Prf_elims:

   621   "\<Turnstile> v : ZERO"

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

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

   624   "\<Turnstile> v : ONE"

   625   "\<Turnstile> v : CHAR c"

   626   "\<Turnstile> vs : STAR r"

   627   "\<Turnstile> vs : UPNTIMES r n"

   628   "\<Turnstile> vs : NTIMES r n"

   629   "\<Turnstile> vs : FROMNTIMES r n"

   630   "\<Turnstile> vs : NMTIMES r n m"

   631 

   632 lemma Prf_Stars_appendE:

   633   assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"

   634   shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" 

   635 using assms

   636 by (auto intro: Prf.intros elim!: Prf_elims)

   637 

   638 

   639 

   640 lemma flats_empty:

   641   assumes "(\<forall>v\<in>set vs. flat v = [])"

   642   shows "flats vs = []"

   643 using assms

   644 by(induct vs) (simp_all)

   645 

   646 lemma Star_cval:

   647   assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r"

   648   shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> [])"

   649 using assms

   650 apply(induct ss)

   651 apply(auto)

   652 apply(rule_tac x="[]" in exI)

   653 apply(simp)

   654 apply(case_tac "flat v = []")

   655 apply(rule_tac x="vs" in exI)

   656 apply(simp)

   657 apply(rule_tac x="v#vs" in exI)

   658 apply(simp)

   659 done

   660 

   661 

   662 lemma flats_cval:

   663   assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r"

   664   shows "\<exists>vs1 vs2. flats (vs1 @ vs2) = concat ss \<and> length (vs1 @ vs2) = length ss \<and> 

   665           (\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []) \<and>

   666           (\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = [])"

   667 using assms

   668 apply(induct ss rule: rev_induct)

   669 apply(rule_tac x="[]" in exI)+

   670 apply(simp)

   671 apply(simp)

   672 apply(clarify)

   673 apply(case_tac "flat v = []")

   674 apply(rule_tac x="vs1" in exI)

   675 apply(rule_tac x="v#vs2" in exI)

   676 apply(simp)

   677 apply(rule_tac x="vs1 @ [v]" in exI)

   678 apply(rule_tac x="vs2" in exI)

   679 apply(simp)

   680 apply(subst (asm) (2) flats_empty)

   681 apply(simp)

   682 apply(simp)

   683 done

   684 

   685 lemma flats_cval_nonempty:

   686   assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r"

   687   shows "\<exists>vs. flats vs = concat ss \<and> length vs \<le> length ss \<and> 

   688           (\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> [])" 

   689 using assms

   690 apply(induct ss)

   691 apply(rule_tac x="[]" in exI)

   692 apply(simp)

   693 apply(simp)

   694 apply(clarify)

   695 apply(case_tac "flat v = []")

   696 apply(rule_tac x="vs" in exI)

   697 apply(simp)

   698 apply(rule_tac x="v # vs" in exI)

   699 apply(simp)

   700 done

   701 

   702 lemma Pow_flats:

   703   assumes "\<forall>v \<in> set vs. flat v \<in> A"

   704   shows "flats vs \<in> A \<up> length vs"

   705 using assms

   706 by(induct vs)(auto simp add: Sequ_def)

   707 

   708 lemma Pow_flats_appends:

   709   assumes "\<forall>v \<in> set vs1. flat v \<in> A" "\<forall>v \<in> set vs2. flat v \<in> A"

   710   shows "flats vs1 @ flats vs2 \<in> A \<up> (length vs1 + length vs2)"

   711 using assms

   712 apply(induct vs1)

   713 apply(auto simp add: Sequ_def Pow_flats)

   714 done

   715 

   716 lemma L_flat_Prf1:

   717   assumes "\<Turnstile> v : r" 

   718   shows "flat v \<in> L r"

   719 using assms

   720 apply(induct) 

   721 apply(auto simp add: Sequ_def Star_concat Pow_flats)

   722 apply(meson Pow_flats atMost_iff)

   723 using Pow_flats_appends apply blast

   724 using Pow_flats_appends apply blast

   725 apply (meson Pow_flats atLeast_iff less_imp_le)

   726 apply(rule_tac x="length vs1 + length vs2" in  bexI)

   727 apply(meson Pow_flats_appends atLeastAtMost_iff)

   728 apply(simp)

   729 apply(meson Pow_flats atLeastAtMost_iff less_or_eq_imp_le)

   730 done

   731 

   732 lemma L_flat_Prf2:

   733   assumes "s \<in> L r" 

   734   shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s"

   735 using assms

   736 proof(induct r arbitrary: s)

   737   case (STAR r s)

   738   have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact

   739   have "s \<in> L (STAR r)" by fact

   740   then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []"

   741   using Star_cstring by auto  

   742   then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []"

   743   using IH Star_cval by metis 

   744   then show "\<exists>v. \<Turnstile> v : STAR r \<and> flat v = s"

   745   using Prf.intros(6) flat_Stars by blast

   746 next 

   747   case (SEQ r1 r2 s)

   748   then show "\<exists>v. \<Turnstile> v : SEQ r1 r2 \<and> flat v = s"

   749   unfolding Sequ_def L.simps by (fastforce intro: Prf.intros)

   750 next

   751   case (ALT r1 r2 s)

   752   then show "\<exists>v. \<Turnstile> v : ALT r1 r2 \<and> flat v = s"

   753   unfolding L.simps by (fastforce intro: Prf.intros)

   754 next

   755   case (NTIMES r n)

   756   have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact

   757   have "s \<in> L (NTIMES r n)" by fact

   758   then obtain ss1 ss2 where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = n" 

   759     "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []"

   760   using Pow_cstring by force

   761   then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = n" 

   762       "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []"

   763   using IH flats_cval 

   764   apply -

   765   apply(drule_tac x="ss1 @ ss2" in meta_spec)

   766   apply(drule_tac x="r" in meta_spec)

   767   apply(drule meta_mp)

   768   apply(simp)

   769   apply (metis Un_iff)

   770   apply(clarify)

   771   apply(drule_tac x="vs1" in meta_spec)

   772   apply(drule_tac x="vs2" in meta_spec)

   773   apply(simp)

   774   done

   775   then show "\<exists>v. \<Turnstile> v : NTIMES r n \<and> flat v = s"

   776   using Prf.intros(8) flat_Stars by blast

   777 next 

   778   case (FROMNTIMES r n)

   779   have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact

   780   have "s \<in> L (FROMNTIMES r n)" by fact 

   781   then obtain ss1 ss2 k where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = k"  "n \<le> k"

   782     "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []"

   783     using Pow_cstring by force 

   784   then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = k" "n \<le> k"

   785       "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []"

   786   using IH flats_cval 

   787   apply -

   788   apply(drule_tac x="ss1 @ ss2" in meta_spec)

   789   apply(drule_tac x="r" in meta_spec)

   790   apply(drule meta_mp)

   791   apply(simp)

   792   apply (metis Un_iff)

   793   apply(clarify)

   794   apply(drule_tac x="vs1" in meta_spec)

   795   apply(drule_tac x="vs2" in meta_spec)

   796   apply(simp)

   797   done

   798   then show "\<exists>v. \<Turnstile> v : FROMNTIMES r n \<and> flat v = s"

   799   apply(case_tac "length vs1 \<le> n")

   800   apply(rule_tac x="Stars (vs1 @ take (n - length vs1) vs2)" in exI)

   801   apply(simp)

   802   apply(subgoal_tac "flats (take (n - length vs1) vs2) = []")

   803   prefer 2

   804   apply (meson flats_empty in_set_takeD)

   805   apply(clarify)

   806     apply(rule conjI)

   807       apply(rule Prf.intros)

   808         apply(simp)

   809        apply (meson in_set_takeD)

   810       apply(simp)

   811      apply(simp)

   812      apply (simp add: flats_empty)

   813       apply(rule_tac x="Stars vs1" in exI)

   814   apply(simp)

   815     apply(rule conjI)

   816      apply(rule Prf.intros(10))

   817       apply(auto)

   818   done    

   819 next 

   820   case (NMTIMES r n m)

   821   have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact

   822   have "s \<in> L (NMTIMES r n m)" by fact 

   823   then obtain ss1 ss2 k where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = k" "n \<le> k" "k \<le> m" 

   824     "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []"

   825   using Pow_cstring by (auto, blast)

   826   then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = k" "n \<le> k" "k \<le> m"

   827       "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []"

   828   using IH flats_cval 

   829   apply -

   830   apply(drule_tac x="ss1 @ ss2" in meta_spec)

   831   apply(drule_tac x="r" in meta_spec)

   832   apply(drule meta_mp)

   833   apply(simp)

   834   apply (metis Un_iff)

   835   apply(clarify)

   836   apply(drule_tac x="vs1" in meta_spec)

   837   apply(drule_tac x="vs2" in meta_spec)

   838   apply(simp)

   839   done

   840   then show "\<exists>v. \<Turnstile> v : NMTIMES r n m \<and> flat v = s"

   841     apply(case_tac "length vs1 \<le> n")

   842   apply(rule_tac x="Stars (vs1 @ take (n - length vs1) vs2)" in exI)

   843   apply(simp)

   844   apply(subgoal_tac "flats (take (n - length vs1) vs2) = []")

   845   prefer 2

   846   apply (meson flats_empty in_set_takeD)

   847   apply(clarify)

   848     apply(rule conjI)

   849       apply(rule Prf.intros)

   850         apply(simp)

   851        apply (meson in_set_takeD)

   852       apply(simp)

   853      apply(simp)

   854      apply (simp add: flats_empty)

   855       apply(rule_tac x="Stars vs1" in exI)

   856   apply(simp)

   857     apply(rule conjI)

   858      apply(rule Prf.intros)

   859       apply(auto)

   860   done    

   861 next 

   862   case (UPNTIMES r n s)

   863   have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact

   864   have "s \<in> L (UPNTIMES r n)" by fact

   865   then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []" "length ss \<le> n"

   866   using Pow_cstring_nonempty by force

   867   then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []" "length vs \<le> n"

   868   using IH flats_cval_nonempty by (smt order.trans) 

   869   then show "\<exists>v. \<Turnstile> v : UPNTIMES r n \<and> flat v = s"

   870   using Prf.intros(7) flat_Stars by blast

   871 qed (auto intro: Prf.intros)

   872 

   873 

   874 lemma L_flat_Prf:

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

   876 using L_flat_Prf1 L_flat_Prf2 by blast

   877 

   878 thm Prf.intros

   879 thm Prf.cases

   880 

   881 lemma

   882   assumes "\<Turnstile> v : (STAR r)" 

   883   shows "\<Turnstile> v : (FROMNTIMES r 0)"

   884   using assms

   885   apply(erule_tac Prf.cases)

   886              apply(simp_all)

   887   apply(case_tac vs)

   888    apply(auto)

   889   apply(subst append_Nil[symmetric])

   890    apply(rule Prf.intros)

   891      apply(auto)

   892   apply(simp add: Prf.intros)

   893   done

   894 

   895 lemma

   896   assumes "\<Turnstile> v : (FROMNTIMES r 0)" 

   897   shows "\<Turnstile> v : (STAR r)"

   898   using assms

   899   apply(erule_tac Prf.cases)

   900              apply(simp_all)

   901    apply(rule Prf.intros)

   902    apply(simp)

   903   apply(rule Prf.intros)

   904    apply(simp)

   905   done

   906 

   907 section {* Sets of Lexical Values *}

   908 

   909 text {*

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

   911 *}

   912 

   913 definition

   914   LV :: "rexp \<Rightarrow> string \<Rightarrow> val set"

   915 where  "LV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}"

   916 

   917 lemma LV_simps:

   918   shows "LV ZERO s = {}"

   919   and   "LV ONE s = (if s = [] then {Void} else {})"

   920   and   "LV (CHAR c) s = (if s = [c] then {Char c} else {})"

   921   and   "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"

   922 unfolding LV_def

   923 apply(auto intro: Prf.intros elim: Prf.cases)

   924 done

   925 

   926 abbreviation

   927   "Prefixes s \<equiv> {s'. prefix s' s}"

   928 

   929 abbreviation

   930   "Suffixes s \<equiv> {s'. suffix s' s}"

   931 

   932 abbreviation

   933   "SSuffixes s \<equiv> {s'. strict_suffix s' s}"

   934 

   935 lemma Suffixes_cons [simp]:

   936   shows "Suffixes (c # s) = Suffixes s \<union> {c # s}"

   937 by (auto simp add: suffix_def Cons_eq_append_conv)

   938 

   939 

   940 lemma finite_Suffixes: 

   941   shows "finite (Suffixes s)"

   942 by (induct s) (simp_all)

   943 

   944 lemma finite_SSuffixes: 

   945   shows "finite (SSuffixes s)"

   946 proof -

   947   have "SSuffixes s \<subseteq> Suffixes s"

   948    unfolding suffix_def strict_suffix_def by auto

   949   then show "finite (SSuffixes s)"

   950    using finite_Suffixes finite_subset by blast

   951 qed

   952 

   953 lemma finite_Prefixes: 

   954   shows "finite (Prefixes s)"

   955 proof -

   956   have "finite (Suffixes (rev s))" 

   957     by (rule finite_Suffixes)

   958   then have "finite (rev ` Suffixes (rev s))" by simp

   959   moreover

   960   have "rev ` (Suffixes (rev s)) = Prefixes s"

   961   unfolding suffix_def prefix_def image_def

   962    by (auto)(metis rev_append rev_rev_ident)+

   963   ultimately show "finite (Prefixes s)" by simp

   964 qed

   965 

   966 definition

   967   "Stars_Cons V Vs \<equiv> {Stars (v # vs) | v vs. v \<in> V \<and> Stars vs \<in> Vs}"

   968   

   969 definition

   970   "Stars_Append Vs1 Vs2 \<equiv> {Stars (vs1 @ vs2) | vs1 vs2. Stars vs1 \<in> Vs1 \<and> Stars vs2 \<in> Vs2}"

   971 

   972 fun Stars_Pow :: "val set \<Rightarrow> nat \<Rightarrow> val set"

   973 where  

   974   "Stars_Pow Vs 0 = {Stars []}"

   975 | "Stars_Pow Vs (Suc n) = Stars_Cons Vs (Stars_Pow Vs n)"

   976   

   977 lemma finite_Stars_Cons:

   978   assumes "finite V" "finite Vs"

   979   shows "finite (Stars_Cons V Vs)"

   980   using assms  

   981 proof -

   982   from assms(2) have "finite (Stars -` Vs)"

   983     by(simp add: finite_vimageI inj_on_def) 

   984   with assms(1) have "finite (V \<times> (Stars -` Vs))"

   985     by(simp)

   986   then have "finite ((\<lambda>(v, vs). Stars (v # vs)) ` (V \<times> (Stars -` Vs)))"

   987     by simp

   988   moreover have "Stars_Cons V Vs = (\<lambda>(v, vs). Stars (v # vs)) ` (V \<times> (Stars -` Vs))"

   989     unfolding Stars_Cons_def by auto    

   990   ultimately show "finite (Stars_Cons V Vs)"   

   991     by simp

   992 qed

   993 

   994 lemma finite_Stars_Append:

   995   assumes "finite Vs1" "finite Vs2"

   996   shows "finite (Stars_Append Vs1 Vs2)"

   997   using assms  

   998 proof -

   999   define UVs1 where "UVs1 \<equiv> Stars -` Vs1"

  1000   define UVs2 where "UVs2 \<equiv> Stars -` Vs2"  

  1001   from assms have "finite UVs1" "finite UVs2"

  1002     unfolding UVs1_def UVs2_def

  1003     by(simp_all add: finite_vimageI inj_on_def) 

  1004   then have "finite ((\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2))"

  1005     by simp

  1006   moreover 

  1007     have "Stars_Append Vs1 Vs2 = (\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2)"

  1008     unfolding Stars_Append_def UVs1_def UVs2_def by auto    

  1009   ultimately show "finite (Stars_Append Vs1 Vs2)"   

  1010     by simp

  1011 qed 

  1012  

  1013 lemma finite_Stars_Pow:

  1014   assumes "finite Vs"

  1015   shows "finite (Stars_Pow Vs n)"    

  1016 by (induct n) (simp_all add: finite_Stars_Cons assms)

  1017     

  1018 lemma LV_STAR_finite:

  1019   assumes "\<forall>s. finite (LV r s)"

  1020   shows "finite (LV (STAR r) s)"

  1021 proof(induct s rule: length_induct)

  1022   fix s::"char list"

  1023   assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')"

  1024   then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')"

  1025     apply(auto simp add: strict_suffix_def suffix_def)

  1026     by force    

  1027   define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)"

  1028   define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'"

  1029   define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. LV (STAR r) s2"

  1030   have "finite S1" using assms

  1031     unfolding S1_def by (simp_all add: finite_Prefixes)

  1032   moreover 

  1033   with IH have "finite S2" unfolding S2_def

  1034     by (auto simp add: finite_SSuffixes)

  1035   ultimately 

  1036   have "finite ({Stars []} \<union> Stars_Cons S1 S2)" 

  1037     by (simp add: finite_Stars_Cons)

  1038   moreover 

  1039   have "LV (STAR r) s \<subseteq> {Stars []} \<union> (Stars_Cons S1 S2)" 

  1040   unfolding S1_def S2_def f_def LV_def Stars_Cons_def

  1041   unfolding prefix_def strict_suffix_def 

  1042   unfolding image_def

  1043   apply(auto)

  1044   apply(case_tac x)

  1045   apply(auto elim: Prf_elims)

  1046   apply(erule Prf_elims)

  1047   apply(auto)

  1048   apply(case_tac vs)

  1049   apply(auto intro: Prf.intros)  

  1050   apply(rule exI)

  1051   apply(rule conjI)

  1052   apply(rule_tac x="flats list" in exI)

  1053    apply(rule conjI)

  1054   apply(simp add: suffix_def)

  1055   apply(blast)

  1056   using Prf.intros(6) flat_Stars by blast  

  1057   ultimately

  1058   show "finite (LV (STAR r) s)" by (simp add: finite_subset)

  1059 qed  

  1060     

  1061 lemma LV_UPNTIMES_STAR:

  1062   "LV (UPNTIMES r n) s \<subseteq> LV (STAR r) s"

  1063 by(auto simp add: LV_def intro: Prf.intros elim: Prf_elims)

  1064 

  1065 lemma LV_NTIMES_3:

  1066   shows "LV (NTIMES r (Suc n)) [] = (\<lambda>(v,vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (NTIMES r n) [])))"

  1067 unfolding LV_def

  1068 apply(auto elim!: Prf_elims simp add: image_def)

  1069 apply(case_tac vs1)

  1070 apply(auto)

  1071 apply(case_tac vs2)

  1072 apply(auto)

  1073 apply(subst append.simps(1)[symmetric])

  1074 apply(rule Prf.intros)

  1075 apply(auto)

  1076 apply(subst append.simps(1)[symmetric])

  1077 apply(rule Prf.intros)

  1078 apply(auto)

  1079   done 

  1080     

  1081 lemma LV_FROMNTIMES_3:

  1082   shows "LV (FROMNTIMES r (Suc n)) [] = 

  1083     (\<lambda>(v,vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (FROMNTIMES r n) [])))"

  1084 unfolding LV_def

  1085 apply(auto elim!: Prf_elims simp add: image_def)

  1086 apply(case_tac vs1)

  1087 apply(auto)

  1088 apply(case_tac vs2)

  1089 apply(auto)

  1090 apply(subst append.simps(1)[symmetric])

  1091 apply(rule Prf.intros)

  1092      apply(auto)

  1093   apply (metis le_imp_less_Suc length_greater_0_conv less_antisym list.exhaust list.set_intros(1) not_less_eq zero_le)

  1094   prefer 2

  1095   using nth_mem apply blast

  1096   apply(case_tac vs1)

  1097   apply (smt Groups.add_ac(2) Prf.intros(9) add.right_neutral add_Suc_right append.simps(1) insert_iff length_append list.set(2) list.size(3) list.size(4))

  1098     apply(auto)

  1099 done     

  1100   

  1101 lemma LV_NTIMES_4:

  1102  "LV (NTIMES r n) [] = Stars_Pow (LV r []) n" 

  1103   apply(induct n)

  1104    apply(simp add: LV_def)    

  1105    apply(auto elim!: Prf_elims simp add: image_def)[1]

  1106    apply(subst append.simps[symmetric])

  1107     apply(rule Prf.intros)

  1108       apply(simp_all)

  1109     apply(simp add: LV_NTIMES_3 image_def Stars_Cons_def)

  1110   apply blast

  1111  done   

  1112 

  1113 lemma LV_NTIMES_5:

  1114   "LV (NTIMES r n) s \<subseteq> Stars_Append (LV (STAR r) s) (\<Union>i\<le>n. LV (NTIMES r i) [])"

  1115 apply(auto simp add: LV_def)

  1116 apply(auto elim!: Prf_elims)

  1117   apply(auto simp add: Stars_Append_def)

  1118   apply(rule_tac x="vs1" in exI)

  1119   apply(rule_tac x="vs2" in exI)  

  1120   apply(auto)

  1121     using Prf.intros(6) apply(auto)

  1122       apply(rule_tac x="length vs2" in bexI)

  1123     thm Prf.intros

  1124       apply(subst append.simps(1)[symmetric])

  1125     apply(rule Prf.intros)

  1126       apply(auto)[1]

  1127       apply(auto)[1]

  1128      apply(simp)

  1129     apply(simp)

  1130       done

  1131       

  1132 lemma ttty:

  1133  "LV (FROMNTIMES r n) [] = Stars_Pow (LV r []) n" 

  1134   apply(induct n)

  1135    apply(simp add: LV_def)