112 fun ALTS :: "rexp list \<Rightarrow> rexp"

   113 where 

   114   "ALTS [] = ZERO"

   115 | "ALTS [r] = r"

   116 | "ALTS (r # rs) = ALT r (ALTS rs)"

   117 

   118 fun SEQS :: "rexp list \<Rightarrow> rexp"

   119 where 

   120   "SEQS [] = ONE"

   121 | "SEQS [r] = r"

   122 | "SEQS (r # rs) = SEQ r (SEQS rs)"

   123 

   135 

   136 lemma L_ALTS:

   137   "L (ALTS rs) = (\<Union>r \<in> set rs. L(r))"

   138 by(induct rs rule: ALTS.induct)(simp_all)

   139 

   140 lemma L_SEQS:

   141   "L (SEQS []) = {[]}"

   142   "L (SEQS (r # rs)) = (L r) ;; (L (SEQS rs))"

   143 apply(simp)

   144 apply(case_tac rs)

   145 apply(simp)

   146 apply(simp)

   147 done

   221 

   222 

   223 

   224 definition

   225   delta :: "rexp \<Rightarrow> rexp"

   226 where

   227   "delta r \<equiv> (if nullable r then ONE else ZERO)"

   228 

   229 lemma delta_simp:

   230   shows "nullable r1 \<Longrightarrow> L (SEQ (delta r1) r2) = L r2"

   231   and   "\<not>nullable r1 \<Longrightarrow> L (SEQ (delta r1) r2) = {}"

   232 unfolding delta_def

   233 by simp_all

   234 

   235 fun str_split :: "string \<Rightarrow> string \<Rightarrow> (string * string) list"

   236 where

   237   "str_split s1 [] = []"

   238 | "str_split s1 [c] = [(s1, [c])]"

   239 | "str_split s1 (c#s2) = (s1, c#s2) # str_split (s1 @ [c]) s2"

   240 

   241 fun ssplit :: "string \<Rightarrow> (string * string) list"

   242 where

   243   "ssplit s = rev (str_split [] s)"  

   244 

   245 fun tsplit :: "string \<Rightarrow> (string * string) list"

   246 where

   247   "tsplit s = tl (str_split [] s)" 

   248 

   249 

   250 value "ssplit([])"

   251 value "ssplit([a1])"

   252 value "ssplit([a1, a2])"

   253 value "ssplit([a1, a2, a3])"

   254 value "ssplit([a1, a2, a3, a4])"

   255 

   256 value "tsplit([])"

   257 value "tsplit([a1])"

   258 value "tsplit([a1, a2])"

   259 value "tsplit([a1, a2, a3])"

   260 value "tsplit([a1, a2, a3, a4])"

   261 

   262 function

   263   D :: "string \<Rightarrow> rexp \<Rightarrow> rexp" 

   264 where

   265   "D s (ZERO) = ZERO"

   266 | "D s (ONE) = (if s = [] then ONE else ZERO)"

   267 | "D s (CHAR c) = (if s = [c] then ONE else 

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

   269 | "D s (ALT r1 r2) = ALT (D s r1) (D s r2)"

   270 | "D s (SEQ r1 r2) = ALTS ((SEQ (D s r1) r2) # [SEQ (delta (D s1 r1)) (D s2 r2). (s1, s2) \<leftarrow> (ssplit s)])"

   271 | "D [] (STAR r) = STAR r"

   272 | "D (c#s) (STAR r) = ALTS (SEQ (D (c#s) r) (STAR r) # 

   273       [SEQS ((map (\<lambda>c. delta (D [c] r)) s1) @ [D s2 (STAR r)]). (s1, s2) \<leftarrow> (tsplit (c#s))])"

   274 sorry

   275 

   276 termination sorry

   277 

   278 thm D.simps

   279 thm tl_def

   280 

   281 lemma D_Nil:

   282   shows "D [] r = r"

   283 apply(induct r)

   284 apply(simp_all)

   285 done

   286 

   287 lemma D_ALTS:

   288   shows "D s (ALTS rs) = ALTS [D s r. r \<leftarrow> rs]"

   289 apply(induct rs rule: ALTS.induct)

   290 apply(simp_all)

   291 done

   292 

   293 (*

   294 lemma 

   295   "D [a] (SEQ E F) = ALT (SEQ (D [a] E) F) (SEQ (delta E) (D [a] F))"

   296 apply(simp add: D_Nil)

   297 done

   298 

   299 lemma 

   300   "D [a1, a2] (SEQ E F) = ALT (SEQ (D [a1, a2] E) F)

   301      (ALT (SEQ (delta (D [a1] E)) (D [a2] F)) (SEQ (delta E) (D [a1, a2] F)))"

   302 apply(simp add: D_Nil)

   303 done

   304 *)

   305 (*

   306 lemma D_Der1:

   307   shows "L(D [c] r) = L(der c r)"

   308 apply(induct r)

   309 apply(simp)

   310 apply(simp)

   311 apply(simp)

   312 prefer 2

   313 apply(simp)

   314 apply(simp)

   315 apply(auto)[1]

   316 apply(simp add: D_Nil)

   317 apply(simp add: delta_def)

   318 apply(simp add: D_Nil)

   319 apply(simp add: delta_def)

   320 apply(simp add: D_Nil)

   321 apply(simp add: delta_def)

   322 apply(simp)

   323 done

   324 

   325 lemma D_Der2:

   326   shows "L(D [a1, a2] r) = L(der a2 (der a1 r))"

   327 apply(induct r)

   328 apply(simp)

   329 apply(simp)

   330 apply(simp)

   331 prefer 2

   332 apply(simp)

   333 apply(simp)

   334 apply(auto)[1]

   335 apply(simp add: delta_def)

   336 apply(auto split: if_splits)[1]

   337 apply(simp add: der_correctness Der_def D_Der1 D_Nil)

   338 apply(simp add: der_correctness Der_def D_Der1 D_Nil)

   339 apply (simp add: delta_def)

   340 apply(simp add: der_correctness Der_def D_Der1 D_Nil)

   341 apply (simp add: D_Der1 delta_def nullable_correctness)

   342 apply (simp add: D_Der1 delta_def nullable_correctness)

   343 apply(simp add: der_correctness Der_def D_Der1 D_Nil)

   344 apply(simp add: der_correctness Der_def D_Der1 D_Nil)

   345 apply (simp add: D_Der1 delta_def nullable_correctness)

   346 apply(simp add: D_Der1 D_Nil delta_def)

   347 apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)

   348 apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)

   349 apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)

   350 apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)

   351 apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)

   352 apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)

   353 apply(auto)[1]

   354 apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)

   355 apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)

   356 apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)

   357 done

   358 

   359 lemma D_Der3:

   360   shows "L(D [a1, a2, a3] r) = L(ders [a1, a2, a3] r)"

   361 apply(induct r)

   362 apply(simp)

   363 apply(simp)

   364 apply(simp)

   365 prefer 2

   366 apply(simp)

   367 apply(simp)

   368 apply(auto)[1]

   369 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   370 apply (simp add: D_Der2 delta_def nullable_correctness)

   371 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   372 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   373 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   374 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   375 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   376 apply (simp add: D_Der2 delta_def nullable_correctness)

   377 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   378 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   379 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   380 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   381 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   382 apply (simp add: D_Der2 delta_def nullable_correctness)

   383 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   384 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   385 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   386 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   387 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   388 apply (simp add: D_Der2 delta_def nullable_correctness)

   389 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   390 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   391 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   392 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   393 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   394 apply (simp add: D_Der2 delta_def nullable_correctness)

   395 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   396 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   397 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   398 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   399 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   400 apply (simp add: D_Der2 delta_def nullable_correctness)

   401 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   402 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   403 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   404 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   405 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   406 apply (simp add: D_Der2 delta_def nullable_correctness)

   407 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   408 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   409 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   410 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   411 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   412 apply (simp add: D_Der2 delta_def nullable_correctness)

   413 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   414 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   415 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   416 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   417 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   418 apply (simp add: D_Der2 delta_def nullable_correctness)

   419 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   420 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   421 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   422 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   423 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   424 apply (simp add: D_Der2 delta_def nullable_correctness)

   425 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   426 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   427 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   428 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   429 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   430 apply (simp add: D_Der2 delta_def nullable_correctness)

   431 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   432 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   433 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   434 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   435 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   436 apply (simp add: D_Der2 delta_def nullable_correctness)

   437 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   438 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   439 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   440 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   441 (* star case *)

   442 apply(simp)

   443 apply(auto)[1]

   444 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   445 apply (simp add: D_Der2 delta_def nullable_correctness)

   446 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   447 apply (simp add: D_Der2 delta_def nullable_correctness)

   448 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   449 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   450 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   451 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   452 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   453 apply (simp add: D_Der2 delta_def nullable_correctness)

   454 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   455 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   456 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   457 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   458 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   459 apply (simp add: D_Der2 delta_def nullable_correctness)

   460 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   461 apply(simp add: Sequ_def)

   462 apply(auto)[1]

   463 defer

   464 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   465 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   466 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   467 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   468 apply (simp add: D_Der2 delta_def nullable_correctness)

   469 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   470 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   471 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   472 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   473 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   474 apply (simp add: D_Der2 delta_def nullable_correctness)

   475 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   476 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   477 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   478 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   479 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   480 apply (simp add: D_Der2 delta_def nullable_correctness)

   481 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   482 defer

   483 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   484 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   485 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   486 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   487 apply (simp add: D_Der2 delta_def nullable_correctness)

   488 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   489 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   490 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   491 defer

   492 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   493 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   494 apply (simp add: D_Der2 delta_def nullable_correctness)

   495 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   496 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   497 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   498 apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)

   499 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   500 apply (simp add: D_Der2 delta_def nullable_correctness)

   501 apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)

   502 defer

   503 done

   504 

   505 lemma D_Ders:

   506   shows "L (D (s1 @ s2) r) = L (D s2 (D s1 r))"

   507 apply(induct r arbitrary: s1 s2)

   508 apply(simp)

   509 apply(simp)

   510 apply(simp)

   511 apply(auto)[1]

   512 apply (metis Cons_eq_append_conv append_is_Nil_conv)

   513 apply(simp)

   514 apply(auto)[1]

   515 apply(simp add: L_ALTS D_ALTS)

   516 apply(auto)[1]

   517 apply(simp add: L_ALTS)

   518 oops

   519 

   520 

   521 lemma D_cons:

   522   shows "L (D (c # s) r) = L (D s (der c r))"

   523 apply(induct r arbitrary: c s)

   524 apply(simp)

   525 apply(simp)

   526 apply(simp)

   527 apply(simp)

   528 apply(auto)[1]

   529 sorry

   530 

   531 lemma D_Zero:

   532   shows "lang (D s Zero) = lang (derivs s Zero)"

   533 by (induct s) (simp_all)

   534 

   535 lemma D_One:

   536   shows "lang (D s One) = lang (derivs s One)"

   537 by (induct s) (simp_all add: D_Zero[symmetric])

   538 

   539 lemma D_Atom:

   540   shows "lang (D s (Atom c)) = lang (derivs s (Atom c))"

   541 by (induct s) (simp_all add: D_Zero[symmetric] D_One[symmetric])

   542 

   543 lemma D_Plus:

   544   shows "lang (D s (Plus r1 r2)) = lang (derivs s (Plus r1 r2))"

   545 by (induct s arbitrary: r1 r2) (simp_all add: D_empty D_cons)

   546 

   547 lemma D_Times:

   548   shows "lang (D s (Times r1 r2)) = lang (derivs s (Times r1 r2))"

   549 apply(induct s arbitrary: r1 r2) 

   550 apply(simp_all add: D_empty D_cons)

   551 apply(auto simp add: conc_def)[1]

   552 apply(simp only: D_Plus[symmetric])

   553 apply(simp only: D.simps)

   554 apply(simp)

   555 *)

   556