# HG changeset patch
# User wenzelm
# Date 1127240215 -7200
# Node ID 2a602a8462d5e0dd9dd00c1c0fb9633de0740a04
# Parent  5c25f27da4ca5506d1d0e44752b1a82b6838fe87
fixed proof script of lemma Cond_sound (Why did it stop working anyway?);

diff -r 5c25f27da4ca -r 2a602a8462d5 src/HOL/HoareParallel/RG_Hoare.thy
--- a/src/HOL/HoareParallel/RG_Hoare.thy	Tue Sep 20 19:38:35 2005 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy	Tue Sep 20 20:16:55 2005 +0200
@@ -591,14 +591,13 @@
    apply arith
   apply arith
  apply simp
- apply(rule conjI)
-  apply clarify
-  apply(case_tac "i\<le>m")
-   apply(drule le_imp_less_or_eq)
-   apply(erule disjE)
-    apply(erule_tac x=i in allE, erule impE, assumption)
-    apply simp+
-  apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
+ apply clarify
+ apply(case_tac "i\<le>m")
+  apply(drule le_imp_less_or_eq)
+  apply(erule disjE)
+   apply(erule_tac x=i in allE, erule impE, assumption)
+   apply simp+
+ apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
   apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
    apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
     apply(rotate_tac -2)
@@ -607,45 +606,41 @@
     apply arith
    apply arith
   apply arith
- apply(simp add:last_drop)
-apply(case_tac "length (drop (Suc m) x)",simp)
-apply(erule_tac x="sa" in allE)
-back
-apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
- apply(rule conjI)
-  apply force
- apply clarify
- apply(subgoal_tac "(Suc m) + i \<le> length x")
-  apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
-   apply(rotate_tac -2)
+  apply(case_tac "length (drop (Suc m) x)",simp)
+  apply(erule_tac x="sa" in allE)
+  back
+  apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
+   apply(rule conjI)
+    apply force
+   apply clarify
+   apply(subgoal_tac "(Suc m) + i \<le> length x")
+    apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
+     apply(rotate_tac -2)
+     apply simp
+     apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
+     apply(subgoal_tac "Suc (Suc (m + i)) < length x")
+      apply simp
+     apply arith
+    apply arith
+   apply arith
+  apply simp
+  apply clarify
+  apply(case_tac "i\<le>m")
+   apply(drule le_imp_less_or_eq)
+   apply(erule disjE)
+    apply(erule_tac x=i in allE, erule impE, assumption)
+    apply simp
    apply simp
-   apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
-   apply(subgoal_tac "Suc (Suc (m + i)) < length x")
+  apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
+  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
+   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
+    apply(rotate_tac -2)
     apply simp
+    apply(erule mp)
    apply arith
   apply arith
  apply arith
-apply simp
-apply clarify
-apply(rule conjI)
- apply clarify
- apply(case_tac "i\<le>m")
-  apply(drule le_imp_less_or_eq)
-  apply(erule disjE)
-   apply(erule_tac x=i in allE, erule impE, assumption)
-   apply simp
-  apply simp
- apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
- apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
-  apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
-   apply(rotate_tac -2)
-   apply simp
-   apply(erule mp)
-   apply arith
-  apply arith
- apply arith
-apply(simp add:last_drop)
-done  
+ done  
 
 subsubsection{* Soundness of the Sequential rule *}