Email Gateway (Aug 19 2022 at 14:15): Email Gateway (Aug 19 2022 at 14:15):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
I am planning some steps to let three separate constructs in
Isabelle/HOL converge:
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
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC