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
[isabelle-dev] NEWS: More thorough check of proof context
* More thorough check of proof context for goal statements and attributed fact expressions: background theory, declared hyps, declared variable names. Potential INCOMPATIBILITY, tools need to observe standard context discipline. This refers to Isabelle/f26a7f06266d. It is a continuation of the thread by Dmitriy about not always reported errors seen in HOL-BNF https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-November/004833.html and one more step towards fully localized proof tools. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: activation of Z3 via z3_non_commercial system option
* Activation of Z3 now works via z3_non_commercial system option (without requiring restart), instead of former settings variable Z3_NON_COMMERCIAL. The option can be edited in Isabelle/jEdit menu Plugin Options / Isabelle / General. This refers to Isabelle/0c07990363a3. For completeness, the included diff shows the update on the Isabelle component z3-3.2-1, which is relevant for Jasmin when he changes z3 again in the future. The change of z3_non_commercial was already planned for Isabelle2013-2, but did not make it into the release, because I could not make up my mind how much hand-holding the user should get. Right now it is the minimal possible approach to it, without any hand-holding apart from some prose text. I have taken the opportunity to experiment with Pretty.para here: traditionally we have short one-line output that is statically broken, but here the long text might look better with dynamic word-wrapping. The disadvantage is that such output is harder to search formally in log files etc. Makariusdiff -r z3-3.2/etc/settings z3-3.2-1/etc/settings 4,6c4 Z3_HOME=$Z3_COMPONENT/$ISABELLE_PLATFORM # Z3_NON_COMMERCIAL=yes --- Z3_HOME=$Z3_COMPONENT/$ISABELLE_PLATFORM32 Only in z3-3.2/etc: ._settings diff -r z3-3.2/README z3-3.2-1/README 16,19c16,17 Z3_NON_COMMERCIAL=yes in the environment or in $ISABELLE_HOME_USER/etc/settings. --- the Isabelle system option z3_non_commercial to yes (e.g. via the Isabelle/jEdit menu Plugin Options / Isabelle / General). Only in z3-3.2/x86-darwin: z3.dbg ___ 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
