--- a/MyhillNerode.thy	Wed Oct 20 14:11:14 2010 +0000
+++ b/MyhillNerode.thy	Thu Oct 21 13:42:08 2010 +0000
@@ -7,7 +7,7 @@
 definition
   lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ; _" [100,100] 100)
 where 
-  "L1 ; L2 = {s1@s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
+  "L1 ; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
 
 lemma lang_seq_empty:
   shows "{[]} ; L = L"
@@ -33,8 +33,10 @@
 
 lemma lang_seq_assoc:
   shows "(L1 ; L2) ; L3 = L1 ; (L2 ; L3)"
-by (simp add: lang_seq_def Collect_def mem_def expand_fun_eq)
-   (metis append_assoc)
+unfolding lang_seq_def
+apply(auto)
+apply(metis)
+by (metis append_assoc)
 
 lemma lang_seq_minus:
   shows "(L1; L2) - {[]} =
@@ -245,485 +247,8 @@
   | "L_rexp (STAR r) = (L_rexp r)\<star>"
 end
 
-definition
-  Ls :: "rexp set \<Rightarrow> string set"
-where
-  "Ls R = (\<Union>r\<in>R. (L r))"
 
-lemma Ls_union:
-  "Ls (R1 \<union> R2) = (Ls R1) \<union> (Ls R2)"
-unfolding Ls_def by auto
-
-text {* helper function for termination proofs *}
-fun
- Left :: "rexp \<Rightarrow> rexp"
-where
- "Left (SEQ r1 r2) = r1"
-
-text {* dagger function *}
-
-function
-  dagger :: "rexp \<Rightarrow> char \<Rightarrow> rexp list" ("_ \<dagger> _")
-where
-  c1: "(NULL \<dagger> c) = []"
-| c2: "(EMPTY) \<dagger> c = []"
-| c3: "(CHAR c') \<dagger> c = (if c = c' then [EMPTY] else [])"
-| c4: "(ALT r1 r2) \<dagger> c = r1 \<dagger> c @ r2 \<dagger> c"
-| c5: "(SEQ NULL r2) \<dagger> c = []" 
-| c6: "(SEQ EMPTY r2) \<dagger> c = r2 \<dagger> c" 
-| c7: "(SEQ (CHAR c') r2) \<dagger> c = (if c = c' then [r2] else [])"
-| c8: "(SEQ (SEQ r11 r12) r2) \<dagger> c = (SEQ r11 (SEQ r12 r2)) \<dagger> c" 
-| c9: "(SEQ (ALT r11 r12) r2) \<dagger> c = (SEQ r11 r2) \<dagger> c @ (SEQ r12 r2) \<dagger> c" 
-| c10: "(SEQ (STAR r1) r2) \<dagger> c = r2 \<dagger> c @ [SEQ r' (SEQ (STAR r1) r2). r' \<leftarrow> r1 \<dagger> c]" 
-| c11: "(STAR r) \<dagger> c = [SEQ r' (STAR r) .  r' \<leftarrow> r \<dagger> c]"
-by (pat_completeness) (auto)
-
-termination dagger
-  by (relation "measures [\<lambda>(r, c). size r, \<lambda>(r, c). size (Left r)]") (simp_all)
-
-lemma dagger_correctness:
-  "Ls (set r \<dagger> c) = {s. c#s \<in> L r}"
-proof (induct rule: dagger.induct)
-  case (1 c)
-  show "Ls (set NULL \<dagger> c) = {s. c#s \<in> L NULL}" by (simp add: Ls_def)
-next  
-  case (2 c)
-  show "Ls (set EMPTY \<dagger> c) = {s. c#s \<in> L EMPTY}" by (simp add: Ls_def)
-next
-  case (3 c' c)
-  show "Ls (set CHAR c' \<dagger> c) = {s. c#s \<in> L (CHAR c')}" by (simp add: Ls_def)
-next
-  case (4 r1 r2 c)
-  have ih1: "Ls (set r1 \<dagger> c) = {s. c#s \<in> L r1}" by fact
-  have ih2: "Ls (set r2 \<dagger> c) = {s. c#s \<in> L r2}" by fact
-  show "Ls (set ALT r1 r2 \<dagger> c) = {s. c#s \<in> L (ALT r1 r2)}"
-    by (simp add: Ls_union ih1 ih2 Collect_disj_eq)
-next
-  case (5 r2 c)
-  show "Ls (set SEQ NULL r2 \<dagger> c) = {s. c#s \<in> L (SEQ NULL r2)}" by (simp add: Ls_def lang_seq_null)
-next
-  case (6 r2 c)
-  have ih: "Ls (set r2 \<dagger> c) = {s. c#s \<in> L r2}" by fact
-  show "Ls (set SEQ EMPTY r2 \<dagger> c) = {s. c#s \<in> L (SEQ EMPTY r2)}"
-    by (simp add: ih lang_seq_empty)
-next
-  case (7 c' r2 c)
-  show "Ls (set SEQ (CHAR c') r2 \<dagger> c) = {s. c#s \<in> L (SEQ (CHAR c') r2)}"
-    by (simp add: Ls_def lang_seq_def)
-next
-  case (8 r11 r12 r2 c)
-  have ih: "Ls (set SEQ r11 (SEQ r12 r2) \<dagger> c) = {s. c#s \<in> L (SEQ r11 (SEQ r12 r2))}" by fact
-  show "Ls (set SEQ (SEQ r11 r12) r2 \<dagger> c) = {s. c#s \<in> L (SEQ (SEQ r11 r12) r2)}"
-    by (simp add: ih lang_seq_assoc)
-next
-  case (9 r11 r12 r2 c)
-  have ih1: "Ls (set SEQ r11 r2 \<dagger> c) = {s. c#s \<in> L (SEQ r11 r2)}" by fact
-  have ih2: "Ls (set SEQ r12 r2 \<dagger> c) = {s. c#s \<in> L (SEQ r12 r2)}" by fact
-  show "Ls (set SEQ (ALT r11 r12) r2 \<dagger> c) = {s. c#s \<in> L (SEQ (ALT r11 r12) r2)}"
-    by (simp add: Ls_union ih1 ih2 lang_seq_union Collect_disj_eq)
-next
-  case (10 r1 r2 c)
-  have ih2: "Ls (set r2 \<dagger> c) = {s. c#s \<in> L r2}" by fact
-  have ih1: "Ls (set r1 \<dagger> c) = {s. c#s \<in> L r1}" by fact
-  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))"
-    by (auto simp add: lang_seq_def Ls_def)
-  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
-  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)
-  also have "\<dots> = {s. c#s \<in> L r2} \<union> {s. c#s \<in> (L r1)\<star>} ; L r2" by (simp add: zzz)
-  also have "\<dots> = {s. c#s \<in> L r2} \<union> {s. c#s \<in> (L r1)\<star> ; L r2}" 
-    by (auto simp add: lang_seq_def Cons_eq_append_conv)
-  also have "\<dots> = {s. c#s \<in> (L r1)\<star> ; L r2}" 
-    by (force simp add: lang_seq_def)
-  finally show "Ls (set SEQ (STAR r1) r2 \<dagger> c) = {s. c#s \<in> L (SEQ (STAR r1) r2)}" by simp
-next
-  case (11 r c)
-  have ih: "Ls (set r \<dagger> c) = {s. c#s \<in> L r}" by fact
-  have "Ls (set (STAR r) \<dagger> c) =  Ls (set r \<dagger> c) ; (L r)\<star>"
-    by (auto simp add: lang_seq_def Ls_def)
-  also have "\<dots> = {s. c#s \<in> L r} ;  (L r)\<star>" using ih by simp
-  also have "\<dots> = {s. c#s \<in> (L r)\<star>}" using zzz by simp
-  finally show "Ls (set (STAR r) \<dagger> c) = {s. c#s \<in> L (STAR r)}" by simp
-qed
-
-
-text {* matcher function (based on the "list"-dagger function) *}
-fun
-  first_True :: "bool list \<Rightarrow> bool"
-where
-  "first_True [] = False"
-| "first_True (x#xs) = (if x then True else first_True xs)"
-
-lemma not_first_True[simp]:
-  shows "(\<not>(first_True xs)) = (\<forall>x \<in> set xs. \<not>x)"
-by (induct xs) (auto)
-
-lemma first_True:
-  shows "(first_True xs) = (\<exists>x \<in> set xs. x)"
-by (induct xs) (auto)
-
-text {* matcher function *}
-
-function
-  matcher :: "rexp \<Rightarrow> string \<Rightarrow> bool" ("_ ! _")
-where
-  "NULL ! s = False"
-| "EMPTY ! s = (s =[])"
-| "CHAR c ! s = (s = [c])" 
-| "ALT r1 r2 ! s = (r1 ! s \<or> r2 ! s)"
-| "STAR r ! [] = True"
-| "STAR r ! c#s =  first_True [SEQ (r') (STAR r) ! s. r' \<leftarrow> r \<dagger> c]"
-| "SEQ r1 r2 ! [] = (r1 ! [] \<and> r2 ! [])"
-| "SEQ NULL r2 ! (c#s) = False"
-| "SEQ EMPTY r2 ! (c#s) = (r2 ! c#s)"
-| "SEQ (CHAR c') r2 ! (c#s) = (if c'=c then r2 ! s else False)" 
-| "SEQ (SEQ r11 r12) r2 ! (c#s) = (SEQ r11 (SEQ r12 r2) ! c#s)"
-| "SEQ (ALT r11 r12) r2 ! (c#s) = ((SEQ r11 r2) ! (c#s) \<or> (SEQ r12 r2) ! (c#s))"
-| "SEQ (STAR r1) r2 ! (c#s) = (r2 ! (c#s) \<or> first_True [SEQ r' (SEQ (STAR r1) r2) ! s. r' \<leftarrow> r1 \<dagger> c])"
-by (pat_completeness) (auto)
-
-termination matcher 
-  by(relation "measures [\<lambda>(r,s). length s, \<lambda>(r,s). size r, \<lambda>(r,s). size (Left r)]") (simp_all)
-
-text {* positive correctness of the matcher *}
-lemma matcher1:
-  shows "r ! s \<Longrightarrow> s \<in> L r"
-proof (induct rule: matcher.induct)
-  case (1 s)
-  have "NULL ! s" by fact
-  then show "s \<in> L NULL" by simp
-next
-  case (2 s)
-  have "EMPTY ! s" by fact
-  then show "s \<in> L EMPTY" by simp
-next
-  case (3 c s)
-  have "CHAR c ! s" by fact
-  then show "s \<in> L (CHAR c)" by simp
-next
-  case (4 r1 r2 s)
-  have ih1: "r1 ! s \<Longrightarrow> s \<in> L r1" by fact
-  have ih2: "r2 ! s \<Longrightarrow> s \<in> L r2" by fact
-  have "ALT r1 r2 ! s" by fact
-  with ih1 ih2 show "s \<in> L (ALT r1 r2)" by auto
-next
-  case (5 r)
-  have "STAR r ! []" by fact 
-  then show "[] \<in> L (STAR r)" by auto
-next
-  case (6 r c s)
-  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
-  have as: "STAR r ! c#s" by fact
-  then obtain r' where imp1: "r' \<in> set r \<dagger> c" and imp2: "SEQ r' (STAR r) ! s" 
-    by (auto simp add: first_True)
-  from imp2 imp1 have "s \<in> L (SEQ r' (STAR r))" using ih1 by simp
-  then have "s \<in> L r' ; (L r)\<star>" by simp
-  then have "s \<in> Ls (set r \<dagger> c) ; (L r)\<star>" using imp1 by (auto simp add: Ls_def lang_seq_def)
-  then have "s \<in> {s. c#s \<in> L r} ; (L r)\<star>" by (auto simp add: dagger_correctness)
-  then have "s \<in> {s. c#s \<in> (L r)\<star>}" by (simp add: zzz)
-  then have "c#s \<in> {[c]}; {s. c#s \<in> (L r)\<star>}" by (auto simp add: lang_seq_def)
-  then have "c#s \<in> (L r)\<star>" by (auto simp add: lang_seq_def)
-  then show "c#s \<in> L (STAR r)" by simp
-next
-  case (7 r1 r2)
-  have ih1: "r1 ! [] \<Longrightarrow> [] \<in> L r1" by fact
-  have ih2: "r2 ! [] \<Longrightarrow> [] \<in> L r2" by fact
-  have as: "SEQ r1 r2 ! []" by fact
-  then have "r1 ! [] \<and> r2 ! []" by simp
-  then show "[] \<in> L (SEQ r1 r2)" using ih1 ih2 by (simp add: lang_seq_def)
-next
-  case (8 r2 c s)
-  have "SEQ NULL r2 ! c#s" by fact
-  then show "c#s \<in> L (SEQ NULL r2)" by simp
-next
-  case (9 r2 c s)
-  have ih1: "r2 ! c#s \<Longrightarrow> c#s \<in> L r2" by fact
-  have "SEQ EMPTY r2 ! c#s" by fact
-  then show "c#s \<in> L (SEQ EMPTY r2)" using ih1 by (simp add: lang_seq_def)
-next
-  case (10 c' r2 c s)
-  have ih1: "\<lbrakk>c' = c; r2 ! s\<rbrakk> \<Longrightarrow> s \<in> L r2" by fact
-  have "SEQ (CHAR c') r2 ! c#s" by fact
-  then show "c#s \<in> L (SEQ (CHAR c') r2)"
-    using ih1 by (auto simp add: lang_seq_def split: if_splits)
-next
-  case (11 r11 r12 r2 c s)
-  have ih1: "SEQ r11 (SEQ r12 r2) ! c#s \<Longrightarrow> c#s \<in> L (SEQ r11 (SEQ r12 r2))" by fact
-  have "SEQ (SEQ r11 r12) r2 ! c#s" by fact
-  then have "c#s \<in> L (SEQ r11 (SEQ r12 r2))" using ih1 by simp
-  then show "c#s \<in> L (SEQ (SEQ r11 r12) r2)" by (simp add: lang_seq_assoc)
-next
-  case (12 r11 r12 r2 c s)
-  have ih1: "SEQ r11 r2 ! c#s \<Longrightarrow> c#s \<in> L (SEQ r11 r2)" by fact
-  have ih2: "SEQ r12 r2 ! c#s \<Longrightarrow> c#s \<in> L (SEQ r12 r2)" by fact
-  have "SEQ (ALT r11 r12) r2 ! c#s" by fact
-  then show "c#s \<in> L (SEQ (ALT r11 r12) r2)"
-    using ih1 ih2 by (auto simp add: lang_seq_union)
-next
-  case (13 r1 r2 c s)
-  have ih1: "r2 ! c#s \<Longrightarrow> c#s \<in> L r2" by fact
-  have ih2: "\<And>r'. \<lbrakk>r' \<in> set r1 \<dagger> c; SEQ r' (SEQ (STAR r1) r2) ! s\<rbrakk> \<Longrightarrow> 
-                         s \<in> L (SEQ r' (SEQ (STAR r1) r2))" by fact
-  have "SEQ (STAR r1) r2 ! c#s" by fact
-  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)
-  moreover
-  { assume "r2 ! c#s"
-    with ih1 have "c#s \<in> L r2" by simp
-    then have "c # s \<in> L r1\<star> ; L r2" 
-      by (auto simp add: lang_seq_def)
-    then have "c#s \<in> L (SEQ (STAR r1) r2)" by simp
-  }
-  moreover
-  { assume "\<exists>r' \<in> set r1 \<dagger> c. SEQ r' (SEQ (STAR r1) r2) ! s"
-    then obtain r' where imp1: "r' \<in> set r1 \<dagger> c" and imp2: "SEQ r' (SEQ (STAR r1) r2) ! s" by blast
-    from imp2 imp1 have "s \<in> L (SEQ r' (SEQ (STAR r1) r2))" using ih2 by simp
-    then have "s \<in> L r' ; ((L r1)\<star> ; L r2)" by simp
-    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)
-    then have "s \<in> {s. c#s \<in> L r1} ; ((L r1)\<star> ; L r2)" by (simp add: dagger_correctness)
-    then have "s \<in> ({s. c#s \<in> L r1} ; (L r1)\<star>) ; L r2" by (simp add: lang_seq_assoc)
-    then have "s \<in> {s. c#s \<in> (L r1)\<star>} ; L r2" by (simp add: zzz)
-    then have "c#s \<in> {[c]}; ({s. c#s \<in> (L r1)\<star>}; L r2)" by (auto simp add: lang_seq_def)
-    then have "c#s \<in> ({[c]}; {s. c#s \<in> (L r1)\<star>}) ; L r2" by (simp add: lang_seq_assoc)
-    then have "c#s \<in> (L r1)\<star>; L r2" by (auto simp add: lang_seq_def)
-    then have "c#s \<in> L (SEQ (STAR r1) r2)" by simp
-  }
-  ultimately show "c#s \<in> L (SEQ (STAR r1) r2)" by blast
-qed
-
-text {* negative correctness of the matcher *}
-lemma matcher2:
-  shows "\<not> r ! s \<Longrightarrow> s \<notin> L r"
-proof (induct rule: matcher.induct)
-  case (1 s)
-  have "\<not> NULL ! s" by fact
-  then show "s \<notin> L NULL" by simp
-next
-  case (2 s)
-  have "\<not> EMPTY ! s" by fact
-  then show "s \<notin> L EMPTY" by simp
-next
-  case (3 c s)
-  have "\<not> CHAR c ! s" by fact
-  then show "s \<notin> L (CHAR c)" by simp
-next
-  case (4 r1 r2 s)
-  have ih2: "\<not> r1 ! s \<Longrightarrow> s \<notin> L r1" by fact
-  have ih4: "\<not> r2 ! s \<Longrightarrow> s \<notin> L r2" by fact
-  have "\<not> ALT r1 r2 ! s" by fact 
-  then show "s \<notin> L (ALT r1 r2)" by (simp add: ih2 ih4)
-next
-  case (5 r)
-  have "\<not> STAR r ! []" by fact
-  then show "[] \<notin> L (STAR r)" by simp
-next
-  case (6 r c s)
-  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
-  have as: "\<not> STAR r ! c#s" by fact
-  then have "\<forall>r'\<in> set r \<dagger> c. \<not> (SEQ r' (STAR r) ! s)" by simp
-  then have "\<forall>r'\<in> set r \<dagger> c. s \<notin> L (SEQ r' (STAR r))" using ih by auto
-  then have "\<forall>r'\<in> set r \<dagger> c. s \<notin> L r' ; ((L r)\<star>)" by simp
-  then have "s \<notin> (Ls (set r \<dagger> c)) ; ((L r)\<star>)" by (auto simp add: Ls_def lang_seq_def)
-  then have "s \<notin> {s. c#s \<in> L r} ; ((L r)\<star>)" by (simp add: dagger_correctness)
-  then have "s \<notin> {s. c#s \<in> (L r)\<star>}" by (simp add: zzz)
-  then have "c#s \<notin> {[c]} ; {s. c#s \<in> (L r)\<star>}" by (auto simp add: lang_seq_assoc lang_seq_def)
-  then have "c#s \<notin> (L r)\<star>" by (simp add: lang_seq_def)
-  then show "c#s \<notin> L (STAR r)" by simp
-next
-  case (7 r1 r2)
-  have ih2: "\<not> r1 ! [] \<Longrightarrow> [] \<notin> L r1" by fact
-  have ih4: "\<not> r2 ! [] \<Longrightarrow> [] \<notin> L r2" by fact
-  have "\<not> SEQ r1 r2 ! []" by fact
-  then have "\<not> r1 ! [] \<or> \<not> r2 ! []" by simp
-  then show "[] \<notin> L (SEQ r1 r2)" using ih2 ih4 
-    by (auto simp add: lang_seq_def)
-next
-  case (8 r2 c s)
-  have "\<not> SEQ NULL r2 ! c#s" by fact
-  then show "c#s \<notin> L (SEQ NULL r2)" by (simp add: lang_seq_null)
-next
-  case (9 r2 c s)
-  have ih1: "\<not> r2 ! c#s \<Longrightarrow> c#s \<notin> L r2" by fact
-  have "\<not> SEQ EMPTY r2 ! c#s" by fact
-  then show "c#s \<notin> L (SEQ EMPTY r2)"
-    using ih1 by (simp add: lang_seq_def)
-next
-  case (10 c' r2 c s)
-  have ih2: "\<lbrakk>c' = c; \<not>r2 ! s\<rbrakk> \<Longrightarrow> s \<notin> L r2" by fact
-  have "\<not> SEQ (CHAR c') r2 ! c#s" by fact
-  then show "c#s \<notin> L (SEQ (CHAR c') r2)"
-    using ih2 by (auto simp add: lang_seq_def)
-next
-  case (11 r11 r12 r2 c s)
-  have ih2: "\<not> SEQ r11 (SEQ r12 r2) ! c#s \<Longrightarrow> c#s \<notin> L (SEQ r11 (SEQ r12 r2))" by fact
-  have "\<not> SEQ (SEQ r11 r12) r2 ! c#s" by fact
-  then show "c#s \<notin> L (SEQ (SEQ r11 r12) r2)"
-    using ih2 by (auto simp add: lang_seq_def)
-next
-  case (12 r11 r12 r2 c s)
-  have ih2: "\<not> SEQ r11 r2 ! c#s \<Longrightarrow> c#s \<notin> L (SEQ r11 r2)" by fact
-  have ih4: "\<not> SEQ r12 r2 ! c#s \<Longrightarrow> c#s \<notin> L (SEQ r12 r2)" by fact
-  have "\<not> SEQ (ALT r11 r12) r2 ! c#s" by fact
-  then show " c#s \<notin> L (SEQ (ALT r11 r12) r2)"
-    using ih2 ih4 by (simp add: lang_seq_union)
-next
-  case (13 r1 r2 c s)
-  have ih1: "\<not>r2 ! c#s \<Longrightarrow> c#s \<notin> L r2" by fact
-  have ih2: "\<And>rx. \<lbrakk>rx \<in> set r1 \<dagger> c; \<not> SEQ rx (SEQ (STAR r1) r2) ! s\<rbrakk> 
-                   \<Longrightarrow> s \<notin> L (SEQ rx (SEQ (STAR r1) r2))" by fact
-  have as: "\<not> SEQ (STAR r1) r2 ! c#s" by fact
-  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
-  from as1 have bs1: "c#s \<notin> L r2" using ih1 by simp
-  from as2 have "\<forall>r1'\<in>set r1 \<dagger> c. \<not> SEQ r1' (SEQ (STAR r1) r2) ! s" by simp
-  then have "\<forall>r1'\<in>set r1 \<dagger> c. s \<notin> L (SEQ r1' (SEQ (STAR r1) r2))" using ih2 by simp
-  then have "\<forall>r1'\<in>set r1 \<dagger> c. s \<notin> L r1'; ((L r1)\<star>; L r2)" by simp
-  then have "s \<notin> (Ls (set r1 \<dagger> c)) ; ((L r1)\<star>; L r2)" by (auto simp add: Ls_def lang_seq_def)
-  then have "s \<notin> {s. c#s \<in> L r1} ; ((L r1)\<star>; L r2)" by (simp add: dagger_correctness)
-  then have "s \<notin> ({s. c#s \<in> L r1} ; (L r1)\<star>); L r2" by (simp add: lang_seq_assoc)
-  then have "s \<notin> {s. c#s \<in> (L r1)\<star>}; L r2" by (simp add: zzz)
-  then have "c#s \<notin> {[c]}; ({s. c#s \<in> (L r1)\<star>}; L r2)" by (auto simp add: lang_seq_def)
-  then have "c#s \<notin> (L r1)\<star>; L r2" using bs1 by (auto simp add: lang_seq_def Cons_eq_append_conv)
-  then show "c#s \<notin> L (SEQ (STAR r1) r2)" by simp
-qed
-
-section {* Questions *}
-
-text {*
-  - Why was the key lemma k1 omitted; is there an easy, non-induction
-    way for obtaining this property? 
-  - Why was False included in the definition of the STAR-clause in
-    the matcher? Has this something to do with executing the code?
-  
-*}
-
-section {* Code *}
-   
-export_code dagger in SML module_name Dagger file - 
-export_code matcher in SML module_name Dagger file -
-
-section {* Examples *}
-
-text {* since now everything is based on lists, the evaluation is quite fast *}
-
-value "NULL ! []"
-value "(CHAR (CHR ''a'')) ! [CHR ''a'']"
-value "((CHAR a) ! [a,a])"
-value "(STAR (CHAR a)) ! []"
-value "(STAR (CHAR a)) ! [a,a]"
-value "(SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ! ''abbbbc''"
-value "(SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ! ''abbcbbc''"
-
-section {* Slind et al's matcher based on derivatives *}
-
-fun
- nullable :: "rexp \<Rightarrow> bool"
-where
-  "nullable (NULL) = False"
-| "nullable (EMPTY) = True"
-| "nullable (CHAR c) = False"
-| "nullable (ALT r1 r2) = ((nullable r1) \<or> (nullable r2))"
-| "nullable (SEQ r1 r2) = ((nullable r1) \<and> (nullable r2))"
-| "nullable (STAR r) = True"
-
-lemma nullable:
-  shows "([] \<in> L r) = nullable r"
-by (induct r)
-   (auto simp add: lang_seq_def) 
-
-fun
- der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
-where
-  "der c (NULL) = NULL"
-| "der c (EMPTY) = NULL"
-| "der c (CHAR c') = (if c=c' then EMPTY else NULL)"
-| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
-| "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)"
-| "der c (STAR r) = SEQ (der c r) (STAR r)"
-
-lemma k2:
-  assumes b: "s \<in> L1\<star>"
-  and a: "s \<noteq> []"
-  shows "s \<in> (L1; (L1\<star>))"
-using b a
-apply(induct rule: Star.induct)
-apply(simp)
-apply(case_tac "s1=[]")
-apply(simp)
-apply(simp add: lang_seq_def)
-apply(blast)
-done
-
-
-lemma der_correctness:
-  shows "(s \<in> L (der c r)) = ((c#s) \<in> L r)"
-proof (induct r arbitrary: s)
-  case (NULL s)
-  show "(s \<in> L (der c NULL)) = (c#s \<in> L NULL)" by simp
-next
-  case (EMPTY s)
-  show "(s \<in> L (der c EMPTY)) = (c#s \<in> L EMPTY)" by simp
-next
-  case (CHAR c' s)
-  show "(s \<in> L (der c (CHAR c'))) = (c#s \<in> L (CHAR c'))" by simp
-next
-  case (SEQ r1 r2 s)
-  have ih1: "\<And>s. (s \<in> L (der c r1)) = (c#s \<in> L r1)" by fact
-  have ih2: "\<And>s. (s \<in> L (der c r2)) = (c#s \<in> L r2)" by fact
-  show "(s \<in> L (der c (SEQ r1 r2))) = (c#s \<in> L (SEQ r1 r2))" 
-    using ih1 ih2
-    by (auto simp add: nullable[symmetric] lang_seq_def Cons_eq_append_conv)
-next
-  case (ALT r1 r2 s)
-  have ih1: "\<And>s. (s \<in> L (der c r1)) = (c#s \<in> L r1)" by fact
-  have ih2: "\<And>s. (s \<in> L (der c r2)) = (c#s \<in> L r2)" by fact
-  show "(s \<in> L (der c (ALT r1 r2))) = (c#s \<in> L (ALT r1 r2))"
-    using ih1 ih2 by (auto simp add: lang_seq_def)
-next
-  case (STAR r s)
-  have ih1: "\<And>s. (s \<in> L (der c r)) = (c#s \<in> L r)" by fact
-  show "(s \<in> L (der c (STAR r))) = (c#s \<in> L (STAR r))"
-    using ih1
-    apply(simp)
-    apply(auto simp add: lang_seq_def)
-    apply(drule lang_seq_append)
-    apply(assumption)
-    apply(simp)
-    apply(subst lang_star_cases)
-    apply(simp)
-    thm k1
-    apply(drule k2)
-    apply(simp)
-    apply(simp add: lang_seq_def)
-    apply(erule exE)+
-    apply(erule conjE)+
-    apply(auto simp add: lang_seq_def Cons_eq_append_conv)
-    apply(drule k1)
-    apply(simp)
-    apply(simp add: lang_seq_def)
-    apply(erule exE)+
-    apply(erule conjE)+
-    apply(auto simp add: lang_seq_def Cons_eq_append_conv)
-    done
-qed
-
-fun 
- derivative :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
-where
-  "derivative [] r = r"
-| "derivative (c#s) r = derivative s (der c r)"
-
-fun
-  slind_matcher :: "rexp \<Rightarrow> string \<Rightarrow> bool"
-where
-  "slind_matcher r s = nullable (derivative s r)"
-
-lemma slind_matcher:
-  shows "slind_matcher r s = (s \<in> L r)"
-by (induct s arbitrary: r)
-   (auto simp add: nullable der_correctness)
-
-export_code slind_matcher in SML module_name Slind file - 
-
-
-(* ******************************************** now is the codes writen by chunhan ************************************* *)
+(* ************ now is the codes writen by chunhan ************************************* *)
 
 section {* Arden's Lemma revised *}
 
@@ -922,7 +447,6 @@
 
 lemma seq_rhs_r_prop1:
   "L (seq_rhs_r rhs r) = (L rhs);(L r)"
-apply (rule set_ext, rule iffI)
 apply (auto simp:seq_rhs_r_def image_def lang_seq_def)
 apply (rule_tac x = "s1 @ s1a" in exI, rule_tac x = "s2a" in exI, simp)
 apply (rule_tac x = a in exI, rule_tac x = b in exI, simp)
@@ -936,13 +460,11 @@
 
 lemma del_x_paired_prop1:  
   "\<lbrakk>distinct_rhs rhs; (X, r) \<in> rhs\<rbrakk> \<Longrightarrow> X ; L r \<union> L (del_x_paired rhs X) = L rhs"
-apply (simp add:del_x_paired_def)
-apply (rule set_ext, rule iffI, simp)
-apply (erule disjE, rule_tac x = X in exI, rule_tac x = r in exI, simp)
-apply (clarify, rule_tac x = Xa in exI, rule_tac x = ra in exI, simp)
-apply (clarsimp, drule_tac x = Xa in spec, drule_tac x = ra in spec)
-apply (auto simp:distinct_rhs_def)
-done
+  apply (simp add:del_x_paired_def)
+  apply (simp add: distinct_rhs_def)
+  apply(auto simp add: lang_seq_def)
+  apply(metis)
+  done
 
 lemma arden_variate_prop:
   assumes "(X, rx) \<in> rhs"