1 theory Predicate_Compile_Examples |
|
2 imports Predicate_Compile_Alternative_Defs |
|
3 begin |
|
4 |
|
5 subsection {* Basic predicates *} |
|
6 |
|
7 inductive False' :: "bool" |
|
8 |
|
9 code_pred (expected_modes: bool) False' . |
|
10 code_pred [dseq] False' . |
|
11 code_pred [random_dseq] False' . |
|
12 |
|
13 values [expected "{}" pred] "{x. False'}" |
|
14 values [expected "{}" dseq 1] "{x. False'}" |
|
15 values [expected "{}" random_dseq 1, 1, 1] "{x. False'}" |
|
16 |
|
17 value "False'" |
|
18 |
|
19 inductive True' :: "bool" |
|
20 where |
|
21 "True ==> True'" |
|
22 |
|
23 code_pred True' . |
|
24 code_pred [dseq] True' . |
|
25 code_pred [random_dseq] True' . |
|
26 |
|
27 thm True'.equation |
|
28 thm True'.dseq_equation |
|
29 thm True'.random_dseq_equation |
|
30 values [expected "{()}" ]"{x. True'}" |
|
31 values [expected "{}" dseq 0] "{x. True'}" |
|
32 values [expected "{()}" dseq 1] "{x. True'}" |
|
33 values [expected "{()}" dseq 2] "{x. True'}" |
|
34 values [expected "{}" random_dseq 1, 1, 0] "{x. True'}" |
|
35 values [expected "{}" random_dseq 1, 1, 1] "{x. True'}" |
|
36 values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}" |
|
37 values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}" |
|
38 |
|
39 inductive EmptySet :: "'a \<Rightarrow> bool" |
|
40 |
|
41 code_pred (expected_modes: o => bool, i => bool) EmptySet . |
|
42 |
|
43 definition EmptySet' :: "'a \<Rightarrow> bool" |
|
44 where "EmptySet' = {}" |
|
45 |
|
46 code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' . |
|
47 |
|
48 inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool" |
|
49 |
|
50 code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel . |
|
51 |
|
52 inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
53 for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
54 |
|
55 code_pred |
|
56 (expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool, |
|
57 (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool, |
|
58 (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool, |
|
59 (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool, |
|
60 (o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool, |
|
61 (o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool, |
|
62 (i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool, |
|
63 (i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool) |
|
64 EmptyClosure . |
|
65 |
|
66 thm EmptyClosure.equation |
|
67 |
|
68 (* TODO: inductive package is broken! |
|
69 inductive False'' :: "bool" |
|
70 where |
|
71 "False \<Longrightarrow> False''" |
|
72 |
|
73 code_pred (expected_modes: []) False'' . |
|
74 |
|
75 inductive EmptySet'' :: "'a \<Rightarrow> bool" |
|
76 where |
|
77 "False \<Longrightarrow> EmptySet'' x" |
|
78 |
|
79 code_pred (expected_modes: [1]) EmptySet'' . |
|
80 code_pred (expected_modes: [], [1]) [inductify] EmptySet'' . |
|
81 *) |
|
82 |
|
83 consts a' :: 'a |
|
84 |
|
85 inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
86 where |
|
87 "Fact a' a'" |
|
88 |
|
89 code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact . |
|
90 |
|
91 inductive zerozero :: "nat * nat => bool" |
|
92 where |
|
93 "zerozero (0, 0)" |
|
94 |
|
95 code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero . |
|
96 code_pred [dseq] zerozero . |
|
97 code_pred [random_dseq] zerozero . |
|
98 |
|
99 thm zerozero.equation |
|
100 thm zerozero.dseq_equation |
|
101 thm zerozero.random_dseq_equation |
|
102 |
|
103 text {* We expect the user to expand the tuples in the values command. |
|
104 The following values command is not supported. *} |
|
105 (*values "{x. zerozero x}" *) |
|
106 text {* Instead, the user must type *} |
|
107 values "{(x, y). zerozero (x, y)}" |
|
108 |
|
109 values [expected "{}" dseq 0] "{(x, y). zerozero (x, y)}" |
|
110 values [expected "{(0::nat, 0::nat)}" dseq 1] "{(x, y). zerozero (x, y)}" |
|
111 values [expected "{(0::nat, 0::nat)}" dseq 2] "{(x, y). zerozero (x, y)}" |
|
112 values [expected "{}" random_dseq 1, 1, 2] "{(x, y). zerozero (x, y)}" |
|
113 values [expected "{(0::nat, 0:: nat)}" random_dseq 1, 1, 3] "{(x, y). zerozero (x, y)}" |
|
114 |
|
115 inductive nested_tuples :: "((int * int) * int * int) => bool" |
|
116 where |
|
117 "nested_tuples ((0, 1), 2, 3)" |
|
118 |
|
119 code_pred nested_tuples . |
|
120 |
|
121 inductive JamesBond :: "nat => int => code_numeral => bool" |
|
122 where |
|
123 "JamesBond 0 0 7" |
|
124 |
|
125 code_pred JamesBond . |
|
126 |
|
127 values [expected "{(0::nat, 0::int , 7::code_numeral)}"] "{(a, b, c). JamesBond a b c}" |
|
128 values [expected "{(0::nat, 7::code_numeral, 0:: int)}"] "{(a, c, b). JamesBond a b c}" |
|
129 values [expected "{(0::int, 0::nat, 7::code_numeral)}"] "{(b, a, c). JamesBond a b c}" |
|
130 values [expected "{(0::int, 7::code_numeral, 0::nat)}"] "{(b, c, a). JamesBond a b c}" |
|
131 values [expected "{(7::code_numeral, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}" |
|
132 values [expected "{(7::code_numeral, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}" |
|
133 |
|
134 values [expected "{(7::code_numeral, 0::int)}"] "{(a, b). JamesBond 0 b a}" |
|
135 values [expected "{(7::code_numeral, 0::nat)}"] "{(c, a). JamesBond a 0 c}" |
|
136 values [expected "{(0::nat, 7::code_numeral)}"] "{(a, c). JamesBond a 0 c}" |
|
137 |
|
138 |
|
139 subsection {* Alternative Rules *} |
|
140 |
|
141 datatype char = C | D | E | F | G | H |
|
142 |
|
143 inductive is_C_or_D |
|
144 where |
|
145 "(x = C) \<or> (x = D) ==> is_C_or_D x" |
|
146 |
|
147 code_pred (expected_modes: i => bool) is_C_or_D . |
|
148 thm is_C_or_D.equation |
|
149 |
|
150 inductive is_D_or_E |
|
151 where |
|
152 "(x = D) \<or> (x = E) ==> is_D_or_E x" |
|
153 |
|
154 lemma [code_pred_intro]: |
|
155 "is_D_or_E D" |
|
156 by (auto intro: is_D_or_E.intros) |
|
157 |
|
158 lemma [code_pred_intro]: |
|
159 "is_D_or_E E" |
|
160 by (auto intro: is_D_or_E.intros) |
|
161 |
|
162 code_pred (expected_modes: o => bool, i => bool) is_D_or_E |
|
163 proof - |
|
164 case is_D_or_E |
|
165 from is_D_or_E.prems show thesis |
|
166 proof |
|
167 fix xa |
|
168 assume x: "x = xa" |
|
169 assume "xa = D \<or> xa = E" |
|
170 from this show thesis |
|
171 proof |
|
172 assume "xa = D" from this x is_D_or_E(2) show thesis by simp |
|
173 next |
|
174 assume "xa = E" from this x is_D_or_E(3) show thesis by simp |
|
175 qed |
|
176 qed |
|
177 qed |
|
178 |
|
179 thm is_D_or_E.equation |
|
180 |
|
181 inductive is_F_or_G |
|
182 where |
|
183 "x = F \<or> x = G ==> is_F_or_G x" |
|
184 |
|
185 lemma [code_pred_intro]: |
|
186 "is_F_or_G F" |
|
187 by (auto intro: is_F_or_G.intros) |
|
188 |
|
189 lemma [code_pred_intro]: |
|
190 "is_F_or_G G" |
|
191 by (auto intro: is_F_or_G.intros) |
|
192 |
|
193 inductive is_FGH |
|
194 where |
|
195 "is_F_or_G x ==> is_FGH x" |
|
196 | "is_FGH H" |
|
197 |
|
198 text {* Compilation of is_FGH requires elimination rule for is_F_or_G *} |
|
199 |
|
200 code_pred (expected_modes: o => bool, i => bool) is_FGH |
|
201 proof - |
|
202 case is_F_or_G |
|
203 from this(1) show thesis |
|
204 proof |
|
205 fix xa |
|
206 assume x: "x = xa" |
|
207 assume "xa = F \<or> xa = G" |
|
208 from this show thesis |
|
209 proof |
|
210 assume "xa = F" |
|
211 from this x is_F_or_G(2) show thesis by simp |
|
212 next |
|
213 assume "xa = G" |
|
214 from this x is_F_or_G(3) show thesis by simp |
|
215 qed |
|
216 qed |
|
217 qed |
|
218 |
|
219 subsection {* Named alternative rules *} |
|
220 |
|
221 inductive appending |
|
222 where |
|
223 nil: "appending [] ys ys" |
|
224 | cons: "appending xs ys zs \<Longrightarrow> appending (x#xs) ys (x#zs)" |
|
225 |
|
226 lemma appending_alt_nil: "ys = zs \<Longrightarrow> appending [] ys zs" |
|
227 by (auto intro: appending.intros) |
|
228 |
|
229 lemma appending_alt_cons: "xs' = x # xs \<Longrightarrow> appending xs ys zs \<Longrightarrow> zs' = x # zs \<Longrightarrow> appending xs' ys zs'" |
|
230 by (auto intro: appending.intros) |
|
231 |
|
232 text {* With code_pred_intro, we can give fact names to the alternative rules, |
|
233 which are used for the code_pred command. *} |
|
234 |
|
235 declare appending_alt_nil[code_pred_intro alt_nil] appending_alt_cons[code_pred_intro alt_cons] |
|
236 |
|
237 code_pred appending |
|
238 proof - |
|
239 case appending |
|
240 from prems show thesis |
|
241 proof(cases) |
|
242 case nil |
|
243 from alt_nil nil show thesis by auto |
|
244 next |
|
245 case cons |
|
246 from alt_cons cons show thesis by fastsimp |
|
247 qed |
|
248 qed |
|
249 |
|
250 |
|
251 inductive ya_even and ya_odd :: "nat => bool" |
|
252 where |
|
253 even_zero: "ya_even 0" |
|
254 | odd_plus1: "ya_even x ==> ya_odd (x + 1)" |
|
255 | even_plus1: "ya_odd x ==> ya_even (x + 1)" |
|
256 |
|
257 |
|
258 declare even_zero[code_pred_intro even_0] |
|
259 |
|
260 lemma [code_pred_intro odd_Suc]: "ya_even x ==> ya_odd (Suc x)" |
|
261 by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros) |
|
262 |
|
263 lemma [code_pred_intro even_Suc]:"ya_odd x ==> ya_even (Suc x)" |
|
264 by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros) |
|
265 |
|
266 code_pred ya_even |
|
267 proof - |
|
268 case ya_even |
|
269 from ya_even.prems show thesis |
|
270 proof (cases) |
|
271 case even_zero |
|
272 from even_zero even_0 show thesis by simp |
|
273 next |
|
274 case even_plus1 |
|
275 from even_plus1 even_Suc show thesis by simp |
|
276 qed |
|
277 next |
|
278 case ya_odd |
|
279 from ya_odd.prems show thesis |
|
280 proof (cases) |
|
281 case odd_plus1 |
|
282 from odd_plus1 odd_Suc show thesis by simp |
|
283 qed |
|
284 qed |
|
285 |
|
286 subsection {* Preprocessor Inlining *} |
|
287 |
|
288 definition "equals == (op =)" |
|
289 |
|
290 inductive zerozero' :: "nat * nat => bool" where |
|
291 "equals (x, y) (0, 0) ==> zerozero' (x, y)" |
|
292 |
|
293 code_pred (expected_modes: i => bool) zerozero' . |
|
294 |
|
295 lemma zerozero'_eq: "zerozero' x == zerozero x" |
|
296 proof - |
|
297 have "zerozero' = zerozero" |
|
298 apply (auto simp add: mem_def) |
|
299 apply (cases rule: zerozero'.cases) |
|
300 apply (auto simp add: equals_def intro: zerozero.intros) |
|
301 apply (cases rule: zerozero.cases) |
|
302 apply (auto simp add: equals_def intro: zerozero'.intros) |
|
303 done |
|
304 from this show "zerozero' x == zerozero x" by auto |
|
305 qed |
|
306 |
|
307 declare zerozero'_eq [code_pred_inline] |
|
308 |
|
309 definition "zerozero'' x == zerozero' x" |
|
310 |
|
311 text {* if preprocessing fails, zerozero'' will not have all modes. *} |
|
312 |
|
313 code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' . |
|
314 |
|
315 subsection {* Sets and Numerals *} |
|
316 |
|
317 definition |
|
318 "one_or_two = {Suc 0, (Suc (Suc 0))}" |
|
319 |
|
320 code_pred [inductify] one_or_two . |
|
321 |
|
322 code_pred [dseq] one_or_two . |
|
323 code_pred [random_dseq] one_or_two . |
|
324 thm one_or_two.dseq_equation |
|
325 values [expected "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}" |
|
326 values [random_dseq 0,0,10] 3 "{x. one_or_two x}" |
|
327 |
|
328 inductive one_or_two' :: "nat => bool" |
|
329 where |
|
330 "one_or_two' 1" |
|
331 | "one_or_two' 2" |
|
332 |
|
333 code_pred one_or_two' . |
|
334 thm one_or_two'.equation |
|
335 |
|
336 values "{x. one_or_two' x}" |
|
337 |
|
338 definition one_or_two'': |
|
339 "one_or_two'' == {1, (2::nat)}" |
|
340 |
|
341 code_pred [inductify] one_or_two'' . |
|
342 thm one_or_two''.equation |
|
343 |
|
344 values "{x. one_or_two'' x}" |
|
345 |
|
346 subsection {* even predicate *} |
|
347 |
|
348 inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where |
|
349 "even 0" |
|
350 | "even n \<Longrightarrow> odd (Suc n)" |
|
351 | "odd n \<Longrightarrow> even (Suc n)" |
|
352 |
|
353 code_pred (expected_modes: i => bool, o => bool) even . |
|
354 code_pred [dseq] even . |
|
355 code_pred [random_dseq] even . |
|
356 |
|
357 thm odd.equation |
|
358 thm even.equation |
|
359 thm odd.dseq_equation |
|
360 thm even.dseq_equation |
|
361 thm odd.random_dseq_equation |
|
362 thm even.random_dseq_equation |
|
363 |
|
364 values "{x. even 2}" |
|
365 values "{x. odd 2}" |
|
366 values 10 "{n. even n}" |
|
367 values 10 "{n. odd n}" |
|
368 values [expected "{}" dseq 2] "{x. even 6}" |
|
369 values [expected "{}" dseq 6] "{x. even 6}" |
|
370 values [expected "{()}" dseq 7] "{x. even 6}" |
|
371 values [dseq 2] "{x. odd 7}" |
|
372 values [dseq 6] "{x. odd 7}" |
|
373 values [dseq 7] "{x. odd 7}" |
|
374 values [expected "{()}" dseq 8] "{x. odd 7}" |
|
375 |
|
376 values [expected "{}" dseq 0] 8 "{x. even x}" |
|
377 values [expected "{0::nat}" dseq 1] 8 "{x. even x}" |
|
378 values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}" |
|
379 values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}" |
|
380 values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}" |
|
381 |
|
382 values [random_dseq 1, 1, 0] 8 "{x. even x}" |
|
383 values [random_dseq 1, 1, 1] 8 "{x. even x}" |
|
384 values [random_dseq 1, 1, 2] 8 "{x. even x}" |
|
385 values [random_dseq 1, 1, 3] 8 "{x. even x}" |
|
386 values [random_dseq 1, 1, 6] 8 "{x. even x}" |
|
387 |
|
388 values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}" |
|
389 values [random_dseq 1, 1, 8] "{x. odd 7}" |
|
390 values [random_dseq 1, 1, 9] "{x. odd 7}" |
|
391 |
|
392 definition odd' where "odd' x == \<not> even x" |
|
393 |
|
394 code_pred (expected_modes: i => bool) [inductify] odd' . |
|
395 code_pred [dseq inductify] odd' . |
|
396 code_pred [random_dseq inductify] odd' . |
|
397 |
|
398 values [expected "{}" dseq 2] "{x. odd' 7}" |
|
399 values [expected "{()}" dseq 9] "{x. odd' 7}" |
|
400 values [expected "{}" dseq 2] "{x. odd' 8}" |
|
401 values [expected "{}" dseq 10] "{x. odd' 8}" |
|
402 |
|
403 |
|
404 inductive is_even :: "nat \<Rightarrow> bool" |
|
405 where |
|
406 "n mod 2 = 0 \<Longrightarrow> is_even n" |
|
407 |
|
408 code_pred (expected_modes: i => bool) is_even . |
|
409 |
|
410 subsection {* append predicate *} |
|
411 |
|
412 inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where |
|
413 "append [] xs xs" |
|
414 | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)" |
|
415 |
|
416 code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix, |
|
417 i => o => i => bool as suffix, i => i => i => bool) append . |
|
418 code_pred (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as "concat", o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as "slice", o \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool as prefix, |
|
419 i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool) append . |
|
420 |
|
421 code_pred [dseq] append . |
|
422 code_pred [random_dseq] append . |
|
423 |
|
424 thm append.equation |
|
425 thm append.dseq_equation |
|
426 thm append.random_dseq_equation |
|
427 |
|
428 values "{(ys, xs). append xs ys [0, Suc 0, 2]}" |
|
429 values "{zs. append [0, Suc 0, 2] [17, 8] zs}" |
|
430 values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}" |
|
431 |
|
432 values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" |
|
433 values [expected "{(([]::nat list), [Suc 0, 2, 3, 4, (5::nat)])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" |
|
434 values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" |
|
435 values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" |
|
436 values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" |
|
437 values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}" |
|
438 values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}" |
|
439 values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}" |
|
440 values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}" |
|
441 values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}" |
|
442 |
|
443 value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])" |
|
444 value [code] "Predicate.the (slice ([]::int list))" |
|
445 |
|
446 |
|
447 text {* tricky case with alternative rules *} |
|
448 |
|
449 inductive append2 |
|
450 where |
|
451 "append2 [] xs xs" |
|
452 | "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)" |
|
453 |
|
454 lemma append2_Nil: "append2 [] (xs::'b list) xs" |
|
455 by (simp add: append2.intros(1)) |
|
456 |
|
457 lemmas [code_pred_intro] = append2_Nil append2.intros(2) |
|
458 |
|
459 code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool, |
|
460 i => o => i => bool, i => i => i => bool) append2 |
|
461 proof - |
|
462 case append2 |
|
463 from append2(1) show thesis |
|
464 proof |
|
465 fix xs |
|
466 assume "xa = []" "xb = xs" "xc = xs" |
|
467 from this append2(2) show thesis by simp |
|
468 next |
|
469 fix xs ys zs x |
|
470 assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs" |
|
471 from this append2(3) show thesis by fastsimp |
|
472 qed |
|
473 qed |
|
474 |
|
475 inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool" |
|
476 where |
|
477 "tupled_append ([], xs, xs)" |
|
478 | "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)" |
|
479 |
|
480 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, |
|
481 i * o * i => bool, i * i * i => bool) tupled_append . |
|
482 |
|
483 code_pred (expected_modes: i \<times> i \<times> o \<Rightarrow> bool, o \<times> o \<times> i \<Rightarrow> bool, o \<times> i \<times> i \<Rightarrow> bool, |
|
484 i \<times> o \<times> i \<Rightarrow> bool, i \<times> i \<times> i \<Rightarrow> bool) tupled_append . |
|
485 |
|
486 code_pred [random_dseq] tupled_append . |
|
487 thm tupled_append.equation |
|
488 |
|
489 values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}" |
|
490 |
|
491 inductive tupled_append' |
|
492 where |
|
493 "tupled_append' ([], xs, xs)" |
|
494 | "[| ys = fst (xa, y); x # zs = snd (xa, y); |
|
495 tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)" |
|
496 |
|
497 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, |
|
498 i * o * i => bool, i * i * i => bool) tupled_append' . |
|
499 thm tupled_append'.equation |
|
500 |
|
501 inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool" |
|
502 where |
|
503 "tupled_append'' ([], xs, xs)" |
|
504 | "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)" |
|
505 |
|
506 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, |
|
507 i * o * i => bool, i * i * i => bool) tupled_append'' . |
|
508 thm tupled_append''.equation |
|
509 |
|
510 inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool" |
|
511 where |
|
512 "tupled_append''' ([], xs, xs)" |
|
513 | "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)" |
|
514 |
|
515 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, |
|
516 i * o * i => bool, i * i * i => bool) tupled_append''' . |
|
517 thm tupled_append'''.equation |
|
518 |
|
519 subsection {* map_ofP predicate *} |
|
520 |
|
521 inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" |
|
522 where |
|
523 "map_ofP ((a, b)#xs) a b" |
|
524 | "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b" |
|
525 |
|
526 code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP . |
|
527 thm map_ofP.equation |
|
528 |
|
529 subsection {* filter predicate *} |
|
530 |
|
531 inductive filter1 |
|
532 for P |
|
533 where |
|
534 "filter1 P [] []" |
|
535 | "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)" |
|
536 | "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys" |
|
537 |
|
538 code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 . |
|
539 code_pred [dseq] filter1 . |
|
540 code_pred [random_dseq] filter1 . |
|
541 |
|
542 thm filter1.equation |
|
543 |
|
544 values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}" |
|
545 values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}" |
|
546 values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}" |
|
547 |
|
548 inductive filter2 |
|
549 where |
|
550 "filter2 P [] []" |
|
551 | "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)" |
|
552 | "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys" |
|
553 |
|
554 code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 . |
|
555 code_pred [dseq] filter2 . |
|
556 code_pred [random_dseq] filter2 . |
|
557 |
|
558 thm filter2.equation |
|
559 thm filter2.random_dseq_equation |
|
560 |
|
561 inductive filter3 |
|
562 for P |
|
563 where |
|
564 "List.filter P xs = ys ==> filter3 P xs ys" |
|
565 |
|
566 code_pred (expected_modes: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) [skip_proof] filter3 . |
|
567 |
|
568 code_pred filter3 . |
|
569 thm filter3.equation |
|
570 |
|
571 (* |
|
572 inductive filter4 |
|
573 where |
|
574 "List.filter P xs = ys ==> filter4 P xs ys" |
|
575 |
|
576 code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 . |
|
577 (*code_pred [depth_limited] filter4 .*) |
|
578 (*code_pred [random] filter4 .*) |
|
579 *) |
|
580 subsection {* reverse predicate *} |
|
581 |
|
582 inductive rev where |
|
583 "rev [] []" |
|
584 | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys" |
|
585 |
|
586 code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev . |
|
587 |
|
588 thm rev.equation |
|
589 |
|
590 values "{xs. rev [0, 1, 2, 3::nat] xs}" |
|
591 |
|
592 inductive tupled_rev where |
|
593 "tupled_rev ([], [])" |
|
594 | "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)" |
|
595 |
|
596 code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev . |
|
597 thm tupled_rev.equation |
|
598 |
|
599 subsection {* partition predicate *} |
|
600 |
|
601 inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
|
602 for f where |
|
603 "partition f [] [] []" |
|
604 | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs" |
|
605 | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)" |
|
606 |
|
607 code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool, |
|
608 (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool) |
|
609 partition . |
|
610 code_pred [dseq] partition . |
|
611 code_pred [random_dseq] partition . |
|
612 |
|
613 values 10 "{(ys, zs). partition is_even |
|
614 [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}" |
|
615 values 10 "{zs. partition is_even zs [0, 2] [3, 5]}" |
|
616 values 10 "{zs. partition is_even zs [0, 7] [3, 5]}" |
|
617 |
|
618 inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool" |
|
619 for f where |
|
620 "tupled_partition f ([], [], [])" |
|
621 | "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)" |
|
622 | "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)" |
|
623 |
|
624 code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool, |
|
625 (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition . |
|
626 |
|
627 thm tupled_partition.equation |
|
628 |
|
629 lemma [code_pred_intro]: |
|
630 "r a b \<Longrightarrow> tranclp r a b" |
|
631 "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c" |
|
632 by auto |
|
633 |
|
634 subsection {* transitive predicate *} |
|
635 |
|
636 text {* Also look at the tabled transitive closure in the Library *} |
|
637 |
|
638 code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl, |
|
639 (o => i => bool) => i => i => bool, (o => i => bool) => o => i => bool as backwards_trancl, (o => o => bool) => i => i => bool, (o => o => bool) => i => o => bool, |
|
640 (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp |
|
641 proof - |
|
642 case tranclp |
|
643 from this converse_tranclpE[OF this(1)] show thesis by metis |
|
644 qed |
|
645 |
|
646 |
|
647 code_pred [dseq] tranclp . |
|
648 code_pred [random_dseq] tranclp . |
|
649 thm tranclp.equation |
|
650 thm tranclp.random_dseq_equation |
|
651 |
|
652 inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool" |
|
653 where |
|
654 "rtrancl' x x r" |
|
655 | "r x y ==> rtrancl' y z r ==> rtrancl' x z r" |
|
656 |
|
657 code_pred [random_dseq] rtrancl' . |
|
658 |
|
659 thm rtrancl'.random_dseq_equation |
|
660 |
|
661 inductive rtrancl'' :: "('a * 'a * ('a \<Rightarrow> 'a \<Rightarrow> bool)) \<Rightarrow> bool" |
|
662 where |
|
663 "rtrancl'' (x, x, r)" |
|
664 | "r x y \<Longrightarrow> rtrancl'' (y, z, r) \<Longrightarrow> rtrancl'' (x, z, r)" |
|
665 |
|
666 code_pred rtrancl'' . |
|
667 |
|
668 inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool" |
|
669 where |
|
670 "rtrancl''' (x, (x, x), r)" |
|
671 | "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)" |
|
672 |
|
673 code_pred rtrancl''' . |
|
674 |
|
675 |
|
676 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
|
677 "succ 0 1" |
|
678 | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)" |
|
679 |
|
680 code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ . |
|
681 code_pred [random_dseq] succ . |
|
682 thm succ.equation |
|
683 thm succ.random_dseq_equation |
|
684 |
|
685 values 10 "{(m, n). succ n m}" |
|
686 values "{m. succ 0 m}" |
|
687 values "{m. succ m 0}" |
|
688 |
|
689 text {* values command needs mode annotation of the parameter succ |
|
690 to disambiguate which mode is to be chosen. *} |
|
691 |
|
692 values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}" |
|
693 values [mode: o => i => bool] 10 "{n. tranclp succ n 10}" |
|
694 values 20 "{(n, m). tranclp succ n m}" |
|
695 |
|
696 inductive example_graph :: "int => int => bool" |
|
697 where |
|
698 "example_graph 0 1" |
|
699 | "example_graph 1 2" |
|
700 | "example_graph 1 3" |
|
701 | "example_graph 4 7" |
|
702 | "example_graph 4 5" |
|
703 | "example_graph 5 6" |
|
704 | "example_graph 7 6" |
|
705 | "example_graph 7 8" |
|
706 |
|
707 inductive not_reachable_in_example_graph :: "int => int => bool" |
|
708 where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y" |
|
709 |
|
710 code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph . |
|
711 |
|
712 thm not_reachable_in_example_graph.equation |
|
713 thm tranclp.equation |
|
714 value "not_reachable_in_example_graph 0 3" |
|
715 value "not_reachable_in_example_graph 4 8" |
|
716 value "not_reachable_in_example_graph 5 6" |
|
717 text {* rtrancl compilation is strange! *} |
|
718 (* |
|
719 value "not_reachable_in_example_graph 0 4" |
|
720 value "not_reachable_in_example_graph 1 6" |
|
721 value "not_reachable_in_example_graph 8 4"*) |
|
722 |
|
723 code_pred [dseq] not_reachable_in_example_graph . |
|
724 |
|
725 values [dseq 6] "{x. tranclp example_graph 0 3}" |
|
726 |
|
727 values [dseq 0] "{x. not_reachable_in_example_graph 0 3}" |
|
728 values [dseq 0] "{x. not_reachable_in_example_graph 0 4}" |
|
729 values [dseq 20] "{x. not_reachable_in_example_graph 0 4}" |
|
730 values [dseq 6] "{x. not_reachable_in_example_graph 0 3}" |
|
731 values [dseq 3] "{x. not_reachable_in_example_graph 4 2}" |
|
732 values [dseq 6] "{x. not_reachable_in_example_graph 4 2}" |
|
733 |
|
734 |
|
735 inductive not_reachable_in_example_graph' :: "int => int => bool" |
|
736 where "\<not> (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y" |
|
737 |
|
738 code_pred not_reachable_in_example_graph' . |
|
739 |
|
740 value "not_reachable_in_example_graph' 0 3" |
|
741 (* value "not_reachable_in_example_graph' 0 5" would not terminate *) |
|
742 |
|
743 |
|
744 (*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*) |
|
745 (*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *) |
|
746 (*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*) |
|
747 (*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*) |
|
748 (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *) |
|
749 (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *) |
|
750 |
|
751 code_pred [dseq] not_reachable_in_example_graph' . |
|
752 |
|
753 (*thm not_reachable_in_example_graph'.dseq_equation*) |
|
754 |
|
755 (*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*) |
|
756 (*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *) |
|
757 (*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}" |
|
758 values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*) |
|
759 (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *) |
|
760 (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *) |
|
761 |
|
762 subsection {* Free function variable *} |
|
763 |
|
764 inductive FF :: "nat => nat => bool" |
|
765 where |
|
766 "f x = y ==> FF x y" |
|
767 |
|
768 code_pred FF . |
|
769 |
|
770 subsection {* IMP *} |
|
771 |
|
772 types |
|
773 var = nat |
|
774 state = "int list" |
|
775 |
|
776 datatype com = |
|
777 Skip | |
|
778 Ass var "state => int" | |
|
779 Seq com com | |
|
780 IF "state => bool" com com | |
|
781 While "state => bool" com |
|
782 |
|
783 inductive exec :: "com => state => state => bool" where |
|
784 "exec Skip s s" | |
|
785 "exec (Ass x e) s (s[x := e(s)])" | |
|
786 "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" | |
|
787 "b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" | |
|
788 "~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" | |
|
789 "~b s ==> exec (While b c) s s" | |
|
790 "b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3" |
|
791 |
|
792 code_pred exec . |
|
793 |
|
794 values "{t. exec |
|
795 (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1)))) |
|
796 [3,5] t}" |
|
797 |
|
798 |
|
799 inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where |
|
800 "tupled_exec (Skip, s, s)" | |
|
801 "tupled_exec (Ass x e, s, s[x := e(s)])" | |
|
802 "tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" | |
|
803 "b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" | |
|
804 "~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" | |
|
805 "~b s ==> tupled_exec (While b c, s, s)" | |
|
806 "b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)" |
|
807 |
|
808 code_pred tupled_exec . |
|
809 |
|
810 values "{s. tupled_exec (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))), [3, 5], s)}" |
|
811 |
|
812 subsection {* CCS *} |
|
813 |
|
814 text{* This example formalizes finite CCS processes without communication or |
|
815 recursion. For simplicity, labels are natural numbers. *} |
|
816 |
|
817 datatype proc = nil | pre nat proc | or proc proc | par proc proc |
|
818 |
|
819 inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where |
|
820 "step (pre n p) n p" | |
|
821 "step p1 a q \<Longrightarrow> step (or p1 p2) a q" | |
|
822 "step p2 a q \<Longrightarrow> step (or p1 p2) a q" | |
|
823 "step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" | |
|
824 "step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)" |
|
825 |
|
826 code_pred step . |
|
827 |
|
828 inductive steps where |
|
829 "steps p [] p" | |
|
830 "step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r" |
|
831 |
|
832 code_pred steps . |
|
833 |
|
834 values 3 |
|
835 "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}" |
|
836 |
|
837 values 5 |
|
838 "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}" |
|
839 |
|
840 values 3 "{(a,q). step (par nil nil) a q}" |
|
841 |
|
842 |
|
843 inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool" |
|
844 where |
|
845 "tupled_step (pre n p, n, p)" | |
|
846 "tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" | |
|
847 "tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" | |
|
848 "tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)" | |
|
849 "tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)" |
|
850 |
|
851 code_pred tupled_step . |
|
852 thm tupled_step.equation |
|
853 |
|
854 subsection {* divmod *} |
|
855 |
|
856 inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where |
|
857 "k < l \<Longrightarrow> divmod_rel k l 0 k" |
|
858 | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r" |
|
859 |
|
860 code_pred divmod_rel . |
|
861 thm divmod_rel.equation |
|
862 value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)" |
|
863 |
|
864 subsection {* Transforming predicate logic into logic programs *} |
|
865 |
|
866 subsection {* Transforming functions into logic programs *} |
|
867 definition |
|
868 "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)" |
|
869 |
|
870 code_pred [inductify, skip_proof] case_f . |
|
871 thm case_fP.equation |
|
872 |
|
873 fun fold_map_idx where |
|
874 "fold_map_idx f i y [] = (y, [])" |
|
875 | "fold_map_idx f i y (x # xs) = |
|
876 (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs |
|
877 in (y'', x' # xs'))" |
|
878 |
|
879 code_pred [inductify] fold_map_idx . |
|
880 |
|
881 subsection {* Minimum *} |
|
882 |
|
883 definition Min |
|
884 where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)" |
|
885 |
|
886 code_pred [inductify] Min . |
|
887 thm Min.equation |
|
888 |
|
889 subsection {* Lexicographic order *} |
|
890 |
|
891 declare lexord_def[code_pred_def] |
|
892 code_pred [inductify] lexord . |
|
893 code_pred [random_dseq inductify] lexord . |
|
894 |
|
895 thm lexord.equation |
|
896 thm lexord.random_dseq_equation |
|
897 |
|
898 inductive less_than_nat :: "nat * nat => bool" |
|
899 where |
|
900 "less_than_nat (0, x)" |
|
901 | "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)" |
|
902 |
|
903 code_pred less_than_nat . |
|
904 |
|
905 code_pred [dseq] less_than_nat . |
|
906 code_pred [random_dseq] less_than_nat . |
|
907 |
|
908 inductive test_lexord :: "nat list * nat list => bool" |
|
909 where |
|
910 "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)" |
|
911 |
|
912 code_pred test_lexord . |
|
913 code_pred [dseq] test_lexord . |
|
914 code_pred [random_dseq] test_lexord . |
|
915 thm test_lexord.dseq_equation |
|
916 thm test_lexord.random_dseq_equation |
|
917 |
|
918 values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}" |
|
919 (*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*) |
|
920 |
|
921 lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv |
|
922 (* |
|
923 code_pred [inductify] lexn . |
|
924 thm lexn.equation |
|
925 *) |
|
926 (* |
|
927 code_pred [random_dseq inductify] lexn . |
|
928 thm lexn.random_dseq_equation |
|
929 |
|
930 values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}" |
|
931 *) |
|
932 inductive has_length |
|
933 where |
|
934 "has_length [] 0" |
|
935 | "has_length xs i ==> has_length (x # xs) (Suc i)" |
|
936 |
|
937 lemma has_length: |
|
938 "has_length xs n = (length xs = n)" |
|
939 proof (rule iffI) |
|
940 assume "has_length xs n" |
|
941 from this show "length xs = n" |
|
942 by (rule has_length.induct) auto |
|
943 next |
|
944 assume "length xs = n" |
|
945 from this show "has_length xs n" |
|
946 by (induct xs arbitrary: n) (auto intro: has_length.intros) |
|
947 qed |
|
948 |
|
949 lemma lexn_intros [code_pred_intro]: |
|
950 "has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)" |
|
951 "lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)" |
|
952 proof - |
|
953 assume "has_length xs i" "has_length ys i" "r (x, y)" |
|
954 from this has_length show "lexn r (Suc i) (x # xs, y # ys)" |
|
955 unfolding lexn_conv Collect_def mem_def |
|
956 by fastsimp |
|
957 next |
|
958 assume "lexn r i (xs, ys)" |
|
959 thm lexn_conv |
|
960 from this show "lexn r (Suc i) (x#xs, x#ys)" |
|
961 unfolding Collect_def mem_def lexn_conv |
|
962 apply auto |
|
963 apply (rule_tac x="x # xys" in exI) |
|
964 by auto |
|
965 qed |
|
966 |
|
967 code_pred [random_dseq] lexn |
|
968 proof - |
|
969 fix r n xs ys |
|
970 assume 1: "lexn r n (xs, ys)" |
|
971 assume 2: "\<And>r' i x xs' y ys'. r = r' ==> n = Suc i ==> (xs, ys) = (x # xs', y # ys') ==> has_length xs' i ==> has_length ys' i ==> r' (x, y) ==> thesis" |
|
972 assume 3: "\<And>r' i x xs' ys'. r = r' ==> n = Suc i ==> (xs, ys) = (x # xs', x # ys') ==> lexn r' i (xs', ys') ==> thesis" |
|
973 from 1 2 3 show thesis |
|
974 unfolding lexn_conv Collect_def mem_def |
|
975 apply (auto simp add: has_length) |
|
976 apply (case_tac xys) |
|
977 apply auto |
|
978 apply fastsimp |
|
979 apply fastsimp done |
|
980 qed |
|
981 |
|
982 values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}" |
|
983 |
|
984 code_pred [inductify, skip_proof] lex . |
|
985 thm lex.equation |
|
986 thm lex_def |
|
987 declare lenlex_conv[code_pred_def] |
|
988 code_pred [inductify, skip_proof] lenlex . |
|
989 thm lenlex.equation |
|
990 |
|
991 code_pred [random_dseq inductify] lenlex . |
|
992 thm lenlex.random_dseq_equation |
|
993 |
|
994 values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}" |
|
995 |
|
996 thm lists.intros |
|
997 code_pred [inductify] lists . |
|
998 thm lists.equation |
|
999 |
|
1000 subsection {* AVL Tree *} |
|
1001 |
|
1002 datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat |
|
1003 fun height :: "'a tree => nat" where |
|
1004 "height ET = 0" |
|
1005 | "height (MKT x l r h) = max (height l) (height r) + 1" |
|
1006 |
|
1007 primrec avl :: "'a tree => bool" |
|
1008 where |
|
1009 "avl ET = True" |
|
1010 | "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> |
|
1011 h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)" |
|
1012 (* |
|
1013 code_pred [inductify] avl . |
|
1014 thm avl.equation*) |
|
1015 |
|
1016 code_pred [new_random_dseq inductify] avl . |
|
1017 thm avl.new_random_dseq_equation |
|
1018 |
|
1019 values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}" |
|
1020 |
|
1021 fun set_of |
|
1022 where |
|
1023 "set_of ET = {}" |
|
1024 | "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)" |
|
1025 |
|
1026 fun is_ord :: "nat tree => bool" |
|
1027 where |
|
1028 "is_ord ET = True" |
|
1029 | "is_ord (MKT n l r h) = |
|
1030 ((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)" |
|
1031 |
|
1032 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of . |
|
1033 thm set_of.equation |
|
1034 |
|
1035 code_pred (expected_modes: i => bool) [inductify] is_ord . |
|
1036 thm is_ord_aux.equation |
|
1037 thm is_ord.equation |
|
1038 |
|
1039 subsection {* Definitions about Relations *} |
|
1040 |
|
1041 term "converse" |
|
1042 code_pred (modes: |
|
1043 (i * i => bool) => i * i => bool, |
|
1044 (i * o => bool) => o * i => bool, |
|
1045 (i * o => bool) => i * i => bool, |
|
1046 (o * i => bool) => i * o => bool, |
|
1047 (o * i => bool) => i * i => bool, |
|
1048 (o * o => bool) => o * o => bool, |
|
1049 (o * o => bool) => i * o => bool, |
|
1050 (o * o => bool) => o * i => bool, |
|
1051 (o * o => bool) => i * i => bool) [inductify] converse . |
|
1052 |
|
1053 thm converse.equation |
|
1054 code_pred [inductify] rel_comp . |
|
1055 thm rel_comp.equation |
|
1056 code_pred [inductify] Image . |
|
1057 thm Image.equation |
|
1058 declare singleton_iff[code_pred_inline] |
|
1059 declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def] |
|
1060 |
|
1061 code_pred (expected_modes: |
|
1062 (o => bool) => o => bool, |
|
1063 (o => bool) => i * o => bool, |
|
1064 (o => bool) => o * i => bool, |
|
1065 (o => bool) => i => bool, |
|
1066 (i => bool) => i * o => bool, |
|
1067 (i => bool) => o * i => bool, |
|
1068 (i => bool) => i => bool) [inductify] Id_on . |
|
1069 thm Id_on.equation |
|
1070 thm Domain_def |
|
1071 code_pred (modes: |
|
1072 (o * o => bool) => o => bool, |
|
1073 (o * o => bool) => i => bool, |
|
1074 (i * o => bool) => i => bool) [inductify] Domain . |
|
1075 thm Domain.equation |
|
1076 |
|
1077 thm Range_def |
|
1078 code_pred (modes: |
|
1079 (o * o => bool) => o => bool, |
|
1080 (o * o => bool) => i => bool, |
|
1081 (o * i => bool) => i => bool) [inductify] Range . |
|
1082 thm Range.equation |
|
1083 |
|
1084 code_pred [inductify] Field . |
|
1085 thm Field.equation |
|
1086 |
|
1087 thm refl_on_def |
|
1088 code_pred [inductify] refl_on . |
|
1089 thm refl_on.equation |
|
1090 code_pred [inductify] total_on . |
|
1091 thm total_on.equation |
|
1092 code_pred [inductify] antisym . |
|
1093 thm antisym.equation |
|
1094 code_pred [inductify] trans . |
|
1095 thm trans.equation |
|
1096 code_pred [inductify] single_valued . |
|
1097 thm single_valued.equation |
|
1098 thm inv_image_def |
|
1099 code_pred [inductify] inv_image . |
|
1100 thm inv_image.equation |
|
1101 |
|
1102 subsection {* Inverting list functions *} |
|
1103 |
|
1104 code_pred [inductify] size_list . |
|
1105 code_pred [new_random_dseq inductify] size_list . |
|
1106 thm size_listP.equation |
|
1107 thm size_listP.new_random_dseq_equation |
|
1108 |
|
1109 values [new_random_dseq 2,3,10] 3 "{xs. size_listP (xs::nat list) (5::nat)}" |
|
1110 |
|
1111 code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat . |
|
1112 thm concatP.equation |
|
1113 |
|
1114 values "{ys. concatP [[1, 2], [3, (4::int)]] ys}" |
|
1115 values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}" |
|
1116 |
|
1117 code_pred [dseq inductify] List.concat . |
|
1118 thm concatP.dseq_equation |
|
1119 |
|
1120 values [dseq 3] 3 |
|
1121 "{xs. concatP xs ([0] :: nat list)}" |
|
1122 |
|
1123 values [dseq 5] 3 |
|
1124 "{xs. concatP xs ([1] :: int list)}" |
|
1125 |
|
1126 values [dseq 5] 3 |
|
1127 "{xs. concatP xs ([1] :: nat list)}" |
|
1128 |
|
1129 values [dseq 5] 3 |
|
1130 "{xs. concatP xs [(1::int), 2]}" |
|
1131 |
|
1132 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd . |
|
1133 thm hdP.equation |
|
1134 values "{x. hdP [1, 2, (3::int)] x}" |
|
1135 values "{(xs, x). hdP [1, 2, (3::int)] 1}" |
|
1136 |
|
1137 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl . |
|
1138 thm tlP.equation |
|
1139 values "{x. tlP [1, 2, (3::nat)] x}" |
|
1140 values "{x. tlP [1, 2, (3::int)] [3]}" |
|
1141 |
|
1142 code_pred [inductify, skip_proof] last . |
|
1143 thm lastP.equation |
|
1144 |
|
1145 code_pred [inductify, skip_proof] butlast . |
|
1146 thm butlastP.equation |
|
1147 |
|
1148 code_pred [inductify, skip_proof] take . |
|
1149 thm takeP.equation |
|
1150 |
|
1151 code_pred [inductify, skip_proof] drop . |
|
1152 thm dropP.equation |
|
1153 code_pred [inductify, skip_proof] zip . |
|
1154 thm zipP.equation |
|
1155 |
|
1156 code_pred [inductify, skip_proof] upt . |
|
1157 code_pred [inductify, skip_proof] remdups . |
|
1158 thm remdupsP.equation |
|
1159 code_pred [dseq inductify] remdups . |
|
1160 values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}" |
|
1161 |
|
1162 code_pred [inductify, skip_proof] remove1 . |
|
1163 thm remove1P.equation |
|
1164 values "{xs. remove1P 1 xs [2, (3::int)]}" |
|
1165 |
|
1166 code_pred [inductify, skip_proof] removeAll . |
|
1167 thm removeAllP.equation |
|
1168 code_pred [dseq inductify] removeAll . |
|
1169 |
|
1170 values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}" |
|
1171 |
|
1172 code_pred [inductify] distinct . |
|
1173 thm distinct.equation |
|
1174 code_pred [inductify, skip_proof] replicate . |
|
1175 thm replicateP.equation |
|
1176 values 5 "{(n, xs). replicateP n (0::int) xs}" |
|
1177 |
|
1178 code_pred [inductify, skip_proof] splice . |
|
1179 thm splice.simps |
|
1180 thm spliceP.equation |
|
1181 |
|
1182 values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}" |
|
1183 |
|
1184 code_pred [inductify, skip_proof] List.rev . |
|
1185 code_pred [inductify] map . |
|
1186 code_pred [inductify] foldr . |
|
1187 code_pred [inductify] foldl . |
|
1188 code_pred [inductify] filter . |
|
1189 code_pred [random_dseq inductify] filter . |
|
1190 |
|
1191 subsection {* Context Free Grammar *} |
|
1192 |
|
1193 datatype alphabet = a | b |
|
1194 |
|
1195 inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where |
|
1196 "[] \<in> S\<^isub>1" |
|
1197 | "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" |
|
1198 | "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1" |
|
1199 | "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1" |
|
1200 | "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" |
|
1201 | "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1" |
|
1202 |
|
1203 code_pred [inductify] S\<^isub>1p . |
|
1204 code_pred [random_dseq inductify] S\<^isub>1p . |
|
1205 thm S\<^isub>1p.equation |
|
1206 thm S\<^isub>1p.random_dseq_equation |
|
1207 |
|
1208 values [random_dseq 5, 5, 5] 5 "{x. S\<^isub>1p x}" |
|
1209 |
|
1210 inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where |
|
1211 "[] \<in> S\<^isub>2" |
|
1212 | "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2" |
|
1213 | "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2" |
|
1214 | "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2" |
|
1215 | "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2" |
|
1216 | "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2" |
|
1217 |
|
1218 code_pred [random_dseq inductify] S\<^isub>2p . |
|
1219 thm S\<^isub>2p.random_dseq_equation |
|
1220 thm A\<^isub>2p.random_dseq_equation |
|
1221 thm B\<^isub>2p.random_dseq_equation |
|
1222 |
|
1223 values [random_dseq 5, 5, 5] 10 "{x. S\<^isub>2p x}" |
|
1224 |
|
1225 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where |
|
1226 "[] \<in> S\<^isub>3" |
|
1227 | "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3" |
|
1228 | "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3" |
|
1229 | "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3" |
|
1230 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3" |
|
1231 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3" |
|
1232 |
|
1233 code_pred [inductify, skip_proof] S\<^isub>3p . |
|
1234 thm S\<^isub>3p.equation |
|
1235 |
|
1236 values 10 "{x. S\<^isub>3p x}" |
|
1237 |
|
1238 inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where |
|
1239 "[] \<in> S\<^isub>4" |
|
1240 | "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4" |
|
1241 | "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4" |
|
1242 | "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4" |
|
1243 | "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4" |
|
1244 | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4" |
|
1245 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4" |
|
1246 |
|
1247 code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p . |
|
1248 |
|
1249 hide_const a b |
|
1250 |
|
1251 subsection {* Lambda *} |
|
1252 |
|
1253 datatype type = |
|
1254 Atom nat |
|
1255 | Fun type type (infixr "\<Rightarrow>" 200) |
|
1256 |
|
1257 datatype dB = |
|
1258 Var nat |
|
1259 | App dB dB (infixl "\<degree>" 200) |
|
1260 | Abs type dB |
|
1261 |
|
1262 primrec |
|
1263 nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91) |
|
1264 where |
|
1265 "[]\<langle>i\<rangle> = None" |
|
1266 | "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)" |
|
1267 |
|
1268 inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool" |
|
1269 where |
|
1270 "nth_el' (x # xs) 0 x" |
|
1271 | "nth_el' xs i y \<Longrightarrow> nth_el' (x # xs) (Suc i) y" |
|
1272 |
|
1273 inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50) |
|
1274 where |
|
1275 Var [intro!]: "nth_el' env x T \<Longrightarrow> env \<turnstile> Var x : T" |
|
1276 | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)" |
|
1277 | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U" |
|
1278 |
|
1279 primrec |
|
1280 lift :: "[dB, nat] => dB" |
|
1281 where |
|
1282 "lift (Var i) k = (if i < k then Var i else Var (i + 1))" |
|
1283 | "lift (s \<degree> t) k = lift s k \<degree> lift t k" |
|
1284 | "lift (Abs T s) k = Abs T (lift s (k + 1))" |
|
1285 |
|
1286 primrec |
|
1287 subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300) |
|
1288 where |
|
1289 subst_Var: "(Var i)[s/k] = |
|
1290 (if k < i then Var (i - 1) else if i = k then s else Var i)" |
|
1291 | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]" |
|
1292 | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])" |
|
1293 |
|
1294 inductive beta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50) |
|
1295 where |
|
1296 beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]" |
|
1297 | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u" |
|
1298 | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t" |
|
1299 | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t" |
|
1300 |
|
1301 code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing . |
|
1302 thm typing.equation |
|
1303 |
|
1304 code_pred (modes: i => i => bool, i => o => bool as reduce') beta . |
|
1305 thm beta.equation |
|
1306 |
|
1307 values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}" |
|
1308 |
|
1309 definition "reduce t = Predicate.the (reduce' t)" |
|
1310 |
|
1311 value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))" |
|
1312 |
|
1313 code_pred [dseq] typing . |
|
1314 code_pred [random_dseq] typing . |
|
1315 |
|
1316 values [random_dseq 1,1,5] 10 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}" |
|
1317 |
|
1318 subsection {* A minimal example of yet another semantics *} |
|
1319 |
|
1320 text {* thanks to Elke Salecker *} |
|
1321 |
|
1322 types |
|
1323 vname = nat |
|
1324 vvalue = int |
|
1325 var_assign = "vname \<Rightarrow> vvalue" --"variable assignment" |
|
1326 |
|
1327 datatype ir_expr = |
|
1328 IrConst vvalue |
|
1329 | ObjAddr vname |
|
1330 | Add ir_expr ir_expr |
|
1331 |
|
1332 datatype val = |
|
1333 IntVal vvalue |
|
1334 |
|
1335 record configuration = |
|
1336 Env :: var_assign |
|
1337 |
|
1338 inductive eval_var :: |
|
1339 "ir_expr \<Rightarrow> configuration \<Rightarrow> val \<Rightarrow> bool" |
|
1340 where |
|
1341 irconst: "eval_var (IrConst i) conf (IntVal i)" |
|
1342 | objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)" |
|
1343 | plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))" |
|
1344 |
|
1345 |
|
1346 code_pred eval_var . |
|
1347 thm eval_var.equation |
|
1348 |
|
1349 values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}" |
|
1350 |
|
1351 section {* Function predicate replacement *} |
|
1352 |
|
1353 text {* |
|
1354 If the mode analysis uses the functional mode, we |
|
1355 replace predicates that resulted from functions again by their functions. |
|
1356 *} |
|
1357 |
|
1358 inductive test_append |
|
1359 where |
|
1360 "List.append xs ys = zs ==> test_append xs ys zs" |
|
1361 |
|
1362 code_pred [inductify, skip_proof] test_append . |
|
1363 thm test_append.equation |
|
1364 |
|
1365 text {* If append is not turned into a predicate, then the mode |
|
1366 o => o => i => bool could not be inferred. *} |
|
1367 |
|
1368 values 4 "{(xs::int list, ys). test_append xs ys [1, 2, 3, 4]}" |
|
1369 |
|
1370 text {* If appendP is not reverted back to a function, then mode i => i => o => bool |
|
1371 fails after deleting the predicate equation. *} |
|
1372 |
|
1373 declare appendP.equation[code del] |
|
1374 |
|
1375 values "{xs::int list. test_append [1,2] [3,4] xs}" |
|
1376 values "{xs::int list. test_append (replicate 1000 1) (replicate 1000 2) xs}" |
|
1377 values "{xs::int list. test_append (replicate 2000 1) (replicate 2000 2) xs}" |
|
1378 |
|
1379 text {* Redeclaring append.equation as code equation *} |
|
1380 |
|
1381 declare appendP.equation[code] |
|
1382 |
|
1383 subsection {* Function with tuples *} |
|
1384 |
|
1385 fun append' |
|
1386 where |
|
1387 "append' ([], ys) = ys" |
|
1388 | "append' (x # xs, ys) = x # append' (xs, ys)" |
|
1389 |
|
1390 inductive test_append' |
|
1391 where |
|
1392 "append' (xs, ys) = zs ==> test_append' xs ys zs" |
|
1393 |
|
1394 code_pred [inductify, skip_proof] test_append' . |
|
1395 |
|
1396 thm test_append'.equation |
|
1397 |
|
1398 values "{(xs::int list, ys). test_append' xs ys [1, 2, 3, 4]}" |
|
1399 |
|
1400 declare append'P.equation[code del] |
|
1401 |
|
1402 values "{zs :: int list. test_append' [1,2,3] [4,5] zs}" |
|
1403 |
|
1404 section {* Arithmetic examples *} |
|
1405 |
|
1406 subsection {* Examples on nat *} |
|
1407 |
|
1408 inductive plus_nat_test :: "nat => nat => nat => bool" |
|
1409 where |
|
1410 "x + y = z ==> plus_nat_test x y z" |
|
1411 |
|
1412 code_pred [inductify, skip_proof] plus_nat_test . |
|
1413 code_pred [new_random_dseq inductify] plus_nat_test . |
|
1414 |
|
1415 thm plus_nat_test.equation |
|
1416 thm plus_nat_test.new_random_dseq_equation |
|
1417 |
|
1418 values [expected "{9::nat}"] "{z. plus_nat_test 4 5 z}" |
|
1419 values [expected "{9::nat}"] "{z. plus_nat_test 7 2 z}" |
|
1420 values [expected "{4::nat}"] "{y. plus_nat_test 5 y 9}" |
|
1421 values [expected "{}"] "{y. plus_nat_test 9 y 8}" |
|
1422 values [expected "{6::nat}"] "{y. plus_nat_test 1 y 7}" |
|
1423 values [expected "{2::nat}"] "{x. plus_nat_test x 7 9}" |
|
1424 values [expected "{}"] "{x. plus_nat_test x 9 7}" |
|
1425 values [expected "{(0::nat,0::nat)}"] "{(x, y). plus_nat_test x y 0}" |
|
1426 values [expected "{(0, Suc 0), (Suc 0, 0)}"] "{(x, y). plus_nat_test x y 1}" |
|
1427 values [expected "{(0, 5), (4, Suc 0), (3, 2), (2, 3), (Suc 0, 4), (5, 0)}"] |
|
1428 "{(x, y). plus_nat_test x y 5}" |
|
1429 |
|
1430 inductive minus_nat_test :: "nat => nat => nat => bool" |
|
1431 where |
|
1432 "x - y = z ==> minus_nat_test x y z" |
|
1433 |
|
1434 code_pred [inductify, skip_proof] minus_nat_test . |
|
1435 code_pred [new_random_dseq inductify] minus_nat_test . |
|
1436 |
|
1437 thm minus_nat_test.equation |
|
1438 thm minus_nat_test.new_random_dseq_equation |
|
1439 |
|
1440 values [expected "{0::nat}"] "{z. minus_nat_test 4 5 z}" |
|
1441 values [expected "{5::nat}"] "{z. minus_nat_test 7 2 z}" |
|
1442 values [expected "{16::nat}"] "{x. minus_nat_test x 7 9}" |
|
1443 values [expected "{16::nat}"] "{x. minus_nat_test x 9 7}" |
|
1444 values [expected "{0, Suc 0, 2, 3}"] "{x. minus_nat_test x 3 0}" |
|
1445 values [expected "{0::nat}"] "{x. minus_nat_test x 0 0}" |
|
1446 |
|
1447 subsection {* Examples on int *} |
|
1448 |
|
1449 inductive plus_int_test :: "int => int => int => bool" |
|
1450 where |
|
1451 "a + b = c ==> plus_int_test a b c" |
|
1452 |
|
1453 code_pred [inductify, skip_proof] plus_int_test . |
|
1454 code_pred [new_random_dseq inductify] plus_int_test . |
|
1455 |
|
1456 thm plus_int_test.equation |
|
1457 thm plus_int_test.new_random_dseq_equation |
|
1458 |
|
1459 values [expected "{1::int}"] "{a. plus_int_test a 6 7}" |
|
1460 values [expected "{1::int}"] "{b. plus_int_test 6 b 7}" |
|
1461 values [expected "{11::int}"] "{c. plus_int_test 5 6 c}" |
|
1462 |
|
1463 inductive minus_int_test :: "int => int => int => bool" |
|
1464 where |
|
1465 "a - b = c ==> minus_int_test a b c" |
|
1466 |
|
1467 code_pred [inductify, skip_proof] minus_int_test . |
|
1468 code_pred [new_random_dseq inductify] minus_int_test . |
|
1469 |
|
1470 thm minus_int_test.equation |
|
1471 thm minus_int_test.new_random_dseq_equation |
|
1472 |
|
1473 values [expected "{4::int}"] "{c. minus_int_test 9 5 c}" |
|
1474 values [expected "{9::int}"] "{a. minus_int_test a 4 5}" |
|
1475 values [expected "{- 1::int}"] "{b. minus_int_test 4 b 5}" |
|
1476 |
|
1477 subsection {* minus on bool *} |
|
1478 |
|
1479 inductive All :: "nat => bool" |
|
1480 where |
|
1481 "All x" |
|
1482 |
|
1483 inductive None :: "nat => bool" |
|
1484 |
|
1485 definition "test_minus_bool x = (None x - All x)" |
|
1486 |
|
1487 code_pred [inductify] test_minus_bool . |
|
1488 thm test_minus_bool.equation |
|
1489 |
|
1490 values "{x. test_minus_bool x}" |
|
1491 |
|
1492 subsection {* Functions *} |
|
1493 |
|
1494 fun partial_hd :: "'a list => 'a option" |
|
1495 where |
|
1496 "partial_hd [] = Option.None" |
|
1497 | "partial_hd (x # xs) = Some x" |
|
1498 |
|
1499 inductive hd_predicate |
|
1500 where |
|
1501 "partial_hd xs = Some x ==> hd_predicate xs x" |
|
1502 |
|
1503 code_pred (expected_modes: i => i => bool, i => o => bool) hd_predicate . |
|
1504 |
|
1505 thm hd_predicate.equation |
|
1506 |
|
1507 subsection {* Locales *} |
|
1508 |
|
1509 inductive hd_predicate2 :: "('a list => 'a option) => 'a list => 'a => bool" |
|
1510 where |
|
1511 "partial_hd' xs = Some x ==> hd_predicate2 partial_hd' xs x" |
|
1512 |
|
1513 |
|
1514 thm hd_predicate2.intros |
|
1515 |
|
1516 code_pred (expected_modes: i => i => i => bool, i => i => o => bool) hd_predicate2 . |
|
1517 thm hd_predicate2.equation |
|
1518 |
|
1519 locale A = fixes partial_hd :: "'a list => 'a option" begin |
|
1520 |
|
1521 inductive hd_predicate_in_locale :: "'a list => 'a => bool" |
|
1522 where |
|
1523 "partial_hd xs = Some x ==> hd_predicate_in_locale xs x" |
|
1524 |
|
1525 end |
|
1526 |
|
1527 text {* The global introduction rules must be redeclared as introduction rules and then |
|
1528 one could invoke code_pred. *} |
|
1529 |
|
1530 declare A.hd_predicate_in_locale.intros [unfolded Predicate.eq_is_eq[symmetric], code_pred_intro] |
|
1531 |
|
1532 code_pred (expected_modes: i => i => i => bool, i => i => o => bool) A.hd_predicate_in_locale |
|
1533 unfolding eq_is_eq by (auto elim: A.hd_predicate_in_locale.cases) |
|
1534 |
|
1535 interpretation A partial_hd . |
|
1536 thm hd_predicate_in_locale.intros |
|
1537 text {* A locally compliant solution with a trivial interpretation fails, because |
|
1538 the predicate compiler has very strict assumptions about the terms and their structure. *} |
|
1539 |
|
1540 (*code_pred hd_predicate_in_locale .*) |
|
1541 |
|
1542 section {* Integer example *} |
|
1543 |
|
1544 definition three :: int |
|
1545 where "three = 3" |
|
1546 |
|
1547 inductive is_three |
|
1548 where |
|
1549 "is_three three" |
|
1550 |
|
1551 code_pred is_three . |
|
1552 |
|
1553 thm is_three.equation |
|
1554 |
|
1555 section {* String.literal example *} |
|
1556 |
|
1557 definition Error_1 |
|
1558 where |
|
1559 "Error_1 = STR ''Error 1''" |
|
1560 |
|
1561 definition Error_2 |
|
1562 where |
|
1563 "Error_2 = STR ''Error 2''" |
|
1564 |
|
1565 inductive "is_error" :: "String.literal \<Rightarrow> bool" |
|
1566 where |
|
1567 "is_error Error_1" |
|
1568 | "is_error Error_2" |
|
1569 |
|
1570 code_pred is_error . |
|
1571 |
|
1572 thm is_error.equation |
|
1573 |
|
1574 inductive is_error' :: "String.literal \<Rightarrow> bool" |
|
1575 where |
|
1576 "is_error' (STR ''Error1'')" |
|
1577 | "is_error' (STR ''Error2'')" |
|
1578 |
|
1579 code_pred is_error' . |
|
1580 |
|
1581 thm is_error'.equation |
|
1582 |
|
1583 datatype ErrorObject = Error String.literal int |
|
1584 |
|
1585 inductive is_error'' :: "ErrorObject \<Rightarrow> bool" |
|
1586 where |
|
1587 "is_error'' (Error Error_1 3)" |
|
1588 | "is_error'' (Error Error_2 4)" |
|
1589 |
|
1590 code_pred is_error'' . |
|
1591 |
|
1592 thm is_error''.equation |
|
1593 |
|
1594 section {* Another function example *} |
|
1595 |
|
1596 consts f :: "'a \<Rightarrow> 'a" |
|
1597 |
|
1598 inductive fun_upd :: "(('a * 'b) * ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" |
|
1599 where |
|
1600 "fun_upd ((x, a), s) (s(x := f a))" |
|
1601 |
|
1602 code_pred fun_upd . |
|
1603 |
|
1604 thm fun_upd.equation |
|
1605 |
|
1606 section {* Another semantics *} |
|
1607 |
|
1608 types |
|
1609 name = nat --"For simplicity in examples" |
|
1610 state' = "name \<Rightarrow> nat" |
|
1611 |
|
1612 datatype aexp = N nat | V name | Plus aexp aexp |
|
1613 |
|
1614 fun aval :: "aexp \<Rightarrow> state' \<Rightarrow> nat" where |
|
1615 "aval (N n) _ = n" | |
|
1616 "aval (V x) st = st x" | |
|
1617 "aval (Plus e\<^isub>1 e\<^isub>2) st = aval e\<^isub>1 st + aval e\<^isub>2 st" |
|
1618 |
|
1619 datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp |
|
1620 |
|
1621 primrec bval :: "bexp \<Rightarrow> state' \<Rightarrow> bool" where |
|
1622 "bval (B b) _ = b" | |
|
1623 "bval (Not b) st = (\<not> bval b st)" | |
|
1624 "bval (And b1 b2) st = (bval b1 st \<and> bval b2 st)" | |
|
1625 "bval (Less a\<^isub>1 a\<^isub>2) st = (aval a\<^isub>1 st < aval a\<^isub>2 st)" |
|
1626 |
|
1627 datatype |
|
1628 com' = SKIP |
|
1629 | Assign name aexp ("_ ::= _" [1000, 61] 61) |
|
1630 | Semi com' com' ("_; _" [60, 61] 60) |
|
1631 | If bexp com' com' ("IF _ THEN _ ELSE _" [0, 0, 61] 61) |
|
1632 | While bexp com' ("WHILE _ DO _" [0, 61] 61) |
|
1633 |
|
1634 inductive |
|
1635 big_step :: "com' * state' \<Rightarrow> state' \<Rightarrow> bool" (infix "\<Rightarrow>" 55) |
|
1636 where |
|
1637 Skip: "(SKIP,s) \<Rightarrow> s" |
|
1638 | Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
|
1639 |
|
1640 | Semi: "(c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2 \<Longrightarrow> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<Longrightarrow> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
|
1641 |
|
1642 | IfTrue: "bval b s \<Longrightarrow> (c\<^isub>1,s) \<Rightarrow> t \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
|
1643 | IfFalse: "\<not>bval b s \<Longrightarrow> (c\<^isub>2,s) \<Rightarrow> t \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
|
1644 |
|
1645 | WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
|
1646 | WhileTrue: "bval b s\<^isub>1 \<Longrightarrow> (c,s\<^isub>1) \<Rightarrow> s\<^isub>2 \<Longrightarrow> (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 |
|
1647 \<Longrightarrow> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
|
1648 |
|
1649 code_pred big_step . |
|
1650 |
|
1651 thm big_step.equation |
|
1652 |
|
1653 section {* General Context Free Grammars *} |
|
1654 text {* a contribution by Aditi Barthwal *} |
|
1655 |
|
1656 datatype ('nts,'ts) symbol = NTS 'nts |
|
1657 | TS 'ts |
|
1658 |
|
1659 |
|
1660 datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list" |
|
1661 |
|
1662 types ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts" |
|
1663 |
|
1664 fun rules :: "('nts,'ts) grammar => ('nts,'ts) rule set" |
|
1665 where |
|
1666 "rules (r, s) = r" |
|
1667 |
|
1668 definition derives |
|
1669 where |
|
1670 "derives g = { (lsl,rsl). \<exists>s1 s2 lhs rhs. |
|
1671 (s1 @ [NTS lhs] @ s2 = lsl) \<and> |
|
1672 (s1 @ rhs @ s2) = rsl \<and> |
|
1673 (rule lhs rhs) \<in> fst g }" |
|
1674 |
|
1675 abbreviation "example_grammar == |
|
1676 ({ rule ''S'' [NTS ''A'', NTS ''B''], |
|
1677 rule ''S'' [TS ''a''], |
|
1678 rule ''A'' [TS ''b'']}, ''S'')" |
|
1679 |
|
1680 |
|
1681 code_pred [inductify, skip_proof] derives . |
|
1682 |
|
1683 thm derives.equation |
|
1684 |
|
1685 definition "test = { rhs. derives example_grammar ([NTS ''S''], rhs) }" |
|
1686 |
|
1687 code_pred (modes: o \<Rightarrow> bool) [inductify] test . |
|
1688 thm test.equation |
|
1689 |
|
1690 values "{rhs. test rhs}" |
|
1691 |
|
1692 declare rtrancl.intros(1)[code_pred_def] converse_rtrancl_into_rtrancl[code_pred_def] |
|
1693 |
|
1694 code_pred [inductify] rtrancl . |
|
1695 |
|
1696 definition "test2 = { rhs. ([NTS ''S''],rhs) \<in> (derives example_grammar)^* }" |
|
1697 |
|
1698 code_pred [inductify, skip_proof] test2 . |
|
1699 |
|
1700 values "{rhs. test2 rhs}" |
|
1701 |
|
1702 |
|
1703 section {* Examples for detecting switches *} |
|
1704 |
|
1705 inductive detect_switches1 where |
|
1706 "detect_switches1 [] []" |
|
1707 | "detect_switches1 (x # xs) (y # ys)" |
|
1708 |
|
1709 code_pred [detect_switches, skip_proof] detect_switches1 . |
|
1710 |
|
1711 thm detect_switches1.equation |
|
1712 |
|
1713 inductive detect_switches2 :: "('a => bool) => bool" |
|
1714 where |
|
1715 "detect_switches2 P" |
|
1716 |
|
1717 code_pred [detect_switches, skip_proof] detect_switches2 . |
|
1718 thm detect_switches2.equation |
|
1719 |
|
1720 inductive detect_switches3 :: "('a => bool) => 'a list => bool" |
|
1721 where |
|
1722 "detect_switches3 P []" |
|
1723 | "detect_switches3 P (x # xs)" |
|
1724 |
|
1725 code_pred [detect_switches, skip_proof] detect_switches3 . |
|
1726 |
|
1727 thm detect_switches3.equation |
|
1728 |
|
1729 inductive detect_switches4 :: "('a => bool) => 'a list => 'a list => bool" |
|
1730 where |
|
1731 "detect_switches4 P [] []" |
|
1732 | "detect_switches4 P (x # xs) (y # ys)" |
|
1733 |
|
1734 code_pred [detect_switches, skip_proof] detect_switches4 . |
|
1735 thm detect_switches4.equation |
|
1736 |
|
1737 inductive detect_switches5 :: "('a => 'a => bool) => 'a list => 'a list => bool" |
|
1738 where |
|
1739 "detect_switches5 P [] []" |
|
1740 | "detect_switches5 P xs ys ==> P x y ==> detect_switches5 P (x # xs) (y # ys)" |
|
1741 |
|
1742 code_pred [detect_switches, skip_proof] detect_switches5 . |
|
1743 |
|
1744 thm detect_switches5.equation |
|
1745 |
|
1746 inductive detect_switches6 :: "(('a => 'b => bool) * 'a list * 'b list) => bool" |
|
1747 where |
|
1748 "detect_switches6 (P, [], [])" |
|
1749 | "detect_switches6 (P, xs, ys) ==> P x y ==> detect_switches6 (P, x # xs, y # ys)" |
|
1750 |
|
1751 code_pred [detect_switches, skip_proof] detect_switches6 . |
|
1752 |
|
1753 inductive detect_switches7 :: "('a => bool) => ('b => bool) => ('a * 'b list) => bool" |
|
1754 where |
|
1755 "detect_switches7 P Q (a, [])" |
|
1756 | "P a ==> Q x ==> detect_switches7 P Q (a, x#xs)" |
|
1757 |
|
1758 code_pred [skip_proof] detect_switches7 . |
|
1759 |
|
1760 thm detect_switches7.equation |
|
1761 |
|
1762 inductive detect_switches8 :: "nat => bool" |
|
1763 where |
|
1764 "detect_switches8 0" |
|
1765 | "x mod 2 = 0 ==> detect_switches8 (Suc x)" |
|
1766 |
|
1767 code_pred [detect_switches, skip_proof] detect_switches8 . |
|
1768 |
|
1769 thm detect_switches8.equation |
|
1770 |
|
1771 inductive detect_switches9 :: "nat => nat => bool" |
|
1772 where |
|
1773 "detect_switches9 0 0" |
|
1774 | "detect_switches9 0 (Suc x)" |
|
1775 | "detect_switches9 (Suc x) 0" |
|
1776 | "x = y ==> detect_switches9 (Suc x) (Suc y)" |
|
1777 | "c1 = c2 ==> detect_switches9 c1 c2" |
|
1778 |
|
1779 code_pred [detect_switches, skip_proof] detect_switches9 . |
|
1780 |
|
1781 thm detect_switches9.equation |
|
1782 |
|
1783 |
|
1784 |
|
1785 end |
|