CODEWITHSUNDEEP
typescode-generationisabelleisar
Username
Username

Reputation: 11

How to evaluate Rep of new type in Isabelle?

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.

Upvotes: 1

Views: 68

Answers (0)

Related Questions