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 