10   "L1 ; L2 = {s1@s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"

    10   "L1 ; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"

    36 by (simp add: lang_seq_def Collect_def mem_def expand_fun_eq)

    36 unfolding lang_seq_def

    37    (metis append_assoc)

    37 apply(auto)

    38 apply(metis)

    39 by (metis append_assoc)

   248 definition

   250 

   249   Ls :: "rexp set \<Rightarrow> string set"

   251 (* ************ now is the codes writen by chunhan ************************************* *)

   250 where

   251   "Ls R = (\<Union>r\<in>R. (L r))"

   252 

   253 lemma Ls_union:

   254   "Ls (R1 \<union> R2) = (Ls R1) \<union> (Ls R2)"

   255 unfolding Ls_def by auto

   256 

   257 text {* helper function for termination proofs *}

   258 fun

   259  Left :: "rexp \<Rightarrow> rexp"

   260 where

   261  "Left (SEQ r1 r2) = r1"

   262 

   263 text {* dagger function *}

   264 

   265 function

   266   dagger :: "rexp \<Rightarrow> char \<Rightarrow> rexp list" ("_ \<dagger> _")

   267 where

   268   c1: "(NULL \<dagger> c) = []"

   269 | c2: "(EMPTY) \<dagger> c = []"

   270 | c3: "(CHAR c') \<dagger> c = (if c = c' then [EMPTY] else [])"

   271 | c4: "(ALT r1 r2) \<dagger> c = r1 \<dagger> c @ r2 \<dagger> c"

   272 | c5: "(SEQ NULL r2) \<dagger> c = []" 

   273 | c6: "(SEQ EMPTY r2) \<dagger> c = r2 \<dagger> c" 

   274 | c7: "(SEQ (CHAR c') r2) \<dagger> c = (if c = c' then [r2] else [])"

   275 | c8: "(SEQ (SEQ r11 r12) r2) \<dagger> c = (SEQ r11 (SEQ r12 r2)) \<dagger> c" 

   276 | c9: "(SEQ (ALT r11 r12) r2) \<dagger> c = (SEQ r11 r2) \<dagger> c @ (SEQ r12 r2) \<dagger> c" 

   277 | c10: "(SEQ (STAR r1) r2) \<dagger> c = r2 \<dagger> c @ [SEQ r' (SEQ (STAR r1) r2). r' \<leftarrow> r1 \<dagger> c]" 

   278 | c11: "(STAR r) \<dagger> c = [SEQ r' (STAR r) .  r' \<leftarrow> r \<dagger> c]"

   279 by (pat_completeness) (auto)

   280 

   281 termination dagger

   282   by (relation "measures [\<lambda>(r, c). size r, \<lambda>(r, c). size (Left r)]") (simp_all)

   283 

   284 lemma dagger_correctness:

   285   "Ls (set r \<dagger> c) = {s. c#s \<in> L r}"

   286 proof (induct rule: dagger.induct)

   287   case (1 c)

   288   show "Ls (set NULL \<dagger> c) = {s. c#s \<in> L NULL}" by (simp add: Ls_def)

   289 next  

   290   case (2 c)

   291   show "Ls (set EMPTY \<dagger> c) = {s. c#s \<in> L EMPTY}" by (simp add: Ls_def)

   292 next

   293   case (3 c' c)

   294   show "Ls (set CHAR c' \<dagger> c) = {s. c#s \<in> L (CHAR c')}" by (simp add: Ls_def)

   295 next

   296   case (4 r1 r2 c)

   297   have ih1: "Ls (set r1 \<dagger> c) = {s. c#s \<in> L r1}" by fact

   298   have ih2: "Ls (set r2 \<dagger> c) = {s. c#s \<in> L r2}" by fact

   299   show "Ls (set ALT r1 r2 \<dagger> c) = {s. c#s \<in> L (ALT r1 r2)}"

   300     by (simp add: Ls_union ih1 ih2 Collect_disj_eq)

   301 next

   302   case (5 r2 c)

   303   show "Ls (set SEQ NULL r2 \<dagger> c) = {s. c#s \<in> L (SEQ NULL r2)}" by (simp add: Ls_def lang_seq_null)

   304 next

   305   case (6 r2 c)

   306   have ih: "Ls (set r2 \<dagger> c) = {s. c#s \<in> L r2}" by fact

   307   show "Ls (set SEQ EMPTY r2 \<dagger> c) = {s. c#s \<in> L (SEQ EMPTY r2)}"

   308     by (simp add: ih lang_seq_empty)

   309 next

   310   case (7 c' r2 c)

   311   show "Ls (set SEQ (CHAR c') r2 \<dagger> c) = {s. c#s \<in> L (SEQ (CHAR c') r2)}"

   312     by (simp add: Ls_def lang_seq_def)

   313 next

   314   case (8 r11 r12 r2 c)

   315   have ih: "Ls (set SEQ r11 (SEQ r12 r2) \<dagger> c) = {s. c#s \<in> L (SEQ r11 (SEQ r12 r2))}" by fact

   316   show "Ls (set SEQ (SEQ r11 r12) r2 \<dagger> c) = {s. c#s \<in> L (SEQ (SEQ r11 r12) r2)}"

   317     by (simp add: ih lang_seq_assoc)

   318 next

   319   case (9 r11 r12 r2 c)

   320   have ih1: "Ls (set SEQ r11 r2 \<dagger> c) = {s. c#s \<in> L (SEQ r11 r2)}" by fact

   321   have ih2: "Ls (set SEQ r12 r2 \<dagger> c) = {s. c#s \<in> L (SEQ r12 r2)}" by fact

   322   show "Ls (set SEQ (ALT r11 r12) r2 \<dagger> c) = {s. c#s \<in> L (SEQ (ALT r11 r12) r2)}"

   323     by (simp add: Ls_union ih1 ih2 lang_seq_union Collect_disj_eq)

   324 next

   325   case (10 r1 r2 c)

   326   have ih2: "Ls (set r2 \<dagger> c) = {s. c#s \<in> L r2}" by fact

   327   have ih1: "Ls (set r1 \<dagger> c) = {s. c#s \<in> L r1}" by fact

   328   have "Ls (set SEQ (STAR r1) r2 \<dagger> c) = Ls (set r2 \<dagger> c) \<union> (Ls (set r1 \<dagger> c); ((L r1)\<star> ; L r2))"

   329     by (auto simp add: lang_seq_def Ls_def)

   330   also have "\<dots> = {s. c#s \<in> L r2} \<union> ({s. c#s \<in> L r1} ; ((L r1)\<star> ; L r2))" using ih1 ih2 by simp

   331   also have "\<dots> = {s. c#s \<in> L r2} \<union> ({s. c#s \<in> L r1} ; (L r1)\<star>) ; L r2" by (simp add: lang_seq_assoc)

   332   also have "\<dots> = {s. c#s \<in> L r2} \<union> {s. c#s \<in> (L r1)\<star>} ; L r2" by (simp add: zzz)

   333   also have "\<dots> = {s. c#s \<in> L r2} \<union> {s. c#s \<in> (L r1)\<star> ; L r2}" 

   334     by (auto simp add: lang_seq_def Cons_eq_append_conv)

   335   also have "\<dots> = {s. c#s \<in> (L r1)\<star> ; L r2}" 

   336     by (force simp add: lang_seq_def)

   337   finally show "Ls (set SEQ (STAR r1) r2 \<dagger> c) = {s. c#s \<in> L (SEQ (STAR r1) r2)}" by simp

   338 next

   339   case (11 r c)

   340   have ih: "Ls (set r \<dagger> c) = {s. c#s \<in> L r}" by fact

   341   have "Ls (set (STAR r) \<dagger> c) =  Ls (set r \<dagger> c) ; (L r)\<star>"

   342     by (auto simp add: lang_seq_def Ls_def)

   343   also have "\<dots> = {s. c#s \<in> L r} ;  (L r)\<star>" using ih by simp

   344   also have "\<dots> = {s. c#s \<in> (L r)\<star>}" using zzz by simp

   345   finally show "Ls (set (STAR r) \<dagger> c) = {s. c#s \<in> L (STAR r)}" by simp

   346 qed

   347 

   348 

   349 text {* matcher function (based on the "list"-dagger function) *}

   350 fun

   351   first_True :: "bool list \<Rightarrow> bool"

   352 where

   353   "first_True [] = False"

   354 | "first_True (x#xs) = (if x then True else first_True xs)"

   355 

   356 lemma not_first_True[simp]:

   357   shows "(\<not>(first_True xs)) = (\<forall>x \<in> set xs. \<not>x)"

   358 by (induct xs) (auto)

   359 

   360 lemma first_True:

   361   shows "(first_True xs) = (\<exists>x \<in> set xs. x)"

   362 by (induct xs) (auto)

   363 

   364 text {* matcher function *}

   365 

   366 function

   367   matcher :: "rexp \<Rightarrow> string \<Rightarrow> bool" ("_ ! _")

   368 where

   369   "NULL ! s = False"

   370 | "EMPTY ! s = (s =[])"

   371 | "CHAR c ! s = (s = [c])" 

   372 | "ALT r1 r2 ! s = (r1 ! s \<or> r2 ! s)"

   373 | "STAR r ! [] = True"

   374 | "STAR r ! c#s =  first_True [SEQ (r') (STAR r) ! s. r' \<leftarrow> r \<dagger> c]"

   375 | "SEQ r1 r2 ! [] = (r1 ! [] \<and> r2 ! [])"

   376 | "SEQ NULL r2 ! (c#s) = False"

   377 | "SEQ EMPTY r2 ! (c#s) = (r2 ! c#s)"

   378 | "SEQ (CHAR c') r2 ! (c#s) = (if c'=c then r2 ! s else False)" 

   379 | "SEQ (SEQ r11 r12) r2 ! (c#s) = (SEQ r11 (SEQ r12 r2) ! c#s)"

   380 | "SEQ (ALT r11 r12) r2 ! (c#s) = ((SEQ r11 r2) ! (c#s) \<or> (SEQ r12 r2) ! (c#s))"

   381 | "SEQ (STAR r1) r2 ! (c#s) = (r2 ! (c#s) \<or> first_True [SEQ r' (SEQ (STAR r1) r2) ! s. r' \<leftarrow> r1 \<dagger> c])"

   382 by (pat_completeness) (auto)

   383 

   384 termination matcher 

   385   by(relation "measures [\<lambda>(r,s). length s, \<lambda>(r,s). size r, \<lambda>(r,s). size (Left r)]") (simp_all)

   386 

   387 text {* positive correctness of the matcher *}

   388 lemma matcher1:

   389   shows "r ! s \<Longrightarrow> s \<in> L r"

   390 proof (induct rule: matcher.induct)

   391   case (1 s)

   392   have "NULL ! s" by fact

   393   then show "s \<in> L NULL" by simp

   394 next

   395   case (2 s)

   396   have "EMPTY ! s" by fact

   397   then show "s \<in> L EMPTY" by simp

   398 next

   399   case (3 c s)

   400   have "CHAR c ! s" by fact

   401   then show "s \<in> L (CHAR c)" by simp

   402 next

   403   case (4 r1 r2 s)

   404   have ih1: "r1 ! s \<Longrightarrow> s \<in> L r1" by fact

   405   have ih2: "r2 ! s \<Longrightarrow> s \<in> L r2" by fact

   406   have "ALT r1 r2 ! s" by fact

   407   with ih1 ih2 show "s \<in> L (ALT r1 r2)" by auto

   408 next

   409   case (5 r)

   410   have "STAR r ! []" by fact 

   411   then show "[] \<in> L (STAR r)" by auto

   412 next

   413   case (6 r c s)

   414   have ih1: "\<And>rx. \<lbrakk>rx \<in> set r \<dagger> c; SEQ rx (STAR r) ! s\<rbrakk> \<Longrightarrow> s \<in> L (SEQ rx (STAR r))" by fact

   415   have as: "STAR r ! c#s" by fact

   416   then obtain r' where imp1: "r' \<in> set r \<dagger> c" and imp2: "SEQ r' (STAR r) ! s" 

   417     by (auto simp add: first_True)

   418   from imp2 imp1 have "s \<in> L (SEQ r' (STAR r))" using ih1 by simp

   419   then have "s \<in> L r' ; (L r)\<star>" by simp

   420   then have "s \<in> Ls (set r \<dagger> c) ; (L r)\<star>" using imp1 by (auto simp add: Ls_def lang_seq_def)

   421   then have "s \<in> {s. c#s \<in> L r} ; (L r)\<star>" by (auto simp add: dagger_correctness)

   422   then have "s \<in> {s. c#s \<in> (L r)\<star>}" by (simp add: zzz)

   423   then have "c#s \<in> {[c]}; {s. c#s \<in> (L r)\<star>}" by (auto simp add: lang_seq_def)

   424   then have "c#s \<in> (L r)\<star>" by (auto simp add: lang_seq_def)

   425   then show "c#s \<in> L (STAR r)" by simp

   426 next

   427   case (7 r1 r2)

   428   have ih1: "r1 ! [] \<Longrightarrow> [] \<in> L r1" by fact

   429   have ih2: "r2 ! [] \<Longrightarrow> [] \<in> L r2" by fact

   430   have as: "SEQ r1 r2 ! []" by fact

   431   then have "r1 ! [] \<and> r2 ! []" by simp

   432   then show "[] \<in> L (SEQ r1 r2)" using ih1 ih2 by (simp add: lang_seq_def)

   433 next

   434   case (8 r2 c s)

   435   have "SEQ NULL r2 ! c#s" by fact

   436   then show "c#s \<in> L (SEQ NULL r2)" by simp

   437 next

   438   case (9 r2 c s)

   439   have ih1: "r2 ! c#s \<Longrightarrow> c#s \<in> L r2" by fact

   440   have "SEQ EMPTY r2 ! c#s" by fact

   441   then show "c#s \<in> L (SEQ EMPTY r2)" using ih1 by (simp add: lang_seq_def)

   442 next

   443   case (10 c' r2 c s)

   444   have ih1: "\<lbrakk>c' = c; r2 ! s\<rbrakk> \<Longrightarrow> s \<in> L r2" by fact

   445   have "SEQ (CHAR c') r2 ! c#s" by fact

   446   then show "c#s \<in> L (SEQ (CHAR c') r2)"

   447     using ih1 by (auto simp add: lang_seq_def split: if_splits)

   448 next

   449   case (11 r11 r12 r2 c s)

   450   have ih1: "SEQ r11 (SEQ r12 r2) ! c#s \<Longrightarrow> c#s \<in> L (SEQ r11 (SEQ r12 r2))" by fact

   451   have "SEQ (SEQ r11 r12) r2 ! c#s" by fact

   452   then have "c#s \<in> L (SEQ r11 (SEQ r12 r2))" using ih1 by simp

   453   then show "c#s \<in> L (SEQ (SEQ r11 r12) r2)" by (simp add: lang_seq_assoc)

   454 next

   455   case (12 r11 r12 r2 c s)

   456   have ih1: "SEQ r11 r2 ! c#s \<Longrightarrow> c#s \<in> L (SEQ r11 r2)" by fact

   457   have ih2: "SEQ r12 r2 ! c#s \<Longrightarrow> c#s \<in> L (SEQ r12 r2)" by fact

   458   have "SEQ (ALT r11 r12) r2 ! c#s" by fact

   459   then show "c#s \<in> L (SEQ (ALT r11 r12) r2)"

   460     using ih1 ih2 by (auto simp add: lang_seq_union)

   461 next

   462   case (13 r1 r2 c s)

   463   have ih1: "r2 ! c#s \<Longrightarrow> c#s \<in> L r2" by fact

   464   have ih2: "\<And>r'. \<lbrakk>r' \<in> set r1 \<dagger> c; SEQ r' (SEQ (STAR r1) r2) ! s\<rbrakk> \<Longrightarrow> 

   465                          s \<in> L (SEQ r' (SEQ (STAR r1) r2))" by fact

   466   have "SEQ (STAR r1) r2 ! c#s" by fact

   467   then have "(r2 ! c#s) \<or> (\<exists>r' \<in> set r1 \<dagger> c. SEQ r' (SEQ (STAR r1) r2) ! s)"  by (auto simp add: first_True)

   468   moreover

   469   { assume "r2 ! c#s"

   470     with ih1 have "c#s \<in> L r2" by simp

   471     then have "c # s \<in> L r1\<star> ; L r2" 

   472       by (auto simp add: lang_seq_def)

   473     then have "c#s \<in> L (SEQ (STAR r1) r2)" by simp

   474   }

   475   moreover

   476   { assume "\<exists>r' \<in> set r1 \<dagger> c. SEQ r' (SEQ (STAR r1) r2) ! s"

   477     then obtain r' where imp1: "r' \<in> set r1 \<dagger> c" and imp2: "SEQ r' (SEQ (STAR r1) r2) ! s" by blast

   478     from imp2 imp1 have "s \<in> L (SEQ r' (SEQ (STAR r1) r2))" using ih2 by simp

   479     then have "s \<in> L r' ; ((L r1)\<star> ; L r2)" by simp

   480     then have "s \<in> Ls (set r1 \<dagger> c) ; ((L r1)\<star> ; L r2)" using imp1 by (auto simp add: Ls_def lang_seq_def)

   481     then have "s \<in> {s. c#s \<in> L r1} ; ((L r1)\<star> ; L r2)" by (simp add: dagger_correctness)

   482     then have "s \<in> ({s. c#s \<in> L r1} ; (L r1)\<star>) ; L r2" by (simp add: lang_seq_assoc)

   483     then have "s \<in> {s. c#s \<in> (L r1)\<star>} ; L r2" by (simp add: zzz)

   484     then have "c#s \<in> {[c]}; ({s. c#s \<in> (L r1)\<star>}; L r2)" by (auto simp add: lang_seq_def)

   485     then have "c#s \<in> ({[c]}; {s. c#s \<in> (L r1)\<star>}) ; L r2" by (simp add: lang_seq_assoc)

   486     then have "c#s \<in> (L r1)\<star>; L r2" by (auto simp add: lang_seq_def)

   487     then have "c#s \<in> L (SEQ (STAR r1) r2)" by simp

   488   }

   489   ultimately show "c#s \<in> L (SEQ (STAR r1) r2)" by blast

   490 qed

   491 

   492 text {* negative correctness of the matcher *}

   493 lemma matcher2:

   494   shows "\<not> r ! s \<Longrightarrow> s \<notin> L r"

   495 proof (induct rule: matcher.induct)

   496   case (1 s)

   497   have "\<not> NULL ! s" by fact

   498   then show "s \<notin> L NULL" by simp

   499 next

   500   case (2 s)

   501   have "\<not> EMPTY ! s" by fact

   502   then show "s \<notin> L EMPTY" by simp

   503 next

   504   case (3 c s)

   505   have "\<not> CHAR c ! s" by fact

   506   then show "s \<notin> L (CHAR c)" by simp

   507 next

   508   case (4 r1 r2 s)

   509   have ih2: "\<not> r1 ! s \<Longrightarrow> s \<notin> L r1" by fact

   510   have ih4: "\<not> r2 ! s \<Longrightarrow> s \<notin> L r2" by fact

   511   have "\<not> ALT r1 r2 ! s" by fact 

   512   then show "s \<notin> L (ALT r1 r2)" by (simp add: ih2 ih4)

   513 next

   514   case (5 r)

   515   have "\<not> STAR r ! []" by fact

   516   then show "[] \<notin> L (STAR r)" by simp

   517 next

   518   case (6 r c s)

   519   have ih: "\<And>rx. \<lbrakk>rx \<in> set r \<dagger> c; \<not>SEQ rx (STAR r) ! s\<rbrakk> \<Longrightarrow> s \<notin> L (SEQ rx (STAR r))" by fact

   520   have as: "\<not> STAR r ! c#s" by fact

   521   then have "\<forall>r'\<in> set r \<dagger> c. \<not> (SEQ r' (STAR r) ! s)" by simp

   522   then have "\<forall>r'\<in> set r \<dagger> c. s \<notin> L (SEQ r' (STAR r))" using ih by auto

   523   then have "\<forall>r'\<in> set r \<dagger> c. s \<notin> L r' ; ((L r)\<star>)" by simp

   524   then have "s \<notin> (Ls (set r \<dagger> c)) ; ((L r)\<star>)" by (auto simp add: Ls_def lang_seq_def)

   525   then have "s \<notin> {s. c#s \<in> L r} ; ((L r)\<star>)" by (simp add: dagger_correctness)

   526   then have "s \<notin> {s. c#s \<in> (L r)\<star>}" by (simp add: zzz)

   527   then have "c#s \<notin> {[c]} ; {s. c#s \<in> (L r)\<star>}" by (auto simp add: lang_seq_assoc lang_seq_def)

   528   then have "c#s \<notin> (L r)\<star>" by (simp add: lang_seq_def)

   529   then show "c#s \<notin> L (STAR r)" by simp

   530 next

   531   case (7 r1 r2)

   532   have ih2: "\<not> r1 ! [] \<Longrightarrow> [] \<notin> L r1" by fact

   533   have ih4: "\<not> r2 ! [] \<Longrightarrow> [] \<notin> L r2" by fact

   534   have "\<not> SEQ r1 r2 ! []" by fact

   535   then have "\<not> r1 ! [] \<or> \<not> r2 ! []" by simp

   536   then show "[] \<notin> L (SEQ r1 r2)" using ih2 ih4 

   537     by (auto simp add: lang_seq_def)

   538 next

   539   case (8 r2 c s)

   540   have "\<not> SEQ NULL r2 ! c#s" by fact

   541   then show "c#s \<notin> L (SEQ NULL r2)" by (simp add: lang_seq_null)

   542 next

   543   case (9 r2 c s)

   544   have ih1: "\<not> r2 ! c#s \<Longrightarrow> c#s \<notin> L r2" by fact

   545   have "\<not> SEQ EMPTY r2 ! c#s" by fact

   546   then show "c#s \<notin> L (SEQ EMPTY r2)"

   547     using ih1 by (simp add: lang_seq_def)

   548 next

   549   case (10 c' r2 c s)

   550   have ih2: "\<lbrakk>c' = c; \<not>r2 ! s\<rbrakk> \<Longrightarrow> s \<notin> L r2" by fact

   551   have "\<not> SEQ (CHAR c') r2 ! c#s" by fact

   552   then show "c#s \<notin> L (SEQ (CHAR c') r2)"

   553     using ih2 by (auto simp add: lang_seq_def)

   554 next

   555   case (11 r11 r12 r2 c s)

   556   have ih2: "\<not> SEQ r11 (SEQ r12 r2) ! c#s \<Longrightarrow> c#s \<notin> L (SEQ r11 (SEQ r12 r2))" by fact

   557   have "\<not> SEQ (SEQ r11 r12) r2 ! c#s" by fact

   558   then show "c#s \<notin> L (SEQ (SEQ r11 r12) r2)"

   559     using ih2 by (auto simp add: lang_seq_def)

   560 next

   561   case (12 r11 r12 r2 c s)

   562   have ih2: "\<not> SEQ r11 r2 ! c#s \<Longrightarrow> c#s \<notin> L (SEQ r11 r2)" by fact

   563   have ih4: "\<not> SEQ r12 r2 ! c#s \<Longrightarrow> c#s \<notin> L (SEQ r12 r2)" by fact

   564   have "\<not> SEQ (ALT r11 r12) r2 ! c#s" by fact

   565   then show " c#s \<notin> L (SEQ (ALT r11 r12) r2)"

   566     using ih2 ih4 by (simp add: lang_seq_union)

   567 next

   568   case (13 r1 r2 c s)

   569   have ih1: "\<not>r2 ! c#s \<Longrightarrow> c#s \<notin> L r2" by fact

   570   have ih2: "\<And>rx. \<lbrakk>rx \<in> set r1 \<dagger> c; \<not> SEQ rx (SEQ (STAR r1) r2) ! s\<rbrakk> 

   571                    \<Longrightarrow> s \<notin> L (SEQ rx (SEQ (STAR r1) r2))" by fact

   572   have as: "\<not> SEQ (STAR r1) r2 ! c#s" by fact

   573   then have as1: "\<not>r2 ! c#s" and as2: "\<forall>r1'\<in>set r1 \<dagger> c. \<not> SEQ r1' (SEQ (STAR r1) r2) ! s" by simp_all

   574   from as1 have bs1: "c#s \<notin> L r2" using ih1 by simp

   575   from as2 have "\<forall>r1'\<in>set r1 \<dagger> c. \<not> SEQ r1' (SEQ (STAR r1) r2) ! s" by simp

   576   then have "\<forall>r1'\<in>set r1 \<dagger> c. s \<notin> L (SEQ r1' (SEQ (STAR r1) r2))" using ih2 by simp

   577   then have "\<forall>r1'\<in>set r1 \<dagger> c. s \<notin> L r1'; ((L r1)\<star>; L r2)" by simp

   578   then have "s \<notin> (Ls (set r1 \<dagger> c)) ; ((L r1)\<star>; L r2)" by (auto simp add: Ls_def lang_seq_def)

   579   then have "s \<notin> {s. c#s \<in> L r1} ; ((L r1)\<star>; L r2)" by (simp add: dagger_correctness)

   580   then have "s \<notin> ({s. c#s \<in> L r1} ; (L r1)\<star>); L r2" by (simp add: lang_seq_assoc)

   581   then have "s \<notin> {s. c#s \<in> (L r1)\<star>}; L r2" by (simp add: zzz)

   582   then have "c#s \<notin> {[c]}; ({s. c#s \<in> (L r1)\<star>}; L r2)" by (auto simp add: lang_seq_def)

   583   then have "c#s \<notin> (L r1)\<star>; L r2" using bs1 by (auto simp add: lang_seq_def Cons_eq_append_conv)

   584   then show "c#s \<notin> L (SEQ (STAR r1) r2)" by simp

   585 qed

   586 

   587 section {* Questions *}

   588 

   589 text {*

   590   - Why was the key lemma k1 omitted; is there an easy, non-induction

   591     way for obtaining this property? 

   592   - Why was False included in the definition of the STAR-clause in

   593     the matcher? Has this something to do with executing the code?

   594   

   595 *}

   596 

   597 section {* Code *}

   598    

   599 export_code dagger in SML module_name Dagger file - 

   600 export_code matcher in SML module_name Dagger file -

   601 

   602 section {* Examples *}

   603 

   604 text {* since now everything is based on lists, the evaluation is quite fast *}

   605 

   606 value "NULL ! []"

   607 value "(CHAR (CHR ''a'')) ! [CHR ''a'']"

   608 value "((CHAR a) ! [a,a])"

   609 value "(STAR (CHAR a)) ! []"

   610 value "(STAR (CHAR a)) ! [a,a]"

   611 value "(SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ! ''abbbbc''"

   612 value "(SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ! ''abbcbbc''"

   613 

   614 section {* Slind et al's matcher based on derivatives *}

   615 

   616 fun

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

   618 where

   619   "nullable (NULL) = False"

   620 | "nullable (EMPTY) = True"

   621 | "nullable (CHAR c) = False"

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

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

   624 | "nullable (STAR r) = True"

   625 

   626 lemma nullable:

   627   shows "([] \<in> L r) = nullable r"

   628 by (induct r)

   629    (auto simp add: lang_seq_def) 

   630 

   631 fun

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

   633 where

   634   "der c (NULL) = NULL"

   635 | "der c (EMPTY) = NULL"

   636 | "der c (CHAR c') = (if c=c' then EMPTY else NULL)"

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

   638 | "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)"

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

   640 

   641 lemma k2:

   642   assumes b: "s \<in> L1\<star>"

   643   and a: "s \<noteq> []"

   644   shows "s \<in> (L1; (L1\<star>))"

   645 using b a

   646 apply(induct rule: Star.induct)

   647 apply(simp)

   648 apply(case_tac "s1=[]")

   649 apply(simp)

   650 apply(simp add: lang_seq_def)

   651 apply(blast)

   652 done

   653 

   654 

   655 lemma der_correctness:

   656   shows "(s \<in> L (der c r)) = ((c#s) \<in> L r)"

   657 proof (induct r arbitrary: s)

   658   case (NULL s)

   659   show "(s \<in> L (der c NULL)) = (c#s \<in> L NULL)" by simp

   660 next

   661   case (EMPTY s)

   662   show "(s \<in> L (der c EMPTY)) = (c#s \<in> L EMPTY)" by simp

   663 next

   664   case (CHAR c' s)

   665   show "(s \<in> L (der c (CHAR c'))) = (c#s \<in> L (CHAR c'))" by simp

   666 next

   667   case (SEQ r1 r2 s)

   668   have ih1: "\<And>s. (s \<in> L (der c r1)) = (c#s \<in> L r1)" by fact

   669   have ih2: "\<And>s. (s \<in> L (der c r2)) = (c#s \<in> L r2)" by fact

   670   show "(s \<in> L (der c (SEQ r1 r2))) = (c#s \<in> L (SEQ r1 r2))" 

   671     using ih1 ih2

   672     by (auto simp add: nullable[symmetric] lang_seq_def Cons_eq_append_conv)

   673 next

   674   case (ALT r1 r2 s)

   675   have ih1: "\<And>s. (s \<in> L (der c r1)) = (c#s \<in> L r1)" by fact

   676   have ih2: "\<And>s. (s \<in> L (der c r2)) = (c#s \<in> L r2)" by fact

   677   show "(s \<in> L (der c (ALT r1 r2))) = (c#s \<in> L (ALT r1 r2))"

   678     using ih1 ih2 by (auto simp add: lang_seq_def)

   679 next

   680   case (STAR r s)

   681   have ih1: "\<And>s. (s \<in> L (der c r)) = (c#s \<in> L r)" by fact

   682   show "(s \<in> L (der c (STAR r))) = (c#s \<in> L (STAR r))"

   683     using ih1

   684     apply(simp)

   685     apply(auto simp add: lang_seq_def)

   686     apply(drule lang_seq_append)

   687     apply(assumption)

   688     apply(simp)

   689     apply(subst lang_star_cases)

   690     apply(simp)

   691     thm k1

   692     apply(drule k2)

   693     apply(simp)

   694     apply(simp add: lang_seq_def)

   695     apply(erule exE)+

   696     apply(erule conjE)+

   697     apply(auto simp add: lang_seq_def Cons_eq_append_conv)

   698     apply(drule k1)

   699     apply(simp)

   700     apply(simp add: lang_seq_def)

   701     apply(erule exE)+

   702     apply(erule conjE)+

   703     apply(auto simp add: lang_seq_def Cons_eq_append_conv)

   704     done

   705 qed

   706 

   707 fun 

   708  derivative :: "string \<Rightarrow> rexp \<Rightarrow> rexp"

   709 where

   710   "derivative [] r = r"

   711 | "derivative (c#s) r = derivative s (der c r)"

   712 

   713 fun

   714   slind_matcher :: "rexp \<Rightarrow> string \<Rightarrow> bool"

   715 where

   716   "slind_matcher r s = nullable (derivative s r)"

   717 

   718 lemma slind_matcher:

   719   shows "slind_matcher r s = (s \<in> L r)"

   720 by (induct s arbitrary: r)

   721    (auto simp add: nullable der_correctness)

   722 

   723 export_code slind_matcher in SML module_name Slind file - 

   724 

   725 

   726 (* ******************************************** now is the codes writen by chunhan ************************************* *)

   939 apply (simp add:del_x_paired_def)

   463   apply (simp add:del_x_paired_def)

   940 apply (rule set_ext, rule iffI, simp)

   464   apply (simp add: distinct_rhs_def)

   941 apply (erule disjE, rule_tac x = X in exI, rule_tac x = r in exI, simp)

   465   apply(auto simp add: lang_seq_def)

   942 apply (clarify, rule_tac x = Xa in exI, rule_tac x = ra in exI, simp)

   466   apply(metis)

   943 apply (clarsimp, drule_tac x = Xa in spec, drule_tac x = ra in spec)

   467   done

   944 apply (auto simp:distinct_rhs_def)

   945 done