src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
 author Lukas Bulwahn Sun Jan 10 20:21:30 2016 +0100 (2016-01-10) changeset 62121 c8a93680b80d parent 60565 b7ee41f72add child 63167 0909deb8059b permissions -rw-r--r--
filter non-matching prems rather than fail in proof procedure in rare cases; include derived example motivating change and some similar other ones
1 theory Predicate_Compile_Tests
2 imports "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
3 begin
5 declare [[values_timeout = 480.0]]
7 subsection {* Basic predicates *}
9 inductive False' :: "bool"
11 code_pred (expected_modes: bool) False' .
12 code_pred [dseq] False' .
13 code_pred [random_dseq] False' .
15 values [expected "{}" pred] "{x. False'}"
16 values [expected "{}" dseq 1] "{x. False'}"
17 values [expected "{}" random_dseq 1, 1, 1] "{x. False'}"
19 value "False'"
21 inductive True' :: "bool"
22 where
23   "True ==> True'"
25 code_pred True' .
26 code_pred [dseq] True' .
27 code_pred [random_dseq] True' .
29 thm True'.equation
30 thm True'.dseq_equation
31 thm True'.random_dseq_equation
32 values [expected "{()}"] "{x. True'}"
33 values [expected "{}" dseq 0] "{x. True'}"
34 values [expected "{()}" dseq 1] "{x. True'}"
35 values [expected "{()}" dseq 2] "{x. True'}"
36 values [expected "{}" random_dseq 1, 1, 0] "{x. True'}"
37 values [expected "{}" random_dseq 1, 1, 1] "{x. True'}"
38 values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}"
39 values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}"
41 inductive EmptyPred :: "'a \<Rightarrow> bool"
43 code_pred (expected_modes: o => bool, i => bool) EmptyPred .
45 definition EmptyPred' :: "'a \<Rightarrow> bool"
46 where "EmptyPred' = (\<lambda> x. False)"
48 code_pred (expected_modes: o => bool, i => bool) [inductify] EmptyPred' .
50 inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
52 code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel .
54 inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
55 for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
57 code_pred
58   (expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool,
59          (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool,
60          (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool,
61          (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool,
62          (o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool,
63          (o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool,
64          (i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool,
65          (i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool)
66   EmptyClosure .
68 thm EmptyClosure.equation
70 (* TODO: inductive package is broken!
71 inductive False'' :: "bool"
72 where
73   "False \<Longrightarrow> False''"
75 code_pred (expected_modes: bool) False'' .
77 inductive EmptySet'' :: "'a \<Rightarrow> bool"
78 where
79   "False \<Longrightarrow> EmptySet'' x"
81 code_pred (expected_modes: i => bool, o => bool) [inductify] EmptySet'' .
82 *)
84 consts a' :: 'a
86 inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
87 where
88   "Fact a' a'"
90 code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
92 text {*
93   The following example was derived from an predicate in the CakeML formalisation provided by Lars Hupel.
94 *}
95 inductive predicate_where_argument_is_condition :: "bool \<Rightarrow> bool"
96 where
97   "ck \<Longrightarrow> predicate_where_argument_is_condition ck"
99 code_pred predicate_where_argument_is_condition .
101 text {* Other similar examples of this kind: *}
103 inductive predicate_where_argument_is_in_equation :: "bool \<Rightarrow> bool"
104 where
105   "ck = True \<Longrightarrow> predicate_where_argument_is_in_equation ck"
107 code_pred predicate_where_argument_is_in_equation .
109 inductive predicate_where_argument_is_condition_and_value :: "bool \<Rightarrow> bool"
110 where
111   "predicate_where_argument_is_condition_and_value ck \<Longrightarrow> ck
112      \<Longrightarrow> predicate_where_argument_is_condition_and_value ck"
114 code_pred predicate_where_argument_is_condition_and_value .
116 inductive predicate_where_argument_is_neg_condition :: "bool \<Rightarrow> bool"
117 where
118   "\<not> ck \<Longrightarrow> predicate_where_argument_is_neg_condition ck"
120 code_pred predicate_where_argument_is_neg_condition .
122 inductive predicate_where_argument_is_neg_condition_and_in_equation :: "bool \<Rightarrow> bool"
123 where
124   "\<not> ck \<Longrightarrow> ck = False \<Longrightarrow> predicate_where_argument_is_neg_condition_and_in_equation ck"
126 code_pred predicate_where_argument_is_neg_condition_and_in_equation .
129 inductive zerozero :: "nat * nat => bool"
130 where
131   "zerozero (0, 0)"
133 code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .
134 code_pred [dseq] zerozero .
135 code_pred [random_dseq] zerozero .
137 thm zerozero.equation
138 thm zerozero.dseq_equation
139 thm zerozero.random_dseq_equation
141 text {* We expect the user to expand the tuples in the values command.
142 The following values command is not supported. *}
143 (*values "{x. zerozero x}" *)
144 text {* Instead, the user must type *}
145 values "{(x, y). zerozero (x, y)}"
147 values [expected "{}" dseq 0] "{(x, y). zerozero (x, y)}"
148 values [expected "{(0::nat, 0::nat)}" dseq 1] "{(x, y). zerozero (x, y)}"
149 values [expected "{(0::nat, 0::nat)}" dseq 2] "{(x, y). zerozero (x, y)}"
150 values [expected "{}" random_dseq 1, 1, 2] "{(x, y). zerozero (x, y)}"
151 values [expected "{(0::nat, 0:: nat)}" random_dseq 1, 1, 3] "{(x, y). zerozero (x, y)}"
153 inductive nested_tuples :: "((int * int) * int * int) => bool"
154 where
155   "nested_tuples ((0, 1), 2, 3)"
157 code_pred nested_tuples .
159 inductive JamesBond :: "nat => int => natural => bool"
160 where
161   "JamesBond 0 0 7"
163 code_pred JamesBond .
165 values [expected "{(0::nat, 0::int , 7::natural)}"] "{(a, b, c). JamesBond a b c}"
166 values [expected "{(0::nat, 7::natural, 0:: int)}"] "{(a, c, b). JamesBond a b c}"
167 values [expected "{(0::int, 0::nat, 7::natural)}"] "{(b, a, c). JamesBond a b c}"
168 values [expected "{(0::int, 7::natural, 0::nat)}"] "{(b, c, a). JamesBond a b c}"
169 values [expected "{(7::natural, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}"
170 values [expected "{(7::natural, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}"
172 values [expected "{(7::natural, 0::int)}"] "{(a, b). JamesBond 0 b a}"
173 values [expected "{(7::natural, 0::nat)}"] "{(c, a). JamesBond a 0 c}"
174 values [expected "{(0::nat, 7::natural)}"] "{(a, c). JamesBond a 0 c}"
177 subsection {* Alternative Rules *}
179 datatype char = C | D | E | F | G | H
181 inductive is_C_or_D
182 where
183   "(x = C) \<or> (x = D) ==> is_C_or_D x"
185 code_pred (expected_modes: i => bool) is_C_or_D .
186 thm is_C_or_D.equation
188 inductive is_D_or_E
189 where
190   "(x = D) \<or> (x = E) ==> is_D_or_E x"
192 lemma [code_pred_intro]:
193   "is_D_or_E D"
194 by (auto intro: is_D_or_E.intros)
196 lemma [code_pred_intro]:
197   "is_D_or_E E"
198 by (auto intro: is_D_or_E.intros)
200 code_pred (expected_modes: o => bool, i => bool) is_D_or_E
201 proof -
202   case is_D_or_E
203   from is_D_or_E.prems show thesis
204   proof
205     fix xa
206     assume x: "x = xa"
207     assume "xa = D \<or> xa = E"
208     from this show thesis
209     proof
210       assume "xa = D" from this x is_D_or_E(1) show thesis by simp
211     next
212       assume "xa = E" from this x is_D_or_E(2) show thesis by simp
213     qed
214   qed
215 qed
217 thm is_D_or_E.equation
219 inductive is_F_or_G
220 where
221   "x = F \<or> x = G ==> is_F_or_G x"
223 lemma [code_pred_intro]:
224   "is_F_or_G F"
225 by (auto intro: is_F_or_G.intros)
227 lemma [code_pred_intro]:
228   "is_F_or_G G"
229 by (auto intro: is_F_or_G.intros)
231 inductive is_FGH
232 where
233   "is_F_or_G x ==> is_FGH x"
234 | "is_FGH H"
236 text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}
238 code_pred (expected_modes: o => bool, i => bool) is_FGH
239 proof -
240   case is_F_or_G
241   from is_F_or_G.prems show thesis
242   proof
243     fix xa
244     assume x: "x = xa"
245     assume "xa = F \<or> xa = G"
246     from this show thesis
247     proof
248       assume "xa = F"
249       from this x is_F_or_G(1) show thesis by simp
250     next
251       assume "xa = G"
252       from this x is_F_or_G(2) show thesis by simp
253     qed
254   qed
255 qed
257 subsection {* Named alternative rules *}
259 inductive appending
260 where
261   nil: "appending [] ys ys"
262 | cons: "appending xs ys zs \<Longrightarrow> appending (x#xs) ys (x#zs)"
264 lemma appending_alt_nil: "ys = zs \<Longrightarrow> appending [] ys zs"
265 by (auto intro: appending.intros)
267 lemma appending_alt_cons: "xs' = x # xs \<Longrightarrow> appending xs ys zs \<Longrightarrow> zs' = x # zs \<Longrightarrow> appending xs' ys zs'"
268 by (auto intro: appending.intros)
270 text {* With code_pred_intro, we can give fact names to the alternative rules,
271   which are used for the code_pred command. *}
273 declare appending_alt_nil[code_pred_intro alt_nil] appending_alt_cons[code_pred_intro alt_cons]
275 code_pred appending
276 proof -
277   case appending
278   from appending.prems show thesis
279   proof(cases)
280     case nil
281     from appending.alt_nil nil show thesis by auto
282   next
283     case cons
284     from appending.alt_cons cons show thesis by fastforce
285   qed
286 qed
289 inductive ya_even and ya_odd :: "nat => bool"
290 where
291   even_zero: "ya_even 0"
292 | odd_plus1: "ya_even x ==> ya_odd (x + 1)"
293 | even_plus1: "ya_odd x ==> ya_even (x + 1)"
296 declare even_zero[code_pred_intro even_0]
298 lemma [code_pred_intro odd_Suc]: "ya_even x ==> ya_odd (Suc x)"
299 by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)
301 lemma [code_pred_intro even_Suc]:"ya_odd x ==> ya_even (Suc x)"
302 by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)
304 code_pred ya_even
305 proof -
306   case ya_even
307   from ya_even.prems show thesis
308   proof (cases)
309     case even_zero
310     from even_zero ya_even.even_0 show thesis by simp
311   next
312     case even_plus1
313     from even_plus1 ya_even.even_Suc show thesis by simp
314   qed
315 next
316   case ya_odd
317   from ya_odd.prems show thesis
318   proof (cases)
319     case odd_plus1
320     from odd_plus1 ya_odd.odd_Suc show thesis by simp
321   qed
322 qed
324 subsection {* Preprocessor Inlining  *}
326 definition "equals == (op =)"
328 inductive zerozero' :: "nat * nat => bool" where
329   "equals (x, y) (0, 0) ==> zerozero' (x, y)"
331 code_pred (expected_modes: i => bool) zerozero' .
333 lemma zerozero'_eq: "zerozero' x == zerozero x"
334 proof -
335   have "zerozero' = zerozero"
336     apply (auto simp add: fun_eq_iff)
337     apply (cases rule: zerozero'.cases)
338     apply (auto simp add: equals_def intro: zerozero.intros)
339     apply (cases rule: zerozero.cases)
340     apply (auto simp add: equals_def intro: zerozero'.intros)
341     done
342   from this show "zerozero' x == zerozero x" by auto
343 qed
345 declare zerozero'_eq [code_pred_inline]
347 definition "zerozero'' x == zerozero' x"
349 text {* if preprocessing fails, zerozero'' will not have all modes. *}
351 code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
353 subsection {* Sets *}
354 (*
355 inductive_set EmptySet :: "'a set"
357 code_pred (expected_modes: o => bool, i => bool) EmptySet .
359 definition EmptySet' :: "'a set"
360 where "EmptySet' = {}"
362 code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
363 *)
364 subsection {* Numerals *}
366 definition
367   "one_or_two = (%x. x = Suc 0 \<or> ( x = Suc (Suc 0)))"
369 code_pred [inductify] one_or_two .
371 code_pred [dseq] one_or_two .
372 code_pred [random_dseq] one_or_two .
373 thm one_or_two.dseq_equation
374 values [expected "{Suc 0, Suc (Suc 0)}"] "{x. one_or_two x}"
375 values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
377 inductive one_or_two' :: "nat => bool"
378 where
379   "one_or_two' 1"
380 | "one_or_two' 2"
382 code_pred one_or_two' .
383 thm one_or_two'.equation
385 values "{x. one_or_two' x}"
387 definition one_or_two'':
388   "one_or_two'' == (%x. x = 1 \<or> x = (2::nat))"
390 code_pred [inductify] one_or_two'' .
391 thm one_or_two''.equation
393 values "{x. one_or_two'' x}"
395 subsection {* even predicate *}
397 inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
398     "even 0"
399   | "even n \<Longrightarrow> odd (Suc n)"
400   | "odd n \<Longrightarrow> even (Suc n)"
402 code_pred (expected_modes: i => bool, o => bool) even .
403 code_pred [dseq] even .
404 code_pred [random_dseq] even .
406 thm odd.equation
407 thm even.equation
408 thm odd.dseq_equation
409 thm even.dseq_equation
410 thm odd.random_dseq_equation
411 thm even.random_dseq_equation
413 values "{x. even 2}"
414 values "{x. odd 2}"
415 values 10 "{n. even n}"
416 values 10 "{n. odd n}"
417 values [expected "{}" dseq 2] "{x. even 6}"
418 values [expected "{}" dseq 6] "{x. even 6}"
419 values [expected "{()}" dseq 7] "{x. even 6}"
420 values [dseq 2] "{x. odd 7}"
421 values [dseq 6] "{x. odd 7}"
422 values [dseq 7] "{x. odd 7}"
423 values [expected "{()}" dseq 8] "{x. odd 7}"
425 values [expected "{}" dseq 0] 8 "{x. even x}"
426 values [expected "{0::nat}" dseq 1] 8 "{x. even x}"
427 values [expected "{0, Suc (Suc 0)}" dseq 3] 8 "{x. even x}"
428 values [expected "{0, Suc (Suc 0)}" dseq 4] 8 "{x. even x}"
429 values [expected "{0, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))}" dseq 6] 8 "{x. even x}"
431 values [random_dseq 1, 1, 0] 8 "{x. even x}"
432 values [random_dseq 1, 1, 1] 8 "{x. even x}"
433 values [random_dseq 1, 1, 2] 8 "{x. even x}"
434 values [random_dseq 1, 1, 3] 8 "{x. even x}"
435 values [random_dseq 1, 1, 6] 8 "{x. even x}"
437 values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}"
438 values [random_dseq 1, 1, 8] "{x. odd 7}"
439 values [random_dseq 1, 1, 9] "{x. odd 7}"
441 definition odd' where "odd' x == \<not> even x"
443 code_pred (expected_modes: i => bool) [inductify] odd' .
444 code_pred [dseq inductify] odd' .
445 code_pred [random_dseq inductify] odd' .
447 values [expected "{}" dseq 2] "{x. odd' 7}"
448 values [expected "{()}" dseq 9] "{x. odd' 7}"
449 values [expected "{}" dseq 2] "{x. odd' 8}"
450 values [expected "{}" dseq 10] "{x. odd' 8}"
453 inductive is_even :: "nat \<Rightarrow> bool"
454 where
455   "n mod 2 = 0 \<Longrightarrow> is_even n"
457 code_pred (expected_modes: i => bool) is_even .
459 subsection {* append predicate *}
461 inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
462     "append [] xs xs"
463   | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
465 code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
466   i => o => i => bool as suffix, i => i => i => bool) append .
467 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,
468   i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool) append .
470 code_pred [dseq] append .
471 code_pred [random_dseq] append .
473 thm append.equation
474 thm append.dseq_equation
475 thm append.random_dseq_equation
477 values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
478 values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
479 values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
481 values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
482 values [expected "{(([]::nat list), [Suc 0, Suc (Suc 0), Suc (Suc (Suc 0)), Suc (Suc (Suc (Suc 0))), Suc (Suc (Suc (Suc (Suc 0))))])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
483 values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
484 values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
485 values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
486 values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}"
487 values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
488 values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
489 values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
490 values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
492 value "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
493 value "Predicate.the (slice ([]::int list))"
496 text {* tricky case with alternative rules *}
498 inductive append2
499 where
500   "append2 [] xs xs"
501 | "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
503 lemma append2_Nil: "append2 [] (xs::'b list) xs"
506 lemmas [code_pred_intro] = append2_Nil append2.intros(2)
508 code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,
509   i => o => i => bool, i => i => i => bool) append2
510 proof -
511   case append2
512   from append2.prems show thesis
513   proof
514     fix xs
515     assume "xa = []" "xb = xs" "xc = xs"
516     from this append2(1) show thesis by simp
517   next
518     fix xs ys zs x
519     assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs"
520     from this append2(2) show thesis by fastforce
521   qed
522 qed
524 inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
525 where
526   "tupled_append ([], xs, xs)"
527 | "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
529 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
530   i * o * i => bool, i * i * i => bool) tupled_append .
532 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,
533   i \<times> o \<times> i \<Rightarrow> bool, i \<times> i \<times> i \<Rightarrow> bool) tupled_append .
535 code_pred [random_dseq] tupled_append .
536 thm tupled_append.equation
538 values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}"
540 inductive tupled_append'
541 where
542 "tupled_append' ([], xs, xs)"
543 | "[| ys = fst (xa, y); x # zs = snd (xa, y);
544  tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
546 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
547   i * o * i => bool, i * i * i => bool) tupled_append' .
548 thm tupled_append'.equation
550 inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
551 where
552   "tupled_append'' ([], xs, xs)"
553 | "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
555 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
556   i * o * i => bool, i * i * i => bool) tupled_append'' .
557 thm tupled_append''.equation
559 inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
560 where
561   "tupled_append''' ([], xs, xs)"
562 | "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
564 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
565   i * o * i => bool, i * i * i => bool) tupled_append''' .
566 thm tupled_append'''.equation
568 subsection {* map_ofP predicate *}
570 inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
571 where
572   "map_ofP ((a, b)#xs) a b"
573 | "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
575 code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .
576 thm map_ofP.equation
578 subsection {* filter predicate *}
580 inductive filter1
581 for P
582 where
583   "filter1 P [] []"
584 | "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
585 | "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
587 code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
588 code_pred [dseq] filter1 .
589 code_pred [random_dseq] filter1 .
591 thm filter1.equation
593 values [expected "{[0, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
594 values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
595 values [expected "{[0, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
597 inductive filter2
598 where
599   "filter2 P [] []"
600 | "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"
601 | "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"
603 code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 .
604 code_pred [dseq] filter2 .
605 code_pred [random_dseq] filter2 .
607 thm filter2.equation
608 thm filter2.random_dseq_equation
610 inductive filter3
611 for P
612 where
613   "List.filter P xs = ys ==> filter3 P xs ys"
615 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 .
617 code_pred filter3 .
618 thm filter3.equation
620 (*
621 inductive filter4
622 where
623   "List.filter P xs = ys ==> filter4 P xs ys"
625 code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
626 (*code_pred [depth_limited] filter4 .*)
627 (*code_pred [random] filter4 .*)
628 *)
629 subsection {* reverse predicate *}
631 inductive rev where
632     "rev [] []"
633   | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
635 code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .
637 thm rev.equation
639 values "{xs. rev [0, 1, 2, 3::nat] xs}"
641 inductive tupled_rev where
642   "tupled_rev ([], [])"
643 | "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"
645 code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
646 thm tupled_rev.equation
648 subsection {* partition predicate *}
650 inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
651   for f where
652     "partition f [] [] []"
653   | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
654   | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
656 code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,
657   (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool)
658   partition .
659 code_pred [dseq] partition .
660 code_pred [random_dseq] partition .
662 values 10 "{(ys, zs). partition is_even
663   [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
664 values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
665 values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
667 inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"
668   for f where
669    "tupled_partition f ([], [], [])"
670   | "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
671   | "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"
673 code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,
674   (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition .
676 thm tupled_partition.equation
678 lemma [code_pred_intro]:
679   "r a b \<Longrightarrow> tranclp r a b"
680   "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
681   by auto
683 subsection {* transitive predicate *}
685 text {* Also look at the tabled transitive closure in the Library *}
687 code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
688   (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,
689   (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
690 proof -
691   case tranclp
692   from this converse_tranclpE[OF tranclp.prems] show thesis by metis
693 qed
696 code_pred [dseq] tranclp .
697 code_pred [random_dseq] tranclp .
698 thm tranclp.equation
699 thm tranclp.random_dseq_equation
701 inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool"
702 where
703   "rtrancl' x x r"
704 | "r x y ==> rtrancl' y z r ==> rtrancl' x z r"
706 code_pred [random_dseq] rtrancl' .
708 thm rtrancl'.random_dseq_equation
710 inductive rtrancl'' :: "('a * 'a * ('a \<Rightarrow> 'a \<Rightarrow> bool)) \<Rightarrow> bool"
711 where
712   "rtrancl'' (x, x, r)"
713 | "r x y \<Longrightarrow> rtrancl'' (y, z, r) \<Longrightarrow> rtrancl'' (x, z, r)"
715 code_pred rtrancl'' .
717 inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool"
718 where
719   "rtrancl''' (x, (x, x), r)"
720 | "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)"
722 code_pred rtrancl''' .
725 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
726     "succ 0 1"
727   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
729 code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ .
730 code_pred [random_dseq] succ .
731 thm succ.equation
732 thm succ.random_dseq_equation
734 values 10 "{(m, n). succ n m}"
735 values "{m. succ 0 m}"
736 values "{m. succ m 0}"
738 text {* values command needs mode annotation of the parameter succ
739 to disambiguate which mode is to be chosen. *}
741 values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
742 values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
743 values 20 "{(n, m). tranclp succ n m}"
745 inductive example_graph :: "int => int => bool"
746 where
747   "example_graph 0 1"
748 | "example_graph 1 2"
749 | "example_graph 1 3"
750 | "example_graph 4 7"
751 | "example_graph 4 5"
752 | "example_graph 5 6"
753 | "example_graph 7 6"
754 | "example_graph 7 8"
756 inductive not_reachable_in_example_graph :: "int => int => bool"
757 where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y"
759 code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
761 thm not_reachable_in_example_graph.equation
762 thm tranclp.equation
763 value "not_reachable_in_example_graph 0 3"
764 value "not_reachable_in_example_graph 4 8"
765 value "not_reachable_in_example_graph 5 6"
766 text {* rtrancl compilation is strange! *}
767 (*
768 value "not_reachable_in_example_graph 0 4"
769 value "not_reachable_in_example_graph 1 6"
770 value "not_reachable_in_example_graph 8 4"*)
772 code_pred [dseq] not_reachable_in_example_graph .
774 values [dseq 6] "{x. tranclp example_graph 0 3}"
776 values [dseq 0] "{x. not_reachable_in_example_graph 0 3}"
777 values [dseq 0] "{x. not_reachable_in_example_graph 0 4}"
778 values [dseq 20] "{x. not_reachable_in_example_graph 0 4}"
779 values [dseq 6] "{x. not_reachable_in_example_graph 0 3}"
780 values [dseq 3] "{x. not_reachable_in_example_graph 4 2}"
781 values [dseq 6] "{x. not_reachable_in_example_graph 4 2}"
784 inductive not_reachable_in_example_graph' :: "int => int => bool"
785 where "\<not> (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y"
787 code_pred not_reachable_in_example_graph' .
789 value "not_reachable_in_example_graph' 0 3"
790 (* value "not_reachable_in_example_graph' 0 5" would not terminate *)
793 (*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*)
794 (*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
795 (*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*)
796 (*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
797 (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
798 (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
800 code_pred [dseq] not_reachable_in_example_graph' .
802 (*thm not_reachable_in_example_graph'.dseq_equation*)
804 (*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*)
805 (*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
806 (*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"
807 values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
808 (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
809 (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
811 subsection {* Free function variable *}
813 inductive FF :: "nat => nat => bool"
814 where
815   "f x = y ==> FF x y"
817 code_pred FF .
819 subsection {* IMP *}
821 type_synonym var = nat
822 type_synonym state = "int list"
824 datatype com =
825   Skip |
826   Ass var "state => int" |
827   Seq com com |
828   IF "state => bool" com com |
829   While "state => bool" com
831 inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where
832 "tupled_exec (Skip, s, s)" |
833 "tupled_exec (Ass x e, s, s[x := e(s)])" |
834 "tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" |
835 "b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
836 "~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
837 "~b s ==> tupled_exec (While b c, s, s)" |
838 "b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)"
840 code_pred tupled_exec .
842 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)}"
844 subsection {* CCS *}
846 text{* This example formalizes finite CCS processes without communication or
847 recursion. For simplicity, labels are natural numbers. *}
849 datatype proc = nil | pre nat proc | or proc proc | par proc proc
851 inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
852 where
853 "tupled_step (pre n p, n, p)" |
854 "tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
855 "tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
856 "tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)" |
857 "tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)"
859 code_pred tupled_step .
860 thm tupled_step.equation
862 subsection {* divmod *}
864 inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
865     "k < l \<Longrightarrow> divmod_rel k l 0 k"
866   | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
868 code_pred divmod_rel .
869 thm divmod_rel.equation
870 value "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
872 subsection {* Transforming predicate logic into logic programs *}
874 subsection {* Transforming functions into logic programs *}
875 definition
876   "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
878 code_pred [inductify, skip_proof] case_f .
879 thm case_fP.equation
881 fun fold_map_idx where
882   "fold_map_idx f i y [] = (y, [])"
883 | "fold_map_idx f i y (x # xs) =
884  (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs
885  in (y'', x' # xs'))"
887 code_pred [inductify] fold_map_idx .
889 subsection {* Minimum *}
891 definition Min
892 where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
894 code_pred [inductify] Min .
895 thm Min.equation
897 subsection {* Lexicographic order *}
898 text {* This example requires to handle the differences of sets and predicates in the predicate compiler,
899 or to have a copy of all definitions on predicates due to the set-predicate distinction. *}
901 (*
902 declare lexord_def[code_pred_def]
903 code_pred [inductify] lexord .
904 code_pred [random_dseq inductify] lexord .
906 thm lexord.equation
907 thm lexord.random_dseq_equation
909 inductive less_than_nat :: "nat * nat => bool"
910 where
911   "less_than_nat (0, x)"
912 | "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)"
914 code_pred less_than_nat .
916 code_pred [dseq] less_than_nat .
917 code_pred [random_dseq] less_than_nat .
919 inductive test_lexord :: "nat list * nat list => bool"
920 where
921   "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)"
923 code_pred test_lexord .
924 code_pred [dseq] test_lexord .
925 code_pred [random_dseq] test_lexord .
926 thm test_lexord.dseq_equation
927 thm test_lexord.random_dseq_equation
929 values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
930 (*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*)
932 lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
933 (*
934 code_pred [inductify] lexn .
935 thm lexn.equation
936 *)
937 (*
938 code_pred [random_dseq inductify] lexn .
939 thm lexn.random_dseq_equation
941 values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
942 *)
944 inductive has_length
945 where
946   "has_length [] 0"
947 | "has_length xs i ==> has_length (x # xs) (Suc i)"
949 lemma has_length:
950   "has_length xs n = (length xs = n)"
951 proof (rule iffI)
952   assume "has_length xs n"
953   from this show "length xs = n"
954     by (rule has_length.induct) auto
955 next
956   assume "length xs = n"
957   from this show "has_length xs n"
958     by (induct xs arbitrary: n) (auto intro: has_length.intros)
959 qed
961 lemma lexn_intros [code_pred_intro]:
962   "has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)"
963   "lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)"
964 proof -
965   assume "has_length xs i" "has_length ys i" "r (x, y)"
966   from this has_length show "lexn r (Suc i) (x # xs, y # ys)"
967     unfolding lexn_conv Collect_def mem_def
968     by fastforce
969 next
970   assume "lexn r i (xs, ys)"
971   thm lexn_conv
972   from this show "lexn r (Suc i) (x#xs, x#ys)"
973     unfolding Collect_def mem_def lexn_conv
974     apply auto
975     apply (rule_tac x="x # xys" in exI)
976     by auto
977 qed
979 code_pred [random_dseq] lexn
980 proof -
981   fix r n xs ys
982   assume 1: "lexn r n (xs, ys)"
983   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"
984   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"
985   from 1 2 3 show thesis
986     unfolding lexn_conv Collect_def mem_def
987     apply (auto simp add: has_length)
988     apply (case_tac xys)
989     apply auto
990     apply fastforce
991     apply fastforce done
992 qed
994 values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
996 code_pred [inductify, skip_proof] lex .
997 thm lex.equation
998 thm lex_def
999 declare lenlex_conv[code_pred_def]
1000 code_pred [inductify, skip_proof] lenlex .
1001 thm lenlex.equation
1003 code_pred [random_dseq inductify] lenlex .
1004 thm lenlex.random_dseq_equation
1006 values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"
1008 thm lists.intros
1009 code_pred [inductify] lists .
1010 thm lists.equation
1011 *)
1012 subsection {* AVL Tree *}
1014 datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
1015 fun height :: "'a tree => nat" where
1016 "height ET = 0"
1017 | "height (MKT x l r h) = max (height l) (height r) + 1"
1019 primrec avl :: "'a tree => bool"
1020 where
1021   "avl ET = True"
1022 | "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and>
1023   h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
1024 (*
1025 code_pred [inductify] avl .
1026 thm avl.equation*)
1028 code_pred [new_random_dseq inductify] avl .
1029 thm avl.new_random_dseq_equation
1030 (* TODO: has highly non-deterministic execution time!
1032 values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
1033 *)
1034 fun set_of
1035 where
1036 "set_of ET = {}"
1037 | "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
1039 fun is_ord :: "nat tree => bool"
1040 where
1041 "is_ord ET = True"
1042 | "is_ord (MKT n l r h) =
1043  ((\<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)"
1045 (*
1046 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
1047 thm set_of.equation
1049 code_pred (expected_modes: i => bool) [inductify] is_ord .
1050 thm is_ord_aux.equation
1051 thm is_ord.equation
1052 *)
1053 subsection {* Definitions about Relations *}
1054 (*
1055 code_pred (modes:
1056   (i * i => bool) => i * i => bool,
1057   (i * o => bool) => o * i => bool,
1058   (i * o => bool) => i * i => bool,
1059   (o * i => bool) => i * o => bool,
1060   (o * i => bool) => i * i => bool,
1061   (o * o => bool) => o * o => bool,
1062   (o * o => bool) => i * o => bool,
1063   (o * o => bool) => o * i => bool,
1064   (o * o => bool) => i * i => bool) [inductify] converse .
1066 thm converse.equation
1067 code_pred [inductify] relcomp .
1068 thm relcomp.equation
1069 code_pred [inductify] Image .
1070 thm Image.equation
1071 declare singleton_iff[code_pred_inline]
1072 declare Id_on_def[unfolded Bex_def UNION_eq singleton_iff, code_pred_def]
1074 code_pred (expected_modes:
1075   (o => bool) => o => bool,
1076   (o => bool) => i * o => bool,
1077   (o => bool) => o * i => bool,
1078   (o => bool) => i => bool,
1079   (i => bool) => i * o => bool,
1080   (i => bool) => o * i => bool,
1081   (i => bool) => i => bool) [inductify] Id_on .
1082 thm Id_on.equation
1083 thm Domain_unfold
1084 code_pred (modes:
1085   (o * o => bool) => o => bool,
1086   (o * o => bool) => i => bool,
1087   (i * o => bool) => i => bool) [inductify] Domain .
1088 thm Domain.equation
1090 thm Domain_converse [symmetric]
1091 code_pred (modes:
1092   (o * o => bool) => o => bool,
1093   (o * o => bool) => i => bool,
1094   (o * i => bool) => i => bool) [inductify] Range .
1095 thm Range.equation
1097 code_pred [inductify] Field .
1098 thm Field.equation
1100 thm refl_on_def
1101 code_pred [inductify] refl_on .
1102 thm refl_on.equation
1103 code_pred [inductify] total_on .
1104 thm total_on.equation
1105 code_pred [inductify] antisym .
1106 thm antisym.equation
1107 code_pred [inductify] trans .
1108 thm trans.equation
1109 code_pred [inductify] single_valued .
1110 thm single_valued.equation
1111 thm inv_image_def
1112 code_pred [inductify] inv_image .
1113 thm inv_image.equation
1114 *)
1115 subsection {* Inverting list functions *}
1117 code_pred [inductify, skip_proof] size_list' .
1118 code_pred [new_random_dseq inductify] size_list' .
1119 thm size_list'P.equation
1120 thm size_list'P.new_random_dseq_equation
1122 values [new_random_dseq 2,3,10] 3 "{xs. size_list'P (xs::nat list) (5::nat)}"
1124 code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
1125 thm concatP.equation
1127 values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
1128 values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
1130 code_pred [dseq inductify] List.concat .
1131 thm concatP.dseq_equation
1133 values [dseq 3] 3
1134   "{xs. concatP xs ([0] :: nat list)}"
1136 values [dseq 5] 3
1137   "{xs. concatP xs ([1] :: int list)}"
1139 values [dseq 5] 3
1140   "{xs. concatP xs ([1] :: nat list)}"
1142 values [dseq 5] 3
1143   "{xs. concatP xs [(1::int), 2]}"
1145 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd .
1146 thm hdP.equation
1147 values "{x. hdP [1, 2, (3::int)] x}"
1148 values "{(xs, x). hdP [1, 2, (3::int)] 1}"
1150 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl .
1151 thm tlP.equation
1152 values "{x. tlP [1, 2, (3::nat)] x}"
1153 values "{x. tlP [1, 2, (3::int)] [3]}"
1155 code_pred [inductify, skip_proof] last .
1156 thm lastP.equation
1158 code_pred [inductify, skip_proof] butlast .
1159 thm butlastP.equation
1161 code_pred [inductify, skip_proof] take .
1162 thm takeP.equation
1164 code_pred [inductify, skip_proof] drop .
1165 thm dropP.equation
1166 code_pred [inductify, skip_proof] zip .
1167 thm zipP.equation
1169 code_pred [inductify, skip_proof] upt .
1170 (*
1171 code_pred [inductify, skip_proof] remdups .
1172 thm remdupsP.equation
1173 code_pred [dseq inductify] remdups .
1174 values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
1175 *)
1176 code_pred [inductify, skip_proof] remove1 .
1177 thm remove1P.equation
1178 values "{xs. remove1P 1 xs [2, (3::int)]}"
1180 code_pred [inductify, skip_proof] removeAll .
1181 thm removeAllP.equation
1182 code_pred [dseq inductify] removeAll .
1184 values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
1185 (*
1186 code_pred [inductify] distinct .
1187 thm distinct.equation
1188 *)
1189 code_pred [inductify, skip_proof] replicate .
1190 thm replicateP.equation
1191 values 5 "{(n, xs). replicateP n (0::int) xs}"
1193 code_pred [inductify, skip_proof] splice .
1194 thm splice.simps
1195 thm spliceP.equation
1197 values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
1199 code_pred [inductify, skip_proof] List.rev .
1200 code_pred [inductify] map .
1201 code_pred [inductify] foldr .
1202 code_pred [inductify] foldl .
1203 code_pred [inductify] filter .
1204 code_pred [random_dseq inductify] filter .
1206 section {* Function predicate replacement *}
1208 text {*
1209 If the mode analysis uses the functional mode, we
1210 replace predicates that resulted from functions again by their functions.
1211 *}
1213 inductive test_append
1214 where
1215   "List.append xs ys = zs ==> test_append xs ys zs"
1217 code_pred [inductify, skip_proof] test_append .
1218 thm test_append.equation
1220 text {* If append is not turned into a predicate, then the mode
1221   o => o => i => bool could not be inferred. *}
1223 values 4 "{(xs::int list, ys). test_append xs ys [1, 2, 3, 4]}"
1225 text {* If appendP is not reverted back to a function, then mode i => i => o => bool
1226   fails after deleting the predicate equation. *}
1228 declare appendP.equation[code del]
1230 values "{xs::int list. test_append [1,2] [3,4] xs}"
1231 values "{xs::int list. test_append (replicate 1000 1) (replicate 1000 2) xs}"
1232 values "{xs::int list. test_append (replicate 2000 1) (replicate 2000 2) xs}"
1234 text {* Redeclaring append.equation as code equation *}
1236 declare appendP.equation[code]
1238 subsection {* Function with tuples *}
1240 fun append'
1241 where
1242   "append' ([], ys) = ys"
1243 | "append' (x # xs, ys) = x # append' (xs, ys)"
1245 inductive test_append'
1246 where
1247   "append' (xs, ys) = zs ==> test_append' xs ys zs"
1249 code_pred [inductify, skip_proof] test_append' .
1251 thm test_append'.equation
1253 values "{(xs::int list, ys). test_append' xs ys [1, 2, 3, 4]}"
1255 declare append'P.equation[code del]
1257 values "{zs :: int list. test_append' [1,2,3] [4,5] zs}"
1259 section {* Arithmetic examples *}
1261 subsection {* Examples on nat *}
1263 inductive plus_nat_test :: "nat => nat => nat => bool"
1264 where
1265   "x + y = z ==> plus_nat_test x y z"
1267 code_pred [inductify, skip_proof] plus_nat_test .
1268 code_pred [new_random_dseq inductify] plus_nat_test .
1270 thm plus_nat_test.equation
1271 thm plus_nat_test.new_random_dseq_equation
1273 values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))}"] "{z. plus_nat_test 4 5 z}"
1274 values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))}"] "{z. plus_nat_test 7 2 z}"
1275 values [expected "{Suc (Suc (Suc (Suc 0)))}"] "{y. plus_nat_test 5 y 9}"
1276 values [expected "{}"] "{y. plus_nat_test 9 y 8}"
1277 values [expected "{Suc (Suc (Suc (Suc (Suc (Suc 0)))))}"] "{y. plus_nat_test 1 y 7}"
1278 values [expected "{Suc (Suc 0)}"] "{x. plus_nat_test x 7 9}"
1279 values [expected "{}"] "{x. plus_nat_test x 9 7}"
1280 values [expected "{(0::nat, 0::nat)}"] "{(x, y). plus_nat_test x y 0}"
1281 values [expected "{(0, Suc 0), (Suc 0, 0)}"] "{(x, y). plus_nat_test x y 1}"
1282 values [expected "{(0, Suc (Suc (Suc (Suc (Suc 0))))),
1283                   (Suc 0, Suc (Suc (Suc (Suc 0)))),
1284                   (Suc (Suc 0), Suc (Suc (Suc 0))),
1285                   (Suc (Suc (Suc 0)), Suc (Suc 0)),
1286                   (Suc (Suc (Suc (Suc 0))), Suc 0),
1287                   (Suc (Suc (Suc (Suc (Suc 0)))), 0)}"]
1288   "{(x, y). plus_nat_test x y 5}"
1290 inductive minus_nat_test :: "nat => nat => nat => bool"
1291 where
1292   "x - y = z ==> minus_nat_test x y z"
1294 code_pred [inductify, skip_proof] minus_nat_test .
1295 code_pred [new_random_dseq inductify] minus_nat_test .
1297 thm minus_nat_test.equation
1298 thm minus_nat_test.new_random_dseq_equation
1300 values [expected "{0::nat}"] "{z. minus_nat_test 4 5 z}"
1301 values [expected "{Suc (Suc (Suc (Suc (Suc 0))))}"] "{z. minus_nat_test 7 2 z}"
1302 values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))}"] "{x. minus_nat_test x 7 9}"
1303 values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))}"] "{x. minus_nat_test x 9 7}"
1304 values [expected "{0, Suc 0, Suc (Suc 0), Suc (Suc (Suc 0))}"] "{x. minus_nat_test x 3 0}"
1305 values [expected "{0::nat}"] "{x. minus_nat_test x 0 0}"
1307 subsection {* Examples on int *}
1309 inductive plus_int_test :: "int => int => int => bool"
1310 where
1311   "a + b = c ==> plus_int_test a b c"
1313 code_pred [inductify, skip_proof] plus_int_test .
1314 code_pred [new_random_dseq inductify] plus_int_test .
1316 thm plus_int_test.equation
1317 thm plus_int_test.new_random_dseq_equation
1319 values [expected "{1::int}"] "{a. plus_int_test a 6 7}"
1320 values [expected "{1::int}"] "{b. plus_int_test 6 b 7}"
1321 values [expected "{11::int}"] "{c. plus_int_test 5 6 c}"
1323 inductive minus_int_test :: "int => int => int => bool"
1324 where
1325   "a - b = c ==> minus_int_test a b c"
1327 code_pred [inductify, skip_proof] minus_int_test .
1328 code_pred [new_random_dseq inductify] minus_int_test .
1330 thm minus_int_test.equation
1331 thm minus_int_test.new_random_dseq_equation
1333 values [expected "{4::int}"] "{c. minus_int_test 9 5 c}"
1334 values [expected "{9::int}"] "{a. minus_int_test a 4 5}"
1335 values [expected "{-1::int}"] "{b. minus_int_test 4 b 5}"
1337 subsection {* minus on bool *}
1339 inductive All :: "nat => bool"
1340 where
1341   "All x"
1343 inductive None :: "nat => bool"
1345 definition "test_minus_bool x = (None x - All x)"
1347 code_pred [inductify] test_minus_bool .
1348 thm test_minus_bool.equation
1350 values "{x. test_minus_bool x}"
1352 subsection {* Functions *}
1354 fun partial_hd :: "'a list => 'a option"
1355 where
1356   "partial_hd [] = Option.None"
1357 | "partial_hd (x # xs) = Some x"
1359 inductive hd_predicate
1360 where
1361   "partial_hd xs = Some x ==> hd_predicate xs x"
1363 code_pred (expected_modes: i => i => bool, i => o => bool) hd_predicate .
1365 thm hd_predicate.equation
1367 subsection {* Locales *}
1369 inductive hd_predicate2 :: "('a list => 'a option) => 'a list => 'a => bool"
1370 where
1371   "partial_hd' xs = Some x ==> hd_predicate2 partial_hd' xs x"
1374 thm hd_predicate2.intros
1376 code_pred (expected_modes: i => i => i => bool, i => i => o => bool) hd_predicate2 .
1377 thm hd_predicate2.equation
1379 locale A = fixes partial_hd :: "'a list => 'a option" begin
1381 inductive hd_predicate_in_locale :: "'a list => 'a => bool"
1382 where
1383   "partial_hd xs = Some x ==> hd_predicate_in_locale xs x"
1385 end
1387 text {* The global introduction rules must be redeclared as introduction rules and then
1388   one could invoke code_pred. *}
1390 declare A.hd_predicate_in_locale.intros [code_pred_intro]
1392 code_pred (expected_modes: i => i => i => bool, i => i => o => bool) A.hd_predicate_in_locale
1393 by (auto elim: A.hd_predicate_in_locale.cases)
1395 interpretation A partial_hd .
1396 thm hd_predicate_in_locale.intros
1397 text {* A locally compliant solution with a trivial interpretation fails, because
1398 the predicate compiler has very strict assumptions about the terms and their structure. *}
1400 (*code_pred hd_predicate_in_locale .*)
1402 section {* Integer example *}
1404 definition three :: int
1405 where "three = 3"
1407 inductive is_three
1408 where
1409   "is_three three"
1411 code_pred is_three .
1413 thm is_three.equation
1415 section {* String.literal example *}
1417 definition Error_1
1418 where
1419   "Error_1 = STR ''Error 1''"
1421 definition Error_2
1422 where
1423   "Error_2 = STR ''Error 2''"
1425 inductive "is_error" :: "String.literal \<Rightarrow> bool"
1426 where
1427   "is_error Error_1"
1428 | "is_error Error_2"
1430 code_pred is_error .
1432 thm is_error.equation
1434 inductive is_error' :: "String.literal \<Rightarrow> bool"
1435 where
1436   "is_error' (STR ''Error1'')"
1437 | "is_error' (STR ''Error2'')"
1439 code_pred is_error' .
1441 thm is_error'.equation
1443 datatype ErrorObject = Error String.literal int
1445 inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
1446 where
1447   "is_error'' (Error Error_1 3)"
1448 | "is_error'' (Error Error_2 4)"
1450 code_pred is_error'' .
1452 thm is_error''.equation
1454 section {* Another function example *}
1456 consts f :: "'a \<Rightarrow> 'a"
1458 inductive fun_upd :: "(('a * 'b) * ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
1459 where
1460   "fun_upd ((x, a), s) (s(x := f a))"
1462 code_pred fun_upd .
1464 thm fun_upd.equation
1466 section {* Examples for detecting switches *}
1468 inductive detect_switches1 where
1469   "detect_switches1 [] []"
1470 | "detect_switches1 (x # xs) (y # ys)"
1472 code_pred [detect_switches, skip_proof] detect_switches1 .
1474 thm detect_switches1.equation
1476 inductive detect_switches2 :: "('a => bool) => bool"
1477 where
1478   "detect_switches2 P"
1480 code_pred [detect_switches, skip_proof] detect_switches2 .
1481 thm detect_switches2.equation
1483 inductive detect_switches3 :: "('a => bool) => 'a list => bool"
1484 where
1485   "detect_switches3 P []"
1486 | "detect_switches3 P (x # xs)"
1488 code_pred [detect_switches, skip_proof] detect_switches3 .
1490 thm detect_switches3.equation
1492 inductive detect_switches4 :: "('a => bool) => 'a list => 'a list => bool"
1493 where
1494   "detect_switches4 P [] []"
1495 | "detect_switches4 P (x # xs) (y # ys)"
1497 code_pred [detect_switches, skip_proof] detect_switches4 .
1498 thm detect_switches4.equation
1500 inductive detect_switches5 :: "('a => 'a => bool) => 'a list => 'a list => bool"
1501 where
1502   "detect_switches5 P [] []"
1503 | "detect_switches5 P xs ys ==> P x y ==> detect_switches5 P (x # xs) (y # ys)"
1505 code_pred [detect_switches, skip_proof] detect_switches5 .
1507 thm detect_switches5.equation
1509 inductive detect_switches6 :: "(('a => 'b => bool) * 'a list * 'b list) => bool"
1510 where
1511   "detect_switches6 (P, [], [])"
1512 | "detect_switches6 (P, xs, ys) ==> P x y ==> detect_switches6 (P, x # xs, y # ys)"
1514 code_pred [detect_switches, skip_proof] detect_switches6 .
1516 inductive detect_switches7 :: "('a => bool) => ('b => bool) => ('a * 'b list) => bool"
1517 where
1518   "detect_switches7 P Q (a, [])"
1519 | "P a ==> Q x ==> detect_switches7 P Q (a, x#xs)"
1521 code_pred [skip_proof] detect_switches7 .
1523 thm detect_switches7.equation
1525 inductive detect_switches8 :: "nat => bool"
1526 where
1527   "detect_switches8 0"
1528 | "x mod 2 = 0 ==> detect_switches8 (Suc x)"
1530 code_pred [detect_switches, skip_proof] detect_switches8 .
1532 thm detect_switches8.equation
1534 inductive detect_switches9 :: "nat => nat => bool"
1535 where
1536   "detect_switches9 0 0"
1537 | "detect_switches9 0 (Suc x)"
1538 | "detect_switches9 (Suc x) 0"
1539 | "x = y ==> detect_switches9 (Suc x) (Suc y)"
1540 | "c1 = c2 ==> detect_switches9 c1 c2"
1542 code_pred [detect_switches, skip_proof] detect_switches9 .
1544 thm detect_switches9.equation
1546 text {* The higher-order predicate r is in an output term *}
1548 datatype result = Result bool
1550 inductive fixed_relation :: "'a => bool"
1552 inductive test_relation_in_output_terms :: "('a => bool) => 'a => result => bool"
1553 where
1554   "test_relation_in_output_terms r x (Result (r x))"
1555 | "test_relation_in_output_terms r x (Result (fixed_relation x))"
1557 code_pred test_relation_in_output_terms .
1559 thm test_relation_in_output_terms.equation
1562 text {*
1563   We want that the argument r is not treated as a higher-order relation, but simply as input.
1564 *}
1566 inductive test_uninterpreted_relation :: "('a => bool) => 'a list => bool"
1567 where
1568   "list_all r xs ==> test_uninterpreted_relation r xs"
1570 code_pred (modes: i => i => bool) test_uninterpreted_relation .
1572 thm test_uninterpreted_relation.equation
1574 inductive list_ex'
1575 where
1576   "P x ==> list_ex' P (x#xs)"
1577 | "list_ex' P xs ==> list_ex' P (x#xs)"
1579 code_pred list_ex' .
1581 inductive test_uninterpreted_relation2 :: "('a => bool) => 'a list => bool"
1582 where
1583   "list_ex r xs ==> test_uninterpreted_relation2 r xs"
1584 | "list_ex' r xs ==> test_uninterpreted_relation2 r xs"
1586 text {* Proof procedure cannot handle this situation yet. *}
1588 code_pred (modes: i => i => bool) [skip_proof] test_uninterpreted_relation2 .
1590 thm test_uninterpreted_relation2.equation
1593 text {* Trivial predicate *}
1595 inductive implies_itself :: "'a => bool"
1596 where
1597   "implies_itself x ==> implies_itself x"
1599 code_pred implies_itself .
1601 text {* Case expressions *}
1603 definition
1604   "map_prods xs ys = (map (%((a, b), c). (a, b, c)) xs = ys)"
1606 code_pred [inductify] map_prods .
1608 end