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 meant
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/subgoal
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 ⟹
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
ru
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 b
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 soun
