1 theory RegExp

     2   imports "Main" 

     3 begin

     4 

     5 text {* sequential composition of languages *}

     6 

     7 definition

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

     9 where 

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

    11 

    12 lemma lang_seq_empty:

    13   shows "{[]} ; L = L"

    14   and   "L ; {[]} = L"

    15 unfolding lang_seq_def by auto

    16 

    17 lemma lang_seq_null:

    18   shows "{} ; L = {}"

    19   and   "L ; {} = {}"

    20 unfolding lang_seq_def by auto

    21 

    22 lemma lang_seq_append:

    23   assumes a: "s1 \<in> L1"

    24   and     b: "s2 \<in> L2"

    25   shows "s1@s2 \<in> L1 ; L2"

    26 unfolding lang_seq_def

    27 using a b by auto 

    28 

    29 lemma lang_seq_union:

    30   shows "(L1 \<union> L2); L3 = (L1; L3) \<union> (L2; L3)"

    31   and   "L1; (L2 \<union> L3) = (L1; L2) \<union> (L1; L3)"

    32 unfolding lang_seq_def by auto

    33 

    34 lemma lang_seq_assoc:

    35   shows "(L1 ; L2) ; L3 = L1 ; (L2 ; L3)"

    36 by (simp add: lang_seq_def Collect_def mem_def expand_fun_eq)

    37    (metis append_assoc)

    38 

    39 lemma lang_seq_minus:

    40   shows "(L1; L2) - {[]} =

    41            (if [] \<in> L1 then L2 - {[]} else {}) \<union> 

    42            (if [] \<in> L2 then L1 - {[]} else {}) \<union> ((L1 - {[]}); (L2 - {[]}))"

    43 apply(auto simp add: lang_seq_def)

    44 apply(metis mem_def self_append_conv)

    45 apply(metis mem_def self_append_conv2)

    46 apply(metis mem_def self_append_conv2)

    47 apply(metis mem_def self_append_conv)

    48 done

    49 

    50 section {* Kleene star for languages defined as least fixed point *}

    51 

    52 inductive_set

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

    54   for L :: "string set"

    55 where

    56   start[intro]: "[] \<in> L\<star>"

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

    58 

    59 lemma lang_star_empty:

    60   shows "{}\<star> = {[]}"

    61 by (auto elim: Star.cases)

    62 

    63 lemma lang_star_cases:

    64   shows "L\<star> =  {[]} \<union> L ; L\<star>"

    65 proof

    66   { fix x

    67     have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ; L\<star>"

    68       unfolding lang_seq_def

    69     by (induct rule: Star.induct) (auto)

    70   }

    71   then show "L\<star> \<subseteq> {[]} \<union> L ; L\<star>" by auto

    72 next

    73   show "{[]} \<union> L ; L\<star> \<subseteq> L\<star>" 

    74     unfolding lang_seq_def by auto

    75 qed

    76 

    77 lemma lang_star_cases':

    78   shows "L\<star> =  {[]} \<union> L\<star> ; L"

    79 proof

    80   { fix x

    81     have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L\<star> ; L"

    82       unfolding lang_seq_def

    83     apply (induct rule: Star.induct)

    84     apply simp

    85     apply simp

    86     apply (erule disjE)

    87     apply (auto)[1]

    88     apply (erule exE | erule conjE)+

    89     apply (rule disjI2)

    90     apply (rule_tac x = "s1 @ s1a" in exI)

    91     by auto

    92   }

    93   then show "L\<star> \<subseteq> {[]} \<union> L\<star> ; L" by auto

    94 next

    95   show "{[]} \<union> L\<star> ; L \<subseteq> L\<star>" 

    96     unfolding lang_seq_def

    97     apply auto

    98     apply (erule Star.induct)

    99     apply auto

   100     apply (drule step[of _ _ "[]"])

   101     by (auto intro:start)

   102 qed

   103 

   104 lemma lang_star_simple:

   105   shows "L \<subseteq> L\<star>"

   106 by (subst lang_star_cases)

   107    (auto simp only: lang_seq_def)

   108 

   109 lemma lang_star_prop0_aux:

   110   "s2 \<in> L\<star> \<Longrightarrow> \<forall> s1. s1 \<in> L \<longrightarrow> (\<exists> s3 s4. s3 \<in> L\<star> \<and> s4 \<in> L \<and> s1 @ s2 = s3 @ s4)" 

   111 apply (erule Star.induct)

   112 apply (clarify, rule_tac x = "[]" in exI, rule_tac x = s1 in exI, simp add:start)

   113 apply (clarify, drule_tac x = s1 in spec)

   114 apply (drule mp, simp, clarify)

   115 apply (rule_tac x = "s1a @ s3" in exI, rule_tac x = s4 in exI)

   116 by auto

   117 

   118 lemma lang_star_prop0:

   119   "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> \<exists> s3 s4. s3 \<in> L\<star> \<and> s4 \<in> L \<and> s1 @ s2 = s3 @ s4" 

   120 by (auto dest:lang_star_prop0_aux)

   121 

   122 lemma lang_star_prop1:

   123   assumes asm: "L1; L2 \<subseteq> L2" 

   124   shows "L1\<star>; L2 \<subseteq> L2"

   125 proof -

   126   { fix s1 s2

   127     assume minor: "s2 \<in> L2"

   128     assume major: "s1 \<in> L1\<star>"

   129     then have "s1@s2 \<in> L2"

   130     proof(induct rule: Star.induct)

   131       case start

   132       show "[]@s2 \<in> L2" using minor by simp

   133     next

   134       case (step s1 s1')

   135       have "s1 \<in> L1" by fact

   136       moreover

   137       have "s1'@s2 \<in> L2" by fact

   138       ultimately have "s1@(s1'@s2) \<in> L1; L2" by (auto simp add: lang_seq_def)

   139       with asm have "s1@(s1'@s2) \<in> L2" by auto

   140       then show "(s1@s1')@s2 \<in> L2" by simp

   141     qed

   142   } 

   143   then show "L1\<star>; L2 \<subseteq> L2" by (auto simp add: lang_seq_def)

   144 qed

   145 

   146 lemma lang_star_prop2_aux:

   147   "s2 \<in> L2\<star> \<Longrightarrow> \<forall> s1. s1 \<in> L1 \<and> L1 ; L2 \<subseteq> L1 \<longrightarrow> s1 @ s2 \<in> L1"

   148 apply (erule Star.induct, simp)

   149 apply (clarify, drule_tac x = "s1a @ s1" in spec)

   150 by (auto simp:lang_seq_def)

   151 

   152 lemma lang_star_prop2:

   153   "L1; L2 \<subseteq> L1 \<Longrightarrow> L1 ; L2\<star> \<subseteq> L1"

   154 by (auto dest!:lang_star_prop2_aux simp:lang_seq_def)

   155 

   156 lemma lang_star_seq_subseteq: 

   157   shows "L ; L\<star> \<subseteq> L\<star>"

   158 using lang_star_cases by blast

   159 

   160 lemma lang_star_double:

   161   shows "L\<star>; L\<star> = L\<star>"

   162 proof

   163   show "L\<star> ; L\<star> \<subseteq> L\<star>" 

   164     using lang_star_prop1 lang_star_seq_subseteq by blast

   165 next

   166   have "L\<star> \<subseteq> L\<star> \<union> L\<star>; (L; L\<star>)" by auto

   167   also have "\<dots> = L\<star>;{[]} \<union> L\<star>; (L; L\<star>)" by (simp add: lang_seq_empty)

   168   also have "\<dots> = L\<star>; ({[]} \<union> L; L\<star>)" by (simp only: lang_seq_union)

   169   also have "\<dots> = L\<star>; L\<star>" using lang_star_cases by simp 

   170   finally show "L\<star> \<subseteq> L\<star> ; L\<star>" by simp

   171 qed

   172 

   173 lemma lang_star_seq_subseteq': 

   174   shows "L\<star>; L \<subseteq> L\<star>"

   175 proof -

   176   have "L \<subseteq> L\<star>" by (rule lang_star_simple)

   177   then have "L\<star>; L \<subseteq> L\<star>; L\<star>" by (auto simp add: lang_seq_def)

   178   then show "L\<star>; L \<subseteq> L\<star>" using lang_star_double by blast

   179 qed

   180 

   181 lemma

   182   shows "L\<star> \<subseteq> L\<star>\<star>"

   183 by (rule lang_star_simple)

   184 

   185 section {* tricky section  *}

   186 

   187 lemma k1:

   188   assumes b: "s \<in> L\<star>"

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

   190   shows "s \<in> (L - {[]}); L\<star>"

   191 using b a

   192 apply(induct rule: Star.induct)

   193 apply(simp)

   194 apply(case_tac "s1=[]")

   195 apply(simp)

   196 apply(simp add: lang_seq_def)

   197 apply(blast)

   198 done

   199 

   200 section {* (relies on lemma k1) *}

   201 

   202 lemma zzz:

   203   shows "{s. c#s \<in> L1\<star>} = {s. c#s \<in> L1} ; (L1\<star>)"

   204 apply(auto simp add: lang_seq_def Cons_eq_append_conv)

   205 apply(drule k1)

   206 apply(auto)[1]

   207 apply(auto simp add: lang_seq_def)[1]

   208 apply(rule_tac x="tl s1" in exI)

   209 apply(rule_tac x="s2" in exI)

   210 apply(auto)[1]

   211 apply(auto simp add: Cons_eq_append_conv)[2]

   212 apply(drule lang_seq_append)

   213 apply(assumption)

   214 apply(rotate_tac 1)

   215 apply(drule rev_subsetD)

   216 apply(rule lang_star_seq_subseteq)

   217 apply(simp)

   218 done

   219 

   220 

   221 

   222 section {* regular expressions *}

   223 

   224 datatype rexp =

   225   NULL

   226 | EMPTY

   227 | CHAR char

   228 | SEQ rexp rexp

   229 | ALT rexp rexp

   230 | STAR rexp

   231 

   232 

   233 consts L:: "'a \<Rightarrow> string set"

   234 

   235 fun

   236   L_rexp :: "rexp \<Rightarrow> string set"

   237 where

   238   "L_rexp (NULL) = {}"

   239 | "L_rexp (EMPTY) = {[]}"

   240 | "L_rexp (CHAR c) = {[c]}"

   241 | "L_rexp (SEQ r1 r2) = (L_rexp r1) ; (L_rexp r2)"

   242 | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"

   243 | "L_rexp (STAR r) = (L_rexp r)\<star>"

   244 

   245 defs (overloaded)

   246   l_rexp_abs: "L rexp \<equiv> L_rexp rexp"

   247 

   248 declare L_rexp.simps [simp del] L_rexp.simps [folded l_rexp_abs, simp add]

   249 

   250 definition

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

   252 where

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

   254 

   255 lemma Ls_union:

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

   257 unfolding Ls_def by auto

   258 

   259 text {* helper function for termination proofs *}

   260 fun

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

   262 where

   263  "Left (SEQ r1 r2) = r1"

   264 

   265 text {* dagger function *}

   266 

   267 function

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

   269 where

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

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

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

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

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

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

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

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

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

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

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

   281 by (pat_completeness) (auto)

   282 

   283 termination dagger

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

   285 

   286 lemma dagger_correctness:

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

   288 proof (induct rule: dagger.induct)

   289   case (1 c)

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

   291 next  

   292   case (2 c)

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

   294 next

   295   case (3 c' c)

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

   297 next

   298   case (4 r1 r2 c)

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

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

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

   302     by (simp add: Ls_union ih1 ih2 Collect_disj_eq)

   303 next

   304   case (5 r2 c)

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

   306 next

   307   case (6 r2 c)

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

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

   310     by (simp add: ih lang_seq_empty)

   311 next

   312   case (7 c' r2 c)

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

   314     by (simp add: Ls_def lang_seq_def)

   315 next

   316   case (8 r11 r12 r2 c)

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

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

   319     by (simp add: ih lang_seq_assoc)

   320 next

   321   case (9 r11 r12 r2 c)

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

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

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

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

   326 next

   327   case (10 r1 r2 c)

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

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

   330   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))"

   331     by (auto simp add: lang_seq_def Ls_def)

   332   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

   333   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)

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

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

   336     by (auto simp add: lang_seq_def Cons_eq_append_conv)

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

   338     by (force simp add: lang_seq_def)

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

   340 next

   341   case (11 r c)

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

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

   344     by (auto simp add: lang_seq_def Ls_def)

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

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

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

   348 qed

   349 

   350 

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

   352 fun

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

   354 where

   355   "first_True [] = False"

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

   357 

   358 lemma not_first_True[simp]:

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

   360 by (induct xs) (auto)

   361 

   362 lemma first_True:

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

   364 by (induct xs) (auto)

   365 

   366 text {* matcher function *}

   367 

   368 function

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

   370 where

   371   "NULL ! s = False"

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

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

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

   375 | "STAR r ! [] = True"

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

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

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

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

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

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

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

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

   384 by (pat_completeness) (auto)

   385 

   386 termination matcher 

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

   388 

   389 text {* positive correctness of the matcher *}

   390 lemma matcher1:

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

   392 proof (induct rule: matcher.induct)

   393   case (1 s)

   394   have "NULL ! s" by fact

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

   396 next

   397   case (2 s)

   398   have "EMPTY ! s" by fact

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

   400 next

   401   case (3 c s)

   402   have "CHAR c ! s" by fact

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

   404 next

   405   case (4 r1 r2 s)

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

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

   408   have "ALT r1 r2 ! s" by fact

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

   410 next

   411   case (5 r)

   412   have "STAR r ! []" by fact 

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

   414 next

   415   case (6 r c s)

   416   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

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

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

   419     by (auto simp add: first_True)

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

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

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

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

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

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

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

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

   428 next

   429   case (7 r1 r2)

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

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

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

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

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

   435 next

   436   case (8 r2 c s)

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

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

   439 next

   440   case (9 r2 c s)

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

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

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

   444 next

   445   case (10 c' r2 c s)

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

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

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

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

   450 next

   451   case (11 r11 r12 r2 c s)

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

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

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

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

   456 next

   457   case (12 r11 r12 r2 c s)

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

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

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

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

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

   463 next

   464   case (13 r1 r2 c s)

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

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

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

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

   469   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)

   470   moreover

   471   { assume "r2 ! c#s"

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

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

   474       by (auto simp add: lang_seq_def)

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

   476   }

   477   moreover

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

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

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

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

   482     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)

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

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

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

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

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

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

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

   490   }

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

   492 qed

   493 

   494 text {* negative correctness of the matcher *}

   495 lemma matcher2:

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

   497 proof (induct rule: matcher.induct)

   498   case (1 s)

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

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

   501 next

   502   case (2 s)

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

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

   505 next

   506   case (3 c s)

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

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

   509 next

   510   case (4 r1 r2 s)

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

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

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

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

   515 next

   516   case (5 r)

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

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

   519 next

   520   case (6 r c s)

   521   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

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

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

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

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

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

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

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

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

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

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

   532 next

   533   case (7 r1 r2)

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

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

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

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

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

   539     by (auto simp add: lang_seq_def)

   540 next

   541   case (8 r2 c s)

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

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

   544 next

   545   case (9 r2 c s)

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

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

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

   549     using ih1 by (simp add: lang_seq_def)

   550 next

   551   case (10 c' r2 c s)

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

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

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

   555     using ih2 by (auto simp add: lang_seq_def)

   556 next

   557   case (11 r11 r12 r2 c s)

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

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

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

   561     using ih2 by (auto simp add: lang_seq_def)

   562 next

   563   case (12 r11 r12 r2 c s)

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

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

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

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

   568     using ih2 ih4 by (simp add: lang_seq_union)

   569 next

   570   case (13 r1 r2 c s)

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

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

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

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

   575   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

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

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

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

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

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

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

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

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

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

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

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

   587 qed

   588 

   589 section {* Questions *}

   590 

   591 text {*

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

   593     way for obtaining this property? 

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

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

   596   

   597 *}

   598 

   599 section {* Code *}

   600    

   601 export_code dagger in SML module_name Dagger file - 

   602 export_code matcher in SML module_name Dagger file -

   603 

   604 section {* Examples *}

   605 

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

   607 

   608 value "NULL ! []"

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

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

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

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

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

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

   615 

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

   617 

   618 fun

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

   620 where

   621   "nullable (NULL) = False"

   622 | "nullable (EMPTY) = True"

   623 | "nullable (CHAR c) = False"

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

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

   626 | "nullable (STAR r) = True"

   627 

   628 lemma nullable:

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

   630 by (induct r)

   631    (auto simp add: lang_seq_def) 

   632 

   633 fun

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

   635 where

   636   "der c (NULL) = NULL"

   637 | "der c (EMPTY) = NULL"

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

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

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

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

   642 

   643 lemma k2:

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

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

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

   647 using b a

   648 apply(induct rule: Star.induct)

   649 apply(simp)

   650 apply(case_tac "s1=[]")

   651 apply(simp)

   652 apply(simp add: lang_seq_def)

   653 apply(blast)

   654 done

   655 

   656 

   657 lemma der_correctness:

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

   659 proof (induct r arbitrary: s)

   660   case (NULL s)

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

   662 next

   663   case (EMPTY s)

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

   665 next

   666   case (CHAR c' s)

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

   668 next

   669   case (SEQ r1 r2 s)

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

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

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

   673     using ih1 ih2

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

   675 next

   676   case (ALT r1 r2 s)

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

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

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

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

   681 next

   682   case (STAR r s)

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

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

   685     using ih1

   686     apply(simp)

   687     apply(auto simp add: lang_seq_def)

   688     apply(drule lang_seq_append)

   689     apply(assumption)

   690     apply(simp)

   691     apply(subst lang_star_cases)

   692     apply(simp)

   693     thm k1

   694     apply(drule k2)

   695     apply(simp)

   696     apply(simp add: lang_seq_def)

   697     apply(erule exE)+

   698     apply(erule conjE)+

   699     apply(auto simp add: lang_seq_def Cons_eq_append_conv)

   700     apply(drule k1)

   701     apply(simp)

   702     apply(simp add: lang_seq_def)

   703     apply(erule exE)+

   704     apply(erule conjE)+

   705     apply(auto simp add: lang_seq_def Cons_eq_append_conv)

   706     done

   707 qed

   708 

   709 fun 

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

   711 where

   712   "derivative [] r = r"

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

   714 

   715 fun

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

   717 where

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

   719 

   720 lemma slind_matcher:

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

   722 by (induct s arbitrary: r)

   723    (auto simp add: nullable der_correctness)

   724 

   725 export_code slind_matcher in SML module_name Slind file - 

   726 

   727 

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

   729 

   730 section {* Arden's Lemma revised *}

   731 

   732 lemma arden_aux1:

   733   assumes a: "X \<subseteq> X ; A \<union> B"

   734   and     b: "[] \<notin> A"

   735   shows      "x \<in> X \<Longrightarrow> x \<in> B ; A\<star>"

   736 apply (induct x taking:length rule:measure_induct)

   737 apply (subgoal_tac "x \<in> X ; A \<union> B")

   738 defer

   739 using a

   740 apply (auto)[1]

   741 apply simp

   742 apply (erule disjE)

   743 defer

   744 apply (auto simp add:lang_seq_def) [1]

   745 apply (subgoal_tac "\<exists> x1 x2. x = x1 @ x2 \<and> x1 \<in> X \<and> x2 \<in> A")

   746 defer

   747 apply (auto simp add:lang_seq_def) [1]

   748 apply (erule exE | erule conjE)+

   749 apply simp

   750 apply (drule_tac x = x1 in spec)

   751 apply (simp)

   752 using b

   753 apply -

   754 apply (auto)[1]

   755 apply (subgoal_tac "x1 @ x2 \<in> (B ; A\<star>) ; A")

   756 defer

   757 apply (auto simp add:lang_seq_def)[1]

   758 by (metis Un_absorb1 lang_seq_assoc lang_seq_union(2) lang_star_double lang_star_simple mem_def sup1CI)

   759 

   760 theorem ardens_revised:

   761   assumes nemp: "[] \<notin> A"

   762   shows "(X = X ; A \<union> B) \<longleftrightarrow> (X = B ; A\<star>)"

   763 apply(rule iffI)

   764 defer

   765 apply(simp)

   766 apply(subst lang_star_cases')

   767 apply(subst lang_seq_union)

   768 apply(simp add: lang_seq_empty)

   769 apply(simp add: lang_seq_assoc)

   770 apply(auto)[1]

   771 proof -

   772   assume "X = X ; A \<union> B"

   773   then have as1: "X ; A \<union> B \<subseteq> X" and as2: "X \<subseteq> X ; A \<union> B" by simp_all

   774   from as1 have a: "X ; A \<subseteq> X" and b: "B \<subseteq> X" by simp_all

   775   from b have "B; A\<star> \<subseteq> X ; A\<star>" by (auto simp add: lang_seq_def)

   776   moreover

   777   from a have "X ; A\<star> \<subseteq> X" 

   778 

   779 by (rule lang_star_prop2)

   780   ultimately have f1: "B ; A\<star> \<subseteq> X" by simp

   781   from as2 nemp

   782   have f2: "X \<subseteq> B; A\<star>" using arden_aux1 by auto

   783   from f1 f2 show "X = B; A\<star>" by auto

   784 qed

   785 

   786 section {* equiv class' definition *}

   787 

   788 definition 

   789   equiv_str :: "string \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> bool" ("_ \<equiv>_\<equiv> _" [100, 100, 100] 100)

   790 where

   791   "x \<equiv>L'\<equiv> y \<longleftrightarrow> (\<forall>z. x@z \<in> L' \<longleftrightarrow> y@z \<in> L')"

   792 

   793 definition

   794   equiv_class :: "string \<Rightarrow> (string set) \<Rightarrow> string set" ("\<lbrakk>_\<rbrakk>_" [100, 100] 100)

   795 where

   796   "\<lbrakk>x\<rbrakk>L' \<equiv> {y. x \<equiv>L'\<equiv> y}"

   797 

   798 text {* Chunhan modifies Q to Quo *}

   799 definition  

   800   quot :: "string set \<Rightarrow> (string set) \<Rightarrow> (string set) set" ("_ Quo _" [100, 100] 100)

   801 where

   802   "L' Quo R \<equiv> { \<lbrakk>x\<rbrakk>R | x. x \<in> L'}" 

   803 

   804 lemma lang_eqs_union_of_eqcls: 

   805   "Lang = \<Union> {X. X \<in> (UNIV Quo Lang) \<and> (\<forall> x \<in> X. x \<in> Lang)}"

   806 proof

   807   show "Lang \<subseteq> \<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}"

   808   proof

   809     fix x

   810     assume "x \<in> Lang"

   811     thus "x \<in> \<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}"

   812     proof (simp add:quot_def)

   813       assume "(1)": "x \<in> Lang"

   814       show "\<exists>xa. (\<exists>x. xa = \<lbrakk>x\<rbrakk>Lang) \<and> (\<forall>x\<in>xa. x \<in> Lang) \<and> x \<in> xa" (is "\<exists>xa.?P xa")

   815       proof -

   816         have "?P (\<lbrakk>x\<rbrakk>Lang)" using "(1)"

   817           by (auto simp:equiv_class_def equiv_str_def dest: spec[where  x = "[]"])

   818         thus ?thesis by blast

   819       qed

   820     qed

   821   qed   

   822 next

   823   show "\<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang} \<subseteq> Lang"

   824     by auto

   825 qed

   826 

   827 lemma empty_notin_CS: "{} \<notin> UNIV Quo Lang"

   828 apply (clarsimp simp:quot_def equiv_class_def)

   829 by (rule_tac x = x in exI, auto simp:equiv_str_def)

   830 

   831 lemma no_two_cls_inters:

   832   "\<lbrakk>X \<in> UNIV Quo Lang; Y \<in> UNIV Quo Lang; X \<noteq> Y\<rbrakk> \<Longrightarrow> X \<inter> Y = {}"

   833 by (auto simp:quot_def equiv_class_def equiv_str_def)

   834 

   835 text {* equiv_class transition *}

   836 definition 

   837   CT :: "string set \<Rightarrow> char \<Rightarrow> string set \<Rightarrow> bool" ("_-_\<rightarrow>_" [99,99]99)

   838 where

   839   "X-c\<rightarrow>Y \<equiv> ((X;{[c]}) \<subseteq> Y)"

   840 

   841 types t_equa_rhs = "(string set \<times> rexp) set"

   842 

   843 types t_equa = "(string set \<times> t_equa_rhs)"

   844 

   845 types t_equas = "t_equa set"

   846 

   847 text {* "empty_rhs" generates "\<lambda>" for init-state, just like "\<lambda>" for final states in Brzozowski method. 

   848         But if the init-state is "{[]}" ("\<lambda>" itself) then empty set is returned, see definition of "equation_rhs" *} 

   849 definition 

   850   empty_rhs :: "string set \<Rightarrow> t_equa_rhs"

   851 where

   852   "empty_rhs X \<equiv> if ([] \<in> X) then {({[]}, EMPTY)} else {}"

   853 

   854 definition 

   855   folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"

   856 where

   857   "folds f z S \<equiv> SOME x. fold_graph f z S x"

   858 

   859 definition 

   860   equation_rhs :: "(string set) set \<Rightarrow> string set \<Rightarrow> t_equa_rhs"

   861 where

   862   "equation_rhs CS X \<equiv> if (X = {[]}) then {({[]}, EMPTY)}

   863                          else {(S, folds ALT NULL {CHAR c| c. S-c\<rightarrow>X} )| S. S \<in> CS} \<union> empty_rhs X"

   864 

   865 definition 

   866   equations :: "(string set) set \<Rightarrow> t_equas"

   867 where

   868   "equations CS \<equiv> {(X, equation_rhs CS X) | X. X \<in> CS}"

   869 

   870 definition

   871   L_rhs :: "t_equa_rhs \<Rightarrow> string set"

   872 where

   873   "L_rhs rhs \<equiv> {x. \<exists> X r. (X, r) \<in> rhs \<and> x \<in> X;(L r)}"

   874 

   875 defs (overloaded)

   876   l_rhs_abs: "L rhs \<equiv> L_rhs rhs"

   877 

   878 lemmas L_def = L_rhs_def [folded l_rhs_abs] L_rexp.simps (* ??? is this OK ?? *)

   879 

   880 definition 

   881   distinct_rhs :: "t_equa_rhs \<Rightarrow> bool"

   882 where

   883   "distinct_rhs rhs \<equiv> \<forall> X reg\<^isub>1 reg\<^isub>2. (X, reg\<^isub>1) \<in> rhs \<and> (X, reg\<^isub>2) \<in> rhs \<longrightarrow> reg\<^isub>1 = reg\<^isub>2"

   884 

   885 definition

   886   distinct_equas_rhs :: "t_equas \<Rightarrow> bool"

   887 where

   888   "distinct_equas_rhs equas \<equiv> \<forall> X rhs. (X, rhs) \<in> equas \<longrightarrow> distinct_rhs rhs"

   889 

   890 definition 

   891   distinct_equas :: "t_equas \<Rightarrow> bool"

   892 where

   893   "distinct_equas equas \<equiv> \<forall> X rhs rhs'. (X, rhs) \<in> equas \<and> (X, rhs') \<in> equas \<longrightarrow> rhs = rhs'"

   894 

   895 definition 

   896   seq_rhs_r :: "t_equa_rhs \<Rightarrow> rexp \<Rightarrow> t_equa_rhs"

   897 where

   898   "seq_rhs_r rhs r \<equiv> (\<lambda>(X, reg). (X, SEQ reg r)) ` rhs"

   899 

   900 definition 

   901   del_x_paired :: "('a \<times> 'b) set \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'b) set"

   902 where

   903   "del_x_paired S x \<equiv> S - {X. X \<in> S \<and> fst X = x}"

   904 

   905 definition

   906   arden_variate :: "string set \<Rightarrow> rexp \<Rightarrow> t_equa_rhs \<Rightarrow> t_equa_rhs"

   907 where

   908   "arden_variate X r rhs \<equiv> seq_rhs_r (del_x_paired rhs X) (STAR r)"

   909 

   910 definition

   911   no_EMPTY_rhs :: "t_equa_rhs \<Rightarrow> bool"

   912 where

   913   "no_EMPTY_rhs rhs \<equiv> \<forall> X r. (X, r) \<in> rhs \<and> X \<noteq> {[]} \<longrightarrow> [] \<notin> L r"

   914 

   915 definition 

   916   no_EMPTY_equas :: "t_equas \<Rightarrow> bool"

   917 where

   918   "no_EMPTY_equas equas \<equiv> \<forall> X rhs. (X, rhs) \<in> equas \<longrightarrow> no_EMPTY_rhs rhs"

   919 

   920 lemma fold_alt_null_eqs:

   921   "finite rS \<Longrightarrow> x \<in> L (folds ALT NULL rS) = (\<exists> r \<in> rS. x \<in> L r)"

   922 apply (simp add:folds_def)

   923 apply (rule someI2_ex)

   924 apply (erule finite_imp_fold_graph)

   925 apply (erule fold_graph.induct)

   926 by auto (*??? how do this be in Isar ?? *)

   927 

   928 lemma seq_rhs_r_prop1:

   929   "L (seq_rhs_r rhs r) = (L rhs);(L r)"

   930 apply (rule set_ext, rule iffI)

   931 apply (auto simp:L_def seq_rhs_r_def image_def lang_seq_def)

   932 apply (rule_tac x = "s1 @ s1a" in exI, rule_tac x = "s2a" in exI, simp)

   933 apply (rule_tac x = a in exI, rule_tac x = b in exI, simp)

   934 apply (rule_tac x = s1 in exI, rule_tac x = s1a in exI, simp)

   935 apply (rule_tac x = X in exI, rule_tac x  = "SEQ ra r" in exI, simp)

   936 apply (rule conjI)

   937 apply (rule_tac x = "(X, ra)" in bexI, simp+) 

   938 apply (rule_tac x = s1a in exI, rule_tac x = "s2a @ s2" in exI, simp)

   939 apply (simp add:lang_seq_def)

   940 by (rule_tac x = s2a in exI, rule_tac x = s2 in exI, simp)

   941 

   942 lemma del_x_paired_prop1:  

   943   "\<lbrakk>distinct_rhs rhs; (X, r) \<in> rhs\<rbrakk> \<Longrightarrow> X ; L r \<union> L (del_x_paired rhs X) = L rhs"

   944 apply (simp add:L_def del_x_paired_def)

   945 apply (rule set_ext, rule iffI, simp)

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

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

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

   949 apply (auto simp:distinct_rhs_def)

   950 done

   951 

   952 lemma arden_variate_prop:

   953   assumes "(X, rx) \<in> rhs"

   954   shows "(\<forall> Y. Y \<noteq> X \<longrightarrow> (\<exists> r. (Y, r) \<in> rhs) = (\<exists> r. (Y, r) \<in> (arden_variate X rx rhs)))"

   955 proof (rule allI, rule impI)

   956   fix Y

   957   assume "(1)": "Y \<noteq> X"

   958   show "(\<exists>r. (Y, r) \<in> rhs) = (\<exists>r. (Y, r) \<in> arden_variate X rx rhs)"

   959   proof

   960     assume "(1_1)": "\<exists>r. (Y, r) \<in> rhs"

   961     show "\<exists>r. (Y, r) \<in> arden_variate X rx rhs" (is "\<exists>r. ?P r")

   962     proof -

   963       from "(1_1)" obtain r where "(Y, r) \<in> rhs" ..

   964       hence "?P (SEQ r (STAR rx))"

   965       proof (simp add:arden_variate_def image_def)

   966         have "(Y, r) \<in> rhs \<Longrightarrow> (Y, r) \<in> del_x_paired rhs X"

   967           by (auto simp:del_x_paired_def "(1)")

   968         thus "(Y, r) \<in> rhs \<Longrightarrow> (Y, SEQ r (STAR rx)) \<in> seq_rhs_r (del_x_paired rhs X) (STAR rx)"

   969           by (auto simp:seq_rhs_r_def)

   970       qed

   971       thus ?thesis by blast

   972     qed

   973   next

   974     assume "(2_1)": "\<exists>r. (Y, r) \<in> arden_variate X rx rhs"

   975     thus "\<exists>r. (Y, r) \<in> rhs" (is "\<exists> r. ?P r")

   976       by (auto simp:arden_variate_def del_x_paired_def seq_rhs_r_def image_def)

   977   qed

   978 qed

   979 

   980 text {*

   981   arden_variate_valid:  proves variation from "X = X;r + Y;ry + \<dots>" to "X = Y;(SEQ ry (STAR r)) + \<dots>" holds the law of "language of left equiv language of right" 

   982 *}

   983 lemma arden_variate_valid:

   984   assumes X_not_empty: "X \<noteq> {[]}"

   985   and     l_eq_r:   "X = L rhs"

   986   and     dist: "distinct_rhs rhs"

   987   and     no_empty: "no_EMPTY_rhs rhs"

   988   and     self_contained: "(X, r) \<in> rhs"

   989   shows   "X = L (arden_variate X r rhs)" 

   990 proof -

   991   have "[] \<notin> L r" using no_empty X_not_empty self_contained

   992     by (auto simp:no_EMPTY_rhs_def)

   993   hence ardens: "X = X;(L r) \<union> (L (del_x_paired rhs X)) \<longleftrightarrow> X = (L (del_x_paired rhs X)) ; (L r)\<star>" 

   994     by (rule ardens_revised)

   995   have del_x: "X = X ; L r \<union> L (del_x_paired rhs X) \<longleftrightarrow> X = L rhs" using dist l_eq_r self_contained

   996     by (auto dest:del_x_paired_prop1)

   997   show ?thesis

   998   proof

   999     show "X \<subseteq> L (arden_variate X r rhs)"

  1000     proof

  1001       fix x

  1002       assume "(1_1)": "x \<in> X" with l_eq_r ardens del_x

  1003       show "x \<in> L (arden_variate X r rhs)" 

  1004         by (simp add:arden_variate_def seq_rhs_r_prop1)

  1005     qed

  1006   next

  1007     show "L (arden_variate X r rhs) \<subseteq> X"

  1008     proof

  1009       fix x

  1010       assume "(2_1)": "x \<in> L (arden_variate X r rhs)" with ardens del_x l_eq_r

  1011       show "x \<in> X" 

  1012         by (simp add:arden_variate_def seq_rhs_r_prop1)

  1013     qed

  1014   qed

  1015 qed

  1016 

  1017 text {* merge_rhs {(X1, r1), (x2, r2}, (x4, r4), \<dots>} {(x1, r1'), (x3, r3'), \<dots>} = {(x1, ALT r1 r1'}, (x2, r2), (x3, r3'), (x4, r4), \<dots>} *}  

  1018 definition 

  1019   merge_rhs :: "t_equa_rhs \<Rightarrow> t_equa_rhs \<Rightarrow> t_equa_rhs"

  1020 where

  1021   "merge_rhs rhs rhs' \<equiv> {(X, r). (\<exists> r1 r2. ((X,r1) \<in> rhs \<and> (X, r2) \<in> rhs') \<and> r = ALT r1 r2)  \<or>

  1022                                  (\<exists> r1. (X, r1) \<in> rhs \<and> (\<not> (\<exists> r2. (X, r2) \<in> rhs')) \<and> r = r1) \<or>

  1023                                  (\<exists> r2. (X, r2) \<in> rhs' \<and> (\<not> (\<exists> r1. (X, r1) \<in> rhs)) \<and> r = r2)    }"                                  

  1024 

  1025 

  1026 text {* rhs_subst rhs X=xrhs r: substitude all occurence of X in rhs((X,r) \<in> rhs) with xrhs *}

  1027 definition 

  1028   rhs_subst :: "t_equa_rhs \<Rightarrow> string set \<Rightarrow> t_equa_rhs \<Rightarrow> rexp \<Rightarrow> t_equa_rhs"

  1029 where

  1030   "rhs_subst rhs X xrhs r \<equiv> merge_rhs (del_x_paired rhs X) (seq_rhs_r xrhs r)"

  1031 

  1032 definition 

  1033   equas_subst_f :: "string set \<Rightarrow> t_equa_rhs \<Rightarrow> t_equa \<Rightarrow> t_equa"

  1034 where

  1035   "equas_subst_f X xrhs equa \<equiv> let (Y, rhs) = equa in

  1036                                  if (\<exists> r. (X, r) \<in> rhs)

  1037                                  then (Y, rhs_subst rhs X xrhs (SOME r. (X, r) \<in> rhs))

  1038                                  else equa"

  1039 

  1040 definition

  1041   equas_subst :: "t_equas \<Rightarrow> string set \<Rightarrow> t_equa_rhs \<Rightarrow> t_equas"

  1042 where

  1043   "equas_subst ES X xrhs \<equiv> del_x_paired (equas_subst_f X xrhs ` ES) X"

  1044 

  1045 lemma lang_seq_prop1:

  1046  "x \<in> X ; L r \<Longrightarrow> x \<in> X ; (L r \<union> L r')"

  1047 by (auto simp:lang_seq_def)

  1048 

  1049 lemma lang_seq_prop1':

  1050   "x \<in> X; L r \<Longrightarrow> x \<in> X ; (L r' \<union> L r)"

  1051 by (auto simp:lang_seq_def)

  1052 

  1053 lemma lang_seq_prop2:

  1054   "x \<in> X; (L r \<union> L r') \<Longrightarrow> x \<in> X;L r \<or> x \<in> X;L r'"

  1055 by (auto simp:lang_seq_def)

  1056 

  1057 lemma merge_rhs_prop1:

  1058   shows "L (merge_rhs rhs rhs') = L rhs \<union> L rhs' "

  1059 apply (auto simp add:merge_rhs_def L_def dest!:lang_seq_prop2 intro:lang_seq_prop1)

  1060 apply (rule_tac x = X in exI, rule_tac x = r1 in exI, simp)

  1061 apply (case_tac "\<exists> r2. (X, r2) \<in> rhs'")

  1062 apply (clarify, rule_tac x = X in exI, rule_tac x = "ALT r r2" in exI, simp add:lang_seq_prop1)

  1063 apply (rule_tac x = X in exI, rule_tac x = r in exI, simp)

  1064 apply (case_tac "\<exists> r1. (X, r1) \<in> rhs")

  1065 apply (clarify, rule_tac x = X in exI, rule_tac x = "ALT r1 r" in exI, simp add:lang_seq_prop1')

  1066 apply (rule_tac x = X in exI, rule_tac x = r in exI, simp)

  1067 done

  1068 

  1069 lemma no_EMPTY_rhss_imp_merge_no_EMPTY:

  1070   "\<lbrakk>no_EMPTY_rhs rhs; no_EMPTY_rhs rhs'\<rbrakk> \<Longrightarrow> no_EMPTY_rhs (merge_rhs rhs rhs')"

  1071 apply (simp add:no_EMPTY_rhs_def merge_rhs_def)

  1072 apply (clarify, (erule conjE | erule exE | erule disjE)+)

  1073 by auto

  1074 

  1075 lemma distinct_rhs_prop:

  1076   "\<lbrakk>distinct_rhs rhs; (X, r1) \<in> rhs; (X, r2) \<in> rhs\<rbrakk> \<Longrightarrow> r1 = r2"

  1077 by (auto simp:distinct_rhs_def)

  1078 

  1079 lemma merge_rhs_prop2:

  1080   assumes dist_rhs: "distinct_rhs rhs"

  1081   and     dist_rhs':"distinct_rhs rhs'"

  1082   shows "distinct_rhs (merge_rhs rhs rhs')"

  1083 apply (auto simp:merge_rhs_def distinct_rhs_def)

  1084 using dist_rhs

  1085 apply (drule distinct_rhs_prop, simp+)

  1086 using dist_rhs'

  1087 apply (drule distinct_rhs_prop, simp+)

  1088 using dist_rhs

  1089 apply (drule distinct_rhs_prop, simp+)

  1090 using dist_rhs'

  1091 apply (drule distinct_rhs_prop, simp+)

  1092 done

  1093 

  1094 lemma seq_rhs_r_holds_distinct: 

  1095   "distinct_rhs rhs \<Longrightarrow> distinct_rhs (seq_rhs_r rhs r)"

  1096 by (auto simp:distinct_rhs_def seq_rhs_r_def)

  1097 

  1098 lemma seq_rhs_r_prop0:

  1099   assumes l_eq_r: "X = L xrhs"

  1100   shows "L (seq_rhs_r xrhs r) = X ; L r "

  1101 using l_eq_r

  1102 by (auto simp:seq_rhs_r_prop1)

  1103 

  1104 lemma rhs_subst_prop1:

  1105   assumes l_eq_r: "X = L xrhs"

  1106   and     dist:  "distinct_rhs rhs"

  1107   shows "(X, r) \<in> rhs \<Longrightarrow> L rhs = L (rhs_subst rhs X xrhs r)"

  1108 apply (simp add:rhs_subst_def merge_rhs_prop1)

  1109 using l_eq_r 

  1110 apply (drule_tac r = r in seq_rhs_r_prop0, simp)

  1111 using dist

  1112 apply (auto dest:del_x_paired_prop1)

  1113 done

  1114 

  1115 lemma del_x_paired_holds_distinct_rhs:

  1116   "distinct_rhs rhs \<Longrightarrow> distinct_rhs (del_x_paired rhs x)"

  1117 by (auto simp:distinct_rhs_def del_x_paired_def)

  1118 

  1119 lemma rhs_subst_holds_distinct_rhs:

  1120   "\<lbrakk>distinct_rhs rhs; distinct_rhs xrhs\<rbrakk> \<Longrightarrow> distinct_rhs (rhs_subst rhs X xrhs r)"

  1121 apply (drule_tac r = r and rhs = xrhs in seq_rhs_r_holds_distinct)

  1122 apply (drule_tac x = X in del_x_paired_holds_distinct_rhs)

  1123 by (auto dest:merge_rhs_prop2[where rhs = "del_x_paired rhs X"] simp:rhs_subst_def)

  1124 

  1125 section {* myhill-nerode theorem *}

  1126 

  1127 definition left_eq_cls :: "t_equas \<Rightarrow> (string set) set"

  1128 where

  1129   "left_eq_cls ES \<equiv> {X. \<exists> rhs. (X, rhs) \<in> ES} "

  1130 

  1131 definition right_eq_cls :: "t_equas \<Rightarrow> (string set) set"

  1132 where

  1133   "right_eq_cls ES \<equiv> {Y. \<exists> X rhs r. (X, rhs) \<in> ES \<and> (Y, r) \<in> rhs }"

  1134 

  1135 definition rhs_eq_cls :: "t_equa_rhs \<Rightarrow> (string set) set"