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 slexer_better_simp:
  "slexer r (c#s) = (case (slexer (fst (simp (der c r))) s) of  
                            None \<Rightarrow> None
                          | Some(v) \<Rightarrow> Some(injval r c ((snd (simp (der c r))) v)))"
by (auto split: prod.split option.split)


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(induct r arbitrary: s v rule: simp.induct)
apply(simp_all)
apply(auto)[1]
using Posix_elims(1) apply blast
apply (simp add: Posix_ALT1)
apply (metis L.simps(1) L_fst_simp Posix_ALT2 empty_iff)
apply (smt F_ALT.simps(1) F_ALT.simps(2) L_fst_simp Posix_ALT1 Posix_ALT2 Posix_elims(4))
apply(auto)[1]
apply (metis (no_types, lifting) Nil_is_append_conv Posix_SEQ Posix_elims(2))
apply(subst append_Nil2[symmetric])
apply(rule Posix_SEQ)
apply(simp)
using Posix_ONE apply blast
apply blast
apply(subst append_Nil[symmetric])
apply(rule Posix_SEQ)
using Posix_ONE apply blast
apply blast
apply(auto)[1]
apply (metis L.simps(2) L_fst_simp ex_in_conv insert_iff)
apply(erule Posix_elims)
apply(auto)
using L_fst_simp Posix_SEQ by auto


lemma slexer_correctness:
  shows "slexer r s = lexer r s"
proof(induct s arbitrary: r)
  case Nil
  show "slexer r [] = lexer r []" by simp
next 
  case (Cons c s r)
  have IH: "\<And>r. slexer r s = lexer r s" by fact
  show "slexer r (c # s) = lexer r (c # s)" 
   proof (cases "s \<in> L (der c r)")
     case True
       assume a1: "s \<in> L (der c r)"
       then obtain v1 where a2: "lexer (der c r) s = Some v1" "s \<in> der c r \<rightarrow> v1"
         using lexer_correct_Some by auto
       from a1 have "s \<in> L (fst (simp (der c r)))" using L_fst_simp[symmetric] by simp
       then obtain v2 where a3: "lexer (fst (simp (der c r))) s = Some v2" "s \<in> (fst (simp (der c r))) \<rightarrow> v2"
          using lexer_correct_Some by auto
       then have a4: "slexer (fst (simp (der c r))) s = Some v2" using IH by simp
       from a3(2) have "s \<in> der c r \<rightarrow> (snd (simp (der c r))) v2" using Posix_simp by simp
       with a2(2) have "v1 = (snd (simp (der c r))) v2" using Posix_determ by simp
       with a2(1) a4 show "slexer r (c # s) = lexer r (c # s)" by (auto split: prod.split)
     next 
     case False
       assume b1: "s \<notin> L (der c r)"
       then have "lexer (der c r) s = None" using lexer_correct_None by simp
       moreover
       from b1 have "s \<notin> L (fst (simp (der c r)))" using L_fst_simp[symmetric] by simp
       then have "lexer (fst (simp (der c r))) s = None" using lexer_correct_None by simp
       then have "slexer (fst (simp (der c r))) s = None" using IH by simp
       ultimately show "slexer r (c # s) = lexer r (c # s)" 
         by (simp del: slexer.simps add: slexer_better_simp)
   qed
qed  

end