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