Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/Lexer.thy
changeset 265 d36be1e356c0
parent 264 e2828c4a1e23
child 266 fff2e1b40dfc
equal deleted inserted replaced
264:e2828c4a1e23 265:d36be1e356c0 
    77   shows "A\<star> = {[]} \<union> A ;; A\<star>"
 
    77   shows "A\<star> = {[]} \<union> A ;; A\<star>"
 
    78 unfolding Sequ_def
 
    78 unfolding Sequ_def
 
    79 by (auto) (metis Star.simps)
 
    79 by (auto) (metis Star.simps)
 
    80 
    80 
    81 lemma Star_decomp: 
    81 lemma Star_decomp: 
    82   assumes a: "c # x \<in> A\<star>" 
    82   assumes "c # x \<in> A\<star>" 
    83   shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
 
    83   shows "\<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A\<star>"
 
    84 using a
 
    84 using assms
 
    85 by (induct x\<equiv>"c # x" rule: Star.induct) 
    85 by (induct x\<equiv>"c # x" rule: Star.induct) 
    86    (auto simp add: append_eq_Cons_conv)
 
    86    (auto simp add: append_eq_Cons_conv)
 
    87 
    87 
    88 lemma Star_Der_Sequ: 
    88 lemma Star_Der_Sequ: 
    89   shows "Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>"
 
    89   shows "Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>"
 
    90 unfolding Der_def
 
    90 unfolding Der_def
 
    91 by(auto simp add: Der_def Sequ_def Star_decomp)
 
    91 apply(rule subsetI)
 
    92 
    92 apply(simp)
 
       
    93 unfolding Sequ_def
 
       
    94 apply(simp)
 
       
    95 by(auto simp add: Sequ_def Star_decomp)
 
    93 
    96 
    94 
    97 
    95 lemma Der_star [simp]:
 
    98 lemma Der_star [simp]:
 
    96   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
 
    99   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
 
    97 proof -    
   100 proof -    
   243  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
 
   246  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
 
   244 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
 
   247 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
 
   245 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 
   248 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 
   246 | "\<turnstile> Void : ONE"
 
   249 | "\<turnstile> Void : ONE"
 
   247 | "\<turnstile> Char c : CHAR c"
 
   250 | "\<turnstile> Char c : CHAR c"
 
   248 | "\<turnstile> Stars [] : STAR r"
 
   251 | "\<forall>v \<in> set vs. \<turnstile> v : r \<Longrightarrow> \<turnstile> Stars vs : STAR r"
 
   249 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
 
       
   250 
   252 
   251 inductive_cases Prf_elims:
 
   253 inductive_cases Prf_elims:
 
   252   "\<turnstile> v : ZERO"
 
   254   "\<turnstile> v : ZERO"
 
   253   "\<turnstile> v : SEQ r1 r2"
 
   255   "\<turnstile> v : SEQ r1 r2"
 
   254   "\<turnstile> v : ALT r1 r2"
 
   256   "\<turnstile> v : ALT r1 r2"
 
   255   "\<turnstile> v : ONE"
 
   257   "\<turnstile> v : ONE"
 
   256   "\<turnstile> v : CHAR c"
 
   258   "\<turnstile> v : CHAR c"
 
   257 (*  "\<turnstile> vs : STAR r"*)
 
   259   "\<turnstile> vs : STAR r"
 
       
   260 
       
   261 lemma Star_concat:
 
       
   262   assumes "\<forall>s \<in> set ss. s \<in> A"  
       
   263   shows "concat ss \<in> A\<star>"
 
       
   264 using assms by (induct ss) (auto)
 
       
   265 
   258 
   266 
   259 lemma Prf_flat_L:
 
   267 lemma Prf_flat_L:
 
   260   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 
   268   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 
   261 using assms
 
   269 using assms
 
   262 by(induct v r rule: Prf.induct)
 
   270 by (induct v r rule: Prf.induct)
 
   263   (auto simp add: Sequ_def)
 
   271    (auto simp add: Sequ_def Star_concat)
 
   264 
       
   265 lemma Prf_Stars:
 
       
   266   assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
 
       
   267   shows "\<turnstile> Stars vs : STAR r"
 
       
   268 using assms
 
       
   269 by(induct vs) (auto intro: Prf.intros)
 
       
   270 
   272 
   271 lemma Prf_Stars_append:
 
   273 lemma Prf_Stars_append:
 
   272   assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r"
 
   274   assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r"
 
   273   shows "\<turnstile> Stars (vs1 @ vs2) : STAR r"
 
   275   shows "\<turnstile> Stars (vs1 @ vs2) : STAR r"
 
   274 using assms
 
   276 using assms
 
   275 apply(induct vs1 arbitrary: vs2)
 
   277 by (auto intro!: Prf.intros elim!: Prf_elims)
 
   276 apply(auto intro: Prf.intros)
 
       
   277 apply(erule Prf.cases)
 
       
   278 apply(simp_all)
 
       
   279 apply(auto intro: Prf.intros)
 
       
   280 done
 
       
   281 
       
   282 
   278 
   283 lemma Star_string:
 
   279 lemma Star_string:
 
   284   assumes "s \<in> A\<star>"
 
   280   assumes "s \<in> A\<star>"
 
   285   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"
 
   281   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"
 
   286 using assms
 
   282 using assms
 
   304 
   300 
   305 lemma L_flat_Prf1:
 
   301 lemma L_flat_Prf1:
 
   306   assumes "\<turnstile> v : r" 
   302   assumes "\<turnstile> v : r" 
   307   shows "flat v \<in> L r"
 
   303   shows "flat v \<in> L r"
 
   308 using assms
 
   304 using assms
 
   309 by (induct)(auto simp add: Sequ_def)
 
   305 by (induct) (auto simp add: Sequ_def Star_concat)
 
   310 
   306 
   311 lemma L_flat_Prf2:
 
   307 lemma L_flat_Prf2:
 
   312   assumes "s \<in> L r" 
   308   assumes "s \<in> L r" 
   313   shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
 
   309   shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
 
   314 using assms
 
   310 using assms
 
   315 apply(induct r arbitrary: s)
 
   311 proof(induct r arbitrary: s)
 
   316 apply(auto simp add: Sequ_def intro: Prf.intros)
 
   312   case (STAR r s)
 
   317 using Prf.intros(1) flat.simps(5) apply blast
 
   313   have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<turnstile> v : r \<and> flat v = s" by fact
 
   318 using Prf.intros(2) flat.simps(3) apply blast
 
   314   have "s \<in> L (STAR r)" by fact
 
   319 using Prf.intros(3) flat.simps(4) apply blast
 
   315   then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r"
 
   320 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)")
 
   316   using Star_string by auto
 
   321 apply(auto)[1]
 
   317   then obtain vs where "concat (map flat vs) = s" "\<forall>v\<in>set vs. \<turnstile> v : r"
 
   322 apply(rule_tac x="Stars vs" in exI)
 
   318   using IH Star_val by blast
 
   323 apply(simp)
 
   319   then show "\<exists>v. \<turnstile> v : STAR r \<and> flat v = s"
 
   324 apply (simp add: Prf_Stars)
 
   320   using Prf.intros(6) flat_Stars by blast
 
   325 apply(drule Star_string)
 
   321 next 
   326 apply(auto)
 
   322   case (SEQ r1 r2 s)
 
   327 apply(rule Star_val)
 
   323   then show "\<exists>v. \<turnstile> v : SEQ r1 r2 \<and> flat v = s"
 
   328 apply(auto)
 
   324   unfolding Sequ_def L.simps by (fastforce intro: Prf.intros)
 
   329 done
 
   325 next
 
       
   326   case (ALT r1 r2 s)
 
       
   327   then show "\<exists>v. \<turnstile> v : ALT r1 r2 \<and> flat v = s"
 
       
   328   unfolding L.simps by (fastforce intro: Prf.intros)
 
       
   329 qed (auto intro: Prf.intros)
 
   330 
   330 
   331 lemma L_flat_Prf:
 
   331 lemma L_flat_Prf:
 
   332   "L(r) = {flat v | v. \<turnstile> v : r}"
 
   332   "L(r) = {flat v | v. \<turnstile> v : r}"
 
   333 using L_flat_Prf1 L_flat_Prf2 by blast
 
   333 using L_flat_Prf1 L_flat_Prf2 by blast
 
   334 
   334 
       
   335 (*
 
   335 lemma Star_values_exists:
 
   336 lemma Star_values_exists:
 
   336   assumes "s \<in> (L r)\<star>"
 
   337   assumes "s \<in> (L r)\<star>"
 
   337   shows "\<exists>vs. concat (map flat vs) = s \<and> \<turnstile> Stars vs : STAR r"
 
   338   shows "\<exists>vs. concat (map flat vs) = s \<and> \<turnstile> Stars vs : STAR r"
 
   338 using assms
 
   339 using assms
 
   339 apply(drule_tac Star_string)
 
   340 apply(drule_tac Star_string)
 
   340 apply(auto)
 
   341 apply(auto)
 
   341 by (metis L_flat_Prf2 Prf_Stars Star_val)
 
   342 by (metis L_flat_Prf2 Prf.intros(6) Star_val)
 
   342 
   343 *)
 
   343 
   344 
   344 
   345 
   345 section {* Sulzmann and Lu functions *}
 
   346 section {* Sulzmann and Lu functions *}
 
   346 
   347 
   347 fun 
   348 fun 
   383   assumes "\<turnstile> v : der c r" 
   384   assumes "\<turnstile> v : der c r" 
   384   shows "\<turnstile> (injval r c v) : r"
 
   385   shows "\<turnstile> (injval r c v) : r"
 
   385 using assms
 
   386 using assms
 
   386 apply(induct r arbitrary: c v rule: rexp.induct)
 
   387 apply(induct r arbitrary: c v rule: rexp.induct)
 
   387 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)
 
   388 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)
 
   388 (* STAR *)
 
   389 done
 
   389 apply(rotate_tac 2)
 
       
   390 apply(erule Prf.cases)
 
       
   391 apply(simp_all)[7]
 
       
   392 apply(auto)
 
       
   393 apply (metis Prf.intros(6) Prf.intros(7))
 
       
   394 by (metis Prf.intros(7))
 
       
   395 
   390 
   396 lemma Prf_injval_flat:
 
   391 lemma Prf_injval_flat:
 
   397   assumes "\<turnstile> v : der c r" 
   392   assumes "\<turnstile> v : der c r" 
   398   shows "flat (injval r c v) = c # (flat v)"
 
   393   shows "flat (injval r c v) = c # (flat v)"
 
   399 using assms
 
   394 using assms
 
   400 apply(induct arbitrary: v rule: der.induct)
 
   395 apply(induct arbitrary: v rule: der.induct)
 
   401 apply(auto elim!: Prf_elims split: if_splits)
 
   396 apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits)
 
   402 apply(metis mkeps_flat)
 
       
   403 apply(rotate_tac 2)
 
       
   404 apply(erule Prf.cases)
 
       
   405 apply(simp_all)[7]
 
       
   406 done
 
   397 done
 
   407 
   398 
   408 
   399 
   409 
   400 
   410 section {* Our Alternative Posix definition *}
 
   401 section {* Our Alternative Posix definition *}
 
   442 
   433 
   443 lemma Posix1a:
 
   434 lemma Posix1a:
 
   444   assumes "s \<in> r \<rightarrow> v"
 
   435   assumes "s \<in> r \<rightarrow> v"
 
   445   shows "\<turnstile> v : r"
 
   436   shows "\<turnstile> v : r"
 
   446 using assms
 
   437 using assms
 
   447 by (induct s r v rule: Posix.induct)(auto intro: Prf.intros)
 
   438 apply(induct s r v rule: Posix.induct)
 
       
   439 apply(auto intro!: Prf.intros elim!: Prf_elims)
 
       
   440 done
 
   448 
   441 
   449 
   442 
   450 lemma Posix_mkeps:
 
   443 lemma Posix_mkeps:
 
   451   assumes "nullable r"
 
   444   assumes "nullable r"
 
   452   shows "[] \<in> r \<rightarrow> mkeps r"
 
   445   shows "[] \<in> r \<rightarrow> mkeps r"
lexing