3   imports Main 

     3   imports Main "~~/src/HOL/Library/Sublist"

   175 apply(induct s arbitrary: r)

   174 by (induct s arbitrary: r)

   176 apply(simp_all add: Ders_def der_correctness Der_def)

   175    (simp_all add: Ders_def der_correctness Der_def)

   177 done

   176 

   204 apply(induct s arbitrary: r1 r2)

   205 by (induct s arbitrary: r1 r2)(simp_all)

   205 apply(simp_all)

   206 

   206 done

   233  "flat (Stars vs) = concat (map flat vs)"

   236  "flat (Stars vs) = flats vs"

   276   shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"

   279   shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"

   316   then obtain vs where "concat (map flat vs) = s" "\<forall>v\<in>set vs. \<turnstile> v : r"

   319   then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<turnstile> v : r"

   334 section {* CPT and CPTpre *}

   337 

   335 

   338 section {* Canonical Values *}

   366 apply(auto intro: CPrf.intros elim: Prf.cases)

   361 apply(auto intro: CPrf.intros)

   367 done

   362 done

   368 

   363 

   369 definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set"

   364 

   370 where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}"

   365 section {* Sets of Lexical and Canonical Values *}

   366 

   367 definition 

   368   LV :: "rexp \<Rightarrow> string \<Rightarrow> val set"

   369 where "LV r s \<equiv> {v.  \<turnstile> v : r \<and> flat v = s}"

   373   "CPT r s = {v. flat v = s \<and> \<Turnstile> v : r}"

   372   CV :: "rexp \<Rightarrow> string \<Rightarrow> val set"

   374 

   373 where  "CV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}"

   375 definition

   374 

   376   "CPTpre r s = {v. \<exists>s'. flat v @ s' = s \<and> \<Turnstile> v : r}"

   375 lemma LV_CV_subset:

   377 

   376   shows "CV r s \<subseteq> LV r s"

   378 lemma CPT_CPTpre_subset:

   377 unfolding CV_def LV_def by(auto simp add: Prf_CPrf)

   379   shows "CPT r s \<subseteq> CPTpre r s"

   378 

   380 by(auto simp add: CPT_def CPTpre_def)

   379 abbreviation

   381 

   380   "Prefixes s \<equiv> {s'. prefixeq s' s}"

   382 lemma CPT_simps:

   381 

   383   shows "CPT ZERO s = {}"

   382 abbreviation

   384   and   "CPT ONE s = (if s = [] then {Void} else {})"

   383   "Suffixes s \<equiv> {s'. suffixeq s' s}"

   385   and   "CPT (CHAR c) s = (if s = [c] then {Char c} else {})"

   384 

   386   and   "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s"

   385 abbreviation

   387   and   "CPT (SEQ r1 r2) s = 

   386   "SSuffixes s \<equiv> {s'. suffix s' s}"

   388           {Seq v1 v2 | v1 v2. flat v1 @ flat v2 = s \<and> v1 \<in> CPT r1 (flat v1) \<and> v2 \<in> CPT r2 (flat v2)}"

   387 

   389   and   "CPT (STAR r) s = 

   388 lemma Suffixes_cons [simp]:

   390           Stars ` {vs. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. v \<in> CPT r (flat v) \<and> flat v \<noteq> [])}"

   389   shows "Suffixes (c # s) = Suffixes s \<union> {c # s}"

   391 apply -

   390 by (auto simp add: suffixeq_def Cons_eq_append_conv)

   392 apply(auto simp add: CPT_def intro: CPrf.intros)[1]

   391 

   392 lemma CV_simps:

   393   shows "CV ZERO s = {}"

   394   and   "CV ONE s = (if s = [] then {Void} else {})"

   395   and   "CV (CHAR c) s = (if s = [c] then {Char c} else {})"

   396   and   "CV (ALT r1 r2) s = Left ` CV r1 s \<union> Right ` CV r2 s"

   397 unfolding CV_def

   398 by (auto intro: CPrf.intros elim: CPrf.cases)

   399 

   400 lemma finite_Suffixes: 

   401   shows "finite (Suffixes s)"

   402 by (induct s) (simp_all)

   403 

   404 lemma finite_SSuffixes: 

   405   shows "finite (SSuffixes s)"

   406 proof -

   407   have "SSuffixes s \<subseteq> Suffixes s"

   408    unfolding suffix_def suffixeq_def by auto

   409   then show "finite (SSuffixes s)"

   410    using finite_Suffixes finite_subset by blast

   411 qed

   412 

   413 lemma finite_Prefixes: 

   414   shows "finite (Prefixes s)"

   415 proof -

   416   have "finite (Suffixes (rev s))" 

   417     by (rule finite_Suffixes)

   418   then have "finite (rev ` Suffixes (rev s))" by simp

   419   moreover

   420   have "rev ` (Suffixes (rev s)) = Prefixes s"

   421   unfolding suffixeq_def prefixeq_def image_def

   422    by (auto)(metis rev_append rev_rev_ident)+

   423   ultimately show "finite (Prefixes s)" by simp

   424 qed

   425 

   426 lemma CV_SEQ_subset:

   427   "CV (SEQ r1 r2) s \<subseteq> (\<lambda>(v1,v2). Seq v1 v2) ` ((\<Union>s' \<in> Prefixes s. CV r1 s') \<times> (\<Union>s' \<in> Suffixes s. CV r2 s'))"

   428 unfolding image_def CV_def prefixeq_def suffixeq_def

   429 by (auto elim: CPrf.cases)

   430 

   431 lemma CV_STAR_subset:

   432   "CV (STAR r) s \<subseteq> {Stars []} \<union>

   433       (\<lambda>(v,vs). Stars (v#vs)) ` ((\<Union>s' \<in> Prefixes s. CV r s') \<times> (\<Union>s2 \<in> SSuffixes s. Stars -` (CV (STAR r) s2)))"

   434 unfolding image_def CV_def prefixeq_def suffix_def

   435 apply(auto)

   394 apply(simp_all)[6]

   437 apply(auto)

   395 apply(auto simp add: CPT_def intro: CPrf.intros)[1]

   438 apply(case_tac vs)

   396 apply(erule CPrf.cases)

   439 apply(auto intro: CPrf.intros)

   397 apply(simp_all)[6]

   440 done

   398 apply(erule CPrf.cases)

   441 

   399 apply(simp_all)[6]

   442 

   400 apply(auto simp add: CPT_def intro: CPrf.intros)[1]

   443 lemma CV_STAR_finite:

   401 apply(erule CPrf.cases)

   444   assumes "\<forall>s. finite (CV r s)"

   402 apply(simp_all)[6]

   445   shows "finite (CV (STAR r) s)"

   403 apply(erule CPrf.cases)

   446 proof(induct s rule: length_induct)

   404 apply(simp_all)[6]

   447   fix s::"char list"

   405 apply(auto simp add: CPT_def intro: CPrf.intros)[1]

   448   assume "\<forall>s'. length s' < length s \<longrightarrow> finite (CV (STAR r) s')"

   406 apply(erule CPrf.cases)

   449   then have IH: "\<forall>s' \<in> SSuffixes s. finite (CV (STAR r) s')"

   407 apply(simp_all)[6]

   450     by (auto simp add: suffix_def) 

   408 apply(auto simp add: CPT_def intro: CPrf.intros)[1]

   451   def f \<equiv> "\<lambda>(v, vs). Stars (v # vs)"

   409 apply(erule CPrf.cases)

   452   def S1 \<equiv> "\<Union>s' \<in> Prefixes s. CV r s'"

   410 apply(simp_all)[6]

   453   def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (CV (STAR r) s2)"

   411 (* STAR case *)

   454   have "finite S1" using assms

   412 apply(auto simp add: CPT_def intro: CPrf.intros)[1]

   455     unfolding S1_def by (simp_all add: finite_Prefixes)

   413 apply(erule CPrf.cases)

   456   moreover 

   414 apply(simp_all)[6]

   457   with IH have "finite S2" unfolding S2_def

   415 done

   458     by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI)

   459   ultimately 

   460   have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp

   461   moreover 

   462   have "CV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" unfolding S1_def S2_def f_def

   463      by (rule CV_STAR_subset)

   464   ultimately

   465   show "finite (CV (STAR r) s)" by (simp add: finite_subset)

   466 qed  

   467     

   468 

   469 lemma CV_finite:

   470   shows "finite (CV r s)"

   471 proof(induct r arbitrary: s)

   472   case (ZERO s) 

   473   show "finite (CV ZERO s)" by (simp add: CV_simps)

   474 next

   475   case (ONE s)

   476   show "finite (CV ONE s)" by (simp add: CV_simps)

   477 next

   478   case (CHAR c s)

   479   show "finite (CV (CHAR c) s)" by (simp add: CV_simps)

   480 next 

   481   case (ALT r1 r2 s)

   482   then show "finite (CV (ALT r1 r2) s)" by (simp add: CV_simps)

   483 next 

   484   case (SEQ r1 r2 s)

   485   def f \<equiv> "\<lambda>(v1, v2). Seq v1 v2"

   486   def S1 \<equiv> "\<Union>s' \<in> Prefixes s. CV r1 s'"

   487   def S2 \<equiv> "\<Union>s' \<in> Suffixes s. CV r2 s'"

   488   have IHs: "\<And>s. finite (CV r1 s)" "\<And>s. finite (CV r2 s)" by fact+

   489   then have "finite S1" "finite S2" unfolding S1_def S2_def

   490     by (simp_all add: finite_Prefixes finite_Suffixes)

   491   moreover

   492   have "CV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)"

   493     unfolding f_def S1_def S2_def by (auto simp add: CV_SEQ_subset)

   494   ultimately 

   495   show "finite (CV (SEQ r1 r2) s)"

   496     by (simp add: finite_subset)

   497 next

   498   case (STAR r s)

   499   then show "finite (CV (STAR r) s)" by (simp add: CV_STAR_finite)

   500 qed

   534 lemma Posix_CPT:

   619 lemma Posix_CV:

   536   shows "v \<in> CPT r s"

   621   shows "v \<in> CV r s"

   539 apply(auto simp add: CPT_def intro: CPrf.intros elim: CPrf.cases)

   624 apply(auto simp add: CV_def intro: CPrf.intros elim: CPrf.cases)

   735   shows "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" 

   634   shows "(Stars vs) \<in> CV (STAR r) (flat (Stars vs))" 

   738 apply(auto simp add: CPT_def)

   637 apply(auto simp add: CV_def)

   743 by (metis (no_types, lifting) CPT_def Posix_CPT mem_Collect_eq)

   642 by (metis (no_types, lifting) CV_def Posix_CV mem_Collect_eq)