--- a/thys/LexerExt.thy Tue Mar 07 00:24:10 2017 +0000
+++ b/thys/LexerExt.thy Wed Mar 08 10:32:51 2017 +0000
@@ -789,11 +789,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 (NMTIMES r n m))\<rbrakk>
\<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)"
| Posix_NMTIMES2: "s \<in> UPNTIMES r m \<rightarrow> Stars vs \<Longrightarrow> s \<in> NMTIMES r 0 m \<rightarrow> Stars vs"
-| Posix_PLUS1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs;
+| Posix_PLUS1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (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 (STAR r))\<rbrakk>
\<Longrightarrow> (s1 @ s2) \<in> PLUS r \<rightarrow> Stars (v # vs)"
-
inductive_cases Posix_elims:
"s \<in> ZERO \<rightarrow> v"
"s \<in> ONE \<rightarrow> v"
@@ -822,6 +821,48 @@
done
+lemma
+ "([] @ []) \<in> PLUS (ONE) \<rightarrow> Stars ([Void])"
+apply(rule Posix_PLUS1)
+apply(rule Posix.intros)
+apply(rule Posix.intros)
+apply(simp)
+apply(simp)
+done
+
+lemma
+ assumes "s \<in> r \<rightarrow> v" "flat v \<noteq> []" "\<forall>s' \<in> L r. length s' < length s"
+ shows "([] @ (s @ [])) \<in> PLUS (ALT ONE r) \<rightarrow> Stars ([Left Void, Right v])"
+using assms
+oops
+
+lemma
+ "([] @ ([] @ [])) \<in> FROMNTIMES (ONE) (Suc (Suc 0)) \<rightarrow> Stars ([Void, Void])"
+apply(rule Posix.intros)
+apply(rule Posix.intros)
+apply(rule Posix.intros)
+apply(rule Posix.intros)
+apply(rule Posix.intros)
+apply(rule Posix.intros)
+apply(auto)
+done
+
+
+lemma
+ assumes "s \<in> r \<rightarrow> v" "flat v \<noteq> []"
+ "s \<in> PLUS (ALT ONE r) \<rightarrow> Stars ([Left(Void), Right(v)])"
+ shows "False"
+using assms
+apply(rotate_tac 2)
+apply(erule_tac Posix.cases)
+apply(simp_all)
+apply(auto)
+oops
+
+
+
+
+
lemma Posix1a:
assumes "s \<in> r \<rightarrow> v"
shows "\<turnstile> v : r"
@@ -1131,12 +1172,12 @@
next
case (Posix_PLUS1 s1 r v s2 vs v2)
have "(s1 @ s2) \<in> PLUS r \<rightarrow> v2"
- "s1 \<in> r \<rightarrow> v" "s2 \<in> (STAR r) \<rightarrow> Stars vs"
+ "s1 \<in> r \<rightarrow> v" "s2 \<in> (STAR r) \<rightarrow> Stars vs" (*"flat v = [] \<Longrightarrow> flat (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 (STAR r))" by fact+
then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')"
apply(cases) apply (auto simp add: append_eq_append_conv2)
using Posix1(1) apply fastforce
- by (metis Posix1(1) Posix_PLUS1.hyps(5) append_Nil2 self_append_conv2)
+ by (metis Posix1(1) Posix_PLUS1.hyps(6) append_self_conv append_self_conv2)
moreover
have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
"\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
@@ -1533,36 +1574,32 @@
case (PLUS r)
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 (PLUS r) \<rightarrow> v" by fact
- then consider
- (cons) v1 vs s1 s2 where
- "v = Seq v1 (Stars vs)" "s = s1 @ s2"
- "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<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 (STAR r))"
- apply(simp)
- apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)
- defer
- apply(rotate_tac 3)
- apply(erule_tac Posix_elims(6))
- apply (simp add: Posix.intros(6))
- using Posix.intros(7) by blast
- then show "(c # s) \<in> PLUS r \<rightarrow> injval (PLUS r) c v"
- proof (cases)
- case cons
- 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> STAR r \<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 (STAR r))" 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 (STAR r))"
- by (simp add: der_correctness Der_def)
- ultimately
- have "((c # s1) @ s2) \<in> (PLUS r) \<rightarrow> Stars (injval r c v1 # vs)"
- apply(rule_tac Posix.intros)
- apply(simp_all)
- done
- then show "(c # s) \<in> PLUS r \<rightarrow> injval (PLUS r) c v" using cons by(simp)
- qed
+ then show "(c # s) \<in> PLUS r \<rightarrow> injval (PLUS r) c v"
+ apply -
+ apply(erule Posix.cases)
+ apply(simp_all)
+ apply(auto)
+ apply(rotate_tac 3)
+ apply(erule Posix.cases)
+ apply(simp_all)
+ apply(subst append_Cons[symmetric])
+ apply(rule Posix.intros)
+ using PLUS.hyps apply auto[1]
+ apply(rule Posix.intros)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ using Posix1a Prf_injval_flat apply auto[1]
+ apply(simp add: der_correctness Der_def)
+ apply(subst append_Nil2[symmetric])
+ apply(rule Posix.intros)
+ using PLUS.hyps apply auto[1]
+ apply(rule Posix.intros)
+ apply(simp)
+ apply(simp)
+ done
qed
@@ -1602,5 +1639,8 @@
using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce
using Posix1(1) lexer_correct_None lexer_correct_Some by blast
+value "lexer (PLUS (ALT ONE (SEQ (CHAR (CHR ''a'')) (CHAR (CHR ''b''))))) [CHR ''a'', CHR ''b'']"
+
+
unused_thms
end
\ No newline at end of file