[isabelle-dev] simplifier and subgoaler not transitive

2012-05-22 Thread Christian Urban
Dear All, Assuming that this is about the bowels of the simplifier, I hope this is the right place to ask the following question. The simplifier has a subgoaler, which helps with rewriting conditional lemmas. This simplifiying/subgoaling process seems to be not transitive (probably is not

Re: [isabelle-dev] simplifier and subgoaler not transitive

2012-05-22 Thread Tobias Nipkow
Am 22/05/2012 18:23, schrieb Christian Urban: Dear All, Assuming that this is about the bowels of the simplifier, I hope this is the right place to ask the following question. The simplifier has a subgoaler, which helps with rewriting conditional lemmas. This simplifiying/subgoaling

Re: [isabelle-dev] simplifier and subgoaler not transitive

2012-05-22 Thread Christian Urban
On Tuesday, May 22, 2012 at 20:59:28 (+0200), Tobias Nipkow wrote: but am at least as confused as you are: [1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM: atom v ♯ (x1, x2) ⟹ atom v ♯ x1 [1]Applying instance of rewrite rule ??.unknown: ?a1 ♯ ?x1.1 ⟹ ?a1 ♯ ?x2.1 ⟹ ?a1 ♯

Re: [isabelle-dev] simplifier and subgoaler not transitive

2012-05-22 Thread Thomas Sewell
Question: it looks to me like (atom v # (x, y)) = (atom v # x atom v # y) It also looks like what you're trying to do is allow the system to reason with the above equality without actually giving it that equality. It looks like you've provided the equality in one direction as a rewrite rule

[isabelle-dev] simplifier trace (and jedit)

2012-05-22 Thread Christian Sternagel
Dear all, I wanted to write this already a long time ago (prompted by an Isabelle course I gave) but somehow forgot about it. Now I had a look at my slides again and was reminded. 1) The first thing is rather subjective, but maybe you could comment on it. I think the simplifier trace would

Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-22 Thread Thomas Sewell
The _2 v.s. (2) thing is just silly. It's in find_theorems output too. It's just the way theorems get their names - probably one of these decisions made years ago and not compatible with Makarius' decisions about how to fetch theorems in Isar. Adding context information to every reduction