theory BitCoded2
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)"
| "Stars_add v _ = Stars [v]"
function
decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)"
where
"decode' ds ZERO = (Void, [])"
| "decode' ds ONE = (Void, ds)"
| "decode' ds (CHAR 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) = CHAR 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)"
lemma decode_code_erase:
assumes "\<Turnstile> v : (erase a)"
shows "decode (code v) (erase a) = Some v"
using assms
by (simp add: decode_code)
fun nonalt :: "arexp \<Rightarrow> bool"
where
"nonalt (AALTs bs2 rs) = False"
| "nonalt r = True"
fun good :: "arexp \<Rightarrow> bool" where
"good AZERO = False"
| "good (AONE cs) = True"
| "good (ACHAR cs c) = True"
| "good (AALTs cs []) = False"
| "good (AALTs cs [r]) = False"
| "good (AALTs cs (r1#r2#rs)) = (\<forall>r' \<in> set (r1#r2#rs). good r' \<and> nonalt r')"
| "good (ASEQ _ AZERO _) = False"
| "good (ASEQ _ (AONE _) _) = False"
| "good (ASEQ _ _ AZERO) = False"
| "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)"
| "good (ASTAR cs 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
fun intern :: "rexp \<Rightarrow> arexp" where
"intern ZERO = AZERO"
| "intern ONE = AONE []"
| "intern (CHAR 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 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 r:
assumes "bnullable (AALTs bs (a # rs))"
shows "bnullable a \<or> (\<not> bnullable a \<and> bnullable (AALTs bs rs))"
using assms
apply(induct rs)
apply(auto)
done
lemma r0:
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 r0)
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
lemma asize0:
shows "0 < asize r"
apply(induct r)
apply(auto)
done
lemma asize_fuse:
shows "asize (fuse bs r) = asize r"
apply(induct r)
apply(auto)
done
lemma bder_fuse:
shows "bder c (fuse bs a) = fuse bs (bder c a)"
apply(induct a arbitrary: bs c)
apply(simp_all)
done
lemma map_bder_fuse:
shows "map (bder c \<circ> fuse bs1) as1 = map (fuse bs1) (map (bder c) as1)"
apply(induct as1)
apply(auto simp add: bder_fuse)
done
fun nonnested :: "arexp \<Rightarrow> bool"
where
"nonnested (AALTs bs2 []) = True"
| "nonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False"
| "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)"
| "nonnested r = True"
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 spill :: "arexp list \<Rightarrow> arexp list"
where
"spill [] = []"
| "spill ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ spill rs"
| "spill (r1 # rs) = r1 # spill rs"
lemma spill_Cons:
shows "spill (r # rs1) = spill [r] @ spill rs1"
apply(induct r arbitrary: rs1)
apply(auto)
done
lemma spill_append:
shows "spill (rs1 @ rs2) = spill rs1 @ spill rs2"
apply(induct rs1 arbitrary: rs2)
apply(auto)
by (metis append.assoc spill_Cons)
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 :: "arexp \<Rightarrow> arexp"
where
"bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"
| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))"
| "bsimp r = r"
inductive contains2 :: "arexp \<Rightarrow> bit list \<Rightarrow> bool" ("_ >>2 _" [51, 50] 50)
where
"AONE bs >>2 bs"
| "ACHAR bs c >>2 bs"
| "\<lbrakk>a1 >>2 bs1; a2 >>2 bs2\<rbrakk> \<Longrightarrow> ASEQ bs a1 a2 >>2 bs @ bs1 @ bs2"
| "r >>2 bs1 \<Longrightarrow> AALTs bs (r#rs) >>2 bs @ bs1"
| "AALTs bs rs >>2 bs @ bs1 \<Longrightarrow> AALTs bs (r#rs) >>2 bs @ bs1"
| "ASTAR bs r >>2 bs @ [S]"
| "\<lbrakk>r >>2 bs1; ASTAR [] r >>2 bs2\<rbrakk> \<Longrightarrow> ASTAR bs r >>2 bs @ Z # bs1 @ bs2"
| "r >>2 bs \<Longrightarrow> (bsimp r) >>2 bs"
inductive contains :: "arexp \<Rightarrow> bit list \<Rightarrow> bool" ("_ >> _" [51, 50] 50)
where
"AONE bs >> bs"
| "ACHAR bs c >> bs"
| "\<lbrakk>a1 >> bs1; a2 >> bs2\<rbrakk> \<Longrightarrow> ASEQ bs a1 a2 >> bs @ bs1 @ bs2"
| "r >> bs1 \<Longrightarrow> AALTs bs (r#rs) >> bs @ bs1"
| "AALTs bs rs >> bs @ bs1 \<Longrightarrow> AALTs bs (r#rs) >> bs @ bs1"
| "ASTAR bs r >> bs @ [S]"
| "\<lbrakk>r >> bs1; ASTAR [] r >> bs2\<rbrakk> \<Longrightarrow> ASTAR bs r >> bs @ Z # bs1 @ bs2"
lemma contains0:
assumes "a >> bs"
shows "(fuse bs1 a) >> bs1 @ bs"
using assms
apply(induct arbitrary: bs1)
apply(auto intro: contains.intros)
apply (metis append.assoc contains.intros(3))
apply (metis append.assoc contains.intros(4))
apply (metis append.assoc contains.intros(5))
apply (metis append.assoc contains.intros(6))
apply (metis append_assoc contains.intros(7))
done
lemma contains1:
assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> intern r >> code v"
shows "ASTAR [] (intern r) >> code (Stars vs)"
using assms
apply(induct vs)
apply(simp)
using contains.simps apply blast
apply(simp)
apply(subst (2) append_Nil[symmetric])
apply(rule contains.intros)
apply(auto)
done
lemma contains2:
assumes "\<Turnstile> v : r"
shows "(intern r) >> code v"
using assms
apply(induct)
prefer 4
apply(simp)
apply(rule contains.intros)
prefer 4
apply(simp)
apply(rule contains.intros)
apply(simp)
apply(subst (3) append_Nil[symmetric])
apply(rule contains.intros)
apply(simp)
apply(simp)
apply(simp)
apply(subst (9) append_Nil[symmetric])
apply(rule contains.intros)
apply (metis append_Cons append_self_conv2 contains0)
apply(simp)
apply(subst (9) append_Nil[symmetric])
apply(rule contains.intros)
back
apply(rule contains.intros)
apply(drule_tac ?bs1.0="[S]" in contains0)
apply(simp)
apply(simp)
apply(case_tac vs)
apply(simp)
apply (metis append_Nil contains.intros(6))
using contains1 by blast
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 r0 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 qq2a:
assumes "\<not> bnullable r" "\<exists>r \<in> set rs1. bnullable r"
shows "bmkeps (AALTs bs (r # rs1)) = bmkeps (AALTs bs rs1)"
using assms
by (simp add: r1)
lemma qq3:
shows "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"
apply(induct rs arbitrary: bs)
apply(simp)
apply(simp)
done
lemma qq4:
assumes "bnullable (AALTs bs rs)"
shows "bmkeps (AALTs bs rs) = bs @ bmkeps (AALTs [] rs)"
by (metis append_Nil2 assms bmkeps_retrieve bnullable_correctness erase_fuse fuse.simps(4) mkeps_nullable retrieve_fuse2)
lemma contains3a:
assumes "AALTs bs lst >> bs @ bs1"
shows "AALTs bs (a # lst) >> bs @ bs1"
using assms
apply -
by (simp add: contains.intros(5))
lemma contains3b:
assumes "a >> bs1"
shows "AALTs bs (a # lst) >> bs @ bs1"
using assms
apply -
apply(rule contains.intros)
apply(simp)
done
lemma contains3:
assumes "\<And>x. \<lbrakk>x \<in> set rs; bnullable x\<rbrakk> \<Longrightarrow> x >> bmkeps x" "x \<in> set rs" "bnullable x"
shows "AALTs bs rs >> bmkeps (AALTs bs rs)"
using assms
apply(induct rs arbitrary: bs x)
apply simp
by (metis contains.intros(4) contains.intros(5) list.set_intros(1) list.set_intros(2) qq3 qq4 r r0 r1)
lemma cont1:
assumes "\<And>v. \<Turnstile> v : erase r \<Longrightarrow> r >> retrieve r v"
"\<forall>v\<in>set vs. \<Turnstile> v : erase r \<and> flat v \<noteq> []"
shows "ASTAR bs r >> retrieve (ASTAR bs r) (Stars vs)"
using assms
apply(induct vs arbitrary: bs r)
apply(simp)
using contains.intros(6) apply auto[1]
by (simp add: contains.intros(7))
lemma contains4:
assumes "bnullable a"
shows "a >> bmkeps a"
using assms
apply(induct a rule: bnullable.induct)
apply(auto intro: contains.intros)
using contains3 by blast
lemma contains5:
assumes "\<Turnstile> v : r"
shows "(intern r) >> retrieve (intern r) v"
using contains2[OF assms] retrieve_code[OF assms]
by (simp)
lemma contains6:
assumes "\<Turnstile> v : (erase r)"
shows "r >> retrieve r v"
using assms
apply(induct r arbitrary: v rule: erase.induct)
apply(auto)[1]
using Prf_elims(1) apply blast
using Prf_elims(4) contains.intros(1) apply force
using Prf_elims(5) contains.intros(2) apply force
apply(auto)[1]
using Prf_elims(1) apply blast
apply(auto)[1]
using contains3b contains3a apply blast
prefer 2
apply(auto)[1]
apply (metis Prf_elims(2) contains.intros(3) retrieve.simps(6))
prefer 2
apply(auto)[1]
apply (metis Prf_elims(6) cont1)
apply(simp)
apply(erule Prf_elims)
apply(auto)
apply (simp add: contains3b)
using retrieve_fuse2 contains3b contains3a
apply(subst retrieve_fuse2[symmetric])
apply (metis append_Nil2 erase_fuse fuse.simps(4))
apply(simp)
by (metis append_Nil2 erase_fuse fuse.simps(4))
lemma contains7:
assumes "\<Turnstile> v : der c (erase r)"
shows "(bder c r) >> retrieve r (injval (erase r) c v)"
using bder_retrieve[OF assms(1)] retrieve_code[OF assms(1)]
by (metis assms contains6 erase_bder)
lemma contains7a:
assumes "\<Turnstile> v : der c (erase r)"
shows "r >> retrieve r (injval (erase r) c v)"
using assms
apply -
apply(drule Prf_injval)
apply(drule contains6)
apply(simp)
done
lemma contains7b:
assumes "\<Turnstile> v : ders s (erase r)"
shows "(bders r s) >> retrieve r (flex (erase r) id s v)"
using assms
apply(induct s arbitrary: r v)
apply(simp)
apply (simp add: contains6)
apply(simp add: bders_append flex_append ders_append)
apply(drule_tac x="bder a r" in meta_spec)
apply(drule meta_spec)
apply(drule meta_mp)
apply(simp)
apply(simp)
apply(subst (asm) bder_retrieve)
defer
apply (simp add: flex_injval)
by (simp add: Prf_flex)
lemma contains7_iff:
assumes "\<Turnstile> v : der c (erase r)"
shows "(bder c r) >> retrieve r (injval (erase r) c v) \<longleftrightarrow>
r >> retrieve r (injval (erase r) c v)"
by (simp add: assms contains7 contains7a)
lemma contains8_iff:
assumes "\<Turnstile> v : ders s (erase r)"
shows "(bders r s) >> retrieve r (flex (erase r) id s v) \<longleftrightarrow>
r >> retrieve r (flex (erase r) id s v)"
using Prf_flex assms contains6 contains7b by blast
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)
apply(simp)
done
lemma bsimp_ASEQ_size:
shows "asize (bsimp_ASEQ bs r1 r2) \<le> Suc (asize r1 + asize r2)"
apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
apply(auto)
done
lemma flts_size:
shows "sum_list (map asize (flts rs)) \<le> sum_list (map asize rs)"
apply(induct rs rule: flts.induct)
apply(simp_all)
by (simp add: asize_fuse comp_def)
lemma bsimp_AALTs_size:
shows "asize (bsimp_AALTs bs rs) \<le> Suc (sum_list (map asize rs))"
apply(induct rs rule: bsimp_AALTs.induct)
apply(auto simp add: asize_fuse)
done
lemma bsimp_size:
shows "asize (bsimp r) \<le> asize r"
apply(induct r)
apply(simp_all)
apply (meson Suc_le_mono add_mono_thms_linordered_semiring(1) bsimp_ASEQ_size le_trans)
apply(rule le_trans)
apply(rule bsimp_AALTs_size)
apply(simp)
apply(rule le_trans)
apply(rule flts_size)
by (simp add: sum_list_mono)
lemma bsimp_asize0:
shows "(\<Sum>x\<leftarrow>rs. asize (bsimp x)) \<le> sum_list (map asize rs)"
apply(induct rs)
apply(auto)
by (simp add: add_mono bsimp_size)
lemma bsimp_AALTs_size2:
assumes "\<forall>r \<in> set rs. nonalt r"
shows "asize (bsimp_AALTs bs rs) \<ge> sum_list (map asize rs)"
using assms
apply(induct rs rule: bsimp_AALTs.induct)
apply(simp_all add: asize_fuse)
done
lemma qq:
shows "map (asize \<circ> fuse bs) rs = map asize rs"
apply(induct rs)
apply(auto simp add: asize_fuse)
done
lemma flts_size2:
assumes "\<exists>bs rs'. AALTs bs rs' \<in> set rs"
shows "sum_list (map asize (flts rs)) < sum_list (map asize rs)"
using assms
apply(induct rs)
apply(auto simp add: qq)
apply (simp add: flts_size less_Suc_eq_le)
apply(case_tac a)
apply(auto simp add: qq)
prefer 2
apply (simp add: flts_size le_imp_less_Suc)
using less_Suc_eq by auto
lemma bsimp_AALTs_size3:
assumes "\<exists>r \<in> set (map bsimp rs). \<not>nonalt r"
shows "asize (bsimp (AALTs bs rs)) < asize (AALTs bs rs)"
using assms flts_size2
apply -
apply(clarify)
apply(simp)
apply(drule_tac x="map bsimp rs" in meta_spec)
apply(drule meta_mp)
apply (metis list.set_map nonalt.elims(3))
apply(simp)
apply(rule order_class.order.strict_trans1)
apply(rule bsimp_AALTs_size)
apply(simp)
by (smt Suc_leI bsimp_asize0 comp_def le_imp_less_Suc le_trans map_eq_conv not_less_eq)
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_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_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 b1:
"bsimp_ASEQ bs1 (AONE bs) r = fuse (bs1 @ bs) r"
apply(induct r)
apply(auto)
done
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 b3:
shows "bnullable r = bnullable (bsimp r)"
using L_bsimp_erase bnullable_correctness nullable_correctness by auto
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 q1:
assumes "\<forall>r \<in> set rs. bmkeps(bsimp r) = bmkeps r"
shows "map (\<lambda>r. bmkeps(bsimp r)) rs = map bmkeps rs"
using assms
apply(induct rs)
apply(simp)
apply(simp)
done
lemma q3:
assumes "\<exists>r \<in> set rs. bnullable r"
shows "bmkeps (AALTs bs rs) = bmkeps (bsimp_AALTs bs rs)"
using assms
apply(induct bs rs rule: bsimp_AALTs.induct)
apply(simp)
apply(simp)
apply (simp add: b2)
apply(simp)
done
lemma fuse_empty:
shows "fuse [] r = r"
apply(induct r)
apply(auto)
done
lemma flts_fuse:
shows "map (fuse bs) (flts rs) = flts (map (fuse bs) rs)"
apply(induct rs arbitrary: bs rule: flts.induct)
apply(auto simp add: fuse_append)
done
lemma bsimp_ASEQ_fuse:
shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2"
apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct)
apply(auto)
done
lemma bsimp_AALTs_fuse:
assumes "\<forall>r \<in> set rs. fuse bs1 (fuse bs2 r) = fuse (bs1 @ bs2) r"
shows "fuse bs1 (bsimp_AALTs bs2 rs) = bsimp_AALTs (bs1 @ bs2) rs"
using assms
apply(induct bs2 rs arbitrary: bs1 rule: bsimp_AALTs.induct)
apply(auto)
done
lemma bsimp_fuse:
shows "fuse bs (bsimp r) = bsimp (fuse bs r)"
apply(induct r arbitrary: bs)
apply(simp)
apply(simp)
apply(simp)
prefer 3
apply(simp)
apply(simp)
apply (simp add: bsimp_ASEQ_fuse)
apply(simp)
by (simp add: bsimp_AALTs_fuse fuse_append)
lemma bsimp_fuse_AALTs:
shows "fuse bs (bsimp (AALTs [] rs)) = bsimp (AALTs bs rs)"
apply(subst bsimp_fuse)
apply(simp)
done
lemma bsimp_fuse_AALTs2:
shows "fuse bs (bsimp_AALTs [] rs) = bsimp_AALTs bs rs"
using bsimp_AALTs_fuse fuse_append by auto
lemma bsimp_ASEQ_idem:
assumes "bsimp (bsimp r1) = bsimp r1" "bsimp (bsimp r2) = bsimp r2"
shows "bsimp (bsimp_ASEQ x1 (bsimp r1) (bsimp r2)) = bsimp_ASEQ x1 (bsimp r1) (bsimp r2)"
using assms
apply(case_tac "bsimp r1 = AZERO")
apply(simp)
apply(case_tac "bsimp r2 = AZERO")
apply(simp)
apply (metis bnullable.elims(2) bnullable.elims(3) bsimp.simps(3) bsimp_ASEQ.simps(2) bsimp_ASEQ.simps(3) bsimp_ASEQ.simps(4) bsimp_ASEQ.simps(5) bsimp_ASEQ.simps(6))
apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
apply(auto)[1]
apply(subst bsimp_ASEQ2)
apply(subst bsimp_ASEQ2)
apply (metis assms(2) bsimp_fuse)
apply(subst bsimp_ASEQ1)
apply(auto)
done
lemma k0:
shows "flts (r # rs1) = flts [r] @ flts rs1"
apply(induct r arbitrary: rs1)
apply(auto)
done
lemma k00:
shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2"
apply(induct rs1 arbitrary: rs2)
apply(auto)
by (metis append.assoc k0)
lemma k0a:
shows "flts [AALTs bs rs] = map (fuse bs) rs"
apply(simp)
done
lemma k0b:
assumes "nonalt r" "r \<noteq> AZERO"
shows "flts [r] = [r]"
using assms
apply(case_tac r)
apply(simp_all)
done
lemma nn1:
assumes "nonnested (AALTs bs rs)"
shows "\<nexists>bs1 rs1. flts rs = [AALTs bs1 rs1]"
using assms
apply(induct rs rule: flts.induct)
apply(auto)
done
lemma nn1q:
assumes "nonnested (AALTs bs rs)"
shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set (flts rs)"
using assms
apply(induct rs rule: flts.induct)
apply(auto)
done
lemma nn1qq:
assumes "nonnested (AALTs bs rs)"
shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set rs"
using assms
apply(induct rs rule: flts.induct)
apply(auto)
done
lemma nn10:
assumes "nonnested (AALTs cs rs)"
shows "nonnested (AALTs (bs @ cs) rs)"
using assms
apply(induct rs arbitrary: cs bs)
apply(simp_all)
apply(case_tac a)
apply(simp_all)
done
lemma nn11a:
assumes "nonalt r"
shows "nonalt (fuse bs r)"
using assms
apply(induct r)
apply(auto)
done
lemma nn1a:
assumes "nonnested r"
shows "nonnested (fuse bs r)"
using assms
apply(induct bs r arbitrary: rule: fuse.induct)
apply(simp_all add: nn10)
done
lemma n0:
shows "nonnested (AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)"
apply(induct rs arbitrary: bs)
apply(auto)
apply (metis list.set_intros(1) nn1qq nonalt.elims(3))
apply (metis list.set_intros(2) nn1qq nonalt.elims(3))
by (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7))
lemma nn1c:
assumes "\<forall>r \<in> set rs. nonnested r"
shows "\<forall>r \<in> set (flts rs). nonalt r"
using assms
apply(induct rs rule: flts.induct)
apply(auto)
apply(rule nn11a)
by (metis nn1qq nonalt.elims(3))
lemma nn1bb:
assumes "\<forall>r \<in> set rs. nonalt r"
shows "nonnested (bsimp_AALTs bs rs)"
using assms
apply(induct bs rs rule: bsimp_AALTs.induct)
apply(auto)
apply (metis nn11a nonalt.simps(1) nonnested.elims(3))
using n0 by auto
lemma nn1b:
shows "nonnested (bsimp r)"
apply(induct r)
apply(simp_all)
apply(case_tac "bsimp r1 = AZERO")
apply(simp)
apply(case_tac "bsimp r2 = AZERO")
apply(simp)
apply(subst bsimp_ASEQ0)
apply(simp)
apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
apply(auto)[1]
apply(subst bsimp_ASEQ2)
apply (simp add: nn1a)
apply(subst bsimp_ASEQ1)
apply(auto)
apply(rule nn1bb)
apply(auto)
by (metis (mono_tags, hide_lams) imageE nn1c set_map)
lemma nn1d:
assumes "bsimp r = AALTs bs rs"
shows "\<forall>r1 \<in> set rs. \<forall> bs. r1 \<noteq> AALTs bs rs2"
using nn1b assms
by (metis nn1qq)
lemma nn_flts:
assumes "nonnested (AALTs bs rs)"
shows "\<forall>r \<in> set (flts rs). nonalt r"
using assms
apply(induct rs arbitrary: bs rule: flts.induct)
apply(auto)
done
lemma rt:
shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)"
apply(induct rs)
apply(simp)
apply(simp)
apply(subst k0)
apply(simp)
by (smt add_le_cancel_right add_mono bsimp_size flts.simps(1) flts_size k0 le_iff_add list.simps(9) map_append sum_list.Cons sum_list.append trans_le_add1)
lemma bsimp_AALTs_qq:
assumes "1 < length rs"
shows "bsimp_AALTs bs rs = AALTs bs rs"
using assms
apply(case_tac rs)
apply(simp)
apply(case_tac list)
apply(simp_all)
done
lemma bsimp_AALTs1:
assumes "nonalt r"
shows "bsimp_AALTs bs (flts [r]) = fuse bs r"
using assms
apply(case_tac r)
apply(simp_all)
done
lemma bbbbs:
assumes "good r" "r = AALTs bs1 rs"
shows "bsimp_AALTs bs (flts [r]) = AALTs bs (map (fuse bs1) rs)"
using assms
by (metis (no_types, lifting) Nil_is_map_conv append.left_neutral append_butlast_last_id bsimp_AALTs.elims butlast.simps(2) good.simps(4) good.simps(5) k0a map_butlast)
lemma bbbbs1:
shows "nonalt r \<or> (\<exists>bs rs. r = AALTs bs rs)"
using nonalt.elims(3) by auto
lemma good_fuse:
shows "good (fuse bs r) = good r"
apply(induct r arbitrary: bs)
apply(auto)
apply(case_tac r1)
apply(simp_all)
apply(case_tac r2)
apply(simp_all)
apply(case_tac r2)
apply(simp_all)
apply(case_tac r2)
apply(simp_all)
apply(case_tac r2)
apply(simp_all)
apply(case_tac r1)
apply(simp_all)
apply(case_tac r2)
apply(simp_all)
apply(case_tac r2)
apply(simp_all)
apply(case_tac r2)
apply(simp_all)
apply(case_tac r2)
apply(simp_all)
apply(case_tac x2a)
apply(simp_all)
apply(case_tac list)
apply(simp_all)
apply(case_tac x2a)
apply(simp_all)
apply(case_tac list)
apply(simp_all)
done
lemma good0:
assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. nonalt r"
shows "good (bsimp_AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)"
using assms
apply(induct bs rs rule: bsimp_AALTs.induct)
apply(auto simp add: good_fuse)
done
lemma good0a:
assumes "flts (map bsimp rs) \<noteq> Nil" "\<forall>r \<in> set (flts (map bsimp rs)). nonalt r"
shows "good (bsimp (AALTs bs rs)) \<longleftrightarrow> (\<forall>r \<in> set (flts (map bsimp rs)). good r)"
using assms
apply(simp)
apply(auto)
apply(subst (asm) good0)
apply(simp)
apply(auto)
apply(subst good0)
apply(simp)
apply(auto)
done
lemma flts0:
assumes "r \<noteq> AZERO" "nonalt r"
shows "flts [r] \<noteq> []"
using assms
apply(induct r)
apply(simp_all)
done
lemma flts1:
assumes "good r"
shows "flts [r] \<noteq> []"
using assms
apply(induct r)
apply(simp_all)
apply(case_tac x2a)
apply(simp)
apply(simp)
done
lemma flts2:
assumes "good r"
shows "\<forall>r' \<in> set (flts [r]). good r' \<and> nonalt r'"
using assms
apply(induct r)
apply(simp)
apply(simp)
apply(simp)
prefer 2
apply(simp)
apply(auto)[1]
apply (metis bsimp_AALTs.elims good.simps(4) good.simps(5) good.simps(6) good_fuse)
apply (metis bsimp_AALTs.elims good.simps(4) good.simps(5) good.simps(6) nn11a)
apply fastforce
apply(simp)
done
lemma flts3:
assumes "\<forall>r \<in> set rs. good r \<or> r = AZERO"
shows "\<forall>r \<in> set (flts rs). good r"
using assms
apply(induct rs arbitrary: rule: flts.induct)
apply(simp_all)
by (metis UnE flts2 k0a set_map)
lemma flts3b:
assumes "\<exists>r\<in>set rs. good r"
shows "flts rs \<noteq> []"
using assms
apply(induct rs arbitrary: rule: flts.induct)
apply(simp)
apply(simp)
apply(simp)
apply(auto)
done
lemma flts4:
assumes "bsimp_AALTs bs (flts rs) = AZERO"
shows "\<forall>r \<in> set rs. \<not> good r"
using assms
apply(induct rs arbitrary: bs rule: flts.induct)
apply(auto)
defer
apply (metis (no_types, lifting) Nil_is_append_conv append_self_conv2 bsimp_AALTs.elims butlast.simps(2) butlast_append flts3b nonalt.simps(1) nonalt.simps(2))
apply (metis arexp.distinct(7) bsimp_AALTs.elims flts2 good.simps(1) good.simps(2) good0 k0b list.distinct(1) list.inject nonalt.simps(3))
apply (metis arexp.distinct(3) arexp.distinct(7) bsimp_AALTs.elims fuse.simps(3) list.distinct(1) list.inject)
apply (metis arexp.distinct(7) bsimp_AALTs.elims good.simps(1) good_fuse list.distinct(1) list.inject)
apply (metis arexp.distinct(7) bsimp_AALTs.elims list.distinct(1) list.inject)
apply (metis arexp.distinct(7) bsimp_AALTs.elims flts2 good.simps(1) good.simps(33) good0 k0b list.distinct(1) list.inject nonalt.simps(6))
by (metis (no_types, lifting) Nil_is_append_conv append_Nil2 arexp.distinct(7) bsimp_AALTs.elims butlast.simps(2) butlast_append flts1 flts2 good.simps(1) good0 k0a)
lemma flts_nil:
assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
good (bsimp y) \<or> bsimp y = AZERO"
and "\<forall>r\<in>set rs. \<not> good (bsimp r)"
shows "flts (map bsimp rs) = []"
using assms
apply(induct rs)
apply(simp)
apply(simp)
apply(subst k0)
apply(simp)
by force
lemma flts_nil2:
assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
good (bsimp y) \<or> bsimp y = AZERO"
and "bsimp_AALTs bs (flts (map bsimp rs)) = AZERO"
shows "flts (map bsimp rs) = []"
using assms
apply(induct rs arbitrary: bs)
apply(simp)
apply(simp)
apply(subst k0)
apply(simp)
apply(subst (asm) k0)
apply(auto)
apply (metis flts.simps(1) flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
by (metis flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
lemma good_SEQ:
assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
shows "good (ASEQ bs r1 r2) = (good r1 \<and> good r2)"
using assms
apply(case_tac r1)
apply(simp_all)
apply(case_tac r2)
apply(simp_all)
apply(case_tac r2)
apply(simp_all)
apply(case_tac r2)
apply(simp_all)
apply(case_tac r2)
apply(simp_all)
done
lemma good1:
shows "good (bsimp a) \<or> bsimp a = AZERO"
apply(induct a taking: asize rule: measure_induct)
apply(case_tac x)
apply(simp)
apply(simp)
apply(simp)
prefer 3
apply(simp)
prefer 2
(* AALTs case *)
apply(simp only:)
apply(case_tac "x52")
apply(simp)
thm good0a
(* AALTs list at least one - case *)
apply(simp only: )
apply(frule_tac x="a" in spec)
apply(drule mp)
apply(simp)
(* either first element is good, or AZERO *)
apply(erule disjE)
prefer 2
apply(simp)
(* in the AZERO case, the size is smaller *)
apply(drule_tac x="AALTs x51 list" in spec)
apply(drule mp)
apply(simp add: asize0)
apply(subst (asm) bsimp.simps)
apply(subst (asm) bsimp.simps)
apply(assumption)
(* in the good case *)
apply(frule_tac x="AALTs x51 list" in spec)
apply(drule mp)
apply(simp add: asize0)
apply(erule disjE)
apply(rule disjI1)
apply(simp add: good0)
apply(subst good0)
apply (metis Nil_is_append_conv flts1 k0)
apply (metis ex_map_conv list.simps(9) nn1b nn1c)
apply(simp)
apply(subst k0)
apply(simp)
apply(auto)[1]
using flts2 apply blast
apply(subst (asm) good0)
prefer 3
apply(auto)[1]
apply auto[1]
apply (metis ex_map_conv nn1b nn1c)
(* in the AZERO case *)
apply(simp)
apply(frule_tac x="a" in spec)
apply(drule mp)
apply(simp)
apply(erule disjE)
apply(rule disjI1)
apply(subst good0)
apply(subst k0)
using flts1 apply blast
apply(auto)[1]
apply (metis (no_types, hide_lams) ex_map_conv list.simps(9) nn1b nn1c)
apply(auto)[1]
apply(subst (asm) k0)
apply(auto)[1]
using flts2 apply blast
apply(frule_tac x="AALTs x51 list" in spec)
apply(drule mp)
apply(simp add: asize0)
apply(erule disjE)
apply(simp)
apply(simp)
apply (metis add.left_commute flts_nil2 less_add_Suc1 less_imp_Suc_add list.distinct(1) list.set_cases nat.inject)
apply(subst (2) k0)
apply(simp)
(* SEQ case *)
apply(simp)
apply(case_tac "bsimp x42 = AZERO")
apply(simp)
apply(case_tac "bsimp x43 = AZERO")
apply(simp)
apply(subst (2) bsimp_ASEQ0)
apply(simp)
apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
apply(auto)[1]
apply(subst bsimp_ASEQ2)
using good_fuse apply force
apply(subst bsimp_ASEQ1)
apply(auto)
apply(subst good_SEQ)
apply(simp)
apply(simp)
apply(simp)
using less_add_Suc1 less_add_Suc2 by blast
lemma good1a:
assumes "L(erase a) \<noteq> {}"
shows "good (bsimp a)"
using good1 assms
using L_bsimp_erase by force
lemma flts_append:
"flts (xs1 @ xs2) = flts xs1 @ flts xs2"
apply(induct xs1 arbitrary: xs2 rule: rev_induct)
apply(auto)
apply(case_tac xs)
apply(auto)
apply(case_tac x)
apply(auto)
apply(case_tac x)
apply(auto)
done
lemma g1:
assumes "good (bsimp_AALTs bs rs)"
shows "bsimp_AALTs bs rs = AALTs bs rs \<or> (\<exists>r. rs = [r] \<and> bsimp_AALTs bs [r] = fuse bs r)"
using assms
apply(induct rs arbitrary: bs)
apply(simp)
apply(case_tac rs)
apply(simp only:)
apply(simp)
apply(case_tac list)
apply(simp)
by simp
lemma flts_0:
assumes "nonnested (AALTs bs rs)"
shows "\<forall>r \<in> set (flts rs). r \<noteq> AZERO"
using assms
apply(induct rs arbitrary: bs rule: flts.induct)
apply(simp)
apply(simp)
defer
apply(simp)
apply(simp)
apply(simp)
apply(simp)
apply(rule ballI)
apply(simp)
done
lemma flts_0a:
assumes "nonnested (AALTs bs rs)"
shows "AZERO \<notin> set (flts rs)"
using assms
using flts_0 by blast
lemma qqq1:
shows "AZERO \<notin> set (flts (map bsimp rs))"
by (metis ex_map_conv flts3 good.simps(1) good1)
fun nonazero :: "arexp \<Rightarrow> bool"
where
"nonazero AZERO = False"
| "nonazero r = True"
lemma flts_concat:
shows "flts rs = concat (map (\<lambda>r. flts [r]) rs)"
apply(induct rs)
apply(auto)
apply(subst k0)
apply(simp)
done
lemma flts_single1:
assumes "nonalt r" "nonazero r"
shows "flts [r] = [r]"
using assms
apply(induct r)
apply(auto)
done
lemma flts_qq:
assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y"
"\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
shows "flts (map bsimp rs) = rs"
using assms
apply(induct rs)
apply(simp)
apply(simp)
apply(subst k0)
apply(subgoal_tac "flts [bsimp a] = [a]")
prefer 2
apply(drule_tac x="a" in spec)
apply(drule mp)
apply(simp)
apply(auto)[1]
using good.simps(1) k0b apply blast
apply(auto)[1]
done
lemma test:
assumes "good r"
shows "bsimp r = r"
using assms
apply(induct r taking: "asize" rule: measure_induct)
apply(erule good.elims)
apply(simp_all)
apply(subst k0)
apply(subst (2) k0)
apply(subst flts_qq)
apply(auto)[1]
apply(auto)[1]
apply (metis append_Cons append_Nil bsimp_AALTs.simps(3) good.simps(1) k0b)
apply force+
apply (metis (no_types, lifting) add_Suc add_Suc_right asize.simps(5) bsimp.simps(1) bsimp_ASEQ.simps(19) less_add_Suc1 less_add_Suc2)
apply (metis add_Suc add_Suc_right arexp.distinct(5) arexp.distinct(7) asize.simps(4) asize.simps(5) bsimp.simps(1) bsimp.simps(2) bsimp_ASEQ1 good.simps(21) good.simps(8) less_add_Suc1 less_add_Suc2)
apply force+
apply (metis (no_types, lifting) add_Suc add_Suc_right arexp.distinct(5) arexp.distinct(7) asize.simps(4) asize.simps(5) bsimp.simps(1) bsimp.simps(2) bsimp_ASEQ1 good.simps(25) good.simps(8) less_add_Suc1 less_add_Suc2)
apply (metis add_Suc add_Suc_right arexp.distinct(7) asize.simps(4) bsimp.simps(2) bsimp_ASEQ1 good.simps(26) good.simps(8) less_add_Suc1 less_add_Suc2)
apply force+
done
lemma test2:
assumes "good r"
shows "bsimp r = r"
using assms
apply(induct r taking: "asize" rule: measure_induct)
apply(case_tac x)
apply(simp_all)
defer
(* AALT case *)
apply(subgoal_tac "1 < length x52")
prefer 2
apply(case_tac x52)
apply(simp)
apply(simp)
apply(case_tac list)
apply(simp)
apply(simp)
apply(subst bsimp_AALTs_qq)
prefer 2
apply(subst flts_qq)
apply(auto)[1]
apply(auto)[1]
apply(case_tac x52)
apply(simp)
apply(simp)
apply(case_tac list)
apply(simp)
apply(simp)
apply(auto)[1]
apply (metis (no_types, lifting) bsimp_AALTs.elims good.simps(6) length_Cons length_pos_if_in_set list.size(3) nat_neq_iff)
apply(simp)
apply(case_tac x52)
apply(simp)
apply(simp)
apply(case_tac list)
apply(simp)
apply(simp)
apply(subst k0)
apply(simp)
apply(subst (2) k0)
apply(simp)
apply (simp add: Suc_lessI flts1 one_is_add)
(* SEQ case *)
apply(case_tac "bsimp x42 = AZERO")
apply simp
apply (metis asize.elims good.simps(10) good.simps(11) good.simps(12) good.simps(2) good.simps(7) good.simps(9) good_SEQ less_add_Suc1)
apply(case_tac "\<exists>bs'. bsimp x42 = AONE bs'")
apply(auto)[1]
defer
apply(case_tac "bsimp x43 = AZERO")
apply(simp)
apply (metis bsimp.elims bsimp.simps(3) good.simps(10) good.simps(11) good.simps(12) good.simps(8) good.simps(9) good_SEQ less_add_Suc2)
apply(auto)
apply (subst bsimp_ASEQ1)
apply(auto)[3]
apply(auto)[1]
apply (metis bsimp.simps(3) good.simps(2) good_SEQ less_add_Suc1)
apply (metis bsimp.simps(3) good.simps(2) good_SEQ less_add_Suc1 less_add_Suc2)
apply (subst bsimp_ASEQ2)
apply(drule_tac x="x42" in spec)
apply(drule mp)
apply(simp)
apply(drule mp)
apply (metis bsimp.elims bsimp.simps(3) good.simps(10) good.simps(11) good.simps(2) good_SEQ)
apply(simp)
done
lemma bsimp_idem:
shows "bsimp (bsimp r) = bsimp r"
using test good1
by force
lemma contains_ex1:
assumes "a = AALTs bs1 [AZERO, AONE bs2]" "a >> bs"
shows "bsimp a >> bs"
using assms
apply(simp)
apply(erule contains.cases)
apply(auto)
using contains.simps apply blast
apply(erule contains.cases)
apply(auto)
using contains0 apply fastforce
using contains.simps by blast
lemma contains_ex2:
assumes "a = AALTs bs1 [AZERO, AONE bs2, AALTs bs5 [AONE bs3, AZERO, AONE bs4]]" "a >> bs"
shows "bsimp a >> bs"
using assms
apply(simp)
apply(erule contains.cases)
apply(auto)
using contains.simps apply blast
apply(erule contains.cases)
apply(auto)
using contains3b apply blast
apply(erule contains.cases)
apply(auto)
apply(erule contains.cases)
apply(auto)
apply (metis contains.intros(4) contains.intros(5) contains0 fuse.simps(2))
apply(erule contains.cases)
apply(auto)
using contains.simps apply blast
apply(erule contains.cases)
apply(auto)
apply (metis contains.intros(4) contains.intros(5) contains0 fuse.simps(2))
apply(erule contains.cases)
apply(auto)
apply(erule contains.cases)
apply(auto)
done
lemma contains48:
assumes "\<And>x2aa bs bs1. \<lbrakk>x2aa \<in> set x2a; fuse bs x2aa >> bs @ bs1\<rbrakk> \<Longrightarrow> x2aa >> bs1"
"AALTs (bs @ x1) x2a >> bs @ bs1"
shows "AALTs x1 x2a >> bs1"
using assms
apply(induct x2a arbitrary: bs x1 bs1)
apply(auto)
apply(erule contains.cases)
apply(auto)
apply(erule contains.cases)
apply(auto)
apply (simp add: contains.intros(4))
using contains.intros(5) by blast
lemma contains49:
assumes "fuse bs a >> bs @ bs1"
shows "a >> bs1"
using assms
apply(induct a arbitrary: bs bs1)
apply(auto)
using contains.simps apply blast
apply(erule contains.cases)
apply(auto)
apply(rule contains.intros)
apply(erule contains.cases)
apply(auto)
apply(rule contains.intros)
apply(erule contains.cases)
apply(auto)
apply(rule contains.intros)
apply(auto)[2]
prefer 2
apply(erule contains.cases)
apply(auto)
apply (simp add: contains.intros(6))
using contains.intros(7) apply blast
using contains48 by blast
lemma contains50:
assumes "bsimp_AALTs bs rs2 >> bs @ bs1"
shows "bsimp_AALTs bs (rs1 @ rs2) >> bs @ bs1"
using assms
apply(induct rs1 arbitrary: bs rs2 bs1)
apply(simp)
apply(auto)
apply(case_tac rs1)
apply(simp)
apply(case_tac rs2)
apply(simp)
using contains.simps apply blast
apply(simp)
apply(case_tac list)
apply(simp)
apply(rule contains.intros)
back
apply(rule contains.intros)
using contains49 apply blast
apply(simp)
using contains.intros(5) apply blast
apply(simp)
by (metis bsimp_AALTs.elims contains.intros(4) contains.intros(5) contains49 list.distinct(1))
lemma contains51:
assumes "bsimp_AALTs bs [r] >> bs @ bs1"
shows "bsimp_AALTs bs ([r] @ rs2) >> bs @ bs1"
using assms
apply(induct rs2 arbitrary: bs r bs1)
apply(simp)
apply(auto)
using contains.intros(4) contains49 by blast
lemma contains51a:
assumes "bsimp_AALTs bs rs2 >> bs @ bs1"
shows "bsimp_AALTs bs (rs2 @ [r]) >> bs @ bs1"
using assms
apply(induct rs2 arbitrary: bs r bs1)
apply(simp)
apply(auto)
using contains.simps apply blast
apply(case_tac rs2)
apply(auto)
using contains3b contains49 apply blast
apply(case_tac list)
apply(auto)
apply(erule contains.cases)
apply(auto)
using contains.intros(4) apply auto[1]
apply(erule contains.cases)
apply(auto)
apply (simp add: contains.intros(4) contains.intros(5))
apply (simp add: contains.intros(5))
apply(erule contains.cases)
apply(auto)
apply (simp add: contains.intros(4))
apply(erule contains.cases)
apply(auto)
using contains.intros(4) contains.intros(5) apply blast
using contains.intros(5) by blast
lemma contains51b:
assumes "bsimp_AALTs bs rs >> bs @ bs1"
shows "bsimp_AALTs bs (rs @ rs2) >> bs @ bs1"
using assms
apply(induct rs2 arbitrary: bs rs bs1)
apply(simp)
using contains51a by fastforce
lemma contains51c:
assumes "AALTs (bs @ bs2) rs >> bs @ bs1"
shows "bsimp_AALTs bs (map (fuse bs2) rs) >> bs @ bs1"
using assms
apply(induct rs arbitrary: bs bs1 bs2)
apply(auto)
apply(erule contains.cases)
apply(auto)
apply(erule contains.cases)
apply(auto)
using contains0 contains51 apply auto[1]
by (metis append.left_neutral append_Cons contains50 list.simps(9))
lemma contains51d:
assumes "fuse bs r >> bs @ bs1"
shows "bsimp_AALTs bs (flts [r]) >> bs @ bs1"
using assms
apply(induct r arbitrary: bs bs1)
apply(auto)
by (simp add: contains51c)
lemma contains52:
assumes "\<exists>r \<in> set rs. (fuse bs r) >> bs @ bs1"
shows "bsimp_AALTs bs (flts rs) >> bs @ bs1"
using assms
apply(induct rs arbitrary: bs bs1)
apply(simp)
apply(auto)
defer
apply (metis contains50 k0)
apply(subst k0)
apply(rule contains51b)
using contains51d by blast
lemma contains55:
assumes "a >> bs"
shows "bsimp a >> bs"
using assms
apply(induct a bs arbitrary:)
apply(auto intro: contains.intros)
apply(case_tac "bsimp a1 = AZERO")
apply(simp)
using contains.simps apply blast
apply(case_tac "bsimp a2 = AZERO")
apply(simp)
using contains.simps apply blast
apply(case_tac "\<exists>bs. bsimp a1 = AONE bs")
apply(auto)[1]
apply(rotate_tac 1)
apply(erule contains.cases)
apply(auto)
apply (simp add: b1 contains0 fuse_append)
apply (simp add: bsimp_ASEQ1 contains.intros(3))
prefer 2
apply(case_tac rs)
apply(simp)
using contains.simps apply blast
apply (metis contains50 k0)
(* AALTS case *)
apply(rule contains52)
apply(rule_tac x="bsimp r" in bexI)
apply(auto)
using contains0 by blast
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 r0)
apply(case_tac "bnullable a")
apply (metis append.assoc b2 bnullable_correctness erase_fuse r0)
apply(case_tac rs)
apply(simp)
apply(simp)
apply(auto)[1]
apply (metis bnullable_correctness erase_fuse)+
done
lemma qq4a:
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: r0)
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: r0)
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: qq4a)
apply(simp)
apply(auto)
apply(case_tac list)
apply(simp)
apply(simp)
apply (simp add: r0)
apply(case_tac "bnullable (ASEQ x41 x42 x43)")
apply(case_tac list)
apply(simp)
apply(simp)
apply (simp add: r0)
apply(simp)
using qq4a r1 r2 by auto
lemma k1:
assumes "\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; bnullable x2aa\<rbrakk> \<Longrightarrow> bmkeps x2aa = bmkeps (bsimp x2aa)"
"\<exists>x\<in>set x2a. bnullable x"
shows "bmkeps (AALTs x1 (flts x2a)) = bmkeps (AALTs x1 (flts (map bsimp x2a)))"
using assms
apply(induct x2a)
apply fastforce
apply(simp)
apply(subst k0)
apply(subst (2) k0)
apply(auto)[1]
apply (metis b3 k0 list.set_intros(1) qs3 r0)
by (smt b3 imageI insert_iff k0 list.set(2) qq3 qs3 r0 r1 set_map)
lemma bmkeps_simp:
assumes "bnullable r"
shows "bmkeps r = bmkeps (bsimp r)"
using assms
apply(induct r)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
prefer 3
apply(simp)
apply(case_tac "bsimp r1 = AZERO")
apply(simp)
apply(auto)[1]
apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(1) mkeps_nullable)
apply(case_tac "bsimp r2 = AZERO")
apply(simp)
apply(auto)[1]
apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(1) mkeps_nullable)
apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
apply(auto)[1]
apply(subst b1)
apply(subst b2)
apply(simp add: b3[symmetric])
apply(simp)
apply(subgoal_tac "bsimp_ASEQ x1 (bsimp r1) (bsimp r2) = ASEQ x1 (bsimp r1) (bsimp r2)")
prefer 2
apply (smt b3 bnullable.elims(2) bsimp_ASEQ.simps(17) bsimp_ASEQ.simps(19) bsimp_ASEQ.simps(20) bsimp_ASEQ.simps(21) bsimp_ASEQ.simps(22) bsimp_ASEQ.simps(24) bsimp_ASEQ.simps(25) bsimp_ASEQ.simps(26) bsimp_ASEQ.simps(27) bsimp_ASEQ.simps(29) bsimp_ASEQ.simps(30) bsimp_ASEQ.simps(31))
apply(simp)
apply(simp)
thm q3
apply(subst q3[symmetric])
apply simp
using b3 qq4a apply auto[1]
apply(subst qs3)
apply simp
using k1 by blast
thm bmkeps_retrieve bmkeps_simp bder_retrieve
lemma bmkeps_bder_AALTs:
assumes "\<exists>r \<in> set rs. bnullable (bder c r)"
shows "bmkeps (bder c (bsimp_AALTs bs rs)) = bmkeps (bsimp_AALTs bs (map (bder c) rs))"
using assms
apply(induct rs)
apply(simp)
apply(simp)
apply(auto)
apply(case_tac rs)
apply(simp)
apply (metis (full_types) Prf_injval bder_retrieve bmkeps_retrieve bnullable_correctness erase_bder erase_fuse mkeps_nullable retrieve_fuse2)
apply(simp)
apply(case_tac rs)
apply(simp_all)
done
lemma bbs0:
shows "blexer_simp r [] = blexer r []"
apply(simp add: blexer_def blexer_simp_def)
done
lemma bbs1:
shows "blexer_simp r [c] = blexer r [c]"
apply(simp add: blexer_def blexer_simp_def)
apply(auto)
defer
using b3 apply auto[1]
using b3 apply auto[1]
apply(subst bmkeps_simp[symmetric])
apply(simp)
apply(simp)
done
lemma oo:
shows "(case (blexer (der c r) s) of None \<Rightarrow> None | Some v \<Rightarrow> Some (injval r c v)) = blexer r (c # s)"
apply(simp add: blexer_correctness)
done
lemma XXX2_helper:
assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y"
"\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
shows "flts (map (bsimp \<circ> bder c) (flts (map bsimp rs))) = flts (map (bsimp \<circ> bder c) rs)"
using assms
apply(induct rs arbitrary: c)
apply(simp)
apply(simp)
apply(subst k0)
apply(simp add: flts_append)
apply(subst (2) k0)
apply(simp add: flts_append)
apply(subgoal_tac "flts [a] = [a]")
prefer 2
using good.simps(1) k0b apply blast
apply(simp)
done
lemma bmkeps_good:
assumes "good a"
shows "bmkeps (bsimp a) = bmkeps a"
using assms
using test2 by auto
lemma xxx_bder:
assumes "good r"
shows "L (erase r) \<noteq> {}"
using assms
apply(induct r rule: good.induct)
apply(auto simp add: Sequ_def)
done
lemma xxx_bder2:
assumes "L (erase (bsimp r)) = {}"
shows "bsimp r = AZERO"
using assms xxx_bder test2 good1
by blast
lemma XXX2aa:
assumes "good a"
shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
using assms
by (simp add: test2)
lemma XXX2aa_ders:
assumes "good a"
shows "bsimp (bders (bsimp a) s) = bsimp (bders a s)"
using assms
by (simp add: test2)
lemma XXX4a:
shows "good (bders_simp (bsimp r) s) \<or> bders_simp (bsimp r) s = AZERO"
apply(induct s arbitrary: r rule: rev_induct)
apply(simp)
apply (simp add: good1)
apply(simp add: bders_simp_append)
apply (simp add: good1)
done
lemma XXX4a_good:
assumes "good a"
shows "good (bders_simp a s) \<or> bders_simp a s = AZERO"
using assms
apply(induct s arbitrary: a rule: rev_induct)
apply(simp)
apply(simp add: bders_simp_append)
apply (simp add: good1)
done
lemma XXX4a_good_cons:
assumes "s \<noteq> []"
shows "good (bders_simp a s) \<or> bders_simp a s = AZERO"
using assms
apply(case_tac s)
apply(auto)
using XXX4a by blast
lemma XXX4b:
assumes "good a" "L (erase (bders_simp a s)) \<noteq> {}"
shows "good (bders_simp a s)"
using assms
apply(induct s arbitrary: a)
apply(simp)
apply(simp)
apply(subgoal_tac "L (erase (bder a aa)) = {} \<or> L (erase (bder a aa)) \<noteq> {}")
prefer 2
apply(auto)[1]
apply(erule disjE)
apply(subgoal_tac "bsimp (bder a aa) = AZERO")
prefer 2
using L_bsimp_erase xxx_bder2 apply auto[1]
apply(simp)
apply (metis L.simps(1) XXX4a erase.simps(1))
apply(drule_tac x="bsimp (bder a aa)" in meta_spec)
apply(drule meta_mp)
apply simp
apply(rule good1a)
apply(auto)
done
lemma bders_AZERO:
shows "bders AZERO s = AZERO"
and "bders_simp AZERO s = AZERO"
apply (induct s)
apply(auto)
done
lemma LA:
assumes "\<Turnstile> v : ders s (erase r)"
shows "retrieve (bders r s) v = retrieve r (flex (erase r) id s v)"
using assms
apply(induct s arbitrary: r v rule: rev_induct)
apply(simp)
apply(simp add: bders_append ders_append)
apply(subst bder_retrieve)
apply(simp)
apply(drule Prf_injval)
by (simp add: flex_append)
lemma LB:
assumes "s \<in> (erase r) \<rightarrow> v"
shows "retrieve r v = retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))"
using assms
apply(induct s arbitrary: r v rule: rev_induct)
apply(simp)
apply(subgoal_tac "v = mkeps (erase r)")
prefer 2
apply (simp add: Posix1(1) Posix_determ Posix_mkeps nullable_correctness)
apply(simp)
apply(simp add: flex_append ders_append)
by (metis Posix_determ Posix_flex Posix_injval Posix_mkeps ders_snoc lexer_correctness(2) lexer_flex)
lemma LB_sym:
assumes "s \<in> (erase r) \<rightarrow> v"
shows "retrieve r v = retrieve r (flex (erase r) id s (mkeps (erase (bders r s))))"
using assms
by (simp add: LB)
lemma LC:
assumes "s \<in> (erase r) \<rightarrow> v"
shows "retrieve r v = retrieve (bders r s) (mkeps (erase (bders r s)))"
apply(simp)
by (metis LA LB Posix1(1) assms lexer_correct_None lexer_flex mkeps_nullable)
lemma L0:
assumes "bnullable a"
shows "retrieve (bsimp a) (mkeps (erase (bsimp a))) = retrieve a (mkeps (erase a))"
using assms b3 bmkeps_retrieve bmkeps_simp bnullable_correctness
by (metis b3 bmkeps_retrieve bmkeps_simp bnullable_correctness)
thm bmkeps_retrieve
lemma L0a:
assumes "s \<in> L(erase a)"
shows "retrieve (bsimp (bders a s)) (mkeps (erase (bsimp (bders a s)))) =
retrieve (bders a s) (mkeps (erase (bders a s)))"
using assms
by (metis L0 bnullable_correctness erase_bders lexer_correct_None lexer_flex)
lemma L0aa:
assumes "s \<in> L (erase a)"
shows "[] \<in> erase (bsimp (bders a s)) \<rightarrow> mkeps (erase (bsimp (bders a s)))"
using assms
by (metis Posix_mkeps b3 bnullable_correctness erase_bders lexer_correct_None lexer_flex)
lemma L0aaa:
assumes "[c] \<in> L (erase a)"
shows "[c] \<in> (erase a) \<rightarrow> flex (erase a) id [c] (mkeps (erase (bder c a)))"
using assms
by (metis bders.simps(1) bders.simps(2) erase_bders lexer_correct_None lexer_correct_Some lexer_flex option.inject)
lemma L0aaaa:
assumes "[c] \<in> L (erase a)"
shows "[c] \<in> (erase a) \<rightarrow> flex (erase a) id [c] (mkeps (erase (bders a [c])))"
using assms
using L0aaa by auto
lemma L02:
assumes "bnullable (bder c a)"
shows "retrieve (bsimp a) (flex (erase (bsimp a)) id [c] (mkeps (erase (bder c (bsimp a))))) =
retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a))))"
using assms
apply(simp)
using bder_retrieve L0 bmkeps_simp bmkeps_retrieve L0 LA LB
apply(subst bder_retrieve[symmetric])
apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder mkeps_nullable nullable_correctness)
apply(simp)
done
lemma L02_bders:
assumes "bnullable (bders a s)"
shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (erase (bders (bsimp a) s)))) =
retrieve (bders (bsimp a) s) (mkeps (erase (bders (bsimp a) s)))"
using assms
by (metis LA L_bsimp_erase bnullable_correctness ders_correctness erase_bders mkeps_nullable nullable_correctness)
lemma L03:
assumes "bnullable (bder c a)"
shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) =
bmkeps (bsimp (bder c (bsimp a)))"
using assms
by (metis L0 L_bsimp_erase bmkeps_retrieve bnullable_correctness der_correctness erase_bder nullable_correctness)
lemma L04:
assumes "bnullable (bder c a)"
shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) =
retrieve (bsimp (bder c (bsimp a))) (mkeps (erase (bsimp (bder c (bsimp a)))))"
using assms
by (metis L0 L_bsimp_erase bnullable_correctness der_correctness erase_bder nullable_correctness)
lemma L05:
assumes "bnullable (bder c a)"
shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) =
retrieve (bsimp (bder c (bsimp a))) (mkeps (erase (bsimp (bder c (bsimp a)))))"
using assms
using L04 by auto
lemma L06:
assumes "bnullable (bder c a)"
shows "bmkeps (bder c (bsimp a)) = bmkeps (bsimp (bder c (bsimp a)))"
using assms
by (metis L03 L_bsimp_erase bmkeps_retrieve bnullable_correctness der_correctness erase_bder nullable_correctness)
lemma L07:
assumes "s \<in> L (erase r)"
shows "retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))
= retrieve (bders r s) (mkeps (erase (bders r s)))"
using assms
using LB LC lexer_correct_Some by auto
lemma L06_2:
assumes "bnullable (bders a [c,d])"
shows "bmkeps (bders (bsimp a) [c,d]) = bmkeps (bsimp (bders (bsimp a) [c,d]))"
using assms
apply(simp)
by (metis L_bsimp_erase bmkeps_simp bnullable_correctness der_correctness erase_bder nullable_correctness)
lemma L06_bders:
assumes "bnullable (bders a s)"
shows "bmkeps (bders (bsimp a) s) = bmkeps (bsimp (bders (bsimp a) s))"
using assms
by (metis L_bsimp_erase bmkeps_simp bnullable_correctness ders_correctness erase_bders nullable_correctness)
lemma LLLL:
shows "L (erase a) = L (erase (bsimp a))"
and "L (erase a) = {flat v | v. \<Turnstile> v: (erase a)}"
and "L (erase a) = {flat v | v. \<Turnstile> v: (erase (bsimp a))}"
using L_bsimp_erase apply(blast)
apply (simp add: L_flat_Prf)
using L_bsimp_erase L_flat_Prf apply(auto)[1]
done
lemma L07XX:
assumes "s \<in> L (erase a)"
shows "s \<in> erase a \<rightarrow> flex (erase a) id s (mkeps (ders s (erase a)))"
using assms
by (meson lexer_correct_None lexer_correctness(1) lexer_flex)
lemma LX0:
assumes "s \<in> L r"
shows "decode (bmkeps (bders (intern r) s)) r = Some(flex r id s (mkeps (ders s r)))"
by (metis assms blexer_correctness blexer_def lexer_correct_None lexer_flex)
lemma L1:
assumes "s \<in> r \<rightarrow> v"
shows "decode (bmkeps (bders (intern r) s)) r = Some v"
using assms
by (metis blexer_correctness blexer_def lexer_correctness(1) option.distinct(1))
lemma L2:
assumes "s \<in> (der c r) \<rightarrow> v"
shows "decode (bmkeps (bders (intern r) (c # s))) r = Some (injval r c v)"
using assms
apply(subst bmkeps_retrieve)
using Posix1(1) lexer_correct_None lexer_flex apply fastforce
using MAIN_decode
apply(subst MAIN_decode[symmetric])
apply(simp)
apply (meson Posix1(1) lexer_correct_None lexer_flex mkeps_nullable)
apply(simp)
apply(subgoal_tac "v = flex (der c r) id s (mkeps (ders s (der c r)))")
prefer 2
apply (metis Posix_determ lexer_correctness(1) lexer_flex option.distinct(1))
apply(simp)
apply(subgoal_tac "injval r c (flex (der c r) id s (mkeps (ders s (der c r)))) =
(flex (der c r) ((\<lambda>v. injval r c v) o id) s (mkeps (ders s (der c r))))")
apply(simp)
using flex_fun_apply by blast
lemma L3:
assumes "s2 \<in> (ders s1 r) \<rightarrow> v"
shows "decode (bmkeps (bders (intern r) (s1 @ s2))) r = Some (flex r id s1 v)"
using assms
apply(induct s1 arbitrary: r s2 v rule: rev_induct)
apply(simp)
using L1 apply blast
apply(simp add: ders_append)
apply(drule_tac x="r" in meta_spec)
apply(drule_tac x="x # s2" in meta_spec)
apply(drule_tac x="injval (ders xs r) x v" in meta_spec)
apply(drule meta_mp)
defer
apply(simp)
apply(simp add: flex_append)
by (simp add: Posix_injval)
lemma bders_snoc:
"bder c (bders a s) = bders a (s @ [c])"
apply(simp add: bders_append)
done
lemma QQ1:
shows "bsimp (bders (bsimp a) []) = bders_simp (bsimp a) []"
apply(simp)
apply(simp add: bsimp_idem)
done
lemma QQ2:
shows "bsimp (bders (bsimp a) [c]) = bders_simp (bsimp a) [c]"
apply(simp)
done
lemma XXX2a_long:
assumes "good a"
shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
using assms
apply(induct a arbitrary: c taking: asize rule: measure_induct)
apply(case_tac x)
apply(simp)
apply(simp)
apply(simp)
prefer 3
apply(simp)
apply(simp)
apply(auto)[1]
apply(case_tac "x42 = AZERO")
apply(simp)
apply(case_tac "x43 = AZERO")
apply(simp)
using test2 apply force
apply(case_tac "\<exists>bs. x42 = AONE bs")
apply(clarify)
apply(simp)
apply(subst bsimp_ASEQ1)
apply(simp)
using b3 apply force
using bsimp_ASEQ0 test2 apply force
thm good_SEQ test2
apply (simp add: good_SEQ test2)
apply (simp add: good_SEQ test2)
apply(case_tac "x42 = AZERO")
apply(simp)
apply(case_tac "x43 = AZERO")
apply(simp)
apply (simp add: bsimp_ASEQ0)
apply(case_tac "\<exists>bs. x42 = AONE bs")
apply(clarify)
apply(simp)
apply(subst bsimp_ASEQ1)
apply(simp)
using bsimp_ASEQ0 test2 apply force
apply (simp add: good_SEQ test2)
apply (simp add: good_SEQ test2)
apply (simp add: good_SEQ test2)
(* AALTs case *)
apply(simp)
using test2 by fastforce
lemma bder_bsimp_AALTs:
shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)"
apply(induct bs rs rule: bsimp_AALTs.induct)
apply(simp)
apply(simp)
apply (simp add: bder_fuse)
apply(simp)
done
lemma flts_nothing:
assumes "\<forall>r \<in> set rs. r \<noteq> AZERO" "\<forall>r \<in> set rs. nonalt r"
shows "flts rs = rs"
using assms
apply(induct rs rule: flts.induct)
apply(auto)
done
lemma flts_flts:
assumes "\<forall>r \<in> set rs. good r"
shows "flts (flts rs) = flts rs"
using assms
apply(induct rs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
apply(case_tac x)
apply(simp)
apply(simp)
apply(case_tac a)
apply(simp_all add: bder_fuse flts_append)
apply(subgoal_tac "\<forall>r \<in> set x52. r \<noteq> AZERO")
prefer 2
apply (metis Nil_is_append_conv bsimp_AALTs.elims good.simps(1) good.simps(5) good0 list.distinct(1) n0 nn1b split_list_last test2)
apply(subgoal_tac "\<forall>r \<in> set x52. nonalt r")
prefer 2
apply (metis n0 nn1b test2)
by (metis flts_fuse flts_nothing)
lemma iii:
assumes "bsimp_AALTs bs rs \<noteq> AZERO"
shows "rs \<noteq> []"
using assms
apply(induct bs rs rule: bsimp_AALTs.induct)
apply(auto)
done
lemma CT1_SEQ:
shows "bsimp (ASEQ bs a1 a2) = bsimp (ASEQ bs (bsimp a1) (bsimp a2))"
apply(simp add: bsimp_idem)
done
lemma CT1:
shows "bsimp (AALTs bs as) = bsimp (AALTs bs (map bsimp as))"
apply(induct as arbitrary: bs)
apply(simp)
apply(simp)
by (simp add: bsimp_idem comp_def)
lemma CT1a:
shows "bsimp (AALT bs a1 a2) = bsimp(AALT bs (bsimp a1) (bsimp a2))"
by (metis CT1 list.simps(8) list.simps(9))
lemma WWW2:
shows "bsimp (bsimp_AALTs bs1 (flts (map bsimp as1))) =
bsimp_AALTs bs1 (flts (map bsimp as1))"
by (metis bsimp.simps(2) bsimp_idem)
lemma CT1b:
shows "bsimp (bsimp_AALTs bs as) = bsimp (bsimp_AALTs bs (map bsimp as))"
apply(induct bs as rule: bsimp_AALTs.induct)
apply(auto simp add: bsimp_idem)
apply (simp add: bsimp_fuse bsimp_idem)
by (metis bsimp_idem comp_apply)
(* CT *)
lemma CTa:
assumes "\<forall>r \<in> set as. nonalt r \<and> r \<noteq> AZERO"
shows "flts as = as"
using assms
apply(induct as)
apply(simp)
apply(case_tac as)
apply(simp)
apply (simp add: k0b)
using flts_nothing by auto
lemma CT0:
assumes "\<forall>r \<in> set as1. nonalt r \<and> r \<noteq> AZERO"
shows "flts [bsimp_AALTs bs1 as1] = flts (map (fuse bs1) as1)"
using assms CTa
apply(induct as1 arbitrary: bs1)
apply(simp)
apply(simp)
apply(case_tac as1)
apply(simp)
apply(simp)
proof -
fix a :: arexp and as1a :: "arexp list" and bs1a :: "bit list" and aa :: arexp and list :: "arexp list"
assume a1: "nonalt a \<and> a \<noteq> AZERO \<and> nonalt aa \<and> aa \<noteq> AZERO \<and> (\<forall>r\<in>set list. nonalt r \<and> r \<noteq> AZERO)"
assume a2: "\<And>as. \<forall>r\<in>set as. nonalt r \<and> r \<noteq> AZERO \<Longrightarrow> flts as = as"
assume a3: "as1a = aa # list"
have "flts [a] = [a]"
using a1 k0b by blast
then show "fuse bs1a a # fuse bs1a aa # map (fuse bs1a) list = flts (fuse bs1a a # fuse bs1a aa # map (fuse bs1a) list)"
using a3 a2 a1 by (metis (no_types) append.left_neutral append_Cons flts_fuse k00 k0b list.simps(9))
qed
lemma CT01:
assumes "\<forall>r \<in> set as1. nonalt r \<and> r \<noteq> AZERO" "\<forall>r \<in> set as2. nonalt r \<and> r \<noteq> AZERO"
shows "flts [bsimp_AALTs bs1 as1, bsimp_AALTs bs2 as2] = flts ((map (fuse bs1) as1) @ (map (fuse bs2) as2))"
using assms CT0
by (metis k0 k00)
lemma CT_exp:
assumes "\<forall>a \<in> set as. bsimp (bder c (bsimp a)) = bsimp (bder c a)"
shows "map bsimp (map (bder c) as) = map bsimp (map (bder c) (map bsimp as))"
using assms
apply(induct as)
apply(auto)
done
lemma asize_set:
assumes "a \<in> set as"
shows "asize a < Suc (sum_list (map asize as))"
using assms
apply(induct as arbitrary: a)
apply(auto)
using le_add2 le_less_trans not_less_eq by blast
lemma L_erase_bder_simp:
shows "L (erase (bsimp (bder a r))) = L (der a (erase (bsimp r)))"
using L_bsimp_erase der_correctness by auto
lemma PPP0:
assumes "s \<in> r \<rightarrow> v"
shows "(bders (intern r) s) >> code v"
using assms
by (smt L07 L1 LX0 Posix1(1) Posix_Prf contains6 erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable option.inject retrieve_code)
thm L07 L1 LX0 Posix1(1) Posix_Prf contains6 erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable option.inject retrieve_code
lemma PPP0_isar:
assumes "s \<in> r \<rightarrow> v"
shows "(bders (intern r) s) >> code v"
proof -
from assms have a1: "\<Turnstile> v : r" using Posix_Prf by simp
from assms have "s \<in> L r" using Posix1(1) by auto
then have "[] \<in> L (ders s r)" by (simp add: ders_correctness Ders_def)
then have a2: "\<Turnstile> mkeps (ders s r) : ders s r"
by (simp add: mkeps_nullable nullable_correctness)
have "retrieve (bders (intern r) s) (mkeps (ders s r)) =
retrieve (intern r) (flex r id s (mkeps (ders s r)))" using a2 LA LB bder_retrieve by simp
also have "... = retrieve (intern r) v"
using LB assms by auto
also have "... = code v" using a1 by (simp add: retrieve_code)
finally have "retrieve (bders (intern r) s) (mkeps (ders s r)) = code v" by simp
moreover
have "\<Turnstile> mkeps (ders s r) : erase (bders (intern r) s)" using a2 by simp
then have "bders (intern r) s >> retrieve (bders (intern r) s) (mkeps (ders s r))"
by (rule contains6)
ultimately
show "(bders (intern r) s) >> code v" by simp
qed
lemma PPP0b:
assumes "s \<in> r \<rightarrow> v"
shows "(intern r) >> code v"
using assms
using Posix_Prf contains2 by auto
lemma PPP0_eq:
assumes "s \<in> r \<rightarrow> v"
shows "(intern r >> code v) = (bders (intern r) s >> code v)"
using assms
using PPP0_isar PPP0b by blast
lemma f_cont1:
assumes "fuse bs1 a >> bs"
shows "\<exists>bs2. bs = bs1 @ bs2"
using assms
apply(induct a arbitrary: bs1 bs)
apply(auto elim: contains.cases)
done
lemma f_cont2:
assumes "bsimp_AALTs bs1 as >> bs"
shows "\<exists>bs2. bs = bs1 @ bs2"
using assms
apply(induct bs1 as arbitrary: bs rule: bsimp_AALTs.induct)
apply(auto elim: contains.cases f_cont1)
done
lemma contains_SEQ1:
assumes "bsimp_ASEQ bs r1 r2 >> bsX"
shows "\<exists>bs1 bs2. r1 >> bs1 \<and> r2 >> bs2 \<and> bsX = bs @ bs1 @ bs2"
using assms
apply(auto)
apply(case_tac "r1 = AZERO")
apply(auto)
using contains.simps apply blast
apply(case_tac "r2 = AZERO")
apply(auto)
apply(simp add: bsimp_ASEQ0)
using contains.simps apply blast
apply(case_tac "\<exists>bsX. r1 = AONE bsX")
apply(auto)
apply(simp add: bsimp_ASEQ2)
apply (metis append_assoc contains.intros(1) contains49 f_cont1)
apply(simp add: bsimp_ASEQ1)
apply(erule contains.cases)
apply(auto)
done
lemma contains59:
assumes "AALTs bs rs >> bs2"
shows "\<exists>r \<in> set rs. (fuse bs r) >> bs2"
using assms
apply(induct rs arbitrary: bs bs2)
apply(auto)
apply(erule contains.cases)
apply(auto)
apply(erule contains.cases)
apply(auto)
using contains0 by blast
lemma contains60:
assumes "\<exists>r \<in> set rs. fuse bs r >> bs2"
shows "AALTs bs rs >> bs2"
using assms
apply(induct rs arbitrary: bs bs2)
apply(auto)
apply (metis contains3b contains49 f_cont1)
using contains.intros(5) f_cont1 by blast
lemma contains61:
assumes "bsimp_AALTs bs rs >> bs2"
shows "\<exists>r \<in> set rs. (fuse bs r) >> bs2"
using assms
apply(induct arbitrary: bs2 rule: bsimp_AALTs.induct)
apply(auto)
using contains.simps apply blast
using contains59 by fastforce
lemma contains61b:
assumes "bsimp_AALTs bs rs >> bs2"
shows "\<exists>r \<in> set (flts rs). (fuse bs r) >> bs2"
using assms
apply(induct bs rs arbitrary: bs2 rule: bsimp_AALTs.induct)
apply(auto)
using contains.simps apply blast
using contains51d contains61 f_cont1 apply blast
by (metis bsimp_AALTs.simps(3) contains52 contains61 f_cont2)
lemma contains61a:
assumes "\<exists>r \<in> set rs. (fuse bs r) >> bs2"
shows "bsimp_AALTs bs rs >> bs2"
using assms
apply(induct rs arbitrary: bs2 bs)
apply(auto)
apply (metis bsimp_AALTs.elims contains60 list.distinct(1) list.inject list.set_intros(1))
by (metis append_Cons append_Nil contains50 f_cont2)
lemma contains62:
assumes "bsimp_AALTs bs (rs1 @ rs2) >> bs2"
shows "bsimp_AALTs bs rs1 >> bs2 \<or> bsimp_AALTs bs rs2 >> bs2"
using assms
apply -
apply(drule contains61)
apply(auto)
apply(case_tac rs1)
apply(auto)
apply(case_tac list)
apply(auto)
apply (simp add: contains60)
apply(case_tac list)
apply(auto)
apply (simp add: contains60)
apply (meson contains60 list.set_intros(2))
apply(case_tac rs2)
apply(auto)
apply(case_tac list)
apply(auto)
apply (simp add: contains60)
apply(case_tac list)
apply(auto)
apply (simp add: contains60)
apply (meson contains60 list.set_intros(2))
done
lemma contains63:
assumes "AALTs bs (map (fuse bs1) rs) >> bs3"
shows "AALTs (bs @ bs1) rs >> bs3"
using assms
apply(induct rs arbitrary: bs bs1 bs3)
apply(auto elim: contains.cases)
apply(erule contains.cases)
apply(auto)
apply (simp add: contains0 contains60 fuse_append)
by (metis contains.intros(5) contains59 f_cont1)
lemma contains64:
assumes "bsimp_AALTs bs (flts rs1 @ flts rs2) >> bs2" "\<forall>r \<in> set rs2. \<not> fuse bs r >> bs2"
shows "bsimp_AALTs bs (flts rs1) >> bs2"
using assms
apply(induct rs2 arbitrary: rs1 bs bs2)
apply(auto)
apply(drule_tac x="rs1" in meta_spec)
apply(drule_tac x="bs" in meta_spec)
apply(drule_tac x="bs2" in meta_spec)
apply(drule meta_mp)
apply(drule contains61)
apply(auto)
using contains51b contains61a f_cont1 apply blast
apply(subst (asm) k0)
apply(auto)
prefer 2
using contains50 contains61a f_cont1 apply blast
apply(case_tac a)
apply(auto)
by (metis contains60 fuse_append)
lemma contains65:
assumes "bsimp_AALTs bs (flts rs) >> bs2"
shows "\<exists>r \<in> set rs. (fuse bs r) >> bs2"
using assms
apply(induct rs arbitrary: bs bs2 taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
apply(case_tac x)
apply(auto elim: contains.cases)
apply(case_tac list)
apply(auto elim: contains.cases)
apply(case_tac a)
apply(auto elim: contains.cases)
apply(drule contains61)
apply(auto)
apply (metis contains60 fuse_append)
apply(case_tac lista)
apply(auto elim: contains.cases)
apply(subst (asm) k0)
apply(drule contains62)
apply(auto)
apply(case_tac a)
apply(auto elim: contains.cases)
apply(case_tac x52)
apply(auto elim: contains.cases)
apply(case_tac list)
apply(auto elim: contains.cases)
apply (simp add: contains60 fuse_append)
apply(erule contains.cases)
apply(auto)
apply (metis append.left_neutral contains0 contains60 fuse.simps(4) in_set_conv_decomp)
apply(erule contains.cases)
apply(auto)
apply (metis contains0 contains60 fuse.simps(4) list.set_intros(1) list.set_intros(2))
apply (simp add: contains.intros(5) contains63)
apply(case_tac aa)
apply(auto)
apply (meson contains60 contains61 contains63)
apply(subst (asm) k0)
apply(drule contains64)
apply(auto)[1]
by (metis append_Nil2 bsimp_AALTs.simps(2) contains50 contains61a contains64 f_cont2 flts.simps(1))
lemma contains55a:
assumes "bsimp r >> bs"
shows "r >> bs"
using assms
apply(induct r arbitrary: bs)
apply(auto)
apply(frule contains_SEQ1)
apply(auto)
apply (simp add: contains.intros(3))
apply(frule f_cont2)
apply(auto)
apply(drule contains65)
apply(auto)
using contains0 contains49 contains60 by blast
lemma PPP1_eq:
shows "bsimp r >> bs \<longleftrightarrow> r >> bs"
using contains55 contains55a by blast
lemma retrieve_code_bder:
assumes "\<Turnstile> v : der c r"
shows "code (injval r c v) = retrieve (bder c (intern r)) v"
using assms
by (simp add: Prf_injval bder_retrieve retrieve_code)
lemma Etrans:
assumes "a >> s" "s = t"
shows "a >> t"
using assms by simp
lemma retrieve_code_bders:
assumes "\<Turnstile> v : ders s r"
shows "code (flex r id s v) = retrieve (bders (intern r) s) v"
using assms
apply(induct s arbitrary: v r rule: rev_induct)
apply(auto simp add: ders_append flex_append bders_append)
apply (simp add: retrieve_code)
apply(frule Prf_injval)
apply(drule_tac meta_spec)+
apply(drule meta_mp)
apply(assumption)
apply(simp)
apply(subst bder_retrieve)
apply(simp)
apply(simp)
done
lemma contains70:
assumes "s \<in> L(r)"
shows "bders (intern r) s >> code (flex r id s (mkeps (ders s r)))"
apply(subst PPP0_eq[symmetric])
apply (meson assms lexer_correct_None lexer_correctness(1) lexer_flex)
by (metis L07XX PPP0b assms erase_intern)
definition FC where
"FC a s v = retrieve a (flex (erase a) id s v)"
definition FE where
"FE a s = retrieve a (flex (erase a) id s (mkeps (ders s (erase a))))"
definition PV where
"PV r s v = flex r id s v"
definition PX where
"PX r s = PV r s (mkeps (ders s r))"
lemma FE_PX:
shows "FE r s = retrieve r (PX (erase r) s)"
unfolding FE_def PX_def PV_def by(simp)
lemma FE_PX_code:
assumes "s \<in> L r"
shows "FE (intern r) s = code (PX r s)"
unfolding FE_def PX_def PV_def
using assms
by (metis L07XX Posix_Prf erase_intern retrieve_code)
lemma PV_id[simp]:
shows "PV r [] v = v"
by (simp add: PV_def)
lemma PX_id[simp]:
shows "PX r [] = mkeps r"
by (simp add: PX_def)
lemma PV_cons:
shows "PV r (c # s) v = injval r c (PV (der c r) s v)"
apply(simp add: PV_def flex_fun_apply)
done
lemma PX_cons:
shows "PX r (c # s) = injval r c (PX (der c r) s)"
apply(simp add: PX_def PV_cons)
done
lemma PV_append:
shows "PV r (s1 @ s2) v = PV r s1 (PV (ders s1 r) s2 v)"
apply(simp add: PV_def flex_append)
by (simp add: flex_fun_apply2)
lemma PX_append:
shows "PX r (s1 @ s2) = PV r s1 (PX (ders s1 r) s2)"
by (simp add: PV_append PX_def ders_append)
lemma code_PV0:
shows "PV r (c # s) v = injval r c (PV (der c r) s v)"
unfolding PX_def PV_def
apply(simp)
by (simp add: flex_injval)
lemma code_PX0:
shows "PX r (c # s) = injval r c (PX (der c r) s)"
unfolding PX_def
apply(simp add: code_PV0)
done
lemma Prf_PV:
assumes "\<Turnstile> v : ders s r"
shows "\<Turnstile> PV r s v : r"
using assms unfolding PX_def PV_def
apply(induct s arbitrary: v r)
apply(simp)
apply(simp)
by (simp add: Prf_injval flex_injval)
lemma Prf_PX:
assumes "s \<in> L r"
shows "\<Turnstile> PX r s : r"
using assms unfolding PX_def PV_def
using L1 LX0 Posix_Prf lexer_correct_Some by fastforce
lemma PV1:
assumes "\<Turnstile> v : ders s r"
shows "(intern r) >> code (PV r s v)"
using assms
by (simp add: Prf_PV contains2)
lemma PX1:
assumes "s \<in> L r"
shows "(intern r) >> code (PX r s)"
using assms
by (simp add: Prf_PX contains2)
lemma PX2:
assumes "s \<in> L (der c r)"
shows "bder c (intern r) >> code (injval r c (PX (der c r) s))"
using assms
by (simp add: Prf_PX contains6 retrieve_code_bder)
lemma PX2a:
assumes "c # s \<in> L r"
shows "bder c (intern r) >> code (injval r c (PX (der c r) s))"
using assms
using PX2 lexer_correct_None by force
lemma PX2b:
assumes "c # s \<in> L r"
shows "bder c (intern r) >> code (PX r (c # s))"
using assms unfolding PX_def PV_def
by (metis Der_def L07XX PV_def PX2a PX_def Posix_determ Posix_injval der_correctness erase_intern mem_Collect_eq)
lemma PV3:
assumes "\<Turnstile> v : ders s r"
shows "bders (intern r) s >> code (PV r s v)"
using assms
using PX_def PV_def contains70
by (simp add: contains6 retrieve_code_bders)
lemma PX3:
assumes "s \<in> L r"
shows "bders (intern r) s >> code (PX r s)"
using assms
using PX_def PV_def contains70 by auto
lemma PV_bders_iff:
assumes "\<Turnstile> v : ders s r"
shows "bders (intern r) s >> code (PV r s v) \<longleftrightarrow> (intern r) >> code (PV r s v)"
by (simp add: PV1 PV3 assms)
lemma PX_bders_iff:
assumes "s \<in> L r"
shows "bders (intern r) s >> code (PX r s) \<longleftrightarrow> (intern r) >> code (PX r s)"
by (simp add: PX1 PX3 assms)
lemma PX4:
assumes "(s1 @ s2) \<in> L r"
shows "bders (intern r) (s1 @ s2) >> code (PX r (s1 @ s2))"
using assms
by (simp add: PX3)
lemma PX_bders_iff2:
assumes "(s1 @ s2) \<in> L r"
shows "bders (intern r) (s1 @ s2) >> code (PX r (s1 @ s2)) \<longleftrightarrow>
(intern r) >> code (PX r (s1 @ s2))"
by (simp add: PX1 PX3 assms)
lemma PV_bders_iff3:
assumes "\<Turnstile> v : ders (s1 @ s2) r"
shows "bders (intern r) (s1 @ s2) >> code (PV r (s1 @ s2) v) \<longleftrightarrow>
bders (intern r) s1 >> code (PV r (s1 @ s2) v)"
by (metis PV3 PV_append Prf_PV assms ders_append)
lemma PX_bders_iff3:
assumes "(s1 @ s2) \<in> L r"
shows "bders (intern r) (s1 @ s2) >> code (PX r (s1 @ s2)) \<longleftrightarrow>
bders (intern r) s1 >> code (PX r (s1 @ s2))"
by (metis Ders_def L07XX PV_append PV_def PX4 PX_def Posix_Prf assms contains6 ders_append ders_correctness erase_bders erase_intern mem_Collect_eq retrieve_code_bders)
lemma PV_bder_iff:
assumes "\<Turnstile> v : ders (s1 @ [c]) r"
shows "bder c (bders (intern r) s1) >> code (PV r (s1 @ [c]) v) \<longleftrightarrow>
bders (intern r) s1 >> code (PV r (s1 @ [c]) v)"
by (simp add: PV_bders_iff3 assms bders_snoc)
lemma PV_bder_IFF:
assumes "\<Turnstile> v : ders (s1 @ c # s2) r"
shows "bder c (bders (intern r) s1) >> code (PV r (s1 @ c # s2) v) \<longleftrightarrow>
bders (intern r) s1 >> code (PV r (s1 @ c # s2) v)"
by (metis LA PV3 PV_def Prf_PV assms bders_append code_PV0 contains7 ders.simps(2) erase_bders erase_intern retrieve_code_bders)
lemma PX_bder_iff:
assumes "(s1 @ [c]) \<in> L r"
shows "bder c (bders (intern r) s1) >> code (PX r (s1 @ [c])) \<longleftrightarrow>
bders (intern r) s1 >> code (PX r (s1 @ [c]))"
by (simp add: PX_bders_iff3 assms bders_snoc)
lemma PV_bder_iff2:
assumes "\<Turnstile> v : ders (c # s1) r"
shows "bders (bder c (intern r)) s1 >> code (PV r (c # s1) v) \<longleftrightarrow>
bder c (intern r) >> code (PV r (c # s1) v)"
by (metis PV3 Prf_PV assms bders.simps(2) code_PV0 contains7 ders.simps(2) erase_intern retrieve_code)
lemma PX_bder_iff2:
assumes "(c # s1) \<in> L r"
shows "bders (bder c (intern r)) s1 >> code (PX r (c # s1)) \<longleftrightarrow>
bder c (intern r) >> code (PX r (c # s1))"
using PX2b PX3 assms by force
lemma FC_id:
shows "FC r [] v = retrieve r v"
by (simp add: FC_def)
lemma FC_char:
shows "FC r [c] v = retrieve r (injval (erase r) c v)"
by (simp add: FC_def)
lemma FC_char2:
assumes "\<Turnstile> v : der c (erase r)"
shows "FC r [c] v = FC (bder c r) [] v"
using assms
by (simp add: FC_char FC_id bder_retrieve)
lemma FC_bders_iff:
assumes "\<Turnstile> v : ders s (erase r)"
shows "bders r s >> FC r s v \<longleftrightarrow> r >> FC r s v"
unfolding FC_def
by (simp add: assms contains8_iff)
lemma FC_bder_iff:
assumes "\<Turnstile> v : der c (erase r)"
shows "bder c r >> FC r [c] v \<longleftrightarrow> r >> FC r [c] v"
apply(subst FC_bders_iff[symmetric])
apply(simp add: assms)
apply(simp)
done
lemma FC_bnullable0:
assumes "bnullable r"
shows "FC r [] (mkeps (erase r)) = FC (bsimp r) [] (mkeps (erase (bsimp r)))"
unfolding FC_def
by (simp add: L0 assms)
lemma FC_nullable2:
assumes "bnullable (bders a s)"
shows "FC (bsimp a) s (mkeps (erase (bders (bsimp a) s))) =
FC (bders (bsimp a) s) [] (mkeps (erase (bders (bsimp a) s)))"
unfolding FC_def
using L02_bders assms by auto
lemma FC_nullable3:
assumes "bnullable (bders a s)"
shows "FC a s (mkeps (erase (bders a s))) =
FC (bders a s) [] (mkeps (erase (bders a s)))"
unfolding FC_def
using LA assms bnullable_correctness mkeps_nullable by fastforce
lemma FE_contains0:
assumes "bnullable r"
shows "r >> FE r []"
by (simp add: FE_def assms bnullable_correctness contains6 mkeps_nullable)
lemma FE_contains1:
assumes "bnullable (bders r s)"
shows "r >> FE r s"
by (metis FE_def Prf_flex assms bnullable_correctness contains6 erase_bders mkeps_nullable)
lemma FE_bnullable0:
assumes "bnullable r"
shows "FE r [] = FE (bsimp r) []"
unfolding FE_def
by (simp add: L0 assms)
lemma FE_nullable1:
assumes "bnullable (bders r s)"
shows "FE r s = FE (bders r s) []"
unfolding FE_def
using LA assms bnullable_correctness mkeps_nullable by fastforce
lemma FE_contains2:
assumes "bnullable (bders r s)"
shows "r >> FE (bders r s) []"
by (metis FE_contains1 FE_nullable1 assms)
lemma FE_contains3:
assumes "bnullable (bder c r)"
shows "r >> FE (bsimp (bder c r)) []"
by (metis FE_def L0 assms bder_retrieve bders.simps(1) bnullable_correctness contains7a erase_bder erase_bders flex.simps(1) id_apply mkeps_nullable)
lemma FE_contains4:
assumes "bnullable (bders r s)"
shows "r >> FE (bsimp (bders r s)) []"
using FE_bnullable0 FE_contains2 assms by auto
(*
lemma FE_bnullable2:
assumes "bnullable (bder c r)"
shows "FE r [c] = FE (bsimp r) [c]"
unfolding FE_def
apply(simp)
using L0
apply(subst FE_nullable1)
using assms apply(simp)
apply(subst FE_bnullable0)
using assms apply(simp)
unfolding FE_def
apply(simp)
apply(subst L0)
using assms apply(simp)
apply(subst bder_retrieve[symmetric])
using LLLL(1) L_erase_bder_simp assms bnullable_correctness mkeps_nullable nullable_correctness apply b last
apply(simp)
find_theorems "retrieve _ (injval _ _ _)"
find_theorems "retrieve (bsimp _) _"
lemma FE_nullable3:
assumes "bnullable (bders a s)"
shows "FE (bsimp a) s = FE a s"
unfolding FE_def
using LA assms bnullable_correctness mkeps_nullable by fas tforce
*)
lemma FC4:
assumes "\<Turnstile> v : ders s (erase a)"
shows "FC a s v = FC (bders a s) [] v"
unfolding FC_def by (simp add: LA assms)
lemma FC5:
assumes "nullable (erase a)"
shows "FC a [] (mkeps (erase a)) = FC (bsimp a) [] (mkeps (erase (bsimp a)))"
unfolding FC_def
using L0 assms bnullable_correctness by auto
lemma FC6:
assumes "nullable (erase (bders a s))"
shows "FC (bsimp a) s (mkeps (erase (bders (bsimp a) s))) = FC a s (mkeps (erase (bders a s)))"
apply(subst (2) FC4)
using assms mkeps_nullable apply auto[1]
apply(subst FC_nullable2)
using assms bnullable_correctness apply blast
oops
(*
lemma FC_bnullable:
assumes "bnullable (bders r s)"
shows "FC r s (mkeps (erase r)) = FC (bsimp r) s (mkeps (erase (bsimp r)))"
using assms
unfolding FC_def
using L0 L0a bder_retrieve L02_bders L04
apply(induct s arbitrary: r)
apply(simp add: FC_id)
apply (simp add: L0 assms)
apply(simp add: bders_append)
apply(drule_tac x="bder a r" in meta_spec)
apply(drule meta_mp)
apply(simp)
apply(subst bder_retrieve[symmetric])
apply(simp)
*)
lemma FC_bnullable:
assumes "bnullable (bders r s)"
shows "FC r s (mkeps (ders s (erase r))) = FC (bsimp r) s (mkeps (ders s (erase (bsimp r))))"
unfolding FC_def
oops
lemma AA0:
assumes "bnullable (bders r s)"
assumes "bders r s >> FC r s (mkeps (erase (bders r s)))"
shows "bders (bsimp r) s >> FC (bsimp r) s (mkeps (erase (bders (bsimp r) s)))"
using assms
apply(subst (asm) FC_bders_iff)
apply(simp)
using bnullable_correctness mkeps_nullable apply fastforce
apply(subst FC_bders_iff)
apply(simp)
apply (metis LLLL(1) bnullable_correctness ders_correctness erase_bders mkeps_nullable nullable_correctness)
apply(simp add: PPP1_eq)
unfolding FC_def
find_theorems "retrieve (bsimp _) _"
using contains7b
oops
lemma AA1:
assumes "\<Turnstile> v : der c (erase r)" "\<Turnstile> v : der c (erase (bsimp r))"
assumes "bder c r >> FC r [c] v"
shows "bder c (bsimp r) >> FC (bsimp r) [c] v"
using assms
apply(subst (asm) FC_bder_iff)
apply(rule assms)
apply(subst FC_bder_iff)
apply(rule assms)
apply(simp add: PPP1_eq)
unfolding FC_def
find_theorems "retrieve (bsimp _) _"
using contains7b
oops
lemma PX_bder_simp_iff:
assumes "\<Turnstile> v: ders (s1 @ s2) r"
shows "bders (bsimp (bders (intern r) s1)) s2 >> code (PV r (s1 @ s2) v) \<longleftrightarrow>
bders (intern r) s1 >> code (PV r (s1 @ s2) v)"
using assms
apply(induct s2 arbitrary: r s1 v)
apply(simp)
apply (simp add: PV3 contains55)
apply(drule_tac x="r" in meta_spec)
apply(drule_tac x="s1 @ [a]" in meta_spec)
apply(drule_tac x="v" in meta_spec)
apply(simp)
apply(simp add: bders_append)
apply(subst (asm) PV_bder_IFF)
oops
lemma in1:
assumes "AALTs bsX rsX \<in> set rs"
shows "\<forall>r \<in> set rsX. fuse bsX r \<in> set (flts rs)"
using assms
apply(induct rs arbitrary: bsX rsX)
apply(auto)
by (metis append_assoc in_set_conv_decomp k0)
lemma in2a:
assumes "nonnested (bsimp r)" "\<not>nonalt(bsimp r)"
shows "(\<exists>bsX rsX. r = AALTs bsX rsX) \<or> (\<exists>bsX rX1 rX2. r = ASEQ bsX rX1 rX2 \<and> bnullable rX1)"
using assms
apply(induct r)
apply(auto)
by (metis arexp.distinct(25) b3 bnullable.simps(2) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1 nonalt.elims(3) nonalt.simps(2))
lemma in2:
assumes "bder c r >> bs2" and
"AALTs bsX rsX = bsimp r" and
"XX \<in> set rsX" "nonnested (bsimp r)"
shows "bder c (fuse bsX XX) >> bs2"
sorry
lemma
assumes "bder c a >> bs"
shows "bder c (bsimp a) >> bs"
using assms
apply(induct a arbitrary: c bs)
apply(auto elim: contains.cases)
apply(case_tac "bnullable a1")
apply(simp)
prefer 2
apply(simp)
apply(erule contains.cases)
apply(auto)
apply(case_tac "(bsimp a1) = AZERO")
apply(simp)
apply (metis append_Nil2 contains0 contains49 fuse.simps(1))
apply(case_tac "(bsimp a2a) = AZERO")
apply(simp)
apply (metis bder.simps(1) bsimp.simps(1) bsimp_ASEQ0 contains.intros(3) contains55)
apply(case_tac "\<exists>bsX. (bsimp a1) = AONE bsX")
apply(auto)[1]
using b3 apply fastforce
apply(subst bsimp_ASEQ1)
apply(auto)[3]
apply(simp)
apply(subgoal_tac "\<not> bnullable (bsimp a1)")
prefer 2
using b3 apply blast
apply(simp)
apply (simp add: contains.intros(3) contains55)
(* SEQ nullable case *)
apply(erule contains.cases)
apply(auto)
apply(erule contains.cases)
apply(auto)
apply(case_tac "(bsimp a1) = AZERO")
apply(simp)
apply (metis append_Nil2 contains0 contains49 fuse.simps(1))
apply(case_tac "(bsimp a2a) = AZERO")
apply(simp)
apply (metis bder.simps(1) bsimp.simps(1) bsimp_ASEQ0 contains.intros(3) contains55)
apply(case_tac "\<exists>bsX. (bsimp a1) = AONE bsX")
apply(auto)[1]
using contains.simps apply blast
apply(subst bsimp_ASEQ1)
apply(auto)[3]
apply(simp)
apply(subgoal_tac "bnullable (bsimp a1)")
prefer 2
using b3 apply blast
apply(simp)
apply (metis contains.intros(3) contains.intros(4) contains55 self_append_conv2)
apply(erule contains.cases)
apply(auto)
apply(case_tac "(bsimp a1) = AZERO")
apply(simp)
using b3 apply force
apply(case_tac "(bsimp a2) = AZERO")
apply(simp)
apply (metis bder.simps(1) bsimp_ASEQ0 bsimp_ASEQ_fuse contains0 contains49 f_cont1)
apply(case_tac "\<exists>bsX. (bsimp a1) = AONE bsX")
apply(auto)[1]
apply (metis append_assoc bder_fuse bmkeps.simps(1) bmkeps_simp bsimp_ASEQ2 contains0 contains49 f_cont1)
apply(subst bsimp_ASEQ1)
apply(auto)[3]
apply(simp)
apply(subgoal_tac "bnullable (bsimp a1)")
prefer 2
using b3 apply blast
apply(simp)
apply (metis bmkeps_simp contains.intros(4) contains.intros(5) contains0 contains49 f_cont1)
apply(erule contains.cases)
apply(auto)
(* ALT case *)
apply(drule contains59)
apply(auto)
apply(subst bder_bsimp_AALTs)
apply(rule contains61a)
apply(auto)
apply(subgoal_tac "bsimp r \<in> set (map bsimp x2a)")
prefer 2
apply simp
apply(case_tac "bsimp r = AZERO")
apply (metis Nil_is_append_conv bder.simps(1) bsimp_AALTs.elims bsimp_AALTs.simps(2) contains49 contains61 f_cont2 list.distinct(1) split_list_last)
apply(subgoal_tac "nonnested (bsimp r)")
prefer 2
using nn1b apply blast
apply(case_tac "nonalt (bsimp r)")
apply(rule_tac x="bsimp r" in bexI)
apply (metis contains0 contains49 f_cont1)
apply (metis append_Cons flts_append in_set_conv_decomp k0 k0b)
(* AALTS case *)
apply(subgoal_tac "\<exists>rsX bsX. (bsimp r) = AALTs bsX rsX \<and> (\<forall>r \<in> set rsX. nonalt r)")
prefer 2
apply (metis n0 nonalt.elims(3))
apply(auto)
apply(subgoal_tac "bsimp r \<in> set (map bsimp x2a)")
prefer 2
apply (metis imageI list.set_map)
apply(simp)
apply(simp add: image_def)
apply(erule bexE)
apply(subgoal_tac "AALTs bsX rsX \<in> set (map bsimp x2a)")
prefer 2
apply simp
apply(drule in1)
apply(subgoal_tac "rsX \<noteq> []")
prefer 2
apply (metis arexp.distinct(7) good.simps(4) good1)
by (metis contains0 contains49 f_cont1 in2 list.exhaust list.set_intros(1))
lemma CONTAINS1:
assumes "a >> bs"
shows "a >>2 bs"
using assms
apply(induct a bs)
apply(auto intro: contains2.intros)
done
lemma CONTAINS2:
assumes "a >>2 bs"
shows "a >> bs"
using assms
apply(induct a bs)
apply(auto intro: contains.intros)
using contains55 by auto
lemma CONTAINS2_IFF:
shows "a >> bs \<longleftrightarrow> a >>2 bs"
using CONTAINS1 CONTAINS2 by blast
lemma
assumes "bders (intern r) s >>2 bs"
shows "bders_simp (intern r) s >>2 bs"
using assms
apply(induct s arbitrary: r bs)
apply(simp)
apply(simp)
oops
lemma
assumes "s \<in> L r"
shows "(bders_simp (intern r) s >> code (PX r s)) \<longleftrightarrow> ((intern r) >> code (PX r s))"
using assms
apply(induct s arbitrary: r rule: rev_induct)
apply(simp)
apply(simp add: bders_simp_append)
apply(simp add: PPP1_eq)
find_theorems "retrieve (bders _ _) _"
find_theorems "_ >> retrieve _ _"
find_theorems "bsimp _ >> _"
oops
lemma PX4a:
assumes "(s1 @ s2) \<in> L r"
shows "bders (intern r) (s1 @ s2) >> code (PV r s1 (PX (ders s1 r) s2))"
using PX4[OF assms]
apply(simp add: PX_append)
done
lemma PV5:
assumes "s2 \<in> (ders s1 r) \<rightarrow> v"
shows "bders (intern r) (s1 @ s2) >> code (PV r s1 v)"
by (simp add: PPP0_isar PV_def Posix_flex assms)
lemma PV6:
assumes "s2 \<in> (ders s1 r) \<rightarrow> v"
shows "bders (bders (intern r) s1) s2 >> code (PV r s1 v)"
using PV5 assms bders_append by auto
find_theorems "retrieve (bders _ _) _"
find_theorems "_ >> retrieve _ _"
find_theorems "bder _ _ >> _"
lemma OO0_PX:
assumes "s \<in> L r"
shows "bders (intern r) s >> code (PX r s)"
using assms
by (simp add: PX3)
lemma OO1:
assumes "[c] \<in> r \<rightarrow> v"
shows "bder c (intern r) >> code v"
using assms
using PPP0_isar by force
lemma OO1a:
assumes "[c] \<in> L r"
shows "bder c (intern r) >> code (PX r [c])"
using assms unfolding PX_def PV_def
using contains70 by fastforce
lemma OO12:
assumes "[c1, c2] \<in> L r"
shows "bders (intern r) [c1, c2] >> code (PX r [c1, c2])"
using assms
using PX_def PV_def contains70 by presburger
lemma OO2:
assumes "[c] \<in> L r"
shows "bders_simp (intern r) [c] >> code (PX r [c])"
using assms
using OO1a Posix1(1) contains55 by auto
lemma OO22:
assumes "[c1, c2] \<in> L r"
shows "bders_simp (intern r) [c1, c2] >> code (PX r [c1, c2])"
using assms
apply(simp)
apply(rule contains55)
apply(rule Etrans)
thm contains7
apply(rule contains7)
oops
lemma contains70:
assumes "s \<in> L(r)"
shows "bders_simp (intern r) s >> code (flex r id s (mkeps (ders s r)))"
using assms
apply(induct s arbitrary: r rule: rev_induct)
apply(simp)
apply (simp add: contains2 mkeps_nullable nullable_correctness)
apply(simp add: bders_simp_append flex_append)
apply(simp add: PPP1_eq)
apply(rule Etrans)
apply(rule_tac v="flex r id xs (mkeps (ders (xs @ [x]) r))" in contains7)
oops
thm L07XX PPP0b erase_intern
find_theorems "retrieve (bders _ _) _"
find_theorems "_ >> retrieve _ _"
find_theorems "bder _ _ >> _"
lemma PPP3:
assumes "\<Turnstile> v : ders s (erase a)"
shows "bders a s >> retrieve a (flex (erase a) id s v)"
using LA[OF assms] contains6 erase_bders assms by metis
find_theorems "bder _ _ >> _"
lemma
fixes n :: nat
shows "(\<Sum>i \<in> {0..n}. i) = n * (n + 1) div 2"
apply(induct n)
apply(simp)
apply(simp)
done
lemma COUNTEREXAMPLE:
assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
shows "bsimp (bder c (bsimp r)) = bsimp (bder c r)"
apply(simp_all add: assms)
oops
lemma COUNTEREXAMPLE:
assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
shows "bsimp r = r"
apply(simp_all add: assms)
oops
lemma COUNTEREXAMPLE:
assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
shows "bsimp r = XXX"
and "bder c r = XXX"
and "bder c (bsimp r) = XXX"
and "bsimp (bder c (bsimp r)) = XXX"
and "bsimp (bder c r) = XXX"
apply(simp_all add: assms)
oops
lemma COUNTEREXAMPLE_contains1:
assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
and "bsimp (bder c r) >> bs"
shows "bsimp (bder c (bsimp r)) >> bs"
using assms
apply(auto elim!: contains.cases)
apply(rule Etrans)
apply(rule contains.intros)
apply(rule contains.intros)
apply(simp)
apply(rule Etrans)
apply(rule contains.intros)
apply(rule contains.intros)
apply(simp)
done
lemma COUNTEREXAMPLE_contains2:
assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
and "bsimp (bder c (bsimp r)) >> bs"
shows "bsimp (bder c r) >> bs"
using assms
apply(auto elim!: contains.cases)
apply(rule Etrans)
apply(rule contains.intros)
apply(rule contains.intros)
apply(simp)
apply(rule Etrans)
apply(rule contains.intros)
apply(rule contains.intros)
apply(simp)
done
end