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
shows "\<turnstile> ((snd (simp r)) v) : r \<longleftrightarrow> \<turnstile> v : (fst (simp r))"
using assms
apply(induct r arbitrary: v rule: simp.induct)
apply(auto intro: Prf.intros)
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(auto)
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)
apply(auto split: if_splits)
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