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

2012-05-23 Thread Christian Urban
I am amazedby you and the simplifier! Yes, indeed one rule in question was added by mksimps. You were spot on. I never knew that they have some more-than-special meaning. ;o) The reason why I prefer to keep the freshness constraints together is that atom a # (x1, x2, x3, x4, x5) would

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

2012-05-23 Thread Makarius
On Tue, 22 May 2012, Christian Urban wrote: Assuming that this is about the bowels of the simplifier, I hope this is the right place to ask the following question. From what I've seen on the thread so far, it is all perfectly normal Isabelle user-space. You did not propose to re-implement

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