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/ 
02:02 

ertes joined #isabelle 
05:35 

cmr joined #isabelle 
05:35 

cmr joined #isabelle 
05:53 

cmr joined #isabelle 
05:53 

cmr joined #isabelle 
06:00 

cmr joined #isabelle 
06:00 

cmr joined #isabelle 
06:11 

cmr joined #isabelle 
06:11 

cmr joined #isabelle 
09:56 
larsrh 
I should stop being so unreasonably irked by failing builds 
10:07 

silver joined #isabelle 
10:17 
pruvisto 
larsrh: you should 
10:17 
pruvisto 
I would have fixed Random_BSTs soonish 
10:18 
pruvisto 
but I'm working on my long term project "Do more work during working hours, do less work during free time" 
10:24 
larsrh 
Let's say I have a relation {(a1, a2). ∃junk1 x xs. a1 = (junk1, xs) ∧ a2 = (junk1, x # xs)} 
10:25 
larsrh 
is it true that there is an injective f s.t. R = map_prod f f ` {(a1, a2). ∃x xs. a1 = xs ∧ a2 = x # xs} 
10:25 
larsrh 
I feel like this is true but I can't seem to get a hold of _the_ "junk1" 
10:26 
larsrh 
wait, no. This is wrong. 
10:27 
larsrh 
R contains all possible junks, so there's no single one 
10:27 
larsrh 
R is more of a union of {(a1, a2). ∃x xs. a1 = xs ∧ a2 = x # xs} joined with all possible junks 
10:27 
larsrh 
To phrase it differently. I know that R' = {(a1, a2). ∃x xs. a1 = xs ∧ a2 = x # xs} is wf. I want to prove that R is wf as well 
10:31 
inte 
R is the lexicographic product of = and R'. 
10:32 
inte 
(err, the empty relation, not =) 
10:34 
larsrh 
inte: how can I express that in Isabelle? 
10:34 
inte 
lemma "{(a1, a2). ∃junk1 x xs. a1 = (junk1, xs) ∧ a2 = (junk1, x # xs)} = {} <*lex*> {(xs, x # xs)x xs. True}" by auto 
10:35 
inte 
(is there a better way to write "{(xs, x # xs)x xs. True}"? The "True" is a bit awkward) 
10:37 
larsrh 
splendid 
10:37 
larsrh 
this looks highly relevant 
10:39 
larsrh 
now the only problem I have left is that R is tupled in slightly the wrong way 
10:39 
larsrh 
it's more like (junk1, (junk2, x)) instead of ((junk1, junk2), x) 
10:40 
inte 
so use the same trick twice? 
10:40 
larsrh 
but this can be solved by giving an injective f that maps it the right way 
10:40 
larsrh 
or that 
10:43 
larsrh 
wooo, that actually works 
10:58 
larsrh 
inte: you have just secured yourself a spot in the acknowledgements of my thesis 
11:20 
inte 
. o O ( uhoh ) 
11:25 
JCaesar 
Because you helped with lars' junk. 
11:29 
pruvisto 
inte: inte I can't think of a better way to write that really 
11:29 
pruvisto 
this sort of thing can sometimes be expressed nicely with the dependent sum operator (SIGMA) 
11:29 
pruvisto 
but you can't get rid of the "True" that way, I think 
11:35 
inte 
it's a small price to pay to get rid of the existential quantifiers anyway 
11:37 
larsrh 
the existential quantifiers come from the function package 
11:37 
larsrh 
little I can do about them 
11:39 
larsrh 
*walk into the function package like* ᕕ( ᐛ )ᕗ 
11:39 
larsrh 
(* FIXME: broken by design *) 
11:39 
larsrh 
(ಠ_ಠ) 
13:02 

tautologico joined #isabelle 
14:32 
larsrh 
ok so the good news is that I have narrowed down the spot in the function package where f_rel is defined 
14:32 
larsrh 
the bad news is that if I change that all hell breaks loose 
17:30 
chindy 
I have a proof with a general outline of this http://downthetypehole.de/paste/YHkbP5an I know that f1 is true and i can obtain y. but using those why cant i derive false ? 
17:33 
larsrh 
chindy: you need "False" in upper case 
18:11 
chindy 
:P i have that... i figured modus ponens or sth like that would suffice 
18:13 

ertesx joined #isabelle 