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