Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2015-12-24

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

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 answer-man 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 meta-logic 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 left-hand side of the equation matches the right-hand 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

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary