# IRC log for #isabelle, 2015-12-28

All times shown according to UTC.

Time Nick Message
02:47 ilbot3 joined #isabelle
02:47 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
08:01 lispy joined #isabelle
08:08 ThreeOfEight tautologico: it's the set of numbers between 0 and n, including 0 but excluding n
08:08 ThreeOfEight using a type is more convenient, but you get into trouble when you want to look at a subgroup of a group
08:09 ThreeOfEight for that, you would need something like a local type definition, which Isabelle does not support (yet)
08:09 ThreeOfEight that's why HOL Algebra uses explicit carrier sets
08:10 ThreeOfEight but that gets a bit tedious because you have to carry around assumptions like "x ∈ carrier G" all the time
08:10 ThreeOfEight in "standard" Isabelle/HOL, "group" etc. is a typeclass
08:10 ThreeOfEight well, actually, no, "group_add" is a typeclass
08:11 ThreeOfEight and "ring", "field", etc. are typeclasses
08:11 ThreeOfEight that makes things much more convenient, but you can only define one ring structure, one field etc. on every type
08:12 ThreeOfEight that is sufficient for most non-algebraic mathematics, since there is usually only one generally useful ring/field/whatever structure on integers, reals, etc.
08:13 ThreeOfEight but in Algebra, you usually want to look at subgroups and subrings and then you have things like field extensions and things become much more painful
08:13 ThreeOfEight which is why HOL-Algebra uses a kind of dictionary construction, where a group/ring/field is just a record containing the carrier and all the operations
08:14 ThreeOfEight unfortunately, HOL Algebra has not seen much development in the last few years because of the difficulties I mentioned
10:51 tautologico ThreeOfEight: this is good to know, thank you
10:51 tautologico I didn't use a typeclass because I wanted to have more than one instance of group for the same type