src/HOL/HoareParallel/RG_Examples.thy
author prensani
Mon Apr 29 16:45:12 2002 +0200 (2002-04-29)
changeset 13099 4bb592cdde0e
parent 13020 791e3b4c4039
child 13103 66659a4b16f6
permissions -rw-r--r--
added abstract;corrected RG_Basic Hoare rule.
     1 
     2 header {* \section{Examples} *}
     3 
     4 theory RG_Examples = RG_Syntax:
     5 
     6 lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def 
     7 
     8 subsection {* Set Elements of an Array to Zero *}
     9 
    10 lemma le_less_trans2: "\<lbrakk>(j::nat)<k; i\<le> j\<rbrakk> \<Longrightarrow> i<k"
    11 by simp
    12 
    13 lemma add_le_less_mono: "\<lbrakk> (a::nat) < c; b\<le>d \<rbrakk> \<Longrightarrow> a + b < c + d"
    14 by simp
    15 
    16 record Example1 =
    17   A :: "nat list"
    18 
    19 lemma Example1: 
    20  "\<turnstile> COBEGIN
    21       SCHEME [0 \<le> i < n]
    22      (\<acute>A := \<acute>A [i := 0], 
    23      \<lbrace> n < length \<acute>A \<rbrace>, 
    24      \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> \<ordmasculine>A ! i = \<ordfeminine>A ! i \<rbrace>, 
    25      \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> (\<forall>j<n. i \<noteq> j \<longrightarrow> \<ordmasculine>A ! j = \<ordfeminine>A ! j) \<rbrace>, 
    26      \<lbrace> \<acute>A ! i = 0 \<rbrace>) 
    27     COEND
    28  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>]"
    29 apply(rule Parallel)
    30     apply simp
    31     apply clarify
    32     apply simp
    33     apply(erule disjE)
    34      apply simp
    35     apply clarify
    36     apply simp
    37    apply auto
    38 apply(rule Basic)
    39 apply auto
    40 done
    41 
    42 lemma Example1_parameterized: 
    43 "k < t \<Longrightarrow>
    44   \<turnstile> COBEGIN 
    45     SCHEME [k*n\<le>i<(Suc k)*n] (\<acute>A:=\<acute>A[i:=0], 
    46    \<lbrace>t*n < length \<acute>A\<rbrace>, 
    47    \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> \<ordmasculine>A!i = \<ordfeminine>A!i\<rbrace>, 
    48    \<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>, 
    49    \<lbrace>\<acute>A!i=0\<rbrace>) 
    50    COEND  
    51  SAT [\<lbrace>t*n < length \<acute>A\<rbrace>, 
    52       \<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>, 
    53       \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> 
    54       (\<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>, 
    55       \<lbrace>\<forall>i<n. \<acute>A!(k*n+i) = 0\<rbrace>]"
    56 apply(rule Parallel)
    57     apply simp
    58     apply clarify
    59     apply simp
    60     apply(erule disjE)
    61      apply clarify
    62      apply simp
    63     apply clarify
    64     apply simp
    65     apply clarify
    66     apply simp
    67     apply(erule_tac x="k*n +i" in allE)
    68     apply(subgoal_tac "k*n+i <length (A b)")
    69      apply force
    70     apply(erule le_less_trans2) 
    71     apply(case_tac t,simp+)
    72     apply (simp add:add_commute)
    73     apply(rule add_le_mono)
    74      apply simp
    75     apply simp
    76    apply simp
    77    apply clarify
    78    apply(rotate_tac -1)
    79    apply force
    80   apply force
    81  apply force
    82 apply simp
    83 apply clarify
    84 apply(rule Basic)
    85    apply simp
    86    apply clarify
    87    apply (subgoal_tac "k*n+i< length (A x)")
    88     apply simp
    89    apply(erule le_less_trans2)
    90    apply(case_tac t,simp+)
    91    apply (simp add:add_commute)
    92    apply(rule add_le_mono)
    93     apply simp
    94    apply simp
    95   apply force+
    96 done
    97 
    98 subsection {* Increment a Variable in Parallel *}
    99 
   100 subsubsection {* Two components *}
   101 
   102 record Example2 =
   103   x  :: nat
   104   c_0 :: nat
   105   c_1 :: nat
   106 
   107 lemma Example2: 
   108  "\<turnstile>  COBEGIN
   109     (\<langle> \<acute>x:=\<acute>x+1;; \<acute>c_0:=\<acute>c_0 + 1 \<rangle>, 
   110      \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1  \<and> \<acute>c_0=0\<rbrace>, 
   111      \<lbrace>\<ordmasculine>c_0 = \<ordfeminine>c_0 \<and> 
   112         (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
   113         \<longrightarrow> \<ordfeminine>x = \<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,  
   114      \<lbrace>\<ordmasculine>c_1 = \<ordfeminine>c_1 \<and> 
   115          (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
   116          \<longrightarrow> \<ordfeminine>x =\<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
   117      \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_0=1 \<rbrace>)
   118   \<parallel>
   119       (\<langle> \<acute>x:=\<acute>x+1;; \<acute>c_1:=\<acute>c_1+1 \<rangle>, 
   120      \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_1=0 \<rbrace>, 
   121      \<lbrace>\<ordmasculine>c_1 = \<ordfeminine>c_1 \<and> 
   122         (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
   123         \<longrightarrow> \<ordfeminine>x = \<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,  
   124      \<lbrace>\<ordmasculine>c_0 = \<ordfeminine>c_0 \<and> 
   125          (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
   126         \<longrightarrow> \<ordfeminine>x =\<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
   127      \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_1=1\<rbrace>)
   128  COEND
   129  SAT [\<lbrace>\<acute>x=0 \<and> \<acute>c_0=0 \<and> \<acute>c_1=0\<rbrace>, 
   130       \<lbrace>\<ordmasculine>x=\<ordfeminine>x \<and>  \<ordmasculine>c_0= \<ordfeminine>c_0 \<and> \<ordmasculine>c_1=\<ordfeminine>c_1\<rbrace>,
   131       \<lbrace>True\<rbrace>,
   132       \<lbrace>\<acute>x=2\<rbrace>]"
   133 apply(rule Parallel)
   134    apply simp_all
   135    apply clarify
   136    apply(case_tac i)
   137     apply simp
   138     apply(erule disjE)
   139      apply clarify
   140      apply simp
   141     apply clarify
   142     apply simp
   143     apply(case_tac j,simp)
   144     apply simp
   145    apply simp
   146    apply(erule disjE)
   147     apply clarify
   148     apply simp
   149    apply clarify
   150    apply simp
   151    apply(case_tac j,simp,simp)
   152   apply clarify
   153   apply(case_tac i,simp,simp)
   154  apply clarify   
   155  apply simp
   156  apply(erule_tac x=0 in all_dupE)
   157  apply(erule_tac x=1 in allE,simp)
   158 apply clarify
   159 apply(case_tac i,simp)
   160  apply(rule Await)
   161   apply simp_all
   162  apply(clarify)
   163  apply(rule Seq)
   164   prefer 2
   165   apply(rule Basic)
   166    apply simp_all
   167   apply(rule subset_refl)
   168  apply(rule Basic)
   169  apply simp_all
   170  apply clarify
   171  apply simp
   172 apply(rule Await)
   173  apply simp_all
   174 apply(clarify)
   175 apply(rule Seq)
   176  prefer 2
   177  apply(rule Basic)
   178   apply simp_all
   179  apply(rule subset_refl)
   180 apply(rule Basic)
   181 apply simp_all
   182 apply clarify
   183 apply simp
   184 done
   185 
   186 subsubsection {* Parameterized *}
   187 
   188 lemma Example2_lemma1: "j<n \<Longrightarrow> (\<Sum>i<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
   189 apply(induct n)
   190  apply simp_all
   191 apply(force simp add: less_Suc_eq)
   192 done
   193 
   194 lemma Example2_lemma2_aux: 
   195  "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))"
   196 apply(induct n)
   197  apply simp_all
   198 apply(simp add:less_Suc_eq)
   199  apply(auto)
   200 apply(subgoal_tac "n - j = Suc(n- Suc j)")
   201   apply simp
   202 apply arith
   203 done 
   204 
   205 lemma Example2_lemma2_aux2: "j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
   206 apply(induct j)
   207  apply simp_all
   208 done
   209 
   210 lemma Example2_lemma2: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< n. (b (j:=1)) i)"
   211 apply(frule_tac b="(b (j:=1))" in Example2_lemma2_aux)
   212 apply(erule_tac  t="Summation (b(j := 1)) n" in ssubst)
   213 apply(frule_tac b=b in Example2_lemma2_aux)
   214 apply(erule_tac  t="Summation b n" in ssubst)
   215 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)))")
   216  apply(rotate_tac -1)
   217  apply(erule ssubst)
   218  apply(subgoal_tac "j\<le>j")
   219   apply(drule_tac b="b" and t=1 in Example2_lemma2_aux2)
   220   apply(rotate_tac -1)
   221   apply(erule ssubst)
   222 apply simp_all
   223 done
   224 
   225 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)"
   226 by(simp add:Example2_lemma2)
   227 
   228 lemma Example2_lemma3: "\<forall>i< n. b i = 1 \<Longrightarrow> (\<Sum>i<n. b i)= n"
   229 apply (induct n)
   230 apply auto
   231 done
   232 
   233 record Example2_parameterized =   
   234   C :: "nat \<Rightarrow> nat"
   235   y  :: nat
   236 
   237 lemma Example2_parameterized: "0<n \<Longrightarrow> 
   238   \<turnstile> COBEGIN SCHEME  [0\<le>i<n]
   239      (\<langle> \<acute>y:=\<acute>y+1;; \<acute>C:=\<acute>C (i:=1) \<rangle>, 
   240      \<lbrace>\<acute>y=(\<Sum>i<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>, 
   241      \<lbrace>\<ordmasculine>C i = \<ordfeminine>C i \<and> 
   242       (\<ordmasculine>y=(\<Sum>i<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i<n. \<ordfeminine>C i))\<rbrace>,  
   243      \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>C j = \<ordfeminine>C j) \<and> 
   244        (\<ordmasculine>y=(\<Sum>i<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i<n. \<ordfeminine>C i))\<rbrace>,
   245      \<lbrace>\<acute>y=(\<Sum>i<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>) 
   246     COEND
   247  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>]"
   248 apply(rule Parallel)
   249 apply force
   250 apply force
   251 apply(force elim:Example2_lemma1)
   252 apply clarify
   253 apply simp
   254 apply(force intro:Example2_lemma3)
   255 apply clarify
   256 apply simp
   257 apply(rule Await)
   258 apply simp_all
   259 apply clarify
   260 apply(rule Seq)
   261 prefer 2
   262 apply(rule Basic)
   263 apply(rule subset_refl)
   264 apply simp+
   265 apply(rule Basic)
   266 apply simp
   267 apply clarify
   268 apply simp
   269 apply(force elim:Example2_lemma2_Suc0)
   270 apply simp+
   271 done
   272 
   273 subsection {* Find Least Element *}
   274 
   275 text {* A previous lemma: *}
   276 
   277 lemma mod_aux :"\<lbrakk>i < (n::nat); a mod n = i;  j < a + n; j mod n = i; a < j\<rbrakk> \<Longrightarrow> False"
   278 apply(subgoal_tac "a=a div n*n + a mod n" )
   279  prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric])
   280 apply(subgoal_tac "j=j div n*n + j mod n")
   281  prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric])
   282 apply simp
   283 apply(subgoal_tac "a div n*n < j div n*n")
   284 prefer 2 apply arith
   285 apply(subgoal_tac "j div n*n < (a div n + 1)*n")
   286 prefer 2 apply simp 
   287 apply (simp only:mult_less_cancel2)
   288 apply arith
   289 done
   290 
   291 record Example3 =
   292   X :: "nat \<Rightarrow> nat"
   293   Y :: "nat \<Rightarrow> nat"
   294 
   295 lemma Example3: "m mod n=0 \<Longrightarrow> 
   296  \<turnstile> COBEGIN 
   297  SCHEME [0\<le>i<n]
   298  (WHILE (\<forall>j<n. \<acute>X i < \<acute>Y j)  DO 
   299    IF P(B!(\<acute>X i)) THEN \<acute>Y:=\<acute>Y (i:=\<acute>X i) 
   300    ELSE \<acute>X:= \<acute>X (i:=(\<acute>X i)+ n) FI 
   301   OD,
   302  \<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>,
   303  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y j \<le> \<ordmasculine>Y j) \<and> \<ordmasculine>X i = \<ordfeminine>X i \<and> 
   304    \<ordmasculine>Y i = \<ordfeminine>Y i\<rbrace>,
   305  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X j = \<ordfeminine>X j \<and> \<ordmasculine>Y j = \<ordfeminine>Y j) \<and>   
   306    \<ordfeminine>Y i \<le> \<ordmasculine>Y i\<rbrace>,
   307  \<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>) 
   308  COEND
   309  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>,
   310   \<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> 
   311     (\<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>]"
   312 apply(rule Parallel)
   313 --{*5 subgoals left *}
   314 apply force+
   315 apply clarify
   316 apply simp
   317 apply(rule While)
   318     apply force
   319    apply force
   320   apply force
   321  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)
   322      apply force
   323     apply(rule subset_refl)+
   324  apply(rule Cond)
   325     apply force
   326    apply(rule Basic)
   327       apply force
   328      apply force
   329     apply force
   330    apply force
   331   apply(rule Basic)
   332      apply simp
   333      apply clarify
   334      apply simp
   335      apply(case_tac "X x (j mod n)\<le> j")
   336       apply(drule le_imp_less_or_eq)
   337       apply(erule disjE)
   338        apply(drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
   339         apply assumption+
   340        apply simp+
   341      apply(erule_tac x=j in allE)
   342      apply force
   343     apply simp
   344     apply clarify
   345     apply(rule conjI)
   346      apply clarify  
   347      apply simp
   348      apply(erule not_sym)
   349     apply force
   350 apply force+
   351 done
   352 
   353 text {* Same but with a list as auxiliary variable: *}
   354 
   355 record Example3_list =
   356   X :: "nat list"
   357   Y :: "nat list"
   358 
   359 lemma Example3_list: "m mod n=0 \<Longrightarrow> \<turnstile> (COBEGIN SCHEME [0\<le>i<n]
   360  (WHILE (\<forall>j<n. \<acute>X!i < \<acute>Y!j)  DO 
   361      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 
   362   OD,
   363  \<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>,
   364  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y!j \<le> \<ordmasculine>Y!j) \<and> \<ordmasculine>X!i = \<ordfeminine>X!i \<and> 
   365    \<ordmasculine>Y!i = \<ordfeminine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
   366  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X!j = \<ordfeminine>X!j \<and> \<ordmasculine>Y!j = \<ordfeminine>Y!j) \<and>   
   367    \<ordfeminine>Y!i \<le> \<ordmasculine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
   368  \<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)
   369  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>,
   370       \<lbrace>\<ordmasculine>X=\<ordfeminine>X \<and> \<ordmasculine>Y=\<ordfeminine>Y\<rbrace>,
   371       \<lbrace>True\<rbrace>,
   372       \<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> 
   373         (\<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>]"
   374 apply(rule Parallel)
   375 --{* 5 subgoals left *}
   376 apply force+
   377 apply clarify
   378 apply simp
   379 apply(rule While)
   380     apply force
   381    apply force
   382   apply force
   383  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)
   384      apply force
   385     apply(rule subset_refl)+
   386  apply(rule Cond)
   387     apply force
   388    apply(rule Basic)
   389       apply force
   390      apply force
   391     apply force
   392    apply force
   393   apply(rule Basic)
   394      apply simp
   395      apply clarify
   396      apply simp
   397      apply(rule allI)
   398      apply(rule impI)+
   399      apply(case_tac "X x ! i\<le> j")
   400       apply(drule le_imp_less_or_eq)
   401       apply(erule disjE)
   402        apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux)
   403         apply assumption+
   404        apply simp
   405 apply force+
   406 done
   407 
   408 end