# IRC log for #isabelle, 2012-04-19

All times shown according to UTC.

Time Nick Message
00:01 Kaki joined #isabelle
00:01 Kaki I couldn't solve my problem but i still thank you a lot
00:02 Kaki It's already pretty late here so I#l
00:02 Kaki I'll leave it be and try it again tomorrow
00:02 Kaki Bye
07:47 Kaki joined #isabelle
08:08 Kaki Hello. Is someone able to prove: "((6::nat)*(n + 1)*(n + 1) + n*(n + 1)*(2 * n + 1)) div 6 = ((n + 1)*(6*(n + 1) + n*(2*n + 1))) div 6" ?
09:00 int-e I found out last night when you left: ... by (simp add: nat_distrib)
09:00 int-e in fact: lemma fixes n::nat shows "mySum(n) = n * (n + 1) * (2 * n + 1) div 6" by (induct n, simp_all add: nat_distrib)
09:23 int-e oh, btw, function application needs no parentheses for the argument, you can write  mySum n = ... and define it by  "mySum 0 = 0" | "mySum (Suc n) = Suc n * Suc n + mySum n"
09:24 Kaki im a bit scared of beeing malinterpreted by the system so im using many parentheses
09:26 Kaki now im a bit confused. why isnt simp considering basic equations like nat_distrib?
09:27 Kaki is there a way, that when i import a theory the method simp and such a like include automatically such equations?
09:27 Kaki or is there a way for me to find those?
09:27 Kaki e.g. i dont know how you found nat_distrib
09:32 int-e Kaki: I suppose nat_distrib is excluded because you don't want simple expressions like (a+b)*(c+d)*(e+f)*(g+h) to blow up exponentially when simplifyinh.
09:34 Kaki int-e: that makes sense
09:37 int-e I stumbled across nat_distrib. find_theorems (C-C C-F in emacs) is often helpful, you can look for theorems matching  '"?c * ((?a :: nat) + ?b) = ?c * ?a + ?c * ?b"' or by name,  'name: distrib name: nat'  would find it. (don't type the single quotes)
09:43 Kaki thanks, you made my morning.
09:53 Kaki what was also surprising that even sledgehammering solved that problem
09:53 Kaki but that might be because i think sledgehammering does something else than what i expect it to do
21:09 int-e joined #isabelle