lexing: comparison thys/LexerExt.thy

equal deleted inserted replaced

-:4c02878e2fe0
+:17c079699ea0
 | SEQ rexp rexp
 | ALT rexp rexp
 | STAR rexp
 | UPNTIMES rexp nat
 | NTIMES rexp nat
+| FROMNTIMES rexp nat
 section {* Semantics of Regular Expressions *}
 fun
 L :: "rexp \<Rightarrow> string set"
 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 | "L (STAR r) = (L r)\<star>"
 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)"
 | "L (NTIMES r n) = ((L r) \<up> n)"
+| "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)"
 section {* Nullable, Derivatives *}
 fun
 nullable :: "rexp \<Rightarrow> bool"
 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 | "nullable (STAR r) = True"
 | "nullable (UPNTIMES r n) = True"
 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
+| "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)"
 fun
 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 where
 "der c (ZERO) = ZERO"
 | "der c (STAR r) = SEQ (der c r) (STAR r)"
 | "der c (UPNTIMES r 0) = ZERO"
 | "der c (UPNTIMES r (Suc n)) = SEQ (der c r) (UPNTIMES r n)"
 | "der c (NTIMES r 0) = ZERO"
 | "der c (NTIMES r (Suc n)) = SEQ (der c r) (NTIMES r n)"
+| "der c (FROMNTIMES r 0) = SEQ (der c r) (STAR r)"
+| "der c (FROMNTIMES r (Suc n)) = SEQ (der c r) (FROMNTIMES r n)"
 fun
 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 where
 "ders [] r = r"
 apply(simp)
 (* NTIMES *)
 apply(simp only: L.simps der.simps)
 apply(simp)
 apply(rule impI)
-by (simp add: Der_Pow_subseteq sup_absorb1)
+apply (simp add: Der_Pow_subseteq sup_absorb1)
+(* FROMNTIMES *)
+apply(simp only: der.simps)
+apply(simp only: L.simps)
+apply(subst Der_star[symmetric])
+apply(subst Star_def2)
+apply(auto)[1]
+apply(simp only: der.simps)
+apply(simp only: L.simps)
+apply(simp add: Der_UNION)
+by (smt Der_Pow Der_Pow_notin Der_Pow_subseteq SUP_cong Seq_UNION Suc_reduce_Union2 sup.absorb_iff1)
 lemma ders_correctness:
 shows "L (ders s r) = Ders s (L r)"
 apply(induct s arbitrary: r)
 apply(simp_all add: Ders_def der_correctness Der_def)
 "\<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 : ONE"
 | "\<turnstile> Char c : CHAR c"
-| "\<turnstile> Stars [] : STAR r"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : STAR r"
-| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<le> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r n"
-| "\<turnstile> Stars [] : UPNTIMES r 0"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs = n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NTIMES r n"
-| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : UPNTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : UPNTIMES r (Suc n)"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : FROMNTIMES r n"
-| "\<lbrakk>\<turnstile> Stars vs : UPNTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r (Suc n)"
-| "\<turnstile> Stars [] : NTIMES r 0"
-| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : NTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : NTIMES r (Suc n)"
 inductive_cases Prf_elims:
 "\<turnstile> v : ZERO"
 "\<turnstile> v : SEQ r1 r2"
 "\<turnstile> v : ALT r1 r2"
 "\<turnstile> v : ONE"
 "\<turnstile> v : CHAR c"
 (*  "\<turnstile> vs : STAR r"*)
+lemma Prf_STAR:
+assumes "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<in> L r"
+shows "concat (map flat vs) \<in> L r\<star>"
+using assms
+apply(induct vs)
+apply(auto)
+done
+lemma Prf_Pow:
+assumes "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<in> L r"
+shows "concat (map flat vs) \<in> L r \<up> length vs"
+using assms
+apply(induct vs)
+apply(auto simp add: Sequ_def)
+done
 lemma Prf_flat_L:
 assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 using assms
 apply(induct v r rule: Prf.induct)
 apply(auto simp add: Sequ_def)
