src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy

back to post-release mode -- after fork point;

theory Predicate_Compile_Tests
imports "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
begin

declare [[values_timeout = 480.0]]

subsection \<open>Basic predicates\<close>

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 EmptyPred :: "'a \<Rightarrow> bool"

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

definition EmptyPred' :: "'a \<Rightarrow> bool"
where "EmptyPred' = (\<lambda> x. False)"

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

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: bool) False'' .

inductive EmptySet'' :: "'a \<Rightarrow> bool"
where
  "False \<Longrightarrow> EmptySet'' x"

code_pred (expected_modes: i => bool, o => bool) [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 .

text \<open>
  The following example was derived from an predicate in the CakeML formalisation provided by Lars Hupel.
\<close>
inductive predicate_where_argument_is_condition :: "bool \<Rightarrow> bool"
where
  "ck \<Longrightarrow> predicate_where_argument_is_condition ck"

code_pred predicate_where_argument_is_condition .

text \<open>Other similar examples of this kind:\<close>

inductive predicate_where_argument_is_in_equation :: "bool \<Rightarrow> bool"
where
  "ck = True \<Longrightarrow> predicate_where_argument_is_in_equation ck"

code_pred predicate_where_argument_is_in_equation .

inductive predicate_where_argument_is_condition_and_value :: "bool \<Rightarrow> bool"
where
  "predicate_where_argument_is_condition_and_value ck \<Longrightarrow> ck
     \<Longrightarrow> predicate_where_argument_is_condition_and_value ck"

code_pred predicate_where_argument_is_condition_and_value .

inductive predicate_where_argument_is_neg_condition :: "bool \<Rightarrow> bool"
where
  "\<not> ck \<Longrightarrow> predicate_where_argument_is_neg_condition ck"

code_pred predicate_where_argument_is_neg_condition .

inductive predicate_where_argument_is_neg_condition_and_in_equation :: "bool \<Rightarrow> bool"
where
  "\<not> ck \<Longrightarrow> ck = False \<Longrightarrow> predicate_where_argument_is_neg_condition_and_in_equation ck"

code_pred predicate_where_argument_is_neg_condition_and_in_equation .


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 \<open>We expect the user to expand the tuples in the values command.
The following values command is not supported.\<close>
(*values "{x. zerozero x}" *)
text \<open>Instead, the user must type\<close>
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 => natural => bool"
where
  "JamesBond 0 0 7"

code_pred JamesBond .

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

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


subsection \<open>Alternative Rules\<close>

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 is_D_or_E.prems 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(1) show thesis by simp
    next
      assume "xa = E" from this x is_D_or_E(2) 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 \<open>Compilation of is_FGH requires elimination rule for is_F_or_G\<close>

code_pred (expected_modes: o => bool, i => bool) is_FGH
proof -
  case is_F_or_G
  from is_F_or_G.prems 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(1) show thesis by simp
    next
      assume "xa = G"
      from this x is_F_or_G(2) show thesis by simp
    qed
  qed
qed

subsection \<open>Named alternative rules\<close>

inductive appending
where
  nil: "appending [] ys ys"
| cons: "appending xs ys zs \<Longrightarrow> appending (x#xs) ys (x#zs)"

lemma appending_alt_nil: "ys = zs \<Longrightarrow> appending [] ys zs"
by (auto intro: appending.intros)

lemma appending_alt_cons: "xs' = x # xs \<Longrightarrow> appending xs ys zs \<Longrightarrow> zs' = x # zs \<Longrightarrow> appending xs' ys zs'"
by (auto intro: appending.intros)

text \<open>With code_pred_intro, we can give fact names to the alternative rules,
  which are used for the code_pred command.\<close>

declare appending_alt_nil[code_pred_intro alt_nil] appending_alt_cons[code_pred_intro alt_cons]
 
code_pred appending
proof -
  case appending
  from appending.prems show thesis
  proof(cases)
    case nil
    from appending.alt_nil nil show thesis by auto
  next
    case cons
    from appending.alt_cons cons show thesis by fastforce
  qed
qed


inductive ya_even and ya_odd :: "nat => bool"
where
  even_zero: "ya_even 0"
| odd_plus1: "ya_even x ==> ya_odd (x + 1)"
| even_plus1: "ya_odd x ==> ya_even (x + 1)"


declare even_zero[code_pred_intro even_0]

lemma [code_pred_intro odd_Suc]: "ya_even x ==> ya_odd (Suc x)"
by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)

lemma [code_pred_intro even_Suc]:"ya_odd x ==> ya_even (Suc x)"
by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)

