theory SizeBoundStrong
imports "Lexer"
begin
section \<open>Bit-Encodings\<close>
datatype bit = Z | S
fun code :: "val \<Rightarrow> bit list"
where
"code Void = []"
| "code (Char c) = []"
| "code (Left v) = Z # (code v)"
| "code (Right v) = S # (code v)"
| "code (Seq v1 v2) = (code v1) @ (code v2)"
| "code (Stars []) = [S]"
| "code (Stars (v # vs)) = (Z # code v) @ code (Stars vs)"
fun
Stars_add :: "val \<Rightarrow> val \<Rightarrow> val"
where
"Stars_add v (Stars vs) = Stars (v # vs)"
function
decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)"
where
"decode' ds ZERO = (Void, [])"
| "decode' ds ONE = (Void, ds)"
| "decode' ds (CH d) = (Char d, ds)"
| "decode' [] (ALT r1 r2) = (Void, [])"
| "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
| "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
| "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in
let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))"
| "decode' [] (STAR r) = (Void, [])"
| "decode' (S # ds) (STAR r) = (Stars [], ds)"
| "decode' (Z # ds) (STAR r) = (let (v, ds') = decode' ds r in
let (vs, ds'') = decode' ds' (STAR r)
in (Stars_add v vs, ds''))"
by pat_completeness auto
lemma decode'_smaller:
assumes "decode'_dom (ds, r)"
shows "length (snd (decode' ds r)) \<le> length ds"
using assms
apply(induct ds r)
apply(auto simp add: decode'.psimps split: prod.split)
using dual_order.trans apply blast
by (meson dual_order.trans le_SucI)
termination "decode'"
apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))")
apply(auto dest!: decode'_smaller)
by (metis less_Suc_eq_le snd_conv)
definition
decode :: "bit list \<Rightarrow> rexp \<Rightarrow> val option"
where
"decode ds r \<equiv> (let (v, ds') = decode' ds r
in (if ds' = [] then Some v else None))"
lemma decode'_code_Stars:
assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> (\<forall>x. decode' (code v @ x) r = (v, x)) \<and> flat v \<noteq> []"
shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)"
using assms
apply(induct vs)
apply(auto)
done
lemma decode'_code:
assumes "\<Turnstile> v : r"
shows "decode' ((code v) @ ds) r = (v, ds)"
using assms
apply(induct v r arbitrary: ds)
apply(auto)
using decode'_code_Stars by blast
lemma decode_code:
assumes "\<Turnstile> v : r"
shows "decode (code v) r = Some v"
using assms unfolding decode_def
by (smt append_Nil2 decode'_code old.prod.case)
section {* Annotated Regular Expressions *}
datatype arexp =
AZERO
| AONE "bit list"
| ACHAR "bit list" char
| ASEQ "bit list" arexp arexp
| AALTs "bit list" "arexp list"
| ASTAR "bit list" arexp
abbreviation
"AALT bs r1 r2 \<equiv> AALTs bs [r1, r2]"
fun asize :: "arexp \<Rightarrow> nat" where
"asize AZERO = 1"
| "asize (AONE cs) = 1"
| "asize (ACHAR cs c) = 1"
| "asize (AALTs cs rs) = Suc (sum_list (map asize rs))"
| "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)"
| "asize (ASTAR cs r) = Suc (asize r)"
fun
erase :: "arexp \<Rightarrow> rexp"
where
"erase AZERO = ZERO"
| "erase (AONE _) = ONE"
| "erase (ACHAR _ c) = CH c"
| "erase (AALTs _ []) = ZERO"
| "erase (AALTs _ [r]) = (erase r)"
| "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
| "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
| "erase (ASTAR _ r) = STAR (erase r)"
fun nonalt :: "arexp \<Rightarrow> bool"
where
"nonalt (AALTs bs2 rs) = False"
| "nonalt r = True"
fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
"fuse bs AZERO = AZERO"
| "fuse bs (AONE cs) = AONE (bs @ cs)"
| "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"
| "fuse bs (AALTs cs rs) = AALTs (bs @ cs) rs"
| "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"
| "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"
lemma fuse_append:
shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)"
apply(induct r)
apply(auto)
done
lemma fuse_Nil:
shows "fuse [] r = r"
by (induct r)(simp_all)
lemma map_fuse_Nil:
shows "map (fuse []) rs = rs"
by (induct rs)(simp_all add: fuse_Nil)
fun intern :: "rexp \<Rightarrow> arexp" where
"intern ZERO = AZERO"
| "intern ONE = AONE []"
| "intern (CH c) = ACHAR [] c"
| "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1))
(fuse [S] (intern r2))"
| "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
| "intern (STAR r) = ASTAR [] (intern r)"
fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
"retrieve (AONE bs) Void = bs"
| "retrieve (ACHAR bs c) (Char d) = bs"
| "retrieve (AALTs bs [r]) v = bs @ retrieve r v"
| "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"
| "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"
| "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
| "retrieve (ASTAR bs r) (Stars []) = bs @ [S]"
| "retrieve (ASTAR bs r) (Stars (v#vs)) =
bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"
fun
bnullable :: "arexp \<Rightarrow> bool"
where
"bnullable (AZERO) = False"
| "bnullable (AONE bs) = True"
| "bnullable (ACHAR bs c) = False"
| "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"
| "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)"
| "bnullable (ASTAR bs r) = True"
fun
bmkeps :: "arexp \<Rightarrow> bit list"
where
"bmkeps(AONE bs) = bs"
| "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)"
| "bmkeps(AALTs bs [r]) = bs @ (bmkeps r)"
| "bmkeps(AALTs bs (r#rs)) = (if bnullable(r) then bs @ (bmkeps r) else (bmkeps (AALTs bs rs)))"
| "bmkeps(ASTAR bs r) = bs @ [S]"
fun
bder :: "char \<Rightarrow> arexp \<Rightarrow> arexp"
where
"bder c (AZERO) = AZERO"
| "bder c (AONE bs) = AZERO"
| "bder c (ACHAR bs d) = (if c = d then AONE bs else AZERO)"
| "bder c (AALTs bs rs) = AALTs bs (map (bder c) rs)"
| "bder c (ASEQ bs r1 r2) =
(if bnullable r1
then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2))
else ASEQ bs (bder c r1) r2)"
| "bder c (ASTAR bs r) = ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)"
fun
bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
where
"bders r [] = r"
| "bders r (c#s) = bders (bder c r) s"
lemma bders_append:
"bders r (s1 @ s2) = bders (bders r s1) s2"
apply(induct s1 arbitrary: r s2)
apply(simp_all)
done
lemma bnullable_correctness:
shows "nullable (erase r) = bnullable r"
apply(induct r rule: erase.induct)
apply(simp_all)
done
lemma erase_fuse:
shows "erase (fuse bs r) = erase r"
apply(induct r rule: erase.induct)
apply(simp_all)
done
lemma erase_intern [simp]:
shows "erase (intern r) = r"
apply(induct r)
apply(simp_all add: erase_fuse)
done
lemma erase_bder [simp]:
shows "erase (bder a r) = der a (erase r)"
apply(induct r rule: erase.induct)
apply(simp_all add: erase_fuse bnullable_correctness)
done
lemma erase_bders [simp]:
shows "erase (bders r s) = ders s (erase r)"
apply(induct s arbitrary: r )
apply(simp_all)
done
lemma bnullable_fuse:
shows "bnullable (fuse bs r) = bnullable r"
apply(induct r arbitrary: bs)
apply(auto)
done
lemma retrieve_encode_STARS:
assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v"
shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)"
using assms
apply(induct vs)
apply(simp_all)
done
lemma retrieve_fuse2:
assumes "\<Turnstile> v : (erase r)"
shows "retrieve (fuse bs r) v = bs @ retrieve r v"
using assms
apply(induct r arbitrary: v bs)
apply(auto elim: Prf_elims)[4]
defer
using retrieve_encode_STARS
apply(auto elim!: Prf_elims)[1]
apply(case_tac vs)
apply(simp)
apply(simp)
(* AALTs case *)
apply(simp)
apply(case_tac x2a)
apply(simp)
apply(auto elim!: Prf_elims)[1]
apply(simp)
apply(case_tac list)
apply(simp)
apply(auto)
apply(auto elim!: Prf_elims)[1]
done
lemma retrieve_fuse:
assumes "\<Turnstile> v : r"
shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v"
using assms
by (simp_all add: retrieve_fuse2)
lemma retrieve_code:
assumes "\<Turnstile> v : r"
shows "code v = retrieve (intern r) v"
using assms
apply(induct v r )
apply(simp_all add: retrieve_fuse retrieve_encode_STARS)
done
lemma bnullable_Hdbmkeps_Hd:
assumes "bnullable a"
shows "bmkeps (AALTs bs (a # rs)) = bs @ (bmkeps a)"
using assms
by (metis bmkeps.simps(3) bmkeps.simps(4) list.exhaust)
lemma r1:
assumes "\<not> bnullable a" "bnullable (AALTs bs rs)"
shows "bmkeps (AALTs bs (a # rs)) = bmkeps (AALTs bs rs)"
using assms
apply(induct rs)
apply(auto)
done
lemma r2:
assumes "x \<in> set rs" "bnullable x"
shows "bnullable (AALTs bs rs)"
using assms
apply(induct rs)
apply(auto)
done
lemma r3:
assumes "\<not> bnullable r"
" \<exists> x \<in> set rs. bnullable x"
shows "retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs))) =
retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))"
using assms
apply(induct rs arbitrary: r bs)
apply(auto)[1]
apply(auto)
using bnullable_correctness apply blast
apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)
apply(subst retrieve_fuse2[symmetric])
apply (smt bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable)
apply(simp)
apply(case_tac "bnullable a")
apply (smt append_Nil2 bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) fuse.simps(4) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable retrieve_fuse2)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="bs" in meta_spec)
apply(drule meta_mp)
apply(simp)
apply(drule meta_mp)
apply(auto)
apply(subst retrieve_fuse2[symmetric])
apply(case_tac rs)
apply(simp)
apply(auto)[1]
apply (simp add: bnullable_correctness)
apply (metis append_Nil2 bnullable_correctness erase_fuse fuse.simps(4) list.set_intros(1) mkeps.simps(3) mkeps_nullable nullable.simps(4) r2)
apply (simp add: bnullable_correctness)
apply (metis append_Nil2 bnullable_correctness erase.simps(6) erase_fuse fuse.simps(4) list.set_intros(2) mkeps.simps(3) mkeps_nullable r2)
apply(simp)
done
lemma t:
assumes "\<forall>r \<in> set rs. nullable (erase r) \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))"
"nullable (erase (AALTs bs rs))"
shows " bmkeps (AALTs bs rs) = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
using assms
apply(induct rs arbitrary: bs)
apply(simp)
apply(auto simp add: bnullable_correctness)
apply(case_tac rs)
apply(auto simp add: bnullable_correctness)[2]
apply(subst r1)
apply(simp)
apply(rule r2)
apply(assumption)
apply(simp)
apply(drule_tac x="bs" in meta_spec)
apply(drule meta_mp)
apply(auto)[1]
prefer 2
apply(case_tac "bnullable a")
apply(subst bnullable_Hdbmkeps_Hd)
apply blast
apply(subgoal_tac "nullable (erase a)")
prefer 2
using bnullable_correctness apply blast
apply (metis (no_types, lifting) erase.simps(5) erase.simps(6) list.exhaust mkeps.simps(3) retrieve.simps(3) retrieve.simps(4))
apply(subst r1)
apply(simp)
using r2 apply blast
apply(drule_tac x="bs" in meta_spec)
apply(drule meta_mp)
apply(auto)[1]
apply(simp)
using r3 apply blast
apply(auto)
using r3 by blast
lemma bmkeps_retrieve:
assumes "nullable (erase r)"
shows "bmkeps r = retrieve r (mkeps (erase r))"
using assms
apply(induct r)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
defer
apply(simp)
apply(rule t)
apply(auto)
done
lemma bder_retrieve:
assumes "\<Turnstile> v : der c (erase r)"
shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"
using assms
apply(induct r arbitrary: v rule: erase.induct)
apply(simp)
apply(erule Prf_elims)
apply(simp)
apply(erule Prf_elims)
apply(simp)
apply(case_tac "c = ca")
apply(simp)
apply(erule Prf_elims)
apply(simp)
apply(simp)
apply(erule Prf_elims)
apply(simp)
apply(erule Prf_elims)
apply(simp)
apply(simp)
apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v)
apply(erule Prf_elims)
apply(simp)
apply(simp)
apply(case_tac rs)
apply(simp)
apply(simp)
apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq)
apply(simp)
apply(case_tac "nullable (erase r1)")
apply(simp)
apply(erule Prf_elims)
apply(subgoal_tac "bnullable r1")
prefer 2
using bnullable_correctness apply blast
apply(simp)
apply(erule Prf_elims)
apply(simp)
apply(subgoal_tac "bnullable r1")
prefer 2
using bnullable_correctness apply blast
apply(simp)
apply(simp add: retrieve_fuse2)
apply(simp add: bmkeps_retrieve)
apply(simp)
apply(erule Prf_elims)
apply(simp)
using bnullable_correctness apply blast
apply(rename_tac bs r v)
apply(simp)
apply(erule Prf_elims)
apply(clarify)
apply(erule Prf_elims)
apply(clarify)
apply(subst injval.simps)
apply(simp del: retrieve.simps)
apply(subst retrieve.simps)
apply(subst retrieve.simps)
apply(simp)
apply(simp add: retrieve_fuse2)
done
lemma MAIN_decode:
assumes "\<Turnstile> v : ders s r"
shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r"
using assms
proof (induct s arbitrary: v rule: rev_induct)
case Nil
have "\<Turnstile> v : ders [] r" by fact
then have "\<Turnstile> v : r" by simp
then have "Some v = decode (retrieve (intern r) v) r"
using decode_code retrieve_code by auto
then show "Some (flex r id [] v) = decode (retrieve (bders (intern r) []) v) r"
by simp
next
case (snoc c s v)
have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow>
Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact
have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact
then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r"
by (simp add: Prf_injval ders_append)
have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))"
by (simp add: flex_append)
also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r"
using asm2 IH by simp
also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r"
using asm by (simp_all add: bder_retrieve ders_append)
finally show "Some (flex r id (s @ [c]) v) =
decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append)
qed
definition blex where
"blex a s \<equiv> if bnullable (bders a s) then Some (bmkeps (bders a s)) else None"
definition blexer where
"blexer r s \<equiv> if bnullable (bders (intern r) s) then
decode (bmkeps (bders (intern r) s)) r else None"
lemma blexer_correctness:
shows "blexer r s = lexer r s"
proof -
{ define bds where "bds \<equiv> bders (intern r) s"
define ds where "ds \<equiv> ders s r"
assume asm: "nullable ds"
have era: "erase bds = ds"
unfolding ds_def bds_def by simp
have mke: "\<Turnstile> mkeps ds : ds"
using asm by (simp add: mkeps_nullable)
have "decode (bmkeps bds) r = decode (retrieve bds (mkeps ds)) r"
using bmkeps_retrieve
using asm era by (simp add: bmkeps_retrieve)
also have "... = Some (flex r id s (mkeps ds))"
using mke by (simp_all add: MAIN_decode ds_def bds_def)
finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))"
unfolding bds_def ds_def .
}
then show "blexer r s = lexer r s"
unfolding blexer_def lexer_flex
apply(subst bnullable_correctness[symmetric])
apply(simp)
done
qed
fun distinctBy :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a list"
where
"distinctBy [] f acc = []"
| "distinctBy (x#xs) f acc =
(if (f x) \<in> acc then distinctBy xs f acc
else x # (distinctBy xs f ({f x} \<union> acc)))"
(*filter (\<lambda>rt. case rt of
SEQ r1p r2p \<Rightarrow> r2p = (erase r2)
r \<Rightarrow> False ) allowableTerms*)
lemma dB_single_step:
shows "distinctBy (a#rs) f {} = a # distinctBy rs f {f a}"
by simp
fun flts :: "arexp list \<Rightarrow> arexp list"
where
"flts [] = []"
| "flts (AZERO # rs) = flts rs"
| "flts ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
| "flts (r1 # rs) = r1 # flts rs"
fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
where
"bsimp_ASEQ _ AZERO _ = AZERO"
| "bsimp_ASEQ _ _ AZERO = AZERO"
| "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"
| "bsimp_ASEQ bs1 r1 r2 = ASEQ bs1 r1 r2"
fun bsimp_AALTs :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
where
"bsimp_AALTs _ [] = AZERO"
| "bsimp_AALTs bs1 [r] = fuse bs1 r"
| "bsimp_AALTs bs1 rs = AALTs bs1 rs"
fun bsimp_ASEQ1 :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
where
"bsimp_ASEQ1 _ AZERO _ = AZERO"
| "bsimp_ASEQ1 bs (AONE bs1) r2 = fuse (bs @ bs1) r2"
| "bsimp_ASEQ1 bs r1 r2 = ASEQ bs r1 r2"
fun collect where
\<open>collect _ [] = []\<close>
| \<open>collect erasedR2 ((SEQ r1 r2) # rs) = (if r2 = erasedR2 then r1 # (collect erasedR2 rs)
else collect erasedR2 rs)\<close>
| \<open>collect erasedR2 (r # rs) = collect erasedR2 rs\<close>
fun pruneRexp where
\<open>pruneRexp (ASEQ bs r1 r2) allowableTerms =
( let termsTruncated = (collect (erase r2) allowableTerms) in (let pruned = pruneRexp r1 termsTruncated in (bsimp_ASEQ1 bs pruned r2)) )\<close>
| \<open>pruneRexp (AALTs bs rs) allowableTerms = (let rsp = (filter (\<lambda>r. r \<noteq> AZERO) (map (\<lambda>r. pruneRexp r allowableTerms) rs) ) in bsimp_AALTs bs rsp )
\<close>
| \<open>pruneRexp r allowableTerms = (if (erase r) \<in> (set allowableTerms) then r else AZERO)\<close>
fun oneSimp :: \<open>rexp \<Rightarrow> rexp\<close> where
\<open> oneSimp (SEQ ONE r) = r \<close>
| \<open> oneSimp (SEQ r1 r2) = SEQ (oneSimp r1) r2 \<close>
| \<open> oneSimp r = r \<close>
fun breakIntoTerms where
\<open>breakIntoTerms (SEQ r1 r2) = map (\<lambda>r1p. SEQ r1p r2) (breakIntoTerms r1)\<close>
| \<open>breakIntoTerms (ALT r1 r2) = (breakIntoTerms r1) @ (breakIntoTerms r2)\<close>
| \<open>breakIntoTerms r = r # [] \<close>
fun addToAcc :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp list"
where
\<open>addToAcc r acc = filter (\<lambda>r1. oneSimp r1 \<notin> set acc) (breakIntoTerms (erase r)) \<close>
fun dBStrong :: "arexp list \<Rightarrow> rexp list \<Rightarrow> arexp list"
where
"dBStrong [] acc = []"
| "dBStrong (r # rs) acc = (if (erase r) \<in> (set acc) then dBStrong rs acc
else (case (pruneRexp r (addToAcc r acc)) of
AZERO \<Rightarrow> dBStrong rs ((addToAcc r acc) @ acc) |
r1 \<Rightarrow> r1 # (dBStrong rs ((addToAcc r acc) @ acc))
)
)
"
fun bsimpStrong :: "arexp \<Rightarrow> arexp "
where
"bsimpStrong (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimpStrong r1) (bsimpStrong r2)"
| "bsimpStrong (AALTs bs1 rs) = bsimp_AALTs bs1 (dBStrong (flts (map bsimpStrong rs)) []) "
| "bsimpStrong r = r"
fun bdersStrong :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
where
"bdersStrong r [] = r"
| "bdersStrong r (c # s) = bdersStrong (bsimpStrong (bder c r)) s"
definition blexerStrong where
"blexerStrong r s \<equiv> if bnullable (bdersStrong (intern r) s) then
decode (bmkeps (bdersStrong (intern r) s)) r else None"
fun bsimp :: "arexp \<Rightarrow> arexp"
where
"bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"
| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {}) "
| "bsimp r = r"
fun
bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
where
"bders_simp r [] = r"
| "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s"
definition blexer_simp where
"blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then
decode (bmkeps (bders_simp (intern r) s)) r else None"
export_code bders_simp in Scala module_name Example
lemma bders_simp_append:
shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"
apply(induct s1 arbitrary: r s2)
apply(simp_all)
done
lemma L_bsimp_ASEQ:
"L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
apply(simp_all)
by (metis erase_fuse fuse.simps(4))
lemma L_bsimp_AALTs:
"L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))"
apply(induct bs rs rule: bsimp_AALTs.induct)
apply(simp_all add: erase_fuse)
done
lemma L_erase_AALTs:
shows "L (erase (AALTs bs rs)) = \<Union> (L ` erase ` (set rs))"
apply(induct rs)
apply(simp)
apply(simp)
apply(case_tac rs)
apply(simp)
apply(simp)
done
lemma L_erase_flts:
shows "\<Union> (L ` erase ` (set (flts rs))) = \<Union> (L ` erase ` (set rs))"
apply(induct rs rule: flts.induct)
apply(simp_all)
apply(auto)
using L_erase_AALTs erase_fuse apply auto[1]
by (simp add: L_erase_AALTs erase_fuse)
lemma L_erase_dB_acc:
shows "( \<Union>(L ` acc) \<union> ( \<Union> (L ` erase ` (set (distinctBy rs erase acc) ) ) )) = \<Union>(L ` acc) \<union> \<Union> (L ` erase ` (set rs))"
apply(induction rs arbitrary: acc)
apply simp
apply simp
by (smt (z3) SUP_absorb UN_insert sup_assoc sup_commute)
lemma L_erase_dB:
shows " ( \<Union> (L ` erase ` (set (distinctBy rs erase {}) ) ) ) = \<Union> (L ` erase ` (set rs))"
by (metis L_erase_dB_acc Un_commute Union_image_empty)
lemma L_bsimp_erase:
shows "L (erase r) = L (erase (bsimp r))"
apply(induct r)
apply(simp)
apply(simp)
apply(simp)
apply(auto simp add: Sequ_def)[1]
apply(subst L_bsimp_ASEQ[symmetric])
apply(auto simp add: Sequ_def)[1]
apply(subst (asm) L_bsimp_ASEQ[symmetric])
apply(auto simp add: Sequ_def)[1]
apply(simp)
apply(subst L_bsimp_AALTs[symmetric])
defer
apply(simp)
apply(subst (2)L_erase_AALTs)
apply(subst L_erase_dB)
apply(subst L_erase_flts)
apply(auto)
apply (simp add: L_erase_AALTs)
using L_erase_AALTs by blast
lemma bsimp_ASEQ0:
shows "bsimp_ASEQ bs r1 AZERO = AZERO"
apply(induct r1)
apply(auto)
done
lemma bsimp_ASEQ1:
assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2"
using assms
apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
apply(auto)
done
lemma bsimp_ASEQ2:
shows "bsimp_ASEQ bs (AONE bs1) r2 = fuse (bs @ bs1) r2"
apply(induct r2)
apply(auto)
done
lemma L_bders_simp:
shows "L (erase (bders_simp r s)) = L (erase (bders r s))"
apply(induct s arbitrary: r rule: rev_induct)
apply(simp)
apply(simp)
apply(simp add: ders_append)
apply(simp add: bders_simp_append)
apply(simp add: L_bsimp_erase[symmetric])
by (simp add: der_correctness)
lemma b2:
assumes "bnullable r"
shows "bmkeps (fuse bs r) = bs @ bmkeps r"
by (simp add: assms bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)
lemma b4:
shows "bnullable (bders_simp r s) = bnullable (bders r s)"
by (metis L_bders_simp bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
lemma qq1:
assumes "\<exists>r \<in> set rs. bnullable r"
shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs)"
using assms
apply(induct rs arbitrary: rs1 bs)
apply(simp)
apply(simp)
by (metis Nil_is_append_conv bmkeps.simps(4) neq_Nil_conv bnullable_Hdbmkeps_Hd split_list_last)
lemma qq2:
assumes "\<forall>r \<in> set rs. \<not> bnullable r" "\<exists>r \<in> set rs1. bnullable r"
shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs1)"
using assms
apply(induct rs arbitrary: rs1 bs)
apply(simp)
apply(simp)
by (metis append_assoc in_set_conv_decomp r1 r2)
lemma qq3:
assumes "bnullable (AALTs bs (rs @ rs1))"
"bnullable (AALTs bs (rs @ rs2))"
"\<lbrakk>bnullable (AALTs bs rs1); bnullable (AALTs bs rs2); \<forall>r\<in>set rs. \<not>bnullable r\<rbrakk> \<Longrightarrow>
bmkeps (AALTs bs rs1) = bmkeps (AALTs bs rs2)"
shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs (rs @ rs2))"
using assms
apply(case_tac "\<exists>r \<in> set rs. bnullable r")
using qq1 apply auto[1]
by (metis UnE bnullable.simps(4) qq2 set_append)
lemma flts_append:
shows "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
by (induct xs1 arbitrary: xs2 rule: flts.induct)(auto)
lemma k0a:
shows "flts [AALTs bs rs] = map (fuse bs) rs"
apply(simp)
done
lemma bbbbs1:
shows "nonalt r \<or> (\<exists>bs rs. r = AALTs bs rs)"
using nonalt.elims(3) by auto
fun nonazero :: "arexp \<Rightarrow> bool"
where
"nonazero AZERO = False"
| "nonazero r = True"
lemma flts_single1:
assumes "nonalt r" "nonazero r"
shows "flts [r] = [r]"
using assms
apply(induct r)
apply(auto)
done
lemma q3a:
assumes "\<exists>r \<in> set rs. bnullable r"
shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)"
using assms
apply(induct rs arbitrary: bs bs1)
apply(simp)
apply(simp)
apply(auto)
apply (metis append_assoc b2 bnullable_correctness erase_fuse bnullable_Hdbmkeps_Hd)
apply(case_tac "bnullable a")
apply (metis append.assoc b2 bnullable_correctness erase_fuse bnullable_Hdbmkeps_Hd)
apply(case_tac rs)
apply(simp)
apply(simp)
apply(auto)[1]
apply (metis bnullable_correctness erase_fuse)+
done
lemma qq4:
assumes "\<exists>x\<in>set list. bnullable x"
shows "\<exists>x\<in>set (flts list). bnullable x"
using assms
apply(induct list rule: flts.induct)
apply(auto)
by (metis UnCI bnullable_correctness erase_fuse imageI)
lemma qs3:
assumes "\<exists>r \<in> set rs. bnullable r"
shows "bmkeps (AALTs bs rs) = bmkeps (AALTs bs (flts rs))"
using assms
apply(induct rs arbitrary: bs taking: size rule: measure_induct)
apply(case_tac x)
apply(simp)
apply(simp)
apply(case_tac a)
apply(simp)
apply (simp add: r1)
apply(simp)
apply (simp add: bnullable_Hdbmkeps_Hd)
apply(simp)
apply(case_tac "flts list")
apply(simp)
apply (metis L_erase_AALTs L_erase_flts L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(4) mkeps_nullable r2)
apply(simp)
apply (simp add: r1)
prefer 3
apply(simp)
apply (simp add: bnullable_Hdbmkeps_Hd)
prefer 2
apply(simp)
apply(case_tac "\<exists>x\<in>set x52. bnullable x")
apply(case_tac "list")
apply(simp)
apply (metis b2 fuse.simps(4) q3a r2)
apply(erule disjE)
apply(subst qq1)
apply(auto)[1]
apply (metis bnullable_correctness erase_fuse)
apply(simp)
apply (metis b2 fuse.simps(4) q3a r2)
apply(simp)
apply(auto)[1]
apply(subst qq1)
apply (metis bnullable_correctness erase_fuse image_eqI set_map)
apply (metis b2 fuse.simps(4) q3a r2)
apply(subst qq1)
apply (metis bnullable_correctness erase_fuse image_eqI set_map)
apply (metis b2 fuse.simps(4) q3a r2)
apply(simp)
apply(subst qq2)
apply (metis bnullable_correctness erase_fuse imageE set_map)
prefer 2
apply(case_tac "list")
apply(simp)
apply(simp)
apply (simp add: qq4)
apply(simp)
apply(auto)
apply(case_tac list)
apply(simp)
apply(simp)
apply (simp add: bnullable_Hdbmkeps_Hd)
apply(case_tac "bnullable (ASEQ x41 x42 x43)")
apply(case_tac list)
apply(simp)
apply(simp)
apply (simp add: bnullable_Hdbmkeps_Hd)
apply(simp)
using qq4 r1 r2 by auto
lemma bder_fuse:
shows "bder c (fuse bs a) = fuse bs (bder c a)"
apply(induct a arbitrary: bs c)
apply(simp_all)
done
inductive
rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
where
"ASEQ bs AZERO r2 \<leadsto> AZERO"
| "ASEQ bs r1 AZERO \<leadsto> AZERO"
| "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r"
| "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"
| "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"
| "r \<leadsto> r' \<Longrightarrow> (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto> (AALTs bs (rs1 @ [r'] @ rs2))"
(*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
| "AALTs bs (rsa@ [AZERO] @ rsb) \<leadsto> AALTs bs (rsa @ rsb)"
| "AALTs bs (rsa@ [AALTs bs1 rs1] @ rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)"
| "AALTs bs [] \<leadsto> AZERO"
| "AALTs bs [r] \<leadsto> fuse bs r"
| "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)"
inductive
rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
where
rs1[intro, simp]:"r \<leadsto>* r"
| rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
inductive
srewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto>* _" [100, 100] 100)
where
ss1: "[] s\<leadsto>* []"
| ss2: "\<lbrakk>r \<leadsto>* r'; rs s\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) s\<leadsto>* (r'#rs')"
(* rewrites for lists *)
inductive
frewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ f\<leadsto>* _" [100, 100] 100)
where
fs1: "[] f\<leadsto>* []"
| fs2: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (AZERO#rs) f\<leadsto>* rs'"
| fs3: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> ((AALTs bs rs1) # rs) f\<leadsto>* ((map (fuse bs) rs1) @ rs')"
| fs4: "\<lbrakk>rs f\<leadsto>* rs'; nonalt r; nonazero r\<rbrakk> \<Longrightarrow> (r#rs) f\<leadsto>* (r#rs')"
lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
using rrewrites.intros(1) rrewrites.intros(2) by blast
lemma real_trans[trans]:
assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3"
shows "r1 \<leadsto>* r3"
using a2 a1
apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct)
apply(auto)
done
lemma many_steps_later: "\<lbrakk>r1 \<leadsto> r2; r2 \<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
by (meson r_in_rstar real_trans)
lemma contextrewrites1: "r \<leadsto>* r' \<Longrightarrow> (AALTs bs (r#rs)) \<leadsto>* (AALTs bs (r'#rs))"
apply(induct r r' rule: rrewrites.induct)
apply simp
by (metis append_Cons append_Nil rrewrite.intros(6) rs2)
lemma contextrewrites2: "r \<leadsto>* r' \<Longrightarrow> (AALTs bs (rs1@[r]@rs)) \<leadsto>* (AALTs bs (rs1@[r']@rs))"
apply(induct r r' rule: rrewrites.induct)
apply simp
using rrewrite.intros(6) by blast
lemma srewrites_alt: "rs1 s\<leadsto>* rs2 \<Longrightarrow> (AALTs bs (rs@rs1)) \<leadsto>* (AALTs bs (rs@rs2))"
apply(induct rs1 rs2 arbitrary: bs rs rule: srewrites.induct)
apply(rule rs1)
apply(drule_tac x = "bs" in meta_spec)
apply(drule_tac x = "rsa@[r']" in meta_spec)
apply simp
apply(rule real_trans)
prefer 2
apply(assumption)
apply(drule contextrewrites2)
apply auto
done
corollary srewrites_alt1:
assumes "rs1 s\<leadsto>* rs2"
shows "AALTs bs rs1 \<leadsto>* AALTs bs rs2"
using assms
by (metis append.left_neutral srewrites_alt)
lemma star_seq:
assumes "r1 \<leadsto>* r2"
shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3"
using assms
apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct)
apply(auto intro: rrewrite.intros)
done
lemma star_seq2:
assumes "r3 \<leadsto>* r4"
shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r1 r4"
using assms
apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct)
apply(auto intro: rrewrite.intros)
done
lemma continuous_rewrite:
assumes "r1 \<leadsto>* AZERO"
shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
using assms
apply(induction ra\<equiv>"r1" rb\<equiv>"AZERO" arbitrary: bs1 r1 r2 rule: rrewrites.induct)
apply(auto intro: rrewrite.intros r_in_rstar star_seq)
by (meson rrewrite.intros(1) rs2 star_seq)
lemma bsimp_aalts_simpcases:
shows "AONE bs \<leadsto>* bsimp (AONE bs)"
and "AZERO \<leadsto>* bsimp AZERO"
and "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)"
by (simp_all)
lemma trivialbsimp_srewrites:
"\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
apply(induction rs)
apply simp
apply(rule ss1)
by (metis insert_iff list.simps(15) list.simps(9) srewrites.simps)
lemma bsimp_AALTs_rewrites:
"AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
apply(induction rs)
apply simp
apply(rule r_in_rstar)
using rrewrite.intros(9) apply blast
by (metis bsimp_AALTs.elims list.discI rrewrite.intros(10) rrewrites.simps)
lemma flts_prepend: "\<lbrakk>nonalt a; nonazero a\<rbrakk> \<Longrightarrow> flts (a#rs) = a # (flts rs)"
by (metis append_Cons append_Nil flts_single1 flts_append)
lemma fltsfrewrites: "rs f\<leadsto>* (flts rs)"
apply(induction rs)
apply simp
apply(rule fs1)
apply(case_tac "a = AZERO")
using fs2 apply auto[1]
apply(case_tac "\<exists>bs rs. a = AALTs bs rs")
apply(erule exE)+
apply (simp add: fs3)
apply(subst flts_prepend)
apply(rule nonalt.elims(2))
prefer 2
thm nonalt.elims
apply blast
using bbbbs1 apply blast
apply(simp)+
apply (meson nonazero.elims(3))
by (meson fs4 nonalt.elims(3) nonazero.elims(3))
lemma rrewrite0away: "AALTs bs (AZERO # rsb) \<leadsto> AALTs bs rsb"
by (metis append_Cons append_Nil rrewrite.intros(7))
lemma frewritesaalts:"rs f\<leadsto>* rs' \<Longrightarrow> (AALTs bs (rs1@rs)) \<leadsto>* (AALTs bs (rs1@rs'))"
apply(induct rs rs' arbitrary: bs rs1 rule:frewrites.induct)
apply(rule rs1)
apply(drule_tac x = "bs" in meta_spec)
apply(drule_tac x = "rs1 @ [AZERO]" in meta_spec)
apply(rule real_trans)
apply simp
using rrewrite.intros(7) apply auto[1]
apply(drule_tac x = "bsa" in meta_spec)
apply(drule_tac x = "rs1a @ [AALTs bs rs1]" in meta_spec)
apply(rule real_trans)
apply simp
using r_in_rstar rrewrite.intros(8) apply auto[1]
apply(drule_tac x = "bs" in meta_spec)
apply(drule_tac x = "rs1@[r]" in meta_spec)
apply(rule real_trans)
apply simp
apply auto
done
lemma flts_rewrites: " AALTs bs1 rs \<leadsto>* AALTs bs1 (flts rs)"
apply(induction rs)
apply simp
apply(case_tac "a = AZERO")
apply (metis flts.simps(2) many_steps_later rrewrite0away)
apply(case_tac "\<exists>bs2 rs2. a = AALTs bs2 rs2")
apply(erule exE)+
apply(simp)
prefer 2
apply(subst flts_prepend)
apply (meson nonalt.elims(3))
apply (meson nonazero.elims(3))
apply(subgoal_tac "(a#rs) f\<leadsto>* (a#flts rs)")
apply (metis append_Nil frewritesaalts)
apply (meson fltsfrewrites fs4 nonalt.elims(3) nonazero.elims(3))
by (metis append_Cons append_Nil fltsfrewrites frewritesaalts flts_append k0a)
(* TEST *)
lemma r:
assumes "AALTs bs rs1 \<leadsto> AALTs bs rs2"
shows "AALTs bs (x # rs1) \<leadsto>* AALTs bs (x # rs2)"
using assms
apply(erule_tac rrewrite.cases)
apply(auto)
apply (metis append_Cons append_Nil rrewrite.intros(6) r_in_rstar)
apply (metis append_Cons append_self_conv2 rrewrite.intros(7) r_in_rstar)
apply (metis Cons_eq_appendI append_eq_append_conv2 rrewrite.intros(8) self_append_conv r_in_rstar)
apply(case_tac rs2)
apply(auto)
apply(case_tac r)
apply(auto)
apply (metis append_Nil2 append_butlast_last_id butlast.simps(2) last.simps list.distinct(1) list.map_disc_iff r_in_rstar rrewrite.intros(8))
apply(case_tac r)
apply(auto)
defer
apply(rule r_in_rstar)
apply (metis append_Cons append_Nil rrewrite.intros(11))
apply(rule real_trans)
apply(rule r_in_rstar)
using rrewrite.intros(8)[where ?rsb = "[]", of "bs" "[x]" "[]" , simplified]
apply(rule_tac rrewrite.intros(8)[where ?rsb = "[]", of "bs" "[x]" "[]" , simplified])
apply(simp add: map_fuse_Nil fuse_Nil)
done
lemma alts_simpalts:
"(\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x) \<Longrightarrow>
AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)"
apply(induct rs)
apply(auto)[1]
using trivialbsimp_srewrites apply auto[1]
by (simp add: srewrites_alt1 ss2)
lemma threelistsappend: "rsa@a#rsb = (rsa@[a])@rsb"
apply auto
done
lemma somewhereInside: "r \<in> set rs \<Longrightarrow> \<exists>rs1 rs2. rs = rs1@[r]@rs2"
using split_list by fastforce
lemma somewhereMapInside: "f r \<in> f ` set rs \<Longrightarrow> \<exists>rs1 rs2 a. rs = rs1@[a]@rs2 \<and> f a = f r"
apply auto
by (metis split_list)
lemma alts_dBrewrites_withFront:
"AALTs bs (rsa @ rs) \<leadsto>* AALTs bs (rsa @ distinctBy rs erase (erase ` set rsa))"
apply(induction rs arbitrary: rsa)
apply simp
apply(drule_tac x = "rsa@[a]" in meta_spec)
apply(subst threelistsappend)
apply(rule real_trans)
apply simp
apply(case_tac "a \<in> set rsa")
apply simp
apply(drule somewhereInside)
apply(erule exE)+
apply simp
apply(subgoal_tac " AALTs bs
(rs1 @
a #
rs2 @
a #
distinctBy rs erase
(insert (erase a)
(erase `
(set rs1 \<union> set rs2)))) \<leadsto> AALTs bs (rs1@ a # rs2 @ distinctBy rs erase
(insert (erase a)
(erase `
(set rs1 \<union> set rs2)))) ")
prefer 2
using rrewrite.intros(11) apply force
using r_in_rstar apply force
apply(subgoal_tac "erase ` set (rsa @ [a]) = insert (erase a) (erase ` set rsa)")
prefer 2
apply auto[1]
apply(case_tac "erase a \<in> erase `set rsa")
apply simp
apply(subgoal_tac "AALTs bs (rsa @ a # distinctBy rs erase (insert (erase a) (erase ` set rsa))) \<leadsto>
AALTs bs (rsa @ distinctBy rs erase (insert (erase a) (erase ` set rsa)))")
apply force
apply (smt (verit, ccfv_threshold) append_Cons append_assoc append_self_conv2 r_in_rstar rrewrite.intros(11) same_append_eq somewhereMapInside)
by force
lemma alts_dBrewrites: "AALTs bs rs \<leadsto>* AALTs bs (distinctBy rs erase {})"
apply(induction rs)
apply simp
apply simp
using alts_dBrewrites_withFront
by (metis append_Nil dB_single_step empty_set image_empty)
lemma bsimp_rewrite:
shows "r \<leadsto>* bsimp r"
proof (induction r rule: bsimp.induct)
case (1 bs1 r1 r2)
then show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)"
apply(simp)
apply(case_tac "bsimp r1 = AZERO")
apply simp
using continuous_rewrite apply blast
apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
apply(erule exE)
apply simp
apply(subst bsimp_ASEQ2)
apply (meson real_trans rrewrite.intros(3) rrewrites.intros(2) star_seq star_seq2)
apply (smt (verit, best) bsimp_ASEQ0 bsimp_ASEQ1 real_trans rrewrite.intros(2) rs2 star_seq star_seq2)
done
next
case (2 bs1 rs)
then show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)"
by (metis alts_dBrewrites alts_simpalts bsimp.simps(2) bsimp_AALTs_rewrites flts_rewrites real_trans)
next
case "3_1"
then show "AZERO \<leadsto>* bsimp AZERO"
by simp
next
case ("3_2" v)
then show "AONE v \<leadsto>* bsimp (AONE v)"
by simp
next
case ("3_3" v va)
then show "ACHAR v va \<leadsto>* bsimp (ACHAR v va)"
by simp
next
case ("3_4" v va)
then show "ASTAR v va \<leadsto>* bsimp (ASTAR v va)"
by simp
qed
lemma rewrite_non_nullable_strong:
assumes "r1 \<leadsto> r2"
shows "bnullable r1 = bnullable r2"
using assms
apply(induction r1 r2 rule: rrewrite.induct)
apply(auto)
apply(metis bnullable_correctness erase_fuse)+
apply(metis UnCI bnullable_correctness erase_fuse imageI)
apply(metis bnullable_correctness erase_fuse)+
done
lemma rewrite_nullable:
assumes "r1 \<leadsto> r2" "bnullable r1"
shows "bnullable r2"
using assms rewrite_non_nullable_strong
by auto
lemma rewritesnullable:
assumes "r1 \<leadsto>* r2" "bnullable r1"
shows "bnullable r2"
using assms
apply(induction r1 r2 rule: rrewrites.induct)
apply simp
using rewrite_non_nullable_strong by blast
lemma bnullable_segment:
"bnullable (AALTs bs (rs1@[r]@rs2)) \<Longrightarrow> bnullable (AALTs bs rs1) \<or> bnullable (AALTs bs rs2) \<or> bnullable r"
by auto
lemma bnullablewhichbmkeps: "\<lbrakk>bnullable (AALTs bs (rs1@[r]@rs2)); \<not> bnullable (AALTs bs rs1); bnullable r \<rbrakk>
\<Longrightarrow> bmkeps (AALTs bs (rs1@[r]@rs2)) = bs @ (bmkeps r)"
using qq2 bnullable_Hdbmkeps_Hd by force
lemma spillbmkepslistr: "bnullable (AALTs bs1 rs1)
\<Longrightarrow> bmkeps (AALTs bs (AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs ( map (fuse bs1) rs1 @ rsb))"
apply(subst bnullable_Hdbmkeps_Hd)
apply simp
by (metis bmkeps.simps(3) k0a list.set_intros(1) qq1 qq4 qs3)
lemma third_segment_bnullable:
"\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow>
bnullable (AALTs bs rs3)"
apply(auto)
done
lemma third_segment_bmkeps:
"\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow>
bmkeps (AALTs bs (rs1@rs2@rs3) ) = bmkeps (AALTs bs rs3)"
by (metis bnullable.simps(1) bnullable.simps(4) bsimp_AALTs.simps(1) bsimp_AALTs_rewrites qq2 rewritesnullable self_append_conv third_segment_bnullable)
lemma rewrite_bmkepsalt:
"\<lbrakk>bnullable (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)); bnullable (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))\<rbrakk>
\<Longrightarrow> bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
apply(rule qq3)
apply(simp)
apply(simp)
apply(case_tac "bnullable (AALTs bs1 rs1)")
using spillbmkepslistr apply blast
apply(subst qq2)
apply(auto simp add: bnullable_fuse r1)
done
lemma rewrite_bmkeps_aux:
assumes "r1 \<leadsto> r2" "bnullable r1" "bnullable r2"
shows "bmkeps r1 = bmkeps r2"
using assms
proof (induction r1 r2 rule: rrewrite.induct)
case (1 bs r2)
then show ?case by simp
next
case (2 bs r1)
then show ?case by simp
next
case (3 bs bs1 r)
then show ?case by (simp add: b2)
next
case (4 r1 r2 bs r3)
then show ?case by simp
next
case (5 r3 r4 bs r1)
then show ?case by simp
next
case (6 r r' bs rs1 rs2)
then show ?case
by (metis append_Cons append_Nil bnullable.simps(4) bnullable_segment bnullablewhichbmkeps qq3 r1 rewrite_non_nullable_strong)
next
case (7 bs rsa rsb)
then show ?case
by (metis bnullable.simps(1) bnullable.simps(4) bnullable_segment qq1 qq2 rewrite_nullable rrewrite.intros(9) rrewrite0away third_segment_bmkeps)
next
case (8 bs rsa bs1 rs1 rsb)
then show ?case
by (simp add: rewrite_bmkepsalt)
next
case (9 bs)
then show ?case
by fastforce
next
case (10 bs r)
then show ?case
by (simp add: b2)
next
case (11 a1 a2 bs rsa rsb rsc)
then show ?case
by (smt (verit, ccfv_threshold) append_Cons append_eq_appendI append_self_conv2 bnullable_correctness list.set_intros(1) qq3 r1)
qed
lemma rewrite_bmkeps:
assumes "r1 \<leadsto> r2" "bnullable r1"
shows "bmkeps r1 = bmkeps r2"
using assms(1) assms(2) rewrite_bmkeps_aux rewrite_nullable by blast
lemma rewrites_bmkeps:
assumes "r1 \<leadsto>* r2" "bnullable r1"
shows "bmkeps r1 = bmkeps r2"
using assms
proof(induction r1 r2 rule: rrewrites.induct)
case (rs1 r)
then show "bmkeps r = bmkeps r" by simp
next
case (rs2 r1 r2 r3)
then have IH: "bmkeps r1 = bmkeps r2" by simp
have a1: "bnullable r1" by fact
have a2: "r1 \<leadsto>* r2" by fact
have a3: "r2 \<leadsto> r3" by fact
have a4: "bnullable r2" using a1 a2 by (simp add: rewritesnullable)
then have "bmkeps r2 = bmkeps r3" using rewrite_bmkeps a3 a4 by simp
then show "bmkeps r1 = bmkeps r3" using IH by simp
qed
lemma alts_rewrite_front: "r \<leadsto> r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto> AALTs bs (r' # rs)"
by (metis append_Cons append_Nil rrewrite.intros(6))
lemma to_zero_in_alt: " AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2"
by (simp add: alts_rewrite_front rrewrite.intros(1))
lemma rewrite_fuse:
assumes "r2 \<leadsto> r3"
shows "fuse bs r2 \<leadsto>* fuse bs r3"
using assms
proof(induction r2 r3 arbitrary: bs rule: rrewrite.induct)
case (1 bs r2)
then show ?case
by (simp add: continuous_rewrite)
next
case (2 bs r1)
then show ?case
using rrewrite.intros(2) by force
next
case (3 bs bs1 r)
then show ?case
by (metis fuse.simps(5) fuse_append r_in_rstar rrewrite.intros(3))
next
case (4 r1 r2 bs r3)
then show ?case
by (simp add: r_in_rstar star_seq)
next
case (5 r3 r4 bs r1)
then show ?case
using fuse.simps(5) r_in_rstar star_seq2 by auto
next
case (6 r r' bs rs1 rs2)
then show ?case
using contextrewrites2 r_in_rstar by force
next
case (7 bs rsa rsb)
then show ?case
using rrewrite.intros(7) by force
next
case (8 bs rsa bs1 rs1 rsb)
then show ?case
using rrewrite.intros(8) by force
next
case (9 bs)
then show ?case
by (simp add: r_in_rstar rrewrite.intros(9))
next
case (10 bs r)
then show ?case
by (metis fuse.simps(4) fuse_append r_in_rstar rrewrite.intros(10))
next
case (11 a1 a2 bs rsa rsb rsc)
then show ?case
using fuse.simps(4) r_in_rstar rrewrite.intros(11) by auto
qed
lemma rewrites_fuse:
assumes "r1 \<leadsto>* r2"
shows "fuse bs r1 \<leadsto>* fuse bs r2"
using assms
apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct)
apply(auto intro: rewrite_fuse real_trans)
done
lemma bder_fuse_list:
shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1"
apply(induction rs1)
apply(simp_all add: bder_fuse)
done
lemma rewrite_der_altmiddle:
"bder c (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
apply simp
apply(simp add: bder_fuse_list del: append.simps)
by (metis append.assoc map_map r_in_rstar rrewrite.intros(8) threelistsappend)
lemma lock_step_der_removal:
shows " erase a1 = erase a2 \<Longrightarrow>
bder c (AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc)) \<leadsto>*
bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))"
apply(simp)
using rrewrite.intros(11) by auto
lemma rewrite_after_der:
assumes "r1 \<leadsto> r2"
shows "(bder c r1) \<leadsto>* (bder c r2)"
using assms
proof(induction r1 r2 rule: rrewrite.induct)
case (1 bs r2)
then show "bder c (ASEQ bs AZERO r2) \<leadsto>* bder c AZERO"
by (simp add: continuous_rewrite)
next
case (2 bs r1)
then show "bder c (ASEQ bs r1 AZERO) \<leadsto>* bder c AZERO"
apply(simp)
by (meson contextrewrites1 r_in_rstar real_trans rrewrite.intros(9) rrewrite.intros(2) rrewrite0away)
next
case (3 bs bs1 r)
then show "bder c (ASEQ bs (AONE bs1) r) \<leadsto>* bder c (fuse (bs @ bs1) r)"
apply(simp)
by (metis bder_fuse fuse_append rrewrite.intros(10) rrewrite0away rrewrites.simps to_zero_in_alt)
next
case (4 r1 r2 bs r3)
have as: "r1 \<leadsto> r2" by fact
have IH: "bder c r1 \<leadsto>* bder c r2" by fact
from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r2 r3)"
by (simp add: contextrewrites1 rewrite_bmkeps rewrite_non_nullable_strong star_seq)
next
case (5 r3 r4 bs r1)
have as: "r3 \<leadsto> r4" by fact
have IH: "bder c r3 \<leadsto>* bder c r4" by fact
from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)"
using bder.simps(5) r_in_rstar rewrites_fuse srewrites_alt1 ss1 ss2 star_seq2 by presburger
next
case (6 r r' bs rs1 rs2)
have as: "r \<leadsto> r'" by fact
have IH: "bder c r \<leadsto>* bder c r'" by fact
from as IH show "bder c (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto>* bder c (AALTs bs (rs1 @ [r'] @ rs2))"
apply(simp)
using contextrewrites2 by force
next
case (7 bs rsa rsb)
then show "bder c (AALTs bs (rsa @ [AZERO] @ rsb)) \<leadsto>* bder c (AALTs bs (rsa @ rsb))"
apply(simp)
using rrewrite.intros(7) by auto
next
case (8 bs rsa bs1 rs1 rsb)
then show
"bder c (AALTs bs (rsa @ [AALTs bs1 rs1] @ rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
using rewrite_der_altmiddle by auto
next
case (9 bs)
then show "bder c (AALTs bs []) \<leadsto>* bder c AZERO"
by (simp add: r_in_rstar rrewrite.intros(9))
next
case (10 bs r)
then show "bder c (AALTs bs [r]) \<leadsto>* bder c (fuse bs r)"
by (simp add: bder_fuse r_in_rstar rrewrite.intros(10))
next
case (11 a1 a2 bs rsa rsb rsc)
have as: "erase a1 = erase a2" by fact
then show "bder c (AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc)) \<leadsto>* bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))"
using lock_step_der_removal by force
qed
lemma rewrites_after_der:
assumes "r1 \<leadsto>* r2"
shows "bder c r1 \<leadsto>* bder c r2"
using assms
apply(induction r1 r2 rule: rrewrites.induct)
apply(simp_all add: rewrite_after_der real_trans)
done
lemma central:
shows "bders r s \<leadsto>* bders_simp r s"
proof(induct s arbitrary: r rule: rev_induct)
case Nil
then show "bders r [] \<leadsto>* bders_simp r []" by simp
next
case (snoc x xs)
have IH: "\<And>r. bders r xs \<leadsto>* bders_simp r xs" by fact
have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append)
also have "... \<leadsto>* bders (bders_simp r xs) [x]" using IH
by (simp add: rewrites_after_der)
also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH
by (simp add: bsimp_rewrite)
finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])"
by (simp add: bders_simp_append)
qed
lemma quasi_main:
assumes "bnullable (bders r s)"
shows "bmkeps (bders r s) = bmkeps (bders_simp r s)"
proof -
have "bders r s \<leadsto>* bders_simp r s" by (rule central)
then
show "bmkeps (bders r s) = bmkeps (bders_simp r s)" using assms
by (rule rewrites_bmkeps)
qed
theorem main_main:
shows "blexer r s = blexer_simp r s"
unfolding blexer_def blexer_simp_def
using b4 quasi_main by simp
theorem blexersimp_correctness:
shows "lexer r s = blexer_simp r s"
using blexer_correctness main_main by simp
export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers
unused_thms
inductive aggressive:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>? _" [99, 99] 99)
where
"ASEQ bs (AALTs bs1 rs) r \<leadsto>? AALTs (bs@bs1) (map (\<lambda>r'. ASEQ [] r' r) rs) "
end