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:

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.


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