# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1489780062 0
# Node ID 2dc1647eab9eceb3ce966d79ddbeaeb00e043b36
# Parent  3cbd19ecdc9dcfd8c46ff1d953365d0ed3330bbe
added AND-regular expression (intersection/conjunction)

diff -r 3cbd19ecdc9d -r 2dc1647eab9e progs/scala/re-basic.scala
--- a/progs/scala/re-basic.scala	Mon Mar 13 14:54:12 2017 +0000
+++ b/progs/scala/re-basic.scala	Fri Mar 17 19:47:42 2017 +0000
@@ -4,6 +4,7 @@
 import scala.language.reflectiveCalls
 import scala.annotation.tailrec   
 import scala.io.Source
+import scala.util._
 
 abstract class Rexp 
 case object ZERO extends Rexp
@@ -141,7 +142,7 @@
   case c::cs => inj(r, c, lex(der(c, r), cs))
 }
 
-def lexing(r: Rexp, s: String) : Val = lex(r, s.toList)
+def lexing(r: Rexp, s: String) : Try[Val] = Try(lex(r, s.toList))
 
 // Examples
 
diff -r 3cbd19ecdc9d -r 2dc1647eab9e thys/LexerExt.thy
--- a/thys/LexerExt.thy	Mon Mar 13 14:54:12 2017 +0000
+++ b/thys/LexerExt.thy	Fri Mar 17 19:47:42 2017 +0000
@@ -67,6 +67,11 @@
 unfolding Der_def Sequ_def
 by (auto simp add: Cons_eq_append_conv)
 
+lemma Der_inter [simp]:
+  shows "Der c (A \<inter> B) = Der c A \<inter> Der c B"
+unfolding Der_def
+by auto
+
 lemma Der_union [simp]:
   shows "Der c (A \<union> B) = Der c A \<union> Der c B"
 unfolding Der_def
@@ -217,6 +222,7 @@
 | FROMNTIMES rexp nat
 | NMTIMES rexp nat nat
 | PLUS rexp
+| AND rexp rexp
 
 section {* Semantics of Regular Expressions *}
  
@@ -234,6 +240,7 @@
 | "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)"
+| "L (AND r1 r2) = (L r1) \<inter> (L r2)"
 
 section {* Nullable, Derivatives *}
 
@@ -251,6 +258,7 @@
 | "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)"
+| "nullable (AND r1 r2) = (nullable r1 \<and> nullable r2)"
 
 fun
  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -276,6 +284,7 @@
                            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)"
+| "der c (AND r1 r2) = AND (der c r1) (der c r2)"
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -402,7 +411,7 @@
 | Right val
 | Left val
 | Stars "val list"
-
+| And val val
 
 section {* The string behind a value *}
 
@@ -416,6 +425,7 @@
 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
 | "flat (Stars []) = []"
 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" 
+| "flat (And v1 v2) = flat v1"
 
 lemma flat_Stars [simp]:
  "flat (Stars vs) = concat (map flat vs)"
@@ -438,6 +448,7 @@
 | "\<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"
+| "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2; flat v1 = flat v2\<rbrakk> \<Longrightarrow> \<turnstile> And v1 v2: AND r1 r2"
 
 
 inductive_cases Prf_elims:
@@ -584,7 +595,8 @@
 apply(simp)
 apply(simp)
 using Star_Pow Star_val_length apply blast
-done
+(* AND *)
+using Prf.intros(12) by fastforce
 
 lemma L_flat_Prf:
   "L(r) = {flat v | v. \<turnstile> v : r}"
@@ -605,6 +617,7 @@
 | "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])"
+| "mkeps(AND r1 r2) = And (mkeps r1) (mkeps r2)"
 
 
 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
@@ -621,17 +634,10 @@
 | "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)"
+| "injval (AND r1 r2) c (And v1 v2) = And (injval r1 c v1) (injval r2 c v2)"
 
 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)
-by (metis Prf.intros(10) in_set_replicate length_replicate not_le order_refl)
-
 lemma mkeps_flat:
   assumes "nullable(r)" 
   shows "flat (mkeps r) = []"
@@ -640,6 +646,52 @@
 apply(auto)
 by meson
 
+lemma mkeps_nullable:
+  assumes "nullable(r)" 
+  shows "\<turnstile> mkeps r : r"
+using assms
+apply(induct r rule: mkeps.induct) 
+apply(auto intro: Prf.intros)
+apply(metis Prf.intros(10) in_set_replicate length_replicate not_le order_refl)
+apply(rule Prf.intros)
+apply(simp_all add: mkeps_flat)
+done
+
+lemma Prf_injval_flat:
+  assumes "\<turnstile> v : der c r" 
+  shows "flat (injval r c v) = c # (flat v)"
+using assms
+apply(induct arbitrary: v rule: der.induct)
+apply(auto elim!: Prf_elims split: if_splits)
+apply(metis mkeps_flat)
+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)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 4)
+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
 
 lemma Prf_injval:
   assumes "\<turnstile> v : der c r" 
@@ -720,41 +772,18 @@
 apply(simp_all)
 apply(auto)
 using Prf.intros apply auto[1]
+(* AND *)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)
+apply(rule Prf.intros)
+apply(simp)
+apply(simp)
+apply(simp add: Prf_injval_flat)
 done
 
 
-lemma Prf_injval_flat:
-  assumes "\<turnstile> v : der c r" 
-  shows "flat (injval r c v) = c # (flat v)"
-using assms
-apply(induct arbitrary: v rule: der.induct)
-apply(auto elim!: Prf_elims split: if_splits)
-apply(metis mkeps_flat)
-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)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(rotate_tac 3)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(rotate_tac 4)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)
-done
+
 
 
 section {* Our Alternative Posix definition *}
@@ -792,6 +821,7 @@
 | 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)"
+| Posix_AND: "\<lbrakk>s \<in> r1 \<rightarrow> v1; s \<in> r2 \<rightarrow> v2\<rbrakk> \<Longrightarrow> s \<in> (AND r1 r2) \<rightarrow> (And v1 v2)"
 
 inductive_cases Posix_elims:
   "s \<in> ZERO \<rightarrow> v"
@@ -926,7 +956,9 @@
 apply(simp_all)
 apply(rule Prf.intros)
 apply(auto)
-done
+apply(rule Prf.intros)
+apply(auto)
+by (simp add: Posix1(2))
 
 
 lemma  Posix_NTIMES_mkeps:
@@ -1181,6 +1213,17 @@
   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
+next 
+  case (Posix_AND s r1 v1 r2 v2 v')
+  have "s \<in> AND r1 r2 \<rightarrow> v'" 
+       "s \<in> r1 \<rightarrow> v1" "s \<in> r2 \<rightarrow> v2" by fact+
+  then obtain v1' v2' where "v' = And v1' v2'" "s \<in> r1 \<rightarrow> v1'" "s \<in> r2 \<rightarrow> v2'"
+  apply(cases) apply (auto simp add: append_eq_append_conv2)
+  done
+  moreover
+  have IHs: "\<And>v1'. s \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'"
+            "\<And>v2'. s \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+
+  ultimately show "And v1 v2 = v'" by simp
 qed
 
 lemma NTIMES_Stars:
@@ -1605,6 +1648,17 @@
   apply(simp)
   apply(simp)
   done  
+next
+  case (AND r1 r2)
+  then show ?case
+  apply -
+  apply(erule Posix.cases)
+  apply(simp_all)
+  apply(auto)
+  apply(rule Posix.intros)
+  apply(simp)
+  apply(simp)
+  done
 qed