[isabelle-dev] simplifier and subgoaler not transitive
christian.urban at kcl.ac.uk
Tue May 22 22:03:24 CEST 2012
On Tuesday, May 22, 2012 at 20:59:28 (+0200), Tobias Nipkow wrote:
> but am at least as confused as you are:
> > SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
> > atom v ♯ (x1, x2) ⟹ atom v ♯ x1
> > 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.
> > 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.
More information about the isabelle-dev