On 08/23/2010 12:30 PM, Thomas Sewell wrote:
Hello again isabelle-dev.
I should clear up some confusion that may have been caused by my mail. I was
trying to avoid repeating all that had been said on this issue, and it seems I
left out some that hadn't been said as well.
This approach avoids
On Tue, 24 Aug 2010, Andreas Schropp wrote:
Naive questions:
* why is inspecting the whole context infeasible?
* why can't we just collect (and cache?) the Frees occuring in assumptions
managed
by assumption.ML and never delete equalities involving them?
Assumptions belong to the
On 08/24/2010 06:35 PM, Makarius wrote:
On Tue, 24 Aug 2010, Andreas Schropp wrote:
Naive questions:
* why is inspecting the whole context infeasible?
* why can't we just collect (and cache?) the Frees occuring in
assumptions managed
by assumption.ML and never delete equalities
Hi Thomas,
Thomas Sewell wrote:
I should clear up some confusion that may have been caused by my
mail. I was trying to avoid repeating all that had been said on this
issue, and it seems I left out some that hadn't been said as well.
This approach avoids ever deleting an equality on a Free
Andreas Schropp wrote:
On 08/24/2010 06:35 PM, Makarius wrote:
Just like global types/consts/defs, local fixes/assumes merely
generate an infinite collection of consequences. The latter is what
you are working with conceptually, but it is not practical. So the
system provides further slots
On 08/24/2010 07:51 PM, Alexander Krauss wrote:
Andreas Schropp wrote:
On 08/24/2010 06:35 PM, Makarius wrote:
Just like global types/consts/defs, local fixes/assumes merely
generate an infinite collection of consequences. The latter is what
you are working with conceptually, but it is not
On 08/24/2010 09:13 PM, Andreas Schropp wrote:
On 08/24/2010 07:51 PM, Alexander Krauss wrote:
lemma fixes x shows A x == B x
apply method
and
lemma fixes x
assumes a: A x
shows B x
apply (insert a)
apply method
Safe or not, this is obviously undesirable.
BTW: if you want to be even
On 08/24/2010 10:51 PM, Makarius wrote:
On Tue, 24 Aug 2010, Andreas Schropp wrote:
And actually any tactic can peek at the assumptions, via examination
of the hyps of the goal-state
A tactic must never peek at the hyps field of the goal state, and it
must never peek at the main goal being
It's interesting that my innocent thread on hypothesis substitution has been
hijacked into a discussion about context-aware coding guidelines. I'm trying to
steer clear of contexts - it would seem more elegant to me if there was a
purely tactical solution to this problem.
To answer Andreas'