-apply(rotate_tac 2)
+apply(rule Prf_STAR)
-apply(rule_tac x="Suc x" in bexI)
+apply(simp)
-apply(auto simp add: Sequ_def)[2]
+apply(rule_tac x="length vs" in bexI)
-done
+apply(rule Prf_Pow)
+apply(simp)
-lemma Prf_Stars:
+apply(simp)
-assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
+apply(rule Prf_Pow)
-shows "\<turnstile> Stars vs : STAR r"
+apply(simp)
-using assms
+apply(rule_tac x="length vs" in bexI)
-by(induct vs) (auto intro: Prf.intros)
+apply(rule Prf_Pow)
+apply(simp)
-lemma Prf_Stars_NTIMES:
+apply(simp)
-assumes "\<forall>v \<in> set vs. \<turnstile> v : r" "(length vs) = n"
-shows "\<turnstile> Stars vs : NTIMES r n"
-using assms
-apply(induct vs arbitrary: n)
-apply(auto intro: Prf.intros)
-done
-lemma Prf_Stars_UPNTIMES:
-assumes "\<forall>v \<in> set vs. \<turnstile> v : r" "(length vs) = n"
-shows "\<turnstile> Stars vs : UPNTIMES r n"
-using assms
-apply(induct vs arbitrary: n)
-apply(auto intro: Prf.intros)
-done
-lemma Prf_UPNTIMES_bigger:
-assumes "\<turnstile> Stars vs : UPNTIMES r n" "n \<le> m"
-shows "\<turnstile> Stars vs : UPNTIMES r m"
-using assms
-apply(induct m arbitrary:)
-apply(auto)
-using Prf.intros(10) le_Suc_eq by blast
-lemma UPNTIMES_Stars:
-assumes "\<turnstile> v : UPNTIMES r n"
-shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs \<le> n"
-using assms
-apply(induct n arbitrary: v)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(auto)
-using le_SucI by blast
-lemma NTIMES_Stars:
-assumes "\<turnstile> v : NTIMES r n"
-shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs = n"
-using assms
-apply(induct n arbitrary: v)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(auto)
 done
 lemma Star_string:
 assumes "s \<in> A\<star>"
 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"
 apply(auto)
 apply(rule_tac x="s1#ss" in exI)
 apply(simp)
 done
-lemma L_flat_Prf1:
-assumes "\<turnstile> v : r" shows "flat v \<in> L r"
-using assms
-apply(induct)
-apply(auto simp add: Sequ_def)
-apply(rule_tac x="Suc x" in bexI)
-apply(auto simp add: Sequ_def)[2]
-done
 lemma L_flat_Prf2:
 assumes "s \<in> L r" shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
 using assms
 apply(induct r arbitrary: s)
 using Prf.intros(3) flat.simps(4) apply blast
 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)")
 apply(auto)[1]
 apply(rule_tac x="Stars vs" in exI)
 apply(simp)
-apply (simp add: Prf_Stars)
+apply(rule Prf.intros)
-apply(drule Star_string)
+apply(simp)
-apply(auto)
+using Star_string Star_val apply force
-apply(rule Star_val)
-apply(auto)
 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)")
 apply(auto)[1]
 apply(rule_tac x="Stars vs" in exI)
 apply(simp)
-apply(drule_tac n="length vs" in Prf_Stars_UPNTIMES)
+apply(rule Prf.intros)
 apply(simp)
-using Prf_UPNTIMES_bigger apply blast
+apply(simp)
-apply(drule Star_Pow)
+using Star_Pow Star_val_length apply blast
-apply(auto)
-using Star_val_length apply blast
 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x2)")
 apply(auto)[1]
 apply(rule_tac x="Stars vs" in exI)
 apply(simp)
-apply(rule Prf_Stars_NTIMES)
+apply(rule Prf.intros)
 apply(simp)
 apply(simp)
-using Star_Pow Star_val_length by blast
+using Star_Pow Star_val_length apply blast
+apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)")
+apply(auto)[1]
+apply(rule_tac x="Stars vs" in exI)
+apply(simp)
+apply(rule Prf.intros)
+apply(simp)
+apply(simp)
+using Star_Pow Star_val_length apply blast
+done
 lemma L_flat_Prf:
 "L(r) = {flat v | v. \<turnstile> v : r}"
-using L_flat_Prf1 L_flat_Prf2 by blast
+using Prf_flat_L L_flat_Prf2 by blast
 section {* Sulzmann and Lu functions *}
 fun
 | "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) = Stars []"
 | "mkeps(UPNTIMES r n) = Stars []"
 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))"
