Re: [isabelle] Questions about number representation in Isabelle



(2) What is the best way in Isabelle to change the representation of
naturals or integers? I am not just talking about types_code
directive, which maps an Isabelle type into an unrelated ML type, but
a representation whose properties (like commutativity of addition) can
be proved in Isabelle.

If you want to use a different representation in the logic but retain all the theorems that you have for the old representation, you essentially have to reprove them. The only way to automate this to a large degree is by factoring out a common axiomatic basis. Then you can use Isabelle's proof terms to reply the old proof but plugging in the new basis. The AWE project may provide the necessary automation: http://www.informatik.uni-bremen.de/~cxl/awe/

If you are "only" interested in code generation, you could use types_code in a disciplined manner: if you want to implement t by t', you describe t' and its operations in HOL and show (roughly speaking) that there is a homomorphism from t' to t. This is not completely foundational because you could make a mistake when writing down the necessary homomorphism conditions.

Tobias





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