code_pred ya_even
proof -
  case ya_even
  from ya_even.prems show thesis
  proof (cases)
    case even_zero
    from even_zero ya_even.even_0 show thesis by simp
  next
    case even_plus1
    from even_plus1 ya_even.even_Suc show thesis by simp
  qed
next
  case ya_odd
  from ya_odd.prems show thesis
  proof (cases)
    case odd_plus1
    from odd_plus1 ya_odd.odd_Suc show thesis by simp
  qed
qed

subsection \<open>Preprocessor Inlining\<close>

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: fun_eq_iff)
    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 \<open>if preprocessing fails, zerozero'' will not have all modes.\<close>

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

subsection \<open>Sets\<close>
(*
inductive_set EmptySet :: "'a set"

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

definition EmptySet' :: "'a set"
where "EmptySet' = {}"

code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
*)
subsection \<open>Numerals\<close>

definition
  "one_or_two = (%x. x = Suc 0 \<or> ( x = 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, Suc (Suc 0)}"] "{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'' == (%x. x = 1 \<or> x = (2::nat))"

code_pred [inductify] one_or_two'' .
thm one_or_two''.equation

values "{x. one_or_two'' x}"

subsection \<open>even predicate\<close>

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, Suc (Suc 0)}" dseq 3] 8 "{x. even x}"
values [expected "{0, Suc (Suc 0)}" dseq 4] 8 "{x. even x}"
values [expected "{0, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))}" 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 \<open>append predicate\<close>

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, Suc (Suc 0), Suc (Suc (Suc 0)), Suc (Suc (Suc (Suc 0))), Suc (Suc (Suc (Suc (Suc 0))))])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
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 "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
value "Predicate.the (slice ([]::int list))"


text \<open>tricky case with alternative rules\<close>

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.prems show thesis
  proof
    fix xs
    assume "xa = []" "xb = xs" "xc = xs"
    from this append2(1) 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(2) show thesis by fastforce
  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 \<open>map_ofP predicate\<close>

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 \<open>filter predicate\<close>

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, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))]}"] "{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, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))]}" 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 filter3 .
thm filter3.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 \<open>reverse predicate\<close>

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 \<open>partition predicate\<close>

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 \<open>transitive predicate\<close>

text \<open>Also look at the tabled transitive closure in the Library\<close>

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 tranclp.prems] 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 \<open>values command needs mode annotation of the parameter succ
to disambiguate which mode is to be chosen.\<close> 

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 \<open>rtrancl compilation is strange!\<close>
(*
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 \<open>Free function variable\<close>

inductive FF :: "nat => nat => bool"
where
  "f x = y ==> FF x y"

code_pred FF .

subsection \<open>IMP\<close>

type_synonym var = nat
type_synonym state = "int list"

datatype com =
  Skip |
  Ass var "state => int" |
  Seq com com |
  IF "state => bool" com com |
  While "state => bool" com

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 \<open>CCS\<close>

text\<open>This example formalizes finite CCS processes without communication or
recursion. For simplicity, labels are natural numbers.\<close>

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

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 \<open>divmod\<close>

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 "Predicate.the (divmod_rel_i_i_o_o 1705 42)"

subsection \<open>Transforming predicate logic into logic programs\<close>

subsection \<open>Transforming functions into logic programs\<close>
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 \<open>Minimum\<close>

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 \<open>Lexicographic order\<close>
text \<open>This example requires to handle the differences of sets and predicates in the predicate compiler,
or to have a copy of all definitions on predicates due to the set-predicate distinction.\<close>

(*
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 fastforce
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 fastforce
    apply fastforce 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 \<open>AVL Tree\<close>

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
(* TODO: has highly non-deterministic execution time!

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 \<open>Definitions about Relations\<close>
(*
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] relcomp .
thm relcomp.equation
code_pred [inductify] Image .
thm Image.equation
declare singleton_iff[code_pred_inline]
declare Id_on_def[unfolded Bex_def UNION_eq 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_unfold
code_pred (modes:
  (o * o => bool) => o => bool,
  (o * o => bool) => i => bool,
  (i * o => bool) => i => bool) [inductify] Domain .
thm Domain.equation

thm Domain_converse [symmetric]
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 \<open>Inverting list functions\<close>

code_pred [inductify, skip_proof] size_list' .
code_pred [new_random_dseq inductify] size_list' .
thm size_list'P.equation
thm size_list'P.new_random_dseq_equation

values [new_random_dseq 2,3,10] 3 "{xs. size_list'P (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 .

section \<open>Function predicate replacement\<close>

text \<open>
If the mode analysis uses the functional mode, we
replace predicates that resulted from functions again by their functions.
\<close>

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 \<open>If append is not turned into a predicate, then the mode
  o => o => i => bool could not be inferred.\<close>

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

text \<open>If appendP is not reverted back to a function, then mode i => i => o => bool
  fails after deleting the predicate equation.\<close>

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

text \<open>Redeclaring append.equation as code equation\<close>

declare appendP.equation[code]

subsection \<open>Function with tuples\<close>

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 \<open>Arithmetic examples\<close>

subsection \<open>Examples on nat\<close>

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 "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))}"] "{z. plus_nat_test 4 5 z}"
values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))}"] "{z. plus_nat_test 7 2 z}"
values [expected "{Suc (Suc (Suc (Suc 0)))}"] "{y. plus_nat_test 5 y 9}"
values [expected "{}"] "{y. plus_nat_test 9 y 8}"
values [expected "{Suc (Suc (Suc (Suc (Suc (Suc 0)))))}"] "{y. plus_nat_test 1 y 7}"
values [expected "{Suc (Suc 0)}"] "{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, Suc (Suc (Suc (Suc (Suc 0))))),
                  (Suc 0, Suc (Suc (Suc (Suc 0)))),
                  (Suc (Suc 0), Suc (Suc (Suc 0))),
                  (Suc (Suc (Suc 0)), Suc (Suc 0)),
                  (Suc (Suc (Suc (Suc 0))), Suc 0),
                  (Suc (Suc (Suc (Suc (Suc 0)))), 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 "{Suc (Suc (Suc (Suc (Suc 0))))}"] "{z. minus_nat_test 7 2 z}"
