# IRC log for #isabelle, 2017-07-13

All times shown according to UTC.

Time Nick Message
00:06 Merv_ joined #isabelle
00:45 dmiles joined #isabelle
01:36 Merv_ joined #isabelle
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/
02:37 Merv_ joined #isabelle
04:07 Merv_ joined #isabelle
07:02 Merv_ joined #isabelle
08:50 chindy Mr. Harrison would be pleased!
09:47 larsrh in unrelated news, isabellectl will soon be able to bootstrap a repository clone
10:38 chindy How can it be that there is no definition of argmax in Isabelle?
10:42 pruvisto chindy: there is now
10:42 pruvisto in Lattices_Big in the development version of Isabelle
10:42 chindy ahh... finally :D now i just have to wait for the next release :D
10:42 pruvisto and the answer to why there wasn't one before is because people didn't need it that much ;)
10:43 pruvisto the problem is that it is, in general, a multi-valued function
10:43 pruvisto there are still a lot of facts missing about it though
10:43 chindy well "my version" has literally one fact... sooo... yea
10:50 larsrh \$ isabellectl --version devel:isabelle-mirror --verbose build # works now
10:50 larsrh (not in the published version though)
10:53 chindy pruvisto: I am confused, why does argmax in the dev version return 'a not 'a set?
10:56 pruvisto it probably involves choice
10:58 pruvisto but you're right, we should probably have a set version as well
10:58 pruvisto and maybe derive the choice-based one from that
10:58 int-e hmm, arg_max f P = (SOME x. is_arg_max f P x) ... you can use {x. is_arg_max f P x} to get a set, but then it could still be empty
10:58 pruvisto shouldn't be too hard
10:58 int-e If I'm looking in the right place
10:58 pruvisto it should be very easy to show that an arg_min/arg_max always exists
10:59 pruvisto I'll bring it up with Tobias
10:59 chindy thanks
10:59 pruvisto maybe we can still improve the situation before the next release
10:59 chindy that would be great!
10:59 pruvisto he needed arg_min for a formalisation of treapss
10:59 pruvisto *treaps
10:59 pruvisto and there the choice was always unique
10:59 pruvisto that's why he simply used choice
11:03 larsrh must ... resist ... joke
11:04 pruvisto ?
11:05 int-e there's always a choice
11:05 int-e anyway, something in that direction, I'd assume
11:06 silver joined #isabelle
11:21 chindy Is it possible to have operators for functions that take 1 arguemtn? so soemthing like [_] ...
11:24 int-e . o O ( fun f :: "nat ⇒ nat" ("[_] ...") where "f x = 23*x + 42" value "[1] ..." )
11:25 pruvisto you can define all kinds of syntax
11:26 pruvisto but it should be used sparingly
11:26 int-e it's a good idea to stay away from syntax that already exists though (the example produces an ambiguous parse tree despite the ...; using [_] would collide with single element lists)
11:26 int-e [_] with a subscript might actually be fine.
11:29 chindy Well i have a function U :: 'i => 'a => 'x and i want to make the first argument subscript so Ui x
11:31 int-e that's probably not a good idea (tokenizing aside, it'll be extremely ugly if i ever is more than a single character)
11:34 pruvisto yes, subscripts are poorly supported by jedit
11:35 pruvisto i used ≤[R] as syntax in social choice theory
13:41 deep-book-gk_ joined #isabelle
13:43 deep-book-gk_ left #isabelle
14:07 wagle joined #isabelle
14:31 chindy Is there a way to do set comprehension in a way like such:  {x ∙ Const . x ∈ S}
14:37 int-e there's the general {f x y |x y. P x y}
14:37 int-e so in your case, just replace . by |x.
14:38 int-e (I don't know what the canonical spacing for this is)
19:06 larsrh pruvisto: "proposition blichfeldt" o.O
19:06 larsrh whwo uses proposition?!
19:07 larsrh *who
19:37 pruvisto larsrh: Larry.
19:37 pruvisto And now I, apparently.
20:44 Merv_ joined #isabelle
22:02 silver_ joined #isabelle
23:53 silver__ joined #isabelle