src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
author haftmann
Fri Feb 15 08:31:31 2013 +0100 (2013-02-15)
changeset 51143 0a2371e7ced3
parent 47433 07f4bf913230
child 51144 0ede9e2266a8
permissions -rw-r--r--
two target language numeral types: integer and natural, as replacement for code_numeral;
former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral;
refined stack of theories implementing int and/or nat by target language numerals;
reduced number of target language numeral types to exactly one
     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 inductive zerozero :: "nat * nat => bool"
    93 where
    94   "zerozero (0, 0)"
    95 
    96 code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .
    97 code_pred [dseq] zerozero .
    98 code_pred [random_dseq] zerozero .
    99 
   100 thm zerozero.equation
   101 thm zerozero.dseq_equation
   102 thm zerozero.random_dseq_equation
   103 
   104 text {* We expect the user to expand the tuples in the values command.
   105 The following values command is not supported. *}
   106 (*values "{x. zerozero x}" *)
   107 text {* Instead, the user must type *}
   108 values "{(x, y). zerozero (x, y)}"
   109 
   110 values [expected "{}" dseq 0] "{(x, y). zerozero (x, y)}"
   111 values [expected "{(0::nat, 0::nat)}" dseq 1] "{(x, y). zerozero (x, y)}"
   112 values [expected "{(0::nat, 0::nat)}" dseq 2] "{(x, y). zerozero (x, y)}"
   113 values [expected "{}" random_dseq 1, 1, 2] "{(x, y). zerozero (x, y)}"
   114 values [expected "{(0::nat, 0:: nat)}" random_dseq 1, 1, 3] "{(x, y). zerozero (x, y)}"
   115 
   116 inductive nested_tuples :: "((int * int) * int * int) => bool"
   117 where
   118   "nested_tuples ((0, 1), 2, 3)"
   119 
   120 code_pred nested_tuples .
   121 
   122 inductive JamesBond :: "nat => int => natural => bool"
   123 where
   124   "JamesBond 0 0 7"
   125 
   126 code_pred JamesBond .
   127 
   128 values [expected "{(0::nat, 0::int , 7::natural)}"] "{(a, b, c). JamesBond a b c}"
   129 values [expected "{(0::nat, 7::natural, 0:: int)}"] "{(a, c, b). JamesBond a b c}"
   130 values [expected "{(0::int, 0::nat, 7::natural)}"] "{(b, a, c). JamesBond a b c}"
   131 values [expected "{(0::int, 7::natural, 0::nat)}"] "{(b, c, a). JamesBond a b c}"
   132 values [expected "{(7::natural, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}"
   133 values [expected "{(7::natural, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}"
   134 
   135 values [expected "{(7::natural, 0::int)}"] "{(a, b). JamesBond 0 b a}"
   136 values [expected "{(7::natural, 0::nat)}"] "{(c, a). JamesBond a 0 c}"
   137 values [expected "{(0::nat, 7::natural)}"] "{(a, c). JamesBond a 0 c}"
   138 
   139 
   140 subsection {* Alternative Rules *}
   141 
   142 datatype char = C | D | E | F | G | H
   143 
   144 inductive is_C_or_D
   145 where
   146   "(x = C) \<or> (x = D) ==> is_C_or_D x"
   147 
   148 code_pred (expected_modes: i => bool) is_C_or_D .
   149 thm is_C_or_D.equation
   150 
   151 inductive is_D_or_E
   152 where
   153   "(x = D) \<or> (x = E) ==> is_D_or_E x"
   154 
   155 lemma [code_pred_intro]:
   156   "is_D_or_E D"
   157 by (auto intro: is_D_or_E.intros)
   158 
   159 lemma [code_pred_intro]:
   160   "is_D_or_E E"
   161 by (auto intro: is_D_or_E.intros)
   162 
   163 code_pred (expected_modes: o => bool, i => bool) is_D_or_E
   164 proof -
   165   case is_D_or_E
   166   from is_D_or_E.prems show thesis
   167   proof 
   168     fix xa
   169     assume x: "x = xa"
   170     assume "xa = D \<or> xa = E"
   171     from this show thesis
   172     proof
   173       assume "xa = D" from this x is_D_or_E(1) show thesis by simp
   174     next
   175       assume "xa = E" from this x is_D_or_E(2) show thesis by simp
   176     qed
   177   qed
   178 qed
   179 
   180 thm is_D_or_E.equation
   181 
   182 inductive is_F_or_G
   183 where
   184   "x = F \<or> x = G ==> is_F_or_G x"
   185 
   186 lemma [code_pred_intro]:
   187   "is_F_or_G F"
   188 by (auto intro: is_F_or_G.intros)
   189 
   190 lemma [code_pred_intro]:
   191   "is_F_or_G G"
   192 by (auto intro: is_F_or_G.intros)
   193 
   194 inductive is_FGH
   195 where
   196   "is_F_or_G x ==> is_FGH x"
   197 | "is_FGH H"
   198 
   199 text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}
   200 
   201 code_pred (expected_modes: o => bool, i => bool) is_FGH
   202 proof -
   203   case is_F_or_G
   204   from is_F_or_G.prems show thesis
   205   proof
   206     fix xa
   207     assume x: "x = xa"
   208     assume "xa = F \<or> xa = G"
   209     from this show thesis
   210     proof
   211       assume "xa = F"
   212       from this x is_F_or_G(1) show thesis by simp
   213     next
   214       assume "xa = G"
   215       from this x is_F_or_G(2) show thesis by simp
   216     qed
   217   qed
   218 qed
   219 
   220 subsection {* Named alternative rules *}
   221 
   222 inductive appending
   223 where
   224   nil: "appending [] ys ys"
   225 | cons: "appending xs ys zs \<Longrightarrow> appending (x#xs) ys (x#zs)"
   226 
   227 lemma appending_alt_nil: "ys = zs \<Longrightarrow> appending [] ys zs"
   228 by (auto intro: appending.intros)
   229 
   230 lemma appending_alt_cons: "xs' = x # xs \<Longrightarrow> appending xs ys zs \<Longrightarrow> zs' = x # zs \<Longrightarrow> appending xs' ys zs'"
   231 by (auto intro: appending.intros)
   232 
   233 text {* With code_pred_intro, we can give fact names to the alternative rules,
   234   which are used for the code_pred command. *}
   235 
   236 declare appending_alt_nil[code_pred_intro alt_nil] appending_alt_cons[code_pred_intro alt_cons]
   237  
   238 code_pred appending
   239 proof -
   240   case appending
   241   from appending.prems show thesis
   242   proof(cases)
   243     case nil
   244     from alt_nil nil show thesis by auto
   245   next
   246     case cons
   247     from alt_cons cons show thesis by fastforce
   248   qed
   249 qed
   250 
   251 
   252 inductive ya_even and ya_odd :: "nat => bool"
   253 where
   254   even_zero: "ya_even 0"
   255 | odd_plus1: "ya_even x ==> ya_odd (x + 1)"
   256 | even_plus1: "ya_odd x ==> ya_even (x + 1)"
   257 
   258 
   259 declare even_zero[code_pred_intro even_0]
   260 
   261 lemma [code_pred_intro odd_Suc]: "ya_even x ==> ya_odd (Suc x)"
   262 by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)
   263 
   264 lemma [code_pred_intro even_Suc]:"ya_odd x ==> ya_even (Suc x)"
   265 by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)
   266 
   267 code_pred ya_even
   268 proof -
   269   case ya_even
   270   from ya_even.prems show thesis
   271   proof (cases)
   272     case even_zero
   273     from even_zero even_0 show thesis by simp
   274   next
   275     case even_plus1
   276     from even_plus1 even_Suc show thesis by simp
   277   qed
   278 next
   279   case ya_odd
   280   from ya_odd.prems show thesis
   281   proof (cases)
   282     case odd_plus1
   283     from odd_plus1 odd_Suc show thesis by simp
   284   qed
   285 qed
   286 
   287 subsection {* Preprocessor Inlining  *}
   288 
   289 definition "equals == (op =)"
   290  
   291 inductive zerozero' :: "nat * nat => bool" where
   292   "equals (x, y) (0, 0) ==> zerozero' (x, y)"
   293 
   294 code_pred (expected_modes: i => bool) zerozero' .
   295 
   296 lemma zerozero'_eq: "zerozero' x == zerozero x"
   297 proof -
   298   have "zerozero' = zerozero"
   299     apply (auto simp add: fun_eq_iff)
   300     apply (cases rule: zerozero'.cases)
   301     apply (auto simp add: equals_def intro: zerozero.intros)
   302     apply (cases rule: zerozero.cases)
   303     apply (auto simp add: equals_def intro: zerozero'.intros)
   304     done
   305   from this show "zerozero' x == zerozero x" by auto
   306 qed
   307 
   308 declare zerozero'_eq [code_pred_inline]
   309 
   310 definition "zerozero'' x == zerozero' x"
   311 
   312 text {* if preprocessing fails, zerozero'' will not have all modes. *}
   313 
   314 code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
   315 
   316 subsection {* Sets *}
   317 (*
   318 inductive_set EmptySet :: "'a set"
   319 
   320 code_pred (expected_modes: o => bool, i => bool) EmptySet .
   321 
   322 definition EmptySet' :: "'a set"
   323 where "EmptySet' = {}"
   324 
   325 code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
   326 *)
   327 subsection {* Numerals *}
   328 
   329 definition
   330   "one_or_two = (%x. x = Suc 0 \<or> ( x = Suc (Suc 0)))"
   331 
   332 code_pred [inductify] one_or_two .
   333 
   334 code_pred [dseq] one_or_two .
   335 code_pred [random_dseq] one_or_two .
   336 thm one_or_two.dseq_equation
   337 values [expected "{1::nat, 2::nat}"] "{x. one_or_two x}"
   338 values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
   339 
   340 inductive one_or_two' :: "nat => bool"
   341 where
   342   "one_or_two' 1"
   343 | "one_or_two' 2"
   344 
   345 code_pred one_or_two' .
   346 thm one_or_two'.equation
   347 
   348 values "{x. one_or_two' x}"
   349 
   350 definition one_or_two'':
   351   "one_or_two'' == (%x. x = 1 \<or> x = (2::nat))"
   352 
   353 code_pred [inductify] one_or_two'' .
   354 thm one_or_two''.equation
   355 
   356 values "{x. one_or_two'' x}"
   357 
   358 subsection {* even predicate *}
   359 
   360 inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
   361     "even 0"
   362   | "even n \<Longrightarrow> odd (Suc n)"
   363   | "odd n \<Longrightarrow> even (Suc n)"
   364 
   365 code_pred (expected_modes: i => bool, o => bool) even .
   366 code_pred [dseq] even .
   367 code_pred [random_dseq] even .
   368 
   369 thm odd.equation
   370 thm even.equation
   371 thm odd.dseq_equation
   372 thm even.dseq_equation
   373 thm odd.random_dseq_equation
   374 thm even.random_dseq_equation
   375 
   376 values "{x. even 2}"
   377 values "{x. odd 2}"
   378 values 10 "{n. even n}"
   379 values 10 "{n. odd n}"
   380 values [expected "{}" dseq 2] "{x. even 6}"
   381 values [expected "{}" dseq 6] "{x. even 6}"
   382 values [expected "{()}" dseq 7] "{x. even 6}"
   383 values [dseq 2] "{x. odd 7}"
   384 values [dseq 6] "{x. odd 7}"
   385 values [dseq 7] "{x. odd 7}"
   386 values [expected "{()}" dseq 8] "{x. odd 7}"
   387 
   388 values [expected "{}" dseq 0] 8 "{x. even x}"
   389 values [expected "{0::nat}" dseq 1] 8 "{x. even x}"
   390 values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}"
   391 values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}"
   392 values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}"
   393 
   394 values [random_dseq 1, 1, 0] 8 "{x. even x}"
   395 values [random_dseq 1, 1, 1] 8 "{x. even x}"
   396 values [random_dseq 1, 1, 2] 8 "{x. even x}"
   397 values [random_dseq 1, 1, 3] 8 "{x. even x}"
   398 values [random_dseq 1, 1, 6] 8 "{x. even x}"
   399 
   400 values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}"
   401 values [random_dseq 1, 1, 8] "{x. odd 7}"
   402 values [random_dseq 1, 1, 9] "{x. odd 7}"
   403 
   404 definition odd' where "odd' x == \<not> even x"
   405 
   406 code_pred (expected_modes: i => bool) [inductify] odd' .
   407 code_pred [dseq inductify] odd' .
   408 code_pred [random_dseq inductify] odd' .
   409 
   410 values [expected "{}" dseq 2] "{x. odd' 7}"
   411 values [expected "{()}" dseq 9] "{x. odd' 7}"
   412 values [expected "{}" dseq 2] "{x. odd' 8}"
   413 values [expected "{}" dseq 10] "{x. odd' 8}"
   414 
   415 
   416 inductive is_even :: "nat \<Rightarrow> bool"
   417 where
   418   "n mod 2 = 0 \<Longrightarrow> is_even n"
   419 
   420 code_pred (expected_modes: i => bool) is_even .
   421 
   422 subsection {* append predicate *}
   423 
   424 inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
   425     "append [] xs xs"
   426   | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
   427 
   428 code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
   429   i => o => i => bool as suffix, i => i => i => bool) append .
   430 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,
   431   i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool) append .
   432 
   433 code_pred [dseq] append .
   434 code_pred [random_dseq] append .
   435 
   436 thm append.equation
   437 thm append.dseq_equation
   438 thm append.random_dseq_equation
   439 
   440 values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
   441 values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
   442 values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
   443 
   444 values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   445 values [expected "{(([]::nat list), [1, 2, 3, 4, (5::nat)])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   446 values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   447 values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   448 values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   449 values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   450 values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   451 values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   452 values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   453 values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   454 
   455 value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
   456 value [code] "Predicate.the (slice ([]::int list))"
   457 
   458 
   459 text {* tricky case with alternative rules *}
   460 
   461 inductive append2
   462 where
   463   "append2 [] xs xs"
   464 | "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
   465 
   466 lemma append2_Nil: "append2 [] (xs::'b list) xs"
   467   by (simp add: append2.intros(1))
   468 
   469 lemmas [code_pred_intro] = append2_Nil append2.intros(2)
   470 
   471 code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,
   472   i => o => i => bool, i => i => i => bool) append2
   473 proof -
   474   case append2
   475   from append2.prems show thesis
   476   proof
   477     fix xs
   478     assume "xa = []" "xb = xs" "xc = xs"
   479     from this append2(1) show thesis by simp
   480   next
   481     fix xs ys zs x
   482     assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs"
   483     from this append2(2) show thesis by fastforce
   484   qed
   485 qed
   486 
   487 inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
   488 where
   489   "tupled_append ([], xs, xs)"
   490 | "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
   491 
   492 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   493   i * o * i => bool, i * i * i => bool) tupled_append .
   494 
   495 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,
   496   i \<times> o \<times> i \<Rightarrow> bool, i \<times> i \<times> i \<Rightarrow> bool) tupled_append .
   497 
   498 code_pred [random_dseq] tupled_append .
   499 thm tupled_append.equation
   500 
   501 values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}"
   502 
   503 inductive tupled_append'
   504 where
   505 "tupled_append' ([], xs, xs)"
   506 | "[| ys = fst (xa, y); x # zs = snd (xa, y);
   507  tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
   508 
   509 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   510   i * o * i => bool, i * i * i => bool) tupled_append' .
   511 thm tupled_append'.equation
   512 
   513 inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
   514 where
   515   "tupled_append'' ([], xs, xs)"
   516 | "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
   517 
   518 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   519   i * o * i => bool, i * i * i => bool) tupled_append'' .
   520 thm tupled_append''.equation
   521 
   522 inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
   523 where
   524   "tupled_append''' ([], xs, xs)"
   525 | "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
   526 
   527 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   528   i * o * i => bool, i * i * i => bool) tupled_append''' .
   529 thm tupled_append'''.equation
   530 
   531 subsection {* map_ofP predicate *}
   532 
   533 inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   534 where
   535   "map_ofP ((a, b)#xs) a b"
   536 | "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
   537 
   538 code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .
   539 thm map_ofP.equation
   540 
   541 subsection {* filter predicate *}
   542 
   543 inductive filter1
   544 for P
   545 where
   546   "filter1 P [] []"
   547 | "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
   548 | "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
   549 
   550 code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
   551 code_pred [dseq] filter1 .
   552 code_pred [random_dseq] filter1 .
   553 
   554 thm filter1.equation
   555 
   556 values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
   557 values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
   558 values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
   559 
   560 inductive filter2
   561 where
   562   "filter2 P [] []"
   563 | "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"
   564 | "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"
   565 
   566 code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 .
   567 code_pred [dseq] filter2 .
   568 code_pred [random_dseq] filter2 .
   569 
   570 thm filter2.equation
   571 thm filter2.random_dseq_equation
   572 
   573 inductive filter3
   574 for P
   575 where
   576   "List.filter P xs = ys ==> filter3 P xs ys"
   577 
   578 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 .
   579 
   580 code_pred filter3 .
   581 thm filter3.equation
   582 
   583 (*
   584 inductive filter4
   585 where
   586   "List.filter P xs = ys ==> filter4 P xs ys"
   587 
   588 code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
   589 (*code_pred [depth_limited] filter4 .*)
   590 (*code_pred [random] filter4 .*)
   591 *)
   592 subsection {* reverse predicate *}
   593 
   594 inductive rev where
   595     "rev [] []"
   596   | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
   597 
   598 code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .
   599 
   600 thm rev.equation
   601 
   602 values "{xs. rev [0, 1, 2, 3::nat] xs}"
   603 
   604 inductive tupled_rev where
   605   "tupled_rev ([], [])"
   606 | "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"
   607 
   608 code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
   609 thm tupled_rev.equation
   610 
   611 subsection {* partition predicate *}
   612 
   613 inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   614   for f where
   615     "partition f [] [] []"
   616   | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
   617   | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
   618 
   619 code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,
   620   (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool)
   621   partition .
   622 code_pred [dseq] partition .
   623 code_pred [random_dseq] partition .
   624 
   625 values 10 "{(ys, zs). partition is_even
   626   [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
   627 values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
   628 values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
   629 
   630 inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"
   631   for f where
   632    "tupled_partition f ([], [], [])"
   633   | "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
   634   | "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"
   635 
   636 code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,
   637   (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition .
   638 
   639 thm tupled_partition.equation
   640 
   641 lemma [code_pred_intro]:
   642   "r a b \<Longrightarrow> tranclp r a b"
   643   "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
   644   by auto
   645 
   646 subsection {* transitive predicate *}
   647 
   648 text {* Also look at the tabled transitive closure in the Library *}
   649 
   650 code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
   651   (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,
   652   (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
   653 proof -
   654   case tranclp
   655   from this converse_tranclpE[OF tranclp.prems] show thesis by metis
   656 qed
   657 
   658 
   659 code_pred [dseq] tranclp .
   660 code_pred [random_dseq] tranclp .
   661 thm tranclp.equation
   662 thm tranclp.random_dseq_equation
   663 
   664 inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool" 
   665 where
   666   "rtrancl' x x r"
   667 | "r x y ==> rtrancl' y z r ==> rtrancl' x z r"
   668 
   669 code_pred [random_dseq] rtrancl' .
   670 
   671 thm rtrancl'.random_dseq_equation
   672 
   673 inductive rtrancl'' :: "('a * 'a * ('a \<Rightarrow> 'a \<Rightarrow> bool)) \<Rightarrow> bool"  
   674 where
   675   "rtrancl'' (x, x, r)"
   676 | "r x y \<Longrightarrow> rtrancl'' (y, z, r) \<Longrightarrow> rtrancl'' (x, z, r)"
   677 
   678 code_pred rtrancl'' .
   679 
   680 inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool" 
   681 where
   682   "rtrancl''' (x, (x, x), r)"
   683 | "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)"
   684 
   685 code_pred rtrancl''' .
   686 
   687 
   688 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   689     "succ 0 1"
   690   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
   691 
   692 code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ .
   693 code_pred [random_dseq] succ .
   694 thm succ.equation
   695 thm succ.random_dseq_equation
   696 
   697 values 10 "{(m, n). succ n m}"
   698 values "{m. succ 0 m}"
   699 values "{m. succ m 0}"
   700 
   701 text {* values command needs mode annotation of the parameter succ
   702 to disambiguate which mode is to be chosen. *} 
   703 
   704 values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
   705 values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
   706 values 20 "{(n, m). tranclp succ n m}"
   707 
   708 inductive example_graph :: "int => int => bool"
   709 where
   710   "example_graph 0 1"
   711 | "example_graph 1 2"
   712 | "example_graph 1 3"
   713 | "example_graph 4 7"
   714 | "example_graph 4 5"
   715 | "example_graph 5 6"
   716 | "example_graph 7 6"
   717 | "example_graph 7 8"
   718  
   719 inductive not_reachable_in_example_graph :: "int => int => bool"
   720 where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y"
   721 
   722 code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
   723 
   724 thm not_reachable_in_example_graph.equation
   725 thm tranclp.equation
   726 value "not_reachable_in_example_graph 0 3"
   727 value "not_reachable_in_example_graph 4 8"
   728 value "not_reachable_in_example_graph 5 6"
   729 text {* rtrancl compilation is strange! *}
   730 (*
   731 value "not_reachable_in_example_graph 0 4"
   732 value "not_reachable_in_example_graph 1 6"
   733 value "not_reachable_in_example_graph 8 4"*)
   734 
   735 code_pred [dseq] not_reachable_in_example_graph .
   736 
   737 values [dseq 6] "{x. tranclp example_graph 0 3}"
   738 
   739 values [dseq 0] "{x. not_reachable_in_example_graph 0 3}"
   740 values [dseq 0] "{x. not_reachable_in_example_graph 0 4}"
   741 values [dseq 20] "{x. not_reachable_in_example_graph 0 4}"
   742 values [dseq 6] "{x. not_reachable_in_example_graph 0 3}"
   743 values [dseq 3] "{x. not_reachable_in_example_graph 4 2}"
   744 values [dseq 6] "{x. not_reachable_in_example_graph 4 2}"
   745 
   746 
   747 inductive not_reachable_in_example_graph' :: "int => int => bool"
   748 where "\<not> (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y"
   749 
   750 code_pred not_reachable_in_example_graph' .
   751 
   752 value "not_reachable_in_example_graph' 0 3"
   753 (* value "not_reachable_in_example_graph' 0 5" would not terminate *)
   754 
   755 
   756 (*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*)
   757 (*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
   758 (*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*)
   759 (*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
   760 (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   761 (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   762 
   763 code_pred [dseq] not_reachable_in_example_graph' .
   764 
   765 (*thm not_reachable_in_example_graph'.dseq_equation*)
   766 
   767 (*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*)
   768 (*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
   769 (*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"
   770 values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
   771 (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   772 (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   773 
   774 subsection {* Free function variable *}
   775 
   776 inductive FF :: "nat => nat => bool"
   777 where
   778   "f x = y ==> FF x y"
   779 
   780 code_pred FF .
   781 
   782 subsection {* IMP *}
   783 
   784 type_synonym var = nat
   785 type_synonym state = "int list"
   786 
   787 datatype com =
   788   Skip |
   789   Ass var "state => int" |
   790   Seq com com |
   791   IF "state => bool" com com |
   792   While "state => bool" com
   793 
   794 inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where
   795 "tupled_exec (Skip, s, s)" |
   796 "tupled_exec (Ass x e, s, s[x := e(s)])" |
   797 "tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" |
   798 "b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
   799 "~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
   800 "~b s ==> tupled_exec (While b c, s, s)" |
   801 "b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)"
   802 
   803 code_pred tupled_exec .
   804 
   805 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)}"
   806 
   807 subsection {* CCS *}
   808 
   809 text{* This example formalizes finite CCS processes without communication or
   810 recursion. For simplicity, labels are natural numbers. *}
   811 
   812 datatype proc = nil | pre nat proc | or proc proc | par proc proc
   813 
   814 inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
   815 where
   816 "tupled_step (pre n p, n, p)" |
   817 "tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
   818 "tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
   819 "tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)" |
   820 "tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)"
   821 
   822 code_pred tupled_step .
   823 thm tupled_step.equation
   824 
   825 subsection {* divmod *}
   826 
   827 inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
   828     "k < l \<Longrightarrow> divmod_rel k l 0 k"
   829   | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
   830 
   831 code_pred divmod_rel .
   832 thm divmod_rel.equation
   833 value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
   834 
   835 subsection {* Transforming predicate logic into logic programs *}
   836 
   837 subsection {* Transforming functions into logic programs *}
   838 definition
   839   "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
   840 
   841 code_pred [inductify, skip_proof] case_f .
   842 thm case_fP.equation
   843 
   844 fun fold_map_idx where
   845   "fold_map_idx f i y [] = (y, [])"
   846 | "fold_map_idx f i y (x # xs) =
   847  (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs
   848  in (y'', x' # xs'))"
   849 
   850 code_pred [inductify] fold_map_idx .
   851 
   852 subsection {* Minimum *}
   853 
   854 definition Min
   855 where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
   856 
   857 code_pred [inductify] Min .
   858 thm Min.equation
   859 
   860 subsection {* Lexicographic order *}
   861 text {* This example requires to handle the differences of sets and predicates in the predicate compiler,
   862 or to have a copy of all definitions on predicates due to the set-predicate distinction. *}
   863 
   864 (*
   865 declare lexord_def[code_pred_def]
   866 code_pred [inductify] lexord .
   867 code_pred [random_dseq inductify] lexord .
   868 
   869 thm lexord.equation
   870 thm lexord.random_dseq_equation
   871 
   872 inductive less_than_nat :: "nat * nat => bool"
   873 where
   874   "less_than_nat (0, x)"
   875 | "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)"
   876  
   877 code_pred less_than_nat .
   878 
   879 code_pred [dseq] less_than_nat .
   880 code_pred [random_dseq] less_than_nat .
   881 
   882 inductive test_lexord :: "nat list * nat list => bool"
   883 where
   884   "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)"
   885 
   886 code_pred test_lexord .
   887 code_pred [dseq] test_lexord .
   888 code_pred [random_dseq] test_lexord .
   889 thm test_lexord.dseq_equation
   890 thm test_lexord.random_dseq_equation
   891 
   892 values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
   893 (*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*)
   894 
   895 lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
   896 (*
   897 code_pred [inductify] lexn .
   898 thm lexn.equation
   899 *)
   900 (*
   901 code_pred [random_dseq inductify] lexn .
   902 thm lexn.random_dseq_equation
   903 
   904 values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
   905 *)
   906 
   907 inductive has_length
   908 where
   909   "has_length [] 0"
   910 | "has_length xs i ==> has_length (x # xs) (Suc i)" 
   911 
   912 lemma has_length:
   913   "has_length xs n = (length xs = n)"
   914 proof (rule iffI)
   915   assume "has_length xs n"
   916   from this show "length xs = n"
   917     by (rule has_length.induct) auto
   918 next
   919   assume "length xs = n"
   920   from this show "has_length xs n"
   921     by (induct xs arbitrary: n) (auto intro: has_length.intros)
   922 qed
   923 
   924 lemma lexn_intros [code_pred_intro]:
   925   "has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)"
   926   "lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)"
   927 proof -
   928   assume "has_length xs i" "has_length ys i" "r (x, y)"
   929   from this has_length show "lexn r (Suc i) (x # xs, y # ys)"
   930     unfolding lexn_conv Collect_def mem_def
   931     by fastforce
   932 next
   933   assume "lexn r i (xs, ys)"
   934   thm lexn_conv
   935   from this show "lexn r (Suc i) (x#xs, x#ys)"
   936     unfolding Collect_def mem_def lexn_conv
   937     apply auto
   938     apply (rule_tac x="x # xys" in exI)
   939     by auto
   940 qed
   941 
   942 code_pred [random_dseq] lexn
   943 proof -
   944   fix r n xs ys
   945   assume 1: "lexn r n (xs, ys)"
   946   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"
   947   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"
   948   from 1 2 3 show thesis
   949     unfolding lexn_conv Collect_def mem_def
   950     apply (auto simp add: has_length)
   951     apply (case_tac xys)
   952     apply auto
   953     apply fastforce
   954     apply fastforce done
   955 qed
   956 
   957 values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
   958 
   959 code_pred [inductify, skip_proof] lex .
   960 thm lex.equation
   961 thm lex_def
   962 declare lenlex_conv[code_pred_def]
   963 code_pred [inductify, skip_proof] lenlex .
   964 thm lenlex.equation
   965 
   966 code_pred [random_dseq inductify] lenlex .
   967 thm lenlex.random_dseq_equation
   968 
   969 values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"
   970 
   971 thm lists.intros
   972 code_pred [inductify] lists .
   973 thm lists.equation
   974 *)
   975 subsection {* AVL Tree *}
   976 
   977 datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
   978 fun height :: "'a tree => nat" where
   979 "height ET = 0"
   980 | "height (MKT x l r h) = max (height l) (height r) + 1"
   981 
   982 primrec avl :: "'a tree => bool"
   983 where
   984   "avl ET = True"
   985 | "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> 
   986   h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
   987 (*
   988 code_pred [inductify] avl .
   989 thm avl.equation*)
   990 
   991 code_pred [new_random_dseq inductify] avl .
   992 thm avl.new_random_dseq_equation
   993 (* TODO: has highly non-deterministic execution time!
   994 
   995 values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
   996 *)
   997 fun set_of
   998 where
   999 "set_of ET = {}"
  1000 | "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
  1001 
  1002 fun is_ord :: "nat tree => bool"
  1003 where
  1004 "is_ord ET = True"
  1005 | "is_ord (MKT n l r h) =
  1006  ((\<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)"
  1007 
  1008 (* 
  1009 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
  1010 thm set_of.equation
  1011 
  1012 code_pred (expected_modes: i => bool) [inductify] is_ord .
  1013 thm is_ord_aux.equation
  1014 thm is_ord.equation
  1015 *)
  1016 subsection {* Definitions about Relations *}
  1017 (*
  1018 code_pred (modes:
  1019   (i * i => bool) => i * i => bool,
  1020   (i * o => bool) => o * i => bool,
  1021   (i * o => bool) => i * i => bool,
  1022   (o * i => bool) => i * o => bool,
  1023   (o * i => bool) => i * i => bool,
  1024   (o * o => bool) => o * o => bool,
  1025   (o * o => bool) => i * o => bool,
  1026   (o * o => bool) => o * i => bool,
  1027   (o * o => bool) => i * i => bool) [inductify] converse .
  1028 
  1029 thm converse.equation
  1030 code_pred [inductify] relcomp .
  1031 thm relcomp.equation
  1032 code_pred [inductify] Image .
  1033 thm Image.equation
  1034 declare singleton_iff[code_pred_inline]
  1035 declare Id_on_def[unfolded Bex_def UNION_eq singleton_iff, code_pred_def]
  1036 
  1037 code_pred (expected_modes:
  1038   (o => bool) => o => bool,
  1039   (o => bool) => i * o => bool,
  1040   (o => bool) => o * i => bool,
  1041   (o => bool) => i => bool,
  1042   (i => bool) => i * o => bool,
  1043   (i => bool) => o * i => bool,
  1044   (i => bool) => i => bool) [inductify] Id_on .
  1045 thm Id_on.equation
  1046 thm Domain_unfold
  1047 code_pred (modes:
  1048   (o * o => bool) => o => bool,
  1049   (o * o => bool) => i => bool,
  1050   (i * o => bool) => i => bool) [inductify] Domain .
  1051 thm Domain.equation
  1052 
  1053 thm Domain_converse [symmetric]
  1054 code_pred (modes:
  1055   (o * o => bool) => o => bool,
  1056   (o * o => bool) => i => bool,
  1057   (o * i => bool) => i => bool) [inductify] Range .
  1058 thm Range.equation
  1059 
  1060 code_pred [inductify] Field .
  1061 thm Field.equation
  1062 
  1063 thm refl_on_def
  1064 code_pred [inductify] refl_on .
  1065 thm refl_on.equation
  1066 code_pred [inductify] total_on .
  1067 thm total_on.equation
  1068 code_pred [inductify] antisym .
  1069 thm antisym.equation
  1070 code_pred [inductify] trans .
  1071 thm trans.equation
  1072 code_pred [inductify] single_valued .
  1073 thm single_valued.equation
  1074 thm inv_image_def
  1075 code_pred [inductify] inv_image .
  1076 thm inv_image.equation
  1077 *)
  1078 subsection {* Inverting list functions *}
  1079 
  1080 code_pred [inductify, skip_proof] size_list .
  1081 code_pred [new_random_dseq inductify] size_list .
  1082 thm size_listP.equation
  1083 thm size_listP.new_random_dseq_equation
  1084 
  1085 values [new_random_dseq 2,3,10] 3 "{xs. size_listP (xs::nat list) (5::nat)}"
  1086 
  1087 code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
  1088 thm concatP.equation
  1089 
  1090 values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
  1091 values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
  1092 
  1093 code_pred [dseq inductify] List.concat .
  1094 thm concatP.dseq_equation
  1095 
  1096 values [dseq 3] 3
  1097   "{xs. concatP xs ([0] :: nat list)}"
  1098 
  1099 values [dseq 5] 3
  1100   "{xs. concatP xs ([1] :: int list)}"
  1101 
  1102 values [dseq 5] 3
  1103   "{xs. concatP xs ([1] :: nat list)}"
  1104 
  1105 values [dseq 5] 3
  1106   "{xs. concatP xs [(1::int), 2]}"
  1107 
  1108 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd .
  1109 thm hdP.equation
  1110 values "{x. hdP [1, 2, (3::int)] x}"
  1111 values "{(xs, x). hdP [1, 2, (3::int)] 1}"
  1112  
  1113 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl .
  1114 thm tlP.equation
  1115 values "{x. tlP [1, 2, (3::nat)] x}"
  1116 values "{x. tlP [1, 2, (3::int)] [3]}"
  1117 
  1118 code_pred [inductify, skip_proof] last .
  1119 thm lastP.equation
  1120 
  1121 code_pred [inductify, skip_proof] butlast .
  1122 thm butlastP.equation
  1123 
  1124 code_pred [inductify, skip_proof] take .
  1125 thm takeP.equation
  1126 
  1127 code_pred [inductify, skip_proof] drop .
  1128 thm dropP.equation
  1129 code_pred [inductify, skip_proof] zip .
  1130 thm zipP.equation
  1131 
  1132 code_pred [inductify, skip_proof] upt .
  1133 (*
  1134 code_pred [inductify, skip_proof] remdups .
  1135 thm remdupsP.equation
  1136 code_pred [dseq inductify] remdups .
  1137 values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
  1138 *)
  1139 code_pred [inductify, skip_proof] remove1 .
  1140 thm remove1P.equation
  1141 values "{xs. remove1P 1 xs [2, (3::int)]}"
  1142 
  1143 code_pred [inductify, skip_proof] removeAll .
  1144 thm removeAllP.equation
  1145 code_pred [dseq inductify] removeAll .
  1146 
  1147 values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
  1148 (*
  1149 code_pred [inductify] distinct .
  1150 thm distinct.equation
  1151 *)
  1152 code_pred [inductify, skip_proof] replicate .
  1153 thm replicateP.equation
  1154 values 5 "{(n, xs). replicateP n (0::int) xs}"
  1155 
  1156 code_pred [inductify, skip_proof] splice .
  1157 thm splice.simps
  1158 thm spliceP.equation
  1159 
  1160 values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
  1161 
  1162 code_pred [inductify, skip_proof] List.rev .
  1163 code_pred [inductify] map .
  1164 code_pred [inductify] foldr .
  1165 code_pred [inductify] foldl .
  1166 code_pred [inductify] filter .
  1167 code_pred [random_dseq inductify] filter .
  1168 
  1169 section {* Function predicate replacement *}
  1170 
  1171 text {*
  1172 If the mode analysis uses the functional mode, we
  1173 replace predicates that resulted from functions again by their functions.
  1174 *}
  1175 
  1176 inductive test_append
  1177 where
  1178   "List.append xs ys = zs ==> test_append xs ys zs"
  1179 
  1180 code_pred [inductify, skip_proof] test_append .
  1181 thm test_append.equation
  1182 
  1183 text {* If append is not turned into a predicate, then the mode
  1184   o => o => i => bool could not be inferred. *}
  1185 
  1186 values 4 "{(xs::int list, ys). test_append xs ys [1, 2, 3, 4]}"
  1187 
  1188 text {* If appendP is not reverted back to a function, then mode i => i => o => bool
  1189   fails after deleting the predicate equation. *}
  1190 
  1191 declare appendP.equation[code del]
  1192 
  1193 values "{xs::int list. test_append [1,2] [3,4] xs}"
  1194 values "{xs::int list. test_append (replicate 1000 1) (replicate 1000 2) xs}"
  1195 values "{xs::int list. test_append (replicate 2000 1) (replicate 2000 2) xs}"
  1196 
  1197 text {* Redeclaring append.equation as code equation *}
  1198 
  1199 declare appendP.equation[code]
  1200 
  1201 subsection {* Function with tuples *}
  1202 
  1203 fun append'
  1204 where
  1205   "append' ([], ys) = ys"
  1206 | "append' (x # xs, ys) = x # append' (xs, ys)"
  1207 
  1208 inductive test_append'
  1209 where
  1210   "append' (xs, ys) = zs ==> test_append' xs ys zs"
  1211 
  1212 code_pred [inductify, skip_proof] test_append' .
  1213 
  1214 thm test_append'.equation
  1215 
  1216 values "{(xs::int list, ys). test_append' xs ys [1, 2, 3, 4]}"
  1217 
  1218 declare append'P.equation[code del]
  1219 
  1220 values "{zs :: int list. test_append' [1,2,3] [4,5] zs}"
  1221 
  1222 section {* Arithmetic examples *}
  1223 
  1224 subsection {* Examples on nat *}
  1225 
  1226 inductive plus_nat_test :: "nat => nat => nat => bool"
  1227 where
  1228   "x + y = z ==> plus_nat_test x y z"
  1229 
  1230 code_pred [inductify, skip_proof] plus_nat_test .
  1231 code_pred [new_random_dseq inductify] plus_nat_test .
  1232 
  1233 thm plus_nat_test.equation
  1234 thm plus_nat_test.new_random_dseq_equation
  1235 
  1236 values [expected "{9::nat}"] "{z. plus_nat_test 4 5 z}"
  1237 values [expected "{9::nat}"] "{z. plus_nat_test 7 2 z}"
  1238 values [expected "{4::nat}"] "{y. plus_nat_test 5 y 9}"
  1239 values [expected "{}"] "{y. plus_nat_test 9 y 8}"
  1240 values [expected "{6::nat}"] "{y. plus_nat_test 1 y 7}"
  1241 values [expected "{2::nat}"] "{x. plus_nat_test x 7 9}"
  1242 values [expected "{}"] "{x. plus_nat_test x 9 7}"
  1243 values [expected "{(0::nat,0::nat)}"] "{(x, y). plus_nat_test x y 0}"
  1244 values [expected "{(0::nat, 1::nat), (1, 0)}"] "{(x, y). plus_nat_test x y 1}"
  1245 values [expected "{(0::nat, 5::nat), (4, 1), (3, 2), (2, 3), (1, 4), (5, 0)}"]
  1246   "{(x, y). plus_nat_test x y 5}"
  1247 
  1248 inductive minus_nat_test :: "nat => nat => nat => bool"
  1249 where
  1250   "x - y = z ==> minus_nat_test x y z"
  1251 
  1252 code_pred [inductify, skip_proof] minus_nat_test .
  1253 code_pred [new_random_dseq inductify] minus_nat_test .
  1254 
  1255 thm minus_nat_test.equation
  1256 thm minus_nat_test.new_random_dseq_equation
  1257 
  1258 values [expected "{0::nat}"] "{z. minus_nat_test 4 5 z}"
  1259 values [expected "{5::nat}"] "{z. minus_nat_test 7 2 z}"
  1260 values [expected "{16::nat}"] "{x. minus_nat_test x 7 9}"
  1261 values [expected "{16::nat}"] "{x. minus_nat_test x 9 7}"
  1262 values [expected "{0::nat, 1, 2, 3}"] "{x. minus_nat_test x 3 0}"
  1263 values [expected "{0::nat}"] "{x. minus_nat_test x 0 0}"
  1264 
  1265 subsection {* Examples on int *}
  1266 
  1267 inductive plus_int_test :: "int => int => int => bool"
  1268 where
  1269   "a + b = c ==> plus_int_test a b c"
  1270 
  1271 code_pred [inductify, skip_proof] plus_int_test .
  1272 code_pred [new_random_dseq inductify] plus_int_test .
  1273 
  1274 thm plus_int_test.equation
  1275 thm plus_int_test.new_random_dseq_equation
  1276 
  1277 values [expected "{1::int}"] "{a. plus_int_test a 6 7}"
  1278 values [expected "{1::int}"] "{b. plus_int_test 6 b 7}"
  1279 values [expected "{11::int}"] "{c. plus_int_test 5 6 c}"
  1280 
  1281 inductive minus_int_test :: "int => int => int => bool"
  1282 where
  1283   "a - b = c ==> minus_int_test a b c"
  1284 
  1285 code_pred [inductify, skip_proof] minus_int_test .
  1286 code_pred [new_random_dseq inductify] minus_int_test .
  1287 
  1288 thm minus_int_test.equation
  1289 thm minus_int_test.new_random_dseq_equation
  1290 
  1291 values [expected "{4::int}"] "{c. minus_int_test 9 5 c}"
  1292 values [expected "{9::int}"] "{a. minus_int_test a 4 5}"
  1293 values [expected "{-1::int}"] "{b. minus_int_test 4 b 5}"
  1294 
  1295 subsection {* minus on bool *}
  1296 
  1297 inductive All :: "nat => bool"
  1298 where
  1299   "All x"
  1300 
  1301 inductive None :: "nat => bool"
  1302 
  1303 definition "test_minus_bool x = (None x - All x)"
  1304 
  1305 code_pred [inductify] test_minus_bool .
  1306 thm test_minus_bool.equation
  1307 
  1308 values "{x. test_minus_bool x}"
  1309 
  1310 subsection {* Functions *}
  1311 
  1312 fun partial_hd :: "'a list => 'a option"
  1313 where
  1314   "partial_hd [] = Option.None"
  1315 | "partial_hd (x # xs) = Some x"
  1316 
  1317 inductive hd_predicate
  1318 where
  1319   "partial_hd xs = Some x ==> hd_predicate xs x"
  1320 
  1321 code_pred (expected_modes: i => i => bool, i => o => bool) hd_predicate .
  1322 
  1323 thm hd_predicate.equation
  1324 
  1325 subsection {* Locales *}
  1326 
  1327 inductive hd_predicate2 :: "('a list => 'a option) => 'a list => 'a => bool"
  1328 where
  1329   "partial_hd' xs = Some x ==> hd_predicate2 partial_hd' xs x"
  1330 
  1331 
  1332 thm hd_predicate2.intros
  1333 
  1334 code_pred (expected_modes: i => i => i => bool, i => i => o => bool) hd_predicate2 .
  1335 thm hd_predicate2.equation
  1336 
  1337 locale A = fixes partial_hd :: "'a list => 'a option" begin
  1338 
  1339 inductive hd_predicate_in_locale :: "'a list => 'a => bool"
  1340 where
  1341   "partial_hd xs = Some x ==> hd_predicate_in_locale xs x"
  1342 
  1343 end
  1344 
  1345 text {* The global introduction rules must be redeclared as introduction rules and then 
  1346   one could invoke code_pred. *}
  1347 
  1348 declare A.hd_predicate_in_locale.intros [code_pred_intro]
  1349 
  1350 code_pred (expected_modes: i => i => i => bool, i => i => o => bool) A.hd_predicate_in_locale
  1351 by (auto elim: A.hd_predicate_in_locale.cases)
  1352     
  1353 interpretation A partial_hd .
  1354 thm hd_predicate_in_locale.intros
  1355 text {* A locally compliant solution with a trivial interpretation fails, because
  1356 the predicate compiler has very strict assumptions about the terms and their structure. *}
  1357  
  1358 (*code_pred hd_predicate_in_locale .*)
  1359 
  1360 section {* Integer example *}
  1361 
  1362 definition three :: int
  1363 where "three = 3"
  1364 
  1365 inductive is_three
  1366 where
  1367   "is_three three"
  1368 
  1369 code_pred is_three .
  1370 
  1371 thm is_three.equation
  1372 
  1373 section {* String.literal example *}
  1374 
  1375 definition Error_1
  1376 where
  1377   "Error_1 = STR ''Error 1''"
  1378 
  1379 definition Error_2
  1380 where
  1381   "Error_2 = STR ''Error 2''"
  1382 
  1383 inductive "is_error" :: "String.literal \<Rightarrow> bool"
  1384 where
  1385   "is_error Error_1"
  1386 | "is_error Error_2"
  1387 
  1388 code_pred is_error .
  1389 
  1390 thm is_error.equation
  1391 
  1392 inductive is_error' :: "String.literal \<Rightarrow> bool"
  1393 where
  1394   "is_error' (STR ''Error1'')"
  1395 | "is_error' (STR ''Error2'')"
  1396 
  1397 code_pred is_error' .
  1398 
  1399 thm is_error'.equation
  1400 
  1401 datatype ErrorObject = Error String.literal int
  1402 
  1403 inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
  1404 where
  1405   "is_error'' (Error Error_1 3)"
  1406 | "is_error'' (Error Error_2 4)"
  1407 
  1408 code_pred is_error'' .
  1409 
  1410 thm is_error''.equation
  1411 
  1412 section {* Another function example *}
  1413 
  1414 consts f :: "'a \<Rightarrow> 'a"
  1415 
  1416 inductive fun_upd :: "(('a * 'b) * ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  1417 where
  1418   "fun_upd ((x, a), s) (s(x := f a))"
  1419 
  1420 code_pred fun_upd .
  1421 
  1422 thm fun_upd.equation
  1423 
  1424 section {* Examples for detecting switches *}
  1425 
  1426 inductive detect_switches1 where
  1427   "detect_switches1 [] []"
  1428 | "detect_switches1 (x # xs) (y # ys)"
  1429 
  1430 code_pred [detect_switches, skip_proof] detect_switches1 .
  1431 
  1432 thm detect_switches1.equation
  1433 
  1434 inductive detect_switches2 :: "('a => bool) => bool"
  1435 where
  1436   "detect_switches2 P"
  1437 
  1438 code_pred [detect_switches, skip_proof] detect_switches2 .
  1439 thm detect_switches2.equation
  1440 
  1441 inductive detect_switches3 :: "('a => bool) => 'a list => bool"
  1442 where
  1443   "detect_switches3 P []"
  1444 | "detect_switches3 P (x # xs)" 
  1445 
  1446 code_pred [detect_switches, skip_proof] detect_switches3 .
  1447 
  1448 thm detect_switches3.equation
  1449 
  1450 inductive detect_switches4 :: "('a => bool) => 'a list => 'a list => bool"
  1451 where
  1452   "detect_switches4 P [] []"
  1453 | "detect_switches4 P (x # xs) (y # ys)"
  1454 
  1455 code_pred [detect_switches, skip_proof] detect_switches4 .
  1456 thm detect_switches4.equation
  1457 
  1458 inductive detect_switches5 :: "('a => 'a => bool) => 'a list => 'a list => bool"
  1459 where
  1460   "detect_switches5 P [] []"
  1461 | "detect_switches5 P xs ys ==> P x y ==> detect_switches5 P (x # xs) (y # ys)"
  1462 
  1463 code_pred [detect_switches, skip_proof] detect_switches5 .
  1464 
  1465 thm detect_switches5.equation
  1466 
  1467 inductive detect_switches6 :: "(('a => 'b => bool) * 'a list * 'b list) => bool"
  1468 where
  1469   "detect_switches6 (P, [], [])"
  1470 | "detect_switches6 (P, xs, ys) ==> P x y ==> detect_switches6 (P, x # xs, y # ys)"
  1471 
  1472 code_pred [detect_switches, skip_proof] detect_switches6 .
  1473 
  1474 inductive detect_switches7 :: "('a => bool) => ('b => bool) => ('a * 'b list) => bool"
  1475 where
  1476   "detect_switches7 P Q (a, [])"
  1477 | "P a ==> Q x ==> detect_switches7 P Q (a, x#xs)"
  1478 
  1479 code_pred [skip_proof] detect_switches7 .
  1480 
  1481 thm detect_switches7.equation
  1482 
  1483 inductive detect_switches8 :: "nat => bool"
  1484 where
  1485   "detect_switches8 0"
  1486 | "x mod 2 = 0 ==> detect_switches8 (Suc x)"
  1487 
  1488 code_pred [detect_switches, skip_proof] detect_switches8 .
  1489 
  1490 thm detect_switches8.equation
  1491 
  1492 inductive detect_switches9 :: "nat => nat => bool"
  1493 where
  1494   "detect_switches9 0 0"
  1495 | "detect_switches9 0 (Suc x)"
  1496 | "detect_switches9 (Suc x) 0"
  1497 | "x = y ==> detect_switches9 (Suc x) (Suc y)"
  1498 | "c1 = c2 ==> detect_switches9 c1 c2"
  1499 
  1500 code_pred [detect_switches, skip_proof] detect_switches9 .
  1501 
  1502 thm detect_switches9.equation
  1503 
  1504 text {* The higher-order predicate r is in an output term *}
  1505 
  1506 datatype result = Result bool
  1507 
  1508 inductive fixed_relation :: "'a => bool"
  1509 
  1510 inductive test_relation_in_output_terms :: "('a => bool) => 'a => result => bool"
  1511 where
  1512   "test_relation_in_output_terms r x (Result (r x))"
  1513 | "test_relation_in_output_terms r x (Result (fixed_relation x))"
  1514 
  1515 code_pred test_relation_in_output_terms .
  1516 
  1517 thm test_relation_in_output_terms.equation
  1518 
  1519 
  1520 text {*
  1521   We want that the argument r is not treated as a higher-order relation, but simply as input.
  1522 *}
  1523 
  1524 inductive test_uninterpreted_relation :: "('a => bool) => 'a list => bool"
  1525 where
  1526   "list_all r xs ==> test_uninterpreted_relation r xs"
  1527 
  1528 code_pred (modes: i => i => bool) test_uninterpreted_relation .
  1529 
  1530 thm test_uninterpreted_relation.equation
  1531 
  1532 inductive list_ex'
  1533 where
  1534   "P x ==> list_ex' P (x#xs)"
  1535 | "list_ex' P xs ==> list_ex' P (x#xs)"
  1536 
  1537 code_pred list_ex' .
  1538 
  1539 inductive test_uninterpreted_relation2 :: "('a => bool) => 'a list => bool"
  1540 where
  1541   "list_ex r xs ==> test_uninterpreted_relation2 r xs"
  1542 | "list_ex' r xs ==> test_uninterpreted_relation2 r xs"
  1543 
  1544 text {* Proof procedure cannot handle this situation yet. *}
  1545 
  1546 code_pred (modes: i => i => bool) [skip_proof] test_uninterpreted_relation2 .
  1547 
  1548 thm test_uninterpreted_relation2.equation
  1549 
  1550 
  1551 text {* Trivial predicate *}
  1552 
  1553 inductive implies_itself :: "'a => bool"
  1554 where
  1555   "implies_itself x ==> implies_itself x"
  1556 
  1557 code_pred implies_itself .
  1558 
  1559 text {* Case expressions *}
  1560 
  1561 definition
  1562   "map_pairs xs ys = (map (%((a, b), c). (a, b, c)) xs = ys)"
  1563 
  1564 code_pred [inductify] map_pairs .
  1565 
  1566 end