# IRC log for #isabelle, 2016-12-01

All times shown according to UTC.

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/
10:28 logicmoo joined #isabelle
10:29 silver joined #isabelle
12:04 dmiles joined #isabelle
15:07 JCaesar Hm. I have n sets. Can I get a set (of sets) representing all possible ways to take out one element from each set?
15:07 JCaesar like… {{f, g, …} | f ∈ F, g ∈ G, …}
15:18 larsrh definition "foo S = (λf. (λs. s - {f s}) ` S) ` Pi S id"
15:19 larsrh does that look like something you want?
17:05 ThreeOfEight larsrh: so the input is a set of sets in that case?
17:05 ThreeOfEight that means the n sets in the input need to be distinct
17:06 ThreeOfEight JCaesar: how are these n sets given? As a list? As a set? As a function?
17:08 JCaesar as a list, yeah…
17:08 JCaesar and looking at lars definition, I dhink I'll try to somehow sneak around this…
17:09 ThreeOfEight this is basically "sequence" in the set monad
17:11 ThreeOfEight (more or less)
17:16 ThreeOfEight definition foo where "foo = foldl (λA B. Set.bind B (λx. insert x ` A)) {{}}"
17:16 ThreeOfEight value "foo [{1,2,3}, {4,5,6}, {7,8::int}]"
17:16 ThreeOfEight This seems to do what you want
17:45 JCaesar find_theorems "set (foldl _ _ _)" has nothing and I do need a set afterwards. And I think I've got a better idea. I'll come back with it in a while…
18:18 ThreeOfEight well, of course, you'll have to do induction
18:18 ThreeOfEight also, my command already returns a set, not a list
18:19 ThreeOfEight so calling "set" on it makes no sense