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