# IRC log for #isabelle, 2016-08-08

All times shown according to UTC.

Time Nick Message
01:47 ilbot3 joined #isabelle
01: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:51 stoopkid joined #isabelle
11:00 st0opkid joined #isabelle
11:40 silver joined #isabelle
13:43 int-e is there a clever trick for combining [ P1 ... Pn ]  ==> Q and [ P1 ... Pn ] ==> R into [ P1 ... Pn ] ==> Q & R?, without restating all the premises? (concretely I want to do that with the induction schemes for two mutually recursive functions)
13:58 ThreeOfEight int-e: conjI[OF … …] ?
13:58 ThreeOfEight oh
13:59 ThreeOfEight you have the same premises every time
13:59 ThreeOfEight then I don't think so
13:59 ThreeOfEight I guess one could introduce something like a "distinct_prems" attribute
14:15 silver_ joined #isabelle
14:20 int-e ThreeOfEight: I just learned that the induct tactic can work on several goals simultaneously, and that circumvents the issue.
14:21 ThreeOfEight I wasn't aware of that either
14:21 ThreeOfEight how does that work?
14:22 int-e apply (induct xs ys and xs xs' y ys taking: nss rule: mult2_impl'_mult2_impl_aux'.induct) <-- basically you can have two variable lists separated by "and".
14:22 int-e (or more, I suppose)
14:30 larsrh In fact you should do that if you're doing mutual recursion
14:30 larsrh otherwise most of the time the proofs won't work
14:31 larsrh 'fun' and 'inductive' should also spit out combined induction rules
14:31 int-e I had worked around it by instantiating the predicates manually
14:31 int-e but it wasn't pretty