theory Simplifying

  imports "ReStar" 

begin

section {* Lexer including simplifications *}

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 f\<^sub>1 f\<^sub>2 (Right v) = Right (f\<^sub>2 v)"

| "F_ALT f\<^sub>1 f\<^sub>2 (Left v) = Left (f\<^sub>1 v)"  

| "F_ALT f1 f2 v = v"

fun F_SEQ1 where

  "F_SEQ1 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 Void) (f\<^sub>2 v)"

fun F_SEQ2 where 

  "F_SEQ2 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 v) (f\<^sub>2 Void)"

fun F_SEQ where 

  "F_SEQ f\<^sub>1 f\<^sub>2 (Seq v\<^sub>1 v\<^sub>2) = Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"

| "F_SEQ f1 f2 v = v"

fun simp_ALT where

  "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)"

| "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)"

| "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)"

fun simp_SEQ where

  "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)"

| "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)"

| "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)"  

lemma simp_SEQ_simps[simp]:

  "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2))

                    else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2))

                    else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))"

by (induct p1 p2 rule: simp_SEQ.induct) (auto)

lemma simp_ALT_simps[simp]:

  "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2))

                    else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1))

                    else (ALT (fst p1) (fst p2), F_ALT (snd p1) (snd p2))))"

by (induct p1 p2 rule: simp_ALT.induct) (auto)

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 

  slexer :: "rexp \<Rightarrow> string \<Rightarrow> val option"

where

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

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

                         (case (slexer rs s) of  

                            None \<Rightarrow> None

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

lemma L_fst_simp:

  shows "L(r) = L(fst (simp r))"

using assms

by (induct r) (auto)

lemma Posix_simp:

  assumes "s \<in> (fst (simp r)) \<rightarrow> v" 

  shows "s \<in> r \<rightarrow> ((snd (simp r)) v)"

using assms

apply(auto)[1]

apply(simp)

apply(auto)[1]

apply(auto)

lemma slexer_correctness:

  shows "slexer r s = lexer r s"

end