+| "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))"
 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 where
 "injval (CHAR d) c Void = Char d"
 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
 | "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 (Stars vs)) = Stars ((injval r c v) # vs)"
 | "injval (UPNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
 | "injval (NTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
+| "injval (FROMNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
 section {* Mkeps, injval *}
 lemma mkeps_nullable:
 assumes "nullable(r)"
 shows "\<turnstile> mkeps r : r"
 using assms
 apply(induct r rule: mkeps.induct)
 apply(auto intro: Prf.intros)
-using Prf.intros(8) Prf_UPNTIMES_bigger apply blast
-apply(case_tac n)
-apply(auto)
-apply(rule Prf.intros)
-apply(rule Prf_Stars_NTIMES)
-apply(simp)
-apply(simp)
 done
 lemma mkeps_flat:
 assumes "nullable(r)"
 shows "flat (mkeps r) = []"
 apply(induct r arbitrary: c v rule: rexp.induct)
 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)
 (* STAR *)
 apply(rotate_tac 2)
 apply(erule Prf.cases)
-apply(simp_all)[7]
+apply(simp_all)
 apply(auto)
-apply (metis Prf.intros(6) Prf.intros(7))
+using Prf.intros(6) apply auto[1]
-apply (metis Prf.intros(7))
 (* UPNTIMES *)
 apply(case_tac x2)
 apply(simp)
 using Prf_elims(1) apply auto[1]
 apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)
 apply(clarify)
-apply(drule UPNTIMES_Stars)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
 apply(clarify)
-apply(simp)
+using Prf.intros(7) apply auto[1]
-apply(rule Prf.intros(9))
-apply(simp)
-using Prf_Stars_UPNTIMES Prf_UPNTIMES_bigger apply blast
 (* NTIMES *)
 apply(case_tac x2)
 apply(simp)
 using Prf_elims(1) apply auto[1]
 apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)
 apply(clarify)
-apply(drule NTIMES_Stars)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
 apply(clarify)
-apply(simp)
+using Prf.intros(8) apply auto[1]
-apply(rule Prf.intros)
+(* FROMNTIMES *)
-apply(simp)
+apply(case_tac x2)
-using Prf_Stars_NTIMES by blast
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(clarify)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(clarify)
+using Prf.intros(9) apply auto[1]
+apply(rotate_tac 1)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(clarify)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(clarify)
+using Prf.intros(9) by auto
 lemma Prf_injval_flat:
 assumes "\<turnstile> v : der c r"
 shows "flat (injval r c v) = c # (flat v)"
 using assms
 apply(auto elim!: Prf_elims split: if_splits)
 apply(metis mkeps_flat)
 apply(rotate_tac 2)
 apply(erule Prf.cases)
 apply(simp_all)
