fixed proof script of lemma Cond_sound (Why did it stop working anyway?);
authorwenzelm
Tue Sep 20 20:16:55 2005 +0200 (2005-09-20)
changeset 175282a602a8462d5
parent 17527 5c25f27da4ca
child 17529 a436d89845af
fixed proof script of lemma Cond_sound (Why did it stop working anyway?);
src/HOL/HoareParallel/RG_Hoare.thy
     1.1 --- a/src/HOL/HoareParallel/RG_Hoare.thy	Tue Sep 20 19:38:35 2005 +0200
     1.2 +++ b/src/HOL/HoareParallel/RG_Hoare.thy	Tue Sep 20 20:16:55 2005 +0200
     1.3 @@ -591,14 +591,13 @@
     1.4     apply arith
     1.5    apply arith
     1.6   apply simp
     1.7 - apply(rule conjI)
     1.8 -  apply clarify
     1.9 -  apply(case_tac "i\<le>m")
    1.10 -   apply(drule le_imp_less_or_eq)
    1.11 -   apply(erule disjE)
    1.12 -    apply(erule_tac x=i in allE, erule impE, assumption)
    1.13 -    apply simp+
    1.14 -  apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
    1.15 + apply clarify
    1.16 + apply(case_tac "i\<le>m")
    1.17 +  apply(drule le_imp_less_or_eq)
    1.18 +  apply(erule disjE)
    1.19 +   apply(erule_tac x=i in allE, erule impE, assumption)
    1.20 +   apply simp+
    1.21 + apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
    1.22    apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
    1.23     apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
    1.24      apply(rotate_tac -2)
    1.25 @@ -607,45 +606,41 @@
    1.26      apply arith
    1.27     apply arith
    1.28    apply arith
    1.29 - apply(simp add:last_drop)
    1.30 -apply(case_tac "length (drop (Suc m) x)",simp)
    1.31 -apply(erule_tac x="sa" in allE)
    1.32 -back
    1.33 -apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
    1.34 - apply(rule conjI)
    1.35 -  apply force
    1.36 - apply clarify
    1.37 - apply(subgoal_tac "(Suc m) + i \<le> length x")
    1.38 -  apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
    1.39 -   apply(rotate_tac -2)
    1.40 +  apply(case_tac "length (drop (Suc m) x)",simp)
    1.41 +  apply(erule_tac x="sa" in allE)
    1.42 +  back
    1.43 +  apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
    1.44 +   apply(rule conjI)
    1.45 +    apply force
    1.46 +   apply clarify
    1.47 +   apply(subgoal_tac "(Suc m) + i \<le> length x")
    1.48 +    apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
    1.49 +     apply(rotate_tac -2)
    1.50 +     apply simp
    1.51 +     apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
    1.52 +     apply(subgoal_tac "Suc (Suc (m + i)) < length x")
    1.53 +      apply simp
    1.54 +     apply arith
    1.55 +    apply arith
    1.56 +   apply arith
    1.57 +  apply simp
    1.58 +  apply clarify
    1.59 +  apply(case_tac "i\<le>m")
    1.60 +   apply(drule le_imp_less_or_eq)
    1.61 +   apply(erule disjE)
    1.62 +    apply(erule_tac x=i in allE, erule impE, assumption)
    1.63 +    apply simp
    1.64     apply simp
    1.65 -   apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
    1.66 -   apply(subgoal_tac "Suc (Suc (m + i)) < length x")
    1.67 +  apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
    1.68 +  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
    1.69 +   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
    1.70 +    apply(rotate_tac -2)
    1.71      apply simp
    1.72 +    apply(erule mp)
    1.73     apply arith
    1.74    apply arith
    1.75   apply arith
    1.76 -apply simp
    1.77 -apply clarify
    1.78 -apply(rule conjI)
    1.79 - apply clarify
    1.80 - apply(case_tac "i\<le>m")
    1.81 -  apply(drule le_imp_less_or_eq)
    1.82 -  apply(erule disjE)
    1.83 -   apply(erule_tac x=i in allE, erule impE, assumption)
    1.84 -   apply simp
    1.85 -  apply simp
    1.86 - apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
    1.87 - apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
    1.88 -  apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
    1.89 -   apply(rotate_tac -2)
    1.90 -   apply simp
    1.91 -   apply(erule mp)
    1.92 -   apply arith
    1.93 -  apply arith
    1.94 - apply arith
    1.95 -apply(simp add:last_drop)
    1.96 -done  
    1.97 + done  
    1.98  
    1.99  subsubsection{* Soundness of the Sequential rule *}
   1.100