On Tue, 14 Jan 2014, Thomas Sewell wrote:
This is also a patch against Isabelle2013-1.
Is that just a typo, or are you still using that failed release? The
current one is Isabelle2013-2, and it does not introduce any
incompatibilities over Isabelle2013-1, so there is no reason to keep
On Tue, 14 Jan 2014, Thomas Sewell wrote:
If there is some collection of proofs that are especially bad, we can
just declare [[ hypsubst_thin = true ]]
Larry, you are the original author of hypsubst.
Does the hypsubst_thin terminology make sense to you? It is used here
both for the
The name makes sense: thin refers to deleting the assumption.
It is ugly of course, which will be an incentive for users to update their
proofs.
Larry
On 15 Jan 2014, at 15:05, Makarius makar...@sketis.net wrote:
On Tue, 14 Jan 2014, Thomas Sewell wrote:
If there is some collection of
Whoops.
It's both a typo and use of the wrong release.
The patch happens to work against Isabelle2013-1 or Isabelle2013-2,
since there are no relevant differences in the theory sources. I can
confirm that isabelle build -a works in either 2013-1 or 2013-2.
Short version of the story, I
Hi Thomas,
Am 14.01.2014 um 14:43 schrieb Thomas Sewell thomas.sew...@nicta.com.au:
To address Jasmin and Larry's concern, it is possible to switch back to the
compatibility mode by setting a config variable in the context, or by
calling the ML version with an extra parameter. Any legacy
This sounds great! You seem to have done everything right.
Having the compatibility mode will make it easy to get everything working again
quickly, with the conversion to the new setup becoming a background task
(possibly to be combined with refactoring horrible old proofs).
Larry
On 14 Jan
On Mon, 2014-01-13 at 12:38 +, Thomas Sewell wrote:
Given a hypothesis of the form x = Suc a or Suc a = x, where x is a
free (blue) variable, hypsubst will substitute Suc a for x throughout
the goal, and then discard the hypothesis. The substitution is almost
always wanted. Discarding the
Hi Thomas,
Am 13.01.2014 um 13:38 schrieb Thomas Sewell thomas.sew...@nicta.com.au:
The change requires, for instance, about a dozen lines of changes to the
files in HOL/Library, which contain about 50K lines of proof, or 3 lines of
changes to HOL/Bali, with 30K. The change to the Nominal
If there's interest in getting this change installed, I'll slog through
these, and then figure out what's broken and what's expected to be broken in
the latest tip of Isabelle and in the AFP. I'd call for volunteers to help
with that bit though.
I would very much appreciate such a
I think the problem is that the unsafe situations cannot be detected locally,
i.e., there is no way for the tactic to know that a particular free variable is
actually a locale constant. I could be wrong: the current treatment of contexts
may make this information available after all. That would
I’m impressed with your determination to slog through so many changes, but I am
not sure that we have the right to impose this on our users, which is why I
would prefer one of the other solutions, namely (1) contextual information if
available (2) some sort of compatibility mode.
Thank you
On Mon, 13 Jan 2014, Lawrence Paulson wrote:
I think the problem is that the unsafe situations cannot be detected
locally, i.e., there is no way for the tactic to know that a particular
free variable is actually a locale constant.
Indeed. The proposed change is basically some form of
Note that this change would affect auto, force, fast, etc.
Possibly a “legacy” version of auto would help with compatibility, or otherwise
some sort of option setting to (locally) restore the old behaviour in all
affected methods.
Larry
On 13 Jan 2014, at 15:47, Makarius makar...@sketis.net
This sounds logical. But what about auto? Like the other three, it is used to
perform obvious steps in a proof, and it is not terminal.
Larry
On 1 Sep 2010, at 14:17, Thomas Sewell wrote:
Let me try to explain the difference from the perspective of a user. There
are three classical tools
I always intended auto to be initial rather than terminal. I'm not aware of the
unsafe mode you refer to, but it may have been introduced later.
Larry
On 1 Sep 2010, at 14:40, Thomas Sewell wrote:
Good point - I think of auto as terminal. My understanding was that auto had
both a safe and
Thanks for looking into this problem, which has been around in one way or
another from the very beginning.
Lost in all the technical discussions is the question of what the user will
see. We have the option of leaving blast and force as they are now to minimise
danger of incompatibility,
Hi Thomas,
Thomas Sewell wrote:
It's interesting that my innocent thread on hypothesis substitution
has been hijacked into a discussion about context-aware coding
guidelines.
There is still hope if we move the unrelated discussions to another
thread...
I have another small comment on the
Let's try to answer everyone again:
Alex:
I think I was wrong about the cases involving algebra. There may be something
interesting going on. The prenormalisation phase calls clarify_tac, then
full_atomize_tac, then some other stuff. With a Free variable x assumed to be
even, the resulting
On Wed, 25 Aug 2010, Thomas Sewell wrote:
Finally, the change to inspect_pair is indeed just a bugfix. I don't
this check is needed for the simplifier driven version of hyp_subst
anyway, so the bug shouldn't often be seen.
Often it is hard to tell what is a bug or an obscure feature required
I'm pretty sure this one is a bug. Try typing this into your favourite
Isabelle session:
lemma foo:
fwrap f = (%v. f v) == P f
apply clarify
And note the system hangs. I think this is a pretty good argument to
support the case that it doesn't occur in any existing Isabelle scripts.
Just
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'
As previously discussed in the thread Safe for boolean equality, the
current strategy for using equality hypotheses 'x = expr', in which
substitution for x is done and then the hypothesis is discarded, is
unsafe. The conclusion of that discussion was that the problem was
annoying but fairly
Hi Thomas,
Thanks for digging into this. The concrete patch is exactly what was
needed to advance this discussion. Here are a few comments. I am sure
others will have more...
I attach the resulting patch. After
several rounds of bugfixes and compatibility improvements, it requires
23 lines
as returned by Logic.strip_assums_hyp, which it gets right.
Yours,
Thomas.
From: Alexander Krauss [kra...@in.tum.de]
Sent: Monday, August 23, 2010 7:35 PM
To: Thomas Sewell
Cc: Isabelle Developers Mailing List
Subject: Re: [isabelle-dev] Safe approach
32 matches
Mail list logo
