--- a/src/HOL/HoareParallel/RG_Hoare.thy Mon Dec 22 18:29:20 2003 +0100
+++ b/src/HOL/HoareParallel/RG_Hoare.thy Mon Dec 22 22:52:38 2003 +0100
@@ -901,8 +901,6 @@
apply(case_tac ys,simp+)
apply clarify
apply(case_tac ys,simp+)
- apply(drule last_length2,simp)
-apply simp
done
subsubsection{* Soundness of the While rule *}
@@ -950,18 +948,6 @@
apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
done
-lemma last_append2:"ys\<noteq>[] \<Longrightarrow> last (xs@ys)=(last ys)"
-apply(frule last_length2)
-apply simp
-apply(subgoal_tac "xs@ys\<noteq>[]")
-apply(drule last_length2)
-back
-apply simp
-apply(drule_tac xs=xs in last_append)
-apply simp
-apply simp
-done
-
lemma While_sound_aux [rule_format]:
"\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar;
stable pre rely; stable post rely; x \<in> cptn_mod \<rbrakk>