Time 
Nick 
Message 
01:48 

ilbot3 joined #isabelle 
01:48 

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/ 
05:54 
pruvisto 
qwertyyyy: what version of Isabelle are you using? 
05:55 
pruvisto 
this sounds like you're using something like Isabelle 2011, where sets and predicates were the same 
05:55 
pruvisto 
my interpretation is that this means that "P(a_1) = True" and "P(x) = False" for any other x 
08:55 

ammbauer joined #isabelle 
10:55 
qwertyyyy 
pruvisto: I'm actually using the "latest" version. (Isabelle20161) 
10:59 
pruvisto 
hm, indeed 
10:59 
pruvisto 
perhaps this is some quirky printing artefact 
10:59 
pruvisto 
or something related to the way QuickCheck does termification 
10:59 
pruvisto 
in any case, the intended meaning is probably exactly what I said above 
11:42 
qwertyyyy 
pruvisto: ok thank you :) 
12:01 

silver joined #isabelle 
12:08 

ammbauer joined #isabelle 
12:15 

exprosic joined #isabelle 
12:18 

exprosic left #isabelle 
14:04 
chindy 
pruvisto: did you have any special reason for using predicates in opose to sets of pairs here https://www.isaafp.org/browser_info/current/AFP/Randomised_Social_Choice/Order_Predicates.html 
14:11 
pruvisto 
chindy: in my experience, predicates are nicer to handle 
14:11 
larsrh 
should've used fsets 
14:12 
pruvisto 
sets of pairs would have worked, too 
14:12 
chindy 
larsrh: what are fsets? 
14:12 
pruvisto 
might actually have been a better choice considering the library material and possibly the notation 
14:12 
pruvisto 
but I do think the proofs get a little nicer when using predicates 
14:12 
larsrh 
chindy: I was just trolling 
14:12 
larsrh 
fsets are finite sets 
14:12 
pruvisto 
it seems more "natural" 
14:12 
larsrh 
they're awesome but also horrible to use 
14:12 
chindy 
i see 
14:13 
pruvisto 
more precisely, they are sets whose finiteness is encoded in the type 
14:13 
pruvisto 
i.e. if you have something of type fset, you automatically know that it's finite 
14:13 
larsrh 
and you can recurse through them in datatypes 
14:13 
pruvisto 
so you don't have to carry around the assumption that they're finite explicitly 
14:13 
larsrh 
(in a way that Cantor doesn't come to your house and wants to have a chat about cardinality) 
14:13 
chindy 
:) i see 
15:09 
chindy 
What is the difference between locales and (type) classes? 
15:37 
pruvisto 
locales are more general in a sense 
15:38 
pruvisto 
a type class is essentially the same thing as a Haskell type class with additional assumptions that need to hold 
15:38 
pruvisto 
type classes also use locales internally, i.e. each type class corresponds to a locale 
15:39 
pruvisto 
the idea of a locale is that you have a "named context" that contains certain constants and facts about them (like e.g. a monoid, a group, a Social Decision Scheme) 
15:39 
pruvisto 
a type class is essentially a locale that fixes a single type plus some constants with assumptions and that is interpreted automatically 
15:40 
pruvisto 
so in particular, for each type, there is a /unique/ interpretation of that locale 
15:41 
pruvisto 
e.g. there is a class "monoid_add" that fixes a type 'a and constants 0 :: 'a and + :: 'a => 'a => 'a and assumes that the usual monoid laws hold for them 
15:41 
pruvisto 
and then you have instances for nat, int, rat, real, complex etc. 
15:41 
pruvisto 
but you could also have instances e.g. for pairs or lists etc. 
15:41 
pruvisto 
that say "if 'a and 'b are monoid_add, then 'a × 'b is also monoid_add" 
15:42 
pruvisto 
it's less flexible than defining and interpreting all the locales by hand, but also more convenient 
18:40 
chindy 
my maths knowledge fails me quite a bit right now... but can someone explain what the difference between real_inner and euclidean_space is? I.e. what doe the addition Basis and 4 assumption entail? 
19:00 
pruvisto 
chindy: a Euclidean space is finitedimensional 
19:01 
pruvisto 
in the isabelle definition, we also assume that we have a orthonormal basis 
19:01 
pruvisto 
(I think the normal mathematical definition doesn't do that, because it can be shown that such a basis always exists) 
19:01 
pruvisto 
(but in the context of Isabelle, it is useful to really explicitly have a canonical one) 
23:38 

silver joined #isabelle 
23:49 

silver joined #isabelle 