On Thursday, May 24, 2012 at 12:14:14 (+1000), Thomas Sewell wrote:
> It looks like you want to implement a simproc.
Thanks a lot for the suggestion. My first "iteration"
was implemented via a solver. It worked. But then,
inspired by the neq-simproc in HOL.thy, I already
modified my code to be
It looks like you want to implement a simproc.
These procedures operate on a family of term patterns and generate
meta-equalities which the simplifier then applies. In this case I think
you want to produce rewrites of the form "a = b == False" and "atom v #
t == True". These rewrites can then
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 th
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
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
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 ⟹
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
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