I'm trying to evaluate terms corresponding to the type t defined as follows.
typedef t = "{(0::nat)..10}" by auto
To evaluate terms of type t, I simply define Abs_t as a constructor.
lemma [code abstype]: "Abs_t (Rep_t x) = x" by (rule Rep_t_inverse)
code_datatype Abs_t
This allows me to use, for example,
value "Abs_t 4"
Now, I want to evaluate terms of the form Rep_t x such that they map back to naturals.
However, Rep_t (Abs_t x) = x only holds for x in {(0::nat)..10} so it cannot be used as a code equation.
I can write a single code equation for each element in the domain like so
lemma[code]:
"Rep_t (Abs_t 0) = 0"
"Rep_t (Abs_t 1) = 1"
(* ... *)
"Rep_t (Abs_t 10) = 10"
by(auto simp add: Abs_t_inverse)
but that becomes infeasible for larger domains.
What is the proper way to define code equations such that value "(Rep_t (Abs_t x))" evaluates to x::nat for all x in the domain?
I tried to use the code equations
lemma [code abstype]: "Rep_t (Abs_t x) = x"
which failed for the reason explained above. I also tried to used
lemma [code abstype]: "Rep_t (Abs_t x) = (if x \in {(0::nat)..10} then x else undefined)"
which I could not manage to proof.