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 
inte 
I found out last night when you left: ... by (simp add: nat_distrib) 
09:00 
inte 
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 
inte 
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 
inte 
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 
inte: that makes sense 
09:37 
inte 
I stumbled across nat_distrib. find_theorems (CC CF 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 

inte joined #isabelle 