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/Re.thy
changeset 7 b409ecf47f64
parent 6 87618dae0e04
child 8 a605dda64267
equal deleted inserted replaced
6:87618dae0e04 7:b409ecf47f64 
     1 theory Matcher3simple
 
     1 theory Re
 
     2   imports "Main" 
     2   imports "Main" 
     3 begin
 
     3 begin
 
     4 
     4 
     5 section {* Sequential Composition of Sets *}
 
     5 section {* Sequential Composition of Sets *}
 
     6 
     6 
    39 | "L (EMPTY) = {[]}"
 
    39 | "L (EMPTY) = {[]}"
 
    40 | "L (CHAR c) = {[c]}"
 
    40 | "L (CHAR c) = {[c]}"
 
    41 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 
    41 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 
    42 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
    42 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
    43 
    43 
       
    44 
       
    45 section {* Values *}
 
       
    46 
    44 datatype val = 
    47 datatype val = 
    45   Void
 
    48   Void
 
    46 | Char char
 
    49 | Char char
 
    47 | Seq val val
 
    50 | Seq val val
 
    48 | Right val
 
    51 | Right val
 
    49 | Left val
 
    52 | Left val
 
    50 
    53 
       
    54 section {* Relation between values and regular expressions *}
 
       
    55 
    51 inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 
    56 inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 
    52 where
 
    57 where
 
    53  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
 
    58  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
 
    54 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
 
    59 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
 
    55 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 
    60 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 
    56 | "\<turnstile> Void : EMPTY"
 
    61 | "\<turnstile> Void : EMPTY"
 
    57 | "\<turnstile> Char c : CHAR c"
 
    62 | "\<turnstile> Char c : CHAR c"
 
    58 
    63 
       
    64 section {* The string behind a value *}
 
       
    65 
    59 fun flat :: "val \<Rightarrow> string"
 
    66 fun flat :: "val \<Rightarrow> string"
 
    60 where
 
    67 where
 
    61   "flat(Void) = []"
 
    68   "flat(Void) = []"
 
    62 | "flat(Char c) = [c]"
 
    69 | "flat(Char c) = [c]"
 
    63 | "flat(Left v) = flat(v)"
 
    70 | "flat(Left v) = flat(v)"
 
    64 | "flat(Right v) = flat(v)"
 
    71 | "flat(Right v) = flat(v)"
 
    65 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
 
    72 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
 
    66 
    73 
    67 (* not actually in the paper *)
 
       
    68 datatype tree = 
       
    69   Leaf string
 
       
    70 | Branch tree tree
 
       
    71 
       
    72 fun flats :: "val \<Rightarrow> tree"
 
       
    73 where
 
       
    74   "flats(Void) = Leaf []"
 
       
    75 | "flats(Char c) = Leaf [c]"
 
       
    76 | "flats(Left v) = flats(v)"
 
       
    77 | "flats(Right v) = flats(v)"
 
       
    78 | "flats(Seq v1 v2) = Branch (flats v1) (flats v2)"
 
       
    79 
       
    80 fun flatten :: "tree \<Rightarrow> string"
 
       
    81 where
 
       
    82   "flatten (Leaf s) = s"
 
       
    83 | "flatten (Branch t1 t2) = flatten t1 @ flatten t2" 
       
    84 
       
    85 lemma flats_flat:
 
       
    86   shows "flat v1 = flatten (flats v1)"
 
       
    87 apply(induct v1)
 
       
    88 apply(simp_all)
 
       
    89 done
 
       
    90 
    74 
    91 lemma Prf_flat_L:
 
    75 lemma Prf_flat_L:
 
    92   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 
    76   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 
    93 using assms
 
    77 using assms
 
    94 apply(induct)
 
    78 apply(induct)
 
   102 apply (metis Prf.intros(4) flat.simps(1))
 
    86 apply (metis Prf.intros(4) flat.simps(1))
 
   103 apply (metis Prf.intros(5) flat.simps(2))
 
    87 apply (metis Prf.intros(5) flat.simps(2))
 
   104 apply (metis Prf.intros(1) flat.simps(5))
 
    88 apply (metis Prf.intros(1) flat.simps(5))
 
   105 apply (metis Prf.intros(2) flat.simps(3))
 
    89 apply (metis Prf.intros(2) flat.simps(3))
 
   106 apply (metis Prf.intros(3) flat.simps(4))
 
    90 apply (metis Prf.intros(3) flat.simps(4))
 
   107 sorry
 
    91 apply(erule Prf.cases)
 
   108 
    92 apply(auto)
 
   109 (*by (smt Prf.cases flat.simps(3) flat.simps(4) rexp.distinct(13) rexp.distinct(17) rexp.distinct(19) rexp.inject(3))*)
 
    93 done
 
       
    94 
       
    95 section {* Ordering of values *}
 
   110 
    96 
   111 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 
    97 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 
   112 where
 
    98 where
 
   113   "\<lbrakk>v1 = v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
    99   "\<lbrakk>v1 = v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
   114 | "v1  \<succ>r1 v1' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
   100 | "v1  \<succ>r1 v1' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
   131 apply(rule ValOrd.intros)
 
   117 apply(rule ValOrd.intros)
 
   132 apply(simp)
 
   118 apply(simp)
 
   133 done
 
   119 done
 
   134 *)
 
   120 *)
 
   135 
   121 
       
   122 section {* Posix definition *}
 
       
   123 
   136 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
   124 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
   137 where
 
   125 where
 
   138   "POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v')"
 
   126   "POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v')"
 
   139 
   127 
   140 (*
 
   128 (*
 
   245 using assms
 
   233 using assms
 
   246 apply(induct)
 
   234 apply(induct)
 
   247 apply(auto intro: ValOrd.intros)
 
   235 apply(auto intro: ValOrd.intros)
 
   248 done
 
   236 done
 
   249 
   237 
   250 (*
 
       
   251 lemma ValOrd_length:
 
       
   252   assumes "v1 \<succ>r v2" shows "length (flat v1) \<ge> length (flat v2)"
 
       
   253 using assms
 
       
   254 apply(induct)
 
       
   255 apply(auto)
 
       
   256 done
 
       
   257 *)
 
       
   258 
   238 
   259 section {* The Matcher *}
 
   239 section {* The Matcher *}
 
   260 
   240 
   261 fun
 
   241 fun
 
   262  nullable :: "rexp \<Rightarrow> bool"
 
   242  nullable :: "rexp \<Rightarrow> bool"
 
   291 using assms
 
   271 using assms
 
   292 apply(induct rule: nullable.induct)
 
   272 apply(induct rule: nullable.induct)
 
   293 apply(auto)
 
   273 apply(auto)
 
   294 done
 
   274 done
 
   295 
   275 
   296 
   276 text {*
 
   297 lemma mkeps_flats:
 
   277   The value mkeps returns is always the correct POSIX
 
   298   assumes "nullable(r)" shows "flatten (flats (mkeps r)) = []"
 
   278   value.
 
   299 using assms
 
   279 *}
 
   300 apply(induct rule: nullable.induct)
 
       
   301 apply(auto)
 
       
   302 done
 
       
   303 
   280 
   304 lemma mkeps_POSIX:
 
   281 lemma mkeps_POSIX:
 
   305   assumes "nullable r"
 
   282   assumes "nullable r"
 
   306   shows "POSIX (mkeps r) r"
 
   283   shows "POSIX (mkeps r) r"
 
   307 using assms
 
   284 using assms
 
   312 apply(erule Prf.cases)
 
   289 apply(erule Prf.cases)
 
   313 apply(simp_all)[5]
 
   290 apply(simp_all)[5]
 
   314 apply (metis ValOrd.intros)
 
   291 apply (metis ValOrd.intros)
 
   315 apply(simp add: POSIX_def)
 
   292 apply(simp add: POSIX_def)
 
   316 apply(auto)[1]
 
   293 apply(auto)[1]
 
   317 sorry
 
   294 apply(simp add: POSIX_def)
 
   318 
   295 apply(auto)[1]
 
       
   296 apply(erule Prf.cases)
 
       
   297 apply(simp_all)[5]
 
       
   298 apply(auto)
 
       
   299 apply (simp add: ValOrd.intros(2) mkeps_flat)
 
       
   300 apply(simp add: POSIX_def)
 
       
   301 apply(auto)[1]
 
       
   302 apply(erule Prf.cases)
 
       
   303 apply(simp_all)[5]
 
       
   304 apply(auto)
 
       
   305 apply (simp add: ValOrd.intros(6))
 
       
   306 apply (simp add: ValOrd.intros(3))
 
       
   307 apply(simp add: POSIX_def)
 
       
   308 apply(auto)[1]
 
       
   309 apply(erule Prf.cases)
 
       
   310 apply(simp_all)[5]
 
       
   311 apply(auto)
 
       
   312 apply (simp add: ValOrd.intros(6))
 
       
   313 apply (simp add: ValOrd.intros(3))
 
       
   314 apply(simp add: POSIX_def)
 
       
   315 apply(auto)[1]
 
       
   316 apply(erule Prf.cases)
 
       
   317 apply(simp_all)[5]
 
       
   318 apply(auto)
 
       
   319 apply (metis Prf_flat_L mkeps_flat nullable_correctness)
 
       
   320 by (simp add: ValOrd.intros(5))
 
       
   321 
       
   322 
       
   323 section {* Derivatives *}
 
   319 
   324 
   320 fun
 
   325 fun
 
   321  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 
   326  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 
   322 where
 
   327 where
 
   323   "der c (NULL) = NULL"
 
   328   "der c (NULL) = NULL"
 
   333  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 
   338  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 
   334 where
 
   339 where
 
   335   "ders [] r = r"
 
   340   "ders [] r = r"
 
   336 | "ders (c # s) r = ders s (der c r)"
 
   341 | "ders (c # s) r = ders s (der c r)"
 
   337 
   342 
       
   343 section {* Injection function *}
 
       
   344 
   338 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 
   345 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 
   339 where
 
   346 where
 
   340   "injval (CHAR d) c Void = Char d"
 
   347   "injval (CHAR d) c Void = Char d"
 
   341 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
 
   348 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
 
   342 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
 
   349 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
 
   343 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
 
   350 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
 
   344 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
 
   351 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
 
   345 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
 
   352 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
 
       
   353 
       
   354 section {* Projection function *}
 
   346 
   355 
   347 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 
   356 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 
   348 where
 
   357 where
 
   349   "projval (CHAR d) c _ = Void"
 
   358   "projval (CHAR d) c _ = Void"
 
   350 | "projval (ALT r1 r2) c (Left v1) = Left(projval r1 c v1)"
 
   359 | "projval (ALT r1 r2) c (Left v1) = Left(projval r1 c v1)"
 
   352 | "projval (SEQ r1 r2) c (Seq v1 v2) = 
   361 | "projval (SEQ r1 r2) c (Seq v1 v2) = 
   353      (if flat v1 = [] then Right(projval r2 c v2) 
   362      (if flat v1 = [] then Right(projval r2 c v2) 
   354       else if nullable r1 then Left (Seq (projval r1 c v1) v2)
 
   363       else if nullable r1 then Left (Seq (projval r1 c v1) v2)
 
   355                           else Seq (projval r1 c v1) v2)"
 
   364                           else Seq (projval r1 c v1) v2)"
 
   356 
   365 
       
   366 text {*
 
       
   367   Injection value is related to r
 
       
   368 *}
 
       
   369 
   357 lemma v3:
 
   370 lemma v3:
 
   358   assumes "\<turnstile> v : der c r" shows "\<turnstile> (injval r c v) : r"
 
   371   assumes "\<turnstile> v : der c r" shows "\<turnstile> (injval r c v) : r"
 
   359 using assms
 
   372 using assms
 
   360 apply(induct arbitrary: v rule: der.induct)
 
   373 apply(induct arbitrary: v rule: der.induct)
 
   361 apply(simp)
 
   374 apply(simp)
 
   392 apply(auto)[1]
 
   405 apply(auto)[1]
 
   393 apply(rule Prf.intros)
 
   406 apply(rule Prf.intros)
 
   394 apply(auto)[2]
 
   407 apply(auto)[2]
 
   395 done
 
   408 done
 
   396 
   409 
   397 fun head where
 
   410 text {*
 
   398   "head [] = None"
 
   411   The string behin the injection value is an added c
 
   399 | "head (x#xs) = Some x"
 
   412 *}
 
   400 
       
   401 lemma head1:
 
       
   402   assumes "head (xs @ ys) = Some x"
 
       
   403   shows "(head xs = Some x) \<or> (xs = [] \<and> head ys = Some x)"
 
       
   404 using assms
 
       
   405 apply(induct xs)
 
       
   406 apply(auto)
 
       
   407 done
 
       
   408 
       
   409 lemma head2:
 
       
   410   assumes "head (xs @ ys) = None"
 
       
   411   shows "(head xs = None) \<and> (head ys = None)"
 
       
   412 using assms
 
       
   413 apply(induct xs)
 
       
   414 apply(auto)
 
       
   415 done
 
       
   416 
   413 
   417 lemma v4:
 
   414 lemma v4:
 
   418   assumes "\<turnstile> v : der c r" shows "flat (injval r c v) = c#(flat v)"
 
   415   assumes "\<turnstile> v : der c r" shows "flat (injval r c v) = c # (flat v)"
 
   419 using assms
 
   416 using assms
 
   420 apply(induct arbitrary: v rule: der.induct)
 
   417 apply(induct arbitrary: v rule: der.induct)
 
   421 apply(simp)
 
   418 apply(simp)
 
   422 apply(erule Prf.cases)
 
   419 apply(erule Prf.cases)
 
   423 apply(simp_all)[5]
 
   420 apply(simp_all)[5]
 
   449 apply(simp)
 
   446 apply(simp)
 
   450 apply(erule Prf.cases)
 
   447 apply(erule Prf.cases)
 
   451 apply(simp_all)[5]
 
   448 apply(simp_all)[5]
 
   452 done
 
   449 done
 
   453 
   450 
       
   451 text {*
 
       
   452   Injection followed by projection is the identity.
 
       
   453 *}
 
   454 
   454 
   455 lemma proj_inj_id:
 
   455 lemma proj_inj_id:
 
   456   assumes "\<turnstile> v : der c r" 
   456   assumes "\<turnstile> v : der c r" 
   457   shows "projval r c (injval r c v) = v"
 
   457   shows "projval r c (injval r c v) = v"
 
   458 using assms
 
   458 using assms
 
   492 apply(simp_all)[5]
 
   492 apply(simp_all)[5]
 
   493 apply(auto)[1]
 
   493 apply(auto)[1]
 
   494 apply(simp add: v4)
 
   494 apply(simp add: v4)
 
   495 done
 
   495 done
 
   496 
   496 
   497 lemma Le_2a: "(head (flat v) = None) = (flat v = [])"
 
   497 text {* 
   498 apply(induct v)
 
   498 
   499 apply(simp_all)
 
   499   HERE: Crucial lemma that does not go through in the sequence case. 
   500 apply (metis Nil_is_append_conv head.elims option.distinct(1))
 
   500 
   501 done
 
   501 *}
 
   502 
       
   503 (* HERE *)
 
       
   504 lemma v5:
 
   502 lemma v5:
 
   505   assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
 
   503   assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
 
   506   shows "POSIX (injval r c v) r"
 
   504   shows "POSIX (injval r c v) r"
 
   507 using assms
 
   505 using assms
 
   508 apply(induct r)
 
       
   509 apply(simp (no_asm) only: POSIX_def)
 
       
   510 apply(rule allI)
 
       
   511 apply(rule impI)
 
       
   512 apply(simp)
 
       
   513 apply(erule Prf.cases)
 
       
   514 apply(simp_all)[5]
 
       
   515 apply(induct arbitrary: v rule: der.induct)
 
   506 apply(induct arbitrary: v rule: der.induct)
 
   516 apply(simp)
 
   507 apply(simp)
 
   517 apply(erule Prf.cases)
 
   508 apply(erule Prf.cases)
 
   518 apply(simp_all)[5]
 
   509 apply(simp_all)[5]
 
   519 apply(simp)
 
   510 apply(simp)
 
   524 apply(auto simp add: POSIX_def)[1]
 
   515 apply(auto simp add: POSIX_def)[1]
 
   525 apply(erule Prf.cases)
 
   516 apply(erule Prf.cases)
 
   526 apply(simp_all)[5]
 
   517 apply(simp_all)[5]
 
   527 apply(erule Prf.cases)
 
   518 apply(erule Prf.cases)
 
   528 apply(simp_all)[5]
 
   519 apply(simp_all)[5]
 
   529 apply (metis ValOrd.intros(7))
 
   520 using ValOrd.simps apply blast
 
   530 apply(erule Prf.cases)
 
   521 apply(auto)
 
   531 apply(simp_all)[5]
 
   522 apply(erule Prf.cases)
 
   532 prefer 2
 
   523 apply(simp_all)[5]
 
   533 apply(simp)
 
   524 prefer 2 
   534 apply(case_tac "nullable r1")
 
   525 apply(case_tac "nullable r1")
 
   535 apply(simp)
 
   526 apply(simp)
 
   536 defer
 
   527 defer
 
   537 apply(simp)
 
   528 apply(simp)
 
   538 apply(erule Prf.cases)
 
   529 apply(erule Prf.cases)
 
   539 apply(simp_all)[5]
 
   530 apply(simp_all)[5]
 
   540 apply(auto)[1]
 
   531 apply(auto)[1]
 
   541 apply(drule POSIX_SEQ)
 
   532 oops
 
   542 apply(assumption)
 
       
   543 apply(assumption)
 
       
   544 apply(auto)[1]
 
       
   545 apply(rule POSIX_SEQ_I)
 
       
   546 apply metis
 
       
   547 apply(simp)
 
       
   548 apply(simp)
 
       
   549 apply(erule Prf.cases)
 
       
   550 apply(simp_all)[5]
 
       
   551 apply(auto)[1]
 
       
   552 apply(drule POSIX_ALT)
 
       
   553 apply(rule POSIX_ALT_I1)
 
       
   554 apply metis
 
       
   555 defer
 
       
   556 apply(erule Prf.cases)
 
       
   557 apply(simp_all)[5]
 
       
   558 apply(auto)
 
       
   559 apply(rotate_tac 5)
 
       
   560 apply(erule Prf.cases)
 
       
   561 apply(simp_all)[5]
 
       
   562 apply(auto)[1]
 
       
   563 apply(drule POSIX_ALT)
 
       
   564 apply(drule POSIX_SEQ)
 
       
   565 apply(simp)
 
       
   566 apply(simp)
 
       
   567 apply(rule POSIX_SEQ_I)
 
       
   568 apply metis
 
       
   569 apply(simp)
 
       
   570 apply(drule POSIX_ALT1a)
 
       
   571 apply(rule POSIX_SEQ_I)
 
       
   572 apply (metis mkeps_POSIX)
 
       
   573 apply(metis)
 
       
   574 apply(frule POSIX_ALT1a)
 
       
   575 apply(rotate_tac 1)
 
       
   576 apply(drule_tac x="v2" in meta_spec)
 
       
   577 apply(simp)
 
       
   578 apply(rule POSIX_ALT_I2)
 
       
   579 apply(simp)
 
       
   580 apply(frule POSIX_ALT1a)
 
       
   581 apply(auto)
 
       
   582 apply(subst v4)
 
       
   583 apply(simp)
 
       
   584 apply(simp)
 
       
   585 apply(case_tac "\<exists>r. v2 \<succ>r v'")
 
       
   586 apply (metis ValOrd_length le_neq_implies_less less_Suc_eq)
 
       
   587 apply(auto)[1]
 
       
   588 apply(frule_tac x="der c r2" in spec)
 
       
   589 apply(subgoal_tac "\<not>(Right v2 \<succ>(ALT (der c r1) (der c r2)) Right v')")
 
       
   590 prefer 2
 
       
   591 apply(rule notI)
 
       
   592 apply(erule ValOrd.cases)
 
       
   593 apply(simp_all)[7]
 
       
   594 apply(subst (asm) (1) POSIX_def)
 
       
   595 apply(simp)
 
       
   596 apply(subgoal_tac "(\<not> \<turnstile> Right v' : ALT (der c r1) (der c r2)) \<or> (flats v2 \<noteq> flats v')")
 
       
   597 prefer 2
 
       
   598 apply (metis flats.simps(4))
 
       
   599 apply(simp)
 
       
   600 apply(auto)[1]
 
       
   601 apply(subst v4)
 
       
   602 apply(simp)
 
       
   603 apply(simp)
 
       
   604 apply(case_tac "v2 \<succ>r1 v'")
 
       
   605 apply (metis ValOrd_length le_neq_implies_less less_Suc_eq)
 
       
   606 apply(
 
       
   607 
       
   608 apply(drule_tac x="projval (ALT r1 r2) c v'" in spec)
 
       
   609 apply(drule mp)
 
       
   610 apply(auto)
 
       
   611 apply(frule POSIX_ALT1b)
 
       
   612 apply(auto)
 
       
   613 apply(subst v4)
 
       
   614 apply(simp)
 
       
   615 apply(simp)
 
       
   616 apply(simp add: flats_flat)
 
       
   617 apply(rotate_tac 1)
 
       
   618 apply(drule_tac x="v2" in meta_spec)
 
       
   619 apply(simp)
 
       
   620 apply(rule POSIX_ALT_I2)
 
       
   621 apply(simp)
 
       
   622 apply(auto)[1]
 
       
   623 apply(subst v4)
 
       
   624 apply(simp)
 
       
   625 defer
 
       
   626 apply(erule Prf.cases)
 
       
   627 apply(simp_all)[5]
 
       
   628 apply(auto)
 
       
   629 apply(rotate_tac 5)
 
       
   630 apply(erule Prf.cases)
 
       
   631 apply(simp_all)[5]
 
       
   632 apply(auto)[1]
 
       
   633 apply(drule POSIX_ALT)
 
       
   634 apply(drule POSIX_SEQ)
 
       
   635 apply(simp)
 
       
   636 apply(simp)
 
       
   637 apply(rule POSIX_SEQ_I)
 
       
   638 apply metis
 
       
   639 apply(simp)
 
       
   640 apply(drule POSIX_ALT1a)
 
       
   641 apply(rule POSIX_SEQ_I)
 
       
   642 apply (metis mkeps_POSIX)
 
       
   643 apply metis
 
       
   644 apply(drule_tac x="projval r1 c v'" in meta_spec)
 
       
   645 apply(drule meta_mp)
 
       
   646 defer
 
       
   647 apply(drule meta_mp)
 
       
   648 defer
 
       
   649 apply(subst (asm) (1) POSIX_def)
 
       
   650 apply(simp)
 
       
   651 
       
   652 
       
   653 
       
   654 lemma inj_proj_id:
 
       
   655   assumes "\<turnstile> v : r" "POSIX v r" "head (flat v) = Some c"  
       
   656   shows "injval r c (projval r c v) = v"
 
       
   657 using assms
 
       
   658 apply(induct v r arbitrary: rule: Prf.induct)
 
       
   659 apply(simp)
 
       
   660 apply(auto)[1]
 
       
   661 
       
   662 apply(simp)
 
       
   663 apply(frule POSIX_head)
 
       
   664 apply(assumption)
 
       
   665 apply(simp)
 
       
   666 apply(drule meta_mp)
 
       
   667 
       
   668 apply(frule POSIX_E1)
 
       
   669 apply(erule Prf.cases)
 
       
   670 apply(simp_all)[7]
 
       
   671 apply(frule POSIX_E1)
 
       
   672 apply(erule Prf.cases)
 
       
   673 apply(simp_all)[7]
 
       
   674 apply(frule POSIX_E1)
 
       
   675 apply(erule Prf.cases)
 
       
   676 apply(simp_all)[7]
 
       
   677 apply(frule POSIX_E1)
 
       
   678 defer
 
       
   679 apply(frule POSIX_E1)
 
       
   680 apply(erule Prf.cases)
 
       
   681 apply(simp_all)[7]
 
       
   682 apply(auto)[1]
 
       
   683 
       
   684 apply(simp)
 
       
   685 apply(erule Prf.cases)
 
       
   686 apply(simp_all)[7]
 
       
   687 apply(simp)
 
       
   688 apply(case_tac "c = char")
 
       
   689 apply(simp)
 
       
   690 apply(erule Prf.cases)
 
       
   691 apply(simp_all)[7]
 
       
   692 apply(simp)
 
       
   693 apply(erule Prf.cases)
 
       
   694 apply(simp_all)[7]
 
       
   695 
       
   696 
       
   697 lemma POSIX_head:
 
       
   698   assumes "POSIX (Stars (v#vs)) (STAR r)" "head (flat v @ flat (Stars vs)) = Some c"
 
       
   699   shows "head (flat v) = Some c"
 
       
   700 using assms
 
       
   701 apply(rule_tac ccontr)
 
       
   702 apply(frule POSIX_E1)
 
       
   703 apply(drule Le_1)
 
       
   704 apply(assumption)
 
       
   705 apply(auto)[1]
 
       
   706 apply(auto simp add: POSIX_def)
 
       
   707 apply(drule_tac x="Stars (v'#vs')" in spec)
 
       
   708 apply(simp)
 
       
   709 apply(simp add: ValOrd_eq_def)
 
       
   710 apply(auto)
 
       
   711 apply(erule ValOrd.cases)
 
       
   712 apply(simp_all)
 
       
   713 apply(auto)
 
       
   714 using Le_2
 
       
   715 
       
   716 by (metis Le_2 Le_2a head1)
 
       
   717 
       
   718 
       
   719 lemma inj_proj_id:
 
       
   720   assumes "\<turnstile> v : r" "POSIX v r" "head (flat v) = Some c"  
       
   721   shows "injval r c (projval r c v) = v"
 
       
   722 using assms
 
       
   723 apply(induct r arbitrary: rule: Prf.induct)
 
       
   724 apply(simp)
 
       
   725 apply(simp)
 
       
   726 apply(frule POSIX_head)
 
       
   727 apply(assumption)
 
       
   728 apply(simp)
 
       
   729 apply(drule meta_mp)
 
       
   730 
       
   731 apply(frule POSIX_E1)
 
       
   732 apply(erule Prf.cases)
 
       
   733 apply(simp_all)[7]
 
       
   734 apply(frule POSIX_E1)
 
       
   735 apply(erule Prf.cases)
 
       
   736 apply(simp_all)[7]
 
       
   737 apply(frule POSIX_E1)
 
       
   738 apply(erule Prf.cases)
 
       
   739 apply(simp_all)[7]
 
       
   740 apply(frule POSIX_E1)
 
       
   741 defer
 
       
   742 apply(frule POSIX_E1)
 
       
   743 apply(erule Prf.cases)
 
       
   744 apply(simp_all)[7]
 
       
   745 apply(auto)[1]
 
       
   746 
       
   747 apply(simp)
 
       
   748 apply(erule Prf.cases)
 
       
   749 apply(simp_all)[7]
 
       
   750 apply(simp)
 
       
   751 apply(case_tac "c = char")
 
       
   752 apply(simp)
 
       
   753 apply(erule Prf.cases)
 
       
   754 apply(simp_all)[7]
 
       
   755 apply(simp)
 
       
   756 apply(erule Prf.cases)
 
       
   757 apply(simp_all)[7]
 
       
   758 defer
 
       
   759 apply(simp)
 
       
   760 apply(erule Prf.cases)
 
       
   761 apply(simp_all)[7]
 
       
   762 apply(simp)
 
       
   763 apply(erule Prf.cases)
 
       
   764 apply(simp_all)[7]
 
       
   765 apply(auto)[1]
 
       
   766 apply(rotate_tac 2)
 
       
   767 apply(erule Prf.cases)
 
       
   768 apply(simp_all)[7]
 
       
   769 apply(case_tac "nullable rexp1")
 
       
   770 apply(simp)
 
       
   771 apply(erule Prf.cases)
 
       
   772 apply(simp_all)[7]
 
       
   773 apply(auto)[1]
 
       
   774 apply(erule Prf.cases)
 
       
   775 apply(simp_all)[7]
 
       
   776 apply(auto)[1]
 
       
   777 apply(simp add: v4)
 
       
   778 apply(auto)[1]
 
       
   779 apply(simp add: v2a)
 
       
   780 apply(simp only: der.simps)
 
       
   781 apply(simp)
 
       
   782 apply(erule Prf.cases)
 
       
   783 apply(simp_all)[7]
 
       
   784 apply(auto)[1]
 
       
   785 apply(simp add: v4)
 
       
   786 done
 
       
   787 
       
   788 
       
   789 
       
   790 lemma STAR_obtain:
 
       
   791   assumes "\<turnstile> v : STAR r"
 
       
   792   obtains vs where "\<turnstile> Stars vs : STAR r" and "v = Stars vs"
 
       
   793 using assms
 
       
   794 by (smt Prf.cases rexp.distinct(17) rexp.distinct(23) rexp.distinct(27) rexp.distinct(29))
 
       
   795 
       
   796 fun first :: "val \<Rightarrow> char option"
 
       
   797 where
 
       
   798   "first Void = None"
 
       
   799 | "first (Char c) = Some c"
 
       
   800 | "first (Seq v1 v2) = (if (\<exists>c. first v1 = Some c) then first v1 else first v2)"
 
       
   801 | "first (Right v) = first v"
 
       
   802 | "first (Left v) = first v"
 
       
   803 | "first (Stars []) = None"
 
       
   804 | "first (Stars (v#vs)) =  (if (\<exists>c. first v = Some c) then first v else first (Stars vs))"   
       
   805 
       
   806 lemma flat: 
       
   807   shows "flat v = [] \<longleftrightarrow> first v = None"
 
       
   808   and "flat (Stars vs) = [] \<longleftrightarrow> first (Stars vs) = None"
 
       
   809 apply(induct v and vs)
 
       
   810 apply(auto)
 
       
   811 done
 
       
   812 
       
   813 lemma first: 
       
   814   shows "first v = Some c \<Longrightarrow> head (flat v @ ys) = Some c"
 
       
   815 apply(induct arbitrary: ys rule: first.induct)
 
       
   816 apply(auto split: if_splits simp add: flat[symmetric])
 
       
   817 done
 
       
   818 
       
   819 
       
   820 
       
   821 lemma v5:
 
       
   822   assumes "POSIX v r" "head (flat v) = Some c" 
       
   823   shows "\<turnstile> projval r c v : der c r"
 
       
   824 using assms
 
       
   825 apply(induct r arbitrary: c v rule: rexp.induct)
 
       
   826 prefer 6
 
       
   827 apply(frule POSIX_E1)
 
       
   828 apply(erule Prf.cases)
 
       
   829 apply(simp_all)[7]
 
       
   830 apply(rule Prf.intros)
 
       
   831 apply(drule_tac x="c" in meta_spec)
 
       
   832 apply(drule_tac x="va" in meta_spec)
 
       
   833 apply(drule meta_mp)
 
       
   834 apply(simp add: POSIX_def)
 
       
   835 apply(auto)[1]
 
       
   836 apply(drule_tac x="Stars (v'#vs)" in spec)
 
       
   837 apply(simp)
 
       
   838 apply(drule mp)
 
       
   839 apply (metis Prf.intros(2))
 
       
   840 apply(simp add: ValOrd_eq_def)
 
       
   841 apply(erule disjE)
 
       
   842 apply(simp)
 
       
   843 apply(erule ValOrd.cases)
 
       
   844 apply(simp_all)[10]
 
       
   845 apply(drule_tac meta_mp)
 
       
   846 apply(drule head1)
 
       
   847 apply(auto)[1]
 
       
   848 apply(simp add: POSIX_def)
 
       
   849 apply(auto)[1]
 
       
   850 apply(drule_tac x="Stars (va#vs)" in spec)
 
       
   851 apply(simp)
 
       
   852 prefer 6
 
       
   853 apply(simp)
 
       
   854 apply(auto split: if_splits)[1]
 
       
   855 apply(erule Prf.cases)
 
       
   856 apply(simp_all)[7]
 
       
   857 apply(rule Prf.intros)
 
       
   858 apply metis
 
       
   859 apply(simp)
 
       
   860 apply(erule Prf.cases)
 
       
   861 apply(simp_all)[7]
 
       
   862 apply(auto split: if_splits)[1]
 
       
   863 apply(rule Prf.intros)
 
       
   864 apply(auto split: if_splits)[1]
 
       
   865 apply(erule Prf.cases)
 
       
   866 apply(simp_all)[7]
 
       
   867 apply(auto)
 
       
   868 apply(case_tac "char = c")
 
       
   869 apply(simp)
 
       
   870 apply(rule Prf.intros)
 
       
   871 apply(simp)
 
       
   872 apply(erule Prf.cases)
 
       
   873 apply(simp_all)[
 
       
   874 
       
   875 
       
   876 lemma uu:
 
       
   877   assumes ih: "\<And>v c. \<lbrakk>head (flat v) = Some c\<rbrakk> \<Longrightarrow> \<turnstile> projval rexp c v : der c rexp"
 
       
   878   assumes "\<turnstile> Stars vs : STAR rexp"
 
       
   879   and "first (Stars (v#vs)) = Some c"
 
       
   880   shows "\<turnstile> projval rexp c v : der c rexp"
 
       
   881 using assms(2,3)
 
       
   882 apply(induct vs)
 
       
   883 apply(simp_all)
 
       
   884 apply(auto split: if_splits)
 
       
   885 apply (metis first head1 ih)
 
       
   886 apply (metis first head1 ih)
 
       
   887 
       
   888 apply(auto)
 
       
   889 
       
   890 lemma v5:
 
       
   891   assumes "\<turnstile> v : r" "head (flat v) = Some c" 
       
   892   shows "\<turnstile> projval r c v : der c r"
 
       
   893 using assms
 
       
   894 apply(induct r arbitrary: v c rule: rexp.induct)
 
       
   895 apply(simp)
 
       
   896 apply(erule Prf.cases)
 
       
   897 apply(simp_all)[7]
 
       
   898 apply(erule Prf.cases)
 
       
   899 apply(simp_all)[7]
 
       
   900 apply(case_tac "char = c")
 
       
   901 apply(simp)
 
       
   902 apply(rule Prf.intros)
 
       
   903 apply(simp)
 
       
   904 apply(erule Prf.cases)
 
       
   905 apply(simp_all)[7]
 
       
   906 prefer 3
 
       
   907 proof -
 
       
   908   fix rexp v c vs
 
       
   909   assume ih: "\<And>v c. \<lbrakk>\<turnstile> v : rexp; head (flat v) = Some c\<rbrakk> \<Longrightarrow> \<turnstile> projval rexp c v : der c rexp"
 
       
   910   assume a: "head (flat (Stars vs)) = Some c"
 
       
   911   assume b: "\<turnstile> Stars vs : STAR rexp"
 
       
   912   have c: "first (Stars vs) = Some c \<Longrightarrow> \<turnstile> (hd vs) : rexp \<Longrightarrow> \<turnstile> projval rexp c (hd vs) : der c rexp"
 
       
   913     using b
 
       
   914     apply(induct arbitrary: rule: Prf.induct) 
       
   915     apply(simp_all)
 
       
   916     apply(case_tac "\<exists>c. first v = Some c")
 
       
   917     apply(auto)[1]
 
       
   918     apply(rule ih)
 
       
   919     apply(simp)
 
       
   920     apply (metis append_Nil2 first)
 
       
   921     apply(auto)[1]
 
       
   922     apply(simp)
 
       
   923     apply(auto split: if_splits)[1]
 
       
   924 apply (metis append_Nil2 first ih)
 
       
   925     apply(drule_tac x="v" in meta_spec)
 
       
   926     apply(simp)
 
       
   927     apply(rotate_tac 1)
 
       
   928     apply(erule Prf.cases)
 
       
   929     apply(simp_all)[7]
 
       
   930     apply(drule_tac x="v" in meta_spec)
 
       
   931     apply(simp)
 
       
   932     using a
 
       
   933     apply(rotate_tac 1)
 
       
   934     apply(erule Prf.cases)
 
       
   935     apply(simp_all)[7]
 
       
   936 
       
   937 
       
   938 apply (metis (full_types) Prf.cases Prf.simps a b flat.simps(6) head.simps(1) list.distinct(1) list.inject option.distinct(1) rexp.distinct(17) rexp.distinct(23) rexp.distinct(27) rexp.distinct(29) val.distinct(17) val.distinct(27) val.distinct(29) val.inject(5))
 
       
   939     
       
   940     apply(auto)[1]
 
       
   941     apply(case_tac "\<exists>c. first a = Some c")
 
       
   942     apply(auto)[1]
 
       
   943     apply(rule ih)
 
       
   944     apply(simp)
 
       
   945 apply (metis append_Nil2 first ih)
 
       
   946     apply(auto)[1]
 
       
   947     apply(case_tac "\<exists>c. first a = Some c")
 
       
   948     apply(auto)[1]
 
       
   949     apply(rule ih)
 
       
   950     apply(simp)
 
       
   951     apply(auto)[1]
 
       
   952     
       
   953     apply(erule Prf.cases)
 
       
   954     apply(simp_all)[7]
 
       
   955 apply (metis append_Nil2 first)
 
       
   956     apply(simp)
 
       
   957     apply(simp add: )
 
       
   958     apply(simp add: flat)
 
       
   959     apply(erule Prf.cases)
 
       
   960     apply(simp_all)[7]
 
       
   961     apply(rule Prf.intros)
 
       
   962       *)
 
       
   963   show "\<turnstile> projval (STAR rexp) c (Stars vs) : SEQ (der c rexp) (STAR rexp)"
 
       
   964     using b a
 
       
   965     apply -
 
       
   966     apply(erule Prf.cases)
 
       
   967     apply(simp_all)[7]
 
       
   968     apply(drule head1)
 
       
   969     apply(auto)
 
       
   970     apply(rule Prf.intros)
 
       
   971     apply(rule ih)
 
       
   972     apply(simp_all)[3]
 
       
   973     using k
 
       
   974     apply -
 
       
   975     apply(rule Prf.intros)
 
       
   976     apply(auto)
 
       
   977 
       
   978 apply(simp)
 
       
   979 apply(erule Prf.cases)
 
       
   980 apply(simp_all)[7]
 
       
   981 apply(rule Prf.intros)
 
       
   982 defer
 
       
   983 apply(rotate_tac 1)
 
       
   984 apply(erule Prf.cases)
 
       
   985 apply(simp_all)[7]
 
       
   986 apply(drule_tac meta_mp)
 
       
   987 apply(erule Prf.cases)
 
       
   988 apply(simp_all)[7]
 
       
   989 apply(rule ih)
 
       
   990 apply(case_tac vs)
 
       
   991 apply(simp)
 
       
   992 apply(simp)
 
       
   993 apply(rotate_tac 3)
 
       
   994 apply(erule Prf.cases)
 
       
   995 apply(simp_all)[7]
 
       
   996 apply(auto)[1]
 
       
   997 apply (metis Prf.intros(1) Prf.intros(3))
 
       
   998 apply(simp)
 
       
   999 
       
  1000 apply(drule head1)
 
       
  1001 apply(auto)[1]
 
       
  1002 apply (metis Prf.intros(3))
 
       
  1003 
       
  1004 
       
  1005 apply (metis Prf.intros)
 
       
  1006 apply(case_tac "nullable r1")
 
       
  1007 apply(simp)
 
       
  1008 apply(erule Prf.cases)
 
       
  1009 apply(simp_all)[7]
 
       
  1010 apply(auto)[1]
 
       
  1011 apply (metis Prf.intros(5))
 
       
  1012 apply (metis Prf.intros(3) Prf.intros(4) head1)
 
       
  1013 apply(simp)
 
       
  1014 apply(erule Prf.cases)
 
       
  1015 apply(simp_all)[7]
 
       
  1016 apply(auto)[1]
 
       
  1017 apply (metis nullable_correctness v1)
 
       
  1018 apply(drule head1)
 
       
  1019 apply(auto)[1]
 
       
  1020 apply (metis Prf.intros(3))
 
       
  1021 apply(simp)
 
       
  1022 apply(erule Prf.cases)
 
       
  1023 apply(simp_all)[7]
 
       
  1024 apply(auto)[1]
 
       
  1025 apply(drule head1)
 
       
  1026 apply(auto)[1]
 
       
  1027 apply(rule Prf.intros)
 
       
  1028 apply(auto)
 
       
  1029 apply(rule Prf.intros)
 
       
  1030 apply(auto)
 
       
  1031 apply(rotate_tac 2)
 
       
  1032 apply(erule Prf.cases)
 
       
  1033 apply(simp_all)[7]
 
       
  1034 apply(auto)
 
       
  1035 apply(drule head1)
 
       
  1036 apply(auto)
 
       
  1037 apply(rule Prf.intros)
 
       
  1038 apply(auto)
 
       
  1039 apply(rule Prf.intros)
 
       
  1040 apply(auto)
 
       
  1041 
       
  1042 defer
 
       
  1043 apply(erule Prf.cases)
 
       
  1044 apply(simp_all)[7]
 
       
  1045 apply(auto)[1]
 
       
  1046 apply(rule Prf.intros)
 
       
  1047 apply(auto)
 
       
  1048 apply(drule head1)
 
       
  1049 apply(auto)[1]
 
       
  1050 defer
 
       
  1051 apply(rotate_tac 3)
 
       
  1052 apply(erule Prf.cases)
 
       
  1053 apply(simp_all)[7]
 
       
  1054 apply(auto)
 
       
  1055 apply(drule head1)
 
       
  1056 apply(auto)[1]
 
       
  1057 
       
  1058 apply(simp)
 
       
  1059 apply(rule Prf.intros)
 
       
  1060 apply(auto)
 
       
  1061 apply(drule_tac x="v" in meta_spec)
 
       
  1062 apply(simp)
 
       
  1063 apply(erule Prf.cases)
 
       
  1064 apply(simp_all)[7]
 
       
  1065 apply(auto)[1]
 
       
  1066 apply(drule head1)
 
       
  1067 apply(auto)[1]
 
       
  1068 apply(rule Prf.intros)
 
       
  1069 apply(auto)
 
       
  1070 apply(drule meta_mp)
 
       
  1071 apply(rule Prf.intros)
 
       
  1072 apply(auto)
 
       
  1073 
       
  1074 apply(simp)
 
       
  1075 apply (metis Prf.intros(3) head1)
 
       
  1076 
       
  1077 defer
 
       
  1078 apply(simp)
 
       
  1079 apply(drule_tac head1)
 
       
  1080 apply(auto)[1]
 
       
  1081 apply(rule Prf.intros)
 
       
  1082 apply(rule Prf.intros)
 
       
  1083 apply(simp)
 
       
  1084 apply(simp)
 
       
  1085 apply(rule Prf.intros)
 
       
  1086 apply(simp)
 
       
  1087 apply(simp)
 
       
  1088 apply(rule Prf.intros)
 
       
  1089 apply(simp)
 
       
  1090 apply (metis nullable_correctness v1)
 
       
  1091 apply(simp)
 
       
  1092 apply(rule Prf.intros)
 
       
  1093 apply(simp)
 
       
  1094 apply(simp)
 
       
  1095 apply(rule Prf.intros)
 
       
  1096 apply(simp)
 
       
  1097 apply(simp)
 
       
  1098 apply(simp)
 
       
  1099 apply(rule Prf.intros)
 
       
  1100 apply(drule_tac head1)
 
       
  1101 apply(auto)[1]
 
       
  1102 apply (metis Prf.intros(3))
 
       
  1103 apply(rotate_tac 2)
 
       
  1104 apply(erule Prf.cases)
 
       
  1105 apply(simp_all)[7]
 
       
  1106 apply(auto)[1]
 
       
  1107 apply(rule Prf.intros)
 
       
  1108 defer
 
       
  1109 apply(drule_tac x="c" in meta_spec)
 
       
  1110 apply(simp)
 
       
  1111 apply(rotate_tac 6)
 
       
  1112 apply(erule Prf.cases)
 
       
  1113 apply(simp_all)[7]
 
       
  1114 apply(auto)[1]
 
       
  1115 apply(rule Prf.intros)
 
       
  1116 apply(auto)[2]
 
       
  1117 apply(drule v1)
 
       
  1118 apply(simp)
 
       
  1119 apply(rule Prf.intros)
 
       
  1120 apply(simp add: nullable_correctness[symmetric])
 
       
  1121 apply(rotate_tac 1)
 
       
  1122 apply(erule Prf.cases)
 
       
  1123 apply(simp_all)[7]
 
       
  1124 apply(auto)[1]
 
       
  1125 apply(drule head1)
 
       
  1126 apply(auto)[1]
 
       
  1127 apply(rule Prf.intros)
 
       
  1128 apply(simp)
 
       
  1129 apply(simp)
 
       
  1130 apply(simp)
 
       
  1131 
       
  1132 lemma inj_proj_id:
 
       
  1133   assumes "\<turnstile> v : r" "head (flat v) = Some c" 
       
  1134   shows "injval r c (projval r c v) = v"
 
       
  1135 using assms
 
       
  1136 apply(induct arbitrary: c rule: Prf.induct)
 
       
  1137 apply(simp)
 
       
  1138 apply(simp)
 
       
  1139 apply(drule head1)
 
       
  1140 apply(auto)[1]
 
       
  1141 apply(rotate_tac 2)
 
       
  1142 apply(erule Prf.cases)
 
       
  1143 apply(simp_all)[7]
 
       
  1144 apply(auto)[1]
 
       
  1145 apply(drule head1)
 
       
  1146 apply(auto)[1]
 
       
  1147 apply(simp)
 
       
  1148 apply(erule Prf.cases)
 
       
  1149 apply(simp_all)[7]
 
       
  1150 apply(simp)
 
       
  1151 apply(case_tac "ca = c'")
 
       
  1152 apply(simp)
 
       
  1153 apply(erule Prf.cases)
 
       
  1154 apply(simp_all)[7]
 
       
  1155 apply(simp)
 
       
  1156 apply(erule Prf.cases)
 
       
  1157 apply(simp_all)[7]
 
       
  1158 defer
 
       
  1159 apply(simp)
 
       
  1160 apply(case_tac "nullable r1")
 
       
  1161 apply(simp)
 
       
  1162 apply(erule Prf.cases)
 
       
  1163 apply(simp_all)[7]
 
       
  1164 apply(auto)[1]
 
       
  1165 apply(erule Prf.cases)
 
       
  1166 apply(simp_all)[7]
 
       
  1167 apply(auto)[1]
 
       
  1168 apply(rotate_tac 2)
 
       
  1169 apply(erule Prf.cases)
 
       
  1170 apply(simp_all)[7]
 
       
  1171 apply(simp)
 
       
  1172 apply(case_tac "nullable rexp1")
 
       
  1173 apply(simp)
 
       
  1174 apply(erule Prf.cases)
 
       
  1175 apply(simp_all)[7]
 
       
  1176 apply(auto)[1]
 
       
  1177 apply(erule Prf.cases)
 
       
  1178 apply(simp_all)[7]
 
       
  1179 apply(auto)[1]
 
       
  1180 apply(simp add: v4)
 
       
  1181 apply(auto)[1]
 
       
  1182 apply(simp add: v2a)
 
       
  1183 apply(simp only: der.simps)
 
       
  1184 apply(simp)
 
       
  1185 apply(erule Prf.cases)
 
       
  1186 apply(simp_all)[7]
 
       
  1187 apply(auto)[1]
 
       
  1188 apply(simp add: v4)
 
       
  1189 done
 
       
  1190 
       
  1191 
       
  1192 
       
  1193 lemma POSIX_I:
 
       
  1194   assumes "\<turnstile> v : r" "\<And>v'.  \<turnstile> v' : r \<Longrightarrow> flat v = flat v' \<Longrightarrow> v \<succeq>r v'"
 
       
  1195   shows "POSIX v r"
 
       
  1196 using assms
 
       
  1197 unfolding POSIX_def
 
       
  1198 apply(auto)
 
       
  1199 done
 
       
  1200 
       
  1201 lemma DISJ:
 
       
  1202   "(\<not> A \<Longrightarrow> B) \<Longrightarrow> A \<or> B"
 
       
  1203 by metis
 
       
  1204 
       
  1205 lemma DISJ2:
 
       
  1206   "\<not>(A \<and> B) \<longleftrightarrow> \<not>A \<or> \<not>B"
 
       
  1207 by metis
 
       
  1208  
       
  1209 lemma APP: "xs @ [] = xs" by simp
 
       
  1210 
       
  1211 lemma v5:
 
       
  1212   assumes "POSIX v (der c r)"
 
       
  1213   shows "POSIX (injval r c v) r"
 
       
  1214 using assms
 
       
  1215 apply(induct arbitrary: v rule: der.induct)
 
       
  1216 apply(simp)
 
       
  1217 apply(auto simp add: POSIX_def)[1]
 
       
  1218 apply(erule Prf.cases)
 
       
  1219 apply(simp_all)[7]
 
       
  1220 apply(erule Prf.cases)
 
       
  1221 apply(simp_all)[7]
 
       
  1222 apply(auto simp add: POSIX_def)[1]
 
       
  1223 apply(erule Prf.cases)
 
       
  1224 apply(simp_all)[7]
 
       
  1225 apply(erule Prf.cases)
 
       
  1226 apply(simp_all)[7]
 
       
  1227 apply(case_tac "c = c'")
 
       
  1228 apply(auto simp add: POSIX_def)[1]
 
       
  1229 apply(erule Prf.cases)
 
       
  1230 apply(simp_all)[7]
 
       
  1231 apply(rule Prf.intros)
 
       
  1232 apply(erule Prf.cases)
 
       
  1233 apply(simp_all)[7]
 
       
  1234 apply(simp add: ValOrd_eq_def)
 
       
  1235 apply(erule Prf.cases)
 
       
  1236 apply(simp_all)[7]
 
       
  1237 apply(simp)
 
       
  1238 apply(auto simp add: POSIX_def)[1]
 
       
  1239 apply(erule Prf.cases)
 
       
  1240 apply(simp_all)[7]
 
       
  1241 apply(erule Prf.cases)
 
       
  1242 apply(simp_all)[7]
 
       
  1243 prefer 3
 
       
  1244 apply(simp)
 
       
  1245 apply(frule POSIX_E1)
 
       
  1246 apply(erule Prf.cases)
 
       
  1247 apply(simp_all)[7]
 
       
  1248 apply(auto)[1]
 
       
  1249 apply(drule_tac x="v1" in meta_spec)
 
       
  1250 apply(drule meta_mp)
 
       
  1251 apply(rule POSIX_I)
 
       
  1252 apply(simp)
 
       
  1253 apply(simp add: POSIX_def)
 
       
  1254 apply(auto)[1]
 
       
  1255 apply(drule_tac x="Seq v' v2" in spec)
 
       
  1256 apply(simp)
 
       
  1257 apply(drule mp)
 
       
  1258 apply (metis Prf.intros(3))
 
       
  1259 apply(simp add: ValOrd_eq_def)
 
       
  1260 apply(erule disjE)
 
       
  1261 apply(simp)
 
       
  1262 apply(erule ValOrd.cases)
 
       
  1263 apply(simp_all)[10]
 
       
  1264 apply(subgoal_tac "\<exists>vs2. v2 = Stars vs2")
 
       
  1265 prefer 2
 
       
  1266 apply(rotate_tac 2)
 
       
  1267 apply(erule Prf.cases)
 
       
  1268 apply(auto)[7]
 
       
  1269 apply(erule exE)
 
       
  1270 apply(clarify)
 
       
  1271 apply(simp only: injval.simps)
 
       
  1272 apply(case_tac "POSIX (Stars (injval r c v1 # vs2)) (STAR r)")
 
       
  1273 apply(simp)
 
       
  1274 apply(subgoal_tac "\<exists>v'' vs''. Stars (v''#vs'')  \<succ>(STAR r) Stars (injval r c v1 # vs2)")
 
       
  1275 apply(erule exE)+
 
       
  1276 apply(erule ValOrd.cases)
 
       
  1277 apply(simp_all)[8]
 
       
  1278 apply(auto)[1]
 
       
  1279 apply(subst (asm) (2) POSIX_def)
 
       
  1280 
       
  1281 
       
  1282 prefer 2
 
       
  1283 apply(subst (asm) (3) POSIX_def)
 
       
  1284 apply(simp)
 
       
  1285 apply(drule mp)
 
       
  1286 apply (metis Prf.intros(2) v3)
 
       
  1287 apply(erule exE)
 
       
  1288 apply(auto)[1]
 
       
  1289 
       
  1290 apply
 
       
  1291 apply(subgoal_tac "\<turnstile> Stars (injval r c v1 # vs2) : STAR r")
 
       
  1292 apply(simp)
 
       
  1293 apply(case_tac "flat () = []")
 
       
  1294 
       
  1295 apply(rule POSIX_I)
 
       
  1296 apply (metis POSIX_E1 der.simps(6) v3)
 
       
  1297 apply(rotate_tac 2)
 
       
  1298 apply(erule Prf.cases)
 
       
  1299 defer
 
       
  1300 defer
 
       
  1301 apply(simp_all)[5]
 
       
  1302 prefer 4
 
       
  1303 apply(clarify)
 
       
  1304 apply(simp only: v4 flat.simps injval.simps)
 
       
  1305 prefer 4
 
       
  1306 apply(clarify)
 
       
  1307 apply(simp only: v4 APP flat.simps injval.simps)
 
       
  1308 prefer 2
 
       
  1309 apply(erule Prf.cases)
 
       
  1310 apply(simp_all)[7]
 
       
  1311 apply(clarify)
 
       
  1312 
       
  1313 
       
  1314 apply(simp add: ValOrd_eq_def)
 
       
  1315 apply(subst (asm) POSIX_def)
 
       
  1316 apply(erule conjE)
 
       
  1317 apply(drule_tac x="va" in spec)
 
       
  1318 apply(simp)
 
       
  1319 apply(simp add: v4)
 
       
  1320 apply(simp add: ValOrd_eq_def)
 
       
  1321 apply(simp)
 
       
  1322 apply(rule disjI2)
 
       
  1323 apply(rule ValOrd.intros)
 
       
  1324 apply(rotate_tac 2)
 
       
  1325 apply(subst (asm) POSIX_def)
 
       
  1326 apply(simp)
 
       
  1327 apply(auto)[1]
 
       
  1328 apply(drule_tac x="v" in spec)
 
       
  1329 apply(simp)
 
       
  1330 apply(drule mp)
 
       
  1331 prefer 2
 
       
  1332 apply(simp add: ValOrd_eq_def)
 
       
  1333 apply(auto)[1]
 
       
  1334 
       
  1335 apply(case_tac "injval rb c v1 = v \<and> [] = vs")
 
       
  1336 apply(simp)
 
       
  1337 apply(simp only: DISJ2)
 
       
  1338 apply(rule disjI2)
 
       
  1339 apply(erule disjE)
 
       
  1340 
       
  1341 
       
  1342 apply(auto)[1]
 
       
  1343 apply (metis list.distinct(1) v4)
 
       
  1344 apply(auto)[1]
 
       
  1345 apply(simp add: ValOrd_eq_def)
 
       
  1346 apply(rule DISJ)
 
       
  1347 apply(simp only: DISJ2)
 
       
  1348 apply(erule disjE)
 
       
  1349 apply(rule ValOrd.intros)
 
       
  1350 apply(subst (asm) POSIX_def)
 
       
  1351 apply(auto)[1]
 
       
  1352 
       
  1353 apply (metis list.distinct(1) v4)
 
       
  1354 apply(subst (asm) POSIX_def)
 
       
  1355 apply(auto)[1]
 
       
  1356 apply(erule Prf.cases)
 
       
  1357 apply(simp_all)[7]
 
       
  1358 apply(rotate_tac 3)
 
       
  1359 apply(erule Prf.cases)
 
       
  1360 apply(simp_all)[7]
 
       
  1361 apply(auto)[1]
 
       
  1362 apply (metis list.distinct(1) v4)
 
       
  1363 apply (metis list.distinct(1) v4)
 
       
  1364 apply(clarify)
 
       
  1365 apply(rotate_tac 3)
 
       
  1366 apply(erule Prf.cases)
 
       
  1367 apply(simp_all)[7]
 
       
  1368 prefer 2
 
       
  1369 apply(clarify)
 
       
  1370 apply(simp add: ValOrd_eq_def)
 
       
  1371 apply(drule_tac x="Stars (v#vs)" in spec)
 
       
  1372 apply(drule mp)
 
       
  1373 apply(auto)[1]
 
       
  1374 
       
  1375 apply(simp add: ValOrd_eq_def)
 
       
  1376 
       
  1377 apply (metis POSIX_E1 der.simps(6) list.distinct(1) v4)
 
       
  1378 apply(rotate_tac 3)
 
       
  1379 apply(erule Prf.cases)
 
       
  1380 apply(simp_all)[7]
 
       
  1381 
       
  1382 apply(simp)
 
       
  1383 apply(case_tac v2)
 
       
  1384 apply(simp)
 
       
  1385 apply(simp (no_asm) POSIX_def)
 
       
  1386 apply(auto)[1]
 
       
  1387 apply(auto)[1]
 
       
  1388  
       
  1389 
       
  1390 apply (metis POSIX_E der.simps(6) v3)
 
       
  1391 
       
  1392 apply(rule Prf.intros)
 
       
  1393 apply(drule_tac x="v1" in meta_spec)
 
       
  1394 apply(drule meta_mp)
 
       
  1395 prefer 2
 
       
  1396 
       
  1397 apply(subgoal_tac "POSIX v1 (der c r)")
 
       
  1398 prefer 2
 
       
  1399 apply(simp add: POSIX_def)
 
       
  1400 apply(auto)[1]
 
       
  1401 apply(simp add: ValOrd_eq_def)
 
       
  1402 apply(auto)[1]
 
       
  1403 
       
  1404 
       
  1405 lemma v5:
 
       
  1406   assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
 
       
  1407   shows "POSIX (injval r c v) r"
 
       
  1408 using assms
 
       
  1409 apply(induct arbitrary: v rule: der.induct)
 
       
  1410 apply(simp)
 
       
  1411 apply(erule Prf.cases)
 
       
  1412 apply(simp_all)[7]
 
       
  1413 apply(simp)
 
       
  1414 apply(erule Prf.cases)
 
       
  1415 apply(simp_all)[7]
 
       
  1416 apply(simp)
 
       
  1417 apply(case_tac "c = c'")
 
       
  1418 apply(simp)
 
       
  1419 apply(erule Prf.cases)
 
       
  1420 apply(simp_all)[7]
 
       
  1421 apply(simp add: POSIX_def)
 
       
  1422 apply(auto)[1]
 
       
  1423 apply(rule Prf.intros)
 
       
  1424 apply(erule Prf.cases)
 
       
  1425 apply(simp_all)[7]
 
       
  1426 apply(simp add: ValOrd_eq_def)
 
       
  1427 apply(erule Prf.cases)
 
       
  1428 apply(simp_all)[7]
 
       
  1429 apply(simp)
 
       
  1430 apply(erule Prf.cases)
 
       
  1431 apply(simp_all)[7]
 
       
  1432 prefer 3
 
       
  1433 apply(simp)
 
       
  1434 apply(erule Prf.cases)
 
       
  1435 apply(simp_all)[7]
 
       
  1436 apply(auto)[1]
 
       
  1437 apply(case_tac "flat (Seq v1 v2) \<noteq> []")
 
       
  1438 apply(subgoal_tac "POSIX v1 (der c r)")
 
       
  1439 prefer 2
 
       
  1440 apply(simp add: POSIX_def)
 
       
  1441 apply(auto)[1]
 
       
  1442 
       
  1443 
       
  1444 apply(drule_tac x="v1" in meta_spec)
 
       
  1445 apply(simp)
 
       
  1446 apply(simp (no_asm) add: POSIX_def)
 
       
  1447 apply(auto)[1]
 
       
  1448 apply(rule v3)
 
       
  1449 apply (metis Prf.intros(3) der.simps(6))
 
       
  1450 apply(rotate_tac 1)
 
       
  1451 apply(erule Prf.cases)
 
       
  1452 apply(simp_all)[7]
 
       
  1453 apply(simp add: ValOrd_eq_def)
 
       
  1454 apply(rule disjI2)
 
       
  1455 apply(rotate_tac 1)
 
       
  1456 apply(erule Prf.cases)
 
       
  1457 apply(simp_all)[7]
 
       
  1458 apply(rule ValOrd.intros)
 
       
  1459 apply(simp)
 
       
  1460 apply (metis list.distinct(1) v4)
 
       
  1461 apply(rule ValOrd.intros)
 
       
  1462 apply(simp add: POSIX_def)
 
       
  1463 apply(auto)[1]
 
       
  1464 apply(rotate_tac 3)
 
       
  1465 apply(erule Prf.cases)
 
       
  1466 apply(simp_all)[7]
 
       
  1467 apply(simp add: ValOrd_eq_def)
 
       
  1468 apply(drule_tac x="v" in spec)
 
       
  1469 apply(simp)
 
       
  1470 apply(auto)[1]
 
       
  1471 apply(simp)
 
       
  1472 
       
  1473 apply(simp add: POSIX_def)
 
       
  1474 apply(auto)[1]
 
       
  1475 apply(
 
       
  1476 
       
  1477 apply(rotate_tac 1)
 
       
  1478 apply(erule Prf.cases)
 
       
  1479 apply(simp_all)[7]
 
       
  1480 apply (metis list.distinct(1) v4)
 
       
  1481 apply(rotate_tac 8)
 
       
  1482 apply(erule Prf.cases)
 
       
  1483 apply(simp_all)[7]
 
       
  1484 apply (metis POSIX_def ValOrd.intros(9) ValOrd_eq_def)
 
       
  1485 apply(simp add: ValOrd_eq_def)
 
       
  1486 apply(simp)
 
       
  1487 
       
  1488 apply(simp add: ValOrd_eq_def)
 
       
  1489 apply(simp add: POSIX_def)
 
       
  1490 apply(auto)[1]
 
       
  1491 
       
  1492 
       
  1493 apply(simp)
 
       
  1494 apply(simp add: ValOrd_eq_def)
 
       
  1495 apply(simp add: POSIX_def)
 
       
  1496 apply(erule conjE)+
 
       
  1497 apply(drule_tac x="Seq v1 v2" in spec)
 
       
  1498 apply(simp)
 
       
  1499 
       
  1500 
       
  1501 
       
  1502 apply(rotate_tac 2)
 
       
  1503 apply(erule Prf.cases)
 
       
  1504 apply(simp_all)[7]
 
       
  1505 apply(auto)[1]
 
       
  1506 apply(simp add: POSIX_def)
 
       
  1507 apply(auto)[1]
 
       
  1508 apply(rule Prf.intros)
 
       
  1509 apply(rule v3)
 
       
  1510 apply(simp)
 
       
  1511 apply(rotate_tac 5)
 
       
  1512 apply(erule Prf.cases)
 
       
  1513 apply(simp_all)[7]
 
       
  1514 apply(auto)[1]
 
       
  1515 apply(rotate_tac 4)
 
       
  1516 apply(erule Prf.cases)
 
       
  1517 apply(simp_all)[7]
 
       
  1518 apply(auto)[1]
 
       
  1519 apply(simp add: ValOrd_eq_def)
 
       
  1520 
       
  1521 apply(simp)
 
       
  1522 
       
  1523 
       
  1524 prefer 2
 
       
  1525 apply(auto)[1]
 
       
  1526 apply(subgoal_tac "POSIX v2 (der c r2)")
 
       
  1527 apply(rotate_tac 1)
 
       
  1528 apply(drule_tac x="v2" in meta_spec)
 
       
  1529 apply(simp)
 
       
  1530 apply(subgoal_tac "\<turnstile> Right (injval r2 c v2) : (ALT r1 r2)") 
       
  1531 prefer 2
 
       
  1532 apply (metis Prf.intros(5) v3)
 
       
  1533 apply(simp (no_asm) add: POSIX_def)
 
       
  1534 apply(auto)[1]
 
       
  1535 apply(rotate_tac 6)
 
       
  1536 apply(erule Prf.cases)
 
       
  1537 apply(simp_all)[7]
 
       
  1538 prefer 2
 
       
  1539 apply(auto)[1]
 
       
  1540 apply(simp add: ValOrd_eq_def)
 
       
  1541 apply (metis POSIX_def ValOrd.intros(5) ValOrd_eq_def)
 
       
  1542 apply(auto)[1]
 
       
  1543 apply(simp add: ValOrd_eq_def)
 
       
  1544 
       
  1545 
       
  1546 section {* Correctness Proof of the Matcher *}
 
       
  1547 
       
  1548 
       
  1549 section {* Left-Quotient of a Set *}
 
       
  1550 
       
  1551 fun
 
       
  1552  zeroable :: "rexp \<Rightarrow> bool"
 
       
  1553 where
 
       
  1554   "zeroable (NULL) = True"
 
       
  1555 | "zeroable (EMPTY) = False"
 
       
  1556 | "zeroable (CHAR c) = False"
 
       
  1557 | "zeroable (ALT r1 r2) = (zeroable r1 \<and> zeroable r2)"
 
       
  1558 | "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)"
 
       
  1559 | "zeroable (STAR r) = False"
 
       
  1560 
       
  1561 
       
  1562 lemma zeroable_correctness:
 
       
  1563   shows "zeroable r  \<longleftrightarrow>  (L r = {})"
 
       
  1564 apply(induct r)
 
       
  1565 apply(auto simp add: Seq_def)[6]
 
       
  1566 done
 
       
  1567 
       
  1568 section {* Left-Quotient of a Set *}
 
       
  1569 
       
  1570 definition
 
       
  1571   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
 
       
  1572 where
 
       
  1573   "Der c A \<equiv> {s. [c] @ s \<in> A}"
 
       
  1574 
       
  1575 lemma Der_null [simp]:
 
       
  1576   shows "Der c {} = {}"
 
       
  1577 unfolding Der_def
 
       
  1578 by auto
 
       
  1579 
       
  1580 lemma Der_empty [simp]:
 
       
  1581   shows "Der c {[]} = {}"
 
       
  1582 unfolding Der_def
 
       
  1583 by auto
 
       
  1584 
       
  1585 lemma Der_char [simp]:
 
       
  1586   shows "Der c {[d]} = (if c = d then {[]} else {})"
 
       
  1587 unfolding Der_def
 
       
  1588 by auto
 
       
  1589 
       
  1590 lemma Der_union [simp]:
 
       
  1591   shows "Der c (A \<union> B) = Der c A \<union> Der c B"
 
       
  1592 unfolding Der_def
 
       
  1593 by auto
 
       
  1594 
       
  1595 lemma Der_seq [simp]:
 
       
  1596   shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
 
       
  1597 unfolding Der_def Seq_def
 
       
  1598 by (auto simp add: Cons_eq_append_conv)
 
       
  1599 
       
  1600 lemma Der_star [simp]:
 
       
  1601   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
 
       
  1602 proof -    
       
  1603   have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"
 
       
  1604     by (simp only: star_cases[symmetric])
 
       
  1605   also have "... = Der c (A ;; A\<star>)"
 
       
  1606     by (simp only: Der_union Der_empty) (simp)
 
       
  1607   also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"
 
       
  1608     by simp
 
       
  1609   also have "... =  (Der c A) ;; A\<star>"
 
       
  1610     unfolding Seq_def Der_def
 
       
  1611     by (auto dest: star_decomp)
 
       
  1612   finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
 
       
  1613 qed
 
       
  1614 
       
  1615 
       
  1616 lemma der_correctness:
 
       
  1617   shows "L (der c r) = Der c (L r)"
 
       
  1618 by (induct r) 
       
  1619    (simp_all add: nullable_correctness)
 
       
  1620 
       
  1621 lemma matcher_correctness:
 
       
  1622   shows "matcher r s \<longleftrightarrow> s \<in> L r"
 
       
  1623 by (induct s arbitrary: r)
 
       
  1624    (simp_all add: nullable_correctness der_correctness Der_def)
 
       
  1625 
       
  1626 section {* Examples *}
 
       
  1627 
       
  1628 definition 
       
  1629   "CHRA \<equiv> CHAR (CHR ''a'')"
 
       
  1630 
       
  1631 definition 
       
  1632   "ALT1 \<equiv> ALT CHRA EMPTY"
 
       
  1633 
       
  1634 definition 
       
  1635   "SEQ3 \<equiv> SEQ (SEQ ALT1 ALT1) ALT1"
 
       
  1636 
       
  1637 value "matcher SEQ3 ''aaa''"
 
       
  1638 
       
  1639 value "matcher NULL []"
 
       
  1640 value "matcher (CHAR (CHR ''a'')) [CHR ''a'']"
 
       
  1641 value "matcher (CHAR a) [a,a]"
 
       
  1642 value "matcher (STAR (CHAR a)) []"
 
       
  1643 value "matcher (STAR (CHAR a))  [a,a]"
 
       
  1644 value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbbbc''"
 
       
  1645 value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbcbbc''"
 
       
  1646 
       
  1647 section {* Incorrect Matcher - fun-definition rejected *}
 
       
  1648 
       
  1649 fun
 
       
  1650   match :: "rexp list \<Rightarrow> string \<Rightarrow> bool"
 
       
  1651 where
 
       
  1652   "match [] [] = True"
 
       
  1653 | "match [] (c # s) = False"
 
       
  1654 | "match (NULL # rs) s = False"  
       
  1655 | "match (EMPTY # rs) s = match rs s"
 
       
  1656 | "match (CHAR c # rs) [] = False"
 
       
  1657 | "match (CHAR c # rs) (d # s) = (if c = d then match rs s else False)"         
       
  1658 | "match (ALT r1 r2 # rs) s = (match (r1 # rs) s \<or> match (r2 # rs) s)" 
       
  1659 | "match (SEQ r1 r2 # rs) s = match (r1 # r2 # rs) s"
 
       
  1660 | "match (STAR r # rs) s = (match rs s \<or> match (r # (STAR r) # rs) s)"
 
       
  1661 
       
  1662 
       
  1663 end
lexing