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 caseof 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 datastructures and algorithms, which are represented as tuples (or singleconstructor 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. 