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 nonalgebraic 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 HOLAlgebra 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 