Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/ReStar.thy
changeset 107 6adda4a667b1
parent 106 489dfa0d7ec9
child 108 73f7dc60c285
equal deleted inserted replaced
106:489dfa0d7ec9 107:6adda4a667b1 
   101 
   101 
   102 
   102 
   103 section {* Regular Expressions *}
 
   103 section {* Regular Expressions *}
 
   104 
   104 
   105 datatype rexp =
 
   105 datatype rexp =
 
   106   NULL
 
   106   ZERO
 
   107 | EMPTY
 
   107 | ONE
 
   108 | CHAR char
 
   108 | CHAR char
 
   109 | SEQ rexp rexp
 
   109 | SEQ rexp rexp
 
   110 | ALT rexp rexp
 
   110 | ALT rexp rexp
 
   111 | STAR rexp
 
   111 | STAR rexp
 
   112 
   112 
   113 section {* Semantics of Regular Expressions *}
 
   113 section {* Semantics of Regular Expressions *}
 
   114  
   114  
   115 fun
 
   115 fun
 
   116   L :: "rexp \<Rightarrow> string set"
 
   116   L :: "rexp \<Rightarrow> string set"
 
   117 where
 
   117 where
 
   118   "L (NULL) = {}"
 
   118   "L (ZERO) = {}"
 
   119 | "L (EMPTY) = {[]}"
 
   119 | "L (ONE) = {[]}"
 
   120 | "L (CHAR c) = {[c]}"
 
   120 | "L (CHAR c) = {[c]}"
 
   121 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 
   121 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 
   122 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
   122 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
   123 | "L (STAR r) = (L r)\<star>"
 
   123 | "L (STAR r) = (L r)\<star>"
 
   124 
   124 
       
   125 
       
   126 section {* Nullable, Derivatives *}
 
       
   127 
   125 fun
 
   128 fun
 
   126  nullable :: "rexp \<Rightarrow> bool"
 
   129  nullable :: "rexp \<Rightarrow> bool"
 
   127 where
 
   130 where
 
   128   "nullable (NULL) = False"
 
   131   "nullable (ZERO) = False"
 
   129 | "nullable (EMPTY) = True"
 
   132 | "nullable (ONE) = True"
 
   130 | "nullable (CHAR c) = False"
 
   133 | "nullable (CHAR c) = False"
 
   131 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 
   134 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 
   132 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 
   135 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 
   133 | "nullable (STAR r) = True"
 
   136 | "nullable (STAR r) = True"
 
   134 
   137 
       
   138 
       
   139 fun
 
       
   140  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 
       
   141 where
 
       
   142   "der c (ZERO) = ZERO"
 
       
   143 | "der c (ONE) = ZERO"
 
       
   144 | "der c (CHAR c') = (if c = c' then ONE else ZERO)"
 
       
   145 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
 
       
   146 | "der c (SEQ r1 r2) = 
       
   147      (if nullable r1
 
       
   148       then ALT (SEQ (der c r1) r2) (der c r2)
 
       
   149       else SEQ (der c r1) r2)"
 
       
   150 | "der c (STAR r) = SEQ (der c r) (STAR r)"
 
       
   151 
       
   152 fun 
       
   153  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 
       
   154 where
 
       
   155   "ders [] r = r"
 
       
   156 | "ders (c # s) r = ders s (der c r)"
 
       
   157 
       
   158 
   135 lemma nullable_correctness:
 
   159 lemma nullable_correctness:
 
   136   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 
   160   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 
   137 by (induct r) (auto simp add: Sequ_def) 
   161 by (induct r) (auto simp add: Sequ_def) 
       
   162 
       
   163 
       
   164 lemma der_correctness:
 
       
   165   shows "L (der c r) = Der c (L r)"
 
       
   166 apply(induct r) 
       
   167 apply(simp_all add: nullable_correctness)
 
       
   168 done
 
       
   169 
       
   170 lemma ders_correctness:
 
       
   171   shows "L (ders s r) = Ders s (L r)"
 
       
   172 apply(induct s arbitrary: r) 
       
   173 apply(simp_all add: der_correctness Der_def Ders_def)
 
       
   174 done
 
   138 
   175 
   139 
   176 
   140 section {* Values *}
 
   177 section {* Values *}
 
   141 
   178 
   142 datatype val = 
   179 datatype val = 
   171   Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 
   208   Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 
   172 where
 
   209 where
 
   173  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
 
   210  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
 
   174 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
 
   211 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
 
   175 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 
   212 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 
   176 | "\<turnstile> Void : EMPTY"
 
   213 | "\<turnstile> Void : ONE"
 
   177 | "\<turnstile> Char c : CHAR c"
 
   214 | "\<turnstile> Char c : CHAR c"
 
   178 | "\<turnstile> Stars [] : STAR r"
 
   215 | "\<turnstile> Stars [] : STAR r"
 
   179 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
 
   216 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
 
   180 
   217 
   181 lemma not_nullable_flat:
 
   218 lemma not_nullable_flat:
 
   243 apply(rule Star_val)
 
   280 apply(rule Star_val)
 
   244 apply(simp)
 
   281 apply(simp)
 
   245 done
 
   282 done
 
   246 
   283 
   247 
   284 
   248 section {* Values Sets *}
 
       
   249 
       
   250 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100)
 
       
   251 where
 
       
   252   "s1 \<sqsubseteq> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"
 
       
   253 
       
   254 definition sprefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
 
       
   255 where
 
       
   256   "s1 \<sqsubset> s2 \<equiv> (s1 \<sqsubseteq> s2 \<and> s1 \<noteq> s2)"
 
       
   257 
       
   258 lemma length_sprefix:
 
       
   259   "s1 \<sqsubset> s2 \<Longrightarrow> length s1 < length s2"
 
       
   260 unfolding sprefix_def prefix_def
 
       
   261 by (auto)
 
       
   262 
       
   263 definition Prefixes :: "string \<Rightarrow> string set" where
 
       
   264   "Prefixes s \<equiv> {sp. sp \<sqsubseteq> s}"
 
       
   265 
       
   266 definition Suffixes :: "string \<Rightarrow> string set" where
 
       
   267   "Suffixes s \<equiv> rev ` (Prefixes (rev s))"
 
       
   268 
       
   269 definition SPrefixes :: "string \<Rightarrow> string set" where
 
       
   270   "SPrefixes s \<equiv> {sp. sp \<sqsubset> s}"
 
       
   271 
       
   272 definition SSuffixes :: "string \<Rightarrow> string set" where
 
       
   273   "SSuffixes s \<equiv> rev ` (SPrefixes (rev s))"
 
       
   274 
       
   275 lemma Suffixes_in: 
       
   276   "\<exists>s1. s1 @ s2 = s3 \<Longrightarrow> s2 \<in> Suffixes s3"
 
       
   277 unfolding Suffixes_def Prefixes_def prefix_def image_def
 
       
   278 apply(auto)
 
       
   279 by (metis rev_rev_ident)
 
       
   280 
       
   281 lemma SSuffixes_in: 
       
   282   "\<exists>s1. s1 \<noteq> [] \<and> s1 @ s2 = s3 \<Longrightarrow> s2 \<in> SSuffixes s3"
 
       
   283 unfolding SSuffixes_def Suffixes_def SPrefixes_def Prefixes_def sprefix_def prefix_def image_def
 
       
   284 apply(auto)
 
       
   285 by (metis append_self_conv rev.simps(1) rev_rev_ident)
 
       
   286 
       
   287 lemma Prefixes_Cons:
 
       
   288   "Prefixes (c # s) = {[]} \<union> {c # sp | sp. sp \<in> Prefixes s}"
 
       
   289 unfolding Prefixes_def prefix_def
 
       
   290 apply(auto simp add: append_eq_Cons_conv) 
       
   291 done
 
       
   292 
       
   293 lemma finite_Prefixes:
 
       
   294   "finite (Prefixes s)"
 
       
   295 apply(induct s)
 
       
   296 apply(auto simp add: Prefixes_def prefix_def)[1]
 
       
   297 apply(simp add: Prefixes_Cons)
 
       
   298 done
 
       
   299 
       
   300 lemma finite_Suffixes:
 
       
   301   "finite (Suffixes s)"
 
       
   302 unfolding Suffixes_def
 
       
   303 apply(rule finite_imageI)
 
       
   304 apply(rule finite_Prefixes)
 
       
   305 done
 
       
   306 
       
   307 lemma prefix_Cons:
 
       
   308   "((c # s1) \<sqsubseteq> (c # s2)) = (s1 \<sqsubseteq> s2)"
 
       
   309 apply(auto simp add: prefix_def)
 
       
   310 done
 
       
   311 
       
   312 lemma prefix_append:
 
       
   313   "((s @ s1) \<sqsubseteq> (s @ s2)) = (s1 \<sqsubseteq> s2)"
 
       
   314 apply(induct s)
 
       
   315 apply(simp)
 
       
   316 apply(simp add: prefix_Cons)
 
       
   317 done
 
       
   318 
       
   319 
       
   320 definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
 
       
   321   "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}"
 
       
   322 
       
   323 definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where
 
       
   324   "rest v s \<equiv> drop (length (flat v)) s"
 
       
   325 
       
   326 lemma rest_Nil:
 
       
   327   "rest v [] = []"
 
       
   328 apply(simp add: rest_def)
 
       
   329 done
 
       
   330 
       
   331 lemma rest_Suffixes:
 
       
   332   "rest v s \<in> Suffixes s"
 
       
   333 unfolding rest_def
 
       
   334 by (metis Suffixes_in append_take_drop_id)
 
       
   335 
       
   336 lemma Values_recs:
 
       
   337   "Values (NULL) s = {}"
 
       
   338   "Values (EMPTY) s = {Void}"
 
       
   339   "Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
       
   340   "Values (ALT r1 r2) s = {Left v | v. v \<in> Values r1 s} \<union> {Right v | v. v \<in> Values r2 s}"
 
       
   341   "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}"
 
       
   342   "Values (STAR r) s = 
       
   343       {Stars []} \<union> {Stars (v # vs) | v vs. v \<in> Values r s \<and> Stars vs \<in> Values (STAR r) (rest v s)}"
 
       
   344 unfolding Values_def
 
       
   345 apply(auto)
 
       
   346 (*NULL*)
 
       
   347 apply(erule Prf.cases)
 
       
   348 apply(simp_all)[7]
 
       
   349 (*EMPTY*)
 
       
   350 apply(erule Prf.cases)
 
       
   351 apply(simp_all)[7]
 
       
   352 apply(rule Prf.intros)
 
       
   353 apply (metis append_Nil prefix_def)
 
       
   354 (*CHAR*)
 
       
   355 apply(erule Prf.cases)
 
       
   356 apply(simp_all)[7]
 
       
   357 apply(rule Prf.intros)
 
       
   358 apply(erule Prf.cases)
 
       
   359 apply(simp_all)[7]
 
       
   360 (*ALT*)
 
       
   361 apply(erule Prf.cases)
 
       
   362 apply(simp_all)[7]
 
       
   363 apply (metis Prf.intros(2))
 
       
   364 apply (metis Prf.intros(3))
 
       
   365 (*SEQ*)
 
       
   366 apply(erule Prf.cases)
 
       
   367 apply(simp_all)[7]
 
       
   368 apply (simp add: append_eq_conv_conj prefix_def rest_def)
 
       
   369 apply (metis Prf.intros(1))
 
       
   370 apply (simp add: append_eq_conv_conj prefix_def rest_def)
 
       
   371 (*STAR*)
 
       
   372 apply(erule Prf.cases)
 
       
   373 apply(simp_all)[7]
 
       
   374 apply(rule conjI)
 
       
   375 apply(simp add: prefix_def)
 
       
   376 apply(auto)[1]
 
       
   377 apply(simp add: prefix_def)
 
       
   378 apply(auto)[1]
 
       
   379 apply (metis append_eq_conv_conj rest_def)
 
       
   380 apply (metis Prf.intros(6))
 
       
   381 apply (metis append_Nil prefix_def)
 
       
   382 apply (metis Prf.intros(7))
 
       
   383 by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
 
       
   384 
       
   385 lemma finite_image_set2:
 
       
   386   "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {(x, y) | x y. P x \<and> Q y}"
 
       
   387   by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {(x, y)}"]) auto
 
       
   388 
       
   389 section {* Sulzmann functions *}
 
   285 section {* Sulzmann functions *}
 
   390 
   286 
   391 fun 
   287 fun 
   392   mkeps :: "rexp \<Rightarrow> val"
 
   288   mkeps :: "rexp \<Rightarrow> val"
 
   393 where
 
   289 where
 
   394   "mkeps(EMPTY) = Void"
 
   290   "mkeps(ONE) = Void"
 
   395 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
 
   291 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
 
   396 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
 
   292 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
 
   397 | "mkeps(STAR r) = Stars []"
 
   293 | "mkeps(STAR r) = Stars []"
 
   398 
       
   399 section {* Derivatives *}
 
       
   400 
       
   401 fun
 
       
   402  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 
       
   403 where
 
       
   404   "der c (NULL) = NULL"
 
       
   405 | "der c (EMPTY) = NULL"
 
       
   406 | "der c (CHAR c') = (if c = c' then EMPTY else NULL)"
 
       
   407 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
 
       
   408 | "der c (SEQ r1 r2) = 
       
   409      (if nullable r1
 
       
   410       then ALT (SEQ (der c r1) r2) (der c r2)
 
       
   411       else SEQ (der c r1) r2)"
 
       
   412 | "der c (STAR r) = SEQ (der c r) (STAR r)"
 
       
   413 
       
   414 fun 
       
   415  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 
       
   416 where
 
       
   417   "ders [] r = r"
 
       
   418 | "ders (c # s) r = ders s (der c r)"
 
       
   419 
       
   420 
       
   421 lemma der_correctness:
 
       
   422   shows "L (der c r) = Der c (L r)"
 
       
   423 apply(induct r) 
       
   424 apply(simp_all add: nullable_correctness)
 
       
   425 done
 
       
   426 
       
   427 lemma ders_correctness:
 
       
   428   shows "L (ders s r) = Ders s (L r)"
 
       
   429 apply(induct s arbitrary: r) 
       
   430 apply(simp add: Ders_def)
 
       
   431 apply(simp)
 
       
   432 apply(subst der_correctness)
 
       
   433 apply(simp add: Ders_def Der_def)
 
       
   434 done
 
       
   435 
       
   436 section {* Injection function *}
 
       
   437 
   294 
   438 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 
   295 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 
   439 where
 
   296 where
 
   440   "injval (CHAR d) c Void = Char d"
 
   297   "injval (CHAR d) c Void = Char d"
 
   441 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
 
   298 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
 
   443 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
 
   300 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
 
   444 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
 
   301 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
 
   445 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
 
   302 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
 
   446 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" 
   303 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" 
   447 
   304 
       
   305 
       
   306 section {* Matcher *}
 
       
   307 
   448 fun 
   308 fun 
   449   lex :: "rexp \<Rightarrow> string \<Rightarrow> val option"
 
   309   matcher :: "rexp \<Rightarrow> string \<Rightarrow> val option"
 
   450 where
 
   310 where
 
   451   "lex r [] = (if nullable r then Some(mkeps r) else None)"
 
   311   "matcher r [] = (if nullable r then Some(mkeps r) else None)"
 
   452 | "lex r (c#s) = (case (lex (der c r) s) of  
   312 | "matcher r (c#s) = (case (matcher (der c r) s) of  
   453                     None \<Rightarrow> None
 
   313                     None \<Rightarrow> None
 
   454                   | Some(v) \<Rightarrow> Some(injval r c v))"
 
   314                   | Some(v) \<Rightarrow> Some(injval r c v))"
 
   455 
   315 
   456 fun 
   316 fun 
   457   lex2 :: "rexp \<Rightarrow> string \<Rightarrow> val"
 
   317   matcher2 :: "rexp \<Rightarrow> string \<Rightarrow> val"
 
   458 where
 
   318 where
 
   459   "lex2 r [] = mkeps r"
 
   319   "matcher2 r [] = mkeps r"
 
   460 | "lex2 r (c#s) = injval r c (lex2 (der c r) s)"
 
   320 | "matcher2 r (c#s) = injval r c (matcher2 (der c r) s)"
 
   461 
   321 
   462 section {* Projection function *}
 
   322 
   463 
   323 
   464 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 
   324 section {* Mkeps, injval *}
 
   465 where
 
       
   466   "projval (CHAR d) c _ = Void"
 
       
   467 | "projval (ALT r1 r2) c (Left v1) = Left (projval r1 c v1)"
 
       
   468 | "projval (ALT r1 r2) c (Right v2) = Right (projval r2 c v2)"
 
       
   469 | "projval (SEQ r1 r2) c (Seq v1 v2) = 
       
   470      (if flat v1 = [] then Right(projval r2 c v2) 
       
   471       else if nullable r1 then Left (Seq (projval r1 c v1) v2)
 
       
   472                           else Seq (projval r1 c v1) v2)"
 
       
   473 | "projval (STAR r) c (Stars (v # vs)) = Seq (projval r c v) (Stars vs)"
 
       
   474 
       
   475 
   325 
   476 lemma mkeps_nullable:
 
   326 lemma mkeps_nullable:
 
   477   assumes "nullable(r)" 
   327   assumes "nullable(r)" 
   478   shows "\<turnstile> mkeps r : r"
 
   328   shows "\<turnstile> mkeps r : r"
 
   479 using assms
 
   329 using assms
 
   487 using assms
 
   337 using assms
 
   488 apply(induct rule: nullable.induct)
 
   338 apply(induct rule: nullable.induct)
 
   489 apply(auto)
 
   339 apply(auto)
 
   490 done
 
   340 done
 
   491 
   341 
   492 
   342 lemma Prf_injval:
 
   493 lemma v3:
 
       
   494   assumes "\<turnstile> v : der c r" 
   343   assumes "\<turnstile> v : der c r" 
   495   shows "\<turnstile> (injval r c v) : r"
 
   344   shows "\<turnstile> (injval r c v) : r"
 
   496 using assms
 
   345 using assms
 
   497 apply(induct arbitrary: v rule: der.induct)
 
   346 apply(induct r arbitrary: c v rule: rexp.induct)
 
   498 apply(simp)
 
   347 apply(simp_all)
 
   499 apply(erule Prf.cases)
 
   348 (* ZERO *)
 
   500 apply(simp_all)[7]
 
   349 apply(erule Prf.cases)
 
   501 apply(simp)
 
   350 apply(simp_all)[7]
 
   502 apply(erule Prf.cases)
 
   351 (* ONE *)
 
   503 apply(simp_all)[7]
 
   352 apply(erule Prf.cases)
 
   504 apply(case_tac "c = c'")
 
   353 apply(simp_all)[7]
 
   505 apply(simp)
 
   354 (* CHAR *)
 
   506 apply(erule Prf.cases)
 
   355 apply(case_tac "c = char")
 
   507 apply(simp_all)[7]
 
   356 apply(simp)
 
   508 apply (metis Prf.intros(5))
 
   357 apply(erule Prf.cases)
 
   509 apply(simp)
 
   358 apply(simp_all)[7]
 
   510 apply(erule Prf.cases)
 
   359 apply(rule Prf.intros(5))
 
   511 apply(simp_all)[7]
 
   360 apply(simp)
 
   512 apply(simp)
 
   361 apply(erule Prf.cases)
 
   513 apply(erule Prf.cases)
 
   362 apply(simp_all)[7]
 
   514 apply(simp_all)[7]
 
   363 (* SEQ *)
 
       
   364 apply(case_tac "nullable rexp1")
 
       
   365 apply(simp)
 
       
   366 apply(erule Prf.cases)
 
       
   367 apply(simp_all)[7]
 
       
   368 apply(auto)[1]
 
       
   369 apply(erule Prf.cases)
 
       
   370 apply(simp_all)[7]
 
       
   371 apply(auto)[1]
 
       
   372 apply(rule Prf.intros)
 
       
   373 apply(auto)[2]
 
       
   374 apply (metis Prf.intros(1) mkeps_nullable)
 
       
   375 apply(simp)
 
       
   376 apply(erule Prf.cases)
 
       
   377 apply(simp_all)[7]
 
       
   378 apply(auto)[1]
 
       
   379 apply(rule Prf.intros)
 
       
   380 apply(auto)[2]
 
       
   381 (* ALT *)
 
       
   382 apply(erule Prf.cases)
 
       
   383 apply(simp_all)[7]
 
       
   384 apply(clarify)
 
   515 apply (metis Prf.intros(2))
 
   385 apply (metis Prf.intros(2))
 
   516 apply (metis Prf.intros(3))
 
   386 apply (metis Prf.intros(3))
 
   517 apply(simp)
 
   387 (* STAR *)
 
   518 apply(case_tac "nullable r1")
 
       
   519 apply(simp)
 
       
   520 apply(erule Prf.cases)
 
       
   521 apply(simp_all)[7]
 
       
   522 apply(auto)[1]
 
       
   523 apply(erule Prf.cases)
 
       
   524 apply(simp_all)[7]
 
       
   525 apply(auto)[1]
 
       
   526 apply (metis Prf.intros(1))
 
       
   527 apply(auto)[1]
 
       
   528 apply (metis Prf.intros(1) mkeps_nullable)
 
       
   529 apply(simp)
 
       
   530 apply(erule Prf.cases)
 
       
   531 apply(simp_all)[7]
 
       
   532 apply(auto)[1]
 
       
   533 apply(rule Prf.intros)
 
       
   534 apply(auto)[2]
 
       
   535 apply(simp)
 
       
   536 apply(erule Prf.cases)
 
   388 apply(erule Prf.cases)
 
   537 apply(simp_all)[7]
 
   389 apply(simp_all)[7]
 
   538 apply(clarify)
 
   390 apply(clarify)
 
   539 apply(rotate_tac 2)
 
   391 apply(rotate_tac 2)
 
   540 apply(erule Prf.cases)
 
   392 apply(erule Prf.cases)
 
   541 apply(simp_all)[7]
 
   393 apply(simp_all)[7]
 
   542 apply(auto)
 
   394 apply(auto)
 
   543 apply (metis Prf.intros(6) Prf.intros(7))
 
   395 apply (metis Prf.intros(6) Prf.intros(7))
 
   544 by (metis Prf.intros(7))
 
   396 by (metis Prf.intros(7))
 
   545 
   397 
   546 
   398 lemma Prf_injval_flat:
 
   547 
       
   548 lemma v4:
 
       
   549   assumes "\<turnstile> v : der c r" 
   399   assumes "\<turnstile> v : der c r" 
   550   shows "flat (injval r c v) = c # (flat v)"
 
   400   shows "flat (injval r c v) = c # (flat v)"
 
   551 using assms
 
   401 using assms
 
   552 apply(induct arbitrary: v rule: der.induct)
 
   402 apply(induct arbitrary: v rule: der.induct)
 
   553 apply(simp)
 
   403 apply(simp)
 
   597 section {* Our Alternative Posix definition *}
 
   447 section {* Our Alternative Posix definition *}
 
   598 
   448 
   599 inductive 
   449 inductive 
   600   PMatch :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
 
   450   PMatch :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
 
   601 where
 
   451 where
 
   602   "[] \<in> EMPTY \<rightarrow> Void"
 
   452   "[] \<in> ONE \<rightarrow> Void"
 
   603 | "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
 
   453 | "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
 
   604 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 
   454 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 
   605 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 
   455 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 
   606 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
 
   456 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
 
   607     \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
   457     \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
   614 lemma PMatch1:
 
   464 lemma PMatch1:
 
   615   assumes "s \<in> r \<rightarrow> v"
 
   465   assumes "s \<in> r \<rightarrow> v"
 
   616   shows "\<turnstile> v : r" "flat v = s"
 
   466   shows "\<turnstile> v : r" "flat v = s"
 
   617 using assms
 
   467 using assms
 
   618 apply(induct s r v rule: PMatch.induct)
 
   468 apply(induct s r v rule: PMatch.induct)
 
   619 apply(auto)
 
   469 apply(auto intro: Prf.intros)
 
   620 apply (metis Prf.intros(4))
 
   470 done
 
   621 apply (metis Prf.intros(5))
 
       
   622 apply (metis Prf.intros(2))
 
       
   623 apply (metis Prf.intros(3))
 
       
   624 apply (metis Prf.intros(1))
 
       
   625 apply (metis Prf.intros(7))
 
       
   626 by (metis Prf.intros(6))
 
       
   627 
   471 
   628 lemma PMatch_mkeps:
 
   472 lemma PMatch_mkeps:
 
   629   assumes "nullable r"
 
   473   assumes "nullable r"
 
   630   shows "[] \<in> r \<rightarrow> mkeps r"
 
   474   shows "[] \<in> r \<rightarrow> mkeps r"
 
   631 using assms
 
   475 using assms
 
   743 apply(clarify)
 
   587 apply(clarify)
 
   744 by (metis PMatch1(2))
 
   588 by (metis PMatch1(2))
 
   745 
   589 
   746 
   590 
   747 
   591 
   748 lemma PMatch_Values:
 
       
   749   assumes "s \<in> r \<rightarrow> v"
 
       
   750   shows "v \<in> Values r s"
 
       
   751 using assms
 
       
   752 apply(simp add: Values_def PMatch1)
 
       
   753 by (metis append_Nil2 prefix_def)
 
       
   754 
   592 
   755 (* a proof that does not need proj *)
 
   593 (* a proof that does not need proj *)
 
   756 lemma PMatch2_roy_version:
 
   594 lemma PMatch2_roy_version:
 
   757   assumes "s \<in> (der c r) \<rightarrow> v"
 
   595   assumes "s \<in> (der c r) \<rightarrow> v"
 
   758   shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
 
   596   shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
 
   759 using assms
 
   597 using assms
 
   760 apply(induct r arbitrary: s v c rule: rexp.induct)
 
   598 apply(induct r arbitrary: s v c rule: rexp.induct)
 
   761 apply(auto)
 
   599 apply(auto)
 
   762 (* NULL case *)
 
   600 (* ZERO case *)
 
   763 apply(erule PMatch.cases)
 
   601 apply(erule PMatch.cases)
 
   764 apply(simp_all)[7]
 
   602 apply(simp_all)[7]
 
   765 (* EMPTY case *)
 
   603 (* ONE case *)
 
   766 apply(erule PMatch.cases)
 
   604 apply(erule PMatch.cases)
 
   767 apply(simp_all)[7]
 
   605 apply(simp_all)[7]
 
   768 (* CHAR case *)
 
   606 (* CHAR case *)
 
   769 apply(case_tac "c = char")
 
   607 apply(case_tac "c = char")
 
   770 apply(simp)
 
   608 apply(simp)
 
   849 apply(rule PMatch.intros)
 
   687 apply(rule PMatch.intros)
 
   850 apply(simp)
 
   688 apply(simp)
 
   851 apply(simp)
 
   689 apply(simp)
 
   852 apply(simp)
 
   690 apply(simp)
 
   853 apply (metis L.simps(6))
 
   691 apply (metis L.simps(6))
 
   854 apply(subst v4)
 
   692 apply(subst Prf_injval_flat)
 
   855 apply (metis PMatch1)
 
   693 apply (metis PMatch1)
 
   856 apply(simp)
 
   694 apply(simp)
 
   857 apply(auto)[1]
 
   695 apply(auto)[1]
 
   858 apply(drule_tac x="s\<^sub>3" in spec)
 
   696 apply(drule_tac x="s\<^sub>3" in spec)
 
   859 apply(drule mp)
 
   697 apply(drule mp)
 
   866 apply(simp)
 
   704 apply(simp)
 
   867 apply(rotate_tac 2)
 
   705 apply(rotate_tac 2)
 
   868 apply(drule PMatch.intros(6))
 
   706 apply(drule PMatch.intros(6))
 
   869 apply(rule PMatch.intros(7))
 
   707 apply(rule PMatch.intros(7))
 
   870 (* HERE *)
 
   708 (* HERE *)
 
   871 apply (metis PMatch1(1) list.distinct(1) v4)
 
   709 apply (metis PMatch1(1) list.distinct(1) Prf_injval_flat)
 
   872 apply (metis Nil_is_append_conv)
 
   710 apply (metis Nil_is_append_conv)
 
   873 apply(simp)
 
   711 apply(simp)
 
   874 apply(subst der_correctness)
 
   712 apply(subst der_correctness)
 
   875 apply(simp add: Der_def)
 
   713 apply(simp add: Der_def)
 
   876 done 
   714 done 
   877 
   715 
   878 
       
   879 lemma lex_correct1:
 
   716 lemma lex_correct1:
 
   880   assumes "s \<notin> L r"
 
   717   assumes "s \<notin> L r"
 
   881   shows "lex r s = None"
 
   718   shows "matcher r s = None"
 
   882 using assms
 
   719 using assms
 
   883 apply(induct s arbitrary: r)
 
   720 apply(induct s arbitrary: r)
 
   884 apply(simp)
 
   721 apply(simp)
 
   885 apply (metis nullable_correctness)
 
   722 apply (metis nullable_correctness)
 
   886 apply(auto)
 
   723 apply(auto)
 
   887 apply(drule_tac x="der a r" in meta_spec)
 
   724 apply(drule_tac x="der a r" in meta_spec)
 
   888 apply(drule meta_mp)
 
   725 apply(drule meta_mp)
 
   889 apply(auto)
 
   726 apply(auto)
 
   890 apply(simp add: L_flat_Prf)
 
   727 apply(simp add: der_correctness Der_def)
 
   891 by (metis v3 v4)
 
   728 done
 
   892 
   729 
   893 
   730 
   894 lemma lex_correct2:
 
   731 lemma lex_correct2:
 
   895   assumes "s \<in> L r"
 
   732   assumes "s \<in> L r"
 
   896   shows "\<exists>v. lex r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s"
 
   733   shows "\<exists>v. matcher r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s"
 
   897 using assms
 
   734 using assms
 
   898 apply(induct s arbitrary: r)
 
   735 apply(induct s arbitrary: r)
 
   899 apply(simp)
 
   736 apply(simp)
 
   900 apply (metis mkeps_flat mkeps_nullable nullable_correctness)
 
   737 apply (metis mkeps_flat mkeps_nullable nullable_correctness)
 
   901 apply(drule_tac x="der a r" in meta_spec)
 
   738 apply(drule_tac x="der a r" in meta_spec)
 
   902 apply(drule meta_mp)
 
   739 apply(drule meta_mp)
 
   903 apply(simp add: der_correctness Der_def)
 
   740 apply(simp add: der_correctness Der_def)
 
   904 apply(auto)
 
   741 apply(auto)
 
   905 apply (metis v3)
 
   742 apply (metis Prf_injval)
 
   906 apply(rule v4)
 
   743 apply(rule Prf_injval_flat)
 
   907 by simp
 
   744 by simp
 
   908 
   745 
   909 lemma lex_correct3:
 
   746 lemma lex_correct3:
 
   910   assumes "s \<in> L r"
 
   747   assumes "s \<in> L r"
 
   911   shows "\<exists>v. lex r s = Some(v) \<and> s \<in> r \<rightarrow> v"
 
   748   shows "\<exists>v. matcher r s = Some(v) \<and> s \<in> r \<rightarrow> v"
 
   912 using assms
 
   749 using assms
 
   913 apply(induct s arbitrary: r)
 
   750 apply(induct s arbitrary: r)
 
   914 apply(simp)
 
   751 apply(simp)
 
   915 apply (metis PMatch_mkeps nullable_correctness)
 
   752 apply (metis PMatch_mkeps nullable_correctness)
 
   916 apply(drule_tac x="der a r" in meta_spec)
 
   753 apply(drule_tac x="der a r" in meta_spec)
 
   919 apply(auto)
 
   756 apply(auto)
 
   920 by (metis PMatch2_roy_version)
 
   757 by (metis PMatch2_roy_version)
 
   921 
   758 
   922 lemma lex_correct5:
 
   759 lemma lex_correct5:
 
   923   assumes "s \<in> L r"
 
   760   assumes "s \<in> L r"
 
   924   shows "s \<in> r \<rightarrow> (lex2 r s)"
 
   761   shows "s \<in> r \<rightarrow> (matcher2 r s)"
 
   925 using assms
 
   762 using assms
 
   926 apply(induct s arbitrary: r)
 
   763 apply(induct s arbitrary: r)
 
   927 apply(simp)
 
   764 apply(simp)
 
   928 apply (metis PMatch_mkeps nullable_correctness)
 
   765 apply (metis PMatch_mkeps nullable_correctness)
 
   929 apply(simp)
 
   766 apply(simp)
 
   933 apply(simp add: der_correctness Der_def)
 
   770 apply(simp add: der_correctness Der_def)
 
   934 apply(auto)
 
   771 apply(auto)
 
   935 done
 
   772 done
 
   936 
   773 
   937 lemma 
   774 lemma 
   938   "lex2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))"
 
   775   "matcher2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))"
 
   939 apply(simp)
 
   776 apply(simp)
 
   940 done
 
   777 done
 
   941 
   778 
       
   779 
       
   780 section {* Attic stuff below *}
 
       
   781 
       
   782 section {* Projection function *}
 
       
   783 
       
   784 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 
       
   785 where
 
       
   786   "projval (CHAR d) c _ = Void"
 
       
   787 | "projval (ALT r1 r2) c (Left v1) = Left (projval r1 c v1)"
 
       
   788 | "projval (ALT r1 r2) c (Right v2) = Right (projval r2 c v2)"
 
       
   789 | "projval (SEQ r1 r2) c (Seq v1 v2) = 
       
   790      (if flat v1 = [] then Right(projval r2 c v2) 
       
   791       else if nullable r1 then Left (Seq (projval r1 c v1) v2)
 
       
   792                           else Seq (projval r1 c v1) v2)"
 
       
   793 | "projval (STAR r) c (Stars (v # vs)) = Seq (projval r c v) (Stars vs)"
 
       
   794 
       
   795 
       
   796 
       
   797 section {* Values Sets *}
 
       
   798 
       
   799 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100)
 
       
   800 where
 
       
   801   "s1 \<sqsubseteq> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"
 
       
   802 
       
   803 definition sprefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
 
       
   804 where
 
       
   805   "s1 \<sqsubset> s2 \<equiv> (s1 \<sqsubseteq> s2 \<and> s1 \<noteq> s2)"
 
       
   806 
       
   807 lemma length_sprefix:
 
       
   808   "s1 \<sqsubset> s2 \<Longrightarrow> length s1 < length s2"
 
       
   809 unfolding sprefix_def prefix_def
 
       
   810 by (auto)
 
       
   811 
       
   812 definition Prefixes :: "string \<Rightarrow> string set" where
 
       
   813   "Prefixes s \<equiv> {sp. sp \<sqsubseteq> s}"
 
       
   814 
       
   815 definition Suffixes :: "string \<Rightarrow> string set" where
 
       
   816   "Suffixes s \<equiv> rev ` (Prefixes (rev s))"
 
       
   817 
       
   818 definition SPrefixes :: "string \<Rightarrow> string set" where
 
       
   819   "SPrefixes s \<equiv> {sp. sp \<sqsubset> s}"
 
       
   820 
       
   821 definition SSuffixes :: "string \<Rightarrow> string set" where
 
       
   822   "SSuffixes s \<equiv> rev ` (SPrefixes (rev s))"
 
       
   823 
       
   824 lemma Suffixes_in: 
       
   825   "\<exists>s1. s1 @ s2 = s3 \<Longrightarrow> s2 \<in> Suffixes s3"
 
       
   826 unfolding Suffixes_def Prefixes_def prefix_def image_def
 
       
   827 apply(auto)
 
       
   828 by (metis rev_rev_ident)
 
       
   829 
       
   830 lemma SSuffixes_in: 
       
   831   "\<exists>s1. s1 \<noteq> [] \<and> s1 @ s2 = s3 \<Longrightarrow> s2 \<in> SSuffixes s3"
 
       
   832 unfolding SSuffixes_def Suffixes_def SPrefixes_def Prefixes_def sprefix_def prefix_def image_def
 
       
   833 apply(auto)
 
       
   834 by (metis append_self_conv rev.simps(1) rev_rev_ident)
 
       
   835 
       
   836 lemma Prefixes_Cons:
 
       
   837   "Prefixes (c # s) = {[]} \<union> {c # sp | sp. sp \<in> Prefixes s}"
 
       
   838 unfolding Prefixes_def prefix_def
 
       
   839 apply(auto simp add: append_eq_Cons_conv) 
       
   840 done
 
       
   841 
       
   842 lemma finite_Prefixes:
 
       
   843   "finite (Prefixes s)"
 
       
   844 apply(induct s)
 
       
   845 apply(auto simp add: Prefixes_def prefix_def)[1]
 
       
   846 apply(simp add: Prefixes_Cons)
 
       
   847 done
 
       
   848 
       
   849 lemma finite_Suffixes:
 
       
   850   "finite (Suffixes s)"
 
       
   851 unfolding Suffixes_def
 
       
   852 apply(rule finite_imageI)
 
       
   853 apply(rule finite_Prefixes)
 
       
   854 done
 
       
   855 
       
   856 lemma prefix_Cons:
 
       
   857   "((c # s1) \<sqsubseteq> (c # s2)) = (s1 \<sqsubseteq> s2)"
 
       
   858 apply(auto simp add: prefix_def)
 
       
   859 done
 
       
   860 
       
   861 lemma prefix_append:
 
       
   862   "((s @ s1) \<sqsubseteq> (s @ s2)) = (s1 \<sqsubseteq> s2)"
 
       
   863 apply(induct s)
 
       
   864 apply(simp)
 
       
   865 apply(simp add: prefix_Cons)
 
       
   866 done
 
       
   867 
       
   868 
       
   869 definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
 
       
   870   "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}"
 
       
   871 
       
   872 definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where
 
       
   873   "rest v s \<equiv> drop (length (flat v)) s"
 
       
   874 
       
   875 lemma rest_Nil:
 
       
   876   "rest v [] = []"
 
       
   877 apply(simp add: rest_def)
 
       
   878 done
 
       
   879 
       
   880 lemma rest_Suffixes:
 
       
   881   "rest v s \<in> Suffixes s"
 
       
   882 unfolding rest_def
 
       
   883 by (metis Suffixes_in append_take_drop_id)
 
       
   884 
       
   885 lemma Values_recs:
 
       
   886   "Values (ZERO) s = {}"
 
       
   887   "Values (ONE) s = {Void}"
 
       
   888   "Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
       
   889   "Values (ALT r1 r2) s = {Left v | v. v \<in> Values r1 s} \<union> {Right v | v. v \<in> Values r2 s}"
 
       
   890   "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}"
 
       
   891   "Values (STAR r) s = 
       
   892       {Stars []} \<union> {Stars (v # vs) | v vs. v \<in> Values r s \<and> Stars vs \<in> Values (STAR r) (rest v s)}"
 
       
   893 unfolding Values_def
 
       
   894 apply(auto)
 
       
   895 (*ZERO*)
 
       
   896 apply(erule Prf.cases)
 
       
   897 apply(simp_all)[7]
 
       
   898 (*ONE*)
 
       
   899 apply(erule Prf.cases)
 
       
   900 apply(simp_all)[7]
 
       
   901 apply(rule Prf.intros)
 
       
   902 apply (metis append_Nil prefix_def)
 
       
   903 (*CHAR*)
 
       
   904 apply(erule Prf.cases)
 
       
   905 apply(simp_all)[7]
 
       
   906 apply(rule Prf.intros)
 
       
   907 apply(erule Prf.cases)
 
       
   908 apply(simp_all)[7]
 
       
   909 (*ALT*)
 
       
   910 apply(erule Prf.cases)
 
       
   911 apply(simp_all)[7]
 
       
   912 apply (metis Prf.intros(2))
 
       
   913 apply (metis Prf.intros(3))
 
       
   914 (*SEQ*)
 
       
   915 apply(erule Prf.cases)
 
       
   916 apply(simp_all)[7]
 
       
   917 apply (simp add: append_eq_conv_conj prefix_def rest_def)
 
       
   918 apply (metis Prf.intros(1))
 
       
   919 apply (simp add: append_eq_conv_conj prefix_def rest_def)
 
       
   920 (*STAR*)
 
       
   921 apply(erule Prf.cases)
 
       
   922 apply(simp_all)[7]
 
       
   923 apply(rule conjI)
 
       
   924 apply(simp add: prefix_def)
 
       
   925 apply(auto)[1]
 
       
   926 apply(simp add: prefix_def)
 
       
   927 apply(auto)[1]
 
       
   928 apply (metis append_eq_conv_conj rest_def)
 
       
   929 apply (metis Prf.intros(6))
 
       
   930 apply (metis append_Nil prefix_def)
 
       
   931 apply (metis Prf.intros(7))
 
       
   932 by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
 
       
   933 
       
   934 lemma PMatch_Values:
 
       
   935   assumes "s \<in> r \<rightarrow> v"
 
       
   936   shows "v \<in> Values r s"
 
       
   937 using assms
 
       
   938 apply(simp add: Values_def PMatch1)
 
       
   939 by (metis append_Nil2 prefix_def)
 
       
   940 
       
   941 lemma finite_image_set2:
 
       
   942   "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {(x, y) | x y. P x \<and> Q y}"
 
       
   943   by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {(x, y)}"]) auto
 
   942 
   944 
   943 
   945 
   944 section {* Connection with Sulzmann's Ordering of values *}
 
   946 section {* Connection with Sulzmann's Ordering of values *}
 
   945 
   947 
   946 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 
   948 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 
   949 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
   951 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
   950 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
 
   952 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
 
   951 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
 
   953 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
 
   952 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
 
   954 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
 
   953 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 
   955 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 
   954 | "Void \<succ>EMPTY Void"
 
   956 | "Void \<succ>ONE Void"
 
   955 | "(Char c) \<succ>(CHAR c) (Char c)"
 
   957 | "(Char c) \<succ>(CHAR c) (Char c)"
 
   956 | "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))"
 
   958 | "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))"
 
   957 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
 
   959 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
 
   958 | "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
 
   960 | "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
 
   959 | "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
 
   961 | "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
 
   967   NPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
 
   969   NPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
 
   968 where
 
   970 where
 
   969  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
 
   971  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
 
   970 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 
   972 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 
   971 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
 
   973 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
 
   972 | "\<Turnstile> Void : EMPTY"
 
   974 | "\<Turnstile> Void : ONE"
 
   973 | "\<Turnstile> Char c : CHAR c"
 
   975 | "\<Turnstile> Char c : CHAR c"
 
   974 | "\<Turnstile> Stars [] : STAR r"
 
   976 | "\<Turnstile> Stars [] : STAR r"
 
   975 | "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Stars vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"
 
   977 | "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Stars vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"
 
   976 
   978 
   977 lemma NPrf_imp_Prf:
 
   979 lemma NPrf_imp_Prf:
 
  1161   assumes "s \<in> (der c r) \<rightarrow> v"
 
  1163   assumes "s \<in> (der c r) \<rightarrow> v"
 
  1162   shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
 
  1164   shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
 
  1163 using assms
 
  1165 using assms
 
  1164 apply(induct c r arbitrary: s v rule: der.induct)
 
  1166 apply(induct c r arbitrary: s v rule: der.induct)
 
  1165 apply(auto)
 
  1167 apply(auto)
 
  1166 (* NULL case *)
 
  1168 (* ZERO case *)
 
  1167 apply(erule PMatch.cases)
 
  1169 apply(erule PMatch.cases)
 
  1168 apply(simp_all)[7]
 
  1170 apply(simp_all)[7]
 
  1169 (* EMPTY case *)
 
  1171 (* ONE case *)
 
  1170 apply(erule PMatch.cases)
 
  1172 apply(erule PMatch.cases)
 
  1171 apply(simp_all)[7]
 
  1173 apply(simp_all)[7]
 
  1172 (* CHAR case *)
 
  1174 (* CHAR case *)
 
  1173 apply(case_tac "c = c'")
 
  1175 apply(case_tac "c = c'")
 
  1174 apply(simp)
 
  1176 apply(simp)
 
  1263 apply(rule PMatch.intros)
 
  1265 apply(rule PMatch.intros)
 
  1264 apply(simp)
 
  1266 apply(simp)
 
  1265 apply(simp)
 
  1267 apply(simp)
 
  1266 apply(simp)
 
  1268 apply(simp)
 
  1267 apply (metis L.simps(6))
 
  1269 apply (metis L.simps(6))
 
  1268 apply(subst v4)
 
  1270 apply(subst Prf_injval_flat)
 
  1269 apply (metis NPrf_imp_Prf PMatch1N)
 
  1271 apply (metis NPrf_imp_Prf PMatch1N)
 
  1270 apply(simp)
 
  1272 apply(simp)
 
  1271 apply(auto)[1]
 
  1273 apply(auto)[1]
 
  1272 apply(drule_tac x="s\<^sub>3" in spec)
 
  1274 apply(drule_tac x="s\<^sub>3" in spec)
 
  1273 apply(drule mp)
 
  1275 apply(drule mp)
 
  1278 apply(drule_tac x="v1" in meta_spec)
 
  1280 apply(drule_tac x="v1" in meta_spec)
 
  1279 apply(simp)
 
  1281 apply(simp)
 
  1280 apply(rotate_tac 2)
 
  1282 apply(rotate_tac 2)
 
  1281 apply(drule PMatch.intros(6))
 
  1283 apply(drule PMatch.intros(6))
 
  1282 apply(rule PMatch.intros(7))
 
  1284 apply(rule PMatch.intros(7))
 
  1283 apply (metis PMatch1(1) list.distinct(1) v4)
 
  1285 apply (metis PMatch1(1) list.distinct(1) Prf_injval_flat)
 
  1284 apply (metis Nil_is_append_conv)
 
  1286 apply (metis Nil_is_append_conv)
 
  1285 apply(simp)
 
  1287 apply(simp)
 
  1286 apply(subst der_correctness)
 
  1288 apply(subst der_correctness)
 
  1287 apply(simp add: Der_def)
 
  1289 apply(simp add: Der_def)
 
  1288 done 
  1290 done 
  1289 
  1291 
  1290 lemma lex_correct4:
 
  1292 lemma lex_correct4:
 
  1291   assumes "s \<in> L r"
 
  1293   assumes "s \<in> L r"
 
  1292   shows "\<exists>v. lex r s = Some(v) \<and> \<Turnstile> v : r \<and> flat v = s"
 
  1294   shows "\<exists>v. matcher r s = Some(v) \<and> \<Turnstile> v : r \<and> flat v = s"
 
  1293 using lex_correct3[OF assms]
 
  1295 using lex_correct3[OF assms]
 
  1294 apply(auto)
 
  1296 apply(auto)
 
  1295 apply (metis PMatch1N)
 
  1297 apply (metis PMatch1N)
 
  1296 by (metis PMatch1(2))
 
  1298 by (metis PMatch1(2))
 
  1297 
  1299
lexing