1    

     2 theory LexerExt

     3   imports Main

     4 begin

     5 

     6 

     7 section {* Sequential Composition of Languages *}

     8 

     9 definition

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

    11 where 

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

    13 

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

    15 

    16 lemma seq_empty [simp]:

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

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

    19 by (simp_all add: Sequ_def)

    20 

    21 lemma seq_null [simp]:

    22   shows "A ;; {} = {}"

    23   and   "{} ;; A = {}"

    24 by (simp_all add: Sequ_def)

    25 

    26 lemma seq_assoc: 

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

    28 apply(auto simp add: Sequ_def)

    29 apply(metis append_assoc)

    30 apply(metis)

    31 done

    32 

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

    34 

    35 definition

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

    37 where

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

    39 

    40 definition

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

    42 where

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

    44 

    45 lemma Der_null [simp]:

    46   shows "Der c {} = {}"

    47 unfolding Der_def

    48 by auto

    49 

    50 lemma Der_empty [simp]:

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

    52 unfolding Der_def

    53 by auto

    54 

    55 lemma Der_char [simp]:

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

    57 unfolding Der_def

    58 by auto

    59 

    60 lemma Der_union [simp]:

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

    62 unfolding Der_def

    63 by auto

    64 

    65 lemma Der_Sequ [simp]:

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

    67 unfolding Der_def Sequ_def

    68 by (auto simp add: Cons_eq_append_conv)

    69 

    70 lemma Der_UNION: 

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

    72 by (auto simp add: Der_def)

    73 

    74 

    75 section {* Power operation for Sets *}

    76 

    77 fun 

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

    79 where

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

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

    82 

    83 lemma Pow_empty [simp]:

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

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

    86 

    87 lemma Pow_plus:

    88   "A \<up> (n + m) = A \<up> n ;; A \<up> m"

    89 by (induct n) (simp_all add: seq_assoc)

    90 

    91 

    92 section {* Kleene Star for Languages *}

    93 

    94 inductive_set

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

    96   for A :: "string set"

    97 where

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

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

   100 

   101 lemma star_cases:

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

   103 unfolding Sequ_def

   104 by (auto) (metis Star.simps)

   105 

   106 lemma star_decomp: 

   107   assumes a: "c # x \<in> A\<star>" 

   108   shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"

   109 using a

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

   111    (auto simp add: append_eq_Cons_conv)

   112 

   113 lemma Der_star [simp]:

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

   115 proof -    

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

   117     by (simp only: star_cases[symmetric])

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

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

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

   121     by simp

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

   123     unfolding Sequ_def Der_def

   124     by (auto dest: star_decomp)

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

   126 qed

   127 

   128 lemma Star_in_Pow:

   129   assumes a: "s \<in> A\<star>"

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

   131 using a

   132 apply(induct)

   133 apply(auto)

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

   135 apply(auto simp add: Sequ_def)

   136 done

   137 

   138 lemma Pow_in_Star:

   139   assumes a: "s \<in> A \<up> n"

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

   141 using a

   142 by (induct n arbitrary: s) (auto simp add: Sequ_def)

   143 

   144 

   145 lemma Star_def2: 

   146   shows "A\<star> = (\<Union>n. A \<up> n)"

   147 using Star_in_Pow Pow_in_Star

   148 by (auto)

   149 

   150 

   151 section {* Regular Expressions *}

   152 

   153 datatype rexp =

   154   ZERO

   155 | ONE

   156 | CHAR char

   157 | SEQ rexp rexp

   158 | ALT rexp rexp

   159 | STAR rexp

   160 | UPNTIMES rexp nat

   161 

   162 section {* Semantics of Regular Expressions *}

   163  

   164 fun

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

   166 where

   167   "L (ZERO) = {}"

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

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

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

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

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

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

   174 

   175 

   176 section {* Nullable, Derivatives *}

   177 

   178 fun

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

   180 where

   181   "nullable (ZERO) = False"

   182 | "nullable (ONE) = True"

   183 | "nullable (CHAR c) = False"

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

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

   186 | "nullable (STAR r) = True"

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

   188 

   189 fun

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

   191 where

   192   "der c (ZERO) = ZERO"

   193 | "der c (ONE) = ZERO"

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

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

   196 | "der c (SEQ r1 r2) = 

   197      (if nullable r1

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

   199       else SEQ (der c r1) r2)"

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

   201 | "der c (UPNTIMES r 0) = ZERO"

   202 | "der c (UPNTIMES r (Suc n)) = SEQ (der c r) (UPNTIMES r n)"

   203 

   204 

   205 fun 

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

   207 where

   208   "ders [] r = r"

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

   210 

   211 

   212 lemma nullable_correctness:

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

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

   215 

   216 lemma Suc_reduce_Union:

   217   "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))"

   218 by (metis UN_extend_simps(10) image_Suc_atLeastAtMost)

   219 

   220 lemma Suc_reduce_Union2:

   221   "(\<Union>x\<in>{Suc n..}. B x) = (\<Union>x\<in>{n..}. B (Suc x))"

   222 apply(auto)

   223 apply(rule_tac x="xa - 1" in bexI)

   224 apply(simp)

   225 apply(simp)

   226 done

   227 

   228 lemma Seq_UNION: 

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

   230 by (auto simp add: Sequ_def)

   231 

   232 lemma Seq_Union:

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

   234 by (auto simp add: Sequ_def)

   235 

   236 lemma Der_Pow [simp]:

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

   238      (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})"

   239 unfolding Der_def Sequ_def 

   240 by(auto simp add: Cons_eq_append_conv Sequ_def)

   241 

   242 lemma Suc_Union:

   243   "(\<Union>x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union>x\<le>m. B x))"

   244 by (metis UN_insert atMost_Suc)

   245 

   246 

   247 lemma test:

   248   shows "(\<Union>x\<le>Suc n. Der c (L r \<up> x)) = (\<Union>x\<le>n. Der c (L r) ;; L r \<up> x)"

   249 apply(induct n)

   250 apply(simp)

   251 apply(auto)[1]

   252 apply(case_tac xa)

   253 apply(simp)

   254 apply(simp)

   255 apply(auto)[1]

   256 apply(case_tac "[] \<in> L r")

   257 apply(simp)

   258 apply(simp)

   259 by (smt Der_Pow Suc_Union inf_sup_aci(5) inf_sup_aci(7) sup_idem)

   260 

   261 

   262 lemma der_correctness:

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

   264 apply(induct c r rule: der.induct) 

   265 apply(simp_all add: nullable_correctness)[7]

   266 apply(simp only: der.simps L.simps)

   267 apply(simp only: Der_UNION)

   268 apply(simp only: Seq_UNION[symmetric])

   269 apply(simp add: test)

   270 done

   271 

   272 

   273 lemma ders_correctness:

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

   275 apply(induct s arbitrary: r)

   276 apply(simp_all add: Ders_def der_correctness Der_def)

   277 done

   278 

   279 lemma ders_ZERO:

   280   shows "ders s (ZERO) = ZERO"

   281 apply(induct s)

   282 apply(simp_all)

   283 done

   284 

   285 lemma ders_ONE:

   286   shows "ders s (ONE) = (if s = [] then ONE else ZERO)"

   287 apply(induct s)

   288 apply(simp_all add: ders_ZERO)

   289 done

   290 

   291 lemma ders_CHAR:

   292   shows "ders s (CHAR c) = (if s = [c] then ONE else 

   293                            (if s = [] then (CHAR c) else ZERO))"

   294 apply(induct s)

   295 apply(simp_all add: ders_ZERO ders_ONE)

   296 done

   297 

   298 lemma  ders_ALT:

   299   shows "ders s (ALT r1 r2) = ALT (ders s r1) (ders s r2)"

   300 apply(induct s arbitrary: r1 r2)

   301 apply(simp_all)

   302 done

   303 

   304 section {* Values *}

   305 

   306 datatype val = 

   307   Void

   308 | Char char

   309 | Seq val val

   310 | Right val

   311 | Left val

   312 | Stars "val list"

   313 

   314 

   315 section {* The string behind a value *}

   316 

   317 fun 

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

   319 where

   320   "flat (Void) = []"

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

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

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

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

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

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

   327 

   328 lemma flat_Stars [simp]:

   329  "flat (Stars vs) = concat (map flat vs)"

   330 by (induct vs) (auto)

   331 

   332 

   333 section {* Relation between values and regular expressions *}

   334 

   335 inductive 

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

   337 where

   338  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"

   339 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"

   340 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"

   341 | "\<turnstile> Void : ONE"

   342 | "\<turnstile> Char c : CHAR c"

   343 | "\<turnstile> Stars [] : STAR r"

   344 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"

   345 | "\<turnstile> Stars [] : UPNTIMES r 0"

   346 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : UPNTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : UPNTIMES r (Suc n)"

   347 | "\<lbrakk>\<turnstile> Stars vs : UPNTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r (Suc n)"

   348 

   349 

   350 

   351 inductive_cases Prf_elims:

   352   "\<turnstile> v : ZERO"

   353   "\<turnstile> v : SEQ r1 r2"

   354   "\<turnstile> v : ALT r1 r2"

   355   "\<turnstile> v : ONE"

   356   "\<turnstile> v : CHAR c"

   357 (*  "\<turnstile> vs : STAR r"*)

   358 

   359 lemma Prf_flat_L:

   360   assumes "\<turnstile> v : r" shows "flat v \<in> L r"

   361 using assms

   362 apply(induct v r rule: Prf.induct)

   363 apply(auto simp add: Sequ_def)

   364 apply(rotate_tac 2)

   365 apply(rule_tac x="Suc x" in bexI)

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

   367 done

   368 

   369 lemma Prf_Stars:

   370   assumes "\<forall>v \<in> set vs. \<turnstile> v : r"

   371   shows "\<turnstile> Stars vs : STAR r"

   372 using assms

   373 by(induct vs) (auto intro: Prf.intros)

   374 

   375 lemma Prf_Stars_UPNTIMES:

   376   assumes "\<forall>v \<in> set vs. \<turnstile> v : r" "(length vs) = n"

   377   shows "\<turnstile> Stars vs : UPNTIMES r n"

   378 using assms

   379 apply(induct vs arbitrary: n) 

   380 apply(auto intro: Prf.intros)

   381 done

   382 

   383 lemma Prf_UPNTIMES_bigger:

   384   assumes "\<turnstile> Stars vs : UPNTIMES r n" "n \<le> m" 

   385   shows "\<turnstile> Stars vs : UPNTIMES r m"

   386 using assms

   387 apply(induct m arbitrary:)

   388 apply(auto)

   389 using Prf.intros(10) le_Suc_eq by blast

   390 

   391 lemma UPNTIMES_Stars:

   392  assumes "\<turnstile> v : UPNTIMES r n"

   393  shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs \<le> n"

   394 using assms

   395 apply(induct n arbitrary: v)

   396 apply(erule Prf.cases)

   397 apply(simp_all)

   398 apply(erule Prf.cases)

   399 apply(simp_all)

   400 apply(auto)

   401 using le_SucI by blast

   402 

   403 lemma Star_string:

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

   405   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"

   406 using assms

   407 apply(induct rule: Star.induct)

   408 apply(auto)

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

   410 apply(simp)

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

   412 apply(simp)

   413 done

   414 

   415 lemma Star_val:

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

   417   shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"

   418 using assms

   419 apply(induct ss)

   420 apply(auto)

   421 apply (metis empty_iff list.set(1))

   422 by (metis concat.simps(2) list.simps(9) set_ConsD)

   423 

   424 lemma Star_val_length:

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

   426   shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r) \<and> (length vs) = (length ss)"

   427 using assms

   428 apply(induct ss)

   429 apply(auto)

   430 by (metis List.bind_def bind_simps(2) length_Suc_conv set_ConsD)

   431 

   432 

   433 lemma Star_Pow:

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

   435   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A) \<and> (length ss = n)"

   436 using assms

   437 apply(induct n arbitrary: s)

   438 apply(auto simp add: Sequ_def)

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

   440 apply(auto)

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

   442 apply(simp)

   443 done

   444 

   445 lemma L_flat_Prf1:

   446   assumes "\<turnstile> v : r" shows "flat v \<in> L r"

   447 using assms

   448 apply(induct)

   449 apply(auto simp add: Sequ_def)

   450 apply(rule_tac x="Suc x" in bexI)

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

   452 done

   453 

   454 lemma L_flat_Prf2:

   455   assumes "s \<in> L r" shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"

   456 using assms

   457 apply(induct r arbitrary: s)

   458 apply(auto simp add: Sequ_def intro: Prf.intros)

   459 using Prf.intros(1) flat.simps(5) apply blast

   460 using Prf.intros(2) flat.simps(3) apply blast

   461 using Prf.intros(3) flat.simps(4) apply blast

   462 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)")

   463 apply(auto)[1]

   464 apply(rule_tac x="Stars vs" in exI)

   465 apply(simp)

   466 apply (simp add: Prf_Stars)

   467 apply(drule Star_string)

   468 apply(auto)

   469 apply(rule Star_val)

   470 apply(auto)

   471 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)")

   472 apply(auto)[1]

   473 apply(rule_tac x="Stars vs" in exI)

   474 apply(simp)

   475 apply(drule_tac n="length vs" in Prf_Stars_UPNTIMES)

   476 apply(simp)

   477 using Prf_UPNTIMES_bigger apply blast

   478 apply(drule Star_Pow)

   479 apply(auto)

   480 using Star_val_length by blast

   481 

   482 lemma L_flat_Prf:

   483   "L(r) = {flat v | v. \<turnstile> v : r}"

   484 using L_flat_Prf1 L_flat_Prf2 by blast

   485 

   486 

   487 section {* Sulzmann and Lu functions *}

   488 

   489 fun 

   490   mkeps :: "rexp \<Rightarrow> val"

   491 where

   492   "mkeps(ONE) = Void"

   493 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"

   494 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"

   495 | "mkeps(STAR r) = Stars []"

   496 | "mkeps(UPNTIMES r n) = Stars []"

   497 

   498 

   499 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"

   500 where

   501   "injval (CHAR d) c Void = Char d"

   502 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"

   503 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"

   504 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"

   505 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"

   506 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"

   507 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" 

   508 | "injval (UPNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"

   509 

   510 section {* Mkeps, injval *}

   511 

   512 lemma mkeps_nullable:

   513   assumes "nullable(r)" 

   514   shows "\<turnstile> mkeps r : r"

   515 using assms

   516 apply(induct rule: nullable.induct) 

   517 apply(auto intro: Prf.intros)

   518 using Prf.intros(8) Prf_UPNTIMES_bigger by blast

   519 

   520 

   521 lemma mkeps_flat:

   522   assumes "nullable(r)" 

   523   shows "flat (mkeps r) = []"

   524 using assms

   525 by (induct rule: nullable.induct) (auto)

   526 

   527 

   528 lemma Prf_injval:

   529   assumes "\<turnstile> v : der c r" 

   530   shows "\<turnstile> (injval r c v) : r"

   531 using assms

   532 apply(induct r arbitrary: c v rule: rexp.induct)

   533 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)

   534 (* STAR *)

   535 apply(rotate_tac 2)

   536 apply(erule Prf.cases)

   537 apply(simp_all)[7]

   538 apply(auto)

   539 apply (metis Prf.intros(6) Prf.intros(7))

   540 apply (metis Prf.intros(7))

   541 (* UPNTIMES *)

   542 apply(case_tac x2)

   543 apply(simp)

   544 using Prf_elims(1) apply auto[1]

   545 apply(simp)

   546 apply(erule Prf.cases)

   547 apply(simp_all)

   548 apply(clarify)

   549 apply(drule UPNTIMES_Stars)

   550 apply(clarify)

   551 apply(simp)

   552 apply(rule Prf.intros(9))

   553 apply(simp)

   554 using Prf_Stars_UPNTIMES Prf_UPNTIMES_bigger by blast

   555 

   556 lemma Prf_injval_flat:

   557   assumes "\<turnstile> v : der c r" 

   558   shows "flat (injval r c v) = c # (flat v)"

   559 using assms

   560 apply(induct arbitrary: v rule: der.induct)

   561 apply(auto elim!: Prf_elims split: if_splits)

   562 apply(metis mkeps_flat)

   563 apply(rotate_tac 2)

   564 apply(erule Prf.cases)

   565 apply(simp_all)

   566 apply(drule UPNTIMES_Stars)

   567 apply(clarify)

   568 apply(simp)

   569 done

   570 

   571 

   572 

   573 section {* Our Alternative Posix definition *}

   574 

   575 inductive 

   576   Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)

   577 where

   578   Posix_ONE: "[] \<in> ONE \<rightarrow> Void"

   579 | Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)"

   580 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"

   581 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"

   582 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;

   583     \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> 

   584     (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"

   585 | Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];

   586     \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>

   587     \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"

   588 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []"

   589 | Posix_UPNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> UPNTIMES r n \<rightarrow> Stars vs; flat v \<noteq> [];

   590     \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r n))\<rbrakk>

   591     \<Longrightarrow> (s1 @ s2) \<in> UPNTIMES r (Suc n) \<rightarrow> Stars (v # vs)"

   592 | Posix_UPNTIMES2: "[] \<in> UPNTIMES r n \<rightarrow> Stars []"

   593 

   594 

   595 inductive_cases Posix_elims:

   596   "s \<in> ZERO \<rightarrow> v"

   597   "s \<in> ONE \<rightarrow> v"

   598   "s \<in> CHAR c \<rightarrow> v"

   599   "s \<in> ALT r1 r2 \<rightarrow> v"

   600   "s \<in> SEQ r1 r2 \<rightarrow> v"

   601   "s \<in> STAR r \<rightarrow> v"

   602 

   603 lemma Posix1:

   604   assumes "s \<in> r \<rightarrow> v"

   605   shows "s \<in> L r" "flat v = s"

   606 using assms

   607 apply (induct s r v rule: Posix.induct)

   608 apply(auto simp add: Sequ_def)

   609 apply(rule_tac x="Suc x" in bexI)

   610 apply(auto simp add: Sequ_def)

   611 done

   612 

   613 

   614 lemma Posix1a:

   615   assumes "s \<in> r \<rightarrow> v"

   616   shows "\<turnstile> v : r"

   617 using assms

   618 apply(induct s r v rule: Posix.induct)

   619 apply(auto intro: Prf.intros)

   620 using Prf.intros(8) Prf_UPNTIMES_bigger by blast

   621 

   622 

   623 lemma Posix_mkeps:

   624   assumes "nullable r"

   625   shows "[] \<in> r \<rightarrow> mkeps r"

   626 using assms

   627 apply(induct r rule: nullable.induct)

   628 apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def)

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

   630 apply(rule Posix.intros)

   631 apply(auto)

   632 done

   633 

   634 

   635 lemma Posix_determ:

   636   assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"

   637   shows "v1 = v2"

   638 using assms

   639 proof (induct s r v1 arbitrary: v2 rule: Posix.induct)

   640   case (Posix_ONE v2)

   641   have "[] \<in> ONE \<rightarrow> v2" by fact

   642   then show "Void = v2" by cases auto

   643 next 

   644   case (Posix_CHAR c v2)

   645   have "[c] \<in> CHAR c \<rightarrow> v2" by fact

   646   then show "Char c = v2" by cases auto

   647 next 

   648   case (Posix_ALT1 s r1 v r2 v2)

   649   have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact

   650   moreover

   651   have "s \<in> r1 \<rightarrow> v" by fact

   652   then have "s \<in> L r1" by (simp add: Posix1)

   653   ultimately obtain v' where eq: "v2 = Left v'" "s \<in> r1 \<rightarrow> v'" by cases auto 

   654   moreover

   655   have IH: "\<And>v2. s \<in> r1 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact

   656   ultimately have "v = v'" by simp

   657   then show "Left v = v2" using eq by simp

   658 next 

   659   case (Posix_ALT2 s r2 v r1 v2)

   660   have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact

   661   moreover

   662   have "s \<notin> L r1" by fact

   663   ultimately obtain v' where eq: "v2 = Right v'" "s \<in> r2 \<rightarrow> v'" 

   664     by cases (auto simp add: Posix1) 

   665   moreover

   666   have IH: "\<And>v2. s \<in> r2 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact

   667   ultimately have "v = v'" by simp

   668   then show "Right v = v2" using eq by simp

   669 next

   670   case (Posix_SEQ s1 r1 v1 s2 r2 v2 v')

   671   have "(s1 @ s2) \<in> SEQ r1 r2 \<rightarrow> v'" 

   672        "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2"

   673        "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact+

   674   then obtain v1' v2' where "v' = Seq v1' v2'" "s1 \<in> r1 \<rightarrow> v1'" "s2 \<in> r2 \<rightarrow> v2'"

   675   apply(cases) apply (auto simp add: append_eq_append_conv2)

   676   using Posix1(1) by fastforce+

   677   moreover

   678   have IHs: "\<And>v1'. s1 \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'"

   679             "\<And>v2'. s2 \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+

   680   ultimately show "Seq v1 v2 = v'" by simp

   681 next

   682   case (Posix_STAR1 s1 r v s2 vs v2)

   683   have "(s1 @ s2) \<in> STAR r \<rightarrow> v2" 

   684        "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" "flat v \<noteq> []"

   685        "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact+

   686   then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')"

   687   apply(cases) apply (auto simp add: append_eq_append_conv2)

   688   using Posix1(1) apply fastforce

   689   apply (metis Posix1(1) Posix_STAR1.hyps(6) append_Nil append_Nil2)

   690   using Posix1(2) by blast

   691   moreover

   692   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"

   693             "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+

   694   ultimately show "Stars (v # vs) = v2" by auto

   695 next

   696   case (Posix_STAR2 r v2)

   697   have "[] \<in> STAR r \<rightarrow> v2" by fact

   698   then show "Stars [] = v2" by cases (auto simp add: Posix1)

   699 next

   700   case (Posix_UPNTIMES1 s1 r v s2 n vs v2)

   701   have "(s1 @ s2) \<in> UPNTIMES r (Suc n) \<rightarrow> v2" 

   702        "s1 \<in> r \<rightarrow> v" "s2 \<in> (UPNTIMES r n) \<rightarrow> Stars vs" "flat v \<noteq> []"

   703        "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r n))" by fact+

   704   then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (UPNTIMES r n) \<rightarrow> (Stars vs')"

   705   apply(cases) apply (auto simp add: append_eq_append_conv2)

   706   using Posix1(1) apply fastforce

   707   apply (metis Posix1(1) Posix_UPNTIMES1.hyps(6) append_Nil append_Nil2)

   708   using Posix1(2) by blast

   709   moreover

   710   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"

   711             "\<And>v2. s2 \<in> UPNTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+

   712   ultimately show "Stars (v # vs) = v2" by auto

   713 next

   714   case (Posix_UPNTIMES2 r n v2)

   715   have "[] \<in> UPNTIMES r n \<rightarrow> v2" by fact

   716   then show "Stars [] = v2" by cases (auto simp add: Posix1)

   717 qed

   718 

   719 

   720 lemma Posix_injval:

   721   assumes "s \<in> (der c r) \<rightarrow> v"

   722   shows "(c # s) \<in> r \<rightarrow> (injval r c v)"

   723 using assms

   724 proof(induct r arbitrary: s v rule: rexp.induct)

   725   case ZERO

   726   have "s \<in> der c ZERO \<rightarrow> v" by fact

   727   then have "s \<in> ZERO \<rightarrow> v" by simp

   728   then have "False" by cases

   729   then show "(c # s) \<in> ZERO \<rightarrow> (injval ZERO c v)" by simp

   730 next

   731   case ONE

   732   have "s \<in> der c ONE \<rightarrow> v" by fact

   733   then have "s \<in> ZERO \<rightarrow> v" by simp

   734   then have "False" by cases

   735   then show "(c # s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp

   736 next 

   737   case (CHAR d)

   738   consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast

   739   then show "(c # s) \<in> (CHAR d) \<rightarrow> (injval (CHAR d) c v)"

   740   proof (cases)

   741     case eq

   742     have "s \<in> der c (CHAR d) \<rightarrow> v" by fact

   743     then have "s \<in> ONE \<rightarrow> v" using eq by simp

   744     then have eqs: "s = [] \<and> v = Void" by cases simp

   745     show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" using eq eqs 

   746     by (auto intro: Posix.intros)

   747   next

   748     case ineq

   749     have "s \<in> der c (CHAR d) \<rightarrow> v" by fact

   750     then have "s \<in> ZERO \<rightarrow> v" using ineq by simp

   751     then have "False" by cases

   752     then show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" by simp

   753   qed

   754 next

   755   case (ALT r1 r2)

   756   have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact

   757   have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact

   758   have "s \<in> der c (ALT r1 r2) \<rightarrow> v" by fact

   759   then have "s \<in> ALT (der c r1) (der c r2) \<rightarrow> v" by simp

   760   then consider (left) v' where "v = Left v'" "s \<in> der c r1 \<rightarrow> v'" 

   761               | (right) v' where "v = Right v'" "s \<notin> L (der c r1)" "s \<in> der c r2 \<rightarrow> v'" 

   762               by cases auto

   763   then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v"

   764   proof (cases)

   765     case left

   766     have "s \<in> der c r1 \<rightarrow> v'" by fact

   767     then have "(c # s) \<in> r1 \<rightarrow> injval r1 c v'" using IH1 by simp

   768     then have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Left v')" by (auto intro: Posix.intros)

   769     then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using left by simp

   770   next 

   771     case right

   772     have "s \<notin> L (der c r1)" by fact

   773     then have "c # s \<notin> L r1" by (simp add: der_correctness Der_def)

   774     moreover 

   775     have "s \<in> der c r2 \<rightarrow> v'" by fact

   776     then have "(c # s) \<in> r2 \<rightarrow> injval r2 c v'" using IH2 by simp

   777     ultimately have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Right v')" 

   778       by (auto intro: Posix.intros)

   779     then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using right by simp

   780   qed

   781 next

   782   case (SEQ r1 r2)

   783   have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact

   784   have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact

   785   have "s \<in> der c (SEQ r1 r2) \<rightarrow> v" by fact

   786   then consider 

   787         (left_nullable) v1 v2 s1 s2 where 

   788         "v = Left (Seq v1 v2)"  "s = s1 @ s2" 

   789         "s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "nullable r1" 

   790         "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)"

   791       | (right_nullable) v1 s1 s2 where 

   792         "v = Right v1" "s = s1 @ s2"  

   793         "s \<in> der c r2 \<rightarrow> v1" "nullable r1" "s1 @ s2 \<notin> L (SEQ (der c r1) r2)"

   794       | (not_nullable) v1 v2 s1 s2 where

   795         "v = Seq v1 v2" "s = s1 @ s2" 

   796         "s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "\<not>nullable r1" 

   797         "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)"

   798         by (force split: if_splits elim!: Posix_elims simp add: Sequ_def der_correctness Der_def)   

   799   then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" 

   800     proof (cases)

   801       case left_nullable

   802       have "s1 \<in> der c r1 \<rightarrow> v1" by fact

   803       then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp

   804       moreover

   805       have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)" by fact

   806       then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def)

   807       ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac Posix.intros)

   808       then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using left_nullable by simp

   809     next

   810       case right_nullable

   811       have "nullable r1" by fact

   812       then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule Posix_mkeps)

   813       moreover

   814       have "s \<in> der c r2 \<rightarrow> v1" by fact

   815       then have "(c # s) \<in> r2 \<rightarrow> (injval r2 c v1)" using IH2 by simp

   816       moreover

   817       have "s1 @ s2 \<notin> L (SEQ (der c r1) r2)" by fact

   818       then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = c # s \<and> [] @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" using right_nullable

   819         by(auto simp add: der_correctness Der_def append_eq_Cons_conv Sequ_def)

   820       ultimately have "([] @ (c # s)) \<in> SEQ r1 r2 \<rightarrow> Seq (mkeps r1) (injval r2 c v1)"

   821       by(rule Posix.intros)

   822       then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using right_nullable by simp

   823     next

   824       case not_nullable

   825       have "s1 \<in> der c r1 \<rightarrow> v1" by fact

   826       then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp

   827       moreover

   828       have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)" by fact

   829       then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def)

   830       ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using not_nullable 

   831         by (rule_tac Posix.intros) (simp_all) 

   832       then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using not_nullable by simp

   833     qed

   834 next

   835   case (STAR r)

   836   have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact

   837   have "s \<in> der c (STAR r) \<rightarrow> v" by fact

   838   then consider

   839       (cons) v1 vs s1 s2 where 

   840         "v = Seq v1 (Stars vs)" "s = s1 @ s2" 

   841         "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)"

   842         "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" 

   843         apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)

   844         apply(rotate_tac 3)

   845         apply(erule_tac Posix_elims(6))

   846         apply (simp add: Posix.intros(6))

   847         using Posix.intros(7) by blast

   848     then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" 

   849     proof (cases)

   850       case cons

   851           have "s1 \<in> der c r \<rightarrow> v1" by fact

   852           then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp

   853         moreover

   854           have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact

   855         moreover 

   856           have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact 

   857           then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)

   858           then have "flat (injval r c v1) \<noteq> []" by simp

   859         moreover 

   860           have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" by fact

   861           then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" 

   862             by (simp add: der_correctness Der_def)

   863         ultimately 

   864         have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros)

   865         then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp)

   866     qed

   867 next 

   868   case (UPNTIMES r n)

   869   have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact

   870   have "s \<in> der c (UPNTIMES r n) \<rightarrow> v" by fact

   871   then consider

   872       (cons) m v1 vs s1 s2 where 

   873         "n = Suc m"

   874         "v = Seq v1 (Stars vs)" "s = s1 @ s2" 

   875         "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (UPNTIMES r m) \<rightarrow> (Stars vs)"

   876         "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (UPNTIMES r m))" 

   877         apply(case_tac n)

   878         apply(simp)

   879         using Posix_elims(1) apply blast

   880         apply(simp)

   881         apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)

   882         by (metis Posix1a UPNTIMES_Stars)

   883     then show "(c # s) \<in> UPNTIMES r n \<rightarrow> injval (UPNTIMES r n) c v" 

   884     proof (cases)

   885       case cons

   886         have "n = Suc m" by fact

   887         moreover

   888           have "s1 \<in> der c r \<rightarrow> v1" by fact

   889           then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp

   890         moreover

   891           have "s2 \<in> UPNTIMES r m \<rightarrow> Stars vs" by fact

   892         moreover 

   893           have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact 

   894           then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)

   895           then have "flat (injval r c v1) \<noteq> []" by simp

   896         moreover 

   897           have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (UPNTIMES r m))" by fact

   898           then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r m))" 

   899             by (simp add: der_correctness Der_def)

   900         ultimately 

   901         have "((c # s1) @ s2) \<in> UPNTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)" 

   902           apply(rule_tac Posix.intros(8))

   903           apply(simp_all)

   904           done

   905         then show "(c # s) \<in> UPNTIMES r n \<rightarrow> injval (UPNTIMES r n) c v" using cons by(simp)

   906     qed

   907 qed

   908 

   909 

   910 section {* The Lexer by Sulzmann and Lu  *}

   911 

   912 fun 

   913   lexer :: "rexp \<Rightarrow> string \<Rightarrow> val option"

   914 where

   915   "lexer r [] = (if nullable r then Some(mkeps r) else None)"

   916 | "lexer r (c#s) = (case (lexer (der c r) s) of  

   917                     None \<Rightarrow> None

   918                   | Some(v) \<Rightarrow> Some(injval r c v))"

   919 

   920 

   921 lemma lexer_correct_None:

   922   shows "s \<notin> L r \<longleftrightarrow> lexer r s = None"

   923 apply(induct s arbitrary: r)

   924 apply(simp add: nullable_correctness)

   925 apply(drule_tac x="der a r" in meta_spec)

   926 apply(auto simp add: der_correctness Der_def)

   927 done

   928 

   929 lemma lexer_correct_Some:

   930   shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"

   931 apply(induct s arbitrary: r)

   932 apply(auto simp add: Posix_mkeps nullable_correctness)[1]

   933 apply(drule_tac x="der a r" in meta_spec)

   934 apply(simp add: der_correctness Der_def)

   935 apply(rule iffI)

   936 apply(auto intro: Posix_injval simp add: Posix1(1))

   937 done 

   938 

   939 lemma lexer_correctness:

   940   shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v"

   941   and   "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)"

   942 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce

   943 using Posix1(1) lexer_correct_None lexer_correct_Some by blast

   944 

   945 

   946 end