Here is a sample theory:
datatype ty = A | B | C
inductive test where
"test A B"
| "test B B"
| "test B C"
inductive test2 where
"The (λy. test x y) = y ⟹
test2 x y"
code_pred [show_modes] test2 .
values "{x. test2 A x}"
The generated code tries to enumerate over ty and fails (as in How to generate code for the existential quantifier). I can't make the data type an instance of enum.
The following code equation is generated:
test2_i_o ?xa ≡
Predicate.bind (Predicate.single ?xa)
(λxa. Predicate.bind (eq_i_o (The (test xa))) Predicate.single
I guess the error is raised because the equation contains test instead of test_i_o.
Could you suggest how to define such a predicate?
I've got it. I should not use The operator. The predicate should be defined as follows. Code is generated fine with the inductify directive. An auxiliary predicate is generated in this case.
inductive test_uniq where
"test x y ⟹
(∀z. test x z ⟶ y = z) ⟹
test_uniq x y"
code_pred [inductify, show_modes] test_uniq .
Alternatively one can define the auxiliary predicate explicitly:
inductive test_not_uniq where
"test x z ⟹
y ≠ z ⟹
test_not_uniq x y"
inductive test_uniq where
"test x y ⟹
¬ test_not_uniq x y ⟹
test_uniq x y"
code_pred [show_modes] test_uniq .
Old Wrong Answer
Maybe It could help someone to generate code for The operator:
inductive test_ex where
"The (λy. test x y) = y ⟹
test_ex x y"
code_pred [show_modes] test .
lemma test_ex_code [code_pred_intro]:
"Predicate.the (test_i_o x) = y ⟹
test_ex x y"
by (rule test_ex.intros) (simp add: Predicate.the_def test_i_o_def)
code_pred [show_modes] test_ex
by (metis test_ex.cases test_ex_code)
inductive test2 where
"test_ex x y ⟹
test2 x y"
code_pred [show_modes] test2 .
values "{x. test2 A x}"
The code equation now contains test_i_o instead of test:
test_ex_i_o ?xa =
Predicate.bind (Predicate.single ?xa)
(λxa. Predicate.bind (eq_i_o (Predicate.the (test_i_o xa))) Predicate.single)