250 assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2" |
250 assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2" |
251 shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)" |
251 shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)" |
252 using assms |
252 using assms |
253 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) |
254 |
254 |
|
255 (*harmless sorry*) |
|
256 lemma existing_preimage : |
|
257 shows "f a \<in> f ` set rs1 \<Longrightarrow> \<exists>rs1a rs1b x. rs1 = rs1a @ [x] @ rs1b \<and> f x = f a " |
|
258 apply(induct rs1) |
|
259 apply simp |
|
260 apply(case_tac "f a = f aa") |
|
261 |
|
262 sorry |
|
263 |
|
264 |
|
265 lemma deletes_dB: |
|
266 shows " \<lbrakk>erase a \<in> erase ` set rs1\<rbrakk> \<Longrightarrow> (rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)" |
|
267 apply(subgoal_tac "\<exists>rs1a rs1b x. rs1 = rs1a @ [x] @ rs1b \<and> erase x = erase a") |
|
268 prefer 2 |
|
269 |
|
270 |
|
271 sorry |
|
272 |
255 lemma ss6_stronger_aux: |
273 lemma ss6_stronger_aux: |
256 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))" |
274 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))" |
257 apply(induct rs2 arbitrary: rs1) |
275 apply(induct rs2 arbitrary: rs1) |
|
276 apply simp |
|
277 apply(case_tac "erase a \<in> erase ` set rs1") |
|
278 apply(simp) |
|
279 apply(drule_tac x = "rs1" in meta_spec) |
|
280 apply(subgoal_tac "(rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)") |
|
281 using srewrites_trans apply blast |
|
282 using deletes_dB apply presburger |
|
283 |
258 apply(auto) |
284 apply(auto) |
259 prefer 2 |
285 prefer 2 |
260 apply(drule_tac x="rs1 @ [a]" in meta_spec) |
286 apply(drule_tac x="rs1 @ [a]" in meta_spec) |
261 apply(simp) |
287 apply(simp) |
262 apply(drule_tac x="rs1" in meta_spec) |
288 apply(drule_tac x="rs1" in meta_spec) |