Here is a sample theory:
datatype ty = A | B | C
inductive test where
"test A B"
| "test B C"
inductive test2 where
"¬(∃z. test x z) ⟹ test2 x"
code_pred [show_modes] test .
code_pred [show_modes] test2 .
values "{x. test2 A}"
The generated code tries to enumerate over ty. And so it fails.
I'm tring to define an executable version of test predicate:
definition "test_ex x ≡ ∃y. test x y"
definition "test_ex_fun x ≡
Predicate.singleton (λ_. False)
(Predicate.map (λ_. True) (test_i_o x))"
lemma test_ex_code [code_abbrev, simp]:
"test_ex_fun = test_ex"
apply (intro ext)
unfolding test_ex_def test_ex_fun_def Predicate.singleton_def
apply (simp split: if_split)
But I can't prove the lemma. Could you suggest a better approach?
Existential quantifiers over an argument to an inductive predicate can be made executable by introducing another inductive predicate. For example:
inductive test2_aux where "test x z ==> test2_aux x"
inductive test2 where "~ test2_aux x ==> test2 x"
with appropriate code_pred statements. The free variable z in the premise of test2_aux acts like an existential. Since this transformation is canonical, code_pred has a preprocessor to do so:
code_pred [inductify] test2 .
does the job.
Well, values complains about the fact that ty is not of sort enum. So, in this particular case it is easiest to perform this instantiation.
instantiation ty :: enum
begin
definition enum_ty :: "ty list" where
"enum_ty = [A,B,C]"
definition "enum_all_ty f = list_all f [A,B,C]"
definition "enum_ex_ty f = list_ex f [A,B,C]"
instance
proof (intro_classes)
let ?U = "UNIV :: ty set"
show id: "?U = set enum_class.enum"
unfolding enum_ty_def
using ty.exhaust by auto
fix P
show "enum_class.enum_all P = Ball ?U P"
"enum_class.enum_ex P = Bex ?U P"
unfolding id enum_all_ty_def enum_ex_ty_def enum_ty_def by auto
show "distinct (enum_class.enum :: ty list)" unfolding enum_ty_def by auto
qed
Afterwards, your values-command evaluates without problems.
I thought that the lemma is unprovable, and I should find another approach. But it can be proven as follows:
lemma test_ex_code [code_abbrev, simp]:
"Predicate.singleton (λ_. False)
(Predicate.map (λ_. True) (test_i_o x)) = (∃y. test x y)"
apply (intro ext iffI)
unfolding Predicate.singleton_def
apply (simp_all split: if_split)
apply (metis SUP1_E mem_Collect_eq pred.sel test_i_o_def)
apply (intro conjI impI)
apply (smt SUP1_E the_equality)
apply (metis (full_types) SUP1_E SUP1_I mem_Collect_eq pred.sel test_i_o_def)
done
The interesting thing is that the lemma structure and the proof structure seems to be independent of the concrete predicate. I guess there could be a general solution for any predicate.
