I'm trying to export code for functions with quantifiers based on a type declared using typedecl, i.e., something like this:
typedecl x
consts set_x1 :: "x set"
consts set_x2 :: "x set"
definition func_1 :: "x set ⇒ bool" where
"func_1 s ≡ ∀ x ∈ s. x ∈ set_x1 ∧ x ∈ set_x2"
definition func_2 :: "x set ⇒ bool" where
"func_2 s ≡ ∃ x ∈ s. x ∈ set_x1 ∧ x ∈ set_x2"
export_code
func_1
func_2
in Haskell module_name funcs
When trying to export, I get a ''wellsortedness error" because type x has not been defined as belonging to the "equal" class. I've tried to bypass this by using axiomatization:
axiomatization where x_equal: "OFCLASS(x, equal_class)"
axiomatization where x_enum: "OFCLASS(x, enum_class)"
instance x :: equal by (rule x_equal)
instance x :: enum by (rule x_enum)
However, I still get the following error saying that some code equations for comparing instances of x are missing:
No code equations for equal_x_inst.equal_x, set_x2, set_x1
For some other functions (not shown here), I also get messages saying that the equations enum_x_inst.enum_ex_x and enum_x_inst.enum_all_x are missing (I've also axiomatized x as being of class enum, as shown above).
How can I define these code equations? The ones for the constant sets seem relatively simple, but I'm not sure how to write the lemmas for the others, and I can't find any examples of something similar online.