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)"  

  "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))))"

  "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))))"

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

lemma 

  shows "\<turnstile> ((snd (simp r)) v) : r \<longleftrightarrow> \<turnstile> v : (fst (simp r))"

using assms

apply(induct r arbitrary: v rule: simp.induct)

using Prf_elims(3) apply blast

apply(erule Prf_elims)

apply(simp)

apply(clarify)

apply(blast)

apply(simp)

apply(erule Prf_elims)

apply(simp)

apply(simp)

apply(clarify)

apply(blast)

apply(erule Prf_elims)

apply(case_tac v)

apply(simp_all)

apply(rule Prf.intros)

apply(clarify)

apply(simp)

apply(case_tac v)

apply(simp_all)

apply(rule Prf.intros)

apply(clarify)

apply(simp)

apply(erule Prf_elims)

apply(simp)

apply(rule Prf.intros)

apply(simp)

apply(simp)

apply(rule Prf.intros)

apply(simp)

apply(erule Prf_elims)

apply(simp)

apply(blast)

apply(rule Prf.intros)

apply(erule Prf_elims)

apply(simp)

apply(rule Prf.intros)

apply(erule Prf_elims)

apply(simp)

apply(rule Prf.intros)

apply(erule Prf_elims)

apply(simp)

apply(clarify)

apply(blast)

apply(rule Prf.intros)

apply(blast)

using Prf.intros(4) apply blast

apply(erule Prf_elims)

apply(simp)

apply(clarify)

apply(blast)

apply(rule Prf.intros)

using Prf.intros(4) apply blast

apply blast

apply(erule Prf_elims)

apply(case_tac v)

apply(simp_all)

apply(rule Prf.intros)

apply(clarify)

apply(simp)

apply(clarify)

apply(blast)

apply(erule Prf_elims)

apply(case_tac v)

apply(simp_all)

apply(rule Prf.intros)

apply(clarify)

apply(simp)

apply(simp)

done

lemma Posix_simp_nullable:

  assumes "nullable r" "[] \<in> (fst (simp r)) \<rightarrow> v"

  shows "((snd (simp r)) v) = mkeps r"

using assms 

apply(induct r arbitrary: v)

apply(erule Posix_elims)

apply(simp)

apply(erule Posix_elims)

apply(clarify)

using Posix.intros(1) apply blast

using Posix.intros(1) apply blast

using Posix.intros(1) apply blast

apply(erule Posix_elims)

apply(simp)

apply(erule Posix_elims)

apply (metis L_fst_simp nullable.simps(1) nullable_correctness)

apply(erule Posix_elims)

apply(clarify)

apply(simp)

apply(clarify)

apply(simp)

apply(simp only: L_fst_simp[symmetric])

apply (simp add: nullable_correctness)

apply(erule Posix_elims)

using L_fst_simp Posix1(1) nullable_correctness apply blast

apply (metis L.simps(1) L_fst_simp Prf_flat_L empty_iff mkeps_nullable)

apply(erule Posix_elims)

apply(clarify)

apply(simp)

apply(simp only: L_fst_simp[symmetric])

apply (simp add: nullable_correctness)

apply(erule Posix_elims)

apply(clarify)

apply(simp)

using L_fst_simp Posix1(1) nullable_correctness apply blast

apply(simp)

apply(erule Posix_elims)

apply(clarify)

apply(simp)

using Posix1(2) apply auto[1]

apply(simp)

done

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: rexp.induct) 

prefer 3

apply(erule Posix_elims)

apply(clarify)

apply(simp)

apply(rule Posix.intros)

apply(blast)

apply(blast)

apply(auto)[1]

apply(simp add: L_fst_simp[symmetric])

apply(auto)[1]

prefer 3

apply(rule Posix.intros)

apply(blast)

apply (metis L.simps(1) L_fst_simp equals0D)

prefer 3

apply(rule Posix.intros)

apply(blast)

prefer 3

apply(erule Posix_elims)

apply(clarify)

apply(simp)

apply(rule Posix.intros)

apply(blast)

apply(simp)

apply(rule Posix.intros)

apply(blast)

apply(simp add: L_fst_simp[symmetric])

apply(subst append.simps[symmetric])

apply(rule Posix.intros)

prefer 2

apply(blast)

prefer 2

apply(auto)[1]

apply (metis L_fst_simp Posix_elims(2) lexer_correct_Some)

apply(subst Posix_simp_nullable)

using Posix.intros(1) Posix1(1) nullable_correctness apply blast

apply(simp)

apply(rule Posix.intros)

apply(rule Posix_mkeps)

using Posix.intros(1) Posix1(1) nullable_correctness apply blast

apply(subst append_Nil2[symmetric])

apply(rule Posix.intros)

apply(blast)

apply(subst Posix_simp_nullable)

using Posix.intros(1) Posix1(1) nullable_correctness apply blast

apply(simp)

apply(rule Posix.intros)

apply(rule Posix_mkeps)

using Posix.intros(1) Posix1(1) nullable_correctness apply blast

apply(auto)

done

lemma slexer_correctness:

  shows "slexer r s = lexer r s"

apply(induct s arbitrary: r)

apply(simp)

apply(auto split: option.split prod.split)

apply (metis L_fst_simp fst_conv lexer_correct_None)

using L_fst_simp lexer_correct_None apply fastforce

by (metis Posix_determ Posix_simp fst_conv lexer_correct_None lexer_correct_Some option.distinct(1) option.inject snd_conv)

end