1    

     2 theory Re

     3   imports "Main" 

     4 begin

     5 

     6 

     7 section {* Sequential Composition of Sets *}

     8 

     9 definition

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

    11 where 

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

    13 

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

    15 

    16 lemma seq_empty [simp]:

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

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

    19 by (simp_all add: Sequ_def)

    20 

    21 lemma seq_null [simp]:

    22   shows "A ;; {} = {}"

    23   and   "{} ;; A = {}"

    24 by (simp_all add: Sequ_def)

    25 

    26 section {* Regular Expressions *}

    27 

    28 datatype rexp =

    29   NULL

    30 | EMPTY

    31 | CHAR char

    32 | SEQ rexp rexp

    33 | ALT rexp rexp

    34 

    35 section {* Semantics of Regular Expressions *}

    36  

    37 fun

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

    39 where

    40   "L (NULL) = {}"

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

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

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

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

    45 

    46 fun

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

    48 where

    49   "nullable (NULL) = False"

    50 | "nullable (EMPTY) = True"

    51 | "nullable (CHAR c) = False"

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

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

    54 

    55 lemma nullable_correctness:

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

    57 apply (induct r) 

    58 apply(auto simp add: Sequ_def) 

    59 done

    60 

    61 section {* Values *}

    62 

    63 datatype val = 

    64   Void

    65 | Char char

    66 | Seq val val

    67 | Right val

    68 | Left val

    69 

    70 section {* The string behind a value *}

    71 

    72 fun 

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

    74 where

    75   "flat(Void) = []"

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

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

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

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

    80 

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

    82 

    83 inductive 

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

    85 where

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

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

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

    89 | "\<turnstile> Void : EMPTY"

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

    91 

    92 lemma not_nullable_flat:

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

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

    95 using assms

    96 apply(induct)

    97 apply(auto)

    98 done

    99 

   100 lemma Prf_flat_L:

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

   102 using assms

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

   104 apply(auto simp add: Sequ_def)

   105 done

   106 

   107 lemma L_flat_Prf:

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

   109 apply(induct r)

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

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

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

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

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

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

   116 apply(erule Prf.cases)

   117 apply(auto)

   118 done

   119 

   120 section {* Greedy Ordering according to Frisch/Cardelli *}

   121 

   122 inductive 

   123   GrOrd :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ gr\<succ> _")

   124 where 

   125   "v1 gr\<succ> v1' \<Longrightarrow> (Seq v1 v2) gr\<succ> (Seq v1' v2')"

   126 | "v2 gr\<succ> v2' \<Longrightarrow> (Seq v1 v2) gr\<succ> (Seq v1 v2')"

   127 | "v1 gr\<succ> v2 \<Longrightarrow> (Left v1) gr\<succ> (Left v2)"

   128 | "v1 gr\<succ> v2 \<Longrightarrow> (Right v1) gr\<succ> (Right v2)"

   129 | "(Left v2) gr\<succ>(Right v1)"

   130 | "(Char c) gr\<succ> (Char c)"

   131 | "(Void) gr\<succ> (Void)"

   132 

   133 lemma Gr_refl:

   134   assumes "\<turnstile> v : r"

   135   shows "v gr\<succ> v"

   136 using assms

   137 apply(induct)

   138 apply(auto intro: GrOrd.intros)

   139 done

   140 

   141 lemma Gr_total:

   142   assumes "\<turnstile> v1 : r" "\<turnstile> v2 : r"

   143   shows "v1 gr\<succ> v2 \<or> v2 gr\<succ> v1"

   144 using assms

   145 apply(induct v1 r arbitrary: v2 rule: Prf.induct)

   146 apply(rotate_tac 4)

   147 apply(erule Prf.cases)

   148 apply(simp_all)[5]

   149 apply(clarify)

   150 apply (metis GrOrd.intros(1) GrOrd.intros(2))

   151 apply(rotate_tac 2)

   152 apply(erule Prf.cases)

   153 apply(simp_all)

   154 apply(clarify)

   155 apply (metis GrOrd.intros(3))

   156 apply(clarify)

   157 apply (metis GrOrd.intros(5))

   158 apply(rotate_tac 2)

   159 apply(erule Prf.cases)

   160 apply(simp_all)

   161 apply(clarify)

   162 apply (metis GrOrd.intros(5))

   163 apply(clarify)

   164 apply (metis GrOrd.intros(4))

   165 apply(erule Prf.cases)

   166 apply(simp_all)

   167 apply (metis GrOrd.intros(7))

   168 apply(erule Prf.cases)

   169 apply(simp_all)

   170 apply (metis GrOrd.intros(6))

   171 done

   172 

   173 lemma Gr_trans: 

   174   assumes "v1 gr\<succ> v2" "v2 gr\<succ> v3" 

   175   and     "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<turnstile> v3 : r"

   176   shows "v1 gr\<succ> v3"

   177 using assms

   178 apply(induct r arbitrary: v1 v2 v3)

   179 apply(erule Prf.cases)

   180 apply(simp_all)[5]

   181 apply(erule Prf.cases)

   182 apply(simp_all)[5]

   183 apply(erule Prf.cases)

   184 apply(simp_all)[5]

   185 apply(erule Prf.cases)

   186 apply(simp_all)[5]

   187 apply(erule Prf.cases)

   188 apply(simp_all)[5]

   189 defer

   190 (* ALT case *)

   191 apply(erule Prf.cases)

   192 apply(simp_all (no_asm_use))[5]

   193 apply(erule Prf.cases)

   194 apply(simp_all (no_asm_use))[5]

   195 apply(erule Prf.cases)

   196 apply(simp_all (no_asm_use))[5]

   197 apply(clarify)

   198 apply(erule GrOrd.cases)

   199 apply(simp_all (no_asm_use))[7]

   200 apply(erule GrOrd.cases)

   201 apply(simp_all (no_asm_use))[7]

   202 apply (metis GrOrd.intros(3))

   203 apply(clarify)

   204 apply(erule GrOrd.cases)

   205 apply(simp_all (no_asm_use))[7]

   206 apply(erule GrOrd.cases)

   207 apply(simp_all (no_asm_use))[7]

   208 apply (metis GrOrd.intros(5))

   209 apply(erule Prf.cases)

   210 apply(simp_all (no_asm_use))[5]

   211 apply(clarify)

   212 apply(erule GrOrd.cases)

   213 apply(simp_all (no_asm_use))[7]

   214 apply(erule GrOrd.cases)

   215 apply(simp_all (no_asm_use))[7]

   216 apply (metis GrOrd.intros(5))

   217 apply(erule Prf.cases)

   218 apply(simp_all (no_asm_use))[5]

   219 apply(erule Prf.cases)

   220 apply(simp_all (no_asm_use))[5]

   221 apply(clarify)

   222 apply(erule GrOrd.cases)

   223 apply(simp_all (no_asm_use))[7]

   224 apply(clarify)

   225 apply(erule GrOrd.cases)

   226 apply(simp_all (no_asm_use))[7]

   227 apply(erule Prf.cases)

   228 apply(simp_all (no_asm_use))[5]

   229 apply(clarify)

   230 apply(erule GrOrd.cases)

   231 apply(simp_all (no_asm_use))[7]

   232 apply(erule GrOrd.cases)

   233 apply(simp_all (no_asm_use))[7]

   234 apply(clarify)

   235 apply(erule GrOrd.cases)

   236 apply(simp_all (no_asm_use))[7]

   237 apply(erule GrOrd.cases)

   238 apply(simp_all (no_asm_use))[7]

   239 apply (metis GrOrd.intros(4))

   240 (* SEQ case *)

   241 apply(erule Prf.cases)

   242 apply(simp_all (no_asm_use))[5]

   243 apply(erule Prf.cases)

   244 apply(simp_all (no_asm_use))[5]

   245 apply(erule Prf.cases)

   246 apply(simp_all (no_asm_use))[5]

   247 apply(clarify)

   248 apply(erule GrOrd.cases)

   249 apply(simp_all (no_asm_use))[7]

   250 apply(erule GrOrd.cases)

   251 apply(simp_all (no_asm_use))[7]

   252 apply(clarify)

   253 apply (metis GrOrd.intros(1))

   254 apply (metis GrOrd.intros(1))

   255 apply(erule GrOrd.cases)

   256 apply(simp_all (no_asm_use))[7]

   257 apply (metis GrOrd.intros(1))

   258 by (metis GrOrd.intros(1) Gr_refl)

   259 

   260 

   261 section {* Values Sets *}

   262 

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

   264 where

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

   266 

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

   268 where

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

   270 

   271 lemma length_sprefix:

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

   273 unfolding sprefix_def prefix_def

   274 by (auto)

   275 

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

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

   278 

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

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

   281 

   282 lemma Suffixes_in: 

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

   284 unfolding Suffixes_def Prefixes_def prefix_def image_def

   285 apply(auto)

   286 by (metis rev_rev_ident)

   287 

   288 lemma Prefixes_Cons:

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

   290 unfolding Prefixes_def prefix_def

   291 apply(auto simp add: append_eq_Cons_conv) 

   292 done

   293 

   294 lemma finite_Prefixes:

   295   "finite (Prefixes s)"

   296 apply(induct s)

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

   298 apply(simp add: Prefixes_Cons)

   299 done

   300 

   301 lemma finite_Suffixes:

   302   "finite (Suffixes s)"

   303 unfolding Suffixes_def

   304 apply(rule finite_imageI)

   305 apply(rule finite_Prefixes)

   306 done

   307 

   308 lemma prefix_Cons:

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

   310 apply(auto simp add: prefix_def)

   311 done

   312 

   313 lemma prefix_append:

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

   315 apply(induct s)

   316 apply(simp)

   317 apply(simp add: prefix_Cons)

   318 done

   319 

   320 

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

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

   323 

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

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

   326 

   327 lemma rest_flat:

   328   assumes "flat v1 \<sqsubseteq> s"

   329   shows "flat v1 @ rest v1 s = s"

   330 using assms

   331 apply(auto simp add: rest_def prefix_def)

   332 done

   333 

   334 

   335 lemma rest_Suffixes:

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

   337 unfolding rest_def

   338 by (metis Suffixes_in append_take_drop_id)

   339 

   340 

   341 lemma Values_recs:

   342   "Values (NULL) s = {}"

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

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

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

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

   347 unfolding Values_def

   348 apply(auto)

   349 (*NULL*)

   350 apply(erule Prf.cases)

   351 apply(simp_all)[5]

   352 (*EMPTY*)

   353 apply(erule Prf.cases)

   354 apply(simp_all)[5]

   355 apply(rule Prf.intros)

   356 apply (metis append_Nil prefix_def)

   357 (*CHAR*)

   358 apply(erule Prf.cases)

   359 apply(simp_all)[5]

   360 apply(rule Prf.intros)

   361 apply(erule Prf.cases)

   362 apply(simp_all)[5]

   363 (*ALT*)

   364 apply(erule Prf.cases)

   365 apply(simp_all)[5]

   366 apply (metis Prf.intros(2))

   367 apply (metis Prf.intros(3))

   368 (*SEQ*)

   369 apply(erule Prf.cases)

   370 apply(simp_all)[5]

   371 apply (simp add: append_eq_conv_conj prefix_def rest_def)

   372 apply (metis Prf.intros(1))

   373 apply (simp add: append_eq_conv_conj prefix_def rest_def)

   374 done

   375 

   376 lemma Values_finite:

   377   "finite (Values r s)"

   378 apply(induct r arbitrary: s)

   379 apply(simp_all add: Values_recs)

   380 thm finite_surj

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

   382                A="{(v1, v2) | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}" in finite_surj)

   383 prefer 2

   384 apply(auto)[1]

   385 apply(rule_tac B="\<Union>sp \<in> Suffixes s. {(v1, v2). v1 \<in> Values r1 s \<and> v2 \<in> Values r2 sp}" in finite_subset)

   386 apply(auto)[1]

   387 apply (metis rest_Suffixes)

   388 apply(rule finite_UN_I)

   389 apply(rule finite_Suffixes)

   390 apply(simp)

   391 done

   392 

   393 section {* Sulzmann functions *}

   394 

   395 fun 

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

   397 where

   398   "mkeps(EMPTY) = Void"

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

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

   401 

   402 section {* Derivatives *}

   403 

   404 fun

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

   406 where

   407   "der c (NULL) = NULL"

   408 | "der c (EMPTY) = NULL"

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

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

   411 | "der c (SEQ r1 r2) = 

   412      (if nullable r1

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

   414       else SEQ (der c r1) r2)"

   415 

   416 fun 

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

   418 where

   419   "ders [] r = r"

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

   421 

   422 

   423 section {* Injection function *}

   424 

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

   426 where

   427   "injval (EMPTY) c Void = Char c"

   428 | "injval (CHAR d) c Void = Char d"

   429 | "injval (CHAR d) c (Char c') = Seq (Char d) (Char c')"

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

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

   432 | "injval (SEQ r1 r2) c (Char c') = Seq (Char c) (Char c')"

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

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

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

   436 

   437 fun 

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

   439 where

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

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

   442                     None \<Rightarrow> None

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

   444 

   445 fun 

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

   447 where

   448   "lex2 r [] = mkeps r"

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

   450 

   451 

   452 section {* Projection function *}

   453 

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

   455 where

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

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

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

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

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

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

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

   463 

   464 

   465 

   466 lemma mkeps_nullable:

   467   assumes "nullable(r)" 

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

   469 using assms

   470 apply(induct rule: nullable.induct)

   471 apply(auto intro: Prf.intros)

   472 done

   473 

   474 lemma mkeps_flat:

   475   assumes "nullable(r)" 

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

   477 using assms

   478 apply(induct rule: nullable.induct)

   479 apply(auto)

   480 done

   481 

   482 lemma v3:

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

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

   485 using assms

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

   487 apply(simp)

   488 apply(erule Prf.cases)

   489 apply(simp_all)[5]

   490 apply(simp)

   491 apply(erule Prf.cases)

   492 apply(simp_all)[5]

   493 apply(case_tac "c = c'")

   494 apply(simp)

   495 apply(erule Prf.cases)

   496 apply(simp_all)[5]

   497 apply (metis Prf.intros(5))

   498 apply(simp)

   499 apply(erule Prf.cases)

   500 apply(simp_all)[5]

   501 apply(simp)

   502 apply(erule Prf.cases)

   503 apply(simp_all)[5]

   504 apply (metis Prf.intros(2))

   505 apply (metis Prf.intros(3))

   506 apply(simp)

   507 apply(case_tac "nullable r1")

   508 apply(simp)

   509 apply(erule Prf.cases)

   510 apply(simp_all)[5]

   511 apply(auto)[1]

   512 apply(erule Prf.cases)

   513 apply(simp_all)[5]

   514 apply(auto)[1]

   515 apply (metis Prf.intros(1))

   516 apply(auto)[1]

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

   518 apply(simp)

   519 apply(erule Prf.cases)

   520 apply(simp_all)[5]

   521 apply(auto)[1]

   522 apply(rule Prf.intros)

   523 apply(auto)[2]

   524 done

   525 

   526 lemma v3_proj:

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

   528   shows "\<turnstile> (projval r c v) : der c r"

   529 using assms

   530 apply(induct rule: Prf.induct)

   531 prefer 4

   532 apply(simp)

   533 prefer 4

   534 apply(simp)

   535 apply (metis Prf.intros(4))

   536 prefer 2

   537 apply(simp)

   538 apply (metis Prf.intros(2))

   539 prefer 2

   540 apply(simp)

   541 apply (metis Prf.intros(3))

   542 apply(auto)

   543 apply(rule Prf.intros)

   544 apply(simp)

   545 apply (metis Prf_flat_L nullable_correctness)

   546 apply(rule Prf.intros)

   547 apply(rule Prf.intros)

   548 apply (metis Cons_eq_append_conv)

   549 apply(simp)

   550 apply(rule Prf.intros)

   551 apply (metis Cons_eq_append_conv)

   552 apply(simp)

   553 done

   554 

   555 lemma v4:

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

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

   558 using assms

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

   560 apply(simp)

   561 apply(erule Prf.cases)

   562 apply(simp_all)[5]

   563 apply(simp)

   564 apply(erule Prf.cases)

   565 apply(simp_all)[5]

   566 apply(simp)

   567 apply(case_tac "c = c'")

   568 apply(simp)

   569 apply(auto)[1]

   570 apply(erule Prf.cases)

   571 apply(simp_all)[5]

   572 apply(simp)

   573 apply(erule Prf.cases)

   574 apply(simp_all)[5]

   575 apply(simp)

   576 apply(erule Prf.cases)

   577 apply(simp_all)[5]

   578 apply(simp)

   579 apply(case_tac "nullable r1")

   580 apply(simp)

   581 apply(erule Prf.cases)

   582 apply(simp_all (no_asm_use))[5]

   583 apply(auto)[1]

   584 apply(erule Prf.cases)

   585 apply(simp_all)[5]

   586 apply(clarify)

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

   588 apply(auto)[1]

   589 apply (metis mkeps_flat)

   590 apply(simp)

   591 apply(erule Prf.cases)

   592 apply(simp_all)[5]

   593 done

   594 

   595 lemma v4_proj:

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

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

   598 using assms

   599 apply(induct rule: Prf.induct)

   600 prefer 4

   601 apply(simp)

   602 prefer 4

   603 apply(simp)

   604 prefer 2

   605 apply(simp)

   606 prefer 2

   607 apply(simp)

   608 apply(auto)

   609 by (metis Cons_eq_append_conv)

   610 

   611 lemma v4_proj2:

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

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

   614 using assms

   615 by (metis list.inject v4_proj)

   616 

   617 

   618 section {* Alternative Posix definition *}

   619 

   620 inductive 

   621   PMatch :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)

   622 where

   623   "[] \<in> EMPTY \<rightarrow> Void"

   624 | "[c] \<in> (CHAR c) \<rightarrow> (Char c)"

   625 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"

   626 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"

   627 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;

   628     \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> 

   629     (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"

   630 

   631 

   632 lemma PMatch_mkeps:

   633   assumes "nullable r"

   634   shows "[] \<in> r \<rightarrow> mkeps r"

   635 using assms

   636 apply(induct r)

   637 apply(auto)

   638 apply (metis PMatch.intros(1))

   639 apply(subst append.simps(1)[symmetric])

   640 apply (rule PMatch.intros)

   641 apply(simp)

   642 apply(simp)

   643 apply(auto)[1]

   644 apply (rule PMatch.intros)

   645 apply(simp)

   646 apply (rule PMatch.intros)

   647 apply(simp)

   648 apply (rule PMatch.intros)

   649 apply(simp)

   650 by (metis nullable_correctness)

   651 

   652 

   653 lemma PMatch1:

   654   assumes "s \<in> r \<rightarrow> v"

   655   shows "\<turnstile> v : r" "flat v = s"

   656 using assms

   657 apply(induct s r v rule: PMatch.induct)

   658 apply(auto)

   659 apply (metis Prf.intros(4))

   660 apply (metis Prf.intros(5))

   661 apply (metis Prf.intros(2))

   662 apply (metis Prf.intros(3))

   663 apply (metis Prf.intros(1))

   664 done

   665 

   666 lemma PMatch_Values:

   667   assumes "s \<in> r \<rightarrow> v"

   668   shows "v \<in> Values r s"

   669 using assms

   670 apply(simp add: Values_def PMatch1)

   671 by (metis append_Nil2 prefix_def)

   672 

   673 lemma PMatch2:

   674   assumes "s \<in> (der c r) \<rightarrow> v"

   675   shows "(c#s) \<in> r \<rightarrow> (injval r c v)"

   676 using assms

   677 apply(induct c r arbitrary: s v rule: der.induct)

   678 apply(auto)

   679 apply(erule PMatch.cases)

   680 apply(simp_all)[5]

   681 apply(erule PMatch.cases)

   682 apply(simp_all)[5]

   683 apply(case_tac "c = c'")

   684 apply(simp)

   685 apply(erule PMatch.cases)

   686 apply(simp_all)[5]

   687 apply (metis PMatch.intros(2))

   688 apply(simp)

   689 apply(erule PMatch.cases)

   690 apply(simp_all)[5]

   691 apply(erule PMatch.cases)

   692 apply(simp_all)[5]

   693 apply (metis PMatch.intros(3))

   694 apply(clarify)

   695 apply(rule PMatch.intros)

   696 apply metis

   697 apply(simp add: L_flat_Prf)

   698 apply(auto)[1]

   699 thm v3_proj

   700 apply(frule_tac c="c" in v3_proj)

   701 apply metis

   702 apply(drule_tac x="projval r1 c v" in spec)

   703 apply(drule mp)

   704 apply (metis v4_proj2)

   705 apply(simp)

   706 apply(case_tac "nullable r1")

   707 apply(simp)

   708 defer

   709 apply(simp)

   710 apply(erule PMatch.cases)

   711 apply(simp_all)[5]

   712 apply(clarify)

   713 apply(subst append.simps(2)[symmetric])

   714 apply(rule PMatch.intros)

   715 apply metis

   716 apply metis

   717 apply(auto)[1]

   718 apply(simp add: L_flat_Prf)

   719 apply(auto)[1]

   720 apply(frule_tac c="c" in v3_proj)

   721 apply metis

   722 apply(drule_tac x="s3" in spec)

   723 apply(drule mp)

   724 apply(rule_tac x="projval r1 c v" in exI)

   725 apply(rule conjI)

   726 apply (metis v4_proj2)

   727 apply(simp)

   728 apply metis

   729 (* nullable case *)

   730 apply(erule PMatch.cases)

   731 apply(simp_all)[5]

   732 apply(clarify)

   733 apply(erule PMatch.cases)

   734 apply(simp_all)[5]

   735 apply(clarify)

   736 apply(subst append.simps(2)[symmetric])

   737 apply(rule PMatch.intros)

   738 apply metis

   739 apply metis

   740 apply(auto)[1]

   741 apply(simp add: L_flat_Prf)

   742 apply(auto)[1]

   743 apply(frule_tac c="c" in v3_proj)

   744 apply metis

   745 apply(drule_tac x="s3" in spec)

   746 apply(drule mp)

   747 apply (metis v4_proj2)

   748 apply(simp)

   749 (* interesting case *)

   750 apply(clarify)

   751 apply(simp)

   752 thm L.simps

   753 apply(subst (asm) L.simps(4)[symmetric])

   754 apply(simp only: L_flat_Prf)

   755 apply(simp)

   756 apply(subst append.simps(1)[symmetric])

   757 apply(rule PMatch.intros)

   758 apply (metis PMatch_mkeps)

   759 apply metis

   760 apply(auto)

   761 apply(simp only: L_flat_Prf)

   762 apply(simp)

   763 apply(auto)

   764 apply(drule_tac x="Seq (projval r1 c v) vb" in spec)

   765 apply(drule mp)

   766 apply(simp)

   767 apply (metis append_Cons butlast_snoc last_snoc neq_Nil_conv rotate1.simps(2) v4_proj2)

   768 apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1")

   769 apply (metis Prf.intros(1))

   770 apply(rule v3_proj)

   771 apply(simp)

   772 by (metis Cons_eq_append_conv)

   773 

   774 lemma lex_correct1:

   775   assumes "s \<notin> L r"

   776   shows "lex r s = None"

   777 using assms

   778 apply(induct s arbitrary: r)

   779 apply(simp)

   780 apply (metis nullable_correctness)

   781 apply(auto)

   782 apply(drule_tac x="der a r" in meta_spec)

   783 apply(drule meta_mp)

   784 apply(auto)

   785 apply(simp add: L_flat_Prf)

   786 by (metis v3 v4)

   787 

   788 

   789 lemma lex_correct2:

   790   assumes "s \<in> L r"

   791   shows "\<exists>v. lex r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s"

   792 using assms

   793 apply(induct s arbitrary: r)

   794 apply(simp)

   795 apply (metis mkeps_flat mkeps_nullable nullable_correctness)

   796 apply(drule_tac x="der a r" in meta_spec)

   797 apply(drule meta_mp)

   798 apply(simp add: L_flat_Prf)

   799 apply(auto)

   800 apply (metis v3_proj v4_proj2)

   801 apply (metis v3)

   802 apply(rule v4)

   803 by metis

   804 

   805 lemma lex_correct3:

   806   assumes "s \<in> L r"

   807   shows "\<exists>v. lex r s = Some(v) \<and> s \<in> r \<rightarrow> v"

   808 using assms

   809 apply(induct s arbitrary: r)

   810 apply(simp)

   811 apply (metis PMatch_mkeps nullable_correctness)

   812 apply(drule_tac x="der a r" in meta_spec)

   813 apply(drule meta_mp)

   814 apply(simp add: L_flat_Prf)

   815 apply(auto)

   816 apply (metis v3_proj v4_proj2)

   817 apply(rule PMatch2)

   818 apply(simp)

   819 done

   820 

   821 lemma lex_correct4:

   822   assumes "s \<in> L r"

   823   shows "s \<in> r \<rightarrow> (lex2 r s)"

   824 using assms

   825 apply(induct s arbitrary: r)

   826 apply(simp)

   827 apply (metis PMatch_mkeps nullable_correctness)

   828 apply(simp)

   829 apply(rule PMatch2)

   830 apply(drule_tac x="der a r" in meta_spec)

   831 apply(drule meta_mp)

   832 apply(simp add: L_flat_Prf)

   833 apply(auto)

   834 apply (metis v3_proj v4_proj2)

   835 done

   836 

   837 lemma 

   838   "lex2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))"

   839 apply(simp)

   840 done

   841 

   842 

   843 section {* Sulzmann's Ordering of values *}

   844 

   845 

   846 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)

   847 where

   848   "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 

   849 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 

   850 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"

   851 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"

   852 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"

   853 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"

   854 | "Void \<succ>EMPTY Void"

   855 | "(Char c) \<succ>(CHAR c) (Char c)"

   856 

   857 inductive ValOrd2 :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ 2\<succ> _" [100, 100] 100)

   858 where

   859   "v2 2\<succ> v2' \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1 v2')" 

   860 | "\<lbrakk>v1 2\<succ> v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1' v2')" 

   861 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) 2\<succ> (Right v2)"

   862 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) 2\<succ> (Left v1)"

   863 | "v2 2\<succ> v2' \<Longrightarrow> (Right v2) 2\<succ> (Right v2')"

   864 | "v1 2\<succ> v1' \<Longrightarrow> (Left v1) 2\<succ> (Left v1')"

   865 | "Void 2\<succ> Void"

   866 | "(Char c) 2\<succ> (Char c)"

   867 

   868 lemma Ord1:

   869   "v1 \<succ>r v2 \<Longrightarrow> v1 2\<succ> v2"

   870 apply(induct rule: ValOrd.induct)

   871 apply(auto intro: ValOrd2.intros)

   872 done

   873 

   874 lemma Ord2:

   875   "v1 2\<succ> v2 \<Longrightarrow> \<exists>r. v1 \<succ>r v2"

   876 apply(induct v1 v2 rule: ValOrd2.induct)

   877 apply(auto intro: ValOrd.intros)

   878 done

   879 

   880 lemma Ord3:

   881   "\<lbrakk>v1 2\<succ> v2; \<turnstile> v1 : r\<rbrakk> \<Longrightarrow> v1 \<succ>r v2"

   882 apply(induct v1 v2 arbitrary: r rule: ValOrd2.induct)

   883 apply(auto intro: ValOrd.intros elim: Prf.cases)

   884 done

   885 

   886 section {* Posix definition *}

   887 

   888 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 

   889 where

   890   "POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v' \<sqsubseteq> flat v) \<longrightarrow> v \<succ>r v'))"

   891 

   892 lemma ValOrd_refl:

   893   assumes "\<turnstile> v : r"

   894   shows "v \<succ>r v"

   895 using assms

   896 apply(induct)

   897 apply(auto intro: ValOrd.intros)

   898 done

   899 

   900 lemma ValOrd_total:

   901   shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r\<rbrakk>  \<Longrightarrow> v1 \<succ>r v2 \<or> v2 \<succ>r v1"

   902 apply(induct r arbitrary: v1 v2)

   903 apply(auto)

   904 apply(erule Prf.cases)

   905 apply(simp_all)[5]

   906 apply(erule Prf.cases)

   907 apply(simp_all)[5]

   908 apply(erule Prf.cases)

   909 apply(simp_all)[5]

   910 apply (metis ValOrd.intros(7))

   911 apply(erule Prf.cases)

   912 apply(simp_all)[5]

   913 apply(erule Prf.cases)

   914 apply(simp_all)[5]

   915 apply (metis ValOrd.intros(8))

   916 apply(erule Prf.cases)

   917 apply(simp_all)[5]

   918 apply(erule Prf.cases)

   919 apply(simp_all)[5]

   920 apply(clarify)

   921 apply(case_tac "v1a = v1b")

   922 apply(simp)

   923 apply(rule ValOrd.intros(1))

   924 apply (metis ValOrd.intros(1))

   925 apply(rule ValOrd.intros(2))

   926 apply(auto)[2]

   927 apply(erule contrapos_np)

   928 apply(rule ValOrd.intros(2))

   929 apply(auto)

   930 apply(erule Prf.cases)

   931 apply(simp_all)[5]

   932 apply(erule Prf.cases)

   933 apply(simp_all)[5]

   934 apply (metis Ord1 Ord3 Prf.intros(2) ValOrd2.intros(6))

   935 apply(rule ValOrd.intros)

   936 apply(erule contrapos_np)

   937 apply(rule ValOrd.intros)

   938 apply (metis le_eq_less_or_eq neq_iff)

   939 apply(erule Prf.cases)

   940 apply(simp_all)[5]

   941 apply(rule ValOrd.intros)

   942 apply(erule contrapos_np)

   943 apply(rule ValOrd.intros)

   944 apply (metis le_eq_less_or_eq neq_iff)

   945 apply(rule ValOrd.intros)

   946 apply(erule contrapos_np)

   947 apply(rule ValOrd.intros)

   948 by metis

   949 

   950 lemma ValOrd_anti:

   951   shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r; v1 \<succ>r v2; v2 \<succ>r v1\<rbrakk> \<Longrightarrow> v1 = v2"

   952 apply(induct r arbitrary: v1 v2)

   953 apply(erule Prf.cases)

   954 apply(simp_all)[5]

   955 apply(erule Prf.cases)

   956 apply(simp_all)[5]

   957 apply(erule Prf.cases)

   958 apply(simp_all)[5]

   959 apply(erule Prf.cases)

   960 apply(simp_all)[5]

   961 apply(erule Prf.cases)

   962 apply(simp_all)[5]

   963 apply(erule Prf.cases)

   964 apply(simp_all)[5]

   965 apply(erule Prf.cases)

   966 apply(simp_all)[5]

   967 apply(erule ValOrd.cases)

   968 apply(simp_all)[8]

   969 apply(erule ValOrd.cases)

   970 apply(simp_all)[8]

   971 apply(erule ValOrd.cases)

   972 apply(simp_all)[8]

   973 apply(erule Prf.cases)

   974 apply(simp_all)[5]

   975 apply(erule Prf.cases)

   976 apply(simp_all)[5]

   977 apply(erule ValOrd.cases)

   978 apply(simp_all)[8]

   979 apply(erule ValOrd.cases)

   980 apply(simp_all)[8]

   981 apply(erule ValOrd.cases)

   982 apply(simp_all)[8]

   983 apply(erule ValOrd.cases)

   984 apply(simp_all)[8]

   985 apply(erule Prf.cases)

   986 apply(simp_all)[5]

   987 apply(erule ValOrd.cases)

   988 apply(simp_all)[8]

   989 apply(erule ValOrd.cases)

   990 apply(simp_all)[8]

   991 apply(erule ValOrd.cases)

   992 apply(simp_all)[8]

   993 apply(erule ValOrd.cases)

   994 apply(simp_all)[8]

   995 done

   996 

   997 lemma POSIX_ALT_I1:

   998   assumes "POSIX v1 r1" 

   999   shows "POSIX (Left v1) (ALT r1 r2)"

  1000 using assms

  1001 unfolding POSIX_def

  1002 apply(auto)

  1003 apply (metis Prf.intros(2))

  1004 apply(rotate_tac 2)

  1005 apply(erule Prf.cases)

  1006 apply(simp_all)[5]

  1007 apply(auto)

  1008 apply(rule ValOrd.intros)

  1009 apply(auto)

  1010 apply(rule ValOrd.intros)

  1011 by (metis le_eq_less_or_eq length_sprefix sprefix_def)

  1012 

  1013 lemma POSIX_ALT_I2:

  1014   assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"

  1015   shows "POSIX (Right v2) (ALT r1 r2)"

  1016 using assms

  1017 unfolding POSIX_def

  1018 apply(auto)

  1019 apply (metis Prf.intros)

  1020 apply(rotate_tac 3)

  1021 apply(erule Prf.cases)

  1022 apply(simp_all)[5]

  1023 apply(auto)

  1024 apply(rule ValOrd.intros)

  1025 apply metis

  1026 apply(rule ValOrd.intros)

  1027 apply metis

  1028 done

  1029 

  1030 section {* tryout with all-mkeps *}

  1031 

  1032 fun 

  1033   alleps :: "rexp \<Rightarrow> val set"

  1034 where

  1035   "alleps(NULL) = {}"

  1036 | "alleps(EMPTY) = {Void}"

  1037 | "alleps(CHAR c) = {}"

  1038 | "alleps(SEQ r1 r2) = {Seq v1 v2 | v1 v2. v1 \<in> alleps r1 \<and> v2 \<in> alleps r2}"

  1039 | "alleps(ALT r1 r2) = {Left v1 | v1. v1 \<in> alleps r1} \<union> {Right v2 | v2. v2 \<in> alleps r2}"

  1040 

  1041 fun injall :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val set"

  1042 where

  1043   "injall (EMPTY) c Void = {}"

  1044 | "injall (CHAR d) c Void = (if c = d then {Char d} else {})"

  1045 | "injall (ALT r1 r2) c (Left v1) = {Left v | v. v \<in> injall r1 c v1}"

  1046 | "injall (ALT r1 r2) c (Right v2) = {Right v | v. v \<in> injall r2 c v2}"

  1047 | "injall (SEQ r1 r2) c (Seq v1 v2) = {Seq v v2 | v. v \<in> injall r1 c v1}"

  1048 | "injall (SEQ r1 r2) c (Left (Seq v1 v2)) = {Seq v v2 | v. v \<in> injall r1 c v1}"

  1049 | "injall (SEQ r1 r2) c (Right v2) = {Seq v v' | v v'. v \<in> alleps r1 \<and> v' \<in> injall r2 c v2}"

  1050 

  1051 fun 

  1052   allvals :: "rexp \<Rightarrow> string \<Rightarrow> val set"

  1053 where

  1054   "allvals r [] = alleps r"

  1055 | "allvals r (c#s) = {v | v v'. v \<in> injall r c v' \<and> v' \<in> allvals (der c r) s}"

  1056 

  1057 lemma q1: 

  1058   assumes "v \<in> alleps r"

  1059   shows "\<turnstile> v : r \<and> flat v = []"

  1060 using assms

  1061 apply(induct r arbitrary: v)

  1062 apply(auto intro: Prf.intros)

  1063 done

  1064 

  1065 

  1066 lemma allvals_NULL:

  1067   shows "allvals (NULL) s = {}"

  1068 apply(induct_tac s)

  1069 apply(simp)

  1070 apply(simp)

  1071 done

  1072 

  1073 lemma allvals_EMPTY:

  1074   shows "allvals (EMPTY) [] = {Void}"

  1075   and   "s \<noteq> [] \<Longrightarrow> allvals (EMPTY) s = {}"

  1076 apply(simp)

  1077 apply(case_tac s)

  1078 apply(simp)

  1079 apply(simp add: allvals_NULL)

  1080 done

  1081 

  1082 lemma allvals_CHAR:

  1083   shows "allvals (CHAR c) [c] = {Char c}"

  1084   and   "s \<noteq> [c] \<Longrightarrow> allvals (CHAR c) s = {}"

  1085 apply(simp)

  1086 apply(case_tac s)

  1087 apply(simp)

  1088 apply(case_tac "c = a")

  1089 apply(simp add: allvals_EMPTY)

  1090 apply(simp add: allvals_NULL)

  1091 done

  1092 

  1093 lemma allvals_ALT:

  1094   shows "allvals (ALT r1 r2) s = {Left v1 | v1. v1 \<in> allvals r1 s} \<union>

  1095                                  {Right v2 | v2. v2 \<in> allvals r2 s}"

  1096 apply(induct s arbitrary: r1 r2)

  1097 apply(simp)

  1098 apply(simp)

  1099 apply(auto)

  1100 apply blast

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

  1102 apply(simp)

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

  1104 apply(simp)

  1105 done

  1106 

  1107 lemma allvals_SEQ_Nil:

  1108   "allvals (SEQ r1 r2) [] = {Seq v1 v2 | v1 v2. v1 \<in> allvals r1 [] \<and> v2 \<in> allvals r2 []}"

  1109 by simp

  1110 

  1111 lemma allvals_SEQ:

  1112   shows "allvals (SEQ r1 r2) s = {Seq v1 v2 | v1 v2 s1 s2. 

  1113       s = s1 @ s2 \<and> v1 \<in> allvals r1 s1 \<and> v2 \<in> allvals r2 s2}"

  1114 using assms

  1115 apply(induct s arbitrary: r1 r2)

  1116 apply(simp)

  1117 apply(simp)

  1118 apply(auto)

  1119 apply(simp_all add: allvals_ALT)

  1120 apply(auto)

  1121 apply (metis (mono_tags, lifting) allvals.simps(2) append_Cons mem_Collect_eq)

  1122 apply fastforce

  1123 prefer 2

  1124 apply(rule_tac x="a#s1" in exI)

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

  1126 apply(simp)

  1127 apply(fastforce)

  1128 prefer 2

  1129 apply(subst (asm) Cons_eq_append_conv)

  1130 apply(auto)[1]

  1131 using Prf_flat_L nullable_correctness q1 apply fastforce

  1132 apply(rule_tac x="Seq v' v2" in exI)

  1133 apply(simp)

  1134 apply(rule_tac x="ys'" in exI)

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