|
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 |
|
|
564
|
80 |
abbreviation "tint \<equiv> turnIntoTerms"
|
|
|
81 |
|
|
|
82 |
fun seqFold :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp" where
|
|
|
83 |
"seqFold acc [] = acc"
|
|
|
84 |
| "seqFold ONE (r # rs1) = seqFold r rs1"
|
|
|
85 |
| "seqFold acc (r # rs1) = seqFold (SEQ acc r) rs1"
|
|
|
86 |
|
|
550
|
87 |
|
|
|
88 |
fun attachCtx :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp set" where
|
|
564
|
89 |
"attachCtx r ctx = set (turnIntoTerms (seqFold (erase r) ctx))"
|
|
550
|
90 |
|
|
|
91 |
|
|
|
92 |
fun rs1_subseteq_rs2 :: "rexp set \<Rightarrow> rexp set \<Rightarrow> bool" where
|
|
|
93 |
"rs1_subseteq_rs2 rs1 rs2 = (rs1 \<subseteq> rs2)"
|
|
|
94 |
|
|
564
|
95 |
|
|
550
|
96 |
fun notZero :: "arexp \<Rightarrow> bool" where
|
|
|
97 |
"notZero AZERO = True"
|
|
|
98 |
| "notZero _ = False"
|
|
|
99 |
|
|
564
|
100 |
|
|
558
|
101 |
fun tset :: "arexp list \<Rightarrow> rexp set" where
|
|
|
102 |
"tset rs = set (concat (map turnIntoTerms (map erase rs)))"
|
|
|
103 |
|
|
|
104 |
|
|
550
|
105 |
fun prune6 :: "rexp set \<Rightarrow> arexp \<Rightarrow> rexp list \<Rightarrow> arexp" where
|
|
|
106 |
"prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else
|
|
|
107 |
(case a of (ASEQ bs r1 r2) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2
|
|
564
|
108 |
| AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0))
|
|
|
109 |
| r \<Rightarrow> r
|
|
|
110 |
)
|
|
|
111 |
)
|
|
|
112 |
"
|
|
550
|
113 |
|
|
558
|
114 |
abbreviation
|
|
564
|
115 |
"p6 acc r \<equiv> prune6 (tset acc) r Nil"
|
|
550
|
116 |
|
|
|
117 |
|
|
|
118 |
fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where
|
|
|
119 |
"dB6 [] acc = []"
|
|
|
120 |
| "dB6 (a # as) acc = (if (erase a \<in> acc) then (dB6 as acc)
|
|
|
121 |
else (let pruned = prune6 acc a [] in
|
|
|
122 |
(case pruned of
|
|
|
123 |
AZERO \<Rightarrow> dB6 as acc
|
|
|
124 |
|xPrime \<Rightarrow> xPrime # (dB6 as ( (set (turnIntoTerms (erase pruned))) \<union> acc) ) ) )) "
|
|
|
125 |
|
|
|
126 |
|
|
|
127 |
fun bsimpStrong6 :: "arexp \<Rightarrow> arexp"
|
|
|
128 |
where
|
|
|
129 |
"bsimpStrong6 (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)"
|
|
|
130 |
| "bsimpStrong6 (AALTs bs1 rs) = bsimp_AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {}) "
|
|
|
131 |
| "bsimpStrong6 r = r"
|
|
|
132 |
|
|
|
133 |
|
|
|
134 |
fun
|
|
|
135 |
bdersStrong6 :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
|
|
|
136 |
where
|
|
|
137 |
"bdersStrong6 r [] = r"
|
|
|
138 |
| "bdersStrong6 r (c # s) = bdersStrong6 (bsimpStrong6 (bder c r)) s"
|
|
|
139 |
|
|
|
140 |
definition blexerStrong where
|
|
|
141 |
"blexerStrong r s \<equiv> if bnullable (bdersStrong6 (intern r) s) then
|
|
|
142 |
decode (bmkeps (bdersStrong6 (intern r) s)) r else None"
|
|
|
143 |
|
|
|
144 |
|
|
|
145 |
|
|
544
|
146 |
inductive
|
|
|
147 |
rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
|
|
|
148 |
and
|
|
|
149 |
srewrite:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto> _" [100, 100] 100)
|
|
|
150 |
where
|
|
|
151 |
bs1: "ASEQ bs AZERO r2 \<leadsto> AZERO"
|
|
|
152 |
| bs2: "ASEQ bs r1 AZERO \<leadsto> AZERO"
|
|
|
153 |
| bs3: "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r"
|
|
|
154 |
| bs4: "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"
|
|
|
155 |
| bs5: "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"
|
|
|
156 |
| bs6: "AALTs bs [] \<leadsto> AZERO"
|
|
|
157 |
| bs7: "AALTs bs [r] \<leadsto> fuse bs r"
|
|
|
158 |
| bs10: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2"
|
|
|
159 |
| ss1: "[] s\<leadsto> []"
|
|
|
160 |
| ss2: "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)"
|
|
|
161 |
| ss3: "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)"
|
|
|
162 |
| ss4: "(AZERO # rs) s\<leadsto> rs"
|
|
|
163 |
| ss5: "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)"
|
|
|
164 |
| ss6: "L (erase a2) \<subseteq> L (erase a1) \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)"
|
|
564
|
165 |
| ss7: " (as @ [a] @ as1) s\<leadsto> (as @ [p6 as a] @ as1)"
|
|
544
|
166 |
|
|
564
|
167 |
thm tset.simps
|
|
544
|
168 |
|
|
|
169 |
inductive
|
|
|
170 |
rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
|
|
|
171 |
where
|
|
|
172 |
rs1[intro, simp]:"r \<leadsto>* r"
|
|
|
173 |
| rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
|
|
|
174 |
|
|
|
175 |
inductive
|
|
|
176 |
srewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" ("_ s\<leadsto>* _" [100, 100] 100)
|
|
|
177 |
where
|
|
|
178 |
sss1[intro, simp]:"rs s\<leadsto>* rs"
|
|
|
179 |
| sss2[intro]: "\<lbrakk>rs1 s\<leadsto> rs2; rs2 s\<leadsto>* rs3\<rbrakk> \<Longrightarrow> rs1 s\<leadsto>* rs3"
|
|
|
180 |
|
|
|
181 |
|
|
|
182 |
lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
|
|
|
183 |
using rrewrites.intros(1) rrewrites.intros(2) by blast
|
|
|
184 |
|
|
|
185 |
lemma rs_in_rstar:
|
|
|
186 |
shows "r1 s\<leadsto> r2 \<Longrightarrow> r1 s\<leadsto>* r2"
|
|
|
187 |
using rrewrites.intros(1) rrewrites.intros(2) by blast
|
|
|
188 |
|
|
|
189 |
|
|
|
190 |
lemma rrewrites_trans[trans]:
|
|
|
191 |
assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3"
|
|
|
192 |
shows "r1 \<leadsto>* r3"
|
|
|
193 |
using a2 a1
|
|
|
194 |
apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct)
|
|
|
195 |
apply(auto)
|
|
|
196 |
done
|
|
|
197 |
|
|
|
198 |
lemma srewrites_trans[trans]:
|
|
|
199 |
assumes a1: "r1 s\<leadsto>* r2" and a2: "r2 s\<leadsto>* r3"
|
|
|
200 |
shows "r1 s\<leadsto>* r3"
|
|
|
201 |
using a1 a2
|
|
|
202 |
apply(induct r1 r2 arbitrary: r3 rule: srewrites.induct)
|
|
|
203 |
apply(auto)
|
|
|
204 |
done
|
|
|
205 |
|
|
|
206 |
lemma contextrewrites0:
|
|
|
207 |
"rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2"
|
|
|
208 |
apply(induct rs1 rs2 rule: srewrites.inducts)
|
|
|
209 |
apply simp
|
|
|
210 |
using bs10 r_in_rstar rrewrites_trans by blast
|
|
|
211 |
|
|
|
212 |
lemma contextrewrites1:
|
|
|
213 |
"r \<leadsto>* r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto>* AALTs bs (r' # rs)"
|
|
|
214 |
apply(induct r r' rule: rrewrites.induct)
|
|
|
215 |
apply simp
|
|
|
216 |
using bs10 ss3 by blast
|
|
|
217 |
|
|
|
218 |
lemma srewrite1:
|
|
|
219 |
shows "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto> (rs @ rs2)"
|
|
|
220 |
apply(induct rs)
|
|
|
221 |
apply(auto)
|
|
|
222 |
using ss2 by auto
|
|
|
223 |
|
|
|
224 |
lemma srewrites1:
|
|
|
225 |
shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto>* (rs @ rs2)"
|
|
|
226 |
apply(induct rs1 rs2 rule: srewrites.induct)
|
|
|
227 |
apply(auto)
|
|
|
228 |
using srewrite1 by blast
|
|
|
229 |
|
|
551
|
230 |
lemma srewrites_prepend:
|
|
|
231 |
shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (r # rs1) s\<leadsto>* (r # rs2)"
|
|
|
232 |
by (metis append_Cons append_Nil srewrites1)
|
|
|
233 |
|
|
544
|
234 |
lemma srewrite2:
|
|
|
235 |
shows "r1 \<leadsto> r2 \<Longrightarrow> True"
|
|
|
236 |
and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
|
|
551
|
237 |
apply(induct arbitrary: rs rule: rrewrite_srewrite.inducts)
|
|
|
238 |
apply simp+
|
|
|
239 |
using srewrites_prepend apply force
|
|
|
240 |
apply (simp add: rs_in_rstar ss3)
|
|
|
241 |
using ss4 apply force
|
|
|
242 |
using rs_in_rstar ss5 apply auto[1]
|
|
|
243 |
using rs_in_rstar ss6 apply auto[1]
|
|
|
244 |
using rs_in_rstar ss7 by force
|
|
|
245 |
|
|
|
246 |
|
|
|
247 |
|
|
544
|
248 |
|
|
|
249 |
lemma srewrites3:
|
|
|
250 |
shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
|
|
|
251 |
apply(induct rs1 rs2 arbitrary: rs rule: srewrites.induct)
|
|
|
252 |
apply(auto)
|
|
|
253 |
by (meson srewrite2(2) srewrites_trans)
|
|
|
254 |
|
|
|
255 |
|
|
|
256 |
lemma srewrites6:
|
|
|
257 |
assumes "r1 \<leadsto>* r2"
|
|
|
258 |
shows "[r1] s\<leadsto>* [r2]"
|
|
|
259 |
using assms
|
|
|
260 |
apply(induct r1 r2 rule: rrewrites.induct)
|
|
|
261 |
apply(auto)
|
|
|
262 |
by (meson srewrites.simps srewrites_trans ss3)
|
|
|
263 |
|
|
|
264 |
lemma srewrites7:
|
|
|
265 |
assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2"
|
|
|
266 |
shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)"
|
|
|
267 |
using assms
|
|
|
268 |
by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans)
|
|
|
269 |
|
|
552
|
270 |
(*harmless sorry*)
|
|
|
271 |
lemma existing_preimage :
|
|
|
272 |
shows "f a \<in> f ` set rs1 \<Longrightarrow> \<exists>rs1a rs1b x. rs1 = rs1a @ [x] @ rs1b \<and> f x = f a "
|
|
|
273 |
apply(induct rs1)
|
|
|
274 |
apply simp
|
|
|
275 |
apply(case_tac "f a = f aa")
|
|
|
276 |
|
|
|
277 |
sorry
|
|
|
278 |
|
|
|
279 |
|
|
|
280 |
lemma deletes_dB:
|
|
|
281 |
shows " \<lbrakk>erase a \<in> erase ` set rs1\<rbrakk> \<Longrightarrow> (rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)"
|
|
|
282 |
apply(subgoal_tac "\<exists>rs1a rs1b x. rs1 = rs1a @ [x] @ rs1b \<and> erase x = erase a")
|
|
|
283 |
prefer 2
|
|
553
|
284 |
apply (meson existing_preimage)
|
|
|
285 |
apply(erule exE)+
|
|
|
286 |
apply simp
|
|
|
287 |
apply(subgoal_tac "(rs1a @ [x] @ rs1b @ [a] @ rs2) s\<leadsto> (rs1a @ [x] @ rs1b @ rs2)")
|
|
|
288 |
apply (simp add: rs_in_rstar)
|
|
|
289 |
apply(subgoal_tac "L (erase a) \<subseteq> L (erase x)")
|
|
|
290 |
using ss6 apply presburger
|
|
|
291 |
by simp
|
|
552
|
292 |
|
|
558
|
293 |
|
|
|
294 |
|
|
553
|
295 |
lemma ss6_realistic:
|
|
558
|
296 |
shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (tset rs1))"
|
|
557
|
297 |
apply(induct rs2 arbitrary: rs1)
|
|
|
298 |
apply simp
|
|
558
|
299 |
apply(rename_tac cc' cc)
|
|
|
300 |
apply(subgoal_tac "(cc @ a # cc') s\<leadsto>* (cc @ a # dB6 cc' (tset (cc @ [a])))")
|
|
|
301 |
prefer 2
|
|
|
302 |
apply (metis append.assoc append.left_neutral append_Cons)
|
|
564
|
303 |
apply(subgoal_tac "(cc @ a # dB6 cc' (tset (cc @ [a]))) s\<leadsto>* (cc @ (p6 cc a) # dB6 cc' (tset (cc @ [a])))")
|
|
552
|
304 |
sorry
|
|
|
305 |
|
|
564
|
306 |
(*
|
|
544
|
307 |
lemma ss6_stronger_aux:
|
|
551
|
308 |
shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))"
|
|
544
|
309 |
apply(induct rs2 arbitrary: rs1)
|
|
552
|
310 |
apply simp
|
|
|
311 |
apply(case_tac "erase a \<in> erase ` set rs1")
|
|
|
312 |
apply(simp)
|
|
|
313 |
apply(drule_tac x = "rs1" in meta_spec)
|
|
|
314 |
apply(subgoal_tac "(rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)")
|
|
|
315 |
using srewrites_trans apply blast
|
|
|
316 |
using deletes_dB apply presburger
|
|
553
|
317 |
apply(case_tac "set (turnIntoTerms (erase a)) \<subseteq> erase ` set rs1")
|
|
|
318 |
|
|
|
319 |
apply simp
|
|
552
|
320 |
|
|
544
|
321 |
apply(auto)
|
|
|
322 |
prefer 2
|
|
|
323 |
apply(drule_tac x="rs1 @ [a]" in meta_spec)
|
|
|
324 |
apply(simp)
|
|
551
|
325 |
sorry
|
|
564
|
326 |
*)
|
|
551
|
327 |
|
|
544
|
328 |
|
|
|
329 |
lemma ss6_stronger:
|
|
551
|
330 |
shows "rs1 s\<leadsto>* dB6 rs1 {}"
|
|
564
|
331 |
using ss6
|
|
|
332 |
by (metis append_Nil concat.simps(1) list.set(1) list.simps(8) ss6_realistic tset.simps)
|
|
|
333 |
|
|
|
334 |
|
|
|
335 |
lemma tint_fuse:
|
|
|
336 |
shows "tint (erase a) = tint (erase (fuse bs a))"
|
|
|
337 |
by (simp add: erase_fuse)
|
|
|
338 |
|
|
|
339 |
lemma tint_fuse2:
|
|
|
340 |
shows " set (tint (erase a)) =
|
|
|
341 |
set (tint (erase (fuse bs a)))"
|
|
|
342 |
using tint_fuse by auto
|
|
|
343 |
|
|
|
344 |
lemma fused_bits_at_head:
|
|
|
345 |
shows "fuse bs a = ASEQ bs1 a1 a2 \<Longrightarrow> \<exists>bs2. bs1 = bs @ bs2"
|
|
|
346 |
|
|
|
347 |
(* by (smt (verit) arexp.distinct(13) arexp.distinct(19) arexp.distinct(25) arexp.distinct(27) arexp.distinct(5) arexp.inject(3) fuse.elims)
|
|
|
348 |
harmless sorry
|
|
|
349 |
*)
|
|
|
350 |
|
|
551
|
351 |
sorry
|
|
544
|
352 |
|
|
564
|
353 |
thm seqFold.simps
|
|
|
354 |
|
|
|
355 |
lemma seqFold_concats:
|
|
|
356 |
shows "r \<noteq> ONE \<Longrightarrow> seqFold r [r1] = SEQ r r1"
|
|
|
357 |
apply(case_tac r)
|
|
|
358 |
apply simp+
|
|
|
359 |
done
|
|
|
360 |
|
|
|
361 |
|
|
|
362 |
lemma "set (tint (seqFold (erase x42) [erase x43])) =
|
|
|
363 |
set (tint (SEQ (erase x42) (erase x43)))"
|
|
|
364 |
apply(case_tac "erase x42 = ONE")
|
|
|
365 |
apply simp
|
|
|
366 |
apply simp
|
|
|
367 |
|
|
|
368 |
lemma prune6_preserves_fuse:
|
|
|
369 |
shows "fuse bs (p6 as a) = p6 as (fuse bs a)"
|
|
|
370 |
using tint_fuse2
|
|
|
371 |
apply simp
|
|
|
372 |
apply(case_tac a)
|
|
|
373 |
apply simp
|
|
|
374 |
apply simp
|
|
|
375 |
apply simp
|
|
|
376 |
|
|
|
377 |
using fused_bits_at_head
|
|
|
378 |
|
|
|
379 |
apply simp
|
|
|
380 |
apply(case_tac "erase x42 = ONE")
|
|
|
381 |
apply simp
|
|
|
382 |
|
|
|
383 |
sorry
|
|
|
384 |
|
|
|
385 |
corollary prune6_preserves_fuse_srewrite:
|
|
|
386 |
shows "(as @ map (fuse bs) [a] @ as2) s\<leadsto>* (as @ map (fuse bs) [p6 as a] @ as2)"
|
|
|
387 |
apply(subgoal_tac "map (fuse bs) [a] = [fuse bs a]")
|
|
|
388 |
apply(subgoal_tac "(as @ [fuse bs a] @ as2) s\<leadsto>* (as @ [ (p6 as (fuse bs a))] @ as2)")
|
|
|
389 |
using prune6_preserves_fuse apply auto[1]
|
|
|
390 |
using rs_in_rstar ss7 apply presburger
|
|
|
391 |
by simp
|
|
|
392 |
|
|
|
393 |
lemma prune6_invariant_fuse:
|
|
|
394 |
shows "p6 as a = p6 (map (fuse bs) as) a"
|
|
|
395 |
apply simp
|
|
|
396 |
using erase_fuse by presburger
|
|
|
397 |
|
|
|
398 |
|
|
|
399 |
lemma p6pfs_cor:
|
|
|
400 |
shows "(map (fuse bs) as @ map (fuse bs) [a] @ map (fuse bs) as1) s\<leadsto>* (map (fuse bs) as @ map (fuse bs) [p6 as a] @ map (fuse bs) as1)"
|
|
|
401 |
by (metis prune6_invariant_fuse prune6_preserves_fuse_srewrite)
|
|
544
|
402 |
|
|
|
403 |
lemma rewrite_preserves_fuse:
|
|
|
404 |
shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3"
|
|
|
405 |
and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3"
|
|
|
406 |
proof(induct rule: rrewrite_srewrite.inducts)
|
|
|
407 |
case (bs3 bs1 bs2 r)
|
|
|
408 |
then show ?case
|
|
|
409 |
by (metis fuse.simps(5) fuse_append rrewrite_srewrite.bs3)
|
|
|
410 |
next
|
|
|
411 |
case (bs7 bs r)
|
|
|
412 |
then show ?case
|
|
|
413 |
by (metis fuse.simps(4) fuse_append rrewrite_srewrite.bs7)
|
|
|
414 |
next
|
|
|
415 |
case (ss2 rs1 rs2 r)
|
|
|
416 |
then show ?case
|
|
|
417 |
using srewrites7 by force
|
|
|
418 |
next
|
|
|
419 |
case (ss3 r1 r2 rs)
|
|
|
420 |
then show ?case by (simp add: r_in_rstar srewrites7)
|
|
|
421 |
next
|
|
|
422 |
case (ss5 bs1 rs1 rsb)
|
|
|
423 |
then show ?case
|
|
|
424 |
apply(simp)
|
|
|
425 |
by (metis (mono_tags, lifting) comp_def fuse_append map_eq_conv rrewrite_srewrite.ss5 srewrites.simps)
|
|
|
426 |
next
|
|
|
427 |
case (ss6 a1 a2 rsa rsb rsc)
|
|
|
428 |
then show ?case
|
|
|
429 |
apply(simp only: map_append)
|
|
|
430 |
by (smt (verit, best) erase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps)
|
|
564
|
431 |
next
|
|
|
432 |
case (ss7 as a as1)
|
|
|
433 |
then show ?case
|
|
|
434 |
apply(simp only: map_append)
|
|
|
435 |
using p6pfs_cor by presburger
|
|
544
|
436 |
qed (auto intro: rrewrite_srewrite.intros)
|
|
564
|
437 |
|
|
544
|
438 |
|
|
|
439 |
|
|
|
440 |
lemma rewrites_fuse:
|
|
|
441 |
assumes "r1 \<leadsto>* r2"
|
|
|
442 |
shows "fuse bs r1 \<leadsto>* fuse bs r2"
|
|
|
443 |
using assms
|
|
|
444 |
apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct)
|
|
|
445 |
apply(auto intro: rewrite_preserves_fuse rrewrites_trans)
|
|
|
446 |
done
|
|
|
447 |
|
|
|
448 |
|
|
|
449 |
lemma star_seq:
|
|
|
450 |
assumes "r1 \<leadsto>* r2"
|
|
|
451 |
shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3"
|
|
|
452 |
using assms
|
|
|
453 |
apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct)
|
|
|
454 |
apply(auto intro: rrewrite_srewrite.intros)
|
|
|
455 |
done
|
|
|
456 |
|
|
|
457 |
lemma star_seq2:
|
|
|
458 |
assumes "r3 \<leadsto>* r4"
|
|
|
459 |
shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r1 r4"
|
|
|
460 |
using assms
|
|
|
461 |
apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct)
|
|
|
462 |
apply(auto intro: rrewrite_srewrite.intros)
|
|
|
463 |
done
|
|
|
464 |
|
|
|
465 |
lemma continuous_rewrite:
|
|
|
466 |
assumes "r1 \<leadsto>* AZERO"
|
|
|
467 |
shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
|
|
|
468 |
using assms bs1 star_seq by blast
|
|
|
469 |
|
|
551
|
470 |
|
|
544
|
471 |
|
|
|
472 |
lemma bsimp_aalts_simpcases:
|
|
551
|
473 |
shows "AONE bs \<leadsto>* bsimpStrong6 (AONE bs)"
|
|
|
474 |
and "AZERO \<leadsto>* bsimpStrong6 AZERO"
|
|
|
475 |
and "ACHAR bs c \<leadsto>* bsimpStrong6 (ACHAR bs c)"
|
|
544
|
476 |
by (simp_all)
|
|
|
477 |
|
|
|
478 |
lemma bsimp_AALTs_rewrites:
|
|
|
479 |
shows "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
|
|
|
480 |
by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps)
|
|
|
481 |
|
|
|
482 |
lemma trivialbsimp_srewrites:
|
|
|
483 |
"\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
|
|
|
484 |
apply(induction rs)
|
|
|
485 |
apply simp
|
|
|
486 |
apply(simp)
|
|
|
487 |
using srewrites7 by auto
|
|
|
488 |
|
|
|
489 |
|
|
|
490 |
|
|
|
491 |
lemma fltsfrewrites: "rs s\<leadsto>* flts rs"
|
|
|
492 |
apply(induction rs rule: flts.induct)
|
|
|
493 |
apply(auto intro: rrewrite_srewrite.intros)
|
|
|
494 |
apply (meson srewrites.simps srewrites1 ss5)
|
|
|
495 |
using rs1 srewrites7 apply presburger
|
|
|
496 |
using srewrites7 apply force
|
|
|
497 |
apply (simp add: srewrites7)
|
|
|
498 |
by (simp add: srewrites7)
|
|
|
499 |
|
|
|
500 |
lemma bnullable0:
|
|
|
501 |
shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2"
|
|
|
502 |
and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2"
|
|
564
|
503 |
apply(induct rule: rrewrite_srewrite.inducts)
|
|
|
504 |
apply simp
|
|
|
505 |
apply simp
|
|
|
506 |
apply (simp add: bnullable_fuse)
|
|
|
507 |
using bnullable.simps(5) apply presburger
|
|
|
508 |
apply simp
|
|
|
509 |
apply simp
|
|
|
510 |
sorry
|
|
548
|
511 |
|
|
544
|
512 |
|
|
|
513 |
|
|
|
514 |
lemma rewritesnullable:
|
|
|
515 |
assumes "r1 \<leadsto>* r2"
|
|
|
516 |
shows "bnullable r1 = bnullable r2"
|
|
|
517 |
using assms
|
|
|
518 |
apply(induction r1 r2 rule: rrewrites.induct)
|
|
|
519 |
apply simp
|
|
564
|
520 |
using bnullable0(1) by presburger
|
|
544
|
521 |
|
|
|
522 |
lemma rewrite_bmkeps_aux:
|
|
|
523 |
shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<and> bnullable r2 \<Longrightarrow> bmkeps r1 = bmkeps r2)"
|
|
|
524 |
and "rs1 s\<leadsto> rs2 \<Longrightarrow> (bnullables rs1 \<and> bnullables rs2 \<Longrightarrow> bmkepss rs1 = bmkepss rs2)"
|
|
|
525 |
proof (induct rule: rrewrite_srewrite.inducts)
|
|
|
526 |
case (bs3 bs1 bs2 r)
|
|
|
527 |
then show ?case by (simp add: bmkeps_fuse)
|
|
|
528 |
next
|
|
|
529 |
case (bs7 bs r)
|
|
|
530 |
then show ?case by (simp add: bmkeps_fuse)
|
|
|
531 |
next
|
|
|
532 |
case (ss3 r1 r2 rs)
|
|
|
533 |
then show ?case
|
|
|
534 |
using bmkepss.simps bnullable0(1) by presburger
|
|
|
535 |
next
|
|
|
536 |
case (ss5 bs1 rs1 rsb)
|
|
|
537 |
then show ?case
|
|
|
538 |
by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse)
|
|
|
539 |
next
|
|
|
540 |
case (ss6 a1 a2 rsa rsb rsc)
|
|
|
541 |
then show ?case
|
|
|
542 |
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)
|
|
|
543 |
qed (auto)
|
|
|
544 |
|
|
|
545 |
lemma rewrites_bmkeps:
|
|
|
546 |
assumes "r1 \<leadsto>* r2" "bnullable r1"
|
|
|
547 |
shows "bmkeps r1 = bmkeps r2"
|
|
|
548 |
using assms
|
|
|
549 |
proof(induction r1 r2 rule: rrewrites.induct)
|
|
|
550 |
case (rs1 r)
|
|
|
551 |
then show "bmkeps r = bmkeps r" by simp
|
|
|
552 |
next
|
|
|
553 |
case (rs2 r1 r2 r3)
|
|
|
554 |
then have IH: "bmkeps r1 = bmkeps r2" by simp
|
|
|
555 |
have a1: "bnullable r1" by fact
|
|
|
556 |
have a2: "r1 \<leadsto>* r2" by fact
|
|
|
557 |
have a3: "r2 \<leadsto> r3" by fact
|
|
|
558 |
have a4: "bnullable r2" using a1 a2 by (simp add: rewritesnullable)
|
|
|
559 |
then have "bmkeps r2 = bmkeps r3"
|
|
|
560 |
using a3 bnullable0(1) rewrite_bmkeps_aux(1) by blast
|
|
|
561 |
then show "bmkeps r1 = bmkeps r3" using IH by simp
|
|
|
562 |
qed
|
|
|
563 |
|
|
|
564 |
|
|
|
565 |
|
|
|
566 |
lemma to_zero_in_alt:
|
|
|
567 |
shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2"
|
|
|
568 |
by (simp add: bs1 bs10 ss3)
|
|
|
569 |
|
|
|
570 |
|
|
|
571 |
|
|
|
572 |
lemma bder_fuse_list:
|
|
|
573 |
shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1"
|
|
|
574 |
apply(induction rs1)
|
|
|
575 |
apply(simp_all add: bder_fuse)
|
|
|
576 |
done
|
|
|
577 |
|
|
|
578 |
lemma map1:
|
|
|
579 |
shows "(map f [a]) = [f a]"
|
|
|
580 |
by (simp)
|
|
|
581 |
|
|
|
582 |
lemma rewrite_preserves_bder:
|
|
|
583 |
shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)"
|
|
|
584 |
and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2"
|
|
|
585 |
proof(induction rule: rrewrite_srewrite.inducts)
|
|
|
586 |
case (bs1 bs r2)
|
|
|
587 |
then show ?case
|
|
|
588 |
by (simp add: continuous_rewrite)
|
|
|
589 |
next
|
|
|
590 |
case (bs2 bs r1)
|
|
|
591 |
then show ?case
|
|
|
592 |
apply(auto)
|
|
|
593 |
apply (meson bs6 contextrewrites0 rrewrite_srewrite.bs2 rs2 ss3 ss4 sss1 sss2)
|
|
|
594 |
by (simp add: r_in_rstar rrewrite_srewrite.bs2)
|
|
|
595 |
next
|
|
|
596 |
case (bs3 bs1 bs2 r)
|
|
|
597 |
then show ?case
|
|
|
598 |
apply(simp)
|
|
|
599 |
|
|
|
600 |
by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt)
|
|
|
601 |
next
|
|
|
602 |
case (bs4 r1 r2 bs r3)
|
|
|
603 |
have as: "r1 \<leadsto> r2" by fact
|
|
|
604 |
have IH: "bder c r1 \<leadsto>* bder c r2" by fact
|
|
|
605 |
from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r2 r3)"
|
|
|
606 |
by (metis bder.simps(5) bnullable0(1) contextrewrites1 rewrite_bmkeps_aux(1) star_seq)
|
|
|
607 |
next
|
|
|
608 |
case (bs5 r3 r4 bs r1)
|
|
|
609 |
have as: "r3 \<leadsto> r4" by fact
|
|
|
610 |
have IH: "bder c r3 \<leadsto>* bder c r4" by fact
|
|
|
611 |
from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)"
|
|
|
612 |
apply(simp)
|
|
|
613 |
apply(auto)
|
|
|
614 |
using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger
|
|
|
615 |
using star_seq2 by blast
|
|
|
616 |
next
|
|
|
617 |
case (bs6 bs)
|
|
|
618 |
then show ?case
|
|
|
619 |
using rrewrite_srewrite.bs6 by force
|
|
|
620 |
next
|
|
|
621 |
case (bs7 bs r)
|
|
|
622 |
then show ?case
|
|
|
623 |
by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7)
|
|
|
624 |
next
|
|
|
625 |
case (bs10 rs1 rs2 bs)
|
|
|
626 |
then show ?case
|
|
|
627 |
using contextrewrites0 by force
|
|
|
628 |
next
|
|
|
629 |
case ss1
|
|
|
630 |
then show ?case by simp
|
|
|
631 |
next
|
|
|
632 |
case (ss2 rs1 rs2 r)
|
|
|
633 |
then show ?case
|
|
|
634 |
by (simp add: srewrites7)
|
|
|
635 |
next
|
|
|
636 |
case (ss3 r1 r2 rs)
|
|
|
637 |
then show ?case
|
|
|
638 |
by (simp add: srewrites7)
|
|
|
639 |
next
|
|
|
640 |
case (ss4 rs)
|
|
|
641 |
then show ?case
|
|
|
642 |
using rrewrite_srewrite.ss4 by fastforce
|
|
|
643 |
next
|
|
|
644 |
case (ss5 bs1 rs1 rsb)
|
|
|
645 |
then show ?case
|
|
|
646 |
apply(simp)
|
|
|
647 |
using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast
|
|
|
648 |
next
|
|
|
649 |
case (ss6 a1 a2 bs rsa rsb)
|
|
|
650 |
then show ?case
|
|
|
651 |
apply(simp only: map_append map1)
|
|
|
652 |
apply(rule srewrites_trans)
|
|
|
653 |
apply(rule rs_in_rstar)
|
|
|
654 |
apply(rule_tac rrewrite_srewrite.ss6)
|
|
|
655 |
using Der_def der_correctness apply auto[1]
|
|
|
656 |
by blast
|
|
|
657 |
qed
|
|
|
658 |
|
|
|
659 |
lemma rewrites_preserves_bder:
|
|
|
660 |
assumes "r1 \<leadsto>* r2"
|
|
|
661 |
shows "bder c r1 \<leadsto>* bder c r2"
|
|
|
662 |
using assms
|
|
|
663 |
apply(induction r1 r2 rule: rrewrites.induct)
|
|
|
664 |
apply(simp_all add: rewrite_preserves_bder rrewrites_trans)
|
|
548
|
665 |
done
|
|
544
|
666 |
|
|
|
667 |
|
|
|
668 |
|
|
548
|
669 |
lemma bders_simp_appendStrong :
|
|
|
670 |
shows "bdersStrong6 r (s1 @ s2) = bdersStrong6 (bdersStrong6 r s1) s2"
|
|
|
671 |
apply(induct s1 arbitrary: s2 rule: rev_induct)
|
|
|
672 |
apply simp
|
|
|
673 |
apply auto
|
|
|
674 |
done
|
|
|
675 |
|
|
|
676 |
|
|
546
|
677 |
|
|
|
678 |
|
|
547
|
679 |
lemma rewrites_to_bsimpStrong:
|
|
|
680 |
shows "r \<leadsto>* bsimpStrong6 r"
|
|
|
681 |
proof (induction r rule: bsimpStrong6.induct)
|
|
|
682 |
case (1 bs1 r1 r2)
|
|
|
683 |
have IH1: "r1 \<leadsto>* bsimpStrong6 r1" by fact
|
|
|
684 |
have IH2: "r2 \<leadsto>* bsimpStrong6 r2" by fact
|
|
|
685 |
{ assume as: "bsimpStrong6 r1 = AZERO \<or> bsimpStrong6 r2 = AZERO"
|
|
|
686 |
with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto
|
|
|
687 |
then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
|
|
|
688 |
by (metis bs2 continuous_rewrite rrewrites.simps star_seq2)
|
|
|
689 |
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" using as by auto
|
|
|
690 |
}
|
|
|
691 |
moreover
|
|
|
692 |
{ assume "\<exists>bs. bsimpStrong6 r1 = AONE bs"
|
|
|
693 |
then obtain bs where as: "bsimpStrong6 r1 = AONE bs" by blast
|
|
|
694 |
with IH1 have "r1 \<leadsto>* AONE bs" by simp
|
|
|
695 |
then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast
|
|
|
696 |
with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimpStrong6 r2)"
|
|
|
697 |
using rewrites_fuse by (meson rrewrites_trans)
|
|
|
698 |
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 (AONE bs) r2)" by simp
|
|
|
699 |
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by (simp add: as)
|
|
|
700 |
}
|
|
|
701 |
moreover
|
|
|
702 |
{ assume as1: "bsimpStrong6 r1 \<noteq> AZERO" "bsimpStrong6 r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimpStrong6 r1 = AONE bs)"
|
|
|
703 |
then have "bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2) = ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)"
|
|
|
704 |
by (simp add: bsimp_ASEQ1)
|
|
|
705 |
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" using as1 as2 IH1 IH2
|
|
|
706 |
by (metis rrewrites_trans star_seq star_seq2)
|
|
|
707 |
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by simp
|
|
|
708 |
}
|
|
|
709 |
ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" sorry
|
|
|
710 |
next
|
|
|
711 |
case (2 bs1 rs)
|
|
|
712 |
have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimpStrong6 x" by fact
|
|
|
713 |
then have "rs s\<leadsto>* (map bsimpStrong6 rs)" by (simp add: trivialbsimp_srewrites)
|
|
|
714 |
also have "... s\<leadsto>* flts (map bsimpStrong6 rs)" by (simp add: fltsfrewrites)
|
|
|
715 |
also have "... s\<leadsto>* distinctWith (flts (map bsimpStrong6 rs)) eq1 {}" by (simp add: ss6_stronger)
|
|
|
716 |
finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})"
|
|
|
717 |
using contextrewrites0 by auto
|
|
|
718 |
also have "... \<leadsto>* bsimp_AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})"
|
|
|
719 |
by (simp add: bsimp_AALTs_rewrites)
|
|
|
720 |
finally show "AALTs bs1 rs \<leadsto>* bsimpStrong6 (AALTs bs1 rs)" sorry
|
|
|
721 |
qed (simp_all)
|
|
|
722 |
|
|
548
|
723 |
|
|
547
|
724 |
|
|
546
|
725 |
|
|
545
|
726 |
lemma centralStrong:
|
|
546
|
727 |
shows "bders r s \<leadsto>* bdersStrong6 r s"
|
|
545
|
728 |
proof(induct s arbitrary: r rule: rev_induct)
|
|
|
729 |
case Nil
|
|
546
|
730 |
then show "bders r [] \<leadsto>* bdersStrong6 r []" by simp
|
|
545
|
731 |
next
|
|
|
732 |
case (snoc x xs)
|
|
546
|
733 |
have IH: "\<And>r. bders r xs \<leadsto>* bdersStrong6 r xs" by fact
|
|
|
734 |
have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append)
|
|
|
735 |
also have "... \<leadsto>* bders (bdersStrong6 r xs) [x]" using IH
|
|
545
|
736 |
by (simp add: rewrites_preserves_bder)
|
|
546
|
737 |
also have "... \<leadsto>* bdersStrong6 (bdersStrong6 r xs) [x]" using IH
|
|
547
|
738 |
by (simp add: rewrites_to_bsimpStrong)
|
|
|
739 |
finally show "bders r (xs @ [x]) \<leadsto>* bdersStrong6 r (xs @ [x])"
|
|
|
740 |
by (simp add: bders_simp_appendStrong)
|
|
545
|
741 |
qed
|
|
|
742 |
|
|
|
743 |
lemma mainStrong:
|
|
|
744 |
assumes "bnullable (bders r s)"
|
|
546
|
745 |
shows "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)"
|
|
545
|
746 |
proof -
|
|
548
|
747 |
have "bders r s \<leadsto>* bdersStrong6 r s"
|
|
|
748 |
using centralStrong by force
|
|
545
|
749 |
then
|
|
546
|
750 |
show "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)"
|
|
548
|
751 |
using assms rewrites_bmkeps by blast
|
|
545
|
752 |
qed
|
|
|
753 |
|
|
|
754 |
|
|
|
755 |
|
|
|
756 |
|
|
|
757 |
theorem blexerStrong_correct :
|
|
548
|
758 |
shows "blexerStrong r s = blexer r s"
|
|
|
759 |
unfolding blexerStrong_def blexer_def
|
|
|
760 |
by (metis centralStrong mainStrong rewritesnullable)
|
|
545
|
761 |
|
|
544
|
762 |
|
|
|
763 |
|
|
|
764 |
end
|