Hi all, following http://isabelle.in.tum.de/reports/Isabelle/rev/ea5bc46c11e6, the first time in Isabelle repository a usable and reasonable abstract specification of gcd and lcm came to light.
Interested volunteers are welcome to go ahead and
* generalize more properties from nat and int to abstract
specifications, from theories
src/HOL/GCD.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
* identity duplicates by branding them accordingly:
lemmas foo_nat = foo [where ?'a = nat]
lemma foo_nat "…" by (fact foo)
* purging duplicates from he distribution and the AFP, building a
corresponding NEWs entry.
After this clarification the next step can be envisaged: a generic
specification of an euclidean ring (with euclidean division and
euclidean algorithm).
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
