# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1488666429 0
# Node ID 80e7a94f6670a69f202f4934a98fd76c76cb1100
# Parent  81c85f2746f50521b4c7c93eae58cd5cc57d71b8
just for fun added the case for PLUS (was already proved as FROMNTIMES)

diff -r 81c85f2746f5 -r 80e7a94f6670 thys/LexerExt.thy
--- a/thys/LexerExt.thy	Sat Mar 04 21:35:12 2017 +0000
+++ b/thys/LexerExt.thy	Sat Mar 04 22:27:09 2017 +0000
@@ -216,6 +216,7 @@
 | NTIMES rexp nat
 | FROMNTIMES rexp nat
 | NMTIMES rexp nat nat
+| PLUS rexp
 
 section {* Semantics of Regular Expressions *}
  
@@ -232,6 +233,7 @@
 | "L (NTIMES r n) = (L r) \<up> n"
 | "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)"
 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" 
+| "L (PLUS r) = (\<Union>i\<in> {1..} . (L r) \<up> i)"
 
 section {* Nullable, Derivatives *}
 
@@ -248,6 +250,7 @@
 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)"
 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
+| "nullable (PLUS r) = (nullable r)"
 
 fun
  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -272,6 +275,7 @@
       else (if n = 0 then (if m = 0 then ZERO else 
                            SEQ (der c r) (UPNTIMES r (m - 1))) else 
                            SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" 
+| "der c (PLUS r) = SEQ (der c r) (STAR r)"
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -340,7 +344,23 @@
 apply(subst Sequ_UNION[symmetric])
 apply(subst test2[symmetric])
 apply(auto simp add: Der_UNION)[1]
-done
+(* PLUS *)
+apply(auto simp add: Sequ_def Star_def)[1]
+apply(simp add: Der_UNION)
+apply(rule_tac x="Suc xa" in bexI)
+apply(auto simp add: Sequ_def Der_def)[2]
+apply (metis append_Cons)
+apply(simp add: Der_UNION)
+apply(erule_tac bexE)
+apply(case_tac xa)
+apply(simp)
+apply(simp)
+apply(auto)
+apply(auto simp add: Sequ_def Der_def)[1]
+using Star_def apply auto[1]
+apply(case_tac "[] \<in> L r")
+apply(auto)
+using Der_UNION Der_star Star_def by fastforce
 
 lemma ders_correctness:
   shows "L (ders s r) = Ders s (L r)"
@@ -417,6 +437,8 @@
 | "\<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"
 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NMTIMES r n m"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> 1\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : PLUS r"
+
 
 inductive_cases Prf_elims:
   "\<turnstile> v : ZERO"
@@ -463,7 +485,7 @@
 apply(rule Prf_Pow)
 apply(simp)
 apply(simp)
-done
+using Prf_Pow by blast
 
 lemma Star_Pow:
   assumes "s \<in> A \<up> n"
@@ -554,6 +576,14 @@
 apply(simp)
 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 = 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:
@@ -574,6 +604,7 @@
 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))"
 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))"
 | "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))"
+| "mkeps(PLUS r) = Stars ([mkeps r])"
 
 
 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
@@ -589,7 +620,7 @@
 | "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)"
 | "injval (NMTIMES r n m) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
-
+| "injval (PLUS r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
 
 section {* Mkeps, injval *}
 
@@ -683,6 +714,12 @@
 apply(rule Prf.intros)
 apply(auto)[2]
 apply simp
+(* PLUS *)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)
+using Prf.intros apply auto[1]
 done
 
 
@@ -714,6 +751,9 @@
 apply(rotate_tac 4)
 apply(erule Prf.cases)
 apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
 done
 
 
@@ -749,6 +789,9 @@
     \<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; 
+    \<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:
@@ -772,6 +815,10 @@
 apply(simp add: Star_def)
 apply(rule_tac x="Suc x" in bexI)
 apply(auto simp add: Sequ_def)
+apply(simp add: Star_def)
+apply(clarify)
+apply(rule_tac x="Suc x" in bexI)
+apply(auto simp add: Sequ_def)
 done
 
 
@@ -833,6 +880,11 @@
 apply(simp_all)
 apply(erule Prf.cases)
 apply(simp_all)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rule Prf.intros)
+apply(auto)
 done
 
 
@@ -927,6 +979,10 @@
 apply(auto)
 apply(rule Posix_NMTIMES_mkeps)
 apply(auto)
+apply(subst append_Nil[symmetric])
+apply(rule Posix.intros)
+apply(auto)
+apply(rule Posix.intros)
 done
 
 
@@ -1072,6 +1128,19 @@
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> NMTIMES r n m \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
   ultimately show "Stars (v # vs) = v2" by auto
+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"
+       "\<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)
+  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+
+  ultimately show "Stars (v # vs) = v2" by auto
 qed
 
 lemma NTIMES_Stars:
@@ -1107,6 +1176,14 @@
 apply(simp_all)
 done
 
+lemma PLUS_Stars:
+ assumes "\<turnstile> v : PLUS r"
+ shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> 1 \<le> length vs"
+using assms
+apply(erule_tac Prf.cases)
+apply(simp_all)
+done
+
 lemma NMTIMES_Stars:
  assumes "\<turnstile> v : NMTIMES r n m"
  shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> n \<le> length vs \<and> length vs \<le> m"
@@ -1452,6 +1529,40 @@
         apply(simp)
         apply(simp add: der_correctness Der_def)
         done
+next 
+  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
 qed