800 

   800 fun F_RIGHT where

   801   "F_RIGHT f v = Right (f v)"

   802 

   803 fun F_LEFT where

   804   "F_LEFT f v = Left (f v)"

   805 

   806 fun F_ALT where

   807   "F_ALT f1 f2 (Right v) = Right (f2 v)"

   808 | "F_ALT f1 f2 (Left v) = Left (f1 v)" 

   809 

   810 fun F_SEQ1 where

   811   "F_SEQ1 f1 f2 v = Seq (f1 Void) (f2 v)"

   812 

   813 fun F_SEQ2 where 

   814   "F_SEQ2 f1 f2 v = Seq (f1 v) (f2 Void)"

   815 

   816 fun F_SEQ where 

   817   "F_SEQ f1 f2 (Seq v1 v2) = Seq (f1 v1) (f2 v2)"

   818 

   819 fun simp_ALT where

   820   "simp_ALT (ZERO, _) (r2, f2) = (r2, F_RIGHT f2)"

   821 | "simp_ALT (r1, f1) (ZERO, _) = (r1, F_LEFT f1)"

   822 | "simp_ALT (r1, f1) (r2, f2) = (ALT r1 r2, F_ALT f1 f2)"

   823 

   824 fun simp_SEQ where

   825   "simp_SEQ (ONE, f1) (r2, f2) = (r2, F_SEQ1 f1 f2)"

   826 | "simp_SEQ (r1, f1) (ONE, f2) = (r1, F_SEQ2 f1 f2)"

   827 | "simp_SEQ (ZERO, f1) (r2, f2) = (ZERO, f1)"

   828 | "simp_SEQ (r1, f1) (ZERO, f2) = (ZERO, f2)"

   829 | "simp_SEQ (r1, f1) (r2, f2) = (SEQ r1 r2, F_SEQ f1 f2)"  

   830  

   831 fun 

   832   simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)"

   833 where

   834   "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)" 

   835 | "simp (SEQ r1 r2) = simp_SEQ (simp r1) (simp r2)" 

   836 | "simp r = (r, id)"

   837 

   838 fun 

   839   matcher3 :: "rexp \<Rightarrow> string \<Rightarrow> val option"

   840 where

   841   "matcher3 r [] = (if nullable r then Some(mkeps r) else None)"

   842 | "matcher3 r (c#s) = (let (rs, fr) = simp (der c r) in

   843                          (case (matcher3 rs s) of  

   844                             None \<Rightarrow> None

   845                           | Some(v) \<Rightarrow> Some(injval r c (fr v))))"