|
544
|
1 |
theory BlexerSimp
|
|
|
2 |
imports Blexer
|
|
|
3 |
begin
|
|
|
4 |
|
|
|
5 |
|
|
|
6 |
fun flts :: "arexp list \<Rightarrow> arexp list"
|
|
|
7 |
where
|
|
|
8 |
"flts [] = []"
|
|
|
9 |
| "flts (AZERO # rs) = flts rs"
|
|
|
10 |
| "flts ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
|
|
|
11 |
| "flts (r1 # rs) = r1 # flts rs"
|
|
|
12 |
|
|
|
13 |
|
|
|
14 |
|
|
|
15 |
fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
|
|
|
16 |
where
|
|
|
17 |
"bsimp_ASEQ _ AZERO _ = AZERO"
|
|
|
18 |
| "bsimp_ASEQ _ _ AZERO = AZERO"
|
|
|
19 |
| "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"
|
|
|
20 |
| "bsimp_ASEQ bs1 r1 r2 = ASEQ bs1 r1 r2"
|
|
|
21 |
|
|
|
22 |
lemma bsimp_ASEQ0[simp]:
|
|
|
23 |
shows "bsimp_ASEQ bs r1 AZERO = AZERO"
|
|
|
24 |
by (case_tac r1)(simp_all)
|
|
|
25 |
|
|
|
26 |
lemma bsimp_ASEQ1:
|
|
|
27 |
assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<nexists>bs. r1 = AONE bs"
|
|
|
28 |
shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2"
|
|
|
29 |
using assms
|
|
|
30 |
apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
|
|
|
31 |
apply(auto)
|
|
|
32 |
done
|
|
|
33 |
|
|
|
34 |
lemma bsimp_ASEQ2[simp]:
|
|
|
35 |
shows "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"
|
|
|
36 |
by (case_tac r2) (simp_all)
|
|
|
37 |
|
|
|
38 |
|
|
|
39 |
fun bsimp_AALTs :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
|
|
|
40 |
where
|
|
|
41 |
"bsimp_AALTs _ [] = AZERO"
|
|
|
42 |
| "bsimp_AALTs bs1 [r] = fuse bs1 r"
|
|
|
43 |
| "bsimp_AALTs bs1 rs = AALTs bs1 rs"
|
|
|
44 |
|
|
|
45 |
lemma bmkeps_fuse:
|
|
|
46 |
assumes "bnullable r"
|
|
|
47 |
shows "bmkeps (fuse bs r) = bs @ bmkeps r"
|
|
|
48 |
using assms
|
|
|
49 |
by (induct r rule: bnullable.induct) (auto)
|
|
|
50 |
|
|
|
51 |
lemma bmkepss_fuse:
|
|
|
52 |
assumes "bnullables rs"
|
|
|
53 |
shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs"
|
|
|
54 |
using assms
|
|
|
55 |
apply(induct rs arbitrary: bs)
|
|
|
56 |
apply(auto simp add: bmkeps_fuse bnullable_fuse)
|
|
|
57 |
done
|
|
|
58 |
|
|
|
59 |
lemma bder_fuse:
|
|
|
60 |
shows "bder c (fuse bs a) = fuse bs (bder c a)"
|
|
|
61 |
apply(induct a arbitrary: bs c)
|
|
|
62 |
apply(simp_all)
|
|
|
63 |
done
|
|
|
64 |
|
|
|
65 |
|
|
|
66 |
|
|
|
67 |
|
|
550
|
68 |
fun ABIncludedByC :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" where
|
|
|
69 |
"ABIncludedByC a b c f subseteqPred = subseteqPred (f a b) c"
|
|
|
70 |
|
|
|
71 |
fun furtherSEQ :: "rexp \<Rightarrow> rexp \<Rightarrow> rexp list" and
|
|
|
72 |
turnIntoTerms :: "rexp \<Rightarrow> rexp list "
|
|
|
73 |
where
|
|
|
74 |
"furtherSEQ ONE r2 = turnIntoTerms r2 "
|
|
|
75 |
| "furtherSEQ r11 r2 = [SEQ r11 r2]"
|
|
|
76 |
| "turnIntoTerms (SEQ ONE r2) = turnIntoTerms r2"
|
|
|
77 |
| "turnIntoTerms (SEQ r1 r2) = concat (map (\<lambda>r11. furtherSEQ r11 r2) (turnIntoTerms r1))"
|
|
|
78 |
| "turnIntoTerms r = [r]"
|
|
|
79 |
|
|
|
80 |
fun regConcat :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp" where
|
|
|
81 |
"regConcat acc [] = acc"
|
|
|
82 |
| "regConcat ONE (r # rs1) = regConcat r rs1"
|
|
|
83 |
| "regConcat acc (r # rs1) = regConcat (SEQ acc r) rs1"
|
|
|
84 |
|
|
|
85 |
fun attachCtx :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp set" where
|
|
|
86 |
"attachCtx r ctx = set (turnIntoTerms (regConcat (erase r) ctx))"
|
|
|
87 |
|
|
|
88 |
|
|
|
89 |
|
|
|
90 |
fun rs1_subseteq_rs2 :: "rexp set \<Rightarrow> rexp set \<Rightarrow> bool" where
|
|
|
91 |
"rs1_subseteq_rs2 rs1 rs2 = (rs1 \<subseteq> rs2)"
|
|
|
92 |
|
|
|
93 |
fun notZero :: "arexp \<Rightarrow> bool" where
|
|
|
94 |
"notZero AZERO = True"
|
|
|
95 |
| "notZero _ = False"
|
|
|
96 |
|
|
|
97 |
fun prune6 :: "rexp set \<Rightarrow> arexp \<Rightarrow> rexp list \<Rightarrow> arexp" where
|
|
|
98 |
"prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else
|
|
|
99 |
(case a of (ASEQ bs r1 r2) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2
|
|
|
100 |
| AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0))) )"
|
|
|
101 |
|
|
|
102 |
|
|
|
103 |
|
|
|
104 |
fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where
|
|
|
105 |
"dB6 [] acc = []"
|
|
|
106 |
| "dB6 (a # as) acc = (if (erase a \<in> acc) then (dB6 as acc)
|
|
|
107 |
else (let pruned = prune6 acc a [] in
|
|
|
108 |
(case pruned of
|
|
|
109 |
AZERO \<Rightarrow> dB6 as acc
|
|
|
110 |
|xPrime \<Rightarrow> xPrime # (dB6 as ( (set (turnIntoTerms (erase pruned))) \<union> acc) ) ) )) "
|
|
|
111 |
|
|
|
112 |
|
|
|
113 |
fun bsimpStrong6 :: "arexp \<Rightarrow> arexp"
|
|
|
114 |
where
|
|
|
115 |
"bsimpStrong6 (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)"
|
|
|
116 |
| "bsimpStrong6 (AALTs bs1 rs) = bsimp_AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {}) "
|
|
|
117 |
| "bsimpStrong6 r = r"
|
|
|
118 |
|
|
|
119 |
|
|
|
120 |
fun
|
|
|
121 |
bdersStrong6 :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
|
|
|
122 |
where
|
|
|
123 |
"bdersStrong6 r [] = r"
|
|
|
124 |
| "bdersStrong6 r (c # s) = bdersStrong6 (bsimpStrong6 (bder c r)) s"
|
|
|
125 |
|
|
|
126 |
definition blexerStrong where
|
|
|
127 |
"blexerStrong r s \<equiv> if bnullable (bdersStrong6 (intern r) s) then
|
|
|
128 |
decode (bmkeps (bdersStrong6 (intern r) s)) r else None"
|
|
|
129 |
|
|
|
130 |
|
|
|
131 |
|
|
544
|
132 |
inductive
|
|
|
133 |
rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
|
|
|
134 |
and
|
|
|
135 |
srewrite:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto> _" [100, 100] 100)
|
|
|
136 |
where
|
|
|
137 |
bs1: "ASEQ bs AZERO r2 \<leadsto> AZERO"
|
|
|
138 |
| bs2: "ASEQ bs r1 AZERO \<leadsto> AZERO"
|
|
|
139 |
| bs3: "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r"
|
|
|
140 |
| bs4: "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"
|
|
|
141 |
| bs5: "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"
|
|
|
142 |
| bs6: "AALTs bs [] \<leadsto> AZERO"
|
|
|
143 |
| bs7: "AALTs bs [r] \<leadsto> fuse bs r"
|
|
|
144 |
| bs10: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2"
|
|
|
145 |
| ss1: "[] s\<leadsto> []"
|
|
|
146 |
| ss2: "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)"
|
|
|
147 |
| ss3: "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)"
|
|
|
148 |
| ss4: "(AZERO # rs) s\<leadsto> rs"
|
|
|
149 |
| ss5: "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)"
|
|
|
150 |
| ss6: "L (erase a2) \<subseteq> L (erase a1) \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)"
|
|
|
151 |
|
|
|
152 |
|
|
|
153 |
inductive
|
|
|
154 |
rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
|
|
|
155 |
where
|
|
|
156 |
rs1[intro, simp]:"r \<leadsto>* r"
|
|
|
157 |
| rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
|
|
|
158 |
|
|
|
159 |
inductive
|
|
|
160 |
srewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" ("_ s\<leadsto>* _" [100, 100] 100)
|
|
|
161 |
where
|
|
|
162 |
sss1[intro, simp]:"rs s\<leadsto>* rs"
|
|
|
163 |
| sss2[intro]: "\<lbrakk>rs1 s\<leadsto> rs2; rs2 s\<leadsto>* rs3\<rbrakk> \<Longrightarrow> rs1 s\<leadsto>* rs3"
|
|
|
164 |
|
|
|
165 |
|
|
|
166 |
lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
|
|
|
167 |
using rrewrites.intros(1) rrewrites.intros(2) by blast
|
|
|
168 |
|
|
|
169 |
lemma rs_in_rstar:
|
|
|
170 |
shows "r1 s\<leadsto> r2 \<Longrightarrow> r1 s\<leadsto>* r2"
|
|
|
171 |
using rrewrites.intros(1) rrewrites.intros(2) by blast
|
|
|
172 |
|
|
|
173 |
|
|
|
174 |
lemma rrewrites_trans[trans]:
|
|
|
175 |
assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3"
|
|
|
176 |
shows "r1 \<leadsto>* r3"
|
|
|
177 |
using a2 a1
|
|
|
178 |
apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct)
|
|
|
179 |
apply(auto)
|
|
|
180 |
done
|
|
|
181 |
|
|
|
182 |
lemma srewrites_trans[trans]:
|
|
|
183 |
assumes a1: "r1 s\<leadsto>* r2" and a2: "r2 s\<leadsto>* r3"
|
|
|
184 |
shows "r1 s\<leadsto>* r3"
|
|
|
185 |
using a1 a2
|
|
|
186 |
apply(induct r1 r2 arbitrary: r3 rule: srewrites.induct)
|
|
|
187 |
apply(auto)
|
|
|
188 |
done
|
|
|
189 |
|
|
|
190 |
|
|
|
191 |
|
|
|
192 |
lemma contextrewrites0:
|
|
|
193 |
"rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2"
|
|
|
194 |
apply(induct rs1 rs2 rule: srewrites.inducts)
|
|
|
195 |
apply simp
|
|
|
196 |
using bs10 r_in_rstar rrewrites_trans by blast
|
|
|
197 |
|
|
|
198 |
lemma contextrewrites1:
|
|
|
199 |
"r \<leadsto>* r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto>* AALTs bs (r' # rs)"
|
|
|
200 |
apply(induct r r' rule: rrewrites.induct)
|
|
|
201 |
apply simp
|
|
|
202 |
using bs10 ss3 by blast
|
|
|
203 |
|
|
|
204 |
lemma srewrite1:
|
|
|
205 |
shows "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto> (rs @ rs2)"
|
|
|
206 |
apply(induct rs)
|
|
|
207 |
apply(auto)
|
|
|
208 |
using ss2 by auto
|
|
|
209 |
|
|
|
210 |
lemma srewrites1:
|
|
|
211 |
shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto>* (rs @ rs2)"
|
|
|
212 |
apply(induct rs1 rs2 rule: srewrites.induct)
|
|
|
213 |
apply(auto)
|
|
|
214 |
using srewrite1 by blast
|
|
|
215 |
|
|
|
216 |
lemma srewrite2:
|
|
|
217 |
shows "r1 \<leadsto> r2 \<Longrightarrow> True"
|
|
|
218 |
and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
|
|
|
219 |
apply(induct rule: rrewrite_srewrite.inducts)
|
|
|
220 |
apply(auto)
|
|
|
221 |
apply (metis append_Cons append_Nil srewrites1)
|
|
|
222 |
apply(meson srewrites.simps ss3)
|
|
|
223 |
apply (meson srewrites.simps ss4)
|
|
|
224 |
apply (meson srewrites.simps ss5)
|
|
|
225 |
by (metis append_Cons append_Nil srewrites.simps ss6)
|
|
|
226 |
|
|
|
227 |
|
|
|
228 |
lemma srewrites3:
|
|
|
229 |
shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
|
|
|
230 |
apply(induct rs1 rs2 arbitrary: rs rule: srewrites.induct)
|
|
|
231 |
apply(auto)
|
|
|
232 |
by (meson srewrite2(2) srewrites_trans)
|
|
|
233 |
|
|
|
234 |
(*
|
|
|
235 |
lemma srewrites4:
|
|
|
236 |
assumes "rs3 s\<leadsto>* rs4" "rs1 s\<leadsto>* rs2"
|
|
|
237 |
shows "(rs1 @ rs3) s\<leadsto>* (rs2 @ rs4)"
|
|
|
238 |
using assms
|
|
|
239 |
apply(induct rs3 rs4 arbitrary: rs1 rs2 rule: srewrites.induct)
|
|
|
240 |
apply (simp add: srewrites3)
|
|
|
241 |
using srewrite1 by blast
|
|
|
242 |
*)
|
|
|
243 |
|
|
|
244 |
lemma srewrites6:
|
|
|
245 |
assumes "r1 \<leadsto>* r2"
|
|
|
246 |
shows "[r1] s\<leadsto>* [r2]"
|
|
|
247 |
using assms
|
|
|
248 |
apply(induct r1 r2 rule: rrewrites.induct)
|
|
|
249 |
apply(auto)
|
|
|
250 |
by (meson srewrites.simps srewrites_trans ss3)
|
|
|
251 |
|
|
|
252 |
lemma srewrites7:
|
|
|
253 |
assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2"
|
|
|
254 |
shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)"
|
|
|
255 |
using assms
|
|
|
256 |
by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans)
|
|
|
257 |
|
|
|
258 |
lemma ss6_stronger_aux:
|
|
|
259 |
shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctWith rs2 eq1 (set rs1))"
|
|
|
260 |
apply(induct rs2 arbitrary: rs1)
|
|
|
261 |
apply(auto)
|
|
|
262 |
prefer 2
|
|
|
263 |
apply(drule_tac x="rs1 @ [a]" in meta_spec)
|
|
|
264 |
apply(simp)
|
|
|
265 |
apply(drule_tac x="rs1" in meta_spec)
|
|
|
266 |
apply(subgoal_tac "(rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)")
|
|
|
267 |
using srewrites_trans apply blast
|
|
|
268 |
apply(subgoal_tac "\<exists>rs1a rs1b. rs1 = rs1a @ [x] @ rs1b")
|
|
|
269 |
prefer 2
|
|
|
270 |
apply (simp add: split_list)
|
|
|
271 |
apply(erule exE)+
|
|
|
272 |
apply(simp)
|
|
|
273 |
using eq1_L rs_in_rstar ss6 by force
|
|
|
274 |
|
|
|
275 |
lemma ss6_stronger:
|
|
|
276 |
shows "rs1 s\<leadsto>* distinctWith rs1 eq1 {}"
|
|
|
277 |
by (metis append_Nil list.set(1) ss6_stronger_aux)
|
|
|
278 |
|
|
|
279 |
|
|
|
280 |
lemma rewrite_preserves_fuse:
|
|
|
281 |
shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3"
|
|
|
282 |
and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3"
|
|
|
283 |
proof(induct rule: rrewrite_srewrite.inducts)
|
|
|
284 |
case (bs3 bs1 bs2 r)
|
|
|
285 |
then show ?case
|
|
|
286 |
by (metis fuse.simps(5) fuse_append rrewrite_srewrite.bs3)
|
|
|
287 |
next
|
|
|
288 |
case (bs7 bs r)
|
|
|
289 |
then show ?case
|
|
|
290 |
by (metis fuse.simps(4) fuse_append rrewrite_srewrite.bs7)
|
|
|
291 |
next
|
|
|
292 |
case (ss2 rs1 rs2 r)
|
|
|
293 |
then show ?case
|
|
|
294 |
using srewrites7 by force
|
|
|
295 |
next
|
|
|
296 |
case (ss3 r1 r2 rs)
|
|
|
297 |
then show ?case by (simp add: r_in_rstar srewrites7)
|
|
|
298 |
next
|
|
|
299 |
case (ss5 bs1 rs1 rsb)
|
|
|
300 |
then show ?case
|
|
|
301 |
apply(simp)
|
|
|
302 |
by (metis (mono_tags, lifting) comp_def fuse_append map_eq_conv rrewrite_srewrite.ss5 srewrites.simps)
|
|
|
303 |
next
|
|
|
304 |
case (ss6 a1 a2 rsa rsb rsc)
|
|
|
305 |
then show ?case
|
|
|
306 |
apply(simp only: map_append)
|
|
|
307 |
by (smt (verit, best) erase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps)
|
|
|
308 |
qed (auto intro: rrewrite_srewrite.intros)
|
|
|
309 |
|
|
|
310 |
|
|
|
311 |
lemma rewrites_fuse:
|
|
|
312 |
assumes "r1 \<leadsto>* r2"
|
|
|
313 |
shows "fuse bs r1 \<leadsto>* fuse bs r2"
|
|
|
314 |
using assms
|
|
|
315 |
apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct)
|
|
|
316 |
apply(auto intro: rewrite_preserves_fuse rrewrites_trans)
|
|
|
317 |
done
|
|
|
318 |
|
|
|
319 |
|
|
|
320 |
lemma star_seq:
|
|
|
321 |
assumes "r1 \<leadsto>* r2"
|
|
|
322 |
shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3"
|
|
|
323 |
using assms
|
|
|
324 |
apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct)
|
|
|
325 |
apply(auto intro: rrewrite_srewrite.intros)
|
|
|
326 |
done
|
|
|
327 |
|
|
|
328 |
lemma star_seq2:
|
|
|
329 |
assumes "r3 \<leadsto>* r4"
|
|
|
330 |
shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r1 r4"
|
|
|
331 |
using assms
|
|
|
332 |
apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct)
|
|
|
333 |
apply(auto intro: rrewrite_srewrite.intros)
|
|
|
334 |
done
|
|
|
335 |
|
|
|
336 |
lemma continuous_rewrite:
|
|
|
337 |
assumes "r1 \<leadsto>* AZERO"
|
|
|
338 |
shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
|
|
|
339 |
using assms bs1 star_seq by blast
|
|
|
340 |
|
|
|
341 |
(*
|
|
|
342 |
lemma continuous_rewrite2:
|
|
|
343 |
assumes "r1 \<leadsto>* AONE bs"
|
|
|
344 |
shows "ASEQ bs1 r1 r2 \<leadsto>* (fuse (bs1 @ bs) r2)"
|
|
|
345 |
using assms by (meson bs3 rrewrites.simps star_seq)
|
|
|
346 |
*)
|
|
|
347 |
|
|
|
348 |
lemma bsimp_aalts_simpcases:
|
|
|
349 |
shows "AONE bs \<leadsto>* bsimp (AONE bs)"
|
|
|
350 |
and "AZERO \<leadsto>* bsimp AZERO"
|
|
|
351 |
and "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)"
|
|
|
352 |
by (simp_all)
|
|
|
353 |
|
|
|
354 |
lemma bsimp_AALTs_rewrites:
|
|
|
355 |
shows "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
|
|
|
356 |
by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps)
|
|
|
357 |
|
|
|
358 |
lemma trivialbsimp_srewrites:
|
|
|
359 |
"\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
|
|
|
360 |
apply(induction rs)
|
|
|
361 |
apply simp
|
|
|
362 |
apply(simp)
|
|
|
363 |
using srewrites7 by auto
|
|
|
364 |
|
|
|
365 |
|
|
|
366 |
|
|
|
367 |
lemma fltsfrewrites: "rs s\<leadsto>* flts rs"
|
|
|
368 |
apply(induction rs rule: flts.induct)
|
|
|
369 |
apply(auto intro: rrewrite_srewrite.intros)
|
|
|
370 |
apply (meson srewrites.simps srewrites1 ss5)
|
|
|
371 |
using rs1 srewrites7 apply presburger
|
|
|
372 |
using srewrites7 apply force
|
|
|
373 |
apply (simp add: srewrites7)
|
|
|
374 |
by (simp add: srewrites7)
|
|
|
375 |
|
|
|
376 |
lemma bnullable0:
|
|
|
377 |
shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2"
|
|
|
378 |
and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2"
|
|
|
379 |
apply(induct rule: rrewrite_srewrite.inducts)
|
|
|
380 |
apply(auto simp add: bnullable_fuse)
|
|
|
381 |
apply (meson UnCI bnullable_fuse imageI)
|
|
548
|
382 |
using bnullable_correctness nullable_correctness by blast
|
|
|
383 |
|
|
|
384 |
|
|
544
|
385 |
|
|
|
386 |
|
|
|
387 |
lemma rewritesnullable:
|
|
|
388 |
assumes "r1 \<leadsto>* r2"
|
|
|
389 |
shows "bnullable r1 = bnullable r2"
|
|
|
390 |
using assms
|
|
|
391 |
apply(induction r1 r2 rule: rrewrites.induct)
|
|
|
392 |
apply simp
|
|
|
393 |
using bnullable0(1) by auto
|
|
|
394 |
|
|
|
395 |
lemma rewrite_bmkeps_aux:
|
|
|
396 |
shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<and> bnullable r2 \<Longrightarrow> bmkeps r1 = bmkeps r2)"
|
|
|
397 |
and "rs1 s\<leadsto> rs2 \<Longrightarrow> (bnullables rs1 \<and> bnullables rs2 \<Longrightarrow> bmkepss rs1 = bmkepss rs2)"
|
|
|
398 |
proof (induct rule: rrewrite_srewrite.inducts)
|
|
|
399 |
case (bs3 bs1 bs2 r)
|
|
|
400 |
then show ?case by (simp add: bmkeps_fuse)
|
|
|
401 |
next
|
|
|
402 |
case (bs7 bs r)
|
|
|
403 |
then show ?case by (simp add: bmkeps_fuse)
|
|
|
404 |
next
|
|
|
405 |
case (ss3 r1 r2 rs)
|
|
|
406 |
then show ?case
|
|
|
407 |
using bmkepss.simps bnullable0(1) by presburger
|
|
|
408 |
next
|
|
|
409 |
case (ss5 bs1 rs1 rsb)
|
|
|
410 |
then show ?case
|
|
|
411 |
by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse)
|
|
|
412 |
next
|
|
|
413 |
case (ss6 a1 a2 rsa rsb rsc)
|
|
|
414 |
then show ?case
|
|
|
415 |
by (smt (verit, best) Nil_is_append_conv bmkepss1 bmkepss2 bnullable_correctness in_set_conv_decomp list.distinct(1) list.set_intros(1) nullable_correctness set_ConsD subsetD)
|
|
|
416 |
qed (auto)
|
|
|
417 |
|
|
|
418 |
lemma rewrites_bmkeps:
|
|
|
419 |
assumes "r1 \<leadsto>* r2" "bnullable r1"
|
|
|
420 |
shows "bmkeps r1 = bmkeps r2"
|
|
|
421 |
using assms
|
|
|
422 |
proof(induction r1 r2 rule: rrewrites.induct)
|
|
|
423 |
case (rs1 r)
|
|
|
424 |
then show "bmkeps r = bmkeps r" by simp
|
|
|
425 |
next
|
|
|
426 |
case (rs2 r1 r2 r3)
|
|
|
427 |
then have IH: "bmkeps r1 = bmkeps r2" by simp
|
|
|
428 |
have a1: "bnullable r1" by fact
|
|
|
429 |
have a2: "r1 \<leadsto>* r2" by fact
|
|
|
430 |
have a3: "r2 \<leadsto> r3" by fact
|
|
|
431 |
have a4: "bnullable r2" using a1 a2 by (simp add: rewritesnullable)
|
|
|
432 |
then have "bmkeps r2 = bmkeps r3"
|
|
|
433 |
using a3 bnullable0(1) rewrite_bmkeps_aux(1) by blast
|
|
|
434 |
then show "bmkeps r1 = bmkeps r3" using IH by simp
|
|
|
435 |
qed
|
|
|
436 |
|
|
|
437 |
|
|
|
438 |
|
|
|
439 |
lemma to_zero_in_alt:
|
|
|
440 |
shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2"
|
|
|
441 |
by (simp add: bs1 bs10 ss3)
|
|
|
442 |
|
|
|
443 |
|
|
|
444 |
|
|
|
445 |
lemma bder_fuse_list:
|
|
|
446 |
shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1"
|
|
|
447 |
apply(induction rs1)
|
|
|
448 |
apply(simp_all add: bder_fuse)
|
|
|
449 |
done
|
|
|
450 |
|
|
|
451 |
lemma map1:
|
|
|
452 |
shows "(map f [a]) = [f a]"
|
|
|
453 |
by (simp)
|
|
|
454 |
|
|
|
455 |
lemma rewrite_preserves_bder:
|
|
|
456 |
shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)"
|
|
|
457 |
and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2"
|
|
|
458 |
proof(induction rule: rrewrite_srewrite.inducts)
|
|
|
459 |
case (bs1 bs r2)
|
|
|
460 |
then show ?case
|
|
|
461 |
by (simp add: continuous_rewrite)
|
|
|
462 |
next
|
|
|
463 |
case (bs2 bs r1)
|
|
|
464 |
then show ?case
|
|
|
465 |
apply(auto)
|
|
|
466 |
apply (meson bs6 contextrewrites0 rrewrite_srewrite.bs2 rs2 ss3 ss4 sss1 sss2)
|
|
|
467 |
by (simp add: r_in_rstar rrewrite_srewrite.bs2)
|
|
|
468 |
next
|
|
|
469 |
case (bs3 bs1 bs2 r)
|
|
|
470 |
then show ?case
|
|
|
471 |
apply(simp)
|
|
|
472 |
|
|
|
473 |
by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt)
|
|
|
474 |
next
|
|
|
475 |
case (bs4 r1 r2 bs r3)
|
|
|
476 |
have as: "r1 \<leadsto> r2" by fact
|
|
|
477 |
have IH: "bder c r1 \<leadsto>* bder c r2" by fact
|
|
|
478 |
from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r2 r3)"
|
|
|
479 |
by (metis bder.simps(5) bnullable0(1) contextrewrites1 rewrite_bmkeps_aux(1) star_seq)
|
|
|
480 |
next
|
|
|
481 |
case (bs5 r3 r4 bs r1)
|
|
|
482 |
have as: "r3 \<leadsto> r4" by fact
|
|
|
483 |
have IH: "bder c r3 \<leadsto>* bder c r4" by fact
|
|
|
484 |
from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)"
|
|
|
485 |
apply(simp)
|
|
|
486 |
apply(auto)
|
|
|
487 |
using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger
|
|
|
488 |
using star_seq2 by blast
|
|
|
489 |
next
|
|
|
490 |
case (bs6 bs)
|
|
|
491 |
then show ?case
|
|
|
492 |
using rrewrite_srewrite.bs6 by force
|
|
|
493 |
next
|
|
|
494 |
case (bs7 bs r)
|
|
|
495 |
then show ?case
|
|
|
496 |
by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7)
|
|
|
497 |
next
|
|
|
498 |
case (bs10 rs1 rs2 bs)
|
|
|
499 |
then show ?case
|
|
|
500 |
using contextrewrites0 by force
|
|
|
501 |
next
|
|
|
502 |
case ss1
|
|
|
503 |
then show ?case by simp
|
|
|
504 |
next
|
|
|
505 |
case (ss2 rs1 rs2 r)
|
|
|
506 |
then show ?case
|
|
|
507 |
by (simp add: srewrites7)
|
|
|
508 |
next
|
|
|
509 |
case (ss3 r1 r2 rs)
|
|
|
510 |
then show ?case
|
|
|
511 |
by (simp add: srewrites7)
|
|
|
512 |
next
|
|
|
513 |
case (ss4 rs)
|
|
|
514 |
then show ?case
|
|
|
515 |
using rrewrite_srewrite.ss4 by fastforce
|
|
|
516 |
next
|
|
|
517 |
case (ss5 bs1 rs1 rsb)
|
|
|
518 |
then show ?case
|
|
|
519 |
apply(simp)
|
|
|
520 |
using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast
|
|
|
521 |
next
|
|
|
522 |
case (ss6 a1 a2 bs rsa rsb)
|
|
|
523 |
then show ?case
|
|
|
524 |
apply(simp only: map_append map1)
|
|
|
525 |
apply(rule srewrites_trans)
|
|
|
526 |
apply(rule rs_in_rstar)
|
|
|
527 |
apply(rule_tac rrewrite_srewrite.ss6)
|
|
|
528 |
using Der_def der_correctness apply auto[1]
|
|
|
529 |
by blast
|
|
|
530 |
qed
|
|
|
531 |
|
|
|
532 |
lemma rewrites_preserves_bder:
|
|
|
533 |
assumes "r1 \<leadsto>* r2"
|
|
|
534 |
shows "bder c r1 \<leadsto>* bder c r2"
|
|
|
535 |
using assms
|
|
|
536 |
apply(induction r1 r2 rule: rrewrites.induct)
|
|
|
537 |
apply(simp_all add: rewrite_preserves_bder rrewrites_trans)
|
|
548
|
538 |
done
|
|
544
|
539 |
|
|
|
540 |
|
|
|
541 |
|
|
548
|
542 |
lemma bders_simp_appendStrong :
|
|
|
543 |
shows "bdersStrong6 r (s1 @ s2) = bdersStrong6 (bdersStrong6 r s1) s2"
|
|
|
544 |
apply(induct s1 arbitrary: s2 rule: rev_induct)
|
|
|
545 |
apply simp
|
|
|
546 |
apply auto
|
|
|
547 |
done
|
|
|
548 |
|
|
|
549 |
|
|
546
|
550 |
|
|
|
551 |
|
|
547
|
552 |
lemma rewrites_to_bsimpStrong:
|
|
|
553 |
shows "r \<leadsto>* bsimpStrong6 r"
|
|
|
554 |
proof (induction r rule: bsimpStrong6.induct)
|
|
|
555 |
case (1 bs1 r1 r2)
|
|
|
556 |
have IH1: "r1 \<leadsto>* bsimpStrong6 r1" by fact
|
|
|
557 |
have IH2: "r2 \<leadsto>* bsimpStrong6 r2" by fact
|
|
|
558 |
{ assume as: "bsimpStrong6 r1 = AZERO \<or> bsimpStrong6 r2 = AZERO"
|
|
|
559 |
with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto
|
|
|
560 |
then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
|
|
|
561 |
by (metis bs2 continuous_rewrite rrewrites.simps star_seq2)
|
|
|
562 |
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" using as by auto
|
|
|
563 |
}
|
|
|
564 |
moreover
|
|
|
565 |
{ assume "\<exists>bs. bsimpStrong6 r1 = AONE bs"
|
|
|
566 |
then obtain bs where as: "bsimpStrong6 r1 = AONE bs" by blast
|
|
|
567 |
with IH1 have "r1 \<leadsto>* AONE bs" by simp
|
|
|
568 |
then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast
|
|
|
569 |
with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimpStrong6 r2)"
|
|
|
570 |
using rewrites_fuse by (meson rrewrites_trans)
|
|
|
571 |
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 (AONE bs) r2)" by simp
|
|
|
572 |
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by (simp add: as)
|
|
|
573 |
}
|
|
|
574 |
moreover
|
|
|
575 |
{ assume as1: "bsimpStrong6 r1 \<noteq> AZERO" "bsimpStrong6 r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimpStrong6 r1 = AONE bs)"
|
|
|
576 |
then have "bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2) = ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)"
|
|
|
577 |
by (simp add: bsimp_ASEQ1)
|
|
|
578 |
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" using as1 as2 IH1 IH2
|
|
|
579 |
by (metis rrewrites_trans star_seq star_seq2)
|
|
|
580 |
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by simp
|
|
|
581 |
}
|
|
|
582 |
ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" sorry
|
|
|
583 |
next
|
|
|
584 |
case (2 bs1 rs)
|
|
|
585 |
have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimpStrong6 x" by fact
|
|
|
586 |
then have "rs s\<leadsto>* (map bsimpStrong6 rs)" by (simp add: trivialbsimp_srewrites)
|
|
|
587 |
also have "... s\<leadsto>* flts (map bsimpStrong6 rs)" by (simp add: fltsfrewrites)
|
|
|
588 |
also have "... s\<leadsto>* distinctWith (flts (map bsimpStrong6 rs)) eq1 {}" by (simp add: ss6_stronger)
|
|
|
589 |
finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})"
|
|
|
590 |
using contextrewrites0 by auto
|
|
|
591 |
also have "... \<leadsto>* bsimp_AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})"
|
|
|
592 |
by (simp add: bsimp_AALTs_rewrites)
|
|
|
593 |
finally show "AALTs bs1 rs \<leadsto>* bsimpStrong6 (AALTs bs1 rs)" sorry
|
|
|
594 |
qed (simp_all)
|
|
|
595 |
|
|
548
|
596 |
|
|
547
|
597 |
|
|
546
|
598 |
|
|
545
|
599 |
lemma centralStrong:
|
|
546
|
600 |
shows "bders r s \<leadsto>* bdersStrong6 r s"
|
|
545
|
601 |
proof(induct s arbitrary: r rule: rev_induct)
|
|
|
602 |
case Nil
|
|
546
|
603 |
then show "bders r [] \<leadsto>* bdersStrong6 r []" by simp
|
|
545
|
604 |
next
|
|
|
605 |
case (snoc x xs)
|
|
546
|
606 |
have IH: "\<And>r. bders r xs \<leadsto>* bdersStrong6 r xs" by fact
|
|
|
607 |
have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append)
|
|
|
608 |
also have "... \<leadsto>* bders (bdersStrong6 r xs) [x]" using IH
|
|
545
|
609 |
by (simp add: rewrites_preserves_bder)
|
|
546
|
610 |
also have "... \<leadsto>* bdersStrong6 (bdersStrong6 r xs) [x]" using IH
|
|
547
|
611 |
by (simp add: rewrites_to_bsimpStrong)
|
|
|
612 |
finally show "bders r (xs @ [x]) \<leadsto>* bdersStrong6 r (xs @ [x])"
|
|
|
613 |
by (simp add: bders_simp_appendStrong)
|
|
545
|
614 |
qed
|
|
|
615 |
|
|
|
616 |
lemma mainStrong:
|
|
|
617 |
assumes "bnullable (bders r s)"
|
|
546
|
618 |
shows "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)"
|
|
545
|
619 |
proof -
|
|
548
|
620 |
have "bders r s \<leadsto>* bdersStrong6 r s"
|
|
|
621 |
using centralStrong by force
|
|
545
|
622 |
then
|
|
546
|
623 |
show "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)"
|
|
548
|
624 |
using assms rewrites_bmkeps by blast
|
|
545
|
625 |
qed
|
|
|
626 |
|
|
|
627 |
|
|
|
628 |
|
|
|
629 |
|
|
|
630 |
theorem blexerStrong_correct :
|
|
548
|
631 |
shows "blexerStrong r s = blexer r s"
|
|
|
632 |
unfolding blexerStrong_def blexer_def
|
|
|
633 |
by (metis centralStrong mainStrong rewritesnullable)
|
|
545
|
634 |
|
|
544
|
635 |
|
|
|
636 |
|
|
|
637 |
end
|