146 | ss2: "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)" |
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)" |
147 | ss3: "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)" |
148 | ss4: "(AZERO # rs) s\<leadsto> rs" |
148 | ss4: "(AZERO # rs) s\<leadsto> rs" |
149 | ss5: "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)" |
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)" |
150 | ss6: "L (erase a2) \<subseteq> L (erase a1) \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)" |
|
151 | ss7: " (as @ [a] @ as1) s\<leadsto> (as @ [prune6 (set (concat (map (\<lambda>r. turnIntoTerms (erase r)) as))) a Nil] @ as1)" |
151 |
152 |
152 |
153 |
153 inductive |
154 inductive |
154 rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100) |
155 rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100) |
155 where |
156 where |
185 using a1 a2 |
186 using a1 a2 |
186 apply(induct r1 r2 arbitrary: r3 rule: srewrites.induct) |
187 apply(induct r1 r2 arbitrary: r3 rule: srewrites.induct) |
187 apply(auto) |
188 apply(auto) |
188 done |
189 done |
189 |
190 |
190 |
|
191 |
|
192 lemma contextrewrites0: |
191 lemma contextrewrites0: |
193 "rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2" |
192 "rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2" |
194 apply(induct rs1 rs2 rule: srewrites.inducts) |
193 apply(induct rs1 rs2 rule: srewrites.inducts) |
195 apply simp |
194 apply simp |
196 using bs10 r_in_rstar rrewrites_trans by blast |
195 using bs10 r_in_rstar rrewrites_trans by blast |
211 shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto>* (rs @ rs2)" |
210 shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto>* (rs @ rs2)" |
212 apply(induct rs1 rs2 rule: srewrites.induct) |
211 apply(induct rs1 rs2 rule: srewrites.induct) |
213 apply(auto) |
212 apply(auto) |
214 using srewrite1 by blast |
213 using srewrite1 by blast |
215 |
214 |
|
215 lemma srewrites_prepend: |
|
216 shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (r # rs1) s\<leadsto>* (r # rs2)" |
|
217 by (metis append_Cons append_Nil srewrites1) |
|
218 |
216 lemma srewrite2: |
219 lemma srewrite2: |
217 shows "r1 \<leadsto> r2 \<Longrightarrow> True" |
220 shows "r1 \<leadsto> r2 \<Longrightarrow> True" |
218 and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)" |
221 and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)" |
219 apply(induct rule: rrewrite_srewrite.inducts) |
222 apply(induct arbitrary: rs rule: rrewrite_srewrite.inducts) |
220 apply(auto) |
223 apply simp+ |
221 apply (metis append_Cons append_Nil srewrites1) |
224 using srewrites_prepend apply force |
222 apply(meson srewrites.simps ss3) |
225 apply (simp add: rs_in_rstar ss3) |
223 apply (meson srewrites.simps ss4) |
226 using ss4 apply force |
224 apply (meson srewrites.simps ss5) |
227 using rs_in_rstar ss5 apply auto[1] |
225 by (metis append_Cons append_Nil srewrites.simps ss6) |
228 using rs_in_rstar ss6 apply auto[1] |
226 |
229 using rs_in_rstar ss7 by force |
|
230 |
|
231 |
|
232 |
227 |
233 |
228 lemma srewrites3: |
234 lemma srewrites3: |
229 shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)" |
235 shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)" |
230 apply(induct rs1 rs2 arbitrary: rs rule: srewrites.induct) |
236 apply(induct rs1 rs2 arbitrary: rs rule: srewrites.induct) |
231 apply(auto) |
237 apply(auto) |
232 by (meson srewrite2(2) srewrites_trans) |
238 by (meson srewrite2(2) srewrites_trans) |
233 |
239 |
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 |
240 |
244 lemma srewrites6: |
241 lemma srewrites6: |
245 assumes "r1 \<leadsto>* r2" |
242 assumes "r1 \<leadsto>* r2" |
246 shows "[r1] s\<leadsto>* [r2]" |
243 shows "[r1] s\<leadsto>* [r2]" |
247 using assms |
244 using assms |
254 shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)" |
251 shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)" |
255 using assms |
252 using assms |
256 by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans) |
253 by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans) |
257 |
254 |
258 lemma ss6_stronger_aux: |
255 lemma ss6_stronger_aux: |
259 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctWith rs2 eq1 (set rs1))" |
256 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))" |
260 apply(induct rs2 arbitrary: rs1) |
257 apply(induct rs2 arbitrary: rs1) |
261 apply(auto) |
258 apply(auto) |
262 prefer 2 |
259 prefer 2 |
263 apply(drule_tac x="rs1 @ [a]" in meta_spec) |
260 apply(drule_tac x="rs1 @ [a]" in meta_spec) |
264 apply(simp) |
261 apply(simp) |
268 apply(subgoal_tac "\<exists>rs1a rs1b. rs1 = rs1a @ [x] @ rs1b") |
265 apply(subgoal_tac "\<exists>rs1a rs1b. rs1 = rs1a @ [x] @ rs1b") |
269 prefer 2 |
266 prefer 2 |
270 apply (simp add: split_list) |
267 apply (simp add: split_list) |
271 apply(erule exE)+ |
268 apply(erule exE)+ |
272 apply(simp) |
269 apply(simp) |
273 using eq1_L rs_in_rstar ss6 by force |
270 using eq1_L rs_in_rstar ss |
|
271 sorry |
|
272 |
274 |
273 |
275 lemma ss6_stronger: |
274 lemma ss6_stronger: |
276 shows "rs1 s\<leadsto>* distinctWith rs1 eq1 {}" |
275 shows "rs1 s\<leadsto>* dB6 rs1 {}" |
277 by (metis append_Nil list.set(1) ss6_stronger_aux) |
276 sorry |
278 |
277 |
279 |
278 |
280 lemma rewrite_preserves_fuse: |
279 lemma rewrite_preserves_fuse: |
281 shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3" |
280 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" |
281 and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3" |
336 lemma continuous_rewrite: |
335 lemma continuous_rewrite: |
337 assumes "r1 \<leadsto>* AZERO" |
336 assumes "r1 \<leadsto>* AZERO" |
338 shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO" |
337 shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO" |
339 using assms bs1 star_seq by blast |
338 using assms bs1 star_seq by blast |
340 |
339 |
341 (* |
340 |
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 |
341 |
348 lemma bsimp_aalts_simpcases: |
342 lemma bsimp_aalts_simpcases: |
349 shows "AONE bs \<leadsto>* bsimp (AONE bs)" |
343 shows "AONE bs \<leadsto>* bsimpStrong6 (AONE bs)" |
350 and "AZERO \<leadsto>* bsimp AZERO" |
344 and "AZERO \<leadsto>* bsimpStrong6 AZERO" |
351 and "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)" |
345 and "ACHAR bs c \<leadsto>* bsimpStrong6 (ACHAR bs c)" |
352 by (simp_all) |
346 by (simp_all) |
353 |
347 |
354 lemma bsimp_AALTs_rewrites: |
348 lemma bsimp_AALTs_rewrites: |
355 shows "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs" |
349 shows "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs" |
356 by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps) |
350 by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps) |