1.1 --- a/src/HOL/HoareParallel/RG_Hoare.thy	Wed Jul 26 13:31:07 2006 +0200
     1.2 +++ b/src/HOL/HoareParallel/RG_Hoare.thy	Wed Jul 26 19:23:04 2006 +0200
     1.3 @@ -361,11 +361,8 @@
     1.4  apply clarify
     1.5  apply(frule_tac j=0 and k="j" and p=pre in stability)
     1.6        apply simp_all
     1.7 -    apply arith
     1.8    apply(erule_tac x=i in allE,simp)
     1.9   apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
    1.10 -  apply arith
    1.11 - apply arith
    1.12  apply(case_tac "x!j")
    1.13  apply clarify
    1.14  apply simp
    1.15 @@ -492,11 +489,8 @@
    1.16  apply(simp add:assum_def)
    1.17  apply clarify
    1.18  apply(frule_tac j=0 and k="j" and p=pre in stability,simp_all)
    1.19 -   apply arith
    1.20    apply(erule_tac x=i in allE,simp)
    1.21   apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
    1.22 -  apply arith
    1.23 - apply arith
    1.24  apply(case_tac "x!j")
    1.25  apply clarify
    1.26  apply simp
    1.27 @@ -543,7 +537,6 @@
    1.28      apply(simp add:assum_def)
    1.29     apply(simp add:assum_def)
    1.30    apply(erule_tac m="length x" in etran_or_ctran,simp+)
    1.31 -  apply(case_tac x,simp+)
    1.32   apply(case_tac x, (simp add:last_length)+)
    1.33  apply(erule exE)
    1.34  apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence)
    1.35 @@ -555,18 +548,7 @@
    1.36   apply(erule_tac x="sa" in allE)
    1.37   apply(drule_tac c="drop (Suc m) x" in subsetD)
    1.38    apply simp
    1.39 -  apply(rule conjI)
    1.40 -   apply force
    1.41    apply clarify
    1.42 -  apply(subgoal_tac "(Suc m) + i \<le> length x")
    1.43 -   apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
    1.44 -    apply(rotate_tac -2)
    1.45 -    apply simp
    1.46 -    apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
    1.47 -    apply(subgoal_tac "Suc (Suc (m + i)) < length x",simp)
    1.48 -    apply arith
    1.49 -   apply arith
    1.50 -  apply arith
    1.51   apply simp
    1.52   apply clarify
    1.53   apply(case_tac "i\<le>m")
    1.54 @@ -575,49 +557,33 @@
    1.55     apply(erule_tac x=i in allE, erule impE, assumption)
    1.56     apply simp+
    1.57   apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
    1.58 -  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
    1.59 -   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
    1.60 -    apply(rotate_tac -2)
    1.61 -    apply simp
    1.62 -    apply(erule mp)
    1.63 -    apply arith
    1.64 -   apply arith
    1.65 -  apply arith
    1.66 -  apply(case_tac "length (drop (Suc m) x)",simp)
    1.67 -  apply(erule_tac x="sa" in allE)
    1.68 -  back
    1.69 -  apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
    1.70 -   apply(rule conjI)
    1.71 -    apply force
    1.72 -   apply clarify
    1.73 -   apply(subgoal_tac "(Suc m) + i \<le> length x")
    1.74 -    apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
    1.75 -     apply(rotate_tac -2)
    1.76 -     apply simp
    1.77 -     apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
    1.78 -     apply(subgoal_tac "Suc (Suc (m + i)) < length x")
    1.79 -      apply simp
    1.80 -     apply arith
    1.81 -    apply arith
    1.82 -   apply arith
    1.83 -  apply simp
    1.84 -  apply clarify
    1.85 -  apply(case_tac "i\<le>m")
    1.86 -   apply(drule le_imp_less_or_eq)
    1.87 -   apply(erule disjE)
    1.88 -    apply(erule_tac x=i in allE, erule impE, assumption)
    1.89 -    apply simp
    1.90 + apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
    1.91 +  apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
    1.92 +   apply(rotate_tac -2)
    1.93     apply simp
    1.94 -  apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
    1.95 -  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
    1.96 -   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
    1.97 -    apply(rotate_tac -2)
    1.98 -    apply simp
    1.99 -    apply(erule mp)
   1.100 -   apply arith
   1.101    apply arith
   1.102   apply arith
   1.103 - done  
   1.104 +apply(case_tac "length (drop (Suc m) x)",simp)
   1.105 +apply(erule_tac x="sa" in allE)
   1.106 +back
   1.107 +apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
   1.108 + apply clarify
   1.109 +apply simp
   1.110 +apply clarify
   1.111 +apply(case_tac "i\<le>m")
   1.112 + apply(drule le_imp_less_or_eq)
   1.113 + apply(erule disjE)
   1.114 +  apply(erule_tac x=i in allE, erule impE, assumption)
   1.115 +  apply simp
   1.116 + apply simp
   1.117 +apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
   1.118 +apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
   1.119 + apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
   1.120 +  apply(rotate_tac -2)
   1.121 +  apply simp
   1.122 + apply arith
   1.123 +apply arith
   1.124 +done
   1.125  
   1.126  subsubsection{* Soundness of the Sequential rule *}
   1.127  
   1.128 @@ -862,8 +828,6 @@
   1.129        apply simp
   1.130        apply(erule mp)
   1.131        apply(case_tac ys,simp+)
   1.132 -     apply arith
   1.133 -    apply arith
   1.134     apply force
   1.135    apply arith
   1.136   apply force