Unable to evaluate expressions with a reflexive transitive closure

user_632199 0
Viewed 54

The following expressions are almost identical:

value "(1,5) ∈ trancl {(1::nat,2::nat),(2,5)}"
value "(1,5) ∈ rtrancl {(1::nat,2::nat),(2,5)}"

However the first one is evaluated fine, and for the second one I get the following error:

Wellsortedness error:
Type nat not of sort {enum,equal}
No type arity nat :: enum

It seems that the error is caused by the identity relation:

value "(1::nat,5::nat) ∈ Id"

However the following code lemma doesn't help:

lemma Id_code [code]: "(a, b) ∈ Id ⟷ a = b" by simp

Could you please suggest how to fix it? Why it doesn't work from the scratch? Is it just an incompleteness of code lemmas or there are more fundamental reasons?

isabelle
1 Answers

The problem becomes apparent when you look at the code equations for rtrancl with code_thms rtrancl:

rtrancl r ≡ trancl r ∪ Id

Here, Id is the identity relation, i.e. the set of all (x, x). If your type is infinite, both Id and its complement will also be infinite, and there is no way to represent that in a set with the Isabelle code generator's default set representation (which is as lists of either all the elements that are in the set or all the elements that are not in the set).

The code equation for Id reflects this as well:

Id = (λx. (x, x)) ` set enum_class.enum

Here, enum_class.enum comes from the enum type class and is a list of all values of a type. This is where the enum constraint comes from when you try to evaluate rtrancl.

I don't think it's possible to evaluate rtrancl without modifying the representation of sets in the code generator setup (and even then, printing the result in a readable form would be challenging). However, getting the code generator to evaluate things like (1, 5) ∈ rtrancl … is relatively easy: you can simply register a code unfold rule like this:

lemma in_rtrancl_code [code_unfold]: "z ∈ rtrancl A ⟷ fst z = snd z ∨ z ∈ trancl A"
  by (metis prod.exhaust_sel rtrancl_eq_or_trancl)

Then your value command works fine.

user_21442270
Related