1    

     2 theory Re

     3   imports "Main" 

     4 begin

     5 

     6 

     7 section {* Sequential Composition of Sets *}

     8 

     9 definition

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

    11 where 

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

    13 

    14 fun spow where

    15   "spow s 0 = []"

    16 | "spow s (Suc n) = s @ spow s n"

    17 

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

    19 

    20 lemma seq_empty [simp]:

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

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

    23 by (simp_all add: Sequ_def)

    24 

    25 lemma seq_null [simp]:

    26   shows "A ;; {} = {}"

    27   and   "{} ;; A = {}"

    28 by (simp_all add: Sequ_def)

    29 

    30 lemma seq_image:

    31   assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"

    32   shows "f ` (A ;; B) = (f ` A) ;; (f ` B)"

    33 apply(auto simp add: Sequ_def image_def)

    34 apply(rule_tac x="f s1" in exI)

    35 apply(rule_tac x="f s2" in exI)

    36 using assms

    37 apply(auto)

    38 apply(rule_tac x="xa @ xb" in exI)

    39 using assms

    40 apply(auto)

    41 done

    42 

    43 section {* Kleene Star for Sets *}

    44 

    45 inductive_set

    46   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)

    47   for A :: "string set"

    48 where

    49   start[intro]: "[] \<in> A\<star>"

    50 | step[intro]:  "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"

    51 

    52 fun 

    53   pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [100,100] 100)

    54 where

    55   "A \<up> 0 = {[]}"

    56 | "A \<up> (Suc n) = A ;; (A \<up> n)"  

    57 

    58 lemma star1: 

    59   shows "s \<in> A\<star> \<Longrightarrow> \<exists>n. s \<in> A \<up> n"

    60   apply(induct rule: Star.induct)

    61   apply (metis Re.pow.simps(1) insertI1)

    62   apply(auto)

    63   apply(rule_tac x="Suc n" in exI)

    64   apply(auto simp add: Sequ_def)

    65   done

    66 

    67 lemma star2:

    68   shows "s \<in> A \<up> n \<Longrightarrow> s \<in> A\<star>"

    69   apply(induct n arbitrary: s)

    70   apply (metis Re.pow.simps(1) Star.simps empty_iff insertE)

    71   apply(auto simp add: Sequ_def)

    72   done

    73 

    74 lemma star3:

    75   shows "A\<star> = (\<Union>i. A \<up> i)"

    76 using star1 star2

    77 apply(auto)

    78 done

    79 

    80 lemma star4:

    81   shows "s \<in> A \<up> n \<Longrightarrow> \<exists>ss. s = concat ss \<and> (\<forall>s' \<in> set ss. s' \<in> A)"

    82   apply(induct n arbitrary: s)

    83   apply(auto simp add: Sequ_def)

    84   apply(rule_tac x="[]" in exI)

    85   apply(auto)

    86   apply(drule_tac x="s2" in meta_spec)

    87   apply(auto)

    88 by (metis concat.simps(2) insertE set_simps(2))

    89 

    90 lemma star5:

    91   assumes "f [] = []"

    92   assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"

    93   shows "(f ` A) \<up> n = f ` (A \<up> n)"

    94 apply(induct n)

    95 apply(simp add: assms)

    96 apply(simp)

    97 apply(subst seq_image[OF assms(2)])

    98 apply(simp)

    99 done

   100 

   101 lemma star6:

   102   assumes "f [] = []"

   103   assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"

   104   shows "(f ` A)\<star> = f ` (A\<star>)"

   105 apply(simp add: star3)

   106 apply(simp add: image_UN)

   107 apply(subst star5[OF assms])

   108 apply(simp)

   109 done

   110 

   111 

   112 lemma star_decomp: 

   113   assumes a: "c # x \<in> A\<star>" 

   114   shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"

   115 using a

   116 by (induct x\<equiv>"c # x" rule: Star.induct) 

   117    (auto simp add: append_eq_Cons_conv)

   118 

   119 section {* Regular Expressions *}

   120 

   121 datatype rexp =

   122   NULL

   123 | EMPTY

   124 | CHAR char

   125 | SEQ rexp rexp

   126 | ALT rexp rexp

   127 | STAR rexp

   128 

   129 section {* Semantics of Regular Expressions *}

   130  

   131 fun

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

   133 where

   134   "L (NULL) = {}"

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

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

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

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

   139 | "L (STAR r) = (L r)\<star>"

   140 

   141 fun

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

   143 where

   144   "nullable (NULL) = False"

   145 | "nullable (EMPTY) = True"

   146 | "nullable (CHAR c) = False"

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

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

   149 | "nullable (STAR r1) = True"

   150 

   151 lemma nullable_correctness:

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

   153 apply (induct r) 

   154 apply(auto simp add: Sequ_def) 

   155 done

   156 

   157 section {* Values *}

   158 

   159 datatype val = 

   160   Void

   161 | Char char

   162 | Seq val val

   163 | Right val

   164 | Left val

   165 | Star "val list"

   166 

   167 section {* The string behind a value *}

   168 

   169 fun 

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

   171 where

   172   "flat (Void) = []"

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

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

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

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

   177 | "flat (Star []) = []"

   178 | "flat (Star (v#vs)) = (flat v) @ (flat (Star vs))" 

   179 

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

   181 

   182 inductive 

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

   184 where

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

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

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

   188 | "\<turnstile> Void : EMPTY"

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

   190 | "\<turnstile> Star [] : STAR r"

   191 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Star vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Star (v#vs) : STAR r"

   192 

   193 lemma not_nullable_flat:

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

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

   196 using assms

   197 apply(induct)

   198 apply(auto)

   199 done

   200 

   201 lemma Prf_flat_L:

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

   203 using assms

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

   205 apply(auto simp add: Sequ_def)

   206 done

   207 

   208 

   209 lemma Prf_Star_flat_L:

   210   assumes "\<turnstile> v : STAR r" shows "flat v \<in> (L r)\<star>"

   211 using assms

   212 apply(induct v r\<equiv>"STAR r" arbitrary: r rule: Prf.induct)

   213 apply(auto)

   214 apply(simp add: star3)

   215 apply(auto)

   216 apply(rule_tac x="Suc x" in exI)

   217 apply(auto simp add: Sequ_def)

   218 apply(rule_tac x="flat v" in exI)

   219 apply(rule_tac x="flat (Star vs)" in exI)

   220 apply(auto)

   221 by (metis Prf_flat_L)

   222 

   223 lemma L_flat_Prf:

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

   225 apply(induct r)

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

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

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

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

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

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

   232 apply(erule Prf.cases)

   233 apply(auto)

   234 apply(simp add: star3)

   235 apply(auto)

   236 sorry

   237 

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

   239 

   240 inductive 

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

   242 where 

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

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

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

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

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

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

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

   250 

   251 lemma Gr_refl:

   252   assumes "\<turnstile> v : r"

   253   shows "v gr\<succ> v"

   254 using assms

   255 apply(induct)

   256 apply(auto intro: GrOrd.intros)

   257 done

   258 

   259 lemma Gr_total:

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

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

   262 using assms

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

   264 apply(rotate_tac 4)

   265 apply(erule Prf.cases)

   266 apply(simp_all)[5]

   267 apply(clarify)

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

   269 apply(rotate_tac 2)

   270 apply(erule Prf.cases)

   271 apply(simp_all)

   272 apply(clarify)

   273 apply (metis GrOrd.intros(3))

   274 apply(clarify)

   275 apply (metis GrOrd.intros(5))

   276 apply(rotate_tac 2)

   277 apply(erule Prf.cases)

   278 apply(simp_all)

   279 apply(clarify)

   280 apply (metis GrOrd.intros(5))

   281 apply(clarify)

   282 apply (metis GrOrd.intros(4))

   283 apply(erule Prf.cases)

   284 apply(simp_all)

   285 apply (metis GrOrd.intros(7))

   286 apply(erule Prf.cases)

   287 apply(simp_all)

   288 apply (metis GrOrd.intros(6))

   289 done

   290 

   291 lemma Gr_trans: 

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

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

   294   shows "v1 gr\<succ> v3"

   295 using assms

   296 apply(induct r arbitrary: v1 v2 v3)

   297 apply(erule Prf.cases)

   298 apply(simp_all)[5]

   299 apply(erule Prf.cases)

   300 apply(simp_all)[5]

   301 apply(erule Prf.cases)

   302 apply(simp_all)[5]

   303 apply(erule Prf.cases)

   304 apply(simp_all)[5]

   305 apply(erule Prf.cases)

   306 apply(simp_all)[5]

   307 defer

   308 (* ALT case *)

   309 apply(erule Prf.cases)

   310 apply(simp_all (no_asm_use))[5]

   311 apply(erule Prf.cases)

   312 apply(simp_all (no_asm_use))[5]

   313 apply(erule Prf.cases)

   314 apply(simp_all (no_asm_use))[5]

   315 apply(clarify)

   316 apply(erule GrOrd.cases)

   317 apply(simp_all (no_asm_use))[7]

   318 apply(erule GrOrd.cases)

   319 apply(simp_all (no_asm_use))[7]

   320 apply (metis GrOrd.intros(3))

   321 apply(clarify)

   322 apply(erule GrOrd.cases)

   323 apply(simp_all (no_asm_use))[7]

   324 apply(erule GrOrd.cases)

   325 apply(simp_all (no_asm_use))[7]

   326 apply (metis GrOrd.intros(5))

   327 apply(erule Prf.cases)

   328 apply(simp_all (no_asm_use))[5]

   329 apply(clarify)

   330 apply(erule GrOrd.cases)

   331 apply(simp_all (no_asm_use))[7]

   332 apply(erule GrOrd.cases)

   333 apply(simp_all (no_asm_use))[7]

   334 apply (metis GrOrd.intros(5))

   335 apply(erule Prf.cases)

   336 apply(simp_all (no_asm_use))[5]

   337 apply(erule Prf.cases)

   338 apply(simp_all (no_asm_use))[5]

   339 apply(clarify)

   340 apply(erule GrOrd.cases)

   341 apply(simp_all (no_asm_use))[7]

   342 apply(clarify)

   343 apply(erule GrOrd.cases)

   344 apply(simp_all (no_asm_use))[7]

   345 apply(erule Prf.cases)

   346 apply(simp_all (no_asm_use))[5]

   347 apply(clarify)

   348 apply(erule GrOrd.cases)

   349 apply(simp_all (no_asm_use))[7]

   350 apply(erule GrOrd.cases)

   351 apply(simp_all (no_asm_use))[7]

   352 apply(clarify)

   353 apply(erule GrOrd.cases)

   354 apply(simp_all (no_asm_use))[7]

   355 apply(erule GrOrd.cases)

   356 apply(simp_all (no_asm_use))[7]

   357 apply (metis GrOrd.intros(4))

   358 (* SEQ case *)

   359 apply(erule Prf.cases)

   360 apply(simp_all (no_asm_use))[5]

   361 apply(erule Prf.cases)

   362 apply(simp_all (no_asm_use))[5]

   363 apply(erule Prf.cases)

   364 apply(simp_all (no_asm_use))[5]

   365 apply(clarify)

   366 apply(erule GrOrd.cases)

   367 apply(simp_all (no_asm_use))[7]

   368 apply(erule GrOrd.cases)

   369 apply(simp_all (no_asm_use))[7]

   370 apply(clarify)

   371 apply (metis GrOrd.intros(1))

   372 apply (metis GrOrd.intros(1))

   373 apply(erule GrOrd.cases)

   374 apply(simp_all (no_asm_use))[7]

   375 apply (metis GrOrd.intros(1))

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

   377 

   378 

   379 section {* Values Sets *}

   380 

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

   382 where

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

   384 

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

   386 where

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

   388 

   389 lemma length_sprefix:

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

   391 unfolding sprefix_def prefix_def

   392 by (auto)

   393 

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

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

   396 

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

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

   399 

   400 lemma Suffixes_in: 

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

   402 unfolding Suffixes_def Prefixes_def prefix_def image_def

   403 apply(auto)

   404 by (metis rev_rev_ident)

   405 

   406 lemma Prefixes_Cons:

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

   408 unfolding Prefixes_def prefix_def

   409 apply(auto simp add: append_eq_Cons_conv) 

   410 done

   411 

   412 lemma finite_Prefixes:

   413   "finite (Prefixes s)"

   414 apply(induct s)

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

   416 apply(simp add: Prefixes_Cons)

   417 done

   418 

   419 lemma finite_Suffixes:

   420   "finite (Suffixes s)"

   421 unfolding Suffixes_def

   422 apply(rule finite_imageI)

   423 apply(rule finite_Prefixes)

   424 done

   425 

   426 lemma prefix_Cons:

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

   428 apply(auto simp add: prefix_def)

   429 done

   430 

   431 lemma prefix_append:

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

   433 apply(induct s)

   434 apply(simp)

   435 apply(simp add: prefix_Cons)

   436 done

   437 

   438 

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

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

   441 

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

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

   444 

   445 lemma rest_Suffixes:

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

   447 unfolding rest_def

   448 by (metis Suffixes_in append_take_drop_id)

   449 

   450 

   451 lemma Values_recs:

   452   "Values (NULL) s = {}"

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

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

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

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

   457 unfolding Values_def

   458 apply(auto)

   459 (*NULL*)

   460 apply(erule Prf.cases)

   461 apply(simp_all)[5]

   462 (*EMPTY*)

   463 apply(erule Prf.cases)

   464 apply(simp_all)[5]

   465 apply(rule Prf.intros)

   466 apply (metis append_Nil prefix_def)

   467 (*CHAR*)

   468 apply(erule Prf.cases)

   469 apply(simp_all)[5]

   470 apply(rule Prf.intros)

   471 apply(erule Prf.cases)

   472 apply(simp_all)[5]

   473 (*ALT*)

   474 apply(erule Prf.cases)

   475 apply(simp_all)[5]

   476 apply (metis Prf.intros(2))

   477 apply (metis Prf.intros(3))

   478 (*SEQ*)

   479 apply(erule Prf.cases)

   480 apply(simp_all)[5]

   481 apply (simp add: append_eq_conv_conj prefix_def rest_def)

   482 apply (metis Prf.intros(1))

   483 apply (simp add: append_eq_conv_conj prefix_def rest_def)

   484 done

   485 

   486 lemma Values_finite:

   487   "finite (Values r s)"

   488 apply(induct r arbitrary: s)

   489 apply(simp_all add: Values_recs)

   490 thm finite_surj

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

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

   493 prefer 2

   494 apply(auto)[1]

   495 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)

   496 apply(auto)[1]

   497 apply (metis rest_Suffixes)

   498 apply(rule finite_UN_I)

   499 apply(rule finite_Suffixes)

   500 apply(simp)

   501 done

   502 

   503 section {* Sulzmann functions *}

   504 

   505 fun 

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

   507 where

   508   "mkeps(EMPTY) = Void"

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

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

   511 

   512 section {* Derivatives *}

   513 

   514 fun

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

   516 where

   517   "der c (NULL) = NULL"

   518 | "der c (EMPTY) = NULL"

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

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

   521 | "der c (SEQ r1 r2) = 

   522      (if nullable r1

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

   524       else SEQ (der c r1) r2)"

   525 

   526 fun 

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

   528 where

   529   "ders [] r = r"

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

   531 

   532 

   533 section {* Injection function *}

   534 

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

   536 where

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

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

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

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

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

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

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

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

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

   546 

   547 fun 

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

   549 where

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

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

   552                     None \<Rightarrow> None

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

   554 

   555 fun 

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

   557 where

   558   "lex2 r [] = mkeps r"

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

   560 

   561 

   562 section {* Projection function *}

   563 

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

   565 where

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

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

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

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

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

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

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

   573 

   574 

   575 

   576 lemma mkeps_nullable:

   577   assumes "nullable(r)" 

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

   579 using assms

   580 apply(induct rule: nullable.induct)

   581 apply(auto intro: Prf.intros)

   582 done

   583 

   584 lemma mkeps_flat:

   585   assumes "nullable(r)" 

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

   587 using assms

   588 apply(induct rule: nullable.induct)

   589 apply(auto)

   590 done

   591 

   592 lemma v3:

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

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

   595 using assms

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

   597 apply(simp)

   598 apply(erule Prf.cases)

   599 apply(simp_all)[5]

   600 apply(simp)

   601 apply(erule Prf.cases)

   602 apply(simp_all)[5]

   603 apply(case_tac "c = c'")

   604 apply(simp)

   605 apply(erule Prf.cases)

   606 apply(simp_all)[5]

   607 apply (metis Prf.intros(5))

   608 apply(simp)

   609 apply(erule Prf.cases)

   610 apply(simp_all)[5]

   611 apply(simp)

   612 apply(erule Prf.cases)

   613 apply(simp_all)[5]

   614 apply (metis Prf.intros(2))

   615 apply (metis Prf.intros(3))

   616 apply(simp)

   617 apply(case_tac "nullable r1")

   618 apply(simp)

   619 apply(erule Prf.cases)

   620 apply(simp_all)[5]

   621 apply(auto)[1]

   622 apply(erule Prf.cases)

   623 apply(simp_all)[5]

   624 apply(auto)[1]

   625 apply (metis Prf.intros(1))

   626 apply(auto)[1]

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

   628 apply(simp)

   629 apply(erule Prf.cases)

   630 apply(simp_all)[5]

   631 apply(auto)[1]

   632 apply(rule Prf.intros)

   633 apply(auto)[2]

   634 done

   635 

   636 lemma v3_proj:

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

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

   639 using assms

   640 apply(induct rule: Prf.induct)

   641 prefer 4

   642 apply(simp)

   643 prefer 4

   644 apply(simp)

   645 apply (metis Prf.intros(4))

   646 prefer 2

   647 apply(simp)

   648 apply (metis Prf.intros(2))

   649 prefer 2

   650 apply(simp)

   651 apply (metis Prf.intros(3))

   652 apply(auto)

   653 apply(rule Prf.intros)

   654 apply(simp)

   655 apply (metis Prf_flat_L nullable_correctness)

   656 apply(rule Prf.intros)

   657 apply(rule Prf.intros)

   658 apply (metis Cons_eq_append_conv)

   659 apply(simp)

   660 apply(rule Prf.intros)

   661 apply (metis Cons_eq_append_conv)

   662 apply(simp)

   663 done

   664 

   665 lemma v4:

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

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

   668 using assms

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

   670 apply(simp)

   671 apply(erule Prf.cases)

   672 apply(simp_all)[5]

   673 apply(simp)

   674 apply(erule Prf.cases)

   675 apply(simp_all)[5]

   676 apply(simp)

   677 apply(case_tac "c = c'")

   678 apply(simp)

   679 apply(auto)[1]

   680 apply(erule Prf.cases)

   681 apply(simp_all)[5]

   682 apply(simp)

   683 apply(erule Prf.cases)

   684 apply(simp_all)[5]

   685 apply(simp)

   686 apply(erule Prf.cases)

   687 apply(simp_all)[5]

   688 apply(simp)

   689 apply(case_tac "nullable r1")

   690 apply(simp)

   691 apply(erule Prf.cases)

   692 apply(simp_all (no_asm_use))[5]

   693 apply(auto)[1]

   694 apply(erule Prf.cases)

   695 apply(simp_all)[5]

   696 apply(clarify)

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

   698 apply(auto)[1]

   699 apply (metis mkeps_flat)

   700 apply(simp)

   701 apply(erule Prf.cases)

   702 apply(simp_all)[5]

   703 done

   704 

   705 lemma v4_proj:

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

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

   708 using assms

   709 apply(induct rule: Prf.induct)

   710 prefer 4

   711 apply(simp)

   712 prefer 4

   713 apply(simp)

   714 prefer 2

   715 apply(simp)

   716 prefer 2

   717 apply(simp)

   718 apply(auto)

   719 by (metis Cons_eq_append_conv)

   720 

   721 lemma v4_proj2:

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

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

   724 using assms

   725 by (metis list.inject v4_proj)

   726 

   727 

   728 section {* Alternative Posix definition *}

   729 

   730 inductive 

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

   732 where

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

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

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

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

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

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

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

   740 

   741 

   742 lemma PMatch_mkeps:

   743   assumes "nullable r"

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

   745 using assms

   746 apply(induct r)

   747 apply(auto)

   748 apply (metis PMatch.intros(1))

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

   750 apply (rule PMatch.intros)

   751 apply(simp)

   752 apply(simp)

   753 apply(auto)[1]

   754 apply (rule PMatch.intros)

   755 apply(simp)

   756 apply (rule PMatch.intros)

   757 apply(simp)

   758 apply (rule PMatch.intros)

   759 apply(simp)

   760 by (metis nullable_correctness)

   761 

   762 

   763 lemma PMatch1:

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

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

   766 using assms

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

   768 apply(auto)

   769 apply (metis Prf.intros(4))

   770 apply (metis Prf.intros(5))

   771 apply (metis Prf.intros(2))

   772 apply (metis Prf.intros(3))

   773 apply (metis Prf.intros(1))

   774 done

   775 

   776 lemma PMatch_Values:

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

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

   779 using assms

   780 apply(simp add: Values_def PMatch1)

   781 by (metis append_Nil2 prefix_def)

   782 

   783 lemma PMatch2:

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

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

   786 using assms

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

   788 apply(auto)

   789 apply(erule PMatch.cases)

   790 apply(simp_all)[5]

   791 apply(erule PMatch.cases)

   792 apply(simp_all)[5]

   793 apply(case_tac "c = c'")

   794 apply(simp)

   795 apply(erule PMatch.cases)

   796 apply(simp_all)[5]

   797 apply (metis PMatch.intros(2))

   798 apply(simp)

   799 apply(erule PMatch.cases)

   800 apply(simp_all)[5]

   801 apply(erule PMatch.cases)

   802 apply(simp_all)[5]

   803 apply (metis PMatch.intros(3))

   804 apply(clarify)

   805 apply(rule PMatch.intros)

   806 apply metis

   807 apply(simp add: L_flat_Prf)

   808 apply(auto)[1]

   809 thm v3_proj

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

   811 apply metis

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

   813 apply(drule mp)

   814 apply (metis v4_proj2)

   815 apply(simp)

   816 apply(case_tac "nullable r1")

   817 apply(simp)

   818 defer

   819 apply(simp)

   820 apply(erule PMatch.cases)

   821 apply(simp_all)[5]

   822 apply(clarify)

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

   824 apply(rule PMatch.intros)

   825 apply metis

   826 apply metis

   827 apply(auto)[1]

   828 apply(simp add: L_flat_Prf)

   829 apply(auto)[1]

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

   831 apply metis

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

   833 apply(drule mp)

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

   835 apply(rule conjI)

   836 apply (metis v4_proj2)

   837 apply(simp)

   838 apply metis

   839 (* nullable case *)

   840 apply(erule PMatch.cases)

   841 apply(simp_all)[5]

   842 apply(clarify)

   843 apply(erule PMatch.cases)

   844 apply(simp_all)[5]

   845 apply(clarify)

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

   847 apply(rule PMatch.intros)

   848 apply metis

   849 apply metis

   850 apply(auto)[1]

   851 apply(simp add: L_flat_Prf)

   852 apply(auto)[1]

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

   854 apply metis

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

   856 apply(drule mp)

   857 apply (metis v4_proj2)

   858 apply(simp)

   859 (* interesting case *)

   860 apply(clarify)

   861 apply(simp)

   862 thm L.simps

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

   864 apply(simp only: L_flat_Prf)

   865 apply(simp)

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

   867 apply(rule PMatch.intros)

   868 apply (metis PMatch_mkeps)

   869 apply metis

   870 apply(auto)

   871 apply(simp only: L_flat_Prf)

   872 apply(simp)

   873 apply(auto)

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

   875 apply(drule mp)

   876 apply(simp)

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

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

   879 apply (metis Prf.intros(1))

   880 apply(rule v3_proj)

   881 apply(simp)

   882 by (metis Cons_eq_append_conv)

   883 

   884 lemma lex_correct1:

   885   assumes "s \<notin> L r"

   886   shows "lex r s = None"

   887 using assms

   888 apply(induct s arbitrary: r)

   889 apply(simp)

   890 apply (metis nullable_correctness)

   891 apply(auto)

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

   893 apply(drule meta_mp)

   894 apply(auto)

   895 apply(simp add: L_flat_Prf)

   896 by (metis v3 v4)

   897 

   898 

   899 lemma lex_correct2:

   900   assumes "s \<in> L r"

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

   902 using assms

   903 apply(induct s arbitrary: r)

   904 apply(simp)

   905 apply (metis mkeps_flat mkeps_nullable nullable_correctness)

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

   907 apply(drule meta_mp)

   908 apply(simp add: L_flat_Prf)

   909 apply(auto)

   910 apply (metis v3_proj v4_proj2)

   911 apply (metis v3)

   912 apply(rule v4)

   913 by metis

   914 

   915 lemma lex_correct3:

   916   assumes "s \<in> L r"

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

   918 using assms

   919 apply(induct s arbitrary: r)

   920 apply(simp)

   921 apply (metis PMatch_mkeps nullable_correctness)

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

   923 apply(drule meta_mp)

   924 apply(simp add: L_flat_Prf)

   925 apply(auto)

   926 apply (metis v3_proj v4_proj2)

   927 apply(rule PMatch2)

   928 apply(simp)

   929 done

   930 

   931 lemma lex_correct4:

   932   assumes "s \<in> L r"

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

   934 using assms

   935 apply(induct s arbitrary: r)

   936 apply(simp)

   937 apply (metis PMatch_mkeps nullable_correctness)

   938 apply(simp)

   939 apply(rule PMatch2)

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

   941 apply(drule meta_mp)

   942 apply(simp add: L_flat_Prf)

   943 apply(auto)

   944 apply (metis v3_proj v4_proj2)

   945 done

   946 

   947 lemma 

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

   949 apply(simp)

   950 done

   951 

   952 

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

   954 

   955 thm PMatch.intros

   956 

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

   958 where

   959   "\<lbrakk>s2 \<turnstile> v2 \<succ>r2 v2'; flat v1 = s1\<rbrakk> \<Longrightarrow> (s1 @ s2) \<turnstile> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 

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

   961 | "\<lbrakk>flat v1 \<sqsubseteq> s; flat v2 \<sqsubseteq> flat v1\<rbrakk> \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Right v2)"

   962 | "\<lbrakk>flat v2 \<sqsubseteq> s; flat v1 \<sqsubset>  flat v2\<rbrakk> \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Left v1)"

   963 | "s \<turnstile> v2 \<succ>r2 v2' \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Right v2')"

   964 | "s \<turnstile> v1 \<succ>r1 v1' \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Left v1')"

   965 | "s \<turnstile> Void \<succ>EMPTY Void"

   966 | "(c#s) \<turnstile> (Char c) \<succ>(CHAR c) (Char c)"

   967 

   968 

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

   970 where

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

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

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

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

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

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

   977 | "Void \<succ>EMPTY Void"

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

   979 

   980 lemma ValOrd_PMatch:

   981   assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2  \<sqsubseteq> s"

   982   shows "v1 \<succ>r v2"

   983 using assms

   984 apply(induct r arbitrary: s v1 v2 rule: rexp.induct)

   985 apply(erule Prf.cases)

   986 apply(simp_all)[5]

   987 apply(erule Prf.cases)

   988 apply(simp_all)[5]

   989 apply(erule PMatch.cases)

   990 apply(simp_all)[5]

   991 apply (metis ValOrd.intros(7))

   992 apply(erule Prf.cases)

   993 apply(simp_all)[5]

   994 apply(erule PMatch.cases)

   995 apply(simp_all)[5]

   996 apply (metis ValOrd.intros(8))

   997 defer

   998 apply(erule Prf.cases)

   999 apply(simp_all)[5]

  1000 apply(erule PMatch.cases)

  1001 apply(simp_all)[5]

  1002 apply (metis ValOrd.intros(6))

  1003 apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)

  1004 apply(clarify)

  1005 apply(erule PMatch.cases)

  1006 apply(simp_all)[5]

  1007 apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)

  1008 apply(clarify)

  1009 apply (metis ValOrd.intros(5))

  1010 (* Seq case *)

  1011 apply(erule Prf.cases)

  1012 apply(simp_all)[5]

  1013 apply(auto)

  1014 apply(erule PMatch.cases)

  1015 apply(simp_all)[5]

  1016 apply(auto)

  1017 apply(case_tac "v1b = v1a")

  1018 apply(auto)

  1019 apply(simp add: prefix_def)

  1020 apply(auto)[1]

  1021 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)

  1022 apply(simp add: prefix_def)

  1023 apply(auto)[1]

  1024 apply(simp add: append_eq_append_conv2)

  1025 apply(auto)

  1026 prefer 2

  1027 apply (metis ValOrd.intros(2))

  1028 prefer 2

  1029 apply (metis ValOrd.intros(2))

  1030 apply(case_tac "us = []")

  1031 apply(simp)

  1032 apply (metis ValOrd.intros(2) append_Nil2)

  1033 apply(drule_tac x="us" in spec)

  1034 apply(simp)

  1035 apply(drule_tac mp)

  1036 apply (metis Prf_flat_L)

  1037 apply(drule_tac x="s1 @ us" in meta_spec)

  1038 apply(drule_tac x="v1b" in meta_spec)

  1039 apply(drule_tac x="v1a" in meta_spec)

  1040 apply(drule_tac meta_mp)

  1041 

  1042 apply(simp)

  1043 apply(drule_tac meta_mp)

  1044 apply(simp)

  1045 apply(simp)

  1046 apply(simp)

  1047 apply(clarify)

  1048 apply (metis ValOrd.intros(6))

  1049 apply(clarify)

  1050 apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)

  1051 apply(erule Prf.cases)

  1052 apply(simp_all)[5]

  1053 apply(clarify)

  1054 apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)

  1055 apply (metis ValOrd.intros(5))

  1056 (* Seq case *)

  1057 apply(erule Prf.cases)

  1058 apply(simp_all)[5]

  1059 apply(auto)

  1060 apply(case_tac "v1 = v1a")

  1061 apply(auto)

  1062 apply(simp add: prefix_def)

  1063 apply(auto)[1]

  1064 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)

  1065 apply(simp add: prefix_def)

  1066 apply(auto)[1]

  1067 apply(frule PMatch1)

  1068 apply(frule PMatch1(2)[symmetric])

  1069 apply(clarify)

  1070 apply(simp add: append_eq_append_conv2)

  1071 apply(auto)

  1072 prefer 2

  1073 apply (metis ValOrd.intros(2))

  1074 prefer 2

  1075 apply (metis ValOrd.intros(2))

  1076 apply(case_tac "us = []")

  1077 apply(simp)

  1078 apply (metis ValOrd.intros(2) append_Nil2)

  1079 apply(drule_tac x="us" in spec)

  1080 apply(simp)

  1081 apply(drule mp)

  1082 apply (metis  Prf_flat_L)

  1083 apply(drule_tac x="v1a" in meta_spec)

  1084 apply(drule_tac meta_mp)

  1085 apply(simp)

  1086 apply(drule_tac meta_mp)

  1087 apply(simp)

  1088 

  1089 lemma ValOrd_PMatch:

  1090   assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2  \<sqsubseteq> s"

  1091   shows "v1 \<succ>r v2"

  1092 using assms

  1093 apply(induct arbitrary: v2 rule: .induct)

  1094 apply(erule Prf.cases)

  1095 apply(simp_all)[5]

  1096 apply (metis ValOrd.intros(7))

  1097 apply(erule Prf.cases)

  1098 apply(simp_all)[5]

  1099 apply (metis ValOrd.intros(8))

  1100 apply(erule Prf.cases)

  1101 apply(simp_all)[5]

  1102 apply(clarify)

  1103 apply (metis ValOrd.intros(6))

  1104 apply(clarify)

  1105 apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)

  1106 apply(erule Prf.cases)

  1107 apply(simp_all)[5]

  1108 apply(clarify)

  1109 apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)

  1110 apply (metis ValOrd.intros(5))

  1111 (* Seq case *)

  1112 apply(erule Prf.cases)

  1113 apply(simp_all)[5]

  1114 apply(auto)

  1115 apply(case_tac "v1 = v1a")

  1116 apply(auto)

  1117 apply(simp add: prefix_def)

  1118 apply(auto)[1]

  1119 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)

  1120 apply(simp add: prefix_def)

  1121 apply(auto)[1]

  1122 apply(frule PMatch1)

  1123 apply(frule PMatch1(2)[symmetric])

  1124 apply(clarify)

  1125 apply(simp add: append_eq_append_conv2)

  1126 apply(auto)

  1127 prefer 2

  1128 apply (metis ValOrd.intros(2))

  1129 prefer 2

  1130 apply (metis ValOrd.intros(2))

  1131 apply(case_tac "us = []")

  1132 apply(simp)

  1133 apply (metis ValOrd.intros(2) append_Nil2)

  1134 apply(drule_tac x="us" in spec)

  1135 apply(simp)