Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error



Dear Gottfried,

arities declares that a type belongs to the given type class, but leaves the parameters of the type class uninterpreted and the assumptions unproven. Thus, it is like axiomatisation: you can use it to introduce inconsistencies. Here's an example:

class false = assumes FalseI: "x = x ==> False"

typedecl my_type
arities my_type :: false

lemma "False"
apply(rule FalseI)
apply(rule refl)
done

Without the arities command, I could not finish the proof of the lemma, because Isabelle does not know whether the type class "false" can be instantiated at all. With the arities command, I declare that my_type satisfies the axiom FalseI for all x of type my_type.

Hence, arities (like axiomatization) belongs to the group of commands for an axiomatic approach to formalisations. As most people nowadays prefer a definitional approach, I would not call arities frequently used.

Have said all this, it is obvious that the arities declarations make the error messages for the values command go away. But not for the code generator, it will continue to complain about missing code equations for the type class parameters. The second evaluation strategy (normalisation by evaluation) works.

Andreas





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