Time 
Nick 
Message 
02:49 

ilbot3 joined #isabelle 
02:49 

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/ 
16:56 

Guest27455 joined #isabelle 
17:07 
IsM 
Newbie to IRC. Thanks to whoever set it up several years ago. ThreeOfEight linked to here recently on the Isabelle user's list. I've been watching this on http://irclog.perlgeek.de/isabelle. The answerman is not in the house; I'm a temp solution. I'll give an answer to yesterday's question, but as a comment to the gist post. It'll take me a while. I'm also a newbie to gist. 
20:03 
ThreeOfEight 
barrucadu: first of all, ∀ and ⋀ are morally the same. 
20:03 
ThreeOfEight 
the latter is part of the metalogic Isabelle pure; the former is part of the object logic HOL 
20:04 
ThreeOfEight 
you can convert one into another, but ⋀ is more easily usable in theorems 
20:04 
ThreeOfEight 
however, ⋀ cannot appear within HOL terms; you can't write something like "(⋀ x. P x) ∨ Q" 
20:05 
ThreeOfEight 
the reason why the second proof in your Gist is more complex is because the lefthand side of the equation matches the righthand side, so the simplifier loops during rewriting. 
20:05 
ThreeOfEight 
(i.e. it rewrites infinitely) 
20:07 
ThreeOfEight 
in fact, this kind of theorem usually requires generalisation, i.e. proving a stronger statement (like your first version of sumtaux_add) first 
20:07 
ThreeOfEight 
I have no idea how metis is able to prove this here 
20:08 
ThreeOfEight 
the reason why the ∀ makes a different is because without it, the value a is fixed during the recursion; you can't plug anything else in for it, which you need to 
20:08 
ThreeOfEight 
if you use a ∀, you can put any value in for a in the inductive step 
20:08 
ThreeOfEight 
(sorry, when I said "recursion", I meant "induction") 
20:09 
ThreeOfEight 
the more idiomatic way would be to write "apply (induct ns arbitrary: a)" and not use an ∀. 
20:09 
ThreeOfEight 
This is explained e.g. in Nipkow's "Concrete Semantics", which you can download for free. 
21:30 

Holistic joined #isabelle 
21:31 
IsM 
I added my comment to your gist, https://gist.github.com/barrucadu/6cf3d1ddaa0b3967ca84 
21:31 
IsM 
Consider it a supplement to 3of8's, the resident answerMan. 
21:33 
IsM 
Tell me if you don't want the clutter, and I'll delete it, or, I assume, you can delete it. As I said, the lesson for me is that binding a variable helped Sledgehammer out. 
22:33 

Holistic joined #isabelle 
23:38 

Holistic joined #isabelle 
23:48 

Holistic joined #isabelle 