[isabelle] Parity refined

Hi all,

I am planning some steps to let three separate constructs in
Isabelle/HOL converge:
* The plain predicate expression »2 dvd _«.
* The predicate »even _« (with the obvious abbreviation »odd _«).
* The predicate expression »_ mod 2 _ = 0«.

Convergence here means the following things:
* Augmented simplifier rewrite rules on »2 dvd _« to gain the same
automation as for expressions involving »_ mod 2 _ = 0«;
* A type class hierarchy to develop »even« uniformly algebraically for
nat and int;
* Replacing definition »even« by a simple abbreviation »even a == 2 dvd
a« within a certain algebraic type class (presumable what is currently
named class »semiring_div_parity«) – n.b. at this stage I am unsure
whether this should be a mere input abbreviation or not.

With this more unified concept of parity, it should be possible
* to integrate the existing infrastructure for division of numeral
expressions (class »semiring_numeral_div«) into the whole picture;
* to bootstrap division on integer solely relying on division of nat
without funny auxiliary definitions;
* to provide native simp rules for division on nat numerals, without
relying on int here altogether.

A future perspective could be to unify and simplify the
bit-representation stuff from the HOL-Word theories.

I am looking forward to comments and suggestions.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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