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/ReStar.thy
changeset 94 5b01f7c233f8
parent 93 37e3f1174974
child 95 a33d3040bf7e
equal deleted inserted replaced
93:37e3f1174974 94:5b01f7c233f8 
   113   shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
 
   113   shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
 
   114 using a
 
   114 using a
 
   115 by (induct x\<equiv>"c # x" rule: Star.induct) 
   115 by (induct x\<equiv>"c # x" rule: Star.induct) 
   116    (auto simp add: append_eq_Cons_conv)
 
   116    (auto simp add: append_eq_Cons_conv)
 
   117 
   117 
   118 (*
 
       
   119 lemma star_induct[consumes 1, case_names Nil append, induct set: Star]:
 
       
   120 assumes "w \<in> A\<star>"
 
       
   121   and "P []"
 
       
   122   and step: "\<And>u v. u \<in> A \<Longrightarrow> v \<in> A\<star> \<Longrightarrow> P v \<Longrightarrow> P (u @ v)"
 
       
   123 shows "P w"
 
       
   124 proof -
 
       
   125   { fix n have "w \<in> A \<up> n \<Longrightarrow> P w"
 
       
   126       apply(induct n arbitrary: w) 
       
   127       apply(auto intro: `P []` step star2 simp add: Sequ_def)
 
       
   128       done
 
       
   129   }
 
       
   130   with `w \<in> A\<star>` show "P w" by (auto simp: star3)
 
       
   131 qed
 
       
   132 *)
 
       
   133 
   118 
   134 section {* Regular Expressions *}
 
   119 section {* Regular Expressions *}
 
   135 
   120 
   136 datatype rexp =
 
   121 datatype rexp =
 
   137   NULL
 
   122   NULL
 
   457   "Prefixes s \<equiv> {sp. sp \<sqsubseteq> s}"
 
   442   "Prefixes s \<equiv> {sp. sp \<sqsubseteq> s}"
 
   458 
   443 
   459 definition Suffixes :: "string \<Rightarrow> string set" where
 
   444 definition Suffixes :: "string \<Rightarrow> string set" where
 
   460   "Suffixes s \<equiv> rev ` (Prefixes (rev s))"
 
   445   "Suffixes s \<equiv> rev ` (Prefixes (rev s))"
 
   461 
   446 
       
   447 definition SPrefixes :: "string \<Rightarrow> string set" where
 
       
   448   "SPrefixes s \<equiv> {sp. sp \<sqsubset> s}"
 
       
   449 
       
   450 definition SSuffixes :: "string \<Rightarrow> string set" where
 
       
   451   "SSuffixes s \<equiv> rev ` (SPrefixes (rev s))"
 
       
   452 
   462 lemma Suffixes_in: 
   453 lemma Suffixes_in: 
   463   "\<exists>s1. s1 @ s2 = s3 \<Longrightarrow> s2 \<in> Suffixes s3"
 
   454   "\<exists>s1. s1 @ s2 = s3 \<Longrightarrow> s2 \<in> Suffixes s3"
 
   464 unfolding Suffixes_def Prefixes_def prefix_def image_def
 
   455 unfolding Suffixes_def Prefixes_def prefix_def image_def
 
   465 apply(auto)
 
   456 apply(auto)
 
   466 by (metis rev_rev_ident)
 
   457 by (metis rev_rev_ident)
 
       
   458 
       
   459 lemma SSuffixes_in: 
       
   460   "\<exists>s1. s1 \<noteq> [] \<and> s1 @ s2 = s3 \<Longrightarrow> s2 \<in> SSuffixes s3"
 
       
   461 unfolding SSuffixes_def Suffixes_def SPrefixes_def Prefixes_def sprefix_def prefix_def image_def
 
       
   462 apply(auto)
 
       
   463 by (metis append_self_conv rev.simps(1) rev_rev_ident)
 
   467 
   464 
   468 lemma Prefixes_Cons:
 
   465 lemma Prefixes_Cons:
 
   469   "Prefixes (c # s) = {[]} \<union> {c # sp | sp. sp \<in> Prefixes s}"
 
   466   "Prefixes (c # s) = {[]} \<union> {c # sp | sp. sp \<in> Prefixes s}"
 
   470 unfolding Prefixes_def prefix_def
 
   467 unfolding Prefixes_def prefix_def
 
   471 apply(auto simp add: append_eq_Cons_conv) 
   468 apply(auto simp add: append_eq_Cons_conv) 
   499 
   496 
   500 
   497 
   501 definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
 
   498 definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
 
   502   "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}"
 
   499   "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}"
 
   503 
   500 
       
   501 definition NValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
 
       
   502   "NValues r s \<equiv> {v. \<Turnstile> v : r \<and> flat v \<sqsubseteq> s}"
 
       
   503 
       
   504 lemma NValues_STAR_Nil:
 
       
   505   "NValues (STAR r) [] = {Star []}"
 
       
   506 apply(auto simp add: NValues_def prefix_def)
 
       
   507 apply(erule NPrf.cases)
 
       
   508 apply(auto)
 
       
   509 by (metis NPrf.intros(6))
 
       
   510 
       
   511 
   504 definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where
 
   512 definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where
 
   505   "rest v s \<equiv> drop (length (flat v)) s"
 
   513   "rest v s \<equiv> drop (length (flat v)) s"
 
       
   514 
       
   515 lemma rest_Nil:
 
       
   516   "rest v [] = []"
 
       
   517 apply(simp add: rest_def)
 
       
   518 done
 
   506 
   519 
   507 lemma rest_Suffixes:
 
   520 lemma rest_Suffixes:
 
   508   "rest v s \<in> Suffixes s"
 
   521   "rest v s \<in> Suffixes s"
 
   509 unfolding rest_def
 
   522 unfolding rest_def
 
   510 by (metis Suffixes_in append_take_drop_id)
 
   523 by (metis Suffixes_in append_take_drop_id)
 
       
   524 
       
   525 lemma rest_SSuffixes:
 
       
   526   assumes "flat v \<noteq> []" "s \<noteq> []"
 
       
   527   shows "rest v s \<in> SSuffixes s"
 
       
   528 using assms
 
       
   529 unfolding rest_def
 
       
   530 thm SSuffixes_in
 
       
   531 apply(rule_tac SSuffixes_in)
 
       
   532 apply(rule_tac x="take (length (flat v)) s" in exI)
 
       
   533 apply(simp add: sprefix_def)
 
       
   534 done
 
   511 
   535 
   512 
   536 
   513 lemma Values_recs:
 
   537 lemma Values_recs:
 
   514   "Values (NULL) s = {}"
 
   538   "Values (NULL) s = {}"
 
   515   "Values (EMPTY) s = {Void}"
 
   539   "Values (EMPTY) s = {Void}"
 
   516   "Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
   540   "Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
   517   "Values (ALT r1 r2) s = {Left v | v. v \<in> Values r1 s} \<union> {Right v | v. v \<in> Values r2 s}"
 
   541   "Values (ALT r1 r2) s = {Left v | v. v \<in> Values r1 s} \<union> {Right v | v. v \<in> Values r2 s}"
 
   518   "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}"
 
   542   "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}"
 
       
   543   "Values (STAR r) s = {Star []} \<union> {Star (v # vs) | v vs. v \<in> Values r s \<and> 
       
   544                                                                Star vs \<in> Values (STAR r) (rest v s)}"
 
   519 unfolding Values_def
 
   545 unfolding Values_def
 
   520 apply(auto)
 
   546 apply(auto)
 
   521 (*NULL*)
 
   547 (*NULL*)
 
   522 apply(erule Prf.cases)
 
   548 apply(erule Prf.cases)
 
   523 apply(simp_all)[7]
 
   549 apply(simp_all)[7]
 
   541 apply(erule Prf.cases)
 
   567 apply(erule Prf.cases)
 
   542 apply(simp_all)[7]
 
   568 apply(simp_all)[7]
 
   543 apply (simp add: append_eq_conv_conj prefix_def rest_def)
 
   569 apply (simp add: append_eq_conv_conj prefix_def rest_def)
 
   544 apply (metis Prf.intros(1))
 
   570 apply (metis Prf.intros(1))
 
   545 apply (simp add: append_eq_conv_conj prefix_def rest_def)
 
   571 apply (simp add: append_eq_conv_conj prefix_def rest_def)
 
   546 done
 
   572 (*STAR*)
 
   547 
   573 apply(erule Prf.cases)
 
   548 (* This lemma needs to be adapted to Star
 
   574 apply(simp_all)[7]
 
   549 lemma Values_finite:
 
   575 apply(rule conjI)
 
   550   "finite (Values r s)"
 
   576 apply(simp add: prefix_def)
 
   551 apply(induct r arbitrary: s)
 
   577 apply(auto)[1]
 
   552 apply(simp_all add: Values_recs)
 
   578 apply(simp add: prefix_def)
 
   553 thm finite_surj
 
   579 apply(auto)[1]
 
       
   580 apply (metis append_eq_conv_conj rest_def)
 
       
   581 apply (metis Prf.intros(6))
 
       
   582 apply (metis append_Nil prefix_def)
 
       
   583 apply (metis Prf.intros(7))
 
       
   584 by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
 
       
   585 
       
   586 lemma NValues_recs:
 
       
   587   "NValues (NULL) s = {}"
 
       
   588   "NValues (EMPTY) s = {Void}"
 
       
   589   "NValues (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
       
   590   "NValues (ALT r1 r2) s = {Left v | v. v \<in> NValues r1 s} \<union> {Right v | v. v \<in> NValues r2 s}"
 
       
   591   "NValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> NValues r1 s \<and> v2 \<in> NValues r2 (rest v1 s)}"
 
       
   592   "NValues (STAR r) s = {Star []} \<union> {Star (v # vs) | v vs. v \<in> NValues r s \<and> flat v \<noteq> [] \<and> 
       
   593                                                                Star vs \<in> NValues (STAR r) (rest v s)}"
 
       
   594 unfolding NValues_def
 
       
   595 apply(auto)
 
       
   596 (*NULL*)
 
       
   597 apply(erule NPrf.cases)
 
       
   598 apply(simp_all)[7]
 
       
   599 (*EMPTY*)
 
       
   600 apply(erule NPrf.cases)
 
       
   601 apply(simp_all)[7]
 
       
   602 apply(rule NPrf.intros)
 
       
   603 apply (metis append_Nil prefix_def)
 
       
   604 (*CHAR*)
 
       
   605 apply(erule NPrf.cases)
 
       
   606 apply(simp_all)[7]
 
       
   607 apply(rule NPrf.intros)
 
       
   608 apply(erule NPrf.cases)
 
       
   609 apply(simp_all)[7]
 
       
   610 (*ALT*)
 
       
   611 apply(erule NPrf.cases)
 
       
   612 apply(simp_all)[7]
 
       
   613 apply (metis NPrf.intros(2))
 
       
   614 apply (metis NPrf.intros(3))
 
       
   615 (*SEQ*)
 
       
   616 apply(erule NPrf.cases)
 
       
   617 apply(simp_all)[7]
 
       
   618 apply (simp add: append_eq_conv_conj prefix_def rest_def)
 
       
   619 apply (metis NPrf.intros(1))
 
       
   620 apply (simp add: append_eq_conv_conj prefix_def rest_def)
 
       
   621 (*STAR*)
 
       
   622 apply(erule NPrf.cases)
 
       
   623 apply(simp_all)
 
       
   624 apply(rule conjI)
 
       
   625 apply(simp add: prefix_def)
 
       
   626 apply(auto)[1]
 
       
   627 apply(simp add: prefix_def)
 
       
   628 apply(auto)[1]
 
       
   629 apply (metis append_eq_conv_conj rest_def)
 
       
   630 apply (metis NPrf.intros(6))
 
       
   631 apply (metis append_Nil prefix_def)
 
       
   632 apply (metis NPrf.intros(7))
 
       
   633 by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
 
       
   634 
       
   635 
       
   636 lemma finite_image_set2:
 
       
   637   "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {(x, y) | x y. P x \<and> Q y}"
 
       
   638   by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {(x, y)}"]) auto
 
       
   639 
       
   640 
       
   641 lemma NValues_finite_aux:
 
       
   642   "(\<lambda>(r, s). finite (NValues r s)) (r, s)"
 
       
   643 apply(rule wf_induct[of "measure size <*lex*> measure length",where P="\<lambda>(r, s). finite (NValues r s)"])
 
       
   644 apply (metis wf_lex_prod wf_measure)
 
       
   645 apply(auto)
 
       
   646 apply(case_tac a)
 
       
   647 apply(simp_all)
 
       
   648 apply(simp add: NValues_recs)
 
       
   649 apply(simp add: NValues_recs)
 
       
   650 apply(simp add: NValues_recs)
 
       
   651 apply(simp add: NValues_recs)
 
   554 apply(rule_tac f="\<lambda>(x, y). Seq x y" and 
   652 apply(rule_tac f="\<lambda>(x, y). Seq x y" and 
   555                A="{(v1, v2) | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}" in finite_surj)
 
   653                A="{(v1, v2) | v1 v2. v1 \<in> NValues rexp1 b \<and> v2 \<in> NValues rexp2 (rest v1 b)}" in finite_surj)
 
   556 prefer 2
 
   654 prefer 2
 
   557 apply(auto)[1]
 
   655 apply(auto)[1]
 
   558 apply(rule_tac B="\<Union>sp \<in> Suffixes s. {(v1, v2). v1 \<in> Values r1 s \<and> v2 \<in> Values r2 sp}" in finite_subset)
 
   656 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)
 
   559 apply(auto)[1]
 
   657 apply(auto)[1]
 
   560 apply (metis rest_Suffixes)
 
   658 apply (metis rest_Suffixes)
 
   561 apply(rule finite_UN_I)
 
   659 apply(rule finite_UN_I)
 
   562 apply(rule finite_Suffixes)
 
   660 apply(rule finite_Suffixes)
 
   563 apply(simp)
 
   661 apply(simp)
 
   564 done
 
   662 apply(simp add: NValues_recs)
 
   565 *)
 
   663 apply(clarify)
 
       
   664 apply(subst NValues_recs)
 
       
   665 apply(simp)
 
       
   666 apply(rule_tac f="\<lambda>(v, vs). Star (v # vs)" and 
       
   667                A="{(v, vs) | v vs. v \<in> NValues rexp b \<and> (flat v \<noteq> [] \<and> Star vs \<in> NValues (STAR rexp) (rest v b))}" in finite_surj)
 
       
   668 prefer 2
 
       
   669 apply(auto)[1]
 
       
   670 apply(auto)
 
       
   671 apply(case_tac b)
 
       
   672 apply(simp)
 
       
   673 defer
 
       
   674 apply(rule_tac B="\<Union>sp \<in> SSuffixes b. {(v, vs) | v vs. v \<in> NValues rexp b \<and> Star vs \<in> NValues (STAR rexp) sp}" in finite_subset)
 
       
   675 apply(auto)[1]
 
       
   676 apply(rule_tac x="rest aa (a # list)" in bexI)
 
       
   677 apply(simp)
 
       
   678 apply (rule rest_SSuffixes)
 
       
   679 apply(simp)
 
       
   680 apply(simp)
 
       
   681 apply(rule finite_UN_I)
 
       
   682 defer
 
       
   683 apply(frule_tac x="rexp" in spec)
 
       
   684 apply(drule_tac x="b" in spec)
 
       
   685 apply(drule conjunct1)
 
       
   686 apply(drule mp)
 
       
   687 apply(simp)
 
       
   688 apply(drule_tac x="STAR rexp" in spec)
 
       
   689 apply(drule_tac x="sp" in spec)
 
       
   690 apply(drule conjunct2)
 
       
   691 apply(drule mp)
 
       
   692 apply(simp)
 
       
   693 apply(simp add: prefix_def SPrefixes_def SSuffixes_def)
 
       
   694 apply(auto)[1]
 
       
   695 apply (metis length_Cons length_rev length_sprefix rev.simps(2))
 
       
   696 apply(simp)
 
       
   697 apply(rule finite_cartesian_product)
 
       
   698 apply(simp)
 
       
   699 apply(rule_tac f="Star" in finite_imageD)
 
       
   700 prefer 2
 
       
   701 apply(auto simp add: inj_on_def)[1]
 
       
   702 apply (metis finite_subset image_Collect_subsetI)
 
       
   703 apply(simp add: rest_Nil)
 
       
   704 apply(simp add: NValues_STAR_Nil)
 
       
   705 apply(rule_tac B="{(v, vs). v \<in> NValues rexp [] \<and> vs = []}" in finite_subset)
 
       
   706 apply(auto)[1]
 
       
   707 apply(simp)
 
       
   708 apply(rule_tac B="Suffixes b" in finite_subset)
 
       
   709 apply(auto simp add: SSuffixes_def Suffixes_def Prefixes_def SPrefixes_def sprefix_def)[1]
 
       
   710 by (metis finite_Suffixes)
 
       
   711 
       
   712 lemma NValues_finite:
 
       
   713   "finite (NValues r s)"
 
       
   714 using NValues_finite_aux
 
       
   715 apply(simp)
 
       
   716 done
 
   566 
   717 
   567 section {* Sulzmann functions *}
 
   718 section {* Sulzmann functions *}
 
   568 
   719 
   569 fun 
   720 fun 
   570   mkeps :: "rexp \<Rightarrow> val"
 
   721   mkeps :: "rexp \<Rightarrow> val"
lexing