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 
inte 
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 
inte: 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 
inte 
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 
inte 
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 
inte 
(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 
inte 
I had worked around it by instantiating the predicates manually 
14:31 
inte 
but it wasn't pretty 