diff -r ff0844860981 -r e866678c29cb thys/ReStar.thy
--- a/thys/ReStar.thy	Tue Mar 08 00:45:09 2016 +0000
+++ b/thys/ReStar.thy	Tue Mar 08 05:03:47 2016 +0000
@@ -797,6 +797,51 @@
 apply(simp)
 done
 
+fun F_RIGHT where
+  "F_RIGHT f v = Right (f v)"
 
+fun F_LEFT where
+  "F_LEFT f v = Left (f v)"
+
+fun F_ALT where
+  "F_ALT f1 f2 (Right v) = Right (f2 v)"
+| "F_ALT f1 f2 (Left v) = Left (f1 v)" 
+
+fun F_SEQ1 where
+  "F_SEQ1 f1 f2 v = Seq (f1 Void) (f2 v)"
+
+fun F_SEQ2 where 
+  "F_SEQ2 f1 f2 v = Seq (f1 v) (f2 Void)"
+
+fun F_SEQ where 
+  "F_SEQ f1 f2 (Seq v1 v2) = Seq (f1 v1) (f2 v2)"
+
+fun simp_ALT where
+  "simp_ALT (ZERO, _) (r2, f2) = (r2, F_RIGHT f2)"
+| "simp_ALT (r1, f1) (ZERO, _) = (r1, F_LEFT f1)"
+| "simp_ALT (r1, f1) (r2, f2) = (ALT r1 r2, F_ALT f1 f2)"
+
+fun simp_SEQ where
+  "simp_SEQ (ONE, f1) (r2, f2) = (r2, F_SEQ1 f1 f2)"
+| "simp_SEQ (r1, f1) (ONE, f2) = (r1, F_SEQ2 f1 f2)"
+| "simp_SEQ (ZERO, f1) (r2, f2) = (ZERO, f1)"
+| "simp_SEQ (r1, f1) (ZERO, f2) = (ZERO, f2)"
+| "simp_SEQ (r1, f1) (r2, f2) = (SEQ r1 r2, F_SEQ f1 f2)"  
+ 
+fun 
+  simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)"
+where
+  "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)" 
+| "simp (SEQ r1 r2) = simp_SEQ (simp r1) (simp r2)" 
+| "simp r = (r, id)"
+
+fun 
+  matcher3 :: "rexp \<Rightarrow> string \<Rightarrow> val option"
+where
+  "matcher3 r [] = (if nullable r then Some(mkeps r) else None)"
+| "matcher3 r (c#s) = (let (rs, fr) = simp (der c r) in
+                         (case (matcher3 rs s) of  
+                            None \<Rightarrow> None
+                          | Some(v) \<Rightarrow> Some(injval r c (fr v))))"
 
 end
\ No newline at end of file