# HG changeset patch
# User nipkow
# Date 1127426142 -7200
# Node ID f2bd501398eef6940492e9a0ba33e45b6a7691f5
# Parent  760c6ade4ab615ac0b02fdf82c3718649434634c
fix because of list lemmas

diff -r 760c6ade4ab6 -r f2bd501398ee src/HOL/HoareParallel/RG_Hoare.thy
--- a/src/HOL/HoareParallel/RG_Hoare.thy	Thu Sep 22 23:43:55 2005 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy	Thu Sep 22 23:55:42 2005 +0200
@@ -526,11 +526,6 @@
 
 subsubsection{* Soundness of the Conditional rule *}
 
-lemma last_length2 [rule_format]: "xs\<noteq>[] \<longrightarrow> (last xs)=(xs!(length xs - (Suc 0)))"
-apply(induct xs,simp+)
-apply(case_tac "length xs",simp+)
-done
-
 lemma Cond_sound: 
   "\<lbrakk> stable pre rely; \<Turnstile> P1 sat [pre \<inter> b, rely, guar, post]; 
   \<Turnstile> P2 sat [pre \<inter> - b, rely, guar, post]; \<forall>s. (s,s)\<in>guar\<rbrakk>
@@ -579,49 +574,49 @@
    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)
+  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(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 mp)
+  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(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="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
-done  
+ done  
 
 subsubsection{* Soundness of the Sequential rule *}
 
@@ -781,7 +776,7 @@
  apply clarify
  apply (simp del:map.simps)
  apply(subgoal_tac "(map (lift Q) ((a, b) # list))\<noteq>[]")
-  apply(drule last_length2)
+  apply(drule last_conv_nth)
   apply (simp del:map.simps)
   apply(simp only:last_lift_not_None)
  apply simp
@@ -810,7 +805,7 @@
 apply(erule_tac x="snd(xs!m)" in allE)
 apply(drule_tac c=ys in subsetD,simp add:cp_def assum_def)
  apply(case_tac "xs\<noteq>[]")
- apply(drule last_length2,simp)
+ apply(drule last_conv_nth,simp)
  apply(rule conjI)
   apply(erule mp)
   apply(case_tac "xs!m")
@@ -873,7 +868,7 @@
  apply force
 apply clarify
 apply(case_tac "(map (lift Q) xs @ tl ys)\<noteq>[]")
- apply(drule last_length2)
+ apply(drule last_conv_nth)
  apply(simp add: snd_lift nth_append)
  apply(rule conjI,clarify)
   apply(case_tac ys,simp+)
@@ -1003,7 +998,7 @@
 --{* last=None *}
 apply clarify
 apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))\<noteq>[]")
- apply(drule last_length2)
+ apply(drule last_conv_nth)
  apply (simp del:map.simps)
  apply(simp only:last_lift_not_None)
 apply simp
@@ -1077,16 +1072,16 @@
 apply(case_tac ys)
  apply(simp add:Cons_lift del:map.simps last.simps)
  apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))\<noteq>[]")
-  apply(drule last_length2)
+  apply(drule last_conv_nth)
   apply (simp del:map.simps)
   apply(simp only:last_lift_not_None)
  apply simp
 apply(subgoal_tac "((Some (Seq P (While b P)), sa) # map (lift (While b P)) xs @ ys)\<noteq>[]")
- apply(drule last_length2)
+ apply(drule last_conv_nth)
  apply (simp del:map.simps last.simps)
  apply(simp add:nth_append del:last.simps)
  apply(subgoal_tac "((Some (While b P), snd (last ((Some P, sa) # xs))) # a # list)\<noteq>[]")
-  apply(drule last_length2)
+  apply(drule last_conv_nth)
   apply (simp del:map.simps last.simps)
  apply simp
 apply simp
@@ -1330,11 +1325,11 @@
  apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> length(?J j)=(?K j)" in allE)
  apply(subgoal_tac "length x - 1 < length x",simp)
   apply(case_tac "x\<noteq>[]")
-   apply(simp add: last_length2)
+   apply(simp add: last_conv_nth)
    apply(erule_tac x="clist!i" in ballE)
     apply(simp add:same_state_def)
     apply(subgoal_tac "clist!i\<noteq>[]")
-     apply(simp add: last_length2)
+     apply(simp add: last_conv_nth)
     apply(case_tac x)
      apply (force simp add:par_cp_def)
     apply (force simp add:par_cp_def)