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

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

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

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

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

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