Is it possible to make the following example work?
inductive elems where
"x |∈| xs ⟹
elems xs x"
code_pred [show_modes] elems .
values "{x. elems {|1::nat,2,3|} x}"
The predicate compiler by default does not know anything about finite sets and the membership operator |∈|. However, if you add the following snippet, then it works.
lemma fmember_code_predI [code_pred_intro]:
"x |∈| xs" if "Predicate_Compile.contains (fset xs) x"
using that by(simp add: Predicate_Compile.contains_def fmember.rep_eq)
code_pred fmember
by(simp add: Predicate_Compile.contains_def fmember.rep_eq)
Here's why this works: The constant Predicate_Compile.contains implements enumeration for ordinary sets and the predicate compiler knows about it. The lemma with the attribute code_pred_intro tells the predicate compiler to treat membership on fset as if it was defined as an inductive predicate with the lemma statement as introduction rule. At the code_pred command itself, you then have to prove the corresponding elimination rule. These two rules (introduction and elimination rule) are enough for the predicate compiler to do the mode analysis and compile the equations and prove them correct.
You don't even need to define your own predicate elems. Membership on fset works directly:
values "{x. x |∈| {|1::nat,2,3|}}"