src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
author haftmann
Thu Dec 02 16:39:07 2010 +0100 (2010-12-02)
changeset 40885 da4bdafeef7c
parent 40137 9eabcb1bfe50
child 41413 64cd30d6b0b8
permissions -rw-r--r--
adapted expected value to more idiomatic numeral representation
     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: bool) False'' .
    74 
    75 inductive EmptySet'' :: "'a \<Rightarrow> bool"
    76 where
    77   "False \<Longrightarrow> EmptySet'' x"
    78 
    79 code_pred (expected_modes: i => bool, o => bool) [inductify] EmptySet'' .
    80 *)
    81 
    82 consts a' :: 'a
    83 
    84 inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    85 where
    86 "Fact a' a'"
    87 
    88 code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
    89 
    90 inductive zerozero :: "nat * nat => bool"
    91 where
    92   "zerozero (0, 0)"
    93 
    94 code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .
    95 code_pred [dseq] zerozero .
    96 code_pred [random_dseq] zerozero .
    97 
    98 thm zerozero.equation
    99 thm zerozero.dseq_equation
   100 thm zerozero.random_dseq_equation
   101 
   102 text {* We expect the user to expand the tuples in the values command.
   103 The following values command is not supported. *}
   104 (*values "{x. zerozero x}" *)
   105 text {* Instead, the user must type *}
   106 values "{(x, y). zerozero (x, y)}"
   107 
   108 values [expected "{}" dseq 0] "{(x, y). zerozero (x, y)}"
   109 values [expected "{(0::nat, 0::nat)}" dseq 1] "{(x, y). zerozero (x, y)}"
   110 values [expected "{(0::nat, 0::nat)}" dseq 2] "{(x, y). zerozero (x, y)}"
   111 values [expected "{}" random_dseq 1, 1, 2] "{(x, y). zerozero (x, y)}"
   112 values [expected "{(0::nat, 0:: nat)}" random_dseq 1, 1, 3] "{(x, y). zerozero (x, y)}"
   113 
   114 inductive nested_tuples :: "((int * int) * int * int) => bool"
   115 where
   116   "nested_tuples ((0, 1), 2, 3)"
   117 
   118 code_pred nested_tuples .
   119 
   120 inductive JamesBond :: "nat => int => code_numeral => bool"
   121 where
   122   "JamesBond 0 0 7"
   123 
   124 code_pred JamesBond .
   125 
   126 values [expected "{(0::nat, 0::int , 7::code_numeral)}"] "{(a, b, c). JamesBond a b c}"
   127 values [expected "{(0::nat, 7::code_numeral, 0:: int)}"] "{(a, c, b). JamesBond a b c}"
   128 values [expected "{(0::int, 0::nat, 7::code_numeral)}"] "{(b, a, c). JamesBond a b c}"
   129 values [expected "{(0::int, 7::code_numeral, 0::nat)}"] "{(b, c, a). JamesBond a b c}"
   130 values [expected "{(7::code_numeral, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}"
   131 values [expected "{(7::code_numeral, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}"
   132 
   133 values [expected "{(7::code_numeral, 0::int)}"] "{(a, b). JamesBond 0 b a}"
   134 values [expected "{(7::code_numeral, 0::nat)}"] "{(c, a). JamesBond a 0 c}"
   135 values [expected "{(0::nat, 7::code_numeral)}"] "{(a, c). JamesBond a 0 c}"
   136 
   137 
   138 subsection {* Alternative Rules *}
   139 
   140 datatype char = C | D | E | F | G | H
   141 
   142 inductive is_C_or_D
   143 where
   144   "(x = C) \<or> (x = D) ==> is_C_or_D x"
   145 
   146 code_pred (expected_modes: i => bool) is_C_or_D .
   147 thm is_C_or_D.equation
   148 
   149 inductive is_D_or_E
   150 where
   151   "(x = D) \<or> (x = E) ==> is_D_or_E x"
   152 
   153 lemma [code_pred_intro]:
   154   "is_D_or_E D"
   155 by (auto intro: is_D_or_E.intros)
   156 
   157 lemma [code_pred_intro]:
   158   "is_D_or_E E"
   159 by (auto intro: is_D_or_E.intros)
   160 
   161 code_pred (expected_modes: o => bool, i => bool) is_D_or_E
   162 proof -
   163   case is_D_or_E
   164   from is_D_or_E.prems show thesis
   165   proof 
   166     fix xa
   167     assume x: "x = xa"
   168     assume "xa = D \<or> xa = E"
   169     from this show thesis
   170     proof
   171       assume "xa = D" from this x is_D_or_E(1) show thesis by simp
   172     next
   173       assume "xa = E" from this x is_D_or_E(2) show thesis by simp
   174     qed
   175   qed
   176 qed
   177 
   178 thm is_D_or_E.equation
   179 
   180 inductive is_F_or_G
   181 where
   182   "x = F \<or> x = G ==> is_F_or_G x"
   183 
   184 lemma [code_pred_intro]:
   185   "is_F_or_G F"
   186 by (auto intro: is_F_or_G.intros)
   187 
   188 lemma [code_pred_intro]:
   189   "is_F_or_G G"
   190 by (auto intro: is_F_or_G.intros)
   191 
   192 inductive is_FGH
   193 where
   194   "is_F_or_G x ==> is_FGH x"
   195 | "is_FGH H"
   196 
   197 text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}
   198 
   199 code_pred (expected_modes: o => bool, i => bool) is_FGH
   200 proof -
   201   case is_F_or_G
   202   from is_F_or_G.prems show thesis
   203   proof
   204     fix xa
   205     assume x: "x = xa"
   206     assume "xa = F \<or> xa = G"
   207     from this show thesis
   208     proof
   209       assume "xa = F"
   210       from this x is_F_or_G(1) show thesis by simp
   211     next
   212       assume "xa = G"
   213       from this x is_F_or_G(2) show thesis by simp
   214     qed
   215   qed
   216 qed
   217 
   218 subsection {* Named alternative rules *}
   219 
   220 inductive appending
   221 where
   222   nil: "appending [] ys ys"
   223 | cons: "appending xs ys zs \<Longrightarrow> appending (x#xs) ys (x#zs)"
   224 
   225 lemma appending_alt_nil: "ys = zs \<Longrightarrow> appending [] ys zs"
   226 by (auto intro: appending.intros)
   227 
   228 lemma appending_alt_cons: "xs' = x # xs \<Longrightarrow> appending xs ys zs \<Longrightarrow> zs' = x # zs \<Longrightarrow> appending xs' ys zs'"
   229 by (auto intro: appending.intros)
   230 
   231 text {* With code_pred_intro, we can give fact names to the alternative rules,
   232   which are used for the code_pred command. *}
   233 
   234 declare appending_alt_nil[code_pred_intro alt_nil] appending_alt_cons[code_pred_intro alt_cons]
   235  
   236 code_pred appending
   237 proof -
   238   case appending
   239   from appending.prems show thesis
   240   proof(cases)
   241     case nil
   242     from alt_nil nil show thesis by auto
   243   next
   244     case cons
   245     from alt_cons cons show thesis by fastsimp
   246   qed
   247 qed
   248 
   249 
   250 inductive ya_even and ya_odd :: "nat => bool"
   251 where
   252   even_zero: "ya_even 0"
   253 | odd_plus1: "ya_even x ==> ya_odd (x + 1)"
   254 | even_plus1: "ya_odd x ==> ya_even (x + 1)"
   255 
   256 
   257 declare even_zero[code_pred_intro even_0]
   258 
   259 lemma [code_pred_intro odd_Suc]: "ya_even x ==> ya_odd (Suc x)"
   260 by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)
   261 
   262 lemma [code_pred_intro even_Suc]:"ya_odd x ==> ya_even (Suc x)"
   263 by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)
   264 
   265 code_pred ya_even
   266 proof -
   267   case ya_even
   268   from ya_even.prems show thesis
   269   proof (cases)
   270     case even_zero
   271     from even_zero even_0 show thesis by simp
   272   next
   273     case even_plus1
   274     from even_plus1 even_Suc show thesis by simp
   275   qed
   276 next
   277   case ya_odd
   278   from ya_odd.prems show thesis
   279   proof (cases)
   280     case odd_plus1
   281     from odd_plus1 odd_Suc show thesis by simp
   282   qed
   283 qed
   284 
   285 subsection {* Preprocessor Inlining  *}
   286 
   287 definition "equals == (op =)"
   288  
   289 inductive zerozero' :: "nat * nat => bool" where
   290   "equals (x, y) (0, 0) ==> zerozero' (x, y)"
   291 
   292 code_pred (expected_modes: i => bool) zerozero' .
   293 
   294 lemma zerozero'_eq: "zerozero' x == zerozero x"
   295 proof -
   296   have "zerozero' = zerozero"
   297     apply (auto simp add: mem_def)
   298     apply (cases rule: zerozero'.cases)
   299     apply (auto simp add: equals_def intro: zerozero.intros)
   300     apply (cases rule: zerozero.cases)
   301     apply (auto simp add: equals_def intro: zerozero'.intros)
   302     done
   303   from this show "zerozero' x == zerozero x" by auto
   304 qed
   305 
   306 declare zerozero'_eq [code_pred_inline]
   307 
   308 definition "zerozero'' x == zerozero' x"
   309 
   310 text {* if preprocessing fails, zerozero'' will not have all modes. *}
   311 
   312 code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
   313 
   314 subsection {* Sets and Numerals *}
   315 
   316 definition
   317   "one_or_two = {Suc 0, (Suc (Suc 0))}"
   318 
   319 code_pred [inductify] one_or_two .
   320 
   321 code_pred [dseq] one_or_two .
   322 code_pred [random_dseq] one_or_two .
   323 thm one_or_two.dseq_equation
   324 values [expected "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}"
   325 values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
   326 
   327 inductive one_or_two' :: "nat => bool"
   328 where
   329   "one_or_two' 1"
   330 | "one_or_two' 2"
   331 
   332 code_pred one_or_two' .
   333 thm one_or_two'.equation
   334 
   335 values "{x. one_or_two' x}"
   336 
   337 definition one_or_two'':
   338   "one_or_two'' == {1, (2::nat)}"
   339 
   340 code_pred [inductify] one_or_two'' .
   341 thm one_or_two''.equation
   342 
   343 values "{x. one_or_two'' x}"
   344 
   345 subsection {* even predicate *}
   346 
   347 inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
   348     "even 0"
   349   | "even n \<Longrightarrow> odd (Suc n)"
   350   | "odd n \<Longrightarrow> even (Suc n)"
   351 
   352 code_pred (expected_modes: i => bool, o => bool) even .
   353 code_pred [dseq] even .
   354 code_pred [random_dseq] even .
   355 
   356 thm odd.equation
   357 thm even.equation
   358 thm odd.dseq_equation
   359 thm even.dseq_equation
   360 thm odd.random_dseq_equation
   361 thm even.random_dseq_equation
   362 
   363 values "{x. even 2}"
   364 values "{x. odd 2}"
   365 values 10 "{n. even n}"
   366 values 10 "{n. odd n}"
   367 values [expected "{}" dseq 2] "{x. even 6}"
   368 values [expected "{}" dseq 6] "{x. even 6}"
   369 values [expected "{()}" dseq 7] "{x. even 6}"
   370 values [dseq 2] "{x. odd 7}"
   371 values [dseq 6] "{x. odd 7}"
   372 values [dseq 7] "{x. odd 7}"
   373 values [expected "{()}" dseq 8] "{x. odd 7}"
   374 
   375 values [expected "{}" dseq 0] 8 "{x. even x}"
   376 values [expected "{0::nat}" dseq 1] 8 "{x. even x}"
   377 values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}"
   378 values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}"
   379 values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}"
   380 
   381 values [random_dseq 1, 1, 0] 8 "{x. even x}"
   382 values [random_dseq 1, 1, 1] 8 "{x. even x}"
   383 values [random_dseq 1, 1, 2] 8 "{x. even x}"
   384 values [random_dseq 1, 1, 3] 8 "{x. even x}"
   385 values [random_dseq 1, 1, 6] 8 "{x. even x}"
   386 
   387 values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}"
   388 values [random_dseq 1, 1, 8] "{x. odd 7}"
   389 values [random_dseq 1, 1, 9] "{x. odd 7}"
   390 
   391 definition odd' where "odd' x == \<not> even x"
   392 
   393 code_pred (expected_modes: i => bool) [inductify] odd' .
   394 code_pred [dseq inductify] odd' .
   395 code_pred [random_dseq inductify] odd' .
   396 
   397 values [expected "{}" dseq 2] "{x. odd' 7}"
   398 values [expected "{()}" dseq 9] "{x. odd' 7}"
   399 values [expected "{}" dseq 2] "{x. odd' 8}"
   400 values [expected "{}" dseq 10] "{x. odd' 8}"
   401 
   402 
   403 inductive is_even :: "nat \<Rightarrow> bool"
   404 where
   405   "n mod 2 = 0 \<Longrightarrow> is_even n"
   406 
   407 code_pred (expected_modes: i => bool) is_even .
   408 
   409 subsection {* append predicate *}
   410 
   411 inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
   412     "append [] xs xs"
   413   | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
   414 
   415 code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
   416   i => o => i => bool as suffix, i => i => i => bool) append .
   417 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,
   418   i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool) append .
   419 
   420 code_pred [dseq] append .
   421 code_pred [random_dseq] append .
   422 
   423 thm append.equation
   424 thm append.dseq_equation
   425 thm append.random_dseq_equation
   426 
   427 values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
   428 values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
   429 values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
   430 
   431 values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   432 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)]}"
   433 values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   434 values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   435 values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   436 values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   437 values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   438 values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   439 values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   440 values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   441 
   442 value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
   443 value [code] "Predicate.the (slice ([]::int list))"
   444 
   445 
   446 text {* tricky case with alternative rules *}
   447 
   448 inductive append2
   449 where
   450   "append2 [] xs xs"
   451 | "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
   452 
   453 lemma append2_Nil: "append2 [] (xs::'b list) xs"
   454   by (simp add: append2.intros(1))
   455 
   456 lemmas [code_pred_intro] = append2_Nil append2.intros(2)
   457 
   458 code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,
   459   i => o => i => bool, i => i => i => bool) append2
   460 proof -
   461   case append2
   462   from append2.prems show thesis
   463   proof
   464     fix xs
   465     assume "xa = []" "xb = xs" "xc = xs"
   466     from this append2(1) show thesis by simp
   467   next
   468     fix xs ys zs x
   469     assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs"
   470     from this append2(2) show thesis by fastsimp
   471   qed
   472 qed
   473 
   474 inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
   475 where
   476   "tupled_append ([], xs, xs)"
   477 | "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
   478 
   479 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   480   i * o * i => bool, i * i * i => bool) tupled_append .
   481 
   482 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,
   483   i \<times> o \<times> i \<Rightarrow> bool, i \<times> i \<times> i \<Rightarrow> bool) tupled_append .
   484 
   485 code_pred [random_dseq] tupled_append .
   486 thm tupled_append.equation
   487 
   488 values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}"
   489 
   490 inductive tupled_append'
   491 where
   492 "tupled_append' ([], xs, xs)"
   493 | "[| ys = fst (xa, y); x # zs = snd (xa, y);
   494  tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
   495 
   496 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   497   i * o * i => bool, i * i * i => bool) tupled_append' .
   498 thm tupled_append'.equation
   499 
   500 inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
   501 where
   502   "tupled_append'' ([], xs, xs)"
   503 | "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
   504 
   505 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   506   i * o * i => bool, i * i * i => bool) tupled_append'' .
   507 thm tupled_append''.equation
   508 
   509 inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
   510 where
   511   "tupled_append''' ([], xs, xs)"
   512 | "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
   513 
   514 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   515   i * o * i => bool, i * i * i => bool) tupled_append''' .
   516 thm tupled_append'''.equation
   517 
   518 subsection {* map_ofP predicate *}
   519 
   520 inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   521 where
   522   "map_ofP ((a, b)#xs) a b"
   523 | "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
   524 
   525 code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .
   526 thm map_ofP.equation
   527 
   528 subsection {* filter predicate *}
   529 
   530 inductive filter1
   531 for P
   532 where
   533   "filter1 P [] []"
   534 | "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
   535 | "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
   536 
   537 code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
   538 code_pred [dseq] filter1 .
   539 code_pred [random_dseq] filter1 .
   540 
   541 thm filter1.equation
   542 
   543 values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
   544 values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
   545 values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
   546 
   547 inductive filter2
   548 where
   549   "filter2 P [] []"
   550 | "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"
   551 | "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"
   552 
   553 code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 .
   554 code_pred [dseq] filter2 .
   555 code_pred [random_dseq] filter2 .
   556 
   557 thm filter2.equation
   558 thm filter2.random_dseq_equation
   559 
   560 inductive filter3
   561 for P
   562 where
   563   "List.filter P xs = ys ==> filter3 P xs ys"
   564 
   565 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 .
   566 
   567 code_pred filter3 .
   568 thm filter3.equation
   569 
   570 (*
   571 inductive filter4
   572 where
   573   "List.filter P xs = ys ==> filter4 P xs ys"
   574 
   575 code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
   576 (*code_pred [depth_limited] filter4 .*)
   577 (*code_pred [random] filter4 .*)
   578 *)
   579 subsection {* reverse predicate *}
   580 
   581 inductive rev where
   582     "rev [] []"
   583   | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
   584 
   585 code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .
   586 
   587 thm rev.equation
   588 
   589 values "{xs. rev [0, 1, 2, 3::nat] xs}"
   590 
   591 inductive tupled_rev where
   592   "tupled_rev ([], [])"
   593 | "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"
   594 
   595 code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
   596 thm tupled_rev.equation
   597 
   598 subsection {* partition predicate *}
   599 
   600 inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   601   for f where
   602     "partition f [] [] []"
   603   | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
   604   | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
   605 
   606 code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,
   607   (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool)
   608   partition .
   609 code_pred [dseq] partition .
   610 code_pred [random_dseq] partition .
   611 
   612 values 10 "{(ys, zs). partition is_even
   613   [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
   614 values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
   615 values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
   616 
   617 inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"
   618   for f where
   619    "tupled_partition f ([], [], [])"
   620   | "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
   621   | "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"
   622 
   623 code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,
   624   (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition .
   625 
   626 thm tupled_partition.equation
   627 
   628 lemma [code_pred_intro]:
   629   "r a b \<Longrightarrow> tranclp r a b"
   630   "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
   631   by auto
   632 
   633 subsection {* transitive predicate *}
   634 
   635 text {* Also look at the tabled transitive closure in the Library *}
   636 
   637 code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
   638   (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,
   639   (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
   640 proof -
   641   case tranclp
   642   from this converse_tranclpE[OF tranclp.prems] show thesis by metis
   643 qed
   644 
   645 
   646 code_pred [dseq] tranclp .
   647 code_pred [random_dseq] tranclp .
   648 thm tranclp.equation
   649 thm tranclp.random_dseq_equation
   650 
   651 inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool" 
   652 where
   653   "rtrancl' x x r"
   654 | "r x y ==> rtrancl' y z r ==> rtrancl' x z r"
   655 
   656 code_pred [random_dseq] rtrancl' .
   657 
   658 thm rtrancl'.random_dseq_equation
   659 
   660 inductive rtrancl'' :: "('a * 'a * ('a \<Rightarrow> 'a \<Rightarrow> bool)) \<Rightarrow> bool"  
   661 where
   662   "rtrancl'' (x, x, r)"
   663 | "r x y \<Longrightarrow> rtrancl'' (y, z, r) \<Longrightarrow> rtrancl'' (x, z, r)"
   664 
   665 code_pred rtrancl'' .
   666 
   667 inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool" 
   668 where
   669   "rtrancl''' (x, (x, x), r)"
   670 | "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)"
   671 
   672 code_pred rtrancl''' .
   673 
   674 
   675 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   676     "succ 0 1"
   677   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
   678 
   679 code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ .
   680 code_pred [random_dseq] succ .
   681 thm succ.equation
   682 thm succ.random_dseq_equation
   683 
   684 values 10 "{(m, n). succ n m}"
   685 values "{m. succ 0 m}"
   686 values "{m. succ m 0}"
   687 
   688 text {* values command needs mode annotation of the parameter succ
   689 to disambiguate which mode is to be chosen. *} 
   690 
   691 values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
   692 values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
   693 values 20 "{(n, m). tranclp succ n m}"
   694 
   695 inductive example_graph :: "int => int => bool"
   696 where
   697   "example_graph 0 1"
   698 | "example_graph 1 2"
   699 | "example_graph 1 3"
   700 | "example_graph 4 7"
   701 | "example_graph 4 5"
   702 | "example_graph 5 6"
   703 | "example_graph 7 6"
   704 | "example_graph 7 8"
   705  
   706 inductive not_reachable_in_example_graph :: "int => int => bool"
   707 where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y"
   708 
   709 code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
   710 
   711 thm not_reachable_in_example_graph.equation
   712 thm tranclp.equation
   713 value "not_reachable_in_example_graph 0 3"
   714 value "not_reachable_in_example_graph 4 8"
   715 value "not_reachable_in_example_graph 5 6"
   716 text {* rtrancl compilation is strange! *}
   717 (*
   718 value "not_reachable_in_example_graph 0 4"
   719 value "not_reachable_in_example_graph 1 6"
   720 value "not_reachable_in_example_graph 8 4"*)
   721 
   722 code_pred [dseq] not_reachable_in_example_graph .
   723 
   724 values [dseq 6] "{x. tranclp example_graph 0 3}"
   725 
   726 values [dseq 0] "{x. not_reachable_in_example_graph 0 3}"
   727 values [dseq 0] "{x. not_reachable_in_example_graph 0 4}"
   728 values [dseq 20] "{x. not_reachable_in_example_graph 0 4}"
   729 values [dseq 6] "{x. not_reachable_in_example_graph 0 3}"
   730 values [dseq 3] "{x. not_reachable_in_example_graph 4 2}"
   731 values [dseq 6] "{x. not_reachable_in_example_graph 4 2}"
   732 
   733 
   734 inductive not_reachable_in_example_graph' :: "int => int => bool"
   735 where "\<not> (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y"
   736 
   737 code_pred not_reachable_in_example_graph' .
   738 
   739 value "not_reachable_in_example_graph' 0 3"
   740 (* value "not_reachable_in_example_graph' 0 5" would not terminate *)
   741 
   742 
   743 (*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*)
   744 (*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
   745 (*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*)
   746 (*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
   747 (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   748 (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   749 
   750 code_pred [dseq] not_reachable_in_example_graph' .
   751 
   752 (*thm not_reachable_in_example_graph'.dseq_equation*)
   753 
   754 (*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*)
   755 (*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
   756 (*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"
   757 values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
   758 (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   759 (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   760 
   761 subsection {* Free function variable *}
   762 
   763 inductive FF :: "nat => nat => bool"
   764 where
   765   "f x = y ==> FF x y"
   766 
   767 code_pred FF .
   768 
   769 subsection {* IMP *}
   770 
   771 types
   772   var = nat
   773   state = "int list"
   774 
   775 datatype com =
   776   Skip |
   777   Ass var "state => int" |
   778   Seq com com |
   779   IF "state => bool" com com |
   780   While "state => bool" com
   781 
   782 inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where
   783 "tupled_exec (Skip, s, s)" |
   784 "tupled_exec (Ass x e, s, s[x := e(s)])" |
   785 "tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" |
   786 "b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
   787 "~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
   788 "~b s ==> tupled_exec (While b c, s, s)" |
   789 "b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)"
   790 
   791 code_pred tupled_exec .
   792 
   793 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)}"
   794 
   795 subsection {* CCS *}
   796 
   797 text{* This example formalizes finite CCS processes without communication or
   798 recursion. For simplicity, labels are natural numbers. *}
   799 
   800 datatype proc = nil | pre nat proc | or proc proc | par proc proc
   801 
   802 inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
   803 where
   804 "tupled_step (pre n p, n, p)" |
   805 "tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
   806 "tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
   807 "tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)" |
   808 "tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)"
   809 
   810 code_pred tupled_step .
   811 thm tupled_step.equation
   812 
   813 subsection {* divmod *}
   814 
   815 inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
   816     "k < l \<Longrightarrow> divmod_rel k l 0 k"
   817   | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
   818 
   819 code_pred divmod_rel .
   820 thm divmod_rel.equation
   821 value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
   822 
   823 subsection {* Transforming predicate logic into logic programs *}
   824 
   825 subsection {* Transforming functions into logic programs *}
   826 definition
   827   "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
   828 
   829 code_pred [inductify, skip_proof] case_f .
   830 thm case_fP.equation
   831 
   832 fun fold_map_idx where
   833   "fold_map_idx f i y [] = (y, [])"
   834 | "fold_map_idx f i y (x # xs) =
   835  (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs
   836  in (y'', x' # xs'))"
   837 
   838 code_pred [inductify] fold_map_idx .
   839 
   840 subsection {* Minimum *}
   841 
   842 definition Min
   843 where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
   844 
   845 code_pred [inductify] Min .
   846 thm Min.equation
   847 
   848 subsection {* Lexicographic order *}
   849 
   850 declare lexord_def[code_pred_def]
   851 code_pred [inductify] lexord .
   852 code_pred [random_dseq inductify] lexord .
   853 
   854 thm lexord.equation
   855 thm lexord.random_dseq_equation
   856 
   857 inductive less_than_nat :: "nat * nat => bool"
   858 where
   859   "less_than_nat (0, x)"
   860 | "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)"
   861  
   862 code_pred less_than_nat .
   863 
   864 code_pred [dseq] less_than_nat .
   865 code_pred [random_dseq] less_than_nat .
   866 
   867 inductive test_lexord :: "nat list * nat list => bool"
   868 where
   869   "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)"
   870 
   871 code_pred test_lexord .
   872 code_pred [dseq] test_lexord .
   873 code_pred [random_dseq] test_lexord .
   874 thm test_lexord.dseq_equation
   875 thm test_lexord.random_dseq_equation
   876 
   877 values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
   878 (*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*)
   879 
   880 lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
   881 (*
   882 code_pred [inductify] lexn .
   883 thm lexn.equation
   884 *)
   885 (*
   886 code_pred [random_dseq inductify] lexn .
   887 thm lexn.random_dseq_equation
   888 
   889 values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
   890 *)
   891 inductive has_length
   892 where
   893   "has_length [] 0"
   894 | "has_length xs i ==> has_length (x # xs) (Suc i)" 
   895 
   896 lemma has_length:
   897   "has_length xs n = (length xs = n)"
   898 proof (rule iffI)
   899   assume "has_length xs n"
   900   from this show "length xs = n"
   901     by (rule has_length.induct) auto
   902 next
   903   assume "length xs = n"
   904   from this show "has_length xs n"
   905     by (induct xs arbitrary: n) (auto intro: has_length.intros)
   906 qed
   907 
   908 lemma lexn_intros [code_pred_intro]:
   909   "has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)"
   910   "lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)"
   911 proof -
   912   assume "has_length xs i" "has_length ys i" "r (x, y)"
   913   from this has_length show "lexn r (Suc i) (x # xs, y # ys)"
   914     unfolding lexn_conv Collect_def mem_def
   915     by fastsimp
   916 next
   917   assume "lexn r i (xs, ys)"
   918   thm lexn_conv
   919   from this show "lexn r (Suc i) (x#xs, x#ys)"
   920     unfolding Collect_def mem_def lexn_conv
   921     apply auto
   922     apply (rule_tac x="x # xys" in exI)
   923     by auto
   924 qed
   925 
   926 code_pred [random_dseq] lexn
   927 proof -
   928   fix r n xs ys
   929   assume 1: "lexn r n (xs, ys)"
   930   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"
   931   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"
   932   from 1 2 3 show thesis
   933     unfolding lexn_conv Collect_def mem_def
   934     apply (auto simp add: has_length)
   935     apply (case_tac xys)
   936     apply auto
   937     apply fastsimp
   938     apply fastsimp done
   939 qed
   940 
   941 values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
   942 
   943 code_pred [inductify, skip_proof] lex .
   944 thm lex.equation
   945 thm lex_def
   946 declare lenlex_conv[code_pred_def]
   947 code_pred [inductify, skip_proof] lenlex .
   948 thm lenlex.equation
   949 
   950 code_pred [random_dseq inductify] lenlex .
   951 thm lenlex.random_dseq_equation
   952 
   953 values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"
   954 
   955 thm lists.intros
   956 code_pred [inductify] lists .
   957 thm lists.equation
   958 
   959 subsection {* AVL Tree *}
   960 
   961 datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
   962 fun height :: "'a tree => nat" where
   963 "height ET = 0"
   964 | "height (MKT x l r h) = max (height l) (height r) + 1"
   965 
   966 primrec avl :: "'a tree => bool"
   967 where
   968   "avl ET = True"
   969 | "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> 
   970   h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
   971 (*
   972 code_pred [inductify] avl .
   973 thm avl.equation*)
   974 
   975 code_pred [new_random_dseq inductify] avl .
   976 thm avl.new_random_dseq_equation
   977 (* TODO: has highly non-deterministic execution time!
   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 text {* The higher-order predicate r is in an output term *}
  1487 
  1488 datatype result = Result bool
  1489 
  1490 inductive fixed_relation :: "'a => bool"
  1491 
  1492 inductive test_relation_in_output_terms :: "('a => bool) => 'a => result => bool"
  1493 where
  1494   "test_relation_in_output_terms r x (Result (r x))"
  1495 | "test_relation_in_output_terms r x (Result (fixed_relation x))"
  1496 
  1497 code_pred test_relation_in_output_terms .
  1498 
  1499 thm test_relation_in_output_terms.equation
  1500 
  1501 
  1502 text {*
  1503   We want that the argument r is not treated as a higher-order relation, but simply as input.
  1504 *}
  1505 
  1506 inductive test_uninterpreted_relation :: "('a => bool) => 'a list => bool"
  1507 where
  1508   "list_all r xs ==> test_uninterpreted_relation r xs"
  1509 
  1510 code_pred (modes: i => i => bool) test_uninterpreted_relation .
  1511 
  1512 thm test_uninterpreted_relation.equation
  1513 
  1514 inductive list_ex'
  1515 where
  1516   "P x ==> list_ex' P (x#xs)"
  1517 | "list_ex' P xs ==> list_ex' P (x#xs)"
  1518 
  1519 code_pred list_ex' .
  1520 
  1521 inductive test_uninterpreted_relation2 :: "('a => bool) => 'a list => bool"
  1522 where
  1523   "list_ex r xs ==> test_uninterpreted_relation2 r xs"
  1524 | "list_ex' r xs ==> test_uninterpreted_relation2 r xs"
  1525 
  1526 text {* Proof procedure cannot handle this situation yet. *}
  1527 
  1528 code_pred (modes: i => i => bool) [skip_proof] test_uninterpreted_relation2 .
  1529 
  1530 thm test_uninterpreted_relation2.equation
  1531 
  1532 
  1533 text {* Trivial predicate *}
  1534 
  1535 inductive implies_itself :: "'a => bool"
  1536 where
  1537   "implies_itself x ==> implies_itself x"
  1538 
  1539 code_pred implies_itself .
  1540 
  1541 text {* Case expressions *}
  1542 
  1543 definition
  1544   "map_pairs xs ys = (map (%((a, b), c). (a, b, c)) xs = ys)"
  1545 
  1546 code_pred [inductify] map_pairs .
  1547 
  1548 end