--- a/thys/LexerExt.thy Tue Feb 28 00:26:34 2017 +0000
+++ b/thys/LexerExt.thy Tue Feb 28 13:35:12 2017 +0000
@@ -159,6 +159,7 @@
| STAR rexp
| UPNTIMES rexp nat
| NTIMES rexp nat
+| FROMNTIMES rexp nat
section {* Semantics of Regular Expressions *}
@@ -173,7 +174,7 @@
| "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 *}
@@ -188,6 +189,7 @@
| "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"
@@ -205,7 +207,8 @@
| "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"
@@ -306,8 +309,17 @@
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)"
@@ -379,14 +391,10 @@
| "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
| "\<turnstile> Void : ONE"
| "\<turnstile> Char c : CHAR c"
-| "\<turnstile> Stars [] : STAR r"
-| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
-| "\<turnstile> Stars [] : UPNTIMES r 0"
-| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : UPNTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : UPNTIMES r (Suc 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)"
-
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : STAR r"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<le> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r n"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs = n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NTIMES r n"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : FROMNTIMES r n"
inductive_cases Prf_elims:
"\<turnstile> v : ZERO"
@@ -396,68 +404,39 @@
"\<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_tac x="Suc x" in bexI)
-apply(auto simp add: Sequ_def)[2]
-done
-
-lemma Prf_Stars:
- assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
- shows "\<turnstile> Stars vs : STAR r"
-using assms
-by(induct vs) (auto intro: Prf.intros)
-
-lemma Prf_Stars_NTIMES:
- 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)
+apply(rule Prf_STAR)
+apply(simp)
+apply(rule_tac x="length vs" in bexI)
+apply(rule Prf_Pow)
+apply(simp)
+apply(simp)
+apply(rule Prf_Pow)
+apply(simp)
+apply(rule_tac x="length vs" in bexI)
+apply(rule Prf_Pow)
+apply(simp)
+apply(simp)
done
lemma Star_string:
@@ -502,14 +481,6 @@
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"
@@ -523,34 +494,38 @@
apply(auto)[1]
apply(rule_tac x="Stars vs" in exI)
apply(simp)
-apply (simp add: Prf_Stars)
-apply(drule Star_string)
-apply(auto)
-apply(rule Star_val)
-apply(auto)
+apply(rule Prf.intros)
+apply(simp)
+using Star_string Star_val apply force
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(drule Star_Pow)
-apply(auto)
-using Star_val_length apply blast
+apply(simp)
+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 = 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 *}
@@ -564,7 +539,7 @@
| "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
@@ -577,7 +552,7 @@
| "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 *}
@@ -587,13 +562,6 @@
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:
@@ -612,10 +580,9 @@
(* 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))
-apply (metis Prf.intros(7))
+using Prf.intros(6) apply auto[1]
(* UPNTIMES *)
apply(case_tac x2)
apply(simp)
@@ -624,12 +591,11 @@
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)
-apply(rule Prf.intros(9))
-apply(simp)
-using Prf_Stars_UPNTIMES Prf_UPNTIMES_bigger apply blast
+using Prf.intros(7) apply auto[1]
(* NTIMES *)
apply(case_tac x2)
apply(simp)
@@ -638,12 +604,32 @@
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)
+using Prf.intros(8) apply auto[1]
+(* FROMNTIMES *)
+apply(case_tac x2)
apply(simp)
-apply(rule Prf.intros)
-apply(simp)
-using Prf_Stars_NTIMES by blast
+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"
@@ -655,16 +641,21 @@
apply(rotate_tac 2)
apply(erule Prf.cases)
apply(simp_all)
-apply(drule UPNTIMES_Stars)
-apply(clarify)
-apply(simp)
-apply(drule NTIMES_Stars)
-apply(clarify)
-apply(simp)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+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
@@ -689,7 +680,10 @@
\<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"
@@ -707,6 +701,8 @@
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
@@ -716,20 +712,29 @@
using assms
apply(induct s r v rule: Posix.induct)
apply(auto intro: Prf.intros)
-using Prf.intros(8) Prf_UPNTIMES_bigger by blast
-
-lemma Posix_NTIMES_length:
- assumes "s \<in> NTIMES r n \<rightarrow> Stars vs"
- shows "length vs = n"
-using assms
-using NTIMES_Stars Posix1a val.inject(5) by blast
-
-lemma Posix_UPNTIMES_length:
- assumes "s \<in> UPNTIMES r n \<rightarrow> Stars vs"
- shows "length vs \<le> n"
-using assms
-using Posix1a UPNTIMES_Stars val.inject(5) by blast
-
+apply(rule Prf.intros)
+apply(auto)[1]
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rule Prf.intros)
+apply(auto)[1]
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+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))
+apply(rule Prf.intros)
+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"
@@ -744,6 +749,20 @@
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"
@@ -756,8 +775,21 @@
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
@@ -861,8 +893,58 @@
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"
@@ -1025,7 +1107,7 @@
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)
+ 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)
@@ -1087,6 +1169,61 @@
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
--- a/thys/ROOT Tue Feb 28 00:26:34 2017 +0000
+++ b/thys/ROOT Tue Feb 28 13:35:12 2017 +0000
@@ -1,6 +1,7 @@
session "Lex" = HOL +
theories [document = false]
- "Lexer"
+ "Lexer"
+ "LexerExt"
"Simplifying"
"Sulzmann"