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 multivalued 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:isabellemirror 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 choicebased one from that 
10:58 
inte 
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 
inte 
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 
inte 
there's always a choice 
11:05 
inte 
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 
inte 
. 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 
inte 
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 
inte 
[_] 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 
inte 
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 

deepbookgk_ joined #isabelle 
13:43 

deepbookgk_ 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 
inte 
there's the general {f x y x y. P x y} 
14:37 
inte 
so in your case, just replace . by x. 
14:38 
inte 
(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 