Re: [isabelle] No type arity nat :: equal

> I get this error
> Wellsortedness error:
> Type nat not of sort {equal,order}
> No type arity nat :: equal
> What do I need to do?
> In a bit more detail: I have generalised the Regular-Sets AFP entry by replacing
> nat by 'a::order. This results in the above error when executing the proof
> method regexp. The latter intentionally still uses nat, but I expected the class
> system to take care of that.

A rough guess: when

  check_eqv :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> bool" …

is generalized to

  check_eqv :: "'a::order rexp \<Rightarrow> 'a::order rexp
\<Rightarrow> bool" …

the instance nat :: equal is not present in the transitive closure of
code equations specified in

> val regexp_conv = Code_Runtime.static_holds_conv thy
>       [ at {const_name Zero}, @{const_name One}, @{const_name Atom}, @{const_name Plus},
>        @{const_name Times}, @{const_name Star}, 
>        @{const_name check_eqv}, @{const_name Trueprop}]

This is easiest resolve by defining a separate

definition check_eqv :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow>
bool" …
  "check_eqv = Equivalence_Checking.check_eqv"

in Regexp_Method.thy and using this in the the definition of regexp_conv
(which in this case means not to change the text of this definition).

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.