src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
author bulwahn
Mon Mar 29 17:30:56 2010 +0200 (2010-03-29)
changeset 36040 fcd7bea01a93
parent 35954 d87d85a5d9ab
child 36055 537876d0fa62
permissions -rw-r--r--
adding skip_proof in the examples because proof procedure cannot handle alternative compilations yet
     1 theory Predicate_Compile_Examples
     2 imports Predicate_Compile_Alternative_Defs
     3 begin
     4 
     5 subsection {* Basic predicates *}
     6 
     7 inductive False' :: "bool"
     8 
     9 code_pred (expected_modes: bool) False' .
    10 code_pred [dseq] False' .
    11 code_pred [random_dseq] False' .
    12 
    13 values [expected "{}" pred] "{x. False'}"
    14 values [expected "{}" dseq 1] "{x. False'}"
    15 values [expected "{}" random_dseq 1, 1, 1] "{x. False'}"
    16 
    17 value "False'"
    18 
    19 
    20 inductive True' :: "bool"
    21 where
    22   "True ==> True'"
    23 
    24 code_pred True' .
    25 code_pred [dseq] True' .
    26 code_pred [random_dseq] True' .
    27 
    28 thm True'.equation
    29 thm True'.dseq_equation
    30 thm True'.random_dseq_equation
    31 values [expected "{()}" ]"{x. True'}"
    32 values [expected "{}" dseq 0] "{x. True'}"
    33 values [expected "{()}" dseq 1] "{x. True'}"
    34 values [expected "{()}" dseq 2] "{x. True'}"
    35 values [expected "{}" random_dseq 1, 1, 0] "{x. True'}"
    36 values [expected "{}" random_dseq 1, 1, 1] "{x. True'}"
    37 values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}"
    38 values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}"
    39 
    40 inductive EmptySet :: "'a \<Rightarrow> bool"
    41 
    42 code_pred (expected_modes: o => bool, i => bool) EmptySet .
    43 
    44 definition EmptySet' :: "'a \<Rightarrow> bool"
    45 where "EmptySet' = {}"
    46 
    47 code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
    48 
    49 inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
    50 
    51 code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel .
    52 
    53 inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    54 for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    55 
    56 code_pred
    57   (expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool,
    58          (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool,
    59          (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool,
    60          (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool,
    61          (o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool,
    62          (o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool,
    63          (i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool,
    64          (i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool)
    65   EmptyClosure .
    66 
    67 thm EmptyClosure.equation
    68 
    69 (* TODO: inductive package is broken!
    70 inductive False'' :: "bool"
    71 where
    72   "False \<Longrightarrow> False''"
    73 
    74 code_pred (expected_modes: []) False'' .
    75 
    76 inductive EmptySet'' :: "'a \<Rightarrow> bool"
    77 where
    78   "False \<Longrightarrow> EmptySet'' x"
    79 
    80 code_pred (expected_modes: [1]) EmptySet'' .
    81 code_pred (expected_modes: [], [1]) [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 this(1) 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(2) show thesis by simp
   174     next
   175       assume "xa = E" from this x is_D_or_E(3) 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 this(1) 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(2) show thesis by simp
   213     next
   214       assume "xa = G"
   215       from this x is_F_or_G(3) show thesis by simp
   216     qed
   217   qed
   218 qed
   219 
   220 subsection {* Preprocessor Inlining  *}
   221 
   222 definition "equals == (op =)"
   223  
   224 inductive zerozero' :: "nat * nat => bool" where
   225   "equals (x, y) (0, 0) ==> zerozero' (x, y)"
   226 
   227 code_pred (expected_modes: i => bool) zerozero' .
   228 
   229 lemma zerozero'_eq: "zerozero' x == zerozero x"
   230 proof -
   231   have "zerozero' = zerozero"
   232     apply (auto simp add: mem_def)
   233     apply (cases rule: zerozero'.cases)
   234     apply (auto simp add: equals_def intro: zerozero.intros)
   235     apply (cases rule: zerozero.cases)
   236     apply (auto simp add: equals_def intro: zerozero'.intros)
   237     done
   238   from this show "zerozero' x == zerozero x" by auto
   239 qed
   240 
   241 declare zerozero'_eq [code_pred_inline]
   242 
   243 definition "zerozero'' x == zerozero' x"
   244 
   245 text {* if preprocessing fails, zerozero'' will not have all modes. *}
   246 
   247 code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
   248 
   249 subsection {* Sets and Numerals *}
   250 
   251 definition
   252   "one_or_two = {Suc 0, (Suc (Suc 0))}"
   253 
   254 code_pred [inductify] one_or_two .
   255 
   256 code_pred [dseq] one_or_two .
   257 code_pred [random_dseq] one_or_two .
   258 thm one_or_two.dseq_equation
   259 values [expected "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}"
   260 values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
   261 
   262 inductive one_or_two' :: "nat => bool"
   263 where
   264   "one_or_two' 1"
   265 | "one_or_two' 2"
   266 
   267 code_pred one_or_two' .
   268 thm one_or_two'.equation
   269 
   270 values "{x. one_or_two' x}"
   271 
   272 definition one_or_two'':
   273   "one_or_two'' == {1, (2::nat)}"
   274 
   275 code_pred [inductify] one_or_two'' .
   276 thm one_or_two''.equation
   277 
   278 values "{x. one_or_two'' x}"
   279 
   280 subsection {* even predicate *}
   281 
   282 inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
   283     "even 0"
   284   | "even n \<Longrightarrow> odd (Suc n)"
   285   | "odd n \<Longrightarrow> even (Suc n)"
   286 
   287 code_pred (expected_modes: i => bool, o => bool) even .
   288 code_pred [dseq] even .
   289 code_pred [random_dseq] even .
   290 
   291 thm odd.equation
   292 thm even.equation
   293 thm odd.dseq_equation
   294 thm even.dseq_equation
   295 thm odd.random_dseq_equation
   296 thm even.random_dseq_equation
   297 
   298 values "{x. even 2}"
   299 values "{x. odd 2}"
   300 values 10 "{n. even n}"
   301 values 10 "{n. odd n}"
   302 values [expected "{}" dseq 2] "{x. even 6}"
   303 values [expected "{}" dseq 6] "{x. even 6}"
   304 values [expected "{()}" dseq 7] "{x. even 6}"
   305 values [dseq 2] "{x. odd 7}"
   306 values [dseq 6] "{x. odd 7}"
   307 values [dseq 7] "{x. odd 7}"
   308 values [expected "{()}" dseq 8] "{x. odd 7}"
   309 
   310 values [expected "{}" dseq 0] 8 "{x. even x}"
   311 values [expected "{0::nat}" dseq 1] 8 "{x. even x}"
   312 values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}"
   313 values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}"
   314 values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}"
   315 
   316 values [random_dseq 1, 1, 0] 8 "{x. even x}"
   317 values [random_dseq 1, 1, 1] 8 "{x. even x}"
   318 values [random_dseq 1, 1, 2] 8 "{x. even x}"
   319 values [random_dseq 1, 1, 3] 8 "{x. even x}"
   320 values [random_dseq 1, 1, 6] 8 "{x. even x}"
   321 
   322 values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}"
   323 values [random_dseq 1, 1, 8] "{x. odd 7}"
   324 values [random_dseq 1, 1, 9] "{x. odd 7}"
   325 
   326 definition odd' where "odd' x == \<not> even x"
   327 
   328 code_pred (expected_modes: i => bool) [inductify] odd' .
   329 code_pred [dseq inductify] odd' .
   330 code_pred [random_dseq inductify] odd' .
   331 
   332 values [expected "{}" dseq 2] "{x. odd' 7}"
   333 values [expected "{()}" dseq 9] "{x. odd' 7}"
   334 values [expected "{}" dseq 2] "{x. odd' 8}"
   335 values [expected "{}" dseq 10] "{x. odd' 8}"
   336 
   337 
   338 inductive is_even :: "nat \<Rightarrow> bool"
   339 where
   340   "n mod 2 = 0 \<Longrightarrow> is_even n"
   341 
   342 code_pred (expected_modes: i => bool) is_even .
   343 
   344 subsection {* append predicate *}
   345 
   346 inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
   347     "append [] xs xs"
   348   | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
   349 
   350 code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
   351   i => o => i => bool as suffix, i => i => i => bool) append .
   352 code_pred [dseq] append .
   353 code_pred [random_dseq] append .
   354 
   355 thm append.equation
   356 thm append.dseq_equation
   357 thm append.random_dseq_equation
   358 
   359 values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
   360 values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
   361 values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
   362 
   363 values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   364 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)]}"
   365 values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   366 values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   367 values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   368 values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   369 values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   370 values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   371 values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   372 values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   373 
   374 value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
   375 value [code] "Predicate.the (slice ([]::int list))"
   376 
   377 
   378 text {* tricky case with alternative rules *}
   379 
   380 inductive append2
   381 where
   382   "append2 [] xs xs"
   383 | "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
   384 
   385 lemma append2_Nil: "append2 [] (xs::'b list) xs"
   386   by (simp add: append2.intros(1))
   387 
   388 lemmas [code_pred_intro] = append2_Nil append2.intros(2)
   389 
   390 code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,
   391   i => o => i => bool, i => i => i => bool) append2
   392 proof -
   393   case append2
   394   from append2(1) show thesis
   395   proof
   396     fix xs
   397     assume "xa = []" "xb = xs" "xc = xs"
   398     from this append2(2) show thesis by simp
   399   next
   400     fix xs ys zs x
   401     assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs"
   402     from this append2(3) show thesis by fastsimp
   403   qed
   404 qed
   405 
   406 inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
   407 where
   408   "tupled_append ([], xs, xs)"
   409 | "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
   410 
   411 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   412   i * o * i => bool, i * i * i => bool) tupled_append .
   413 code_pred [random_dseq] tupled_append .
   414 thm tupled_append.equation
   415 
   416 values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}"
   417 
   418 inductive tupled_append'
   419 where
   420 "tupled_append' ([], xs, xs)"
   421 | "[| ys = fst (xa, y); x # zs = snd (xa, y);
   422  tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
   423 
   424 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   425   i * o * i => bool, i * i * i => bool) tupled_append' .
   426 thm tupled_append'.equation
   427 
   428 inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
   429 where
   430   "tupled_append'' ([], xs, xs)"
   431 | "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
   432 
   433 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   434   i * o * i => bool, i * i * i => bool) tupled_append'' .
   435 thm tupled_append''.equation
   436 
   437 inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
   438 where
   439   "tupled_append''' ([], xs, xs)"
   440 | "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
   441 
   442 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   443   i * o * i => bool, i * i * i => bool) tupled_append''' .
   444 thm tupled_append'''.equation
   445 
   446 subsection {* map_ofP predicate *}
   447 
   448 inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   449 where
   450   "map_ofP ((a, b)#xs) a b"
   451 | "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
   452 
   453 code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .
   454 thm map_ofP.equation
   455 
   456 subsection {* filter predicate *}
   457 
   458 inductive filter1
   459 for P
   460 where
   461   "filter1 P [] []"
   462 | "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
   463 | "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
   464 
   465 code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
   466 code_pred [dseq] filter1 .
   467 code_pred [random_dseq] filter1 .
   468 
   469 thm filter1.equation
   470 
   471 values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
   472 values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
   473 values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
   474 
   475 inductive filter2
   476 where
   477   "filter2 P [] []"
   478 | "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"
   479 | "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"
   480 
   481 code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 .
   482 code_pred [dseq] filter2 .
   483 code_pred [random_dseq] filter2 .
   484 
   485 thm filter2.equation
   486 thm filter2.random_dseq_equation
   487 
   488 (*
   489 inductive filter3
   490 for P
   491 where
   492   "List.filter P xs = ys ==> filter3 P xs ys"
   493 
   494 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 .
   495 
   496 code_pred [dseq] filter3 .
   497 thm filter3.dseq_equation
   498 *)
   499 (*
   500 inductive filter4
   501 where
   502   "List.filter P xs = ys ==> filter4 P xs ys"
   503 
   504 code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
   505 (*code_pred [depth_limited] filter4 .*)
   506 (*code_pred [random] filter4 .*)
   507 *)
   508 subsection {* reverse predicate *}
   509 
   510 inductive rev where
   511     "rev [] []"
   512   | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
   513 
   514 code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .
   515 
   516 thm rev.equation
   517 
   518 values "{xs. rev [0, 1, 2, 3::nat] xs}"
   519 
   520 inductive tupled_rev where
   521   "tupled_rev ([], [])"
   522 | "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"
   523 
   524 code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
   525 thm tupled_rev.equation
   526 
   527 subsection {* partition predicate *}
   528 
   529 inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   530   for f where
   531     "partition f [] [] []"
   532   | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
   533   | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
   534 
   535 code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,
   536   (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool)
   537   partition .
   538 code_pred [dseq] partition .
   539 code_pred [random_dseq] partition .
   540 
   541 values 10 "{(ys, zs). partition is_even
   542   [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
   543 values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
   544 values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
   545 
   546 inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"
   547   for f where
   548    "tupled_partition f ([], [], [])"
   549   | "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
   550   | "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"
   551 
   552 code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,
   553   (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition .
   554 
   555 thm tupled_partition.equation
   556 
   557 lemma [code_pred_intro]:
   558   "r a b \<Longrightarrow> tranclp r a b"
   559   "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
   560   by auto
   561 
   562 subsection {* transitive predicate *}
   563 
   564 text {* Also look at the tabled transitive closure in the Library *}
   565 
   566 code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
   567   (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,
   568   (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
   569 proof -
   570   case tranclp
   571   from this converse_tranclpE[OF this(1)] show thesis by metis
   572 qed
   573 
   574 
   575 code_pred [dseq] tranclp .
   576 code_pred [random_dseq] tranclp .
   577 thm tranclp.equation
   578 thm tranclp.random_dseq_equation
   579 
   580 inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool" 
   581 where
   582   "rtrancl' x x r"
   583 | "r x y ==> rtrancl' y z r ==> rtrancl' x z r"
   584 
   585 code_pred [random_dseq] rtrancl' .
   586 
   587 thm rtrancl'.random_dseq_equation
   588 
   589 inductive rtrancl'' :: "('a * 'a * ('a \<Rightarrow> 'a \<Rightarrow> bool)) \<Rightarrow> bool"  
   590 where
   591   "rtrancl'' (x, x, r)"
   592 | "r x y \<Longrightarrow> rtrancl'' (y, z, r) \<Longrightarrow> rtrancl'' (x, z, r)"
   593 
   594 code_pred rtrancl'' .
   595 
   596 inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool" 
   597 where
   598   "rtrancl''' (x, (x, x), r)"
   599 | "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)"
   600 
   601 code_pred rtrancl''' .
   602 
   603 
   604 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   605     "succ 0 1"
   606   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
   607 
   608 code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ .
   609 code_pred [random_dseq] succ .
   610 thm succ.equation
   611 thm succ.random_dseq_equation
   612 
   613 values 10 "{(m, n). succ n m}"
   614 values "{m. succ 0 m}"
   615 values "{m. succ m 0}"
   616 
   617 text {* values command needs mode annotation of the parameter succ
   618 to disambiguate which mode is to be chosen. *} 
   619 
   620 values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
   621 values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
   622 values 20 "{(n, m). tranclp succ n m}"
   623 
   624 inductive example_graph :: "int => int => bool"
   625 where
   626   "example_graph 0 1"
   627 | "example_graph 1 2"
   628 | "example_graph 1 3"
   629 | "example_graph 4 7"
   630 | "example_graph 4 5"
   631 | "example_graph 5 6"
   632 | "example_graph 7 6"
   633 | "example_graph 7 8"
   634  
   635 inductive not_reachable_in_example_graph :: "int => int => bool"
   636 where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y"
   637 
   638 code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
   639 
   640 thm not_reachable_in_example_graph.equation
   641 thm tranclp.equation
   642 value "not_reachable_in_example_graph 0 3"
   643 value "not_reachable_in_example_graph 4 8"
   644 value "not_reachable_in_example_graph 5 6"
   645 text {* rtrancl compilation is strange! *}
   646 (*
   647 value "not_reachable_in_example_graph 0 4"
   648 value "not_reachable_in_example_graph 1 6"
   649 value "not_reachable_in_example_graph 8 4"*)
   650 
   651 code_pred [dseq] not_reachable_in_example_graph .
   652 
   653 values [dseq 6] "{x. tranclp example_graph 0 3}"
   654 
   655 values [dseq 0] "{x. not_reachable_in_example_graph 0 3}"
   656 values [dseq 0] "{x. not_reachable_in_example_graph 0 4}"
   657 values [dseq 20] "{x. not_reachable_in_example_graph 0 4}"
   658 values [dseq 6] "{x. not_reachable_in_example_graph 0 3}"
   659 values [dseq 3] "{x. not_reachable_in_example_graph 4 2}"
   660 values [dseq 6] "{x. not_reachable_in_example_graph 4 2}"
   661 
   662 
   663 inductive not_reachable_in_example_graph' :: "int => int => bool"
   664 where "\<not> (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y"
   665 
   666 code_pred not_reachable_in_example_graph' .
   667 
   668 value "not_reachable_in_example_graph' 0 3"
   669 (* value "not_reachable_in_example_graph' 0 5" would not terminate *)
   670 
   671 
   672 (*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*)
   673 (*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
   674 (*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*)
   675 (*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
   676 (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   677 (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   678 
   679 code_pred [dseq] not_reachable_in_example_graph' .
   680 
   681 (*thm not_reachable_in_example_graph'.dseq_equation*)
   682 
   683 (*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*)
   684 (*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
   685 (*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"
   686 values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
   687 (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   688 (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   689 
   690 
   691 subsection {* IMP *}
   692 
   693 types
   694   var = nat
   695   state = "int list"
   696 
   697 datatype com =
   698   Skip |
   699   Ass var "state => int" |
   700   Seq com com |
   701   IF "state => bool" com com |
   702   While "state => bool" com
   703 
   704 inductive exec :: "com => state => state => bool" where
   705 "exec Skip s s" |
   706 "exec (Ass x e) s (s[x := e(s)])" |
   707 "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
   708 "b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
   709 "~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
   710 "~b s ==> exec (While b c) s s" |
   711 "b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
   712 
   713 code_pred exec .
   714 
   715 values "{t. exec
   716  (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))))
   717  [3,5] t}"
   718 
   719 
   720 inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where
   721 "tupled_exec (Skip, s, s)" |
   722 "tupled_exec (Ass x e, s, s[x := e(s)])" |
   723 "tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" |
   724 "b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
   725 "~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
   726 "~b s ==> tupled_exec (While b c, s, s)" |
   727 "b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)"
   728 
   729 code_pred tupled_exec .
   730 
   731 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)}"
   732 
   733 subsection {* CCS *}
   734 
   735 text{* This example formalizes finite CCS processes without communication or
   736 recursion. For simplicity, labels are natural numbers. *}
   737 
   738 datatype proc = nil | pre nat proc | or proc proc | par proc proc
   739 
   740 inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
   741 "step (pre n p) n p" |
   742 "step p1 a q \<Longrightarrow> step (or p1 p2) a q" |
   743 "step p2 a q \<Longrightarrow> step (or p1 p2) a q" |
   744 "step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" |
   745 "step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)"
   746 
   747 code_pred step .
   748 
   749 inductive steps where
   750 "steps p [] p" |
   751 "step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r"
   752 
   753 code_pred steps .
   754 
   755 values 3 
   756  "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
   757 
   758 values 5
   759  "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
   760 
   761 values 3 "{(a,q). step (par nil nil) a q}"
   762 
   763 
   764 inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
   765 where
   766 "tupled_step (pre n p, n, p)" |
   767 "tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
   768 "tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
   769 "tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)" |
   770 "tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)"
   771 
   772 code_pred tupled_step .
   773 thm tupled_step.equation
   774 
   775 subsection {* divmod *}
   776 
   777 inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
   778     "k < l \<Longrightarrow> divmod_rel k l 0 k"
   779   | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
   780 
   781 code_pred divmod_rel ..
   782 thm divmod_rel.equation
   783 value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
   784 
   785 subsection {* Transforming predicate logic into logic programs *}
   786 
   787 subsection {* Transforming functions into logic programs *}
   788 definition
   789   "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
   790 
   791 code_pred [inductify, skip_proof] case_f .
   792 thm case_fP.equation
   793 thm case_fP.intros
   794 
   795 fun fold_map_idx where
   796   "fold_map_idx f i y [] = (y, [])"
   797 | "fold_map_idx f i y (x # xs) =
   798  (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs
   799  in (y'', x' # xs'))"
   800 
   801 text {* mode analysis explores thousand modes - this is infeasible at the moment... *}
   802 (*code_pred [inductify, show_steps] fold_map_idx .*)
   803 
   804 subsection {* Minimum *}
   805 
   806 definition Min
   807 where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
   808 
   809 code_pred [inductify] Min .
   810 thm Min.equation
   811 
   812 subsection {* Lexicographic order *}
   813 
   814 declare lexord_def[code_pred_def]
   815 code_pred [inductify] lexord .
   816 code_pred [random_dseq inductify] lexord .
   817 
   818 thm lexord.equation
   819 thm lexord.random_dseq_equation
   820 
   821 inductive less_than_nat :: "nat * nat => bool"
   822 where
   823   "less_than_nat (0, x)"
   824 | "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)"
   825  
   826 code_pred less_than_nat .
   827 
   828 code_pred [dseq] less_than_nat .
   829 code_pred [random_dseq] less_than_nat .
   830 
   831 inductive test_lexord :: "nat list * nat list => bool"
   832 where
   833   "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)"
   834 
   835 code_pred test_lexord .
   836 code_pred [dseq] test_lexord .
   837 code_pred [random_dseq] test_lexord .
   838 thm test_lexord.dseq_equation
   839 thm test_lexord.random_dseq_equation
   840 
   841 values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
   842 (*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*)
   843 
   844 declare list.size(3,4)[code_pred_def]
   845 lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
   846 (*
   847 code_pred [inductify] lexn .
   848 thm lexn.equation
   849 *)
   850 (*
   851 code_pred [random_dseq inductify] lexn .
   852 thm lexn.random_dseq_equation
   853 
   854 values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
   855 *)
   856 inductive has_length
   857 where
   858   "has_length [] 0"
   859 | "has_length xs i ==> has_length (x # xs) (Suc i)" 
   860 
   861 lemma has_length:
   862   "has_length xs n = (length xs = n)"
   863 proof (rule iffI)
   864   assume "has_length xs n"
   865   from this show "length xs = n"
   866     by (rule has_length.induct) auto
   867 next
   868   assume "length xs = n"
   869   from this show "has_length xs n"
   870     by (induct xs arbitrary: n) (auto intro: has_length.intros)
   871 qed
   872 
   873 lemma lexn_intros [code_pred_intro]:
   874   "has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)"
   875   "lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)"
   876 proof -
   877   assume "has_length xs i" "has_length ys i" "r (x, y)"
   878   from this has_length show "lexn r (Suc i) (x # xs, y # ys)"
   879     unfolding lexn_conv Collect_def mem_def
   880     by fastsimp
   881 next
   882   assume "lexn r i (xs, ys)"
   883   thm lexn_conv
   884   from this show "lexn r (Suc i) (x#xs, x#ys)"
   885     unfolding Collect_def mem_def lexn_conv
   886     apply auto
   887     apply (rule_tac x="x # xys" in exI)
   888     by auto
   889 qed
   890 
   891 code_pred [random_dseq inductify] lexn
   892 proof -
   893   fix r n xs ys
   894   assume 1: "lexn r n (xs, ys)"
   895   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"
   896   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"
   897   from 1 2 3 show thesis
   898     unfolding lexn_conv Collect_def mem_def
   899     apply (auto simp add: has_length)
   900     apply (case_tac xys)
   901     apply auto
   902     apply fastsimp
   903     apply fastsimp done
   904 qed
   905 
   906 
   907 values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
   908 thm lenlex_conv
   909 thm lex_conv
   910 declare list.size(3,4)[code_pred_def]
   911 (*code_pred [inductify, show_steps, show_intermediate_results] length .*)
   912 setup {* Predicate_Compile_Data.ignore_consts [@{const_name Orderings.top_class.top}] *}
   913 code_pred [inductify, skip_proof] lex .
   914 thm lex.equation
   915 thm lex_def
   916 declare lenlex_conv[code_pred_def]
   917 code_pred [inductify, skip_proof] lenlex .
   918 thm lenlex.equation
   919 
   920 code_pred [random_dseq inductify] lenlex .
   921 thm lenlex.random_dseq_equation
   922 
   923 values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"
   924 thm lists.intros
   925 
   926 code_pred [inductify] lists .
   927 thm lists.equation
   928 
   929 subsection {* AVL Tree *}
   930 
   931 datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
   932 fun height :: "'a tree => nat" where
   933 "height ET = 0"
   934 | "height (MKT x l r h) = max (height l) (height r) + 1"
   935 
   936 consts avl :: "'a tree => bool"
   937 primrec
   938   "avl ET = True"
   939   "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> 
   940   h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
   941 (*
   942 code_pred [inductify] avl .
   943 thm avl.equation*)
   944 
   945 code_pred [random_dseq inductify] avl .
   946 thm avl.random_dseq_equation
   947 
   948 values [random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
   949 
   950 fun set_of
   951 where
   952 "set_of ET = {}"
   953 | "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
   954 
   955 fun is_ord :: "nat tree => bool"
   956 where
   957 "is_ord ET = True"
   958 | "is_ord (MKT n l r h) =
   959  ((\<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)"
   960 
   961 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
   962 thm set_of.equation
   963 
   964 code_pred (expected_modes: i => bool) [inductify] is_ord .
   965 thm is_ord_aux.equation
   966 thm is_ord.equation
   967 
   968 
   969 subsection {* Definitions about Relations *}
   970 term "converse"
   971 code_pred (modes:
   972   (i * i => bool) => i * i => bool,
   973   (i * o => bool) => o * i => bool,
   974   (i * o => bool) => i * i => bool,
   975   (o * i => bool) => i * o => bool,
   976   (o * i => bool) => i * i => bool,
   977   (o * o => bool) => o * o => bool,
   978   (o * o => bool) => i * o => bool,
   979   (o * o => bool) => o * i => bool,
   980   (o * o => bool) => i * i => bool) [inductify] converse .
   981 
   982 thm converse.equation
   983 code_pred [inductify] rel_comp .
   984 thm rel_comp.equation
   985 code_pred [inductify] Image .
   986 thm Image.equation
   987 declare singleton_iff[code_pred_inline]
   988 declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def]
   989 
   990 code_pred (expected_modes:
   991   (o => bool) => o => bool,
   992   (o => bool) => i * o => bool,
   993   (o => bool) => o * i => bool,
   994   (o => bool) => i => bool,
   995   (i => bool) => i * o => bool,
   996   (i => bool) => o * i => bool,
   997   (i => bool) => i => bool) [inductify] Id_on .
   998 thm Id_on.equation
   999 thm Domain_def
  1000 code_pred (modes:
  1001   (o * o => bool) => o => bool,
  1002   (o * o => bool) => i => bool,
  1003   (i * o => bool) => i => bool) [inductify] Domain .
  1004 thm Domain.equation
  1005 
  1006 thm Range_def
  1007 code_pred (modes:
  1008   (o * o => bool) => o => bool,
  1009   (o * o => bool) => i => bool,
  1010   (o * i => bool) => i => bool) [inductify] Range .
  1011 thm Range.equation
  1012 
  1013 code_pred [inductify] Field .
  1014 thm Field.equation
  1015 
  1016 thm refl_on_def
  1017 code_pred [inductify] refl_on .
  1018 thm refl_on.equation
  1019 code_pred [inductify] total_on .
  1020 thm total_on.equation
  1021 code_pred [inductify] antisym .
  1022 thm antisym.equation
  1023 code_pred [inductify] trans .
  1024 thm trans.equation
  1025 code_pred [inductify] single_valued .
  1026 thm single_valued.equation
  1027 thm inv_image_def
  1028 code_pred [inductify] inv_image .
  1029 thm inv_image.equation
  1030 
  1031 subsection {* Inverting list functions *}
  1032 
  1033 (*code_pred [inductify] length .
  1034 code_pred [random inductify] length .
  1035 thm size_listP.equation
  1036 thm size_listP.random_equation
  1037 *)
  1038 (*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*)
  1039 
  1040 code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
  1041 thm concatP.equation
  1042 
  1043 values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
  1044 values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
  1045 
  1046 code_pred [dseq inductify] List.concat .
  1047 thm concatP.dseq_equation
  1048 
  1049 values [dseq 3] 3
  1050   "{xs. concatP xs ([0] :: nat list)}"
  1051 
  1052 values [dseq 5] 3
  1053   "{xs. concatP xs ([1] :: int list)}"
  1054 
  1055 values [dseq 5] 3
  1056   "{xs. concatP xs ([1] :: nat list)}"
  1057 
  1058 values [dseq 5] 3
  1059   "{xs. concatP xs [(1::int), 2]}"
  1060 
  1061 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd .
  1062 thm hdP.equation
  1063 values "{x. hdP [1, 2, (3::int)] x}"
  1064 values "{(xs, x). hdP [1, 2, (3::int)] 1}"
  1065  
  1066 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl .
  1067 thm tlP.equation
  1068 values "{x. tlP [1, 2, (3::nat)] x}"
  1069 values "{x. tlP [1, 2, (3::int)] [3]}"
  1070 
  1071 code_pred [inductify, skip_proof] last .
  1072 thm lastP.equation
  1073 
  1074 code_pred [inductify, skip_proof] butlast .
  1075 thm butlastP.equation
  1076 
  1077 code_pred [inductify, skip_proof] take .
  1078 thm takeP.equation
  1079 
  1080 code_pred [inductify, skip_proof] drop .
  1081 thm dropP.equation
  1082 code_pred [inductify, skip_proof] zip .
  1083 thm zipP.equation
  1084 
  1085 code_pred [inductify, skip_proof] upt .
  1086 code_pred [inductify, skip_proof] remdups .
  1087 thm remdupsP.equation
  1088 code_pred [dseq inductify] remdups .
  1089 values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
  1090 
  1091 code_pred [inductify, skip_proof] remove1 .
  1092 thm remove1P.equation
  1093 values "{xs. remove1P 1 xs [2, (3::int)]}"
  1094 
  1095 code_pred [inductify, skip_proof] removeAll .
  1096 thm removeAllP.equation
  1097 code_pred [dseq inductify] removeAll .
  1098 
  1099 values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
  1100 
  1101 code_pred [inductify] distinct .
  1102 thm distinct.equation
  1103 code_pred [inductify, skip_proof] replicate .
  1104 thm replicateP.equation
  1105 values 5 "{(n, xs). replicateP n (0::int) xs}"
  1106 
  1107 code_pred [inductify, skip_proof] splice .
  1108 thm splice.simps
  1109 thm spliceP.equation
  1110 
  1111 values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
  1112 
  1113 code_pred [inductify, skip_proof] List.rev .
  1114 code_pred [inductify] map .
  1115 code_pred [inductify] foldr .
  1116 code_pred [inductify] foldl .
  1117 code_pred [inductify] filter .
  1118 code_pred [random_dseq inductify] filter .
  1119 
  1120 subsection {* Context Free Grammar *}
  1121 
  1122 datatype alphabet = a | b
  1123 
  1124 inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
  1125   "[] \<in> S\<^isub>1"
  1126 | "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
  1127 | "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
  1128 | "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
  1129 | "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
  1130 | "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
  1131 
  1132 code_pred [inductify] S\<^isub>1p .
  1133 code_pred [random_dseq inductify] S\<^isub>1p .
  1134 thm S\<^isub>1p.equation
  1135 thm S\<^isub>1p.random_dseq_equation
  1136 
  1137 values [random_dseq 5, 5, 5] 5 "{x. S\<^isub>1p x}"
  1138 
  1139 inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
  1140   "[] \<in> S\<^isub>2"
  1141 | "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
  1142 | "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
  1143 | "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
  1144 | "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
  1145 | "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
  1146 
  1147 code_pred [random_dseq inductify] S\<^isub>2p .
  1148 thm S\<^isub>2p.random_dseq_equation
  1149 thm A\<^isub>2p.random_dseq_equation
  1150 thm B\<^isub>2p.random_dseq_equation
  1151 
  1152 values [random_dseq 5, 5, 5] 10 "{x. S\<^isub>2p x}"
  1153 
  1154 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
  1155   "[] \<in> S\<^isub>3"
  1156 | "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
  1157 | "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
  1158 | "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
  1159 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
  1160 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
  1161 
  1162 code_pred [inductify, skip_proof] S\<^isub>3p .
  1163 thm S\<^isub>3p.equation
  1164 
  1165 values 10 "{x. S\<^isub>3p x}"
  1166 
  1167 inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
  1168   "[] \<in> S\<^isub>4"
  1169 | "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
  1170 | "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
  1171 | "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
  1172 | "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
  1173 | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
  1174 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
  1175 
  1176 code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .
  1177 
  1178 subsection {* Lambda *}
  1179 
  1180 datatype type =
  1181     Atom nat
  1182   | Fun type type    (infixr "\<Rightarrow>" 200)
  1183 
  1184 datatype dB =
  1185     Var nat
  1186   | App dB dB (infixl "\<degree>" 200)
  1187   | Abs type dB
  1188 
  1189 primrec
  1190   nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
  1191 where
  1192   "[]\<langle>i\<rangle> = None"
  1193 | "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
  1194 
  1195 inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
  1196 where
  1197   "nth_el' (x # xs) 0 x"
  1198 | "nth_el' xs i y \<Longrightarrow> nth_el' (x # xs) (Suc i) y"
  1199 
  1200 inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
  1201   where
  1202     Var [intro!]: "nth_el' env x T \<Longrightarrow> env \<turnstile> Var x : T"
  1203   | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
  1204   | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
  1205 
  1206 primrec
  1207   lift :: "[dB, nat] => dB"
  1208 where
  1209     "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
  1210   | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
  1211   | "lift (Abs T s) k = Abs T (lift s (k + 1))"
  1212 
  1213 primrec
  1214   subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
  1215 where
  1216     subst_Var: "(Var i)[s/k] =
  1217       (if k < i then Var (i - 1) else if i = k then s else Var i)"
  1218   | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
  1219   | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"
  1220 
  1221 inductive beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
  1222   where
  1223     beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
  1224   | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
  1225   | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
  1226   | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
  1227 
  1228 code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing .
  1229 thm typing.equation
  1230 
  1231 code_pred (modes: i => i => bool,  i => o => bool as reduce') beta .
  1232 thm beta.equation
  1233 
  1234 values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}"
  1235 
  1236 definition "reduce t = Predicate.the (reduce' t)"
  1237 
  1238 value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))"
  1239 
  1240 code_pred [dseq] typing .
  1241 code_pred [random_dseq] typing .
  1242 
  1243 values [random_dseq 1,1,5] 10 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
  1244 
  1245 subsection {* A minimal example of yet another semantics *}
  1246 
  1247 text {* thanks to Elke Salecker *}
  1248 
  1249 types
  1250   vname = nat
  1251   vvalue = int
  1252   var_assign = "vname \<Rightarrow> vvalue"  --"variable assignment"
  1253 
  1254 datatype ir_expr = 
  1255   IrConst vvalue
  1256 | ObjAddr vname
  1257 | Add ir_expr ir_expr
  1258 
  1259 datatype val =
  1260   IntVal  vvalue
  1261 
  1262 record  configuration =
  1263   Env :: var_assign
  1264 
  1265 inductive eval_var ::
  1266   "ir_expr \<Rightarrow> configuration \<Rightarrow> val \<Rightarrow> bool"
  1267 where
  1268   irconst: "eval_var (IrConst i) conf (IntVal i)"
  1269 | objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
  1270 | plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
  1271 
  1272 
  1273 code_pred eval_var .
  1274 thm eval_var.equation
  1275 
  1276 values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}"
  1277 
  1278 end