theory Predicate_Compile_Examples

 imports Predicate_Compile_Alternative_Defs

 begin

 subsection {* Basic predicates *}

 inductive False' :: "bool"

 code_pred (expected_modes: bool) False' .

 code_pred [dseq] False' .

 code_pred [random_dseq] False' .

 values [expected "{}" pred] "{x. False'}"

 values [expected "{}" dseq 1] "{x. False'}"

 values [expected "{}" random_dseq 1, 1, 1] "{x. False'}"

 value "False'"

 inductive True' :: "bool"

 where

   "True ==> True'"

 code_pred True' .

 code_pred [dseq] True' .

 code_pred [random_dseq] True' .

 thm True'.equation

 thm True'.dseq_equation

 thm True'.random_dseq_equation

 values [expected "{()}" ]"{x. True'}"

 values [expected "{}" dseq 0] "{x. True'}"

 values [expected "{()}" dseq 1] "{x. True'}"

 values [expected "{()}" dseq 2] "{x. True'}"

 values [expected "{}" random_dseq 1, 1, 0] "{x. True'}"

 values [expected "{}" random_dseq 1, 1, 1] "{x. True'}"

 values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}"

 values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}"

 inductive EmptySet :: "'a \<Rightarrow> bool"

 code_pred (expected_modes: o => bool, i => bool) EmptySet .

 definition EmptySet' :: "'a \<Rightarrow> bool"

 where "EmptySet' = {}"

 code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .

 inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"

 code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel .

 inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"

 for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

 code_pred

   (expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool,

          (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool,

          (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool,

          (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool,

          (o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool,

          (o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool,

          (i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool,

          (i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool)

   EmptyClosure .

 thm EmptyClosure.equation

 (* TODO: inductive package is broken!

 inductive False'' :: "bool"

 where

   "False \<Longrightarrow> False''"

 code_pred (expected_modes: []) False'' .

 inductive EmptySet'' :: "'a \<Rightarrow> bool"

 where

   "False \<Longrightarrow> EmptySet'' x"

 code_pred (expected_modes: [1]) EmptySet'' .

 code_pred (expected_modes: [], [1]) [inductify] EmptySet'' .

 *)

 consts a' :: 'a

 inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

 where

 "Fact a' a'"

 code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .

 inductive zerozero :: "nat * nat => bool"

 where

   "zerozero (0, 0)"

 code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .

 code_pred [dseq] zerozero .

 code_pred [random_dseq] zerozero .

 thm zerozero.equation

 thm zerozero.dseq_equation

 thm zerozero.random_dseq_equation

 text {* We expect the user to expand the tuples in the values command.

 The following values command is not supported. *}

 (*values "{x. zerozero x}" *)

 text {* Instead, the user must type *}

 values "{(x, y). zerozero (x, y)}"

 values [expected "{}" dseq 0] "{(x, y). zerozero (x, y)}"

 values [expected "{(0::nat, 0::nat)}" dseq 1] "{(x, y). zerozero (x, y)}"

 values [expected "{(0::nat, 0::nat)}" dseq 2] "{(x, y). zerozero (x, y)}"

 values [expected "{}" random_dseq 1, 1, 2] "{(x, y). zerozero (x, y)}"

 values [expected "{(0::nat, 0:: nat)}" random_dseq 1, 1, 3] "{(x, y). zerozero (x, y)}"

 inductive nested_tuples :: "((int * int) * int * int) => bool"

 where

   "nested_tuples ((0, 1), 2, 3)"

 code_pred nested_tuples .

 inductive JamesBond :: "nat => int => code_numeral => bool"

 where

   "JamesBond 0 0 7"

 code_pred JamesBond .

 values [expected "{(0::nat, 0::int , 7::code_numeral)}"] "{(a, b, c). JamesBond a b c}"

 values [expected "{(0::nat, 7::code_numeral, 0:: int)}"] "{(a, c, b). JamesBond a b c}"

 values [expected "{(0::int, 0::nat, 7::code_numeral)}"] "{(b, a, c). JamesBond a b c}"

 values [expected "{(0::int, 7::code_numeral, 0::nat)}"] "{(b, c, a). JamesBond a b c}"

 values [expected "{(7::code_numeral, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}"

 values [expected "{(7::code_numeral, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}"

 values [expected "{(7::code_numeral, 0::int)}"] "{(a, b). JamesBond 0 b a}"

 values [expected "{(7::code_numeral, 0::nat)}"] "{(c, a). JamesBond a 0 c}"

 values [expected "{(0::nat, 7::code_numeral)}"] "{(a, c). JamesBond a 0 c}"

 subsection {* Alternative Rules *}

 datatype char = C | D | E | F | G | H

 inductive is_C_or_D

 where

   "(x = C) \<or> (x = D) ==> is_C_or_D x"

 code_pred (expected_modes: i => bool) is_C_or_D .

 thm is_C_or_D.equation

 inductive is_D_or_E

 where

   "(x = D) \<or> (x = E) ==> is_D_or_E x"

 lemma [code_pred_intro]:

   "is_D_or_E D"

 by (auto intro: is_D_or_E.intros)

 lemma [code_pred_intro]:

   "is_D_or_E E"

 by (auto intro: is_D_or_E.intros)

 code_pred (expected_modes: o => bool, i => bool) is_D_or_E

 proof -

   case is_D_or_E

   from this(1) show thesis

   proof

     fix xa

     assume x: "x = xa"

     assume "xa = D \<or> xa = E"

     from this show thesis

     proof

       assume "xa = D" from this x is_D_or_E(2) show thesis by simp

     next

       assume "xa = E" from this x is_D_or_E(3) show thesis by simp

     qed

   qed

 qed

 thm is_D_or_E.equation

 inductive is_F_or_G

 where

   "x = F \<or> x = G ==> is_F_or_G x"

 lemma [code_pred_intro]:

   "is_F_or_G F"

 by (auto intro: is_F_or_G.intros)

 lemma [code_pred_intro]:

   "is_F_or_G G"

 by (auto intro: is_F_or_G.intros)

 inductive is_FGH

 where

   "is_F_or_G x ==> is_FGH x"

 | "is_FGH H"

 text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}

 code_pred (expected_modes: o => bool, i => bool) is_FGH

 proof -

   case is_F_or_G

   from this(1) show thesis

   proof

     fix xa

     assume x: "x = xa"

     assume "xa = F \<or> xa = G"

     from this show thesis

     proof

       assume "xa = F"

       from this x is_F_or_G(2) show thesis by simp

     next

       assume "xa = G"

       from this x is_F_or_G(3) show thesis by simp

     qed

   qed

 qed

 subsection {* Preprocessor Inlining  *}

 definition "equals == (op =)"

 inductive zerozero' :: "nat * nat => bool" where

   "equals (x, y) (0, 0) ==> zerozero' (x, y)"

 code_pred (expected_modes: i => bool) zerozero' .

 lemma zerozero'_eq: "zerozero' x == zerozero x"

 proof -

   have "zerozero' = zerozero"

     apply (auto simp add: mem_def)

     apply (cases rule: zerozero'.cases)

     apply (auto simp add: equals_def intro: zerozero.intros)

     apply (cases rule: zerozero.cases)

     apply (auto simp add: equals_def intro: zerozero'.intros)

     done

   from this show "zerozero' x == zerozero x" by auto

 qed

 declare zerozero'_eq [code_pred_inline]

 definition "zerozero'' x == zerozero' x"

 text {* if preprocessing fails, zerozero'' will not have all modes. *}

 code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .

 subsection {* Sets and Numerals *}

 definition

   "one_or_two = {Suc 0, (Suc (Suc 0))}"

 code_pred [inductify] one_or_two .

 code_pred [dseq] one_or_two .

 code_pred [random_dseq] one_or_two .

 thm one_or_two.dseq_equation

 values [expected "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}"

 values [random_dseq 0,0,10] 3 "{x. one_or_two x}"

 inductive one_or_two' :: "nat => bool"

 where

   "one_or_two' 1"

 | "one_or_two' 2"

 code_pred one_or_two' .

 thm one_or_two'.equation

 values "{x. one_or_two' x}"

 definition one_or_two'':

   "one_or_two'' == {1, (2::nat)}"

 code_pred [inductify] one_or_two'' .

 thm one_or_two''.equation

 values "{x. one_or_two'' x}"

 subsection {* even predicate *}

 inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where

     "even 0"

   | "even n \<Longrightarrow> odd (Suc n)"

   | "odd n \<Longrightarrow> even (Suc n)"

 code_pred (expected_modes: i => bool, o => bool) even .

 code_pred [dseq] even .

 code_pred [random_dseq] even .

 thm odd.equation

 thm even.equation

 thm odd.dseq_equation

 thm even.dseq_equation

 thm odd.random_dseq_equation

 thm even.random_dseq_equation

 values "{x. even 2}"

 values "{x. odd 2}"

 values 10 "{n. even n}"

 values 10 "{n. odd n}"

 values [expected "{}" dseq 2] "{x. even 6}"

 values [expected "{}" dseq 6] "{x. even 6}"

 values [expected "{()}" dseq 7] "{x. even 6}"

 values [dseq 2] "{x. odd 7}"

 values [dseq 6] "{x. odd 7}"

 values [dseq 7] "{x. odd 7}"

 values [expected "{()}" dseq 8] "{x. odd 7}"

 values [expected "{}" dseq 0] 8 "{x. even x}"

 values [expected "{0::nat}" dseq 1] 8 "{x. even x}"

 values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}"

 values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}"

 values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}"

 values [random_dseq 1, 1, 0] 8 "{x. even x}"

 values [random_dseq 1, 1, 1] 8 "{x. even x}"

 values [random_dseq 1, 1, 2] 8 "{x. even x}"

 values [random_dseq 1, 1, 3] 8 "{x. even x}"

 values [random_dseq 1, 1, 6] 8 "{x. even x}"

 values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}"

 values [random_dseq 1, 1, 8] "{x. odd 7}"

 values [random_dseq 1, 1, 9] "{x. odd 7}"

 definition odd' where "odd' x == \<not> even x"

 code_pred (expected_modes: i => bool) [inductify] odd' .

 code_pred [dseq inductify] odd' .

 code_pred [random_dseq inductify] odd' .

 values [expected "{}" dseq 2] "{x. odd' 7}"

 values [expected "{()}" dseq 9] "{x. odd' 7}"

 values [expected "{}" dseq 2] "{x. odd' 8}"

 values [expected "{}" dseq 10] "{x. odd' 8}"

 inductive is_even :: "nat \<Rightarrow> bool"

 where

   "n mod 2 = 0 \<Longrightarrow> is_even n"

 code_pred (expected_modes: i => bool) is_even .

 subsection {* append predicate *}

 inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where

     "append [] xs xs"

   | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"

 code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,

   i => o => i => bool as suffix, i => i => i => bool) append .

 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,

   i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool) append .

 code_pred [dseq] append .

 code_pred [random_dseq] append .

 thm append.equation

 thm append.dseq_equation

 thm append.random_dseq_equation

 values "{(ys, xs). append xs ys [0, Suc 0, 2]}"

 values "{zs. append [0, Suc 0, 2] [17, 8] zs}"

 values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"

 values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"

 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)]}"

 values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"

 values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"

 values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"

 values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}"

 values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"

 values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"

 values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"

 values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"

 value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"

 value [code] "Predicate.the (slice ([]::int list))"

 text {* tricky case with alternative rules *}

 inductive append2

 where

   "append2 [] xs xs"

 | "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"

 lemma append2_Nil: "append2 [] (xs::'b list) xs"

   by (simp add: append2.intros(1))

 lemmas [code_pred_intro] = append2_Nil append2.intros(2)

 code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,

   i => o => i => bool, i => i => i => bool) append2

 proof -

   case append2

   from append2(1) show thesis

   proof

     fix xs

     assume "xa = []" "xb = xs" "xc = xs"

     from this append2(2) show thesis by simp

   next

     fix xs ys zs x

     assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs"

     from this append2(3) show thesis by fastsimp

   qed

 qed

 inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"

 where

   "tupled_append ([], xs, xs)"

 | "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"

 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,

   i * o * i => bool, i * i * i => bool) tupled_append .

 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,

   i \<times> o \<times> i \<Rightarrow> bool, i \<times> i \<times> i \<Rightarrow> bool) tupled_append .

 code_pred [random_dseq] tupled_append .

 thm tupled_append.equation

 values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}"

 inductive tupled_append'

 where

 "tupled_append' ([], xs, xs)"

 | "[| ys = fst (xa, y); x # zs = snd (xa, y);

  tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"

 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,

   i * o * i => bool, i * i * i => bool) tupled_append' .

 thm tupled_append'.equation

 inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"

 where

   "tupled_append'' ([], xs, xs)"

 | "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"

 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,

   i * o * i => bool, i * i * i => bool) tupled_append'' .

 thm tupled_append''.equation

 inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"

 where

   "tupled_append''' ([], xs, xs)"

 | "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"

 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,

   i * o * i => bool, i * i * i => bool) tupled_append''' .

 thm tupled_append'''.equation

 subsection {* map_ofP predicate *}

 inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"

 where

   "map_ofP ((a, b)#xs) a b"

 | "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"

 code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .

 thm map_ofP.equation

 subsection {* filter predicate *}

 inductive filter1

 for P

 where

   "filter1 P [] []"

 | "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"

 | "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"

 code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .

 code_pred [dseq] filter1 .

 code_pred [random_dseq] filter1 .

 thm filter1.equation

 values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"

 values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"

 values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"

 inductive filter2

 where

   "filter2 P [] []"

 | "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"

 | "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"

 code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 .

 code_pred [dseq] filter2 .

 code_pred [random_dseq] filter2 .

 thm filter2.equation

 thm filter2.random_dseq_equation

 (*

 inductive filter3

 for P

 where

   "List.filter P xs = ys ==> filter3 P xs ys"

 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 .

 code_pred [dseq] filter3 .

 thm filter3.dseq_equation

 *)

 (*

 inductive filter4

 where

   "List.filter P xs = ys ==> filter4 P xs ys"

 code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .

 (*code_pred [depth_limited] filter4 .*)

 (*code_pred [random] filter4 .*)

 *)

 subsection {* reverse predicate *}

 inductive rev where

     "rev [] []"

   | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"

 code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .

 thm rev.equation

 values "{xs. rev [0, 1, 2, 3::nat] xs}"

 inductive tupled_rev where

   "tupled_rev ([], [])"

 | "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"

 code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .

 thm tupled_rev.equation

 subsection {* partition predicate *}

 inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"

   for f where

     "partition f [] [] []"

   | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"

   | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"

 code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,

   (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool)

   partition .

 code_pred [dseq] partition .

 code_pred [random_dseq] partition .

 values 10 "{(ys, zs). partition is_even

   [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"

 values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"

 values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"

 inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"

   for f where

    "tupled_partition f ([], [], [])"

   | "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"

   | "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"

 code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,

   (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition .

 thm tupled_partition.equation

 lemma [code_pred_intro]:

   "r a b \<Longrightarrow> tranclp r a b"

   "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"

   by auto

 subsection {* transitive predicate *}

 text {* Also look at the tabled transitive closure in the Library *}

 code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,

   (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,

   (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp

 proof -

   case tranclp

   from this converse_tranclpE[OF this(1)] show thesis by metis

 qed

 code_pred [dseq] tranclp .

 code_pred [random_dseq] tranclp .

 thm tranclp.equation

 thm tranclp.random_dseq_equation

 inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool" 

 where

   "rtrancl' x x r"

 | "r x y ==> rtrancl' y z r ==> rtrancl' x z r"

 code_pred [random_dseq] rtrancl' .

 thm rtrancl'.random_dseq_equation

 inductive rtrancl'' :: "('a * 'a * ('a \<Rightarrow> 'a \<Rightarrow> bool)) \<Rightarrow> bool"  

 where

   "rtrancl'' (x, x, r)"

 | "r x y \<Longrightarrow> rtrancl'' (y, z, r) \<Longrightarrow> rtrancl'' (x, z, r)"

 code_pred rtrancl'' .

 inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool" 

 where

   "rtrancl''' (x, (x, x), r)"

 | "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)"

 code_pred rtrancl''' .

 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where

     "succ 0 1"

   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"

 code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ .

 code_pred [random_dseq] succ .

 thm succ.equation

 thm succ.random_dseq_equation

 values 10 "{(m, n). succ n m}"

 values "{m. succ 0 m}"

 values "{m. succ m 0}"

 text {* values command needs mode annotation of the parameter succ

 to disambiguate which mode is to be chosen. *} 

 values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"

 values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"

 values 20 "{(n, m). tranclp succ n m}"

 inductive example_graph :: "int => int => bool"

 where

   "example_graph 0 1"

 | "example_graph 1 2"

 | "example_graph 1 3"

 | "example_graph 4 7"

 | "example_graph 4 5"

 | "example_graph 5 6"

 | "example_graph 7 6"

 | "example_graph 7 8"

 inductive not_reachable_in_example_graph :: "int => int => bool"

 where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y"

 code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .

 thm not_reachable_in_example_graph.equation

 thm tranclp.equation

 value "not_reachable_in_example_graph 0 3"

 value "not_reachable_in_example_graph 4 8"

 value "not_reachable_in_example_graph 5 6"

 text {* rtrancl compilation is strange! *}

 (*

 value "not_reachable_in_example_graph 0 4"

 value "not_reachable_in_example_graph 1 6"

 value "not_reachable_in_example_graph 8 4"*)

 code_pred [dseq] not_reachable_in_example_graph .

 values [dseq 6] "{x. tranclp example_graph 0 3}"

 values [dseq 0] "{x. not_reachable_in_example_graph 0 3}"

 values [dseq 0] "{x. not_reachable_in_example_graph 0 4}"

 values [dseq 20] "{x. not_reachable_in_example_graph 0 4}"

 values [dseq 6] "{x. not_reachable_in_example_graph 0 3}"

 values [dseq 3] "{x. not_reachable_in_example_graph 4 2}"

 values [dseq 6] "{x. not_reachable_in_example_graph 4 2}"

 inductive not_reachable_in_example_graph' :: "int => int => bool"

 where "\<not> (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y"

 code_pred not_reachable_in_example_graph' .

 value "not_reachable_in_example_graph' 0 3"

 (* value "not_reachable_in_example_graph' 0 5" would not terminate *)

 (*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*)

 (*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)

 (*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*)

 (*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)

 (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)

 (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)

 code_pred [dseq] not_reachable_in_example_graph' .

 (*thm not_reachable_in_example_graph'.dseq_equation*)

 (*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*)

 (*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)

 (*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"

 values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)

 (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)

 (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)

 subsection {* Free function variable *}

 inductive FF :: "nat => nat => bool"

 where

   "f x = y ==> FF x y"

 code_pred FF .

 subsection {* IMP *}

 types

   var = nat

   state = "int list"

 datatype com =

   Skip |

   Ass var "state => int" |

   Seq com com |

   IF "state => bool" com com |

   While "state => bool" com

 inductive exec :: "com => state => state => bool" where

 "exec Skip s s" |

 "exec (Ass x e) s (s[x := e(s)])" |

 "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |

 "b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" |

 "~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" |

 "~b s ==> exec (While b c) s s" |

 "b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"

 code_pred exec .

 values "{t. exec

  (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))))

  [3,5] t}"

 inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where

 "tupled_exec (Skip, s, s)" |

 "tupled_exec (Ass x e, s, s[x := e(s)])" |

 "tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" |

 "b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |

 "~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |

 "~b s ==> tupled_exec (While b c, s, s)" |

 "b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)"

 code_pred tupled_exec .

 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)}"

 subsection {* CCS *}

 text{* This example formalizes finite CCS processes without communication or

 recursion. For simplicity, labels are natural numbers. *}

 datatype proc = nil | pre nat proc | or proc proc | par proc proc

 inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where

 "step (pre n p) n p" |

 "step p1 a q \<Longrightarrow> step (or p1 p2) a q" |

 "step p2 a q \<Longrightarrow> step (or p1 p2) a q" |

 "step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" |

 "step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)"

 code_pred step .

 inductive steps where

 "steps p [] p" |

 "step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r"

 code_pred steps .

 values 3 

  "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"

 values 5

  "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"

 values 3 "{(a,q). step (par nil nil) a q}"

 inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"

 where

 "tupled_step (pre n p, n, p)" |

 "tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |

 "tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |

 "tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)" |

 "tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)"

 code_pred tupled_step .

 thm tupled_step.equation

 subsection {* divmod *}

 inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where

     "k < l \<Longrightarrow> divmod_rel k l 0 k"

   | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"

 code_pred divmod_rel .

 thm divmod_rel.equation

 value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"

 subsection {* Transforming predicate logic into logic programs *}

 subsection {* Transforming functions into logic programs *}

 definition

   "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"

 code_pred [inductify, skip_proof] case_f .

 thm case_fP.equation

 fun fold_map_idx where

   "fold_map_idx f i y [] = (y, [])"

 | "fold_map_idx f i y (x # xs) =

  (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs

  in (y'', x' # xs'))"

 code_pred [inductify] fold_map_idx .

 subsection {* Minimum *}

 definition Min

 where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"

 code_pred [inductify] Min .

 thm Min.equation

 subsection {* Lexicographic order *}

 declare lexord_def[code_pred_def]

 code_pred [inductify] lexord .

 code_pred [random_dseq inductify] lexord .

 thm lexord.equation

 thm lexord.random_dseq_equation

 inductive less_than_nat :: "nat * nat => bool"

 where

   "less_than_nat (0, x)"

 | "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)"

 code_pred less_than_nat .

 code_pred [dseq] less_than_nat .

 code_pred [random_dseq] less_than_nat .

 inductive test_lexord :: "nat list * nat list => bool"

 where

   "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)"

 code_pred test_lexord .

 code_pred [dseq] test_lexord .

 code_pred [random_dseq] test_lexord .

 thm test_lexord.dseq_equation

 thm test_lexord.random_dseq_equation

 values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"

 (*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*)

 lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv

 (*

 code_pred [inductify] lexn .

 thm lexn.equation

 *)

 (*

 code_pred [random_dseq inductify] lexn .

 thm lexn.random_dseq_equation

 values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"

 *)

 inductive has_length

 where

   "has_length [] 0"

 | "has_length xs i ==> has_length (x # xs) (Suc i)" 

 lemma has_length:

   "has_length xs n = (length xs = n)"

 proof (rule iffI)

   assume "has_length xs n"

   from this show "length xs = n"

     by (rule has_length.induct) auto

 next

   assume "length xs = n"

   from this show "has_length xs n"

     by (induct xs arbitrary: n) (auto intro: has_length.intros)

 qed

 lemma lexn_intros [code_pred_intro]:

   "has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)"

   "lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)"

 proof -

   assume "has_length xs i" "has_length ys i" "r (x, y)"

   from this has_length show "lexn r (Suc i) (x # xs, y # ys)"

     unfolding lexn_conv Collect_def mem_def

     by fastsimp

 next

   assume "lexn r i (xs, ys)"

   thm lexn_conv

   from this show "lexn r (Suc i) (x#xs, x#ys)"

     unfolding Collect_def mem_def lexn_conv

     apply auto

     apply (rule_tac x="x # xys" in exI)

     by auto

 qed

 code_pred [random_dseq] lexn

 proof -

   fix r n xs ys

   assume 1: "lexn r n (xs, ys)"

   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"

   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"

   from 1 2 3 show thesis

     unfolding lexn_conv Collect_def mem_def

     apply (auto simp add: has_length)

     apply (case_tac xys)

     apply auto

     apply fastsimp

     apply fastsimp done

 qed

 values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"

 code_pred [inductify, skip_proof] lex .

 thm lex.equation

 thm lex_def

 declare lenlex_conv[code_pred_def]

 code_pred [inductify, skip_proof] lenlex .

 thm lenlex.equation

 code_pred [random_dseq inductify] lenlex .

 thm lenlex.random_dseq_equation

 values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"

 thm lists.intros

 code_pred [inductify] lists .

 thm lists.equation

 subsection {* AVL Tree *}

 datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat

 fun height :: "'a tree => nat" where

 "height ET = 0"

 | "height (MKT x l r h) = max (height l) (height r) + 1"

 primrec avl :: "'a tree => bool"

 where

   "avl ET = True"

 | "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> 

   h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"

 (*

 code_pred [inductify] avl .

 thm avl.equation*)

 code_pred [new_random_dseq inductify] avl .

 thm avl.new_random_dseq_equation

 values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"

 fun set_of

 where

 "set_of ET = {}"

 | "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"

 fun is_ord :: "nat tree => bool"

 where

 "is_ord ET = True"

 | "is_ord (MKT n l r h) =

  ((\<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)"

 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .

 thm set_of.equation

 code_pred (expected_modes: i => bool) [inductify] is_ord .

 thm is_ord_aux.equation

 thm is_ord.equation

 subsection {* Definitions about Relations *}

 term "converse"

 code_pred (modes:

   (i * i => bool) => i * i => bool,

   (i * o => bool) => o * i => bool,

   (i * o => bool) => i * i => bool,

   (o * i => bool) => i * o => bool,

   (o * i => bool) => i * i => bool,

   (o * o => bool) => o * o => bool,

   (o * o => bool) => i * o => bool,

   (o * o => bool) => o * i => bool,

   (o * o => bool) => i * i => bool) [inductify] converse .

 thm converse.equation

 code_pred [inductify] rel_comp .

 thm rel_comp.equation

 code_pred [inductify] Image .

 thm Image.equation

 declare singleton_iff[code_pred_inline]

 declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def]

 code_pred (expected_modes:

   (o => bool) => o => bool,

   (o => bool) => i * o => bool,

   (o => bool) => o * i => bool,

   (o => bool) => i => bool,

   (i => bool) => i * o => bool,

   (i => bool) => o * i => bool,

   (i => bool) => i => bool) [inductify] Id_on .

 thm Id_on.equation

 thm Domain_def

 code_pred (modes:

   (o * o => bool) => o => bool,

   (o * o => bool) => i => bool,

   (i * o => bool) => i => bool) [inductify] Domain .

 thm Domain.equation

 thm Range_def

 code_pred (modes:

   (o * o => bool) => o => bool,

   (o * o => bool) => i => bool,

   (o * i => bool) => i => bool) [inductify] Range .

 thm Range.equation

 code_pred [inductify] Field .

 thm Field.equation

 thm refl_on_def

 code_pred [inductify] refl_on .

 thm refl_on.equation

 code_pred [inductify] total_on .

 thm total_on.equation

 code_pred [inductify] antisym .

 thm antisym.equation

 code_pred [inductify] trans .

 thm trans.equation

 code_pred [inductify] single_valued .

 thm single_valued.equation

 thm inv_image_def

 code_pred [inductify] inv_image .

 thm inv_image.equation

 subsection {* Inverting list functions *}

 code_pred [inductify] size_list .

 code_pred [new_random_dseq inductify] size_list .

 thm size_listP.equation

 thm size_listP.new_random_dseq_equation

 values [new_random_dseq 2,3,10] 3 "{xs. size_listP (xs::nat list) (5::nat)}"

 code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .

 thm concatP.equation

 values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"

 values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"

 code_pred [dseq inductify] List.concat .

 thm concatP.dseq_equation

 values [dseq 3] 3

   "{xs. concatP xs ([0] :: nat list)}"

 values [dseq 5] 3

   "{xs. concatP xs ([1] :: int list)}"

 values [dseq 5] 3

   "{xs. concatP xs ([1] :: nat list)}"

 values [dseq 5] 3

   "{xs. concatP xs [(1::int), 2]}"

 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd .

 thm hdP.equation

 values "{x. hdP [1, 2, (3::int)] x}"

 values "{(xs, x). hdP [1, 2, (3::int)] 1}"

 code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl .

 thm tlP.equation

 values "{x. tlP [1, 2, (3::nat)] x}"

 values "{x. tlP [1, 2, (3::int)] [3]}"

 code_pred [inductify, skip_proof] last .

 thm lastP.equation

 code_pred [inductify, skip_proof] butlast .

 thm butlastP.equation

 code_pred [inductify, skip_proof] take .

 thm takeP.equation

 code_pred [inductify, skip_proof] drop .

 thm dropP.equation

 code_pred [inductify, skip_proof] zip .

 thm zipP.equation

 code_pred [inductify, skip_proof] upt .

 code_pred [inductify, skip_proof] remdups .

 thm remdupsP.equation

 code_pred [dseq inductify] remdups .

 values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"

 code_pred [inductify, skip_proof] remove1 .

 thm remove1P.equation

 values "{xs. remove1P 1 xs [2, (3::int)]}"

 code_pred [inductify, skip_proof] removeAll .

 thm removeAllP.equation

 code_pred [dseq inductify] removeAll .

 values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"

 code_pred [inductify] distinct .

 thm distinct.equation

 code_pred [inductify, skip_proof] replicate .

 thm replicateP.equation

 values 5 "{(n, xs). replicateP n (0::int) xs}"

 code_pred [inductify, skip_proof] splice .

 thm splice.simps

 thm spliceP.equation

 values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"

 code_pred [inductify, skip_proof] List.rev .

 code_pred [inductify] map .

 code_pred [inductify] foldr .

 code_pred [inductify] foldl .

 code_pred [inductify] filter .

 code_pred [random_dseq inductify] filter .

 subsection {* Context Free Grammar *}

 datatype alphabet = a | b

 inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where

   "[] \<in> S\<^isub>1"

 | "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"

 | "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"

 | "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"

 | "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"

 | "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"

 code_pred [inductify] S\<^isub>1p .

 code_pred [random_dseq inductify] S\<^isub>1p .

 thm S\<^isub>1p.equation

 thm S\<^isub>1p.random_dseq_equation

 values [random_dseq 5, 5, 5] 5 "{x. S\<^isub>1p x}"

 inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where

   "[] \<in> S\<^isub>2"

 | "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"

 | "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"

 | "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"

 | "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"

 | "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"

 code_pred [random_dseq inductify] S\<^isub>2p .

 thm S\<^isub>2p.random_dseq_equation

 thm A\<^isub>2p.random_dseq_equation

 thm B\<^isub>2p.random_dseq_equation

 values [random_dseq 5, 5, 5] 10 "{x. S\<^isub>2p x}"

 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where

   "[] \<in> S\<^isub>3"

 | "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"

 | "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"

 | "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"

 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"

 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"

 code_pred [inductify, skip_proof] S\<^isub>3p .

 thm S\<^isub>3p.equation

 values 10 "{x. S\<^isub>3p x}"

 inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where

   "[] \<in> S\<^isub>4"

 | "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"

 | "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"

 | "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"

 | "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"

 | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"

 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"

 code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .

 hide_const a b

 subsection {* Lambda *}

 datatype type =

     Atom nat

   | Fun type type    (infixr "\<Rightarrow>" 200)

 datatype dB =

     Var nat

   | App dB dB (infixl "\<degree>" 200)

   | Abs type dB

 primrec

   nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)

 where

   "[]\<langle>i\<rangle> = None"

 | "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"

 inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"

 where

   "nth_el' (x # xs) 0 x"

 | "nth_el' xs i y \<Longrightarrow> nth_el' (x # xs) (Suc i) y"

 inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)

   where

     Var [intro!]: "nth_el' env x T \<Longrightarrow> env \<turnstile> Var x : T"

   | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"

   | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"

 primrec

   lift :: "[dB, nat] => dB"

 where

     "lift (Var i) k = (if i < k then Var i else Var (i + 1))"

   | "lift (s \<degree> t) k = lift s k \<degree> lift t k"

   | "lift (Abs T s) k = Abs T (lift s (k + 1))"

 primrec

   subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)

 where

     subst_Var: "(Var i)[s/k] =

       (if k < i then Var (i - 1) else if i = k then s else Var i)"

   | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"

   | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"

 inductive beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)

   where

     beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"

   | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"

   | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"

   | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"

 code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing .

 thm typing.equation

 code_pred (modes: i => i => bool,  i => o => bool as reduce') beta .

 thm beta.equation

 values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}"

 definition "reduce t = Predicate.the (reduce' t)"

 value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))"

 code_pred [dseq] typing .

 code_pred [random_dseq] typing .

 values [random_dseq 1,1,5] 10 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"

 subsection {* A minimal example of yet another semantics *}

 text {* thanks to Elke Salecker *}

 types

   vname = nat

   vvalue = int

   var_assign = "vname \<Rightarrow> vvalue"  --"variable assignment"

 datatype ir_expr = 

   IrConst vvalue

 | ObjAddr vname

 | Add ir_expr ir_expr

 datatype val =

   IntVal  vvalue

 record  configuration =

   Env :: var_assign

 inductive eval_var ::

   "ir_expr \<Rightarrow> configuration \<Rightarrow> val \<Rightarrow> bool"

 where

   irconst: "eval_var (IrConst i) conf (IntVal i)"

 | objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"

 | 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))"

 code_pred eval_var .

 thm eval_var.equation

 values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}"

 section {* Function predicate replacement *}

 text {*

 If the mode analysis uses the functional mode, we

 replace predicates that resulted from functions again by their functions.

 *}

 inductive test_append

 where

   "List.append xs ys = zs ==> test_append xs ys zs"

 code_pred [inductify, skip_proof] test_append .

 thm test_append.equation

 text {* If append is not turned into a predicate, then the mode

   o => o => i => bool could not be inferred. *}

 values 4 "{(xs::int list, ys). test_append xs ys [1, 2, 3, 4]}"

 text {* If appendP is not reverted back to a function, then mode i => i => o => bool

   fails after deleting the predicate equation. *}

 declare appendP.equation[code del]

 values "{xs::int list. test_append [1,2] [3,4] xs}"

 values "{xs::int list. test_append (replicate 1000 1) (replicate 1000 2) xs}"

 values "{xs::int list. test_append (replicate 2000 1) (replicate 2000 2) xs}"

 subsection {* Function with tuples *}

 fun append'

 where

   "append' ([], ys) = ys"

 | "append' (x # xs, ys) = x # append' (xs, ys)"

 inductive test_append'

 where

   "append' (xs, ys) = zs ==> test_append' xs ys zs"

 code_pred [inductify, skip_proof] test_append' .

 thm test_append'.equation

 values "{(xs::int list, ys). test_append' xs ys [1, 2, 3, 4]}"

 declare append'P.equation[code del]

 values "{zs :: int list. test_append' [1,2,3] [4,5] zs}"

 section {* Arithmetic examples *}

 subsection {* Examples on nat *}

 inductive plus_nat_test :: "nat => nat => nat => bool"

 where

   "x + y = z ==> plus_nat_test x y z"

 code_pred [inductify, skip_proof] plus_nat_test .

 code_pred [new_random_dseq inductify] plus_nat_test .

 thm plus_nat_test.equation

 thm plus_nat_test.new_random_dseq_equation

 values [expected "{9::nat}"] "{z. plus_nat_test 4 5 z}"

 values [expected "{9::nat}"] "{z. plus_nat_test 7 2 z}"

 values [expected "{4::nat}"] "{y. plus_nat_test 5 y 9}"

 values [expected "{}"] "{y. plus_nat_test 9 y 8}"

 values [expected "{6::nat}"] "{y. plus_nat_test 1 y 7}"

 values [expected "{2::nat}"] "{x. plus_nat_test x 7 9}"

 values [expected "{}"] "{x. plus_nat_test x 9 7}"

 values [expected "{(0::nat,0::nat)}"] "{(x, y). plus_nat_test x y 0}"

 values [expected "{(0, Suc 0), (Suc 0, 0)}"] "{(x, y). plus_nat_test x y 1}"

 values [expected "{(0, 5), (4, Suc 0), (3, 2), (2, 3), (Suc 0, 4), (5, 0)}"]

   "{(x, y). plus_nat_test x y 5}"

 inductive minus_nat_test :: "nat => nat => nat => bool"

 where

   "x - y = z ==> minus_nat_test x y z"

 code_pred [inductify, skip_proof] minus_nat_test .

 code_pred [new_random_dseq inductify] minus_nat_test .

 thm minus_nat_test.equation

 thm minus_nat_test.new_random_dseq_equation

 values [expected "{0::nat}"] "{z. minus_nat_test 4 5 z}"

 values [expected "{5::nat}"] "{z. minus_nat_test 7 2 z}"

 values [expected "{16::nat}"] "{x. minus_nat_test x 7 9}"

 values [expected "{16::nat}"] "{x. minus_nat_test x 9 7}"

 values [expected "{0, Suc 0, 2, 3}"] "{x. minus_nat_test x 3 0}"

 values [expected "{0::nat}"] "{x. minus_nat_test x 0 0}"

 subsection {* Examples on int *}

 inductive plus_int_test :: "int => int => int => bool"

 where

   "a + b = c ==> plus_int_test a b c"

 code_pred [inductify, skip_proof] plus_int_test .

 code_pred [new_random_dseq inductify] plus_int_test .

 thm plus_int_test.equation

 thm plus_int_test.new_random_dseq_equation

 values [expected "{1::int}"] "{a. plus_int_test a 6 7}"

 values [expected "{1::int}"] "{b. plus_int_test 6 b 7}"

 values [expected "{11::int}"] "{c. plus_int_test 5 6 c}"

 inductive minus_int_test :: "int => int => int => bool"

 where

   "a - b = c ==> minus_int_test a b c"

 code_pred [inductify, skip_proof] minus_int_test .

 code_pred [new_random_dseq inductify] minus_int_test .

 thm minus_int_test.equation

 thm minus_int_test.new_random_dseq_equation

 values [expected "{4::int}"] "{c. minus_int_test 9 5 c}"

 values [expected "{9::int}"] "{a. minus_int_test a 4 5}"

 values [expected "{- 1::int}"] "{b. minus_int_test 4 b 5}"

 subsection {* minus on bool *}

 inductive All :: "nat => bool"

 where

   "All x"

 inductive None :: "nat => bool"

 definition "test_minus_bool x = (None x - All x)"

 code_pred [inductify] test_minus_bool .

 thm test_minus_bool.equation

 values "{x. test_minus_bool x}"

 subsection {* Functions *}

 fun partial_hd :: "'a list => 'a option"

 where

   "partial_hd [] = Option.None"

 | "partial_hd (x # xs) = Some x"

 inductive hd_predicate

 where

   "partial_hd xs = Some x ==> hd_predicate xs x"

 code_pred (expected_modes: i => i => bool, i => o => bool) hd_predicate .

 thm hd_predicate.equation

 subsection {* Locales *}

 inductive hd_predicate2 :: "('a list => 'a option) => 'a list => 'a => bool"

 where

   "partial_hd' xs = Some x ==> hd_predicate2 partial_hd' xs x"

 thm hd_predicate2.intros

 code_pred (expected_modes: i => i => i => bool, i => i => o => bool) hd_predicate2 .

 thm hd_predicate2.equation

 locale A = fixes partial_hd :: "'a list => 'a option" begin

 inductive hd_predicate_in_locale :: "'a list => 'a => bool"

 where

   "partial_hd xs = Some x ==> hd_predicate_in_locale xs x"

 end

 text {* The global introduction rules must be redeclared as introduction rules and then 

   one could invoke code_pred. *}

 declare A.hd_predicate_in_locale.intros [unfolded Predicate.eq_is_eq[symmetric], code_pred_intro]

 code_pred (expected_modes: i => i => i => bool, i => i => o => bool) A.hd_predicate_in_locale

 unfolding eq_is_eq by (auto elim: A.hd_predicate_in_locale.cases)

 interpretation A partial_hd .

 thm hd_predicate_in_locale.intros

 text {* A locally compliant solution with a trivial interpretation fails, because

 the predicate compiler has very strict assumptions about the terms and their structure. *}

 (*code_pred hd_predicate_in_locale .*)

 section {* Integer example *}

 definition three :: int

 where "three = 3"

 inductive is_three

 where

   "is_three three"

 code_pred is_three .

 thm is_three.equation

 section {* String.literal example *}

 definition Error_1

 where

   "Error_1 = STR ''Error 1''"

 definition Error_2

 where

   "Error_2 = STR ''Error 2''"

 inductive "is_error" :: "String.literal \<Rightarrow> bool"

 where

   "is_error Error_1"

 | "is_error Error_2"

 code_pred is_error .

 thm is_error.equation

 inductive is_error' :: "String.literal \<Rightarrow> bool"

 where

   "is_error' (STR ''Error1'')"

 | "is_error' (STR ''Error2'')"

 code_pred is_error' .

 thm is_error'.equation

 datatype ErrorObject = Error String.literal int

 inductive is_error'' :: "ErrorObject \<Rightarrow> bool"

 where

   "is_error'' (Error Error_1 3)"

 | "is_error'' (Error Error_2 4)"

 code_pred is_error'' .

 thm is_error''.equation

 section {* Another function example *}

 consts f :: "'a \<Rightarrow> 'a"

 inductive fun_upd :: "(('a * 'b) * ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"

 where

   "fun_upd ((x, a), s) (s(x := f a))"

 code_pred fun_upd .

 thm fun_upd.equation

 section {* Another semantics *}

 types

   name = nat --"For simplicity in examples"

   state' = "name \<Rightarrow> nat"

 datatype aexp = N nat | V name | Plus aexp aexp

 fun aval :: "aexp \<Rightarrow> state' \<Rightarrow> nat" where

 "aval (N n) _ = n" |

 "aval (V x) st = st x" |

 "aval (Plus e\<^isub>1 e\<^isub>2) st = aval e\<^isub>1 st + aval e\<^isub>2 st"

 datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp

 primrec bval :: "bexp \<Rightarrow> state' \<Rightarrow> bool" where

 "bval (B b) _ = b" |

 "bval (Not b) st = (\<not> bval b st)" |

 "bval (And b1 b2) st = (bval b1 st \<and> bval b2 st)" |

 "bval (Less a\<^isub>1 a\<^isub>2) st = (aval a\<^isub>1 st < aval a\<^isub>2 st)"

 datatype

   com' = SKIP 

       | Assign name aexp         ("_ ::= _" [1000, 61] 61)

       | Semi   com'  com'          ("_; _"  [60, 61] 60)

       | If     bexp com' com'     ("IF _ THEN _ ELSE _"  [0, 0, 61] 61)

       | While  bexp com'         ("WHILE _ DO _"  [0, 61] 61)

 inductive

   big_step :: "com' * state' \<Rightarrow> state' \<Rightarrow> bool" (infix "\<Rightarrow>" 55)

 where

   Skip:    "(SKIP,s) \<Rightarrow> s"

 | Assign:  "(x ::= a,s) \<Rightarrow> s(x := aval a s)"

 | Semi:    "(c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2  \<Longrightarrow>  (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3  \<Longrightarrow> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3"

 | IfTrue:  "bval b s  \<Longrightarrow>  (c\<^isub>1,s) \<Rightarrow> t  \<Longrightarrow>  (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t"

 | IfFalse: "\<not>bval b s  \<Longrightarrow>  (c\<^isub>2,s) \<Rightarrow> t  \<Longrightarrow>  (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t"

 | WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s"

 | WhileTrue:  "bval b s\<^isub>1  \<Longrightarrow>  (c,s\<^isub>1) \<Rightarrow> s\<^isub>2  \<Longrightarrow>  (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3

                \<Longrightarrow> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"

 code_pred big_step .

 thm big_step.equation

 section {* Examples for detecting switches *}

 inductive detect_switches1 where

   "detect_switches1 [] []"

 | "detect_switches1 (x # xs) (y # ys)"

 code_pred [detect_switches, skip_proof] detect_switches1 .

 thm detect_switches1.equation

 inductive detect_switches2 :: "('a => bool) => bool"

 where

   "detect_switches2 P"

 code_pred [detect_switches, skip_proof] detect_switches2 .

 thm detect_switches2.equation

 inductive detect_switches3 :: "('a => bool) => 'a list => bool"

 where

   "detect_switches3 P []"

 | "detect_switches3 P (x # xs)" 

 code_pred [detect_switches, skip_proof] detect_switches3 .

 thm detect_switches3.equation

 inductive detect_switches4 :: "('a => bool) => 'a list => 'a list => bool"

 where

   "detect_switches4 P [] []"

 | "detect_switches4 P (x # xs) (y # ys)"

 code_pred [detect_switches, skip_proof] detect_switches4 .

 thm detect_switches4.equation

 inductive detect_switches5 :: "('a => 'a => bool) => 'a list => 'a list => bool"

 where

   "detect_switches5 P [] []"

 | "detect_switches5 P xs ys ==> P x y ==> detect_switches5 P (x # xs) (y # ys)"

 code_pred [detect_switches, skip_proof] detect_switches5 .

 thm detect_switches5.equation

 inductive detect_switches6 :: "(('a => 'b => bool) * 'a list * 'b list) => bool"

 where

   "detect_switches6 (P, [], [])"

 | "detect_switches6 (P, xs, ys) ==> P x y ==> detect_switches6 (P, x # xs, y # ys)"

 code_pred [detect_switches, skip_proof] detect_switches6 .

 inductive detect_switches7 :: "('a => bool) => ('b => bool) => ('a * 'b list) => bool"

 where

   "detect_switches7 P Q (a, [])"

 | "P a ==> Q x ==> detect_switches7 P Q (a, x#xs)"

 code_pred [skip_proof] detect_switches7 .

 thm detect_switches7.equation

 inductive detect_switches8 :: "nat => bool"

 where

   "detect_switches8 0"

 | "x mod 2 = 0 ==> detect_switches8 (Suc x)"

 code_pred [detect_switches, skip_proof] detect_switches8 .

 thm detect_switches8.equation

 inductive detect_switches9 :: "nat => nat => bool"

 where

   "detect_switches9 0 0"

 | "detect_switches9 0 (Suc x)"

 | "detect_switches9 (Suc x) 0"

 | "x = y ==> detect_switches9 (Suc x) (Suc y)"

 | "c1 = c2 ==> detect_switches9 c1 c2"

 code_pred [detect_switches, skip_proof] detect_switches9 .

 thm detect_switches9.equation

 end