values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))}"] "{x. minus_nat_test x 7 9}"
values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))}"] "{x. minus_nat_test x 9 7}"
values [expected "{0, Suc 0, Suc (Suc 0), Suc (Suc (Suc 0))}"] "{x. minus_nat_test x 3 0}"
values [expected "{0::nat}"] "{x. minus_nat_test x 0 0}"

subsection \<open>Examples on int\<close>

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 \<open>minus on bool\<close>

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 \<open>Functions\<close>

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 \<open>Locales\<close>

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 \<open>The global introduction rules must be redeclared as introduction rules and then 
  one could invoke code_pred.\<close>

declare A.hd_predicate_in_locale.intros [code_pred_intro]

code_pred (expected_modes: i => i => i => bool, i => i => o => bool) A.hd_predicate_in_locale
by (auto elim: A.hd_predicate_in_locale.cases)
    
interpretation A partial_hd .
thm hd_predicate_in_locale.intros
text \<open>A locally compliant solution with a trivial interpretation fails, because
the predicate compiler has very strict assumptions about the terms and their structure.\<close>
 
(*code_pred hd_predicate_in_locale .*)

section \<open>Integer example\<close>

definition three :: int
where "three = 3"

inductive is_three
where
  "is_three three"

code_pred is_three .

thm is_three.equation

section \<open>String.literal example\<close>

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 \<open>Another function example\<close>

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 \<open>Examples for detecting switches\<close>

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

text \<open>The higher-order predicate r is in an output term\<close>

datatype result = Result bool

inductive fixed_relation :: "'a => bool"

inductive test_relation_in_output_terms :: "('a => bool) => 'a => result => bool"
where
  "test_relation_in_output_terms r x (Result (r x))"
| "test_relation_in_output_terms r x (Result (fixed_relation x))"

code_pred test_relation_in_output_terms .

thm test_relation_in_output_terms.equation


text \<open>
  We want that the argument r is not treated as a higher-order relation, but simply as input.
\<close>

inductive test_uninterpreted_relation :: "('a => bool) => 'a list => bool"
where
  "list_all r xs ==> test_uninterpreted_relation r xs"

code_pred (modes: i => i => bool) test_uninterpreted_relation .

thm test_uninterpreted_relation.equation

inductive list_ex'
where
  "P x ==> list_ex' P (x#xs)"
| "list_ex' P xs ==> list_ex' P (x#xs)"

code_pred list_ex' .

inductive test_uninterpreted_relation2 :: "('a => bool) => 'a list => bool"
where
  "list_ex r xs ==> test_uninterpreted_relation2 r xs"
| "list_ex' r xs ==> test_uninterpreted_relation2 r xs"

text \<open>Proof procedure cannot handle this situation yet.\<close>

code_pred (modes: i => i => bool) [skip_proof] test_uninterpreted_relation2 .

thm test_uninterpreted_relation2.equation


text \<open>Trivial predicate\<close>

inductive implies_itself :: "'a => bool"
where
  "implies_itself x ==> implies_itself x"

code_pred implies_itself .

text \<open>Case expressions\<close>

definition
  "map_prods xs ys = (map (%((a, b), c). (a, b, c)) xs = ys)"

code_pred [inductify] map_prods .

end