theory SizeBound3
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 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"
abbreviation
bnullables :: "arexp list \<Rightarrow> bool"
where
"bnullables rs \<equiv> (\<exists>r \<in> set rs. bnullable r)"
fun
bmkeps :: "arexp \<Rightarrow> bit list" and
bmkepss :: "arexp list \<Rightarrow> bit list"
where
"bmkeps(AONE bs) = bs"
| "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)"
| "bmkeps(AALTs bs rs) = bs @ (bmkepss rs)"
| "bmkeps(ASTAR bs r) = bs @ [S]"
| "bmkepss [] = []"
| "bmkepss (r # rs) = (if bnullable(r) then (bmkeps r) else (bmkepss rs))"
lemma bmkepss1:
assumes "\<not> bnullables rs1"
shows "bmkepss (rs1 @ rs2) = bmkepss rs2"
using assms
by (induct rs1) (auto)
lemma bmkepss2:
assumes "bnullables rs1"
shows "bmkepss (rs1 @ rs2) = bmkepss rs1"
using assms
by (induct rs1) (auto)
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 simp
*)
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"
"bnullables rs"
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. bnullable r \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))"
"bnullables rs"
shows "bs @ bmkepss rs = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
using assms
apply(induct rs arbitrary: bs)
apply(auto)
apply (metis (no_types, opaque_lifting) bmkepss.cases bnullable_correctness erase.simps(5) erase.simps(6) mkeps.simps(3) retrieve.simps(3) retrieve.simps(4))
apply (metis r3)
apply (metis (no_types, lifting) bmkepss.cases bnullable_correctness empty_iff erase.simps(6) list.set(1) mkeps.simps(3) retrieve.simps(4))
apply (metis r3)
done
lemma bmkeps_retrieve:
assumes "bnullable r"
shows "bmkeps r = retrieve r (mkeps (erase r))"
using assms
apply(induct r)
apply(auto)
using t by auto
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 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
using bnullable_correctness by force
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
by (auto simp add: bnullable_correctness[symmetric])
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)))"
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"
lemma bsimp_ASEQ0[simp]:
shows "bsimp_ASEQ bs r1 AZERO = AZERO"
by (case_tac r1)(simp_all)
lemma bsimp_ASEQ1:
assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<nexists>bs. r1 = 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[simp]:
shows "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"
by (case_tac r2) (simp_all)
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 :: "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"
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 (erase (ASEQ bs r1 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_all
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 (simp add: L_erase_AALTs)
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 bmkeps_fuse:
assumes "bnullable r"
shows "bmkeps (fuse bs r) = bs @ bmkeps r"
by (metis assms bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)
lemma bmkepss_fuse:
assumes "bnullables rs"
shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs"
using assms
apply(induct rs arbitrary: bs)
apply(auto simp add: bmkeps_fuse bnullable_fuse)
done
lemma b4:
shows "bnullable (bders_simp r s) = bnullable (bders r s)"
proof -
have "L (erase (bders_simp r s)) = L (erase (bders r s))"
using L_bders_simp by force
then show "bnullable (bders_simp r s) = bnullable (bders r s)"
using bnullable_correctness nullable_correctness by blast
qed
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)
and
srewrite:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto> _" [100, 100] 100)
where
bs1: "ASEQ bs AZERO r2 \<leadsto> AZERO"
| bs2: "ASEQ bs r1 AZERO \<leadsto> AZERO"
| bs3: "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r"
| bs4: "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"
| bs5: "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"
| bs6: "AALTs bs [] \<leadsto> AZERO"
| bs7: "AALTs bs [r] \<leadsto> fuse bs r"
| bs10: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2"
| ss1: "[] s\<leadsto> []"
| ss2: "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)"
| ss3: "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)"
| ss4: "(AZERO # rs) s\<leadsto> rs"
| ss5: "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)"
| ss6: "erase a1 = erase a2 \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (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
sss1[intro, simp]:"rs s\<leadsto>* rs"
| sss2[intro]: "\<lbrakk>rs1 s\<leadsto> rs2; rs2 s\<leadsto>* rs3\<rbrakk> \<Longrightarrow> rs1 s\<leadsto>* rs3"
lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
using rrewrites.intros(1) rrewrites.intros(2) by blast
lemma rrewrites_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 srewrites_trans[trans]:
assumes a1: "r1 s\<leadsto>* r2" and a2: "r2 s\<leadsto>* r3"
shows "r1 s\<leadsto>* r3"
using a1 a2
apply(induct r1 r2 arbitrary: r3 rule: srewrites.induct)
apply(auto)
done
lemma contextrewrites0:
"rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2"
apply(induct rs1 rs2 rule: srewrites.inducts)
apply simp
using bs10 r_in_rstar rrewrites_trans by blast
lemma contextrewrites1:
"r \<leadsto>* r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto>* AALTs bs (r' # rs)"
apply(induct r r' rule: rrewrites.induct)
apply simp
using bs10 ss3 by blast
lemma srewrite1:
shows "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto> (rs @ rs2)"
apply(induct rs)
apply(auto)
using ss2 by auto
lemma srewrites1:
shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto>* (rs @ rs2)"
apply(induct rs1 rs2 rule: srewrites.induct)
apply(auto)
using srewrite1 by blast
lemma srewrite2:
shows "r1 \<leadsto> r2 \<Longrightarrow> True"
and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
apply(induct rule: rrewrite_srewrite.inducts)
apply(auto)
apply (metis append_Cons append_Nil srewrites1)
apply(meson srewrites.simps ss3)
apply (meson srewrites.simps ss4)
apply (meson srewrites.simps ss5)
by (metis append_Cons append_Nil srewrites.simps ss6)
lemma srewrites3:
shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
apply(induct rs1 rs2 arbitrary: rs rule: srewrites.induct)
apply(auto)
by (meson srewrite2(2) srewrites_trans)
(*
lemma srewrites4:
assumes "rs3 s\<leadsto>* rs4" "rs1 s\<leadsto>* rs2"
shows "(rs1 @ rs3) s\<leadsto>* (rs2 @ rs4)"
using assms
apply(induct rs3 rs4 arbitrary: rs1 rs2 rule: srewrites.induct)
apply (simp add: srewrites3)
using srewrite1 by blast
*)
lemma srewrites6:
assumes "r1 \<leadsto>* r2"
shows "[r1] s\<leadsto>* [r2]"
using assms
apply(induct r1 r2 rule: rrewrites.induct)
apply(auto)
by (meson srewrites.simps srewrites_trans ss3)
lemma srewrites7:
assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2"
shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)"
using assms
by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans)
lemma ss6_stronger_aux:
shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctBy rs2 erase (set (map erase rs1)))"
apply(induct rs2 arbitrary: rs1)
apply(auto)
apply (smt (verit, best) append.assoc append.right_neutral append_Cons append_Nil split_list srewrite2(2) srewrites_trans ss6)
apply(drule_tac x="rs1 @ [a]" in meta_spec)
apply(simp)
done
lemma ss6_stronger:
shows "rs1 s\<leadsto>* distinctBy rs1 erase {}"
using ss6_stronger_aux[of "[]" _] by auto
lemma rewrite_preserves_fuse:
shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3"
and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3"
proof(induct rule: rrewrite_srewrite.inducts)
case (bs3 bs1 bs2 r)
then show ?case
by (metis fuse.simps(5) fuse_append rrewrite_srewrite.bs3)
next
case (bs7 bs r)
then show ?case
by (metis fuse.simps(4) fuse_append rrewrite_srewrite.bs7)
next
case (ss2 rs1 rs2 r)
then show ?case
using srewrites7 by force
next
case (ss3 r1 r2 rs)
then show ?case by (simp add: r_in_rstar srewrites7)
next
case (ss5 bs1 rs1 rsb)
then show ?case
apply(simp)
by (metis (mono_tags, lifting) comp_def fuse_append map_eq_conv rrewrite_srewrite.ss5 srewrites.simps)
next
case (ss6 a1 a2 rsa rsb rsc)
then show ?case
apply(simp only: map_append)
by (smt (verit, ccfv_threshold) erase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps)
qed (auto intro: rrewrite_srewrite.intros)
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_preserves_fuse rrewrites_trans)
done
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_srewrite.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_srewrite.intros)
done
lemma continuous_rewrite:
assumes "r1 \<leadsto>* AZERO"
shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
using assms bs1 star_seq by blast
(*
lemma continuous_rewrite2:
assumes "r1 \<leadsto>* AONE bs"
shows "ASEQ bs1 r1 r2 \<leadsto>* (fuse (bs1 @ bs) r2)"
using assms by (meson bs3 rrewrites.simps 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 bsimp_AALTs_rewrites:
shows "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps)
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(simp)
using srewrites7 by auto
lemma fltsfrewrites: "rs s\<leadsto>* flts rs"
apply(induction rs rule: flts.induct)
apply(auto intro: rrewrite_srewrite.intros)
apply (meson srewrites.simps srewrites1 ss5)
using rs1 srewrites7 apply presburger
using srewrites7 apply force
apply (simp add: srewrites7)
by (simp add: srewrites7)
lemma bnullable0:
shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2"
and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2"
apply(induct rule: rrewrite_srewrite.inducts)
apply(auto simp add: bnullable_fuse)
apply (meson UnCI bnullable_fuse imageI)
by (metis bnullable_correctness)
lemma rewritesnullable:
assumes "r1 \<leadsto>* r2"
shows "bnullable r1 = bnullable r2"
using assms
apply(induction r1 r2 rule: rrewrites.induct)
apply simp
using bnullable0(1) by auto
lemma rewrite_bmkeps_aux:
shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<and> bnullable r2 \<Longrightarrow> bmkeps r1 = bmkeps r2)"
and "rs1 s\<leadsto> rs2 \<Longrightarrow> (bnullables rs1 \<and> bnullables rs2 \<Longrightarrow> bmkepss rs1 = bmkepss rs2)"
proof (induct rule: rrewrite_srewrite.inducts)
case (bs3 bs1 bs2 r)
then show ?case by (simp add: bmkeps_fuse)
next
case (bs7 bs r)
then show ?case by (simp add: bmkeps_fuse)
next
case (ss3 r1 r2 rs)
then show ?case
by (metis bmkepss.simps(2) bnullable0(1))
next
case (ss5 bs1 rs1 rsb)
then show ?case
by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse)
next
case (ss6 a1 a2 rsa rsb rsc)
then show ?case
by (smt (verit, best) append_Cons bmkeps.simps(3) bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness)
qed (auto)
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 a3 bnullable0(1) rewrite_bmkeps_aux(1) by blast
then show "bmkeps r1 = bmkeps r3" using IH by simp
qed
lemma rewrites_to_bsimp:
shows "r \<leadsto>* bsimp r"
proof (induction r rule: bsimp.induct)
case (1 bs1 r1 r2)
have IH1: "r1 \<leadsto>* bsimp r1" by fact
have IH2: "r2 \<leadsto>* bsimp r2" by fact
{ assume as: "bsimp r1 = AZERO \<or> bsimp r2 = AZERO"
with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto
then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
by (metis bs2 continuous_rewrite rrewrites.simps star_seq2)
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" using as by auto
}
moreover
{ assume "\<exists>bs. bsimp r1 = AONE bs"
then obtain bs where as: "bsimp r1 = AONE bs" by blast
with IH1 have "r1 \<leadsto>* AONE bs" by simp
then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast
with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimp r2)"
using rewrites_fuse by (meson rrewrites_trans)
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 (AONE bs) r2)" by simp
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by (simp add: as)
}
moreover
{ assume as1: "bsimp r1 \<noteq> AZERO" "bsimp r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimp r1 = AONE bs)"
then have "bsimp_ASEQ bs1 (bsimp r1) (bsimp r2) = ASEQ bs1 (bsimp r1) (bsimp r2)"
by (simp add: bsimp_ASEQ1)
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" using as1 as2 IH1 IH2
by (metis rrewrites_trans star_seq star_seq2)
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by simp
}
ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by blast
next
case (2 bs1 rs)
have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x" by fact
then have "rs s\<leadsto>* (map bsimp rs)" by (simp add: trivialbsimp_srewrites)
also have "... s\<leadsto>* flts (map bsimp rs)" by (simp add: fltsfrewrites)
also have "... s\<leadsto>* distinctBy (flts (map bsimp rs)) erase {}" by (simp add: ss6_stronger)
finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})"
using contextrewrites0 by blast
also have "... \<leadsto>* bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})"
by (simp add: bsimp_AALTs_rewrites)
finally show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)" by simp
qed (simp_all)
lemma to_zero_in_alt:
shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2"
by (simp add: bs1 bs10 ss3)
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_preserves_bder:
shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)"
and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2"
proof(induction rule: rrewrite_srewrite.inducts)
case (bs1 bs r2)
then show ?case
by (simp add: continuous_rewrite)
next
case (bs2 bs r1)
then show ?case
apply(auto)
apply (meson bs6 contextrewrites0 rrewrite_srewrite.bs2 rs2 ss3 ss4 sss1 sss2)
by (simp add: r_in_rstar rrewrite_srewrite.bs2)
next
case (bs3 bs1 bs2 r)
then show ?case
apply(simp)
by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt)
next
case (bs4 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 (metis bder.simps(5) bnullable0(1) contextrewrites1 rewrite_bmkeps_aux(1) star_seq)
next
case (bs5 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)"
apply(simp)
apply(auto)
using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger
using star_seq2 by blast
next
case (bs6 bs)
then show ?case
using rrewrite_srewrite.bs6 by force
next
case (bs7 bs r)
then show ?case
by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7)
next
case (bs10 rs1 rs2 bs)
then show ?case
using contextrewrites0 by force
next
case ss1
then show ?case by simp
next
case (ss2 rs1 rs2 r)
then show ?case
by (simp add: srewrites7)
next
case (ss3 r1 r2 rs)
then show ?case
by (simp add: srewrites7)
next
case (ss4 rs)
then show ?case
using rrewrite_srewrite.ss4 by fastforce
next
case (ss5 bs1 rs1 rsb)
then show ?case
apply(simp)
using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast
next
case (ss6 a1 a2 bs rsa rsb)
then show ?case
apply(simp only: map_append)
by (smt (verit, best) erase_bder list.simps(8) list.simps(9) local.ss6 rrewrite_srewrite.ss6 srewrites.simps)
qed
lemma rewrites_preserves_bder:
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_preserves_bder rrewrites_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_preserves_bder)
also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH
by (simp add: rewrites_to_bsimp)
finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])"
by (simp add: bders_simp_append)
qed
lemma main_aux:
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_blexer_simp:
shows "blexer r s = blexer_simp r s"
unfolding blexer_def blexer_simp_def
using b4 main_aux by simp
theorem blexersimp_correctness:
shows "lexer r s = blexer_simp r s"
using blexer_correctness main_blexer_simp 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