author | berghofe |
Mon, 30 Sep 2002 16:14:02 +0200 | |
changeset 13601 | fd3e3d6b37b2 |
parent 13517 | 42efec18f5b2 |
child 14174 | f3cafd2929d5 |
permissions | -rw-r--r-- |
13020 | 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 |
|
13187 | 150 |
apply(subgoal_tac "j=0") |
151 |
apply (rotate_tac -1) |
|
13601 | 152 |
apply (simp (asm_lr)) |
13187 | 153 |
apply arith |
13020 | 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" ) |
|
13517 | 281 |
prefer 2 apply (simp (no_asm_use)) |
13020 | 282 |
apply(subgoal_tac "j=j div n*n + j mod n") |
13517 | 283 |
prefer 2 apply (simp (no_asm_use)) |
13020 | 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") |
|
13517 | 288 |
prefer 2 apply simp |
13020 | 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) |
|
13099 | 315 |
--{*5 subgoals left *} |
13020 | 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 |
|
13187 | 330 |
apply fastsimp |
13020 | 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+ |
|
13103
66659a4b16f6
Added insert_disjoint and disjoint_insert [simp], and simplified proofs
nipkow
parents:
13099
diff
changeset
|
343 |
apply clarsimp |
13187 | 344 |
apply fastsimp |
13020 | 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) |
|
13099 | 370 |
--{* 5 subgoals left *} |
13020 | 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 |
||
13187 | 403 |
end |