src/HOL/HoareParallel/RG_Examples.thy
author berghofe
Mon Sep 30 16:14:02 2002 +0200 (2002-09-30)
changeset 13601 fd3e3d6b37b2
parent 13517 42efec18f5b2
child 14174 f3cafd2929d5
permissions -rw-r--r--
Adapted to new simplifier.
     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(subgoal_tac "j=0")
   151     apply (rotate_tac -1)
   152     apply (simp (asm_lr))
   153    apply arith
   154   apply clarify
   155   apply(case_tac i,simp,simp)
   156  apply clarify   
   157  apply simp
   158  apply(erule_tac x=0 in all_dupE)
   159  apply(erule_tac x=1 in allE,simp)
   160 apply clarify
   161 apply(case_tac i,simp)
   162  apply(rule Await)
   163   apply simp_all
   164  apply(clarify)
   165  apply(rule Seq)
   166   prefer 2
   167   apply(rule Basic)
   168    apply simp_all
   169   apply(rule subset_refl)
   170  apply(rule Basic)
   171  apply simp_all
   172  apply clarify
   173  apply simp
   174 apply(rule Await)
   175  apply simp_all
   176 apply(clarify)
   177 apply(rule Seq)
   178  prefer 2
   179  apply(rule Basic)
   180   apply simp_all
   181  apply(rule subset_refl)
   182 apply(rule Basic)
   183 apply simp_all
   184 apply clarify
   185 apply simp
   186 done
   187 
   188 subsubsection {* Parameterized *}
   189 
   190 lemma Example2_lemma1: "j<n \<Longrightarrow> (\<Sum>i<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
   191 apply(induct n)
   192  apply simp_all
   193 apply(force simp add: less_Suc_eq)
   194 done
   195 
   196 lemma Example2_lemma2_aux: 
   197  "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))"
   198 apply(induct n)
   199  apply simp_all
   200 apply(simp add:less_Suc_eq)
   201  apply(auto)
   202 apply(subgoal_tac "n - j = Suc(n- Suc j)")
   203   apply simp
   204 apply arith
   205 done 
   206 
   207 lemma Example2_lemma2_aux2: "j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
   208 apply(induct j)
   209  apply simp_all
   210 done
   211 
   212 lemma Example2_lemma2: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< n. (b (j:=1)) i)"
   213 apply(frule_tac b="(b (j:=1))" in Example2_lemma2_aux)
   214 apply(erule_tac  t="Summation (b(j := 1)) n" in ssubst)
   215 apply(frule_tac b=b in Example2_lemma2_aux)
   216 apply(erule_tac  t="Summation b n" in ssubst)
   217 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)))")
   218  apply(rotate_tac -1)
   219  apply(erule ssubst)
   220  apply(subgoal_tac "j\<le>j")
   221   apply(drule_tac b="b" and t=1 in Example2_lemma2_aux2)
   222   apply(rotate_tac -1)
   223   apply(erule ssubst)
   224 apply simp_all
   225 done
   226 
   227 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)"
   228 by(simp add:Example2_lemma2)
   229 
   230 lemma Example2_lemma3: "\<forall>i< n. b i = 1 \<Longrightarrow> (\<Sum>i<n. b i)= n"
   231 apply (induct n)
   232 apply auto
   233 done
   234 
   235 record Example2_parameterized =   
   236   C :: "nat \<Rightarrow> nat"
   237   y  :: nat
   238 
   239 lemma Example2_parameterized: "0<n \<Longrightarrow> 
   240   \<turnstile> COBEGIN SCHEME  [0\<le>i<n]
   241      (\<langle> \<acute>y:=\<acute>y+1;; \<acute>C:=\<acute>C (i:=1) \<rangle>, 
   242      \<lbrace>\<acute>y=(\<Sum>i<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>, 
   243      \<lbrace>\<ordmasculine>C i = \<ordfeminine>C i \<and> 
   244       (\<ordmasculine>y=(\<Sum>i<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i<n. \<ordfeminine>C i))\<rbrace>,  
   245      \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>C j = \<ordfeminine>C j) \<and> 
   246        (\<ordmasculine>y=(\<Sum>i<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i<n. \<ordfeminine>C i))\<rbrace>,
   247      \<lbrace>\<acute>y=(\<Sum>i<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>) 
   248     COEND
   249  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>]"
   250 apply(rule Parallel)
   251 apply force
   252 apply force
   253 apply(force elim:Example2_lemma1)
   254 apply clarify
   255 apply simp
   256 apply(force intro:Example2_lemma3)
   257 apply clarify
   258 apply simp
   259 apply(rule Await)
   260 apply simp_all
   261 apply clarify
   262 apply(rule Seq)
   263 prefer 2
   264 apply(rule Basic)
   265 apply(rule subset_refl)
   266 apply simp+
   267 apply(rule Basic)
   268 apply simp
   269 apply clarify
   270 apply simp
   271 apply(force elim:Example2_lemma2_Suc0)
   272 apply simp+
   273 done
   274 
   275 subsection {* Find Least Element *}
   276 
   277 text {* A previous lemma: *}
   278 
   279 lemma mod_aux :"\<lbrakk>i < (n::nat); a mod n = i;  j < a + n; j mod n = i; a < j\<rbrakk> \<Longrightarrow> False"
   280 apply(subgoal_tac "a=a div n*n + a mod n" )
   281  prefer 2 apply (simp (no_asm_use))
   282 apply(subgoal_tac "j=j div n*n + j mod n")
   283  prefer 2 apply (simp (no_asm_use))
   284 apply simp
   285 apply(subgoal_tac "a div n*n < j div n*n")
   286 prefer 2 apply arith
   287 apply(subgoal_tac "j div n*n < (a div n + 1)*n")
   288 prefer 2 apply simp
   289 apply (simp only:mult_less_cancel2)
   290 apply arith
   291 done
   292 
   293 record Example3 =
   294   X :: "nat \<Rightarrow> nat"
   295   Y :: "nat \<Rightarrow> nat"
   296 
   297 lemma Example3: "m mod n=0 \<Longrightarrow> 
   298  \<turnstile> COBEGIN 
   299  SCHEME [0\<le>i<n]
   300  (WHILE (\<forall>j<n. \<acute>X i < \<acute>Y j)  DO 
   301    IF P(B!(\<acute>X i)) THEN \<acute>Y:=\<acute>Y (i:=\<acute>X i) 
   302    ELSE \<acute>X:= \<acute>X (i:=(\<acute>X i)+ n) FI 
   303   OD,
   304  \<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>,
   305  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y j \<le> \<ordmasculine>Y j) \<and> \<ordmasculine>X i = \<ordfeminine>X i \<and> 
   306    \<ordmasculine>Y i = \<ordfeminine>Y i\<rbrace>,
   307  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X j = \<ordfeminine>X j \<and> \<ordmasculine>Y j = \<ordfeminine>Y j) \<and>   
   308    \<ordfeminine>Y i \<le> \<ordmasculine>Y i\<rbrace>,
   309  \<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>) 
   310  COEND
   311  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>,
   312   \<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> 
   313     (\<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>]"
   314 apply(rule Parallel)
   315 --{*5 subgoals left *}
   316 apply force+
   317 apply clarify
   318 apply simp
   319 apply(rule While)
   320     apply force
   321    apply force
   322   apply force
   323  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)
   324      apply force
   325     apply(rule subset_refl)+
   326  apply(rule Cond)
   327     apply force
   328    apply(rule Basic)
   329       apply force
   330      apply fastsimp
   331     apply force
   332    apply force
   333   apply(rule Basic)
   334      apply simp
   335      apply clarify
   336      apply simp
   337      apply(case_tac "X x (j mod n)\<le> j")
   338       apply(drule le_imp_less_or_eq)
   339       apply(erule disjE)
   340        apply(drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
   341         apply assumption+
   342        apply simp+
   343     apply clarsimp
   344     apply fastsimp
   345 apply force+
   346 done
   347 
   348 text {* Same but with a list as auxiliary variable: *}
   349 
   350 record Example3_list =
   351   X :: "nat list"
   352   Y :: "nat list"
   353 
   354 lemma Example3_list: "m mod n=0 \<Longrightarrow> \<turnstile> (COBEGIN SCHEME [0\<le>i<n]
   355  (WHILE (\<forall>j<n. \<acute>X!i < \<acute>Y!j)  DO 
   356      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 
   357   OD,
   358  \<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>,
   359  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y!j \<le> \<ordmasculine>Y!j) \<and> \<ordmasculine>X!i = \<ordfeminine>X!i \<and> 
   360    \<ordmasculine>Y!i = \<ordfeminine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
   361  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X!j = \<ordfeminine>X!j \<and> \<ordmasculine>Y!j = \<ordfeminine>Y!j) \<and>   
   362    \<ordfeminine>Y!i \<le> \<ordmasculine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
   363  \<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)
   364  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>,
   365       \<lbrace>\<ordmasculine>X=\<ordfeminine>X \<and> \<ordmasculine>Y=\<ordfeminine>Y\<rbrace>,
   366       \<lbrace>True\<rbrace>,
   367       \<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> 
   368         (\<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>]"
   369 apply(rule Parallel)
   370 --{* 5 subgoals left *}
   371 apply force+
   372 apply clarify
   373 apply simp
   374 apply(rule While)
   375     apply force
   376    apply force
   377   apply force
   378  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)
   379      apply force
   380     apply(rule subset_refl)+
   381  apply(rule Cond)
   382     apply force
   383    apply(rule Basic)
   384       apply force
   385      apply force
   386     apply force
   387    apply force
   388   apply(rule Basic)
   389      apply simp
   390      apply clarify
   391      apply simp
   392      apply(rule allI)
   393      apply(rule impI)+
   394      apply(case_tac "X x ! i\<le> j")
   395       apply(drule le_imp_less_or_eq)
   396       apply(erule disjE)
   397        apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux)
   398         apply assumption+
   399        apply simp
   400 apply force+
   401 done
   402 
   403 end