equal
deleted
inserted
replaced
264 |
264 |
265 lemma deletes_dB: |
265 lemma deletes_dB: |
266 shows " \<lbrakk>erase a \<in> erase ` set rs1\<rbrakk> \<Longrightarrow> (rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)" |
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") |
267 apply(subgoal_tac "\<exists>rs1a rs1b x. rs1 = rs1a @ [x] @ rs1b \<and> erase x = erase a") |
268 prefer 2 |
268 prefer 2 |
269 |
269 apply (meson existing_preimage) |
|
270 apply(erule exE)+ |
|
271 apply simp |
|
272 apply(subgoal_tac "(rs1a @ [x] @ rs1b @ [a] @ rs2) s\<leadsto> (rs1a @ [x] @ rs1b @ rs2)") |
|
273 apply (simp add: rs_in_rstar) |
|
274 apply(subgoal_tac "L (erase a) \<subseteq> L (erase x)") |
|
275 using ss6 apply presburger |
|
276 by simp |
|
277 |
|
278 lemma ss6_realistic: |
|
279 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (concat (map turnIntoTerms (map erase rs2)))))" |
|
280 |
270 |
281 |
271 sorry |
282 sorry |
|
283 |
272 |
284 |
273 lemma ss6_stronger_aux: |
285 lemma ss6_stronger_aux: |
274 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))" |
286 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))" |
275 apply(induct rs2 arbitrary: rs1) |
287 apply(induct rs2 arbitrary: rs1) |
276 apply simp |
288 apply simp |
278 apply(simp) |
290 apply(simp) |
279 apply(drule_tac x = "rs1" in meta_spec) |
291 apply(drule_tac x = "rs1" in meta_spec) |
280 apply(subgoal_tac "(rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)") |
292 apply(subgoal_tac "(rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)") |
281 using srewrites_trans apply blast |
293 using srewrites_trans apply blast |
282 using deletes_dB apply presburger |
294 using deletes_dB apply presburger |
|
295 apply(case_tac "set (turnIntoTerms (erase a)) \<subseteq> erase ` set rs1") |
|
296 |
|
297 apply simp |
283 |
298 |
284 apply(auto) |
299 apply(auto) |
285 prefer 2 |
300 prefer 2 |
286 apply(drule_tac x="rs1 @ [a]" in meta_spec) |
301 apply(drule_tac x="rs1 @ [a]" in meta_spec) |
287 apply(simp) |
302 apply(simp) |