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

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/
14:57 tautologico say I formalize groups as locales, how can I formalize Zn, the group of integers with addition modulo n? (for all n)
14:58 tautologico I thought about defining a locale that imports group and fixes n
14:58 tautologico but I'd like to prove just once that Zn is a group for all n
19:43 ThreeOfEight tautologico: you'd probably define a function "int_mod :: nat => nat set group"
19:44 ThreeOfEight that takes a nat as its parameter (the modulus) and returns a group structure where the elements are the equivalence classes modulo the modulus
19:44 ThreeOfEight and then you prove something like "group (int_mod n)"
19:45 ThreeOfEight although I would imagine it's easier to just define them as a factor group
19:45 ThreeOfEight not sure if Isabelle already has factor groups, but it probably does
19:47 tautologico hmm
19:48 tautologico I haven't considered to return a group from a function... actually I don't think I know how to do it yet
20:09 ThreeOfEight are you using HOL Algebra?
20:10 ThreeOfEight iirc, groups in HOL algebra are simply records that specify the carrier set, the operation, the neutral element etc.
20:13 tautologico no
20:14 tautologico I will look up the standard definitions later
20:14 tautologico I wanted to try and define them on my own
21:08 ThreeOfEight well you can still do it
21:09 ThreeOfEight you should probably prove a theorem like "group {0..<n} 0 (λx y. (x + y) mod n) (λx. (-x) mod n)"
21:10 ThreeOfEight or whatever your group definition looks like
21:10 ThreeOfEight but I would imagine it's something like that