1    

     2 theory Re1

     3   imports "Main" 

     4 begin

     5 

     6 

     7 section {* Sequential Composition of Sets *}

     8 

     9 definition

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

    11 where 

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

    13 

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

    15 

    16 lemma seq_empty [simp]:

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

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

    19 by (simp_all add: Sequ_def)

    20 

    21 lemma seq_null [simp]:

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

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

    24 by (simp_all add: Sequ_def)

    25 

    26 section {* Regular Expressions *}

    27 

    28 datatype rexp =

    29   NULL

    30 | EMPTY

    31 | CHAR char

    32 | SEQ rexp rexp

    33 | ALT rexp rexp

    34 

    35 fun SEQS :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp"

    36 where

    37   "SEQS r [] = r"

    38 | "SEQS r (r'#rs) = SEQ r (SEQS r' rs)"

    39 

    40 section {* Semantics of Regular Expressions *}

    41  

    42 fun

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

    44 where

    45   "L (NULL) = {}"

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

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

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

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

    50 

    51 fun zeroable where

    52   "zeroable NULL = True"

    53 | "zeroable EMPTY = False"

    54 | "zeroable (CHAR c) = False"

    55 | "zeroable (ALT r1 r2) = (zeroable r1 \<and> zeroable r2)"

    56 | "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)"

    57 

    58 lemma L_ALT_cases:

    59   "L (ALT r1 r2) \<noteq> {} \<Longrightarrow> (L r1 \<noteq> {}) \<or> (L r1 = {} \<and> L r2 \<noteq> {})"

    60 by(auto)

    61 

    62 fun

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

    64 where

    65   "nullable (NULL) = False"

    66 | "nullable (EMPTY) = True"

    67 | "nullable (CHAR c) = False"

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

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

    70 

    71 lemma nullable_correctness:

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

    73 apply (induct r) 

    74 apply(auto simp add: Sequ_def) 

    75 done

    76 

    77 section {* Values *}

    78 

    79 datatype val = 

    80   Void

    81 | Char char

    82 | Seq val val

    83 | Right val

    84 | Left val

    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 

    92 section {* The string behind a value *}

    93 

    94 fun flat :: "val \<Rightarrow> string"

    95 where

    96   "flat(Void) = []"

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

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

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

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

   101 

   102 fun flats :: "val \<Rightarrow> string list"

   103 where

   104   "flats(Void) = [[]]"

   105 | "flats(Char c) = [[c]]"

   106 | "flats(Left v) = flats(v)"

   107 | "flats(Right v) = flats(v)"

   108 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)"

   109 

   110 value "flats(Seq(Char c)(Char b))"

   111 

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

   113 

   114 

   115 inductive Prfs :: "string \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile>_ _ : _" [100, 100, 100] 100)

   116 where

   117  "\<lbrakk>\<Turnstile>s1 v1 : r1; \<Turnstile>s2 v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>(s1 @ s2) (Seq v1 v2) : SEQ r1 r2"

   118 | "\<Turnstile>s v1 : r1 \<Longrightarrow> \<Turnstile>s (Left v1) : ALT r1 r2"

   119 | "\<Turnstile>s v2 : r2 \<Longrightarrow> \<Turnstile>s (Right v2) : ALT r1 r2"

   120 | "\<Turnstile>[] Void : EMPTY"

   121 | "\<Turnstile>[c] (Char c) : CHAR c"

   122 

   123 lemma Prfs_flat:

   124   "\<Turnstile>s v : r \<Longrightarrow> flat v = s"

   125 apply(induct s v r rule: Prfs.induct)

   126 apply(auto)

   127 done

   128 

   129 inductive Prfn :: "nat \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> bool" ("\<TTurnstile>_ _ : _" [100, 100, 100] 100)

   130 where

   131  "\<lbrakk>\<TTurnstile>n1 v1 : r1; \<TTurnstile>n2 v2 : r2\<rbrakk> \<Longrightarrow> \<TTurnstile>(n1 + n2) (Seq v1 v2) : SEQ r1 r2"

   132 | "\<TTurnstile>n v1 : r1 \<Longrightarrow> \<TTurnstile>n (Left v1) : ALT r1 r2"

   133 | "\<TTurnstile>n v2 : r2 \<Longrightarrow> \<TTurnstile>n (Right v2) : ALT r1 r2"

   134 | "\<TTurnstile>0 Void : EMPTY"

   135 | "\<TTurnstile>1 (Char c) : CHAR c"

   136 

   137 lemma Prfn_flat:

   138   "\<TTurnstile>n v : r \<Longrightarrow> length (flat v) = n"

   139 apply(induct rule: Prfn.induct)

   140 apply(auto)

   141 done

   142 

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

   144 where

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

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

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

   148 | "\<turnstile> Void : EMPTY"

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

   150 

   151 lemma Prf_Prfn:

   152   shows "\<turnstile> v : r \<Longrightarrow> \<TTurnstile>(length (flat v)) v : r"

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

   154 apply(auto intro: Prfn.intros)

   155 by (metis One_nat_def Prfn.intros(5))

   156 

   157 lemma Prfn_Prf:

   158   shows "\<TTurnstile>n v : r \<Longrightarrow> \<turnstile> v : r"

   159 apply(induct n v r rule: Prfn.induct)

   160 apply(auto intro: Prf.intros)

   161 done

   162 

   163 lemma Prf_Prfs:

   164   shows "\<turnstile> v : r \<Longrightarrow> \<Turnstile>(flat v) v : r"

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

   166 apply(auto intro: Prfs.intros)

   167 done

   168 

   169 lemma Prfs_Prf:

   170   shows "\<Turnstile>s v : r \<Longrightarrow> \<turnstile> v : r"

   171 apply(induct s v r rule: Prfs.induct)

   172 apply(auto intro: Prf.intros)

   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 

   183 

   184 fun mkeps :: "rexp \<Rightarrow> val"

   185 where

   186   "mkeps(EMPTY) = Void"

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

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

   189 

   190 lemma mkeps_nullable:

   191   assumes "nullable(r)" shows "\<turnstile> mkeps r : r"

   192 using assms

   193 apply(induct rule: nullable.induct)

   194 apply(auto intro: Prf.intros)

   195 done

   196 

   197 lemma mkeps_nullable_n:

   198   assumes "nullable(r)" shows "\<TTurnstile>0 (mkeps r) : r"

   199 using assms

   200 apply(induct rule: nullable.induct)

   201 apply(auto intro: Prfn.intros)

   202 apply(drule Prfn.intros(1))

   203 apply(assumption)

   204 apply(simp)

   205 done

   206 

   207 lemma mkeps_nullable_s:

   208   assumes "nullable(r)" shows "\<Turnstile>[] (mkeps r) : r"

   209 using assms

   210 apply(induct rule: nullable.induct)

   211 apply(auto intro: Prfs.intros)

   212 apply(drule Prfs.intros(1))

   213 apply(assumption)

   214 apply(simp)

   215 done

   216 

   217 lemma mkeps_flat:

   218   assumes "nullable(r)" shows "flat (mkeps r) = []"

   219 using assms

   220 apply(induct rule: nullable.induct)

   221 apply(auto)

   222 done

   223 

   224 text {*

   225   The value mkeps returns is always the correct POSIX

   226   value.

   227 *}

   228 

   229 lemma Prf_flat_L:

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

   231 using assms

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

   233 apply(auto simp add: Sequ_def)

   234 done

   235 

   236 lemma L_flat_Prf:

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

   238 apply(induct r)

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

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

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

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

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

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

   245 apply(erule Prf.cases)

   246 apply(auto)

   247 done

   248 

   249 

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

   251 where

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

   253 

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

   255 where

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

   257 

   258 lemma length_sprefix:

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

   260 unfolding sprefix_def prefix_def

   261 by (auto)

   262 

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

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

   265 

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

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

   268 

   269 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 *}

   536 

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

   538 where

   539   "v2 \<succ>r2 v2' \<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')" 

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

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

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

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

   545 | "Void \<succ>EMPTY Void"

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

   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 

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

   559 where

   560   "v2 2\<succ> v2' \<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')" 

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

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

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

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

   566 | "Void 2\<succ> Void"

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

   568 

   569 lemma Ord1:

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

   571 apply(induct rule: ValOrd.induct)

   572 apply(auto intro: ValOrd2.intros)

   573 done

   574 

   575 lemma Ord2:

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

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

   578 apply(auto intro: ValOrd.intros)

   579 done

   580 

   581 lemma Ord3:

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

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

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

   585 done

   586 

   587 

   588 lemma ValOrd_refl:

   589   assumes "\<turnstile> v : r"

   590   shows "v \<succ>r v"

   591 using assms

   592 apply(induct)

   593 apply(auto intro: ValOrd.intros)

   594 done

   595 

   596 lemma 

   597   "flat Void = []"

   598   "flat (Seq Void Void) = []"

   599 apply(simp_all)

   600 done

   601 

   602 

   603 lemma ValOrd_total:

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

   605 apply(induct r arbitrary: v1 v2)

   606 apply(auto)

   607 apply(erule Prf.cases)

   608 apply(simp_all)[5]

   609 apply(erule Prf.cases)

   610 apply(simp_all)[5]

   611 apply(erule Prf.cases)

   612 apply(simp_all)[5]

   613 apply (metis ValOrd.intros(7))

   614 apply(erule Prf.cases)

   615 apply(simp_all)[5]

   616 apply(erule Prf.cases)

   617 apply(simp_all)[5]

   618 apply (metis ValOrd.intros(8))

   619 apply(erule Prf.cases)

   620 apply(simp_all)[5]

   621 apply(erule Prf.cases)

   622 apply(simp_all)[5]

   623 apply(clarify)

   624 apply(case_tac "v1a = v1b")

   625 apply(simp)

   626 apply(rule ValOrd.intros(1))

   627 apply (metis ValOrd.intros(1))

   628 apply(rule ValOrd.intros(2))

   629 apply(auto)[2]

   630 apply(erule contrapos_np)

   631 apply(rule ValOrd.intros(2))

   632 apply(auto)

   633 apply(erule Prf.cases)

   634 apply(simp_all)[5]

   635 apply(erule Prf.cases)

   636 apply(simp_all)[5]

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

   638 apply(rule ValOrd.intros)

   639 apply(erule contrapos_np)

   640 apply(rule ValOrd.intros)

   641 apply (metis le_eq_less_or_eq neq_iff)

   642 apply(erule Prf.cases)

   643 apply(simp_all)[5]

   644 apply(rule ValOrd.intros)

   645 apply(erule contrapos_np)

   646 apply(rule ValOrd.intros)

   647 apply (metis le_eq_less_or_eq neq_iff)

   648 apply(rule ValOrd.intros)

   649 apply(erule contrapos_np)

   650 apply(rule ValOrd.intros)

   651 by metis

   652 

   653 lemma ValOrd_anti:

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

   655 apply(induct r arbitrary: v1 v2)

   656 apply(erule Prf.cases)

   657 apply(simp_all)[5]

   658 apply(erule Prf.cases)

   659 apply(simp_all)[5]

   660 apply(erule Prf.cases)

   661 apply(simp_all)[5]

   662 apply(erule Prf.cases)

   663 apply(simp_all)[5]

   664 apply(erule Prf.cases)

   665 apply(simp_all)[5]

   666 apply(erule Prf.cases)

   667 apply(simp_all)[5]

   668 apply(erule Prf.cases)

   669 apply(simp_all)[5]

   670 apply(erule ValOrd.cases)

   671 apply(simp_all)[8]

   672 apply(erule ValOrd.cases)

   673 apply(simp_all)[8]

   674 apply(erule ValOrd.cases)

   675 apply(simp_all)[8]

   676 apply(erule Prf.cases)

   677 apply(simp_all)[5]

   678 apply(erule Prf.cases)

   679 apply(simp_all)[5]

   680 apply(erule ValOrd.cases)

   681 apply(simp_all)[8]

   682 apply(erule ValOrd.cases)

   683 apply(simp_all)[8]

   684 apply(erule ValOrd.cases)

   685 apply(simp_all)[8]

   686 apply(erule ValOrd.cases)

   687 apply(simp_all)[8]

   688 apply(erule Prf.cases)

   689 apply(simp_all)[5]

   690 apply(erule ValOrd.cases)

   691 apply(simp_all)[8]

   692 apply(erule ValOrd.cases)

   693 apply(simp_all)[8]

   694 apply(erule ValOrd.cases)

   695 apply(simp_all)[8]

   696 apply(erule ValOrd.cases)

   697 apply(simp_all)[8]

   698 done

   699 

   700 lemma refl_on_ValOrd:

   701   "refl_on (Values r s) {(v1, v2). v1 \<succ>r v2 \<and> v1 \<in> Values r s \<and> v2 \<in> Values r s}"

   702 unfolding refl_on_def

   703 apply(auto)

   704 apply(rule ValOrd_refl)

   705 apply(simp add: Values_def)

   706 done

   707 

   708 (*

   709 inductive ValOrd3 :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ 3\<succ>_ _" [100, 100, 100] 100)

   710 where

   711   "\<lbrakk>v2 3\<succ>r2 v2'; \<turnstile> v1 : r1\<rbrakk> \<Longrightarrow> (Seq v1 v2) 3\<succ>(SEQ r1 r2) (Seq v1 v2')" 

   712 | "\<lbrakk>v1 3\<succ>r1 v1'; v1 \<noteq> v1'; flat v2 = flat v2'; \<turnstile> v2 : r2; \<turnstile> v2' : r2\<rbrakk> 

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

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

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

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

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

   718 | "Void 3\<succ>EMPTY Void"

   719 | "(Char c) 3\<succ>(CHAR c) (Char c)"

   720 *)

   721 

   722 section {* Posix definition *}

   723 

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

   725 where

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

   727 

   728 definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 

   729 where

   730   "POSIX2 v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v 2\<succ> v'))"

   731 

   732 lemma "POSIX v r = POSIX2 v r"

   733 unfolding POSIX_def POSIX2_def

   734 apply(auto)

   735 apply(rule Ord1)

   736 apply(auto)

   737 apply(rule Ord3)

   738 apply(auto)

   739 done

   740 

   741 definition POSIXs :: "val \<Rightarrow> rexp \<Rightarrow> string \<Rightarrow> bool" 

   742 where

   743   "POSIXs v r s \<equiv> (\<Turnstile>s v : r \<and> (\<forall>v'. (\<Turnstile>s v' : r \<longrightarrow> v 2\<succ> v')))"

   744 

   745 definition POSIXn :: "val \<Rightarrow> rexp \<Rightarrow> nat \<Rightarrow> bool" 

   746 where

   747   "POSIXn v r n \<equiv> (\<TTurnstile>n v : r \<and> (\<forall>v'. (\<TTurnstile>n v' : r \<longrightarrow> v 2\<succ> v')))"

   748 

   749 lemma "POSIXn v r (length (flat v)) \<Longrightarrow> POSIX2 v r"

   750 unfolding POSIXn_def POSIX2_def

   751 apply(auto)

   752 apply (metis Prfn_Prf)

   753 by (metis Prf_Prfn)

   754 

   755 lemma Prfs_POSIX:

   756   "POSIXs v r s \<Longrightarrow> \<Turnstile>s v: r \<and> flat v = s"

   757 apply(simp add: POSIXs_def)

   758 by (metis Prfs_flat)

   759 

   760 

   761 lemma "POSIXs v r (flat v) =  POSIX2 v r"

   762 unfolding POSIXs_def POSIX2_def

   763 apply(auto)

   764 apply (metis Prfs_Prf)

   765 apply (metis Prf_Prfs)

   766 apply (metis Prf_Prfs)

   767 by (metis Prfs_Prf Prfs_flat)

   768 

   769 section {* POSIX for some constructors *}

   770 

   771 lemma POSIX_SEQ1:

   772   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"

   773   shows "POSIX v1 r1"

   774 using assms

   775 unfolding POSIX_def

   776 apply(auto)

   777 apply(drule_tac x="Seq v' v2" in spec)

   778 apply(simp)

   779 apply(erule impE)

   780 apply(rule Prf.intros)

   781 apply(simp)

   782 apply(simp)

   783 apply(erule ValOrd.cases)

   784 apply(simp_all)

   785 apply(clarify)

   786 by (metis ValOrd_refl)

   787 

   788 lemma POSIXn_SEQ1:

   789   assumes "POSIXn (Seq v1 v2) (SEQ r1 r2) (n1 + n2)" "\<TTurnstile>n1 v1 : r1" "\<TTurnstile>n2 v2 : r2"

   790   shows "POSIXn v1 r1 n1"

   791 using assms

   792 unfolding POSIXn_def

   793 apply(auto)

   794 apply(drule_tac x="Seq v' v2" in spec)

   795 apply(erule impE)

   796 apply(rule Prfn.intros)

   797 apply(simp)

   798 apply(simp)

   799 apply(erule ValOrd2.cases)

   800 apply(simp_all)

   801 apply(clarify)

   802 by (metis Ord1 Prfn_Prf ValOrd_refl)

   803 

   804 lemma POSIXs_SEQ1:

   805   assumes "POSIXs (Seq v1 v2) (SEQ r1 r2) (s1 @ s2)" "\<Turnstile>s1 v1 : r1" "\<Turnstile>s2 v2 : r2"

   806   shows "POSIXs v1 r1 s1"

   807 using assms

   808 unfolding POSIXs_def

   809 apply(auto)

   810 apply(drule_tac x="Seq v' v2" in spec)

   811 apply(erule impE)

   812 apply(rule Prfs.intros)

   813 apply(simp)

   814 apply(simp)

   815 apply(erule ValOrd2.cases)

   816 apply(simp_all)

   817 apply(clarify)

   818 by (metis Ord1 Prfs_Prf ValOrd_refl)

   819 

   820 lemma POSIX_SEQ2:

   821   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" 

   822   shows "POSIX v2 r2"

   823 using assms

   824 unfolding POSIX_def

   825 apply(auto)

   826 apply(drule_tac x="Seq v1 v'" in spec)

   827 apply(simp)

   828 apply(erule impE)

   829 apply(rule Prf.intros)

   830 apply(simp)

   831 apply(simp)

   832 apply(erule ValOrd.cases)

   833 apply(simp_all)

   834 done

   835 

   836 lemma POSIXn_SEQ2:

   837   assumes "POSIXn (Seq v1 v2) (SEQ r1 r2) (n1 + n2)" "\<TTurnstile>n1 v1 : r1" "\<TTurnstile>n2 v2 : r2" 

   838   shows "POSIXn v2 r2 n2"

   839 using assms

   840 unfolding POSIXn_def

   841 apply(auto)

   842 apply(drule_tac x="Seq v1 v'" in spec)

   843 apply(erule impE)

   844 apply(rule Prfn.intros)

   845 apply(simp)

   846 apply(simp)

   847 apply(erule ValOrd2.cases)

   848 apply(simp_all)

   849 done

   850 

   851 lemma POSIXs_SEQ2:

   852   assumes "POSIXs (Seq v1 v2) (SEQ r1 r2) (s1 @ s2)" "\<Turnstile>s1 v1 : r1" "\<Turnstile>s2 v2 : r2" 

   853   shows "POSIXs v2 r2 s2"

   854 using assms

   855 unfolding POSIXs_def

   856 apply(auto)

   857 apply(drule_tac x="Seq v1 v'" in spec)

   858 apply(erule impE)

   859 apply(rule Prfs.intros)

   860 apply(simp)

   861 apply(simp)

   862 apply(erule ValOrd2.cases)

   863 apply(simp_all)

   864 done

   865 

   866 lemma POSIX_ALT2:

   867   assumes "POSIX (Left v1) (ALT r1 r2)"

   868   shows "POSIX v1 r1"

   869 using assms

   870 unfolding POSIX_def

   871 apply(auto)

   872 apply(erule Prf.cases)

   873 apply(simp_all)[5]

   874 apply(drule_tac x="Left v'" in spec)

   875 apply(simp)

   876 apply(drule mp)

   877 apply(rule Prf.intros)

   878 apply(auto)

   879 apply(erule ValOrd.cases)

   880 apply(simp_all)

   881 done

   882 

   883 lemma POSIXn_ALT2:

   884   assumes "POSIXn (Left v1) (ALT r1 r2) n"

   885   shows "POSIXn v1 r1 n"

   886 using assms

   887 unfolding POSIXn_def

   888 apply(auto)

   889 apply(erule Prfn.cases)

   890 apply(simp_all)[5]

   891 apply(drule_tac x="Left v'" in spec)

   892 apply(drule mp)

   893 apply(rule Prfn.intros)

   894 apply(auto)

   895 apply(erule ValOrd2.cases)

   896 apply(simp_all)

   897 done

   898 

   899 lemma POSIXs_ALT2:

   900   assumes "POSIXs (Left v1) (ALT r1 r2) s"

   901   shows "POSIXs v1 r1 s"

   902 using assms

   903 unfolding POSIXs_def

   904 apply(auto)

   905 apply(erule Prfs.cases)

   906 apply(simp_all)[5]

   907 apply(drule_tac x="Left v'" in spec)

   908 apply(drule mp)

   909 apply(rule Prfs.intros)

   910 apply(auto)

   911 apply(erule ValOrd2.cases)

   912 apply(simp_all)

   913 done

   914 

   915 lemma POSIX_ALT1a:

   916   assumes "POSIX (Right v2) (ALT r1 r2)"

   917   shows "POSIX v2 r2"

   918 using assms

   919 unfolding POSIX_def

   920 apply(auto)

   921 apply(erule Prf.cases)

   922 apply(simp_all)[5]

   923 apply(drule_tac x="Right v'" in spec)

   924 apply(simp)

   925 apply(drule mp)

   926 apply(rule Prf.intros)

   927 apply(auto)

   928 apply(erule ValOrd.cases)

   929 apply(simp_all)

   930 done

   931 

   932 lemma POSIXn_ALT1a:

   933   assumes "POSIXn (Right v2) (ALT r1 r2) n"

   934   shows "POSIXn v2 r2 n"

   935 using assms

   936 unfolding POSIXn_def

   937 apply(auto)

   938 apply(erule Prfn.cases)

   939 apply(simp_all)[5]

   940 apply(drule_tac x="Right v'" in spec)

   941 apply(drule mp)

   942 apply(rule Prfn.intros)

   943 apply(auto)

   944 apply(erule ValOrd2.cases)

   945 apply(simp_all)

   946 done

   947 

   948 lemma POSIXs_ALT1a:

   949   assumes "POSIXs (Right v2) (ALT r1 r2) s"

   950   shows "POSIXs v2 r2 s"

   951 using assms

   952 unfolding POSIXs_def

   953 apply(auto)

   954 apply(erule Prfs.cases)

   955 apply(simp_all)[5]

   956 apply(drule_tac x="Right v'" in spec)

   957 apply(drule mp)

   958 apply(rule Prfs.intros)

   959 apply(auto)

   960 apply(erule ValOrd2.cases)

   961 apply(simp_all)

   962 done

   963 

   964 lemma POSIX_ALT1b:

   965   assumes "POSIX (Right v2) (ALT r1 r2)"

   966   shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')"

   967 using assms

   968 apply(drule_tac POSIX_ALT1a)

   969 unfolding POSIX_def

   970 apply(auto)

   971 done

   972 

   973 lemma POSIXn_ALT1b:

   974   assumes "POSIXn (Right v2) (ALT r1 r2) n"

   975   shows "(\<forall>v'. (\<TTurnstile>n v' : r2 \<longrightarrow> v2 2\<succ> v'))"

   976 using assms

   977 apply(drule_tac POSIXn_ALT1a)

   978 unfolding POSIXn_def

   979 apply(auto)

   980 done

   981 

   982 lemma POSIXs_ALT1b:

   983   assumes "POSIXs (Right v2) (ALT r1 r2) s"

   984   shows "(\<forall>v'. (\<Turnstile>s v' : r2 \<longrightarrow> v2 2\<succ> v'))"

   985 using assms

   986 apply(drule_tac POSIXs_ALT1a)

   987 unfolding POSIXs_def

   988 apply(auto)

   989 done

   990 

   991 lemma POSIX_ALT_I1:

   992   assumes "POSIX v1 r1" 

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

   994 using assms

   995 unfolding POSIX_def

   996 apply(auto)

   997 apply (metis Prf.intros(2))

   998 apply(rotate_tac 2)

   999 apply(erule Prf.cases)

  1000 apply(simp_all)[5]

  1001 apply(auto)

  1002 apply(rule ValOrd.intros)

  1003 apply(auto)

  1004 apply(rule ValOrd.intros)

  1005 by simp

  1006 

  1007 lemma POSIXn_ALT_I1:

  1008   assumes "POSIXn v1 r1 n" 

  1009   shows "POSIXn (Left v1) (ALT r1 r2) n"

  1010 using assms

  1011 unfolding POSIXn_def

  1012 apply(auto)

  1013 apply (metis Prfn.intros(2))

  1014 apply(rotate_tac 2)

  1015 apply(erule Prfn.cases)

  1016 apply(simp_all)[5]

  1017 apply(auto)

  1018 apply(rule ValOrd2.intros)

  1019 apply(auto)

  1020 apply(rule ValOrd2.intros)

  1021 by (metis Prfn_flat order_refl)

  1022 

  1023 lemma POSIXs_ALT_I1:

  1024   assumes "POSIXs v1 r1 s" 

  1025   shows "POSIXs (Left v1) (ALT r1 r2) s"

  1026 using assms

  1027 unfolding POSIXs_def

  1028 apply(auto)

  1029 apply (metis Prfs.intros(2))

  1030 apply(rotate_tac 2)

  1031 apply(erule Prfs.cases)

  1032 apply(simp_all)[5]

  1033 apply(auto)

  1034 apply(rule ValOrd2.intros)

  1035 apply(auto)

  1036 apply(rule ValOrd2.intros)

  1037 by (metis Prfs_flat order_refl)

  1038 

  1039 lemma POSIX_ALT_I2:

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

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

  1042 using assms

  1043 unfolding POSIX_def

  1044 apply(auto)

  1045 apply (metis Prf.intros)

  1046 apply(rotate_tac 3)

  1047 apply(erule Prf.cases)

  1048 apply(simp_all)[5]

  1049 apply(auto)

  1050 apply(rule ValOrd.intros)

  1051 apply metis

  1052 done

  1053 

  1054 lemma POSIXs_ALT_I2:

  1055   assumes "POSIXs v2 r2 s" "\<forall>s' v'. \<Turnstile>s' v' : r1 \<longrightarrow> length s > length s'"

  1056   shows "POSIXs (Right v2) (ALT r1 r2) s"

  1057 using assms

  1058 unfolding POSIXs_def

  1059 apply(auto)

  1060 apply (metis Prfs.intros)

  1061 apply(rotate_tac 3)

  1062 apply(erule Prfs.cases)

  1063 apply(simp_all)[5]

  1064 apply(auto)

  1065 apply(rule ValOrd2.intros)

  1066 apply metis

  1067 done

  1068 

  1069 lemma 

  1070   "\<lbrakk>POSIX (mkeps r2) r2; nullable r2; \<not> nullable r1\<rbrakk>

  1071    \<Longrightarrow> POSIX (Right (mkeps r2)) (ALT r1 r2)" 

  1072 apply(auto simp add: POSIX_def)

  1073 apply(rule Prf.intros(3))

  1074 apply(auto)

  1075 apply(rotate_tac 3)

  1076 apply(erule Prf.cases)

  1077 apply(simp_all)[5]

  1078 apply(simp add: mkeps_flat)

  1079 apply(auto)[1]

  1080 apply (metis Prf_flat_L nullable_correctness)

  1081 apply(rule ValOrd.intros)

  1082 apply(auto)

  1083 done

  1084 

  1085 lemma mkeps_POSIX:

  1086   assumes "nullable r"

  1087   shows "POSIX (mkeps r) r"

  1088 using assms

  1089 apply(induct r)

  1090 apply(auto)[1]

  1091 apply(simp add: POSIX_def)

  1092 apply(auto)[1]

  1093 apply (metis Prf.intros(4))

  1094 apply(erule Prf.cases)

  1095 apply(simp_all)[5]

  1096 apply (metis ValOrd.intros)

  1097 apply(simp)

  1098 apply(auto)[1]

  1099 apply(simp add: POSIX_def)

  1100 apply(auto)[1]

  1101 apply (metis mkeps.simps(2) mkeps_nullable nullable.simps(5))

  1102 apply(rotate_tac 6)

  1103 apply(erule Prf.cases)

  1104 apply(simp_all)[5]

  1105 apply (simp add: mkeps_flat)

  1106 apply(case_tac "mkeps r1a = v1")

  1107 apply(simp)

  1108 apply (metis ValOrd.intros(1))

  1109 apply (rule ValOrd.intros(2))

  1110 apply metis

  1111 apply(simp)

  1112 (* ALT case *)

  1113 thm mkeps.simps

  1114 apply(simp)

  1115 apply(erule disjE)

  1116 apply(simp)

  1117 apply (metis POSIX_ALT_I1)

  1118 (* *)

  1119 apply(auto)[1]

  1120 thm  POSIX_ALT_I1

  1121 apply (metis POSIX_ALT_I1)

  1122 apply(simp (no_asm) add: POSIX_def)

  1123 apply(auto)[1]

  1124 apply(rule Prf.intros(3))

  1125 apply(simp only: POSIX_def)

  1126 apply(rotate_tac 4)

  1127 apply(erule Prf.cases)

  1128 apply(simp_all)[5]

  1129 thm mkeps_flat

  1130 apply(simp add: mkeps_flat)

  1131 apply(auto)[1]

  1132 thm Prf_flat_L nullable_correctness

  1133 apply (metis Prf_flat_L nullable_correctness)

  1134 apply(rule ValOrd.intros)

  1135 apply(subst (asm) POSIX_def)