Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
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 using that. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
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 configuration option and its attribute, and the alternate proof method that has it already enabled. For me it does make sense, i.e. we don't need to make it explicitly legacy in the wording. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
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 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 configuration option and its attribute, and the alternate proof method that has it already enabled. For me it does make sense, i.e. we don't need to make it explicitly legacy in the wording. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
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 forgot the name of the newest release. Long version: The confusion was caused in part because the newest l4.verified branch is called '2013-1'. It contains Isabelle 2013-2, but the switch was accomplished so straightforwardly that we didn't end up with a new branch name. Apologies about the confusion, Thomas. On 16/01/14 02:00, Makarius wrote: 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 using that. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
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 proof script can be repaired by adding the line using [[ hypsubst_thin = true ]] before any apply/by line. That's perfect. I understand why Tjark and Larry would prefer a minimal change, using contextual information to decide when to deviate from the old behaviour. It would certainly create less maintenance work. Let me elaborate why this approach is my first preference: [...] 2) Having the behaviour of tactics change because of largely invisible background concerns seems a recipe for confusion. This particularly applies to building-block tactics such as safe and clarify. I would prefer they be predictable and reliable. Yes. While I agree with Tjark in principle, it appears to me that the syntactic conditions you described are weird enough (even though they make sense upon reflection) that they would confuse users, possibly even those who have been following this thread. Regards, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
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 2014, at 13:43, Thomas Sewell thomas.sew...@nicta.com.au wrote: For those reasons I'd prefer to plough ahead as long as the impact is manageable. I'll test the AFP and ISABELLE_FULL_TEST soon. I'm running out of energy for this side project, however. If there is some collection of proofs that are especially bad, we can just declare [[ hypsubst_thin = true ]] globally in them, but I hope to avoid that for the same reason as (2) above: having invisible adjustments to standard tactics seems like something we should avoid. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
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 hypothesis may, however, be unsafe, since there may be facts about x at the proof or locale level that now cannot be used. It may also be unsafe in the subtle case where a schematic variable in the goal can be instantiated to functions of x but not of Suc a. This unsafeness is undesirable because hypsubst is called from tactics that are meant to be safe. I will freely admit my ignorance of the issues involved, but perhaps it would be desirable to identify these unsafe situations in the code and discard the hypothesis if (and only if) doing so is safe? Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
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 examples (30K), however, is a bit longer (100 changes) and a bit more unpleasant. I've also checked the change against one chunk of L4.verified, with 70K lines in it, and have around 60 lines of changes to make. From my perspective, this level of impact seems to be annoying but not too annoying. I'm interested in what others think. Your suggested change looks very reasonable to me. However, if possible, it would be nice if the old behavior could be kept via a flag -- unless it's easy to simulate reliably (e.g. using thin_rl). One reason for my concern is that the new (co)datatype package's tactics rely extensively on hyp_subst_tac and we currently don't have enough tests in the repository to catch all failures. Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
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 change to hypsubst! (Having thought of doing this patch myself several times, not knowing about the older discussion on this list ;) ) -- Peter All comments welcome, Thomas. The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
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 be the best solution. But if this contextual information is not available, then I think that some sort of compatibility mode will unfortunately be necessary, given the number of instances where introducing the safe behaviour causes proofs to fail. I have to say, in most cases these are tricky proofs that refer to specific assumptions, but lots of these still exist. Larry On 13 Jan 2014, at 12:50, Tjark Weber webe...@in.tum.de wrote: I will freely admit my ignorance of the issues involved, but perhaps it would be desirable to identify these unsafe situations in the code and discard the hypothesis if (and only if) doing so is safe? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
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 very much indeed for taking up this matter again, because I do believe it is important. Larry On 13 Jan 2014, at 12:38, Thomas Sewell thomas.sew...@nicta.com.au wrote: 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. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
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 localization of hypsubst, in the sense that it does not make implicit assumptions how free variables got introduced, their scope etc. In ancient times, a Free was fixed in the immediate scape of the goal state, but that is long past. the current treatment of contexts may make this information available after all. That is a very old topic, and there are various ideas in some drawer that have accumulated a lot of dust. It could easily take a few more years to revisit that. It somehow belongs to the national debts problem from 2006. Since December 2013, I am again improving the situation concerning the formal proof context within proof tools, notably the Simplifier and its add-ons. It is always surprising how long really tiny steps take, e.g. see current Isabelle/f26a7f06266d. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
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 wrote: With an easy escape, i.e. the alternate name of the proof method and a confifuration option to recover the old behaviour, users should manage to convert their old stuff reasonably well. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
