src/HOL/HoareParallel/RG_Examples.thy
changeset 13020 791e3b4c4039
child 13099 4bb592cdde0e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy	Tue Mar 05 17:11:25 2002 +0100
     1.3 @@ -0,0 +1,408 @@
     1.4 +
     1.5 +header {* \section{Examples} *}
     1.6 +
     1.7 +theory RG_Examples = RG_Syntax:
     1.8 +
     1.9 +lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def 
    1.10 +
    1.11 +subsection {* Set Elements of an Array to Zero *}
    1.12 +
    1.13 +lemma le_less_trans2: "\<lbrakk>(j::nat)<k; i\<le> j\<rbrakk> \<Longrightarrow> i<k"
    1.14 +by simp
    1.15 +
    1.16 +lemma add_le_less_mono: "\<lbrakk> (a::nat) < c; b\<le>d \<rbrakk> \<Longrightarrow> a + b < c + d"
    1.17 +by simp
    1.18 +
    1.19 +record Example1 =
    1.20 +  A :: "nat list"
    1.21 +
    1.22 +lemma Example1: 
    1.23 + "\<turnstile> COBEGIN
    1.24 +      SCHEME [0 \<le> i < n]
    1.25 +     (\<acute>A := \<acute>A [i := 0], 
    1.26 +     \<lbrace> n < length \<acute>A \<rbrace>, 
    1.27 +     \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> \<ordmasculine>A ! i = \<ordfeminine>A ! i \<rbrace>, 
    1.28 +     \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> (\<forall>j<n. i \<noteq> j \<longrightarrow> \<ordmasculine>A ! j = \<ordfeminine>A ! j) \<rbrace>, 
    1.29 +     \<lbrace> \<acute>A ! i = 0 \<rbrace>) 
    1.30 +    COEND
    1.31 + SAT [\<lbrace> n < length \<acute>A \<rbrace>, \<lbrace> \<ordmasculine>A = \<ordfeminine>A \<rbrace>, \<lbrace> True \<rbrace>, \<lbrace> \<forall>i < n. \<acute>A ! i = 0 \<rbrace>]"
    1.32 +apply(rule Parallel)
    1.33 +    apply simp
    1.34 +    apply clarify
    1.35 +    apply simp
    1.36 +    apply(erule disjE)
    1.37 +     apply simp
    1.38 +    apply clarify
    1.39 +    apply simp
    1.40 +   apply auto
    1.41 +apply(rule Basic)
    1.42 +apply auto
    1.43 +done
    1.44 +
    1.45 +lemma Example1_parameterized: 
    1.46 +"k < t \<Longrightarrow>
    1.47 +  \<turnstile> COBEGIN 
    1.48 +    SCHEME [k*n\<le>i<(Suc k)*n] (\<acute>A:=\<acute>A[i:=0], 
    1.49 +   \<lbrace>t*n < length \<acute>A\<rbrace>, 
    1.50 +   \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> \<ordmasculine>A!i = \<ordfeminine>A!i\<rbrace>, 
    1.51 +   \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> (\<forall>j<length \<ordmasculine>A . i\<noteq>j \<longrightarrow> \<ordmasculine>A!j = \<ordfeminine>A!j)\<rbrace>, 
    1.52 +   \<lbrace>\<acute>A!i=0\<rbrace>) 
    1.53 +   COEND  
    1.54 + SAT [\<lbrace>t*n < length \<acute>A\<rbrace>, 
    1.55 +      \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> (\<forall>i<n. \<ordmasculine>A!(k*n+i)=\<ordfeminine>A!(k*n+i))\<rbrace>, 
    1.56 +      \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> 
    1.57 +      (\<forall>i<length \<ordmasculine>A . (i<k*n \<longrightarrow> \<ordmasculine>A!i = \<ordfeminine>A!i) \<and> ((Suc k)*n \<le> i\<longrightarrow> \<ordmasculine>A!i = \<ordfeminine>A!i))\<rbrace>, 
    1.58 +      \<lbrace>\<forall>i<n. \<acute>A!(k*n+i) = 0\<rbrace>]"
    1.59 +apply(rule Parallel)
    1.60 +    apply simp
    1.61 +    apply clarify
    1.62 +    apply simp
    1.63 +    apply(erule disjE)
    1.64 +     apply clarify
    1.65 +     apply simp
    1.66 +    apply clarify
    1.67 +    apply simp
    1.68 +    apply clarify
    1.69 +    apply simp
    1.70 +    apply(erule_tac x="k*n +i" in allE)
    1.71 +    apply(subgoal_tac "k*n+i <length (A b)")
    1.72 +     apply force
    1.73 +    apply(erule le_less_trans2) 
    1.74 +    apply(case_tac t,simp+)
    1.75 +    apply (simp add:add_commute)
    1.76 +    apply(rule add_le_mono)
    1.77 +     apply simp
    1.78 +    apply simp
    1.79 +   apply simp
    1.80 +   apply clarify
    1.81 +   apply(rotate_tac -1)
    1.82 +   apply force
    1.83 +  apply force
    1.84 + apply force
    1.85 +apply simp
    1.86 +apply clarify
    1.87 +apply(rule Basic)
    1.88 +   apply simp
    1.89 +   apply clarify
    1.90 +   apply (subgoal_tac "k*n+i< length (A x)")
    1.91 +    apply simp
    1.92 +   apply(erule le_less_trans2)
    1.93 +   apply(case_tac t,simp+)
    1.94 +   apply (simp add:add_commute)
    1.95 +   apply(rule add_le_mono)
    1.96 +    apply simp
    1.97 +   apply simp
    1.98 +  apply force+
    1.99 +done
   1.100 +
   1.101 +subsection {* Increment a Variable in Parallel *}
   1.102 +
   1.103 +subsubsection {* Two components *}
   1.104 +
   1.105 +record Example2 =
   1.106 +  x  :: nat
   1.107 +  c_0 :: nat
   1.108 +  c_1 :: nat
   1.109 +
   1.110 +lemma Example2: 
   1.111 + "\<turnstile>  COBEGIN
   1.112 +    (\<langle> \<acute>x:=\<acute>x+1;; \<acute>c_0:=\<acute>c_0 + 1 \<rangle>, 
   1.113 +     \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1  \<and> \<acute>c_0=0\<rbrace>, 
   1.114 +     \<lbrace>\<ordmasculine>c_0 = \<ordfeminine>c_0 \<and> 
   1.115 +        (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
   1.116 +        \<longrightarrow> \<ordfeminine>x = \<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,  
   1.117 +     \<lbrace>\<ordmasculine>c_1 = \<ordfeminine>c_1 \<and> 
   1.118 +         (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
   1.119 +         \<longrightarrow> \<ordfeminine>x =\<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
   1.120 +     \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_0=1 \<rbrace>)
   1.121 +  \<parallel>
   1.122 +      (\<langle> \<acute>x:=\<acute>x+1;; \<acute>c_1:=\<acute>c_1+1 \<rangle>, 
   1.123 +     \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_1=0 \<rbrace>, 
   1.124 +     \<lbrace>\<ordmasculine>c_1 = \<ordfeminine>c_1 \<and> 
   1.125 +        (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
   1.126 +        \<longrightarrow> \<ordfeminine>x = \<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,  
   1.127 +     \<lbrace>\<ordmasculine>c_0 = \<ordfeminine>c_0 \<and> 
   1.128 +         (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
   1.129 +        \<longrightarrow> \<ordfeminine>x =\<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
   1.130 +     \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_1=1\<rbrace>)
   1.131 + COEND
   1.132 + SAT [\<lbrace>\<acute>x=0 \<and> \<acute>c_0=0 \<and> \<acute>c_1=0\<rbrace>, 
   1.133 +      \<lbrace>\<ordmasculine>x=\<ordfeminine>x \<and>  \<ordmasculine>c_0= \<ordfeminine>c_0 \<and> \<ordmasculine>c_1=\<ordfeminine>c_1\<rbrace>,
   1.134 +      \<lbrace>True\<rbrace>,
   1.135 +      \<lbrace>\<acute>x=2\<rbrace>]"
   1.136 +apply(rule Parallel)
   1.137 +   apply simp_all
   1.138 +   apply clarify
   1.139 +   apply(case_tac i)
   1.140 +    apply simp
   1.141 +    apply(erule disjE)
   1.142 +     apply clarify
   1.143 +     apply simp
   1.144 +    apply clarify
   1.145 +    apply simp
   1.146 +    apply(case_tac j,simp)
   1.147 +    apply simp
   1.148 +   apply simp
   1.149 +   apply(erule disjE)
   1.150 +    apply clarify
   1.151 +    apply simp
   1.152 +   apply clarify
   1.153 +   apply simp
   1.154 +   apply(case_tac j,simp,simp)
   1.155 +  apply clarify
   1.156 +  apply(case_tac i,simp,simp)
   1.157 + apply clarify   
   1.158 + apply simp
   1.159 + apply(erule_tac x=0 in all_dupE)
   1.160 + apply(erule_tac x=1 in allE,simp)
   1.161 +apply clarify
   1.162 +apply(case_tac i,simp)
   1.163 + apply(rule Await)
   1.164 +  apply simp_all
   1.165 + apply(clarify)
   1.166 + apply(rule Seq)
   1.167 +  prefer 2
   1.168 +  apply(rule Basic)
   1.169 +   apply simp_all
   1.170 +  apply(rule subset_refl)
   1.171 + apply(rule Basic)
   1.172 + apply simp_all
   1.173 + apply clarify
   1.174 + apply simp
   1.175 +apply(rule Await)
   1.176 + apply simp_all
   1.177 +apply(clarify)
   1.178 +apply(rule Seq)
   1.179 + prefer 2
   1.180 + apply(rule Basic)
   1.181 +  apply simp_all
   1.182 + apply(rule subset_refl)
   1.183 +apply(rule Basic)
   1.184 +apply simp_all
   1.185 +apply clarify
   1.186 +apply simp
   1.187 +done
   1.188 +
   1.189 +subsubsection {* Parameterized *}
   1.190 +
   1.191 +lemma Example2_lemma1: "j<n \<Longrightarrow> (\<Sum>i<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
   1.192 +apply(induct n)
   1.193 + apply simp_all
   1.194 +apply(force simp add: less_Suc_eq)
   1.195 +done
   1.196 +
   1.197 +lemma Example2_lemma2_aux: 
   1.198 + "j<n \<Longrightarrow> (\<Sum>i<n. (b i::nat)) = (\<Sum>i<j. b i) + b j + (\<Sum>i<n-(Suc j) . b (Suc j + i))"
   1.199 +apply(induct n)
   1.200 + apply simp_all
   1.201 +apply(simp add:less_Suc_eq)
   1.202 + apply(auto)
   1.203 +apply(subgoal_tac "n - j = Suc(n- Suc j)")
   1.204 +  apply simp
   1.205 +apply arith
   1.206 +done 
   1.207 +
   1.208 +lemma Example2_lemma2_aux2: "j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
   1.209 +apply(induct j)
   1.210 + apply simp_all
   1.211 +done
   1.212 +
   1.213 +lemma Example2_lemma2: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< n. (b (j:=1)) i)"
   1.214 +apply(frule_tac b="(b (j:=1))" in Example2_lemma2_aux)
   1.215 +apply(erule_tac  t="Summation (b(j := 1)) n" in ssubst)
   1.216 +apply(frule_tac b=b in Example2_lemma2_aux)
   1.217 +apply(erule_tac  t="Summation b n" in ssubst)
   1.218 +apply(subgoal_tac "Suc (Summation b j + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(Summation b j + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
   1.219 + apply(rotate_tac -1)
   1.220 + apply(erule ssubst)
   1.221 + apply(subgoal_tac "j\<le>j")
   1.222 +  apply(drule_tac b="b" and t=1 in Example2_lemma2_aux2)
   1.223 +  apply(rotate_tac -1)
   1.224 +  apply(erule ssubst)
   1.225 +apply simp_all
   1.226 +done
   1.227 +
   1.228 +lemma Example2_lemma2_Suc0: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< n. (b (j:=Suc 0)) i)"
   1.229 +by(simp add:Example2_lemma2)
   1.230 +
   1.231 +lemma Example2_lemma3: "\<forall>i< n. b i = 1 \<Longrightarrow> (\<Sum>i<n. b i)= n"
   1.232 +apply (induct n)
   1.233 +apply auto
   1.234 +done
   1.235 +
   1.236 +record Example2_parameterized =   
   1.237 +  C :: "nat \<Rightarrow> nat"
   1.238 +  y  :: nat
   1.239 +
   1.240 +lemma Example2_parameterized: "0<n \<Longrightarrow> 
   1.241 +  \<turnstile> COBEGIN SCHEME  [0\<le>i<n]
   1.242 +     (\<langle> \<acute>y:=\<acute>y+1;; \<acute>C:=\<acute>C (i:=1) \<rangle>, 
   1.243 +     \<lbrace>\<acute>y=(\<Sum>i<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>, 
   1.244 +     \<lbrace>\<ordmasculine>C i = \<ordfeminine>C i \<and> 
   1.245 +      (\<ordmasculine>y=(\<Sum>i<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i<n. \<ordfeminine>C i))\<rbrace>,  
   1.246 +     \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>C j = \<ordfeminine>C j) \<and> 
   1.247 +       (\<ordmasculine>y=(\<Sum>i<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i<n. \<ordfeminine>C i))\<rbrace>,
   1.248 +     \<lbrace>\<acute>y=(\<Sum>i<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>) 
   1.249 +    COEND
   1.250 + SAT [\<lbrace>\<acute>y=0 \<and> (\<Sum>i<n. \<acute>C i)=0 \<rbrace>, \<lbrace>\<ordmasculine>C=\<ordfeminine>C \<and> \<ordmasculine>y=\<ordfeminine>y\<rbrace>, \<lbrace>True\<rbrace>, \<lbrace>\<acute>y=n\<rbrace>]"
   1.251 +apply(rule Parallel)
   1.252 +apply force
   1.253 +apply force
   1.254 +apply(force elim:Example2_lemma1)
   1.255 +apply clarify
   1.256 +apply simp
   1.257 +apply(force intro:Example2_lemma3)
   1.258 +apply clarify
   1.259 +apply simp
   1.260 +apply(rule Await)
   1.261 +apply simp_all
   1.262 +apply clarify
   1.263 +apply(rule Seq)
   1.264 +prefer 2
   1.265 +apply(rule Basic)
   1.266 +apply(rule subset_refl)
   1.267 +apply simp+
   1.268 +apply(rule Basic)
   1.269 +apply simp
   1.270 +apply clarify
   1.271 +apply simp
   1.272 +apply(force elim:Example2_lemma2_Suc0)
   1.273 +apply simp+
   1.274 +done
   1.275 +
   1.276 +subsection {* Find Least Element *}
   1.277 +
   1.278 +text {* A previous lemma: *}
   1.279 +
   1.280 +lemma mod_aux :"\<lbrakk>i < (n::nat); a mod n = i;  j < a + n; j mod n = i; a < j\<rbrakk> \<Longrightarrow> False"
   1.281 +apply(subgoal_tac "a=a div n*n + a mod n" )
   1.282 + prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric])
   1.283 +apply(subgoal_tac "j=j div n*n + j mod n")
   1.284 + prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric])
   1.285 +apply simp
   1.286 +apply(subgoal_tac "a div n*n < j div n*n")
   1.287 +prefer 2 apply arith
   1.288 +apply(subgoal_tac "j div n*n < (a div n + 1)*n")
   1.289 +prefer 2 apply simp 
   1.290 +apply (simp only:mult_less_cancel2)
   1.291 +apply arith
   1.292 +done
   1.293 +
   1.294 +record Example3 =
   1.295 +  X :: "nat \<Rightarrow> nat"
   1.296 +  Y :: "nat \<Rightarrow> nat"
   1.297 +
   1.298 +lemma Example3: "m mod n=0 \<Longrightarrow> 
   1.299 + \<turnstile> COBEGIN 
   1.300 + SCHEME [0\<le>i<n]
   1.301 + (WHILE (\<forall>j<n. \<acute>X i < \<acute>Y j)  DO 
   1.302 +   IF P(B!(\<acute>X i)) THEN \<acute>Y:=\<acute>Y (i:=\<acute>X i) 
   1.303 +   ELSE \<acute>X:= \<acute>X (i:=(\<acute>X i)+ n) FI 
   1.304 +  OD,
   1.305 + \<lbrace>(\<acute>X i) mod n=i \<and> (\<forall>j<\<acute>X i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y i<m \<longrightarrow> P(B!(\<acute>Y i)) \<and> \<acute>Y i\<le> m+i)\<rbrace>,
   1.306 + \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y j \<le> \<ordmasculine>Y j) \<and> \<ordmasculine>X i = \<ordfeminine>X i \<and> 
   1.307 +   \<ordmasculine>Y i = \<ordfeminine>Y i\<rbrace>,
   1.308 + \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X j = \<ordfeminine>X j \<and> \<ordmasculine>Y j = \<ordfeminine>Y j) \<and>   
   1.309 +   \<ordfeminine>Y i \<le> \<ordmasculine>Y i\<rbrace>,
   1.310 + \<lbrace>(\<acute>X i) mod n=i \<and> (\<forall>j<\<acute>X i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y i<m \<longrightarrow> P(B!(\<acute>Y i)) \<and> \<acute>Y i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y j \<le> \<acute>X i) \<rbrace>) 
   1.311 + COEND
   1.312 + SAT [\<lbrace> \<forall>i<n. \<acute>X i=i \<and> \<acute>Y i=m+i \<rbrace>,\<lbrace>\<ordmasculine>X=\<ordfeminine>X \<and> \<ordmasculine>Y=\<ordfeminine>Y\<rbrace>,\<lbrace>True\<rbrace>,
   1.313 +  \<lbrace>\<forall>i<n. (\<acute>X i) mod n=i \<and> (\<forall>j<\<acute>X i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> 
   1.314 +    (\<acute>Y i<m \<longrightarrow> P(B!(\<acute>Y i)) \<and> \<acute>Y i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y j \<le> \<acute>X i)\<rbrace>]"
   1.315 +apply(rule Parallel)
   1.316 +(*5*)
   1.317 +apply force+
   1.318 +apply clarify
   1.319 +apply simp
   1.320 +apply(rule While)
   1.321 +    apply force
   1.322 +   apply force
   1.323 +  apply force
   1.324 + apply(rule_tac "pre'"="\<lbrace> \<acute>X i mod n = i \<and> (\<forall>j. j<\<acute>X i \<longrightarrow> j mod n = i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y i < n * q \<longrightarrow> P (B!(\<acute>Y i))) \<and> \<acute>X i<\<acute>Y i\<rbrace>" in Conseq)
   1.325 +     apply force
   1.326 +    apply(rule subset_refl)+
   1.327 + apply(rule Cond)
   1.328 +    apply force
   1.329 +   apply(rule Basic)
   1.330 +      apply force
   1.331 +     apply force
   1.332 +    apply force
   1.333 +   apply force
   1.334 +  apply(rule Basic)
   1.335 +     apply simp
   1.336 +     apply clarify
   1.337 +     apply simp
   1.338 +     apply(case_tac "X x (j mod n)\<le> j")
   1.339 +      apply(drule le_imp_less_or_eq)
   1.340 +      apply(erule disjE)
   1.341 +       apply(drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
   1.342 +        apply assumption+
   1.343 +       apply simp+
   1.344 +     apply(erule_tac x=j in allE)
   1.345 +     apply force
   1.346 +    apply simp
   1.347 +    apply clarify
   1.348 +    apply(rule conjI)
   1.349 +     apply clarify  
   1.350 +     apply simp
   1.351 +     apply(erule not_sym)
   1.352 +    apply force
   1.353 +apply force+
   1.354 +done
   1.355 +
   1.356 +text {* Same but with a list as auxiliary variable: *}
   1.357 +
   1.358 +record Example3_list =
   1.359 +  X :: "nat list"
   1.360 +  Y :: "nat list"
   1.361 +
   1.362 +lemma Example3_list: "m mod n=0 \<Longrightarrow> \<turnstile> (COBEGIN SCHEME [0\<le>i<n]
   1.363 + (WHILE (\<forall>j<n. \<acute>X!i < \<acute>Y!j)  DO 
   1.364 +     IF P(B!(\<acute>X!i)) THEN \<acute>Y:=\<acute>Y[i:=\<acute>X!i] ELSE \<acute>X:= \<acute>X[i:=(\<acute>X!i)+ n] FI 
   1.365 +  OD,
   1.366 + \<lbrace>n<length \<acute>X \<and> n<length \<acute>Y \<and> (\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i)\<rbrace>,
   1.367 + \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y!j \<le> \<ordmasculine>Y!j) \<and> \<ordmasculine>X!i = \<ordfeminine>X!i \<and> 
   1.368 +   \<ordmasculine>Y!i = \<ordfeminine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
   1.369 + \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X!j = \<ordfeminine>X!j \<and> \<ordmasculine>Y!j = \<ordfeminine>Y!j) \<and>   
   1.370 +   \<ordfeminine>Y!i \<le> \<ordmasculine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
   1.371 + \<lbrace>(\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y!j \<le> \<acute>X!i) \<rbrace>) COEND)
   1.372 + SAT [\<lbrace>n<length \<acute>X \<and> n<length \<acute>Y \<and> (\<forall>i<n. \<acute>X!i=i \<and> \<acute>Y!i=m+i) \<rbrace>,
   1.373 +      \<lbrace>\<ordmasculine>X=\<ordfeminine>X \<and> \<ordmasculine>Y=\<ordfeminine>Y\<rbrace>,
   1.374 +      \<lbrace>True\<rbrace>,
   1.375 +      \<lbrace>\<forall>i<n. (\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> 
   1.376 +        (\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y!j \<le> \<acute>X!i)\<rbrace>]"
   1.377 +apply(rule Parallel)
   1.378 +(*5*)
   1.379 +apply force+
   1.380 +apply clarify
   1.381 +apply simp
   1.382 +apply(rule While)
   1.383 +    apply force
   1.384 +   apply force
   1.385 +  apply force
   1.386 + apply(rule_tac "pre'"="\<lbrace>n<length \<acute>X \<and> n<length \<acute>Y \<and> \<acute>X ! i mod n = i \<and> (\<forall>j. j < \<acute>X ! i \<longrightarrow> j mod n = i \<longrightarrow> \<not> P (B ! j)) \<and> (\<acute>Y ! i < n * q \<longrightarrow> P (B ! (\<acute>Y ! i))) \<and> \<acute>X!i<\<acute>Y!i\<rbrace>" in Conseq)
   1.387 +     apply force
   1.388 +    apply(rule subset_refl)+
   1.389 + apply(rule Cond)
   1.390 +    apply force
   1.391 +   apply(rule Basic)
   1.392 +      apply force
   1.393 +     apply force
   1.394 +    apply force
   1.395 +   apply force
   1.396 +  apply(rule Basic)
   1.397 +     apply simp
   1.398 +     apply clarify
   1.399 +     apply simp
   1.400 +     apply(rule allI)
   1.401 +     apply(rule impI)+
   1.402 +     apply(case_tac "X x ! i\<le> j")
   1.403 +      apply(drule le_imp_less_or_eq)
   1.404 +      apply(erule disjE)
   1.405 +       apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux)
   1.406 +        apply assumption+
   1.407 +       apply simp
   1.408 +apply force+
   1.409 +done
   1.410 +
   1.411 +end
   1.412 \ No newline at end of file