# IRC log for #isabelle, 2017-02-17

All times shown according to UTC.

Time Nick Message
01:08 stoopkid joined #isabelle
02:48 ilbot3 joined #isabelle
02: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/
04:42 deepbook5broo joined #isabelle
04:42 deepbook5broo left #isabelle
08:28 silver joined #isabelle
13:37 ammbauer joined #isabelle
14:08 ski joined #isabelle
21:48 aneas joined #isabelle
22:01 aneas hi, I'm very new to isabelle and quite often have the following problem: i have a function "foo" of type "a \times b => something" where "foo (x,y) = ...", and want to prove a lemma like "!!z. P (foo z)". since z is used as an argument to foo, isabelle correctly infers the type z::"a \times b", as can be seen in the proof state. however, in order to replace the call to foo by its definition, I always need to do an "apply (induct z)"
22:01 aneas first, followed by "apply auto". is this normal? am i doing something completely wrong? sometimes, the induction can't even figure out an induct rule...
22:02 aneas maybe i should never write "foo z" in the first place, and use "foo (x,y)" instead?
22:29 pruvisto aneas: first of all, if you can avoid it, don't tuple your arguments in the first place
22:30 pruvisto and secondly, you can prove an alternative definition of that function using "case" or a lambda
22:30 pruvisto e.g. "foo z = (case z of (x, y) ⇒ ...)" or "foo = (λ(x,y). ...)"
22:30 pruvisto and then unfold that
22:30 pruvisto the simp rule case_prod_unfold may also help then
22:31 pruvisto also note you can also do "cases z" instead of "induct z", but that doesn't really make a difference
22:31 pruvisto But I really recommend avoiding tuples whenever you can
22:31 pruvisto it makes things messy
22:35 aneas pruvisto, thank you! I never thought of using case-of and lambda for this. I agree with trying to avoid tuples. It's just that I'm trying to use isabelle to proof aspects of some data-structures and algorithms, which are represented as tuples (or single-constructor datatypes)
22:35 aneas I'll look into all your suggestions, thanks again!
23:12 JCaesar aneas: also, apply(simp split: xy.splits) is often helpful in a situation with case asdf of …
23:13 JCaesar where xy gets substituted with prod in case asdf is a product.