CODEWITHSUNDEEP
radixisabellemodular-arithmetic
Charles Staats
Charles Staats

Reputation: 203

Base-n integer representations library in Isabelle/HOL?

Context: I am trying to translate math contest problems into Isabelle/HOL. A lot of these contest problems involve questions like "what are the last two digits of this number when written in base 7"?

Isabelle/HOL has a rudimentary treatment of base-10 integer representations in the ThreeDivides theory. It also has a far more elaborate theory for binary numeral representations. And arguably the fundamental nat datatype is a base-one representation. But so far I have been unable to find any theory file that deals with base-n representations in general. Am I missing anything?

I'd like it to include basic theorems like the existence and uniqueness of the representation (which ThreeDivides actually does not show for its decimal representations), an easy way to write things down (e.g., "[4, 3]⇘base 5⇙ = 23"), and basic rules for manipulation. I can create such a theory file myself of course, but I'd rather not waste the time if it already exists.

Is there a standard theory in Isabelle/HOL for stating and proving facts about the digits of integers in arbitrary natural number bases?

Upvotes: 2

Views: 62

Answers (0)

Related Questions