lexing: comparison thys/ReStar.thy

equal deleted inserted replaced

-:c3d7125f9950
+:38696f516c6b
 "nullable (NULL) = False"
 | "nullable (EMPTY) = True"
 | "nullable (CHAR c) = False"
 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
-| "nullable (STAR r1) = True"
+| "nullable (STAR r) = True"
 lemma nullable_correctness:
 shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 apply (induct r)
 apply(auto simp add: Sequ_def)
 Void
 | Char char
 | Seq val val
 | Right val
 | Left val
-| Star "val list"
+| Stars "val list"
 section {* The string behind a value *}
 fun
 flat :: "val \<Rightarrow> string"
 "flat (Void) = []"
 | "flat (Char c) = [c]"
 | "flat (Left v) = flat v"
 | "flat (Right v) = flat v"
 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
-| "flat (Star []) = []"
+| "flat (Stars []) = []"
-| "flat (Star (v#vs)) = (flat v) @ (flat (Star vs))"
+| "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))"
 lemma [simp]:
-"flat (Star vs) = concat (map flat vs)"
+"flat (Stars vs) = concat (map flat vs)"
 apply(induct vs)
 apply(auto)
 done
 section {* Relation between values and regular expressions *}
 "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
 | "\<Turnstile> Void : EMPTY"
 | "\<Turnstile> Char c : CHAR c"
-| "\<Turnstile> Star [] : STAR r"
+| "\<Turnstile> Stars [] : STAR r"
-| "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Star vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Star (v # vs) : STAR r"
+| "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Stars vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"
 inductive
 Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 where
 "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 | "\<turnstile> Void : EMPTY"
 | "\<turnstile> Char c : CHAR c"
-| "\<turnstile> Star [] : STAR r"
+| "\<turnstile> Stars [] : STAR r"
-| "\<lbrakk>\<turnstile> v : r; \<turnstile> Star vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Star (v # vs) : STAR r"
+| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
 lemma NPrf_imp_Prf:
 assumes "\<Turnstile> v : r"
 shows "\<turnstile> v : r"
 using assms
 apply(auto intro: Prf.intros)
 done
 lemma NPrf_Prf_val:
 shows "\<turnstile> v : r \<Longrightarrow> \<exists>v'. flat v' = flat v \<and> \<Turnstile> v' : r"
-and   "\<turnstile> Star vs : r \<Longrightarrow> \<exists>vs'. flat (Star vs') = flat (Star vs) \<and> \<Turnstile> Star vs' : r"
+and   "\<turnstile> Stars vs : r \<Longrightarrow> \<exists>vs'. flat (Stars vs') = flat (Stars vs) \<and> \<Turnstile> Stars vs' : r"
 using assms
 apply(induct v and vs arbitrary: r and r rule: val.inducts)
 apply(auto)[1]
 apply(erule Prf.cases)
 apply(simp_all)[7]
 apply(simp)
 apply (metis NPrf.intros)
 apply(drule_tac x="r" in meta_spec)
 apply(simp)
 apply(auto)[1]
-apply(rule_tac x="Star vs'" in exI)
+apply(rule_tac x="Stars vs'" in exI)
 apply(simp)
 apply(rule_tac x="[]" in exI)
 apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[7]
 lemma NPrf_flat_L:
 assumes "\<Turnstile> v : r" shows "flat v \<in> L r"
 using assms
 by (metis NPrf_imp_Prf Prf_flat_L)
-lemma Prf_Star:
+lemma Prf_Stars:
 assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
-shows "\<turnstile> Star vs : STAR r"
+shows "\<turnstile> Stars vs : STAR r"
 using assms
 apply(induct vs)
 apply (metis Prf.intros(6))
 by (metis Prf.intros(7) insert_iff set_simps(2))
 apply (metis Prf.intros(3) flat.simps(4))
 apply(erule Prf.cases)
 apply(auto)
 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = x \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)")
 apply(auto)[1]
-apply(rule_tac x="Star vs" in exI)
+apply(rule_tac x="Stars vs" in exI)
 apply(simp)
-apply(rule Prf_Star)
+apply(rule Prf_Stars)
 apply(simp)
 apply(drule Star_string)
 apply(auto)
 apply(rule Star_val)
 apply(simp)
 apply(simp add: star3)
 apply(auto)
 apply(rule_tac x="Suc x" in exI)
 apply(auto simp add: Sequ_def)
 apply(rule_tac x="flat v" in exI)
