[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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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