[isabelle-dev] simplifier and subgoaler not transitive

[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 ♯ (?x1.1, ?x2.1) ≡ True
 > 
 > Where does this rewrite rule come from? Its name suggests it was created during
 > the simp process, but there is no indication of that.
 > 
 > >  [1]Trying to rewrite:
 > > atom v ♯ x1 ⟹ atom v ♯ t ⟹ atom v ♯ (x1, x2) ≡ True
 > 
 > This should be an instance of the above rule, but it is not, there is a funny t.
 > I have no idea where that comes from. I'm confused.

Sorry, this was because of my postediting of the trace.
It should be a x2. Not sure whether this improves things.

Christian