author | wenzelm |
Sun, 11 Feb 2018 12:51:23 +0100 | |
changeset 67593 | 5efb88c90051 |
parent 67443 | 3abf6a722518 |
child 68260 | 61188c781cdd |
permissions | -rw-r--r-- |
59189 | 1 |
section \<open>Examples\<close> |
13020 | 2 |
|
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
16733
diff
changeset
|
3 |
theory RG_Examples |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
16733
diff
changeset
|
4 |
imports RG_Syntax |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
16733
diff
changeset
|
5 |
begin |
13020 | 6 |
|
59189 | 7 |
lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def |
13020 | 8 |
|
59189 | 9 |
subsection \<open>Set Elements of an Array to Zero\<close> |
13020 | 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 |
||
59189 | 20 |
lemma Example1: |
13020 | 21 |
"\<turnstile> COBEGIN |
22 |
SCHEME [0 \<le> i < n] |
|
59189 | 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>) |
|
13020 | 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) |
|
59189 | 31 |
apply (auto intro!: Basic) |
13020 | 32 |
done |
33 |
||
59189 | 34 |
lemma Example1_parameterized: |
13020 | 35 |
"k < t \<Longrightarrow> |
59189 | 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>, |
|
13020 | 47 |
\<lbrace>\<forall>i<n. \<acute>A!(k*n+i) = 0\<rbrace>]" |
48 |
apply(rule Parallel) |
|
15102 | 49 |
apply auto |
50 |
apply(erule_tac x="k*n +i" in allE) |
|
51 |
apply(subgoal_tac "k*n+i <length (A b)") |
|
13020 | 52 |
apply force |
59189 | 53 |
apply(erule le_less_trans2) |
15102 | 54 |
apply(case_tac t,simp+) |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56248
diff
changeset
|
55 |
apply (simp add:add.commute) |
15102 | 56 |
apply(simp add: add_le_mono) |
13020 | 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+) |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56248
diff
changeset
|
64 |
apply (simp add:add.commute) |
15102 | 65 |
apply(rule add_le_mono, auto) |
13020 | 66 |
done |
67 |
||
15102 | 68 |
|
59189 | 69 |
subsection \<open>Increment a Variable in Parallel\<close> |
13020 | 70 |
|
59189 | 71 |
subsubsection \<open>Two components\<close> |
13020 | 72 |
|
73 |
record Example2 = |
|
74 |
x :: nat |
|
75 |
c_0 :: nat |
|
76 |
c_1 :: nat |
|
77 |
||
59189 | 78 |
lemma Example2: |
13020 | 79 |
"\<turnstile> COBEGIN |
59189 | 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 |
|
13020 | 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> |
|
59189 | 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 |
|
13020 | 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 |
|
59189 | 100 |
SAT [\<lbrace>\<acute>x=0 \<and> \<acute>c_0=0 \<and> \<acute>c_1=0\<rbrace>, |
13020 | 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 |
|
15102 | 109 |
apply(rule conjI) |
13020 | 110 |
apply clarify |
111 |
apply simp |
|
112 |
apply clarify |
|
113 |
apply simp |
|
114 |
apply simp |
|
15102 | 115 |
apply(rule conjI) |
13020 | 116 |
apply clarify |
117 |
apply simp |
|
118 |
apply clarify |
|
119 |
apply simp |
|
56248
67dc9549fa15
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
haftmann
parents:
52567
diff
changeset
|
120 |
apply(subgoal_tac "xa=0") |
67dc9549fa15
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
haftmann
parents:
52567
diff
changeset
|
121 |
apply simp |
13187 | 122 |
apply arith |
13020 | 123 |
apply clarify |
56248
67dc9549fa15
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
haftmann
parents:
52567
diff
changeset
|
124 |
apply(case_tac xaa, simp, simp) |
34233
156c42518cfc
removed more asm_rl's - unfortunately slowdown of 1 min.
nipkow
parents:
32621
diff
changeset
|
125 |
apply clarify |
13020 | 126 |
apply simp |
127 |
apply(erule_tac x=0 in all_dupE) |
|
128 |
apply(erule_tac x=1 in allE,simp) |
|
129 |
apply clarify |
|
130 |
apply(case_tac i,simp) |
|
131 |
apply(rule Await) |
|
132 |
apply simp_all |
|
133 |
apply(clarify) |
|
134 |
apply(rule Seq) |
|
135 |
prefer 2 |
|
136 |
apply(rule Basic) |
|
137 |
apply simp_all |
|
138 |
apply(rule subset_refl) |
|
139 |
apply(rule Basic) |
|
140 |
apply simp_all |
|
141 |
apply clarify |
|
142 |
apply simp |
|
143 |
apply(rule Await) |
|
144 |
apply simp_all |
|
145 |
apply(clarify) |
|
146 |
apply(rule Seq) |
|
147 |
prefer 2 |
|
148 |
apply(rule Basic) |
|
149 |
apply simp_all |
|
150 |
apply(rule subset_refl) |
|
15102 | 151 |
apply(auto intro!: Basic) |
13020 | 152 |
done |
153 |
||
59189 | 154 |
subsubsection \<open>Parameterized\<close> |
13020 | 155 |
|
59189 | 156 |
lemma Example2_lemma2_aux: "j<n \<Longrightarrow> |
15561 | 157 |
(\<Sum>i=0..<n. (b i::nat)) = |
158 |
(\<Sum>i=0..<j. b i) + b j + (\<Sum>i=0..<n-(Suc j) . b (Suc j + i))" |
|
13020 | 159 |
apply(induct n) |
160 |
apply simp_all |
|
161 |
apply(simp add:less_Suc_eq) |
|
162 |
apply(auto) |
|
163 |
apply(subgoal_tac "n - j = Suc(n- Suc j)") |
|
164 |
apply simp |
|
165 |
apply arith |
|
15561 | 166 |
done |
13020 | 167 |
|
59189 | 168 |
lemma Example2_lemma2_aux2: |
15561 | 169 |
"j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)" |
52567 | 170 |
by (induct j) simp_all |
13020 | 171 |
|
59189 | 172 |
lemma Example2_lemma2: |
15561 | 173 |
"\<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)" |
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14174
diff
changeset
|
174 |
apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux) |
64267 | 175 |
apply(erule_tac t="sum (b(j := (Suc 0))) {0..<n}" in ssubst) |
13020 | 176 |
apply(frule_tac b=b in Example2_lemma2_aux) |
64267 | 177 |
apply(erule_tac t="sum b {0..<n}" in ssubst) |
178 |
apply(subgoal_tac "Suc (sum b {0..<j} + b j + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))=(sum b {0..<j} + Suc (b j) + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))") |
|
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14174
diff
changeset
|
179 |
apply(rotate_tac -1) |
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14174
diff
changeset
|
180 |
apply(erule ssubst) |
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14174
diff
changeset
|
181 |
apply(subgoal_tac "j\<le>j") |
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14174
diff
changeset
|
182 |
apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2) |
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14174
diff
changeset
|
183 |
apply(rotate_tac -1) |
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14174
diff
changeset
|
184 |
apply(erule ssubst) |
13020 | 185 |
apply simp_all |
186 |
done |
|
187 |
||
15561 | 188 |
lemma Example2_lemma2_Suc0: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> |
189 |
Suc (\<Sum>i::nat=0..< n. b i)=(\<Sum>i=0..< n. (b (j:=Suc 0)) i)" |
|
13020 | 190 |
by(simp add:Example2_lemma2) |
191 |
||
59189 | 192 |
record Example2_parameterized = |
13020 | 193 |
C :: "nat \<Rightarrow> nat" |
194 |
y :: nat |
|
195 |
||
59189 | 196 |
lemma Example2_parameterized: "0<n \<Longrightarrow> |
13020 | 197 |
\<turnstile> COBEGIN SCHEME [0\<le>i<n] |
59189 | 198 |
(\<langle> \<acute>y:=\<acute>y+1;; \<acute>C:=\<acute>C (i:=1) \<rangle>, |
199 |
\<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>, |
|
200 |
\<lbrace>\<ordmasculine>C i = \<ordfeminine>C i \<and> |
|
201 |
(\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>, |
|
202 |
\<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>C j = \<ordfeminine>C j) \<and> |
|
15561 | 203 |
(\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>, |
59189 | 204 |
\<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>) |
13020 | 205 |
COEND |
15561 | 206 |
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>]" |
13020 | 207 |
apply(rule Parallel) |
208 |
apply force |
|
209 |
apply force |
|
15561 | 210 |
apply(force) |
13020 | 211 |
apply clarify |
212 |
apply simp |
|
52567 | 213 |
apply simp |
13020 | 214 |
apply clarify |
215 |
apply simp |
|
216 |
apply(rule Await) |
|
217 |
apply simp_all |
|
218 |
apply clarify |
|
219 |
apply(rule Seq) |
|
220 |
prefer 2 |
|
221 |
apply(rule Basic) |
|
222 |
apply(rule subset_refl) |
|
223 |
apply simp+ |
|
224 |
apply(rule Basic) |
|
225 |
apply simp |
|
226 |
apply clarify |
|
227 |
apply simp |
|
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16417
diff
changeset
|
228 |
apply(simp add:Example2_lemma2_Suc0 cong:if_cong) |
52567 | 229 |
apply simp_all |
13020 | 230 |
done |
231 |
||
59189 | 232 |
subsection \<open>Find Least Element\<close> |
13020 | 233 |
|
59189 | 234 |
text \<open>A previous lemma:\<close> |
13020 | 235 |
|
236 |
lemma mod_aux :"\<lbrakk>i < (n::nat); a mod n = i; j < a + n; j mod n = i; a < j\<rbrakk> \<Longrightarrow> False" |
|
237 |
apply(subgoal_tac "a=a div n*n + a mod n" ) |
|
13517 | 238 |
prefer 2 apply (simp (no_asm_use)) |
13020 | 239 |
apply(subgoal_tac "j=j div n*n + j mod n") |
13517 | 240 |
prefer 2 apply (simp (no_asm_use)) |
13020 | 241 |
apply simp |
242 |
apply(subgoal_tac "a div n*n < j div n*n") |
|
243 |
prefer 2 apply arith |
|
244 |
apply(subgoal_tac "j div n*n < (a div n + 1)*n") |
|
13517 | 245 |
prefer 2 apply simp |
13020 | 246 |
apply (simp only:mult_less_cancel2) |
247 |
apply arith |
|
248 |
done |
|
249 |
||
250 |
record Example3 = |
|
251 |
X :: "nat \<Rightarrow> nat" |
|
252 |
Y :: "nat \<Rightarrow> nat" |
|
253 |
||
59189 | 254 |
lemma Example3: "m mod n=0 \<Longrightarrow> |
255 |
\<turnstile> COBEGIN |
|
13020 | 256 |
SCHEME [0\<le>i<n] |
59189 | 257 |
(WHILE (\<forall>j<n. \<acute>X i < \<acute>Y j) DO |
258 |
IF P(B!(\<acute>X i)) THEN \<acute>Y:=\<acute>Y (i:=\<acute>X i) |
|
259 |
ELSE \<acute>X:= \<acute>X (i:=(\<acute>X i)+ n) FI |
|
13020 | 260 |
OD, |
261 |
\<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>, |
|
59189 | 262 |
\<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y j \<le> \<ordmasculine>Y j) \<and> \<ordmasculine>X i = \<ordfeminine>X i \<and> |
13020 | 263 |
\<ordmasculine>Y i = \<ordfeminine>Y i\<rbrace>, |
59189 | 264 |
\<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X j = \<ordfeminine>X j \<and> \<ordmasculine>Y j = \<ordfeminine>Y j) \<and> |
13020 | 265 |
\<ordfeminine>Y i \<le> \<ordmasculine>Y i\<rbrace>, |
59189 | 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) \<and> (\<exists>j<n. \<acute>Y j \<le> \<acute>X i) \<rbrace>) |
13020 | 267 |
COEND |
268 |
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>, |
|
59189 | 269 |
\<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> |
13020 | 270 |
(\<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>]" |
271 |
apply(rule Parallel) |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
272 |
\<comment> \<open>5 subgoals left\<close> |
13020 | 273 |
apply force+ |
274 |
apply clarify |
|
275 |
apply simp |
|
276 |
apply(rule While) |
|
277 |
apply force |
|
278 |
apply force |
|
279 |
apply force |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13601
diff
changeset
|
280 |
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) |
13020 | 281 |
apply force |
282 |
apply(rule subset_refl)+ |
|
283 |
apply(rule Cond) |
|
284 |
apply force |
|
285 |
apply(rule Basic) |
|
286 |
apply force |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41842
diff
changeset
|
287 |
apply fastforce |
13020 | 288 |
apply force |
289 |
apply force |
|
290 |
apply(rule Basic) |
|
27676 | 291 |
apply simp |
13020 | 292 |
apply clarify |
293 |
apply simp |
|
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
16733
diff
changeset
|
294 |
apply (case_tac "X x (j mod n) \<le> j") |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
16733
diff
changeset
|
295 |
apply (drule le_imp_less_or_eq) |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
16733
diff
changeset
|
296 |
apply (erule disjE) |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
16733
diff
changeset
|
297 |
apply (drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux) |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
16733
diff
changeset
|
298 |
apply auto |
13020 | 299 |
done |
300 |
||
59189 | 301 |
text \<open>Same but with a list as auxiliary variable:\<close> |
13020 | 302 |
|
303 |
record Example3_list = |
|
304 |
X :: "nat list" |
|
305 |
Y :: "nat list" |
|
306 |
||
307 |
lemma Example3_list: "m mod n=0 \<Longrightarrow> \<turnstile> (COBEGIN SCHEME [0\<le>i<n] |
|
59189 | 308 |
(WHILE (\<forall>j<n. \<acute>X!i < \<acute>Y!j) DO |
309 |
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 |
|
13020 | 310 |
OD, |
311 |
\<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>, |
|
59189 | 312 |
\<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y!j \<le> \<ordmasculine>Y!j) \<and> \<ordmasculine>X!i = \<ordfeminine>X!i \<and> |
13020 | 313 |
\<ordmasculine>Y!i = \<ordfeminine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>, |
59189 | 314 |
\<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X!j = \<ordfeminine>X!j \<and> \<ordmasculine>Y!j = \<ordfeminine>Y!j) \<and> |
13020 | 315 |
\<ordfeminine>Y!i \<le> \<ordmasculine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>, |
316 |
\<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) |
|
317 |
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>, |
|
318 |
\<lbrace>\<ordmasculine>X=\<ordfeminine>X \<and> \<ordmasculine>Y=\<ordfeminine>Y\<rbrace>, |
|
319 |
\<lbrace>True\<rbrace>, |
|
59189 | 320 |
\<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> |
13020 | 321 |
(\<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>]" |
56248
67dc9549fa15
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
haftmann
parents:
52567
diff
changeset
|
322 |
apply (rule Parallel) |
59189 | 323 |
apply (auto cong del: strong_INF_cong strong_SUP_cong) |
56248
67dc9549fa15
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
haftmann
parents:
52567
diff
changeset
|
324 |
apply force |
67dc9549fa15
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
haftmann
parents:
52567
diff
changeset
|
325 |
apply (rule While) |
13020 | 326 |
apply force |
327 |
apply force |
|
328 |
apply force |
|
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13601
diff
changeset
|
329 |
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) |
13020 | 330 |
apply force |
331 |
apply(rule subset_refl)+ |
|
332 |
apply(rule Cond) |
|
333 |
apply force |
|
334 |
apply(rule Basic) |
|
335 |
apply force |
|
336 |
apply force |
|
337 |
apply force |
|
338 |
apply force |
|
339 |
apply(rule Basic) |
|
340 |
apply simp |
|
341 |
apply clarify |
|
27676 | 342 |
apply simp |
13020 | 343 |
apply(rule allI) |
344 |
apply(rule impI)+ |
|
345 |
apply(case_tac "X x ! i\<le> j") |
|
346 |
apply(drule le_imp_less_or_eq) |
|
347 |
apply(erule disjE) |
|
348 |
apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux) |
|
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
16733
diff
changeset
|
349 |
apply auto |
13020 | 350 |
done |
351 |
||
13187 | 352 |
end |