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/ 
18:07 

relrod_ joined #isabelle 
18:07 

relrod_ joined #isabelle 
22:45 
JCaesar 
Is there a rule that would allow me to do induction on multiple list at once? i.e. I have to prove P [] [] [] [] and given P a b c d that P with an element appended to one of its arguments. 
22:46 
JCaesar 
I can construct myself a rule for the argument count I need, but it's a bit messy… 
23:28 
larsrh 
JCaesar: there are list_induct2 etc. variants, but your example looks like a special case to me 
23:28 
inte 
just curious, is induction on length a + length b + length c + length d too tedious for some reason? 
23:31 
larsrh 
inte: it would probably be possible, but tedious because you'd end up doing a big case distinction over which summand increased 
23:32 
inte 
One can also abuse the function package http://sprunge.us/HdHe (the induction scheme is not exactly what you asked though... it's a bit stronger) 
23:32 
JCaesar 
heh. 