# IRC log for #isabelle, 2017-06-28

All times shown according to UTC.

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. (Isabelle2016-1)
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.isa-afp.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 finite-dimensional
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