1    

     2 theory ReTest

     3   imports "Main" 

     4 begin

     5 

     6 

     7 section {* Sequential Composition of Sets *}

     8 

     9 definition

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

    11 where 

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

    13 

    14 fun spow where

    15   "spow s 0 = []"

    16 | "spow s (Suc n) = s @ spow s n"

    17 

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

    19 

    20 lemma seq_empty [simp]:

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

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

    23 by (simp_all add: Sequ_def)

    24 

    25 lemma seq_null [simp]:

    26   shows "A ;; {} = {}"

    27   and   "{} ;; A = {}"

    28 by (simp_all add: Sequ_def)

    29 

    30 definition

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

    32 where

    33   "Der c A \<equiv> {s. [c] @ s \<in> A}"

    34 

    35 definition 

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

    37 where  

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

    39 

    40 lemma Der_null [simp]:

    41   shows "Der c {} = {}"

    42 unfolding Der_def

    43 by auto

    44 

    45 lemma Der_empty [simp]:

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

    47 unfolding Der_def

    48 by auto

    49 

    50 lemma Der_char [simp]:

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

    52 unfolding Der_def

    53 by auto

    54 

    55 lemma Der_union [simp]:

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

    57 unfolding Der_def

    58 by auto

    59 

    60 lemma Der_seq [simp]:

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

    62 unfolding Der_def Sequ_def

    63 apply (auto simp add: Cons_eq_append_conv)

    64 done

    65 

    66 lemma seq_image:

    67   assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"

    68   shows "f ` (A ;; B) = (f ` A) ;; (f ` B)"

    69 apply(auto simp add: Sequ_def image_def)

    70 apply(rule_tac x="f s1" in exI)

    71 apply(rule_tac x="f s2" in exI)

    72 using assms

    73 apply(auto)

    74 apply(rule_tac x="xa @ xb" in exI)

    75 using assms

    76 apply(auto)

    77 done

    78 

    79 section {* Kleene Star for Sets *}

    80 

    81 inductive_set

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

    83   for A :: "string set"

    84 where

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

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

    87 

    88 lemma star_cases:

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

    90 unfolding Sequ_def

    91 by (auto) (metis Star.simps)

    92 

    93 

    94 fun 

    95   pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [100,100] 100)

    96 where

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

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

    99 

   100 lemma star1: 

   101   shows "s \<in> A\<star> \<Longrightarrow> \<exists>n. s \<in> A \<up> n"

   102   apply(induct rule: Star.induct)

   103   apply (metis pow.simps(1) insertI1)

   104   apply(auto)

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

   106   apply(auto simp add: Sequ_def)

   107   done

   108 

   109 lemma star2:

   110   shows "s \<in> A \<up> n \<Longrightarrow> s \<in> A\<star>"

   111   apply(induct n arbitrary: s)

   112   apply (metis pow.simps(1) Star.simps empty_iff insertE)

   113   apply(auto simp add: Sequ_def)

   114   done

   115 

   116 lemma star3:

   117   shows "A\<star> = (\<Union>i. A \<up> i)"

   118 using star1 star2

   119 apply(auto)

   120 done

   121 

   122 lemma star4:

   123   shows "s \<in> A \<up> n \<Longrightarrow> \<exists>ss. s = concat ss \<and> (\<forall>s' \<in> set ss. s' \<in> A)"

   124   apply(induct n arbitrary: s)

   125   apply(auto simp add: Sequ_def)

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

   127   apply(auto)

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

   129   apply(auto)

   130 by (metis concat.simps(2) insertE set_simps(2))

   131 

   132 lemma star5:

   133   assumes "f [] = []"

   134   assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"

   135   shows "(f ` A) \<up> n = f ` (A \<up> n)"

   136 apply(induct n)

   137 apply(simp add: assms)

   138 apply(simp)

   139 apply(subst seq_image[OF assms(2)])

   140 apply(simp)

   141 done

   142 

   143 lemma star6:

   144   assumes "f [] = []"

   145   assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"

   146   shows "(f ` A)\<star> = f ` (A\<star>)"

   147 apply(simp add: star3)

   148 apply(simp add: image_UN)

   149 apply(subst star5[OF assms])

   150 apply(simp)

   151 done

   152 

   153 lemma star_decomp: 

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

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

   156 using a

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

   158    (auto simp add: append_eq_Cons_conv)

   159 

   160 lemma Der_star [simp]:

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

   162 proof -    

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

   164     

   165     by (simp only: star_cases[symmetric])

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

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

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

   169     by simp

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

   171     unfolding Sequ_def Der_def

   172     by (auto dest: star_decomp)

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

   174 qed

   175 

   176 

   177 

   178 section {* Regular Expressions *}

   179 

   180 datatype rexp =

   181   NULL

   182 | EMPTY

   183 | CHAR char

   184 | SEQ rexp rexp

   185 | ALT rexp rexp

   186 | STAR rexp

   187 

   188 section {* Semantics of Regular Expressions *}

   189  

   190 fun

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

   192 where

   193   "L (NULL) = {}"

   194 | "L (EMPTY) = {[]}"

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

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

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

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

   199 

   200 fun

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

   202 where

   203   "nullable (NULL) = False"

   204 | "nullable (EMPTY) = True"

   205 | "nullable (CHAR c) = False"

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

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

   208 | "nullable (STAR r) = True"

   209 

   210 lemma nullable_correctness:

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

   212 apply (induct r) 

   213 apply(auto simp add: Sequ_def) 

   214 done

   215 

   216 

   217 

   218 section {* Values *}

   219 

   220 datatype val = 

   221   Void

   222 | Char char

   223 | Seq val val

   224 | Right val

   225 | Left val

   226 | Stars "val list"

   227 

   228 section {* The string behind a value *}

   229 

   230 fun 

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

   232 where

   233   "flat (Void) = []"

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

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

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

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

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

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

   240 

   241 lemma [simp]:

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

   243 apply(induct vs)

   244 apply(auto)

   245 done

   246 

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

   248 

   249 inductive 

   250   NPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)

   251 where

   252  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"

   253 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"

   254 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"

   255 | "\<Turnstile> Void : EMPTY"

   256 | "\<Turnstile> Char c : CHAR c"

   257 | "\<Turnstile> Stars [] : STAR r"

   258 | "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Stars vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"

   259 

   260 inductive 

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

   262 where

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

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

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

   266 | "\<turnstile> Void : EMPTY"

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

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

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

   270 

   271 lemma NPrf_imp_Prf:

   272   assumes "\<Turnstile> v : r" 

   273   shows "\<turnstile> v : r"

   274 using assms

   275 apply(induct)

   276 apply(auto intro: Prf.intros)

   277 done

   278 

   279 lemma NPrf_Prf_val:

   280   shows "\<turnstile> v : r \<Longrightarrow> \<exists>v'. flat v' = flat v \<and> \<Turnstile> v' : r"

   281   and   "\<turnstile> Stars vs : r \<Longrightarrow> \<exists>vs'. flat (Stars vs') = flat (Stars vs) \<and> \<Turnstile> Stars vs' : r"

   282 using assms

   283 apply(induct v and vs arbitrary: r and r rule: val.inducts)

   284 apply(auto)[1]

   285 apply(erule Prf.cases)

   286 apply(simp_all)[7]

   287 apply(rule_tac x="Void" in exI)

   288 apply(simp)

   289 apply(rule NPrf.intros)

   290 apply(erule Prf.cases)

   291 apply(simp_all)[7]

   292 apply(rule_tac x="Char c" in exI)

   293 apply(simp)

   294 apply(rule NPrf.intros)

   295 apply(erule Prf.cases)

   296 apply(simp_all)[7]

   297 apply(auto)[1]

   298 apply(drule_tac x="r1" in meta_spec)

   299 apply(drule_tac x="r2" in meta_spec)

   300 apply(simp)

   301 apply(auto)[1]

   302 apply(rule_tac x="Seq v' v'a" in exI)

   303 apply(simp)

   304 apply (metis NPrf.intros(1))

   305 apply(erule Prf.cases)

   306 apply(simp_all)[7]

   307 apply(clarify)

   308 apply(drule_tac x="r2" in meta_spec)

   309 apply(simp)

   310 apply(auto)[1]

   311 apply(rule_tac x="Right v'" in exI)

   312 apply(simp)

   313 apply (metis NPrf.intros)

   314 apply(erule Prf.cases)

   315 apply(simp_all)[7]

   316 apply(clarify)

   317 apply(drule_tac x="r1" in meta_spec)

   318 apply(simp)

   319 apply(auto)[1]

   320 apply(rule_tac x="Left v'" in exI)

   321 apply(simp)

   322 apply (metis NPrf.intros)

   323 apply(drule_tac x="r" in meta_spec)

   324 apply(simp)

   325 apply(auto)[1]

   326 apply(rule_tac x="Stars vs'" in exI)

   327 apply(simp)

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

   329 apply(simp)

   330 apply(erule Prf.cases)

   331 apply(simp_all)[7]

   332 apply (metis NPrf.intros(6))

   333 apply(erule Prf.cases)

   334 apply(simp_all)[7]

   335 apply(auto)[1]

   336 apply(drule_tac x="ra" in meta_spec)

   337 apply(simp)

   338 apply(drule_tac x="STAR ra" in meta_spec)

   339 apply(simp)

   340 apply(auto)

   341 apply(case_tac "flat v = []")

   342 apply(rule_tac x="vs'" in exI)

   343 apply(simp)

   344 apply(rule_tac x="v' # vs'" in exI)

   345 apply(simp)

   346 apply(rule NPrf.intros)

   347 apply(auto)

   348 done

   349 

   350 lemma NPrf_Prf:

   351   shows "{flat v | v. \<turnstile> v : r} = {flat v | v. \<Turnstile> v : r}"

   352 apply(auto)

   353 apply (metis NPrf_Prf_val(1))

   354 by (metis NPrf_imp_Prf)

   355 

   356 

   357 lemma not_nullable_flat:

   358   assumes "\<turnstile> v : r" "\<not>nullable r"

   359   shows "flat v \<noteq> []"

   360 using assms

   361 apply(induct)

   362 apply(auto)

   363 done

   364 

   365 lemma Prf_flat_L:

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

   367 using assms

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

   369 apply(auto simp add: Sequ_def)

   370 done

   371 

   372 lemma NPrf_flat_L:

   373   assumes "\<Turnstile> v : r" shows "flat v \<in> L r"

   374 using assms

   375 by (metis NPrf_imp_Prf Prf_flat_L)

   376 

   377 lemma Prf_Stars:

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

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

   380 using assms

   381 apply(induct vs)

   382 apply (metis Prf.intros(6))

   383 by (metis Prf.intros(7) insert_iff set_simps(2))

   384 

   385 lemma Star_string:

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

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

   388 using assms

   389 apply(induct rule: Star.induct)

   390 apply(auto)

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

   392 apply(simp)

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

   394 apply(simp)

   395 done

   396 

   397 lemma Star_val:

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

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

   400 using assms

   401 apply(induct ss)

   402 apply(auto)

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

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

   405 

   406 lemma Star_valN:

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

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

   409 using assms

   410 apply(induct ss)

   411 apply(auto)

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

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

   414 

   415 lemma L_flat_Prf:

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

   417 apply(induct r)

   418 apply(auto dest: Prf_flat_L simp add: Sequ_def)

   419 apply (metis Prf.intros(4) flat.simps(1))

   420 apply (metis Prf.intros(5) flat.simps(2))

   421 apply (metis Prf.intros(1) flat.simps(5))

   422 apply (metis Prf.intros(2) flat.simps(3))

   423 apply (metis Prf.intros(3) flat.simps(4))

   424 apply(erule Prf.cases)

   425 apply(auto)

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

   427 apply(auto)[1]

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

   429 apply(simp)

   430 apply(rule Prf_Stars)

   431 apply(simp)

   432 apply(drule Star_string)

   433 apply(auto)

   434 apply(rule Star_val)

   435 apply(simp)

   436 done

   437 

   438 lemma L_flat_NPrf:

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

   440 by (metis L_flat_Prf NPrf_Prf)

   441 

   442 text {* nicer proofs by Fahad *}

   443 

   444 lemma Prf_Star_flat_L:

   445   assumes "\<turnstile> v : STAR r" shows "flat v \<in> (L r)\<star>"

   446 using assms

   447 apply(induct v r\<equiv>"STAR r" arbitrary: r rule: Prf.induct)

   448 apply(auto)

   449 apply(simp add: star3)

   450 apply(auto)

   451 apply(rule_tac x="Suc x" in exI)

   452 apply(auto simp add: Sequ_def)

   453 apply(rule_tac x="flat v" in exI)

   454 apply(rule_tac x="flat (Stars vs)" in exI)

   455 apply(auto)

   456 by (metis Prf_flat_L)

   457 

   458 lemma L_flat_Prf2:

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

   460 apply(induct r)

   461 apply(auto)

   462 using L.simps(1) Prf_flat_L 

   463 apply(blast)

   464 using Prf.intros(4) 

   465 apply(force)

   466 using L.simps(2) Prf_flat_L 

   467 apply(blast)

   468 using Prf.intros(5) apply force

   469 using L.simps(3) Prf_flat_L apply blast

   470 using L_flat_Prf apply auto[1]

   471 apply (smt L.simps(4) Sequ_def mem_Collect_eq)

   472 using Prf_flat_L 

   473 apply(fastforce)

   474 apply(metis Prf.intros(2) flat.simps(3))

   475 apply(metis Prf.intros(3) flat.simps(4))

   476 apply(erule Prf.cases)

   477 apply(simp)

   478 apply(simp)

   479 apply(auto)

   480 using L_flat_Prf apply auto[1]

   481 apply (smt Collect_cong L.simps(6) mem_Collect_eq)

   482 using Prf_Star_flat_L 

   483 apply(fastforce)

   484 done

   485 

   486 

   487 section {* Values Sets *}

   488 

   489 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100)

   490 where

   491   "s1 \<sqsubseteq> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"

   492 

   493 definition sprefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)

   494 where

   495   "s1 \<sqsubset> s2 \<equiv> (s1 \<sqsubseteq> s2 \<and> s1 \<noteq> s2)"

   496 

   497 lemma length_sprefix:

   498   "s1 \<sqsubset> s2 \<Longrightarrow> length s1 < length s2"

   499 unfolding sprefix_def prefix_def

   500 by (auto)

   501 

   502 definition Prefixes :: "string \<Rightarrow> string set" where

   503   "Prefixes s \<equiv> {sp. sp \<sqsubseteq> s}"

   504 

   505 definition Suffixes :: "string \<Rightarrow> string set" where

   506   "Suffixes s \<equiv> rev ` (Prefixes (rev s))"

   507 

   508 definition SPrefixes :: "string \<Rightarrow> string set" where

   509   "SPrefixes s \<equiv> {sp. sp \<sqsubset> s}"

   510 

   511 definition SSuffixes :: "string \<Rightarrow> string set" where

   512   "SSuffixes s \<equiv> rev ` (SPrefixes (rev s))"

   513 

   514 lemma Suffixes_in: 

   515   "\<exists>s1. s1 @ s2 = s3 \<Longrightarrow> s2 \<in> Suffixes s3"

   516 unfolding Suffixes_def Prefixes_def prefix_def image_def

   517 apply(auto)

   518 by (metis rev_rev_ident)

   519 

   520 lemma SSuffixes_in: 

   521   "\<exists>s1. s1 \<noteq> [] \<and> s1 @ s2 = s3 \<Longrightarrow> s2 \<in> SSuffixes s3"

   522 unfolding SSuffixes_def Suffixes_def SPrefixes_def Prefixes_def sprefix_def prefix_def image_def

   523 apply(auto)

   524 by (metis append_self_conv rev.simps(1) rev_rev_ident)

   525 

   526 lemma Prefixes_Cons:

   527   "Prefixes (c # s) = {[]} \<union> {c # sp | sp. sp \<in> Prefixes s}"

   528 unfolding Prefixes_def prefix_def

   529 apply(auto simp add: append_eq_Cons_conv) 

   530 done

   531 

   532 lemma finite_Prefixes:

   533   "finite (Prefixes s)"

   534 apply(induct s)

   535 apply(auto simp add: Prefixes_def prefix_def)[1]

   536 apply(simp add: Prefixes_Cons)

   537 done

   538 

   539 lemma finite_Suffixes:

   540   "finite (Suffixes s)"

   541 unfolding Suffixes_def

   542 apply(rule finite_imageI)

   543 apply(rule finite_Prefixes)

   544 done

   545 

   546 lemma prefix_Cons:

   547   "((c # s1) \<sqsubseteq> (c # s2)) = (s1 \<sqsubseteq> s2)"

   548 apply(auto simp add: prefix_def)

   549 done

   550 

   551 lemma prefix_append:

   552   "((s @ s1) \<sqsubseteq> (s @ s2)) = (s1 \<sqsubseteq> s2)"

   553 apply(induct s)

   554 apply(simp)

   555 apply(simp add: prefix_Cons)

   556 done

   557 

   558 

   559 definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where

   560   "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}"

   561 

   562 definition SValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where

   563   "SValues r s \<equiv> {v. \<turnstile> v : r \<and> flat v = s}"

   564 

   565 

   566 definition NValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where

   567   "NValues r s \<equiv> {v. \<Turnstile> v : r \<and> flat v \<sqsubseteq> s}"

   568 

   569 lemma NValues_STAR_Nil:

   570   "NValues (STAR r) [] = {Stars []}"

   571 apply(auto simp add: NValues_def prefix_def)

   572 apply(erule NPrf.cases)

   573 apply(auto)

   574 by (metis NPrf.intros(6))

   575 

   576 

   577 definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where

   578   "rest v s \<equiv> drop (length (flat v)) s"

   579 

   580 lemma rest_Nil:

   581   "rest v [] = []"

   582 apply(simp add: rest_def)

   583 done

   584 

   585 lemma rest_Suffixes:

   586   "rest v s \<in> Suffixes s"

   587 unfolding rest_def

   588 by (metis Suffixes_in append_take_drop_id)

   589 

   590 lemma rest_SSuffixes:

   591   assumes "flat v \<noteq> []" "s \<noteq> []"

   592   shows "rest v s \<in> SSuffixes s"

   593 using assms

   594 unfolding rest_def

   595 thm SSuffixes_in

   596 apply(rule_tac SSuffixes_in)

   597 apply(rule_tac x="take (length (flat v)) s" in exI)

   598 apply(simp add: sprefix_def)

   599 done

   600 

   601 

   602 lemma Values_recs:

   603   "Values (NULL) s = {}"

   604   "Values (EMPTY) s = {Void}"

   605   "Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 

   606   "Values (ALT r1 r2) s = {Left v | v. v \<in> Values r1 s} \<union> {Right v | v. v \<in> Values r2 s}"

   607   "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}"

   608   "Values (STAR r) s = 

   609       {Stars []} \<union> {Stars (v # vs) | v vs. v \<in> Values r s \<and> Stars vs \<in> Values (STAR r) (rest v s)}"

   610 unfolding Values_def

   611 apply(auto)

   612 (*NULL*)

   613 apply(erule Prf.cases)

   614 apply(simp_all)[7]

   615 (*EMPTY*)

   616 apply(erule Prf.cases)

   617 apply(simp_all)[7]

   618 apply(rule Prf.intros)

   619 apply (metis append_Nil prefix_def)

   620 (*CHAR*)

   621 apply(erule Prf.cases)

   622 apply(simp_all)[7]

   623 apply(rule Prf.intros)

   624 apply(erule Prf.cases)

   625 apply(simp_all)[7]

   626 (*ALT*)

   627 apply(erule Prf.cases)

   628 apply(simp_all)[7]

   629 apply (metis Prf.intros(2))

   630 apply (metis Prf.intros(3))

   631 (*SEQ*)

   632 apply(erule Prf.cases)

   633 apply(simp_all)[7]

   634 apply (simp add: append_eq_conv_conj prefix_def rest_def)

   635 apply (metis Prf.intros(1))

   636 apply (simp add: append_eq_conv_conj prefix_def rest_def)

   637 (*STAR*)

   638 apply(erule Prf.cases)

   639 apply(simp_all)[7]

   640 apply(rule conjI)

   641 apply(simp add: prefix_def)

   642 apply(auto)[1]

   643 apply(simp add: prefix_def)

   644 apply(auto)[1]

   645 apply (metis append_eq_conv_conj rest_def)

   646 apply (metis Prf.intros(6))

   647 apply (metis append_Nil prefix_def)

   648 apply (metis Prf.intros(7))

   649 by (metis append_eq_conv_conj prefix_append prefix_def rest_def)

   650 

   651 lemma NValues_recs:

   652   "NValues (NULL) s = {}"

   653   "NValues (EMPTY) s = {Void}"

   654   "NValues (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 

   655   "NValues (ALT r1 r2) s = {Left v | v. v \<in> NValues r1 s} \<union> {Right v | v. v \<in> NValues r2 s}"

   656   "NValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> NValues r1 s \<and> v2 \<in> NValues r2 (rest v1 s)}"

   657   "NValues (STAR r) s = 

   658   {Stars []} \<union> {Stars (v # vs) | v vs. v \<in> NValues r s \<and> flat v \<noteq> [] \<and>  Stars vs \<in> NValues (STAR r) (rest v s)}"

   659 unfolding NValues_def

   660 apply(auto)

   661 (*NULL*)

   662 apply(erule NPrf.cases)

   663 apply(simp_all)[7]

   664 (*EMPTY*)

   665 apply(erule NPrf.cases)

   666 apply(simp_all)[7]

   667 apply(rule NPrf.intros)

   668 apply (metis append_Nil prefix_def)

   669 (*CHAR*)

   670 apply(erule NPrf.cases)

   671 apply(simp_all)[7]

   672 apply(rule NPrf.intros)

   673 apply(erule NPrf.cases)

   674 apply(simp_all)[7]

   675 (*ALT*)

   676 apply(erule NPrf.cases)

   677 apply(simp_all)[7]

   678 apply (metis NPrf.intros(2))

   679 apply (metis NPrf.intros(3))

   680 (*SEQ*)

   681 apply(erule NPrf.cases)

   682 apply(simp_all)[7]

   683 apply (simp add: append_eq_conv_conj prefix_def rest_def)

   684 apply (metis NPrf.intros(1))

   685 apply (simp add: append_eq_conv_conj prefix_def rest_def)

   686 (*STAR*)

   687 apply(erule NPrf.cases)

   688 apply(simp_all)

   689 apply(rule conjI)

   690 apply(simp add: prefix_def)

   691 apply(auto)[1]

   692 apply(simp add: prefix_def)

   693 apply(auto)[1]

   694 apply (metis append_eq_conv_conj rest_def)

   695 apply (metis NPrf.intros(6))

   696 apply (metis append_Nil prefix_def)

   697 apply (metis NPrf.intros(7))

   698 by (metis append_eq_conv_conj prefix_append prefix_def rest_def)

   699 

   700 lemma SValues_recs:

   701  "SValues (NULL) s = {}"

   702  "SValues (EMPTY) s = (if s = [] then {Void} else {})"

   703  "SValues (CHAR c) s = (if [c] = s then {Char c} else {})" 

   704  "SValues (ALT r1 r2) s = {Left v | v. v \<in> SValues r1 s} \<union> {Right v | v. v \<in> SValues r2 s}"

   705  "SValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. \<exists>s1 s2. s = s1 @ s2 \<and> v1 \<in> SValues r1 s1 \<and> v2 \<in> SValues r2 s2}"

   706  "SValues (STAR r) s = (if s = [] then {Stars []} else {}) \<union> 

   707    {Stars (v # vs) | v vs. \<exists>s1 s2. s = s1 @ s2 \<and> v \<in> SValues r s1 \<and> Stars vs \<in> SValues (STAR r) s2}"

   708 unfolding SValues_def

   709 apply(auto)

   710 (*NULL*)

   711 apply(erule Prf.cases)

   712 apply(simp_all)[7]

   713 (*EMPTY*)

   714 apply(erule Prf.cases)

   715 apply(simp_all)[7]

   716 apply(rule Prf.intros)

   717 apply(erule Prf.cases)

   718 apply(simp_all)[7]

   719 (*CHAR*)

   720 apply(erule Prf.cases)

   721 apply(simp_all)[7]

   722 apply (metis Prf.intros(5))

   723 apply(erule Prf.cases)

   724 apply(simp_all)[7]

   725 (*ALT*)

   726 apply(erule Prf.cases)

   727 apply(simp_all)[7]

   728 apply metis

   729 apply(erule Prf.intros)

   730 apply(erule Prf.intros)

   731 (* SEQ case *)

   732 apply(erule Prf.cases)

   733 apply(simp_all)[7]

   734 apply (metis Prf.intros(1))

   735 (* STAR case *)

   736 apply(erule Prf.cases)

   737 apply(simp_all)[7]

   738 apply(rule Prf.intros)

   739 apply (metis Prf.intros(7))

   740 apply(erule Prf.cases)

   741 apply(simp_all)[7]

   742 apply (metis Prf.intros(7))

   743 by (metis Prf.intros(7))

   744 

   745 lemma finite_image_set2:

   746   "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {(x, y) | x y. P x \<and> Q y}"

   747   by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {(x, y)}"]) auto

   748 

   749 

   750 lemma NValues_finite_aux:

   751   "(\<lambda>(r, s). finite (NValues r s)) (r, s)"

   752 apply(rule wf_induct[of "measure size <*lex*> measure length",where P="\<lambda>(r, s). finite (NValues r s)"])

   753 apply (metis wf_lex_prod wf_measure)

   754 apply(auto)

   755 apply(case_tac a)

   756 apply(simp_all)

   757 apply(simp add: NValues_recs)

   758 apply(simp add: NValues_recs)

   759 apply(simp add: NValues_recs)

   760 apply(simp add: NValues_recs)

   761 apply(rule_tac f="\<lambda>(x, y). Seq x y" and 

   762                A="{(v1, v2) | v1 v2. v1 \<in> NValues rexp1 b \<and> v2 \<in> NValues rexp2 (rest v1 b)}" in finite_surj)

   763 prefer 2

   764 apply(auto)[1]

   765 apply(rule_tac B="\<Union>sp \<in> Suffixes b. {(v1, v2). v1 \<in> NValues rexp1 b \<and> v2 \<in> NValues rexp2 sp}" in finite_subset)

   766 apply(auto)[1]

   767 apply (metis rest_Suffixes)

   768 apply(rule finite_UN_I)

   769 apply(rule finite_Suffixes)

   770 apply(simp)

   771 apply(simp add: NValues_recs)

   772 apply(clarify)

   773 apply(subst NValues_recs)

   774 apply(simp)

   775 apply(rule_tac f="\<lambda>(v, vs). Stars (v # vs)" and 

   776                A="{(v, vs) | v vs. v \<in> NValues rexp b \<and> (flat v \<noteq> [] \<and> Stars vs \<in> NValues (STAR rexp) (rest v b))}" in finite_surj)

   777 prefer 2

   778 apply(auto)[1]

   779 apply(auto)

   780 apply(case_tac b)

   781 apply(simp)

   782 defer

   783 apply(rule_tac B="\<Union>sp \<in> SSuffixes b. {(v, vs) | v vs. v \<in> NValues rexp b \<and> Stars vs \<in> NValues (STAR rexp) sp}" in finite_subset)

   784 apply(auto)[1]

   785 apply(rule_tac x="rest aa (a # list)" in bexI)

   786 apply(simp)

   787 apply (rule rest_SSuffixes)

   788 apply(simp)

   789 apply(simp)

   790 apply(rule finite_UN_I)

   791 defer

   792 apply(frule_tac x="rexp" in spec)

   793 apply(drule_tac x="b" in spec)

   794 apply(drule conjunct1)

   795 apply(drule mp)

   796 apply(simp)

   797 apply(drule_tac x="STAR rexp" in spec)

   798 apply(drule_tac x="sp" in spec)

   799 apply(drule conjunct2)

   800 apply(drule mp)

   801 apply(simp)

   802 apply(simp add: prefix_def SPrefixes_def SSuffixes_def)

   803 apply(auto)[1]

   804 apply (metis length_Cons length_rev length_sprefix rev.simps(2))

   805 apply(simp)

   806 apply(rule finite_cartesian_product)

   807 apply(simp)

   808 apply(rule_tac f="Stars" in finite_imageD)

   809 prefer 2

   810 apply(auto simp add: inj_on_def)[1]

   811 apply (metis finite_subset image_Collect_subsetI)

   812 apply(simp add: rest_Nil)

   813 apply(simp add: NValues_STAR_Nil)

   814 apply(rule_tac B="{(v, vs). v \<in> NValues rexp [] \<and> vs = []}" in finite_subset)

   815 apply(auto)[1]

   816 apply(simp)

   817 apply(rule_tac B="Suffixes b" in finite_subset)

   818 apply(auto simp add: SSuffixes_def Suffixes_def Prefixes_def SPrefixes_def sprefix_def)[1]

   819 by (metis finite_Suffixes)

   820 

   821 lemma NValues_finite:

   822   "finite (NValues r s)"

   823 using NValues_finite_aux

   824 apply(simp)

   825 done

   826 

   827 section {* Sulzmann functions *}

   828 

   829 fun 

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

   831 where

   832   "mkeps(EMPTY) = Void"

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

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

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

   836 

   837 section {* Derivatives *}

   838 

   839 fun

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

   841 where

   842   "der c (NULL) = NULL"

   843 | "der c (EMPTY) = NULL"

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

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

   846 | "der c (SEQ r1 r2) = 

   847      (if nullable r1

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

   849       else SEQ (der c r1) r2)"

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

   851 

   852 fun 

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

   854 where

   855   "ders [] r = r"

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

   857 

   858 

   859 lemma der_correctness:

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

   861 apply(induct r) 

   862 apply(simp_all add: nullable_correctness)

   863 done

   864 

   865 lemma ders_correctness:

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

   867 apply(induct s arbitrary: r) 

   868 apply(simp add: Ders_def)

   869 apply(simp)

   870 apply(subst der_correctness)

   871 apply(simp add: Ders_def Der_def)

   872 done

   873 

   874 section {* Injection function *}

   875 

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

   877 where

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

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

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

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

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

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

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

   885 

   886 fun 

   887   lex :: "rexp \<Rightarrow> string \<Rightarrow> val option"

   888 where

   889   "lex r [] = (if nullable r then Some(mkeps r) else None)"

   890 | "lex r (c#s) = (case (lex (der c r) s) of  

   891                     None \<Rightarrow> None

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

   893 

   894 fun 

   895   lex2 :: "rexp \<Rightarrow> string \<Rightarrow> val"

   896 where

   897   "lex2 r [] = mkeps r"

   898 | "lex2 r (c#s) = injval r c (lex2 (der c r) s)"

   899 

   900 

   901 section {* Projection function *}

   902 

   903 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"

   904 where

   905   "projval (CHAR d) c _ = Void"

   906 | "projval (ALT r1 r2) c (Left v1) = Left (projval r1 c v1)"

   907 | "projval (ALT r1 r2) c (Right v2) = Right (projval r2 c v2)"

   908 | "projval (SEQ r1 r2) c (Seq v1 v2) = 

   909      (if flat v1 = [] then Right(projval r2 c v2) 

   910       else if nullable r1 then Left (Seq (projval r1 c v1) v2)

   911                           else Seq (projval r1 c v1) v2)"

   912 | "projval (STAR r) c (Stars (v # vs)) = Seq (projval r c v) (Stars vs)"

   913 

   914 

   915 

   916 lemma mkeps_nullable:

   917   assumes "nullable(r)" 

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

   919 using assms

   920 apply(induct rule: nullable.induct)

   921 apply(auto intro: Prf.intros)

   922 done

   923 

   924 lemma mkeps_flat:

   925   assumes "nullable(r)" 

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

   927 using assms

   928 apply(induct rule: nullable.induct)

   929 apply(auto)

   930 done

   931 

   932 

   933 lemma v3:

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

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

   936 using assms

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

   938 apply(simp)

   939 apply(erule Prf.cases)

   940 apply(simp_all)[7]

   941 apply(simp)

   942 apply(erule Prf.cases)

   943 apply(simp_all)[7]

   944 apply(case_tac "c = c'")

   945 apply(simp)

   946 apply(erule Prf.cases)

   947 apply(simp_all)[7]

   948 apply (metis Prf.intros(5))

   949 apply(simp)

   950 apply(erule Prf.cases)

   951 apply(simp_all)[7]

   952 apply(simp)

   953 apply(erule Prf.cases)

   954 apply(simp_all)[7]

   955 apply (metis Prf.intros(2))

   956 apply (metis Prf.intros(3))

   957 apply(simp)

   958 apply(case_tac "nullable r1")

   959 apply(simp)

   960 apply(erule Prf.cases)

   961 apply(simp_all)[7]

   962 apply(auto)[1]

   963 apply(erule Prf.cases)

   964 apply(simp_all)[7]

   965 apply(auto)[1]

   966 apply (metis Prf.intros(1))

   967 apply(auto)[1]

   968 apply (metis Prf.intros(1) mkeps_nullable)

   969 apply(simp)

   970 apply(erule Prf.cases)

   971 apply(simp_all)[7]

   972 apply(auto)[1]

   973 apply(rule Prf.intros)

   974 apply(auto)[2]

   975 apply(simp)

   976 apply(erule Prf.cases)

   977 apply(simp_all)[7]

   978 apply(clarify)

   979 apply(rotate_tac 2)

   980 apply(erule Prf.cases)

   981 apply(simp_all)[7]

   982 apply(auto)

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

   984 by (metis Prf.intros(7))

   985 

   986 lemma v3_proj:

   987   assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"

   988   shows "\<Turnstile> (projval r c v) : der c r"

   989 using assms

   990 apply(induct rule: NPrf.induct)

   991 prefer 4

   992 apply(simp)

   993 prefer 4

   994 apply(simp)

   995 apply (metis NPrf.intros(4))

   996 prefer 2

   997 apply(simp)

   998 apply (metis NPrf.intros(2))

   999 prefer 2

  1000 apply(simp)

  1001 apply (metis NPrf.intros(3))

  1002 apply(auto)

  1003 apply(rule NPrf.intros)

  1004 apply(simp)

  1005 apply (metis NPrf_imp_Prf not_nullable_flat)

  1006 apply(rule NPrf.intros)

  1007 apply(rule NPrf.intros)

  1008 apply (metis Cons_eq_append_conv)

  1009 apply(simp)

  1010 apply(rule NPrf.intros)

  1011 apply (metis Cons_eq_append_conv)

  1012 apply(simp)

  1013 (* Stars case *)

  1014 apply(rule NPrf.intros)

  1015 apply (metis Cons_eq_append_conv)

  1016 apply(auto)

  1017 done

  1018 

  1019 lemma v4:

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

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

  1022 using assms

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

  1024 apply(simp)

  1025 apply(erule Prf.cases)

  1026 apply(simp_all)[7]

  1027 apply(simp)

  1028 apply(erule Prf.cases)

  1029 apply(simp_all)[7]

  1030 apply(simp)

  1031 apply(case_tac "c = c'")

  1032 apply(simp)

  1033 apply(auto)[1]

  1034 apply(erule Prf.cases)

  1035 apply(simp_all)[7]

  1036 apply(simp)

  1037 apply(erule Prf.cases)

  1038 apply(simp_all)[7]

  1039 apply(simp)

  1040 apply(erule Prf.cases)

  1041 apply(simp_all)[7]

  1042 apply(simp)

  1043 apply(case_tac "nullable r1")

  1044 apply(simp)

  1045 apply(erule Prf.cases)

  1046 apply(simp_all (no_asm_use))[7]

  1047 apply(auto)[1]

  1048 apply(erule Prf.cases)

  1049 apply(simp_all)[7]

  1050 apply(clarify)

  1051 apply(simp only: injval.simps flat.simps)

  1052 apply(auto)[1]

  1053 apply (metis mkeps_flat)

  1054 apply(simp)

  1055 apply(erule Prf.cases)

  1056 apply(simp_all)[7]

  1057 apply(simp)

  1058 apply(erule Prf.cases)

  1059 apply(simp_all)[7]

  1060 apply(auto)

  1061 apply(rotate_tac 2)

  1062 apply(erule Prf.cases)

  1063 apply(simp_all)[7]

  1064 done

  1065 

  1066 lemma v4_proj:

  1067   assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"

  1068   shows "c # flat (projval r c v) = flat v"

  1069 using assms

  1070 apply(induct rule: NPrf.induct)

  1071 prefer 4

  1072 apply(simp)

  1073 prefer 4

  1074 apply(simp)

  1075 prefer 2

  1076 apply(simp)

  1077 prefer 2

  1078 apply(simp)

  1079 apply(auto)

  1080 apply (metis Cons_eq_append_conv)

  1081 apply(simp add: append_eq_Cons_conv)

  1082 apply(auto)

  1083 done

  1084 

  1085 lemma v4_proj2:

  1086   assumes "\<Turnstile> v : r" and "(flat v) = c # s"

  1087   shows "flat (projval r c v) = s"

  1088 using assms

  1089 by (metis list.inject v4_proj)

  1090 

  1091 

  1092 definition 

  1093   PC31 :: "string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool"

  1094 where

  1095   "PC31 s r r' \<equiv> s \<notin> L r"

  1096 

  1097 definition 

  1098   PC41 :: "string \<Rightarrow> string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool"

  1099 where

  1100   "PC41 s s' r r' \<equiv> (\<forall>x. (s @ x \<in> L r \<longrightarrow> s' \<in> {x} ;; L r' \<longrightarrow> x = []))"

  1101 

  1102 

  1103 lemma

  1104  L1: "\<not>(nullable r1) \<longrightarrow> [] \<in> L r2 \<longrightarrow> PC31 [] r1 r2" and

  1105  L2: "s1 \<in> L(r1) \<longrightarrow> [] \<in> L(r2) \<longrightarrow> PC41 s1 [] r1 r2" and

  1106  L3: "s2 \<in> L(der c r2) \<longrightarrow> PC31 s2 (der c r1) (der c r2) \<longrightarrow> PC31 (c#s2) r1 r2" and

  1107  L4: "s1 \<in> L(der c r1) \<longrightarrow> s2 \<in> L(r2) \<longrightarrow> PC41 s1 s2 (der c r1) r2 \<longrightarrow> PC41 (c#s1) s2 r1 r2" and

  1108  L5: "nullable(r1) \<longrightarrow> s2 \<in> L(der c r2) \<longrightarrow> PC31 s2 (SEQ (der c r1) r2) (der c r2) \<longrightarrow> PC41 [] (c#s2) r1 r2" and

  1109  L6: "s0 \<in> L(der c r0) \<longrightarrow>  s \<in> L(STAR r0) \<longrightarrow>  PC41 s0 s (der c r0) (STAR r0) \<longrightarrow> PC41 (c#s0) s r0 (STAR r0)" and

  1110  L7: "s' \<in> L(r') \<longrightarrow> s' \<in> L(r) \<longrightarrow> \<not>PC31 s' r r'" and

  1111  L8: "s \<in> L(r) \<longrightarrow> s' \<in> L(r') \<longrightarrow> s @ x \<in> L(r) \<longrightarrow> s' \<in> {x} ;; (L(r') ;; {y}) \<longrightarrow>  x \<noteq> [] \<longrightarrow> \<not>PC41 s s' r r'"

  1112 apply(auto simp add: PC31_def PC41_def)[1]

  1113 apply (metis nullable_correctness)

  1114 apply(auto simp add: PC31_def PC41_def)[1]

  1115 apply(simp add: Sequ_def)

  1116 apply(auto simp add: PC31_def PC41_def)[1]

  1117 apply(simp add: der_correctness Der_def)

  1118 apply(auto simp add: PC31_def PC41_def)[1]

  1119 apply(simp add: der_correctness Der_def Sequ_def)

  1120 apply(auto simp add: PC31_def PC41_def)[1]

  1121 apply(simp add: Sequ_def)

  1122 apply(simp add: der_correctness Der_def)

  1123 apply(auto)[1]

  1124 apply (metis append_eq_Cons_conv)

  1125 apply(auto simp add: PC31_def PC41_def)[1]

  1126 apply(simp add: Sequ_def)

  1127 apply(simp add: der_correctness Der_def)

  1128 apply(auto simp add: PC31_def PC41_def)[1]

  1129 apply(rule impI)+

  1130 apply(rule notI)

  1131 (* 8 fails *)

  1132 oops

  1133 

  1134 definition 

  1135   PC32 :: "string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool"