# HG changeset patch # User nipkow # Date 1127390534 -7200 # Node ID df49216dc5926e0a33cc3e009a7ffbdf7e0ac959 # Parent a50a53081808512ea455373ac4500286a3bd21c3 Fix because of new lemma in List diff -r a50a53081808 -r df49216dc592 src/HOL/HoareParallel/RG_Hoare.thy --- a/src/HOL/HoareParallel/RG_Hoare.thy Thu Sep 22 13:52:55 2005 +0200 +++ b/src/HOL/HoareParallel/RG_Hoare.thy Thu Sep 22 14:02:14 2005 +0200 @@ -531,25 +531,6 @@ apply(case_tac "length xs",simp+) done -lemma last_drop: "Suc m last(drop (Suc m) x) = last x" -apply(case_tac "(drop (Suc m) x)\[]") - apply(drule last_length2) - apply(erule ssubst) - apply(simp only:length_drop) - apply(subgoal_tac "Suc m + (length x - Suc m - (Suc 0)) \ length x") - apply(simp only:nth_drop) - apply(case_tac "x\[]") - apply(drule last_length2) - apply(erule ssubst) - apply simp - apply(subgoal_tac "Suc (length x - 2)=(length x - Suc 0)") - apply simp - apply arith - apply simp - apply arith -apply (simp add:length_greater_0_conv [THEN sym]) -done - lemma Cond_sound: "\ stable pre rely; \ P1 sat [pre \ b, rely, guar, post]; \ P2 sat [pre \ - b, rely, guar, post]; \s. (s,s)\guar\ @@ -598,49 +579,49 @@ apply(erule_tac x=i in allE, erule impE, assumption) apply simp+ apply(erule_tac x="i - (Suc m)" and P="\j. ?H j \ ?J j \ (?I j)\guar" in allE) - apply(subgoal_tac "(Suc m)+(i - Suc m) \ length x") - apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \ 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 \ length x") - apply(subgoal_tac "(Suc m) + (Suc i) \ length x") - apply(rotate_tac -2) - apply simp - apply(erule_tac x="Suc (m + i)" and P="\j. ?H j \ ?J j \ ?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\m") - apply(drule le_imp_less_or_eq) - apply(erule disjE) - apply(erule_tac x=i in allE, erule impE, assumption) - apply simp + apply(subgoal_tac "(Suc m)+(i - Suc m) \ length x") + apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \ length x") + apply(rotate_tac -2) apply simp - apply(erule_tac x="i - (Suc m)" and P="\j. ?H j \ ?J j \ (?I j)\guar" in allE) - apply(subgoal_tac "(Suc m)+(i - Suc m) \ length x") - apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \ length x") - apply(rotate_tac -2) - apply simp - apply(erule mp) + apply(erule mp) apply arith apply arith apply arith - done +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 \ length x") + apply(subgoal_tac "(Suc m) + (Suc i) \ length x") + apply(rotate_tac -2) + apply simp + apply(erule_tac x="Suc (m + i)" and P="\j. ?H j \ ?J j \ ?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\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="\j. ?H j \ ?J j \ (?I j)\guar" in allE) +apply(subgoal_tac "(Suc m)+(i - Suc m) \ length x") + apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \ length x") + apply(rotate_tac -2) + apply simp + apply(erule mp) + apply arith + apply arith +apply arith +done subsubsection{* Soundness of the Sequential rule *}