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 81 7ac7782a7318
parent 79 ca8f9645db69
equal deleted inserted replaced
80:85ef42888929 81:7ac7782a7318 
     1    
     1    
     2 theory Re1
 
     2 theory Re1
 
     3   imports "Main" 
     3   imports "Main" 
     4 begin
 
     4 begin
 
       
     5 
     5 
     6 
     6 section {* Sequential Composition of Sets *}
 
     7 section {* Sequential Composition of Sets *}
 
     7 
     8 
     8 definition
 
     9 definition
 
     9   Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
 
    10   Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
 
    81 | Seq val val
 
    82 | Seq val val
 
    82 | Right val
 
    83 | Right val
 
    83 | Left val
 
    84 | Left val
 
    84 
    85 
    85 
    86 
       
    87 fun Seqs :: "val \<Rightarrow> val list \<Rightarrow> val"
 
       
    88 where
 
       
    89   "Seqs v [] = v"
 
       
    90 | "Seqs v (v'#vs) = Seqs (Seq v v') vs"
 
       
    91 
    86 section {* The string behind a value *}
 
    92 section {* The string behind a value *}
 
    87 
    93 
    88 fun flat :: "val \<Rightarrow> string"
 
    94 fun flat :: "val \<Rightarrow> string"
 
    89 where
 
    95 where
 
    90   "flat(Void) = []"
 
    96   "flat(Void) = []"
 
   163 lemma Prfs_Prf:
 
   169 lemma Prfs_Prf:
 
   164   shows "\<Turnstile>s v : r \<Longrightarrow> \<turnstile> v : r"
 
   170   shows "\<Turnstile>s v : r \<Longrightarrow> \<turnstile> v : r"
 
   165 apply(induct s v r rule: Prfs.induct)
 
   171 apply(induct s v r rule: Prfs.induct)
 
   166 apply(auto intro: Prf.intros)
 
   172 apply(auto intro: Prf.intros)
 
   167 done
 
   173 done
 
       
   174 
       
   175 lemma not_nullable_flat:
 
       
   176   assumes "\<turnstile> v : r" "\<not>nullable r"
 
       
   177   shows "flat v \<noteq> []"
 
       
   178 using assms
 
       
   179 apply(induct)
 
       
   180 apply(auto)
 
       
   181 done
 
       
   182 
   168 
   183 
   169 fun mkeps :: "rexp \<Rightarrow> val"
 
   184 fun mkeps :: "rexp \<Rightarrow> val"
 
   170 where
 
   185 where
 
   171   "mkeps(EMPTY) = Void"
 
   186   "mkeps(EMPTY) = Void"
 
   172 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
 
   187 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
 
   230 apply(erule Prf.cases)
 
   245 apply(erule Prf.cases)
 
   231 apply(auto)
 
   246 apply(auto)
 
   232 done
 
   247 done
 
   233 
   248 
   234 
   249 
   235 
   250 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100)
 
   236 section {* Ordering of values *}
 
   251 where
 
       
   252   "s1 \<sqsubseteq> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"
 
       
   253 
       
   254 definition sprefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
 
       
   255 where
 
       
   256   "s1 \<sqsubset> s2 \<equiv> (s1 \<sqsubseteq> s2 \<and> s1 \<noteq> s2)"
 
       
   257 
       
   258 lemma length_sprefix:
 
       
   259   "s1 \<sqsubset> s2 \<Longrightarrow> length s1 < length s2"
 
       
   260 unfolding sprefix_def prefix_def
 
       
   261 by (auto)
 
       
   262 
       
   263 definition Prefixes :: "string \<Rightarrow> string set" where
 
       
   264   "Prefixes s \<equiv> {sp. sp \<sqsubseteq> s}"
 
       
   265 
       
   266 definition Suffixes :: "string \<Rightarrow> string set" where
 
       
   267   "Suffixes s \<equiv> rev ` (Prefixes (rev s))"
 
       
   268 
       
   269 lemma Suffixes_in: 
       
   270   "\<exists>s1. s1 @ s2 = s3 \<Longrightarrow> s2 \<in> Suffixes s3"
 
       
   271 unfolding Suffixes_def Prefixes_def prefix_def image_def
 
       
   272 apply(auto)
 
       
   273 by (metis rev_rev_ident)
 
       
   274 
       
   275 lemma Prefixes_Cons:
 
       
   276   "Prefixes (c # s) = {[]} \<union> {c # sp | sp. sp \<in> Prefixes s}"
 
       
   277 unfolding Prefixes_def prefix_def
 
       
   278 apply(auto simp add: append_eq_Cons_conv) 
       
   279 done
 
       
   280 
       
   281 lemma finite_Prefixes:
 
       
   282   "finite (Prefixes s)"
 
       
   283 apply(induct s)
 
       
   284 apply(auto simp add: Prefixes_def prefix_def)[1]
 
       
   285 apply(simp add: Prefixes_Cons)
 
       
   286 done
 
       
   287 
       
   288 lemma finite_Suffixes:
 
       
   289   "finite (Suffixes s)"
 
       
   290 unfolding Suffixes_def
 
       
   291 apply(rule finite_imageI)
 
       
   292 apply(rule finite_Prefixes)
 
       
   293 done
 
       
   294 
       
   295 lemma prefix_Cons:
 
       
   296   "((c # s1) \<sqsubseteq> (c # s2)) = (s1 \<sqsubseteq> s2)"
 
       
   297 apply(auto simp add: prefix_def)
 
       
   298 done
 
       
   299 
       
   300 lemma prefix_append:
 
       
   301   "((s @ s1) \<sqsubseteq> (s @ s2)) = (s1 \<sqsubseteq> s2)"
 
       
   302 apply(induct s)
 
       
   303 apply(simp)
 
       
   304 apply(simp add: prefix_Cons)
 
       
   305 done
 
       
   306 
       
   307 
       
   308 
       
   309 definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
 
       
   310   "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}"
 
       
   311 
       
   312 definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where
 
       
   313   "rest v s \<equiv> drop (length (flat v)) s"
 
       
   314 
       
   315 lemma rest_Suffixes:
 
       
   316   "rest v s \<in> Suffixes s"
 
       
   317 unfolding rest_def
 
       
   318 by (metis Suffixes_in append_take_drop_id)
 
       
   319 
       
   320 
       
   321 lemma Values_recs:
 
       
   322   "Values (NULL) s = {}"
 
       
   323   "Values (EMPTY) s = {Void}"
 
       
   324   "Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
       
   325   "Values (ALT r1 r2) s = {Left v | v. v \<in> Values r1 s} \<union> {Right v | v. v \<in> Values r2 s}"
 
       
   326   "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}"
 
       
   327 unfolding Values_def
 
       
   328 apply(auto)
 
       
   329 (*NULL*)
 
       
   330 apply(erule Prf.cases)
 
       
   331 apply(simp_all)[5]
 
       
   332 (*EMPTY*)
 
       
   333 apply(erule Prf.cases)
 
       
   334 apply(simp_all)[5]
 
       
   335 apply(rule Prf.intros)
 
       
   336 apply (metis append_Nil prefix_def)
 
       
   337 (*CHAR*)
 
       
   338 apply(erule Prf.cases)
 
       
   339 apply(simp_all)[5]
 
       
   340 apply(rule Prf.intros)
 
       
   341 apply(erule Prf.cases)
 
       
   342 apply(simp_all)[5]
 
       
   343 (*ALT*)
 
       
   344 apply(erule Prf.cases)
 
       
   345 apply(simp_all)[5]
 
       
   346 apply (metis Prf.intros(2))
 
       
   347 apply (metis Prf.intros(3))
 
       
   348 (*SEQ*)
 
       
   349 apply(erule Prf.cases)
 
       
   350 apply(simp_all)[5]
 
       
   351 apply (simp add: append_eq_conv_conj prefix_def rest_def)
 
       
   352 apply (metis Prf.intros(1))
 
       
   353 apply (simp add: append_eq_conv_conj prefix_def rest_def)
 
       
   354 done
 
       
   355 
       
   356 lemma Values_finite:
 
       
   357   "finite (Values r s)"
 
       
   358 apply(induct r arbitrary: s)
 
       
   359 apply(simp_all add: Values_recs)
 
       
   360 thm finite_surj
 
       
   361 apply(rule_tac f="\<lambda>(x, y). Seq x y" and 
       
   362                A="{(v1, v2) | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}" in finite_surj)
 
       
   363 prefer 2
 
       
   364 apply(auto)[1]
 
       
   365 apply(rule_tac B="\<Union>sp \<in> Suffixes s. {(v1, v2). v1 \<in> Values r1 s \<and> v2 \<in> Values r2 sp}" in finite_subset)
 
       
   366 apply(auto)[1]
 
       
   367 apply (metis rest_Suffixes)
 
       
   368 apply(rule finite_UN_I)
 
       
   369 apply(rule finite_Suffixes)
 
       
   370 apply(simp)
 
       
   371 done
 
       
   372 
       
   373 section {* Greedy Ordering according to Frisch/Cardelli *}
 
       
   374 
       
   375 inductive GrOrd :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ \<prec> _")
 
       
   376 where 
       
   377   "v1 \<prec> v1' \<Longrightarrow> (Seq v1 v2) \<prec> (Seq v1' v2')"
 
       
   378 | "v2 \<prec> v2' \<Longrightarrow> (Seq v1 v2) \<prec> (Seq v1 v2')"
 
       
   379 | "v1 \<prec> v2 \<Longrightarrow> (Left v1) \<prec> (Left v2)"
 
       
   380 | "v1 \<prec> v2 \<Longrightarrow> (Right v1) \<prec> (Right v2)"
 
       
   381 | "(Right v1) \<prec> (Left v2)"
 
       
   382 | "(Char c) \<prec> (Char c)"
 
       
   383 | "(Void) \<prec> (Void)"
 
       
   384 
       
   385 lemma Gr_refl:
 
       
   386   assumes "\<turnstile> v : r"
 
       
   387   shows "v \<prec> v"
 
       
   388 using assms
 
       
   389 apply(induct)
 
       
   390 apply(auto intro: GrOrd.intros)
 
       
   391 done
 
       
   392 
       
   393 lemma Gr_total:
 
       
   394   assumes "\<turnstile> v1 : r" "\<turnstile> v2 : r"
 
       
   395   shows "v1 \<prec> v2 \<or> v2 \<prec> v1"
 
       
   396 using assms
 
       
   397 apply(induct v1 r arbitrary: v2 rule: Prf.induct)
 
       
   398 apply(rotate_tac 4)
 
       
   399 apply(erule Prf.cases)
 
       
   400 apply(simp_all)[5]
 
       
   401 apply(clarify)
 
       
   402 apply (metis GrOrd.intros(1) GrOrd.intros(2))
 
       
   403 apply(rotate_tac 2)
 
       
   404 apply(erule Prf.cases)
 
       
   405 apply(simp_all)
 
       
   406 apply(clarify)
 
       
   407 apply (metis GrOrd.intros(3))
 
       
   408 apply(clarify)
 
       
   409 apply (metis GrOrd.intros(5))
 
       
   410 apply(rotate_tac 2)
 
       
   411 apply(erule Prf.cases)
 
       
   412 apply(simp_all)
 
       
   413 apply(clarify)
 
       
   414 apply (metis GrOrd.intros(5))
 
       
   415 apply(clarify)
 
       
   416 apply (metis GrOrd.intros(4))
 
       
   417 apply(erule Prf.cases)
 
       
   418 apply(simp_all)
 
       
   419 apply (metis GrOrd.intros(7))
 
       
   420 apply(erule Prf.cases)
 
       
   421 apply(simp_all)
 
       
   422 apply (metis GrOrd.intros(6))
 
       
   423 done
 
       
   424 
       
   425 lemma Gr_trans: 
       
   426   assumes "v1 \<prec> v2" "v2 \<prec> v3" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<turnstile> v3 : r"
 
       
   427   shows "v1 \<prec> v3"
 
       
   428 using assms
 
       
   429 apply(induct r arbitrary: v1 v2 v3)
 
       
   430 apply(erule Prf.cases)
 
       
   431 apply(simp_all)[5]
 
       
   432 apply(erule Prf.cases)
 
       
   433 apply(simp_all)[5]
 
       
   434 apply(erule Prf.cases)
 
       
   435 apply(simp_all)[5]
 
       
   436 apply(erule Prf.cases)
 
       
   437 apply(simp_all)[5]
 
       
   438 apply(erule Prf.cases)
 
       
   439 apply(simp_all)[5]
 
       
   440 defer
 
       
   441 (* ALT case *)
 
       
   442 apply(erule Prf.cases)
 
       
   443 apply(simp_all (no_asm_use))[5]
 
       
   444 apply(erule Prf.cases)
 
       
   445 apply(simp_all (no_asm_use))[5]
 
       
   446 apply(erule Prf.cases)
 
       
   447 apply(simp_all (no_asm_use))[5]
 
       
   448 apply(clarify)
 
       
   449 apply(erule GrOrd.cases)
 
       
   450 apply(simp_all (no_asm_use))[7]
 
       
   451 apply(erule GrOrd.cases)
 
       
   452 apply(simp_all (no_asm_use))[7]
 
       
   453 apply (metis GrOrd.intros(3))
 
       
   454 apply(clarify)
 
       
   455 apply(erule GrOrd.cases)
 
       
   456 apply(simp_all (no_asm_use))[7]
 
       
   457 apply(erule GrOrd.cases)
 
       
   458 apply(simp_all (no_asm_use))[7]
 
       
   459 apply(erule Prf.cases)
 
       
   460 apply(simp_all (no_asm_use))[5]
 
       
   461 apply(clarify)
 
       
   462 apply(erule GrOrd.cases)
 
       
   463 apply(simp_all (no_asm_use))[7]
 
       
   464 apply(clarify)
 
       
   465 apply(erule GrOrd.cases)
 
       
   466 apply(simp_all (no_asm_use))[7]
 
       
   467 apply(erule Prf.cases)
 
       
   468 apply(simp_all (no_asm_use))[5]
 
       
   469 apply(erule Prf.cases)
 
       
   470 apply(simp_all (no_asm_use))[5]
 
       
   471 apply(clarify)
 
       
   472 apply(erule GrOrd.cases)
 
       
   473 apply(simp_all (no_asm_use))[7]
 
       
   474 apply(erule GrOrd.cases)
 
       
   475 apply(simp_all (no_asm_use))[7]
 
       
   476 apply (metis GrOrd.intros(5))
 
       
   477 apply(clarify)
 
       
   478 apply(erule GrOrd.cases)
 
       
   479 apply(simp_all (no_asm_use))[7]
 
       
   480 apply(erule GrOrd.cases)
 
       
   481 apply(simp_all (no_asm_use))[7]
 
       
   482 apply(erule Prf.cases)
 
       
   483 apply(simp_all (no_asm_use))[5]
 
       
   484 apply(clarify)
 
       
   485 apply(erule GrOrd.cases)
 
       
   486 apply(simp_all (no_asm_use))[7]
 
       
   487 apply(erule GrOrd.cases)
 
       
   488 apply(simp_all (no_asm_use))[7]
 
       
   489 apply (metis GrOrd.intros(5))
 
       
   490 apply(clarify)
 
       
   491 apply(erule GrOrd.cases)
 
       
   492 apply(simp_all (no_asm_use))[7]
 
       
   493 apply(erule GrOrd.cases)
 
       
   494 apply(simp_all (no_asm_use))[7]
 
       
   495 apply (metis GrOrd.intros(4))
 
       
   496 (* seq case *)
 
       
   497 apply(erule Prf.cases)
 
       
   498 apply(simp_all (no_asm_use))[5]
 
       
   499 apply(erule Prf.cases)
 
       
   500 apply(simp_all (no_asm_use))[5]
 
       
   501 apply(erule Prf.cases)
 
       
   502 apply(simp_all (no_asm_use))[5]
 
       
   503 apply(clarify)
 
       
   504 apply(erule GrOrd.cases)
 
       
   505 apply(simp_all (no_asm_use))[7]
 
       
   506 apply(erule GrOrd.cases)
 
       
   507 apply(simp_all (no_asm_use))[7]
 
       
   508 apply(clarify)
 
       
   509 apply (metis GrOrd.intros(1))
 
       
   510 apply (metis GrOrd.intros(1))
 
       
   511 apply(erule GrOrd.cases)
 
       
   512 apply(simp_all (no_asm_use))[7]
 
       
   513 apply (metis GrOrd.intros(1))
 
       
   514 by (metis GrOrd.intros(1) Gr_refl)
 
       
   515 
       
   516 definition
 
       
   517   GrMaxM :: "val set => val" where
 
       
   518   "GrMaxM S == SOME v.  v \<in> S \<and> (\<forall>v' \<in> S. v' \<prec> v)"
 
       
   519 
       
   520 definition
 
       
   521   "GrMax r s \<equiv> GrMaxM {v. \<turnstile> v : r \<and> flat v = s}"
 
       
   522 
       
   523 inductive ValOrd3 :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ 3\<succ> _" [100, 100] 100)
 
       
   524 where
 
       
   525   "v2 3\<succ> v2' \<Longrightarrow> (Seq v1 v2) 3\<succ> (Seq v1 v2')" 
       
   526 | "v1 3\<succ> v1' \<Longrightarrow> (Seq v1 v2) 3\<succ> (Seq v1' v2')" 
       
   527 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) 3\<succ> (Right v2)"
 
       
   528 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) 3\<succ> (Left v1)"
 
       
   529 | "v2 3\<succ> v2' \<Longrightarrow> (Right v2) 3\<succ> (Right v2')"
 
       
   530 | "v1 3\<succ> v1' \<Longrightarrow> (Left v1) 3\<succ> (Left v1')"
 
       
   531 | "Void 3\<succ> Void"
 
       
   532 | "(Char c) 3\<succ> (Char c)"
 
       
   533 
       
   534 
       
   535 section {* Sulzmann's Ordering of values *}
 
   237 
   536 
   238 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 
   537 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 
   239 where
 
   538 where
 
   240   "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
   539   "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
   241 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
   540 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
   244 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
 
   543 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
 
   245 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 
   544 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 
   246 | "Void \<succ>EMPTY Void"
 
   545 | "Void \<succ>EMPTY Void"
 
   247 | "(Char c) \<succ>(CHAR c) (Char c)"
 
   546 | "(Char c) \<succ>(CHAR c) (Char c)"
 
   248 
   547 
       
   548 inductive ValOrdStr :: "string \<Rightarrow> val \<Rightarrow> val \<Rightarrow> bool" ("_ \<turnstile> _ \<succ>_" [100, 100, 100] 100)
 
       
   549 where
 
       
   550   "\<lbrakk>s \<turnstile> v1 \<succ> v1'; rest v1 s \<turnstile> v2 \<succ> v2'\<rbrakk> \<Longrightarrow> s \<turnstile> (Seq v1 v2) \<succ> (Seq v1' v2')" 
       
   551 | "\<lbrakk>flat v2 \<sqsubseteq> flat v1; flat v1 \<sqsubseteq> s\<rbrakk> \<Longrightarrow> s \<turnstile> (Left v1) \<succ> (Right v2)"
 
       
   552 | "\<lbrakk>flat v1 \<sqsubset> flat v2; flat v2 \<sqsubseteq> s\<rbrakk> \<Longrightarrow> s \<turnstile> (Right v2) \<succ> (Left v1)"
 
       
   553 | "s \<turnstile> v2 \<succ> v2' \<Longrightarrow> s \<turnstile> (Right v2) \<succ> (Right v2')"
 
       
   554 | "s \<turnstile> v1 \<succ> v1' \<Longrightarrow> s \<turnstile> (Left v1) \<succ> (Left v1')"
 
       
   555 | "s \<turnstile> Void \<succ> Void"
 
       
   556 | "(c#s) \<turnstile> (Char c) \<succ> (Char c)"
 
       
   557 
   249 inductive ValOrd2 :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ 2\<succ> _" [100, 100] 100)
 
   558 inductive ValOrd2 :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ 2\<succ> _" [100, 100] 100)
 
   250 where
 
   559 where
 
   251   "v2 2\<succ> v2' \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1 v2')" 
   560   "v2 2\<succ> v2' \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1 v2')" 
   252 | "\<lbrakk>v1 2\<succ> v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1' v2')" 
   561 | "\<lbrakk>v1 2\<succ> v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1' v2')" 
   253 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) 2\<succ> (Right v2)"
 
   562 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) 2\<succ> (Right v2)"
 
   386 apply(simp_all)[8]
 
   695 apply(simp_all)[8]
 
   387 apply(erule ValOrd.cases)
 
   696 apply(erule ValOrd.cases)
 
   388 apply(simp_all)[8]
 
   697 apply(simp_all)[8]
 
   389 done
 
   698 done
 
   390 
   699 
   391 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100)
 
   700 lemma refl_on_ValOrd:
 
   392 where
 
   701   "refl_on (Values r s) {(v1, v2). v1 \<succ>r v2 \<and> v1 \<in> Values r s \<and> v2 \<in> Values r s}"
 
   393   "s1 \<sqsubseteq> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"
 
   702 unfolding refl_on_def
 
   394 
   703 apply(auto)
 
   395 
   704 apply(rule ValOrd_refl)
 
   396 lemma
 
   705 apply(simp add: Values_def)
 
   397   "L r \<noteq> {} \<longrightarrow> (\<exists>vmax \<in> {v. \<turnstile> v : r}. \<forall>v \<in> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> flat vmax}. vmax 2\<succ> v)"
 
   706 done
 
   398 apply(induct r)
 
   707 
   399 apply(simp)
 
   708 (*
 
   400 apply(rule impI)
 
       
   401 apply(simp)
 
       
   402 apply(rule_tac x="Void" in exI)
 
       
   403 apply(simp)
 
       
   404 apply(rule conjI)
 
       
   405 apply (metis Prf.intros(4))
 
       
   406 apply(rule allI)
 
       
   407 apply(rule impI)
 
       
   408 apply(erule conjE)
 
       
   409 apply(erule Prf.cases)
 
       
   410 apply(simp_all)[5]
 
       
   411 apply (metis ValOrd2.intros(7))
 
       
   412 apply(simp)
 
       
   413 apply(rule_tac x="Char char" in exI)
 
       
   414 apply(simp)
 
       
   415 apply(rule conjI)
 
       
   416 apply (metis Prf.intros)
 
       
   417 apply(rule allI)
 
       
   418 apply(rule impI)
 
       
   419 apply(erule conjE)
 
       
   420 apply(erule Prf.cases)
 
       
   421 apply(simp_all)[5]
 
       
   422 apply (metis ValOrd2.intros(8))
 
       
   423 apply(simp)
 
       
   424 apply(rule impI)
 
       
   425 apply(simp add: Sequ_def)[1]
 
       
   426 apply(erule exE)+
 
       
   427 apply(erule conjE)+
 
       
   428 apply(clarify)
 
       
   429 defer
 
       
   430 apply(rule impI)
 
       
   431 apply(drule L_ALT_cases)
 
       
   432 apply(erule disjE)
 
       
   433 apply(simp)
 
       
   434 apply(erule exE)
 
       
   435 apply(clarify)
 
       
   436 apply(rule_tac x="Left vmax" in exI)
 
       
   437 apply(rule conjI)
 
       
   438 apply (metis Prf.intros(2))
 
       
   439 apply(simp)
 
       
   440 apply(rule allI)
 
       
   441 apply(rule impI)
 
       
   442 apply(erule conjE)
 
       
   443 apply(rotate_tac 4)
 
       
   444 apply(erule Prf.cases)
 
       
   445 apply(simp_all)[5]
 
       
   446 apply (metis ValOrd2.intros(6))
 
       
   447 apply(clarify)
 
       
   448 apply (metis ValOrd2.intros(3) length_append ordered_cancel_comm_monoid_diff_class.le_iff_add prefix_def)
 
       
   449 apply(simp)
 
       
   450 apply(clarify)
 
       
   451 apply(rule_tac x="Right vmax" in exI)
 
       
   452 apply(rule conjI)
 
       
   453 apply (metis Prf.intros(3))
 
       
   454 apply(rule allI)
 
       
   455 apply(rule impI)
 
       
   456 apply(erule conjE)+
 
       
   457 apply(simp)
 
       
   458 apply(rotate_tac 4)
 
       
   459 apply(erule Prf.cases)
 
       
   460 apply(simp_all)[5]
 
       
   461 apply (metis Prf_flat_L empty_iff)
 
       
   462 apply (metis ValOrd2.intros(5))
 
       
   463 apply(drule mp)
 
       
   464 apply (metis empty_iff)
 
       
   465 apply(drule mp)
 
       
   466 apply (metis empty_iff)
 
       
   467 apply(erule exE)+
 
       
   468 apply(erule conjE)+
 
       
   469 apply(rule_tac x="Seq vmax vmaxa" in exI)
 
       
   470 apply(rule conjI)
 
       
   471 apply (metis Prf.intros(1))
 
       
   472 apply(rule allI)
 
       
   473 apply(rule impI)
 
       
   474 apply(erule conjE)+
 
       
   475 apply(simp)
 
       
   476 apply(rotate_tac 6)
 
       
   477 apply(erule Prf.cases)
 
       
   478 apply(simp_all)[5]
 
       
   479 apply(auto)
 
       
   480 apply(case_tac "vmax = v1")
 
       
   481 apply(simp)
 
       
   482 apply (simp add: ValOrd2.intros(1) prefix_def)
 
       
   483 
       
   484 lemma
 
       
   485   "s \<in> L r \<longrightarrow> (\<exists>vmax \<in> {v. \<turnstile> v : r \<and> flat v = s}. \<forall>v \<in> {v. \<turnstile> v : r \<and> flat v = s}. vmax 2\<succ> v)"
 
       
   486 apply(induct s arbitrary: r rule: length_induct)
 
       
   487 apply(induct_tac r rule: rexp.induct)
 
       
   488 apply(rule impI)
 
       
   489 apply(simp)
 
       
   490 apply(simp)
 
       
   491 apply(rule impI)
 
       
   492 apply(simp)
 
       
   493 apply(rule_tac x="Void" in exI)
 
       
   494 apply(simp)
 
       
   495 apply(rule conjI)
 
       
   496 apply (metis Prf.intros(4))
 
       
   497 apply(rule allI)
 
       
   498 apply(rule impI)
 
       
   499 apply(erule conjE)
 
       
   500 apply(erule Prf.cases)
 
       
   501 apply(simp_all)[5]
 
       
   502 apply (metis ValOrd2.intros(7))
 
       
   503 apply(simp)
 
       
   504 apply(rule impI)
 
       
   505 apply(rule_tac x="Char char" in exI)
 
       
   506 apply(simp)
 
       
   507 apply(rule conjI)
 
       
   508 apply (metis Prf.intros)
 
       
   509 apply(rule allI)
 
       
   510 apply(rule impI)
 
       
   511 apply(erule conjE)
 
       
   512 apply(erule Prf.cases)
 
       
   513 apply(simp_all)[5]
 
       
   514 apply (metis ValOrd2.intros(8))
 
       
   515 apply(simp)
 
       
   516 apply(rule impI)
 
       
   517 apply(simp add: Sequ_def)[1]
 
       
   518 apply(erule exE)+
 
       
   519 apply(erule conjE)+
 
       
   520 apply(clarify)
 
       
   521 defer
 
       
   522 apply(simp)
 
       
   523 apply(rule conjI)
 
       
   524 apply(rule impI)
 
       
   525 apply(simp)
 
       
   526 apply(erule exE)
 
       
   527 apply(clarify)
 
       
   528 apply(rule_tac x="Left vmax" in exI)
 
       
   529 apply(rule conjI)
 
       
   530 apply (metis Prf.intros(2))
 
       
   531 apply(simp)
 
       
   532 apply(rule allI)
 
       
   533 apply(rule impI)
 
       
   534 apply(erule conjE)
 
       
   535 apply(rotate_tac 5)
 
       
   536 apply(erule Prf.cases)
 
       
   537 apply(simp_all)[5]
 
       
   538 apply (metis ValOrd2.intros(6))
 
       
   539 apply(clarify)
 
       
   540 apply (metis ValOrd2.intros(3) order_refl)
 
       
   541 apply(rule impI)
 
       
   542 apply(simp)
 
       
   543 apply(erule exE)
 
       
   544 apply(clarify)
 
       
   545 apply(rule_tac x="Right vmax" in exI)
 
       
   546 apply(simp)
 
       
   547 apply(rule conjI)
 
       
   548 apply (metis Prf.intros(3))
 
       
   549 apply(rule allI)
 
       
   550 apply(rule impI)
 
       
   551 apply(erule conjE)+
 
       
   552 apply(rotate_tac 5)
 
       
   553 apply(erule Prf.cases)
 
       
   554 apply(simp_all)[5]
 
       
   555 apply (metis ValOrd2.intros(8))
 
       
   556 apply(simp)
 
       
   557 apply(rule impI)
 
       
   558 apply(simp add: Sequ_def)[1]
 
       
   559 apply(erule exE)+
 
       
   560 apply(erule conjE)+
 
       
   561 apply(clarify)
 
       
   562 
       
   563 
       
   564 inductive ValOrd3 :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ 3\<succ>_ _" [100, 100, 100] 100)
 
   709 inductive ValOrd3 :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ 3\<succ>_ _" [100, 100, 100] 100)
 
   565 where
 
   710 where
 
   566   "\<lbrakk>v2 3\<succ>r2 v2'; \<turnstile> v1 : r1\<rbrakk> \<Longrightarrow> (Seq v1 v2) 3\<succ>(SEQ r1 r2) (Seq v1 v2')" 
   711   "\<lbrakk>v2 3\<succ>r2 v2'; \<turnstile> v1 : r1\<rbrakk> \<Longrightarrow> (Seq v1 v2) 3\<succ>(SEQ r1 r2) (Seq v1 v2')" 
   567 | "\<lbrakk>v1 3\<succ>r1 v1'; v1 \<noteq> v1'; flat v2 = flat v2'; \<turnstile> v2 : r2; \<turnstile> v2' : r2\<rbrakk> 
   712 | "\<lbrakk>v1 3\<succ>r1 v1'; v1 \<noteq> v1'; flat v2 = flat v2'; \<turnstile> v2 : r2; \<turnstile> v2' : r2\<rbrakk> 
   568       \<Longrightarrow> (Seq v1 v2) 3\<succ>(SEQ r1 r2) (Seq v1' v2')" 
   713       \<Longrightarrow> (Seq v1 v2) 3\<succ>(SEQ r1 r2) (Seq v1' v2')" 
   570 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) 3\<succ>(ALT r1 r2) (Left v1)"
 
   715 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) 3\<succ>(ALT r1 r2) (Left v1)"
 
   571 | "v2 3\<succ>r2 v2' \<Longrightarrow> (Right v2) 3\<succ>(ALT r1 r2) (Right v2')"
 
   716 | "v2 3\<succ>r2 v2' \<Longrightarrow> (Right v2) 3\<succ>(ALT r1 r2) (Right v2')"
 
   572 | "v1 3\<succ>r1 v1' \<Longrightarrow> (Left v1) 3\<succ>(ALT r1 r2) (Left v1')"
 
   717 | "v1 3\<succ>r1 v1' \<Longrightarrow> (Left v1) 3\<succ>(ALT r1 r2) (Left v1')"
 
   573 | "Void 3\<succ>EMPTY Void"
 
   718 | "Void 3\<succ>EMPTY Void"
 
   574 | "(Char c) 3\<succ>(CHAR c) (Char c)"
 
   719 | "(Char c) 3\<succ>(CHAR c) (Char c)"
 
   575 
   720 *)
 
   576 
       
   577 lemma "v1 3\<succ>r v2 \<Longrightarrow> v1 \<succ>r v2 \<and> \<turnstile> v1 : r \<and> \<turnstile> v2 : r \<and> flat v1 = flat v2"
 
       
   578 apply(induct rule: ValOrd3.induct)
 
       
   579 prefer 8
 
       
   580 apply(simp)
 
       
   581 apply (metis Prf.intros(5) ValOrd.intros(8))
 
       
   582 prefer 7
 
       
   583 apply(simp)
 
       
   584 apply (metis Prf.intros(4) ValOrd.intros(7))
 
       
   585 apply(simp)
 
       
   586 apply (metis Prf.intros(1) ValOrd.intros(1))
 
       
   587 apply(simp)
 
       
   588 
       
   589 
       
   590 
       
   591 
       
   592 lemma ValOrd_trans:
 
       
   593   assumes "v1 \<succ>r v2" "v2 \<succ>r v3" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<turnstile> v3 : r" 
       
   594      "flat v1 = flat v2" "flat v2 = flat v3"
 
       
   595   shows "v1 \<succ>r v3"
 
       
   596 using assms
 
       
   597 apply(induct r arbitrary: v1 v2 v3 s1 s2 s3)
 
       
   598 apply(erule Prf.cases)
 
       
   599 apply(simp_all)[5]
 
       
   600 apply(erule Prf.cases)
 
       
   601 apply(simp_all)[5]
 
       
   602 apply(erule Prf.cases)
 
       
   603 apply(simp_all)[5]
 
       
   604 apply(erule Prf.cases)
 
       
   605 apply(simp_all)[5]
 
       
   606 apply(erule Prf.cases)
 
       
   607 apply(simp_all)[5]
 
       
   608 apply(erule Prf.cases)
 
       
   609 apply(simp_all)[5]
 
       
   610 apply(erule Prf.cases)
 
       
   611 apply(simp_all)[5]
 
       
   612 apply(erule Prf.cases)
 
       
   613 apply(simp_all)[5]
 
       
   614 apply(clarify)
 
       
   615 apply(erule ValOrd.cases)
 
       
   616 apply(simp_all)[8]
 
       
   617 apply(erule ValOrd.cases)
 
       
   618 apply(simp_all)[8]
 
       
   619 apply(clarify)
 
       
   620 apply (metis ValOrd.intros(1))
 
       
   621 apply(clarify)
 
       
   622 apply (metis ValOrd.intros(2))
 
       
   623 apply(erule ValOrd.cases)
 
       
   624 apply(simp_all)[8]
 
       
   625 apply (metis ValOrd.intros(2))
 
       
   626 apply(clarify)
 
       
   627 apply(case_tac "v1d = v1'a")
 
       
   628 apply(simp)
 
       
   629 apply (metis ValOrd_anti)
 
       
   630 apply (rule ValOrd.intros(2))
 
       
   631 prefer 2
 
       
   632 apply(auto)[1]
 
       
   633 apply metis
 
       
   634 apply(erule Prf.cases)
 
       
   635 apply(simp_all)[5]
 
       
   636 apply(erule Prf.cases)
 
       
   637 apply(simp_all)[5]
 
       
   638 apply(erule Prf.cases)
 
       
   639 apply(simp_all)[5]
 
       
   640 apply(erule ValOrd.cases)
 
       
   641 apply(simp_all)[8]
 
       
   642 apply(erule ValOrd.cases)
 
       
   643 apply(simp_all)[8]
 
       
   644 apply (metis Ord1 Ord3 Prf.intros(2) ValOrd2.intros(6))
 
       
   645 apply(erule ValOrd.cases)
 
       
   646 apply(simp_all)[8]
 
       
   647 apply(erule ValOrd.cases)
 
       
   648 apply(simp_all)[8]
 
       
   649 apply (rule ValOrd.intros)
 
       
   650 apply(clarify)
 
       
   651 oops
 
       
   652 
       
   653 
       
   654 lemma ValOrd_max:
 
       
   655   shows "L r \<noteq> {} \<Longrightarrow> \<exists>v. \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<longrightarrow> v' \<succ>r v \<longrightarrow> v = v'))" 
       
   656 using assms
 
       
   657 apply(induct r)
 
       
   658 apply(auto)[3]
 
       
   659 apply(rule_tac x="Void" in exI)
 
       
   660 apply(rule conjI)
 
       
   661 apply (metis Prf.intros(4))
 
       
   662 apply(rule allI)
 
       
   663 apply(rule impI)+
 
       
   664 apply(erule ValOrd.cases)
 
       
   665 apply(simp_all)[8]
 
       
   666 apply(rule_tac x="Char char" in exI)
 
       
   667 apply(rule conjI)
 
       
   668 apply (metis Prf.intros(5))
 
       
   669 apply(rule allI)
 
       
   670 apply(rule impI)+
 
       
   671 apply(erule ValOrd.cases)
 
       
   672 apply(simp_all)[8]
 
       
   673 apply(simp add: L.simps)
 
       
   674 apply(auto simp: Sequ_def)[1]
 
       
   675 apply(drule meta_mp)
 
       
   676 apply (metis empty_iff)
 
       
   677 apply(drule meta_mp)
 
       
   678 apply (metis empty_iff)
 
       
   679 apply(erule exE)+
 
       
   680 apply(rule_tac x="Seq v va" in exI)
 
       
   681 apply(rule conjI)
 
       
   682 apply (metis Prf.intros(1))
 
       
   683 apply(rule allI)
 
       
   684 apply(rule impI)+
 
       
   685 apply(rotate_tac 4)
 
       
   686 apply(erule Prf.cases)
 
       
   687 apply(simp_all)[5]
 
       
   688 apply(erule ValOrd.cases)
 
       
   689 apply(simp_all)[8]
 
       
   690 apply metis
 
       
   691 apply(simp only: L.simps Lattices.bounded_lattice_bot_class.sup_eq_bot_iff HOL.de_Morgan_conj)
 
       
   692 apply(erule disjE)
 
       
   693 apply(drule meta_mp)
 
       
   694 apply (metis empty_iff)
 
       
   695 apply(erule exE)+
 
       
   696 apply(rule exI)
 
       
   697 apply(rule conjI)
 
       
   698 apply(rule Prf.intros)
 
       
   699 apply(erule conjE)+
 
       
   700 apply(assumption)
 
       
   701 apply(rule allI)
 
       
   702 apply(rule impI)+
 
       
   703 apply(erule Prf.cases)
 
       
   704 apply(simp_all)[5]
 
       
   705 apply(clarify)
 
       
   706 apply(erule ValOrd.cases)
 
       
   707 apply(simp_all)[8]
 
       
   708 apply(clarify)
 
       
   709 apply(drule meta_mp)
 
       
   710 apply (metis Prf_flat_L empty_iff)
 
       
   711 apply(auto)[1]
 
       
   712 apply(erule ValOrd.cases)
 
       
   713 apply(simp_all)[8]
 
       
   714 apply(clarify)
 
       
   715 oops
 
       
   716 
   721 
   717 section {* Posix definition *}
 
   722 section {* Posix definition *}
 
   718 
   723 
   719 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
   724 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
   720 where
 
   725 where
 
   759 apply (metis Prfs_Prf)
 
   764 apply (metis Prfs_Prf)
 
   760 apply (metis Prf_Prfs)
 
   765 apply (metis Prf_Prfs)
 
   761 apply (metis Prf_Prfs)
 
   766 apply (metis Prf_Prfs)
 
   762 by (metis Prfs_Prf Prfs_flat)
 
   767 by (metis Prfs_Prf Prfs_flat)
 
   763 
   768 
   764 lemma 
       
   765   assumes "POSIX v1 r1" "\<turnstile> v1' : r1"
 
       
   766   shows "Seq v1 v2 \<succ>(SEQ r1 r2) Seq v1' v2'"
 
       
   767 using assms
 
       
   768 apply(rule_tac ValOrd.intros)
 
       
   769 apply(simp add: POSIX_def)
 
       
   770 oops
 
       
   771 
       
   772 lemma
 
       
   773 "L r \<noteq> {} \<Longrightarrow> \<exists>v. POSIXs v r (flat v)"
 
       
   774 apply(induct r arbitrary: )
 
       
   775 apply(simp)
 
       
   776 apply(rule_tac x="Void" in exI)
 
       
   777 apply(simp add: POSIXs_def)
 
       
   778 apply(rule conjI)
 
       
   779 apply (metis Prfs.intros(4))
 
       
   780 apply(auto)[1]
 
       
   781 apply(erule Prfs.cases)
 
       
   782 apply(simp_all)[5]
 
       
   783 apply (metis ValOrd2.intros(7))
 
       
   784 apply(simp)
 
       
   785 apply(rule_tac x="Char char" in exI)
 
       
   786 apply(simp add: POSIXs_def)
 
       
   787 apply(rule conjI)
 
       
   788 apply (metis Prfs.intros(5))
 
       
   789 apply(auto)[1]
 
       
   790 apply(erule Prfs.cases)
 
       
   791 apply(simp_all)[5]
 
       
   792 apply (metis ValOrd2.intros)
 
       
   793 apply(auto simp add: Sequ_def)
 
       
   794 apply(drule meta_mp)
 
       
   795 apply (metis empty_iff)
 
       
   796 apply(drule meta_mp)
 
       
   797 apply (metis empty_iff)
 
       
   798 apply(auto)
 
       
   799 oops
 
       
   800 
       
   801 section {* POSIX for some constructors *}
 
   769 section {* POSIX for some constructors *}
 
   802 
   770 
   803 lemma POSIX_SEQ1:
 
   771 lemma POSIX_SEQ1:
 
   804   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
 
   772   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
 
   805   shows "POSIX v1 r1"
 
   773   shows "POSIX v1 r1"
 
  1095 apply(simp_all)[5]
 
  1063 apply(simp_all)[5]
 
  1096 apply(auto)
 
  1064 apply(auto)
 
  1097 apply(rule ValOrd2.intros)
 
  1065 apply(rule ValOrd2.intros)
 
  1098 apply metis
 
  1066 apply metis
 
  1099 done
 
  1067 done
 
  1100 
       
  1101 
  1068 
  1102 lemma 
  1069 lemma 
  1103   "\<lbrakk>POSIX (mkeps r2) r2; nullable r2; \<not> nullable r1\<rbrakk>
 
  1070   "\<lbrakk>POSIX (mkeps r2) r2; nullable r2; \<not> nullable r1\<rbrakk>
 
  1104    \<Longrightarrow> POSIX (Right (mkeps r2)) (ALT r1 r2)" 
  1071    \<Longrightarrow> POSIX (Right (mkeps r2)) (ALT r1 r2)" 
  1105 apply(auto simp add: POSIX_def)
 
  1072 apply(auto simp add: POSIX_def)
 
  1189  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 
  1156  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 
  1190 where
 
  1157 where
 
  1191   "ders [] r = r"
 
  1158   "ders [] r = r"
 
  1192 | "ders (c # s) r = ders s (der c r)"
 
  1159 | "ders (c # s) r = ders s (der c r)"
 
  1193 
  1160 
       
  1161 fun
 
       
  1162  red :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 
       
  1163 where
 
       
  1164   "red c (NULL) = NULL"
 
       
  1165 | "red c (EMPTY) = CHAR c"
 
       
  1166 | "red c (CHAR c') = SEQ (CHAR c) (CHAR c')"
 
       
  1167 | "red c (ALT r1 r2) = ALT (red c r1) (red c r2)"
 
       
  1168 | "red c (SEQ r1 r2) = 
       
  1169      (if nullable r1
 
       
  1170       then ALT (SEQ (red c r1) r2) (red c r2)
 
       
  1171       else SEQ (red c r1) r2)"
 
       
  1172 
       
  1173 lemma L_der:
 
       
  1174   shows "L (der c r) = {s. c#s \<in> L r}"
 
       
  1175 apply(induct r)
 
       
  1176 apply(simp_all)
 
       
  1177 apply(simp add: Sequ_def)
 
       
  1178 apply(auto)[1]
 
       
  1179 apply (metis append_Cons)
 
       
  1180 apply (metis append_Nil nullable_correctness)
 
       
  1181 apply (metis append_eq_Cons_conv)
 
       
  1182 apply (metis append_Cons)
 
       
  1183 apply (metis Cons_eq_append_conv nullable_correctness)
 
       
  1184 apply(auto)
 
       
  1185 done
 
       
  1186 
       
  1187 lemma L_red:
 
       
  1188   shows "L (red c r) = {c#s | s. s \<in> L r}"
 
       
  1189 apply(induct r)
 
       
  1190 apply(simp_all)
 
       
  1191 apply(simp add: Sequ_def)
 
       
  1192 apply(simp add: Sequ_def)
 
       
  1193 apply(auto)[1]
 
       
  1194 apply (metis append_Nil nullable_correctness)
 
       
  1195 apply (metis append_Cons)
 
       
  1196 apply (metis append_Cons)
 
       
  1197 apply(auto)
 
       
  1198 done
 
       
  1199 
       
  1200 lemma L_red_der:
 
       
  1201   "L(red c (der c r)) = {c#s | s. c#s \<in> L r}"
 
       
  1202 apply(simp add: L_red)
 
       
  1203 apply(simp add: L_der)
 
       
  1204 done
 
       
  1205 
       
  1206 lemma L_der_red:
 
       
  1207   "L(der c (red c r)) = L r"
 
       
  1208 apply(simp add: L_der)
 
       
  1209 apply(simp add: L_red)
 
       
  1210 done
 
       
  1211 
  1194 section {* Injection function *}
 
  1212 section {* Injection function *}
 
  1195 
  1213 
  1196 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 
  1214 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 
  1197 where
 
  1215 where
 
  1198   "injval (CHAR d) c Void = Char d"
 
  1216   "injval (EMPTY) c Void = Char c"
 
       
  1217 | "injval (CHAR d) c Void = Char d"
 
       
  1218 | "injval (CHAR d) c (Char c') = Seq (Char d) (Char c')"
 
  1199 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
 
  1219 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
 
  1200 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
 
  1220 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
 
       
  1221 | "injval (SEQ r1 r2) c (Char c') = Seq (Char c) (Char c')"
 
  1201 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
 
  1222 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
 
  1202 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
 
  1223 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
 
  1203 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
 
  1224 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
 
  1204 
  1225 
  1205 
  1226 
  1260 apply(auto)[1]
 
  1281 apply(auto)[1]
 
  1261 apply(rule Prf.intros)
 
  1282 apply(rule Prf.intros)
 
  1262 apply(auto)[2]
 
  1283 apply(auto)[2]
 
  1263 done
 
  1284 done
 
  1264 
  1285 
       
  1286 lemma v3_red:
 
       
  1287   assumes "\<turnstile> v : r" shows "\<turnstile> (injval (red c r) c v) : (red c r)"
 
       
  1288 using assms
 
       
  1289 apply(induct c r arbitrary: v rule: red.induct)
 
       
  1290 apply(simp)
 
       
  1291 apply(erule Prf.cases)
 
       
  1292 apply(simp_all)[5]
 
       
  1293 apply(simp)
 
       
  1294 apply(erule Prf.cases)
 
       
  1295 apply(simp_all)[5]
 
       
  1296 apply (metis Prf.intros(5))
 
       
  1297 apply(erule Prf.cases)
 
       
  1298 apply(simp_all)[5]
 
       
  1299 apply (metis Prf.intros(1) Prf.intros(5))
 
       
  1300 apply(erule Prf.cases)
 
       
  1301 apply(simp_all)[5]
 
       
  1302 apply (metis Prf.intros(2))
 
       
  1303 apply (metis Prf.intros(3))
 
       
  1304 apply(erule Prf.cases)
 
       
  1305 apply(simp_all)[5]
 
       
  1306 apply(auto)
 
       
  1307 prefer 2
 
       
  1308 apply (metis Prf.intros(1))
 
       
  1309 oops
 
       
  1310 
  1265 lemma v3s:
 
  1311 lemma v3s:
 
  1266   assumes "\<Turnstile>s v : der c r" shows "\<Turnstile>(c#s) (injval r c v) : r"
 
  1312   assumes "\<Turnstile>s v : der c r" shows "\<Turnstile>(c#s) (injval r c v) : r"
 
  1267 using assms
 
  1313 using assms
 
  1268 apply(induct arbitrary: s v rule: der.induct)
 
  1314 apply(induct arbitrary: s v rule: der.induct)
 
  1269 apply(simp)
 
  1315 apply(simp)
 
  1487 apply(simp)
 
  1533 apply(simp)
 
  1488 apply(erule Prf.cases)
 
  1534 apply(erule Prf.cases)
 
  1489 apply(simp_all)[5]
 
  1535 apply(simp_all)[5]
 
  1490 done
 
  1536 done
 
  1491 
  1537 
  1492 lemma v4_flats:
 
       
  1493   assumes "\<turnstile> v : der c r" "\<not>nullable r" shows "hd (flats (injval r c v)) \<noteq> []"
 
       
  1494 using assms
 
       
  1495 apply(induct arbitrary: v rule: der.induct)
 
       
  1496 apply(simp)
 
       
  1497 apply(erule Prf.cases)
 
       
  1498 apply(simp_all)[5]
 
       
  1499 apply(simp)
 
       
  1500 apply(case_tac "c = c'")
 
       
  1501 apply(simp)
 
       
  1502 apply(auto)[1]
 
       
  1503 apply(erule Prf.cases)
 
       
  1504 apply(simp_all)[5]
 
       
  1505 apply(simp)
 
       
  1506 apply(erule Prf.cases)
 
       
  1507 apply(simp_all)[5]
 
       
  1508 apply(simp)
 
       
  1509 apply(erule Prf.cases)
 
       
  1510 apply(simp_all)[5]
 
       
  1511 apply(simp)
 
       
  1512 apply(case_tac "nullable r1")
 
       
  1513 apply(simp)
 
       
  1514 apply(erule Prf.cases)
 
       
  1515 apply(simp_all)[5]
 
       
  1516 apply(auto)[1]
 
       
  1517 apply(erule Prf.cases)
 
       
  1518 apply(simp_all)[5]
 
       
  1519 apply(clarify)
 
       
  1520 oops
 
       
  1521 
       
  1522 lemma v4_flat_left:
 
       
  1523   assumes "\<turnstile> v : der c r" "\<not>(nullable_left r)" shows "flat_left (injval r c v) = c # (flat_left v)"
 
       
  1524 using assms
 
       
  1525 apply(induct arbitrary: v rule: der.induct)
 
       
  1526 apply(simp)
 
       
  1527 apply(erule Prf.cases)
 
       
  1528 apply(simp_all)[5]
 
       
  1529 apply(simp)
 
       
  1530 apply(case_tac "c = c'")
 
       
  1531 apply(simp)
 
       
  1532 apply(erule Prf.cases)
 
       
  1533 apply(simp_all)[5]
 
       
  1534 apply(simp)
 
       
  1535 apply(erule Prf.cases)
 
       
  1536 apply(simp_all)[5]
 
       
  1537 apply(simp)
 
       
  1538 apply(erule Prf.cases)
 
       
  1539 apply(simp_all)[5]
 
       
  1540 apply(simp)
 
       
  1541 apply(case_tac "nullable r1")
 
       
  1542 apply(simp)
 
       
  1543 apply(erule Prf.cases)
 
       
  1544 apply(simp_all (no_asm_use))[5]
 
       
  1545 apply(auto)[1]
 
       
  1546 apply(erule Prf.cases)
 
       
  1547 apply(simp_all)[5]
 
       
  1548 apply(clarify)
 
       
  1549 apply(simp only: injval.simps)
 
       
  1550 apply (metis nullable_left)
 
       
  1551 apply(simp)
 
       
  1552 apply(erule Prf.cases)
 
       
  1553 apply(simp_all)[5]
 
       
  1554 done
 
       
  1555 
       
  1556 
       
  1557 lemma v4_proj:
 
  1538 lemma v4_proj:
 
  1558   assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
 
  1539   assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
 
  1559   shows "c # flat (projval r c v) = flat v"
 
  1540   shows "c # flat (projval r c v) = flat v"
 
  1560 using assms
 
  1541 using assms
 
  1561 apply(induct rule: Prf.induct)
 
  1542 apply(induct rule: Prf.induct)
 
  1624 apply(erule Prf.cases)
 
  1605 apply(erule Prf.cases)
 
  1625 apply(simp_all)[5]
 
  1606 apply(simp_all)[5]
 
  1626 apply(erule Prf.cases)
 
  1607 apply(erule Prf.cases)
 
  1627 apply(simp_all)[5]
 
  1608 apply(simp_all)[5]
 
  1628 done
 
  1609 done
 
       
  1610 
       
  1611 lemma Values_nullable:
 
       
  1612   assumes "nullable r1"
 
       
  1613   shows "mkeps r1 \<in> Values r1 s"
 
       
  1614 using assms
 
       
  1615 apply(induct r1 arbitrary: s)
 
       
  1616 apply(simp_all)
 
       
  1617 apply(simp add: Values_recs)
 
       
  1618 apply(simp add: Values_recs)
 
       
  1619 apply(simp add: Values_recs)
 
       
  1620 apply(auto)[1]
 
       
  1621 done
 
       
  1622 
       
  1623 lemma Values_injval:
 
       
  1624   assumes "v \<in> Values (der c r) s"
 
       
  1625   shows "injval r c v \<in> Values r (c#s)"
 
       
  1626 using assms
 
       
  1627 apply(induct c r arbitrary: v s rule: der.induct)
 
       
  1628 apply(simp add: Values_recs)
 
       
  1629 apply(simp add: Values_recs)
 
       
  1630 apply(case_tac "c = c'")
 
       
  1631 apply(simp)
 
       
  1632 apply(simp add: Values_recs)
 
       
  1633 apply(simp add: prefix_def)
 
       
  1634 apply(simp)
 
       
  1635 apply(simp add: Values_recs)
 
       
  1636 apply(simp)
 
       
  1637 apply(simp add: Values_recs)
 
       
  1638 apply(auto)[1]
 
       
  1639 apply(case_tac "nullable r1")
 
       
  1640 apply(simp)
 
       
  1641 apply(simp add: Values_recs)
 
       
  1642 apply(auto)[1]
 
       
  1643 apply(simp add: rest_def)
 
       
  1644 apply(subst v4)
 
       
  1645 apply(simp add: Values_def)
 
       
  1646 apply(simp add: Values_def)
 
       
  1647 apply(rule Values_nullable)
 
       
  1648 apply(assumption)
 
       
  1649 apply(simp add: rest_def)
 
       
  1650 apply(subst mkeps_flat)
 
       
  1651 apply(assumption)
 
       
  1652 apply(simp)
 
       
  1653 apply(simp)
 
       
  1654 apply(simp add: Values_recs)
 
       
  1655 apply(auto)[1]
 
       
  1656 apply(simp add: rest_def)
 
       
  1657 apply(subst v4)
 
       
  1658 apply(simp add: Values_def)
 
       
  1659 apply(simp add: Values_def)
 
       
  1660 done
 
       
  1661 
       
  1662 lemma Values_projval:
 
       
  1663   assumes "v \<in> Values r (c#s)" "\<exists>s. flat v = c # s"
 
       
  1664   shows "projval r c v \<in> Values (der c r) s"
 
       
  1665 using assms
 
       
  1666 apply(induct r arbitrary: v s c rule: rexp.induct)
 
       
  1667 apply(simp add: Values_recs)
 
       
  1668 apply(simp add: Values_recs)
 
       
  1669 apply(case_tac "c = x")
 
       
  1670 apply(simp)
 
       
  1671 apply(simp add: Values_recs)
 
       
  1672 apply(simp)
 
       
  1673 apply(simp add: Values_recs)
 
       
  1674 apply(simp add: prefix_def)
 
       
  1675 apply(case_tac "nullable x1")
 
       
  1676 apply(simp)
 
       
  1677 apply(simp add: Values_recs)
 
       
  1678 apply(auto)[1]
 
       
  1679 apply(simp add: rest_def)
 
       
  1680 apply (metis hd_Cons_tl hd_append2 list.sel(1))
 
       
  1681 apply(simp add: rest_def)
 
       
  1682 apply(simp add: append_eq_Cons_conv)
 
       
  1683 apply(auto)[1]
 
       
  1684 apply(subst v4_proj2)
 
       
  1685 apply(simp add: Values_def)
 
       
  1686 apply(assumption)
 
       
  1687 apply(simp)
 
       
  1688 apply(simp)
 
       
  1689 apply(simp add: Values_recs)
 
       
  1690 apply(auto)[1]
 
       
  1691 apply(auto simp add: Values_def not_nullable_flat)[1]
 
       
  1692 apply(simp add: append_eq_Cons_conv)
 
       
  1693 apply(auto)[1]
 
       
  1694 apply(simp add: append_eq_Cons_conv)
 
       
  1695 apply(auto)[1]
 
       
  1696 apply(simp add: rest_def)
 
       
  1697 apply(subst v4_proj2)
 
       
  1698 apply(simp add: Values_def)
 
       
  1699 apply(assumption)
 
       
  1700 apply(simp)
 
       
  1701 apply(simp add: Values_recs)
 
       
  1702 apply(auto)[1]
 
       
  1703 done
 
       
  1704 
       
  1705 
       
  1706 definition "MValue v r s \<equiv> (v \<in> Values r s \<and> (\<forall>v' \<in> Values r s. v 2\<succ> v'))"
 
       
  1707 
       
  1708 lemma 
       
  1709   assumes "MValue v1 r1 s"
 
       
  1710   shows "MValue (Seq v1 v2) (SEQ r1 r2) s
 
       
  1711 
       
  1712 
       
  1713 lemma MValue_SEQE:
 
       
  1714   assumes "MValue v (SEQ r1 r2) s"
 
       
  1715   shows "(\<exists>v1 v2. MValue v1 r1 s \<and> MValue v2 r2 (rest v1 s) \<and> v = Seq v1 v2)"
 
       
  1716 using assms
 
       
  1717 apply(simp add: MValue_def)
 
       
  1718 apply(simp add: Values_recs)
 
       
  1719 apply(erule conjE)
 
       
  1720 apply(erule exE)+
 
       
  1721 apply(erule conjE)+
 
       
  1722 apply(simp)
 
       
  1723 apply(auto)
 
       
  1724 apply(drule_tac x="Seq x v2" in spec)
 
       
  1725 apply(drule mp)
 
       
  1726 apply(rule_tac x="x" in exI)
 
       
  1727 apply(rule_tac x="v2" in exI)
 
       
  1728 apply(simp)
 
       
  1729 oops
 
       
  1730 
       
  1731 
       
  1732 lemma MValue_ALTE:
 
       
  1733   assumes "MValue v (ALT r1 r2) s"
 
       
  1734   shows "(\<exists>vl. v = Left vl \<and> MValue vl r1 s \<and> (\<forall>vr \<in> Values r2 s. length (flat vr) \<le> length (flat vl))) \<or> 
       
  1735          (\<exists>vr. v = Right vr \<and> MValue vr r2 s \<and> (\<forall>vl \<in> Values r1 s. length (flat vl) < length (flat vr)))"
 
       
  1736 using assms
 
       
  1737 apply(simp add: MValue_def)
 
       
  1738 apply(simp add: Values_recs)
 
       
  1739 apply(auto)
 
       
  1740 apply(drule_tac x="Left x" in bspec)
 
       
  1741 apply(simp)
 
       
  1742 apply(erule ValOrd2.cases)
 
       
  1743 apply(simp_all)
 
       
  1744 apply(drule_tac x="Right vr" in bspec)
 
       
  1745 apply(simp)
 
       
  1746 apply(erule ValOrd2.cases)
 
       
  1747 apply(simp_all)
 
       
  1748 apply(drule_tac x="Right x" in bspec)
 
       
  1749 apply(simp)
 
       
  1750 apply(erule ValOrd2.cases)
 
       
  1751 apply(simp_all)
 
       
  1752 apply(drule_tac x="Left vl" in bspec)
 
       
  1753 apply(simp)
 
       
  1754 apply(erule ValOrd2.cases)
 
       
  1755 apply(simp_all)
 
       
  1756 done
 
       
  1757 
       
  1758 lemma MValue_ALTI1:
 
       
  1759   assumes "MValue vl r1 s"  "\<forall>vr \<in> Values r2 s. length (flat vr) \<le> length (flat vl)"
 
       
  1760   shows "MValue (Left vl) (ALT r1 r2) s"
 
       
  1761 using assms
 
       
  1762 apply(simp add: MValue_def)
 
       
  1763 apply(simp add: Values_recs)
 
       
  1764 apply(auto)
 
       
  1765 apply(rule ValOrd2.intros)
 
       
  1766 apply metis
 
       
  1767 apply(rule ValOrd2.intros)
 
       
  1768 apply metis
 
       
  1769 done
 
       
  1770 
       
  1771 lemma MValue_ALTI2:
 
       
  1772   assumes "MValue vr r2 s"  "\<forall>vl \<in> Values r1 s. length (flat vl) < length (flat vr)"
 
       
  1773   shows "MValue (Right vr) (ALT r1 r2) s"
 
       
  1774 using assms
 
       
  1775 apply(simp add: MValue_def)
 
       
  1776 apply(simp add: Values_recs)
 
       
  1777 apply(auto)
 
       
  1778 apply(rule ValOrd2.intros)
 
       
  1779 apply metis
 
       
  1780 apply(rule ValOrd2.intros)
 
       
  1781 apply metis
 
       
  1782 done
 
       
  1783 
       
  1784 lemma MValue_injval:
 
       
  1785   assumes "MValue v (der c r) s"
 
       
  1786   shows "MValue (injval r c v) r (c#s)"
 
       
  1787 using assms
 
       
  1788 apply(induct c r arbitrary: v s rule: der.induct)
 
       
  1789 apply(simp add: MValue_def)
 
       
  1790 apply(simp add: Values_recs)
 
       
  1791 apply(simp add: MValue_def)
 
       
  1792 apply(simp add: Values_recs)
 
       
  1793 apply(case_tac "c = c'")
 
       
  1794 apply(simp)
 
       
  1795 apply(simp add: MValue_def)
 
       
  1796 apply(simp add: Values_recs)
 
       
  1797 apply(simp add: prefix_def)
 
       
  1798 apply(rule ValOrd2.intros)
 
       
  1799 apply(simp)
 
       
  1800 apply(simp add: MValue_def)
 
       
  1801 apply(simp add: Values_recs)
 
       
  1802 apply(simp)
 
       
  1803 apply(drule MValue_ALTE)
 
       
  1804 apply(erule disjE)
 
       
  1805 apply(auto)[1]
 
       
  1806 apply(rule MValue_ALTI1)
 
       
  1807 apply(simp)
 
       
  1808 apply(subst v4)
 
       
  1809 apply(simp add: MValue_def Values_def)
 
       
  1810 apply(rule ballI)
 
       
  1811 apply(simp)
 
       
  1812 apply(case_tac "flat vr = []")
 
       
  1813 apply(simp)
 
       
  1814 apply(drule_tac x="projval r2 c vr" in bspec)
 
       
  1815 apply(rule Values_projval)
 
       
  1816 apply(simp)
 
       
  1817 apply(simp add: Values_def prefix_def)
 
       
  1818 apply(auto)[1]
 
       
  1819 apply(simp add: append_eq_Cons_conv)
 
       
  1820 apply(auto)[1]
 
       
  1821 apply(simp add: Values_def prefix_def)
 
       
  1822 apply(auto)[1]
 
       
  1823 apply(simp add: append_eq_Cons_conv)
 
       
  1824 apply(auto)[1]
 
       
  1825 apply(subst (asm) v4_proj2)
 
       
  1826 apply(assumption)
 
       
  1827 apply(assumption)
 
       
  1828 apply(simp)
 
       
  1829 apply(auto)[1]
 
       
  1830 apply(rule MValue_ALTI2)
 
       
  1831 apply(simp)
 
       
  1832 apply(subst v4)
 
       
  1833 apply(simp add: MValue_def Values_def)
 
       
  1834 apply(rule ballI)
 
       
  1835 apply(simp)
 
       
  1836 apply(case_tac "flat vl = []")
 
       
  1837 apply(simp)
 
       
  1838 apply(drule_tac x="projval r1 c vl" in bspec)
 
       
  1839 apply(rule Values_projval)
 
       
  1840 apply(simp)
 
       
  1841 apply(simp add: Values_def prefix_def)
 
       
  1842 apply(auto)[1]
 
       
  1843 apply(simp add: append_eq_Cons_conv)
 
       
  1844 apply(auto)[1]
 
       
  1845 apply(simp add: Values_def prefix_def)
 
       
  1846 apply(auto)[1]
 
       
  1847 apply(simp add: append_eq_Cons_conv)
 
       
  1848 apply(auto)[1]
 
       
  1849 apply(subst (asm) v4_proj2)
 
       
  1850 apply(simp add: MValue_def Values_def)
 
       
  1851 apply(assumption)
 
       
  1852 apply(assumption)
 
       
  1853 apply(case_tac "nullable r1")
 
       
  1854 defer
 
       
  1855 apply(simp)
 
       
  1856 apply(frule MValue_SEQE)
 
       
  1857 apply(auto)[1]
 
       
  1858 
       
  1859 
       
  1860 apply(simp add: MValue_def)
 
       
  1861 apply(simp add: Values_recs)
 
       
  1862 
       
  1863 lemma nullable_red:
 
       
  1864   "\<not>nullable (red c r)"
 
       
  1865 apply(induct r)
 
       
  1866 apply(auto)
 
       
  1867 done
 
       
  1868 
       
  1869 lemma twq:
 
       
  1870   assumes "\<turnstile> v : r" 
       
  1871   shows "\<turnstile> injval r c v : red c r"
 
       
  1872 using assms
 
       
  1873 apply(induct)
 
       
  1874 apply(auto)
 
       
  1875 oops
 
       
  1876 
       
  1877 lemma injval_inj_red: "inj_on (injval (red c r) c) {v. \<turnstile> v : r}"
 
       
  1878 using injval_inj
 
       
  1879 apply(auto simp add: inj_on_def)
 
       
  1880 apply(drule_tac x="red c r" in meta_spec)
 
       
  1881 apply(drule_tac x="c" in meta_spec)
 
       
  1882 apply(drule_tac x="x" in spec)
 
       
  1883 apply(drule mp)
 
       
  1884 oops
 
  1629 
  1885 
  1630 lemma 
  1886 lemma 
  1631   assumes "POSIXs v (der c r) s" 
  1887   assumes "POSIXs v (der c r) s" 
  1632   shows "POSIXs (injval r c v) r (c # s)"
 
  1888   shows "POSIXs (injval r c v) r (c # s)"
 
  1633 using assms
 
  1889 using assms
 
  1675 by (metis list.sel(3))
 
  1931 by (metis list.sel(3))
 
  1676 
  1932 
  1677 lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)"
 
  1933 lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)"
 
  1678 by (metis)
 
  1934 by (metis)
 
  1679 
  1935 
  1680 
       
  1681 
       
  1682 lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])"
 
  1936 lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])"
 
  1683 by (metis Prf_flat_L nullable_correctness)
 
  1937 by (metis Prf_flat_L nullable_correctness)
 
  1684 
  1938 
  1685 
  1939 
  1686 lemma LeftRight:
 
  1940 lemma LeftRight:
 
  1768 lemma rr1: 
  2022 lemma rr1: 
  1769   assumes "\<turnstile> v : r" "\<not>nullable r" 
  2023   assumes "\<turnstile> v : r" "\<not>nullable r" 
  1770   shows "flat v \<noteq> []"
 
  2024   shows "flat v \<noteq> []"
 
  1771 using assms
 
  2025 using assms
 
  1772 by (metis Prf_flat_L nullable_correctness)
 
  2026 by (metis Prf_flat_L nullable_correctness)
 
       
  2027 
       
  2028 section {* TESTTEST *}
 
       
  2029 
       
  2030 inductive ValOrdA :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ A\<succ>_ _" [100, 100, 100] 100)
 
       
  2031 where
 
       
  2032   "v2 A\<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) A\<succ>(SEQ r1 r2) (Seq v1 v2')" 
       
  2033 | "v1 A\<succ>r1 v1' \<Longrightarrow> (Seq v1 v2) A\<succ>(SEQ r1 r2) (Seq v1' v2')" 
       
  2034 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) A\<succ>(ALT r1 r2) (Right v2)"
 
       
  2035 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) A\<succ>(ALT r1 r2) (Left v1)"
 
       
  2036 | "v2 A\<succ>r2 v2' \<Longrightarrow> (Right v2) A\<succ>(ALT r1 r2) (Right v2')"
 
       
  2037 | "v1 A\<succ>r1 v1' \<Longrightarrow> (Left v1) A\<succ>(ALT r1 r2) (Left v1')"
 
       
  2038 | "Void A\<succ>EMPTY Void"
 
       
  2039 | "(Char c) A\<succ>(CHAR c) (Char c)"
 
       
  2040 
       
  2041 inductive ValOrd4 :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ 4\<succ> _ _" [100, 100] 100)
 
       
  2042 where
 
       
  2043   (*"v1 4\<succ>(der c r) v1' \<Longrightarrow> (injval r c v1) 4\<succ>r (injval r c v1')" 
       
  2044 | "\<lbrakk>v1 4\<succ>r v2; v2 4\<succ>r v3\<rbrakk> \<Longrightarrow> v1 4\<succ>r v3" 
       
  2045 |*) 
       
  2046   "\<lbrakk>v1 4\<succ>r1 v1'; flat v2 = flat v2'; \<turnstile> v2 : r2; \<turnstile> v2' : r2\<rbrakk> \<Longrightarrow> (Seq v1 v2) 4\<succ>(SEQ r1 r2)  (Seq v1' v2')"
 
       
  2047 | "\<lbrakk>v2 4\<succ>r2 v2'; \<turnstile> v1 : r1\<rbrakk> \<Longrightarrow> (Seq v1 v2) 4\<succ>(SEQ r1 r2)  (Seq v1 v2')"
 
       
  2048 | "\<lbrakk>flat v1 = flat v2; \<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> (Left v1) 4\<succ>(ALT r1 r2) (Right v2)"
 
       
  2049 | "v2 4\<succ>r2 v2' \<Longrightarrow> (Right v2) 4\<succ>(ALT r1 r2) (Right v2')"
 
       
  2050 | "v1 4\<succ>r1 v1' \<Longrightarrow> (Left v1) 4\<succ>(ALT r1 r2) (Left v1')"
 
       
  2051 | "Void 4\<succ>(EMPTY) Void"
 
       
  2052 | "(Char c) 4\<succ>(CHAR c) (Char c)"
 
       
  2053 
       
  2054 lemma ValOrd4_Prf:
 
       
  2055   assumes "v1 4\<succ>r v2"
 
       
  2056   shows "\<turnstile> v1 : r \<and> \<turnstile> v2 : r"
 
       
  2057 using assms
 
       
  2058 apply(induct v1 r v2)
 
       
  2059 apply(auto intro: Prf.intros)
 
       
  2060 done
 
       
  2061 
       
  2062 lemma ValOrd4_flat:
 
       
  2063   assumes "v1 4\<succ>r v2"
 
       
  2064   shows "flat v1 = flat v2"
 
       
  2065 using assms
 
       
  2066 apply(induct v1 r v2)
 
       
  2067 apply(simp_all)
 
       
  2068 done
 
       
  2069 
       
  2070 lemma ValOrd4_refl:
 
       
  2071   assumes "\<turnstile> v : r"
 
       
  2072   shows "v 4\<succ>r v"
 
       
  2073 using assms
 
       
  2074 apply(induct v r)
 
       
  2075 apply(auto intro: ValOrd4.intros)
 
       
  2076 done
 
       
  2077 
       
  2078 lemma 
       
  2079   assumes "v1 4\<succ>r v2" "v2 4\<succ>r v3" 
       
  2080   shows "v1 A\<succ>r v3"
 
       
  2081 using assms
 
       
  2082 apply(induct v1 r v2 arbitrary: v3)
 
       
  2083 apply(rotate_tac 5)
 
       
  2084 apply(erule ValOrd4.cases)
 
       
  2085 apply(simp_all)
 
       
  2086 apply(clarify)
 
       
  2087 apply (metis ValOrdA.intros(2))
 
       
  2088 apply(clarify)
 
       
  2089 apply (metis ValOrd4_refl ValOrdA.intros(2))
 
       
  2090 apply(rotate_tac 3)
 
       
  2091 apply(erule ValOrd4.cases)
 
       
  2092 apply(simp_all)
 
       
  2093 apply(clarify)
 
       
  2094 
       
  2095 apply (metis ValOrdA.intros(2))
 
       
  2096 apply (metis ValOrdA.intros(1))
 
       
  2097 apply (metis ValOrdA.intros(3) order_refl)
 
       
  2098 apply (auto intro: ValOrdA.intros)
 
       
  2099 done
 
       
  2100 
       
  2101 lemma 
       
  2102   assumes "v1 4\<succ>r v2"
 
       
  2103   shows "v1 A\<succ>r v2"
 
       
  2104 using assms
 
       
  2105 apply(induct v1 r v2 arbitrary:)
 
       
  2106 apply (metis ValOrdA.intros(2))
 
       
  2107 apply (metis ValOrdA.intros(1))
 
       
  2108 apply (metis ValOrdA.intros(3) order_refl)
 
       
  2109 apply (auto intro: ValOrdA.intros)
 
       
  2110 done
 
       
  2111 
       
  2112 lemma 
       
  2113   assumes "v1 \<succ>r v2" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "flat v1 = flat v2"
 
       
  2114   shows "v1 4\<succ>r v2"
 
       
  2115 using assms
 
       
  2116 apply(induct v1 r v2 arbitrary:)
 
       
  2117 apply(erule Prf.cases)
 
       
  2118 apply(simp_all (no_asm_use))[5]
 
       
  2119 apply(erule Prf.cases)
 
       
  2120 apply(simp_all (no_asm_use))[5]
 
       
  2121 apply(clarify)
 
       
  2122 apply (metis ValOrd4.intros(4) ValOrd4_flat ValOrd4_refl)
 
       
  2123 apply(simp)
 
       
  2124 apply(erule Prf.cases)
 
       
  2125 apply(simp_all (no_asm_use))[5]
 
       
  2126 apply(erule Prf.cases)
 
       
  2127 apply(simp_all (no_asm_use))[5]
 
       
  2128 apply(clarify)
 
       
  2129 
       
  2130 lemma 
       
  2131   assumes "v1 \<succ>r v2" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "flat v1 = flat v2"
 
       
  2132   shows "v1 4\<succ>r v2"
 
       
  2133 using assms
 
       
  2134 apply(induct v1 r v2 arbitrary:)
 
       
  2135 apply(erule Prf.cases)
 
       
  2136 apply(simp_all (no_asm_use))[5]
 
       
  2137 apply(erule Prf.cases)
 
       
  2138 apply(simp_all (no_asm_use))[5]
 
       
  2139 apply(clarify)
 
       
  2140 apply (metis ValOrd4.intros(4) ValOrd4_flat ValOrd4_refl)
 
       
  2141 apply(simp)
 
       
  2142 apply(erule Prf.cases)
 
       
  2143 apply(simp_all (no_asm_use))[5]
 
       
  2144 apply(erule Prf.cases)
 
       
  2145 apply(simp_all (no_asm_use))[5]
 
       
  2146 apply(clarify)
 
       
  2147 
       
  2148 
       
  2149 apply(simp)
 
       
  2150 apply(erule Prf.cases)
 
       
  2151 
       
  2152 
       
  2153 
  1773 
  2154 
  1774 lemma rr2: "hd (flats v) \<noteq> [] \<Longrightarrow> flats v \<noteq> []"
 
  2155 lemma rr2: "hd (flats v) \<noteq> [] \<Longrightarrow> flats v \<noteq> []"
 
  1775 apply(induct v)
 
  2156 apply(induct v)
 
  1776 apply(auto)
 
  2157 apply(auto)
 
  1777 done
 
  2158 done
 
  1796 apply(simp)
 
  2177 apply(simp)
 
  1797 thm v3s_proj
 
  2178 thm v3s_proj
 
  1798 apply(drule v3s_proj)
 
  2179 apply(drule v3s_proj)
 
  1799 oops
 
  2180 oops
 
  1800 
  2181 
       
  2182 term Values
 
       
  2183 (* HERE *)
 
       
  2184 
  1801 lemma Prf_inj_test:
 
  2185 lemma Prf_inj_test:
 
  1802   assumes "v1 2\<succ> v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" 
  2186   assumes "v1 \<succ>(der c r) v2" 
  1803   "length (flat v1) = length (flat v2)"
 
  2187           "v1 \<in> Values (der c r) s"
 
       
  2188           "v2 \<in> Values (der c r) s"
 
       
  2189           "injval r c v1 \<in> Values r (c#s)"
 
       
  2190           "injval r c v2 \<in> Values r (c#s)"
 
  1804   shows "(injval r c v1) 2\<succ>  (injval r c v2)"
 
  2191   shows "(injval r c v1) 2\<succ>  (injval r c v2)"
 
  1805 using assms
 
  2192 using assms
 
  1806 apply(induct c r arbitrary: v1 v2 rule: der.induct)
 
  2193 apply(induct c r arbitrary: v1 v2 s rule: der.induct)
 
  1807 (* NULL case *)
 
  2194 (* NULL case *)
 
  1808 apply(simp)
 
  2195 apply(simp add: Values_recs)
 
  1809 apply(erule Prf.cases)
 
       
  1810 apply(simp_all)[5]
 
       
  1811 (* EMPTY case *)
 
  2196 (* EMPTY case *)
 
  1812 apply(simp)
 
  2197 apply(simp add: Values_recs)
 
  1813 apply(erule Prf.cases)
 
       
  1814 apply(simp_all)[5]
 
       
  1815 (* CHAR case *)
 
  2198 (* CHAR case *)
 
  1816 apply(case_tac "c = c'")
 
  2199 apply(case_tac "c = c'")
 
  1817 apply(simp)
 
  2200 apply(simp)
 
  1818 apply(erule Prf.cases)
 
  2201 apply(simp add: Values_recs)
 
  1819 apply(simp_all)[5]
 
  2202 apply (metis ValOrd2.intros(8))
 
  1820 apply(erule Prf.cases)
 
  2203 apply(simp add: Values_recs)
 
  1821 apply(simp_all)[5]
 
       
  1822 apply(erule ValOrd2.cases)
 
       
  1823 apply(simp_all)[8]
 
       
  1824 apply(rule ValOrd2.intros)
 
       
  1825 apply(simp)
 
       
  1826 apply(erule Prf.cases)
 
       
  1827 apply(simp_all)[5]
 
       
  1828 (* ALT case *)
 
  2204 (* ALT case *)
 
  1829 apply(simp)
 
  2205 apply(simp)
 
  1830 apply(erule Prf.cases)
 
  2206 apply(simp add: Values_recs)
 
  1831 apply(simp_all)[5]
 
  2207 apply(auto)[1]
 
  1832 apply(auto)[2]
 
  2208 apply(erule ValOrd.cases)
 
  1833 apply(erule Prf.cases)
 
  2209 apply(simp_all)[8]
 
  1834 apply(simp_all)[5]
 
  2210 apply (metis ValOrd2.intros(6))
 
  1835 apply(auto)[2]
 
  2211 apply(erule ValOrd.cases)
 
  1836 apply(erule ValOrd2.cases)
 
       
  1837 apply(simp_all)[8]
 
       
  1838 apply(rule ValOrd2.intros)
 
       
  1839 apply(auto)[1]
 
       
  1840 apply(erule ValOrd2.cases)
 
       
  1841 apply(simp_all)[8]
 
  2212 apply(simp_all)[8]
 
  1842 apply(rule ValOrd2.intros)
 
  2213 apply(rule ValOrd2.intros)
 
  1843 apply(subst v4)
 
  2214 apply(subst v4)
 
       
  2215 apply(simp add: Values_def)
 
       
  2216 apply(subst v4)
 
       
  2217 apply(simp add: Values_def)
 
       
  2218 apply(simp)
 
       
  2219 apply(erule ValOrd.cases)
 
       
  2220 apply(simp_all)[8]
 
       
  2221 apply(rule ValOrd2.intros)
 
       
  2222 apply(subst v4)
 
       
  2223 apply(simp add: Values_def)
 
       
  2224 apply(subst v4)
 
       
  2225 apply(simp add: Values_def)
 
       
  2226 apply(simp)
 
       
  2227 apply(erule ValOrd.cases)
 
       
  2228 apply(simp_all)[8]
 
       
  2229 apply (metis ValOrd2.intros(5))
 
       
  2230 (* SEQ case*)
 
       
  2231 apply(simp)
 
       
  2232 apply(case_tac "nullable r1")
 
       
  2233 apply(simp)
 
       
  2234 defer
 
       
  2235 apply(simp)
 
       
  2236 apply(simp add: Values_recs)
 
       
  2237 apply(auto)[1]
 
       
  2238 apply(erule ValOrd.cases)
 
       
  2239 apply(simp_all)[8]
 
       
  2240 apply(clarify)
 
       
  2241 apply(rule ValOrd2.intros)
 
       
  2242 apply(simp)
 
       
  2243 apply (metis Ord1)
 
       
  2244 apply(clarify)
 
       
  2245 apply(rule ValOrd2.intros)
 
       
  2246 apply(subgoal_tac "rest v1 (flat v1 @ flat v2) = flat v2")
 
       
  2247 apply(simp)
 
       
  2248 apply(subgoal_tac "rest (injval r1 c v1) (c # flat v1 @ flat v2) = flat v2")
 
       
  2249 apply(simp)
 
       
  2250 
  1844 apply metis
 
  2251 apply metis
 
       
  2252 using injval_inj
 
       
  2253 apply(simp add: Values_def inj_on_def)
 
       
  2254 apply metis
 
       
  2255 apply(simp add: Values_recs)
 
       
  2256 apply(auto)[1]
 
       
  2257 apply(erule ValOrd.cases)
 
       
  2258 apply(simp_all)[8]
 
       
  2259 apply(clarify)
 
       
  2260 apply(erule ValOrd.cases)
 
       
  2261 apply(simp_all)[8]
 
       
  2262 apply(clarify)
 
       
  2263 apply (metis Ord1 ValOrd2.intros(1))
 
       
  2264 apply(clarify)
 
       
  2265 apply(rule ValOrd2.intros(2))
 
       
  2266 apply metis
 
       
  2267 using injval_inj
 
       
  2268 apply(simp add: Values_def inj_on_def)
 
       
  2269 apply metis
 
       
  2270 apply(erule ValOrd.cases)
 
       
  2271 apply(simp_all)[8]
 
       
  2272 apply(rule ValOrd2.intros(2))
 
       
  2273 thm h
 
       
  2274 apply(rule Ord1)
 
       
  2275 apply(rule h)
 
       
  2276 apply(simp)
 
       
  2277 apply(simp add: Values_def)
 
       
  2278 apply(simp add: Values_def)
 
       
  2279 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  2280 apply(erule ValOrd.cases)
 
       
  2281 apply(simp_all)[8]
 
       
  2282 apply(clarify)
 
       
  2283 apply(simp add: Values_def)
 
       
  2284 defer
 
       
  2285 apply(erule ValOrd.cases)
 
       
  2286 apply(simp_all)[8]
 
       
  2287 apply(clarify)
 
       
  2288 apply(rule ValOrd2.intros(1))
 
       
  2289 apply(rotate_tac 1)
 
       
  2290 apply(drule_tac x="v2" in meta_spec)
 
       
  2291 apply(rotate_tac 8)
 
       
  2292 apply(drule_tac x="v2'" in meta_spec)
 
       
  2293 apply(rotate_tac 8)
 
       
  2294 apply(drule_tac x="s" in meta_spec)
 
       
  2295 apply(simp)
 
       
  2296 apply(drule_tac meta_mp)
 
       
  2297 apply(simp add: rest_def mkeps_flat)
 
       
  2298 apply(drule_tac meta_mp)
 
       
  2299 apply(simp add: rest_def mkeps_flat)
 
       
  2300 apply(simp)
 
       
  2301 apply(simp add: rest_def mkeps_flat)
 
       
  2302 apply(subst (asm) (5) v4)
 
       
  2303 apply(simp)
 
       
  2304 apply(subst (asm) (5) v4)
 
       
  2305 apply(simp)
 
       
  2306 apply(subst (asm) (5) v4)
 
       
  2307 apply(simp)
 
       
  2308 apply(simp)
 
       
  2309 apply(clarify)
 
       
  2310 apply(simp add: prefix_Cons)
 
       
  2311 apply(subgoal_tac "((flat v1c) @ (flat v2b)) \<sqsubseteq> (flat v2)")
 
       
  2312 prefer 2
 
       
  2313 apply(simp add: prefix_def)
 
       
  2314 apply(auto)[1]
 
       
  2315 (* HEREHERE *)
 
       
  2316 
       
  2317 
       
  2318 lemma Prf_inj_test:
 
       
  2319   assumes "v1 \<succ>r v2" 
       
  2320           "v1 \<in> Values r s"
 
       
  2321           "v2 \<in> Values r s"
 
       
  2322           "injval r c v1 \<in> Values (red c r) (c#s)"
 
       
  2323           "injval r c v2 \<in> Values (red c r) (c#s)"
 
       
  2324   shows "(injval r c v1) \<succ>(red c r)  (injval r c v2)"
 
       
  2325 using assms
 
       
  2326 apply(induct v1 r v2 arbitrary: s rule: ValOrd.induct)
 
       
  2327 apply(simp add: Values_recs)
 
       
  2328 apply (metis ValOrd.intros(1))
 
       
  2329 apply(simp add: Values_recs)
 
       
  2330 apply(rule ValOrd.intros(2))
 
       
  2331 apply(metis)
 
       
  2332 defer
 
       
  2333 apply(simp add: Values_recs)
 
       
  2334 apply(rule ValOrd.intros)
 
  1845 apply(subst v4)
 
  2335 apply(subst v4)
 
  1846 apply (metis)
 
  2336 apply(simp add: Values_def)
 
  1847 apply(simp)
 
  2337 apply(subst v4)
 
  1848 apply(erule Prf.cases)
 
  2338 apply(simp add: Values_def)
 
  1849 apply(simp_all)[5]
 
  2339 using injval_inj_red
 
  1850 apply(auto)[2]
 
  2340 apply(simp add: Values_def inj_on_def)
 
  1851 apply(erule ValOrd2.cases)
 
  2341 apply(rule notI)
 
       
  2342 apply(drule_tac x="r1" in meta_spec)
 
       
  2343 apply(drule_tac x="c" in meta_spec)
 
       
  2344 apply(drule_tac x="injval r1 c v1" in spec)
 
       
  2345 apply(simp)
 
       
  2346 
       
  2347 apply(drule_tac x="c" in meta_spec)
 
       
  2348 
       
  2349 apply metis
 
       
  2350 apply (metis ValOrd.intros(1))
 
       
  2351 
       
  2352 
       
  2353 
       
  2354 done
 
       
  2355 (* EMPTY case *)
 
       
  2356 apply(simp add: Values_recs)
 
       
  2357 (* CHAR case *)
 
       
  2358 apply(case_tac "c = c'")
 
       
  2359 apply(simp)
 
       
  2360 apply(simp add: Values_recs)
 
       
  2361 apply (metis ValOrd2.intros(8))
 
       
  2362 apply(simp add: Values_recs)
 
       
  2363 (* ALT case *)
 
       
  2364 apply(simp)
 
       
  2365 apply(simp add: Values_recs)
 
       
  2366 apply(auto)[1]
 
       
  2367 apply(erule ValOrd.cases)
 
       
  2368 apply(simp_all)[8]
 
       
  2369 apply (metis ValOrd2.intros(6))
 
       
  2370 apply(erule ValOrd.cases)
 
  1852 apply(simp_all)[8]
 
  2371 apply(simp_all)[8]
 
  1853 apply(rule ValOrd2.intros)
 
  2372 apply(rule ValOrd2.intros)
 
  1854 apply(erule ValOrd2.cases)
 
  2373 apply(subst v4)
 
  1855 apply(simp_all)[8]
 
  2374 apply(simp add: Values_def)
 
       
  2375 apply(subst v4)
 
       
  2376 apply(simp add: Values_def)
 
       
  2377 apply(simp)
 
       
  2378 apply(erule ValOrd.cases)
 
       
  2379 apply(simp_all)[8]
 
       
  2380 apply(rule ValOrd2.intros)
 
       
  2381 apply(subst v4)
 
       
  2382 apply(simp add: Values_def)
 
       
  2383 apply(subst v4)
 
       
  2384 apply(simp add: Values_def)
 
       
  2385 apply(simp)
 
       
  2386 apply(erule ValOrd.cases)
 
       
  2387 apply(simp_all)[8]
 
       
  2388 apply (metis ValOrd2.intros(5))
 
  1856 (* SEQ case*)
 
  2389 (* SEQ case*)
 
  1857 apply(simp)
 
  2390 apply(simp)
 
  1858 apply(case_tac "nullable r1")
 
  2391 apply(case_tac "nullable r1")
 
  1859 apply(simp)
 
  2392 apply(simp)
 
  1860 defer
 
  2393 defer
 
  1861 apply(simp)
 
  2394 apply(simp)
 
  1862 apply(erule Prf.cases)
 
  2395 apply(simp add: Values_recs)
 
  1863 apply(simp_all)[5]
 
  2396 apply(auto)[1]
 
  1864 apply(erule Prf.cases)
 
  2397 apply(erule ValOrd.cases)
 
  1865 apply(simp_all)[5]
 
       
  1866 apply(clarify)
 
       
  1867 apply(erule ValOrd2.cases)
 
       
  1868 apply(simp_all)[8]
 
  2398 apply(simp_all)[8]
 
  1869 apply(clarify)
 
  2399 apply(clarify)
 
  1870 apply(rule ValOrd2.intros)
 
  2400 apply(rule ValOrd2.intros)
 
  1871 apply(simp)
 
  2401 apply(simp)
 
  1872 apply(rule ValOrd2.intros)
 
  2402 apply (metis Ord1)
 
  1873 apply(auto)[1]
 
  2403 apply(clarify)
 
  1874 
       
  1875 using injval_inj
 
       
  1876 apply(simp add: inj_on_def)
 
       
  1877 apply metis
 
       
  1878 apply(erule Prf.cases)
 
       
  1879 apply(simp_all)[5]
 
       
  1880 apply(erule Prf.cases)
 
       
  1881 apply(simp_all)[5]
 
       
  1882 apply(clarify)
 
       
  1883 apply(erule Prf.cases)
 
       
  1884 apply(simp_all)[5]
 
       
  1885 apply(erule Prf.cases)
 
       
  1886 apply(simp_all)[5]
 
       
  1887 apply(clarify)
 
       
  1888 apply(erule ValOrd2.cases)
 
       
  1889 apply(simp_all)[8]
 
       
  1890 apply(clarify)
 
       
  1891 apply(erule ValOrd2.cases)
 
       
  1892 apply(simp_all)[8]
 
       
  1893 apply(clarify)
 
       
  1894 apply (metis ValOrd2.intros(1))
 
       
  1895 apply(rule ValOrd2.intros)
 
  2404 apply(rule ValOrd2.intros)
 
  1896 apply metis
 
  2405 apply metis
 
  1897 using injval_inj
 
  2406 using injval_inj
 
  1898 apply(simp add: inj_on_def)
 
  2407 apply(simp add: Values_def inj_on_def)
 
  1899 apply metis
 
  2408 apply metis
 
  1900 apply(clarify)
 
  2409 apply(simp add: Values_recs)
 
  1901 apply(simp)
 
  2410 apply(auto)[1]
 
  1902 apply(erule Prf.cases)
 
  2411 apply(erule ValOrd.cases)
 
  1903 apply(simp_all)[5]
 
  2412 apply(simp_all)[8]
 
  1904 apply(clarify)
 
  2413 apply(clarify)
 
  1905 apply(rule ValOrd2.intros)
 
  2414 apply(erule ValOrd.cases)
 
       
  2415 apply(simp_all)[8]
 
       
  2416 apply(clarify)
 
       
  2417 apply (metis Ord1 ValOrd2.intros(1))
 
       
  2418 apply(clarify)
 
       
  2419 apply(rule ValOrd2.intros(2))
 
       
  2420 apply metis
 
       
  2421 using injval_inj
 
       
  2422 apply(simp add: Values_def inj_on_def)
 
       
  2423 apply metis
 
       
  2424 apply(erule ValOrd.cases)
 
       
  2425 apply(simp_all)[8]
 
       
  2426 apply(rule ValOrd2.intros(2))
 
       
  2427 thm h
 
  1906 apply(rule Ord1)
 
  2428 apply(rule Ord1)
 
  1907 apply(rule h)
 
  2429 apply(rule h)
 
  1908 apply(simp)
 
  2430 apply(simp)
 
  1909 apply(simp)
 
  2431 apply(simp add: Values_def)
 
       
  2432 apply(simp add: Values_def)
 
  1910 apply (metis list.distinct(1) mkeps_flat v4)
 
  2433 apply (metis list.distinct(1) mkeps_flat v4)
 
  1911 apply(clarify)
 
  2434 apply(erule ValOrd.cases)
 
  1912 apply(erule Prf.cases)
 
  2435 apply(simp_all)[8]
 
  1913 apply(simp_all)[5]
 
  2436 apply(clarify)
 
  1914 apply(clarify)
 
  2437 apply(simp add: Values_def)
 
  1915 apply(rotate_tac 7)
 
       
  1916 apply(erule Prf.cases)
 
       
  1917 apply(simp_all)[5]
 
       
  1918 apply(clarify)
 
       
  1919 defer
 
  2438 defer
 
  1920 apply(clarify)
 
  2439 apply(erule ValOrd.cases)
 
  1921 apply(erule ValOrd2.cases)
 
  2440 apply(simp_all)[8]
 
  1922 apply(simp_all)[8]
 
  2441 apply(clarify)
 
  1923 apply(clarify)
 
  2442 apply(rule ValOrd2.intros(1))
 
  1924 apply (metis ValOrd2.intros(1))
 
  2443 apply(rotate_tac 1)
 
  1925 apply(erule ValOrd2.cases)
 
  2444 apply(drule_tac x="v2" in meta_spec)
 
  1926 apply(simp_all)[8]
 
  2445 apply(rotate_tac 8)
 
  1927 apply(clarify)
 
  2446 apply(drule_tac x="v2'" in meta_spec)
 
  1928 apply(simp)
 
  2447 apply(rotate_tac 8)
 
  1929 apply (rule_tac ValOrd2.intros(2))
 
  2448 apply(drule_tac x="s" in meta_spec)
 
       
  2449 apply(simp)
 
       
  2450 apply(drule_tac meta_mp)
 
       
  2451 apply(simp add: rest_def mkeps_flat)
 
       
  2452 apply(drule_tac meta_mp)
 
       
  2453 apply(simp add: rest_def mkeps_flat)
 
       
  2454 apply(simp)
 
       
  2455 apply(simp add: rest_def mkeps_flat)
 
       
  2456 apply(subst (asm) (5) v4)
 
       
  2457 apply(simp)
 
       
  2458 apply(subst (asm) (5) v4)
 
       
  2459 apply(simp)
 
       
  2460 apply(subst (asm) (5) v4)
 
       
  2461 apply(simp)
 
       
  2462 apply(simp)
 
       
  2463 apply(clarify)
 
       
  2464 apply(simp add: prefix_Cons)
 
       
  2465 apply(subgoal_tac "((flat v1c) @ (flat v2b)) \<sqsubseteq> (flat v2)")
 
  1930 prefer 2
 
  2466 prefer 2
 
  1931 apply (metis list.distinct(1) mkeps_flat v4)
 
  2467 apply(simp add: prefix_def)
 
  1932 
  2468 apply(auto)[1]
 
       
  2469 (* HEREHERE *)
 
  1933 
  2470 
  1934 lemma Prf_inj_test:
 
  2471 lemma Prf_inj_test:
 
  1935   assumes "v1 2\<succ> v2" "\<Turnstile>s1 v1 : der c r" "\<Turnstile>s2 v2 : der c r"  
  2472   assumes "v1 \<succ>(der c r) v2" 
       
  2473           "v1 \<in> Values (der c r) s"
 
       
  2474           "v2 \<in> Values (der c r) s"
 
       
  2475           "injval r c v1 \<in> Values r (c#s)"
 
       
  2476           "injval r c v2 \<in> Values r (c#s)"
 
  1936   shows "(injval r c v1) 2\<succ>  (injval r c v2)"
 
  2477   shows "(injval r c v1) 2\<succ>  (injval r c v2)"
 
  1937 using assms
 
  2478 using assms
 
  1938 apply(induct c r arbitrary: s1 s2 v1 v2 rule: der.induct)
 
  2479 apply(induct c r arbitrary: v1 v2 s rule: der.induct)
 
  1939 (* NULL case *)
 
  2480 (* NULL case *)
 
  1940 apply(erule Prfs.cases)
 
  2481 apply(simp add: Values_recs)
 
  1941 apply(simp_all)[5]
 
       
  1942 (* EMPTY case *)
 
  2482 (* EMPTY case *)
 
  1943 apply(simp)
 
  2483 apply(simp add: Values_recs)
 
  1944 apply(erule Prfs.cases)
 
       
  1945 apply(simp_all)[5]
 
       
  1946 (* CHAR case *)
 
  2484 (* CHAR case *)
 
  1947 apply(case_tac "c = c'")
 
  2485 apply(case_tac "c = c'")
 
  1948 apply(simp)
 
  2486 apply(simp)
 
  1949 apply(erule Prfs.cases)
 
  2487 apply(simp add: Values_recs)
 
  1950 apply(simp_all)[5]
 
  2488 apply (metis ValOrd2.intros(8))
 
  1951 apply(erule Prfs.cases)
 
  2489 apply(simp add: Values_recs)
 
  1952 apply(simp_all)[5]
 
       
  1953 apply(erule ValOrd2.cases)
 
       
  1954 apply(simp_all)[8]
 
       
  1955 apply(rule ValOrd2.intros)
 
       
  1956 apply(simp)
 
       
  1957 apply(erule Prfs.cases)
 
       
  1958 apply(simp_all)[5]
 
       
  1959 (* ALT case *)
 
  2490 (* ALT case *)
 
  1960 apply(simp)
 
  2491 apply(simp)
 
  1961 apply(erule Prfs.cases)
 
  2492 apply(simp add: Values_recs)
 
  1962 apply(simp_all)[5]
 
  2493 apply(auto)[1]
 
  1963 apply(auto)[2]
 
  2494 apply(erule ValOrd.cases)
 
  1964 apply(erule Prfs.cases)
 
  2495 apply(simp_all)[8]
 
  1965 apply(simp_all)[5]
 
  2496 apply (metis ValOrd2.intros(6))
 
  1966 apply(auto)[2]
 
  2497 apply(erule ValOrd.cases)
 
  1967 apply(erule ValOrd2.cases)
 
       
  1968 apply(simp_all)[8]
 
       
  1969 apply(rule ValOrd2.intros)
 
       
  1970 apply(auto)[1]
 
       
  1971 apply(erule ValOrd2.cases)
 
       
  1972 apply(simp_all)[8]
 
  2498 apply(simp_all)[8]
 
  1973 apply(rule ValOrd2.intros)
 
  2499 apply(rule ValOrd2.intros)
 
  1974 apply(subst v4)
 
  2500 apply(subst v4)
 
  1975 apply (metis Prfs_Prf)
 
  2501 apply(simp add: Values_def)
 
  1976 apply(subst v4)
 
  2502 apply(subst v4)
 
  1977 apply (metis Prfs_Prf)
 
  2503 apply(simp add: Values_def)
 
  1978 apply(simp)
 
  2504 apply(simp)
 
  1979 apply(erule Prfs.cases)
 
  2505 apply(erule ValOrd.cases)
 
  1980 apply(simp_all)[5]
 
       
  1981 apply(auto)[2]
 
       
  1982 apply(erule ValOrd2.cases)
 
       
  1983 apply(simp_all)[8]
 
  2506 apply(simp_all)[8]
 
  1984 apply(rule ValOrd2.intros)
 
  2507 apply(rule ValOrd2.intros)
 
  1985 apply(subst v4)
 
  2508 apply(subst v4)
 
  1986 apply (metis Prfs_Prf)
 
  2509 apply(simp add: Values_def)
 
  1987 apply(subst v4)
 
  2510 apply(subst v4)
 
  1988 apply (metis Prfs_Prf)
 
  2511 apply(simp add: Values_def)
 
  1989 apply(simp)
 
  2512 apply(simp)
 
  1990 apply(erule ValOrd2.cases)
 
  2513 apply(erule ValOrd.cases)
 
  1991 apply(simp_all)[8]
 
  2514 apply(simp_all)[8]
 
       
  2515 apply (metis ValOrd2.intros(5))
 
       
  2516 (* SEQ case*)
 
       
  2517 apply(simp)
 
       
  2518 apply(case_tac "nullable r1")
 
       
  2519 apply(simp)
 
       
  2520 defer
 
       
  2521 apply(simp)
 
       
  2522 apply(simp add: Values_recs)
 
       
  2523 apply(auto)[1]
 
       
  2524 apply(erule ValOrd.cases)
 
       
  2525 apply(simp_all)[8]
 
       
  2526 apply(clarify)
 
       
  2527 apply(rule ValOrd2.intros)
 
       
  2528 apply(simp)
 
       
  2529 apply (metis Ord1)
 
       
  2530 apply(clarify)
 
  1992 apply(rule ValOrd2.intros)
 
  2531 apply(rule ValOrd2.intros)
 
  1993 apply metis
 
  2532 apply metis
 
  1994 (* SEQ case*)
 
  2533 using injval_inj
 
  1995 apply(simp)
 
  2534 apply(simp add: Values_def inj_on_def)
 
  1996 apply(case_tac "nullable r1")
 
       
  1997 apply(simp)
 
       
  1998 defer
 
       
  1999 apply(simp)
 
       
  2000 apply(erule Prfs.cases)
 
       
  2001 apply(simp_all)[5]
 
       
  2002 apply(erule Prfs.cases)
 
       
  2003 apply(simp_all)[5]
 
       
  2004 apply(clarify)
 
       
  2005 apply(erule ValOrd2.cases)
 
       
  2006 apply(simp_all)[8]
 
       
  2007 apply(clarify)
 
       
  2008 apply(rule ValOrd2.intros)
 
       
  2009 apply(simp)
 
       
  2010 apply(rule ValOrd2.intros)
 
       
  2011 apply(auto)[1]
 
       
  2012 defer
 
       
  2013 apply(erule Prfs.cases)
 
       
  2014 apply(simp_all)[5]
 
       
  2015 apply(erule Prfs.cases)
 
       
  2016 apply(simp_all)[5]
 
       
  2017 apply(clarify)
 
       
  2018 apply(erule Prfs.cases)
 
       
  2019 apply(simp_all)[5]
 
       
  2020 apply(erule Prfs.cases)
 
       
  2021 apply(simp_all)[5]
 
       
  2022 apply(clarify)
 
       
  2023 apply(erule ValOrd2.cases)
 
       
  2024 apply(simp_all)[8]
 
       
  2025 apply(clarify)
 
       
  2026 apply(erule ValOrd2.cases)
 
       
  2027 apply(simp_all)[8]
 
       
  2028 apply(clarify)
 
       
  2029 apply (metis ValOrd2.intros(1))
 
       
  2030 apply(rule ValOrd2.intros)
 
       
  2031 apply metis
 
  2535 apply metis
 
  2032 defer
 
  2536 apply(simp add: Values_recs)
 
  2033 apply(clarify)
 
  2537 apply(auto)[1]
 
  2034 apply(simp)
 
  2538 apply(erule ValOrd.cases)
 
  2035 apply(erule Prfs.cases)
 
  2539 apply(simp_all)[8]
 
  2036 apply(simp_all)[5]
 
  2540 apply(clarify)
 
  2037 apply(clarify)
 
  2541 apply(erule ValOrd.cases)
 
  2038 apply(rule ValOrd2.intros)
 
  2542 apply(simp_all)[8]
 
       
  2543 apply(clarify)
 
       
  2544 apply (metis Ord1 ValOrd2.intros(1))
 
       
  2545 apply(clarify)
 
       
  2546 apply(rule ValOrd2.intros(2))
 
       
  2547 apply metis
 
       
  2548 using injval_inj
 
       
  2549 apply(simp add: Values_def inj_on_def)
 
       
  2550 apply metis
 
       
  2551 apply(erule ValOrd.cases)
 
       
  2552 apply(simp_all)[8]
 
       
  2553 apply(rule ValOrd2.intros(2))
 
       
  2554 thm h
 
  2039 apply(rule Ord1)
 
  2555 apply(rule Ord1)
 
  2040 apply(rule h)
 
  2556 apply(rule h)
 
  2041 apply(simp)
 
  2557 apply(simp)
 
  2042 apply(simp)
 
  2558 apply(simp add: Values_def)
 
  2043 apply (metis Prfs_Prf)
 
  2559 apply(simp add: Values_def)
 
       
  2560 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  2561 apply(erule ValOrd.cases)
 
       
  2562 apply(simp_all)[8]
 
       
  2563 apply(clarify)
 
       
  2564 apply(simp add: Values_def)
 
  2044 defer
 
  2565 defer
 
  2045 apply(erule Prfs.cases)
 
  2566 apply(erule ValOrd.cases)
 
  2046 apply(simp_all)[5]
 
  2567 apply(simp_all)[8]
 
  2047 apply(clarify)
 
  2568 apply(clarify)
 
  2048 apply(rotate_tac 6)
 
  2569 apply(rule ValOrd2.intros(1))
 
  2049 apply(erule Prfs.cases)
 
  2570 apply(rotate_tac 1)
 
  2050 apply(simp_all)[5]
 
  2571 apply(drule_tac x="v2" in meta_spec)
 
  2051 apply(clarify)
 
  2572 apply(rotate_tac 8)
 
  2052 apply(erule ValOrd2.cases)
 
  2573 apply(drule_tac x="v2'" in meta_spec)
 
  2053 apply(simp_all)[8]
 
  2574 apply(rotate_tac 8)
 
  2054 apply(clarify)
 
  2575 apply(drule_tac x="s" in meta_spec)
 
  2055 apply(simp)
 
  2576 apply(simp)
 
  2056 
  2577 apply(drule_tac meta_mp)
 
  2057 apply(erule ValOrd2.cases)
 
  2578 apply(simp add: rest_def mkeps_flat)
 
  2058 apply(simp_all)[8]
 
  2579 apply(drule_tac meta_mp)
 
  2059 apply(simp)
 
  2580 apply(simp add: rest_def mkeps_flat)
 
  2060 apply metis
 
  2581 apply(simp)
 
  2061 using injval_inj
 
  2582 apply(simp add: rest_def mkeps_flat)
 
  2062 apply(simp add: inj_on_def)
 
  2583 apply(subst (asm) (5) v4)
 
  2063 apply metis
 
  2584 apply(simp)
 
  2064 (* SEQ nullable case *)
 
  2585 apply(subst (asm) (5) v4)
 
  2065 apply(erule Prf.cases)
 
  2586 apply(simp)
 
  2066 apply(simp_all)[5]
 
  2587 apply(subst (asm) (5) v4)
 
  2067 apply(clarify)
 
  2588 apply(simp)
 
  2068 apply(erule Prf.cases)
 
  2589 apply(simp)
 
  2069 apply(simp_all)[5]
 
  2590 apply(clarify)
 
  2070 apply(clarify)
 
  2591 apply(simp add: prefix_Cons)
 
  2071 apply(erule Prf.cases)
 
  2592 apply(subgoal_tac "((flat v1c) @ (flat v2b)) \<sqsubseteq> (flat v2)")
 
  2072 apply(simp_all)[5]
 
       
  2073 apply(clarify)
 
       
  2074 apply(erule Prf.cases)
 
       
  2075 apply(simp_all)[5]
 
       
  2076 apply(clarify)
 
       
  2077 apply(erule ValOrd.cases)
 
       
  2078 apply(simp_all)[8]
 
       
  2079 apply(clarify)
 
       
  2080 apply(erule ValOrd.cases)
 
       
  2081 apply(simp_all)[8]
 
       
  2082 apply(clarify)
 
       
  2083 apply(rule ValOrd.intros(1))
 
       
  2084 apply(simp)
 
       
  2085 apply(rule ValOrd.intros(2))
 
       
  2086 apply metis
 
       
  2087 using injval_inj
 
       
  2088 apply(simp add: inj_on_def)
 
       
  2089 apply metis
 
       
  2090 apply(clarify)
 
       
  2091 apply(simp)
 
       
  2092 apply(erule Prf.cases)
 
       
  2093 apply(simp_all)[5]
 
       
  2094 apply(clarify)
 
       
  2095 apply(erule ValOrd.cases)
 
       
  2096 apply(simp_all)[8]
 
       
  2097 apply(clarify)
 
       
  2098 apply(simp)
 
       
  2099 apply(rule ValOrd.intros(2))
 
       
  2100 apply (metis h)
 
       
  2101 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  2102 (* last case *)
 
       
  2103 apply(clarify)
 
       
  2104 apply(erule Prf.cases)
 
       
  2105 apply(simp_all)[5]
 
       
  2106 apply(clarify)
 
       
  2107 apply(rotate_tac 6)
 
       
  2108 apply(erule Prf.cases)
 
       
  2109 apply(simp_all)[5]
 
       
  2110 apply(clarify)
 
       
  2111 prefer 2
 
  2593 prefer 2
 
  2112 apply(clarify)
 
       
  2113 apply(erule ValOrd.cases)
 
       
  2114 apply(simp_all)[8]
 
       
  2115 apply(clarify)
 
       
  2116 apply(rule ValOrd.intros(1))
 
       
  2117 apply(metis)
 
       
  2118 apply(rule ValOrd.intros(2))
 
       
  2119 prefer 2
 
       
  2120 thm mkeps_flat v4
 
       
  2121 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  2122 oops
 
       
  2123 
       
  2124 
       
  2125 lemma Prf_inj_test:
 
       
  2126   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r"  
       
  2127           "flat v1 = flat v2"
 
       
  2128   shows "(injval r c v1) \<succ>r  (injval r c v2)"
 
       
  2129 using assms
 
       
  2130 apply(induct v1 arbitrary: r v2 taking: "length o flat" rule: measure_induct_rule)
 
       
  2131 apply(case_tac r)
 
       
  2132 (* NULL case *)
 
       
  2133 apply(simp)
 
       
  2134 apply(erule Prf.cases)
 
       
  2135 apply(simp_all)[5]
 
       
  2136 (* EMPTY case *)
 
       
  2137 apply(simp)
 
       
  2138 apply(erule Prf.cases)
 
       
  2139 apply(simp_all)[5]
 
       
  2140 (* CHAR case *)
 
       
  2141 apply(case_tac "c = char")
 
       
  2142 apply(simp)
 
       
  2143 apply(erule Prf.cases)
 
       
  2144 apply(simp_all)[5]
 
       
  2145 apply(erule Prf.cases)
 
       
  2146 apply(simp_all)[5]
 
       
  2147 apply (metis ValOrd.intros(8))
 
       
  2148 apply(simp)
 
       
  2149 apply(erule Prf.cases)
 
       
  2150 apply(simp_all)[5]
 
       
  2151 (* ALT case *)
 
       
  2152 prefer 2
 
       
  2153 apply(simp)
 
       
  2154 apply(erule Prf.cases)
 
       
  2155 apply(simp_all)[5]
 
       
  2156 apply(erule Prf.cases)
 
       
  2157 apply(simp_all)[5]
 
       
  2158 apply(clarify)
 
       
  2159 apply(erule ValOrd.cases)
 
       
  2160 apply(simp_all)[8]
 
       
  2161 apply(clarify)
 
       
  2162 apply (rule ValOrd.intros(6))
 
       
  2163 apply(drule_tac x="v1b" in meta_spec)
 
       
  2164 apply(drule_tac x="rexp1" in meta_spec)
 
       
  2165 apply(drule_tac x="v1'" in meta_spec)
 
       
  2166 apply(drule_tac meta_mp)
 
       
  2167 apply(assumption)
 
       
  2168 apply(drule_tac meta_mp)
 
       
  2169 apply(assumption)
 
       
  2170 apply(drule_tac meta_mp)
 
       
  2171 
       
  2172 apply(clarify)
 
       
  2173 apply(erule ValOrd.cases)
 
       
  2174 apply(simp_all)[8]
 
       
  2175 apply(clarify)
 
       
  2176 apply (metis ValOrd.intros(3) monoid_add_class.add.right_neutral order_refl v4)
 
       
  2177 apply(clarify)
 
       
  2178 apply(erule Prf.cases)
 
       
  2179 apply(simp_all)[5]
 
       
  2180 apply(clarify)
 
       
  2181 apply (metis RightLeft der.simps(4) injval.simps(2) injval.simps(3))
 
       
  2182 apply(clarify)
 
       
  2183 apply(erule ValOrd.cases)
 
       
  2184 apply(simp_all)[8]
 
       
  2185 apply(clarify)
 
       
  2186 apply (metis ValOrd.intros(5))
 
       
  2187 (* SEQ case *)
 
       
  2188 apply(simp)
 
       
  2189 apply(case_tac "nullable r1")
 
       
  2190 apply(simp)
 
       
  2191 defer
 
       
  2192 apply(simp)
 
       
  2193 apply(erule Prf.cases)
 
       
  2194 apply(simp_all)[5]
 
       
  2195 apply(erule Prf.cases)
 
       
  2196 apply(simp_all)[5]
 
       
  2197 apply(clarify)
 
       
  2198 apply(erule ValOrd.cases)
 
       
  2199 apply(simp_all)[8]
 
       
  2200 apply(clarify)
 
       
  2201 apply(rule ValOrd.intros)
 
       
  2202 apply(simp)
 
       
  2203 apply(clarify)
 
       
  2204 apply(rule ValOrd.intros(2))
 
       
  2205 apply(rotate_tac 2)
 
       
  2206 apply(drule_tac x="v1c" in meta_spec)
 
       
  2207 apply(rotate_tac 9)
 
       
  2208 apply(drule_tac x="v1'" in meta_spec)
 
       
  2209 apply(drule_tac meta_mp)
 
       
  2210 apply(assumption)
 
       
  2211 apply(drule_tac meta_mp)
 
       
  2212 apply(assumption)
 
       
  2213 apply(drule_tac meta_mp)
 
       
  2214 apply(assumption)
 
       
  2215 apply(drule_tac meta_mp)
 
       
  2216 apply(simp)
 
       
  2217 apply (metis POSIX_SEQ1)
 
       
  2218 apply(simp)
 
       
  2219 apply (metis proj_inj_id)
 
       
  2220 apply(erule Prf.cases)
 
       
  2221 apply(simp_all)[5]
 
       
  2222 apply(erule Prf.cases)
 
       
  2223 apply(simp_all)[5]
 
       
  2224 apply(clarify)
 
       
  2225 apply(rotate_tac 6)
 
       
  2226 apply(erule Prf.cases)
 
       
  2227 apply(simp_all)[5]
 
       
  2228 apply(erule Prf.cases)
 
       
  2229 apply(simp_all)[5]
 
       
  2230 apply(clarify)
 
       
  2231 apply(erule ValOrd.cases)
 
       
  2232 apply(simp_all)[8]
 
       
  2233 apply(clarify)
 
       
  2234 apply(erule ValOrd.cases)
 
       
  2235 apply(simp_all)[8]
 
       
  2236 apply(clarify)
 
       
  2237 apply(rule ValOrd.intros(1))
 
       
  2238 apply(simp)
 
       
  2239 apply(clarify)
 
       
  2240 apply (metis POSIX_ALT2 POSIX_SEQ1 ValOrd.intros(2) proj_inj_id)
 
       
  2241 apply(clarify)
 
       
  2242 apply(erule Prf.cases)
 
       
  2243 apply(simp_all)[5]
 
       
  2244 apply(clarify)
 
       
  2245 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))
 
       
  2246 apply(clarify)
 
       
  2247 apply(erule Prf.cases)
 
       
  2248 apply(simp_all)[5]
 
       
  2249 apply(clarify)
 
       
  2250 apply(rotate_tac 7)
 
       
  2251 apply(erule Prf.cases)
 
       
  2252 apply(simp_all)[5]
 
       
  2253 apply(clarify)
 
       
  2254 apply(erule ValOrd.cases)
 
       
  2255 apply(simp_all)[8]
 
       
  2256 apply(clarify)
 
       
  2257 apply(simp)
 
       
  2258 apply(drule POSIX_ALT1a)
 
       
  2259 apply(rule ValOrd.intros(2))
 
       
  2260 defer
 
       
  2261 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  2262 apply(rule ValOrd.intros(1))
 
       
  2263 apply(erule ValOrd.cases)
 
       
  2264 apply(simp_all)[8]
 
       
  2265 apply (metis POSIX_ALT1a)
 
       
  2266 
       
  2267 apply(clarify)
 
       
  2268 apply(erule ValOrd.cases)
 
       
  2269 apply(simp_all)[8]
 
       
  2270 apply(clarify)
 
       
  2271 apply(rule ValOrd.intros(1))
 
       
  2272 apply(simp)
 
       
  2273 
       
  2274 apply(subgoal_tac "flats v1c \<noteq> []")
 
       
  2275 
       
  2276 apply(simp)
 
       
  2277 apply(subst v4)
 
       
  2278 apply(simp)
 
       
  2279 apply(subst (asm) v4)
 
       
  2280 apply(simp)
 
       
  2281 apply(simp)
 
       
  2282 apply(simp add: prefix_def)
 
  2594 apply(simp add: prefix_def)
 
  2283 oops
 
  2595 apply(auto)[1]
 
  2284 
  2596 (* HEREHERE *)
 
  2285 lemma Prf_inj:
 
  2597 
  2286   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*)
 
  2598 apply(subst (asm) (7) v4)
 
  2287   shows "(injval r c v1) \<succ>r (injval r c v2)"
 
  2599 apply(simp)
 
  2288 using assms
 
  2600 
  2289 apply(induct c r arbitrary: v1 v2 rule: der.induct)
 
  2601 
  2290 (* NULL case *)
 
  2602 (* HEREHERE *)
 
  2291 apply(simp)
 
  2603 
  2292 apply(erule ValOrd.cases)
 
  2604 apply(simp add: Values_def)
 
  2293 apply(simp_all)[8]
 
  2605 apply(simp add: Values_recs)
 
  2294 (* EMPTY case *)
 
  2606 apply(simp add: Values_recs)
 
  2295 apply(simp)
 
  2607 done
 
  2296 apply(erule ValOrd.cases)
 
       
  2297 apply(simp_all)[8]
 
       
  2298 (* CHAR case *)
 
       
  2299 apply(case_tac "c = c'")
 
       
  2300 apply(simp)
 
       
  2301 apply(erule ValOrd.cases)
 
       
  2302 apply(simp_all)[8]
 
       
  2303 apply(rule ValOrd.intros)
 
       
  2304 apply(simp)
 
       
  2305 apply(erule ValOrd.cases)
 
       
  2306 apply(simp_all)[8]
 
       
  2307 (* ALT case *)
 
       
  2308 apply(simp)
 
       
  2309 apply(erule ValOrd.cases)
 
       
  2310 apply(simp_all)[8]
 
       
  2311 apply(rule ValOrd.intros)
 
       
  2312 apply(subst v4)
 
       
  2313 apply(clarify)
 
       
  2314 apply(rotate_tac 3)
 
       
  2315 apply(erule Prf.cases)
 
       
  2316 apply(simp_all)[5]
 
       
  2317 apply(subst v4)
 
       
  2318 apply(clarify)
 
       
  2319 apply(rotate_tac 2)
 
       
  2320 apply(erule Prf.cases)
 
       
  2321 apply(simp_all)[5]
 
       
  2322 apply(simp)
 
       
  2323 apply(rule ValOrd.intros)
 
       
  2324 apply(clarify)
 
       
  2325 apply(rotate_tac 3)
 
       
  2326 apply(erule Prf.cases)
 
       
  2327 apply(simp_all)[5]
 
       
  2328 apply(clarify)
 
       
  2329 apply(erule Prf.cases)
 
       
  2330 apply(simp_all)[5]
 
       
  2331 apply(clarify)
 
       
  2332 apply(subst v4)
 
       
  2333 apply(simp)
 
       
  2334 apply(subst v4)
 
       
  2335 apply(simp)
 
       
  2336 apply(simp)
 
       
  2337 apply(rule ValOrd.intros)
 
       
  2338 apply(clarify)
 
       
  2339 apply(erule Prf.cases)
 
       
  2340 apply(simp_all)[5]
 
       
  2341 apply(erule Prf.cases)
 
       
  2342 apply(simp_all)[5]
 
       
  2343 apply(rule ValOrd.intros)
 
       
  2344 apply(clarify)
 
       
  2345 apply(erule Prf.cases)
 
       
  2346 apply(simp_all)[5]
 
       
  2347 apply(erule Prf.cases)
 
       
  2348 apply(simp_all)[5]
 
       
  2349 (* SEQ case*)
 
       
  2350 apply(simp)
 
       
  2351 apply(case_tac "nullable r1")
 
       
  2352 apply(simp)
 
       
  2353 defer
 
       
  2354 apply(simp)
 
       
  2355 apply(erule Prf.cases)
 
       
  2356 apply(simp_all)[5]
 
       
  2357 apply(erule Prf.cases)
 
       
  2358 apply(simp_all)[5]
 
       
  2359 apply(clarify)
 
       
  2360 apply(erule ValOrd.cases)
 
       
  2361 apply(simp_all)[8]
 
       
  2362 apply(clarify)
 
       
  2363 apply(rule ValOrd.intros)
 
       
  2364 apply(simp)
 
       
  2365 apply(clarify)
 
       
  2366 apply(rule ValOrd.intros(2))
 
       
  2367 apply metis
 
       
  2368 using injval_inj
 
       
  2369 apply(simp add: inj_on_def)
 
       
  2370 apply metis
 
       
  2371 (* SEQ nullable case *)
 
       
  2372 apply(erule Prf.cases)
 
       
  2373 apply(simp_all)[5]
 
       
  2374 apply(clarify)
 
       
  2375 apply(erule Prf.cases)
 
       
  2376 apply(simp_all)[5]
 
       
  2377 apply(clarify)
 
       
  2378 apply(erule Prf.cases)
 
       
  2379 apply(simp_all)[5]
 
       
  2380 apply(clarify)
 
       
  2381 apply(erule Prf.cases)
 
       
  2382 apply(simp_all)[5]
 
       
  2383 apply(clarify)
 
       
  2384 apply(erule ValOrd.cases)
 
       
  2385 apply(simp_all)[8]
 
       
  2386 apply(clarify)
 
       
  2387 apply(erule ValOrd.cases)
 
       
  2388 apply(simp_all)[8]
 
       
  2389 apply(clarify)
 
       
  2390 apply(rule ValOrd.intros(1))
 
       
  2391 apply(simp)
 
       
  2392 apply(rule ValOrd.intros(2))
 
       
  2393 apply metis
 
       
  2394 using injval_inj
 
       
  2395 apply(simp add: inj_on_def)
 
       
  2396 apply metis
 
       
  2397 apply(clarify)
 
       
  2398 apply(simp)
 
       
  2399 apply(erule Prf.cases)
 
       
  2400 apply(simp_all)[5]
 
       
  2401 apply(clarify)
 
       
  2402 apply(erule ValOrd.cases)
 
       
  2403 apply(simp_all)[8]
 
       
  2404 apply(clarify)
 
       
  2405 apply(simp)
 
       
  2406 apply(rule ValOrd.intros(2))
 
       
  2407 apply (metis h)
 
       
  2408 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  2409 (* last case *)
 
       
  2410 apply(clarify)
 
       
  2411 apply(erule Prf.cases)
 
       
  2412 apply(simp_all)[5]
 
       
  2413 apply(clarify)
 
       
  2414 apply(rotate_tac 6)
 
       
  2415 apply(erule Prf.cases)
 
       
  2416 apply(simp_all)[5]
 
       
  2417 apply(clarify)
 
       
  2418 prefer 2
 
       
  2419 apply(clarify)
 
       
  2420 apply(erule ValOrd.cases)
 
       
  2421 apply(simp_all)[8]
 
       
  2422 apply(clarify)
 
       
  2423 apply(rule ValOrd.intros(1))
 
       
  2424 apply(metis)
 
       
  2425 apply(rule ValOrd.intros(2))
 
       
  2426 prefer 2
 
       
  2427 thm mkeps_flat v4
 
       
  2428 apply (metis list.distinct(1) mkeps_flat v4)
 
       
  2429 oops
 
       
  2430 
       
  2431 
  2608 
  2432 lemma POSIX_der:
 
  2609 lemma POSIX_der:
 
  2433   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
 
  2610   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
 
  2434   shows "POSIX (injval r c v) r"
 
  2611   shows "POSIX (injval r c v) r"
 
  2435 using assms
 
  2612 using assms
 
  2455 apply(subst v4_proj)
 
  2632 apply(subst v4_proj)
 
  2456 apply(simp)
 
  2633 apply(simp)
 
  2457 apply(rule_tac x="flat v" in exI)
 
  2634 apply(rule_tac x="flat v" in exI)
 
  2458 apply(simp)
 
  2635 apply(simp)
 
  2459 apply(simp)
 
  2636 apply(simp)
 
       
  2637 thm  Prf_inj_test
 
       
  2638 apply(drule_tac r="r" in Prf_inj_test)
 
  2460 oops
 
  2639 oops
 
  2461 
  2640 
  2462 lemma POSIX_der:
 
  2641 lemma POSIX_der:
 
  2463   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
 
  2642   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
 
  2464   shows "POSIX (injval r c v) r"
 
  2643   shows "POSIX (injval r c v) r"
lexing