src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
author Lukas Bulwahn <lukas.bulwahn@gmail.com>
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
     4 
     5 declare [[values_timeout = 480.0]]
     6 
     7 subsection {* Basic predicates *}
     8 
     9 inductive False' :: "bool"
    10 
    11 code_pred (expected_modes: bool) False' .
    12 code_pred [dseq] False' .
    13 code_pred [random_dseq] False' .
    14 
    15 values [expected "{}" pred] "{x. False'}"
    16 values [expected "{}" dseq 1] "{x. False'}"
    17 values [expected "{}" random_dseq 1, 1, 1] "{x. False'}"
    18 
    19 value "False'"
    20 
    21 inductive True' :: "bool"
    22 where
    23   "True ==> True'"
    24 
    25 code_pred True' .
    26 code_pred [dseq] True' .
    27 code_pred [random_dseq] True' .
    28 
    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'}"
    40 
    41 inductive EmptyPred :: "'a \<Rightarrow> bool"
    42 
    43 code_pred (expected_modes: o => bool, i => bool) EmptyPred .
    44 
    45 definition EmptyPred' :: "'a \<Rightarrow> bool"
    46 where "EmptyPred' = (\<lambda> x. False)"
    47 
    48 code_pred (expected_modes: o => bool, i => bool) [inductify] EmptyPred' .
    49 
    50 inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
    51 
    52 code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel .
    53 
    54 inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    55 for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    56 
    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 .
    67 
    68 thm EmptyClosure.equation
    69 
    70 (* TODO: inductive package is broken!
    71 inductive False'' :: "bool"
    72 where
    73   "False \<Longrightarrow> False''"
    74 
    75 code_pred (expected_modes: bool) False'' .
    76 
    77 inductive EmptySet'' :: "'a \<Rightarrow> bool"
    78 where
    79   "False \<Longrightarrow> EmptySet'' x"
    80 
    81 code_pred (expected_modes: i => bool, o => bool) [inductify] EmptySet'' .
    82 *)
    83 
    84 consts a' :: 'a
    85 
    86 inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    87 where
    88   "Fact a' a'"
    89 
    90 code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
    91 
    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"
    98 
    99 code_pred predicate_where_argument_is_condition .
   100 
   101 text {* Other similar examples of this kind: *}
   102 
   103 inductive predicate_where_argument_is_in_equation :: "bool \<Rightarrow> bool"
   104 where
   105   "ck = True \<Longrightarrow> predicate_where_argument_is_in_equation ck"
   106 
   107 code_pred predicate_where_argument_is_in_equation .
   108 
   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"
   113 
   114 code_pred predicate_where_argument_is_condition_and_value .
   115 
   116 inductive predicate_where_argument_is_neg_condition :: "bool \<Rightarrow> bool"
   117 where
   118   "\<not> ck \<Longrightarrow> predicate_where_argument_is_neg_condition ck"
   119 
   120 code_pred predicate_where_argument_is_neg_condition .
   121 
   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"
   125 
   126 code_pred predicate_where_argument_is_neg_condition_and_in_equation .
   127 
   128 
   129 inductive zerozero :: "nat * nat => bool"
   130 where
   131   "zerozero (0, 0)"
   132 
   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 .
   136 
   137 thm zerozero.equation
   138 thm zerozero.dseq_equation
   139 thm zerozero.random_dseq_equation
   140 
   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)}"
   146 
   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)}"
   152 
   153 inductive nested_tuples :: "((int * int) * int * int) => bool"
   154 where
   155   "nested_tuples ((0, 1), 2, 3)"
   156 
   157 code_pred nested_tuples .
   158 
   159 inductive JamesBond :: "nat => int => natural => bool"
   160 where
   161   "JamesBond 0 0 7"
   162 
   163 code_pred JamesBond .
   164 
   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}"
   171 
   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}"
   175 
   176 
   177 subsection {* Alternative Rules *}
   178 
   179 datatype char = C | D | E | F | G | H
   180 
   181 inductive is_C_or_D
   182 where
   183   "(x = C) \<or> (x = D) ==> is_C_or_D x"
   184 
   185 code_pred (expected_modes: i => bool) is_C_or_D .
   186 thm is_C_or_D.equation
   187 
   188 inductive is_D_or_E
   189 where
   190   "(x = D) \<or> (x = E) ==> is_D_or_E x"
   191 
   192 lemma [code_pred_intro]:
   193   "is_D_or_E D"
   194 by (auto intro: is_D_or_E.intros)
   195 
   196 lemma [code_pred_intro]:
   197   "is_D_or_E E"
   198 by (auto intro: is_D_or_E.intros)
   199 
   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
   216 
   217 thm is_D_or_E.equation
   218 
   219 inductive is_F_or_G
   220 where
   221   "x = F \<or> x = G ==> is_F_or_G x"
   222 
   223 lemma [code_pred_intro]:
   224   "is_F_or_G F"
   225 by (auto intro: is_F_or_G.intros)
   226 
   227 lemma [code_pred_intro]:
   228   "is_F_or_G G"
   229 by (auto intro: is_F_or_G.intros)
   230 
   231 inductive is_FGH
   232 where
   233   "is_F_or_G x ==> is_FGH x"
   234 | "is_FGH H"
   235 
   236 text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}
   237 
   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
   256 
   257 subsection {* Named alternative rules *}
   258 
   259 inductive appending
   260 where
   261   nil: "appending [] ys ys"
   262 | cons: "appending xs ys zs \<Longrightarrow> appending (x#xs) ys (x#zs)"
   263 
   264 lemma appending_alt_nil: "ys = zs \<Longrightarrow> appending [] ys zs"
   265 by (auto intro: appending.intros)
   266 
   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)
   269 
   270 text {* With code_pred_intro, we can give fact names to the alternative rules,
   271   which are used for the code_pred command. *}
   272 
   273 declare appending_alt_nil[code_pred_intro alt_nil] appending_alt_cons[code_pred_intro alt_cons]
   274  
   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
   287 
   288 
   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)"
   294 
   295 
   296 declare even_zero[code_pred_intro even_0]
   297 
   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)
   300 
   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)
   303 
   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
   323 
   324 subsection {* Preprocessor Inlining  *}
   325 
   326 definition "equals == (op =)"
   327  
   328 inductive zerozero' :: "nat * nat => bool" where
   329   "equals (x, y) (0, 0) ==> zerozero' (x, y)"
   330 
   331 code_pred (expected_modes: i => bool) zerozero' .
   332 
   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
   344 
   345 declare zerozero'_eq [code_pred_inline]
   346 
   347 definition "zerozero'' x == zerozero' x"
   348 
   349 text {* if preprocessing fails, zerozero'' will not have all modes. *}
   350 
   351 code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
   352 
   353 subsection {* Sets *}
   354 (*
   355 inductive_set EmptySet :: "'a set"
   356 
   357 code_pred (expected_modes: o => bool, i => bool) EmptySet .
   358 
   359 definition EmptySet' :: "'a set"
   360 where "EmptySet' = {}"
   361 
   362 code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
   363 *)
   364 subsection {* Numerals *}
   365 
   366 definition
   367   "one_or_two = (%x. x = Suc 0 \<or> ( x = Suc (Suc 0)))"
   368 
   369 code_pred [inductify] one_or_two .
   370 
   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}"
   376 
   377 inductive one_or_two' :: "nat => bool"
   378 where
   379   "one_or_two' 1"
   380 | "one_or_two' 2"
   381 
   382 code_pred one_or_two' .
   383 thm one_or_two'.equation
   384 
   385 values "{x. one_or_two' x}"
   386 
   387 definition one_or_two'':
   388   "one_or_two'' == (%x. x = 1 \<or> x = (2::nat))"
   389 
   390 code_pred [inductify] one_or_two'' .
   391 thm one_or_two''.equation
   392 
   393 values "{x. one_or_two'' x}"
   394 
   395 subsection {* even predicate *}
   396 
   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)"
   401 
   402 code_pred (expected_modes: i => bool, o => bool) even .
   403 code_pred [dseq] even .
   404 code_pred [random_dseq] even .
   405 
   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
   412 
   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}"
   424 
   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}"
   430 
   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}"
   436 
   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}"
   440 
   441 definition odd' where "odd' x == \<not> even x"
   442 
   443 code_pred (expected_modes: i => bool) [inductify] odd' .
   444 code_pred [dseq inductify] odd' .
   445 code_pred [random_dseq inductify] odd' .
   446 
   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}"
   451 
   452 
   453 inductive is_even :: "nat \<Rightarrow> bool"
   454 where
   455   "n mod 2 = 0 \<Longrightarrow> is_even n"
   456 
   457 code_pred (expected_modes: i => bool) is_even .
   458 
   459 subsection {* append predicate *}
   460 
   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)"
   464 
   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 .
   469 
   470 code_pred [dseq] append .
   471 code_pred [random_dseq] append .
   472 
   473 thm append.equation
   474 thm append.dseq_equation
   475 thm append.random_dseq_equation
   476 
   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]}"
   480 
   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}"
   491 
   492 value "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
   493 value "Predicate.the (slice ([]::int list))"
   494 
   495 
   496 text {* tricky case with alternative rules *}
   497 
   498 inductive append2
   499 where
   500   "append2 [] xs xs"
   501 | "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
   502 
   503 lemma append2_Nil: "append2 [] (xs::'b list) xs"
   504   by (simp add: append2.intros(1))
   505 
   506 lemmas [code_pred_intro] = append2_Nil append2.intros(2)
   507 
   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
   523 
   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)"
   528 
   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 .
   531 
   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 .
   534 
   535 code_pred [random_dseq] tupled_append .
   536 thm tupled_append.equation
   537 
   538 values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}"
   539 
   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)"
   545 
   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
   549 
   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)"
   554 
   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
   558 
   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)"
   563 
   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
   567 
   568 subsection {* map_ofP predicate *}
   569 
   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"
   574 
   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
   577 
   578 subsection {* filter predicate *}
   579 
   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"
   586 
   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 .
   590 
   591 thm filter1.equation
   592 
   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}"
   596 
   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"
   602 
   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 .
   606 
   607 thm filter2.equation
   608 thm filter2.random_dseq_equation
   609 
   610 inductive filter3
   611 for P
   612 where
   613   "List.filter P xs = ys ==> filter3 P xs ys"
   614 
   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 .
   616 
   617 code_pred filter3 .
   618 thm filter3.equation
   619 
   620 (*
   621 inductive filter4
   622 where
   623   "List.filter P xs = ys ==> filter4 P xs ys"
   624 
   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 *}
   630 
   631 inductive rev where
   632     "rev [] []"
   633   | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
   634 
   635 code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .
   636 
   637 thm rev.equation
   638 
   639 values "{xs. rev [0, 1, 2, 3::nat] xs}"
   640 
   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)"
   644 
   645 code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
   646 thm tupled_rev.equation
   647 
   648 subsection {* partition predicate *}
   649 
   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)"
   655 
   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 .
   661 
   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]}"
   666 
   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)"
   672 
   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 .
   675 
   676 thm tupled_partition.equation
   677 
   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
   682 
   683 subsection {* transitive predicate *}
   684 
   685 text {* Also look at the tabled transitive closure in the Library *}
   686 
   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
   694 
   695 
   696 code_pred [dseq] tranclp .
   697 code_pred [random_dseq] tranclp .
   698 thm tranclp.equation
   699 thm tranclp.random_dseq_equation
   700 
   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"
   705 
   706 code_pred [random_dseq] rtrancl' .
   707 
   708 thm rtrancl'.random_dseq_equation
   709 
   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)"
   714 
   715 code_pred rtrancl'' .
   716 
   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)"
   721 
   722 code_pred rtrancl''' .
   723 
   724 
   725 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   726     "succ 0 1"
   727   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
   728 
   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
   733 
   734 values 10 "{(m, n). succ n m}"
   735 values "{m. succ 0 m}"
   736 values "{m. succ m 0}"
   737 
   738 text {* values command needs mode annotation of the parameter succ
   739 to disambiguate which mode is to be chosen. *} 
   740 
   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}"
   744 
   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"
   755  
   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"
   758 
   759 code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
   760 
   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"*)
   771 
   772 code_pred [dseq] not_reachable_in_example_graph .
   773 
   774 values [dseq 6] "{x. tranclp example_graph 0 3}"
   775 
   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}"
   782 
   783 
   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"
   786 
   787 code_pred not_reachable_in_example_graph' .
   788 
   789 value "not_reachable_in_example_graph' 0 3"
   790 (* value "not_reachable_in_example_graph' 0 5" would not terminate *)
   791 
   792 
   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 *)
   799 
   800 code_pred [dseq] not_reachable_in_example_graph' .
   801 
   802 (*thm not_reachable_in_example_graph'.dseq_equation*)
   803 
   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 *)
   810 
   811 subsection {* Free function variable *}
   812 
   813 inductive FF :: "nat => nat => bool"
   814 where
   815   "f x = y ==> FF x y"
   816 
   817 code_pred FF .
   818 
   819 subsection {* IMP *}
   820 
   821 type_synonym var = nat
   822 type_synonym state = "int list"
   823 
   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
   830 
   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)"
   839 
   840 code_pred tupled_exec .
   841 
   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)}"
   843 
   844 subsection {* CCS *}
   845 
   846 text{* This example formalizes finite CCS processes without communication or
   847 recursion. For simplicity, labels are natural numbers. *}
   848 
   849 datatype proc = nil | pre nat proc | or proc proc | par proc proc
   850 
   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)"
   858 
   859 code_pred tupled_step .
   860 thm tupled_step.equation
   861 
   862 subsection {* divmod *}
   863 
   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"
   867 
   868 code_pred divmod_rel .
   869 thm divmod_rel.equation
   870 value "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
   871 
   872 subsection {* Transforming predicate logic into logic programs *}
   873 
   874 subsection {* Transforming functions into logic programs *}
   875 definition
   876   "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
   877 
   878 code_pred [inductify, skip_proof] case_f .
   879 thm case_fP.equation
   880 
   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'))"
   886 
   887 code_pred [inductify] fold_map_idx .
   888 
   889 subsection {* Minimum *}
   890 
   891 definition Min
   892 where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
   893 
   894 code_pred [inductify] Min .
   895 thm Min.equation
   896 
   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. *}
   900 
   901 (*
   902 declare lexord_def[code_pred_def]
   903 code_pred [inductify] lexord .
   904 code_pred [random_dseq inductify] lexord .
   905 
   906 thm lexord.equation
   907 thm lexord.random_dseq_equation
   908 
   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)"
   913  
   914 code_pred less_than_nat .
   915 
   916 code_pred [dseq] less_than_nat .
   917 code_pred [random_dseq] less_than_nat .
   918 
   919 inductive test_lexord :: "nat list * nat list => bool"
   920 where
   921   "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)"
   922 
   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
   928 
   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])}"*)
   931 
   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
   940 
   941 values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
   942 *)
   943 
   944 inductive has_length
   945 where
   946   "has_length [] 0"
   947 | "has_length xs i ==> has_length (x # xs) (Suc i)" 
   948 
   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
   960 
   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
   978 
   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
   993 
   994 values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
   995 
   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
  1002 
  1003 code_pred [random_dseq inductify] lenlex .
  1004 thm lenlex.random_dseq_equation
  1005 
  1006 values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"
  1007 
  1008 thm lists.intros
  1009 code_pred [inductify] lists .
  1010 thm lists.equation
  1011 *)
  1012 subsection {* AVL Tree *}
  1013 
  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"
  1018 
  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*)
  1027 
  1028 code_pred [new_random_dseq inductify] avl .
  1029 thm avl.new_random_dseq_equation
  1030 (* TODO: has highly non-deterministic execution time!
  1031 
  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)"
  1038 
  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)"
  1044 
  1045 (* 
  1046 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
  1047 thm set_of.equation
  1048 
  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 .
  1065 
  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]
  1073 
  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
  1089 
  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
  1096 
  1097 code_pred [inductify] Field .
  1098 thm Field.equation
  1099 
  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 *}
  1116 
  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
  1121 
  1122 values [new_random_dseq 2,3,10] 3 "{xs. size_list'P (xs::nat list) (5::nat)}"
  1123 
  1124 code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
  1125 thm concatP.equation
  1126 
  1127 values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
  1128 values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
  1129 
  1130 code_pred [dseq inductify] List.concat .
  1131 thm concatP.dseq_equation
  1132 
  1133 values [dseq 3] 3
  1134   "{xs. concatP xs ([0] :: nat list)}"
  1135 
  1136 values [dseq 5] 3
  1137   "{xs. concatP xs ([1] :: int list)}"
  1138 
  1139 values [dseq 5] 3
  1140   "{xs. concatP xs ([1] :: nat list)}"
  1141 
  1142 values [dseq 5] 3
  1143   "{xs. concatP xs [(1::int), 2]}"
  1144 
  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}"
  1149  
  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]}"
  1154 
  1155 code_pred [inductify, skip_proof] last .
  1156 thm lastP.equation
  1157 
  1158 code_pred [inductify, skip_proof] butlast .
  1159 thm butlastP.equation
  1160 
  1161 code_pred [inductify, skip_proof] take .
  1162 thm takeP.equation
  1163 
  1164 code_pred [inductify, skip_proof] drop .
  1165 thm dropP.equation
  1166 code_pred [inductify, skip_proof] zip .
  1167 thm zipP.equation
  1168 
  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)]}"
  1179 
  1180 code_pred [inductify, skip_proof] removeAll .
  1181 thm removeAllP.equation
  1182 code_pred [dseq inductify] removeAll .
  1183 
  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}"
  1192 
  1193 code_pred [inductify, skip_proof] splice .
  1194 thm splice.simps
  1195 thm spliceP.equation
  1196 
  1197 values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
  1198 
  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 .
  1205 
  1206 section {* Function predicate replacement *}
  1207 
  1208 text {*
  1209 If the mode analysis uses the functional mode, we
  1210 replace predicates that resulted from functions again by their functions.
  1211 *}
  1212 
  1213 inductive test_append
  1214 where
  1215   "List.append xs ys = zs ==> test_append xs ys zs"
  1216 
  1217 code_pred [inductify, skip_proof] test_append .
  1218 thm test_append.equation
  1219 
  1220 text {* If append is not turned into a predicate, then the mode
  1221   o => o => i => bool could not be inferred. *}
  1222 
  1223 values 4 "{(xs::int list, ys). test_append xs ys [1, 2, 3, 4]}"
  1224 
  1225 text {* If appendP is not reverted back to a function, then mode i => i => o => bool
  1226   fails after deleting the predicate equation. *}
  1227 
  1228 declare appendP.equation[code del]
  1229 
  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}"
  1233 
  1234 text {* Redeclaring append.equation as code equation *}
  1235 
  1236 declare appendP.equation[code]
  1237 
  1238 subsection {* Function with tuples *}
  1239 
  1240 fun append'
  1241 where
  1242   "append' ([], ys) = ys"
  1243 | "append' (x # xs, ys) = x # append' (xs, ys)"
  1244 
  1245 inductive test_append'
  1246 where
  1247   "append' (xs, ys) = zs ==> test_append' xs ys zs"
  1248 
  1249 code_pred [inductify, skip_proof] test_append' .
  1250 
  1251 thm test_append'.equation
  1252 
  1253 values "{(xs::int list, ys). test_append' xs ys [1, 2, 3, 4]}"
  1254 
  1255 declare append'P.equation[code del]
  1256 
  1257 values "{zs :: int list. test_append' [1,2,3] [4,5] zs}"
  1258 
  1259 section {* Arithmetic examples *}
  1260 
  1261 subsection {* Examples on nat *}
  1262 
  1263 inductive plus_nat_test :: "nat => nat => nat => bool"
  1264 where
  1265   "x + y = z ==> plus_nat_test x y z"
  1266 
  1267 code_pred [inductify, skip_proof] plus_nat_test .
  1268 code_pred [new_random_dseq inductify] plus_nat_test .
  1269 
  1270 thm plus_nat_test.equation
  1271 thm plus_nat_test.new_random_dseq_equation
  1272 
  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}"
  1289 
  1290 inductive minus_nat_test :: "nat => nat => nat => bool"
  1291 where
  1292   "x - y = z ==> minus_nat_test x y z"
  1293 
  1294 code_pred [inductify, skip_proof] minus_nat_test .
  1295 code_pred [new_random_dseq inductify] minus_nat_test .
  1296 
  1297 thm minus_nat_test.equation
  1298 thm minus_nat_test.new_random_dseq_equation
  1299 
  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}"
  1306 
  1307 subsection {* Examples on int *}
  1308 
  1309 inductive plus_int_test :: "int => int => int => bool"
  1310 where
  1311   "a + b = c ==> plus_int_test a b c"
  1312 
  1313 code_pred [inductify, skip_proof] plus_int_test .
  1314 code_pred [new_random_dseq inductify] plus_int_test .
  1315 
  1316 thm plus_int_test.equation
  1317 thm plus_int_test.new_random_dseq_equation
  1318 
  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}"
  1322 
  1323 inductive minus_int_test :: "int => int => int => bool"
  1324 where
  1325   "a - b = c ==> minus_int_test a b c"
  1326 
  1327 code_pred [inductify, skip_proof] minus_int_test .
  1328 code_pred [new_random_dseq inductify] minus_int_test .
  1329 
  1330 thm minus_int_test.equation
  1331 thm minus_int_test.new_random_dseq_equation
  1332 
  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}"
  1336 
  1337 subsection {* minus on bool *}
  1338 
  1339 inductive All :: "nat => bool"
  1340 where
  1341   "All x"
  1342 
  1343 inductive None :: "nat => bool"
  1344 
  1345 definition "test_minus_bool x = (None x - All x)"
  1346 
  1347 code_pred [inductify] test_minus_bool .
  1348 thm test_minus_bool.equation
  1349 
  1350 values "{x. test_minus_bool x}"
  1351 
  1352 subsection {* Functions *}
  1353 
  1354 fun partial_hd :: "'a list => 'a option"
  1355 where
  1356   "partial_hd [] = Option.None"
  1357 | "partial_hd (x # xs) = Some x"
  1358 
  1359 inductive hd_predicate
  1360 where
  1361   "partial_hd xs = Some x ==> hd_predicate xs x"
  1362 
  1363 code_pred (expected_modes: i => i => bool, i => o => bool) hd_predicate .
  1364 
  1365 thm hd_predicate.equation
  1366 
  1367 subsection {* Locales *}
  1368 
  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"
  1372 
  1373 
  1374 thm hd_predicate2.intros
  1375 
  1376 code_pred (expected_modes: i => i => i => bool, i => i => o => bool) hd_predicate2 .
  1377 thm hd_predicate2.equation
  1378 
  1379 locale A = fixes partial_hd :: "'a list => 'a option" begin
  1380 
  1381 inductive hd_predicate_in_locale :: "'a list => 'a => bool"
  1382 where
  1383   "partial_hd xs = Some x ==> hd_predicate_in_locale xs x"
  1384 
  1385 end
  1386 
  1387 text {* The global introduction rules must be redeclared as introduction rules and then 
  1388   one could invoke code_pred. *}
  1389 
  1390 declare A.hd_predicate_in_locale.intros [code_pred_intro]
  1391 
  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)
  1394     
  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. *}
  1399  
  1400 (*code_pred hd_predicate_in_locale .*)
  1401 
  1402 section {* Integer example *}
  1403 
  1404 definition three :: int
  1405 where "three = 3"
  1406 
  1407 inductive is_three
  1408 where
  1409   "is_three three"
  1410 
  1411 code_pred is_three .
  1412 
  1413 thm is_three.equation
  1414 
  1415 section {* String.literal example *}
  1416 
  1417 definition Error_1
  1418 where
  1419   "Error_1 = STR ''Error 1''"
  1420 
  1421 definition Error_2
  1422 where
  1423   "Error_2 = STR ''Error 2''"
  1424 
  1425 inductive "is_error" :: "String.literal \<Rightarrow> bool"
  1426 where
  1427   "is_error Error_1"
  1428 | "is_error Error_2"
  1429 
  1430 code_pred is_error .
  1431 
  1432 thm is_error.equation
  1433 
  1434 inductive is_error' :: "String.literal \<Rightarrow> bool"
  1435 where
  1436   "is_error' (STR ''Error1'')"
  1437 | "is_error' (STR ''Error2'')"
  1438 
  1439 code_pred is_error' .
  1440 
  1441 thm is_error'.equation
  1442 
  1443 datatype ErrorObject = Error String.literal int
  1444 
  1445 inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
  1446 where
  1447   "is_error'' (Error Error_1 3)"
  1448 | "is_error'' (Error Error_2 4)"
  1449 
  1450 code_pred is_error'' .
  1451 
  1452 thm is_error''.equation
  1453 
  1454 section {* Another function example *}
  1455 
  1456 consts f :: "'a \<Rightarrow> 'a"
  1457 
  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))"
  1461 
  1462 code_pred fun_upd .
  1463 
  1464 thm fun_upd.equation
  1465 
  1466 section {* Examples for detecting switches *}
  1467 
  1468 inductive detect_switches1 where
  1469   "detect_switches1 [] []"
  1470 | "detect_switches1 (x # xs) (y # ys)"
  1471 
  1472 code_pred [detect_switches, skip_proof] detect_switches1 .
  1473 
  1474 thm detect_switches1.equation
  1475 
  1476 inductive detect_switches2 :: "('a => bool) => bool"
  1477 where
  1478   "detect_switches2 P"
  1479 
  1480 code_pred [detect_switches, skip_proof] detect_switches2 .
  1481 thm detect_switches2.equation
  1482 
  1483 inductive detect_switches3 :: "('a => bool) => 'a list => bool"
  1484 where
  1485   "detect_switches3 P []"
  1486 | "detect_switches3 P (x # xs)" 
  1487 
  1488 code_pred [detect_switches, skip_proof] detect_switches3 .
  1489 
  1490 thm detect_switches3.equation
  1491 
  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)"
  1496 
  1497 code_pred [detect_switches, skip_proof] detect_switches4 .
  1498 thm detect_switches4.equation
  1499 
  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)"
  1504 
  1505 code_pred [detect_switches, skip_proof] detect_switches5 .
  1506 
  1507 thm detect_switches5.equation
  1508 
  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)"
  1513 
  1514 code_pred [detect_switches, skip_proof] detect_switches6 .
  1515 
  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)"
  1520 
  1521 code_pred [skip_proof] detect_switches7 .
  1522 
  1523 thm detect_switches7.equation
  1524 
  1525 inductive detect_switches8 :: "nat => bool"
  1526 where
  1527   "detect_switches8 0"
  1528 | "x mod 2 = 0 ==> detect_switches8 (Suc x)"
  1529 
  1530 code_pred [detect_switches, skip_proof] detect_switches8 .
  1531 
  1532 thm detect_switches8.equation
  1533 
  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"
  1541 
  1542 code_pred [detect_switches, skip_proof] detect_switches9 .
  1543 
  1544 thm detect_switches9.equation
  1545 
  1546 text {* The higher-order predicate r is in an output term *}
  1547 
  1548 datatype result = Result bool
  1549 
  1550 inductive fixed_relation :: "'a => bool"
  1551 
  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))"
  1556 
  1557 code_pred test_relation_in_output_terms .
  1558 
  1559 thm test_relation_in_output_terms.equation
  1560 
  1561 
  1562 text {*
  1563   We want that the argument r is not treated as a higher-order relation, but simply as input.
  1564 *}
  1565 
  1566 inductive test_uninterpreted_relation :: "('a => bool) => 'a list => bool"
  1567 where
  1568   "list_all r xs ==> test_uninterpreted_relation r xs"
  1569 
  1570 code_pred (modes: i => i => bool) test_uninterpreted_relation .
  1571 
  1572 thm test_uninterpreted_relation.equation
  1573 
  1574 inductive list_ex'
  1575 where
  1576   "P x ==> list_ex' P (x#xs)"
  1577 | "list_ex' P xs ==> list_ex' P (x#xs)"
  1578 
  1579 code_pred list_ex' .
  1580 
  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"
  1585 
  1586 text {* Proof procedure cannot handle this situation yet. *}
  1587 
  1588 code_pred (modes: i => i => bool) [skip_proof] test_uninterpreted_relation2 .
  1589 
  1590 thm test_uninterpreted_relation2.equation
  1591 
  1592 
  1593 text {* Trivial predicate *}
  1594 
  1595 inductive implies_itself :: "'a => bool"
  1596 where
  1597   "implies_itself x ==> implies_itself x"
  1598 
  1599 code_pred implies_itself .
  1600 
  1601 text {* Case expressions *}
  1602 
  1603 definition
  1604   "map_prods xs ys = (map (%((a, b), c). (a, b, c)) xs = ys)"
  1605 
  1606 code_pred [inductify] map_prods .
  1607 
  1608 end