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