Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-01-08

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

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/
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 int-e just curious, is induction on length a + length b + length c + length d too tedious for some reason?
23:31 larsrh int-e: it would probably be possible, but tedious because you'd end up doing a big case distinction over which summand increased
23:32 int-e 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.

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary