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