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:11 

barrucadu joined #isabelle 
09:11 

barrucadu joined #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 
21:26 

barrucadu joined #isabelle 
23:16 
tautologico 
what's {0..<n}, a set? 
23:18 
tautologico 
my first idea was using a (HOL) set to represent the group set, but then I switched to using a type, because then I can specify the group operation as 'a => 'a => 'a 
23:19 
tautologico 
in the HOL semantics a type is supposed to denote a set 
23:19 
tautologico 
but there are difficulties like specifying Zn or Z* (integers without zero) 