-apply(drule UPNTIMES_Stars)
+apply(rotate_tac 2)
-apply(clarify)
+apply(erule Prf.cases)
-apply(simp)
+apply(simp_all)
-apply(drule NTIMES_Stars)
+apply(rotate_tac 2)
-apply(clarify)
+apply(erule Prf.cases)
-apply(simp)
+apply(simp_all)
-done
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+done
 section {* Our Alternative Posix definition *}
 inductive
 | Posix_UPNTIMES2: "[] \<in> UPNTIMES r n \<rightarrow> Stars []"
 | Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r n \<rightarrow> Stars vs;
 \<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 (NTIMES r n))\<rbrakk>
 \<Longrightarrow> (s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> Stars (v # vs)"
 | Posix_NTIMES2: "[] \<in> NTIMES r 0 \<rightarrow> Stars []"
+| Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r n \<rightarrow> Stars vs;
+\<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 (FROMNTIMES r n))\<rbrakk>
+\<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> Stars (v # vs)"
+| Posix_FROMNTIMES2: "[] \<in> FROMNTIMES r 0 \<rightarrow> Stars []"
 inductive_cases Posix_elims:
 "s \<in> ZERO \<rightarrow> v"
 "s \<in> ONE \<rightarrow> v"
 "s \<in> CHAR c \<rightarrow> v"
 using assms
 apply (induct s r v rule: Posix.induct)
 apply(auto simp add: Sequ_def)
 apply(rule_tac x="Suc x" in bexI)
 apply(auto simp add: Sequ_def)
+apply(rule_tac x="Suc x" in bexI)
+apply(auto simp add: Sequ_def)
 done
 lemma Posix1a:
 assumes "s \<in> r \<rightarrow> v"
 shows "\<turnstile> v : r"
 using assms
 apply(induct s r v rule: Posix.induct)
 apply(auto intro: Prf.intros)
-using Prf.intros(8) Prf_UPNTIMES_bigger by blast
+apply(rule Prf.intros)
+apply(auto)[1]
-lemma Posix_NTIMES_length:
+apply(rotate_tac 3)
-assumes "s \<in> NTIMES r n \<rightarrow> Stars vs"
+apply(erule Prf.cases)
-shows "length vs = n"
+apply(simp_all)
-using assms
+apply(rule Prf.intros)
-using NTIMES_Stars Posix1a val.inject(5) by blast
+apply(auto)[1]
+apply(rotate_tac 3)
-lemma Posix_UPNTIMES_length:
+apply(erule Prf.cases)
-assumes "s \<in> UPNTIMES r n \<rightarrow> Stars vs"
+apply(simp_all)
-shows "length vs \<le> n"
+apply (smt Posix_UPNTIMES2 Posix_elims(2) Prf.simps le_0_eq le_Suc_eq length_0_conv nat_induct nullable.simps(3) nullable.simps(7) rexp.distinct(61) rexp.distinct(67) rexp.distinct(69) rexp.inject(5) val.inject(5) val.simps(29) val.simps(33) val.simps(35))
-using assms
+apply(rule Prf.intros)
-using Posix1a UPNTIMES_Stars val.inject(5) by blast
+apply(auto)[1]
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply (smt Prf.simps rexp.distinct(63) rexp.distinct(67) rexp.distinct(71) rexp.inject(6) val.distinct(17) val.distinct(9) val.inject(5) val.simps(29) val.simps(33) val.simps(35))
+apply(rule Prf.intros)
+apply(auto)[1]
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+using Prf.simps by blast
 lemma  Posix_NTIMES_mkeps:
 assumes "[] \<in> r \<rightarrow> mkeps r"
 shows "[] \<in> NTIMES r n \<rightarrow> Stars (replicate n (mkeps r))"
 apply(induct n)
 apply(subst append_Nil[symmetric])
 apply (rule Posix_NTIMES1)
 apply(auto)
 apply(rule assms)
 done
+lemma  Posix_FROMNTIMES_mkeps:
+assumes "[] \<in> r \<rightarrow> mkeps r"
+shows "[] \<in> FROMNTIMES r n \<rightarrow> Stars (replicate n (mkeps r))"
+apply(induct n)
+apply(simp)
+apply (rule Posix_FROMNTIMES2)
+apply(simp)
+apply(subst append_Nil[symmetric])
+apply (rule Posix_FROMNTIMES1)
+apply(auto)
+apply(rule assms)
+done
 lemma Posix_mkeps:
 assumes "nullable r"
 shows "[] \<in> r \<rightarrow> mkeps r"
 using assms
 apply(rule Posix.intros)
 apply(auto)
 apply(case_tac n)
 apply(simp)
 apply (simp add: Posix_NTIMES2)
+apply(simp)
+apply(subst append.simps(1)[symmetric])
+apply(rule Posix.intros)
+apply(auto)
 apply(rule Posix_NTIMES_mkeps)
+apply(simp)
+apply(case_tac n)
+apply(simp)
+apply (simp add: Posix_FROMNTIMES2)
+apply(simp)
+apply(subst append.simps(1)[symmetric])
+apply(rule Posix.intros)
+apply(auto)
+apply(rule Posix_FROMNTIMES_mkeps)
 apply(simp)
 done
 lemma Posix_determ:
 done
 moreover
 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
 "\<And>v2. s2 \<in> NTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
 ultimately show "Stars (v # vs) = v2" by auto
+next
+case (Posix_FROMNTIMES2 r v2)
+have "[] \<in> FROMNTIMES r 0 \<rightarrow> v2" by fact
+then show "Stars [] = v2" by cases (auto simp add: Posix1)
+next
+case (Posix_FROMNTIMES1 s1 r v s2 n vs v2)
+have "(s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> v2"
+"s1 \<in> r \<rightarrow> v" "s2 \<in> (FROMNTIMES r n) \<rightarrow> Stars vs"
+"\<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 (FROMNTIMES r n))" by fact+
+then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (FROMNTIMES r n) \<rightarrow> (Stars vs')"
+apply(cases) apply (auto simp add: append_eq_append_conv2)
+using Posix1(1) apply fastforce
+by (metis Posix1(1) Posix_FROMNTIMES1.hyps(5) append_Nil2 self_append_conv2)
+moreover
+have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+"\<And>v2. s2 \<in> FROMNTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+ultimately show "Stars (v # vs) = v2" by auto
 qed
+lemma NTIMES_Stars:
+assumes "\<turnstile> v : NTIMES r n"
+shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs = n"
+using assms
+apply(induct n arbitrary: v)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+done
+lemma UPNTIMES_Stars:
+assumes "\<turnstile> v : UPNTIMES r n"
+shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs \<le> n"
+using assms
+apply(induct n arbitrary: v)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+done
+lemma FROMNTIMES_Stars:
+assumes "\<turnstile> v : FROMNTIMES r n"
+shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> n \<le> length vs"
+using assms
+apply(induct n arbitrary: v)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+done
 lemma Posix_injval:
 assumes "s \<in> (der c r) \<rightarrow> v"
 shows "(c # s) \<in> r \<rightarrow> (injval r c v)"
 "\<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 (der c r) \<and> s\<^sub>4 \<in> L (UPNTIMES r m))"
 apply(case_tac n)
 apply(simp)
 using Posix_elims(1) apply blast
 apply(simp)
 apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)
 by (metis Posix1a UPNTIMES_Stars)
 then show "(c # s) \<in> UPNTIMES r n \<rightarrow> injval (UPNTIMES r n) c v"
 proof (cases)
 case cons
 have "n = Suc m" by fact
 apply(rule_tac Posix.intros(10))
 apply(simp_all)
 done
 then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" using cons by(simp)
 qed
+next
+case (FROMNTIMES r n)
+have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
+have "s \<in> der c (FROMNTIMES r n) \<rightarrow> v" by fact
+then consider
+(null) v1 vs s1 s2 where
+"v = Seq v1 (Stars vs)" "s = s1 @ s2"
+"s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r 0) \<rightarrow> (Stars vs)"
+"\<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 (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r 0))"
+| (cons) m v1 vs s1 s2 where
+"n = Suc m"
+"v = Seq v1 (Stars vs)" "s = s1 @ s2"
+"s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r m) \<rightarrow> (Stars vs)"
+"\<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 (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r m))"
+apply(case_tac n)
+apply(simp)
+apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)
+defer
+apply (metis FROMNTIMES_Stars Posix1a)
+apply(rotate_tac 5)
+apply(erule_tac Posix_elims(6))
+apply(auto)
+apply(drule_tac x="v1" in meta_spec)
+apply(simp)
+apply(drule_tac x="v # vs" in meta_spec)
+apply(simp)
+apply(drule_tac x="s1" in meta_spec)
+apply(simp)
+apply(drule_tac x="s1a @ s2a" in meta_spec)
+apply(simp)
+apply(drule meta_mp)
+defer
+using Pow_in_Star apply blast
+apply (meson Posix_FROMNTIMES2 append_is_Nil_conv self_append_conv)
+sorry
+then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v"
+proof (cases)
+case cons
+have "n = Suc m" by fact
+moreover
+have "s1 \<in> der c r \<rightarrow> v1" by fact
+then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+moreover
+have "s2 \<in> FROMNTIMES r m \<rightarrow> Stars vs" by fact
+moreover
+have "\<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 (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r m))" by fact
+then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (FROMNTIMES r m))"
+by (simp add: der_correctness Der_def)
+ultimately
+have "((c # s1) @ s2) \<in> FROMNTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)"
+apply(rule_tac Posix.intros(12))
+apply(simp_all)
+done
+then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp)
+qed
 qed
 section {* The Lexer by Sulzmann and Lu  *}

changeset 223	17c079699ea0
parent 222	4c02878e2fe0
child 224	624b4154325b