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/Re1.thy
changeset 77 4b4c677501e7
parent 76 39cef7b9212a
child 78 279d0bc48308
equal deleted inserted replaced
76:39cef7b9212a 77:4b4c677501e7 
   138 | "flats(Right v) = flats(v)"
 
   138 | "flats(Right v) = flats(v)"
 
   139 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)"
 
   139 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)"
 
   140 
   140 
   141 value "flats(Seq(Char c)(Char b))"
 
   141 value "flats(Seq(Char c)(Char b))"
 
   142 
   142 
   143 inductive StrOrd :: "string list \<Rightarrow> string list \<Rightarrow> bool" ("_ \<sqsupset> _" [100, 100] 100)
 
   143 section {* Relation between values and regular expressions *}
 
       
   144 
       
   145 inductive Prfs :: "string \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile>_ _ : _" [100, 100, 100] 100)
 
   144 where
 
   146 where
 
   145    "[] \<sqsupset> []"
 
   147  "\<lbrakk>\<Turnstile>s1 v1 : r1; \<Turnstile>s2 v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>(s1 @ s2) (Seq v1 v2) : SEQ r1 r2"
 
   146 |  "xs \<sqsupset> ys \<Longrightarrow> (x#xs) \<sqsupset> (x#ys)"
 
   148 | "\<Turnstile>s v1 : r1 \<Longrightarrow> \<Turnstile>s (Left v1) : ALT r1 r2"
 
   147 |  "length x \<ge> length y \<Longrightarrow> (x#xs) \<sqsupset> (y#xs)"
 
   149 | "\<Turnstile>s v2 : r2 \<Longrightarrow> \<Turnstile>s (Right v2) : ALT r1 r2"
 
   148 
   150 | "\<Turnstile>[] Void : EMPTY"
 
   149 lemma StrOrd_append: 
   151 | "\<Turnstile>[c] (Char c) : CHAR c"
 
   150   "xs \<sqsupset> ys \<Longrightarrow> (zs @ xs) \<sqsupset> (zs @ ys)"
 
   152 
   151 apply(induct zs)
 
   153 lemma Prfs_flat:
 
   152 apply(auto intro: StrOrd.intros) 
   154   "\<Turnstile>s v : r \<Longrightarrow> flat v = s"
 
   153 done
 
   155 apply(induct s v r rule: Prfs.induct)
 
   154 
   156 apply(auto)
 
   155 section {* Relation between values and regular expressions *}
 
   157 done
 
       
   158 
       
   159 
       
   160 inductive Prfn :: "nat \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> bool" ("\<TTurnstile>_ _ : _" [100, 100, 100] 100)
 
       
   161 where
 
       
   162  "\<lbrakk>\<TTurnstile>n1 v1 : r1; \<TTurnstile>n2 v2 : r2\<rbrakk> \<Longrightarrow> \<TTurnstile>(n1 + n2) (Seq v1 v2) : SEQ r1 r2"
 
       
   163 | "\<TTurnstile>n v1 : r1 \<Longrightarrow> \<TTurnstile>n (Left v1) : ALT r1 r2"
 
       
   164 | "\<TTurnstile>n v2 : r2 \<Longrightarrow> \<TTurnstile>n (Right v2) : ALT r1 r2"
 
       
   165 | "\<TTurnstile>0 Void : EMPTY"
 
       
   166 | "\<TTurnstile>1 (Char c) : CHAR c"
 
       
   167 
       
   168 lemma Prfn_flat:
 
       
   169   "\<TTurnstile>n v : r \<Longrightarrow> length(flat v) = n"
 
       
   170 apply(induct rule: Prfn.induct)
 
       
   171 apply(auto)
 
       
   172 done
 
   156 
   173 
   157 inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 
   174 inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 
   158 where
 
   175 where
 
   159  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
 
   176  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
 
   160 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
 
   177 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
 
   161 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 
   178 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 
   162 | "\<turnstile> Void : EMPTY"
 
   179 | "\<turnstile> Void : EMPTY"
 
   163 | "\<turnstile> Char c : CHAR c"
 
   180 | "\<turnstile> Char c : CHAR c"
 
   164 
   181 
   165 inductive Prfs :: "val list \<Rightarrow> rexp list \<Rightarrow> bool"  ("\<Turnstile> _ : _" [100, 100] 100)
 
   182 lemma Prf_Prfn:
 
   166 where
 
   183   shows "\<turnstile> v : r \<Longrightarrow> \<TTurnstile>(length (flat v)) v : r"
 
   167   "\<Turnstile> [] : []"
 
   184 apply(induct v r rule: Prf.induct)
 
   168 | "\<lbrakk>\<turnstile>v : r; \<Turnstile> vs : rs\<rbrakk> \<Longrightarrow> \<Turnstile> (v#vs) : (r#rs)"
 
   185 apply(auto intro: Prfn.intros)
 
       
   186 by (metis One_nat_def Prfn.intros(5))
 
       
   187 
       
   188 lemma Prfn_Prf:
 
       
   189   shows "\<TTurnstile>n v : r \<Longrightarrow> \<turnstile> v : r"
 
       
   190 apply(induct n v r rule: Prfn.induct)
 
       
   191 apply(auto intro: Prf.intros)
 
       
   192 done
 
       
   193 
       
   194 lemma Prf_Prfs:
 
       
   195   shows "\<turnstile> v : r \<Longrightarrow> \<Turnstile>(flat v) v : r"
 
       
   196 apply(induct v r rule: Prf.induct)
 
       
   197 apply(auto intro: Prfs.intros)
 
       
   198 done
 
       
   199 
       
   200 lemma Prfs_Prf:
 
       
   201   shows "\<Turnstile>s v : r \<Longrightarrow> \<turnstile> v : r"
 
       
   202 apply(induct s v r rule: Prfs.induct)
 
       
   203 apply(auto intro: Prf.intros)
 
       
   204 done
 
   169 
   205 
   170 fun mkeps :: "rexp \<Rightarrow> val"
 
   206 fun mkeps :: "rexp \<Rightarrow> val"
 
   171 where
 
   207 where
 
   172   "mkeps(EMPTY) = Void"
 
   208   "mkeps(EMPTY) = Void"
 
   173 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
 
   209 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
 
   178 using assms
 
   214 using assms
 
   179 apply(induct rule: nullable.induct)
 
   215 apply(induct rule: nullable.induct)
 
   180 apply(auto intro: Prf.intros)
 
   216 apply(auto intro: Prf.intros)
 
   181 done
 
   217 done
 
   182 
   218 
   183 value "flat(Seq(Char c)(Char b))"
 
   219 lemma mkeps_nullable_n:
 
   184 value "flat(Right(Void))"
 
   220   assumes "nullable(r)" shows "\<TTurnstile>0 (mkeps r) : r"
 
       
   221 using assms
 
       
   222 apply(induct rule: nullable.induct)
 
       
   223 apply(auto intro: Prfn.intros)
 
       
   224 apply(drule Prfn.intros(1))
 
       
   225 apply(assumption)
 
       
   226 apply(simp)
 
       
   227 done
 
       
   228 
       
   229 lemma mkeps_nullable_s:
 
       
   230   assumes "nullable(r)" shows "\<Turnstile>[] (mkeps r) : r"
 
       
   231 using assms
 
       
   232 apply(induct rule: nullable.induct)
 
       
   233 apply(auto intro: Prfs.intros)
 
       
   234 apply(drule Prfs.intros(1))
 
       
   235 apply(assumption)
 
       
   236 apply(simp)
 
       
   237 done
 
   185 
   238 
   186 lemma mkeps_flat:
 
   239 lemma mkeps_flat:
 
   187   assumes "nullable(r)" shows "flat (mkeps r) = []"
 
   240   assumes "nullable(r)" shows "flat (mkeps r) = []"
 
   188 using assms
 
   241 using assms
 
   189 apply(induct rule: nullable.induct)
 
   242 apply(induct rule: nullable.induct)
 
   194   assumes "nullable(r)" shows "flat_left (mkeps r) = []"
 
   247   assumes "nullable(r)" shows "flat_left (mkeps r) = []"
 
   195 using assms
 
   248 using assms
 
   196 apply(induct rule: nullable.induct)
 
   249 apply(induct rule: nullable.induct)
 
   197 apply(auto)
 
   250 apply(auto)
 
   198 done
 
   251 done
 
   199 
       
   200 
       
   201 
   252 
   202 text {*
 
   253 text {*
 
   203   The value mkeps returns is always the correct POSIX
 
   254   The value mkeps returns is always the correct POSIX
 
   204   value.
 
   255   value.
 
   205 *}
 
   256 *}
 
   206 
       
   207 
       
   208 
       
   209 
       
   210 
   257 
   211 lemma Prf_flat_L:
 
   258 lemma Prf_flat_L:
 
   212   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 
   259   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 
   213 using assms
 
   260 using assms
 
   214 apply(induct v r rule: Prf.induct)
 
   261 apply(induct v r rule: Prf.induct)
 
   281 using assms
 
   328 using assms
 
   282 apply(induct)
 
   329 apply(induct)
 
   283 apply(auto intro: ValOrd.intros)
 
   330 apply(auto intro: ValOrd.intros)
 
   284 done
 
   331 done
 
   285 
   332 
       
   333 lemma 
       
   334   "flat Void = []"
 
       
   335   "flat (Seq Void Void) = []"
 
       
   336 apply(simp_all)
 
       
   337 done
 
       
   338 
       
   339 
       
   340 lemma ValOrd_total:
 
       
   341   shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r\<rbrakk>  \<Longrightarrow> v1 \<succ>r v2 \<or> v2 \<succ>r v1"
 
       
   342 apply(induct r arbitrary: v1 v2)
 
       
   343 apply(auto)
 
       
   344 apply(erule Prf.cases)
 
       
   345 apply(simp_all)[5]
 
       
   346 apply(erule Prf.cases)
 
       
   347 apply(simp_all)[5]
 
       
   348 apply(erule Prf.cases)
 
       
   349 apply(simp_all)[5]
 
       
   350 apply (metis ValOrd.intros(7))
 
       
   351 apply(erule Prf.cases)
 
       
   352 apply(simp_all)[5]
 
       
   353 apply(erule Prf.cases)
 
       
   354 apply(simp_all)[5]
 
       
   355 apply (metis ValOrd.intros(8))
 
       
   356 apply(erule Prf.cases)
 
       
   357 apply(simp_all)[5]
 
       
   358 apply(erule Prf.cases)
 
       
   359 apply(simp_all)[5]
 
       
   360 apply(clarify)
 
       
   361 apply(case_tac "v1a = v1b")
 
       
   362 apply(simp)
 
       
   363 apply(rule ValOrd.intros(1))
 
       
   364 apply (metis ValOrd.intros(1))
 
       
   365 apply(rule ValOrd.intros(2))
 
       
   366 apply(auto)[2]
 
       
   367 apply(erule contrapos_np)
 
       
   368 apply(rule ValOrd.intros(2))
 
       
   369 apply(auto)
 
       
   370 apply(erule Prf.cases)
 
       
   371 apply(simp_all)[5]
 
       
   372 apply(erule Prf.cases)
 
       
   373 apply(simp_all)[5]
 
       
   374 apply (metis Ord1 Ord3 Prf.intros(2) ValOrd2.intros(6))
 
       
   375 apply(rule ValOrd.intros)
 
       
   376 apply(erule contrapos_np)
 
       
   377 apply(rule ValOrd.intros)
 
       
   378 apply (metis le_eq_less_or_eq neq_iff)
 
       
   379 apply(erule Prf.cases)
 
       
   380 apply(simp_all)[5]
 
       
   381 apply(rule ValOrd.intros)
 
       
   382 apply(erule contrapos_np)
 
       
   383 apply(rule ValOrd.intros)
 
       
   384 apply (metis le_eq_less_or_eq neq_iff)
 
       
   385 apply(rule ValOrd.intros)
 
       
   386 apply(erule contrapos_np)
 
       
   387 apply(rule ValOrd.intros)
 
       
   388 by metis
 
       
   389 
       
   390 lemma ValOrd_anti:
 
       
   391   shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r; v1 \<succ>r v2; v2 \<succ>r v1\<rbrakk> \<Longrightarrow> v1 = v2"
 
       
   392 apply(induct r arbitrary: v1 v2)
 
       
   393 apply(erule Prf.cases)
 
       
   394 apply(simp_all)[5]
 
       
   395 apply(erule Prf.cases)
 
       
   396 apply(simp_all)[5]
 
       
   397 apply(erule Prf.cases)
 
       
   398 apply(simp_all)[5]
 
       
   399 apply(erule Prf.cases)
 
       
   400 apply(simp_all)[5]
 
       
   401 apply(erule Prf.cases)
 
       
   402 apply(simp_all)[5]
 
       
   403 apply(erule Prf.cases)
 
       
   404 apply(simp_all)[5]
 
       
   405 apply(erule Prf.cases)
 
       
   406 apply(simp_all)[5]
 
       
   407 apply(erule ValOrd.cases)
 
       
   408 apply(simp_all)[8]
 
       
   409 apply(erule ValOrd.cases)
 
       
   410 apply(simp_all)[8]
 
       
   411 apply(erule ValOrd.cases)
 
       
   412 apply(simp_all)[8]
 
       
   413 apply(erule Prf.cases)
 
       
   414 apply(simp_all)[5]
 
       
   415 apply(erule Prf.cases)
 
       
   416 apply(simp_all)[5]
 
       
   417 apply(erule ValOrd.cases)
 
       
   418 apply(simp_all)[8]
 
       
   419 apply(erule ValOrd.cases)
 
       
   420 apply(simp_all)[8]
 
       
   421 apply(erule ValOrd.cases)
 
       
   422 apply(simp_all)[8]
 
       
   423 apply(erule ValOrd.cases)
 
       
   424 apply(simp_all)[8]
 
       
   425 apply(erule Prf.cases)
 
       
   426 apply(simp_all)[5]
 
       
   427 apply(erule ValOrd.cases)
 
       
   428 apply(simp_all)[8]
 
       
   429 apply(erule ValOrd.cases)
 
       
   430 apply(simp_all)[8]
 
       
   431 apply(erule ValOrd.cases)
 
       
   432 apply(simp_all)[8]
 
       
   433 apply(erule ValOrd.cases)
 
       
   434 apply(simp_all)[8]
 
       
   435 done
 
       
   436 
       
   437 lemma ValOrd_max:
 
       
   438   shows "\<exists>v. \<forall>v'. (v' \<succ>r v \<longrightarrow> v = v')" 
       
   439 apply(induct r)
 
       
   440 apply(auto)
 
       
   441 apply(rule exI)
 
       
   442 apply(rule allI)
 
       
   443 apply(rule impI)
 
       
   444 apply(erule ValOrd.cases)
 
       
   445 apply(simp_all)[8]
 
       
   446 apply(rule exI)
 
       
   447 apply(rule allI)
 
       
   448 apply(rule impI)
 
       
   449 apply(erule ValOrd.cases)
 
       
   450 apply(simp_all)[8]
 
       
   451 apply(rule exI)
 
       
   452 apply(rule allI)
 
       
   453 apply(rule impI)
 
       
   454 apply(erule ValOrd.cases)
 
       
   455 apply(simp_all)[8]
 
       
   456 apply(rule exI)
 
       
   457 apply(rule allI)
 
       
   458 apply(rule impI)
 
       
   459 apply(erule ValOrd.cases)
 
       
   460 apply(simp_all)[8]
 
       
   461 apply(rule exI)
 
       
   462 apply(rule allI)
 
       
   463 apply(rule impI)
 
       
   464 apply(erule ValOrd.cases)
 
       
   465 apply(simp_all)[8]
 
       
   466 done
 
       
   467 
       
   468 lemma ValOrd_max:
 
       
   469   assumes "L r \<noteq> {}"
 
       
   470   shows "\<exists>v. \<turnstile> v : r \<and> (\<forall>v'. ((\<turnstile> v' : r \<and> v' \<succ>r v) \<longrightarrow> v = v'))" 
       
   471 using assms
 
       
   472 apply(induct r)
 
       
   473 apply(auto)
 
       
   474 apply(rule exI)
 
       
   475 apply(rule conjI)
 
       
   476 apply(rule Prf.intros)
 
       
   477 apply(rule allI)
 
       
   478 apply(rule impI)
 
       
   479 apply(erule conjE)
 
       
   480 apply(erule ValOrd.cases)
 
       
   481 apply(simp_all)[8]
 
       
   482 apply(rule exI)
 
       
   483 apply(rule conjI)
 
       
   484 apply(rule Prf.intros)
 
       
   485 apply(rule allI)
 
       
   486 apply(rule impI)
 
       
   487 apply(erule conjE)
 
       
   488 apply(erule ValOrd.cases)
 
       
   489 apply(simp_all)[8]
 
       
   490 apply(auto simp add: Sequ_def)[1]
 
       
   491 apply(drule meta_mp)
 
       
   492 apply (metis empty_iff)
 
       
   493 apply(drule meta_mp)
 
       
   494 apply (metis empty_iff)
 
       
   495 apply(auto)[1]
 
       
   496 apply(drule_tac x="Seq v va" in spec)
 
       
   497 apply(drule mp)
 
       
   498 apply (metis Prf.intros(1))
 
       
   499 apply(auto)[1]
 
       
   500 apply(erule ValOrd.cases)
 
       
   501 apply(simp_all)[8]
 
       
   502 apply(rotate_tac 6)
 
       
   503 apply(erule Prf.cases)
 
       
   504 apply(simp_all)[5]
 
       
   505 apply(rotate_tac 6)
 
       
   506 apply(erule Prf.cases)
 
       
   507 apply(simp_all)[5]
 
       
   508 apply(clarify)
 
       
   509 apply metis
 
       
   510 apply(drule meta_mp)
 
       
   511 apply (metis empty_iff)
 
       
   512 apply(auto)[1]
 
       
   513 apply(drule_tac x="Left v" in spec)
 
       
   514 apply(drule mp)
 
       
   515 apply (metis Prf.intros)
 
       
   516 apply(auto)[1]
 
       
   517 apply(rotate_tac 4)
 
       
   518 apply(erule Prf.cases)
 
       
   519 apply(simp_all)[5]
 
       
   520 apply(erule ValOrd.cases)
 
       
   521 apply(simp_all)[8]
 
       
   522 apply(erule ValOrd.cases)
 
       
   523 apply(simp_all)[8]
 
       
   524 apply(clarify)
 
       
   525 apply(auto)[1]
 
       
   526 oops
 
       
   527 
       
   528 lemma ValOrd_max2:
 
       
   529   shows "\<exists>v. \<turnstile> v : r \<and> (\<forall>v'. v \<succ>r v')" 
       
   530 using ValOrd_max[where r="r"]
 
       
   531 apply -
 
       
   532 apply(auto)
 
       
   533 apply(rule_tac x="v" in exI)
 
       
   534 apply(auto)
 
       
   535 oops
 
       
   536 
       
   537 lemma ValOrd_trans:
 
       
   538   assumes "v1 \<succ>r v2" "v2 \<succ>r v3" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<turnstile> v3 : r" "flat v1 = flat v2" "flat v2 = flat v3"
 
       
   539   shows "v1 \<succ>r v3"
 
       
   540 using assms
 
       
   541 apply(induct r arbitrary: v1 v2 v3)
 
       
   542 apply(erule Prf.cases)
 
       
   543 apply(simp_all)[5]
 
       
   544 apply(erule Prf.cases)
 
       
   545 apply(simp_all)[5]
 
       
   546 apply(erule Prf.cases)
 
       
   547 apply(simp_all)[5]
 
       
   548 apply(erule Prf.cases)
 
       
   549 apply(simp_all)[5]
 
       
   550 apply(erule Prf.cases)
 
       
   551 apply(simp_all)[5]
 
       
   552 apply(erule Prf.cases)
 
       
   553 apply(simp_all)[5]
 
       
   554 apply(erule Prf.cases)
 
       
   555 apply(simp_all)[5]
 
       
   556 apply(erule Prf.cases)
 
       
   557 apply(simp_all)[5]
 
       
   558 apply(clarify)
 
       
   559 apply(erule ValOrd.cases)
 
       
   560 apply(simp_all)[8]
 
       
   561 apply(erule ValOrd.cases)
 
       
   562 apply(simp_all)[8]
 
       
   563 apply(clarify)
 
       
   564 apply (metis ValOrd.intros(1))
 
       
   565 apply(clarify)
 
       
   566 apply (metis ValOrd.intros(2))
 
       
   567 apply(erule ValOrd.cases)
 
       
   568 apply(simp_all)[8]
 
       
   569 apply (metis ValOrd.intros(2))
 
       
   570 apply(clarify)
 
       
   571 apply(case_tac "v1d = v1'a")
 
       
   572 apply(simp)
 
       
   573 apply (metis ValOrd_anti)
 
       
   574 apply (rule ValOrd.intros(2))
 
       
   575 prefer 2
 
       
   576 apply(auto)[1]
 
       
   577 prefer 2
 
       
   578 oops
 
       
   579 
       
   580 
       
   581 
   286 section {* Posix definition *}
 
   582 section {* Posix definition *}
 
   287 
   583 
   288 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
   584 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
   289 where
 
   585 where
 
   290   "POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v'))"
 
   586   "POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v'))"
 
   300 apply(auto)
 
   596 apply(auto)
 
   301 apply(rule Ord3)
 
   597 apply(rule Ord3)
 
   302 apply(auto)
 
   598 apply(auto)
 
   303 done
 
   599 done
 
   304 
   600 
   305 (*
 
   601 definition POSIXs :: "val \<Rightarrow> rexp \<Rightarrow> string \<Rightarrow> bool" 
   306 an alternative definition: might cause problems
 
       
   307 with theorem mkeps_POSIX
 
       
   308 *)
 
       
   309 
       
   310 (*
 
       
   311 definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
       
   312 where
 
   602 where
 
   313   "POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')"
 
   603   "POSIXs v r s \<equiv> (\<Turnstile>s v : r \<and> (\<forall>v'. (\<Turnstile>s v' : r \<longrightarrow> v 2\<succ> v')))"
 
   314 *)
 
   604 
   315 
   605 definition POSIXn :: "val \<Rightarrow> rexp \<Rightarrow> nat \<Rightarrow> bool" 
   316 (*
 
       
   317 definition POSIX3 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
       
   318 where
 
   606 where
 
   319   "POSIX3 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> length (flat v') \<le> length(flat v)) \<longrightarrow> v \<succ>r v')"
 
   607   "POSIXn v r n \<equiv> (\<TTurnstile>n v : r \<and> (\<forall>v'. (\<TTurnstile>n v' : r \<longrightarrow> v 2\<succ> v')))"
 
   320 *)
 
   608 
       
   609 lemma "POSIXn v r (length (flat v)) \<Longrightarrow> POSIX2 v r"
 
       
   610 unfolding POSIXn_def POSIX2_def
 
       
   611 apply(auto)
 
       
   612 apply (metis Prfn_Prf)
 
       
   613 by (metis Prf_Prfn)
 
       
   614 
       
   615 lemma Prfs_POSIX:
 
       
   616   "POSIXs v r s \<Longrightarrow> \<Turnstile>s v: r \<and> flat v = s"
 
       
   617 apply(simp add: POSIXs_def)
 
       
   618 by (metis Prfs_flat)
 
       
   619 
       
   620 
       
   621 lemma "POSIXs v r (flat v) =  POSIX2 v r"
 
       
   622 unfolding POSIXs_def POSIX2_def
 
       
   623 apply(auto)
 
       
   624 apply (metis Prfs_Prf)
 
       
   625 apply (metis Prf_Prfs)
 
       
   626 apply (metis Prf_Prfs)
 
       
   627 by (metis Prfs_Prf Prfs_flat)
 
       
   628 
       
   629 lemma 
       
   630   assumes "POSIX v1 r1" "\<turnstile> v1' : r1"
 
       
   631   shows "Seq v1 v2 \<succ>(SEQ r1 r2) Seq v1' v2'"
 
       
   632 using assms
 
       
   633 apply(rule_tac ValOrd.intros)
 
       
   634 apply(simp add: POSIX_def)
 
       
   635 oops
 
       
   636 
       
   637 lemma
 
       
   638 "L r \<noteq> {} \<Longrightarrow> \<exists>v. POSIXs v r (flat v)"
 
       
   639 apply(induct r arbitrary: )
 
       
   640 apply(simp)
 
       
   641 apply(rule_tac x="Void" in exI)
 
       
   642 apply(simp add: POSIXs_def)
 
       
   643 apply(rule conjI)
 
       
   644 apply (metis Prfs.intros(4))
 
       
   645 apply(auto)[1]
 
       
   646 apply(erule Prfs.cases)
 
       
   647 apply(simp_all)[5]
 
       
   648 apply (metis ValOrd2.intros(7))
 
       
   649 apply(simp)
 
       
   650 apply(rule_tac x="Char char" in exI)
 
       
   651 apply(simp add: POSIXs_def)
 
       
   652 apply(rule conjI)
 
       
   653 apply (metis Prfs.intros(5))
 
       
   654 apply(auto)[1]
 
       
   655 apply(erule Prfs.cases)
 
       
   656 apply(simp_all)[5]
 
       
   657 apply (metis ValOrd2.intros)
 
       
   658 apply(auto simp add: Sequ_def)
 
       
   659 apply(drule meta_mp)
 
       
   660 apply (metis empty_iff)
 
       
   661 apply(drule meta_mp)
 
       
   662 apply (metis empty_iff)
 
       
   663 apply(auto)
 
       
   664 
       
   665 section {* POSIX for some constructors *}
 
   321 
   666 
   322 lemma POSIX_SEQ1:
 
   667 lemma POSIX_SEQ1:
 
   323   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
 
   668   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
 
   324   shows "POSIX v1 r1"
 
   669   shows "POSIX v1 r1"
 
   325 using assms
 
   670 using assms
 
   334 apply(erule ValOrd.cases)
 
   679 apply(erule ValOrd.cases)
 
   335 apply(simp_all)
 
   680 apply(simp_all)
 
   336 apply(clarify)
 
   681 apply(clarify)
 
   337 by (metis ValOrd_refl)
 
   682 by (metis ValOrd_refl)
 
   338 
   683 
       
   684 lemma POSIXn_SEQ1:
 
       
   685   assumes "POSIXn (Seq v1 v2) (SEQ r1 r2) (n1 + n2)" "\<TTurnstile>n1 v1 : r1" "\<TTurnstile>n2 v2 : r2"
 
       
   686   shows "POSIXn v1 r1 n1"
 
       
   687 using assms
 
       
   688 unfolding POSIXn_def
 
       
   689 apply(auto)
 
       
   690 apply(drule_tac x="Seq v' v2" in spec)
 
       
   691 apply(erule impE)
 
       
   692 apply(rule Prfn.intros)
 
       
   693 apply(simp)
 
       
   694 apply(simp)
 
       
   695 apply(erule ValOrd2.cases)
 
       
   696 apply(simp_all)
 
       
   697 apply(clarify)
 
       
   698 by (metis Ord1 Prfn_Prf ValOrd_refl)
 
       
   699 
       
   700 lemma POSIXs_SEQ1:
 
       
   701   assumes "POSIXs (Seq v1 v2) (SEQ r1 r2) (s1 @ s2)" "\<Turnstile>s1 v1 : r1" "\<Turnstile>s2 v2 : r2"
 
       
   702   shows "POSIXs v1 r1 s1"
 
       
   703 using assms
 
       
   704 unfolding POSIXs_def
 
       
   705 apply(auto)
 
       
   706 apply(drule_tac x="Seq v' v2" in spec)
 
       
   707 apply(erule impE)
 
       
   708 apply(rule Prfs.intros)
 
       
   709 apply(simp)
 
       
   710 apply(simp)
 
       
   711 apply(erule ValOrd2.cases)
 
       
   712 apply(simp_all)
 
       
   713 apply(clarify)
 
       
   714 by (metis Ord1 Prfs_Prf ValOrd_refl)
 
       
   715 
   339 lemma POSIX_SEQ2:
 
   716 lemma POSIX_SEQ2:
 
   340   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" 
   717   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" 
   341   shows "POSIX v2 r2"
 
   718   shows "POSIX v2 r2"
 
   342 using assms
 
   719 using assms
 
   343 unfolding POSIX_def
 
   720 unfolding POSIX_def
 
   350 apply(simp)
 
   727 apply(simp)
 
   351 apply(erule ValOrd.cases)
 
   728 apply(erule ValOrd.cases)
 
   352 apply(simp_all)
 
   729 apply(simp_all)
 
   353 done
 
   730 done
 
   354 
   731 
       
   732 lemma POSIXn_SEQ2:
 
       
   733   assumes "POSIXn (Seq v1 v2) (SEQ r1 r2) (n1 + n2)" "\<TTurnstile>n1 v1 : r1" "\<TTurnstile>n2 v2 : r2" 
       
   734   shows "POSIXn v2 r2 n2"
 
       
   735 using assms
 
       
   736 unfolding POSIXn_def
 
       
   737 apply(auto)
 
       
   738 apply(drule_tac x="Seq v1 v'" in spec)
 
       
   739 apply(erule impE)
 
       
   740 apply(rule Prfn.intros)
 
       
   741 apply(simp)
 
       
   742 apply(simp)
 
       
   743 apply(erule ValOrd2.cases)
 
       
   744 apply(simp_all)
 
       
   745 done
 
       
   746 
       
   747 lemma POSIXs_SEQ2:
 
       
   748   assumes "POSIXs (Seq v1 v2) (SEQ r1 r2) (s1 @ s2)" "\<Turnstile>s1 v1 : r1" "\<Turnstile>s2 v2 : r2" 
       
   749   shows "POSIXs v2 r2 s2"
 
       
   750 using assms
 
       
   751 unfolding POSIXs_def
 
       
   752 apply(auto)
 
       
   753 apply(drule_tac x="Seq v1 v'" in spec)
 
       
   754 apply(erule impE)
 
       
   755 apply(rule Prfs.intros)
 
       
   756 apply(simp)
 
       
   757 apply(simp)
 
       
   758 apply(erule ValOrd2.cases)
 
       
   759 apply(simp_all)
 
       
   760 done
 
       
   761 
   355 lemma POSIX_ALT2:
 
   762 lemma POSIX_ALT2:
 
   356   assumes "POSIX (Left v1) (ALT r1 r2)"
 
   763   assumes "POSIX (Left v1) (ALT r1 r2)"
 
   357   shows "POSIX v1 r1"
 
   764   shows "POSIX v1 r1"
 
   358 using assms
 
   765 using assms
 
   359 unfolding POSIX_def
 
   766 unfolding POSIX_def
 
   367 apply(auto)
 
   774 apply(auto)
 
   368 apply(erule ValOrd.cases)
 
   775 apply(erule ValOrd.cases)
 
   369 apply(simp_all)
 
   776 apply(simp_all)
 
   370 done
 
   777 done
 
   371 
   778 
       
   779 lemma POSIXn_ALT2:
 
       
   780   assumes "POSIXn (Left v1) (ALT r1 r2) n"
 
       
   781   shows "POSIXn v1 r1 n"
 
       
   782 using assms
 
       
   783 unfolding POSIXn_def
 
       
   784 apply(auto)
 
       
   785 apply(erule Prfn.cases)
 
       
   786 apply(simp_all)[5]
 
       
   787 apply(drule_tac x="Left v'" in spec)
 
       
   788 apply(drule mp)
 
       
   789 apply(rule Prfn.intros)
 
       
   790 apply(auto)
 
       
   791 apply(erule ValOrd2.cases)
 
       
   792 apply(simp_all)
 
       
   793 done
 
       
   794 
       
   795 lemma POSIXs_ALT2:
 
       
   796   assumes "POSIXs (Left v1) (ALT r1 r2) s"
 
       
   797   shows "POSIXs v1 r1 s"
 
       
   798 using assms
 
       
   799 unfolding POSIXs_def
 
       
   800 apply(auto)
 
       
   801 apply(erule Prfs.cases)
 
       
   802 apply(simp_all)[5]
 
       
   803 apply(drule_tac x="Left v'" in spec)
 
       
   804 apply(drule mp)
 
       
   805 apply(rule Prfs.intros)
 
       
   806 apply(auto)
 
       
   807 apply(erule ValOrd2.cases)
 
       
   808 apply(simp_all)
 
       
   809 done
 
       
   810 
   372 lemma POSIX_ALT1a:
 
   811 lemma POSIX_ALT1a:
 
   373   assumes "POSIX (Right v2) (ALT r1 r2)"
 
   812   assumes "POSIX (Right v2) (ALT r1 r2)"
 
   374   shows "POSIX v2 r2"
 
   813   shows "POSIX v2 r2"
 
   375 using assms
 
   814 using assms
 
   376 unfolding POSIX_def
 
   815 unfolding POSIX_def
 
   384 apply(auto)
 
   823 apply(auto)
 
   385 apply(erule ValOrd.cases)
 
   824 apply(erule ValOrd.cases)
 
   386 apply(simp_all)
 
   825 apply(simp_all)
 
   387 done
 
   826 done
 
   388 
   827 
       
   828 lemma POSIXn_ALT1a:
 
       
   829   assumes "POSIXn (Right v2) (ALT r1 r2) n"
 
       
   830   shows "POSIXn v2 r2 n"
 
       
   831 using assms
 
       
   832 unfolding POSIXn_def
 
       
   833 apply(auto)
 
       
   834 apply(erule Prfn.cases)
 
       
   835 apply(simp_all)[5]
 
       
   836 apply(drule_tac x="Right v'" in spec)
 
       
   837 apply(drule mp)
 
       
   838 apply(rule Prfn.intros)
 
       
   839 apply(auto)
 
       
   840 apply(erule ValOrd2.cases)
 
       
   841 apply(simp_all)
 
       
   842 done
 
       
   843 
       
   844 lemma POSIXs_ALT1a:
 
       
   845   assumes "POSIXs (Right v2) (ALT r1 r2) s"
 
       
   846   shows "POSIXs v2 r2 s"
 
       
   847 using assms
 
       
   848 unfolding POSIXs_def
 
       
   849 apply(auto)
 
       
   850 apply(erule Prfs.cases)
 
       
   851 apply(simp_all)[5]
 
       
   852 apply(drule_tac x="Right v'" in spec)
 
       
   853 apply(drule mp)
 
       
   854 apply(rule Prfs.intros)
 
       
   855 apply(auto)
 
       
   856 apply(erule ValOrd2.cases)
 
       
   857 apply(simp_all)
 
       
   858 done
 
       
   859 
   389 lemma POSIX_ALT1b:
 
   860 lemma POSIX_ALT1b:
 
   390   assumes "POSIX (Right v2) (ALT r1 r2)"
 
   861   assumes "POSIX (Right v2) (ALT r1 r2)"
 
   391   shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')"
 
   862   shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')"
 
   392 using assms
 
   863 using assms
 
   393 apply(drule_tac POSIX_ALT1a)
 
   864 apply(drule_tac POSIX_ALT1a)
 
   394 unfolding POSIX_def
 
   865 unfolding POSIX_def
 
   395 apply(auto)
 
   866 apply(auto)
 
   396 done
 
   867 done
 
   397 
   868 
       
   869 lemma POSIXn_ALT1b:
 
       
   870   assumes "POSIXn (Right v2) (ALT r1 r2) n"
 
       
   871   shows "(\<forall>v'. (\<TTurnstile>n v' : r2 \<longrightarrow> v2 2\<succ> v'))"
 
       
   872 using assms
 
       
   873 apply(drule_tac POSIXn_ALT1a)
 
       
   874 unfolding POSIXn_def
 
       
   875 apply(auto)
 
       
   876 done
 
       
   877 
       
   878 lemma POSIXs_ALT1b:
 
       
   879   assumes "POSIXs (Right v2) (ALT r1 r2) s"
 
       
   880   shows "(\<forall>v'. (\<Turnstile>s v' : r2 \<longrightarrow> v2 2\<succ> v'))"
 
       
   881 using assms
 
       
   882 apply(drule_tac POSIXs_ALT1a)
 
       
   883 unfolding POSIXs_def
 
       
   884 apply(auto)
 
       
   885 done
 
       
   886 
   398 lemma POSIX_ALT_I1:
 
   887 lemma POSIX_ALT_I1:
 
   399   assumes "POSIX v1 r1" 
   888   assumes "POSIX v1 r1" 
   400   shows "POSIX (Left v1) (ALT r1 r2)"
 
   889   shows "POSIX (Left v1) (ALT r1 r2)"
 
   401 using assms
 
   890 using assms
 
   402 unfolding POSIX_def
 
   891 unfolding POSIX_def
 
   409 apply(rule ValOrd.intros)
 
   898 apply(rule ValOrd.intros)
 
   410 apply(auto)
 
   899 apply(auto)
 
   411 apply(rule ValOrd.intros)
 
   900 apply(rule ValOrd.intros)
 
   412 by simp
 
   901 by simp
 
   413 
   902 
       
   903 lemma POSIXn_ALT_I1:
 
       
   904   assumes "POSIXn v1 r1 n" 
       
   905   shows "POSIXn (Left v1) (ALT r1 r2) n"
 
       
   906 using assms
 
       
   907 unfolding POSIXn_def
 
       
   908 apply(auto)
 
       
   909 apply (metis Prfn.intros(2))
 
       
   910 apply(rotate_tac 2)
 
       
   911 apply(erule Prfn.cases)
 
       
   912 apply(simp_all)[5]
 
       
   913 apply(auto)
 
       
   914 apply(rule ValOrd2.intros)
 
       
   915 apply(auto)
 
       
   916 apply(rule ValOrd2.intros)
 
       
   917 by (metis Prfn_flat order_refl)
 
       
   918 
       
   919 lemma POSIXs_ALT_I1:
 
       
   920   assumes "POSIXs v1 r1 s" 
       
   921   shows "POSIXs (Left v1) (ALT r1 r2) s"
 
       
   922 using assms
 
       
   923 unfolding POSIXs_def
 
       
   924 apply(auto)
 
       
   925 apply (metis Prfs.intros(2))
 
       
   926 apply(rotate_tac 2)
 
       
   927 apply(erule Prfs.cases)
 
       
   928 apply(simp_all)[5]
 
       
   929 apply(auto)
 
       
   930 apply(rule ValOrd2.intros)
 
       
   931 apply(auto)
 
       
   932 apply(rule ValOrd2.intros)
 
       
   933 by (metis Prfs_flat order_refl)
 
   414 
   934 
   415 lemma POSIX_ALT_I2:
 
   935 lemma POSIX_ALT_I2:
 
   416   assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
 
   936   assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
 
   417   shows "POSIX (Right v2) (ALT r1 r2)"
 
   937   shows "POSIX (Right v2) (ALT r1 r2)"
 
   418 using assms
 
   938 using assms
 
   425 apply(auto)
 
   945 apply(auto)
 
   426 apply(rule ValOrd.intros)
 
   946 apply(rule ValOrd.intros)
 
   427 apply metis
 
   947 apply metis
 
   428 done
 
   948 done
 
   429 
   949 
       
   950 lemma POSIXs_ALT_I2:
 
       
   951   assumes "POSIXs v2 r2 s" "\<forall>s' v'. \<Turnstile>s' v' : r1 \<longrightarrow> length s > length s'"
 
       
   952   shows "POSIXs (Right v2) (ALT r1 r2) s"
 
       
   953 using assms
 
       
   954 unfolding POSIXs_def
 
       
   955 apply(auto)
 
       
   956 apply (metis Prfs.intros)
 
       
   957 apply(rotate_tac 3)
 
       
   958 apply(erule Prfs.cases)
 
       
   959 apply(simp_all)[5]
 
       
   960 apply(auto)
 
       
   961 apply(rule ValOrd2.intros)
 
       
   962 apply metis
 
       
   963 done
 
       
   964 
   430 
   965 
   431 lemma 
   966 lemma 
   432   "\<lbrakk>POSIX (mkeps r2) r2; nullable r2; \<not> nullable r1\<rbrakk>
 
   967   "\<lbrakk>POSIX (mkeps r2) r2; nullable r2; \<not> nullable r1\<rbrakk>
 
   433    \<Longrightarrow> POSIX (val.Right (mkeps r2)) (ALT r1 r2)" 
   968    \<Longrightarrow> POSIX (Right (mkeps r2)) (ALT r1 r2)" 
   434 apply(auto simp add: POSIX_def)
 
   969 apply(auto simp add: POSIX_def)
 
   435 apply(rule Prf.intros(3))
 
   970 apply(rule Prf.intros(3))
 
   436 apply(auto)
 
   971 apply(auto)
 
   437 apply(rotate_tac 3)
 
   972 apply(rotate_tac 3)
 
   438 apply(erule Prf.cases)
 
   973 apply(erule Prf.cases)
 
   589 apply(auto)[1]
 
  1124 apply(auto)[1]
 
   590 apply(rule Prf.intros)
 
  1125 apply(rule Prf.intros)
 
   591 apply(auto)[2]
 
  1126 apply(auto)[2]
 
   592 done
 
  1127 done
 
   593 
  1128 
       
  1129 lemma v3s:
 
       
  1130   assumes "\<Turnstile>s v : der c r" shows "\<Turnstile>(c#s) (injval r c v) : r"
 
       
  1131 using assms
 
       
  1132 apply(induct arbitrary: s v rule: der.induct)
 
       
  1133 apply(simp)
 
       
  1134 apply(erule Prfs.cases)
 
       
  1135 apply(simp_all)[5]
 
       
  1136 apply(simp)
 
       
  1137 apply(erule Prfs.cases)
 
       
  1138 apply(simp_all)[5]
 
       
  1139 apply(case_tac "c = c'")
 
       
  1140 apply(simp)
 
       
  1141 apply(erule Prfs.cases)
 
       
  1142 apply(simp_all)[5]
 
       
  1143 apply (metis Prfs.intros(5))
 
       
  1144 apply(simp)
 
       
  1145 apply(erule Prfs.cases)
 
       
  1146 apply(simp_all)[5]
 
       
  1147 apply(simp)
 
       
  1148 apply(erule Prfs.cases)
 
       
  1149 apply(simp_all)[5]
 
       
  1150 apply (metis Prfs.intros(2))
 
       
  1151 apply (metis Prfs.intros(3))
 
       
  1152 apply(simp)
 
       
  1153 apply(case_tac "nullable r1")
 
       
  1154 apply(simp)
 
       
  1155 apply(erule Prfs.cases)
 
       
  1156 apply(simp_all)[5]
 
       
  1157 apply(auto)[1]
 
       
  1158 apply(erule Prfs.cases)
 
       
  1159 apply(simp_all)[5]
 
       
  1160 apply(auto)[1]
 
       
  1161 apply (metis Prfs.intros(1) append_Cons)
 
       
  1162 apply(auto)[1]
 
       
  1163 apply (metis Prfs.intros(1) append_Nil mkeps_nullable_s)
 
       
  1164 apply(simp)
 
       
  1165 apply(erule Prfs.cases)
 
       
  1166 apply(simp_all)[5]
 
       
  1167 apply(auto)[1]
 
       
  1168 by (metis Prfs.intros(1) append_Cons)
 
       
  1169 
       
  1170 lemma v3n:
 
       
  1171   assumes "\<TTurnstile>n v : der c r" shows "\<TTurnstile>(Suc n) (injval r c v) : r"
 
       
  1172 using assms
 
       
  1173 apply(induct arbitrary: n v rule: der.induct)
 
       
  1174 apply(simp)
 
       
  1175 apply(erule Prfn.cases)
 
       
  1176 apply(simp_all)[5]
 
       
  1177 apply(simp)
 
       
  1178 apply(erule Prfn.cases)
 
       
  1179 apply(simp_all)[5]
 
       
  1180 apply(case_tac "c = c'")
 
       
  1181 apply(simp)
 
       
  1182 apply(erule Prfn.cases)
 
       
  1183 apply(simp_all)[5]
 
       
  1184 apply (metis One_nat_def Prfn.intros(5))
 
       
  1185 apply(simp)
 
       
  1186 apply(erule Prfn.cases)
 
       
  1187 apply(simp_all)[5]
 
       
  1188 apply(simp)
 
       
  1189 apply(erule Prfn.cases)
 
       
  1190 apply(simp_all)[5]
 
       
  1191 apply (metis Prfn.intros(2))
 
       
  1192 apply (metis Prfn.intros(3))
 
       
  1193 apply(simp)
 
       
  1194 apply(case_tac "nullable r1")
 
       
  1195 apply(simp)
 
       
  1196 apply(erule Prfn.cases)
 
       
  1197 apply(simp_all)[5]
 
       
  1198 apply(auto)[1]
 
       
  1199 apply(erule Prfn.cases)
 
       
  1200 apply(simp_all)[5]
 
       
  1201 apply(auto)[1]
 
       
  1202 apply (metis Prfn.intros(1) add.commute add_Suc_right)
 
       
  1203 apply(auto)[1]
 
       
  1204 apply (metis Prfn.intros(1) mkeps_nullable_n plus_nat.add_0)
 
       
  1205 apply(simp)
 
       
  1206 apply(erule Prfn.cases)
 
       
  1207 apply(simp_all)[5]
 
       
  1208 apply(auto)[1]
 
       
  1209 by (metis Prfn.intros(1) add_Suc)
 
       
  1210 
   594 lemma v3_proj:
 
  1211 lemma v3_proj:
 
   595   assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
 
  1212   assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
 
   596   shows "\<turnstile> (projval r c v) : der c r"
 
  1213   shows "\<turnstile> (projval r c v) : der c r"
 
   597 using assms
 
  1214 using assms
 
   598 apply(induct rule: Prf.induct)
 
  1215 apply(induct rule: Prf.induct)
 
   618 apply(rule Prf.intros)
 
  1235 apply(rule Prf.intros)
 
   619 apply (metis Cons_eq_append_conv)
 
  1236 apply (metis Cons_eq_append_conv)
 
   620 apply(simp)
 
  1237 apply(simp)
 
   621 done
 
  1238 done
 
   622 
  1239 
       
  1240 lemma v3s_proj:
 
       
  1241   assumes "\<Turnstile>(c#s) v : r"
 
       
  1242   shows "\<Turnstile>s (projval r c v) : der c r"
 
       
  1243 using assms
 
       
  1244 apply(induct s\<equiv>"c#s" v r arbitrary: s rule: Prfs.induct)
 
       
  1245 prefer 4
 
       
  1246 apply(simp)
 
       
  1247 apply (metis Prfs.intros(4))
 
       
  1248 prefer 2
 
       
  1249 apply(simp)
 
       
  1250 apply (metis Prfs.intros(2))
 
       
  1251 prefer 2
 
       
  1252 apply(simp)
 
       
  1253 apply (metis Prfs.intros(3))
 
       
  1254 apply(auto)
 
       
  1255 apply(rule Prfs.intros)
 
       
  1256 apply (metis Prfs_flat append_Nil)
 
       
  1257 prefer 2
 
       
  1258 apply(rule Prfs.intros)
 
       
  1259 apply(subst (asm) append_eq_Cons_conv)
 
       
  1260 apply(auto)[1]
 
       
  1261 apply (metis Prfs_flat)
 
       
  1262 apply(rule Prfs.intros)
 
       
  1263 apply metis
 
       
  1264 apply(simp)
 
       
  1265 apply(subst (asm) append_eq_Cons_conv)
 
       
  1266 apply(auto)[1]
 
       
  1267 apply (metis Prf_flat_L Prfs_Prf nullable_correctness)
 
       
  1268 apply (metis Prfs_flat list.distinct(1))
 
       
  1269 apply(subst (asm) append_eq_Cons_conv)
 
       
  1270 apply(auto)[1]
 
       
  1271 apply (metis Prfs_flat)
 
       
  1272 by (metis Prfs.intros(1))
 
       
  1273 
   623 text {*
 
  1274 text {*
 
   624   The string behind the injection value is an added c
 
  1275   The string behind the injection value is an added c
 
   625 *}
 
  1276 *}
 
   626 
  1277 
       
  1278 lemma v4s:
 
       
  1279   assumes "\<Turnstile>s v : der c r" shows "flat (injval r c v) = c # (flat v)"
 
       
  1280 using assms
 
       
  1281 apply(induct arbitrary: s v rule: der.induct)
 
       
  1282 apply(simp)
 
       
  1283 apply(erule Prfs.cases)
 
       
  1284 apply(simp_all)[5]
 
       
  1285 apply(simp)
 
       
  1286 apply(erule Prfs.cases)
 
       
  1287 apply(simp_all)[5]
 
       
  1288 apply(simp)
 
       
  1289 apply(case_tac "c = c'")
 
       
  1290 apply(simp)
 
       
  1291 apply(auto)[1]
 
       
  1292 apply(erule Prfs.cases)
 
       
  1293 apply(simp_all)[5]
 
       
  1294 apply(simp)
 
       
  1295 apply(erule Prfs.cases)
 
       
  1296 apply(simp_all)[5]
 
       
  1297 apply(simp)
 
       
  1298 apply(erule Prfs.cases)
 
       
  1299 apply(simp_all)[5]
 
       
  1300 apply(simp)
 
       
  1301 apply(case_tac "nullable r1")
 
       
  1302 apply(simp)
 
       
  1303 apply(erule Prfs.cases)
 
       
  1304 apply(simp_all (no_asm_use))[5]
 
       
  1305 apply(auto)[1]
 
       
  1306 apply(erule Prfs.cases)
 
       
  1307 apply(simp_all)[5]
 
       
  1308 apply(clarify)
 
       
  1309 apply(simp only: injval.simps flat.simps)
 
       
  1310 apply(auto)[1]
 
       
  1311 apply (metis mkeps_flat)
 
       
  1312 apply(simp)
 
       
  1313 apply(erule Prfs.cases)
 
       
  1314 apply(simp_all)[5]
 
       
  1315 done
 
       
  1316 
   627 lemma v4:
 
  1317 lemma v4:
 
   628   assumes "\<turnstile> v : der c r" shows "flat (injval r c v) = c # (flat v)"
 
  1318   assumes "\<turnstile> v : der c r" shows "flat (injval r c v) = c # (flat v)"
 
   629 using assms
 
  1319 using assms
 
   630 apply(induct arbitrary: v rule: der.induct)
 
  1320 apply(induct arbitrary: v rule: der.induct)
 
   631 apply(simp)
 
  1321 apply(simp)
 
   660 apply (metis mkeps_flat)
 
  1350 apply (metis mkeps_flat)
 
   661 apply(simp)
 
  1351 apply(simp)
 
   662 apply(erule Prf.cases)
 
  1352 apply(erule Prf.cases)
 
   663 apply(simp_all)[5]
 
  1353 apply(simp_all)[5]
 
   664 done
 
  1354 done
 
       
  1355 
       
  1356 lemma v4_flats:
 
       
  1357   assumes "\<turnstile> v : der c r" "\<not>nullable r" shows "hd (flats (injval r c v)) \<noteq> []"
 
       
  1358 using assms
 
       
  1359 apply(induct arbitrary: v rule: der.induct)
 
       
  1360 apply(simp)
 
       
  1361 apply(erule Prf.cases)
 
       
  1362 apply(simp_all)[5]
 
       
  1363 apply(simp)
 
       
  1364 apply(case_tac "c = c'")
 
       
  1365 apply(simp)
 
       
  1366 apply(auto)[1]
 
       
  1367 apply(erule Prf.cases)
 
       
  1368 apply(simp_all)[5]
 
       
  1369 apply(simp)
 
       
  1370 apply(erule Prf.cases)
 
       
  1371 apply(simp_all)[5]
 
       
  1372 apply(simp)
 
       
  1373 apply(erule Prf.cases)
 
       
  1374 apply(simp_all)[5]
 
       
  1375 apply(simp)
 
       
  1376 apply(case_tac "nullable r1")
 
       
  1377 apply(simp)
 
       
  1378 apply(erule Prf.cases)
 
       
  1379 apply(simp_all)[5]
 
       
  1380 apply(auto)[1]
 
       
  1381 apply(erule Prf.cases)
 
       
  1382 apply(simp_all)[5]
 
       
  1383 apply(clarify)
 
       
  1384 oops
 
   665 
  1385 
   666 lemma v4_flat_left:
 
  1386 lemma v4_flat_left:
 
   667   assumes "\<turnstile> v : der c r" "\<not>(nullable_left r)" shows "flat_left (injval r c v) = c # (flat_left v)"
 
  1387   assumes "\<turnstile> v : der c r" "\<not>(nullable_left r)" shows "flat_left (injval r c v) = c # (flat_left v)"
 
   668 using assms
 
  1388 using assms
 
   669 apply(induct arbitrary: v rule: der.induct)
 
  1389 apply(induct arbitrary: v rule: der.induct)
 
   768 apply(erule Prf.cases)
 
  1488 apply(erule Prf.cases)
 
   769 apply(simp_all)[5]
 
  1489 apply(simp_all)[5]
 
   770 apply(erule Prf.cases)
 
  1490 apply(erule Prf.cases)
 
   771 apply(simp_all)[5]
 
  1491 apply(simp_all)[5]
 
   772 done
 
  1492 done
 
       
  1493 
       
  1494 lemma 
       
  1495   assumes "POSIXs v (der c r) s" 
       
  1496   shows "POSIXs (injval r c v) r (c # s)"
 
       
  1497 using assms
 
       
  1498 apply(induct c r arbitrary: v s rule: der.induct)
 
       
  1499 apply(auto simp add: POSIXs_def)[1]
 
       
  1500 apply(erule Prfs.cases)
 
       
  1501 apply(simp_all)[5]
 
       
  1502 apply(erule Prfs.cases)
 
       
  1503 apply(simp_all)[5]
 
       
  1504 apply(auto simp add: POSIXs_def)[1]
 
       
  1505 apply(erule Prfs.cases)
 
       
  1506 apply(simp_all)[5]
 
       
  1507 apply(erule Prfs.cases)
 
       
  1508 apply(simp_all)[5]
 
       
  1509 apply(case_tac "c = c'")
 
       
  1510 apply(auto simp add: POSIXs_def)[1]
 
       
  1511 apply(erule Prfs.cases)
 
       
  1512 apply(simp_all)[5]
 
       
  1513 apply (metis Prfs.intros(5))
 
       
  1514 apply(erule Prfs.cases)
 
       
  1515 apply(simp_all)[5]
 
       
  1516 apply(erule Prfs.cases)
 
       
  1517 apply(simp_all)[5]
 
       
  1518 apply (metis ValOrd2.intros(8))
 
       
  1519 apply(auto simp add: POSIXs_def)[1]
 
       
  1520 apply(erule Prfs.cases)
 
       
  1521 apply(simp_all)[5]
 
       
  1522 apply(erule Prfs.cases)
 
       
  1523 apply(simp_all)[5]
 
       
  1524 apply(frule Prfs_POSIX)
 
       
  1525 apply(drule conjunct1)
 
       
  1526 apply(erule Prfs.cases)
 
       
  1527 apply(simp_all)[5]
 
       
  1528 apply(rule POSIXs_ALT_I1)
 
       
  1529 apply (metis POSIXs_ALT2)
 
       
  1530 apply(rule POSIXs_ALT_I2)
 
       
  1531 apply (metis POSIXs_ALT1a)
 
       
  1532 apply(frule POSIXs_ALT1b)
 
       
  1533 apply(auto)
 
       
  1534 apply(frule POSIXs_ALT1a)
 
       
  1535 (* HERE *)
 
       
  1536 apply(auto)
 
       
  1537 apply(rule ccontr)
 
       
  1538 apply(simp)
 
       
  1539 apply(auto)[1]
 
       
  1540 apply(drule POSIXs_ALT1a)
 
       
  1541 thm ValOrd2.intros
 
       
  1542 
       
  1543 apply(simp (no_asm) add: POSIXs_def)
 
       
  1544 apply(auto)[1]
 
       
  1545 apply (metis POSIXs_def 
       
  1546 der.simps(4) v3s)
 
       
  1547 apply(subst (asm) (5) POSIXs_def)
 
       
  1548 apply(auto)[1]
 
       
  1549 apply(erule Prfs.cases)
 
       
  1550 apply(simp_all)[5]
 
       
  1551 apply(erule Prfs.cases)
 
       
  1552 apply(simp_all)[5]
 
       
  1553 apply(auto)[1]
 
       
  1554 apply(rule ValOrd2.intros)
 
       
  1555 apply(drule_tac x="v1a" in meta_spec)
 
       
  1556 apply(drule_tac x="sb" in meta_spec)
 
       
  1557 apply(drule_tac meta_mp)
 
       
  1558 defer
 
       
  1559 apply (metis POSIXs_def)
 
       
  1560 apply(auto)[1]
 
       
  1561 apply(rule ValOrd2.intros)
 
       
  1562 apply(subst v4)
 
       
  1563 apply (metis Prfs_Prf)
 
       
  1564 apply(simp)
 
       
  1565 apply(drule_tac x="Left (injval r1a c v1)" in spec)
 
       
  1566 apply(drule mp)
 
       
  1567 apply(rule Prfs.intros)
 
       
  1568 defer
 
       
  1569 apply(erule ValOrd2.cases)
 
       
  1570 apply(simp_all)[8] 
       
  1571 apply(clarify)
 
       
  1572 thm v4s
 
       
  1573 apply(subst (asm) v4s[of "sb"])
 
       
  1574 apply(assumption)
 
       
  1575 apply(simp)
 
       
  1576 apply(clarify)
 
       
  1577 apply(erule Prfs.cases)
 
       
  1578 apply(simp_all)[5]
 
       
  1579 apply(auto)[1]
 
       
  1580 apply(rule ValOrd2.intros)
 
       
  1581 apply(subst v4)
 
       
  1582 apply (metis Prfs_Prf)
 
       
  1583 apply(simp)
 
       
  1584 apply(drule_tac x="Right (injval r2a c v2)" in spec)
 
       
  1585 apply(drule mp)
 
       
  1586 apply(rule Prfs.intros)
 
       
  1587 defer
 
       
  1588 apply(erule ValOrd2.cases)
 
       
  1589 apply(simp_all)[8] 
       
  1590 apply(clarify)
 
       
  1591 apply(subst (asm) v4)
 
       
  1592 defer
 
       
  1593 apply(simp)
 
       
  1594 apply(rule ValOrd2.intros)
 
       
  1595 apply (metis POSIXs_ALT1a POSIXs_def Prfs.intros(3))
 
       
  1596 apply(case_tac "nullable r1")
 
       
  1597 apply(simp (no_asm) add: POSIXs_def)
 
       
  1598 apply(auto)[1]
 
       
  1599 apply(subst (asm) (6) POSIXs_def)
 
       
  1600 apply(auto)[1]
 
       
  1601 apply(erule Prfs.cases)
 
       
  1602 apply(simp_all)[5]
 
       
  1603 apply(clarify)
 
       
  1604 defer
 
       
  1605 apply (metis Prfs.intros(3) der.simps(5) injval.simps(6) v3s)
 
       
  1606 apply(erule Prfs.cases)
 
       
  1607 apply(simp_all)[5]
 
       
  1608 apply(clarify)
 
       
  1609 apply(subst (asm) (6) POSIXs_def)
 
       
  1610 apply(auto)[1]
 
       
  1611 apply(rotate_tac 7)
 
       
  1612 apply(erule Prfs.cases)
 
       
  1613 apply(simp_all)[5]
 
       
  1614 apply(clarify)
 
       
  1615 apply(simp)
 
       
  1616 apply(rotate_tac 8)
 
       
  1617 apply(erule Prfs.cases)
 
       
  1618 apply(simp_all)[5]
 
       
  1619 apply(clarify)
 
       
  1620 apply(rule ValOrd2.intros(2))
 
       
  1621 apply(drule_tac x="v1b" in meta_spec)
 
       
  1622 apply(drule_tac x="s1a" in meta_spec)
 
       
  1623 apply(drule meta_mp)
 
       
  1624 defer
 
       
  1625 apply(subst (asm) Cons_eq_append_conv)
 
       
  1626 apply(auto)
 
       
  1627 defer
 
       
  1628 defer
 
       
  1629 
       
  1630 
       
  1631 thm v4
 
   773 
  1632 
   774 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
 
  1633 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
 
   775 by (metis list.sel(3))
 
  1634 by (metis list.sel(3))
 
   776 
  1635 
   777 lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)"
 
  1636 lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)"
 
   785 | "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)"
 
  1644 | "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)"
 
   786 
  1645 
   787 lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])"
 
  1646 lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])"
 
   788 by (metis Prf_flat_L nullable_correctness)
 
  1647 by (metis Prf_flat_L nullable_correctness)
 
   789 
  1648 
   790 lemma proj_inj_id:
 
       
   791   assumes "\<turnstile> v : der c r" 
       
   792   shows "projval r c (injval r c v) = v"
 
       
   793 using assms
 
       
   794 apply(induct c r arbitrary: v rule: der.induct)
 
       
   795 apply(simp)
 
       
   796 apply(erule Prf.cases)
 
       
   797 apply(simp_all)[5]
 
       
   798 apply(simp)
 
       
   799 apply(erule Prf.cases)
 
       
   800 apply(simp_all)[5]
 
       
   801 apply(simp)
 
       
   802 apply(case_tac "c = c'")
 
       
   803 apply(simp)
 
       
   804 apply(erule Prf.cases)
 
       
   805 apply(simp_all)[5]
 
       
   806 apply(simp)
 
       
   807 apply(erule Prf.cases)
 
       
   808 apply(simp_all)[5]
 
       
   809 apply(simp)
 
       
   810 apply(erule Prf.cases)
 
       
   811 apply(simp_all)[5]
 
       
   812 apply(simp)
 
       
   813 apply(case_tac "nullable r1")
 
       
   814 apply(simp)
 
       
   815 apply(erule Prf.cases)
 
       
   816 apply(simp_all)[5]
 
       
   817 apply(auto)[1]
 
       
   818 apply(erule Prf.cases)
 
       
   819 apply(simp_all)[5]
 
       
   820 apply(auto)[1]
 
       
   821 apply (metis list.distinct(1) v4)
 
       
   822 apply(auto)[1]
 
       
   823 apply (metis mkeps_flat)
 
       
   824 apply(auto)
 
       
   825 apply(erule Prf.cases)
 
       
   826 apply(simp_all)[5]
 
       
   827 apply(auto)[1]
 
       
   828 apply(simp add: v4)
 
       
   829 done
 
       
   830 
  1649 
   831 lemma LeftRight:
 
  1650 lemma LeftRight:
 
   832   assumes "(Left v1) \<succ>(der c (ALT r1 r2)) (Right v2)"
 
  1651   assumes "(Left v1) \<succ>(der c (ALT r1 r2)) (Right v2)"
 
   833   and "\<turnstile> v1 : der c r1" "\<turnstile> v2 : der c r2" 
  1652   and "\<turnstile> v1 : der c r1" "\<turnstile> v2 : der c r2" 
   834   shows "(injval (ALT r1 r2) c (Left v1)) \<succ>(ALT r1 r2) (injval (ALT r1 r2) c (Right v2))"
 
  1653   shows "(injval (ALT r1 r2) c (Left v1)) \<succ>(ALT r1 r2) (injval (ALT r1 r2) c (Right v2))"
 
   908 apply(rule ValOrd.intros(2))
 
  1727 apply(rule ValOrd.intros(2))
 
   909 prefer 2
 
  1728 prefer 2
 
   910 apply (metis list.distinct(1) mkeps_flat v4)
 
  1729 apply (metis list.distinct(1) mkeps_flat v4)
 
   911 by (metis h)
 
  1730 by (metis h)
 
   912 
  1731 
       
  1732 lemma rr1: 
       
  1733   assumes "\<turnstile> v : r" "\<not>nullable r" 
       
  1734   shows "flat v \<noteq> []"
 
       
  1735 using assms
 
       
  1736 by (metis Prf_flat_L nullable_correctness)
 
       
  1737 
       
  1738 lemma rr2: "hd (flats v) \<noteq> [] \<Longrightarrow> flats v \<noteq> []"
 
       
  1739 apply(induct v)
 
       
  1740 apply(auto)
 
       
  1741 done
 
       
  1742 
       
  1743 lemma rr3: "flats v = [] \<Longrightarrow> flat v = []"
 
       
  1744 apply(induct v)
 
       
  1745 apply(auto)
 
       
  1746 done
 
       
  1747 
       
  1748 lemma POSIXs_der:
 
       
  1749   assumes "POSIXs v (der c r) s" "\<Turnstile>s v : der c r"
 
       
  1750   shows "POSIXs (injval r c v) r (c#s)"
 
       
  1751 using assms
 
       
  1752 unfolding POSIXs_def
 
       
  1753 apply(auto)
 
       
  1754 thm v3s 
       
  1755 apply (erule v3s)
 
       
  1756 apply(drule_tac x="projval r c v'" in spec)
 
       
  1757 apply(drule mp)
 
       
  1758 thm v3s_proj
 
       
  1759 apply(rule v3s_proj)
 
       
  1760 apply(simp)
 
       
  1761 thm v3s_proj
 
       
  1762 apply(drule v3s_proj)
 
       
  1763 oops
 
       
  1764 
       
  1765 lemma Prf_inj_test:
 
       
  1766   assumes "v1 2\<succ> v2" "\<Turnstile>s1 v1 : der c r" "\<Turnstile>s2 v2 : der c r"  
       
  1767   shows "(injval r c v1) 2\<succ>  (injval r c v2)"
 
       
  1768 using assms
 
       
  1769 apply(induct c r arbitrary: s1 s2 v1 v2 rule: der.induct)
 
       
  1770 (* NULL case *)
 
       
  1771 apply(erule Prfs.cases)
 
       
  1772 apply(simp_all)[5]
 
       
  1773 (* EMPTY case *)
 
       
  1774 apply(simp)
 
       
  1775 apply(erule Prfs.cases)
 
       
  1776 apply(simp_all)[5]
 
       
  1777 (* CHAR case *)
 
       
  1778 apply(case_tac "c = c'")
 
       
  1779 apply(simp)
 
       
  1780 apply(erule Prfs.cases)
 
       
  1781 apply(simp_all)[5]
 
       
  1782 apply(erule Prfs.cases)
 
       
  1783 apply(simp_all)[5]
 
       
  1784 apply(erule ValOrd2.cases)
 
       
  1785 apply(simp_all)[8]
 
       
  1786 apply(rule ValOrd2.intros)
 
       
  1787 apply(simp)
 
       
  1788 apply(erule Prfs.cases)
 
       
  1789 apply(simp_all)[5]
 
       
  1790 (* ALT case *)
 
       
  1791 apply(simp)
 
       
  1792 apply(erule Prfs.cases)
 
       
  1793 apply(simp_all)[5]
 
       
  1794 apply(auto)[2]
 
       
  1795 apply(erule Prfs.cases)
 
       
  1796 apply(simp_all)[5]
 
       
  1797 apply(auto)[2]
 
       
  1798 apply(erule ValOrd2.cases)
 
       
  1799 apply(simp_all)[8]
 
       
  1800 apply(rule ValOrd2.intros)
 
       
  1801 apply(auto)[1]
 
       
  1802 apply(erule ValOrd2.cases)
 
       
  1803 apply(simp_all)[8]
 
       
  1804 apply(rule ValOrd2.intros)
 
       
  1805 apply(subst v4)
 
       
  1806 apply (metis Prfs_Prf)
 
       
  1807 apply(subst v4)
 
       
  1808 apply (metis Prfs_Prf)
 
       
  1809 apply(simp)
 
       
  1810 apply(erule Prfs.cases)
 
       
  1811 apply(simp_all)[5]
 
       
  1812 apply(auto)[2]
 
       
  1813 apply(erule ValOrd2.cases)
 
       
  1814 apply(simp_all)[8]
 
       
  1815 apply(rule ValOrd2.intros)
 
       
  1816 apply(subst v4)
 
       
  1817 apply (metis Prfs_Prf)
 
       
  1818 apply(subst v4)
 
       
  1819 apply (metis Prfs_Prf)
 
       
  1820 apply(simp)
 
       
  1821 apply(erule ValOrd2.cases)
 
       
  1822 apply(simp_all)[8]
 
       
  1823 apply(rule ValOrd2.intros)
 
       
  1824 apply metis
 
       
  1825 (* SEQ case*)
 
       
  1826 apply(simp)
 
       
  1827 apply(case_tac "nullable r1")
 
       
  1828 apply(simp)
 
       
  1829 defer
 
       
  1830 apply(simp)
 
       
  1831 apply(erule Prfs.cases)
 
       
  1832 apply(simp_all)[5]
 
       
  1833 apply(erule Prfs.cases)
 
       
  1834 apply(simp_all)[5]
 
       
  1835 apply(clarify)
 
       
  1836 apply(erule ValOrd2.cases)
 
       
  1837 apply(simp_all)[8]
 
       
  1838 apply(clarify)
 
       
  1839 apply(rule ValOrd2.intros)
 
       
  1840 apply(simp)
 
       
  1841 apply(rule ValOrd2.intros)
 
       
  1842 apply(auto)[1]
 
       
  1843 defer
 
       
  1844 apply(erule Prfs.cases)
 
       
  1845 apply(simp_all)[5]
 
       
  1846 apply(erule Prfs.cases)
 
       
  1847 apply(simp_all)[5]
 
       
  1848 apply(clarify)
 
       
  1849 apply(erule Prfs.cases)
 
       
  1850 apply(simp_all)[5]
 
       
  1851 apply(erule Prfs.cases)
 
       
  1852 apply(simp_all)[5]
 
       
  1853 apply(clarify)
 
       
  1854 apply(erule ValOrd2.cases)
 
       
  1855 apply(simp_all)[8]
 
       
  1856 apply(clarify)
 
       
  1857 apply(erule ValOrd2.cases)
 
       
  1858 apply(simp_all)[8]
 
       
  1859 apply(clarify)
 
       
  1860 apply (metis ValOrd2.intros(1))
 
       
  1861 apply(rule ValOrd2.intros)
 
       
  1862 apply metis
 
       
  1863 defer
 
       
  1864 apply(clarify)
 
       
  1865 apply(simp)
 
       
  1866 apply(erule Prfs.cases)
 
       
  1867 apply(simp_all)[5]
 
       
  1868 apply(clarify)
 
       
  1869 apply(rule ValOrd2.intros)
 
       
  1870 apply(rule Ord1)
 
       
  1871 apply(rule h)
 
       
  1872 apply(simp)
 
       
  1873 apply(simp)
 
       
  1874 apply (metis Prfs_Prf)
 
       
  1875 defer
 
       
  1876 apply(erule Prfs.cases)
 
       
  1877 apply(simp_all)[5]
 
       
  1878 apply(clarify)
 
       
  1879 apply(rotate_tac 6)
 
       
  1880 apply(erule Prfs.cases)
 
       
  1881 apply(simp_all)[5]
 
       
  1882 apply(clarify)
 
       
  1883 apply(erule ValOrd2.cases)
 
       
  1884 apply(simp_all)[8]
 
       
  1885 apply(clarify)
 
       
  1886 apply(simp)
 
       
  1887 
       
  1888 apply(erule ValOrd2.cases)
 
       
  1889 apply(simp_all)[8]
 
       
  1890 apply(simp)
 
       
  1891 apply metis
 
       
  1892 using injval_inj
 
       
  1893 apply(simp add: inj_on_def)
 
       
  1894 apply metis
 
       
  1895 (* SEQ nullable case *)
 
       
  1896 apply(erule Prf.cases)
 
       
  1897 apply(simp_all)[5]
 
       
  1898 apply(clarify)
 
       
  1899 apply(erule Prf.cases)
 
       
  1900 apply(simp_all)[5]
 
       
  1901 apply(clarify)
 
       
  1902 apply(erule Prf.cases)
 
       
  1903 apply(simp_all)[5]
 
       
  1904 apply(clarify)
 
       
  1905 apply(erule Prf.cases)
 
       
  1906 apply(simp_all)[5]
 
       
  1907 apply(clarify)
 
       
  1908 apply(erule ValOrd.cases)
 
       
  1909 apply(simp_all)[8]
 
       
  1910 apply(clarify)
 
       
  1911 apply(erule ValOrd.cases)
 
       
  1912 apply(simp_all)[8]
 
       
  1913 apply(clarify)
 
       
  1914 apply(rule ValOrd.intros(1))
 
       
  1915 apply(simp)
 
       
  1916 apply(rule ValOrd.intros(2))
 
       
  1917 apply metis
 
       
  1918 using injval_inj
 
       
  1919 apply(simp add: inj_on_def)
 
       
  1920 apply metis
 
       
  1921 apply(clarify)
 
       
  1922 apply(simp)
 
       
  1923 apply(erule Prf.cases)
 
       
  1924 apply(simp_all)[5]
 
       
  1925 apply(clarify)
 
       
  1926 apply(erule ValOrd.cases)
 
       
  1927 apply(simp_all)[8]
 
       
  1928 apply(clarify)
 
       
  1929 apply(simp)
 
       
  1930 apply(rule ValOrd.intros(2))
 
       
  1931 apply (metis h)
 
       
  1932 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  1933 (* last case *)
 
       
  1934 apply(clarify)
 
       
  1935 apply(erule Prf.cases)
 
       
  1936 apply(simp_all)[5]
 
       
  1937 apply(clarify)
 
       
  1938 apply(rotate_tac 6)
 
       
  1939 apply(erule Prf.cases)
 
       
  1940 apply(simp_all)[5]
 
       
  1941 apply(clarify)
 
       
  1942 prefer 2
 
       
  1943 apply(clarify)
 
       
  1944 apply(erule ValOrd.cases)
 
       
  1945 apply(simp_all)[8]
 
       
  1946 apply(clarify)
 
       
  1947 apply(rule ValOrd.intros(1))
 
       
  1948 apply(metis)
 
       
  1949 apply(rule ValOrd.intros(2))
 
       
  1950 prefer 2
 
       
  1951 thm mkeps_flat v4
 
       
  1952 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  1953 oops
 
       
  1954 
       
  1955 
       
  1956 lemma Prf_inj_test:
 
       
  1957   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r"  
       
  1958           "flat v1 = flat v2"
 
       
  1959   shows "(injval r c v1) \<succ>r  (injval r c v2)"
 
       
  1960 using assms
 
       
  1961 apply(induct v1 arbitrary: r v2 taking: "length o flat" rule: measure_induct_rule)
 
       
  1962 apply(case_tac r)
 
       
  1963 (* NULL case *)
 
       
  1964 apply(simp)
 
       
  1965 apply(erule Prf.cases)
 
       
  1966 apply(simp_all)[5]
 
       
  1967 (* EMPTY case *)
 
       
  1968 apply(simp)
 
       
  1969 apply(erule Prf.cases)
 
       
  1970 apply(simp_all)[5]
 
       
  1971 (* CHAR case *)
 
       
  1972 apply(case_tac "c = char")
 
       
  1973 apply(simp)
 
       
  1974 apply(erule Prf.cases)
 
       
  1975 apply(simp_all)[5]
 
       
  1976 apply(erule Prf.cases)
 
       
  1977 apply(simp_all)[5]
 
       
  1978 apply (metis ValOrd.intros(8))
 
       
  1979 apply(simp)
 
       
  1980 apply(erule Prf.cases)
 
       
  1981 apply(simp_all)[5]
 
       
  1982 (* ALT case *)
 
       
  1983 prefer 2
 
       
  1984 apply(simp)
 
       
  1985 apply(erule Prf.cases)
 
       
  1986 apply(simp_all)[5]
 
       
  1987 apply(erule Prf.cases)
 
       
  1988 apply(simp_all)[5]
 
       
  1989 apply(clarify)
 
       
  1990 apply(erule ValOrd.cases)
 
       
  1991 apply(simp_all)[8]
 
       
  1992 apply(clarify)
 
       
  1993 apply (rule ValOrd.intros(6))
 
       
  1994 apply(drule_tac x="v1b" in meta_spec)
 
       
  1995 apply(drule_tac x="rexp1" in meta_spec)
 
       
  1996 apply(drule_tac x="v1'" in meta_spec)
 
       
  1997 apply(drule_tac meta_mp)
 
       
  1998 apply(assumption)
 
       
  1999 apply(drule_tac meta_mp)
 
       
  2000 apply(assumption)
 
       
  2001 apply(drule_tac meta_mp)
 
       
  2002 
       
  2003 apply(clarify)
 
       
  2004 apply(erule ValOrd.cases)
 
       
  2005 apply(simp_all)[8]
 
       
  2006 apply(clarify)
 
       
  2007 apply (metis ValOrd.intros(3) monoid_add_class.add.right_neutral order_refl v4)
 
       
  2008 apply(clarify)
 
       
  2009 apply(erule Prf.cases)
 
       
  2010 apply(simp_all)[5]
 
       
  2011 apply(clarify)
 
       
  2012 apply (metis RightLeft der.simps(4) injval.simps(2) injval.simps(3))
 
       
  2013 apply(clarify)
 
       
  2014 apply(erule ValOrd.cases)
 
       
  2015 apply(simp_all)[8]
 
       
  2016 apply(clarify)
 
       
  2017 apply (metis ValOrd.intros(5))
 
       
  2018 (* SEQ case *)
 
       
  2019 apply(simp)
 
       
  2020 apply(case_tac "nullable r1")
 
       
  2021 apply(simp)
 
       
  2022 defer
 
       
  2023 apply(simp)
 
       
  2024 apply(erule Prf.cases)
 
       
  2025 apply(simp_all)[5]
 
       
  2026 apply(erule Prf.cases)
 
       
  2027 apply(simp_all)[5]
 
       
  2028 apply(clarify)
 
       
  2029 apply(erule ValOrd.cases)
 
       
  2030 apply(simp_all)[8]
 
       
  2031 apply(clarify)
 
       
  2032 apply(rule ValOrd.intros)
 
       
  2033 apply(simp)
 
       
  2034 apply(clarify)
 
       
  2035 apply(rule ValOrd.intros(2))
 
       
  2036 apply(rotate_tac 2)
 
       
  2037 apply(drule_tac x="v1c" in meta_spec)
 
       
  2038 apply(rotate_tac 9)
 
       
  2039 apply(drule_tac x="v1'" in meta_spec)
 
       
  2040 apply(drule_tac meta_mp)
 
       
  2041 apply(assumption)
 
       
  2042 apply(drule_tac meta_mp)
 
       
  2043 apply(assumption)
 
       
  2044 apply(drule_tac meta_mp)
 
       
  2045 apply(assumption)
 
       
  2046 apply(drule_tac meta_mp)
 
       
  2047 apply(simp)
 
       
  2048 apply (metis POSIX_SEQ1)
 
       
  2049 apply(simp)
 
       
  2050 apply (metis proj_inj_id)
 
       
  2051 apply(erule Prf.cases)
 
       
  2052 apply(simp_all)[5]
 
       
  2053 apply(erule Prf.cases)
 
       
  2054 apply(simp_all)[5]
 
       
  2055 apply(clarify)
 
       
  2056 apply(rotate_tac 6)
 
       
  2057 apply(erule Prf.cases)
 
       
  2058 apply(simp_all)[5]
 
       
  2059 apply(erule Prf.cases)
 
       
  2060 apply(simp_all)[5]
 
       
  2061 apply(clarify)
 
       
  2062 apply(erule ValOrd.cases)
 
       
  2063 apply(simp_all)[8]
 
       
  2064 apply(clarify)
 
       
  2065 apply(erule ValOrd.cases)
 
       
  2066 apply(simp_all)[8]
 
       
  2067 apply(clarify)
 
       
  2068 apply(rule ValOrd.intros(1))
 
       
  2069 apply(simp)
 
       
  2070 apply(clarify)
 
       
  2071 apply (metis POSIX_ALT2 POSIX_SEQ1 ValOrd.intros(2) proj_inj_id)
 
       
  2072 apply(clarify)
 
       
  2073 apply(erule Prf.cases)
 
       
  2074 apply(simp_all)[5]
 
       
  2075 apply(clarify)
 
       
  2076 apply (metis Prf.intros(1) Prf.intros(2) ValOrd.intros(2) der.simps(5) h injval.simps(5) mkeps_flat proj_inj_id projval.simps(4) val.distinct(19))
 
       
  2077 apply(clarify)
 
       
  2078 apply(erule Prf.cases)
 
       
  2079 apply(simp_all)[5]
 
       
  2080 apply(clarify)
 
       
  2081 apply(rotate_tac 7)
 
       
  2082 apply(erule Prf.cases)
 
       
  2083 apply(simp_all)[5]
 
       
  2084 apply(clarify)
 
       
  2085 apply(erule ValOrd.cases)
 
       
  2086 apply(simp_all)[8]
 
       
  2087 apply(clarify)
 
       
  2088 apply(simp)
 
       
  2089 apply(drule POSIX_ALT1a)
 
       
  2090 apply(rule ValOrd.intros(2))
 
       
  2091 defer
 
       
  2092 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  2093 apply(rule ValOrd.intros(1))
 
       
  2094 apply(erule ValOrd.cases)
 
       
  2095 apply(simp_all)[8]
 
       
  2096 apply (metis POSIX_ALT1a)
 
       
  2097 
       
  2098 apply(clarify)
 
       
  2099 apply(erule ValOrd.cases)
 
       
  2100 apply(simp_all)[8]
 
       
  2101 apply(clarify)
 
       
  2102 apply(rule ValOrd.intros(1))
 
       
  2103 apply(simp)
 
       
  2104 
       
  2105 apply(subgoal_tac "flats v1c \<noteq> []")
 
       
  2106 
       
  2107 apply(simp)
 
       
  2108 apply(subst v4)
 
       
  2109 apply(simp)
 
       
  2110 apply(subst (asm) v4)
 
       
  2111 apply(simp)
 
       
  2112 apply(simp)
 
       
  2113 apply(simp add: prefix_def)
 
       
  2114 oops
 
       
  2115 
       
  2116 lemma Prf_inj:
 
       
  2117   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*)
 
       
  2118   shows "(injval r c v1) \<succ>r (injval r c v2)"
 
       
  2119 using assms
 
       
  2120 apply(induct c r arbitrary: v1 v2 rule: der.induct)
 
       
  2121 (* NULL case *)
 
       
  2122 apply(simp)
 
       
  2123 apply(erule ValOrd.cases)
 
       
  2124 apply(simp_all)[8]
 
       
  2125 (* EMPTY case *)
 
       
  2126 apply(simp)
 
       
  2127 apply(erule ValOrd.cases)
 
       
  2128 apply(simp_all)[8]
 
       
  2129 (* CHAR case *)
 
       
  2130 apply(case_tac "c = c'")
 
       
  2131 apply(simp)
 
       
  2132 apply(erule ValOrd.cases)
 
       
  2133 apply(simp_all)[8]
 
       
  2134 apply(rule ValOrd.intros)
 
       
  2135 apply(simp)
 
       
  2136 apply(erule ValOrd.cases)
 
       
  2137 apply(simp_all)[8]
 
       
  2138 (* ALT case *)
 
       
  2139 apply(simp)
 
       
  2140 apply(erule ValOrd.cases)
 
       
  2141 apply(simp_all)[8]
 
       
  2142 apply(rule ValOrd.intros)
 
       
  2143 apply(subst v4)
 
       
  2144 apply(clarify)
 
       
  2145 apply(rotate_tac 3)
 
       
  2146 apply(erule Prf.cases)
 
       
  2147 apply(simp_all)[5]
 
       
  2148 apply(subst v4)
 
       
  2149 apply(clarify)
 
       
  2150 apply(rotate_tac 2)
 
       
  2151 apply(erule Prf.cases)
 
       
  2152 apply(simp_all)[5]
 
       
  2153 apply(simp)
 
       
  2154 apply(rule ValOrd.intros)
 
       
  2155 apply(clarify)
 
       
  2156 apply(rotate_tac 3)
 
       
  2157 apply(erule Prf.cases)
 
       
  2158 apply(simp_all)[5]
 
       
  2159 apply(clarify)
 
       
  2160 apply(erule Prf.cases)
 
       
  2161 apply(simp_all)[5]
 
       
  2162 apply(clarify)
 
       
  2163 apply(subst v4)
 
       
  2164 apply(simp)
 
       
  2165 apply(subst v4)
 
       
  2166 apply(simp)
 
       
  2167 apply(simp)
 
       
  2168 apply(rule ValOrd.intros)
 
       
  2169 apply(clarify)
 
       
  2170 apply(erule Prf.cases)
 
       
  2171 apply(simp_all)[5]
 
       
  2172 apply(erule Prf.cases)
 
       
  2173 apply(simp_all)[5]
 
       
  2174 apply(rule ValOrd.intros)
 
       
  2175 apply(clarify)
 
       
  2176 apply(erule Prf.cases)
 
       
  2177 apply(simp_all)[5]
 
       
  2178 apply(erule Prf.cases)
 
       
  2179 apply(simp_all)[5]
 
       
  2180 (* SEQ case*)
 
       
  2181 apply(simp)
 
       
  2182 apply(case_tac "nullable r1")
 
       
  2183 apply(simp)
 
       
  2184 defer
 
       
  2185 apply(simp)
 
       
  2186 apply(erule Prf.cases)
 
       
  2187 apply(simp_all)[5]
 
       
  2188 apply(erule Prf.cases)
 
       
  2189 apply(simp_all)[5]
 
       
  2190 apply(clarify)
 
       
  2191 apply(erule ValOrd.cases)
 
       
  2192 apply(simp_all)[8]
 
       
  2193 apply(clarify)
 
       
  2194 apply(rule ValOrd.intros)
 
       
  2195 apply(simp)
 
       
  2196 apply(clarify)
 
       
  2197 apply(rule ValOrd.intros(2))
 
       
  2198 apply metis
 
       
  2199 using injval_inj
 
       
  2200 apply(simp add: inj_on_def)
 
       
  2201 apply metis
 
       
  2202 (* SEQ nullable case *)
 
       
  2203 apply(erule Prf.cases)
 
       
  2204 apply(simp_all)[5]
 
       
  2205 apply(clarify)
 
       
  2206 apply(erule Prf.cases)
 
       
  2207 apply(simp_all)[5]
 
       
  2208 apply(clarify)
 
       
  2209 apply(erule Prf.cases)
 
       
  2210 apply(simp_all)[5]
 
       
  2211 apply(clarify)
 
       
  2212 apply(erule Prf.cases)
 
       
  2213 apply(simp_all)[5]
 
       
  2214 apply(clarify)
 
       
  2215 apply(erule ValOrd.cases)
 
       
  2216 apply(simp_all)[8]
 
       
  2217 apply(clarify)
 
       
  2218 apply(erule ValOrd.cases)
 
       
  2219 apply(simp_all)[8]
 
       
  2220 apply(clarify)
 
       
  2221 apply(rule ValOrd.intros(1))
 
       
  2222 apply(simp)
 
       
  2223 apply(rule ValOrd.intros(2))
 
       
  2224 apply metis
 
       
  2225 using injval_inj
 
       
  2226 apply(simp add: inj_on_def)
 
       
  2227 apply metis
 
       
  2228 apply(clarify)
 
       
  2229 apply(simp)
 
       
  2230 apply(erule Prf.cases)
 
       
  2231 apply(simp_all)[5]
 
       
  2232 apply(clarify)
 
       
  2233 apply(erule ValOrd.cases)
 
       
  2234 apply(simp_all)[8]
 
       
  2235 apply(clarify)
 
       
  2236 apply(simp)
 
       
  2237 apply(rule ValOrd.intros(2))
 
       
  2238 apply (metis h)
 
       
  2239 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  2240 (* last case *)
 
       
  2241 apply(clarify)
 
       
  2242 apply(erule Prf.cases)
 
       
  2243 apply(simp_all)[5]
 
       
  2244 apply(clarify)
 
       
  2245 apply(rotate_tac 6)
 
       
  2246 apply(erule Prf.cases)
 
       
  2247 apply(simp_all)[5]
 
       
  2248 apply(clarify)
 
       
  2249 prefer 2
 
       
  2250 apply(clarify)
 
       
  2251 apply(erule ValOrd.cases)
 
       
  2252 apply(simp_all)[8]
 
       
  2253 apply(clarify)
 
       
  2254 apply(rule ValOrd.intros(1))
 
       
  2255 apply(metis)
 
       
  2256 apply(rule ValOrd.intros(2))
 
       
  2257 prefer 2
 
       
  2258 thm mkeps_flat v4
 
       
  2259 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  2260 oops
 
       
  2261 
       
  2262 
   913 lemma POSIX_der:
 
  2263 lemma POSIX_der:
 
   914   assumes "POSIX2 v (der c r)" "\<turnstile> v : der c r"
 
  2264   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
 
   915   shows "POSIX2 (injval r c v) r"
 
  2265   shows "POSIX (injval r c v) r"
 
   916 using assms
 
  2266 using assms
 
   917 unfolding POSIX2_def
 
  2267 unfolding POSIX_def
 
   918 apply(auto)
 
  2268 apply(auto)
 
   919 thm v3
 
  2269 thm v3
 
   920 apply (erule v3)
 
  2270 apply (erule v3)
 
   921 thm v4
 
  2271 thm v4
 
   922 apply(subst (asm) v4)
 
  2272 apply(subst (asm) v4)
 
   938 apply(rule_tac x="flat v" in exI)
 
  2288 apply(rule_tac x="flat v" in exI)
 
   939 apply(simp)
 
  2289 apply(simp)
 
   940 apply(simp)
 
  2290 apply(simp)
 
   941 oops
 
  2291 oops
 
   942 
  2292 
   943 
       
   944 lemma Prf_inj_test:
 
       
   945   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r"  "\<Turnstile> vs : rs" "flat v1 = flat v2"
 
       
   946   shows "Seqs (injval r c v1) vs \<succ>(SEQS r rs) Seqs (injval r c v2) vs"
 
       
   947 using assms
 
       
   948 apply(induct arbitrary: v1 v2 vs rs rule: der.induct)
 
       
   949 (* NULL case *)
 
       
   950 apply(simp)
 
       
   951 apply(erule ValOrd.cases)
 
       
   952 apply(simp_all)[8]
 
       
   953 (* EMPTY case *)
 
       
   954 apply(simp)
 
       
   955 apply(erule ValOrd.cases)
 
       
   956 apply(simp_all)[8]
 
       
   957 (* CHAR case *)
 
       
   958 apply(case_tac "c = c'")
 
       
   959 apply(simp)
 
       
   960 apply(erule Prf.cases)
 
       
   961 apply(simp_all)[5]
 
       
   962 apply(erule Prf.cases)
 
       
   963 apply(simp_all)[5]
 
       
   964 apply (metis ValOrd.intros(8))
 
       
   965 apply(simp)
 
       
   966 apply(erule Prf.cases)
 
       
   967 apply(simp_all)[5]
 
       
   968 (* ALT case *)
 
       
   969 apply(simp)
 
       
   970 apply(erule Prf.cases)
 
       
   971 apply(simp_all)[5]
 
       
   972 apply(erule Prf.cases)
 
       
   973 apply(simp_all)[5]
 
       
   974 apply(erule ValOrd.cases)
 
       
   975 apply(simp_all)[8]
 
       
   976 apply (metis ValOrd.intros(6))
 
       
   977 apply(erule ValOrd.cases)
 
       
   978 apply(simp_all)[8]
 
       
   979 apply (metis LeftRight ValOrd.intros(3) der.simps(4) injval.simps(2) injval.simps(3))
 
       
   980 apply(erule Prf.cases)
 
       
   981 apply(simp_all)[5]
 
       
   982 apply(erule ValOrd.cases)
 
       
   983 apply(simp_all)[8]
 
       
   984 apply (metis RightLeft ValOrd.intros(4) der.simps(4) injval.simps(2) injval.simps(3))
 
       
   985 apply(erule ValOrd.cases)
 
       
   986 apply(simp_all)[8]
 
       
   987 apply (metis ValOrd.intros(5))
 
       
   988 (* SEQ case *)
 
       
   989 apply(simp)
 
       
   990 apply(case_tac "nullable r1")
 
       
   991 apply(simp)
 
       
   992 defer
 
       
   993 apply(simp)
 
       
   994 apply(erule Prf.cases)
 
       
   995 apply(simp_all)[5]
 
       
   996 apply(erule Prf.cases)
 
       
   997 apply(simp_all)[5]
 
       
   998 apply(clarify)
 
       
   999 apply(erule ValOrd.cases)
 
       
  1000 apply(simp_all)[8]
 
       
  1001 apply(clarify)
 
       
  1002 apply(rule ValOrd.intros)
 
       
  1003 apply(simp)
 
       
  1004 apply(clarify)
 
       
  1005 apply(rule ValOrd.intros(2))
 
       
  1006 apply(rotate_tac 2)
 
       
  1007 apply(drule_tac x="v1c" in meta_spec)
 
       
  1008 apply(rotate_tac 10)
 
       
  1009 apply(drule_tac x="v1'" in meta_spec)
 
       
  1010 apply(drule_tac meta_mp)
 
       
  1011 apply(assumption)
 
       
  1012 apply(drule_tac meta_mp)
 
       
  1013 apply(assumption)
 
       
  1014 apply(drule_tac meta_mp)
 
       
  1015 apply(assumption)
 
       
  1016 apply(drule_tac meta_mp)
 
       
  1017 apply(simp)
 
       
  1018 apply(subst v4)
 
       
  1019 apply(simp)
 
       
  1020 apply(subst (asm) v4)
 
       
  1021 apply(simp)
 
       
  1022 apply(simp)
 
       
  1023 apply(simp add: prefix_def)
 
       
  1024 oops
 
       
  1025 
       
  1026 lemma Prf_inj:
 
       
  1027   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*)
 
       
  1028   shows "(injval r c v1) \<succ>r (injval r c v2)"
 
       
  1029 using assms
 
       
  1030 apply(induct c r arbitrary: v1 v2 rule: der.induct)
 
       
  1031 (* NULL case *)
 
       
  1032 apply(simp)
 
       
  1033 apply(erule ValOrd.cases)
 
       
  1034 apply(simp_all)[8]
 
       
  1035 (* EMPTY case *)
 
       
  1036 apply(simp)
 
       
  1037 apply(erule ValOrd.cases)
 
       
  1038 apply(simp_all)[8]
 
       
  1039 (* CHAR case *)
 
       
  1040 apply(case_tac "c = c'")
 
       
  1041 apply(simp)
 
       
  1042 apply(erule ValOrd.cases)
 
       
  1043 apply(simp_all)[8]
 
       
  1044 apply(rule ValOrd.intros)
 
       
  1045 apply(simp)
 
       
  1046 apply(erule ValOrd.cases)
 
       
  1047 apply(simp_all)[8]
 
       
  1048 (* ALT case *)
 
       
  1049 apply(simp)
 
       
  1050 apply(erule ValOrd.cases)
 
       
  1051 apply(simp_all)[8]
 
       
  1052 apply(rule ValOrd.intros)
 
       
  1053 apply(subst v4)
 
       
  1054 apply(clarify)
 
       
  1055 apply(rotate_tac 3)
 
       
  1056 apply(erule Prf.cases)
 
       
  1057 apply(simp_all)[5]
 
       
  1058 apply(subst v4)
 
       
  1059 apply(clarify)
 
       
  1060 apply(rotate_tac 2)
 
       
  1061 apply(erule Prf.cases)
 
       
  1062 apply(simp_all)[5]
 
       
  1063 apply(simp)
 
       
  1064 apply(rule ValOrd.intros)
 
       
  1065 apply(clarify)
 
       
  1066 apply(rotate_tac 3)
 
       
  1067 apply(erule Prf.cases)
 
       
  1068 apply(simp_all)[5]
 
       
  1069 apply(clarify)
 
       
  1070 apply(erule Prf.cases)
 
       
  1071 apply(simp_all)[5]
 
       
  1072 apply(clarify)
 
       
  1073 apply(subst v4)
 
       
  1074 apply(simp)
 
       
  1075 apply(subst v4)
 
       
  1076 apply(simp)
 
       
  1077 apply(simp)
 
       
  1078 apply(rule ValOrd.intros)
 
       
  1079 apply(clarify)
 
       
  1080 apply(erule Prf.cases)
 
       
  1081 apply(simp_all)[5]
 
       
  1082 apply(erule Prf.cases)
 
       
  1083 apply(simp_all)[5]
 
       
  1084 apply(rule ValOrd.intros)
 
       
  1085 apply(clarify)
 
       
  1086 apply(erule Prf.cases)
 
       
  1087 apply(simp_all)[5]
 
       
  1088 apply(erule Prf.cases)
 
       
  1089 apply(simp_all)[5]
 
       
  1090 (* SEQ case*)
 
       
  1091 apply(simp)
 
       
  1092 apply(case_tac "nullable r1")
 
       
  1093 apply(simp)
 
       
  1094 defer
 
       
  1095 apply(simp)
 
       
  1096 apply(erule Prf.cases)
 
       
  1097 apply(simp_all)[5]
 
       
  1098 apply(erule Prf.cases)
 
       
  1099 apply(simp_all)[5]
 
       
  1100 apply(clarify)
 
       
  1101 apply(erule ValOrd.cases)
 
       
  1102 apply(simp_all)[8]
 
       
  1103 apply(clarify)
 
       
  1104 apply(rule ValOrd.intros)
 
       
  1105 apply(simp)
 
       
  1106 apply(clarify)
 
       
  1107 apply(rule ValOrd.intros(2))
 
       
  1108 apply metis
 
       
  1109 using injval_inj
 
       
  1110 apply(simp add: inj_on_def)
 
       
  1111 apply metis
 
       
  1112 (* SEQ nullable case *)
 
       
  1113 apply(erule Prf.cases)
 
       
  1114 apply(simp_all)[5]
 
       
  1115 apply(clarify)
 
       
  1116 apply(erule Prf.cases)
 
       
  1117 apply(simp_all)[5]
 
       
  1118 apply(clarify)
 
       
  1119 apply(erule Prf.cases)
 
       
  1120 apply(simp_all)[5]
 
       
  1121 apply(clarify)
 
       
  1122 apply(erule Prf.cases)
 
       
  1123 apply(simp_all)[5]
 
       
  1124 apply(clarify)
 
       
  1125 apply(erule ValOrd.cases)
 
       
  1126 apply(simp_all)[8]
 
       
  1127 apply(clarify)
 
       
  1128 apply(erule ValOrd.cases)
 
       
  1129 apply(simp_all)[8]
 
       
  1130 apply(clarify)
 
       
  1131 apply(rule ValOrd.intros(1))
 
       
  1132 apply(simp)
 
       
  1133 apply(rule ValOrd.intros(2))
 
       
  1134 apply metis
 
       
  1135 using injval_inj
 
       
  1136 apply(simp add: inj_on_def)
 
       
  1137 apply metis
 
       
  1138 apply(clarify)
 
       
  1139 apply(simp)
 
       
  1140 apply(erule Prf.cases)
 
       
  1141 apply(simp_all)[5]
 
       
  1142 apply(clarify)
 
       
  1143 apply(erule ValOrd.cases)
 
       
  1144 apply(simp_all)[8]
 
       
  1145 apply(clarify)
 
       
  1146 apply(simp)
 
       
  1147 apply(rule ValOrd.intros(2))
 
       
  1148 apply (metis h)
 
       
  1149 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  1150 (* last case *)
 
       
  1151 apply(clarify)
 
       
  1152 apply(erule Prf.cases)
 
       
  1153 apply(simp_all)[5]
 
       
  1154 apply(clarify)
 
       
  1155 apply(rotate_tac 6)
 
       
  1156 apply(erule Prf.cases)
 
       
  1157 apply(simp_all)[5]
 
       
  1158 apply(clarify)
 
       
  1159 prefer 2
 
       
  1160 apply(clarify)
 
       
  1161 apply(erule ValOrd.cases)
 
       
  1162 apply(simp_all)[8]
 
       
  1163 apply(clarify)
 
       
  1164 apply(rule ValOrd.intros(1))
 
       
  1165 apply(metis)
 
       
  1166 apply(rule ValOrd.intros(2))
 
       
  1167 prefer 2
 
       
  1168 thm mkeps_flat v4
 
       
  1169 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  1170 oops
 
       
  1171 
       
  1172 
       
  1173 lemma POSIX_der:
 
  2293 lemma POSIX_der:
 
  1174   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
 
  2294   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
 
  1175   shows "POSIX (injval r c v) r"
 
  2295   shows "POSIX (injval r c v) r"
 
  1176 using assms
 
  2296 using assms
 
  1177 unfolding POSIX_def
 
  2297 apply(induct c r arbitrary: v rule: der.induct)
 
       
  2298 (* null case*)
 
       
  2299 apply(simp add: POSIX_def)
 
       
  2300 apply(auto)[1]
 
       
  2301 apply(erule Prf.cases)
 
       
  2302 apply(simp_all)[5]
 
       
  2303 apply(erule Prf.cases)
 
       
  2304 apply(simp_all)[5]
 
       
  2305 (* empty case *)
 
       
  2306 apply(simp add: POSIX_def)
 
       
  2307 apply(auto)[1]
 
       
  2308 apply(erule Prf.cases)
 
       
  2309 apply(simp_all)[5]
 
       
  2310 apply(erule Prf.cases)
 
       
  2311 apply(simp_all)[5]
 
       
  2312 (* char case *)
 
       
  2313 apply(simp add: POSIX_def)
 
       
  2314 apply(case_tac "c = c'")
 
       
  2315 apply(auto)[1]
 
       
  2316 apply(erule Prf.cases)
 
       
  2317 apply(simp_all)[5]
 
       
  2318 apply (metis Prf.intros(5))
 
       
  2319 apply(erule Prf.cases)
 
       
  2320 apply(simp_all)[5]
 
       
  2321 apply(erule Prf.cases)
 
       
  2322 apply(simp_all)[5]
 
       
  2323 apply (metis ValOrd.intros(8))
 
       
  2324 apply(auto)[1]
 
       
  2325 apply(erule Prf.cases)
 
       
  2326 apply(simp_all)[5]
 
       
  2327 apply(erule Prf.cases)
 
       
  2328 apply(simp_all)[5]
 
       
  2329 (* alt case *)
 
       
  2330 apply(erule Prf.cases)
 
       
  2331 apply(simp_all)[5]
 
       
  2332 apply(clarify)
 
       
  2333 apply(simp (no_asm) add: POSIX_def)
 
       
  2334 apply(auto)[1]
 
       
  2335 apply (metis Prf.intros(2) v3)
 
       
  2336 apply(rotate_tac 4)
 
       
  2337 apply(erule Prf.cases)
 
       
  2338 apply(simp_all)[5]
 
       
  2339 apply (metis POSIX_ALT2 POSIX_def ValOrd.intros(6))
 
       
  2340 apply (metis ValOrd.intros(3) order_refl)
 
       
  2341 apply(simp (no_asm) add: POSIX_def)
 
       
  2342 apply(auto)[1]
 
       
  2343 apply (metis Prf.intros(3) v3)
 
       
  2344 apply(rotate_tac 4)
 
       
  2345 apply(erule Prf.cases)
 
       
  2346 apply(simp_all)[5]
 
       
  2347 defer
 
       
  2348 apply (metis POSIX_ALT1a POSIX_def ValOrd.intros(5))
 
       
  2349 prefer 2
 
       
  2350 apply(subst (asm) (5) POSIX_def)
 
       
  2351 apply(auto)[1]
 
       
  2352 apply(rotate_tac 5)
 
       
  2353 apply(erule Prf.cases)
 
       
  2354 apply(simp_all)[5]
 
       
  2355 apply(rule ValOrd.intros)
 
       
  2356 apply(subst (asm) v4)
 
       
  2357 apply(simp)
 
       
  2358 apply(drule_tac x="Left (projval r1a c v1)" in spec)
 
       
  2359 apply(clarify)
 
       
  2360 apply(drule mp)
 
       
  2361 apply(rule conjI)
 
       
  2362 apply (metis Prf.intros(2) v3_proj)
 
       
  2363 apply(simp)
 
       
  2364 apply (metis v4_proj2)
 
       
  2365 apply(erule ValOrd.cases)
 
       
  2366 apply(simp_all)[8]
 
       
  2367 apply (metis less_not_refl v4_proj2)
 
       
  2368 (* seq case *)
 
       
  2369 apply(case_tac "nullable r1")
 
       
  2370 defer
 
       
  2371 apply(simp add: POSIX_def)
 
       
  2372 apply(auto)[1]
 
       
  2373 apply(erule Prf.cases)
 
       
  2374 apply(simp_all)[5]
 
       
  2375 apply (metis Prf.intros(1) v3)
 
       
  2376 apply(erule Prf.cases)
 
       
  2377 apply(simp_all)[5]
 
       
  2378 apply(erule Prf.cases)
 
       
  2379 apply(simp_all)[5]
 
       
  2380 apply(clarify)
 
       
  2381 apply(subst (asm) (3) v4)
 
       
  2382 apply(simp)
 
       
  2383 apply(simp)
 
       
  2384 apply(subgoal_tac "flat v1a \<noteq> []")
 
       
  2385 prefer 2
 
       
  2386 apply (metis Prf_flat_L nullable_correctness)
 
       
  2387 apply(subgoal_tac "\<exists>s. flat v1a = c # s")
 
       
  2388 prefer 2
 
       
  2389 apply (metis append_eq_Cons_conv)
 
       
  2390 apply(auto)[1]
 
       
  2391  
       
  2392 
  1178 apply(auto)
 
  2393 apply(auto)
 
  1179 thm v3
 
  2394 thm v3
 
  1180 apply (erule v3)
 
  2395 apply (erule v3)
 
  1181 thm v4
 
  2396 thm v4
 
  1182 apply(subst (asm) v4)
 
  2397 apply(subst (asm) v4)
 
  1198 apply(rule_tac x="flat v" in exI)
 
  2413 apply(rule_tac x="flat v" in exI)
 
  1199 apply(simp)
 
  2414 apply(simp)
 
  1200 apply(simp)
 
  2415 apply(simp)
 
  1201 oops
 
  2416 oops
 
  1202 
  2417 
  1203 lemma POSIX_der:
 
       
  1204   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
 
       
  1205   shows "POSIX (injval r c v) r"
 
       
  1206 using assms
 
       
  1207 apply(induct c r arbitrary: v rule: der.induct)
 
       
  1208 (* null case*)
 
       
  1209 apply(simp add: POSIX_def)
 
       
  1210 apply(auto)[1]
 
       
  1211 apply(erule Prf.cases)
 
       
  1212 apply(simp_all)[5]
 
       
  1213 apply(erule Prf.cases)
 
       
  1214 apply(simp_all)[5]
 
       
  1215 (* empty case *)
 
       
  1216 apply(simp add: POSIX_def)
 
       
  1217 apply(auto)[1]
 
       
  1218 apply(erule Prf.cases)
 
       
  1219 apply(simp_all)[5]
 
       
  1220 apply(erule Prf.cases)
 
       
  1221 apply(simp_all)[5]
 
       
  1222 (* char case *)
 
       
  1223 apply(simp add: POSIX_def)
 
       
  1224 apply(case_tac "c = c'")
 
       
  1225 apply(auto)[1]
 
       
  1226 apply(erule Prf.cases)
 
       
  1227 apply(simp_all)[5]
 
       
  1228 apply (metis Prf.intros(5))
 
       
  1229 apply(erule Prf.cases)
 
       
  1230 apply(simp_all)[5]
 
       
  1231 apply(erule Prf.cases)
 
       
  1232 apply(simp_all)[5]
 
       
  1233 apply (metis ValOrd.intros(8))
 
       
  1234 apply(auto)[1]
 
       
  1235 apply(erule Prf.cases)
 
       
  1236 apply(simp_all)[5]
 
       
  1237 apply(erule Prf.cases)
 
       
  1238 apply(simp_all)[5]
 
       
  1239 (* alt case *)
 
       
  1240 apply(erule Prf.cases)
 
       
  1241 apply(simp_all)[5]
 
       
  1242 apply(clarify)
 
       
  1243 apply(simp (no_asm) add: POSIX_def)
 
       
  1244 apply(auto)[1]
 
       
  1245 apply (metis Prf.intros(2) v3)
 
       
  1246 apply(rotate_tac 4)
 
       
  1247 apply(erule Prf.cases)
 
       
  1248 apply(simp_all)[5]
 
       
  1249 apply (metis POSIX_ALT2 POSIX_def ValOrd.intros(6))
 
       
  1250 apply (metis ValOrd.intros(3) order_refl)
 
       
  1251 apply(simp (no_asm) add: POSIX_def)
 
       
  1252 apply(auto)[1]
 
       
  1253 apply (metis Prf.intros(3) v3)
 
       
  1254 apply(rotate_tac 4)
 
       
  1255 apply(erule Prf.cases)
 
       
  1256 apply(simp_all)[5]
 
       
  1257 defer
 
       
  1258 apply (metis POSIX_ALT1a POSIX_def ValOrd.intros(5))
 
       
  1259 prefer 2
 
       
  1260 apply(subst (asm) (5) POSIX_def)
 
       
  1261 apply(auto)[1]
 
       
  1262 apply(rotate_tac 5)
 
       
  1263 apply(erule Prf.cases)
 
       
  1264 apply(simp_all)[5]
 
       
  1265 apply(rule ValOrd.intros)
 
       
  1266 apply(subst (asm) v4)
 
       
  1267 apply(simp)
 
       
  1268 apply(drule_tac x="Left (projval r1a c v1)" in spec)
 
       
  1269 apply(clarify)
 
       
  1270 apply(drule mp)
 
       
  1271 apply(rule conjI)
 
       
  1272 apply (metis Prf.intros(2) v3_proj)
 
       
  1273 apply(simp)
 
       
  1274 apply (metis v4_proj2)
 
       
  1275 apply(erule ValOrd.cases)
 
       
  1276 apply(simp_all)[8]
 
       
  1277 apply (metis less_not_refl v4_proj2)
 
       
  1278 (* seq case *)
 
       
  1279 apply(case_tac "nullable r1")
 
       
  1280 defer
 
       
  1281 apply(simp add: POSIX_def)
 
       
  1282 apply(auto)[1]
 
       
  1283 apply(erule Prf.cases)
 
       
  1284 apply(simp_all)[5]
 
       
  1285 apply (metis Prf.intros(1) v3)
 
       
  1286 apply(erule Prf.cases)
 
       
  1287 apply(simp_all)[5]
 
       
  1288 apply(erule Prf.cases)
 
       
  1289 apply(simp_all)[5]
 
       
  1290 apply(clarify)
 
       
  1291 apply(subst (asm) (3) v4)
 
       
  1292 apply(simp)
 
       
  1293 apply(simp)
 
       
  1294 apply(subgoal_tac "flat v1a \<noteq> []")
 
       
  1295 prefer 2
 
       
  1296 apply (metis Prf_flat_L nullable_correctness)
 
       
  1297 apply(subgoal_tac "\<exists>s. flat v1a = c # s")
 
       
  1298 prefer 2
 
       
  1299 apply (metis append_eq_Cons_conv)
 
       
  1300 apply(auto)[1]
 
       
  1301  
       
  1302 
       
  1303 apply(auto)
 
       
  1304 thm v3
 
       
  1305 apply (erule v3)
 
       
  1306 thm v4
 
       
  1307 apply(subst (asm) v4)
 
       
  1308 apply(assumption)
 
       
  1309 apply(drule_tac x="projval r c v'" in spec)
 
       
  1310 apply(drule mp)
 
       
  1311 apply(rule conjI)
 
       
  1312 thm v3_proj
 
       
  1313 apply(rule v3_proj)
 
       
  1314 apply(simp)
 
       
  1315 apply(rule_tac x="flat v" in exI)
 
       
  1316 apply(simp)
 
       
  1317 thm t
 
       
  1318 apply(rule_tac c="c" in  t)
 
       
  1319 apply(simp)
 
       
  1320 thm v4_proj
 
       
  1321 apply(subst v4_proj)
 
       
  1322 apply(simp)
 
       
  1323 apply(rule_tac x="flat v" in exI)
 
       
  1324 apply(simp)
 
       
  1325 apply(simp)
 
       
  1326 oops
 
       
  1327 
       
  1328 
  2418 
  1329 lemma POSIX_ex: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r"
 
  2419 lemma POSIX_ex: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r"
 
  1330 apply(induct r arbitrary: v)
 
  2420 apply(induct r arbitrary: v)
 
  1331 apply(erule Prf.cases)
 
  2421 apply(erule Prf.cases)
 
  1332 apply(simp_all)[5]
 
  2422 apply(simp_all)[5]
 
  1418 apply(simp)
 
  2508 apply(simp)
 
  1419 apply(drule_tac x="Seq v va" in spec)
 
  2509 apply(drule_tac x="Seq v va" in spec)
 
  1420 apply(drule mp)
 
  2510 apply(drule mp)
 
  1421 defer
 
  2511 defer
 
  1422 apply (metis Prf.intros(1))
 
  2512 apply (metis Prf.intros(1))
 
  1423 
       
  1424 
       
  1425 oops
 
  2513 oops
 
  1426 
  2514 
  1427 lemma POSIX_ALT_cases:
 
  2515 lemma POSIX_ALT_cases:
 
  1428   assumes "\<turnstile> v : (ALT r1 r2)" "POSIX v (ALT r1 r2)"
 
  2516   assumes "\<turnstile> v : (ALT r1 r2)" "POSIX v (ALT r1 r2)"
 
  1429   shows "(\<exists>v1. v = Left v1 \<and> POSIX v1 r1) \<or> (\<exists>v2. v = Right v2 \<and> POSIX v2 r2)"
 
  2517   shows "(\<exists>v1. v = Left v1 \<and> POSIX v1 r1) \<or> (\<exists>v2. v = Right v2 \<and> POSIX v2 r2)"
lexing