-apply(rule_tac x="flat (Star vs)" in exI)
+apply(rule_tac x="flat (Stars vs)" in exI)
 apply(auto)
 by (metis Prf_flat_L)
 lemma L_flat_Prf2:
 "L(r) = {flat v | v. \<turnstile> v : r}"
 definition NValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
 "NValues r s \<equiv> {v. \<Turnstile> v : r \<and> flat v \<sqsubseteq> s}"
 lemma NValues_STAR_Nil:
-"NValues (STAR r) [] = {Star []}"
+"NValues (STAR r) [] = {Stars []}"
 apply(auto simp add: NValues_def prefix_def)
 apply(erule NPrf.cases)
 apply(auto)
 by (metis NPrf.intros(6))
 "Values (EMPTY) s = {Void}"
 "Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})"
 "Values (ALT r1 r2) s = {Left v | v. v \<in> Values r1 s} \<union> {Right v | v. v \<in> Values r2 s}"
 "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}"
 "Values (STAR r) s =
-{Star []} \<union> {Star (v # vs) | v vs. v \<in> Values r s \<and> Star vs \<in> Values (STAR r) (rest v s)}"
+{Stars []} \<union> {Stars (v # vs) | v vs. v \<in> Values r s \<and> Stars vs \<in> Values (STAR r) (rest v s)}"
 unfolding Values_def
 apply(auto)
 (*NULL*)
 apply(erule Prf.cases)
 apply(simp_all)[7]
 "NValues (EMPTY) s = {Void}"
 "NValues (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})"
 "NValues (ALT r1 r2) s = {Left v | v. v \<in> NValues r1 s} \<union> {Right v | v. v \<in> NValues r2 s}"
 "NValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> NValues r1 s \<and> v2 \<in> NValues r2 (rest v1 s)}"
 "NValues (STAR r) s =
-{Star []} \<union> {Star (v # vs) | v vs. v \<in> NValues r s \<and> flat v \<noteq> [] \<and>  Star vs \<in> NValues (STAR r) (rest v s)}"
+{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)}"
 unfolding NValues_def
 apply(auto)
 (*NULL*)
 apply(erule NPrf.cases)
 apply(simp_all)[7]
 apply(simp)
 apply(simp add: NValues_recs)
 apply(clarify)
 apply(subst NValues_recs)
 apply(simp)
-apply(rule_tac f="\<lambda>(v, vs). Star (v # vs)" and
+apply(rule_tac f="\<lambda>(v, vs). Stars (v # vs)" and
-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)
+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)
 prefer 2
 apply(auto)[1]
 apply(auto)
 apply(case_tac b)
 apply(simp)
 defer
-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)
+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)
 apply(auto)[1]
 apply(rule_tac x="rest aa (a # list)" in bexI)
 apply(simp)
 apply (rule rest_SSuffixes)
 apply(simp)
 apply(auto)[1]
 apply (metis length_Cons length_rev length_sprefix rev.simps(2))
 apply(simp)
 apply(rule finite_cartesian_product)
 apply(simp)
-apply(rule_tac f="Star" in finite_imageD)
+apply(rule_tac f="Stars" in finite_imageD)
 prefer 2
 apply(auto simp add: inj_on_def)[1]
 apply (metis finite_subset image_Collect_subsetI)
 apply(simp add: rest_Nil)
 apply(simp add: NValues_STAR_Nil)
 mkeps :: "rexp \<Rightarrow> val"
 where
 "mkeps(EMPTY) = Void"
 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
-| "mkeps(STAR r) = Star []"
+| "mkeps(STAR r) = Stars []"
 section {* Derivatives *}
 fun
 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 "injval (EMPTY) c Void = Char c"
 | "injval (CHAR d) c Void = Char d"
 | "injval (CHAR d) c (Char c') = Seq (Char d) (Char c')"
 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
-| "injval (SEQ r1 r2) c (Char c') = Seq (Char c) (Char c')"
 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
-| "injval (STAR r) c (Seq v (Star vs)) = Star ((injval r c v) # vs)"
+| "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
 fun
 lex :: "rexp \<Rightarrow> string \<Rightarrow> val option"
 where
 "lex r [] = (if nullable r then Some(mkeps r) else None)"
 | "projval (ALT r1 r2) c (Right v2) = Right (projval r2 c v2)"
 | "projval (SEQ r1 r2) c (Seq v1 v2) =
 (if flat v1 = [] then Right(projval r2 c v2)
 else if nullable r1 then Left (Seq (projval r1 c v1) v2)
 else Seq (projval r1 c v1) v2)"
-| "projval (STAR r) c (Star (v # vs)) = Seq (projval r c v) (Star vs)"
+| "projval (STAR r) c (Stars (v # vs)) = Seq (projval r c v) (Stars vs)"
 lemma mkeps_nullable:
 assumes "nullable(r)"
 apply (metis Cons_eq_append_conv)
 apply(simp)
 apply(rule NPrf.intros)
 apply (metis Cons_eq_append_conv)
 apply(simp)
-(* Star case *)
+(* Stars case *)
 apply(rule NPrf.intros)
 apply (metis Cons_eq_append_conv)
 apply(auto)
 done
 "[] \<in> EMPTY \<rightarrow> Void"
 | "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
-\<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow>
+\<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>
 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
-| "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Star vs; flat v \<noteq> []\<rbrakk>
+| "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []\<rbrakk>
-\<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Star (v # vs)"
+\<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
-| "[] \<in> STAR r \<rightarrow> Star []"
+| "[] \<in> STAR r \<rightarrow> Stars []"
 lemma PMatch_mkeps:
 assumes "nullable r"
 shows "[] \<in> r \<rightarrow> mkeps r"
 using assms
 apply(auto)[1]
 apply(simp add: L_flat_NPrf)
 apply(auto)[1]
 apply(frule_tac c="c" in v3_proj)
 apply metis
-apply(drule_tac x="s3" in spec)
+apply(drule_tac x="s\<^sub>3" in spec)
 apply(drule mp)
 apply(rule_tac x="projval r1 c v" in exI)
 apply(rule conjI)
 apply (metis v4_proj2)
 apply (metis NPrf_imp_Prf)
 apply(auto)[1]
 apply(simp add: L_flat_NPrf)
 apply(auto)[1]
 apply(frule_tac c="c" in v3_proj)
 apply metis
-apply(drule_tac x="s3" in spec)
+apply(drule_tac x="s\<^sub>3" in spec)
 apply(drule mp)
 apply (metis NPrf_imp_Prf v4_proj2)
 apply(simp)
 (* interesting case *)
 apply(clarify)
 apply (metis NPrf_imp_Prf Prf.intros(1))
 apply(rule NPrf_imp_Prf)
 apply(rule v3_proj)
 apply(simp)
 apply (metis Cons_eq_append_conv)
-(* Star case *)
+(* Stars case *)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
 apply(clarify)
 apply(rotate_tac 2)
 apply(frule_tac PMatch1)
 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 | "Void \<succ>EMPTY Void"
 | "(Char c) \<succ>(CHAR c) (Char c)"
-| "flat (Star (v # vs)) = [] \<Longrightarrow> (Star []) \<succ>(STAR r) (Star (v # vs))"
+| "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))"
-| "flat (Star (v # vs)) \<noteq> [] \<Longrightarrow> (Star (v # vs)) \<succ>(STAR r) (Star [])"
+| "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
-| "v1 \<succ>r v2 \<Longrightarrow> (Star (v1 # vs1)) \<succ>(STAR r) (Star (v2 # vs2))"
+| "v1 \<succ>r v2 \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
-| "(Star vs1) \<succ>(STAR r) (Star vs2) \<Longrightarrow> (Star (v # vs1)) \<succ>(STAR r) (Star (v # vs2))"
+| "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
-| "(Star []) \<succ>(STAR r) (Star [])"
+| "(Stars []) \<succ>(STAR r) (Stars [])"
 (*
 lemma ValOrd_PMatch:
 assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2  \<sqsubseteq> s"
 apply(erule PMatch.cases)
 apply(simp_all)[7]
 apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
 apply(clarify)
 apply (metis ValOrd.intros(5))
-(* Star case *)
+(* Stars case *)
 apply(erule Prf.cases)
 apply(simp_all)[7]
 apply(erule PMatch.cases)
 apply(simp_all)
 apply (metis Nil_is_append_conv ValOrd.intros(10) flat.simps(7))
 apply(erule Prf.cases)
 apply(simp_all)[5]
 oops
 *)
 end

changeset 97	38696f516c6b
parent 95	a33d3040bf7e
child 99	f76c250906d5