thys/ReTest.thy
changeset 104 59bad592a009
child 105 80218dddbb15
equal deleted inserted replaced
103:ffe5d850df62 104:59bad592a009
       
     1    
       
     2 theory ReTest
       
     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 definition
       
    31   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
       
    32 where
       
    33   "Der c A \<equiv> {s. [c] @ s \<in> A}"
       
    34 
       
    35 definition 
       
    36   Ders :: "string \<Rightarrow> string set \<Rightarrow> string set"
       
    37 where  
       
    38   "Ders s A \<equiv> {s' | s'. s @ s' \<in> A}"
       
    39 
       
    40 lemma Der_null [simp]:
       
    41   shows "Der c {} = {}"
       
    42 unfolding Der_def
       
    43 by auto
       
    44 
       
    45 lemma Der_empty [simp]:
       
    46   shows "Der c {[]} = {}"
       
    47 unfolding Der_def
       
    48 by auto
       
    49 
       
    50 lemma Der_char [simp]:
       
    51   shows "Der c {[d]} = (if c = d then {[]} else {})"
       
    52 unfolding Der_def
       
    53 by auto
       
    54 
       
    55 lemma Der_union [simp]:
       
    56   shows "Der c (A \<union> B) = Der c A \<union> Der c B"
       
    57 unfolding Der_def
       
    58 by auto
       
    59 
       
    60 lemma Der_seq [simp]:
       
    61   shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
       
    62 unfolding Der_def Sequ_def
       
    63 apply (auto simp add: Cons_eq_append_conv)
       
    64 done
       
    65 
       
    66 lemma seq_image:
       
    67   assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"
       
    68   shows "f ` (A ;; B) = (f ` A) ;; (f ` B)"
       
    69 apply(auto simp add: Sequ_def image_def)
       
    70 apply(rule_tac x="f s1" in exI)
       
    71 apply(rule_tac x="f s2" in exI)
       
    72 using assms
       
    73 apply(auto)
       
    74 apply(rule_tac x="xa @ xb" in exI)
       
    75 using assms
       
    76 apply(auto)
       
    77 done
       
    78 
       
    79 section {* Kleene Star for Sets *}
       
    80 
       
    81 inductive_set
       
    82   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
       
    83   for A :: "string set"
       
    84 where
       
    85   start[intro]: "[] \<in> A\<star>"
       
    86 | step[intro]:  "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"
       
    87 
       
    88 lemma star_cases:
       
    89   shows "A\<star> = {[]} \<union> A ;; A\<star>"
       
    90 unfolding Sequ_def
       
    91 by (auto) (metis Star.simps)
       
    92 
       
    93 
       
    94 fun 
       
    95   pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [100,100] 100)
       
    96 where
       
    97   "A \<up> 0 = {[]}"
       
    98 | "A \<up> (Suc n) = A ;; (A \<up> n)"  
       
    99 
       
   100 lemma star1: 
       
   101   shows "s \<in> A\<star> \<Longrightarrow> \<exists>n. s \<in> A \<up> n"
       
   102   apply(induct rule: Star.induct)
       
   103   apply (metis pow.simps(1) insertI1)
       
   104   apply(auto)
       
   105   apply(rule_tac x="Suc n" in exI)
       
   106   apply(auto simp add: Sequ_def)
       
   107   done
       
   108 
       
   109 lemma star2:
       
   110   shows "s \<in> A \<up> n \<Longrightarrow> s \<in> A\<star>"
       
   111   apply(induct n arbitrary: s)
       
   112   apply (metis pow.simps(1) Star.simps empty_iff insertE)
       
   113   apply(auto simp add: Sequ_def)
       
   114   done
       
   115 
       
   116 lemma star3:
       
   117   shows "A\<star> = (\<Union>i. A \<up> i)"
       
   118 using star1 star2
       
   119 apply(auto)
       
   120 done
       
   121 
       
   122 lemma star4:
       
   123   shows "s \<in> A \<up> n \<Longrightarrow> \<exists>ss. s = concat ss \<and> (\<forall>s' \<in> set ss. s' \<in> A)"
       
   124   apply(induct n arbitrary: s)
       
   125   apply(auto simp add: Sequ_def)
       
   126   apply(rule_tac x="[]" in exI)
       
   127   apply(auto)
       
   128   apply(drule_tac x="s2" in meta_spec)
       
   129   apply(auto)
       
   130 by (metis concat.simps(2) insertE set_simps(2))
       
   131 
       
   132 lemma star5:
       
   133   assumes "f [] = []"
       
   134   assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"
       
   135   shows "(f ` A) \<up> n = f ` (A \<up> n)"
       
   136 apply(induct n)
       
   137 apply(simp add: assms)
       
   138 apply(simp)
       
   139 apply(subst seq_image[OF assms(2)])
       
   140 apply(simp)
       
   141 done
       
   142 
       
   143 lemma star6:
       
   144   assumes "f [] = []"
       
   145   assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"
       
   146   shows "(f ` A)\<star> = f ` (A\<star>)"
       
   147 apply(simp add: star3)
       
   148 apply(simp add: image_UN)
       
   149 apply(subst star5[OF assms])
       
   150 apply(simp)
       
   151 done
       
   152 
       
   153 lemma star_decomp: 
       
   154   assumes a: "c # x \<in> A\<star>" 
       
   155   shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
       
   156 using a
       
   157 by (induct x\<equiv>"c # x" rule: Star.induct) 
       
   158    (auto simp add: append_eq_Cons_conv)
       
   159 
       
   160 lemma Der_star [simp]:
       
   161   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
       
   162 proof -    
       
   163   have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"
       
   164     
       
   165     by (simp only: star_cases[symmetric])
       
   166   also have "... = Der c (A ;; A\<star>)"
       
   167     by (simp only: Der_union Der_empty) (simp)
       
   168   also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"
       
   169     by simp
       
   170   also have "... =  (Der c A) ;; A\<star>"
       
   171     unfolding Sequ_def Der_def
       
   172     by (auto dest: star_decomp)
       
   173   finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
       
   174 qed
       
   175 
       
   176 
       
   177 
       
   178 section {* Regular Expressions *}
       
   179 
       
   180 datatype rexp =
       
   181   NULL
       
   182 | EMPTY
       
   183 | CHAR char
       
   184 | SEQ rexp rexp
       
   185 | ALT rexp rexp
       
   186 | STAR rexp
       
   187 
       
   188 section {* Semantics of Regular Expressions *}
       
   189  
       
   190 fun
       
   191   L :: "rexp \<Rightarrow> string set"
       
   192 where
       
   193   "L (NULL) = {}"
       
   194 | "L (EMPTY) = {[]}"
       
   195 | "L (CHAR c) = {[c]}"
       
   196 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
       
   197 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
       
   198 | "L (STAR r) = (L r)\<star>"
       
   199 
       
   200 fun
       
   201  nullable :: "rexp \<Rightarrow> bool"
       
   202 where
       
   203   "nullable (NULL) = False"
       
   204 | "nullable (EMPTY) = True"
       
   205 | "nullable (CHAR c) = False"
       
   206 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
       
   207 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
       
   208 | "nullable (STAR r) = True"
       
   209 
       
   210 lemma nullable_correctness:
       
   211   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
       
   212 apply (induct r) 
       
   213 apply(auto simp add: Sequ_def) 
       
   214 done
       
   215 
       
   216 
       
   217 
       
   218 section {* Values *}
       
   219 
       
   220 datatype val = 
       
   221   Void
       
   222 | Char char
       
   223 | Seq val val
       
   224 | Right val
       
   225 | Left val
       
   226 | Stars "val list"
       
   227 
       
   228 section {* The string behind a value *}
       
   229 
       
   230 fun 
       
   231   flat :: "val \<Rightarrow> string"
       
   232 where
       
   233   "flat (Void) = []"
       
   234 | "flat (Char c) = [c]"
       
   235 | "flat (Left v) = flat v"
       
   236 | "flat (Right v) = flat v"
       
   237 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
       
   238 | "flat (Stars []) = []"
       
   239 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" 
       
   240 
       
   241 lemma [simp]:
       
   242  "flat (Stars vs) = concat (map flat vs)"
       
   243 apply(induct vs)
       
   244 apply(auto)
       
   245 done
       
   246 
       
   247 section {* Relation between values and regular expressions *}
       
   248 
       
   249 inductive 
       
   250   NPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
       
   251 where
       
   252  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
       
   253 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
       
   254 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
       
   255 | "\<Turnstile> Void : EMPTY"
       
   256 | "\<Turnstile> Char c : CHAR c"
       
   257 | "\<Turnstile> Stars [] : STAR r"
       
   258 | "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Stars vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"
       
   259 
       
   260 inductive 
       
   261   Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
       
   262 where
       
   263  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
       
   264 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
       
   265 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
       
   266 | "\<turnstile> Void : EMPTY"
       
   267 | "\<turnstile> Char c : CHAR c"
       
   268 | "\<turnstile> Stars [] : STAR r"
       
   269 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
       
   270 
       
   271 lemma NPrf_imp_Prf:
       
   272   assumes "\<Turnstile> v : r" 
       
   273   shows "\<turnstile> v : r"
       
   274 using assms
       
   275 apply(induct)
       
   276 apply(auto intro: Prf.intros)
       
   277 done
       
   278 
       
   279 lemma NPrf_Prf_val:
       
   280   shows "\<turnstile> v : r \<Longrightarrow> \<exists>v'. flat v' = flat v \<and> \<Turnstile> v' : r"
       
   281   and   "\<turnstile> Stars vs : r \<Longrightarrow> \<exists>vs'. flat (Stars vs') = flat (Stars vs) \<and> \<Turnstile> Stars vs' : r"
       
   282 using assms
       
   283 apply(induct v and vs arbitrary: r and r rule: val.inducts)
       
   284 apply(auto)[1]
       
   285 apply(erule Prf.cases)
       
   286 apply(simp_all)[7]
       
   287 apply(rule_tac x="Void" in exI)
       
   288 apply(simp)
       
   289 apply(rule NPrf.intros)
       
   290 apply(erule Prf.cases)
       
   291 apply(simp_all)[7]
       
   292 apply(rule_tac x="Char c" in exI)
       
   293 apply(simp)
       
   294 apply(rule NPrf.intros)
       
   295 apply(erule Prf.cases)
       
   296 apply(simp_all)[7]
       
   297 apply(auto)[1]
       
   298 apply(drule_tac x="r1" in meta_spec)
       
   299 apply(drule_tac x="r2" in meta_spec)
       
   300 apply(simp)
       
   301 apply(auto)[1]
       
   302 apply(rule_tac x="Seq v' v'a" in exI)
       
   303 apply(simp)
       
   304 apply (metis NPrf.intros(1))
       
   305 apply(erule Prf.cases)
       
   306 apply(simp_all)[7]
       
   307 apply(clarify)
       
   308 apply(drule_tac x="r2" in meta_spec)
       
   309 apply(simp)
       
   310 apply(auto)[1]
       
   311 apply(rule_tac x="Right v'" in exI)
       
   312 apply(simp)
       
   313 apply (metis NPrf.intros)
       
   314 apply(erule Prf.cases)
       
   315 apply(simp_all)[7]
       
   316 apply(clarify)
       
   317 apply(drule_tac x="r1" in meta_spec)
       
   318 apply(simp)
       
   319 apply(auto)[1]
       
   320 apply(rule_tac x="Left v'" in exI)
       
   321 apply(simp)
       
   322 apply (metis NPrf.intros)
       
   323 apply(drule_tac x="r" in meta_spec)
       
   324 apply(simp)
       
   325 apply(auto)[1]
       
   326 apply(rule_tac x="Stars vs'" in exI)
       
   327 apply(simp)
       
   328 apply(rule_tac x="[]" in exI)
       
   329 apply(simp)
       
   330 apply(erule Prf.cases)
       
   331 apply(simp_all)[7]
       
   332 apply (metis NPrf.intros(6))
       
   333 apply(erule Prf.cases)
       
   334 apply(simp_all)[7]
       
   335 apply(auto)[1]
       
   336 apply(drule_tac x="ra" in meta_spec)
       
   337 apply(simp)
       
   338 apply(drule_tac x="STAR ra" in meta_spec)
       
   339 apply(simp)
       
   340 apply(auto)
       
   341 apply(case_tac "flat v = []")
       
   342 apply(rule_tac x="vs'" in exI)
       
   343 apply(simp)
       
   344 apply(rule_tac x="v' # vs'" in exI)
       
   345 apply(simp)
       
   346 apply(rule NPrf.intros)
       
   347 apply(auto)
       
   348 done
       
   349 
       
   350 lemma NPrf_Prf:
       
   351   shows "{flat v | v. \<turnstile> v : r} = {flat v | v. \<Turnstile> v : r}"
       
   352 apply(auto)
       
   353 apply (metis NPrf_Prf_val(1))
       
   354 by (metis NPrf_imp_Prf)
       
   355 
       
   356 
       
   357 lemma not_nullable_flat:
       
   358   assumes "\<turnstile> v : r" "\<not>nullable r"
       
   359   shows "flat v \<noteq> []"
       
   360 using assms
       
   361 apply(induct)
       
   362 apply(auto)
       
   363 done
       
   364 
       
   365 lemma Prf_flat_L:
       
   366   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
       
   367 using assms
       
   368 apply(induct v r rule: Prf.induct)
       
   369 apply(auto simp add: Sequ_def)
       
   370 done
       
   371 
       
   372 lemma NPrf_flat_L:
       
   373   assumes "\<Turnstile> v : r" shows "flat v \<in> L r"
       
   374 using assms
       
   375 by (metis NPrf_imp_Prf Prf_flat_L)
       
   376 
       
   377 lemma Prf_Stars:
       
   378   assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
       
   379   shows "\<turnstile> Stars vs : STAR r"
       
   380 using assms
       
   381 apply(induct vs)
       
   382 apply (metis Prf.intros(6))
       
   383 by (metis Prf.intros(7) insert_iff set_simps(2))
       
   384 
       
   385 lemma Star_string:
       
   386   assumes "s \<in> A\<star>"
       
   387   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"
       
   388 using assms
       
   389 apply(induct rule: Star.induct)
       
   390 apply(auto)
       
   391 apply(rule_tac x="[]" in exI)
       
   392 apply(simp)
       
   393 apply(rule_tac x="s1#ss" in exI)
       
   394 apply(simp)
       
   395 done
       
   396 
       
   397 lemma Star_val:
       
   398   assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
       
   399   shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"
       
   400 using assms
       
   401 apply(induct ss)
       
   402 apply(auto)
       
   403 apply (metis empty_iff list.set(1))
       
   404 by (metis concat.simps(2) list.simps(9) set_ConsD)
       
   405 
       
   406 lemma Star_valN:
       
   407   assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r"
       
   408   shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r)"
       
   409 using assms
       
   410 apply(induct ss)
       
   411 apply(auto)
       
   412 apply (metis empty_iff list.set(1))
       
   413 by (metis concat.simps(2) list.simps(9) set_ConsD)
       
   414 
       
   415 lemma L_flat_Prf:
       
   416   "L(r) = {flat v | v. \<turnstile> v : r}"
       
   417 apply(induct r)
       
   418 apply(auto dest: Prf_flat_L simp add: Sequ_def)
       
   419 apply (metis Prf.intros(4) flat.simps(1))
       
   420 apply (metis Prf.intros(5) flat.simps(2))
       
   421 apply (metis Prf.intros(1) flat.simps(5))
       
   422 apply (metis Prf.intros(2) flat.simps(3))
       
   423 apply (metis Prf.intros(3) flat.simps(4))
       
   424 apply(erule Prf.cases)
       
   425 apply(auto)
       
   426 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = x \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)")
       
   427 apply(auto)[1]
       
   428 apply(rule_tac x="Stars vs" in exI)
       
   429 apply(simp)
       
   430 apply(rule Prf_Stars)
       
   431 apply(simp)
       
   432 apply(drule Star_string)
       
   433 apply(auto)
       
   434 apply(rule Star_val)
       
   435 apply(simp)
       
   436 done
       
   437 
       
   438 lemma L_flat_NPrf:
       
   439   "L(r) = {flat v | v. \<Turnstile> v : r}"
       
   440 by (metis L_flat_Prf NPrf_Prf)
       
   441 
       
   442 text {* nicer proofs by Fahad *}
       
   443 
       
   444 lemma Prf_Star_flat_L:
       
   445   assumes "\<turnstile> v : STAR r" shows "flat v \<in> (L r)\<star>"
       
   446 using assms
       
   447 apply(induct v r\<equiv>"STAR r" arbitrary: r rule: Prf.induct)
       
   448 apply(auto)
       
   449 apply(simp add: star3)
       
   450 apply(auto)
       
   451 apply(rule_tac x="Suc x" in exI)
       
   452 apply(auto simp add: Sequ_def)
       
   453 apply(rule_tac x="flat v" in exI)
       
   454 apply(rule_tac x="flat (Stars vs)" in exI)
       
   455 apply(auto)
       
   456 by (metis Prf_flat_L)
       
   457 
       
   458 lemma L_flat_Prf2:
       
   459   "L(r) = {flat v | v. \<turnstile> v : r}"
       
   460 apply(induct r)
       
   461 apply(auto)
       
   462 using L.simps(1) Prf_flat_L 
       
   463 apply(blast)
       
   464 using Prf.intros(4) 
       
   465 apply(force)
       
   466 using L.simps(2) Prf_flat_L 
       
   467 apply(blast)
       
   468 using Prf.intros(5) apply force
       
   469 using L.simps(3) Prf_flat_L apply blast
       
   470 using L_flat_Prf apply auto[1]
       
   471 apply (smt L.simps(4) Sequ_def mem_Collect_eq)
       
   472 using Prf_flat_L 
       
   473 apply(fastforce)
       
   474 apply(metis Prf.intros(2) flat.simps(3))
       
   475 apply(metis Prf.intros(3) flat.simps(4))
       
   476 apply(erule Prf.cases)
       
   477 apply(simp)
       
   478 apply(simp)
       
   479 apply(auto)
       
   480 using L_flat_Prf apply auto[1]
       
   481 apply (smt Collect_cong L.simps(6) mem_Collect_eq)
       
   482 using Prf_Star_flat_L 
       
   483 apply(fastforce)
       
   484 done
       
   485 
       
   486 
       
   487 section {* Values Sets *}
       
   488 
       
   489 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100)
       
   490 where
       
   491   "s1 \<sqsubseteq> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"
       
   492 
       
   493 definition sprefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
       
   494 where
       
   495   "s1 \<sqsubset> s2 \<equiv> (s1 \<sqsubseteq> s2 \<and> s1 \<noteq> s2)"
       
   496 
       
   497 lemma length_sprefix:
       
   498   "s1 \<sqsubset> s2 \<Longrightarrow> length s1 < length s2"
       
   499 unfolding sprefix_def prefix_def
       
   500 by (auto)
       
   501 
       
   502 definition Prefixes :: "string \<Rightarrow> string set" where
       
   503   "Prefixes s \<equiv> {sp. sp \<sqsubseteq> s}"
       
   504 
       
   505 definition Suffixes :: "string \<Rightarrow> string set" where
       
   506   "Suffixes s \<equiv> rev ` (Prefixes (rev s))"
       
   507 
       
   508 definition SPrefixes :: "string \<Rightarrow> string set" where
       
   509   "SPrefixes s \<equiv> {sp. sp \<sqsubset> s}"
       
   510 
       
   511 definition SSuffixes :: "string \<Rightarrow> string set" where
       
   512   "SSuffixes s \<equiv> rev ` (SPrefixes (rev s))"
       
   513 
       
   514 lemma Suffixes_in: 
       
   515   "\<exists>s1. s1 @ s2 = s3 \<Longrightarrow> s2 \<in> Suffixes s3"
       
   516 unfolding Suffixes_def Prefixes_def prefix_def image_def
       
   517 apply(auto)
       
   518 by (metis rev_rev_ident)
       
   519 
       
   520 lemma SSuffixes_in: 
       
   521   "\<exists>s1. s1 \<noteq> [] \<and> s1 @ s2 = s3 \<Longrightarrow> s2 \<in> SSuffixes s3"
       
   522 unfolding SSuffixes_def Suffixes_def SPrefixes_def Prefixes_def sprefix_def prefix_def image_def
       
   523 apply(auto)
       
   524 by (metis append_self_conv rev.simps(1) rev_rev_ident)
       
   525 
       
   526 lemma Prefixes_Cons:
       
   527   "Prefixes (c # s) = {[]} \<union> {c # sp | sp. sp \<in> Prefixes s}"
       
   528 unfolding Prefixes_def prefix_def
       
   529 apply(auto simp add: append_eq_Cons_conv) 
       
   530 done
       
   531 
       
   532 lemma finite_Prefixes:
       
   533   "finite (Prefixes s)"
       
   534 apply(induct s)
       
   535 apply(auto simp add: Prefixes_def prefix_def)[1]
       
   536 apply(simp add: Prefixes_Cons)
       
   537 done
       
   538 
       
   539 lemma finite_Suffixes:
       
   540   "finite (Suffixes s)"
       
   541 unfolding Suffixes_def
       
   542 apply(rule finite_imageI)
       
   543 apply(rule finite_Prefixes)
       
   544 done
       
   545 
       
   546 lemma prefix_Cons:
       
   547   "((c # s1) \<sqsubseteq> (c # s2)) = (s1 \<sqsubseteq> s2)"
       
   548 apply(auto simp add: prefix_def)
       
   549 done
       
   550 
       
   551 lemma prefix_append:
       
   552   "((s @ s1) \<sqsubseteq> (s @ s2)) = (s1 \<sqsubseteq> s2)"
       
   553 apply(induct s)
       
   554 apply(simp)
       
   555 apply(simp add: prefix_Cons)
       
   556 done
       
   557 
       
   558 
       
   559 definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
       
   560   "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}"
       
   561 
       
   562 definition SValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
       
   563   "SValues r s \<equiv> {v. \<turnstile> v : r \<and> flat v = s}"
       
   564 
       
   565 
       
   566 definition NValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
       
   567   "NValues r s \<equiv> {v. \<Turnstile> v : r \<and> flat v \<sqsubseteq> s}"
       
   568 
       
   569 lemma NValues_STAR_Nil:
       
   570   "NValues (STAR r) [] = {Stars []}"
       
   571 apply(auto simp add: NValues_def prefix_def)
       
   572 apply(erule NPrf.cases)
       
   573 apply(auto)
       
   574 by (metis NPrf.intros(6))
       
   575 
       
   576 
       
   577 definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where
       
   578   "rest v s \<equiv> drop (length (flat v)) s"
       
   579 
       
   580 lemma rest_Nil:
       
   581   "rest v [] = []"
       
   582 apply(simp add: rest_def)
       
   583 done
       
   584 
       
   585 lemma rest_Suffixes:
       
   586   "rest v s \<in> Suffixes s"
       
   587 unfolding rest_def
       
   588 by (metis Suffixes_in append_take_drop_id)
       
   589 
       
   590 lemma rest_SSuffixes:
       
   591   assumes "flat v \<noteq> []" "s \<noteq> []"
       
   592   shows "rest v s \<in> SSuffixes s"
       
   593 using assms
       
   594 unfolding rest_def
       
   595 thm SSuffixes_in
       
   596 apply(rule_tac SSuffixes_in)
       
   597 apply(rule_tac x="take (length (flat v)) s" in exI)
       
   598 apply(simp add: sprefix_def)
       
   599 done
       
   600 
       
   601 
       
   602 lemma Values_recs:
       
   603   "Values (NULL) s = {}"
       
   604   "Values (EMPTY) s = {Void}"
       
   605   "Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
       
   606   "Values (ALT r1 r2) s = {Left v | v. v \<in> Values r1 s} \<union> {Right v | v. v \<in> Values r2 s}"
       
   607   "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}"
       
   608   "Values (STAR r) s = 
       
   609       {Stars []} \<union> {Stars (v # vs) | v vs. v \<in> Values r s \<and> Stars vs \<in> Values (STAR r) (rest v s)}"
       
   610 unfolding Values_def
       
   611 apply(auto)
       
   612 (*NULL*)
       
   613 apply(erule Prf.cases)
       
   614 apply(simp_all)[7]
       
   615 (*EMPTY*)
       
   616 apply(erule Prf.cases)
       
   617 apply(simp_all)[7]
       
   618 apply(rule Prf.intros)
       
   619 apply (metis append_Nil prefix_def)
       
   620 (*CHAR*)
       
   621 apply(erule Prf.cases)
       
   622 apply(simp_all)[7]
       
   623 apply(rule Prf.intros)
       
   624 apply(erule Prf.cases)
       
   625 apply(simp_all)[7]
       
   626 (*ALT*)
       
   627 apply(erule Prf.cases)
       
   628 apply(simp_all)[7]
       
   629 apply (metis Prf.intros(2))
       
   630 apply (metis Prf.intros(3))
       
   631 (*SEQ*)
       
   632 apply(erule Prf.cases)
       
   633 apply(simp_all)[7]
       
   634 apply (simp add: append_eq_conv_conj prefix_def rest_def)
       
   635 apply (metis Prf.intros(1))
       
   636 apply (simp add: append_eq_conv_conj prefix_def rest_def)
       
   637 (*STAR*)
       
   638 apply(erule Prf.cases)
       
   639 apply(simp_all)[7]
       
   640 apply(rule conjI)
       
   641 apply(simp add: prefix_def)
       
   642 apply(auto)[1]
       
   643 apply(simp add: prefix_def)
       
   644 apply(auto)[1]
       
   645 apply (metis append_eq_conv_conj rest_def)
       
   646 apply (metis Prf.intros(6))
       
   647 apply (metis append_Nil prefix_def)
       
   648 apply (metis Prf.intros(7))
       
   649 by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
       
   650 
       
   651 lemma NValues_recs:
       
   652   "NValues (NULL) s = {}"
       
   653   "NValues (EMPTY) s = {Void}"
       
   654   "NValues (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
       
   655   "NValues (ALT r1 r2) s = {Left v | v. v \<in> NValues r1 s} \<union> {Right v | v. v \<in> NValues r2 s}"
       
   656   "NValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> NValues r1 s \<and> v2 \<in> NValues r2 (rest v1 s)}"
       
   657   "NValues (STAR r) s = 
       
   658   {Stars []} \<union> {Stars (v # vs) | v vs. v \<in> NValues r s \<and> flat v \<noteq> [] \<and>  Stars vs \<in> NValues (STAR r) (rest v s)}"
       
   659 unfolding NValues_def
       
   660 apply(auto)
       
   661 (*NULL*)
       
   662 apply(erule NPrf.cases)
       
   663 apply(simp_all)[7]
       
   664 (*EMPTY*)
       
   665 apply(erule NPrf.cases)
       
   666 apply(simp_all)[7]
       
   667 apply(rule NPrf.intros)
       
   668 apply (metis append_Nil prefix_def)
       
   669 (*CHAR*)
       
   670 apply(erule NPrf.cases)
       
   671 apply(simp_all)[7]
       
   672 apply(rule NPrf.intros)
       
   673 apply(erule NPrf.cases)
       
   674 apply(simp_all)[7]
       
   675 (*ALT*)
       
   676 apply(erule NPrf.cases)
       
   677 apply(simp_all)[7]
       
   678 apply (metis NPrf.intros(2))
       
   679 apply (metis NPrf.intros(3))
       
   680 (*SEQ*)
       
   681 apply(erule NPrf.cases)
       
   682 apply(simp_all)[7]
       
   683 apply (simp add: append_eq_conv_conj prefix_def rest_def)
       
   684 apply (metis NPrf.intros(1))
       
   685 apply (simp add: append_eq_conv_conj prefix_def rest_def)
       
   686 (*STAR*)
       
   687 apply(erule NPrf.cases)
       
   688 apply(simp_all)
       
   689 apply(rule conjI)
       
   690 apply(simp add: prefix_def)
       
   691 apply(auto)[1]
       
   692 apply(simp add: prefix_def)
       
   693 apply(auto)[1]
       
   694 apply (metis append_eq_conv_conj rest_def)
       
   695 apply (metis NPrf.intros(6))
       
   696 apply (metis append_Nil prefix_def)
       
   697 apply (metis NPrf.intros(7))
       
   698 by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
       
   699 
       
   700 lemma SValues_recs:
       
   701  "SValues (NULL) s = {}"
       
   702  "SValues (EMPTY) s = (if s = [] then {Void} else {})"
       
   703  "SValues (CHAR c) s = (if [c] = s then {Char c} else {})" 
       
   704  "SValues (ALT r1 r2) s = {Left v | v. v \<in> SValues r1 s} \<union> {Right v | v. v \<in> SValues r2 s}"
       
   705  "SValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. \<exists>s1 s2. s = s1 @ s2 \<and> v1 \<in> SValues r1 s1 \<and> v2 \<in> SValues r2 s2}"
       
   706  "SValues (STAR r) s = (if s = [] then {Stars []} else {}) \<union> 
       
   707    {Stars (v # vs) | v vs. \<exists>s1 s2. s = s1 @ s2 \<and> v \<in> SValues r s1 \<and> Stars vs \<in> SValues (STAR r) s2}"
       
   708 unfolding SValues_def
       
   709 apply(auto)
       
   710 (*NULL*)
       
   711 apply(erule Prf.cases)
       
   712 apply(simp_all)[7]
       
   713 (*EMPTY*)
       
   714 apply(erule Prf.cases)
       
   715 apply(simp_all)[7]
       
   716 apply(rule Prf.intros)
       
   717 apply(erule Prf.cases)
       
   718 apply(simp_all)[7]
       
   719 (*CHAR*)
       
   720 apply(erule Prf.cases)
       
   721 apply(simp_all)[7]
       
   722 apply (metis Prf.intros(5))
       
   723 apply(erule Prf.cases)
       
   724 apply(simp_all)[7]
       
   725 (*ALT*)
       
   726 apply(erule Prf.cases)
       
   727 apply(simp_all)[7]
       
   728 apply metis
       
   729 apply(erule Prf.intros)
       
   730 apply(erule Prf.intros)
       
   731 (* SEQ case *)
       
   732 apply(erule Prf.cases)
       
   733 apply(simp_all)[7]
       
   734 apply (metis Prf.intros(1))
       
   735 (* STAR case *)
       
   736 apply(erule Prf.cases)
       
   737 apply(simp_all)[7]
       
   738 apply(rule Prf.intros)
       
   739 apply (metis Prf.intros(7))
       
   740 apply(erule Prf.cases)
       
   741 apply(simp_all)[7]
       
   742 apply (metis Prf.intros(7))
       
   743 by (metis Prf.intros(7))
       
   744 
       
   745 lemma finite_image_set2:
       
   746   "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {(x, y) | x y. P x \<and> Q y}"
       
   747   by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {(x, y)}"]) auto
       
   748 
       
   749 
       
   750 lemma NValues_finite_aux:
       
   751   "(\<lambda>(r, s). finite (NValues r s)) (r, s)"
       
   752 apply(rule wf_induct[of "measure size <*lex*> measure length",where P="\<lambda>(r, s). finite (NValues r s)"])
       
   753 apply (metis wf_lex_prod wf_measure)
       
   754 apply(auto)
       
   755 apply(case_tac a)
       
   756 apply(simp_all)
       
   757 apply(simp add: NValues_recs)
       
   758 apply(simp add: NValues_recs)
       
   759 apply(simp add: NValues_recs)
       
   760 apply(simp add: NValues_recs)
       
   761 apply(rule_tac f="\<lambda>(x, y). Seq x y" and 
       
   762                A="{(v1, v2) | v1 v2. v1 \<in> NValues rexp1 b \<and> v2 \<in> NValues rexp2 (rest v1 b)}" in finite_surj)
       
   763 prefer 2
       
   764 apply(auto)[1]
       
   765 apply(rule_tac B="\<Union>sp \<in> Suffixes b. {(v1, v2). v1 \<in> NValues rexp1 b \<and> v2 \<in> NValues rexp2 sp}" in finite_subset)
       
   766 apply(auto)[1]
       
   767 apply (metis rest_Suffixes)
       
   768 apply(rule finite_UN_I)
       
   769 apply(rule finite_Suffixes)
       
   770 apply(simp)
       
   771 apply(simp add: NValues_recs)
       
   772 apply(clarify)
       
   773 apply(subst NValues_recs)
       
   774 apply(simp)
       
   775 apply(rule_tac f="\<lambda>(v, vs). Stars (v # vs)" and 
       
   776                A="{(v, vs) | v vs. v \<in> NValues rexp b \<and> (flat v \<noteq> [] \<and> Stars vs \<in> NValues (STAR rexp) (rest v b))}" in finite_surj)
       
   777 prefer 2
       
   778 apply(auto)[1]
       
   779 apply(auto)
       
   780 apply(case_tac b)
       
   781 apply(simp)
       
   782 defer
       
   783 apply(rule_tac B="\<Union>sp \<in> SSuffixes b. {(v, vs) | v vs. v \<in> NValues rexp b \<and> Stars vs \<in> NValues (STAR rexp) sp}" in finite_subset)
       
   784 apply(auto)[1]
       
   785 apply(rule_tac x="rest aa (a # list)" in bexI)
       
   786 apply(simp)
       
   787 apply (rule rest_SSuffixes)
       
   788 apply(simp)
       
   789 apply(simp)
       
   790 apply(rule finite_UN_I)
       
   791 defer
       
   792 apply(frule_tac x="rexp" in spec)
       
   793 apply(drule_tac x="b" in spec)
       
   794 apply(drule conjunct1)
       
   795 apply(drule mp)
       
   796 apply(simp)
       
   797 apply(drule_tac x="STAR rexp" in spec)
       
   798 apply(drule_tac x="sp" in spec)
       
   799 apply(drule conjunct2)
       
   800 apply(drule mp)
       
   801 apply(simp)
       
   802 apply(simp add: prefix_def SPrefixes_def SSuffixes_def)
       
   803 apply(auto)[1]
       
   804 apply (metis length_Cons length_rev length_sprefix rev.simps(2))
       
   805 apply(simp)
       
   806 apply(rule finite_cartesian_product)
       
   807 apply(simp)
       
   808 apply(rule_tac f="Stars" in finite_imageD)
       
   809 prefer 2
       
   810 apply(auto simp add: inj_on_def)[1]
       
   811 apply (metis finite_subset image_Collect_subsetI)
       
   812 apply(simp add: rest_Nil)
       
   813 apply(simp add: NValues_STAR_Nil)
       
   814 apply(rule_tac B="{(v, vs). v \<in> NValues rexp [] \<and> vs = []}" in finite_subset)
       
   815 apply(auto)[1]
       
   816 apply(simp)
       
   817 apply(rule_tac B="Suffixes b" in finite_subset)
       
   818 apply(auto simp add: SSuffixes_def Suffixes_def Prefixes_def SPrefixes_def sprefix_def)[1]
       
   819 by (metis finite_Suffixes)
       
   820 
       
   821 lemma NValues_finite:
       
   822   "finite (NValues r s)"
       
   823 using NValues_finite_aux
       
   824 apply(simp)
       
   825 done
       
   826 
       
   827 section {* Sulzmann functions *}
       
   828 
       
   829 fun 
       
   830   mkeps :: "rexp \<Rightarrow> val"
       
   831 where
       
   832   "mkeps(EMPTY) = Void"
       
   833 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
       
   834 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
       
   835 | "mkeps(STAR r) = Stars []"
       
   836 
       
   837 section {* Derivatives *}
       
   838 
       
   839 fun
       
   840  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
       
   841 where
       
   842   "der c (NULL) = NULL"
       
   843 | "der c (EMPTY) = NULL"
       
   844 | "der c (CHAR c') = (if c = c' then EMPTY else NULL)"
       
   845 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
       
   846 | "der c (SEQ r1 r2) = 
       
   847      (if nullable r1
       
   848       then ALT (SEQ (der c r1) r2) (der c r2)
       
   849       else SEQ (der c r1) r2)"
       
   850 | "der c (STAR r) = SEQ (der c r) (STAR r)"
       
   851 
       
   852 fun 
       
   853  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
       
   854 where
       
   855   "ders [] r = r"
       
   856 | "ders (c # s) r = ders s (der c r)"
       
   857 
       
   858 
       
   859 lemma der_correctness:
       
   860   shows "L (der c r) = Der c (L r)"
       
   861 apply(induct r) 
       
   862 apply(simp_all add: nullable_correctness)
       
   863 done
       
   864 
       
   865 lemma ders_correctness:
       
   866   shows "L (ders s r) = Ders s (L r)"
       
   867 apply(induct s arbitrary: r) 
       
   868 apply(simp add: Ders_def)
       
   869 apply(simp)
       
   870 apply(subst der_correctness)
       
   871 apply(simp add: Ders_def Der_def)
       
   872 done
       
   873 
       
   874 section {* Injection function *}
       
   875 
       
   876 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
       
   877 where
       
   878   "injval (CHAR d) c Void = Char d"
       
   879 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
       
   880 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
       
   881 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
       
   882 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
       
   883 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
       
   884 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" 
       
   885 
       
   886 fun 
       
   887   lex :: "rexp \<Rightarrow> string \<Rightarrow> val option"
       
   888 where
       
   889   "lex r [] = (if nullable r then Some(mkeps r) else None)"
       
   890 | "lex r (c#s) = (case (lex (der c r) s) of  
       
   891                     None \<Rightarrow> None
       
   892                   | Some(v) \<Rightarrow> Some(injval r c v))"
       
   893 
       
   894 fun 
       
   895   lex2 :: "rexp \<Rightarrow> string \<Rightarrow> val"
       
   896 where
       
   897   "lex2 r [] = mkeps r"
       
   898 | "lex2 r (c#s) = injval r c (lex2 (der c r) s)"
       
   899 
       
   900 
       
   901 section {* Projection function *}
       
   902 
       
   903 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
       
   904 where
       
   905   "projval (CHAR d) c _ = Void"
       
   906 | "projval (ALT r1 r2) c (Left v1) = Left (projval r1 c v1)"
       
   907 | "projval (ALT r1 r2) c (Right v2) = Right (projval r2 c v2)"
       
   908 | "projval (SEQ r1 r2) c (Seq v1 v2) = 
       
   909      (if flat v1 = [] then Right(projval r2 c v2) 
       
   910       else if nullable r1 then Left (Seq (projval r1 c v1) v2)
       
   911                           else Seq (projval r1 c v1) v2)"
       
   912 | "projval (STAR r) c (Stars (v # vs)) = Seq (projval r c v) (Stars vs)"
       
   913 
       
   914 
       
   915 
       
   916 lemma mkeps_nullable:
       
   917   assumes "nullable(r)" 
       
   918   shows "\<turnstile> mkeps r : r"
       
   919 using assms
       
   920 apply(induct rule: nullable.induct)
       
   921 apply(auto intro: Prf.intros)
       
   922 done
       
   923 
       
   924 lemma mkeps_flat:
       
   925   assumes "nullable(r)" 
       
   926   shows "flat (mkeps r) = []"
       
   927 using assms
       
   928 apply(induct rule: nullable.induct)
       
   929 apply(auto)
       
   930 done
       
   931 
       
   932 
       
   933 lemma v3:
       
   934   assumes "\<turnstile> v : der c r" 
       
   935   shows "\<turnstile> (injval r c v) : r"
       
   936 using assms
       
   937 apply(induct arbitrary: v rule: der.induct)
       
   938 apply(simp)
       
   939 apply(erule Prf.cases)
       
   940 apply(simp_all)[7]
       
   941 apply(simp)
       
   942 apply(erule Prf.cases)
       
   943 apply(simp_all)[7]
       
   944 apply(case_tac "c = c'")
       
   945 apply(simp)
       
   946 apply(erule Prf.cases)
       
   947 apply(simp_all)[7]
       
   948 apply (metis Prf.intros(5))
       
   949 apply(simp)
       
   950 apply(erule Prf.cases)
       
   951 apply(simp_all)[7]
       
   952 apply(simp)
       
   953 apply(erule Prf.cases)
       
   954 apply(simp_all)[7]
       
   955 apply (metis Prf.intros(2))
       
   956 apply (metis Prf.intros(3))
       
   957 apply(simp)
       
   958 apply(case_tac "nullable r1")
       
   959 apply(simp)
       
   960 apply(erule Prf.cases)
       
   961 apply(simp_all)[7]
       
   962 apply(auto)[1]
       
   963 apply(erule Prf.cases)
       
   964 apply(simp_all)[7]
       
   965 apply(auto)[1]
       
   966 apply (metis Prf.intros(1))
       
   967 apply(auto)[1]
       
   968 apply (metis Prf.intros(1) mkeps_nullable)
       
   969 apply(simp)
       
   970 apply(erule Prf.cases)
       
   971 apply(simp_all)[7]
       
   972 apply(auto)[1]
       
   973 apply(rule Prf.intros)
       
   974 apply(auto)[2]
       
   975 apply(simp)
       
   976 apply(erule Prf.cases)
       
   977 apply(simp_all)[7]
       
   978 apply(clarify)
       
   979 apply(rotate_tac 2)
       
   980 apply(erule Prf.cases)
       
   981 apply(simp_all)[7]
       
   982 apply(auto)
       
   983 apply (metis Prf.intros(6) Prf.intros(7))
       
   984 by (metis Prf.intros(7))
       
   985 
       
   986 lemma v3_proj:
       
   987   assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
       
   988   shows "\<Turnstile> (projval r c v) : der c r"
       
   989 using assms
       
   990 apply(induct rule: NPrf.induct)
       
   991 prefer 4
       
   992 apply(simp)
       
   993 prefer 4
       
   994 apply(simp)
       
   995 apply (metis NPrf.intros(4))
       
   996 prefer 2
       
   997 apply(simp)
       
   998 apply (metis NPrf.intros(2))
       
   999 prefer 2
       
  1000 apply(simp)
       
  1001 apply (metis NPrf.intros(3))
       
  1002 apply(auto)
       
  1003 apply(rule NPrf.intros)
       
  1004 apply(simp)
       
  1005 apply (metis NPrf_imp_Prf not_nullable_flat)
       
  1006 apply(rule NPrf.intros)
       
  1007 apply(rule NPrf.intros)
       
  1008 apply (metis Cons_eq_append_conv)
       
  1009 apply(simp)
       
  1010 apply(rule NPrf.intros)
       
  1011 apply (metis Cons_eq_append_conv)
       
  1012 apply(simp)
       
  1013 (* Stars case *)
       
  1014 apply(rule NPrf.intros)
       
  1015 apply (metis Cons_eq_append_conv)
       
  1016 apply(auto)
       
  1017 done
       
  1018 
       
  1019 lemma v4:
       
  1020   assumes "\<turnstile> v : der c r" 
       
  1021   shows "flat (injval r c v) = c # (flat v)"
       
  1022 using assms
       
  1023 apply(induct arbitrary: v rule: der.induct)
       
  1024 apply(simp)
       
  1025 apply(erule Prf.cases)
       
  1026 apply(simp_all)[7]
       
  1027 apply(simp)
       
  1028 apply(erule Prf.cases)
       
  1029 apply(simp_all)[7]
       
  1030 apply(simp)
       
  1031 apply(case_tac "c = c'")
       
  1032 apply(simp)
       
  1033 apply(auto)[1]
       
  1034 apply(erule Prf.cases)
       
  1035 apply(simp_all)[7]
       
  1036 apply(simp)
       
  1037 apply(erule Prf.cases)
       
  1038 apply(simp_all)[7]
       
  1039 apply(simp)
       
  1040 apply(erule Prf.cases)
       
  1041 apply(simp_all)[7]
       
  1042 apply(simp)
       
  1043 apply(case_tac "nullable r1")
       
  1044 apply(simp)
       
  1045 apply(erule Prf.cases)
       
  1046 apply(simp_all (no_asm_use))[7]
       
  1047 apply(auto)[1]
       
  1048 apply(erule Prf.cases)
       
  1049 apply(simp_all)[7]
       
  1050 apply(clarify)
       
  1051 apply(simp only: injval.simps flat.simps)
       
  1052 apply(auto)[1]
       
  1053 apply (metis mkeps_flat)
       
  1054 apply(simp)
       
  1055 apply(erule Prf.cases)
       
  1056 apply(simp_all)[7]
       
  1057 apply(simp)
       
  1058 apply(erule Prf.cases)
       
  1059 apply(simp_all)[7]
       
  1060 apply(auto)
       
  1061 apply(rotate_tac 2)
       
  1062 apply(erule Prf.cases)
       
  1063 apply(simp_all)[7]
       
  1064 done
       
  1065 
       
  1066 lemma v4_proj:
       
  1067   assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
       
  1068   shows "c # flat (projval r c v) = flat v"
       
  1069 using assms
       
  1070 apply(induct rule: NPrf.induct)
       
  1071 prefer 4
       
  1072 apply(simp)
       
  1073 prefer 4
       
  1074 apply(simp)
       
  1075 prefer 2
       
  1076 apply(simp)
       
  1077 prefer 2
       
  1078 apply(simp)
       
  1079 apply(auto)
       
  1080 apply (metis Cons_eq_append_conv)
       
  1081 apply(simp add: append_eq_Cons_conv)
       
  1082 apply(auto)
       
  1083 done
       
  1084 
       
  1085 lemma v4_proj2:
       
  1086   assumes "\<Turnstile> v : r" and "(flat v) = c # s"
       
  1087   shows "flat (projval r c v) = s"
       
  1088 using assms
       
  1089 by (metis list.inject v4_proj)
       
  1090 
       
  1091 
       
  1092 definition 
       
  1093   PC31 :: "string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool"
       
  1094 where
       
  1095   "PC31 s r r' \<equiv> s \<notin> L r"
       
  1096 
       
  1097 definition 
       
  1098   PC41 :: "string \<Rightarrow> string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool"
       
  1099 where
       
  1100   "PC41 s s' r r' \<equiv> (\<forall>x. (s @ x \<in> L r \<longrightarrow> s' \<in> {x} ;; L r' \<longrightarrow> x = []))"
       
  1101 
       
  1102 
       
  1103 lemma
       
  1104  L1: "\<not>(nullable r1) \<longrightarrow> [] \<in> L r2 \<longrightarrow> PC31 [] r1 r2" and
       
  1105  L2: "s1 \<in> L(r1) \<longrightarrow> [] \<in> L(r2) \<longrightarrow> PC41 s1 [] r1 r2" and
       
  1106  L3: "s2 \<in> L(der c r2) \<longrightarrow> PC31 s2 (der c r1) (der c r2) \<longrightarrow> PC31 (c#s2) r1 r2" and
       
  1107  L4: "s1 \<in> L(der c r1) \<longrightarrow> s2 \<in> L(r2) \<longrightarrow> PC41 s1 s2 (der c r1) r2 \<longrightarrow> PC41 (c#s1) s2 r1 r2" and
       
  1108  L5: "nullable(r1) \<longrightarrow> s2 \<in> L(der c r2) \<longrightarrow> PC31 s2 (SEQ (der c r1) r2) (der c r2) \<longrightarrow> PC41 [] (c#s2) r1 r2" and
       
  1109  L6: "s0 \<in> L(der c r0) \<longrightarrow>  s \<in> L(STAR r0) \<longrightarrow>  PC41 s0 s (der c r0) (STAR r0) \<longrightarrow> PC41 (c#s0) s r0 (STAR r0)" and
       
  1110  L7: "s' \<in> L(r') \<longrightarrow> s' \<in> L(r) \<longrightarrow> \<not>PC31 s' r r'" and
       
  1111  L8: "s \<in> L(r) \<longrightarrow> s' \<in> L(r') \<longrightarrow> s @ x \<in> L(r) \<longrightarrow> s' \<in> {x} ;; (L(r') ;; {y}) \<longrightarrow>  x \<noteq> [] \<longrightarrow> \<not>PC41 s s' r r'"
       
  1112 apply(auto simp add: PC31_def PC41_def)[1]
       
  1113 apply (metis nullable_correctness)
       
  1114 apply(auto simp add: PC31_def PC41_def)[1]
       
  1115 apply(simp add: Sequ_def)
       
  1116 apply(auto simp add: PC31_def PC41_def)[1]
       
  1117 apply(simp add: der_correctness Der_def)
       
  1118 apply(auto simp add: PC31_def PC41_def)[1]
       
  1119 apply(simp add: der_correctness Der_def Sequ_def)
       
  1120 apply(auto simp add: PC31_def PC41_def)[1]
       
  1121 apply(simp add: Sequ_def)
       
  1122 apply(simp add: der_correctness Der_def)
       
  1123 apply(auto)[1]
       
  1124 apply (metis append_eq_Cons_conv)
       
  1125 apply(auto simp add: PC31_def PC41_def)[1]
       
  1126 apply(simp add: Sequ_def)
       
  1127 apply(simp add: der_correctness Der_def)
       
  1128 apply(auto simp add: PC31_def PC41_def)[1]
       
  1129 apply(rule impI)+
       
  1130 apply(rule notI)
       
  1131 (* 8 fails *)
       
  1132 oops
       
  1133 
       
  1134 definition 
       
  1135   PC32 :: "string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool"
       
  1136 where
       
  1137   "PC32 s r r' \<equiv> \<forall>y. s \<notin> (L r ;; {y})"
       
  1138 
       
  1139 definition 
       
  1140   PC42 :: "string \<Rightarrow> string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool"
       
  1141 where
       
  1142   "PC42 s s' r r' \<equiv> (\<forall>x. (s @ x \<in> L r \<longrightarrow> (\<exists>y. s' \<in> {x} ;; (L r' ;; {y})) \<longrightarrow> x = []))"
       
  1143 
       
  1144 
       
  1145 lemma
       
  1146  L1: "\<not>(nullable r1) \<longrightarrow> [] \<in> L r2 \<longrightarrow> PC32 [] r1 r2" and
       
  1147  L2: "s1 \<in> L(r1) \<longrightarrow> [] \<in> L(r2) \<longrightarrow> PC42 s1 [] r1 r2" and
       
  1148  L3: "s2 \<in> L(der c r2) \<longrightarrow> PC32 s2 (der c r1) (der c r2) \<longrightarrow> PC32 (c#s2) r1 r2" and
       
  1149  L4: "s1 \<in> L(der c r1) \<longrightarrow> s2 \<in> L(r2) \<longrightarrow> PC42 s1 s2 (der c r1) r2 \<longrightarrow> PC42 (c#s1) s2 r1 r2" and
       
  1150  L5: "nullable(r1) \<longrightarrow> s2 \<in> L(der c r2) \<longrightarrow> PC32 s2 (SEQ (der c r1) r2) (der c r2) \<longrightarrow> PC42 [] (c#s2) r1 r2" and
       
  1151  L6: "s0 \<in> L(der c r0) \<longrightarrow>  s \<in> L(STAR r0) \<longrightarrow>  PC42 s0 s (der c r0) (STAR r0) \<longrightarrow> PC42 (c#s0) s r0 (STAR r0)" and
       
  1152  L7: "s' \<in> L(r') \<longrightarrow> s' \<in> L(r) \<longrightarrow> \<not>PC32 s' r r'" and
       
  1153  L8: "s \<in> L(r) \<longrightarrow> s' \<in> L(r') \<longrightarrow> s @ x \<in> L(r) \<longrightarrow> s' \<in> {x} ;; (L(r') ;; {y}) \<longrightarrow>  x \<noteq> [] \<longrightarrow> \<not>PC42 s s' r r'"
       
  1154 apply(auto simp add: PC32_def PC42_def)[1]
       
  1155 oops
       
  1156 
       
  1157 definition 
       
  1158   PC33 :: "string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool"
       
  1159 where
       
  1160   "PC33 s r r' \<equiv> s \<notin> L r"
       
  1161 
       
  1162 definition 
       
  1163   PC43 :: "string \<Rightarrow> string \<Rightarrow> rexp \<Rightarrow> rexp \<Rightarrow> bool"
       
  1164 where
       
  1165   "PC43 s s' r r' \<equiv> (\<forall>x. (s @ x \<in> L r \<longrightarrow> (\<exists>y. s' \<in> {x} ;; (L r' ;; {y})) \<longrightarrow> x = []))"
       
  1166 
       
  1167 lemma
       
  1168  L1: "\<not>(nullable r1) \<longrightarrow> [] \<in> L r2 \<longrightarrow> PC33 [] r1 r2" and
       
  1169  L2: "s1 \<in> L(r1) \<longrightarrow> [] \<in> L(r2) \<longrightarrow> PC43 s1 [] r1 r2" and
       
  1170  L3: "s2 \<in> L(der c r2) \<longrightarrow> PC33 s2 (der c r1) (der c r2) \<longrightarrow> PC33 (c#s2) r1 r2" and
       
  1171  L4: "s1 \<in> L(der c r1) \<longrightarrow> s2 \<in> L(r2) \<longrightarrow> PC43 s1 s2 (der c r1) r2 \<longrightarrow> PC43 (c#s1) s2 r1 r2" and
       
  1172  L5: "nullable(r1) \<longrightarrow> s2 \<in> L(der c r2) \<longrightarrow> PC33 s2 (SEQ (der c r1) r2) (der c r2) \<longrightarrow> PC43 [] (c#s2) r1 r2" and
       
  1173  L6: "s0 \<in> L(der c r0) \<longrightarrow>  s \<in> L(STAR r0) \<longrightarrow>  PC43 s0 s (der c r0) (STAR r0) \<longrightarrow> PC43 (c#s0) s r0 (STAR r0)" and
       
  1174  L7: "s' \<in> L(r') \<longrightarrow> s' \<in> L(r) \<longrightarrow> \<not>PC33 s' r r'" and
       
  1175  L8: "s \<in> L(r) \<longrightarrow> s' \<in> L(r') \<longrightarrow> s @ x \<in> L(r) \<longrightarrow> s' \<in> {x} ;; (L(r') ;; {y}) \<longrightarrow>  x \<noteq> [] \<longrightarrow> \<not>PC43 s s' r r'"
       
  1176 apply(auto simp add: PC33_def PC43_def)[1]
       
  1177 apply (metis nullable_correctness)
       
  1178 apply(auto simp add: PC33_def PC43_def)[1]
       
  1179 apply(simp add: Sequ_def)
       
  1180 apply(auto simp add: PC33_def PC43_def)[1]
       
  1181 apply(simp add: der_correctness Der_def)
       
  1182 apply(auto simp add: PC33_def PC43_def)[1]
       
  1183 apply(simp add: der_correctness Der_def Sequ_def)
       
  1184 apply metis
       
  1185 (* 5 *)
       
  1186 apply(auto simp add: PC33_def PC43_def)[1]
       
  1187 apply(simp add: Sequ_def)
       
  1188 apply(simp add: der_correctness Der_def)
       
  1189 apply(auto)[1]
       
  1190 defer
       
  1191 apply(auto simp add: PC33_def PC43_def)[1]
       
  1192 apply(simp add: Sequ_def)
       
  1193 apply(simp add: der_correctness Der_def)
       
  1194 apply metis
       
  1195 apply(auto simp add: PC33_def PC43_def)[1]
       
  1196 apply(auto simp add: PC33_def PC43_def)[1]
       
  1197 (* 5 fails *)
       
  1198 apply(simp add: Cons_eq_append_conv)
       
  1199 apply(auto)[1]
       
  1200 apply(drule_tac x="ys'" in spec)
       
  1201 apply(simp)
       
  1202 oops
       
  1203 
       
  1204 section {* Roy's Definition *}
       
  1205 
       
  1206 inductive 
       
  1207   Roy :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<rhd> _ : _" [100, 100] 100)
       
  1208 where
       
  1209   "\<rhd> Void : EMPTY"
       
  1210 | "\<rhd> Char c : CHAR c"
       
  1211 | "\<rhd> v : r1 \<Longrightarrow> \<rhd> Left v : ALT r1 r2"
       
  1212 | "\<lbrakk>\<rhd> v : r2; flat v \<notin> L r1\<rbrakk> \<Longrightarrow> \<rhd> Right v : ALT r1 r2"
       
  1213 | "\<lbrakk>\<rhd> v1 : r1; \<rhd> v2 : r2; \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow>
       
  1214       \<rhd> Seq v1 v2 : SEQ r1 r2"
       
  1215 | "\<lbrakk>\<rhd> v : r; \<rhd> Stars vs : STAR r; flat v \<noteq> []; 
       
  1216    \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat (Stars vs) \<and> (flat v @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk> \<Longrightarrow>
       
  1217       \<rhd> Stars (v#vs) : STAR r"
       
  1218 | "\<rhd> Stars [] : STAR r"
       
  1219 
       
  1220 lemma drop_append:
       
  1221   assumes "s1 \<sqsubseteq> s2"
       
  1222   shows "s1 @ drop (length s1) s2 = s2"
       
  1223 using assms
       
  1224 apply(simp add: prefix_def)
       
  1225 apply(auto)
       
  1226 done
       
  1227 
       
  1228 lemma royA: 
       
  1229   assumes "\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)"
       
  1230   shows "\<forall>s. (s \<in> L(ders (flat v1) r1) \<and> 
       
  1231               s \<sqsubseteq> (flat v2) \<and> drop (length s) (flat v2) \<in> L r2 \<longrightarrow> s = [])" 
       
  1232 using assms
       
  1233 apply -
       
  1234 apply(rule allI)
       
  1235 apply(rule impI)
       
  1236 apply(simp add: ders_correctness)
       
  1237 apply(simp add: Ders_def)
       
  1238 thm rest_def
       
  1239 apply(drule_tac x="s" in spec)
       
  1240 apply(simp)
       
  1241 apply(erule disjE)
       
  1242 apply(simp)
       
  1243 apply(drule_tac x="drop (length s) (flat v2)" in spec)
       
  1244 apply(simp add: drop_append)
       
  1245 done
       
  1246 
       
  1247 lemma royB:
       
  1248   assumes "\<forall>s. (s \<in> L(ders (flat v1) r1) \<and> 
       
  1249               s \<sqsubseteq> (flat v2) \<and> drop (length s) (flat v2) \<in> L r2 \<longrightarrow> s = [])"
       
  1250   shows "\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" 
       
  1251 using assms
       
  1252 apply -
       
  1253 apply(auto simp add: prefix_def ders_correctness Ders_def)
       
  1254 by (metis append_eq_conv_conj)
       
  1255 
       
  1256 lemma royC: 
       
  1257   assumes "\<forall>s t. (s \<in> L(ders (flat v1) r1) \<and> 
       
  1258                 s \<sqsubseteq> (flat v2 @ t) \<and> drop (length s) (flat v2 @ t) \<in> L r2 \<longrightarrow> s = [])" 
       
  1259   shows "\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v2 \<and> (flat v1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)"
       
  1260 using assms
       
  1261 apply -
       
  1262 apply(rule royB)
       
  1263 apply(rule allI)
       
  1264 apply(drule_tac x="s" in spec)
       
  1265 apply(drule_tac x="[]" in spec)
       
  1266 apply(simp)
       
  1267 done
       
  1268 
       
  1269 inductive 
       
  1270   Roy2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("2\<rhd> _ : _" [100, 100] 100)
       
  1271 where
       
  1272   "2\<rhd> Void : EMPTY"
       
  1273 | "2\<rhd> Char c : CHAR c"
       
  1274 | "2\<rhd> v : r1 \<Longrightarrow> 2\<rhd> Left v : ALT r1 r2"
       
  1275 | "\<lbrakk>2\<rhd> v : r2; \<forall>t. flat v \<notin> (L r1 ;; {t})\<rbrakk> \<Longrightarrow> 2\<rhd> Right v : ALT r1 r2"
       
  1276 | "\<lbrakk>2\<rhd> v1 : r1; 2\<rhd> v2 : r2;
       
  1277     \<forall>s. ((flat v1 @ s \<in> L r1) \<and> 
       
  1278          (\<exists>t. s \<sqsubseteq> (flat v2 @ t) \<and> drop (length s) (flat v2) \<in> (L r2 ;; {t}))) \<longrightarrow> s = []\<rbrakk> \<Longrightarrow>
       
  1279     2\<rhd> Seq v1 v2 : SEQ r1 r2"
       
  1280 | "\<lbrakk>2\<rhd> v : r; 2\<rhd> Stars vs : STAR r; flat v \<noteq> []; 
       
  1281     \<forall>s. ((flat v @ s \<in> L r) \<and> 
       
  1282        (\<exists>t. s \<sqsubseteq> (flat (Stars vs) @ t) \<and> drop (length s) (flat (Stars vs)) \<in> (L (STAR r) ;; {t}))) \<longrightarrow> s = []\<rbrakk>
       
  1283     \<Longrightarrow> 2\<rhd> Stars (v#vs) : STAR r"
       
  1284 | "2\<rhd> Stars [] : STAR r"
       
  1285 
       
  1286 lemma Roy2_props:
       
  1287   assumes "2\<rhd> v : r"
       
  1288   shows "\<turnstile> v : r"
       
  1289 using assms
       
  1290 apply(induct)
       
  1291 apply(auto intro: Prf.intros)
       
  1292 done
       
  1293 
       
  1294 lemma Roy_mkeps_nullable:
       
  1295   assumes "nullable(r)" 
       
  1296   shows "2\<rhd> (mkeps r) : r"
       
  1297 using assms
       
  1298 apply(induct rule: nullable.induct)
       
  1299 apply(auto intro: Roy2.intros)
       
  1300 apply(rule Roy2.intros)
       
  1301 apply(simp_all)
       
  1302 apply(simp add: mkeps_flat)
       
  1303 apply(simp add: Sequ_def)
       
  1304 apply (metis nullable_correctness)
       
  1305 apply(rule Roy2.intros)
       
  1306 apply(simp_all)
       
  1307 apply(rule allI)
       
  1308 apply(rule impI)
       
  1309 apply(auto simp add: Sequ_def)
       
  1310 apply(simp add: mkeps_flat)
       
  1311 apply(auto simp add: prefix_def)
       
  1312 done
       
  1313 
       
  1314 section {* Alternative Posix definition *}
       
  1315 
       
  1316 inductive 
       
  1317   PMatch :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
       
  1318 where
       
  1319   "[] \<in> EMPTY \<rightarrow> Void"
       
  1320 | "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
       
  1321 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
       
  1322 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
       
  1323 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
       
  1324     \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
       
  1325     (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
       
  1326 | "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];
       
  1327     \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>
       
  1328     \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
       
  1329 | "[] \<in> STAR r \<rightarrow> Stars []"
       
  1330 
       
  1331 inductive 
       
  1332   PMatchX :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("\<turnstile> _ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
       
  1333 where
       
  1334   "\<turnstile> s \<in> EMPTY \<rightarrow> Void"
       
  1335 | "\<turnstile> (c # s) \<in> (CHAR c) \<rightarrow> (Char c)"
       
  1336 | "\<turnstile> s \<in> r1 \<rightarrow> v \<Longrightarrow> \<turnstile> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
       
  1337 | "\<lbrakk>\<turnstile> s \<in> r2 \<rightarrow> v; \<not>(\<exists>s'. s' \<sqsubseteq> s \<and> flat v \<sqsubseteq> s' \<and> s' \<in> L(r1))\<rbrakk> \<Longrightarrow> \<turnstile> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
       
  1338 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; \<turnstile> s2 \<in> r2 \<rightarrow> v2;
       
  1339     \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> (s3 @ s4) \<sqsubseteq> s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
       
  1340     \<turnstile> (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
       
  1341 | "\<lbrakk>s1 \<in> r \<rightarrow> v; \<turnstile> s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];
       
  1342     \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> (s\<^sub>3 @ s\<^sub>4) \<sqsubseteq> s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>
       
  1343     \<Longrightarrow> \<turnstile> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
       
  1344 | "\<turnstile> s \<in> STAR r \<rightarrow> Stars []"
       
  1345 
       
  1346 lemma PMatch1:
       
  1347   assumes "s \<in> r \<rightarrow> v"
       
  1348   shows "\<turnstile> v : r" "flat v = s"
       
  1349 using assms
       
  1350 apply(induct s r v rule: PMatch.induct)
       
  1351 apply(auto)
       
  1352 apply (metis Prf.intros(4))
       
  1353 apply (metis Prf.intros(5))
       
  1354 apply (metis Prf.intros(2))
       
  1355 apply (metis Prf.intros(3))
       
  1356 apply (metis Prf.intros(1))
       
  1357 apply (metis Prf.intros(7))
       
  1358 by (metis Prf.intros(6))
       
  1359 
       
  1360 
       
  1361 lemma PMatchX1:
       
  1362   assumes "\<turnstile> s \<in> r \<rightarrow> v"
       
  1363   shows "\<turnstile> v : r"
       
  1364 using assms
       
  1365 apply(induct s r v rule: PMatchX.induct)
       
  1366 apply(auto simp add: prefix_def intro: Prf.intros)
       
  1367 apply (metis PMatch1(1) Prf.intros(1))
       
  1368 by (metis PMatch1(1) Prf.intros(7))
       
  1369 
       
  1370 
       
  1371 lemma PMatchX:
       
  1372   assumes "\<turnstile> s \<in> r \<rightarrow> v"
       
  1373   shows "flat v \<sqsubseteq> s"
       
  1374 using assms
       
  1375 apply(induct s r v rule: PMatchX.induct)
       
  1376 apply(auto simp add: prefix_def PMatch1)
       
  1377 done
       
  1378 
       
  1379 lemma PMatchX_PMatch:
       
  1380   assumes "\<turnstile> s \<in> r \<rightarrow> v" "flat v = s"
       
  1381   shows "s \<in> r \<rightarrow> v"
       
  1382 using assms
       
  1383 apply(induct s r v rule: PMatchX.induct)
       
  1384 apply(auto intro: PMatch.intros)
       
  1385 apply(rule PMatch.intros)
       
  1386 apply(simp)
       
  1387 apply (metis PMatchX Prefixes_def mem_Collect_eq)
       
  1388 apply (smt2 PMatch.intros(5) PMatch1(2) PMatchX append_Nil2 append_assoc append_self_conv prefix_def)
       
  1389 by (metis L.simps(6) PMatch.intros(6) PMatch1(2) append_Nil2 append_eq_conv_conj prefix_def)
       
  1390 
       
  1391 lemma PMatch_PMatchX:
       
  1392   assumes "s \<in> r \<rightarrow> v" 
       
  1393   shows "\<turnstile> s \<in> r \<rightarrow> v"
       
  1394 using assms
       
  1395 apply(induct s r v arbitrary: s' rule: PMatch.induct)
       
  1396 apply(auto intro: PMatchX.intros)
       
  1397 apply(rule PMatchX.intros)
       
  1398 apply(simp)
       
  1399 apply(rule notI)
       
  1400 apply(auto)[1]
       
  1401 apply (metis PMatch1(2) append_eq_conv_conj length_sprefix less_imp_le_nat prefix_def sprefix_def take_all)
       
  1402 apply(rule PMatchX.intros)
       
  1403 apply(simp)
       
  1404 apply(simp)
       
  1405 apply(auto)[1]
       
  1406 oops
       
  1407 
       
  1408 lemma 
       
  1409   assumes "\<rhd> v : r"
       
  1410   shows "(flat v) \<in> r \<rightarrow> v"
       
  1411 using assms
       
  1412 apply(induct)
       
  1413 apply(auto intro: PMatch.intros)
       
  1414 apply(rule PMatch.intros)
       
  1415 apply(simp)
       
  1416 apply(simp)
       
  1417 apply(simp)
       
  1418 apply(auto)[1]
       
  1419 done
       
  1420 
       
  1421 lemma 
       
  1422   assumes "s \<in> r \<rightarrow> v"
       
  1423   shows "\<rhd> v : r"
       
  1424 using assms
       
  1425 apply(induct)
       
  1426 apply(auto intro: Roy.intros)
       
  1427 apply (metis PMatch1(2) Roy.intros(4))
       
  1428 apply (metis PMatch1(2) Roy.intros(5))
       
  1429 by (metis L.simps(6) PMatch1(2) Roy.intros(6))
       
  1430 
       
  1431 
       
  1432 lemma PMatch_mkeps:
       
  1433   assumes "nullable r"
       
  1434   shows "[] \<in> r \<rightarrow> mkeps r"
       
  1435 using assms
       
  1436 apply(induct r)
       
  1437 apply(auto)
       
  1438 apply (metis PMatch.intros(1))
       
  1439 apply(subst append.simps(1)[symmetric])
       
  1440 apply (rule PMatch.intros)
       
  1441 apply(simp)
       
  1442 apply(simp)
       
  1443 apply(auto)[1]
       
  1444 apply (rule PMatch.intros)
       
  1445 apply(simp)
       
  1446 apply (rule PMatch.intros)
       
  1447 apply(simp)
       
  1448 apply (rule PMatch.intros)
       
  1449 apply(simp)
       
  1450 apply (metis nullable_correctness)
       
  1451 apply(metis PMatch.intros(7))
       
  1452 done
       
  1453 
       
  1454 
       
  1455 lemma PMatch1N:
       
  1456   assumes "s \<in> r \<rightarrow> v"
       
  1457   shows "\<Turnstile> v : r" 
       
  1458 using assms
       
  1459 apply(induct s r v rule: PMatch.induct)
       
  1460 apply(auto)
       
  1461 apply (metis NPrf.intros(4))
       
  1462 apply (metis NPrf.intros(5))
       
  1463 apply (metis NPrf.intros(2))
       
  1464 apply (metis NPrf.intros(3))
       
  1465 apply (metis NPrf.intros(1))
       
  1466 apply(rule NPrf.intros)
       
  1467 apply(simp)
       
  1468 apply(simp)
       
  1469 apply(simp)
       
  1470 apply(rule NPrf.intros)
       
  1471 done
       
  1472 
       
  1473 lemma PMatch_determ:
       
  1474   shows "\<lbrakk>s \<in> r \<rightarrow> v1; s \<in> r \<rightarrow> v2\<rbrakk> \<Longrightarrow> v1 = v2"
       
  1475   and   "\<lbrakk>s \<in> (STAR r) \<rightarrow> Stars vs1; s \<in> (STAR r) \<rightarrow> Stars vs2\<rbrakk> \<Longrightarrow> vs1 = vs2"
       
  1476 apply(induct v1 and vs1 arbitrary: s r v2 and s r vs2 rule: val.inducts)
       
  1477 apply(erule PMatch.cases)
       
  1478 apply(simp_all)[7]
       
  1479 apply(erule PMatch.cases)
       
  1480 apply(simp_all)[7]
       
  1481 apply(erule PMatch.cases)
       
  1482 apply(simp_all)[7]
       
  1483 apply(erule PMatch.cases)
       
  1484 apply(simp_all)[7]
       
  1485 apply(erule PMatch.cases)
       
  1486 apply(simp_all)[7]
       
  1487 apply(erule PMatch.cases)
       
  1488 apply(simp_all)[7]
       
  1489 apply(clarify)
       
  1490 apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
       
  1491 apply metis
       
  1492 apply(rule conjI)
       
  1493 apply(simp add: append_eq_append_conv2)
       
  1494 apply(auto)[1]
       
  1495 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
       
  1496 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
       
  1497 apply(simp add: append_eq_append_conv2)
       
  1498 apply(auto)[1]
       
  1499 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
       
  1500 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
       
  1501 apply(erule PMatch.cases)
       
  1502 apply(simp_all)[7]
       
  1503 apply(clarify)
       
  1504 apply(erule PMatch.cases)
       
  1505 apply(simp_all)[7]
       
  1506 apply(clarify)
       
  1507 apply (metis NPrf_flat_L PMatch1(2) PMatch1N)
       
  1508 apply(erule PMatch.cases)
       
  1509 apply(simp_all)[7]
       
  1510 apply(clarify)
       
  1511 apply(erule PMatch.cases)
       
  1512 apply(simp_all)[7]
       
  1513 apply(clarify)
       
  1514 apply (metis NPrf_flat_L PMatch1(2) PMatch1N)
       
  1515 (* star case *)
       
  1516 defer
       
  1517 apply(erule PMatch.cases)
       
  1518 apply(simp_all)[7]
       
  1519 apply(clarify)
       
  1520 apply(erule PMatch.cases)
       
  1521 apply(simp_all)[7]
       
  1522 apply(clarify)
       
  1523 apply (metis PMatch1(2))
       
  1524 apply(rotate_tac  3)
       
  1525 apply(erule PMatch.cases)
       
  1526 apply(simp_all)[7]
       
  1527 apply(clarify)
       
  1528 apply(erule PMatch.cases)
       
  1529 apply(simp_all)[7]
       
  1530 apply(clarify)
       
  1531 apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
       
  1532 apply metis
       
  1533 apply(simp add: append_eq_append_conv2)
       
  1534 apply(auto)[1]
       
  1535 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
       
  1536 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
       
  1537 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
       
  1538 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
       
  1539 apply(erule PMatch.cases)
       
  1540 apply(simp_all)[7]
       
  1541 apply(clarify)
       
  1542 apply (metis PMatch1(2))
       
  1543 apply(erule PMatch.cases)
       
  1544 apply(simp_all)[7]
       
  1545 apply(clarify)
       
  1546 apply(erule PMatch.cases)
       
  1547 apply(simp_all)[7]
       
  1548 apply(clarify)
       
  1549 apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
       
  1550 apply(drule_tac x="s1 @ s2" in meta_spec)
       
  1551 apply(drule_tac x="rb" in meta_spec)
       
  1552 apply(drule_tac x="(va#vsa)" in meta_spec)
       
  1553 apply(simp)
       
  1554 apply(drule meta_mp)
       
  1555 apply (metis L.simps(6) PMatch.intros(6))
       
  1556 apply (metis L.simps(6) PMatch.intros(6))
       
  1557 apply(simp add: append_eq_append_conv2)
       
  1558 apply(auto)[1]
       
  1559 apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
       
  1560 apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
       
  1561 apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
       
  1562 apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N)
       
  1563 apply (metis PMatch1(2))
       
  1564 apply(erule PMatch.cases)
       
  1565 apply(simp_all)[7]
       
  1566 apply(clarify)
       
  1567 by (metis PMatch1(2))
       
  1568 
       
  1569 
       
  1570 lemma PMatch_Values:
       
  1571   assumes "s \<in> r \<rightarrow> v"
       
  1572   shows "v \<in> Values r s"
       
  1573 using assms
       
  1574 apply(simp add: Values_def PMatch1)
       
  1575 by (metis append_Nil2 prefix_def)
       
  1576 
       
  1577 lemma PMatch2:
       
  1578   assumes "s \<in> (der c r) \<rightarrow> v"
       
  1579   shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
       
  1580 using assms
       
  1581 apply(induct c r arbitrary: s v rule: der.induct)
       
  1582 apply(auto)
       
  1583 apply(erule PMatch.cases)
       
  1584 apply(simp_all)[7]
       
  1585 apply(erule PMatch.cases)
       
  1586 apply(simp_all)[7]
       
  1587 apply(case_tac "c = c'")
       
  1588 apply(simp)
       
  1589 apply(erule PMatch.cases)
       
  1590 apply(simp_all)[7]
       
  1591 apply (metis PMatch.intros(2))
       
  1592 apply(simp)
       
  1593 apply(erule PMatch.cases)
       
  1594 apply(simp_all)[7]
       
  1595 apply(erule PMatch.cases)
       
  1596 apply(simp_all)[7]
       
  1597 apply (metis PMatch.intros(3))
       
  1598 apply(clarify)
       
  1599 apply(rule PMatch.intros)
       
  1600 apply metis
       
  1601 apply(simp add: L_flat_NPrf)
       
  1602 apply(auto)[1]
       
  1603 apply(frule_tac c="c" in v3_proj)
       
  1604 apply metis
       
  1605 apply(drule_tac x="projval r1 c v" in spec)
       
  1606 apply(drule mp)
       
  1607 apply (metis v4_proj2)
       
  1608 apply (metis NPrf_imp_Prf)
       
  1609 (* SEQ case *)
       
  1610 apply(case_tac "nullable r1")
       
  1611 apply(simp)
       
  1612 prefer 2
       
  1613 apply(simp)
       
  1614 apply(erule PMatch.cases)
       
  1615 apply(simp_all)[7]
       
  1616 apply(clarify)
       
  1617 apply(subst append.simps(2)[symmetric])
       
  1618 apply(rule PMatch.intros)
       
  1619 apply metis
       
  1620 apply metis
       
  1621 apply(auto)[1]
       
  1622 apply(simp add: der_correctness Der_def)
       
  1623 apply(auto)[1]
       
  1624 (* nullable case *)
       
  1625 apply(erule PMatch.cases)
       
  1626 apply(simp_all)[7]
       
  1627 apply(clarify)
       
  1628 apply(erule PMatch.cases)
       
  1629 apply(simp_all)[4]
       
  1630 apply(clarify)
       
  1631 apply(simp (no_asm))
       
  1632 apply(subst append.simps(2)[symmetric])
       
  1633 apply(rule PMatch.intros)
       
  1634 apply metis
       
  1635 apply metis
       
  1636 apply(erule contrapos_nn)
       
  1637 apply(erule exE)+
       
  1638 apply(auto)[1]
       
  1639 apply(simp add: L_flat_NPrf)
       
  1640 apply(auto)[1]
       
  1641 thm v3_proj
       
  1642 apply(frule_tac c="c" in v3_proj)
       
  1643 apply metis
       
  1644 apply(rule_tac x="s\<^sub>3" in exI)
       
  1645 apply(simp)
       
  1646 apply (metis NPrf_imp_Prf v4_proj2)
       
  1647 apply(simp)
       
  1648 (* interesting case *)
       
  1649 apply(clarify)
       
  1650 apply(clarify)
       
  1651 apply(simp)
       
  1652 apply(subst (asm) L.simps(4)[symmetric])
       
  1653 apply(simp only: L_flat_Prf)
       
  1654 apply(simp)
       
  1655 apply(subst append.simps(1)[symmetric])
       
  1656 apply(rule PMatch.intros)
       
  1657 apply (metis PMatch_mkeps)
       
  1658 apply metis
       
  1659 apply(auto)
       
  1660 apply(simp only: L_flat_NPrf)
       
  1661 apply(simp)
       
  1662 apply(auto)
       
  1663 apply(drule_tac x="Seq (projval r1 c v) vb" in spec)
       
  1664 apply(drule mp)
       
  1665 apply(simp)
       
  1666 apply (metis append_Cons butlast_snoc list.sel(1) neq_Nil_conv rotate1.simps(2) v4_proj2)
       
  1667 apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1")
       
  1668 apply (metis NPrf_imp_Prf Prf.intros(1))
       
  1669 apply(rule NPrf_imp_Prf)
       
  1670 apply(rule v3_proj)
       
  1671 apply(simp)
       
  1672 apply (metis Cons_eq_append_conv)
       
  1673 (* Stars case *)
       
  1674 apply(erule PMatch.cases)
       
  1675 apply(simp_all)[7]
       
  1676 apply(clarify)
       
  1677 apply(rotate_tac 2)
       
  1678 apply(frule_tac PMatch1)
       
  1679 apply(erule PMatch.cases)
       
  1680 apply(simp_all)[7]
       
  1681 apply(subst append.simps(2)[symmetric])
       
  1682 apply(rule PMatch.intros)
       
  1683 apply metis
       
  1684 apply(auto)[1]
       
  1685 apply(rule PMatch.intros)
       
  1686 apply(simp)
       
  1687 apply(simp)
       
  1688 apply(simp)
       
  1689 apply (metis L.simps(6))
       
  1690 apply(subst v4)
       
  1691 apply (metis NPrf_imp_Prf PMatch1N)
       
  1692 apply(simp)
       
  1693 apply(auto)[1]
       
  1694 apply(drule_tac x="s\<^sub>3" in spec)
       
  1695 apply(drule mp)
       
  1696 defer
       
  1697 apply metis
       
  1698 apply(clarify)
       
  1699 apply(drule_tac x="s1" in meta_spec)
       
  1700 apply(drule_tac x="v1" in meta_spec)
       
  1701 apply(simp)
       
  1702 apply(rotate_tac 2)
       
  1703 apply(drule PMatch.intros(6))
       
  1704 apply(rule PMatch.intros(7))
       
  1705 apply (metis PMatch1(1) list.distinct(1) v4)
       
  1706 apply (metis Nil_is_append_conv)
       
  1707 apply(simp)
       
  1708 apply(subst der_correctness)
       
  1709 apply(simp add: Der_def)
       
  1710 done
       
  1711 
       
  1712 
       
  1713 
       
  1714 lemma Sequ_single:
       
  1715   "(A ;; {t}) = {s @ t | s . s \<in> A}"
       
  1716 apply(simp add: Sequ_def)
       
  1717 done
       
  1718 
       
  1719 lemma Sequ_not:
       
  1720   assumes "\<forall>t. s \<notin> (L(der c r1) ;; {t})" "L r1 \<noteq> {}" 
       
  1721   shows "\<forall>t. c # s \<notin> (L r1 ;; {t})"
       
  1722 using assms
       
  1723 apply(simp add: der_correctness)
       
  1724 apply(simp add: Der_def)
       
  1725 apply(simp add: Sequ_def)
       
  1726 apply(rule allI)+
       
  1727 apply(rule impI)
       
  1728 apply(simp add: Cons_eq_append_conv)
       
  1729 apply(auto)
       
  1730 
       
  1731 oops
       
  1732 
       
  1733 lemma PMatch_Roy2:
       
  1734   assumes "2\<rhd> v : (der c r)" "\<exists>s. c # s \<in> L r"
       
  1735   shows "2\<rhd> (injval r c v) : r"
       
  1736 using assms
       
  1737 apply(induct c r arbitrary: v rule: der.induct)
       
  1738 apply(auto)
       
  1739 apply(erule Roy2.cases)
       
  1740 apply(simp_all)
       
  1741 apply (metis Roy2.intros(2))
       
  1742 (* alt case *)
       
  1743 apply(erule Roy2.cases)
       
  1744 apply(simp_all)
       
  1745 apply(clarify)
       
  1746 apply (metis Roy2.intros(3))
       
  1747 apply(clarify)
       
  1748 apply(rule Roy2.intros(4))
       
  1749 apply (metis (full_types) Prf_flat_L Roy2_props v3 v4)
       
  1750 apply(subgoal_tac "\<forall>t. c # flat va \<notin> L r1 ;; {t}")
       
  1751 prefer 2
       
  1752 apply(simp add: der_correctness)
       
  1753 apply(simp add: Der_def)
       
  1754 apply(simp add: Sequ_def)
       
  1755 apply(rule allI)+
       
  1756 apply(rule impI)
       
  1757 apply(simp add: Cons_eq_append_conv)
       
  1758 apply(erule disjE)
       
  1759 apply(erule conjE)
       
  1760 prefer 2
       
  1761 apply metis
       
  1762 apply(simp)
       
  1763 apply(drule_tac x="[]" in spec)
       
  1764 apply(drule_tac x="drop 1 t" in spec)
       
  1765 apply(clarify)
       
  1766 apply(simp)
       
  1767 oops 
       
  1768 
       
  1769 lemma lex_correct1:
       
  1770   assumes "s \<notin> L r"
       
  1771   shows "lex r s = None"
       
  1772 using assms
       
  1773 apply(induct s arbitrary: r)
       
  1774 apply(simp)
       
  1775 apply (metis nullable_correctness)
       
  1776 apply(auto)
       
  1777 apply(drule_tac x="der a r" in meta_spec)
       
  1778 apply(drule meta_mp)
       
  1779 apply(auto)
       
  1780 apply(simp add: L_flat_Prf)
       
  1781 by (metis v3 v4)
       
  1782 
       
  1783 
       
  1784 lemma lex_correct2:
       
  1785   assumes "s \<in> L r"
       
  1786   shows "\<exists>v. lex r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s"
       
  1787 using assms
       
  1788 apply(induct s arbitrary: r)
       
  1789 apply(simp)
       
  1790 apply (metis mkeps_flat mkeps_nullable nullable_correctness)
       
  1791 apply(drule_tac x="der a r" in meta_spec)
       
  1792 apply(drule meta_mp)
       
  1793 apply(simp add: L_flat_NPrf)
       
  1794 apply(auto)
       
  1795 apply (metis v3_proj v4_proj2)
       
  1796 apply (metis v3)
       
  1797 apply(rule v4)
       
  1798 by metis
       
  1799 
       
  1800 lemma lex_correct3:
       
  1801   assumes "s \<in> L r"
       
  1802   shows "\<exists>v. lex r s = Some(v) \<and> s \<in> r \<rightarrow> v"
       
  1803 using assms
       
  1804 apply(induct s arbitrary: r)
       
  1805 apply(simp)
       
  1806 apply (metis PMatch_mkeps nullable_correctness)
       
  1807 apply(drule_tac x="der a r" in meta_spec)
       
  1808 apply(drule meta_mp)
       
  1809 apply(simp add: L_flat_NPrf)
       
  1810 apply(auto)
       
  1811 apply (metis v3_proj v4_proj2)
       
  1812 apply(rule PMatch2)
       
  1813 apply(simp)
       
  1814 done
       
  1815 
       
  1816 lemma lex_correct4:
       
  1817   assumes "s \<in> L r"
       
  1818   shows "\<exists>v. lex r s = Some(v) \<and> \<Turnstile> v : r \<and> flat v = s"
       
  1819 using lex_correct3[OF assms]
       
  1820 apply(auto)
       
  1821 apply (metis PMatch1N)
       
  1822 by (metis PMatch1(2))
       
  1823 
       
  1824 
       
  1825 lemma lex_correct5:
       
  1826   assumes "s \<in> L r"
       
  1827   shows "s \<in> r \<rightarrow> (lex2 r s)"
       
  1828 using assms
       
  1829 apply(induct s arbitrary: r)
       
  1830 apply(simp)
       
  1831 apply (metis PMatch_mkeps nullable_correctness)
       
  1832 apply(simp)
       
  1833 apply(rule PMatch2)
       
  1834 apply(drule_tac x="der a r" in meta_spec)
       
  1835 apply(drule meta_mp)
       
  1836 apply(simp add: L_flat_NPrf)
       
  1837 apply(auto)
       
  1838 apply (metis v3_proj v4_proj2)
       
  1839 done
       
  1840 
       
  1841 lemma 
       
  1842   "lex2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))"
       
  1843 apply(simp)
       
  1844 done
       
  1845 
       
  1846 
       
  1847 (* NOT DONE YET *)
       
  1848 
       
  1849 section {* Sulzmann's Ordering of values *}
       
  1850 
       
  1851 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
       
  1852 where
       
  1853   "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
       
  1854 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
       
  1855 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
       
  1856 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
       
  1857 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
       
  1858 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
       
  1859 | "Void \<succ>EMPTY Void"
       
  1860 | "(Char c) \<succ>(CHAR c) (Char c)"
       
  1861 | "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))"
       
  1862 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
       
  1863 | "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
       
  1864 | "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
       
  1865 | "(Stars []) \<succ>(STAR r) (Stars [])"
       
  1866 
       
  1867 lemma PMatch_ValOrd:
       
  1868   assumes "s \<in> r \<rightarrow> v" "v' \<in> SValues r s"
       
  1869   shows "v \<succ>r v'"
       
  1870 using assms
       
  1871 apply(induct r arbitrary: v v' s rule: rexp.induct)
       
  1872 apply(simp add: SValues_recs)
       
  1873 apply(simp add: SValues_recs)
       
  1874 apply(erule PMatch.cases)
       
  1875 apply(simp_all)[7]
       
  1876 apply (metis ValOrd.intros(7))
       
  1877 apply(simp add: SValues_recs)
       
  1878 apply(erule PMatch.cases)
       
  1879 apply(simp_all)[7]
       
  1880 apply (metis ValOrd.intros(8) empty_iff singletonD)
       
  1881 apply(simp add: SValues_recs)
       
  1882 apply(clarify)
       
  1883 apply(erule PMatch.cases)
       
  1884 apply(simp_all)[7]
       
  1885 apply(clarify)
       
  1886 apply(case_tac "v1a = v1")
       
  1887 apply(simp)
       
  1888 apply(rule ValOrd.intros)
       
  1889 apply(rotate_tac 1)
       
  1890 apply(drule_tac x="v2a" in meta_spec)
       
  1891 apply(rotate_tac 8)
       
  1892 apply(drule_tac x="v2" in meta_spec)
       
  1893 apply(drule_tac x="s2a" in meta_spec)
       
  1894 apply(simp)
       
  1895 apply(drule_tac meta_mp)
       
  1896 apply(simp add: SValues_def)
       
  1897 apply (metis PMatch1(2) same_append_eq)
       
  1898 apply(simp)
       
  1899 apply(rule ValOrd.intros)
       
  1900 apply(drule_tac x="v1a" in meta_spec)
       
  1901 apply(rotate_tac 8)
       
  1902 apply(drule_tac x="v1" in meta_spec)
       
  1903 apply(drule_tac x="s1a" in meta_spec)
       
  1904 apply(simp)
       
  1905 apply(drule_tac meta_mp)
       
  1906 apply(simp add: append_eq_append_conv2)
       
  1907 apply(auto)[1]
       
  1908 apply(case_tac "us=[]")
       
  1909 apply(simp)
       
  1910 apply(drule_tac x="us" in spec)
       
  1911 apply(drule mp)
       
  1912 apply(simp add: SValues_def)
       
  1913 apply (metis Prf_flat_L)
       
  1914 apply(erule disjE)
       
  1915 apply(simp)
       
  1916 apply(simp)
       
  1917 apply(simp add: SValues_def)
       
  1918 apply (metis Prf_flat_L)
       
  1919 
       
  1920 apply(subst (asm) (2) Values_def)
       
  1921 apply(simp)
       
  1922 apply(clarify)
       
  1923 apply(simp add: rest_def)
       
  1924 apply(simp add: prefix_def)
       
  1925 apply(auto)[1]
       
  1926 apply(simp add: append_eq_append_conv2)
       
  1927 apply(auto)[1]
       
  1928 apply(case_tac "us = []")
       
  1929 apply(simp)
       
  1930 apply(simp add: Values_def)
       
  1931 apply (metis append_Nil2 prefix_def)
       
  1932 apply(drule_tac x="us" in spec)
       
  1933 apply(simp)
       
  1934 apply(drule_tac mp)
       
  1935 
       
  1936 
       
  1937 oops
       
  1938 (*HERE *)
       
  1939 
       
  1940 inductive ValOrd2 :: "val \<Rightarrow> string \<Rightarrow> val \<Rightarrow> bool" ("_ 2\<succ>_ _" [100, 100, 100] 100)
       
  1941 where 
       
  1942   "v2 2\<succ>s v2' \<Longrightarrow> (Seq v1 v2) 2\<succ>(flat v1 @ s) (Seq v1 v2')" 
       
  1943 | "\<lbrakk>v1 2\<succ>s v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) 2\<succ>s (Seq v1' v2')" 
       
  1944 | "(flat v2) \<sqsubseteq> (flat v1) \<Longrightarrow> (Left v1) 2\<succ>(flat v1) (Right v2)"
       
  1945 | "(flat v1) \<sqsubset> (flat v2) \<Longrightarrow> (Right v2) 2\<succ>(flat v2) (Left v1)"
       
  1946 | "v2 2\<succ>s v2' \<Longrightarrow> (Right v2) 2\<succ>s (Right v2')"
       
  1947 | "v1 2\<succ>s v1' \<Longrightarrow> (Left v1) 2\<succ>s (Left v1')" 
       
  1948 | "Void 2\<succ>[] Void"
       
  1949 | "(Char c) 2\<succ>[c] (Char c)" 
       
  1950 | "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) 2\<succ>[] (Stars (v # vs))"
       
  1951 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) 2\<succ>(flat (Stars (v # vs))) (Stars [])"
       
  1952 | "\<lbrakk>v1 2\<succ>s v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) 2\<succ>s (Stars (v2 # vs2))"
       
  1953 | "(Stars vs1) 2\<succ>s (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) 2\<succ>(flat v @ s) (Stars (v # vs2))"
       
  1954 | "(Stars []) 2\<succ>[] (Stars [])"
       
  1955 
       
  1956 lemma ValOrd2_string1:
       
  1957   assumes "v1 2\<succ>s v2"
       
  1958   shows "s \<sqsubseteq> flat v1"
       
  1959 using assms
       
  1960 apply(induct)
       
  1961 apply(auto simp add: prefix_def)
       
  1962 apply (metis append_assoc)
       
  1963 by (metis append_assoc)
       
  1964 
       
  1965 
       
  1966 lemma admissibility:
       
  1967   assumes "s \<in> r \<rightarrow> v" "\<turnstile> v' : r" 
       
  1968   shows "(\<forall>s'. (s' \<in> L(r) \<and> s' \<sqsubseteq> s) \<longrightarrow> v 2\<succ>s' v')"
       
  1969 using assms
       
  1970 apply(induct arbitrary: v')
       
  1971 apply(erule Prf.cases)
       
  1972 apply(simp_all)[7]
       
  1973 apply (metis ValOrd2.intros(7))
       
  1974 apply(erule Prf.cases)
       
  1975 apply(simp_all)[7]
       
  1976 apply (metis ValOrd2.intros(8) append_Nil2 prefix_Cons prefix_append prefix_def)
       
  1977 apply(erule Prf.cases)
       
  1978 apply(simp_all)[7]
       
  1979 apply(auto)[1]
       
  1980 apply (metis ValOrd2.intros(6))
       
  1981 apply(rule ValOrd2.intros)
       
  1982 apply(drule_tac x="v1" in meta_spec)
       
  1983 apply(simp)
       
  1984 
       
  1985 apply(clarify)
       
  1986 apply (metis PMatch1(2) ValOrd2.intros(3))
       
  1987 apply(erule Prf.cases)
       
  1988 apply(simp_all)[7]
       
  1989 apply(auto)
       
  1990 
       
  1991 apply(case_tac "v1 = v1a")
       
  1992 apply(simp)
       
  1993 apply(rotate_tac 3)
       
  1994 apply(drule_tac x="v2a" in meta_spec)
       
  1995 apply(drule meta_mp)
       
  1996 apply(simp)
       
  1997 apply(auto)
       
  1998 apply(rule_tac x="flat v1a @ s'" in exI)
       
  1999 apply (metis PMatch1(2) ValOrd2.intros(1) prefix_append)
       
  2000 apply (metis PMatch1(2) ValOrd2.intros(2) ValOrd2_string1 flat.simps(5))
       
  2001 prefer 4
       
  2002 apply(erule Prf.cases)
       
  2003 apply(simp_all)[7]
       
  2004 prefer 2
       
  2005 apply (metis ValOrd2.intros(5))
       
  2006 
       
  2007 
       
  2008 apply (metis ValOrd.intros(6))
       
  2009 oops
       
  2010 
       
  2011 
       
  2012 lemma admissibility:
       
  2013   assumes "\<turnstile> s \<in> r \<rightarrow> v" "\<turnstile> v' : r" 
       
  2014   shows "v \<succ>r v'"
       
  2015 using assms
       
  2016 apply(induct arbitrary: v')
       
  2017 apply(erule Prf.cases)
       
  2018 apply(simp_all)[7]
       
  2019 apply (metis ValOrd.intros(7))
       
  2020 apply(erule Prf.cases)
       
  2021 apply(simp_all)[7]
       
  2022 apply (metis ValOrd.intros(8))
       
  2023 apply(erule Prf.cases)
       
  2024 apply(simp_all)[7]
       
  2025 apply (metis ValOrd.intros(6))
       
  2026 oops
       
  2027 
       
  2028 lemma admissibility:
       
  2029   assumes "2\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v"
       
  2030   shows "v \<succ>r v'"
       
  2031 using assms
       
  2032 apply(induct arbitrary: v')
       
  2033 apply(erule Prf.cases)
       
  2034 apply(simp_all)[7]
       
  2035 apply (metis ValOrd.intros(7))
       
  2036 apply(erule Prf.cases)
       
  2037 apply(simp_all)[7]
       
  2038 apply (metis ValOrd.intros(8))
       
  2039 apply(erule Prf.cases)
       
  2040 apply(simp_all)[7]
       
  2041 apply (metis ValOrd.intros(6))
       
  2042 apply (metis ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
       
  2043 apply(erule Prf.cases)
       
  2044 apply(simp_all)[7]
       
  2045 apply (metis Prf_flat_L ValOrd.intros(4) length_sprefix seq_empty(1) sprefix_def)
       
  2046 apply (metis ValOrd.intros(5))
       
  2047 oops
       
  2048 
       
  2049 
       
  2050 lemma admisibility:
       
  2051   assumes "\<rhd> v : r" "\<turnstile> v' : r"
       
  2052   shows "v \<succ>r v'"
       
  2053 using assms
       
  2054 apply(induct arbitrary: v')
       
  2055 prefer 5
       
  2056 apply(drule royA)
       
  2057 apply(erule Prf.cases)
       
  2058 apply(simp_all)[7]
       
  2059 apply(clarify)
       
  2060 apply(case_tac "v1 = v1a")
       
  2061 apply(simp)
       
  2062 apply(rule ValOrd.intros)
       
  2063 apply metis
       
  2064 apply (metis ValOrd.intros(2))
       
  2065 apply(erule Prf.cases)
       
  2066 apply(simp_all)[7]
       
  2067 apply (metis ValOrd.intros(7))
       
  2068 apply(erule Prf.cases)
       
  2069 apply(simp_all)[7]
       
  2070 apply (metis ValOrd.intros(8))
       
  2071 apply(erule Prf.cases)
       
  2072 apply(simp_all)[7]
       
  2073 apply (metis ValOrd.intros(6))
       
  2074 apply(rule ValOrd.intros)
       
  2075 defer
       
  2076 apply(erule Prf.cases)
       
  2077 apply(simp_all)[7]
       
  2078 apply(clarify)
       
  2079 apply(rule ValOrd.intros)
       
  2080 (* seq case goes through *)
       
  2081 oops
       
  2082 
       
  2083 
       
  2084 lemma admisibility:
       
  2085   assumes "\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v"
       
  2086   shows "v \<succ>r v'"
       
  2087 using assms
       
  2088 apply(induct arbitrary: v')
       
  2089 prefer 5
       
  2090 apply(drule royA)
       
  2091 apply(erule Prf.cases)
       
  2092 apply(simp_all)[7]
       
  2093 apply(clarify)
       
  2094 apply(case_tac "v1 = v1a")
       
  2095 apply(simp)
       
  2096 apply(rule ValOrd.intros)
       
  2097 apply(subst (asm) (3) prefix_def)
       
  2098 apply(erule exE)
       
  2099 apply(simp)
       
  2100 apply (metis prefix_def)
       
  2101 (* the unequal case *)
       
  2102 apply(subgoal_tac "flat v1 \<sqsubset> flat v1a \<or> flat v1a \<sqsubseteq> flat v1")
       
  2103 prefer 2
       
  2104 apply(simp add: prefix_def sprefix_def)
       
  2105 apply (metis append_eq_append_conv2)
       
  2106 apply(erule disjE)
       
  2107 (* first case  flat v1 \<sqsubset> flat v1a *)
       
  2108 apply(subst (asm) sprefix_def)
       
  2109 apply(subst (asm) (5) prefix_def)
       
  2110 apply(clarify)
       
  2111 apply(subgoal_tac "(s3 @ flat v2a) \<sqsubseteq> flat v2")
       
  2112 prefer 2
       
  2113 apply(simp)
       
  2114 apply (metis append_assoc prefix_append)
       
  2115 apply(subgoal_tac "s3 \<noteq> []")
       
  2116 prefer 2
       
  2117 apply (metis append_Nil2)
       
  2118 (* HERE *)
       
  2119 apply(subst (asm) (5) prefix_def)
       
  2120 apply(erule exE)
       
  2121 apply(simp add: ders_correctness Ders_def)
       
  2122 apply(simp add: prefix_def)
       
  2123 apply(clarify)
       
  2124 apply(subst (asm) append_eq_append_conv2)
       
  2125 apply(erule exE)
       
  2126 apply(erule disjE)
       
  2127 apply(clarify)
       
  2128 oops
       
  2129 
       
  2130 
       
  2131 
       
  2132 lemma ValOrd_refl:
       
  2133   assumes "\<turnstile> v : r"
       
  2134   shows "v \<succ>r v"
       
  2135 using assms
       
  2136 apply(induct)
       
  2137 apply(auto intro: ValOrd.intros)
       
  2138 done
       
  2139 
       
  2140 lemma ValOrd_total:
       
  2141   shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r\<rbrakk>  \<Longrightarrow> v1 \<succ>r v2 \<or> v2 \<succ>r v1"
       
  2142 apply(induct r arbitrary: v1 v2)
       
  2143 apply(auto)
       
  2144 apply(erule Prf.cases)
       
  2145 apply(simp_all)[7]
       
  2146 apply(erule Prf.cases)
       
  2147 apply(simp_all)[7]
       
  2148 apply(erule Prf.cases)
       
  2149 apply(simp_all)[7]
       
  2150 apply (metis ValOrd.intros(7))
       
  2151 apply(erule Prf.cases)
       
  2152 apply(simp_all)[7]
       
  2153 apply(erule Prf.cases)
       
  2154 apply(simp_all)[7]
       
  2155 apply (metis ValOrd.intros(8))
       
  2156 apply(erule Prf.cases)
       
  2157 apply(simp_all)[7]
       
  2158 apply(erule Prf.cases)
       
  2159 apply(simp_all)[7]
       
  2160 apply(clarify)
       
  2161 apply(case_tac "v1a = v1b")
       
  2162 apply(simp)
       
  2163 apply(rule ValOrd.intros(1))
       
  2164 apply (metis ValOrd.intros(1))
       
  2165 apply(rule ValOrd.intros(2))
       
  2166 apply(auto)[2]
       
  2167 apply(erule contrapos_np)
       
  2168 apply(rule ValOrd.intros(2))
       
  2169 apply(auto)
       
  2170 apply(erule Prf.cases)
       
  2171 apply(simp_all)[7]
       
  2172 apply(erule Prf.cases)
       
  2173 apply(simp_all)[7]
       
  2174 apply(clarify)
       
  2175 apply (metis ValOrd.intros(6))
       
  2176 apply(rule ValOrd.intros)
       
  2177 apply(erule contrapos_np)
       
  2178 apply(rule ValOrd.intros)
       
  2179 apply (metis le_eq_less_or_eq neq_iff)
       
  2180 apply(erule Prf.cases)
       
  2181 apply(simp_all)[7]
       
  2182 apply(rule ValOrd.intros)
       
  2183 apply(erule contrapos_np)
       
  2184 apply(rule ValOrd.intros)
       
  2185 apply (metis le_eq_less_or_eq neq_iff)
       
  2186 apply(rule ValOrd.intros)
       
  2187 apply(erule contrapos_np)
       
  2188 apply(rule ValOrd.intros)
       
  2189 apply(metis)
       
  2190 apply(erule Prf.cases)
       
  2191 apply(simp_all)[7]
       
  2192 apply(erule Prf.cases)
       
  2193 apply(simp_all)[7]
       
  2194 apply(auto)
       
  2195 apply (metis ValOrd.intros(13))
       
  2196 apply (metis ValOrd.intros(10) ValOrd.intros(9))
       
  2197 apply(erule Prf.cases)
       
  2198 apply(simp_all)[7]
       
  2199 apply(auto)
       
  2200 apply (metis ValOrd.intros(10) ValOrd.intros(9))
       
  2201 apply(case_tac "v = va")
       
  2202 prefer 2
       
  2203 apply (metis ValOrd.intros(11))
       
  2204 apply(simp)
       
  2205 apply(rule ValOrd.intros(12))
       
  2206 apply(erule contrapos_np)
       
  2207 apply(rule ValOrd.intros(12))
       
  2208 oops
       
  2209 
       
  2210 lemma Roy_posix:
       
  2211   assumes "\<rhd> v : r" "\<turnstile> v' : r" "flat v' \<sqsubseteq> flat v"
       
  2212   shows "v \<succ>r v'"
       
  2213 using assms
       
  2214 apply(induct r arbitrary: v v' rule: rexp.induct)
       
  2215 apply(erule Prf.cases)
       
  2216 apply(simp_all)[7]
       
  2217 apply(erule Prf.cases)
       
  2218 apply(simp_all)[7]
       
  2219 apply(erule Roy.cases)
       
  2220 apply(simp_all)
       
  2221 apply (metis ValOrd.intros(7))
       
  2222 apply(erule Prf.cases)
       
  2223 apply(simp_all)[7]
       
  2224 apply(erule Roy.cases)
       
  2225 apply(simp_all)
       
  2226 apply (metis ValOrd.intros(8))
       
  2227 prefer 2
       
  2228 apply(erule Prf.cases)
       
  2229 apply(simp_all)[7]
       
  2230 apply(erule Roy.cases)
       
  2231 apply(simp_all)
       
  2232 apply(clarify)
       
  2233 apply (metis ValOrd.intros(6))
       
  2234 apply(clarify)
       
  2235 apply (metis Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
       
  2236 apply(erule Roy.cases)
       
  2237 apply(simp_all)
       
  2238 apply (metis ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
       
  2239 apply(clarify)
       
  2240 apply (metis ValOrd.intros(5))
       
  2241 apply(erule Prf.cases)
       
  2242 apply(simp_all)[7]
       
  2243 apply(erule Roy.cases)
       
  2244 apply(simp_all)
       
  2245 apply(clarify)
       
  2246 apply(case_tac "v1a = v1")
       
  2247 apply(simp)
       
  2248 apply(rule ValOrd.intros)
       
  2249 apply (metis prefix_append)
       
  2250 apply(rule ValOrd.intros)
       
  2251 prefer 2
       
  2252 apply(simp)
       
  2253 apply(simp add: prefix_def)
       
  2254 apply(auto)[1]
       
  2255 apply(simp add: append_eq_append_conv2)
       
  2256 apply(auto)[1]
       
  2257 apply(drule_tac x="v1a" in meta_spec)
       
  2258 apply(rotate_tac 9)
       
  2259 apply(drule_tac x="v1" in meta_spec)
       
  2260 apply(drule_tac meta_mp)
       
  2261 apply(simp)
       
  2262 apply(drule_tac meta_mp)
       
  2263 apply(simp)
       
  2264 apply(drule_tac meta_mp)
       
  2265 apply(simp)
       
  2266 apply(drule_tac x="us" in spec)
       
  2267 apply(drule_tac mp)
       
  2268 apply (metis Prf_flat_L)
       
  2269 apply(auto)[1]
       
  2270 oops
       
  2271 
       
  2272 
       
  2273 lemma ValOrd_anti:
       
  2274   shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r; v1 \<succ>r v2; v2 \<succ>r v1\<rbrakk> \<Longrightarrow> v1 = v2"
       
  2275   and   "\<lbrakk>\<turnstile> Stars vs1 : r; \<turnstile> Stars vs2 : r; Stars vs1 \<succ>r Stars vs2; Stars vs2 \<succ>r Stars vs1\<rbrakk>  \<Longrightarrow> vs1 = vs2"
       
  2276 apply(induct v1 and vs1 arbitrary: r v2 and r vs2 rule: val.inducts)
       
  2277 apply(erule Prf.cases)
       
  2278 apply(simp_all)[7]
       
  2279 apply(erule Prf.cases)
       
  2280 apply(simp_all)[7]
       
  2281 apply(erule Prf.cases)
       
  2282 apply(simp_all)[7]
       
  2283 apply(erule Prf.cases)
       
  2284 apply(simp_all)[7]
       
  2285 apply(erule Prf.cases)
       
  2286 apply(simp_all)[7]
       
  2287 apply(erule Prf.cases)
       
  2288 apply(simp_all)[7]
       
  2289 apply(erule ValOrd.cases)
       
  2290 apply(simp_all)
       
  2291 apply(erule ValOrd.cases)
       
  2292 apply(simp_all)
       
  2293 apply(erule ValOrd.cases)
       
  2294 apply(simp_all)
       
  2295 apply(erule Prf.cases)
       
  2296 apply(simp_all)[7]
       
  2297 apply(erule Prf.cases)
       
  2298 apply(simp_all)[7]
       
  2299 apply(erule ValOrd.cases)
       
  2300 apply(simp_all)
       
  2301 apply(erule ValOrd.cases)
       
  2302 apply(simp_all)
       
  2303 apply(erule ValOrd.cases)
       
  2304 apply(simp_all)
       
  2305 apply(erule ValOrd.cases)
       
  2306 apply(simp_all)
       
  2307 apply(erule Prf.cases)
       
  2308 apply(simp_all)[7]
       
  2309 apply(erule Prf.cases)
       
  2310 apply(simp_all)[7]
       
  2311 apply(erule ValOrd.cases)
       
  2312 apply(simp_all)
       
  2313 apply(erule ValOrd.cases)
       
  2314 apply(simp_all)
       
  2315 apply(erule ValOrd.cases)
       
  2316 apply(simp_all)
       
  2317 apply(erule ValOrd.cases)
       
  2318 apply(simp_all)
       
  2319 apply(erule Prf.cases)
       
  2320 apply(simp_all)[7]
       
  2321 apply(erule Prf.cases)
       
  2322 apply(simp_all)[7]
       
  2323 apply(erule ValOrd.cases)
       
  2324 apply(simp_all)
       
  2325 apply(erule ValOrd.cases)
       
  2326 apply(simp_all)
       
  2327 apply(erule Prf.cases)
       
  2328 apply(simp_all)[7]
       
  2329 apply(erule ValOrd.cases)
       
  2330 apply(simp_all)
       
  2331 apply(erule ValOrd.cases)
       
  2332 apply(simp_all)
       
  2333 apply(erule ValOrd.cases)
       
  2334 apply(simp_all)
       
  2335 apply(erule ValOrd.cases)
       
  2336 apply(simp_all)
       
  2337 apply(auto)[1]
       
  2338 prefer 2
       
  2339 oops
       
  2340 
       
  2341 
       
  2342 (*
       
  2343 
       
  2344 lemma ValOrd_PMatch:
       
  2345   assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2  \<sqsubseteq> s"
       
  2346   shows "v1 \<succ>r v2"
       
  2347 using assms
       
  2348 apply(induct r arbitrary: s v1 v2 rule: rexp.induct)
       
  2349 apply(erule Prf.cases)
       
  2350 apply(simp_all)[7]
       
  2351 apply(erule Prf.cases)
       
  2352 apply(simp_all)[7]
       
  2353 apply(erule PMatch.cases)
       
  2354 apply(simp_all)[7]
       
  2355 apply (metis ValOrd.intros(7))
       
  2356 apply(erule Prf.cases)
       
  2357 apply(simp_all)[7]
       
  2358 apply(erule PMatch.cases)
       
  2359 apply(simp_all)[7]
       
  2360 apply (metis ValOrd.intros(8))
       
  2361 defer
       
  2362 apply(erule Prf.cases)
       
  2363 apply(simp_all)[7]
       
  2364 apply(erule PMatch.cases)
       
  2365 apply(simp_all)[7]
       
  2366 apply (metis ValOrd.intros(6))
       
  2367 apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
       
  2368 apply(clarify)
       
  2369 apply(erule PMatch.cases)
       
  2370 apply(simp_all)[7]
       
  2371 apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
       
  2372 apply(clarify)
       
  2373 apply (metis ValOrd.intros(5))
       
  2374 (* Stars case *)
       
  2375 apply(erule Prf.cases)
       
  2376 apply(simp_all)[7]
       
  2377 apply(erule PMatch.cases)
       
  2378 apply(simp_all)
       
  2379 apply (metis Nil_is_append_conv ValOrd.intros(10) flat.simps(7))
       
  2380 apply (metis ValOrd.intros(13))
       
  2381 apply(clarify)
       
  2382 apply(erule PMatch.cases)
       
  2383 apply(simp_all)
       
  2384 prefer 2
       
  2385 apply(rule ValOrd.intros)
       
  2386 apply(simp add: prefix_def)
       
  2387 apply(rule ValOrd.intros)
       
  2388 apply(drule_tac x="s1" in meta_spec)
       
  2389 apply(drule_tac x="va" in meta_spec)
       
  2390 apply(drule_tac x="v" in meta_spec)
       
  2391 apply(drule_tac meta_mp)
       
  2392 apply(simp)
       
  2393 apply(drule_tac meta_mp)
       
  2394 apply(simp)
       
  2395 apply(drule_tac meta_mp)
       
  2396 apply(simp add: prefix_def)
       
  2397 apply(auto)[1]
       
  2398 prefer 3
       
  2399 (* Seq case *)
       
  2400 apply(erule Prf.cases)
       
  2401 apply(simp_all)[5]
       
  2402 apply(auto)
       
  2403 apply(erule PMatch.cases)
       
  2404 apply(simp_all)[5]
       
  2405 apply(auto)
       
  2406 apply(case_tac "v1b = v1a")
       
  2407 apply(auto)
       
  2408 apply(simp add: prefix_def)
       
  2409 apply(auto)[1]
       
  2410 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
       
  2411 apply(simp add: prefix_def)
       
  2412 apply(auto)[1]
       
  2413 apply(simp add: append_eq_append_conv2)
       
  2414 apply(auto)
       
  2415 prefer 2
       
  2416 apply (metis ValOrd.intros(2))
       
  2417 prefer 2
       
  2418 apply (metis ValOrd.intros(2))
       
  2419 apply(case_tac "us = []")
       
  2420 apply(simp)
       
  2421 apply (metis ValOrd.intros(2) append_Nil2)
       
  2422 apply(drule_tac x="us" in spec)
       
  2423 apply(simp)
       
  2424 apply(drule_tac mp)
       
  2425 apply (metis Prf_flat_L)
       
  2426 apply(drule_tac x="s1 @ us" in meta_spec)
       
  2427 apply(drule_tac x="v1b" in meta_spec)
       
  2428 apply(drule_tac x="v1a" in meta_spec)
       
  2429 apply(drule_tac meta_mp)
       
  2430 
       
  2431 apply(simp)
       
  2432 apply(drule_tac meta_mp)
       
  2433 apply(simp)
       
  2434 apply(simp)
       
  2435 apply(simp)
       
  2436 apply(clarify)
       
  2437 apply (metis ValOrd.intros(6))
       
  2438 apply(clarify)
       
  2439 apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
       
  2440 apply(erule Prf.cases)
       
  2441 apply(simp_all)[5]
       
  2442 apply(clarify)
       
  2443 apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
       
  2444 apply (metis ValOrd.intros(5))
       
  2445 (* Seq case *)
       
  2446 apply(erule Prf.cases)
       
  2447 apply(simp_all)[5]
       
  2448 apply(auto)
       
  2449 apply(case_tac "v1 = v1a")
       
  2450 apply(auto)
       
  2451 apply(simp add: prefix_def)
       
  2452 apply(auto)[1]
       
  2453 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
       
  2454 apply(simp add: prefix_def)
       
  2455 apply(auto)[1]
       
  2456 apply(frule PMatch1)
       
  2457 apply(frule PMatch1(2)[symmetric])
       
  2458 apply(clarify)
       
  2459 apply(simp add: append_eq_append_conv2)
       
  2460 apply(auto)
       
  2461 prefer 2
       
  2462 apply (metis ValOrd.intros(2))
       
  2463 prefer 2
       
  2464 apply (metis ValOrd.intros(2))
       
  2465 apply(case_tac "us = []")
       
  2466 apply(simp)
       
  2467 apply (metis ValOrd.intros(2) append_Nil2)
       
  2468 apply(drule_tac x="us" in spec)
       
  2469 apply(simp)
       
  2470 apply(drule mp)
       
  2471 apply (metis  Prf_flat_L)
       
  2472 apply(drule_tac x="v1a" in meta_spec)
       
  2473 apply(drule_tac meta_mp)
       
  2474 apply(simp)
       
  2475 apply(drule_tac meta_mp)
       
  2476 apply(simp)
       
  2477 
       
  2478 lemma ValOrd_PMatch:
       
  2479   assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2  \<sqsubseteq> s"
       
  2480   shows "v1 \<succ>r v2"
       
  2481 using assms
       
  2482 apply(induct arbitrary: v2 rule: .induct)
       
  2483 apply(erule Prf.cases)
       
  2484 apply(simp_all)[5]
       
  2485 apply (metis ValOrd.intros(7))
       
  2486 apply(erule Prf.cases)
       
  2487 apply(simp_all)[5]
       
  2488 apply (metis ValOrd.intros(8))
       
  2489 apply(erule Prf.cases)
       
  2490 apply(simp_all)[5]
       
  2491 apply(clarify)
       
  2492 apply (metis ValOrd.intros(6))
       
  2493 apply(clarify)
       
  2494 apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
       
  2495 apply(erule Prf.cases)
       
  2496 apply(simp_all)[5]
       
  2497 apply(clarify)
       
  2498 apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
       
  2499 apply (metis ValOrd.intros(5))
       
  2500 (* Seq case *)
       
  2501 apply(erule Prf.cases)
       
  2502 apply(simp_all)[5]
       
  2503 apply(auto)
       
  2504 apply(case_tac "v1 = v1a")
       
  2505 apply(auto)
       
  2506 apply(simp add: prefix_def)
       
  2507 apply(auto)[1]
       
  2508 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
       
  2509 apply(simp add: prefix_def)
       
  2510 apply(auto)[1]
       
  2511 apply(frule PMatch1)
       
  2512 apply(frule PMatch1(2)[symmetric])
       
  2513 apply(clarify)
       
  2514 apply(simp add: append_eq_append_conv2)
       
  2515 apply(auto)
       
  2516 prefer 2
       
  2517 apply (metis ValOrd.intros(2))
       
  2518 prefer 2
       
  2519 apply (metis ValOrd.intros(2))
       
  2520 apply(case_tac "us = []")
       
  2521 apply(simp)
       
  2522 apply (metis ValOrd.intros(2) append_Nil2)
       
  2523 apply(drule_tac x="us" in spec)
       
  2524 apply(simp)
       
  2525 apply(drule mp)
       
  2526 apply (metis  Prf_flat_L)
       
  2527 apply(drule_tac x="v1a" in meta_spec)
       
  2528 apply(drule_tac meta_mp)
       
  2529 apply(simp)
       
  2530 apply(drule_tac meta_mp)
       
  2531 apply(simp)
       
  2532 
       
  2533 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
       
  2534 apply(rule ValOrd.intros(2))
       
  2535 apply(auto)
       
  2536 apply(drule_tac x="v1a" in meta_spec)
       
  2537 apply(drule_tac meta_mp)
       
  2538 apply(simp)
       
  2539 apply(drule_tac meta_mp)
       
  2540 prefer 2
       
  2541 apply(simp)
       
  2542 thm append_eq_append_conv
       
  2543 apply(simp add: append_eq_append_conv2)
       
  2544 apply(auto)
       
  2545 apply (metis Prf_flat_L)
       
  2546 apply(case_tac "us = []")
       
  2547 apply(simp)
       
  2548 apply(drule_tac x="us" in spec)
       
  2549 apply(drule mp)
       
  2550 
       
  2551 
       
  2552 inductive ValOrd2 :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ 2\<succ> _" [100, 100] 100)
       
  2553 where
       
  2554   "v2 2\<succ> v2' \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1 v2')" 
       
  2555 | "\<lbrakk>v1 2\<succ> v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1' v2')" 
       
  2556 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) 2\<succ> (Right v2)"
       
  2557 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) 2\<succ> (Left v1)"
       
  2558 | "v2 2\<succ> v2' \<Longrightarrow> (Right v2) 2\<succ> (Right v2')"
       
  2559 | "v1 2\<succ> v1' \<Longrightarrow> (Left v1) 2\<succ> (Left v1')"
       
  2560 | "Void 2\<succ> Void"
       
  2561 | "(Char c) 2\<succ> (Char c)"
       
  2562 
       
  2563 lemma Ord1:
       
  2564   "v1 \<succ>r v2 \<Longrightarrow> v1 2\<succ> v2"
       
  2565 apply(induct rule: ValOrd.induct)
       
  2566 apply(auto intro: ValOrd2.intros)
       
  2567 done
       
  2568 
       
  2569 lemma Ord2:
       
  2570   "v1 2\<succ> v2 \<Longrightarrow> \<exists>r. v1 \<succ>r v2"
       
  2571 apply(induct v1 v2 rule: ValOrd2.induct)
       
  2572 apply(auto intro: ValOrd.intros)
       
  2573 done
       
  2574 
       
  2575 lemma Ord3:
       
  2576   "\<lbrakk>v1 2\<succ> v2; \<turnstile> v1 : r\<rbrakk> \<Longrightarrow> v1 \<succ>r v2"
       
  2577 apply(induct v1 v2 arbitrary: r rule: ValOrd2.induct)
       
  2578 apply(auto intro: ValOrd.intros elim: Prf.cases)
       
  2579 done
       
  2580 
       
  2581 section {* Posix definition *}
       
  2582 
       
  2583 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
       
  2584 where
       
  2585   "POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v' \<sqsubseteq> flat v) \<longrightarrow> v \<succ>r v'))"
       
  2586 
       
  2587 lemma ValOrd_refl:
       
  2588   assumes "\<turnstile> v : r"
       
  2589   shows "v \<succ>r v"
       
  2590 using assms
       
  2591 apply(induct)
       
  2592 apply(auto intro: ValOrd.intros)
       
  2593 done
       
  2594 
       
  2595 lemma ValOrd_total:
       
  2596   shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r\<rbrakk>  \<Longrightarrow> v1 \<succ>r v2 \<or> v2 \<succ>r v1"
       
  2597 apply(induct r arbitrary: v1 v2)
       
  2598 apply(auto)
       
  2599 apply(erule Prf.cases)
       
  2600 apply(simp_all)[5]
       
  2601 apply(erule Prf.cases)
       
  2602 apply(simp_all)[5]
       
  2603 apply(erule Prf.cases)
       
  2604 apply(simp_all)[5]
       
  2605 apply (metis ValOrd.intros(7))
       
  2606 apply(erule Prf.cases)
       
  2607 apply(simp_all)[5]
       
  2608 apply(erule Prf.cases)
       
  2609 apply(simp_all)[5]
       
  2610 apply (metis ValOrd.intros(8))
       
  2611 apply(erule Prf.cases)
       
  2612 apply(simp_all)[5]
       
  2613 apply(erule Prf.cases)
       
  2614 apply(simp_all)[5]
       
  2615 apply(clarify)
       
  2616 apply(case_tac "v1a = v1b")
       
  2617 apply(simp)
       
  2618 apply(rule ValOrd.intros(1))
       
  2619 apply (metis ValOrd.intros(1))
       
  2620 apply(rule ValOrd.intros(2))
       
  2621 apply(auto)[2]
       
  2622 apply(erule contrapos_np)
       
  2623 apply(rule ValOrd.intros(2))
       
  2624 apply(auto)
       
  2625 apply(erule Prf.cases)
       
  2626 apply(simp_all)[5]
       
  2627 apply(erule Prf.cases)
       
  2628 apply(simp_all)[5]
       
  2629 apply (metis Ord1 Ord3 Prf.intros(2) ValOrd2.intros(6))
       
  2630 apply(rule ValOrd.intros)
       
  2631 apply(erule contrapos_np)
       
  2632 apply(rule ValOrd.intros)
       
  2633 apply (metis le_eq_less_or_eq neq_iff)
       
  2634 apply(erule Prf.cases)
       
  2635 apply(simp_all)[5]
       
  2636 apply(rule ValOrd.intros)
       
  2637 apply(erule contrapos_np)
       
  2638 apply(rule ValOrd.intros)
       
  2639 apply (metis le_eq_less_or_eq neq_iff)
       
  2640 apply(rule ValOrd.intros)
       
  2641 apply(erule contrapos_np)
       
  2642 apply(rule ValOrd.intros)
       
  2643 by metis
       
  2644 
       
  2645 lemma ValOrd_anti:
       
  2646   shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r; v1 \<succ>r v2; v2 \<succ>r v1\<rbrakk> \<Longrightarrow> v1 = v2"
       
  2647 apply(induct r arbitrary: v1 v2)
       
  2648 apply(erule Prf.cases)
       
  2649 apply(simp_all)[5]
       
  2650 apply(erule Prf.cases)
       
  2651 apply(simp_all)[5]
       
  2652 apply(erule Prf.cases)
       
  2653 apply(simp_all)[5]
       
  2654 apply(erule Prf.cases)
       
  2655 apply(simp_all)[5]
       
  2656 apply(erule Prf.cases)
       
  2657 apply(simp_all)[5]
       
  2658 apply(erule Prf.cases)
       
  2659 apply(simp_all)[5]
       
  2660 apply(erule Prf.cases)
       
  2661 apply(simp_all)[5]
       
  2662 apply(erule ValOrd.cases)
       
  2663 apply(simp_all)[8]
       
  2664 apply(erule ValOrd.cases)
       
  2665 apply(simp_all)[8]
       
  2666 apply(erule ValOrd.cases)
       
  2667 apply(simp_all)[8]
       
  2668 apply(erule Prf.cases)
       
  2669 apply(simp_all)[5]
       
  2670 apply(erule Prf.cases)
       
  2671 apply(simp_all)[5]
       
  2672 apply(erule ValOrd.cases)
       
  2673 apply(simp_all)[8]
       
  2674 apply(erule ValOrd.cases)
       
  2675 apply(simp_all)[8]
       
  2676 apply(erule ValOrd.cases)
       
  2677 apply(simp_all)[8]
       
  2678 apply(erule ValOrd.cases)
       
  2679 apply(simp_all)[8]
       
  2680 apply(erule Prf.cases)
       
  2681 apply(simp_all)[5]
       
  2682 apply(erule ValOrd.cases)
       
  2683 apply(simp_all)[8]
       
  2684 apply(erule ValOrd.cases)
       
  2685 apply(simp_all)[8]
       
  2686 apply(erule ValOrd.cases)
       
  2687 apply(simp_all)[8]
       
  2688 apply(erule ValOrd.cases)
       
  2689 apply(simp_all)[8]
       
  2690 done
       
  2691 
       
  2692 lemma POSIX_ALT_I1:
       
  2693   assumes "POSIX v1 r1" 
       
  2694   shows "POSIX (Left v1) (ALT r1 r2)"
       
  2695 using assms
       
  2696 unfolding POSIX_def
       
  2697 apply(auto)
       
  2698 apply (metis Prf.intros(2))
       
  2699 apply(rotate_tac 2)
       
  2700 apply(erule Prf.cases)
       
  2701 apply(simp_all)[5]
       
  2702 apply(auto)
       
  2703 apply(rule ValOrd.intros)
       
  2704 apply(auto)
       
  2705 apply(rule ValOrd.intros)
       
  2706 by (metis le_eq_less_or_eq length_sprefix sprefix_def)
       
  2707 
       
  2708 lemma POSIX_ALT_I2:
       
  2709   assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
       
  2710   shows "POSIX (Right v2) (ALT r1 r2)"
       
  2711 using assms
       
  2712 unfolding POSIX_def
       
  2713 apply(auto)
       
  2714 apply (metis Prf.intros)
       
  2715 apply(rotate_tac 3)
       
  2716 apply(erule Prf.cases)
       
  2717 apply(simp_all)[5]
       
  2718 apply(auto)
       
  2719 apply(rule ValOrd.intros)
       
  2720 apply metis
       
  2721 apply(rule ValOrd.intros)
       
  2722 apply metis
       
  2723 done
       
  2724 
       
  2725 thm PMatch.intros[no_vars]
       
  2726 
       
  2727 lemma POSIX_PMatch:
       
  2728   assumes "s \<in> r \<rightarrow> v" "\<turnstile> v' : r"
       
  2729   shows "length (flat v') \<le> length (flat v)" 
       
  2730 using assms
       
  2731 apply(induct arbitrary: s v v' rule: rexp.induct)
       
  2732 apply(erule Prf.cases)
       
  2733 apply(simp_all)[5]
       
  2734 apply(erule Prf.cases)
       
  2735 apply(simp_all)[5]
       
  2736 apply(erule Prf.cases)
       
  2737 apply(simp_all)[5]
       
  2738 apply(erule PMatch.cases)
       
  2739 apply(simp_all)[5]
       
  2740 defer
       
  2741 apply(erule Prf.cases)
       
  2742 apply(simp_all)[5]
       
  2743 apply(erule PMatch.cases)
       
  2744 apply(simp_all)[5]
       
  2745 apply(clarify)
       
  2746 apply(simp add: L_flat_Prf)
       
  2747 
       
  2748 apply(clarify)
       
  2749 apply (metis ValOrd.intros(8))
       
  2750 apply (metis POSIX_ALT_I1)
       
  2751 apply(rule POSIX_ALT_I2)
       
  2752 apply(simp)
       
  2753 apply(auto)[1]
       
  2754 apply(simp add: POSIX_def)
       
  2755 apply(frule PMatch1(1))
       
  2756 apply(frule PMatch1(2))
       
  2757 apply(simp)
       
  2758 
       
  2759 
       
  2760 lemma POSIX_PMatch:
       
  2761   assumes "s \<in> r \<rightarrow> v" 
       
  2762   shows "POSIX v r" 
       
  2763 using assms
       
  2764 apply(induct arbitrary: rule: PMatch.induct)
       
  2765 apply(auto)
       
  2766 apply(simp add: POSIX_def)
       
  2767 apply(auto)[1]
       
  2768 apply (metis Prf.intros(4))
       
  2769 apply(erule Prf.cases)
       
  2770 apply(simp_all)[5]
       
  2771 apply (metis ValOrd.intros(7))
       
  2772 apply(simp add: POSIX_def)
       
  2773 apply(auto)[1]
       
  2774 apply (metis Prf.intros(5))
       
  2775 apply(erule Prf.cases)
       
  2776 apply(simp_all)[5]
       
  2777 apply (metis ValOrd.intros(8))
       
  2778 apply (metis POSIX_ALT_I1)
       
  2779 apply(rule POSIX_ALT_I2)
       
  2780 apply(simp)
       
  2781 apply(auto)[1]
       
  2782 apply(simp add: POSIX_def)
       
  2783 apply(frule PMatch1(1))
       
  2784 apply(frule PMatch1(2))
       
  2785 apply(simp)
       
  2786 
       
  2787 
       
  2788 
       
  2789 lemma ValOrd_PMatch:
       
  2790   assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2 = s"
       
  2791   shows "v1 \<succ>r v2"
       
  2792 using assms
       
  2793 apply(induct arbitrary: v2 rule: PMatch.induct)
       
  2794 apply(erule Prf.cases)
       
  2795 apply(simp_all)[5]
       
  2796 apply (metis ValOrd.intros(7))
       
  2797 apply(erule Prf.cases)
       
  2798 apply(simp_all)[5]
       
  2799 apply (metis ValOrd.intros(8))
       
  2800 apply(erule Prf.cases)
       
  2801 apply(simp_all)[5]
       
  2802 apply(clarify)
       
  2803 apply (metis ValOrd.intros(6))
       
  2804 apply(clarify)
       
  2805 apply (metis PMatch1(2) ValOrd.intros(3) order_refl)
       
  2806 apply(erule Prf.cases)
       
  2807 apply(simp_all)[5]
       
  2808 apply(clarify)
       
  2809 apply (metis Prf_flat_L)
       
  2810 apply (metis ValOrd.intros(5))
       
  2811 (* Seq case *)
       
  2812 apply(erule Prf.cases)
       
  2813 apply(simp_all)[5]
       
  2814 apply(auto)
       
  2815 apply(case_tac "v1 = v1a")
       
  2816 apply(auto)
       
  2817 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
       
  2818 apply(rule ValOrd.intros(2))
       
  2819 apply(auto)
       
  2820 apply(drule_tac x="v1a" in meta_spec)
       
  2821 apply(drule_tac meta_mp)
       
  2822 apply(simp)
       
  2823 apply(drule_tac meta_mp)
       
  2824 prefer 2
       
  2825 apply(simp)
       
  2826 apply(simp add: append_eq_append_conv2)
       
  2827 apply(auto)
       
  2828 apply (metis Prf_flat_L)
       
  2829 apply(case_tac "us = []")
       
  2830 apply(simp)
       
  2831 apply(drule_tac x="us" in spec)
       
  2832 apply(drule mp)
       
  2833 
       
  2834 thm L_flat_Prf
       
  2835 apply(simp add: L_flat_Prf)
       
  2836 thm append_eq_append_conv2
       
  2837 apply(simp add: append_eq_append_conv2)
       
  2838 apply(auto)
       
  2839 apply(drule_tac x="us" in spec)
       
  2840 apply(drule mp)
       
  2841 apply metis
       
  2842 apply (metis append_Nil2)
       
  2843 apply(case_tac "us = []")
       
  2844 apply(auto)
       
  2845 apply(drule_tac x="s2" in spec)
       
  2846 apply(drule mp)
       
  2847 
       
  2848 apply(auto)[1]
       
  2849 apply(drule_tac x="v1a" in meta_spec)
       
  2850 apply(simp)
       
  2851 
       
  2852 lemma refl_on_ValOrd:
       
  2853   "refl_on (Values r s) {(v1, v2). v1 \<succ>r v2 \<and> v1 \<in> Values r s \<and> v2 \<in> Values r s}"
       
  2854 unfolding refl_on_def
       
  2855 apply(auto)
       
  2856 apply(rule ValOrd_refl)
       
  2857 apply(simp add: Values_def)
       
  2858 done
       
  2859 
       
  2860 
       
  2861 section {* Posix definition *}
       
  2862 
       
  2863 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
       
  2864 where
       
  2865   "POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v'))"
       
  2866 
       
  2867 definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
       
  2868 where
       
  2869   "POSIX2 v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v 2\<succ> v'))"
       
  2870 
       
  2871 lemma "POSIX v r = POSIX2 v r"
       
  2872 unfolding POSIX_def POSIX2_def
       
  2873 apply(auto)
       
  2874 apply(rule Ord1)
       
  2875 apply(auto)
       
  2876 apply(rule Ord3)
       
  2877 apply(auto)
       
  2878 done
       
  2879 
       
  2880 section {* POSIX for some constructors *}
       
  2881 
       
  2882 lemma POSIX_SEQ1:
       
  2883   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
       
  2884   shows "POSIX v1 r1"
       
  2885 using assms
       
  2886 unfolding POSIX_def
       
  2887 apply(auto)
       
  2888 apply(drule_tac x="Seq v' v2" in spec)
       
  2889 apply(simp)
       
  2890 apply(erule impE)
       
  2891 apply(rule Prf.intros)
       
  2892 apply(simp)
       
  2893 apply(simp)
       
  2894 apply(erule ValOrd.cases)
       
  2895 apply(simp_all)
       
  2896 apply(clarify)
       
  2897 by (metis ValOrd_refl)
       
  2898 
       
  2899 lemma POSIX_SEQ2:
       
  2900   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" 
       
  2901   shows "POSIX v2 r2"
       
  2902 using assms
       
  2903 unfolding POSIX_def
       
  2904 apply(auto)
       
  2905 apply(drule_tac x="Seq v1 v'" in spec)
       
  2906 apply(simp)
       
  2907 apply(erule impE)
       
  2908 apply(rule Prf.intros)
       
  2909 apply(simp)
       
  2910 apply(simp)
       
  2911 apply(erule ValOrd.cases)
       
  2912 apply(simp_all)
       
  2913 done
       
  2914 
       
  2915 lemma POSIX_ALT2:
       
  2916   assumes "POSIX (Left v1) (ALT r1 r2)"
       
  2917   shows "POSIX v1 r1"
       
  2918 using assms
       
  2919 unfolding POSIX_def
       
  2920 apply(auto)
       
  2921 apply(erule Prf.cases)
       
  2922 apply(simp_all)[5]
       
  2923 apply(drule_tac x="Left v'" in spec)
       
  2924 apply(simp)
       
  2925 apply(drule mp)
       
  2926 apply(rule Prf.intros)
       
  2927 apply(auto)
       
  2928 apply(erule ValOrd.cases)
       
  2929 apply(simp_all)
       
  2930 done
       
  2931 
       
  2932 lemma POSIX_ALT1a:
       
  2933   assumes "POSIX (Right v2) (ALT r1 r2)"
       
  2934   shows "POSIX v2 r2"
       
  2935 using assms
       
  2936 unfolding POSIX_def
       
  2937 apply(auto)
       
  2938 apply(erule Prf.cases)
       
  2939 apply(simp_all)[5]
       
  2940 apply(drule_tac x="Right v'" in spec)
       
  2941 apply(simp)
       
  2942 apply(drule mp)
       
  2943 apply(rule Prf.intros)
       
  2944 apply(auto)
       
  2945 apply(erule ValOrd.cases)
       
  2946 apply(simp_all)
       
  2947 done
       
  2948 
       
  2949 lemma POSIX_ALT1b:
       
  2950   assumes "POSIX (Right v2) (ALT r1 r2)"
       
  2951   shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')"
       
  2952 using assms
       
  2953 apply(drule_tac POSIX_ALT1a)
       
  2954 unfolding POSIX_def
       
  2955 apply(auto)
       
  2956 done
       
  2957 
       
  2958 lemma POSIX_ALT_I1:
       
  2959   assumes "POSIX v1 r1" 
       
  2960   shows "POSIX (Left v1) (ALT r1 r2)"
       
  2961 using assms
       
  2962 unfolding POSIX_def
       
  2963 apply(auto)
       
  2964 apply (metis Prf.intros(2))
       
  2965 apply(rotate_tac 2)
       
  2966 apply(erule Prf.cases)
       
  2967 apply(simp_all)[5]
       
  2968 apply(auto)
       
  2969 apply(rule ValOrd.intros)
       
  2970 apply(auto)
       
  2971 apply(rule ValOrd.intros)
       
  2972 by simp
       
  2973 
       
  2974 lemma POSIX_ALT_I2:
       
  2975   assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
       
  2976   shows "POSIX (Right v2) (ALT r1 r2)"
       
  2977 using assms
       
  2978 unfolding POSIX_def
       
  2979 apply(auto)
       
  2980 apply (metis Prf.intros)
       
  2981 apply(rotate_tac 3)
       
  2982 apply(erule Prf.cases)
       
  2983 apply(simp_all)[5]
       
  2984 apply(auto)
       
  2985 apply(rule ValOrd.intros)
       
  2986 apply metis
       
  2987 done
       
  2988 
       
  2989 lemma mkeps_POSIX:
       
  2990   assumes "nullable r"
       
  2991   shows "POSIX (mkeps r) r"
       
  2992 using assms
       
  2993 apply(induct r)
       
  2994 apply(auto)[1]
       
  2995 apply(simp add: POSIX_def)
       
  2996 apply(auto)[1]
       
  2997 apply (metis Prf.intros(4))
       
  2998 apply(erule Prf.cases)
       
  2999 apply(simp_all)[5]
       
  3000 apply (metis ValOrd.intros)
       
  3001 apply(simp)
       
  3002 apply(auto)[1]
       
  3003 apply(simp add: POSIX_def)
       
  3004 apply(auto)[1]
       
  3005 apply (metis mkeps.simps(2) mkeps_nullable nullable.simps(5))
       
  3006 apply(rotate_tac 6)
       
  3007 apply(erule Prf.cases)
       
  3008 apply(simp_all)[5]
       
  3009 apply (simp add: mkeps_flat)
       
  3010 apply(case_tac "mkeps r1a = v1")
       
  3011 apply(simp)
       
  3012 apply (metis ValOrd.intros(1))
       
  3013 apply (rule ValOrd.intros(2))
       
  3014 apply metis
       
  3015 apply(simp)
       
  3016 (* ALT case *)
       
  3017 thm mkeps.simps
       
  3018 apply(simp)
       
  3019 apply(erule disjE)
       
  3020 apply(simp)
       
  3021 apply (metis POSIX_ALT_I1)
       
  3022 (* *)
       
  3023 apply(auto)[1]
       
  3024 thm  POSIX_ALT_I1
       
  3025 apply (metis POSIX_ALT_I1)
       
  3026 apply(simp (no_asm) add: POSIX_def)
       
  3027 apply(auto)[1]
       
  3028 apply(rule Prf.intros(3))
       
  3029 apply(simp only: POSIX_def)
       
  3030 apply(rotate_tac 4)
       
  3031 apply(erule Prf.cases)
       
  3032 apply(simp_all)[5]
       
  3033 thm mkeps_flat
       
  3034 apply(simp add: mkeps_flat)
       
  3035 apply(auto)[1]
       
  3036 thm Prf_flat_L nullable_correctness
       
  3037 apply (metis Prf_flat_L nullable_correctness)
       
  3038 apply(rule ValOrd.intros)
       
  3039 apply(subst (asm) POSIX_def)
       
  3040 apply(clarify)
       
  3041 apply(drule_tac x="v2" in spec)
       
  3042 by simp
       
  3043 
       
  3044 
       
  3045 
       
  3046 text {*
       
  3047   Injection value is related to r
       
  3048 *}
       
  3049 
       
  3050 
       
  3051 
       
  3052 text {*
       
  3053   The string behind the injection value is an added c
       
  3054 *}
       
  3055 
       
  3056 
       
  3057 lemma injval_inj: "inj_on (injval r c) {v. \<turnstile> v : der c r}"
       
  3058 apply(induct c r rule: der.induct)
       
  3059 unfolding inj_on_def
       
  3060 apply(auto)[1]
       
  3061 apply(erule Prf.cases)
       
  3062 apply(simp_all)[5]
       
  3063 apply(auto)[1]
       
  3064 apply(erule Prf.cases)
       
  3065 apply(simp_all)[5]
       
  3066 apply(auto)[1]
       
  3067 apply(erule Prf.cases)
       
  3068 apply(simp_all)[5]
       
  3069 apply(erule Prf.cases)
       
  3070 apply(simp_all)[5]
       
  3071 apply(erule Prf.cases)
       
  3072 apply(simp_all)[5]
       
  3073 apply(auto)[1]
       
  3074 apply(erule Prf.cases)
       
  3075 apply(simp_all)[5]
       
  3076 apply(erule Prf.cases)
       
  3077 apply(simp_all)[5]
       
  3078 apply(erule Prf.cases)
       
  3079 apply(simp_all)[5]
       
  3080 apply(auto)[1]
       
  3081 apply(erule Prf.cases)
       
  3082 apply(simp_all)[5]
       
  3083 apply(erule Prf.cases)
       
  3084 apply(simp_all)[5]
       
  3085 apply(clarify)
       
  3086 apply(erule Prf.cases)
       
  3087 apply(simp_all)[5]
       
  3088 apply(erule Prf.cases)
       
  3089 apply(simp_all)[5]
       
  3090 apply(clarify)
       
  3091 apply(erule Prf.cases)
       
  3092 apply(simp_all)[5]
       
  3093 apply(clarify)
       
  3094 apply (metis list.distinct(1) mkeps_flat v4)
       
  3095 apply(erule Prf.cases)
       
  3096 apply(simp_all)[5]
       
  3097 apply(clarify)
       
  3098 apply(rotate_tac 6)
       
  3099 apply(erule Prf.cases)
       
  3100 apply(simp_all)[5]
       
  3101 apply (metis list.distinct(1) mkeps_flat v4)
       
  3102 apply(erule Prf.cases)
       
  3103 apply(simp_all)[5]
       
  3104 apply(erule Prf.cases)
       
  3105 apply(simp_all)[5]
       
  3106 done
       
  3107 
       
  3108 lemma Values_nullable:
       
  3109   assumes "nullable r1"
       
  3110   shows "mkeps r1 \<in> Values r1 s"
       
  3111 using assms
       
  3112 apply(induct r1 arbitrary: s)
       
  3113 apply(simp_all)
       
  3114 apply(simp add: Values_recs)
       
  3115 apply(simp add: Values_recs)
       
  3116 apply(simp add: Values_recs)
       
  3117 apply(auto)[1]
       
  3118 done
       
  3119 
       
  3120 lemma Values_injval:
       
  3121   assumes "v \<in> Values (der c r) s"
       
  3122   shows "injval r c v \<in> Values r (c#s)"
       
  3123 using assms
       
  3124 apply(induct c r arbitrary: v s rule: der.induct)
       
  3125 apply(simp add: Values_recs)
       
  3126 apply(simp add: Values_recs)
       
  3127 apply(case_tac "c = c'")
       
  3128 apply(simp)
       
  3129 apply(simp add: Values_recs)
       
  3130 apply(simp add: prefix_def)
       
  3131 apply(simp)
       
  3132 apply(simp add: Values_recs)
       
  3133 apply(simp)
       
  3134 apply(simp add: Values_recs)
       
  3135 apply(auto)[1]
       
  3136 apply(case_tac "nullable r1")
       
  3137 apply(simp)
       
  3138 apply(simp add: Values_recs)
       
  3139 apply(auto)[1]
       
  3140 apply(simp add: rest_def)
       
  3141 apply(subst v4)
       
  3142 apply(simp add: Values_def)
       
  3143 apply(simp add: Values_def)
       
  3144 apply(rule Values_nullable)
       
  3145 apply(assumption)
       
  3146 apply(simp add: rest_def)
       
  3147 apply(subst mkeps_flat)
       
  3148 apply(assumption)
       
  3149 apply(simp)
       
  3150 apply(simp)
       
  3151 apply(simp add: Values_recs)
       
  3152 apply(auto)[1]
       
  3153 apply(simp add: rest_def)
       
  3154 apply(subst v4)
       
  3155 apply(simp add: Values_def)
       
  3156 apply(simp add: Values_def)
       
  3157 done
       
  3158 
       
  3159 lemma Values_projval:
       
  3160   assumes "v \<in> Values r (c#s)" "\<exists>s. flat v = c # s"
       
  3161   shows "projval r c v \<in> Values (der c r) s"
       
  3162 using assms
       
  3163 apply(induct r arbitrary: v s c rule: rexp.induct)
       
  3164 apply(simp add: Values_recs)
       
  3165 apply(simp add: Values_recs)
       
  3166 apply(case_tac "c = char")
       
  3167 apply(simp)
       
  3168 apply(simp add: Values_recs)
       
  3169 apply(simp)
       
  3170 apply(simp add: Values_recs)
       
  3171 apply(simp add: prefix_def)
       
  3172 apply(case_tac "nullable rexp1")
       
  3173 apply(simp)
       
  3174 apply(simp add: Values_recs)
       
  3175 apply(auto)[1]
       
  3176 apply(simp add: rest_def)
       
  3177 apply (metis hd_Cons_tl hd_append2 list.sel(1))
       
  3178 apply(simp add: rest_def)
       
  3179 apply(simp add: append_eq_Cons_conv)
       
  3180 apply(auto)[1]
       
  3181 apply(subst v4_proj2)
       
  3182 apply(simp add: Values_def)
       
  3183 apply(assumption)
       
  3184 apply(simp)
       
  3185 apply(simp)
       
  3186 apply(simp add: Values_recs)
       
  3187 apply(auto)[1]
       
  3188 apply(auto simp add: Values_def not_nullable_flat)[1]
       
  3189 apply(simp add: append_eq_Cons_conv)
       
  3190 apply(auto)[1]
       
  3191 apply(simp add: append_eq_Cons_conv)
       
  3192 apply(auto)[1]
       
  3193 apply(simp add: rest_def)
       
  3194 apply(subst v4_proj2)
       
  3195 apply(simp add: Values_def)
       
  3196 apply(assumption)
       
  3197 apply(simp)
       
  3198 apply(simp add: Values_recs)
       
  3199 apply(auto)[1]
       
  3200 done
       
  3201 
       
  3202 
       
  3203 definition "MValue v r s \<equiv> (v \<in> Values r s \<and> (\<forall>v' \<in> Values r s. v 2\<succ> v'))"
       
  3204 
       
  3205 lemma MValue_ALTE:
       
  3206   assumes "MValue v (ALT r1 r2) s"
       
  3207   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> 
       
  3208          (\<exists>vr. v = Right vr \<and> MValue vr r2 s \<and> (\<forall>vl \<in> Values r1 s. length (flat vl) < length (flat vr)))"
       
  3209 using assms
       
  3210 apply(simp add: MValue_def)
       
  3211 apply(simp add: Values_recs)
       
  3212 apply(auto)
       
  3213 apply(drule_tac x="Left x" in bspec)
       
  3214 apply(simp)
       
  3215 apply(erule ValOrd2.cases)
       
  3216 apply(simp_all)
       
  3217 apply(drule_tac x="Right vr" in bspec)
       
  3218 apply(simp)
       
  3219 apply(erule ValOrd2.cases)
       
  3220 apply(simp_all)
       
  3221 apply(drule_tac x="Right x" in bspec)
       
  3222 apply(simp)
       
  3223 apply(erule ValOrd2.cases)
       
  3224 apply(simp_all)
       
  3225 apply(drule_tac x="Left vl" in bspec)
       
  3226 apply(simp)
       
  3227 apply(erule ValOrd2.cases)
       
  3228 apply(simp_all)
       
  3229 done
       
  3230 
       
  3231 lemma MValue_ALTI1:
       
  3232   assumes "MValue vl r1 s"  "\<forall>vr \<in> Values r2 s. length (flat vr) \<le> length (flat vl)"
       
  3233   shows "MValue (Left vl) (ALT r1 r2) s"
       
  3234 using assms
       
  3235 apply(simp add: MValue_def)
       
  3236 apply(simp add: Values_recs)
       
  3237 apply(auto)
       
  3238 apply(rule ValOrd2.intros)
       
  3239 apply metis
       
  3240 apply(rule ValOrd2.intros)
       
  3241 apply metis
       
  3242 done
       
  3243 
       
  3244 lemma MValue_ALTI2:
       
  3245   assumes "MValue vr r2 s"  "\<forall>vl \<in> Values r1 s. length (flat vl) < length (flat vr)"
       
  3246   shows "MValue (Right vr) (ALT r1 r2) s"
       
  3247 using assms
       
  3248 apply(simp add: MValue_def)
       
  3249 apply(simp add: Values_recs)
       
  3250 apply(auto)
       
  3251 apply(rule ValOrd2.intros)
       
  3252 apply metis
       
  3253 apply(rule ValOrd2.intros)
       
  3254 apply metis
       
  3255 done
       
  3256 
       
  3257 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
       
  3258 by (metis list.sel(3))
       
  3259 
       
  3260 lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)"
       
  3261 by (metis)
       
  3262 
       
  3263 lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])"
       
  3264 by (metis Prf_flat_L nullable_correctness)
       
  3265 
       
  3266 
       
  3267 lemma LeftRight:
       
  3268   assumes "(Left v1) \<succ>(der c (ALT r1 r2)) (Right v2)"
       
  3269   and "\<turnstile> v1 : der c r1" "\<turnstile> v2 : der c r2" 
       
  3270   shows "(injval (ALT r1 r2) c (Left v1)) \<succ>(ALT r1 r2) (injval (ALT r1 r2) c (Right v2))"
       
  3271 using assms
       
  3272 apply(simp)
       
  3273 apply(erule ValOrd.cases)
       
  3274 apply(simp_all)[8]
       
  3275 apply(rule ValOrd.intros)
       
  3276 apply(clarify)
       
  3277 apply(subst v4)
       
  3278 apply(simp)
       
  3279 apply(subst v4)
       
  3280 apply(simp)
       
  3281 apply(simp)
       
  3282 done
       
  3283 
       
  3284 lemma RightLeft:
       
  3285   assumes "(Right v1) \<succ>(der c (ALT r1 r2)) (Left v2)"
       
  3286   and "\<turnstile> v1 : der c r2" "\<turnstile> v2 : der c r1" 
       
  3287   shows "(injval (ALT r1 r2) c (Right v1)) \<succ>(ALT r1 r2) (injval (ALT r1 r2) c (Left v2))"
       
  3288 using assms
       
  3289 apply(simp)
       
  3290 apply(erule ValOrd.cases)
       
  3291 apply(simp_all)[8]
       
  3292 apply(rule ValOrd.intros)
       
  3293 apply(clarify)
       
  3294 apply(subst v4)
       
  3295 apply(simp)
       
  3296 apply(subst v4)
       
  3297 apply(simp)
       
  3298 apply(simp)
       
  3299 done
       
  3300 
       
  3301 lemma h: 
       
  3302   assumes "nullable r1" "\<turnstile> v1 : der c r1"
       
  3303   shows "injval r1 c v1 \<succ>r1 mkeps r1"
       
  3304 using assms
       
  3305 apply(induct r1 arbitrary: v1 rule: der.induct)
       
  3306 apply(simp)
       
  3307 apply(simp)
       
  3308 apply(erule Prf.cases)
       
  3309 apply(simp_all)[5]
       
  3310 apply(simp)
       
  3311 apply(simp)
       
  3312 apply(erule Prf.cases)
       
  3313 apply(simp_all)[5]
       
  3314 apply(clarify)
       
  3315 apply(auto)[1]
       
  3316 apply (metis ValOrd.intros(6))
       
  3317 apply (metis ValOrd.intros(6))
       
  3318 apply (metis ValOrd.intros(3) le_add2 list.size(3) mkeps_flat monoid_add_class.add.right_neutral)
       
  3319 apply(auto)[1]
       
  3320 apply (metis ValOrd.intros(4) length_greater_0_conv list.distinct(1) list.size(3) mkeps_flat v4)
       
  3321 apply (metis ValOrd.intros(4) length_greater_0_conv list.distinct(1) list.size(3) mkeps_flat v4)
       
  3322 apply (metis ValOrd.intros(5))
       
  3323 apply(simp)
       
  3324 apply(erule Prf.cases)
       
  3325 apply(simp_all)[5]
       
  3326 apply(clarify)
       
  3327 apply(erule Prf.cases)
       
  3328 apply(simp_all)[5]
       
  3329 apply(clarify)
       
  3330 apply (metis ValOrd.intros(2) list.distinct(1) mkeps_flat v4)
       
  3331 apply(clarify)
       
  3332 by (metis ValOrd.intros(1))
       
  3333 
       
  3334 lemma LeftRightSeq:
       
  3335   assumes "(Left (Seq v1 v2)) \<succ>(der c (SEQ r1 r2)) (Right v3)"
       
  3336   and "nullable r1" "\<turnstile> v1 : der c r1"
       
  3337   shows "(injval (SEQ r1 r2) c (Seq v1 v2)) \<succ>(SEQ r1 r2) (injval (SEQ r1 r2) c (Right v2))"
       
  3338 using assms
       
  3339 apply(simp)
       
  3340 apply(erule ValOrd.cases)
       
  3341 apply(simp_all)[8]
       
  3342 apply(clarify)
       
  3343 apply(simp)
       
  3344 apply(rule ValOrd.intros(2))
       
  3345 prefer 2
       
  3346 apply (metis list.distinct(1) mkeps_flat v4)
       
  3347 by (metis h)
       
  3348 
       
  3349 lemma rr1: 
       
  3350   assumes "\<turnstile> v : r" "\<not>nullable r" 
       
  3351   shows "flat v \<noteq> []"
       
  3352 using assms
       
  3353 by (metis Prf_flat_L nullable_correctness)
       
  3354 
       
  3355 (* HERE *)
       
  3356 
       
  3357 lemma Prf_inj_test:
       
  3358   assumes "v1 \<succ>(der c r) v2" 
       
  3359           "v1 \<in> Values (der c r) s"
       
  3360           "v2 \<in> Values (der c r) s"
       
  3361           "injval r c v1 \<in> Values r (c#s)"
       
  3362           "injval r c v2 \<in> Values r (c#s)"
       
  3363   shows "(injval r c v1) 2\<succ>  (injval r c v2)"
       
  3364 using assms
       
  3365 apply(induct c r arbitrary: v1 v2 s rule: der.induct)
       
  3366 (* NULL case *)
       
  3367 apply(simp add: Values_recs)
       
  3368 (* EMPTY case *)
       
  3369 apply(simp add: Values_recs)
       
  3370 (* CHAR case *)
       
  3371 apply(case_tac "c = c'")
       
  3372 apply(simp)
       
  3373 apply(simp add: Values_recs)
       
  3374 apply (metis ValOrd2.intros(8))
       
  3375 apply(simp add: Values_recs)
       
  3376 (* ALT case *)
       
  3377 apply(simp)
       
  3378 apply(simp add: Values_recs)
       
  3379 apply(auto)[1]
       
  3380 apply(erule ValOrd.cases)
       
  3381 apply(simp_all)[8]
       
  3382 apply (metis ValOrd2.intros(6))
       
  3383 apply(erule ValOrd.cases)
       
  3384 apply(simp_all)[8]
       
  3385 apply(rule ValOrd2.intros)
       
  3386 apply(subst v4)
       
  3387 apply(simp add: Values_def)
       
  3388 apply(subst v4)
       
  3389 apply(simp add: Values_def)
       
  3390 apply(simp)
       
  3391 apply(erule ValOrd.cases)
       
  3392 apply(simp_all)[8]
       
  3393 apply(rule ValOrd2.intros)
       
  3394 apply(subst v4)
       
  3395 apply(simp add: Values_def)
       
  3396 apply(subst v4)
       
  3397 apply(simp add: Values_def)
       
  3398 apply(simp)
       
  3399 apply(erule ValOrd.cases)
       
  3400 apply(simp_all)[8]
       
  3401 apply (metis ValOrd2.intros(5))
       
  3402 (* SEQ case*)
       
  3403 apply(simp)
       
  3404 apply(case_tac "nullable r1")
       
  3405 apply(simp)
       
  3406 defer
       
  3407 apply(simp)
       
  3408 apply(simp add: Values_recs)
       
  3409 apply(auto)[1]
       
  3410 apply(erule ValOrd.cases)
       
  3411 apply(simp_all)[8]
       
  3412 apply(clarify)
       
  3413 apply(rule ValOrd2.intros)
       
  3414 apply(simp)
       
  3415 apply (metis Ord1)
       
  3416 apply(clarify)
       
  3417 apply(rule ValOrd2.intros)
       
  3418 apply(subgoal_tac "rest v1 (flat v1 @ flat v2) = flat v2")
       
  3419 apply(simp)
       
  3420 apply(subgoal_tac "rest (injval r1 c v1) (c # flat v1 @ flat v2) = flat v2")
       
  3421 apply(simp)
       
  3422 oops
       
  3423 
       
  3424 lemma Prf_inj_test:
       
  3425   assumes "v1 \<succ>(der c r) v2" 
       
  3426           "v1 \<in> Values (der c r) s"
       
  3427           "v2 \<in> Values (der c r) s"
       
  3428           "injval r c v1 \<in> Values r (c#s)"
       
  3429           "injval r c v2 \<in> Values r (c#s)"
       
  3430   shows "(injval r c v1) 2\<succ>  (injval r c v2)"
       
  3431 using assms
       
  3432 apply(induct c r arbitrary: v1 v2 s rule: der.induct)
       
  3433 (* NULL case *)
       
  3434 apply(simp add: Values_recs)
       
  3435 (* EMPTY case *)
       
  3436 apply(simp add: Values_recs)
       
  3437 (* CHAR case *)
       
  3438 apply(case_tac "c = c'")
       
  3439 apply(simp)
       
  3440 apply(simp add: Values_recs)
       
  3441 apply (metis ValOrd2.intros(8))
       
  3442 apply(simp add: Values_recs)
       
  3443 (* ALT case *)
       
  3444 apply(simp)
       
  3445 apply(simp add: Values_recs)
       
  3446 apply(auto)[1]
       
  3447 apply(erule ValOrd.cases)
       
  3448 apply(simp_all)[8]
       
  3449 apply (metis ValOrd2.intros(6))
       
  3450 apply(erule ValOrd.cases)
       
  3451 apply(simp_all)[8]
       
  3452 apply(rule ValOrd2.intros)
       
  3453 apply(subst v4)
       
  3454 apply(simp add: Values_def)
       
  3455 apply(subst v4)
       
  3456 apply(simp add: Values_def)
       
  3457 apply(simp)
       
  3458 apply(erule ValOrd.cases)
       
  3459 apply(simp_all)[8]
       
  3460 apply(rule ValOrd2.intros)
       
  3461 apply(subst v4)
       
  3462 apply(simp add: Values_def)
       
  3463 apply(subst v4)
       
  3464 apply(simp add: Values_def)
       
  3465 apply(simp)
       
  3466 apply(erule ValOrd.cases)
       
  3467 apply(simp_all)[8]
       
  3468 apply (metis ValOrd2.intros(5))
       
  3469 (* SEQ case*)
       
  3470 apply(simp)
       
  3471 apply(case_tac "nullable r1")
       
  3472 apply(simp)
       
  3473 defer
       
  3474 apply(simp)
       
  3475 apply(simp add: Values_recs)
       
  3476 apply(auto)[1]
       
  3477 apply(erule ValOrd.cases)
       
  3478 apply(simp_all)[8]
       
  3479 apply(clarify)
       
  3480 apply(rule ValOrd2.intros)
       
  3481 apply(simp)
       
  3482 apply (metis Ord1)
       
  3483 apply(clarify)
       
  3484 apply(rule ValOrd2.intros)
       
  3485 apply metis
       
  3486 using injval_inj
       
  3487 apply(simp add: Values_def inj_on_def)
       
  3488 apply metis
       
  3489 apply(simp add: Values_recs)
       
  3490 apply(auto)[1]
       
  3491 apply(erule ValOrd.cases)
       
  3492 apply(simp_all)[8]
       
  3493 apply(clarify)
       
  3494 apply(erule ValOrd.cases)
       
  3495 apply(simp_all)[8]
       
  3496 apply(clarify)
       
  3497 apply (metis Ord1 ValOrd2.intros(1))
       
  3498 apply(clarify)
       
  3499 apply(rule ValOrd2.intros(2))
       
  3500 apply metis
       
  3501 using injval_inj
       
  3502 apply(simp add: Values_def inj_on_def)
       
  3503 apply metis
       
  3504 apply(erule ValOrd.cases)
       
  3505 apply(simp_all)[8]
       
  3506 apply(rule ValOrd2.intros(2))
       
  3507 thm h
       
  3508 apply(rule Ord1)
       
  3509 apply(rule h)
       
  3510 apply(simp)
       
  3511 apply(simp add: Values_def)
       
  3512 apply(simp add: Values_def)
       
  3513 apply (metis list.distinct(1) mkeps_flat v4)
       
  3514 apply(erule ValOrd.cases)
       
  3515 apply(simp_all)[8]
       
  3516 apply(clarify)
       
  3517 apply(simp add: Values_def)
       
  3518 defer
       
  3519 apply(erule ValOrd.cases)
       
  3520 apply(simp_all)[8]
       
  3521 apply(clarify)
       
  3522 apply(rule ValOrd2.intros(1))
       
  3523 apply(rotate_tac 1)
       
  3524 apply(drule_tac x="v2" in meta_spec)
       
  3525 apply(rotate_tac 8)
       
  3526 apply(drule_tac x="v2'" in meta_spec)
       
  3527 apply(rotate_tac 8)
       
  3528 oops
       
  3529 
       
  3530 lemma POSIX_der:
       
  3531   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
       
  3532   shows "POSIX (injval r c v) r"
       
  3533 using assms
       
  3534 unfolding POSIX_def
       
  3535 apply(auto)
       
  3536 thm v3
       
  3537 apply (erule v3)
       
  3538 thm v4
       
  3539 apply(subst (asm) v4)
       
  3540 apply(assumption)
       
  3541 apply(drule_tac x="projval r c v'" in spec)
       
  3542 apply(drule mp)
       
  3543 apply(rule conjI)
       
  3544 thm v3_proj
       
  3545 apply(rule v3_proj)
       
  3546 apply(simp)
       
  3547 apply(rule_tac x="flat v" in exI)
       
  3548 apply(simp)
       
  3549 thm t
       
  3550 apply(rule_tac c="c" in  t)
       
  3551 apply(simp)
       
  3552 thm v4_proj
       
  3553 apply(subst v4_proj)
       
  3554 apply(simp)
       
  3555 apply(rule_tac x="flat v" in exI)
       
  3556 apply(simp)
       
  3557 apply(simp)
       
  3558 oops
       
  3559 
       
  3560 lemma POSIX_der:
       
  3561   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
       
  3562   shows "POSIX (injval r c v) r"
       
  3563 using assms
       
  3564 apply(induct c r arbitrary: v rule: der.induct)
       
  3565 (* null case*)
       
  3566 apply(simp add: POSIX_def)
       
  3567 apply(auto)[1]
       
  3568 apply(erule Prf.cases)
       
  3569 apply(simp_all)[5]
       
  3570 apply(erule Prf.cases)
       
  3571 apply(simp_all)[5]
       
  3572 (* empty case *)
       
  3573 apply(simp add: POSIX_def)
       
  3574 apply(auto)[1]
       
  3575 apply(erule Prf.cases)
       
  3576 apply(simp_all)[5]
       
  3577 apply(erule Prf.cases)
       
  3578 apply(simp_all)[5]
       
  3579 (* char case *)
       
  3580 apply(simp add: POSIX_def)
       
  3581 apply(case_tac "c = c'")
       
  3582 apply(auto)[1]
       
  3583 apply(erule Prf.cases)
       
  3584 apply(simp_all)[5]
       
  3585 apply (metis Prf.intros(5))
       
  3586 apply(erule Prf.cases)
       
  3587 apply(simp_all)[5]
       
  3588 apply(erule Prf.cases)
       
  3589 apply(simp_all)[5]
       
  3590 apply (metis ValOrd.intros(8))
       
  3591 apply(auto)[1]
       
  3592 apply(erule Prf.cases)
       
  3593 apply(simp_all)[5]
       
  3594 apply(erule Prf.cases)
       
  3595 apply(simp_all)[5]
       
  3596 (* alt case *)
       
  3597 apply(erule Prf.cases)
       
  3598 apply(simp_all)[5]
       
  3599 apply(clarify)
       
  3600 apply(simp (no_asm) add: POSIX_def)
       
  3601 apply(auto)[1]
       
  3602 apply (metis Prf.intros(2) v3)
       
  3603 apply(rotate_tac 4)
       
  3604 apply(erule Prf.cases)
       
  3605 apply(simp_all)[5]
       
  3606 apply (metis POSIX_ALT2 POSIX_def ValOrd.intros(6))
       
  3607 apply (metis ValOrd.intros(3) order_refl)
       
  3608 apply(simp (no_asm) add: POSIX_def)
       
  3609 apply(auto)[1]
       
  3610 apply (metis Prf.intros(3) v3)
       
  3611 apply(rotate_tac 4)
       
  3612 apply(erule Prf.cases)
       
  3613 apply(simp_all)[5]
       
  3614 defer
       
  3615 apply (metis POSIX_ALT1a POSIX_def ValOrd.intros(5))
       
  3616 prefer 2
       
  3617 apply(subst (asm) (5) POSIX_def)
       
  3618 apply(auto)[1]
       
  3619 apply(rotate_tac 5)
       
  3620 apply(erule Prf.cases)
       
  3621 apply(simp_all)[5]
       
  3622 apply(rule ValOrd.intros)
       
  3623 apply(subst (asm) v4)
       
  3624 apply(simp)
       
  3625 apply(drule_tac x="Left (projval r1a c v1)" in spec)
       
  3626 apply(clarify)
       
  3627 apply(drule mp)
       
  3628 apply(rule conjI)
       
  3629 apply (metis Prf.intros(2) v3_proj)
       
  3630 apply(simp)
       
  3631 apply (metis v4_proj2)
       
  3632 apply(erule ValOrd.cases)
       
  3633 apply(simp_all)[8]
       
  3634 apply (metis less_not_refl v4_proj2)
       
  3635 (* seq case *)
       
  3636 apply(case_tac "nullable r1")
       
  3637 defer
       
  3638 apply(simp add: POSIX_def)
       
  3639 apply(auto)[1]
       
  3640 apply(erule Prf.cases)
       
  3641 apply(simp_all)[5]
       
  3642 apply (metis Prf.intros(1) v3)
       
  3643 apply(erule Prf.cases)
       
  3644 apply(simp_all)[5]
       
  3645 apply(erule Prf.cases)
       
  3646 apply(simp_all)[5]
       
  3647 apply(clarify)
       
  3648 apply(subst (asm) (3) v4)
       
  3649 apply(simp)
       
  3650 apply(simp)
       
  3651 apply(subgoal_tac "flat v1a \<noteq> []")
       
  3652 prefer 2
       
  3653 apply (metis Prf_flat_L nullable_correctness)
       
  3654 apply(subgoal_tac "\<exists>s. flat v1a = c # s")
       
  3655 prefer 2
       
  3656 apply (metis append_eq_Cons_conv)
       
  3657 apply(auto)[1]
       
  3658 oops
       
  3659 
       
  3660 
       
  3661 lemma POSIX_ex: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r"
       
  3662 apply(induct r arbitrary: v)
       
  3663 apply(erule Prf.cases)
       
  3664 apply(simp_all)[5]
       
  3665 apply(erule Prf.cases)
       
  3666 apply(simp_all)[5]
       
  3667 apply(rule_tac x="Void" in exI)
       
  3668 apply(simp add: POSIX_def)
       
  3669 apply(auto)[1]
       
  3670 apply (metis Prf.intros(4))
       
  3671 apply(erule Prf.cases)
       
  3672 apply(simp_all)[5]
       
  3673 apply (metis ValOrd.intros(7))
       
  3674 apply(erule Prf.cases)
       
  3675 apply(simp_all)[5]
       
  3676 apply(rule_tac x="Char c" in exI)
       
  3677 apply(simp add: POSIX_def)
       
  3678 apply(auto)[1]
       
  3679 apply (metis Prf.intros(5))
       
  3680 apply(erule Prf.cases)
       
  3681 apply(simp_all)[5]
       
  3682 apply (metis ValOrd.intros(8))
       
  3683 apply(erule Prf.cases)
       
  3684 apply(simp_all)[5]
       
  3685 apply(auto)[1]
       
  3686 apply(drule_tac x="v1" in meta_spec)
       
  3687 apply(drule_tac x="v2" in meta_spec)
       
  3688 apply(auto)[1]
       
  3689 defer
       
  3690 apply(erule Prf.cases)
       
  3691 apply(simp_all)[5]
       
  3692 apply(auto)[1]
       
  3693 apply (metis POSIX_ALT_I1)
       
  3694 apply (metis POSIX_ALT_I1 POSIX_ALT_I2)
       
  3695 apply(case_tac "nullable r1a")
       
  3696 apply(rule_tac x="Seq (mkeps r1a) va" in exI)
       
  3697 apply(auto simp add: POSIX_def)[1]
       
  3698 apply (metis Prf.intros(1) mkeps_nullable)
       
  3699 apply(simp add: mkeps_flat)
       
  3700 apply(rotate_tac 7)
       
  3701 apply(erule Prf.cases)
       
  3702 apply(simp_all)[5]
       
  3703 apply(case_tac "mkeps r1 = v1a")
       
  3704 apply(simp)
       
  3705 apply (rule ValOrd.intros(1))
       
  3706 apply (metis append_Nil mkeps_flat)
       
  3707 apply (rule ValOrd.intros(2))
       
  3708 apply(drule mkeps_POSIX)
       
  3709 apply(simp add: POSIX_def)
       
  3710 oops
       
  3711 
       
  3712 lemma POSIX_ex2: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r \<and> \<turnstile> v : r"
       
  3713 apply(induct r arbitrary: v)
       
  3714 apply(erule Prf.cases)
       
  3715 apply(simp_all)[5]
       
  3716 apply(erule Prf.cases)
       
  3717 apply(simp_all)[5]
       
  3718 apply(rule_tac x="Void" in exI)
       
  3719 apply(simp add: POSIX_def)
       
  3720 apply(auto)[1]
       
  3721 oops
       
  3722 
       
  3723 lemma POSIX_ALT_cases:
       
  3724   assumes "\<turnstile> v : (ALT r1 r2)" "POSIX v (ALT r1 r2)"
       
  3725   shows "(\<exists>v1. v = Left v1 \<and> POSIX v1 r1) \<or> (\<exists>v2. v = Right v2 \<and> POSIX v2 r2)"
       
  3726 using assms
       
  3727 apply(erule_tac Prf.cases)
       
  3728 apply(simp_all)
       
  3729 unfolding POSIX_def
       
  3730 apply(auto)
       
  3731 apply (metis POSIX_ALT2 POSIX_def assms(2))
       
  3732 by (metis POSIX_ALT1b assms(2))
       
  3733 
       
  3734 lemma POSIX_ALT_cases2:
       
  3735   assumes "POSIX v (ALT r1 r2)" "\<turnstile> v : (ALT r1 r2)" 
       
  3736   shows "(\<exists>v1. v = Left v1 \<and> POSIX v1 r1) \<or> (\<exists>v2. v = Right v2 \<and> POSIX v2 r2)"
       
  3737 using assms POSIX_ALT_cases by auto
       
  3738 
       
  3739 lemma Prf_flat_empty:
       
  3740   assumes "\<turnstile> v : r" "flat v = []"
       
  3741   shows "nullable r"
       
  3742 using assms
       
  3743 apply(induct)
       
  3744 apply(auto)
       
  3745 done
       
  3746 
       
  3747 lemma POSIX_proj:
       
  3748   assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
       
  3749   shows "POSIX (projval r c v) (der c r)"
       
  3750 using assms
       
  3751 apply(induct r c v arbitrary: rule: projval.induct)
       
  3752 defer
       
  3753 defer
       
  3754 defer
       
  3755 defer
       
  3756 apply(erule Prf.cases)
       
  3757 apply(simp_all)[5]
       
  3758 apply(erule Prf.cases)
       
  3759 apply(simp_all)[5]
       
  3760 apply(erule Prf.cases)
       
  3761 apply(simp_all)[5]
       
  3762 apply(erule Prf.cases)
       
  3763 apply(simp_all)[5]
       
  3764 apply(erule Prf.cases)
       
  3765 apply(simp_all)[5]
       
  3766 apply(erule Prf.cases)
       
  3767 apply(simp_all)[5]
       
  3768 apply(erule Prf.cases)
       
  3769 apply(simp_all)[5]
       
  3770 apply(erule Prf.cases)
       
  3771 apply(simp_all)[5]
       
  3772 apply(erule Prf.cases)
       
  3773 apply(simp_all)[5]
       
  3774 apply(erule Prf.cases)
       
  3775 apply(simp_all)[5]
       
  3776 apply(simp add: POSIX_def)
       
  3777 apply(auto)[1]
       
  3778 apply(erule Prf.cases)
       
  3779 apply(simp_all)[5]
       
  3780 oops
       
  3781 
       
  3782 lemma POSIX_proj:
       
  3783   assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
       
  3784   shows "POSIX (projval r c v) (der c r)"
       
  3785 using assms
       
  3786 apply(induct r arbitrary: c v rule: rexp.induct)
       
  3787 apply(erule Prf.cases)
       
  3788 apply(simp_all)[5]
       
  3789 apply(erule Prf.cases)
       
  3790 apply(simp_all)[5]
       
  3791 apply(erule Prf.cases)
       
  3792 apply(simp_all)[5]
       
  3793 apply(simp add: POSIX_def)
       
  3794 apply(auto)[1]
       
  3795 apply(erule Prf.cases)
       
  3796 apply(simp_all)[5]
       
  3797 oops
       
  3798 
       
  3799 lemma POSIX_proj:
       
  3800   assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
       
  3801   shows "POSIX (projval r c v) (der c r)"
       
  3802 using assms
       
  3803 apply(induct r c v arbitrary: rule: projval.induct)
       
  3804 defer
       
  3805 defer
       
  3806 defer
       
  3807 defer
       
  3808 apply(erule Prf.cases)
       
  3809 apply(simp_all)[5]
       
  3810 apply(erule Prf.cases)
       
  3811 apply(simp_all)[5]
       
  3812 apply(erule Prf.cases)
       
  3813 apply(simp_all)[5]
       
  3814 apply(erule Prf.cases)
       
  3815 apply(simp_all)[5]
       
  3816 apply(erule Prf.cases)
       
  3817 apply(simp_all)[5]
       
  3818 apply(erule Prf.cases)
       
  3819 apply(simp_all)[5]
       
  3820 apply(erule Prf.cases)
       
  3821 apply(simp_all)[5]
       
  3822 apply(erule Prf.cases)
       
  3823 apply(simp_all)[5]
       
  3824 apply(erule Prf.cases)
       
  3825 apply(simp_all)[5]
       
  3826 apply(erule Prf.cases)
       
  3827 apply(simp_all)[5]
       
  3828 apply(simp add: POSIX_def)
       
  3829 apply(auto)[1]
       
  3830 apply(erule Prf.cases)
       
  3831 apply(simp_all)[5]
       
  3832 oops
       
  3833 
       
  3834 lemma Prf_inj:
       
  3835   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" "flat v1 = flat v2"
       
  3836   shows "(injval r c v1) \<succ>r (injval r c v2)"
       
  3837 using assms
       
  3838 apply(induct arbitrary: v1 v2 rule: der.induct)
       
  3839 (* NULL case *)
       
  3840 apply(simp)
       
  3841 apply(erule ValOrd.cases)
       
  3842 apply(simp_all)[8]
       
  3843 (* EMPTY case *)
       
  3844 apply(erule ValOrd.cases)
       
  3845 apply(simp_all)[8]
       
  3846 (* CHAR case *)
       
  3847 apply(case_tac "c = c'")
       
  3848 apply(simp)
       
  3849 apply(erule ValOrd.cases)
       
  3850 apply(simp_all)[8]
       
  3851 apply(rule ValOrd.intros)
       
  3852 apply(simp)
       
  3853 apply(erule ValOrd.cases)
       
  3854 apply(simp_all)[8]
       
  3855 (* ALT case *)
       
  3856 apply(simp)
       
  3857 apply(erule ValOrd.cases)
       
  3858 apply(simp_all)[8]
       
  3859 apply(rule ValOrd.intros)
       
  3860 apply(subst v4)
       
  3861 apply(clarify)
       
  3862 apply(rotate_tac 3)
       
  3863 apply(erule Prf.cases)
       
  3864 apply(simp_all)[5]
       
  3865 apply(subst v4)
       
  3866 apply(clarify)
       
  3867 apply(rotate_tac 2)
       
  3868 apply(erule Prf.cases)
       
  3869 apply(simp_all)[5]
       
  3870 apply(simp)
       
  3871 apply(rule ValOrd.intros)
       
  3872 apply(clarify)
       
  3873 apply(rotate_tac 3)
       
  3874 apply(erule Prf.cases)
       
  3875 apply(simp_all)[5]
       
  3876 apply(clarify)
       
  3877 apply(erule Prf.cases)
       
  3878 apply(simp_all)[5]
       
  3879 apply(rule ValOrd.intros)
       
  3880 apply(clarify)
       
  3881 apply(erule Prf.cases)
       
  3882 apply(simp_all)[5]
       
  3883 apply(erule Prf.cases)
       
  3884 apply(simp_all)[5]
       
  3885 (* SEQ case*)
       
  3886 apply(simp)
       
  3887 apply(case_tac "nullable r1")
       
  3888 defer
       
  3889 apply(simp)
       
  3890 apply(erule ValOrd.cases)
       
  3891 apply(simp_all)[8]
       
  3892 apply(clarify)
       
  3893 apply(erule Prf.cases)
       
  3894 apply(simp_all)[5]
       
  3895 apply(erule Prf.cases)
       
  3896 apply(simp_all)[5]
       
  3897 apply(clarify)
       
  3898 apply(rule ValOrd.intros)
       
  3899 apply(simp)
       
  3900 oops
       
  3901 
       
  3902 
       
  3903 text {*
       
  3904   Injection followed by projection is the identity.
       
  3905 *}
       
  3906 
       
  3907 lemma proj_inj_id:
       
  3908   assumes "\<turnstile> v : der c r" 
       
  3909   shows "projval r c (injval r c v) = v"
       
  3910 using assms
       
  3911 apply(induct r arbitrary: c v rule: rexp.induct)
       
  3912 apply(simp)
       
  3913 apply(erule Prf.cases)
       
  3914 apply(simp_all)[5]
       
  3915 apply(simp)
       
  3916 apply(erule Prf.cases)
       
  3917 apply(simp_all)[5]
       
  3918 apply(simp)
       
  3919 apply(case_tac "c = char")
       
  3920 apply(simp)
       
  3921 apply(erule Prf.cases)
       
  3922 apply(simp_all)[5]
       
  3923 apply(simp)
       
  3924 apply(erule Prf.cases)
       
  3925 apply(simp_all)[5]
       
  3926 defer
       
  3927 apply(simp)
       
  3928 apply(erule Prf.cases)
       
  3929 apply(simp_all)[5]
       
  3930 apply(simp)
       
  3931 apply(case_tac "nullable rexp1")
       
  3932 apply(simp)
       
  3933 apply(erule Prf.cases)
       
  3934 apply(simp_all)[5]
       
  3935 apply(auto)[1]
       
  3936 apply(erule Prf.cases)
       
  3937 apply(simp_all)[5]
       
  3938 apply(auto)[1]
       
  3939 apply (metis list.distinct(1) v4)
       
  3940 apply(auto)[1]
       
  3941 apply (metis mkeps_flat)
       
  3942 apply(auto)
       
  3943 apply(erule Prf.cases)
       
  3944 apply(simp_all)[5]
       
  3945 apply(auto)[1]
       
  3946 apply(simp add: v4)
       
  3947 done
       
  3948 
       
  3949 text {* 
       
  3950 
       
  3951   HERE: Crucial lemma that does not go through in the sequence case. 
       
  3952 
       
  3953 *}
       
  3954 lemma v5:
       
  3955   assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
       
  3956   shows "POSIX (injval r c v) r"
       
  3957 using assms
       
  3958 apply(induct arbitrary: v rule: der.induct)
       
  3959 (* NULL case *)
       
  3960 apply(simp)
       
  3961 apply(erule Prf.cases)
       
  3962 apply(simp_all)[5]
       
  3963 (* EMPTY case *)
       
  3964 apply(simp)
       
  3965 apply(erule Prf.cases)
       
  3966 apply(simp_all)[5]
       
  3967 (* CHAR case *)
       
  3968 apply(simp)
       
  3969 apply(case_tac "c = c'")
       
  3970 apply(auto simp add: POSIX_def)[1]
       
  3971 apply(erule Prf.cases)
       
  3972 apply(simp_all)[5]
       
  3973 oops
       
  3974 *)
       
  3975 
       
  3976 
       
  3977 end